English
If a uniform convergence on s holds along l, then for any sequence u: ℕ → ι with hu : Tendsto u atTop l, the transformed sequence F(u(n)) converges uniformly on s to f along atTop.
Русский
Если имеем равномерное сходение на s вдоль l, то для любой последовательности u: ℕ → ι с hu : Tendsto u atTop l последовательность F(u(n)) сходится равномерно на s к f по atTop.
LaTeX
$$$h:\\ TendstoUniformlyOn F f l s \\Rightarrow \\forall u:\\mathbb{N} \\to ι,\\; (hu: \\text{Tendsto } u \\text{ atTop } l) \\Rightarrow \\text{TendstoUniformlyOn } (\\lambda n. F (u n)) f \\text{ atTop } s$$$
Lean4
theorem seq_tendstoUniformlyOn {l : Filter ι} (h : TendstoUniformlyOn F f l s) (u : ℕ → ι) (hu : Tendsto u atTop l) :
TendstoUniformlyOn (fun n => F (u n)) f atTop s :=
by
rw [tendstoUniformlyOn_iff_tendsto] at h ⊢
exact h.comp ((hu.comp tendsto_fst).prodMk tendsto_snd)
