exists_mapClusterPt_of_frequently

English

If s is compact and f frequently hits s, then there exists x ∈ s with MapClusterPt x f.

Русский

Если s компактно и f часто попадать в s, то существует x ∈ s с MapClusterPt x f.

LaTeX

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

Lean4

theorem exists_mapClusterPt_of_frequently {l : Filter ι} {f : ι → X} (hs : IsCompact s) (hf : ∃ᶠ x in l, f x ∈ s) :
    ∃ a ∈ s, MapClusterPt a l f :=
  hs.exists_clusterPt_of_frequently hf

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