Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ereal.le_neg_of_le_neg

Modification history

2020-01-25 23:45
src/data/real/ereal.lean
feat(data/real/ereal): add `ereal` := [-oo,oo] (#1703) …
Added ereal.le_neg_of_le_negView on Github →