mul — Mathlib

English

If f and g are absolutely continuous on [a,b], then the product f(x) · g(x) is absolutely continuous on [a,b].

Русский

Если f и g абсолютно непрерывны на [a,b], то их произведение f(x)g(x) абсолютно непрерывно на [a,b].

LaTeX

$$$\forall a,b:\mathbb{R},\; \forall f,g:\mathbb{R}\to\mathbb{R},\; (\text{AC}(f,a,b) \land \text{AC}(g,a,b)) \Rightarrow \text{AC}(x\mapsto f(x)\,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 mul {f g : ℝ → ℝ} (hf : AbsolutelyContinuousOnInterval f a b) (hg : AbsolutelyContinuousOnInterval g a b) :
    AbsolutelyContinuousOnInterval (fun x ↦ f x * g x) a b :=
  hf.fun_mul hg

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