English
From an order isomorphism e : α ≃o β between frames α and β, there is a Frm isomorphism α ≅ β with hom := ofHom e and inv := ofHom e.symm (the inverse isomorphism).
Русский
Из порядкового изоморфизма e : α ≃o β между рамками α и β существует Frm-изоморфизм α ≅ β с hom := ofHom e и inv := ofHom e.symm.
LaTeX
$$$\exists\phi : \alpha \cong \beta,\; \phi.\mathrm{hom} = \mathrm{ofHom}(e) \land \phi.\mathrm{inv} = \mathrm{ofHom}(e^{\mathrm{symm}}) $$$
Lean4
/-- Constructs an isomorphism of frames from an order isomorphism between them. -/
@[simps]
def mk {α β : Frm.{u}} (e : α ≃o β) : α ≅ β where
hom := ofHom e
inv := ofHom e.symm
