Theorem ENNReal.ofReal_mono

Modification history

2025-09-01 08:25
Mathlib/Data/ENNReal/Real.lean
feat(ENNReal): `min x y = 0 ↔ x = 0 ∨ y = 0` and other lemmas (#29165)
Added ENNReal.ofReal_monoView on Github →