le_cofinite_iff_compl_singleton_mem

English

A filter l is below cofinite iff every complement of a singleton belongs to l.

Русский

Фильтр l меньше или равен cofinite тогда и только тогда, когда для каждого элемента x множества {x}ᶜ принадлежит l.

LaTeX

$$$l \le \operatorname{cofinite} \iff \forall x, \{x\}^c \in l$$$

Lean4

theorem le_cofinite_iff_compl_singleton_mem : l ≤ cofinite ↔ ∀ x, { x }ᶜ ∈ l :=
  by
  refine ⟨fun h x => h (finite_singleton x).compl_mem_cofinite, fun h s (hs : sᶜ.Finite) => ?_⟩
  rw [← compl_compl s, ← biUnion_of_singleton sᶜ, compl_iUnion₂, Filter.biInter_mem hs]
  exact fun x _ => h x

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