Commit 2024-01-25 21:01 f9daa988

View on Github →

chore(Data/ENNReal/Basic): split file (#9869)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/ENNReal/Basic.lean

deleted theorem ENNReal.Ioo_zero_top_eq_iUnion_Ico_zpow

deleted theorem ENNReal.addLECancellable_iff_ne

deleted theorem ENNReal.add_eq_top

deleted theorem ENNReal.add_iInf

deleted theorem ENNReal.add_left_inj

deleted theorem ENNReal.add_lt_add

deleted theorem ENNReal.add_lt_top

deleted theorem ENNReal.add_ne_top

deleted theorem ENNReal.add_right_inj

deleted theorem ENNReal.add_thirds

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_div

deleted theorem ENNReal.coe_finset_prod

deleted theorem ENNReal.coe_finset_sum

deleted theorem ENNReal.coe_inv

deleted theorem ENNReal.coe_inv_le

deleted theorem ENNReal.coe_inv_two

deleted theorem ENNReal.coe_pow

deleted theorem ENNReal.coe_smul

deleted theorem ENNReal.coe_sub

deleted theorem ENNReal.coe_zpow

deleted theorem ENNReal.div_eq_one_iff

deleted theorem ENNReal.div_eq_top

deleted theorem ENNReal.div_eq_zero_iff

deleted theorem ENNReal.div_le_of_le_mul'

deleted theorem ENNReal.div_le_of_le_mul

deleted theorem ENNReal.div_lt_of_lt_mul'

deleted theorem ENNReal.div_lt_of_lt_mul

deleted theorem ENNReal.div_lt_top

deleted theorem ENNReal.div_pos_iff

deleted theorem ENNReal.div_top

deleted theorem ENNReal.div_zero

deleted theorem ENNReal.eq_div_iff

deleted theorem ENNReal.eq_top_of_forall_nnreal_le

deleted theorem ENNReal.exists_inv_nat_lt

deleted theorem ENNReal.exists_inv_two_pow_lt

deleted theorem ENNReal.exists_le_of_sum_le

deleted theorem ENNReal.exists_mem_Ico_zpow

deleted theorem ENNReal.exists_mem_Ioc_zpow

deleted theorem ENNReal.exists_nat_mul_gt

deleted theorem ENNReal.exists_nat_pos_inv_mul_lt

deleted theorem ENNReal.exists_nat_pos_mul_gt

deleted theorem ENNReal.exists_nnreal_pos_mul_lt

deleted theorem ENNReal.iInf_add

deleted theorem ENNReal.iInf_add_iInf

deleted theorem ENNReal.iInf_mul

deleted theorem ENNReal.iInf_mul_of_ne

deleted theorem ENNReal.iInf_sum

deleted theorem ENNReal.iSup_coe_nat

deleted theorem ENNReal.iSup_eq_zero

deleted theorem ENNReal.iSup_sub

deleted theorem ENNReal.iSup_zero_eq_zero

deleted theorem ENNReal.inv_eq_top

deleted theorem ENNReal.inv_le_iff_inv_le

deleted theorem ENNReal.inv_le_iff_le_mul

deleted theorem ENNReal.inv_lt_iff_inv_lt

deleted theorem ENNReal.inv_lt_top

deleted theorem ENNReal.inv_ne_top

deleted theorem ENNReal.inv_strictAnti

deleted theorem ENNReal.inv_three_add_inv_three

deleted theorem ENNReal.inv_top

deleted theorem ENNReal.inv_two_add_inv_two

deleted theorem ENNReal.inv_zero

deleted theorem ENNReal.le_inv_iff_le_inv

deleted theorem ENNReal.le_inv_iff_mul_le

deleted theorem ENNReal.le_ofReal_iff_toReal_le

deleted theorem ENNReal.le_of_forall_nnreal_lt

deleted theorem ENNReal.le_of_forall_pos_nnreal_lt

deleted theorem ENNReal.le_sub_of_add_le_left

deleted theorem ENNReal.le_sub_of_add_le_right

deleted theorem ENNReal.le_toReal_sub

deleted theorem ENNReal.lt_add_right

deleted theorem ENNReal.lt_inv_iff_lt_inv

deleted theorem ENNReal.lt_ofReal_iff_toReal_lt

deleted theorem ENNReal.lt_top_of_mul_ne_top_left

deleted theorem ENNReal.lt_top_of_mul_ne_top_right

deleted theorem ENNReal.lt_top_of_sum_ne_top

deleted theorem ENNReal.max_mul

deleted theorem ENNReal.mem_Iio_self_add

deleted theorem ENNReal.mem_Ioo_self_sub_add

deleted theorem ENNReal.monotone_zpow

deleted theorem ENNReal.mul_div_le

deleted theorem ENNReal.mul_eq_mul_left

deleted theorem ENNReal.mul_eq_mul_right

deleted theorem ENNReal.mul_eq_top

deleted theorem ENNReal.mul_iInf

deleted theorem ENNReal.mul_iInf_of_ne

deleted theorem ENNReal.mul_le_iff_le_inv

deleted theorem ENNReal.mul_le_mul_left

deleted theorem ENNReal.mul_le_mul_right

deleted theorem ENNReal.mul_le_of_le_div'

deleted theorem ENNReal.mul_le_of_le_div

deleted theorem ENNReal.mul_left_mono

deleted theorem ENNReal.mul_left_strictMono

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_of_lt_div'

deleted theorem ENNReal.mul_lt_of_lt_div

deleted theorem ENNReal.mul_lt_top

deleted theorem ENNReal.mul_lt_top_iff

deleted theorem ENNReal.mul_max

deleted theorem ENNReal.mul_ne_top

deleted theorem ENNReal.mul_pos

deleted theorem ENNReal.mul_pos_iff

deleted theorem ENNReal.mul_right_mono

deleted theorem ENNReal.mul_self_lt_top_iff

deleted theorem ENNReal.mul_sub

deleted theorem ENNReal.mul_top'

deleted theorem ENNReal.mul_top

deleted theorem ENNReal.nat_cast_le_ofReal

deleted theorem ENNReal.nat_cast_lt_ofReal

deleted theorem ENNReal.nat_cast_sub

deleted theorem ENNReal.not_lt_top

deleted theorem ENNReal.not_lt_zero

deleted theorem ENNReal.ofNat_le_ofReal

deleted theorem ENNReal.ofNat_lt_ofReal

deleted theorem ENNReal.ofReal_add

deleted theorem ENNReal.ofReal_add_le

deleted theorem ENNReal.ofReal_div_of_pos

deleted theorem ENNReal.ofReal_eq_nat_cast

deleted theorem ENNReal.ofReal_eq_ofNat

deleted theorem ENNReal.ofReal_eq_ofReal_iff

deleted theorem ENNReal.ofReal_eq_one

deleted theorem ENNReal.ofReal_eq_zero

deleted theorem ENNReal.ofReal_inv_of_pos

deleted theorem ENNReal.ofReal_le_iff_le_toReal

deleted theorem ENNReal.ofReal_le_nat_cast

deleted theorem ENNReal.ofReal_le_ofNat

deleted theorem ENNReal.ofReal_le_ofReal

deleted theorem ENNReal.ofReal_le_ofReal_iff'

deleted theorem ENNReal.ofReal_le_ofReal_iff

deleted theorem ENNReal.ofReal_le_of_le_toReal

deleted theorem ENNReal.ofReal_le_one

deleted theorem ENNReal.ofReal_lt_coe_iff

deleted theorem ENNReal.ofReal_lt_iff_lt_toReal

deleted theorem ENNReal.ofReal_lt_nat_cast

deleted theorem ENNReal.ofReal_lt_ofNat

deleted theorem ENNReal.ofReal_lt_ofReal_iff'

deleted theorem ENNReal.ofReal_lt_ofReal_iff

deleted theorem ENNReal.ofReal_lt_ofReal_iff_of_nonneg

deleted theorem ENNReal.ofReal_lt_one

deleted theorem ENNReal.ofReal_mul'

deleted theorem ENNReal.ofReal_mul

deleted theorem ENNReal.ofReal_nsmul

deleted theorem ENNReal.ofReal_pos

deleted theorem ENNReal.ofReal_pow

deleted theorem ENNReal.ofReal_prod_of_nonneg

deleted theorem ENNReal.ofReal_sub

deleted theorem ENNReal.ofReal_sum_of_nonneg

deleted theorem ENNReal.one_le_ofReal

deleted theorem ENNReal.one_lt_ofReal

deleted theorem ENNReal.one_sub_inv_two

deleted def ENNReal.orderIsoIicCoe

deleted theorem ENNReal.orderIsoIicCoe_symm_apply_coe

deleted def ENNReal.orderIsoIicOneBirational

deleted theorem ENNReal.orderIsoIicOneBirational_symm_apply

deleted def ENNReal.orderIsoUnitIntervalBirational

deleted theorem ENNReal.orderIsoUnitIntervalBirational_apply_coe

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.pow_strictMono

deleted theorem ENNReal.prod_lt_top

deleted theorem ENNReal.sInf_add

deleted theorem ENNReal.smul_def

deleted theorem ENNReal.smul_toNNReal

deleted theorem ENNReal.smul_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_half

deleted theorem ENNReal.sub_iInf

deleted theorem ENNReal.sub_lt_of_sub_lt

deleted theorem ENNReal.sub_mul

deleted theorem ENNReal.sub_ne_top

deleted theorem ENNReal.sub_right_inj

deleted theorem ENNReal.sub_sub_cancel

deleted theorem ENNReal.sub_top

deleted theorem ENNReal.sum_eq_top_iff

deleted theorem ENNReal.sum_lt_sum_of_nonempty

deleted theorem ENNReal.sum_lt_top

deleted theorem ENNReal.sum_lt_top_iff

deleted theorem ENNReal.sup_eq_zero

deleted def ENNReal.toNNRealHom

deleted theorem ENNReal.toNNReal_add

deleted theorem ENNReal.toNNReal_div

deleted theorem ENNReal.toNNReal_iInf

deleted theorem ENNReal.toNNReal_iSup

deleted theorem ENNReal.toNNReal_inv

deleted theorem ENNReal.toNNReal_le_toNNReal

deleted theorem ENNReal.toNNReal_lt_toNNReal

deleted theorem ENNReal.toNNReal_mono

deleted theorem ENNReal.toNNReal_mul

deleted theorem ENNReal.toNNReal_mul_top

deleted theorem ENNReal.toNNReal_pos

deleted theorem ENNReal.toNNReal_pos_iff

deleted theorem ENNReal.toNNReal_pow

deleted theorem ENNReal.toNNReal_prod

deleted theorem ENNReal.toNNReal_sInf

deleted theorem ENNReal.toNNReal_sSup

deleted theorem ENNReal.toNNReal_strict_mono

deleted theorem ENNReal.toNNReal_sum

deleted theorem ENNReal.toNNReal_top_mul

deleted def ENNReal.toRealHom

deleted theorem ENNReal.toReal_add

deleted theorem ENNReal.toReal_add_le

deleted theorem ENNReal.toReal_div

deleted theorem ENNReal.toReal_eq_toReal

deleted theorem ENNReal.toReal_iInf

deleted theorem ENNReal.toReal_iSup

deleted theorem ENNReal.toReal_inf

deleted theorem ENNReal.toReal_inv

deleted theorem ENNReal.toReal_le_add'

deleted theorem ENNReal.toReal_le_add

deleted theorem ENNReal.toReal_le_of_le_ofReal

deleted theorem ENNReal.toReal_le_toReal

deleted theorem ENNReal.toReal_lt_of_lt_ofReal

deleted theorem ENNReal.toReal_lt_toReal

deleted theorem ENNReal.toReal_max

deleted theorem ENNReal.toReal_min

deleted theorem ENNReal.toReal_mono'

deleted theorem ENNReal.toReal_mono

deleted theorem ENNReal.toReal_mul

deleted theorem ENNReal.toReal_mul_top

deleted theorem ENNReal.toReal_nsmul

deleted theorem ENNReal.toReal_ofReal_mul

deleted theorem ENNReal.toReal_pos

deleted theorem ENNReal.toReal_pos_iff

deleted theorem ENNReal.toReal_pos_iff_ne_top

deleted theorem ENNReal.toReal_pow

deleted theorem ENNReal.toReal_prod

deleted theorem ENNReal.toReal_sInf

deleted theorem ENNReal.toReal_sSup

deleted theorem ENNReal.toReal_smul

deleted theorem ENNReal.toReal_strict_mono

deleted theorem ENNReal.toReal_sub_of_le

deleted theorem ENNReal.toReal_sum

deleted theorem ENNReal.toReal_sup

deleted theorem ENNReal.toReal_top_mul

deleted theorem ENNReal.top_div

deleted theorem ENNReal.top_div_coe

deleted theorem ENNReal.top_div_of_lt_top

deleted theorem ENNReal.top_div_of_ne_top

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_coe

deleted theorem ENNReal.zero_eq_ofReal

deleted theorem ENNReal.zpow_le_of_le

deleted theorem ENNReal.zpow_lt_top

deleted theorem ENNReal.zpow_pos

deleted def Mathlib.Meta.Positivity.evalENNRealOfReal

deleted def OrderIso.invENNReal

deleted theorem OrderIso.invENNReal_symm_apply

Created Mathlib/Data/ENNReal/Inv.lean

added theorem ENNReal.Ioo_zero_top_eq_iUnion_Ico_zpow

added theorem ENNReal.add_thirds

added theorem ENNReal.coe_div

added theorem ENNReal.coe_inv

added theorem ENNReal.coe_inv_le

added theorem ENNReal.coe_inv_two

added theorem ENNReal.coe_zpow

added theorem ENNReal.div_eq_one_iff

added theorem ENNReal.div_eq_top

added theorem ENNReal.div_eq_zero_iff

added theorem ENNReal.div_le_of_le_mul'

added theorem ENNReal.div_le_of_le_mul

added theorem ENNReal.div_lt_of_lt_mul'

added theorem ENNReal.div_lt_of_lt_mul

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.eq_top_of_forall_nnreal_le

added theorem ENNReal.exists_inv_nat_lt

added theorem ENNReal.exists_inv_two_pow_lt

added theorem ENNReal.exists_mem_Ico_zpow

added theorem ENNReal.exists_mem_Ioc_zpow

added theorem ENNReal.exists_nat_mul_gt

added theorem ENNReal.exists_nat_pos_inv_mul_lt

added theorem ENNReal.exists_nat_pos_mul_gt

added theorem ENNReal.exists_nnreal_pos_mul_lt

added theorem ENNReal.inv_eq_top

added theorem ENNReal.inv_le_iff_inv_le

added theorem ENNReal.inv_le_iff_le_mul

added theorem ENNReal.inv_lt_iff_inv_lt

added theorem ENNReal.inv_lt_top

added theorem ENNReal.inv_ne_top

added theorem ENNReal.inv_strictAnti

added theorem ENNReal.inv_three_add_inv_three

added theorem ENNReal.inv_top

added theorem ENNReal.inv_two_add_inv_two

added theorem ENNReal.inv_zero

added theorem ENNReal.le_inv_iff_le_inv

added theorem ENNReal.le_inv_iff_mul_le

added theorem ENNReal.le_of_forall_nnreal_lt

added theorem ENNReal.le_of_forall_pos_nnreal_lt

added theorem ENNReal.lt_inv_iff_lt_inv

added theorem ENNReal.monotone_zpow

added theorem ENNReal.mul_div_le

added theorem ENNReal.mul_le_iff_le_inv

added theorem ENNReal.mul_le_of_le_div'

added theorem ENNReal.mul_le_of_le_div

added theorem ENNReal.mul_lt_of_lt_div'

added theorem ENNReal.mul_lt_of_lt_div

added theorem ENNReal.one_sub_inv_two

added def ENNReal.orderIsoIicCoe

added theorem ENNReal.orderIsoIicCoe_symm_apply_coe

added def ENNReal.orderIsoIicOneBirational

added theorem ENNReal.orderIsoIicOneBirational_symm_apply

added def ENNReal.orderIsoUnitIntervalBirational

added theorem ENNReal.orderIsoUnitIntervalBirational_apply_coe

added theorem ENNReal.sub_half

added theorem ENNReal.top_div

added theorem ENNReal.top_div_coe

added theorem ENNReal.top_div_of_lt_top

added theorem ENNReal.top_div_of_ne_top

added theorem ENNReal.zpow_le_of_le

added theorem ENNReal.zpow_lt_top

added theorem ENNReal.zpow_pos

added def OrderIso.invENNReal

added theorem OrderIso.invENNReal_symm_apply

Created Mathlib/Data/ENNReal/Operations.lean

added theorem ENNReal.addLECancellable_iff_ne

added theorem ENNReal.add_eq_top

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.cancel_coe

added theorem ENNReal.cancel_of_lt'

added theorem ENNReal.cancel_of_lt

added theorem ENNReal.cancel_of_ne

added theorem ENNReal.coe_finset_prod

added theorem ENNReal.coe_finset_sum

added theorem ENNReal.coe_pow

added theorem ENNReal.coe_smul

added theorem ENNReal.coe_sub

added theorem ENNReal.exists_le_of_sum_le

added theorem ENNReal.le_sub_of_add_le_left

added theorem ENNReal.le_sub_of_add_le_right

added theorem ENNReal.lt_add_right

added theorem ENNReal.lt_top_of_mul_ne_top_left

added theorem ENNReal.lt_top_of_mul_ne_top_right

added theorem ENNReal.lt_top_of_sum_ne_top

added theorem ENNReal.max_mul

added theorem ENNReal.mem_Iio_self_add

added theorem ENNReal.mem_Ioo_self_sub_add

added theorem ENNReal.mul_eq_mul_left

added theorem ENNReal.mul_eq_mul_right

added theorem ENNReal.mul_eq_top

added theorem ENNReal.mul_le_mul_left

added theorem ENNReal.mul_le_mul_right

added theorem ENNReal.mul_left_mono

added theorem ENNReal.mul_left_strictMono

added theorem ENNReal.mul_lt_mul

added theorem ENNReal.mul_lt_mul_left

added theorem ENNReal.mul_lt_mul_right

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_self_lt_top_iff

added theorem ENNReal.mul_sub

added theorem ENNReal.mul_top'

added theorem ENNReal.mul_top

added theorem ENNReal.nat_cast_sub

added theorem ENNReal.not_lt_top

added theorem ENNReal.not_lt_zero

added theorem ENNReal.ofReal_sum_of_nonneg

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_top

added theorem ENNReal.sub_eq_of_add_eq

added theorem ENNReal.sub_eq_sInf

added theorem ENNReal.sub_eq_top_iff

added theorem ENNReal.sub_lt_of_sub_lt

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_sum_of_nonempty

added theorem ENNReal.sum_lt_top

added theorem ENNReal.sum_lt_top_iff

added theorem ENNReal.toNNReal_add

added theorem ENNReal.toNNReal_sum

added 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_coe

Created Mathlib/Data/ENNReal/Real.lean

added theorem ENNReal.add_iInf

added theorem ENNReal.iInf_add

added theorem ENNReal.iInf_add_iInf

added theorem ENNReal.iInf_mul

added theorem ENNReal.iInf_mul_of_ne

added theorem ENNReal.iInf_sum

added theorem ENNReal.iSup_coe_nat

added theorem ENNReal.iSup_eq_zero

added theorem ENNReal.iSup_sub

added theorem ENNReal.iSup_zero_eq_zero

added theorem ENNReal.le_ofReal_iff_toReal_le

added theorem ENNReal.le_toReal_sub

added theorem ENNReal.lt_ofReal_iff_toReal_lt

added theorem ENNReal.mul_iInf

added theorem ENNReal.mul_iInf_of_ne

added theorem ENNReal.nat_cast_le_ofReal

added theorem ENNReal.nat_cast_lt_ofReal

added theorem ENNReal.ofNat_le_ofReal

added theorem ENNReal.ofNat_lt_ofReal

added theorem ENNReal.ofReal_add

added theorem ENNReal.ofReal_add_le

added theorem ENNReal.ofReal_div_of_pos

added theorem ENNReal.ofReal_eq_nat_cast

added theorem ENNReal.ofReal_eq_ofNat

added theorem ENNReal.ofReal_eq_ofReal_iff

added theorem ENNReal.ofReal_eq_one

added theorem ENNReal.ofReal_eq_zero

added theorem ENNReal.ofReal_inv_of_pos

added theorem ENNReal.ofReal_le_iff_le_toReal

added theorem ENNReal.ofReal_le_nat_cast

added theorem ENNReal.ofReal_le_ofNat

added theorem ENNReal.ofReal_le_ofReal

added theorem ENNReal.ofReal_le_ofReal_iff'

added theorem ENNReal.ofReal_le_ofReal_iff

added theorem ENNReal.ofReal_le_of_le_toReal

added theorem ENNReal.ofReal_le_one

added theorem ENNReal.ofReal_lt_coe_iff

added theorem ENNReal.ofReal_lt_iff_lt_toReal

added theorem ENNReal.ofReal_lt_nat_cast

added theorem ENNReal.ofReal_lt_ofNat

added theorem ENNReal.ofReal_lt_ofReal_iff'

added theorem ENNReal.ofReal_lt_ofReal_iff

added theorem ENNReal.ofReal_lt_ofReal_iff_of_nonneg

added theorem ENNReal.ofReal_lt_one

added theorem ENNReal.ofReal_mul'

added theorem ENNReal.ofReal_mul

added theorem ENNReal.ofReal_nsmul

added theorem ENNReal.ofReal_pos

added theorem ENNReal.ofReal_pow

added theorem ENNReal.ofReal_prod_of_nonneg

added theorem ENNReal.ofReal_sub

added theorem ENNReal.one_le_ofReal

added theorem ENNReal.one_lt_ofReal

added theorem ENNReal.sInf_add

added theorem ENNReal.smul_toNNReal

added theorem ENNReal.sub_iInf

added theorem ENNReal.sup_eq_zero

added def ENNReal.toNNRealHom

added theorem ENNReal.toNNReal_div

added theorem ENNReal.toNNReal_iInf

added theorem ENNReal.toNNReal_iSup

added theorem ENNReal.toNNReal_inv

added theorem ENNReal.toNNReal_le_toNNReal

added theorem ENNReal.toNNReal_lt_toNNReal

added theorem ENNReal.toNNReal_mono

added theorem ENNReal.toNNReal_mul

added theorem ENNReal.toNNReal_mul_top

added theorem ENNReal.toNNReal_pos

added theorem ENNReal.toNNReal_pos_iff

added theorem ENNReal.toNNReal_pow

added theorem ENNReal.toNNReal_prod

added theorem ENNReal.toNNReal_sInf

added theorem ENNReal.toNNReal_sSup

added theorem ENNReal.toNNReal_strict_mono

added theorem ENNReal.toNNReal_top_mul

added def ENNReal.toRealHom

added theorem ENNReal.toReal_add

added theorem ENNReal.toReal_add_le

added theorem ENNReal.toReal_div

added theorem ENNReal.toReal_eq_toReal

added theorem ENNReal.toReal_iInf

added theorem ENNReal.toReal_iSup

added theorem ENNReal.toReal_inf

added theorem ENNReal.toReal_inv

added theorem ENNReal.toReal_le_add'

added theorem ENNReal.toReal_le_add

added theorem ENNReal.toReal_le_of_le_ofReal

added theorem ENNReal.toReal_le_toReal

added theorem ENNReal.toReal_lt_of_lt_ofReal

added theorem ENNReal.toReal_lt_toReal

added theorem ENNReal.toReal_max

added theorem ENNReal.toReal_min

added theorem ENNReal.toReal_mono'

added theorem ENNReal.toReal_mono

added theorem ENNReal.toReal_mul

added theorem ENNReal.toReal_mul_top

added theorem ENNReal.toReal_nsmul

added theorem ENNReal.toReal_ofReal_mul

added theorem ENNReal.toReal_pos

added theorem ENNReal.toReal_pos_iff

added theorem ENNReal.toReal_pos_iff_ne_top

added theorem ENNReal.toReal_pow

added theorem ENNReal.toReal_prod

added theorem ENNReal.toReal_sInf

added theorem ENNReal.toReal_sSup

added theorem ENNReal.toReal_smul

added theorem ENNReal.toReal_strict_mono

added theorem ENNReal.toReal_sub_of_le

added theorem ENNReal.toReal_sup

added theorem ENNReal.toReal_top_mul

added theorem ENNReal.zero_eq_ofReal

added def Mathlib.Meta.Positivity.evalENNRealOfReal

Modified Mathlib/Data/Real/ConjugateExponents.lean

Modified Mathlib/Data/Real/EReal.lean

Modified Mathlib/Topology/EMetricSpace/Basic.lean