English
If F f and F' f' converge uniformly on p and q, then the map (i,i') ↦ (F i, F' i') converges uniformly to (f,f') on the product filter with s and s'.
Русский
Если F сходится к f и F' сходится к f', то отображение пар сходится к паре пределов.
LaTeX
$$TendstoUniformlyOnFilter F f p p' → TendstoUniformlyOnFilter F' f' q q' → TendstoUniformlyOnFilter (fun (i : ι × ι') a => (F i.1 a, F' i.2 a)) (fun a => (f a, f' a)) (p ×ˢ q) (p' ×ˢ q')$$
Lean4
protected theorem prodMk {ι' β' : Type*} [UniformSpace β'] {F' : ι' → α → β'} {f' : α → β'} {p' : Filter ι'}
(h : TendstoUniformlyOn F f p s) (h' : TendstoUniformlyOn F' f' p' s) :
TendstoUniformlyOn (fun (i : ι × ι') a => (F i.1 a, F' i.2 a)) (fun a => (f a, f' a)) (p ×ˢ p') s :=
(congr_arg _ s.inter_self).mp ((h.prodMap h').comp fun a => (a, a))
