Theorem BoundedContinuousFunction.NNReal.coe_ennreal_comp_measurable
Modification history
2023-09-27 23:08
Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
feat: Lemmas about integrals of bounded continuous functions. (#7222) …
Deleted BoundedContinuousFunction.NNReal.coe_ennreal_comp_measurableView on Github →