Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-08 07:33 9ecdd380

View on Github →

chore(algebra/order/sub): generalize 2 lemmas (#9611)

  • generalize lt_sub_iff_left and lt_sub_iff_right;
  • use general lemmas in data.real.ennreal.

Estimated changes

added theorem lt_sub_comm
modified theorem ennreal.lt_sub_comm
modified theorem ennreal.lt_sub_iff_add_lt