Theorems · Theorem · measure theory

MeasureTheory.setLIntegral_lt_top_of_bddAbove

∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  μ s ≠ ⊤ → ∀ {f : α → NNReal}, BddAbove (f '' s) → ∫⁻ (x : α) in s, ↑(f x) ∂μ < ⊤

Lebesgue integral of a bounded function over a set of finite measure is finite. Note that this lemma assumes no regularity of either f or s.

Defined in

Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Cited by

2 results in Mathlib

Foundations

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