Theorems · Theorem · measure theory

MeasureTheory.exists_lt_lintegral_simpleFunc_of_lt_lintegral

∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {f : α → NNReal}
  {L : ENNReal},
  L < ∫⁻ (x : α), ↑(f x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Defined in

Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.SigmaFinite