cof_omega_eq

Mathlib.SetTheory.Cardinal.Regular

URI: https://scilib.ai/kg/mathlib#Cardinal.IsRegular.cof_omega_eq

English

If o is an ordinal and H ensures regularity of (ℵ_o), then cof(ω_o) = ℵ_o.

Русский

Если o — ординал и выполняется условие регулярности для (ℵ_o), то cof(ω_o) = ℵ_o.

LaTeX

$$$\mathrm{cof}(\omega_o) = \aleph_o.$$$

Lean4

theorem cof_omega_eq {o : Ordinal} (H : (ℵ_ o).IsRegular) : (ω_ o).cof = ℵ_ o := by rw [← ord_aleph, H.cof_eq]

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

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

Разделы

Аффилиация

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