isInitialIso — Mathlib

English

Initial ordinals are in natural order isomorphism with cardinals.

Русский

Начальные ординалы образуют упорядоченное изоморфное соответствие кардиналам.

LaTeX

$$$\exists \phi\colon \{x \mid \mathrm{IsInitial}(x)\} \cong_o \mathrm{Cardinal}$$$

Lean4

/-- Initial ordinals are order-isomorphic to the cardinals. -/
@[simps!]
def isInitialIso : { x // IsInitial x } ≃o Cardinal
    where
  toFun x := x.1.card
  invFun x := ⟨x.ord, isInitial_ord _⟩
  left_inv x := Subtype.ext x.2.ord_card
  right_inv x := card_ord x
  map_rel_iff' {a _} := a.2.card_le_card

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