Commit 2023-02-28 07:22 127bbb26

View on Github →

feat: port Data.Real.EReal (#2501)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Real/EReal.lean

added def ENNReal.toEReal

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

added theorem EReal.add_bot

added theorem EReal.add_eq_bot_iff

added theorem EReal.add_lt_add

added theorem EReal.add_lt_add_left_coe

added theorem EReal.add_lt_add_of_lt_of_le'

added theorem EReal.add_lt_add_of_lt_of_le

added theorem EReal.add_lt_add_right_coe

added theorem EReal.add_lt_top

added theorem EReal.bot_add

added theorem EReal.bot_lt_add_iff

added theorem EReal.bot_lt_coe

added theorem EReal.bot_lt_coe_ennreal

added theorem EReal.bot_lt_zero

added theorem EReal.bot_mul_bot

added theorem EReal.bot_mul_coe_of_neg

added theorem EReal.bot_mul_coe_of_pos

added theorem EReal.bot_mul_of_neg

added theorem EReal.bot_mul_of_pos

added theorem EReal.bot_mul_top

added theorem EReal.bot_ne_coe

added theorem EReal.bot_ne_zero

added theorem EReal.bot_sub

added theorem EReal.coe_abs

added theorem EReal.coe_add

added theorem EReal.coe_add_top

added theorem EReal.coe_coe_sign

added theorem EReal.coe_ennreal_add

added theorem EReal.coe_ennreal_eq_coe_ennreal_iff

added theorem EReal.coe_ennreal_eq_one

added theorem EReal.coe_ennreal_eq_top_iff

added theorem EReal.coe_ennreal_eq_zero

added theorem EReal.coe_ennreal_injective

added theorem EReal.coe_ennreal_le_coe_ennreal_iff

added theorem EReal.coe_ennreal_lt_coe_ennreal_iff

added theorem EReal.coe_ennreal_mul

added theorem EReal.coe_ennreal_ne_bot

added theorem EReal.coe_ennreal_ne_coe_ennreal_iff

added theorem EReal.coe_ennreal_ne_one

added theorem EReal.coe_ennreal_ne_zero

added theorem EReal.coe_ennreal_nonneg

added theorem EReal.coe_ennreal_nsmul

added theorem EReal.coe_ennreal_ofReal

added theorem EReal.coe_ennreal_one

added theorem EReal.coe_ennreal_pos

added theorem EReal.coe_ennreal_pow

added theorem EReal.coe_ennreal_strictMono

added theorem EReal.coe_ennreal_top

added theorem EReal.coe_ennreal_zero

added theorem EReal.coe_eq_one

added theorem EReal.coe_eq_zero

added theorem EReal.coe_injective

added theorem EReal.coe_lt_top

added theorem EReal.coe_mul

added theorem EReal.coe_mul_bot_of_neg

added theorem EReal.coe_mul_bot_of_pos

added theorem EReal.coe_mul_top_of_neg

added theorem EReal.coe_mul_top_of_pos

added theorem EReal.coe_ne_bot

added theorem EReal.coe_ne_one

added theorem EReal.coe_ne_top

added theorem EReal.coe_ne_zero

added theorem EReal.coe_neg

added theorem EReal.coe_nnreal_eq_coe_real

added theorem EReal.coe_nnreal_lt_top

added theorem EReal.coe_nnreal_ne_top

added theorem EReal.coe_nsmul

added theorem EReal.coe_one

added theorem EReal.coe_pow

added theorem EReal.coe_real_ereal_eq_coe_toNNReal_sub_coe_toNNReal

added theorem EReal.coe_strictMono

added theorem EReal.coe_sub

added theorem EReal.coe_sub_bot

added theorem EReal.coe_toReal

added theorem EReal.coe_toReal_le

added theorem EReal.coe_zero

added theorem EReal.coe_zsmul

added theorem EReal.eq_bot_iff_forall_lt

added theorem EReal.eq_top_iff_forall_lt

added theorem EReal.exists_rat_btwn_of_lt

added theorem EReal.induction₂

added theorem EReal.induction₂_neg_left

added theorem EReal.induction₂_symm

added theorem EReal.induction₂_symm_neg

added theorem EReal.le_coe_toReal

added theorem EReal.le_iff_sign

added theorem EReal.le_neg_of_le_neg

added theorem EReal.lt_iff_exists_rat_btwn

added theorem EReal.lt_iff_exists_real_btwn

added theorem EReal.mul_bot_of_neg

added theorem EReal.mul_bot_of_pos

added theorem EReal.mul_top_of_neg

added theorem EReal.mul_top_of_pos

added def EReal.neTopBotEquivReal

added def EReal.negOrderIso

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_iff_neg_lt

added theorem EReal.neg_lt_neg_iff

added theorem EReal.neg_lt_of_neg_lt

added theorem EReal.neg_strictAnti

added theorem EReal.neg_top

added theorem EReal.sign_bot

added theorem EReal.sign_coe

added theorem EReal.sign_eq_and_abs_eq_iff_eq

added theorem EReal.sign_mul

added theorem EReal.sign_neg

added theorem EReal.sign_top

added theorem EReal.sub_le_sub

added theorem EReal.sub_lt_sub_of_lt_of_le

added theorem EReal.sub_top

added def EReal.toReal

added theorem EReal.toReal_add

added theorem EReal.toReal_bot

added theorem EReal.toReal_coe

added theorem EReal.toReal_coe_ennreal

added theorem EReal.toReal_le_toReal

added theorem EReal.toReal_mul

added theorem EReal.toReal_neg

added theorem EReal.toReal_one

added theorem EReal.toReal_sub

added theorem EReal.toReal_top

added theorem EReal.toReal_zero

added theorem EReal.top_add_coe

added theorem EReal.top_add_top

added theorem EReal.top_mul_bot

added theorem EReal.top_mul_coe_of_neg

added theorem EReal.top_mul_coe_of_pos

added theorem EReal.top_mul_of_neg

added theorem EReal.top_mul_of_pos

added theorem EReal.top_mul_top

added theorem EReal.top_ne_coe

added theorem EReal.top_ne_zero

added theorem EReal.top_sub_bot

added theorem EReal.top_sub_coe

added theorem EReal.zero_lt_top

added theorem EReal.zero_ne_bot

added theorem EReal.zero_ne_top

added def EReal

added def Real.toEReal

Modified Mathlib/Data/Sign.lean

added theorem abs_mul_sign

added theorem sign_mul_abs

modified theorem sign_pow

Modified Mathlib/Order/WithBot.lean

added theorem WithBot.strictAnti_iff

added theorem WithTop.strictAnti_iff