cofinite_neBot — Mathlib

English

On any infinite type α, the cofinite filter is not the bottom filter (it is nontrivial).

Русский

На любом бесконечном множстве α кофинитный фильтр не является нижним (он не тривиален).

LaTeX

$$$\text{Infinite}(\alpha) \Rightarrow \operatorname{cofinite}(\alpha) \neq \bot$$$

Lean4

instance cofinite_neBot [Infinite α] : NeBot (@cofinite α) :=
  hasBasis_cofinite.neBot_iff.2 fun hs => hs.infinite_compl.nonempty

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