Commit 2023-05-14 21:50 e066c3b8

View on Github →

chore: forward port leanprover-community/mathlib#18946 (#3888) Forward port leanprover-community/mathlib#18946.

Estimated changes

modified theorem ENNReal.coe_iInf
added theorem ENNReal.coe_iSup
added theorem ENNReal.toNNReal_iSup
added theorem ENNReal.toNNReal_sInf
added theorem ENNReal.toNNReal_sSup
added theorem ENNReal.toReal_iSup
added theorem ENNReal.toReal_sInf
added theorem ENNReal.toReal_sSup