Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ennreal.lt_sub_comm

Modification history

2021-10-21 18:28
src/data/real/ennreal.lean
refactor(data/real/ennreal): remove sub lemmas (#9857) …
Deleted ennreal.lt_sub_commView on Github →
2021-10-20 15:39
src/data/real/ennreal.lean
refactor(algebra/order/sub): rename sub -> tsub (#9793) …
Modified ennreal.lt_sub_commView on Github →
2021-10-08 07:33
src/data/real/ennreal.lean
chore(algebra/order/sub): generalize 2 lemmas (#9611) …
Modified ennreal.lt_sub_commView on Github →
2021-09-24 11:04
src/data/real/ennreal.lean
refactor(measure_theory/measure/regular): add `inner_regular`, `outer_regular`, generalize (#9283) …
Added ennreal.lt_sub_commView on Github →