cofinite

Mathlib.Order.Filter.Cofinite

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

← MathLib Explorer

English

The cofinite filter is the filter of subsets whose complements are finite.

Русский

Кофинитный фильтр — это фильтр подмножеств, дополнения которых конечны.

LaTeX

$$cofinite : Filter α :=$$

Lean4

/-- The cofinite filter is the filter of subsets whose complements are finite. -/
def cofinite : Filter α :=
  comk Set.Finite finite_empty (fun _t ht _s hsub ↦ ht.subset hsub) fun _ h _ ↦ h.union

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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