preAleph_le_of_isSuccPrelimit — Mathlib

English

If o is a successor-prelimit ordinal, preAleph(o) is the supremum of preAleph(a) for a < o.

Русский

Если o — ординал-предпределитель, то preAleph(o) — верхняя грань значений preAleph(a) по a < o.

LaTeX

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

Lean4

theorem preAleph_le_of_isSuccPrelimit {o : Ordinal} (l : IsSuccPrelimit o) {c} :
    preAleph o ≤ c ↔ ∀ o' < o, preAleph o' ≤ c :=
  by
  obtain rfl | ho := eq_or_ne o 0
  · simp
  · exact isNormal_preAleph.le_iff_forall_le ⟨by simpa, l⟩

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