omega_le_omega

Mathlib.SetTheory.Cardinal.Aleph

URI: https://scilib.ai/kg/mathlib#Ordinal.omega_le_omega

English

For all ordinals o1, o2, the comparison of ω_{o1} and ω_{o2} reflects the order of o1 and o2: ω_{o1} ≤ ω_{o2} iff o1 ≤ o2.

Русский

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

LaTeX

$$$ \omega_{o_1} \le \omega_{o_2} \iff o_1 \le o_2 $$$

Lean4

theorem omega_le_omega {o₁ o₂ : Ordinal} : ω_ o₁ ≤ ω_ o₂ ↔ o₁ ≤ o₂ :=
  omega.le_iff_le

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

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

Разделы

Аффилиация

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