cof_blsub_le_lift

Mathlib.SetTheory.Cardinal.Cofinality

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

← MathLib Explorer

English

For any o and f on a domain below o, cof(blsub(o,f)) ≤ lift(o.card).

Русский

Для любого o и функции f над доменом ниже o, cof(blsub(o,f)) ≤ lift(o.card).

LaTeX

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

Lean4

theorem cof_blsub_le_lift {o} (f : ∀ a < o, Ordinal) : cof (blsub.{u, v} o f) ≤ Cardinal.lift.{v, u} o.card :=
  by
  rw [← mk_toType o]
  exact cof_lsub_le_lift _

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

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

Разделы

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

Аффилиация

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