Set_Equivalence_is_Equivalence_Relation
Provedequivalence-relationsproofwikiset-equivalence
Set equivalence (existence of a bijection between sets) is an equivalence relation.
Preamble
import Mathlib.Logic.Equiv.Basic
Formal statement
theorem Set_Equivalence_is_Equivalence_Relation : Equivalence (fun (α β : Type _) => Nonempty (α ≃ β)) := by sorry
Source