Trivial_Relation_is_Equivalence
Provedequivalence-relationsproofwikitrivial-relation
The trivial relation R = S x S on a set S is always an equivalence relation on S.
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Trivial_Relation_is_Equivalence {α : Type _} : @Equivalence α (fun _ _ => True) := by sorrySource