omega0_lt_omega1

Mathlib.SetTheory.Cardinal.Aleph

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

English

We have ω_0 < ω_1.

Русский

Мы имеем ω_0 < ω_1.

LaTeX

$$$ \omega_{0} < \omega_{1}$$$

Lean4

theorem omega0_lt_omega1 : ω < ω₁ := by
  rw [← omega_zero, omega_lt_omega]
  exact zero_lt_one

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

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

Разделы

Аффилиация

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