exists_clusterPt_of_compactSpace — Mathlib

English

In a compact space X, every nontrivial filter F on X has a cluster point x ∈ X; i.e., there exists x with ClusterPt x F.

Русский

В компактном пространстве X любый ненулевой фильтр имеет кластерную точку x ∈ X; то есть существует x, удовлетворяющая ClusterPt x F.

LaTeX

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

Lean4

theorem exists_clusterPt_of_compactSpace [CompactSpace X] (f : Filter X) [NeBot f] : ∃ x, ClusterPt x f := by
  simpa using isCompact_univ (show f ≤ 𝓟 univ by simp)

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