tendsto_comp' — Mathlib

English

If a Tendsto φ p F holds and MapClusterPt x p (u ∘ φ), then MapClusterPt x F u.

Русский

Если Tendsto φ p F и MapClusterPt x p (u ∘ φ), то MapClusterPt x F u.

LaTeX

$$$\\operatorname{Tendsto} \\phi p F \\rightarrow \\mathrm{MapClusterPt}(x,p,u\\circ \\phi) \\Rightarrow \\mathrm{MapClusterPt}(x,F,u)$$$

Lean4

theorem tendsto_comp' [TopologicalSpace Y] {f : X → Y} {y : Y} (hf : Tendsto f (𝓝 x ⊓ map u F) (𝓝 y))
    (hu : MapClusterPt x F u) : MapClusterPt y F (f ∘ u) :=
  (tendsto_inf.2 ⟨hf, tendsto_map.mono_left inf_le_right⟩).neBot (hx := hu)

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