Theorems · Definition · order theory

OrderIso.ofHomInv

{α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → (f : α →o β) → (g : β →o α) → f.comp g = OrderHom.id → g.comp f = OrderHom.id → α ≃o β

To show that f : α →o β and g : β →o α make up an order isomorphism it is enough to show that g is the inverse of f.

Defined in

Mathlib.Order.Hom.Basic

Cited by

3 results in Mathlib

Foundations

Depth 16 from the axioms · uses Quot.sound

Assumes

PreorderPreorder