English
If F_n converges locally uniformly on a neighborhood of x to f, and f is continuous at x, and g_n → x, then F_n(g_n) → f(x).
Русский
Если F_n сходится локально равномерно в окрестности x к f, и f непрерывна в x, и g_n → x, то F_n(g_n) → f(x).
LaTeX
$$$$\\forall f:\\ \\alpha \\to \\beta,\\ x\\in \\alpha,\\ p:\\ \\mathcal{F},\\ g:\\ ι \\to \\alpha,\\ h:\\ ContinuousAt(f,x),\\ hg:\\ Tendsto(g,p,\\mathcal{N}(x)),\\ hunif:\\ \\forall u\\in 𝓤(\\beta),\\exists t\\in 𝓝(x),\\forall^\\infty n\\in p,\\ \\forall 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ₙ` converges locally uniformly on a neighborhood of `x` to a function `f` which is
continuous at `x`, and `gₙ` tends to `x`, then `Fₙ (gₙ)` tends to `f x`. -/
theorem tendsto_comp_of_locally_uniform_limit (h : ContinuousAt f x) (hg : Tendsto g p (𝓝 x))
(hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∀ᶠ n in p, ∀ y ∈ t, (f y, F n y) ∈ u) : Tendsto (fun n => F n (g n)) p (𝓝 (f x)) :=
by
rw [← continuousWithinAt_univ] at h
rw [← nhdsWithin_univ] at hunif hg
exact tendsto_comp_of_locally_uniform_limit_within h hg hunif
