mul_const' — Mathlib

English

If f is uniformly continuous with a UniformContinuousConstSMul structure on R, then the map x ↦ f(x) · a is uniformly continuous for any a ∈ R, using the opposite action.

Русский

Если f равномерно непрерывна и имеет структуру UniformContinuousConstSMul на R, то отображение x ↦ f(x) · a равно uniformly continuous для любого a ∈ R, используя противоположное действие.

LaTeX

$$$UniformContinuousConstSMul (R) (R) \Rightarrow (\forall f, UniformContinuous f) \Rightarrow UniformContinuous (\lambda x. f(x) \cdot a)$$$

Lean4

theorem mul_const' [UniformContinuousConstSMul Rᵐᵒᵖ R] {f : β → R} (hf : UniformContinuous f) (a : R) :
    UniformContinuous fun x ↦ f x * a :=
  hf.const_smul (MulOpposite.op a)

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