English
If F and F' converge uniformly on p to f and f' respectively, then the map i ↦ (F i, F' i) converges uniformly to (f, f') with respect to p and the appropriate domain filters.
Русский
Если F и F' сходятся равномерно, то их параллельная карта сходится к соответствующей паре значений.
LaTeX
$$TendstoUniformly F f p → TendstoUniformly F' f' q → TendstoUniformly (fun i => Prod.map (F i) (F' i)) (Prod.map f f') (p ×ˢ q)$$
Lean4
theorem prodMap {ι' α' β' : Type*} [UniformSpace β'] {F' : ι' → α' → β'} {f' : α' → β'} {p' : Filter ι'}
(h : TendstoUniformly F f p) (h' : TendstoUniformly F' f' p') :
TendstoUniformly (fun i : ι × ι' => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') :=
by
rw [← tendstoUniformlyOn_univ, ← univ_prod_univ] at *
exact h.prodMap h'
