English
Let F_n: α → β and s ⊆ α, x ∈ α. If F_n converges locally uniformly to f on a neighborhood of x within s, and f is continuous at x within s, and g_n → x within s, then F_n(g_n) → f(x).
Русский
Пусть F_n: α → β, s ⊆ α, x ∈ α. если F_n сходится локально равномерно к f на окрестности x внутри s, и f непрерывна в точке x относительно s, и g_n → x внутри s, тогда F_n(g_n) → f(x).
LaTeX
$$$$\\forall f:\\ \\alpha \\to \\beta,\\ F:\\ \\iota \\to (\\alpha \\to \\beta),\\ s\\subseteq \\alpha,\\ x\\in \\alpha,\\ p:\\ \\mathcal{F},\\ g:\\ \\iota \\to \\alpha,\\ h:\\ ContinuousWithinAt(f,s,x),\\ hg:\\ Tendsto(g,p,\\mathcal{N}_s(x)),\\ hunif:\\ \\forall u\\in 𝓤(\\beta),\\exists t\\in 𝓝_s(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` within a set `s` to a function `f`
which is continuous at `x` within `s`, and `gₙ` tends to `x` within `s`, then `Fₙ (gₙ)` tends
to `f x`. -/
theorem tendsto_comp_of_locally_uniform_limit_within (h : ContinuousWithinAt f s x) (hg : Tendsto g p (𝓝[s] x))
(hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∀ᶠ n in p, ∀ y ∈ t, (f y, F n y) ∈ u) :
Tendsto (fun n => F n (g n)) p (𝓝 (f x)) :=
by
refine Uniform.tendsto_nhds_right.2 fun u₀ hu₀ => ?_
obtain ⟨u₁, h₁, u₁₀⟩ : ∃ u ∈ 𝓤 β, u ○ u ⊆ u₀ := comp_mem_uniformity_sets hu₀
rcases hunif u₁ h₁ with ⟨s, sx, hs⟩
have A : ∀ᶠ n in p, g n ∈ s := hg sx
have B : ∀ᶠ n in p, (f x, f (g n)) ∈ u₁ := hg (Uniform.continuousWithinAt_iff'_right.1 h h₁)
exact B.mp <| A.mp <| hs.mono fun y H1 H2 H3 => u₁₀ (prodMk_mem_compRel H3 (H1 _ H2))
