cof_omega0

Mathlib.SetTheory.Cardinal.Cofinality

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

English

Let ω be the first infinite ordinal. Then cof(ω) = ℵ0.

Русский

Пусть ω — первый бесконечный порядковый тип. Тогда cof(ω) = ℵ0.

LaTeX

$$$$ \operatorname{cof}(\omega) = \aleph_0 $$$$

Lean4

@[simp]
theorem cof_omega0 : cof ω = ℵ₀ :=
  (aleph0_le_cof.2 isSuccLimit_omega0).antisymm' <|
    by
    rw [← card_omega0]
    apply cof_le_card

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

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

Разделы

Аффилиация

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