lsub_lt_ord

Mathlib.SetTheory.Cardinal.Cofinality

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

← MathLib Explorer

English

For any f, cof(lsub(f)) ≤ lift(#ι).

Русский

Для любой f: cof(lsub(f)) ≤ lift(|ι|).

LaTeX

$$$\\operatorname{cof}(\\operatorname{lsub}(f)) \\le \\operatorname{lift}(\\#\\iota).$$$

Lean4

theorem lsub_lt_ord {ι} {f : ι → Ordinal} {c : Ordinal} (hι : #ι < c.cof) : (∀ i, f i < c) → lsub.{u, u} f < c :=
  lsub_lt_ord_lift (by rwa [(#ι).lift_id])

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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