Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nnreal.coe_nonneg

Modification history

2020-12-16 07:31
src/data/real/nnreal.lean
chore(*): use notation `ℝ≥0` (#5391)
Modified nnreal.coe_nonnegView on Github →
2019-01-25 17:50
src/data/real/nnreal.lean
feat(measure_theory): add Hahn decomposition
Added nnreal.coe_nonnegView on Github →