aleph_le_aleph

Mathlib.SetTheory.Cardinal.Aleph

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

English

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

Русский

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

LaTeX

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

Lean4

theorem aleph_le_aleph {o₁ o₂ : Ordinal} : ℵ_ o₁ ≤ ℵ_ o₂ ↔ o₁ ≤ o₂ :=
  aleph.le_iff_le

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

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

Разделы

Аффилиация

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