exists_clusterPt_of_frequently — Mathlib

English

If s is compact and l is frequently meeting s (∃ᶠ x ∈ s in l), then there exists a ∈ s which is a cluster point of l.

Русский

Если s компактно и l встречается часто в s, тогда найдется a ∈ s, который является кластерной точкой l.

LaTeX

$$$ \exists a \in s, ClusterPt a l $$$

Lean4

theorem exists_clusterPt_of_frequently {l : Filter X} (hs : IsCompact s) (hl : ∃ᶠ x in l, x ∈ s) :
    ∃ a ∈ s, ClusterPt a l :=
  let ⟨a, has, ha⟩ := @hs _ (frequently_mem_iff_neBot.mp hl) inf_le_right
  ⟨a, has, ha.mono inf_le_left⟩

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