Commit 2022-04-21 20:30 08323cda

View on Github →

feat(data/real/ennreal): tsub lemmas (#13525) Inherit lemmas about subtraction on ℝ≥0∞ from algebra.order.sub. Generalize add_le_cancellable.tsub_lt_self in passing. New ennreal lemmas

Estimated changes

Modified src/algebra/order/sub.lean

modified theorem tsub_lt_self

Modified src/data/real/ennreal.lean

modified theorem ennreal.add_div

deleted theorem ennreal.add_sub_self'

deleted theorem ennreal.add_sub_self

Modified src/measure_theory/measure/regular.lean

Modified src/topology/instances/ennreal.lean