English
If F is locally uniform on α and you restrict to a subset via composition with g, then the composed map is locally uniform on the subset t.
Русский
Если локально равномерна F на α и ограничение через композицию с g сохраняет область t, то композиция локально равномерна на t.
LaTeX
$$$$\operatorname{TendstoLocallyUniformlyOn}(F,f,p,s) \Rightarrow \operatorname{TendstoLocallyUniformlyOn}(F\circ g, f\circ g, p, t)$$$$
Lean4
theorem comp [TopologicalSpace γ] {t : Set γ} (h : TendstoLocallyUniformlyOn F f p s) (g : γ → α) (hg : MapsTo g t s)
(cg : ContinuousOn g t) : TendstoLocallyUniformlyOn (fun n => F n ∘ g) (f ∘ g) p t :=
by
intro u hu x hx
rcases h u hu (g x) (hg hx) with ⟨a, ha, H⟩
have : g ⁻¹' a ∈ 𝓝[t] x := (cg x hx).preimage_mem_nhdsWithin' (nhdsWithin_mono (g x) hg.image_subset ha)
exact ⟨g ⁻¹' a, this, H.mono fun n hn y hy => hn _ hy⟩
