mul — Mathlib

English

If u and v are Cauchy sequences in a uniform group, then their pointwise product is also Cauchy.

Русский

Если u и v — последовательности Коши в равномерной группе, то их точечное произведение также является последовательностью Коши.

LaTeX

$$$CauchySeq\\,u \\to CauchySeq\\,v \\implies CauchySeq\\,(u * v)$$$

Lean4

@[to_additive]
theorem mul {ι : Type*} [Preorder ι] {u v : ι → α} (hu : CauchySeq u) (hv : CauchySeq v) : CauchySeq (u * v) :=
  uniformContinuous_mul.comp_cauchySeq (hu.prodMk hv)

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