Theorems · Theorem · measure theory

IntervalIntegrable.comp_mul_left_iff

∀ {E : Type u_5} [inst : NormedAddCommGroup E] {a b : ℝ} {f : ℝ → E} {c : ℝ},
  c ≠ 0 →
    autoParam (‖f (min a b)‖ₑ ≠ ⊤) IntervalIntegrable.comp_mul_left_iff._auto_1 →
      autoParam (‖f (c * min (a / c) (b / c))‖ₑ ≠ ⊤) IntervalIntegrable.comp_mul_left_iff._auto_3 →
        (IntervalIntegrable (fun x => f (c * x)) MeasureTheory.volume (a / c) (b / c) ↔
          IntervalIntegrable f MeasureTheory.volume a b)

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroup