English
If g is uniformly continuous on s and F_i → f uniformly (on α) with respect to p, then g∘F_i → g∘f uniformly (on α).
Русский
Если g равномерно непрерывна на s и F_i сходятся равномерно к f на α, то g∘F_i сходится к g∘f равномерно на α.
LaTeX
$$$\\text{UniformContinuousOn } g\\, s \\; \\wedge \\; \\operatorname{TendstoUniformly} F f p \\Rightarrow \\operatorname{TendstoUniformly}(i \\mapsto g(F i)) (g \\circ f) p$$$
Lean4
/-- Composing on the left by a uniformly continuous function preserves uniform convergence -/
theorem comp_tendstoUniformly (hF : ∀ i x, F i x ∈ s) (hf : ∀ x, f x ∈ s) (hg : UniformContinuousOn g s)
(h : TendstoUniformly F f p) : TendstoUniformly (fun i x => g (F i x)) (fun x => g (f x)) p :=
by
rw [uniformContinuousOn_iff_restrict] at hg
lift F to ι → α → s using hF with F' hF'
lift f to α → s using hf with f' hf'
rw [tendstoUniformly_iff_tendsto] at h
have : Tendsto (fun q ↦ (f' q.2, F' q.1 q.2)) (p ×ˢ ⊤) (𝓤 s) :=
h.of_tendsto_comp isUniformEmbedding_subtype_val.comap_uniformity.le
apply UniformContinuous.comp_tendstoUniformly hg ?_
rwa [← tendstoUniformly_iff_tendsto] at this
