Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nnreal.val_eq_coe

Modification history

2020-12-16 07:31
src/data/real/nnreal.lean
chore(*): use notation `ℝ≥0` (#5391)
Modified nnreal.val_eq_coeView on Github →
2020-04-06 15:34
src/data/real/nnreal.lean
feat(topology/bounded_continuous_function): composition of limits when uniform convergence (#2260) …
Added nnreal.val_eq_coeView on Github →