Theorem ENNReal.top_ne_ofNat

Modification history

2025-01-31 16:21
Mathlib/Data/ENNReal/Basic.lean
feat(ENNReal/Basic): add `ofNat_ne_top` and `top_ne_ofNat` (#14486) …
Added ENNReal.top_ne_ofNatView on Github →