Theorem NNReal.range_coe

Modification history

2026-10-13 14:51
Mathlib/Basic/NNReal/Basic.lean
refactor(Data): make `Set` a one-field structure (#41506) …
Modified NNReal.range_coeView on Github →
2026-01-20 01:13
Mathlib/Data/NNReal/Basic.lean
feat(NNReal): add lemmas about images of intervals (#34126)
Added NNReal.range_coeView on Github →