cof_bsup_le

Mathlib.SetTheory.Cardinal.Cofinality

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

← MathLib Explorer

English

If ∀ a < o, f(a) < bsup(o,f), then cof(bsup(o,f)) ≤ o.card.

Русский

Если ∀ a < o, f(a) < bsup(o,f), тогда cof(bsup(o,f)) ≤ o.card.

LaTeX

$$$\\forall o\\,\\forall f:\\, (\\forall a

Lean4

theorem cof_bsup_le {o : Ordinal} {f : ∀ a < o, Ordinal} :
    (∀ i h, f i h < bsup.{u, u} o f) → cof (bsup.{u, u} o f) ≤ o.card :=
  by
  rw [← o.card.lift_id]
  exact cof_bsup_le_lift

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

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

Разделы

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

Аффилиация

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