English
If eventually F_i x ∈ s and F_i converges uniformly to f on p, then g∘F_i converges uniformly to g∘f on p, given g is uniformly continuous on s.
Русский
Если для большого i F_i x принадлежит s и F_i сходится равномерно к f на p, то g(F_i) сходится к g(f) равномерно, если g равномерно непрерывна на s.
LaTeX
$$$(\\forall^\\mathrm{f} i \\in p, \\forall x, F_i x \\in s) \\Rightarrow (\\text{...})$$$
Lean4
theorem comp_tendstoUniformly_eventually (hF : ∀ᶠ i in p, ∀ 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
classical
obtain ⟨s', hs', hs⟩ := eventually_iff_exists_mem.mp hF
let F' : ι → α → β := fun i x => if i ∈ s' then F i x else f x
have hF : F =ᶠ[p] F' := by
rw [eventuallyEq_iff_exists_mem]
refine ⟨s', hs', fun y hy => by aesop⟩
have h' : TendstoUniformly F' f p := by rwa [tendstoUniformly_congr hF] at h
apply (tendstoUniformly_congr _).mpr (UniformContinuousOn.comp_tendstoUniformly (by aesop) hf hg h')
rw [eventuallyEq_iff_exists_mem]
refine ⟨s', hs', fun i hi => by aesop⟩
