English
An order isomorphism e : α ≃o β between bounded orders induces a category isomorphism α ≅ β in BddOrd, with forward map given by ofHom e and inverse by ofHom e.symm; the usual hom_inv_id and inv_hom_id hold.
Русский
Изоморфизм порядков e : α ≃o β между ограниченными порядками порождает изоморфизм α ≅ β в категории BddOrd, где переход вперед задан как.ofHom e, обратный — as.ofHom e.symm; выполняются стандартные равенства обратной композиции.
LaTeX
$$$\alpha \cong \beta \quad \text{in } \mathbf{BddOrd}$$$
Lean4
/-- Constructs an equivalence between bounded orders from an order isomorphism between them. -/
@[simps]
def mk {α β : BddOrd.{u}} (e : α ≃o β) : α ≅ β where
hom := ofHom e
inv := ofHom e.symm
hom_inv_id := by ext; exact e.symm_apply_apply _
inv_hom_id := by ext; exact e.apply_symm_apply _
