prodMk — Mathlib

English

If F f and F' f' converge uniformly, then the pairwise product map converges uniformly to the pair (f,f').

Русский

Если существуют равномерные пределы F к f и F' к f', то пара функций сходится к паре (f,f').

LaTeX

$$TendstoUniformly F f p → TendstoUniformly F' f' q → TendstoUniformly (fun i a => (F i a, F' i a)) (fun a => (f a, f' a)) (p ×ˢ q)$$

Lean4

theorem prodMk {ι' β' : Type*} [UniformSpace β'] {F' : ι' → α → β'} {f' : α → β'} {q : Filter ι'}
    (h : TendstoUniformlyOnFilter F f p p') (h' : TendstoUniformlyOnFilter F' f' q p') :
    TendstoUniformlyOnFilter (fun (i : ι × ι') a => (F i.1 a, F' i.2 a)) (fun a => (f a, f' a)) (p ×ˢ q) p' :=
  fun u hu => ((h.prodMap h') u hu).diag_of_prod_right

Похожие утверждения