mk — Mathlib · SciLib

English

Let α and β be nonempty finite linear orders and e: α ≃o β an order isomorphism. Then there exists an isomorphism α ≅ β in the category NonemptyFinLinOrd, induced by e.

Русский

Пусть α и β — ненулевые конечные линейные порядки, и e: α ≃o β — упорядоченный изоморфизм. Тогда существует изоморфизм α ≅ β в категории NonemptyFinLinOrd, индуцированный e.

LaTeX

$$$\alpha \cong \beta$$$

Lean4

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

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