omega0_lt_ord

Mathlib.SetTheory.Ordinal.Basic

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

English

ω < a.ord iff ℵ₀ < a.

Русский

ω < a.ord эквивалентно ℵ₀ < a.

LaTeX

$$$ \omega < a.\operatorname{ord} \iff \aleph_0 < a $$$

Lean4

@[simp]
theorem omega0_lt_ord {a : Cardinal} : ω < a.ord ↔ ℵ₀ < a :=
  le_iff_le_iff_lt_iff_lt.1 ord_le_omega0

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

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

Разделы

Аффилиация

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