lt_omega_iff_card_lt

Mathlib.SetTheory.Cardinal.Aleph

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

English

For any ordinals x and o, x < ω_o if and only if the cardinality of x is less than ℵ_o.

Русский

Для ординалов x и o верно: x < ω_o эквивалентно тому, что кардинал x меньше ℵ_o.

LaTeX

$$$x < \omega_o \ \iff \ |x| < \aleph_o$$$

Lean4

theorem lt_omega_iff_card_lt {x o : Ordinal} : x < ω_ o ↔ x.card < ℵ_ o := by
  rw [← (isInitial_omega o).card_lt_card, card_omega]

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

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

Разделы

Аффилиация

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