tendsto_comp — Mathlib

English

If F_n tends uniformly to f, and g_n tends to x, then F_n(g_n) tends to f(x) provided f is continuous at x.

Русский

Если F_n сходится равномерно к f, и g_n стремится к x, то F_n(g_n) стремится к f(x) при условии непрерывности f в x.

LaTeX

$$$$\\forall u\\in 𝓤(\\beta),\\ \\forall n\\to p,\\ (f(x),F(n,x))\\in u \\Rightarrow \\ Tendsto(\\lambda n. F(n,g(n)))\\ p\\ (\\mathcal{N}(f(x))). $$$$

Lean4

/-- If `Fₙ` tends uniformly to `f`, and `gₙ` tends to `x`, then `Fₙ gₙ` tends to `f x`. -/
theorem tendsto_comp (h : TendstoUniformly F f p) (hf : ContinuousAt f x) (hg : Tendsto g p (𝓝 x)) :
    Tendsto (fun n => F n (g n)) p (𝓝 (f x)) :=
  h.tendstoLocallyUniformly.tendsto_comp hf hg

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