Mathlib v3 is deprecated. Go to Mathlib v4

Theorem 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 measurable_coe_nnreal_real_iff View on Github →