iSup_sequence_lt_omega1 — Mathlib

English

The supremum of a countable sequence of ordinals below ω1 is still below ω1.

Русский

Наибольшая верхняя граница счетной последовательности ordinals, лежащей ниже ω1, остаётся ниже ω1.

LaTeX

$$Let α be countable and o: α → Ordinal with ∀ n, o(n) < ω1. Then iSup o < ω1.$$

Lean4

theorem iSup_sequence_lt_omega1 {α : Type u} [Countable α] (o : α → Ordinal.{max u v}) (ho : ∀ n, o n < (aleph 1).ord) :
    iSup o < (aleph 1).ord := by
  apply iSup_lt_ord_lift _ ho
  rw [Cardinal.isRegular_aleph_one.cof_eq]
  exact lt_of_le_of_lt mk_le_aleph0 aleph0_lt_aleph_one

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