cof_eq_cof_toType

Mathlib.SetTheory.Cardinal.Cofinality

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

English

For an ordinal o, cof(o) = cof(o.toType) where toType converts an ordinal into its type.

Русский

Для окрo используя преобразование toType, cof(o) = cof(o.toType).

LaTeX

$$$o.cof = cof(o.toType)$$$

Lean4

theorem cof_eq_cof_toType (o : Ordinal) : o.cof = @Order.cof o.toType (· ≤ ·) := by
  conv_lhs => rw [← type_toType o, cof_type_lt]

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

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

Разделы

Аффилиация

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