tendsto_comp — Mathlib

English

If f is continuous at x and x has a MapClusterPt x F u, then MapClusterPt (f x) F (f ∘ u).

Русский

Если f непрерывна в точке x и есть MapClusterPt x F u, то MapClusterPt (f x) F (f ∘ u).

LaTeX

$$$\\text{ContinuousAt}(f,x) \\wedge \\mathrm{MapClusterPt}(x,F,u) \\Rightarrow \\mathrm{MapClusterPt}(f(x),F,f\\circ u)$$$

Lean4

theorem tendsto_comp [TopologicalSpace Y] {f : X → Y} {y : Y} (hf : Tendsto f (𝓝 x) (𝓝 y)) (hu : MapClusterPt x F u) :
    MapClusterPt y F (f ∘ u) :=
  hu.tendsto_comp' (hf.mono_left inf_le_left)

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