Theorems · Theorem · real analysis

AbsolutelyContinuousOnInterval.smul

∀ {F : Type u_2} [inst : SeminormedAddCommGroup F] {a b : ℝ} {M : Type u_3} [inst_1 : SeminormedRing M]
  [inst_2 : Module M F] [NormSMulClass M F] {f : ℝ → M} {g : ℝ → F},
  AbsolutelyContinuousOnInterval f a b →
    AbsolutelyContinuousOnInterval g a b → AbsolutelyContinuousOnInterval (f • g) a b

If f and g are absolutely continuous on uIcc a b, then f • g is absolutely continuous on uIcc a b.

Defined in

Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Cited by

2 results in Mathlib

Foundations

Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedAddCommGroupSeminormedRingModuleNormSMulClass