Commit 2025-06-25 10:56 22cd4a11

View on Github →

refactor: move stuff on addition of iInf and iSup in ENNReal to a common place (#26356) Currently, they follow very similar API but the stuff on iInf is in ENNReal.Real and the stuff on iSup is in ENNReal.Inv. In this PR, I move them both to the end of the (intermediate) file ENNReal.Operations (as a lemma on subtraction is needed to prove some property of iSup). The end goal is to expand the APIs to make them even closer, but for now this PR is just a pure moving step.

Estimated changes

deleted theorem ENNReal.add_biSup'
deleted theorem ENNReal.add_biSup
deleted theorem ENNReal.add_iSup
deleted theorem ENNReal.add_sSup
deleted theorem ENNReal.biSup_add'
deleted theorem ENNReal.biSup_add
deleted theorem ENNReal.iSup_add
deleted theorem ENNReal.iSup_add_iSup
deleted theorem ENNReal.iSup_add_iSup_le
deleted theorem ENNReal.iSup_eq_zero
deleted theorem ENNReal.iSup_lt_eq_self
deleted theorem ENNReal.iSup_natCast
deleted theorem ENNReal.iSup_zero
deleted theorem ENNReal.sSup_add
deleted theorem ENNReal.sub_iSup
added theorem ENNReal.add_biSup'
added theorem ENNReal.add_biSup
added theorem ENNReal.add_iInf
added theorem ENNReal.add_iSup
added theorem ENNReal.add_sSup
added theorem ENNReal.biSup_add'
added theorem ENNReal.biSup_add
added theorem ENNReal.iInf_add
added theorem ENNReal.iInf_add_iInf
added theorem ENNReal.iSup_add
added theorem ENNReal.iSup_add_iSup
added theorem ENNReal.iSup_eq_zero
added theorem ENNReal.iSup_natCast
added theorem ENNReal.iSup_sub
added theorem ENNReal.iSup_zero
added theorem ENNReal.ofReal_iInf
added theorem ENNReal.sInf_add
added theorem ENNReal.sSup_add
added theorem ENNReal.sub_iInf
added theorem ENNReal.sub_iSup
added theorem ENNReal.toNNReal_iInf
added theorem ENNReal.toNNReal_iSup
added theorem ENNReal.toNNReal_sInf
added theorem ENNReal.toNNReal_sSup
added theorem ENNReal.toReal_iInf
added theorem ENNReal.toReal_iSup
added theorem ENNReal.toReal_sInf
added theorem ENNReal.toReal_sSup
deleted theorem ENNReal.add_iInf
deleted theorem ENNReal.iInf_add
deleted theorem ENNReal.iInf_add_iInf
deleted theorem ENNReal.iSup_sub
deleted theorem ENNReal.ofReal_iInf
deleted theorem ENNReal.sInf_add
deleted theorem ENNReal.sub_iInf
deleted theorem ENNReal.toNNReal_iInf
deleted theorem ENNReal.toNNReal_iSup
deleted theorem ENNReal.toNNReal_sInf
deleted theorem ENNReal.toNNReal_sSup
deleted theorem ENNReal.toReal_iInf
deleted theorem ENNReal.toReal_iSup
deleted theorem ENNReal.toReal_sInf
deleted theorem ENNReal.toReal_sSup