prodMk — Mathlib

English

Given Cauchy sequences u and v, the product sequence is Cauchy.

Русский

Дано Коши-последовательности u и v; их произведение по координатам тоже Коши.

LaTeX

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

Lean4

theorem prodMk {γ} [UniformSpace β] [Preorder γ] {u : γ → α} {v : γ → β} (hu : CauchySeq u) (hv : CauchySeq v) :
    CauchySeq fun x => (u x, v x) :=
  haveI := hu.1.of_map
  (Cauchy.prod hu hv).mono (tendsto_map.prodMk tendsto_map)

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