const_mul — Mathlib

English

If a ∈ α is fixed and f: β → α is uniformly continuous, then the map x ↦ a · f(x) is uniformly continuous.

Русский

Если a фиксировано взят в α и f: β → α равномерно непрерывна, то отображение x ↦ a · f(x) равно равномерно непрерывному.

LaTeX

$$$\\mathrm{Uniformly\\;continuous}(f) \\rightarrow \\forall a \\in \\alpha,\\ \\mathrm{Uniformly\\;continuous}(x \\mapsto a \\cdot f(x))$$$

Lean4

@[to_additive]
theorem const_mul [UniformSpace β] {f : β → α} (hf : UniformContinuous f) (a : α) : UniformContinuous fun x ↦ a * f x :=
  uniformContinuous_const.mul hf

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