const_smul — Mathlib

English

If a function is uniformly continuous and there is a uniform continuous-smul action, then multiplying a fixed scalar by the function remains uniformly continuous.

Русский

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

LaTeX

$$$(\text{uniformContinuous}_\text{const\_smul} c) \circ f$$$

Lean4

@[to_additive]
theorem const_smul [UniformContinuousConstSMul M X] {f : Y → X} (hf : UniformContinuous f) (c : M) :
    UniformContinuous (c • f) :=
  (uniformContinuous_const_smul c).comp hf

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