aleph_limit

Mathlib.SetTheory.Cardinal.Aleph

URI: https://scilib.ai/kg/mathlib#Cardinal.aleph_limit

English

If o is a succLimit, then ℵ_o equals the supremum of ℵ_a for a < o.

Русский

Если o —succLimit, тогда ℵ_o равняется верхней грань ℵ_a по a < o.

LaTeX

$$$$ \aleph_{o} = \bigvee_{a: Iio(o)} \aleph_{a}. $$$$

Lean4

theorem aleph_limit {o : Ordinal} (ho : IsSuccLimit o) : ℵ_ o = ⨆ a : Iio o, ℵ_ a :=
  isNormal_aleph.apply_of_isSuccLimit ho

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru