Convexity and products

Stream: Is there code for X?

[Heather Macbeth]

I couldn't find these in the library, do they exist?

import analysis.convex.basic

open_locale big_operators
open set

variables {E : Type*} {F : Type*}
  [add_comm_group E] [vector_space ℝ E] [add_comm_group F] [vector_space ℝ F]

lemma prod_convex {s : set E} {t : set F} (hs : convex s) (ht : convex t) :
  convex (s.prod t) :=
sorry

lemma prod_convex_hull (s : set E) (t : set F) :
  convex_hull (s.prod t) = (convex_hull s).prod (convex_hull t) :=
sorry

[Heather Macbeth]

I have proofs of both (the latter rather terrible), will clean up and PR if missing.

[Patrick Massot]

Beware that @Yury G. Kudryashov is working on refactoring convexity.

[Patrick Massot]

So maybe you shouldn't invest too much time on this lemma right now.

[Heather Macbeth]

@Yury G. Kudryashov, how will your refactor interact with goals like this? I can post my proof if it would help you assess whether it's the kind of thing that would change a lot after the refactor.

[Yury G. Kudryashov]

Let me open a WIP PR tonight.

[Heather Macbeth]

Thanks!