mk — Mathlib · SciLib

English

Construct an isomorphism between partial orders from an order isomorphism between them.

Русский

Построить изоморфизм частичных порядков из изоморфизма порядка между ними.

LaTeX

$$$\alpha \cong \beta$ from $e: \alpha \simeq_o \beta$$$

Lean4

/-- Constructs an equivalence between partial orders from an order isomorphism between them. -/
@[simps]
def mk {α β : PartOrd.{u}} (e : α ≃o β) : α ≅ β where
  hom := ofHom e
  inv := ofHom e.symm

Похожие утверждения