Commit 2024-08-27 20:26 7b52ff5d

View on Github →

feat(NNReal/ENNReal): More basic lemmas (#16133) Add a few simple lemmas, make some existing distributivity lemmas simp, make it so that lemmas proving ≠ ⊤ take ≠ ⊤ assumptions and lemmas proving < ⊤ take < ⊤ assumptions. From LeanAPAP

Estimated changes

added theorem WithBot.bot_lt_prod
added theorem WithBot.prod_ne_bot
modified theorem WithTop.prod_lt_top
added theorem WithTop.prod_ne_top
added theorem WithTop.sum_eq_top
deleted theorem WithTop.sum_eq_top_iff
modified theorem WithTop.sum_lt_top
deleted theorem WithTop.sum_lt_top_iff
added theorem WithTop.sum_ne_top
added theorem WithTop.natCast_lt_top
deleted theorem WithBot.bot_lt_mul'
modified theorem WithBot.bot_lt_mul
added theorem WithBot.mul_ne_bot
deleted theorem WithTop.mul_lt_top'
modified theorem WithTop.mul_lt_top
added theorem WithTop.mul_ne_top
added theorem ENNReal.natCast_lt_top
modified theorem ENNReal.toNNReal_coe
modified theorem ENNReal.mul_lt_top
modified theorem ENNReal.mul_ne_top
modified theorem ENNReal.prod_lt_top
added theorem ENNReal.prod_ne_top
added theorem ENNReal.sum_eq_top
deleted theorem ENNReal.sum_eq_top_iff
modified theorem ENNReal.sum_lt_top
deleted theorem ENNReal.sum_lt_top_iff
added theorem ENNReal.sum_ne_top
modified theorem ENNReal.toNNReal_div
modified theorem ENNReal.toNNReal_inv
modified theorem ENNReal.toReal_div
modified theorem ENNReal.toReal_inv
modified theorem NNReal.coe_nsmul
added theorem NNReal.iSup_eq_zero