English
If F and F' converge uniformly on p and q to f and f' respectively, then the map sending (i,i') ↦ (F i, F' i') converges uniformly to (f,f') with respect to the product filter p ×ˢ q.
Русский
Если F сходится равномерно к f и F' сходится равномерно к f' по фильтрам p и q, то отображение (i,i')↦(F i, F' i') сходится равномерно к (f,f') по произведению фильтров.
LaTeX
$$TendstoUniformlyOnFilter F f p p' → TendstoUniformlyOnFilter F' f' q q' → TendstoUniformlyOnFilter (fun i => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ q) (p' ×ˢ q')$$
Lean4
theorem prodMap {ι' α' β' : Type*} [UniformSpace β'] {F' : ι' → α' → β'} {f' : α' → β'} {q : Filter ι'} {q' : Filter α'}
(h : TendstoUniformlyOnFilter F f p p') (h' : TendstoUniformlyOnFilter F' f' q q') :
TendstoUniformlyOnFilter (fun i : ι × ι' => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ q) (p' ×ˢ q') :=
by
rw [tendstoUniformlyOnFilter_iff_tendsto] at h h' ⊢
rw [uniformity_prod_eq_comap_prod, tendsto_comap_iff, ← map_swap4_prod, tendsto_map'_iff]
simpa using h.prodMap h'
