enumOrd_surjective — Mathlib

English

If s is not bounded above, then for every b ∈ s there exists a with enumOrd s a = b.

Русский

Если s не ограничено сверху, то для любого b ∈ s существует a такое, что enumOrd s a = b.

LaTeX

$$$$ \\forall b \\in s, \\; \\exists a, \\; \\mathrm{enumOrd}(s)(a) = b $$$$

Lean4

theorem enumOrd_surjective (hs : ¬BddAbove s) {b : Ordinal} (hb : b ∈ s) : ∃ a, enumOrd s a = b := by
  rwa [← range_enumOrd hs] at hb

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