cofinite_eq

Mathlib.Topology.Instances.Int

URI: https://scilib.ai/kg/mathlib#Int.cofinite_eq

English

The cofinite filter on ℤ equals the supremum of the bottom and top filters.

Русский

Фильтр кофинит на \mathbb{Z} равен верхнему объединению нижнего и верхнего фильтров.

LaTeX

$$$\operatorname{cofinite} = \operatorname{atBot} \sqcup \operatorname{atTop}$$$

Lean4

@[simp]
theorem cofinite_eq : (cofinite : Filter ℤ) = atBot ⊔ atTop := by rw [← cocompact_eq_cofinite, cocompact_eq_atBot_atTop]

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

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

Разделы

Аффилиация

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