prod — Mathlib

English

Let F and F' be families of functions with F i : α → β and F' j : α → β'. If each family is uniformly Cauchy on a set s with respect to p and p', then the map (i, j, a) ↦ (F i a, F' j a) is uniformly Cauchy on s with respect to the product filter p ×ˢ p'.

Русский

Пусть F и F' — семейства отображений F i: α → β и F' j: α → β'. Если каждое семейство является равномерно Коши на множества s относительно p и p', то отображение (i, j, a) ↦ (F i a, F' j a) образует равномерно Коши последовательность на s при произведении фильтров p ×ˢ p'.

LaTeX

$$$$ UniformCauchySeqOn F p s \\land UniformCauchySeqOn F' p' s \\Rightarrow UniformCauchySeqOn ((i,i')\\ a \\mapsto (F i a, F' i' a)) (p\\times^{\\mathrm{s}} p') s. $$$$

Lean4

theorem prod {ι' β' : Type*} [UniformSpace β'] {F' : ι' → α → β'} {p' : Filter ι'} (h : UniformCauchySeqOn F p s)
    (h' : UniformCauchySeqOn F' p' s) :
    UniformCauchySeqOn (fun (i : ι × ι') a => (F i.fst a, F' i.snd a)) (p ×ˢ p') s :=
  (congr_arg _ s.inter_self).mp ((h.prodMap h').comp fun a => (a, a))

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