aleph_lt_aleph

Mathlib.SetTheory.Cardinal.Aleph

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

English

For all ordinals o1, o2, ℵ_{o1} < ℵ_{o2} iff o1 < o2.

Русский

Для любых ординалов o1, o2 выполняется ℵ_{o1} < ℵ_{o2} тогда и только тогда, когда o1 < o2.

LaTeX

$$$$ \aleph_{o_1} < \aleph_{o_2} \iff o_1 < o_2. $$$$

Lean4

theorem aleph_lt_aleph {o₁ o₂ : Ordinal} : ℵ_ o₁ < ℵ_ o₂ ↔ o₁ < o₂ :=
  aleph.lt_iff_lt

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

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

Разделы

Аффилиация

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