clusterPt_iff_forall_mem_closure — Mathlib

English

Let X be a topological space and F a filter on X with a basis {s_i} defined by p_i. Then x is a cluster point of F if and only if x belongs to the closure of every basis member s_i for which p_i holds.

Русский

Пусть X — топологическое пространство и F — фильтр на X, имеющий базис {s_i} с помощью p_i. Тогда x является кластерной точкой F тогда и только тогда, когда для каждого i с p_i выполняется x ∈ closure(s_i).

LaTeX

$$$\\mathrm{ClusterPt}(x,F) \\iff \\forall i\\, (p(i) \\rightarrow x \\in \\overline{s_i})$$$

Lean4

protected theorem clusterPt_iff_forall_mem_closure {ι} {p : ι → Prop} {s : ι → Set X} {F : Filter X}
    (hF : F.HasBasis p s) : ClusterPt x F ↔ ∀ i, p i → x ∈ closure (s i) :=
  by
  simp only [(nhds_basis_opens _).clusterPt_iff hF, mem_closure_iff]
  tauto

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