Theorems · Theorem · order theory

OrderIso.ofHomInv_apply

∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β) (g : β →o α)
  (h₁ : f.comp g = OrderHom.id) (h₂ : g.comp f = OrderHom.id) (a : α), (OrderIso.ofHomInv f g h₁ h₂) a = f a

Defined in

Mathlib.Order.Hom.Basic

Cited by

3 results in Mathlib

Foundations

Depth 21 from the axioms · uses Quot.sound

Assumes

PreorderPreorder