Commit 2023-02-27 08:10 1979f8d9

View on Github →

feat: port Data.Real.ENNReal (#2388) I did some fixes/refactors while working on this PR. I'm going to move them to new PRs soon.

Estimated changes

added theorem ENNReal.add_eq_top
added theorem ENNReal.add_infᵢ
added theorem ENNReal.add_left_inj
added theorem ENNReal.add_lt_add
added theorem ENNReal.add_lt_top
added theorem ENNReal.add_ne_top
added theorem ENNReal.add_right_inj
added theorem ENNReal.add_thirds
added theorem ENNReal.bot_eq_zero
added theorem ENNReal.cancel_coe
added theorem ENNReal.cancel_of_lt'
added theorem ENNReal.cancel_of_lt
added theorem ENNReal.cancel_of_ne
added theorem ENNReal.cinfi_ne_top
added theorem ENNReal.coe_add
added theorem ENNReal.coe_div
added theorem ENNReal.coe_eq_coe
added theorem ENNReal.coe_eq_one
added theorem ENNReal.coe_eq_zero
added theorem ENNReal.coe_finset_sum
added theorem ENNReal.coe_finset_sup
added theorem ENNReal.coe_indicator
added theorem ENNReal.coe_infₛ
added theorem ENNReal.coe_inv
added theorem ENNReal.coe_inv_le
added theorem ENNReal.coe_inv_two
added theorem ENNReal.coe_le_coe
added theorem ENNReal.coe_le_iff
added theorem ENNReal.coe_le_one_iff
added theorem ENNReal.coe_lt_coe
added theorem ENNReal.coe_lt_coe_nat
added theorem ENNReal.coe_lt_one_iff
added theorem ENNReal.coe_lt_top
added theorem ENNReal.coe_max
added theorem ENNReal.coe_min
added theorem ENNReal.coe_mono
added theorem ENNReal.coe_mul
added theorem ENNReal.coe_nat
added theorem ENNReal.coe_nat_lt_coe
added theorem ENNReal.coe_ne_top
added theorem ENNReal.coe_ne_zero
added theorem ENNReal.coe_nnreal_eq
added theorem ENNReal.coe_ofNat
added theorem ENNReal.coe_one
added theorem ENNReal.coe_pos
added theorem ENNReal.coe_pow
added theorem ENNReal.coe_smul
added theorem ENNReal.coe_sub
added theorem ENNReal.coe_supₛ
added theorem ENNReal.coe_toNNReal
added theorem ENNReal.coe_toReal
added theorem ENNReal.coe_two
added theorem ENNReal.coe_zero
added theorem ENNReal.coe_zpow
added theorem ENNReal.csupr_ne_top
added theorem ENNReal.div_eq_inv_mul
added theorem ENNReal.div_eq_one_iff
added theorem ENNReal.div_eq_top
added theorem ENNReal.div_lt_top
added theorem ENNReal.div_pos_iff
added theorem ENNReal.div_top
added theorem ENNReal.div_zero
added theorem ENNReal.eq_div_iff
added theorem ENNReal.exists_ne_top'
added theorem ENNReal.exists_ne_top
added theorem ENNReal.forall_ennreal
added theorem ENNReal.forall_ne_top
added theorem ENNReal.infᵢ_add
added theorem ENNReal.infᵢ_ennreal
added theorem ENNReal.infᵢ_mul
added theorem ENNReal.infᵢ_ne_top
added theorem ENNReal.infᵢ_sum
added theorem ENNReal.infₛ_add
added theorem ENNReal.inv_eq_top
added theorem ENNReal.inv_lt_top
added theorem ENNReal.inv_ne_top
added theorem ENNReal.inv_strictAnti
added theorem ENNReal.inv_top
added theorem ENNReal.inv_zero
added theorem ENNReal.le_coe_iff
added theorem ENNReal.le_toReal_sub
added theorem ENNReal.lt_add_right
added theorem ENNReal.max_mul
added theorem ENNReal.max_zero_left
added theorem ENNReal.max_zero_right
added theorem ENNReal.monotone_zpow
added theorem ENNReal.mul_div_le
added theorem ENNReal.mul_eq_top
added theorem ENNReal.mul_infᵢ
added theorem ENNReal.mul_le_mul
added theorem ENNReal.mul_left_mono
added theorem ENNReal.mul_lt_mul
added theorem ENNReal.mul_lt_top
added theorem ENNReal.mul_lt_top_iff
added theorem ENNReal.mul_max
added theorem ENNReal.mul_ne_top
added theorem ENNReal.mul_pos
added theorem ENNReal.mul_pos_iff
added theorem ENNReal.mul_right_mono
added theorem ENNReal.mul_sub
added theorem ENNReal.mul_top'
added theorem ENNReal.mul_top
added theorem ENNReal.nat_cast_sub
added theorem ENNReal.nat_ne_top
added theorem ENNReal.none_eq_top
added theorem ENNReal.not_lt_top
added theorem ENNReal.not_lt_zero
added theorem ENNReal.not_top_le_coe
added theorem ENNReal.ofReal_add
added theorem ENNReal.ofReal_add_le
added theorem ENNReal.ofReal_coe_nat
added theorem ENNReal.ofReal_eq_zero
added theorem ENNReal.ofReal_lt_top
added theorem ENNReal.ofReal_mul'
added theorem ENNReal.ofReal_mul
added theorem ENNReal.ofReal_ne_top
added theorem ENNReal.ofReal_nsmul
added theorem ENNReal.ofReal_ofNat
added theorem ENNReal.ofReal_one
added theorem ENNReal.ofReal_pos
added theorem ENNReal.ofReal_pow
added theorem ENNReal.ofReal_sub
added theorem ENNReal.ofReal_toReal
added theorem ENNReal.ofReal_zero
added theorem ENNReal.one_eq_coe
added theorem ENNReal.one_le_coe_iff
added theorem ENNReal.one_lt_coe_iff
added theorem ENNReal.one_lt_top
added theorem ENNReal.one_ne_top
added theorem ENNReal.one_toNNReal
added theorem ENNReal.one_toReal
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
added theorem ENNReal.pow_strictMono
added theorem ENNReal.prod_lt_top
added theorem ENNReal.smul_def
added theorem ENNReal.smul_toNNReal
added def ENNReal.some
added theorem ENNReal.some_eq_coe'
added theorem ENNReal.some_eq_coe
added theorem ENNReal.sub_eq_infₛ
added theorem ENNReal.sub_eq_top_iff
added theorem ENNReal.sub_half
added theorem ENNReal.sub_infᵢ
added theorem ENNReal.sub_mul
added theorem ENNReal.sub_ne_top
added theorem ENNReal.sub_right_inj
added theorem ENNReal.sub_sub_cancel
added theorem ENNReal.sub_top
added theorem ENNReal.sum_eq_top_iff
added theorem ENNReal.sum_lt_top
added theorem ENNReal.sum_lt_top_iff
added theorem ENNReal.sup_eq_max
added theorem ENNReal.sup_eq_zero
added theorem ENNReal.supᵢ_coe_nat
added theorem ENNReal.supᵢ_ennreal
added theorem ENNReal.supᵢ_eq_zero
added theorem ENNReal.supᵢ_ne_top
added theorem ENNReal.supᵢ_sub
added theorem ENNReal.toNNReal_add
added theorem ENNReal.toNNReal_coe
added theorem ENNReal.toNNReal_div
added theorem ENNReal.toNNReal_inv
added theorem ENNReal.toNNReal_mono
added theorem ENNReal.toNNReal_mul
added theorem ENNReal.toNNReal_nat
added theorem ENNReal.toNNReal_pos
added theorem ENNReal.toNNReal_pow
added theorem ENNReal.toNNReal_prod
added theorem ENNReal.toNNReal_sum
added theorem ENNReal.toReal_add
added theorem ENNReal.toReal_add_le
added theorem ENNReal.toReal_div
added theorem ENNReal.toReal_inf
added theorem ENNReal.toReal_inv
added theorem ENNReal.toReal_max
added theorem ENNReal.toReal_min
added theorem ENNReal.toReal_mono
added theorem ENNReal.toReal_mul
added theorem ENNReal.toReal_mul_top
added theorem ENNReal.toReal_nat
added theorem ENNReal.toReal_nonneg
added theorem ENNReal.toReal_ofReal'
added theorem ENNReal.toReal_ofReal
added theorem ENNReal.toReal_pos
added theorem ENNReal.toReal_pos_iff
added theorem ENNReal.toReal_pow
added theorem ENNReal.toReal_prod
added theorem ENNReal.toReal_smul
added theorem ENNReal.toReal_sum
added theorem ENNReal.toReal_sup
added theorem ENNReal.toReal_top_mul
added theorem ENNReal.top_div
added theorem ENNReal.top_div_coe
added theorem ENNReal.top_mul'
added theorem ENNReal.top_mul
added theorem ENNReal.top_mul_top
added theorem ENNReal.top_ne_coe
added theorem ENNReal.top_ne_nat
added theorem ENNReal.top_ne_ofReal
added theorem ENNReal.top_ne_one
added theorem ENNReal.top_ne_zero
added theorem ENNReal.top_pow
added theorem ENNReal.top_sub_coe
added theorem ENNReal.top_toNNReal
added theorem ENNReal.top_toReal
added theorem ENNReal.two_ne_top
added theorem ENNReal.two_ne_zero
added theorem ENNReal.zero_eq_coe
added theorem ENNReal.zero_eq_ofReal
added theorem ENNReal.zero_ne_top
added theorem ENNReal.zero_toNNReal
added theorem ENNReal.zero_toReal
added theorem ENNReal.zpow_le_of_le
added theorem ENNReal.zpow_lt_top
added theorem ENNReal.zpow_pos
added def ENNReal