enumOrdOrderIso — Mathlib

English

If s is not bounded above, there exists an order isomorphism between the class of all ordinals and s.

Русский

Пусть s — неограниченное подмножество ординалов. Тогда существует отображение-по-порядку из ординалов в s, то есть полное изоморфизм по порядку.

LaTeX

$$$\exists \phi:\ \mathrm{Ordinal} \cong_o s$$$

Lean4

/-- An order isomorphism between an unbounded set of ordinals and the ordinals. -/
noncomputable def enumOrdOrderIso (s : Set Ordinal) (hs : ¬BddAbove s) : Ordinal ≃o s :=
  StrictMono.orderIsoOfSurjective (fun o => ⟨_, enumOrd_mem hs o⟩) (enumOrd_strictMono hs) fun s =>
    let ⟨a, ha⟩ := enumOrd_surjective hs s.prop
    ⟨a, Subtype.eq ha⟩

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