const_mul' — Mathlib

English

Given a function f that is uniformly continuous and a uniformly continuous smul action, multiplying by a fixed scalar preserves uniform continuity.

Русский

Если f равномерно непрерывна и действует равномерно непрерывное умножение на скаляр, то умножение на константу сохраняет равномерную непрерывность.

LaTeX

$$$\text{UniformContinuous}(f) \Rightarrow \text{UniformContinuous}(c \cdot f)$$$

Lean4

theorem const_mul' [UniformContinuousConstSMul R R] {f : β → R} (hf : UniformContinuous f) (a : R) :
    UniformContinuous fun x ↦ a * f x :=
  hf.const_smul a

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