import algebra.module
import data.real.basic
import data.set.intervals

variables {α : Type*}
  [add_comm_group α] [vector_space ℝ α]
  (A : set α) (B : set α) (x : α)

open set

def convex (A : set α) :=
∀ {x y : α} {a b : ℝ}, x ∈ A → y ∈ A → 0 ≤ a → 0 ≤ b → a + b = 1 →
a • x  + b • y ∈ A

lemma convex_Ioo (r s : ℝ): convex (Ioo r s) :=
begin
  intros x y a b hx hy ha hb hab,
  wlog h : x ≤ y using [x y a b, y x b a],
end