Theorem Measurable.nnreal_mk

Modification history

2026-04-04 20:14
Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
feat: use a constructor for NNReal (#37609) …
Added Measurable.nnreal_mkView on Github →