mul_const — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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