prodMk — Mathlib

English

Uniform convergence of F to a constant on a product of filters is equivalent to convergence of F to that constant function uniformly on the set.

Русский

Сходимость по произведению фильтров к константе эквивалентна равномерной сходимости к константной функции.

LaTeX

$$$\text{Tendsto } ↿F (p ×ˢ p') (𝓝 c) \iff \text{TendstoUniformlyOnFilter } F (\text{const}_c) p p'$$

Lean4

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

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