continuousAt_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 и x имеет MapClusterPt x F u, то MapClusterPt (f x) F (f ∘ u).

LaTeX

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

Lean4

theorem continuousAt_comp [TopologicalSpace Y] {f : X → Y} (hf : ContinuousAt f x) (hu : MapClusterPt x F u) :
    MapClusterPt (f x) F (f ∘ u) :=
  hu.tendsto_comp hf

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