mapClusterPt_iff — Mathlib

English

If f tends to y along nhds x ⊓ map u F and x has a MapClusterPt x F u, then MapClusterPt y F (f ∘ u).

Русский

Если f стремится к y по отношению к nhds x ⊓ map u F и есть MapClusterPt x F u, то MapClusterPt y F (f ∘ u).

LaTeX

$$$(\\operatorname{Tendsto} f (\\mathcal{N}(x) \\cap \\operatorname{map} u F)(\\mathcal{N}(y))) \\wedge \\mathrm{MapClusterPt}(x,F,u) \\Rightarrow \\mathrm{MapClusterPt}(y,F,f\\circ u)$$$

Lean4

theorem mapClusterPt_iff {v : α → X} (h : u =ᶠ[F] v) : MapClusterPt x F u ↔ MapClusterPt x F v := by
  simp only [mapClusterPt_def, map_congr h]

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