cof_eq

Mathlib.SetTheory.Cardinal.Cofinality

URI: https://scilib.ai/kg/mathlib#Ordinal.IsNormal.cof_eq

← MathLib Explorer

English

If f is fundamental, then s p hp < a for p below o, i.e., lt-property holds.

Русский

Если f фундаментальна, то для каждого p < o выполняется s p hp < a (свойство lt).

LaTeX

$$$$\forall p

Lean4

theorem cof_eq {f} (hf : IsNormal f) {a} (ha : IsSuccLimit a) : cof (f a) = cof a :=
  let ⟨_, hg⟩ := exists_fundamental_sequence a
  ord_injective (hf.isFundamentalSequence ha hg).cof_eq

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

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

Разделы

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

Аффилиация

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