Theorems · Theorem · real analysis

AbsolutelyContinuousOnInterval.const_smul

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

Defined in

Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Cited by

1 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedRingModuleNormSMulClass