## Stream: Is there code for X?

### Topic: Convexity and products

#### Heather Macbeth (Oct 25 2020 at 20:41):

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*}

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 (Oct 25 2020 at 20:42):

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

#### Patrick Massot (Oct 25 2020 at 20:43):

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

#### Patrick Massot (Oct 25 2020 at 20:43):

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

#### Heather Macbeth (Oct 25 2020 at 22:28):

@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 (Oct 25 2020 at 22:41):

Let me open a WIP PR tonight.

#### Heather Macbeth (Oct 25 2020 at 22:41):

Thanks!

Last updated: May 19 2021 at 00:40 UTC