Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-21 18:28 15d4e5f1

View on Github →

refactor(data/real/ennreal): remove sub lemmas (#9857)

Remove all lemmas about subtraction on ennreal that are special cases of has_ordered_sub lemmas.
This gives a list of renamings.
The lemmas that have a @[simp] attribute will be done in a separate PR

Estimated changes

Modified src/analysis/analytic/basic.lean

Modified src/analysis/box_integral/integrability.lean

Modified src/data/real/ennreal.lean

deleted theorem ennreal.le_sub_add_self

deleted theorem ennreal.lt_sub_comm

deleted theorem ennreal.lt_sub_iff_add_lt

modified theorem ennreal.mul_sub

deleted theorem ennreal.sub_add_self_eq_max

deleted theorem ennreal.sub_le_self

deleted theorem ennreal.sub_le_sub

deleted theorem ennreal.sub_le_sub_add_sub

deleted theorem ennreal.sub_self

deleted theorem ennreal.sub_zero

deleted theorem ennreal.zero_sub

Modified src/measure_theory/integral/lebesgue.lean

Modified src/measure_theory/integral/set_integral.lean

Modified src/measure_theory/measure/content.lean

Modified src/measure_theory/measure/haar_lebesgue.lean

Modified src/measure_theory/measure/hausdorff.lean

Modified src/measure_theory/measure/measure_space.lean

Modified src/measure_theory/measure/regular.lean

Modified src/topology/instances/ennreal.lean

Modified src/topology/metric_space/contracting.lean