clusterPt_iff_forall_mem_closure — Mathlib

English

Let F be a filter on X. Then x is a cluster point of F if and only if every member s of F has x in its closure, i.e., every neighborhood of x meets s.

Русский

Пусть F — фильтр на X. Тогда x является кластерной точкой F тогда и только тогда, когда каждое множество s ∈ F удовлетворяет x ∈ closure(s), то есть каждая окрестность x пересекает s.

LaTeX

$$$\\mathrm{ClusterPt}(x,F) \\iff \\forall s\\in F,\, x \\in \\overline{s}$$$

Lean4

theorem clusterPt_iff_forall_mem_closure {F : Filter X} : ClusterPt x F ↔ ∀ s ∈ F, x ∈ closure s :=
  F.basis_sets.clusterPt_iff_forall_mem_closure

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