cocardinal_aleph0_eq_cofinite

Mathlib.Order.Filter.Cocardinal

URI: https://scilib.ai/kg/mathlib#Filter.cocardinal_aleph0_eq_cofinite

English

If hreg is regular aleph0, then cocardinal α hreg equals cofinite.

Русский

Если hreg является регулярным алфев0, то cocardinal α hreg равно cofinite.

LaTeX

$$cocardinal(α, isRegular_aleph0) = cofinite$$

Lean4

@[simp]
theorem cocardinal_aleph0_eq_cofinite : cocardinal (α := α) isRegular_aleph0 = cofinite := by aesop

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

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

Разделы

Аффилиация

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