omega_zero

Mathlib.SetTheory.Cardinal.Aleph

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

English

The first indexed omega equals the usual omega: ω_0 = ω.

Русский

Первая ω-ин декса равна обычному ω: ω_0 = ω.

LaTeX

$$$ \omega_{0} = \omega $$$

Lean4

@[simp]
theorem omega_zero : ω_ 0 = ω := by rw [omega_eq_preOmega, add_zero, preOmega_omega0]

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

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

Разделы

Аффилиация

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