English
If F and F' are uniform Cauchy sequences on p s and p' s', then the map sending (i,i') to (F_i i, F'_i i') is UniformCauchySeqOn on p × p' with s × s'.
Русский
Если F и F' — равномерно космические последовательности по p и p', то отображение, отправляющее (i,i') на (F_i, F'_i), является UniformCauchySeqOn на произведении p и p' и на s × s'.
LaTeX
$$$UniformCauchySeqOn F p s \\to UniformCauchySeqOn F' p' s' \\Rightarrow UniformCauchySeqOn (\\lambda i, \\lambda j: Prod.map (F i.1) (F' i.2)) (p ×^ s) (s ×^ s')$$$
Lean4
/-- Composing on the right by a function preserves uniform Cauchy sequences -/
theorem comp {γ : Type*} (hf : UniformCauchySeqOn F p s) (g : γ → α) :
UniformCauchySeqOn (fun n => F n ∘ g) p (g ⁻¹' s) :=
by
rw [uniformCauchySeqOn_iff_uniformCauchySeqOnFilter] at hf ⊢
simpa only [UniformCauchySeqOn, comap_principal] using hf.comp g
