prodMap — Mathlib

English

If u and v are CauchySeq, then the sequence x ↦ (u x, v x) is Cauchy.

Русский

Если две последовательности Коши, то их попарное отображение в произведение тоже Коши.

LaTeX

$$$\\text{CauchySeq}(u) \\Rightarrow \\text{CauchySeq}(v) \\Rightarrow \\text{CauchySeq}(\\mathrm{ProdMk}(u,v)).$$$

Lean4

theorem prodMap {γ δ} [UniformSpace β] [Preorder γ] [Preorder δ] {u : γ → α} {v : δ → β} (hu : CauchySeq u)
    (hv : CauchySeq v) : CauchySeq (Prod.map u v) := by
  simpa only [CauchySeq, prod_map_map_eq', prod_atTop_atTop_eq] using hu.prod hv

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