Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ennreal.lt_sub_iff_add_lt

Modification history

2021-10-21 18:28
src/data/real/ennreal.lean
refactor(data/real/ennreal): remove sub lemmas (#9857) …
Deleted ennreal.lt_sub_iff_add_ltView on Github →
2021-10-20 15:39
src/data/real/ennreal.lean
refactor(algebra/order/sub): rename sub -> tsub (#9793) …
Modified ennreal.lt_sub_iff_add_ltView on Github →
2021-10-08 07:33
src/data/real/ennreal.lean
chore(algebra/order/sub): generalize 2 lemmas (#9611) …
Modified ennreal.lt_sub_iff_add_ltView on Github →
2020-03-17 01:31
src/data/real/ennreal.lean
feat(data/real/*nnreal): add division lemmas (#2167) …
Added ennreal.lt_sub_iff_add_ltView on Github →