Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ae_measurable_coe_nnreal_real_iff

Modification history

2022-05-22 08:40
src/measure_theory/constructions/borel_space.lean
feat(measure_theory/constructions/borel_space): add `norm_cast` lemmas (#14295)
Added ae_measurable_coe_nnreal_real_iffView on Github →