Commit 2023-02-20 08:04 8c9ab0d1

View on Github →

feat: port Data.Real.NNReal (#2234)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Real/NNReal.lean

added theorem NNReal.abs_eq

added theorem NNReal.bddAbove_coe

added theorem NNReal.bddBelow_coe

added theorem NNReal.bot_eq_zero

added theorem NNReal.coe_image

added theorem NNReal.coe_indicator

added theorem NNReal.coe_infᵢ

added theorem NNReal.coe_infₛ

added theorem NNReal.coe_list_prod

added theorem NNReal.coe_list_sum

added theorem NNReal.coe_max

added theorem NNReal.coe_min

added theorem NNReal.coe_mk

added theorem NNReal.coe_multiset_prod

added theorem NNReal.coe_multiset_sum

added theorem NNReal.coe_ne_zero

added theorem NNReal.coe_nonneg

added theorem NNReal.coe_nsmul

added theorem NNReal.coe_pow

added theorem NNReal.coe_prod

added theorem NNReal.coe_sub_def

added theorem NNReal.coe_sum

added theorem NNReal.coe_supᵢ

added theorem NNReal.coe_supₛ

added theorem NNReal.coe_toRealHom

added theorem NNReal.coe_zpow

added theorem NNReal.div_le_div_left_of_le

added theorem NNReal.div_le_iff

added theorem NNReal.div_le_of_le_mul'

added theorem NNReal.div_le_of_le_mul

added theorem NNReal.div_lt_iff'

added theorem NNReal.div_lt_iff

added theorem NNReal.div_lt_one_of_lt

added theorem NNReal.div_self_le

added theorem NNReal.finset_sup_div

added theorem NNReal.finset_sup_mul

added theorem NNReal.infᵢ_const_zero

added theorem NNReal.infᵢ_empty

added theorem NNReal.infᵢ_mul

added theorem NNReal.infₛ_empty

added theorem NNReal.inv_le

added theorem NNReal.inv_le_of_le_mul

added theorem NNReal.inv_lt_inv

added theorem NNReal.inv_lt_inv_iff

added theorem NNReal.inv_lt_one_iff

added theorem NNReal.le_div_iff_mul_le

added theorem NNReal.le_infᵢ_add_infᵢ

added theorem NNReal.le_infᵢ_mul

added theorem NNReal.le_infᵢ_mul_infᵢ

added theorem NNReal.le_inv_iff_mul_le

added theorem NNReal.le_mul_infᵢ

added theorem NNReal.le_of_forall_lt_one_mul_le

added theorem NNReal.le_toNNReal_of_coe_le

added theorem NNReal.lt_div_iff'

added theorem NNReal.lt_div_iff

added theorem NNReal.lt_iff_exists_rat_btwn

added theorem NNReal.lt_inv_iff_mul_lt

added theorem NNReal.mk_coe_nat

added theorem NNReal.mul_eq_mul_left

added theorem NNReal.mul_finset_sup

added theorem NNReal.mul_infᵢ

added theorem NNReal.mul_le_iff_le_inv

added theorem NNReal.mul_lt_of_lt_div

added theorem NNReal.mul_sup

added theorem NNReal.mul_supᵢ

added theorem NNReal.mul_supᵢ_le

added theorem NNReal.ne_iff

added def NNReal.orderIsoIccZeroCoe

added theorem NNReal.orderIsoIccZeroCoe_apply_coe_coe

added theorem NNReal.orderIsoIccZeroCoe_symm_apply_coe

added theorem NNReal.pow_antitone_exp

added theorem NNReal.smul_def

added theorem NNReal.sub_def

added theorem NNReal.sub_div

added theorem NNReal.sum_div

added theorem NNReal.sup_mul

added theorem NNReal.supᵢ_div

added theorem NNReal.supᵢ_empty

added theorem NNReal.supᵢ_mul

added theorem NNReal.supᵢ_mul_le

added theorem NNReal.supᵢ_mul_supᵢ_le

added theorem NNReal.supᵢ_of_not_bddAbove

added theorem NNReal.toNNReal_coe_nat

added def NNReal.toReal

added def NNReal.toRealHom

added theorem NNReal.val_eq_coe

added theorem NNReal.zero_le_coe

added theorem NNReal.zpow_pos

added def NNReal

added theorem Real.cast_natAbs_eq_nnabs_cast

added theorem Real.coe_nnabs

added theorem Real.coe_toNNReal'

added theorem Real.coe_toNNReal

added theorem Real.coe_toNNReal_le

added theorem Real.le_coe_toNNReal

added theorem Real.le_toNNReal_iff_coe_le'

added theorem Real.le_toNNReal_iff_coe_le

added theorem Real.lt_toNNReal_iff_coe_lt

added def Real.nnabs

added theorem Real.nnabs_coe

added theorem Real.nnabs_of_nonneg

added theorem Real.toNNReal_add

added theorem Real.toNNReal_add_le

added theorem Real.toNNReal_add_toNNReal

added theorem Real.toNNReal_coe

added theorem Real.toNNReal_div'

added theorem Real.toNNReal_div

added theorem Real.toNNReal_eq_toNNReal_iff

added theorem Real.toNNReal_eq_zero

added theorem Real.toNNReal_inv

added theorem Real.toNNReal_le_iff_le_coe

added theorem Real.toNNReal_le_toNNReal

added theorem Real.toNNReal_le_toNNReal_iff

added theorem Real.toNNReal_lt_iff_lt_coe

added theorem Real.toNNReal_lt_toNNReal_iff'

added theorem Real.toNNReal_lt_toNNReal_iff

added theorem Real.toNNReal_lt_toNNReal_iff_of_nonneg

added theorem Real.toNNReal_mul

added theorem Real.toNNReal_of_nonneg

added theorem Real.toNNReal_of_nonpos

added theorem Real.toNNReal_one

added theorem Real.toNNReal_pos

added theorem Real.toNNReal_pow

added theorem Real.toNNReal_prod_of_nonneg

added theorem Real.toNNReal_sum_of_nonneg

added theorem Real.toNNReal_zero

added theorem Set.OrdConnected.image_coe_nnreal_real

added theorem Set.OrdConnected.image_real_toNNReal

added theorem Set.OrdConnected.preimage_coe_nnreal_real

added theorem Set.OrdConnected.preimage_real_toNNReal