English
If F and F' converge uniformly on p to f and f' on sets s and q on respective indices, then the map sending (i,i') to (F i, F' i') converges uniformly to (f,f') on the product of filters, restricted to s and q.
Русский
Если F сходится равномерно к f на s и F' сходится равномерно к f' на 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' : α' → β'} {p' : Filter ι'} {s' : Set α'}
(h : TendstoUniformlyOn F f p s) (h' : TendstoUniformlyOn F' f' p' s') :
TendstoUniformlyOn (fun i : ι × ι' => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (s ×ˢ s') :=
by
rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter] at h h' ⊢
simpa only [prod_principal_principal] using h.prodMap h'
