Commit 2024-10-15 09:10 41475d2a

View on Github →

chore(Topology.Instances.EReal): simplify proofs (#17738) And remove a couple of unnecessary hypotheses along the way.

Estimated changes

modified theorem EReal.add_iInf_le_iInf_add
modified theorem EReal.iSup_add_le_add_iSup