English
Given the setup of OfCmpEqCmp, the auxiliary lemmas assert properties about how f and g interact with the order.
Русский
В условиях OfCmpEqCmp вспомогательные леммы описывают взаимодействие f и g с порядком.
LaTeX
$$$\text{(auxiliary proofs about } f,g,\, h\text{)}$$$
Lean4
/-- 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`. -/
@[simps! apply]
def ofHomInv {F G : Type*} [FunLike F α β] [OrderHomClass F α β] [FunLike G β α] [OrderHomClass G β α] (f : F) (g : G)
(h₁ : (f : α →o β).comp (g : β →o α) = OrderHom.id) (h₂ : (g : β →o α).comp (f : α →o β) = OrderHom.id) : α ≃o β
where
toFun := f
invFun := g
left_inv := DFunLike.congr_fun h₂
right_inv := DFunLike.congr_fun h₁
map_rel_iff' :=
@fun a b =>
⟨fun h => by
replace h := map_rel g h
rwa [Equiv.coe_fn_mk, show g (f a) = (g : β →o α).comp (f : α →o β) a from rfl,
show g (f b) = (g : β →o α).comp (f : α →o β) b from rfl, h₂] at h,
fun h => (f : α →o β).monotone h⟩
