Missing essential supremum for extended reals

[hoheinzollern]

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

@jmmarulang