Theorem ENNReal.ofReal_le_coe

Modification history

2025-11-02 21:27
Mathlib/Data/ENNReal/Real.lean
refactor(Topology): cleaner way to get metric spaces from emetric spaces (#29321) …
Added ENNReal.ofReal_le_coeView on Github →