English
If, for every sequence u: ℕ → ι with u tending to atTop along l, the sequence F(u(n)) converges uniformly to f on s, then F converges uniformly to f on s along l.
Русский
Если для каждой последовательности u: ℕ → ι с u(n) сходится к atTop по l, последовательность F(u(n)) сходится равномерно к f на s, то F сходится равномерно к f на s по l.
LaTeX
$$$\\Big( \\forall u:\\mathbb{N} \\to ι,\\; \\text{Tendsto } u \\text{ atTop } l \\to \\text{TendstoUniformlyOn} (F \\circ u) f \\text{ atTop } s \\Big) \\Rightarrow \\text{TendstoUniformlyOn } F f l s$$$
Lean4
theorem tendstoUniformlyOn_of_seq_tendstoUniformlyOn {l : Filter ι} [l.IsCountablyGenerated]
(h : ∀ u : ℕ → ι, Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop s) :
TendstoUniformlyOn F f l s :=
by
rw [tendstoUniformlyOn_iff_tendsto, tendsto_iff_seq_tendsto]
intro u hu
rw [tendsto_prod_iff'] at hu
specialize h (fun n => (u n).fst) hu.1
rw [tendstoUniformlyOn_iff_tendsto] at h
exact h.comp (tendsto_id.prodMk hu.2)
