English
If F_n tends 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 within s at x.
Русский
Если F_n сходится равномерно к f на множестве s, и g_n стремится к x внутри s, тогда F_n(g_n) стремится к f(x), если f непрерывна внутри s в x.
LaTeX
$$$$\\forall u\\in 𝓤(\\beta),\\ \\forall n\\to p,\\ \\forall x\\in s:\\ (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` 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`. -/
theorem tendsto_comp (h : TendstoUniformlyOn F f p s) (hf : ContinuousWithinAt f s x) (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 => ⟨s, self_mem_nhdsWithin, h u hu⟩
