Theorem aEMeasurable_coe_nnreal_real_iff

Modification history

2024-02-27 15:33
Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
feat(MeasureTheory/Integral): hasSum_integral_of_summable_integral_norm (#10614) …
Deleted aEMeasurable_coe_nnreal_real_iffView on Github →
2023-05-21 12:07
Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
feat: port MeasureTheory.Constructions.BorelSpace.Basic (#4018)
Added aEMeasurable_coe_nnreal_real_iffView on Github →