Missing essential supremum for extended reals #1360
Description
This code could be generalized to extended reals without much issues, it seems that not much depends on these definitions
https://github.com/math-comp/analysis/blob/6dfceaafefdeace2147a1ad9a307223641dccdb1/theories/measure.v#L5250C1-L5266C24