Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-22 08:40 37647bf2

View on Github →

feat(measure_theory/constructions/borel_space): add norm_cast lemmas (#14295)

Estimated changes

Modified src/measure_theory/constructions/borel_space.lean

added theorem ae_measurable_coe_nnreal_ennreal_iff

added theorem ae_measurable_coe_nnreal_real_iff

modified theorem measurable_coe_nnreal_ennreal_iff

added theorem measurable_coe_nnreal_real_iff