Description: The supremum function distributes over multiplication, in the sense that ( sup A ) x. ( sup B ) = sup ( A x. B ) , where A x. B is shorthand for { a x. b | a e. A , b e. B } and is defined as C below. We made use of this in our definition of multiplication in the Dedekind cut construction of the reals (see df-mp ). (Contributed by Mario Carneiro, 5-Jul-2013) (Revised by Mario Carneiro, 6-Sep-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | supmul.1 | |
|
supmul.2 | |
||
Assertion | supmul | |