supremum of pointwise product of sets of real numbers

Stream: Is there code for X?

[Jujian Zhang]

Do we have that $\sup A\cdot B = \sup A \cdot \sup B$ where $A, B$ are sets of real number?

import data.real.basic
open_locale pointwise

example
  (s : set ℝ) (hs : ∀ (a : ℝ), a ∈ s → 0 ≤ a)
  (t : set ℝ) (ht : ∀ (a : ℝ), a ∈ t → 0 ≤ a): Sup s * Sup t = Sup (s * t) :=
sorry

[Sebastien Gouezel]

What about s = t = [-2, -1]?

[Jujian Zhang]

Good point! but in my case s and t are all nonnegative, let me change the code.

[Yaël Dillies]

file#data/real/pointwise