Pointwise multiplication of sets preserves boundedness above. #
TODO: Can be combined with future results about pointwise multiplication on sets that use ordered algebraic classes.
theorem
Set.BddAbove.add
{α : Type u_1}
[OrderedAddCommMonoid α]
{A : Set α}
{B : Set α}
(hA : BddAbove A)
(hB : BddAbove B)
:
theorem
Set.BddAbove.mul
{α : Type u_1}
[OrderedCommMonoid α]
{A : Set α}
{B : Set α}
(hA : BddAbove A)
(hB : BddAbove B)
: