English
If hf: UniformCauchySeqOn F p s and h': UniformCauchySeqOn F' p s, then the map i ↦ (F i a, F' i a) is UniformCauchy on p with respect to s.
Русский
Пусть hf: UniformCauchySeqOn F p s и h': UniformCauchySeqOn F' p s. Тогда отображение i ↦ (F i a, F' i a) является равномерно Коши на p по отношению к s.
LaTeX
$$$$ UniformCauchySeqOn F p s \\land UniformCauchySeqOn F' p s \\Rightarrow UniformCauchySeqOn (\\lambda i\\ a. (F i a, F' i a)) p s. $$$$
Lean4
theorem prod' {β' : Type*} [UniformSpace β'] {F' : ι → α → β'} (h : UniformCauchySeqOn F p s)
(h' : UniformCauchySeqOn F' p s) : UniformCauchySeqOn (fun (i : ι) a => (F i a, F' i a)) p s := fun u hu =>
have hh : Tendsto (fun x : ι => (x, x)) p (p ×ˢ p) := tendsto_diag
(hh.prodMap hh).eventually ((h.prod h') u hu)
