Commit 2024-10-02 20:35 3c0774cd

View on Github →

refactor(ENNReal): detopologise sSup/sInf lemmas (#16742) These lemmas can be proved much earlier with no topology.

Estimated changes

added theorem ENNReal.add_biSup'
added theorem ENNReal.add_biSup
added theorem ENNReal.add_iSup
added theorem ENNReal.add_sSup
added theorem ENNReal.biSup_add'
added theorem ENNReal.biSup_add
added theorem ENNReal.finsetSum_iSup
added theorem ENNReal.iInf_div'
added theorem ENNReal.iInf_div
added theorem ENNReal.iInf_div_of_ne
added theorem ENNReal.iInf_mul'
added theorem ENNReal.iInf_mul
added theorem ENNReal.iInf_mul_of_ne
added theorem ENNReal.iSup_add
added theorem ENNReal.iSup_add_iSup
added theorem ENNReal.iSup_div
added theorem ENNReal.iSup_eq_zero
added theorem ENNReal.iSup_mul
added theorem ENNReal.iSup_natCast
added theorem ENNReal.inv_iInf
added theorem ENNReal.inv_iSup
added theorem ENNReal.inv_sInf
added theorem ENNReal.inv_sSup
added theorem ENNReal.isUnit_iff
added theorem ENNReal.mul_iInf'
added theorem ENNReal.mul_iInf
added theorem ENNReal.mul_iInf_of_ne
added theorem ENNReal.mul_iSup
added theorem ENNReal.mul_sSup
added theorem ENNReal.sSup_add
added theorem ENNReal.sSup_div
added theorem ENNReal.sSup_mul
added theorem ENNReal.smul_iSup
added theorem ENNReal.smul_sSup
added theorem ENNReal.sub_iSup
deleted theorem ENNReal.iInf_mul
deleted theorem ENNReal.iInf_mul_of_ne
deleted theorem ENNReal.iSup_eq_zero
deleted theorem ENNReal.iSup_natCast
deleted theorem ENNReal.iSup_zero_eq_zero
deleted theorem ENNReal.mul_iInf
deleted theorem ENNReal.mul_iInf_of_ne
added theorem ENNReal.ofReal_iInf
deleted theorem ENNReal.add_biSup'
deleted theorem ENNReal.add_biSup
deleted theorem ENNReal.add_iSup
deleted theorem ENNReal.biSup_add'
deleted theorem ENNReal.biSup_add
deleted theorem ENNReal.finsetSum_iSup
deleted theorem ENNReal.iSup_add
deleted theorem ENNReal.iSup_add_iSup
deleted theorem ENNReal.iSup_add_iSup_le
deleted theorem ENNReal.iSup_div
deleted theorem ENNReal.iSup_mul
deleted theorem ENNReal.mul_iSup
deleted theorem ENNReal.mul_sSup
deleted theorem ENNReal.sSup_add
deleted theorem ENNReal.smul_iSup
deleted theorem ENNReal.smul_sSup
deleted theorem ENNReal.sub_iSup