Theorem ENNReal.ofReal_min

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_minView on Github →