Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ennreal.of_real_lt_of_real_iff_of_nonneg

Modification history

2020-01-21 09:56
src/data/real/ennreal.lean
feat(*): assorted simple lemmas, simplify some proofs (#1895) …
Added ennreal.of_real_lt_of_real_iff_of_nonnegView on Github →