Commit 2025-03-31 03:39 f8f8d42d

View on Github →

chore: split Data.EReal.Basic (#23428)

  • Data.EReal.Basic contains mostly coercion properties.
  • Data.EReal.Operations contains properties of add neg mul sub. (And Data.ENNReal.Order -> .Operations -> .BigOperators.)
  • Data.EReal.Inv contains properties of abs sign inv div. (Inspired by Data.ENNReal.Inv.)

Estimated changes

added theorem ENNReal.coe_finset_sum
added theorem ENNReal.finsetSum_iSup
added theorem ENNReal.iInf_sum
added theorem ENNReal.prod_lt_top
added theorem ENNReal.prod_ne_top
added theorem ENNReal.sum_eq_top
added theorem ENNReal.sum_lt_top
added theorem ENNReal.sum_ne_top
added theorem ENNReal.toNNReal_prod
added theorem ENNReal.toNNReal_sum
added theorem ENNReal.toReal_prod
added theorem ENNReal.toReal_sum
added theorem ENNReal.add_eq_top
added theorem ENNReal.add_left_inj
added theorem ENNReal.add_lt_top
added theorem ENNReal.add_ne_top
added theorem ENNReal.add_right_inj
added theorem ENNReal.cancel_coe
added theorem ENNReal.cancel_of_lt'
added theorem ENNReal.cancel_of_lt
added theorem ENNReal.cancel_of_ne
deleted theorem ENNReal.coe_finset_prod
deleted theorem ENNReal.coe_finset_sum
added theorem ENNReal.coe_sub
deleted theorem ENNReal.finsetSum_iSup
deleted theorem ENNReal.iInf_sum
added theorem ENNReal.image_coe_Icc
added theorem ENNReal.image_coe_Ici
added theorem ENNReal.image_coe_Ico
added theorem ENNReal.image_coe_Iic
added theorem ENNReal.image_coe_Iio
added theorem ENNReal.image_coe_Ioc
added theorem ENNReal.image_coe_Ioi
added theorem ENNReal.image_coe_Ioo
added theorem ENNReal.image_coe_uIcc
added theorem ENNReal.image_coe_uIoc
added theorem ENNReal.image_coe_uIoo
added theorem ENNReal.le_toReal_sub
added theorem ENNReal.lt_add_right
added theorem ENNReal.mul_eq_top
added theorem ENNReal.mul_lt_mul
added theorem ENNReal.mul_lt_top
added theorem ENNReal.mul_lt_top_iff
added theorem ENNReal.mul_ne_top
added theorem ENNReal.mul_pos
added theorem ENNReal.mul_pos_iff
added theorem ENNReal.mul_top'
added theorem ENNReal.mul_top
added theorem ENNReal.natCast_sub
added theorem ENNReal.not_lt_top
added theorem ENNReal.not_lt_zero
added theorem ENNReal.ofReal_sub
added theorem ENNReal.pow_eq_top
added theorem ENNReal.pow_eq_top_iff
added theorem ENNReal.pow_lt_top
added theorem ENNReal.pow_ne_top
deleted theorem ENNReal.prod_inv_distrib
deleted theorem ENNReal.prod_lt_top
deleted theorem ENNReal.prod_ne_top
added theorem ENNReal.sub_eq_sInf
added theorem ENNReal.sub_eq_top_iff
added theorem ENNReal.sub_ne_top
added theorem ENNReal.sub_ne_top_iff
added theorem ENNReal.sub_right_inj
added theorem ENNReal.sub_sub_cancel
added theorem ENNReal.sub_top
deleted theorem ENNReal.sum_eq_top
deleted theorem ENNReal.sum_lt_top
deleted theorem ENNReal.sum_ne_top
added theorem ENNReal.toNNReal_add
deleted theorem ENNReal.toNNReal_prod
added theorem ENNReal.toNNReal_sub
deleted theorem ENNReal.toNNReal_sum
added theorem ENNReal.toReal_le_add'
added theorem ENNReal.toReal_le_add
deleted theorem ENNReal.toReal_prod
deleted theorem ENNReal.toReal_sum
added theorem ENNReal.top_mul'
added theorem ENNReal.top_mul
added theorem ENNReal.top_mul_top
added theorem ENNReal.top_pow
added theorem ENNReal.top_sub
added theorem ENNReal.top_sub_coe
deleted theorem ENNReal.add_eq_top
deleted theorem ENNReal.add_left_inj
deleted theorem ENNReal.add_lt_top
deleted theorem ENNReal.add_ne_top
deleted theorem ENNReal.add_right_inj
deleted theorem ENNReal.cancel_coe
deleted theorem ENNReal.cancel_of_lt'
deleted theorem ENNReal.cancel_of_lt
deleted theorem ENNReal.cancel_of_ne
deleted theorem ENNReal.coe_sub
deleted theorem ENNReal.image_coe_Icc
deleted theorem ENNReal.image_coe_Ici
deleted theorem ENNReal.image_coe_Ico
deleted theorem ENNReal.image_coe_Iic
deleted theorem ENNReal.image_coe_Iio
deleted theorem ENNReal.image_coe_Ioc
deleted theorem ENNReal.image_coe_Ioi
deleted theorem ENNReal.image_coe_Ioo
deleted theorem ENNReal.image_coe_uIcc
deleted theorem ENNReal.image_coe_uIoc
deleted theorem ENNReal.image_coe_uIoo
deleted theorem ENNReal.le_toReal_sub
deleted theorem ENNReal.lt_add_right
deleted theorem ENNReal.mem_Iio_self_add
deleted theorem ENNReal.mul_eq_top
deleted theorem ENNReal.mul_le_mul_left
deleted theorem ENNReal.mul_le_mul_right
deleted theorem ENNReal.mul_lt_mul
deleted theorem ENNReal.mul_lt_mul_left
deleted theorem ENNReal.mul_lt_mul_right
deleted theorem ENNReal.mul_lt_top
deleted theorem ENNReal.mul_lt_top_iff
deleted theorem ENNReal.mul_ne_top
deleted theorem ENNReal.mul_pos
deleted theorem ENNReal.mul_pos_iff
deleted theorem ENNReal.mul_top'
deleted theorem ENNReal.mul_top
deleted theorem ENNReal.natCast_sub
deleted theorem ENNReal.not_lt_top
deleted theorem ENNReal.not_lt_zero
deleted theorem ENNReal.ofReal_sub
deleted theorem ENNReal.pow_eq_top
deleted theorem ENNReal.pow_eq_top_iff
deleted theorem ENNReal.pow_lt_top
deleted theorem ENNReal.pow_ne_top
deleted theorem ENNReal.sub_eq_of_add_eq
deleted theorem ENNReal.sub_eq_sInf
deleted theorem ENNReal.sub_eq_top_iff
deleted theorem ENNReal.sub_lt_of_sub_lt
deleted theorem ENNReal.sub_ne_top
deleted theorem ENNReal.sub_ne_top_iff
deleted theorem ENNReal.sub_right_inj
deleted theorem ENNReal.sub_sub_cancel
deleted theorem ENNReal.sub_top
deleted theorem ENNReal.toNNReal_add
deleted theorem ENNReal.toNNReal_sub
deleted theorem ENNReal.toReal_le_add'
deleted theorem ENNReal.toReal_le_add
deleted theorem ENNReal.toReal_sub_of_le
deleted theorem ENNReal.top_mul'
deleted theorem ENNReal.top_mul
deleted theorem ENNReal.top_mul_top
deleted theorem ENNReal.top_pow
deleted theorem ENNReal.top_sub
deleted theorem ENNReal.top_sub_coe
deleted theorem ENNReal.toEReal_sub
deleted theorem EReal.abs_bot
deleted theorem EReal.abs_coe_lt_top
deleted theorem EReal.abs_def
deleted theorem EReal.abs_eq_zero_iff
deleted theorem EReal.abs_mul
deleted theorem EReal.abs_top
deleted theorem EReal.abs_zero
deleted theorem EReal.add_bot
deleted theorem EReal.add_eq_bot_iff
deleted theorem EReal.add_le_of_forall_lt
deleted theorem EReal.add_le_of_le_sub
deleted theorem EReal.add_lt_add
deleted theorem EReal.add_lt_add_left_coe
deleted theorem EReal.add_lt_of_lt_sub
deleted theorem EReal.add_lt_top
deleted theorem EReal.add_ne_bot_iff
deleted theorem EReal.add_ne_top
deleted theorem EReal.add_pos
deleted theorem EReal.add_sub_cancel_left
deleted theorem EReal.add_top_iff_ne_bot
deleted theorem EReal.add_top_of_ne_bot
deleted theorem EReal.bot_add
deleted theorem EReal.bot_lt_add_iff
deleted theorem EReal.bot_lt_inv
deleted theorem EReal.bot_mul_bot
deleted theorem EReal.bot_mul_coe_of_neg
deleted theorem EReal.bot_mul_coe_of_pos
deleted theorem EReal.bot_mul_of_neg
deleted theorem EReal.bot_mul_of_pos
deleted theorem EReal.bot_mul_top
deleted theorem EReal.bot_sub
deleted theorem EReal.coe_abs
deleted theorem EReal.coe_add_top
deleted theorem EReal.coe_coe_sign
deleted theorem EReal.coe_div
deleted theorem EReal.coe_ennreal_mul_top
deleted theorem EReal.coe_ennreal_pow
deleted theorem EReal.coe_inv
deleted theorem EReal.coe_mul_bot_of_neg
deleted theorem EReal.coe_mul_bot_of_pos
deleted theorem EReal.coe_mul_top_of_neg
deleted theorem EReal.coe_mul_top_of_pos
deleted theorem EReal.coe_neg
deleted theorem EReal.coe_pow
deleted theorem EReal.coe_sub
deleted theorem EReal.coe_sub_bot
deleted theorem EReal.coe_zsmul
deleted theorem EReal.div_bot
deleted theorem EReal.div_div
deleted theorem EReal.div_eq_iff
deleted theorem EReal.div_le_iff_le_mul
deleted theorem EReal.div_lt_iff
deleted theorem EReal.div_mul_cancel
deleted theorem EReal.div_mul_div_comm
deleted theorem EReal.div_nonneg
deleted theorem EReal.div_pos
deleted theorem EReal.div_self
deleted theorem EReal.div_top
deleted theorem EReal.div_zero
deleted theorem EReal.inv_bot
deleted theorem EReal.inv_inv
deleted theorem EReal.inv_lt_top
deleted theorem EReal.inv_neg
deleted theorem EReal.inv_top
deleted theorem EReal.inv_zero
deleted theorem EReal.le_add_of_forall_gt
deleted theorem EReal.le_div_iff_mul_le
deleted theorem EReal.le_iff_sign
deleted theorem EReal.le_mul_of_forall_lt
deleted theorem EReal.le_sub_iff_add_le
deleted theorem EReal.lt_div_iff
deleted theorem EReal.lt_neg_comm
deleted theorem EReal.max_neg_neg
deleted theorem EReal.min_neg_neg
deleted theorem EReal.mul_bot_of_neg
deleted theorem EReal.mul_bot_of_pos
deleted theorem EReal.mul_div
deleted theorem EReal.mul_div_cancel
deleted theorem EReal.mul_div_left_comm
deleted theorem EReal.mul_div_mul_cancel
deleted theorem EReal.mul_div_right
deleted theorem EReal.mul_eq_bot
deleted theorem EReal.mul_eq_top
deleted theorem EReal.mul_inv
deleted theorem EReal.mul_ne_bot
deleted theorem EReal.mul_ne_top
deleted theorem EReal.mul_neg_iff
deleted theorem EReal.mul_nonneg_iff
deleted theorem EReal.mul_nonpos_iff
deleted theorem EReal.mul_pos
deleted theorem EReal.mul_pos_iff
deleted theorem EReal.mul_top_of_neg
deleted theorem EReal.mul_top_of_pos
deleted theorem EReal.natCast_div_le
deleted def EReal.negOrderIso
deleted theorem EReal.neg_add
deleted theorem EReal.neg_bot
deleted theorem EReal.neg_eq_bot_iff
deleted theorem EReal.neg_eq_top_iff
deleted theorem EReal.neg_eq_zero_iff
deleted theorem EReal.neg_le_neg_iff
deleted theorem EReal.neg_lt_comm
deleted theorem EReal.neg_lt_neg_iff
deleted theorem EReal.neg_strictAnti
deleted theorem EReal.neg_sub
deleted theorem EReal.neg_top
deleted theorem EReal.nsmul_eq_mul
deleted theorem EReal.sign_bot
deleted theorem EReal.sign_coe
deleted theorem EReal.sign_mul
deleted theorem EReal.sign_mul_inv_abs'
deleted theorem EReal.sign_mul_inv_abs
deleted theorem EReal.sign_neg
deleted theorem EReal.sign_top
deleted theorem EReal.sub_add_cancel
deleted theorem EReal.sub_add_cancel_left
deleted theorem EReal.sub_bot
deleted theorem EReal.sub_le_iff_le_add
deleted theorem EReal.sub_le_of_le_add'
deleted theorem EReal.sub_le_of_le_add
deleted theorem EReal.sub_le_sub
deleted theorem EReal.sub_lt_iff
deleted theorem EReal.sub_lt_of_lt_add'
deleted theorem EReal.sub_lt_of_lt_add
deleted theorem EReal.sub_neg
deleted theorem EReal.sub_nonneg
deleted theorem EReal.sub_nonpos
deleted theorem EReal.sub_pos
deleted theorem EReal.sub_self
deleted theorem EReal.sub_self_le_zero
deleted theorem EReal.sub_top
deleted theorem EReal.toENNReal_add
deleted theorem EReal.toENNReal_add_le
deleted theorem EReal.toENNReal_mul'
deleted theorem EReal.toENNReal_mul
deleted theorem EReal.toENNReal_sub
deleted theorem EReal.toReal_add
deleted theorem EReal.toReal_mul
deleted theorem EReal.toReal_neg
deleted theorem EReal.toReal_sub
deleted theorem EReal.top_add_coe
deleted theorem EReal.top_add_iff_ne_bot
deleted theorem EReal.top_add_of_ne_bot
deleted theorem EReal.top_add_top
deleted theorem EReal.top_mul_bot
deleted theorem EReal.top_mul_coe_ennreal
deleted theorem EReal.top_mul_coe_of_neg
deleted theorem EReal.top_mul_coe_of_pos
deleted theorem EReal.top_mul_of_neg
deleted theorem EReal.top_mul_of_pos
deleted theorem EReal.top_mul_top
deleted theorem EReal.top_sub
deleted theorem EReal.top_sub_bot
deleted theorem EReal.top_sub_coe
deleted theorem EReal.zero_div
added theorem EReal.abs_bot
added theorem EReal.abs_coe_lt_top
added theorem EReal.abs_def
added theorem EReal.abs_eq_zero_iff
added theorem EReal.abs_mul
added theorem EReal.abs_top
added theorem EReal.abs_zero
added theorem EReal.bot_lt_inv
added theorem EReal.coe_abs
added theorem EReal.coe_coe_sign
added theorem EReal.coe_div
added theorem EReal.coe_ennreal_pow
added theorem EReal.coe_inv
added theorem EReal.coe_pow
added theorem EReal.div_bot
added theorem EReal.div_div
added theorem EReal.div_eq_iff
added theorem EReal.div_lt_iff
added theorem EReal.div_mul_cancel
added theorem EReal.div_mul_div_comm
added theorem EReal.div_nonneg
added theorem EReal.div_pos
added theorem EReal.div_self
added theorem EReal.div_top
added theorem EReal.div_zero
added theorem EReal.inv_bot
added theorem EReal.inv_inv
added theorem EReal.inv_lt_top
added theorem EReal.inv_neg
added theorem EReal.inv_top
added theorem EReal.inv_zero
added theorem EReal.le_iff_sign
added theorem EReal.lt_div_iff
added theorem EReal.max_neg_neg
added theorem EReal.min_neg_neg
added theorem EReal.mul_div
added theorem EReal.mul_div_cancel
added theorem EReal.mul_div_right
added theorem EReal.mul_inv
added theorem EReal.natCast_div_le
added theorem EReal.sign_bot
added theorem EReal.sign_coe
added theorem EReal.sign_mul
added theorem EReal.sign_mul_inv_abs
added theorem EReal.sign_neg
added theorem EReal.sign_top
added theorem EReal.zero_div
added theorem ENNReal.toEReal_sub
added theorem EReal.add_bot
added theorem EReal.add_eq_bot_iff
added theorem EReal.add_le_of_le_sub
added theorem EReal.add_lt_add
added theorem EReal.add_lt_of_lt_sub
added theorem EReal.add_lt_top
added theorem EReal.add_ne_bot_iff
added theorem EReal.add_ne_top
added theorem EReal.add_pos
added theorem EReal.bot_add
added theorem EReal.bot_lt_add_iff
added theorem EReal.bot_mul_bot
added theorem EReal.bot_mul_of_neg
added theorem EReal.bot_mul_of_pos
added theorem EReal.bot_mul_top
added theorem EReal.bot_sub
added theorem EReal.coe_add_top
added theorem EReal.coe_neg
added theorem EReal.coe_sub
added theorem EReal.coe_sub_bot
added theorem EReal.coe_zsmul
added theorem EReal.lt_neg_comm
added theorem EReal.mul_bot_of_neg
added theorem EReal.mul_bot_of_pos
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
added theorem EReal.mul_pos
added theorem EReal.mul_pos_iff
added theorem EReal.mul_top_of_neg
added theorem EReal.mul_top_of_pos
added theorem EReal.neg_add
added theorem EReal.neg_bot
added theorem EReal.neg_eq_bot_iff
added theorem EReal.neg_eq_top_iff
added theorem EReal.neg_eq_zero_iff
added theorem EReal.neg_le_neg_iff
added theorem EReal.neg_lt_comm
added theorem EReal.neg_lt_neg_iff
added theorem EReal.neg_strictAnti
added theorem EReal.neg_sub
added theorem EReal.neg_top
added theorem EReal.nsmul_eq_mul
added theorem EReal.sub_add_cancel
added theorem EReal.sub_bot
added theorem EReal.sub_le_of_le_add
added theorem EReal.sub_le_sub
added theorem EReal.sub_lt_iff
added theorem EReal.sub_lt_of_lt_add
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.sub_top
added theorem EReal.toENNReal_add
added theorem EReal.toENNReal_add_le
added theorem EReal.toENNReal_mul'
added theorem EReal.toENNReal_mul
added theorem EReal.toENNReal_sub
added theorem EReal.toReal_add
added theorem EReal.toReal_mul
added theorem EReal.toReal_neg
added theorem EReal.toReal_sub
added theorem EReal.top_add_coe
added theorem EReal.top_add_top
added theorem EReal.top_mul_bot
added theorem EReal.top_mul_of_neg
added theorem EReal.top_mul_of_pos
added theorem EReal.top_mul_top
added theorem EReal.top_sub
added theorem EReal.top_sub_bot
added theorem EReal.top_sub_coe