mapClusterPt_iff_frequently — Mathlib

English

If (𝓝 x) has a basis p, s, then MapClusterPt x F u is equivalent to every basis piece having frequently a ∈ F with u a ∈ s_i.

Русский

Если (𝓝 x) имеет базис p, s, то MapClusterPt x F u эквивалентно тому, что для каждого i с p i существует часто встречающееся a в F, такое что u a ∈ s_i.

LaTeX

$$$\\bigl( (\\mathcal{N}x)\\text{ HasBasis } p s \\bigr) \\Rightarrow\\ \\mathrm{MapClusterPt}(x,F,u) \\iff \\forall i, p(i) \\rightarrow \\exists^\\mathrm{freq} a \\in F,\\; u(a) \\in s_i$$$

Lean4

theorem mapClusterPt_iff_frequently {ι : Sort*} {p : ι → Prop} {s : ι → Set X} (hx : (𝓝 x).HasBasis p s) :
    MapClusterPt x F u ↔ ∀ i, p i → ∃ᶠ a in F, u a ∈ s i := by
  simp_rw [MapClusterPt, hx.clusterPt_iff_frequently, frequently_map]

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