clusterPt_iff_frequently — Mathlib

English

Let hx be a nhds x HasBasis pX sX. Then ClusterPt x F holds iff for all i with pX i, the set sX i is frequently hit by F in G.

Русский

Пусть hx — база HasBasis для nhds x: pX i, sX i. Тогда ClusterPt x F эквивалентно тому, что для всех i с pX i множество sX i часто встречается по отношению к F.

LaTeX

$$$\operatorname{ClusterPt} x F \\iff \\forall i, pX i \\to \\operatorname{Frequently}(\\lambda y \\in F, y \\in sX i) F$$$

Lean4

theorem clusterPt_iff_frequently {ι} {p : ι → Prop} {s : ι → Set X} {F : Filter X} (hx : (𝓝 x).HasBasis p s) :
    ClusterPt x F ↔ ∀ i, p i → ∃ᶠ x in F, x ∈ s i := by
  simp only [hx.clusterPt_iff F.basis_sets, Filter.frequently_iff, inter_comm (s _), Set.Nonempty, id, mem_inter_iff]

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