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.