le_omega_self

Mathlib.SetTheory.Cardinal.Aleph

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

English

For every ordinal o, o ≤ ω_o.

Русский

Для каждого ординала o выполняется o ≤ ω_o.

LaTeX

$$$ o \le \omega_{o}$$$

Lean4

theorem le_omega_self (o : Ordinal) : o ≤ omega o :=
  omega_strictMono.le_apply

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

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

Разделы

Аффилиация

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