Theorem BoundedContinuousFunction.integral_eq_integral_nnrealPart_sub

Modification history

2024-08-09 00:58
Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean
chore: backports for leanprover/lean4#4814 (part 33) (#15605)
Modified BoundedContinuousFunction.integral_eq_integral_nnrealPart_subView on Github →
2023-09-27 23:08
Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean
feat: Lemmas about integrals of bounded continuous functions. (#7222) …
Modified BoundedContinuousFunction.integral_eq_integral_nnrealPart_subView on Github →
2023-06-07 00:35
Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
feat: port MeasureTheory.Measure.FiniteMeasure (#4747)
Added BoundedContinuousFunction.integral_eq_integral_nnrealPart_subView on Github →