exists_mapClusterPt — Mathlib

English

For a compact s and a filter f, if map u f ≤ principal s, there exists x ∈ s with MapClusterPt x f u.

Русский

Для компактного s и фильтра f, если отображение u результирует в связке флаг principal s, существует x ∈ s с MapClusterPt x f u.

LaTeX

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

Lean4

theorem exists_mapClusterPt {ι : Type*} (hs : IsCompact s) {f : Filter ι} [NeBot f] {u : ι → X}
    (hf : Filter.map u f ≤ 𝓟 s) : ∃ x ∈ s, MapClusterPt x f u :=
  hs hf

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