English
If F_n tends locally uniformly to f on a set s, and g_n tends to x within s, then F_n(g_n) tends to f(x) provided f is continuous at x within s.
Русский
Если F_n сходится локально равномерно к f на множестве s, и g_n стремится к x внутри s, тогда F_n(g_n) стремится к f(x), если f непрерывна в x относительно s.
LaTeX
$$$$\\text{Let } h: \\, \\text{TendstoLocallyUniformlyOn } F f p s,\\ hf:\\ ContinuousWithinAt(f,s,x),\\ hx: x\\in s,\\ hg:\\ Tendsto(g,p,\\mathcal{N}_s(x)) \\\\Rightarrow\\ Tendsto(\\lambda n. F(n, g(n)))\\ p\\ (\\mathcal{N}(f(x))). $$$$
Lean4
/-- If `Fₙ` tends locally uniformly to `f` on a set `s`, and `gₙ` tends to `x` within `s`, then
`Fₙ gₙ` tends to `f x` if `f` is continuous at `x` within `s` and `x ∈ s`. -/
theorem tendsto_comp (h : TendstoLocallyUniformlyOn F f p s) (hf : ContinuousWithinAt f s x) (hx : x ∈ s)
(hg : Tendsto g p (𝓝[s] x)) : Tendsto (fun n => F n (g n)) p (𝓝 (f x)) :=
tendsto_comp_of_locally_uniform_limit_within hf hg fun u hu => h u hu x hx
