clusterPt_iff_frequently — Mathlib

English

Let F be a filter and p a predicate; ClusterPt x F is equivalent to frequently along nhds x of the predicate p(y) holding for y in s.

Русский

Пусть F — фильтр и p — предикат; ClusterPt x F эквивалентно тому, что вдоль nhds x часто выполняется предикат p(y) для y в s.

LaTeX

$$$\operatorname{ClusterPt} x F \\iff \\forall s \\in \\mathcal{F}, \\exists^{\\text{frequent}} y \\in F, y \\in s$$$

Lean4

theorem clusterPt_iff_frequently {F : Filter X} : ClusterPt x F ↔ ∀ s ∈ 𝓝 x, ∃ᶠ y in F, y ∈ s :=
  (𝓝 x).basis_sets.clusterPt_iff_frequently

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