mapClusterPt_iff_frequently — Mathlib

English

MapClusterPt x F u is equivalent to the condition that for every neighborhood s of x, the set of a with u a ∈ s is frequently realized in F.

Русский

MapClusterPt x F u эквивалентно тому, что для каждого окрестности s x множество a с u a ∈ s встречается часто в F.

LaTeX

$$$\\mathrm{MapClusterPt}(x,F,u) \\iff \\forall s \\in \\mathcal{N}(x),\\; \\exists^\\mathrm{freq} a \\in F,\\; u(a) \\in s$$$

Lean4

theorem mapClusterPt_iff_frequently : MapClusterPt x F u ↔ ∀ s ∈ 𝓝 x, ∃ᶠ a in F, u a ∈ s :=
  (𝓝 x).basis_sets.mapClusterPt_iff_frequently

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