English
If two families converge uniformly on a filter with respective limits, then their pairwise product converges uniformly on the product filter.
Русский
Если две последовательности сходятся равномерно на фильтре к ставленным пределам, значит их попарное произведение сходится равномерно на произведении фильтров.
LaTeX
$$$$\\text{TendstoUniformlyOnFilter}(F,f,p,p') \\land \\text{TendstoUniformlyOnFilter}(F',f',q,q') \\Rightarrow \\text{TendstoUniformlyOnFilter}(\\lambda i a. (F i a, F' i a), (f a, f' a), \\text{Filter.instSProd.sprod}(p,q), \\text{Filter.instSProd.sprod}(p',q'))$$$$
Lean4
/-- A sequence of functions `Fₙ` converges uniformly on a filter `p'` to a limiting function `f` w.r.t.
filter `p` iff the function `(n, x) ↦ (f x, Fₙ x)` converges along `p ×ˢ p'` to the uniformity.
In other words: one knows nothing about the behavior of `x` in this limit besides it being in `p'`.
-/
theorem tendstoUniformlyOnFilter_iff_tendsto :
TendstoUniformlyOnFilter F f p p' ↔ Tendsto (fun q : ι × α => (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β) :=
Iff.rfl
