Theorem MeasureTheory.Integrable.of_mem_Icc

Modification history

2025-01-03 11:53
Mathlib/MeasureTheory/Function/L1Space.lean
feat: `fun ω ↦ exp (t * X ω)` is integrable if `X` is bounded above (#20017) …
Added MeasureTheory.Integrable.of_mem_IccView on Github →