Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-25 10:59 26c838fc

View on Github →

refactor(data/real/ennreal): remove ordered sub simp lemmas (#9902)

They are now simp lemmas in algebra/order/sub
Squeeze some simps

Estimated changes

Modified src/algebra/order/sub.lean

modified theorem add_tsub_cancel_of_le

modified theorem tsub_eq_zero_iff_le

added theorem tsub_eq_zero_of_le

modified theorem tsub_pos_iff_lt

Modified src/analysis/special_functions/integrals.lean

Modified src/analysis/specific_limits.lean

Modified src/computability/halting.lean

Modified src/data/real/ennreal.lean

deleted theorem ennreal.sub_eq_zero_of_le

Modified src/measure_theory/decomposition/lebesgue.lean

Modified src/measure_theory/integral/lebesgue.lean

Modified src/measure_theory/measure/regular.lean

Modified src/topology/instances/ennreal.lean

Modified src/topology/metric_space/emetric_space.lean