English
From an OrderIso e, the induced Lat.Iso mk yields the corresponding isomorphism between the lattices with the given forward and inverse maps.
Русский
Из OrderIso e получают соответствующий изоморфизм решеток через Lat.Iso.mk с заданными forward и inverse отображениями.
LaTeX
$$$ \alpha \cong \beta \quad\text{via } \mathrm{Iso.mk}(e)\text{ with } \mathrm{hom} = \mathrm{ofHom}(e),\ \mathrm{inv} = \mathrm{ofHom}(e.symm). $$$
Lean4
/-- Constructs an equivalence between linear orders from an order isomorphism between them. -/
@[simps]
def mk {α β : LinOrd.{u}} (e : α ≃o β) : α ≅ β where
hom := ofHom e
inv := ofHom e.symm
