Inverse_of_Order_Isomorphism_is_Order_Isomorphism
Provedorder-isomorphismsproofwiki
If φ is an order isomorphism from (S, ≤₁) to (T, ≤₂), then there exists an order isomorphism from (T, ≤₂) to (S, ≤₁).
Preamble
import Mathlib.Order.Hom.Basic
Formal statement
theorem Inverse_of_Order_Isomorphism_is_Order_Isomorphism {α : Type _} {β : Type _} [Preorder α] [Preorder β] (φ : α ≃o β) : Nonempty (β ≃o α) := by sorrySource