const_mul — Mathlib

English

If f is absolutely continuous on [a,b], then the function x ↦ α · f(x) is absolutely continuous on [a,b] for any real α.

Русский

Если f абсолютно непрерывна на [a,b], то для любого числа α функция x ↦ α · f(x) также абсолютно непрерывна на [a,b].

LaTeX

$$$\forall \alpha \in \mathbb{R},\, \text{AbsolutelyContinuousOnInterval}(f,a,b) \Rightarrow \text{AbsolutelyContinuousOnInterval}(\lambda x.\alpha \cdot f(x),a,b)$$$

Lean4

theorem const_mul {f : ℝ → ℝ} (α : ℝ) (hf : AbsolutelyContinuousOnInterval f a b) :
    AbsolutelyContinuousOnInterval (fun x ↦ α * f x) a b :=
  hf.const_smul α

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