Theorem EReal.add_ne_top_iff_of_ne_bot_of_ne_top

Modification history

2025-03-31 03:39
Mathlib/Data/EReal/Basic.lean
chore: split `Data.EReal.Basic` (#23428) …
Modified EReal.add_ne_top_iff_of_ne_bot_of_ne_topView on Github →
2025-01-13 10:36
Mathlib/Data/Real/EReal.lean
feat(EReal): add `toENNReal` (#18885) …
Added EReal.add_ne_top_iff_of_ne_bot_of_ne_topView on Github →