English
For a family F: ι → α →ᵇ β and f ∈ α →ᵇ β with l a filter on ι, Tendsto F l (nhds f) holds iff TendstoUniformly (λ i, F i) f l holds. That is, convergence in the sup-norm topology is equivalent to uniform convergence.
Русский
Для семейства F: ι → α →ᵇ β и f ∈ α →ᵇ β, при фильтре l: Tendsto F l (nhds f) эквивалентно TendstoUniformly F i f l. То есть сходимость в топологии с полной нормой эквивалентна равномерной сходимости.
LaTeX
$$$\\operatorname{Tendsto} F\\,l\\, (\\mathcal{N} f) \\;\\Longleftrightarrow\\; \\operatorname{TendstoUniformly} (\\lambda i. F i)\\; f\\; l$$$
Lean4
theorem tendsto_iff_tendstoUniformly {ι : Type*} {F : ι → α →ᵇ β} {f : α →ᵇ β} {l : Filter ι} :
Tendsto F l (𝓝 f) ↔ TendstoUniformly (fun i => F i) f l :=
Iff.intro
(fun h =>
tendstoUniformly_iff.2 fun ε ε0 =>
(Metric.tendsto_nhds.mp h ε ε0).mp
(Eventually.of_forall fun n hn x => lt_of_le_of_lt (dist_coe_le_dist x) (dist_comm (F n) f ▸ hn)))
fun h =>
Metric.tendsto_nhds.mpr fun _ ε_pos =>
(h _ (dist_mem_uniformity <| half_pos ε_pos)).mp
(Eventually.of_forall fun n hn =>
lt_of_le_of_lt ((dist_le (half_pos ε_pos).le).mpr fun x => dist_comm (f x) (F n x) ▸ le_of_lt (hn x))
(half_lt_self ε_pos))
