## Stream: Is there code for X?

### Topic: affine span is convex

#### Bhavik Mehta (Mar 06 2021 at 22:40):

I'm struggling to find any connection in mathlib between affine spans and convex sets, for instance, how do I show the following?

example {m : ℕ} (X : set (fin m → ℝ)) :
convex (affine_span ℝ X : set (fin m → ℝ)) :=
begin
end


#### Kenny Lau (Mar 06 2021 at 22:58):

import analysis.convex.basic
import linear_algebra.affine_space.affine_subspace

example {m : ℕ} (M : Type*) [add_comm_group M] [vector_space ℝ M] (s : affine_subspace ℝ M) :
convex (s : set M) :=
λ x y hxs hys a b ha hb hab,
calc  a • x + b • y
= (1 - b) • x + b • y : by rw eq_sub_of_add_eq hab
... = b • (y - x) + x :
... ∈ s : s.2 _ hys hxs hxs


#### Bhavik Mehta (Mar 06 2021 at 23:01):

Wow I didn't know calc allowed x = y ∈ s chains

Thanks!

#### Bhavik Mehta (Mar 06 2021 at 23:03):

golfed:

example (M : Type*) [add_comm_group M] [vector_space ℝ M] (s : affine_subspace ℝ M) :
convex (s : set M) :=
λ x y hxs hys a b ha hb hab,
calc a • x + b • y = b • (y - x) + x : convex.combo_to_vadd hab
... ∈ s : s.2 _ hys hxs hxs


#### Kenny Lau (Mar 06 2021 at 23:20):

golfed:

import analysis.convex.basic
import linear_algebra.affine_space.affine_subspace

example (M : Type*) [add_comm_group M] [vector_space ℝ M] (s : affine_subspace ℝ M) :
convex (s : set M) :=
λ x y hx hy a b ha hb hab, (convex.combo_to_vadd hab : a • x + b • y = _).symm ▸ s.2 _ hy hx hx


Last updated: May 16 2021 at 05:21 UTC