English
If f: R → M and g: R → F are absolutely continuous on [a,b], then the product x ↦ f(x) · g(x) is absolutely continuous on [a,b].
Русский
Если f: R → M и g: R → F абсолютно непрерывны на [a,b], то функция x ↦ f(x)·g(x) абсолютно непрерывна на [a,b].
LaTeX
$$$\text{AbsolutelyContinuousOnInterval}(f,a,b) \wedge \text{AbsolutelyContinuousOnInterval}(g,a,b) \Rightarrow \text{AbsolutelyContinuousOnInterval}(x\mapsto f(x)\,\cdot\, g(x), a,b)$$$
Lean4
/-- If `f` and `g` are absolutely continuous on `uIcc a b`, then `f • g` is absolutely continuous
on `uIcc a b`. -/
theorem smul {M : Type*} [SeminormedRing M] [Module M F] [NormSMulClass M F] {f : ℝ → M} {g : ℝ → F}
(hf : AbsolutelyContinuousOnInterval f a b) (hg : AbsolutelyContinuousOnInterval g a b) :
AbsolutelyContinuousOnInterval (f • g) a b :=
hf.fun_smul hg
