Commit 2024-12-17 13:46 bb0575e3

View on Github →

feat(Data/EReal): Add results about EReal (#17087) Add results about operations on the extended real numbers.

  • Instances for EReal: CharZero and NoZeroDivisors.
  • Results about the coercion to the reals: toReal_eq_zero_iff, toReal_ne_zero_iff, toReal_nonneg, toReal_nonpos, coe_ennreal_toReal.
  • Results about the addition of EReals: add_ne_bot_iff, bot_lt_add_iff, add_ne_top and similar.
  • Reorganize and rename the lemmas le_neg and similar to make them more consistent, add the missing ones.
  • Results about the subtraction of EReals: top_sub_of_ne_top, sub_self, sub_self_le_zero, sub_nonneg and similar, sub_add_cancel and similar.
  • Results about the multiplication of Ereals: top_mul_coe_ennreal, coe_ennreal_mul_top, mul_pos_iff and similar, mul_eq_top and similar, coe_mul_add_of_nonneg and other distributivity lemmas, nsmul_eq_mul.
  • Move and simplify proof of mul_pos.
  • Clenaup.

Estimated changes

modified theorem EReal.add_lt_top
added theorem EReal.add_ne_bot_iff
added theorem EReal.add_ne_top
deleted theorem EReal.le_neg_of_le_neg
deleted theorem EReal.lt_neg_of_lt_neg
added theorem EReal.mul_eq_bot
added theorem EReal.mul_eq_top
added theorem EReal.mul_ne_bot
added theorem EReal.mul_ne_top
added theorem EReal.mul_neg_iff
added theorem EReal.mul_nonneg_iff
added theorem EReal.mul_nonpos_iff
modified theorem EReal.mul_pos
added theorem EReal.mul_pos_iff
deleted theorem EReal.neg_lt_of_neg_lt
added theorem EReal.nsmul_eq_mul
added theorem EReal.sub_add_cancel
modified theorem EReal.sub_add_cancel_left
modified theorem EReal.sub_bot
added theorem EReal.sub_neg
added theorem EReal.sub_nonneg
added theorem EReal.sub_nonpos
added theorem EReal.sub_pos
added theorem EReal.sub_self
added theorem EReal.sub_self_le_zero
added theorem EReal.toReal_eq_toReal
added theorem EReal.toReal_nonneg
added theorem EReal.toReal_nonpos
added theorem EReal.top_sub