exists_clusterPt — Mathlib

English

For a compact set s and a filter f, there exists x ∈ s that is a cluster point of f.

Русский

Для компактного множества s и фильтра f существует точка x ∈ s, которая является кластерной точкой фильтра f.

LaTeX

$$$ \exists x \in s, ClusterPt x f $$$

Lean4

theorem exists_clusterPt (hs : IsCompact s) {f : Filter X} [NeBot f] (hf : f ≤ 𝓟 s) : ∃ x ∈ s, ClusterPt x f :=
  hs hf

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