aleph0_le_preAleph

Mathlib.SetTheory.Cardinal.Aleph

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

English

ℵ₀ ≤ preAleph(o) ↔ ω ≤ o.

Русский

ℵ₀ ≤ preAleph(o) ⇔ ω ≤ o.

LaTeX

$$$ \aleph_0 \le preAleph(o) \iff \omega \le o $$$

Lean4

@[simp]
theorem aleph0_le_preAleph {o : Ordinal} : ℵ₀ ≤ preAleph o ↔ ω ≤ o := by rw [← preAleph_omega0, preAleph_le_preAleph]

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

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

Разделы

Аффилиация

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