multiplication in EReal, least upper bounds over Real, ENNRe

Stream: new members

[Pietro Lavino]

How is 0 multiplied by top or bottom defined? is the least upper bound over a set Real numbers a Real number or ca it be infinite, or is that only if we take supremum over ENNReal or EReal?

[Johan Commelin]

The supremum of a set of real numbers that doesn't actually have a supremum is defined to be 0, I think

[Damien Thomine]

How is 0 multiplied by top or bottom defined?

It's defined to be 0. For EReal, it is explained in a comment; you can go to the source to see the details.

For ENNReal, it is somewhat hidden. ENNReal is defined as WithTop NNReal, that is, NNReal (nonnegative reals) to which we add a top element. NNReal already has a multiplication, and ENNReal extends it using the construction in Algebra.Order.Ring.WithTop. Again, you can look at that file and its source to see that 0 * a = 0 for any a, including top.