cluster_point_of_Lindelof — Mathlib

English

In a Lindelöf space X, for any nontrivial filter f with countable intersection property, there exists a cluster point x with respect to f.

Русский

В Линдельфовом пространстве X для любого не-тривиального фильтра f с свойством счётного пересечения существует кластерная точка x относительно f.

LaTeX

$$$\exists x, \mathrm{ClusterPt}(x,f)$$$

Lean4

theorem cluster_point_of_Lindelof [LindelofSpace X] (f : Filter X) [NeBot f] [CountableInterFilter f] :
    ∃ x, ClusterPt x f := by simpa using isLindelof_univ (show f ≤ 𝓟 univ by simp)

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