Order_Isomorphism_is_Equivalence_Relation
Provedequivalence-relationsorder-isomorphismsproofwiki
Order isomorphism between ordered sets is an equivalence relation: it is reflexive, symmetric, and transitive.
Preamble
import Mathlib.Order.Hom.Basic
Formal statement
theorem Order_Isomorphism_is_Equivalence_Relation {α : Type _} [Preorder α] : Nonempty (α ≃o α) := by sorrySource