Theorem aemeasurable_coe_nnreal_real_iff

Modification history

2024-05-18 13:04

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

chore(MeasureTheory.Constructions.BorelSpace.Basic): split file (#12470) …

Modified aemeasurable_coe_nnreal_real_iff View on Github →

2024-02-27 15:33

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

feat(MeasureTheory/Integral): hasSum_integral_of_summable_integral_norm (#10614) …

Added aemeasurable_coe_nnreal_real_iff View on Github →