diff --git a/src/analysis/calculus/local_extr.lean b/src/analysis/calculus/local_extr.lean
index f81806979a878..17bb55339a19a 100644
--- a/src/analysis/calculus/local_extr.lean
+++ b/src/analysis/calculus/local_extr.lean
@@ -84,14 +84,14 @@ begin
   exact ⟨c, d, mem_of_superset hd $ λ h hn, hst hn, hc, hcd⟩
 end
 
-lemma mem_pos_tangent_cone_at_of_segment_subset {s : set E} {x y : E} (h : segment x y ⊆ s) :
+lemma mem_pos_tangent_cone_at_of_segment_subset {s : set E} {x y : E} (h : segment ℝ x y ⊆ s) :
   y - x ∈ pos_tangent_cone_at s x :=
 begin
   let c := λn:ℕ, (2:ℝ)^n,
   let d := λn:ℕ, (c n)⁻¹ • (y-x),
   refine ⟨c, d, filter.univ_mem' (λn, h _),
     tendsto_pow_at_top_at_top_of_one_lt one_lt_two, _⟩,
-  show x + d n ∈ segment x y,
+  show x + d n ∈ segment ℝ x y,
   { rw segment_eq_image',
     refine ⟨(c n)⁻¹, ⟨_, _⟩, rfl⟩,
     exacts [inv_nonneg.2 (pow_nonneg zero_le_two _),
@@ -103,7 +103,8 @@ begin
     exact pow_ne_zero _ two_ne_zero }
 end
 
-lemma mem_pos_tangent_cone_at_of_segment_subset' {s : set E} {x y : E} (h : segment x (x + y) ⊆ s) :
+lemma mem_pos_tangent_cone_at_of_segment_subset' {s : set E} {x y : E}
+  (h : segment ℝ x (x + y) ⊆ s) :
   y ∈ pos_tangent_cone_at s x :=
 by simpa only [add_sub_cancel'] using mem_pos_tangent_cone_at_of_segment_subset h
 
diff --git a/src/analysis/calculus/mean_value.lean b/src/analysis/calculus/mean_value.lean
index 750cd57d7ff88..fd325bf58dc93 100644
--- a/src/analysis/calculus/mean_value.lean
+++ b/src/analysis/calculus/mean_value.lean
@@ -1083,12 +1083,12 @@ concave_on_open_of_deriv2_nonpos convex_univ is_open_univ hf'.differentiable_on
 theorem domain_mvt
   {f : E → ℝ} {s : set E} {x y : E} {f' : E → (E →L[ℝ] ℝ)}
   (hf : ∀ x ∈ s, has_fderiv_within_at f (f' x) s x) (hs : convex s) (xs : x ∈ s) (ys : y ∈ s) :
-  ∃ z ∈ segment x y, f y - f x = f' z (y - x) :=
+  ∃ z ∈ segment ℝ x y, f y - f x = f' z (y - x) :=
 begin
   have hIccIoo := @Ioo_subset_Icc_self ℝ _ 0 1,
 -- parametrize segment
   set g : ℝ → E := λ t, x + t • (y - x),
-  have hseg : ∀ t ∈ Icc (0:ℝ) 1, g t ∈ segment x y,
+  have hseg : ∀ t ∈ Icc (0:ℝ) 1, g t ∈ segment ℝ x y,
   { rw segment_eq_image',
     simp only [mem_image, and_imp, add_right_inj],
     intros t ht, exact ⟨t, ht, rfl⟩ },
diff --git a/src/analysis/calculus/tangent_cone.lean b/src/analysis/calculus/tangent_cone.lean
index 38976983a7b84..114f612eb32d1 100644
--- a/src/analysis/calculus/tangent_cone.lean
+++ b/src/analysis/calculus/tangent_cone.lean
@@ -208,13 +208,13 @@ end
 
 /-- If a subset of a real vector space contains a segment, then the direction of this
 segment belongs to the tangent cone at its endpoints. -/
-lemma mem_tangent_cone_of_segment_subset {s : set G} {x y : G} (h : segment x y ⊆ s) :
+lemma mem_tangent_cone_of_segment_subset {s : set G} {x y : G} (h : segment ℝ x y ⊆ s) :
   y - x ∈ tangent_cone_at ℝ s x :=
 begin
   let c := λn:ℕ, (2:ℝ)^n,
   let d := λn:ℕ, (c n)⁻¹ • (y-x),
   refine ⟨c, d, filter.univ_mem' (λn, h _), _, _⟩,
-  show x + d n ∈ segment x y,
+  show x + d n ∈ segment ℝ x y,
   { rw segment_eq_image,
     refine ⟨(c n)⁻¹, ⟨_, _⟩, _⟩,
     { rw inv_nonneg, apply pow_nonneg, norm_num },
diff --git a/src/analysis/convex/basic.lean b/src/analysis/convex/basic.lean
index f946328527b96..497872bc64aff 100644
--- a/src/analysis/convex/basic.lean
+++ b/src/analysis/convex/basic.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Alexander Bentkamp. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Alexander Bentkamp, Yury Kudriashov
+Authors: Alexander Bentkamp, Yury Kudriashov, Yaël Dillies
 -/
 import data.complex.module
 import data.set.intervals.image_preimage
@@ -9,13 +9,12 @@ import linear_algebra.affine_space.affine_map
 import order.closure
 
 /-!
-# Convex sets and functions on real vector spaces
+# Convex sets and functions in vector spaces
 
-In a real vector space, we define the following objects and properties.
-
-* `segment x y` is the closed segment joining `x` and `y`.
-* `open_segment x y` is the open segment joining `x` and `y`.
-* A set `s` is `convex` if for any two points `x y ∈ s` it includes `segment x y`;
+In a 𝕜-vector space, we define the following objects and properties.
+* `segment 𝕜 x y` is the closed segment joining `x` and `y`.
+* `open_segment 𝕜 x y` is the open segment joining `x` and `y`.
+* A set `s` is `convex` if for any two points `x y ∈ s` it includes `segment 𝕜 x y`.
 * A function `f : E → β` is `convex_on` a set `s` if `s` is itself a convex set, and for any two
   points `x y ∈ s` the segment joining `(x, f x)` to `(y, f y)` is (non-strictly) above the graph
   of `f`; equivalently, `convex_on f s` means that the epigraph
@@ -29,207 +28,384 @@ We also provide various equivalent versions of the definitions above, prove that
 are convex, and prove Jensen's inequality.
 
 Note: To define convexity for functions `f : E → β`, we need `β` to be an ordered vector space,
-defined using the instance `ordered_smul ℝ β`.
+defined using the instance `ordered_smul 𝕜 β`.
 
 ## Notations
 
-We use the following local notations:
-
-* `I = Icc (0:ℝ) 1`;
-* `[x, y] = segment x y`.
-
-They are defined using `local notation`, so they are not available outside of this file.
+We provide the following notation:
+* `[x -[𝕜] y] = segment 𝕜 x y` in locale `convex`
 
 ## Implementation notes
 
 `convex_hull` is defined as a closure operator. This gives access to the `closure_operator` API
 while the impact on writing code is minimal as `convex_hull s` is automatically elaborated as
 `⇑convex_hull s`.
--/
 
-universes u' u v v' w x
+## TODO
 
-variables {E : Type u} {F : Type v} {ι : Type w} {ι' : Type x} {α : Type v'}
-  [add_comm_group E] [module ℝ E] [add_comm_group F] [module ℝ F]
-  [linear_ordered_field α]
-  {s : set E}
+Generalize all this file to affine spaces.
 
-open set linear_map
-open_locale classical big_operators pointwise
+Should we rename `segment` and `open_segment` to `convex.Icc` and `convex.Ioo`? Should we also
+define `clopen_segment`/`convex.Ico`/`convex.Ioc`?
+-/
 
-local notation `I` := (Icc 0 1 : set ℝ)
+universes u u'
+variables (𝕜 : Type*) {E F : Type*}
 
-section sets
+open linear_map set
+open_locale big_operators classical pointwise
 
 /-! ### Segment -/
 
 /-- Segments in a vector space. -/
-def segment (x y : E) : set E :=
-{z : E | ∃ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), a • x + b • y = z}
+def segment [add_comm_monoid E] [ordered_semiring 𝕜] [has_scalar 𝕜 E] (x y : E) : set E :=
+{z : E | ∃ (a b : 𝕜) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), a • x + b • y = z}
 
-local notation `[`x `, ` y `]` := segment x y
+/-- Open segment in a vector space. Note that `open_segment 𝕜 x x = {x}` instead of being `∅` when
+the base semiring has some element between `0` and `1`. -/
+def open_segment [add_comm_monoid E] [ordered_semiring 𝕜] [has_scalar 𝕜 E] (x y : E) : set E :=
+{z : E | ∃ (a b : 𝕜) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1), a • x + b • y = z}
+
+localized "notation `[` x ` -[` 𝕜 `] ` y `]` := segment 𝕜 x y" in convex
+
+section ordered_semiring
+variables [add_comm_monoid E] [ordered_semiring 𝕜] [module 𝕜 E]
+
+lemma segment_symm (x y : E) : [x -[𝕜] y] = [y -[𝕜] x] :=
+set.ext $ λ z,
+⟨λ ⟨a, b, ha, hb, hab, H⟩, ⟨b, a, hb, ha, (add_comm _ _).trans hab, (add_comm _ _).trans H⟩,
+  λ ⟨a, b, ha, hb, hab, H⟩, ⟨b, a, hb, ha, (add_comm _ _).trans hab, (add_comm _ _).trans H⟩⟩
 
-lemma segment_symm (x y : E) : [x, y] = [y, x] :=
+lemma open_segment_symm (x y : E) :
+  open_segment 𝕜 x y = open_segment 𝕜 y x :=
 set.ext $ λ z,
 ⟨λ ⟨a, b, ha, hb, hab, H⟩, ⟨b, a, hb, ha, (add_comm _ _).trans hab, (add_comm _ _).trans H⟩,
   λ ⟨a, b, ha, hb, hab, H⟩, ⟨b, a, hb, ha, (add_comm _ _).trans hab, (add_comm _ _).trans H⟩⟩
 
-lemma left_mem_segment (x y : E) : x ∈ [x, y] :=
+lemma left_mem_segment (x y : E) : x ∈ [x -[𝕜] y] :=
 ⟨1, 0, zero_le_one, le_refl 0, add_zero 1, by rw [zero_smul, one_smul, add_zero]⟩
 
-lemma right_mem_segment (x y : E) : y ∈ [x, y] :=
-segment_symm y x ▸ left_mem_segment y x
+lemma right_mem_segment (x y : E) : y ∈ [x -[𝕜] y] :=
+segment_symm 𝕜 y x ▸ left_mem_segment 𝕜 y x
 
-lemma segment_same (x : E) : [x, x] = {x} :=
+lemma segment_same (x : E) : [x -[𝕜] x] = {x} :=
 set.ext $ λ z, ⟨λ ⟨a, b, ha, hb, hab, hz⟩,
   by simpa only [(add_smul _ _ _).symm, mem_singleton_iff, hab, one_smul, eq_comm] using hz,
-  λ h, mem_singleton_iff.1 h ▸ left_mem_segment z z⟩
+  λ h, mem_singleton_iff.1 h ▸ left_mem_segment 𝕜 z z⟩
 
-lemma segment_eq_image (x y : E) : [x, y] = (λ θ : ℝ, (1 - θ) • x + θ • y) '' I :=
+lemma open_segment_subset_segment (x y : E) :
+  open_segment 𝕜 x y ⊆ [x -[𝕜] y] :=
+λ z ⟨a, b, ha, hb, hab, hz⟩, ⟨a, b, ha.le, hb.le, hab, hz⟩
+
+lemma mem_open_segment_of_ne_left_right {x y z : E} (hx : x ≠ z) (hy : y ≠ z)
+  (hz : z ∈ [x -[𝕜] y]) :
+  z ∈ open_segment 𝕜 x y :=
+begin
+  obtain ⟨a, b, ha, hb, hab, hz⟩ := hz,
+    by_cases ha' : a = 0,
+  { rw [ha', zero_add] at hab,
+    rw [ha', hab, zero_smul, one_smul, zero_add] at hz,
+    exact (hy hz).elim },
+  by_cases hb' : b = 0,
+  { rw [hb', add_zero] at hab,
+    rw [hb', hab, zero_smul, one_smul, add_zero] at hz,
+    exact (hx hz).elim },
+  exact ⟨a, b, ha.lt_of_ne (ne.symm ha'), hb.lt_of_ne (ne.symm hb'), hab, hz⟩,
+end
+
+variables {𝕜}
+
+lemma open_segment_subset_iff_segment_subset {x y : E} {s : set E} (hx : x ∈ s) (hy : y ∈ s) :
+  open_segment 𝕜 x y ⊆ s ↔ [x -[𝕜] y] ⊆ s :=
+begin
+  refine ⟨λ h z hz, _, (open_segment_subset_segment 𝕜 x y).trans⟩,
+  obtain rfl | hxz := eq_or_ne x z,
+  { exact hx },
+  obtain rfl | hyz := eq_or_ne y z,
+  { exact hy },
+  exact h (mem_open_segment_of_ne_left_right 𝕜 hxz hyz hz),
+end
+
+lemma convex.combo_self {x y : 𝕜} (h : x + y = 1) (a : 𝕜) : x • a + y • a = a :=
+by rw [←add_smul, h, one_smul]
+
+end ordered_semiring
+
+section ordered_ring
+variables [ordered_ring 𝕜]
+
+section add_comm_monoid
+variables [add_comm_monoid E] [module 𝕜 E] [add_comm_monoid F] [module 𝕜 F]
+
+section densely_ordered
+variables [nontrivial 𝕜] [densely_ordered 𝕜]
+
+@[simp] lemma open_segment_same (x : E) :
+  open_segment 𝕜 x x = {x} :=
+set.ext $ λ z, ⟨λ ⟨a, b, ha, hb, hab, hz⟩,
+  by simpa only [← add_smul, mem_singleton_iff, hab, one_smul, eq_comm] using hz,
+  λ (h : z = x), begin
+    obtain ⟨a, ha₀, ha₁⟩ := densely_ordered.dense (0 : 𝕜) 1 zero_lt_one,
+    refine ⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel'_right _ _, _⟩,
+    rw [←add_smul, add_sub_cancel'_right, one_smul, h],
+  end⟩
+
+end densely_ordered
+
+lemma segment_eq_image (x y : E) : [x -[𝕜] y] = (λ θ : 𝕜, (1 - θ) • x + θ • y) '' Icc (0 : 𝕜) 1 :=
 set.ext $ λ z,
   ⟨λ ⟨a, b, ha, hb, hab, hz⟩,
     ⟨b, ⟨hb, hab ▸ le_add_of_nonneg_left ha⟩, hab ▸ hz ▸ by simp only [add_sub_cancel]⟩,
     λ ⟨θ, ⟨hθ₀, hθ₁⟩, hz⟩, ⟨1-θ, θ, sub_nonneg.2 hθ₁, hθ₀, sub_add_cancel _ _, hz⟩⟩
 
-lemma segment_eq_image' (x y : E) : [x, y] = (λ (θ : ℝ), x + θ • (y - x)) '' I :=
-by { convert segment_eq_image x y, ext θ, simp only [smul_sub, sub_smul, one_smul], abel }
-
 lemma segment_eq_image₂ (x y : E) :
-  [x, y] = (λ p : ℝ×ℝ, p.1 • x + p.2 • y) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} :=
+  [x -[𝕜] y] = (λ p : 𝕜 × 𝕜, p.1 • x + p.2 • y) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} :=
 by simp only [segment, image, prod.exists, mem_set_of_eq, exists_prop, and_assoc]
 
-lemma segment_eq_Icc {a b : ℝ} (h : a ≤ b) : [a, b] = Icc a b :=
-begin
-  rw [segment_eq_image'],
-  show (((+) a) ∘ (λ t, t * (b - a))) '' Icc 0 1 = Icc a b,
-  rw [image_comp, image_mul_right_Icc (@zero_le_one ℝ _) (sub_nonneg.2 h), image_const_add_Icc],
-  simp
-end
+lemma open_segment_eq_image (x y : E) :
+  open_segment 𝕜 x y = (λ (θ : 𝕜), (1 - θ) • x + θ • y) '' Ioo (0 : 𝕜) 1 :=
+set.ext $ λ z,
+  ⟨λ ⟨a, b, ha, hb, hab, hz⟩,
+    ⟨b, ⟨hb, hab ▸ lt_add_of_pos_left _ ha⟩, hab ▸ hz ▸ by simp only [add_sub_cancel]⟩,
+    λ ⟨θ, ⟨hθ₀, hθ₁⟩, hz⟩, ⟨1 - θ, θ, sub_pos.2 hθ₁, hθ₀, sub_add_cancel _ _, hz⟩⟩
 
-lemma segment_eq_Icc' (a b : ℝ) : [a, b] = Icc (min a b) (max a b) :=
-by cases le_total a b; [skip, rw segment_symm]; simp [segment_eq_Icc, *]
+lemma open_segment_eq_image₂ (x y : E) :
+  open_segment 𝕜 x y =
+    (λ p : 𝕜 × 𝕜, p.1 • x + p.2 • y) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} :=
+by simp only [open_segment, image, prod.exists, mem_set_of_eq, exists_prop, and_assoc]
 
-lemma segment_eq_interval (a b : ℝ) : segment a b = interval a b :=
-segment_eq_Icc' _ _
+lemma segment_image (f : E →ₗ[𝕜] F) (a b : E) : f '' [a -[𝕜] b] = [f a -[𝕜] f b] :=
+set.ext (λ x, by simp_rw [segment_eq_image, mem_image, exists_exists_and_eq_and, map_add, map_smul])
+
+@[simp] lemma open_segment_image (f : E →ₗ[𝕜] F) (a b : E) :
+  f '' open_segment 𝕜 a b = open_segment 𝕜 (f a) (f b) :=
+set.ext (λ x, by simp_rw [open_segment_eq_image, mem_image, exists_exists_and_eq_and, map_add,
+  map_smul])
+
+end add_comm_monoid
+
+section add_comm_group
+variables [add_comm_group E] [module 𝕜 E]
 
-lemma mem_segment_translate (a : E) {x b c} : a + x ∈ [a + b, a + c] ↔ x ∈ [b, c] :=
+lemma segment_eq_image' (x y : E) :
+  [x -[𝕜] y] = (λ (θ : 𝕜), x + θ • (y - x)) '' Icc (0 : 𝕜) 1 :=
+by { convert segment_eq_image 𝕜 x y, ext θ, simp only [smul_sub, sub_smul, one_smul], abel }
+
+lemma open_segment_eq_image' (x y : E) :
+  open_segment 𝕜 x y = (λ (θ : 𝕜), x + θ • (y - x)) '' Ioo (0 : 𝕜) 1 :=
+by { convert open_segment_eq_image 𝕜 x y, ext θ, simp only [smul_sub, sub_smul, one_smul], abel }
+
+lemma mem_segment_translate (a : E) {x b c} : a + x ∈ [a + b -[𝕜] a + c] ↔ x ∈ [b -[𝕜] c] :=
 begin
   rw [segment_eq_image', segment_eq_image'],
   refine exists_congr (λ θ, and_congr iff.rfl _),
-  simp only [add_sub_add_left_eq_sub, add_assoc, add_right_inj]
+  simp only [add_sub_add_left_eq_sub, add_assoc, add_right_inj],
 end
 
-lemma segment_translate_preimage (a b c : E) : (λ x, a + x) ⁻¹' [a + b, a + c] = [b, c] :=
-set.ext $ λ x, mem_segment_translate a
+@[simp] lemma mem_open_segment_translate (a : E) {x b c : E} :
+  a + x ∈ open_segment 𝕜 (a + b) (a + c) ↔ x ∈ open_segment 𝕜 b c :=
+begin
+  rw [open_segment_eq_image', open_segment_eq_image'],
+  refine exists_congr (λ θ, and_congr iff.rfl _),
+  simp only [add_sub_add_left_eq_sub, add_assoc, add_right_inj],
+end
 
-lemma segment_translate_image (a b c : E) : (λx, a + x) '' [b, c] = [a + b, a + c] :=
-segment_translate_preimage a b c ▸ image_preimage_eq _ $ add_left_surjective a
+lemma segment_translate_preimage (a b c : E) : (λ x, a + x) ⁻¹' [a + b -[𝕜] a + c] = [b -[𝕜] c] :=
+set.ext $ λ x, mem_segment_translate 𝕜 a
 
-lemma segment_image (f : E →ₗ[ℝ] F) (a b : E) : f '' [a, b] = [f a, f b] :=
-set.ext (λ x, by simp [segment_eq_image])
+lemma open_segment_translate_preimage (a b c : E) :
+  (λ x, a + x) ⁻¹' open_segment 𝕜 (a + b) (a + c) = open_segment 𝕜 b c :=
+set.ext $ λ x, mem_open_segment_translate 𝕜 a
 
-/-- Open segment in a vector space. Note that `open_segment x x = {x}` instead of being `∅`. -/
-def open_segment (x y : E) : set E :=
-{z : E | ∃ (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1), a • x + b • y = z}
+lemma segment_translate_image (a b c : E) : (λ x, a + x) '' [b -[𝕜] c] = [a + b -[𝕜] a + c] :=
+segment_translate_preimage 𝕜 a b c ▸ image_preimage_eq _ $ add_left_surjective a
 
-lemma open_segment_subset_segment (x y : E) :
-  open_segment x y ⊆ [x, y] :=
-λ z ⟨a, b, ha, hb, hab, hz⟩, ⟨a, b, ha.le, hb.le, hab, hz⟩
+lemma open_segment_translate_image (a b c : E) :
+  (λ x, a + x) '' open_segment 𝕜 b c = open_segment 𝕜 (a + b) (a + c) :=
+open_segment_translate_preimage 𝕜 a b c ▸ image_preimage_eq _ $ add_left_surjective a
 
-lemma mem_open_segment_of_ne_left_right {x y z : E} (hx : x ≠ z) (hy : y ≠ z) (hz : z ∈ [x, y]) :
-  z ∈ open_segment x y :=
-begin
-  obtain ⟨a, b, ha, hb, hab, hz⟩ := hz,
-  by_cases ha' : a ≠ 0,
-  by_cases hb' : b ≠ 0,
-  { exact ⟨a, b, ha.lt_of_ne (ne.symm ha'), hb.lt_of_ne (ne.symm hb'), hab, hz⟩ },
-  all_goals { simp only [*, add_zero, not_not, one_smul, zero_smul, zero_add] at * }
-end
+end add_comm_group
+end ordered_ring
 
-lemma open_segment_symm (x y : E) :
-  open_segment x y = open_segment y x :=
-set.ext $ λ z,
-⟨λ ⟨a, b, ha, hb, hab, H⟩, ⟨b, a, hb, ha, (add_comm _ _).trans hab, (add_comm _ _).trans H⟩,
-  λ ⟨a, b, ha, hb, hab, H⟩, ⟨b, a, hb, ha, (add_comm _ _).trans hab, (add_comm _ _).trans H⟩⟩
+section linear_ordered_field
+variables [linear_ordered_field 𝕜]
 
-@[simp] lemma open_segment_same (x : E) :
-  open_segment x x = {x} :=
-set.ext $ λ z, ⟨λ ⟨a, b, ha, hb, hab, hz⟩,
-  by simpa only [← add_smul, mem_singleton_iff, hab, one_smul, eq_comm] using hz,
-  λ h, mem_singleton_iff.1 h ▸ ⟨1/2, 1/2, one_half_pos, one_half_pos, add_halves 1,
-    by rw [←add_smul, add_halves, one_smul]⟩⟩
+section add_comm_group
+variables [add_comm_group E] [module 𝕜 E] [add_comm_group F] [module 𝕜 F] {𝕜}
 
-@[simp] lemma left_mem_open_segment_iff {x y : E} :
-  x ∈ open_segment x y ↔ x = y :=
+@[simp] lemma left_mem_open_segment_iff [no_zero_smul_divisors 𝕜 E] {x y : E} :
+  x ∈ open_segment 𝕜 x y ↔ x = y :=
 begin
   split,
   { rintro ⟨a, b, ha, hb, hab, hx⟩,
     refine smul_right_injective _ hb.ne' ((add_right_inj (a • x)).1 _),
     rw [hx, ←add_smul, hab, one_smul] },
-  rintro rfl,
-  simp only [open_segment_same, mem_singleton],
+  { rintro rfl,
+    rw open_segment_same,
+    exact mem_singleton _ }
 end
 
 @[simp] lemma right_mem_open_segment_iff {x y : E} :
-  y ∈ open_segment x y ↔ x = y :=
+  y ∈ open_segment 𝕜 x y ↔ x = y :=
 by rw [open_segment_symm, left_mem_open_segment_iff, eq_comm]
 
-lemma open_segment_eq_image (x y : E) :
-  open_segment x y = (λ (θ : ℝ), (1 - θ) • x + θ • y) '' (Ioo 0 1 : set ℝ) :=
-set.ext $ λ z,
-  ⟨λ ⟨a, b, ha, hb, hab, hz⟩,
-    ⟨b, ⟨hb, hab ▸ lt_add_of_pos_left _ ha⟩, hab ▸ hz ▸ by simp only [add_sub_cancel]⟩,
-    λ ⟨θ, ⟨hθ₀, hθ₁⟩, hz⟩, ⟨1 - θ, θ, sub_pos.2 hθ₁, hθ₀, sub_add_cancel _ _, hz⟩⟩
+end add_comm_group
+end linear_ordered_field
 
-lemma open_segment_eq_image' (x y : E) :
-  open_segment x y = (λ (θ : ℝ), x + θ • (y - x)) '' (Ioo 0 1 : set ℝ) :=
-by { convert open_segment_eq_image x y, ext θ, simp only [smul_sub, sub_smul, one_smul], abel }
+/-!
+#### Segments in an ordered space
+Relates `segment`, `open_segment` and `set.Icc`, `set.Ico`, `set.Ioc`, `set.Ioo`
+-/
+section ordered_semiring
+variables [ordered_semiring 𝕜]
 
-lemma open_segment_eq_image₂ (x y : E) :
-  open_segment x y = (λ p:ℝ×ℝ, p.1 • x + p.2 • y) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} :=
-by simp only [open_segment, image, prod.exists, mem_set_of_eq, exists_prop, and_assoc]
+section ordered_add_comm_monoid
+variables [ordered_add_comm_monoid E] [module 𝕜 E] [ordered_smul 𝕜 E] {𝕜}
 
-@[simp] lemma open_segment_eq_Ioo {a b : ℝ} (h : a < b) :
-  open_segment a b = Ioo a b :=
+lemma segment_subset_Icc {x y : E} (h : x ≤ y) : [x -[𝕜] y] ⊆ Icc x y :=
 begin
-  rw open_segment_eq_image',
-  show (((+) a) ∘ (λ t, t * (b - a))) '' Ioo 0 1 = Ioo a b,
-  rw [image_comp, image_mul_right_Ioo _ _ (sub_pos.2 h), image_const_add_Ioo],
-  simp
+  rintro z ⟨a, b, ha, hb, hab, rfl⟩,
+  split,
+  calc
+    x   = a • x + b • x : by rw [←add_smul, hab, one_smul]
+    ... ≤ a • x + b • y : add_le_add_left (smul_le_smul_of_nonneg h hb) _,
+  calc
+    a • x + b • y
+        ≤ a • y + b • y : add_le_add_right (smul_le_smul_of_nonneg h ha) _
+    ... = y : by rw [←add_smul, hab, one_smul],
 end
 
-lemma open_segment_eq_Ioo' {a b : ℝ} (hab : a ≠ b) :
-  open_segment a b = Ioo (min a b) (max a b) :=
+end ordered_add_comm_monoid
+
+section ordered_cancel_add_comm_monoid
+variables [ordered_cancel_add_comm_monoid E] [module 𝕜 E] [ordered_smul 𝕜 E] {𝕜}
+
+lemma open_segment_subset_Ioo {x y : E} (h : x < y) : open_segment 𝕜 x y ⊆ Ioo x y :=
 begin
-  cases le_total a b,
-  { rw open_segment_eq_Ioo (h.lt_of_ne hab),
-    simp * },
-  rw [open_segment_symm, open_segment_eq_Ioo (h.lt_of_ne hab.symm)],
-  simp *,
+  rintro z ⟨a, b, ha, hb, hab, rfl⟩,
+  split,
+  calc
+    x   = a • x + b • x : by rw [←add_smul, hab, one_smul]
+    ... < a • x + b • y : add_lt_add_left (smul_lt_smul_of_pos h hb) _,
+  calc
+    a • x + b • y
+        < a • y + b • y : add_lt_add_right (smul_lt_smul_of_pos h ha) _
+    ... = y : by rw [←add_smul, hab, one_smul],
 end
 
-@[simp] lemma mem_open_segment_translate (a : E) {x b c : E} :
-  a + x ∈ open_segment (a + b) (a + c)  ↔ x ∈ open_segment b c :=
+end ordered_cancel_add_comm_monoid
+end ordered_semiring
+
+section linear_ordered_field
+variables [linear_ordered_field 𝕜] {𝕜}
+
+lemma Icc_subset_segment {x y : 𝕜} : Icc x y ⊆ [x -[𝕜] y] :=
 begin
-  rw [open_segment_eq_image', open_segment_eq_image'],
-  refine exists_congr (λ θ, and_congr iff.rfl _),
-  simp only [add_sub_add_left_eq_sub, add_assoc, add_right_inj],
+  rintro z ⟨hxz, hyz⟩,
+  obtain rfl | h := (hxz.trans hyz).eq_or_lt,
+  { rw segment_same,
+    exact hyz.antisymm hxz },
+  rw ←sub_nonneg at hxz hyz,
+  rw ←sub_pos at h,
+  refine ⟨(y - z) / (y - x), (z - x) / (y - x), div_nonneg hyz h.le, div_nonneg hxz h.le, _, _⟩,
+  { rw [←add_div, sub_add_sub_cancel, div_self h.ne'] },
+  { rw [smul_eq_mul, smul_eq_mul, ←mul_div_right_comm, ←mul_div_right_comm, ←add_div,
+      div_eq_iff h.ne', add_comm, sub_mul, sub_mul, mul_comm x, sub_add_sub_cancel, mul_sub] }
 end
 
-@[simp] lemma open_segment_translate_preimage (a b c : E) :
-  (λ x, a + x) ⁻¹' open_segment (a + b) (a + c) = open_segment b c :=
-set.ext $ λ x, mem_open_segment_translate a
+@[simp] lemma segment_eq_Icc {x y : 𝕜} (h : x ≤ y) : [x -[𝕜] y] = Icc x y :=
+(segment_subset_Icc h).antisymm Icc_subset_segment
 
-lemma open_segment_translate_image (a b c : E) :
-  (λ x, a + x) '' open_segment b c = open_segment (a + b) (a + c) :=
-open_segment_translate_preimage a b c ▸ image_preimage_eq _ $ add_left_surjective a
+lemma Ioo_subset_open_segment {x y : 𝕜} : Ioo x y ⊆ open_segment 𝕜 x y :=
+λ z hz, mem_open_segment_of_ne_left_right _ hz.1.ne hz.2.ne'
+    (Icc_subset_segment $ Ioo_subset_Icc_self hz)
+
+@[simp] lemma open_segment_eq_Ioo {x y : 𝕜} (h : x < y) : open_segment 𝕜 x y = Ioo x y :=
+(open_segment_subset_Ioo h).antisymm Ioo_subset_open_segment
+
+lemma segment_eq_Icc' (x y : 𝕜) : [x -[𝕜] y] = Icc (min x y) (max x y) :=
+begin
+  cases le_total x y,
+  { rw [segment_eq_Icc h, max_eq_right h, min_eq_left h] },
+  { rw [segment_symm, segment_eq_Icc h, max_eq_left h, min_eq_right h] }
+end
+
+lemma open_segment_eq_Ioo' {x y : 𝕜} (hxy : x ≠ y) :
+  open_segment 𝕜 x y = Ioo (min x y) (max x y) :=
+begin
+  cases hxy.lt_or_lt,
+  { rw [open_segment_eq_Ioo h, max_eq_right h.le, min_eq_left h.le] },
+  { rw [open_segment_symm, open_segment_eq_Ioo h, max_eq_left h.le, min_eq_right h.le] }
+end
+
+lemma segment_eq_interval (x y : 𝕜) : [x -[𝕜] y] = interval x y :=
+segment_eq_Icc' _ _
 
-@[simp] lemma open_segment_image (f : E →ₗ[ℝ] F) (a b : E) :
-  f '' open_segment a b = open_segment (f a) (f b) :=
-set.ext (λ x, by simp [open_segment_eq_image])
+/-- A point is in an `Icc` iff it can be expressed as a convex combination of the endpoints. -/
+lemma convex.mem_Icc {x y : 𝕜} (h : x ≤ y) {z : 𝕜} :
+  z ∈ Icc x y ↔ ∃ (a b : 𝕜), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z :=
+begin
+  rw ←segment_eq_Icc h,
+  simp_rw [←exists_prop],
+  refl,
+end
+
+/-- A point is in an `Ioo` iff it can be expressed as a strict convex combination of the endpoints.
+-/
+lemma convex.mem_Ioo {x y : 𝕜} (h : x < y) {z : 𝕜} :
+  z ∈ Ioo x y ↔ ∃ (a b : 𝕜), 0 < a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z :=
+begin
+  rw ←open_segment_eq_Ioo h,
+  simp_rw [←exists_prop],
+  refl,
+end
+
+/-- A point is in an `Ioc` iff it can be expressed as a semistrict convex combination of the
+endpoints. -/
+lemma convex.mem_Ioc {x y : 𝕜} (h : x < y) {z : 𝕜} :
+  z ∈ Ioc x y ↔ ∃ (a b : 𝕜), 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z :=
+begin
+  split,
+  { rintro hz,
+    obtain ⟨a, b, ha, hb, hab, rfl⟩ := (convex.mem_Icc h.le).1 (Ioc_subset_Icc_self hz),
+    obtain rfl | hb' := hb.eq_or_lt,
+    { rw add_zero at hab,
+      rw [hab, one_mul, zero_mul, add_zero] at hz,
+      exact (hz.1.ne rfl).elim },
+    { exact ⟨a, b, ha, hb', hab, rfl⟩ } },
+  { rintro ⟨a, b, ha, hb, hab, rfl⟩,
+    obtain rfl | ha' := ha.eq_or_lt,
+    { rw zero_add at hab,
+      rwa [hab, one_mul, zero_mul, zero_add, right_mem_Ioc] },
+    { exact Ioo_subset_Ioc_self ((convex.mem_Ioo h).2 ⟨a, b, ha', hb, hab, rfl⟩) } }
+end
+
+/-- A point is in an `Ico` iff it can be expressed as a semistrict convex combination of the
+endpoints. -/
+lemma convex.mem_Ico {x y : 𝕜} (h : x < y) {z : 𝕜} :
+  z ∈ Ico x y ↔ ∃ (a b : 𝕜), 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z :=
+begin
+  split,
+  { rintro hz,
+    obtain ⟨a, b, ha, hb, hab, rfl⟩ := (convex.mem_Icc h.le).1 (Ico_subset_Icc_self hz),
+    obtain rfl | ha' := ha.eq_or_lt,
+    { rw zero_add at hab,
+      rw [hab, one_mul, zero_mul, zero_add] at hz,
+      exact (hz.2.ne rfl).elim },
+    { exact ⟨a, b, ha', hb, hab, rfl⟩ } },
+  { rintro ⟨a, b, ha, hb, hab, rfl⟩,
+    obtain rfl | hb' := hb.eq_or_lt,
+    { rw add_zero at hab,
+      rwa [hab, one_mul, zero_mul, add_zero, left_mem_Ico] },
+    { exact Ioo_subset_Ico_self ((convex.mem_Ioo h).2 ⟨a, b, ha, hb', hab, rfl⟩) } }
+end
+
+end linear_ordered_field
 
 /-! ### Convexity of sets -/
 
+variables {ι ι' : Type*} [add_comm_group E] [module ℝ E] [add_comm_group F] [module ℝ F] {s : set E}
+
 /-- Convexity of sets. -/
 def convex (s : set E) :=
 ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 →
@@ -248,20 +424,20 @@ begin
 end
 
 lemma convex_iff_segment_subset :
-  convex s ↔ ∀ ⦃x y⦄, x ∈ s → y ∈ s → [x, y] ⊆ s :=
+  convex s ↔ ∀ ⦃x y⦄, x ∈ s → y ∈ s → [x -[ℝ] y] ⊆ s :=
 by simp only [convex, segment_eq_image₂, subset_def, ball_image_iff, prod.forall,
   mem_set_of_eq, and_imp]
 
 lemma convex_iff_open_segment_subset :
-  convex s ↔ ∀ ⦃x y⦄, x ∈ s → y ∈ s → open_segment x y ⊆ s :=
+  convex s ↔ ∀ ⦃x y⦄, x ∈ s → y ∈ s → open_segment ℝ x y ⊆ s :=
 by simp only [convex_iff_forall_pos, open_segment_eq_image₂, subset_def, ball_image_iff,
   prod.forall, mem_set_of_eq, and_imp]
 
-lemma convex.segment_subset (h : convex s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) : [x, y] ⊆ s :=
+lemma convex.segment_subset (h : convex s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) : [x -[ℝ] y] ⊆ s :=
 convex_iff_segment_subset.1 h hx hy
 
 lemma convex.open_segment_subset (h : convex s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
-  open_segment x y ⊆ s :=
+  open_segment ℝ x y ⊆ s :=
 convex_iff_open_segment_subset.1 h hx hy
 
 lemma convex.add_smul_sub_mem (h : convex s) {x y : E} (hx : x ∈ s) (hy : y ∈ s)
@@ -322,7 +498,7 @@ end⟩
 
 /-! ### Examples of convex sets -/
 
-lemma convex_empty : convex (∅ : set E) :=  by finish
+lemma convex_empty : convex (∅ : set E) := by finish
 
 lemma convex_singleton (c : E) : convex ({c} : set E) :=
 begin
@@ -437,10 +613,10 @@ hs.linear_image (linear_map.lsmul _ _ c)
 lemma convex.smul_preimage (c : ℝ) (hs : convex s) : convex ((λ z, c • z) ⁻¹' s) :=
 hs.linear_preimage (linear_map.lsmul _ _ c)
 
-lemma convex.add {t : set E}  (hs : convex s) (ht : convex t) : convex (s + t) :=
+lemma convex.add {t : set E} (hs : convex s) (ht : convex t) : convex (s + t) :=
 by { rw ← add_image_prod, exact (hs.prod ht).is_linear_image is_linear_map.is_linear_map_add }
 
-lemma convex.sub {t : set E}  (hs : convex s) (ht : convex t) :
+lemma convex.sub {t : set E} (hs : convex s) (ht : convex t) :
   convex ((λx : E × E, x.1 - x.2) '' (s.prod t)) :=
 (hs.prod ht).is_linear_image is_linear_map.is_linear_map_sub
 
@@ -500,7 +676,7 @@ lemma convex_Ioc (r : ℝ) (s : ℝ) : convex (Ioc r s) := ord_connected_Ioc.con
 lemma convex_Icc (r : ℝ) (s : ℝ) : convex (Icc r s) := ord_connected_Icc.convex
 lemma convex_interval (r : ℝ) (s : ℝ) : convex (interval r s) := ord_connected_interval.convex
 
-lemma convex_segment (a b : E) : convex [a, b] :=
+lemma convex_segment (a b : E) : convex [a -[ℝ] b] :=
 begin
   have : (λ (t : ℝ), a + t • (b - a)) = (λ z : E, a + z) ∘ (λ t : ℝ, t • (b - a)) := rfl,
   rw [segment_eq_image', this, image_comp],
@@ -508,7 +684,7 @@ begin
   exact is_linear_map.is_linear_map_smul' _
 end
 
-lemma convex_open_segment (a b : E) : convex (open_segment a b) :=
+lemma convex_open_segment (a b : E) : convex (open_segment ℝ a b) :=
 begin
   have : (λ (t : ℝ), a + t • (b - a)) = (λ z : E, a + z) ∘ (λ t : ℝ, t • (b - a)) := rfl,
   rw [open_segment_eq_image', this, image_comp],
@@ -564,92 +740,8 @@ convex_halfspace_gt (is_linear_map.mk complex.add_im complex.smul_im) _
 lemma convex_halfspace_im_lge (r : ℝ) : convex {c : ℂ | r ≤ c.im} :=
 convex_halfspace_ge (is_linear_map.mk complex.add_im complex.smul_im) _
 
-/-! ### Convex combinations in intervals -/
-
-lemma convex.combo_self (a : α) {x y : α} (h : x + y = 1) : a = x * a + y * a :=
-calc
-  a   = 1 * a         : by rw [one_mul]
-  ... = (x + y) * a   : by rw [h]
-  ... = x * a + y * a : by rw [add_mul]
-
-/--
-If `x` is in an `Ioo`, it can be expressed as a convex combination of the endpoints.
--/
-lemma convex.mem_Ioo {a b x : α} (h : a < b) :
-  x ∈ Ioo a b ↔ ∃ (x_a x_b : α), 0 < x_a ∧ 0 < x_b ∧ x_a + x_b = 1 ∧ x_a * a + x_b * b = x :=
-begin
-  split,
-  { rintros ⟨h_ax, h_bx⟩,
-    by_cases hab : ¬a < b,
-    { exfalso; exact hab h },
-    { refine ⟨(b-x) / (b-a), (x-a) / (b-a), _⟩,
-      refine ⟨div_pos (by linarith) (by linarith), div_pos (by linarith) (by linarith),_,_⟩;
-      { field_simp [show b - a ≠ 0, by linarith], ring } } },
-  { rw [mem_Ioo],
-    rintros ⟨xa, xb, ⟨hxa, hxb, hxaxb, h₂⟩⟩,
-    rw [←h₂],
-    exact ⟨by nlinarith [convex.combo_self a hxaxb], by nlinarith [convex.combo_self b hxaxb]⟩ }
-end
-
-/-- If `x` is in an `Ioc`, it can be expressed as a convex combination of the endpoints. -/
-lemma convex.mem_Ioc {a b x : α} (h : a < b) :
-  x ∈ Ioc a b ↔ ∃ (x_a x_b : α), 0 ≤ x_a ∧ 0 < x_b ∧ x_a + x_b = 1 ∧ x_a * a + x_b * b = x :=
-begin
-  split,
-  { rintros ⟨h_ax, h_bx⟩,
-    by_cases h_x : x = b,
-    { exact ⟨0, 1, by linarith, by linarith, by ring, by {rw [h_x], ring}⟩ },
-    { rcases (convex.mem_Ioo h).mp ⟨h_ax, lt_of_le_of_ne h_bx h_x⟩ with ⟨x_a, x_b, Ioo_case⟩,
-      exact ⟨x_a, x_b, by linarith, Ioo_case.2⟩ } },
-  { rw [mem_Ioc],
-    rintros ⟨xa, xb, ⟨hxa, hxb, hxaxb, h₂⟩⟩,
-    rw [←h₂],
-    exact ⟨by nlinarith [convex.combo_self a hxaxb], by nlinarith [convex.combo_self b hxaxb]⟩ }
-end
-
-/-- If `x` is in an `Ico`, it can be expressed as a convex combination of the endpoints. -/
-lemma convex.mem_Ico {a b x : α} (h : a < b) :
-  x ∈ Ico a b ↔ ∃ (x_a x_b : α), 0 < x_a ∧ 0 ≤ x_b ∧ x_a + x_b = 1 ∧ x_a * a + x_b * b = x :=
-begin
-  split,
-  { rintros ⟨h_ax, h_bx⟩,
-    by_cases h_x : x = a,
-    { exact ⟨1, 0, by linarith, by linarith, by ring, by {rw [h_x], ring}⟩ },
-    { rcases (convex.mem_Ioo h).mp ⟨lt_of_le_of_ne h_ax (ne.symm h_x), h_bx⟩
-              with ⟨x_a, x_b, Ioo_case⟩,
-      exact ⟨x_a, x_b, Ioo_case.1, by linarith, (Ioo_case.2).2⟩ } },
-  { rw [mem_Ico],
-    rintros ⟨xa, xb, ⟨hxa, hxb, hxaxb, h₂⟩⟩,
-    rw [←h₂],
-    exact ⟨by nlinarith [convex.combo_self a hxaxb], by nlinarith [convex.combo_self b hxaxb]⟩ }
-end
-
-/-- If `x` is in an `Icc`, it can be expressed as a convex combination of the endpoints. -/
-lemma convex.mem_Icc {a b x : α} (h : a ≤ b) :
-  x ∈ Icc a b ↔ ∃ (x_a x_b : α), 0 ≤ x_a ∧ 0 ≤ x_b ∧ x_a + x_b = 1 ∧ x_a * a + x_b * b = x :=
-begin
-  split,
-  { intro x_in_I,
-    rw [Icc, mem_set_of_eq] at x_in_I,
-    rcases x_in_I with ⟨h_ax, h_bx⟩,
-    by_cases hab' : a = b,
-    { exact ⟨0, 1, le_refl 0, by linarith, by ring, by linarith⟩ },
-    change a ≠ b at hab',
-    replace h : a < b, exact lt_of_le_of_ne h hab',
-    by_cases h_x : x = a,
-    { exact ⟨1, 0, by linarith, by linarith, by ring, by {rw [h_x], ring}⟩ },
-    { rcases (convex.mem_Ioc h).mp ⟨lt_of_le_of_ne h_ax (ne.symm h_x), h_bx⟩
-              with ⟨x_a, x_b, Ioo_case⟩,
-      exact ⟨x_a, x_b, Ioo_case.1, by linarith, (Ioo_case.2).2⟩ } },
-  { rw [mem_Icc],
-    rintros ⟨xa, xb, ⟨hxa, hxb, hxaxb, h₂⟩⟩,
-    rw [←h₂],
-    exact ⟨by nlinarith [convex.combo_self a hxaxb], by nlinarith [convex.combo_self b hxaxb]⟩ }
-end
-
 
 section submodule
-
 open submodule
 
 lemma submodule.convex (K : submodule ℝ E) : convex (↑K : set E) :=
@@ -659,8 +751,6 @@ lemma subspace.convex (K : subspace ℝ E) : convex (↑K : set E) := K.convex
 
 end submodule
 
-end sets
-
 /-! ### Convex and concave functions -/
 
 section functions
@@ -722,7 +812,7 @@ lemma concave_on_const (c : β) (hs : convex s) : concave_on s (λ x:E, c) :=
 variables {t : set E}
 
 lemma convex_on_iff_div {f : E → β} :
-  convex_on s f ↔ convex s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀  ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → 0 < a + b →
+  convex_on s f ↔ convex s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → 0 < a + b →
     f ((a/(a+b)) • x + (b/(a+b)) • y) ≤ (a/(a+b)) • f x + (b/(a+b)) • f y :=
 and_congr iff.rfl
 ⟨begin
@@ -737,7 +827,7 @@ begin
 end⟩
 
 lemma concave_on_iff_div {f : E → β} :
-  concave_on s f ↔ convex s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀  ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → 0 < a + b →
+  concave_on s f ↔ convex s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → 0 < a + b →
     (a/(a+b)) • f x + (b/(a+b)) • f y ≤ f ((a/(a+b)) • x + (b/(a+b)) • y) :=
 @convex_on_iff_div _ _ _ _ (order_dual β) _ _ _
 
@@ -962,13 +1052,13 @@ lemma concave_on.le_on_segment' (hf : concave_on s f) {x y : E} {a b : ℝ}
 
 /-- A convex function on a segment is upper-bounded by the max of its endpoints. -/
 lemma convex_on.le_on_segment (hf : convex_on s f) {x y z : E}
-  (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ [x, y]) :
+  (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ [x -[ℝ] y]) :
   f z ≤ max (f x) (f y) :=
 let ⟨a, b, ha, hb, hab, hz⟩ := hz in hz ▸ hf.le_on_segment' hx hy ha hb hab
 
 /-- A concave function on a segment is lower-bounded by the min of its endpoints. -/
 lemma concave_on.le_on_segment {f : E → γ} (hf : concave_on s f) {x y z : E}
-  (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ [x, y]) :
+  (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ [x -[ℝ] y]) :
     min (f x) (f y) ≤ f z :=
 @convex_on.le_on_segment _ _ _ _ (order_dual γ) _ _ _ f hf x y z hx hy hz
 
@@ -1014,7 +1104,7 @@ lemma concave_on.le_right_of_left_le' (hf : concave_on s f) {x y : E} {a b : ℝ
 @convex_on.le_right_of_left_le' _ _ _ _ (order_dual γ) _ _ _ f hf x y a b hx hy ha hb hab hxy
 
 lemma convex_on.le_left_of_right_le (hf : convex_on s f) {x y z : E} (hx : x ∈ s)
-  (hy : y ∈ s) (hz : z ∈ open_segment x y) (hyz : f y ≤ f z) :
+  (hy : y ∈ s) (hz : z ∈ open_segment ℝ x y) (hyz : f y ≤ f z) :
   f z ≤ f x :=
 begin
   obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz,
@@ -1022,12 +1112,12 @@ begin
 end
 
 lemma concave_on.left_le_of_le_right (hf : concave_on s f) {x y z : E} (hx : x ∈ s)
-  (hy : y ∈ s) (hz : z ∈ open_segment x y) (hyz : f z ≤ f y) :
+  (hy : y ∈ s) (hz : z ∈ open_segment ℝ x y) (hyz : f z ≤ f y) :
   f x ≤ f z :=
 @convex_on.le_left_of_right_le _ _ _ _ (order_dual γ) _ _ _ f hf x y z hx hy hz hyz
 
 lemma convex_on.le_right_of_left_le (hf : convex_on s f) {x y z : E} (hx : x ∈ s)
-  (hy : y ∈ s) (hz : z ∈ open_segment x y) (hxz : f x ≤ f z) :
+  (hy : y ∈ s) (hz : z ∈ open_segment ℝ x y) (hxz : f x ≤ f z) :
   f z ≤ f y :=
 begin
   obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz,
@@ -1035,7 +1125,7 @@ begin
 end
 
 lemma concave_on.le_right_of_left_le (hf : concave_on s f) {x y z : E} (hx : x ∈ s)
-  (hy : y ∈ s) (hz : z ∈ open_segment x y) (hxz : f z ≤ f x) :
+  (hy : y ∈ s) (hz : z ∈ open_segment ℝ x y) (hxz : f z ≤ f x) :
   f y ≤ f z :=
 @convex_on.le_right_of_left_le _ _ _ _ (order_dual γ) _ _ _ f hf x y z hx hy hz hxz
 
@@ -1167,12 +1257,12 @@ hf.comp_affine_map $ affine_map.const ℝ E a +ᵥ affine_map.id ℝ E
 /-- If a function is convex on `s`, it remains convex after a translation. -/
 lemma convex_on.translate_left {f : E → β} {s : set E} {a : E} (hf : convex_on s f) :
   convex_on ((λ z, a + z) ⁻¹' s) (f ∘ (λ z, z + a)) :=
-by simpa only [add_comm] using  hf.translate_right
+by simpa only [add_comm] using hf.translate_right
 
 /-- If a function is concave on `s`, it remains concave after a translation. -/
 lemma concave_on.translate_left {f : E → β} {s : set E} {a : E} (hf : concave_on s f) :
   concave_on ((λ z, a + z) ⁻¹' s) (f ∘ (λ z, z + a)) :=
-by simpa only [add_comm] using  hf.translate_right
+by simpa only [add_comm] using hf.translate_right
 
 end functions
 
@@ -1525,7 +1615,7 @@ begin
       apply_rules [add_nonneg, mul_nonneg, hwx₀, hwy₀], },
     { simp only [finset.sum_add_distrib, finset.mul_sum.symm, mul_one, *] } },
   { rintros _ ⟨w, hw₀, hw₁, rfl⟩,
-    exact s.center_mass_mem_convex_hull (λ x hx, hw₀ _  hx)
+    exact s.center_mass_mem_convex_hull (λ x hx, hw₀ _ hx)
       (hw₁.symm ▸ zero_lt_one) (λ x hx, hx) }
 end
 
@@ -1539,7 +1629,7 @@ lemma convex_hull_eq_union_convex_hull_finite_subsets (s : set E) :
   convex_hull s = ⋃ (t : finset E) (w : ↑t ⊆ s), convex_hull ↑t :=
 begin
   refine subset.antisymm _ _,
-  { rw [convex_hull_eq.{u}],
+  { rw convex_hull_eq,
     rintros x ⟨ι, t, w, z, hw₀, hw₁, hz, rfl⟩,
     simp only [mem_Union],
     refine ⟨t.image z, _, _⟩,
@@ -1628,7 +1718,7 @@ end
 
 /-- All values of a function `f ∈ std_simplex ι` belong to `[0, 1]`. -/
 lemma mem_Icc_of_mem_std_simplex (hf : f ∈ std_simplex ι) (x) :
-  f x ∈ I :=
+  f x ∈ Icc (0 : ℝ) 1 :=
 ⟨hf.1 x, hf.2 ▸ finset.single_le_sum (λ y hy, hf.1 y) (finset.mem_univ x)⟩
 
 end simplex
diff --git a/src/analysis/convex/extreme.lean b/src/analysis/convex/extreme.lean
index 5cf0df95d33c3..9170fc0379219 100644
--- a/src/analysis/convex/extreme.lean
+++ b/src/analysis/convex/extreme.lean
@@ -49,7 +49,7 @@ variables {E : Type*} [add_comm_group E] [module ℝ E] {x : E} {A B C : set E}
 /-- A set `B` is an extreme subset of `A` if `B ⊆ A` and all points of `B` only belong to open
 segments whose ends are in `B`. -/
 def is_extreme (A B : set E) : Prop :=
-B ⊆ A ∧ ∀ x₁ x₂ ∈ A, ∀ x ∈ B, x ∈ open_segment x₁ x₂ → x₁ ∈ B ∧ x₂ ∈ B
+B ⊆ A ∧ ∀ x₁ x₂ ∈ A, ∀ x ∈ B, x ∈ open_segment ℝ x₁ x₂ → x₁ ∈ B ∧ x₂ ∈ B
 
 namespace is_extreme
 
@@ -136,16 +136,16 @@ end is_extreme
 /-- A point `x` is an extreme point of a set `A` if `x` belongs to no open segment with ends in
 `A`, except for the obvious `open_segment x x`. -/
 def set.extreme_points (A : set E) : set E :=
-{x ∈ A | ∀ (x₁ x₂ ∈ A), x ∈ open_segment x₁ x₂ → x₁ = x ∧ x₂ = x}
+{x ∈ A | ∀ (x₁ x₂ ∈ A), x ∈ open_segment ℝ x₁ x₂ → x₁ = x ∧ x₂ = x}
 
 lemma extreme_points_def :
-  x ∈ A.extreme_points ↔ x ∈ A ∧ ∀ (x₁ x₂ ∈ A), x ∈ open_segment x₁ x₂ → x₁ = x ∧ x₂ = x :=
+  x ∈ A.extreme_points ↔ x ∈ A ∧ ∀ (x₁ x₂ ∈ A), x ∈ open_segment ℝ x₁ x₂ → x₁ = x ∧ x₂ = x :=
 iff.rfl
 
 /-- A useful restatement using `segment`: `x` is an extreme point iff the only (closed) segments
 that contain it are those with `x` as one of their endpoints. -/
 lemma mem_extreme_points_iff_forall_segment :
-  x ∈ A.extreme_points ↔ x ∈ A ∧ ∀ (x₁ x₂ ∈ A), x ∈ segment x₁ x₂ → x₁ = x ∨ x₂ = x :=
+  x ∈ A.extreme_points ↔ x ∈ A ∧ ∀ (x₁ x₂ ∈ A), x ∈ segment ℝ x₁ x₂ → x₁ = x ∨ x₂ = x :=
 begin
   split,
   { rintro ⟨hxA, hAx⟩,
@@ -153,11 +153,11 @@ begin
     rintro x₁ x₂ hx₁ hx₂ hx,
     by_contra,
     push_neg at h,
-    exact h.1 (hAx _ _ hx₁ hx₂ (mem_open_segment_of_ne_left_right h.1 h.2 hx)).1 },
+    exact h.1 (hAx _ _ hx₁ hx₂ (mem_open_segment_of_ne_left_right ℝ h.1 h.2 hx)).1 },
   rintro ⟨hxA, hAx⟩,
   use hxA,
   rintro x₁ x₂ hx₁ hx₂ hx,
-  obtain rfl | rfl := hAx x₁ x₂ hx₁ hx₂ (open_segment_subset_segment _ _ hx),
+  obtain rfl | rfl := hAx x₁ x₂ hx₁ hx₂ (open_segment_subset_segment ℝ _ _ hx),
   { exact ⟨rfl, (left_mem_open_segment_iff.1 hx).symm⟩ },
   exact ⟨right_mem_open_segment_iff.1 hx, rfl⟩,
 end
diff --git a/src/data/set/intervals/unordered_interval.lean b/src/data/set/intervals/unordered_interval.lean
index 7cfc5a2ec5d35..4673fb7071a52 100644
--- a/src/data/set/intervals/unordered_interval.lean
+++ b/src/data/set/intervals/unordered_interval.lean
@@ -16,7 +16,7 @@ In any decidable linear order `α`, we define the set of elements lying between
 interval as defined in this file is always the set of things lying between `a` and `b`, regardless
 of the relative order of `a` and `b`.
 
-For real numbers, `Icc (min a b) (max a b)` is the same as `segment a b`.
+For real numbers, `Icc (min a b) (max a b)` is the same as `segment ℝ a b`.
 
 ## Notation