Commit 2022-10-11 21:54 7507876b

View on Github →

feat(data/real/ereal): coe : ℝ → ereal is strictly monotone (#16607) and golf existing lemmas with it. Also delete ereal.bot_lt_top and friends in terms of the more general bot_lt_top.

Estimated changes

Modified src/data/real/ereal.lean

deleted theorem ereal.bot_lt_top

deleted theorem ereal.bot_ne_top

modified theorem ereal.coe_add

added theorem ereal.coe_bit0

added theorem ereal.coe_bit1

added theorem ereal.coe_ennreal_bit0

added theorem ereal.coe_ennreal_bit1

modified theorem ereal.coe_ennreal_eq_coe_ennreal_iff

added theorem ereal.coe_ennreal_injective

modified theorem ereal.coe_ennreal_le_coe_ennreal_iff

modified theorem ereal.coe_ennreal_lt_coe_ennreal_iff

added theorem ereal.coe_ennreal_mul

added theorem ereal.coe_ennreal_ne_coe_ennreal_iff

added theorem ereal.coe_ennreal_nsmul

added theorem ereal.coe_ennreal_pow

added theorem ereal.coe_ennreal_strict_mono

modified theorem ereal.coe_mul

modified theorem ereal.coe_neg

added theorem ereal.coe_nsmul

modified theorem ereal.coe_one

added theorem ereal.coe_pow

added theorem ereal.coe_sub

added theorem ereal.coe_zsmul

deleted theorem ereal.neg_eg_bot_iff

deleted theorem ereal.neg_eg_top_iff

deleted theorem ereal.neg_eg_zero_iff

added theorem ereal.neg_eq_bot_iff

added theorem ereal.neg_eq_top_iff

added theorem ereal.neg_eq_zero_iff

deleted theorem ereal.zero_sub

Modified src/topology/instances/ereal.lean