Theorems · Theorem · measure theory

MeasureTheory.setIntegral_ge_of_const_le_real

∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {s : Set X} {f : X → ℝ} {c : ℝ},
  MeasurableSet s →
    μ s ≠ ⊤ → (∀ x ∈ s, c ≤ f x) → MeasureTheory.IntegrableOn (fun x => f x) s μ → c * μ.real s ≤ ∫ (x : X) in s, 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