cofinite_inf_principal_neBot_iff — Mathlib

English

For any subset s, the infimum of cofinite and the principal filter of s is nontrivial iff s is infinite.

Русский

Для любого множества s пределы кофинитного фильтра и принципиального фильтра по s не тривиальны тогда, когда s бесконечно.

LaTeX

$$(cofinite ⊓ principal(s)).NeBot \iff s.Infinite$$

Lean4

@[simp]
theorem cofinite_inf_principal_neBot_iff {s : Set α} : (cofinite ⊓ 𝓟 s).NeBot ↔ s.Infinite :=
  frequently_mem_iff_neBot.symm.trans frequently_cofinite_mem_iff_infinite

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