English
If h is locally uniform on s and g is a continuous map with domain, then h.comp g is locally uniform on the image.
Русский
Если h локально равномерна на s и g непрерывна, то h∘g локально равномерна на образе.
LaTeX
$$$$\operatorname{TendstoLocallyUniformlyOn}(F,f,p,s) \Rightarrow \operatorname{TendstoLocallyUniformlyOn}(F\circ g,f\circ g,p,t).$$$$
Lean4
/-- If every `x ∈ s` has a neighbourhood within `s` on which `F i` tends uniformly to `f`, then
`F i` tends locally uniformly on `s` to `f`.
Note this is **not** a tautology, since our definition of `TendstoLocallyUniformlyOn` is slightly
more general (although the conditions are equivalent if `β` is locally compact and `s` is open,
see `tendstoLocallyUniformlyOn_TFAE`). -/
theorem tendstoLocallyUniformlyOn_of_forall_exists_nhds (h : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, TendstoUniformlyOn F f p t) :
TendstoLocallyUniformlyOn F f p s :=
by
refine tendstoLocallyUniformlyOn_iff_forall_tendsto.mpr fun x hx ↦ ?_
obtain ⟨t, ht, htr⟩ := h x hx
rw [tendstoUniformlyOn_iff_tendsto] at htr
exact htr.mono_left <| prod_mono_right _ <| le_principal_iff.mpr ht
