const_mul — Mathlib

English

If u is a Cauchy sequence, then n ↦ x · u(n) is Cauchy for any fixed x.

Русский

Если u — последовательность Коши, то n ↦ x · u(n) является последовательностью Коши для любого фиксированного x.

LaTeX

$$$CauchySeq\\,u \\Rightarrow CauchySeq\\,(\\lambda n. x \\cdot u(n))$$$

Lean4

@[to_additive]
theorem const_mul {ι : Type*} [Preorder ι] {u : ι → α} {x : α} (hu : CauchySeq u) : CauchySeq fun n => x * u n :=
  (uniformContinuous_const.mul uniformContinuous_id).comp_cauchySeq hu

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