affine span is convex

Stream: Is there code for X?

[Bhavik Mehta]

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]

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 :
  by rw [sub_smul, one_smul, sub_add_eq_add_sub, smul_sub, add_comm _ x, add_sub_assoc]
... ∈ s : s.2 _ hys hxs hxs

[Bhavik Mehta]

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

[Bhavik Mehta]

Thanks!

[Bhavik Mehta]

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]

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