English
If f: F → α and g: G → β are order-homomorphisms with inverses (g ∘ f) = id and (f ∘ g) = id, then f and g form an order isomorphism α ≃o β.
Русский
Если f: F → α и g: G → β являются порядковыми гомоморфизмами с обратными отображениями, удовлетворяющими (g ∘ f)=id и (f ∘ g)=id, то f и g образуют порядковый изоморфизм α ≃o β.
LaTeX
$$$\exists f:G \to α,\; g:β \to α\; \text{ с условиями } (f\circ g)=id, (g\circ f)=id \Rightarrow α \simeq_o β$$$
Lean4
@[simp]
theorem ofHomInv_symm_apply {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) (a : β) : (ofHomInv f g h₁ h₂).symm a = g a :=
rfl
