infinite_iff_frequently_cofinite — Mathlib

English

A set s is infinite if and only if it holds frequently in the cofinite filter.

Русский

Множество s бесконечно тогда и только тогда, когда оно часто встречается в кофинитном фильтре.

LaTeX

$$$s \text{ Infinite} \iff (\text{Frequently } (x\in s) \text{ in } \operatorname{cofinite})$$$

Lean4

theorem _root_.Set.infinite_iff_frequently_cofinite {s : Set α} : Set.Infinite s ↔ ∃ᶠ x in cofinite, x ∈ s :=
  frequently_cofinite_iff_infinite.symm

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