preOmega_le_of_forall_lt

Mathlib.SetTheory.Cardinal.Aleph

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

English

If a is initial and for all b < o, preOmega(b) < a, then preOmega(o) ≤ a.

Русский

Если a начальный и для любого b < o верно preOmega(b) < a, то preOmega(o) ≤ a.

LaTeX

$$$\text{IsInitial}(a) \to (\forall b < o,\ preOmega(b) < a) \to preOmega(o) \le a$$$

Lean4

theorem preOmega_le_of_forall_lt {o a : Ordinal} (ha : IsInitial a) (H : ∀ b < o, preOmega b < a) : preOmega o ≤ a :=
  enumOrd_le_of_forall_lt ha H

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

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

Разделы

Аффилиация

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