tendsto_comp — Mathlib

English

If F_n tends locally uniformly to f, and g_n tends to x, then F_n(g_n) → 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),\\ ∃ t\\in 𝓝(x),\\ ∀^\\infty n,\\ ∀ y\\in t, (f(y),F(n,y))\\in u \\Rightarrow \\ Tendsto(\\lambda n. F(n,g(n)))\\ p\\ (\\mathcal{N}(f(x))). $$$$

Lean4

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

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