Theorems · Theorem · measure theory

MeasureTheory.setIntegral_gt_gt

∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {R : ℝ} {f : X → ℝ},
  0 ≤ R →
    MeasureTheory.IntegrableOn f {x | R < f x} μ →
      μ {x | R < f x} ≠ 0 → μ.real {x | R < f x} * R < ∫ (x : X) in {x | R < f x}, f x ∂μ

Defined in

Mathlib.MeasureTheory.Integral.Bochner.Set

Cited by

1 results in Mathlib

Foundations

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