preAleph_limit — Mathlib

English

If o is a succLimit, then preAleph(o) equals the supremum of preAleph(a) over a < o.

Русский

Если o — суффиксный предел, то preAleph(o) равняется верхней грани из {preAleph(a) | a < o}.

LaTeX

$$$$ \forall o:\mathrm{Ordinal}, \mathrm{IsSuccLimit}(o) \rightarrow \operatorname{preAleph}(o) = \bigvee_{a: Iio(o)} \operatorname{preAleph}(a). $$$$

Lean4

theorem preAleph_limit {o : Ordinal} (ho : IsSuccPrelimit o) : preAleph o = ⨆ a : Iio o, preAleph a :=
  by
  obtain rfl | h := eq_or_ne o 0
  · simp
  · exact isNormal_preAleph.apply_of_isSuccLimit ⟨by simpa, ho⟩

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