diff --git a/src/algebra/add_torsor.lean b/src/algebra/add_torsor.lean
index cb175ffbb8011..de3d59f50abf4 100644
--- a/src/algebra/add_torsor.lean
+++ b/src/algebra/add_torsor.lean
@@ -221,7 +221,8 @@ variables {s s' : set G} {t t' : set P}
 @[mono] lemma vadd_subset_vadd (hs : s ⊆ s') (ht : t ⊆ t') : s +ᵥ t ⊆ s' +ᵥ t' :=
 image2_subset hs ht
 
-@[simp] lemma vadd_singleton (s : set G) (p : P) : s +ᵥ {p} = (+ᵥ p) '' s := image2_singleton_right
+@[simp] lemma set_vadd_singleton (s : set G) (p : P) : s +ᵥ {p} = (+ᵥ p) '' s :=
+image2_singleton_right
 
 lemma finite.vadd (hs : finite s) (ht : finite t) : finite (s +ᵥ t) := hs.image2 _ ht
 
diff --git a/src/algebra/pointwise.lean b/src/algebra/pointwise.lean
index e8745cea2a812..564d04fda150f 100644
--- a/src/algebra/pointwise.lean
+++ b/src/algebra/pointwise.lean
@@ -3,11 +3,11 @@ Copyright (c) 2019 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Floris van Doorn
 -/
-import group_theory.submonoid.basic
 import algebra.big_operators.basic
-import group_theory.group_action.group
-import data.set.finite
 import algebra.smul_with_zero
+import data.set.finite
+import group_theory.group_action.group
+import group_theory.submonoid.basic
 
 /-!
 # Pointwise addition, multiplication, and scalar multiplication of sets.
@@ -512,6 +512,10 @@ ext $ λ x, ⟨λ hx, let ⟨p, q, ⟨i, hi⟩, ⟨j, hj⟩, hpq⟩ := set.mem_s
   ⟨(i, j), hpq ▸ hi ▸ hj ▸ rfl⟩,
 λ ⟨⟨i, j⟩, h⟩, set.mem_smul.2 ⟨b i, c j, ⟨i, rfl⟩, ⟨j, rfl⟩, h⟩⟩
 
+@[simp, to_additive]
+lemma smul_singleton [has_scalar α β] (a : α) (b : β) : a • ({b} : set β) = {a • b} :=
+image_singleton
+
 @[simp, to_additive]
 lemma singleton_smul [has_scalar α β] {t : set β} : ({a} : set α) • t = a • t :=
 image2_singleton_left
diff --git a/src/analysis/convex/basic.lean b/src/analysis/convex/basic.lean
index 66145d33801e1..973f28db3aaf3 100644
--- a/src/analysis/convex/basic.lean
+++ b/src/analysis/convex/basic.lean
@@ -785,9 +785,8 @@ calc
   a • x + b • y = (b • y - b • x) + (a • x + b • x) : by abel
             ... = b • (y - x) + x                   : by rw [smul_sub, convex.combo_self h]
 
-lemma convex.sub (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
+lemma convex.sub {s : set (E × E)} (hs : convex 𝕜 s) : convex 𝕜 ((λ x : E × E, x.1 - x.2) '' s) :=
+hs.is_linear_image is_linear_map.is_linear_map_sub
 
 lemma convex_segment (x y : E) : convex 𝕜 [x -[𝕜] y] :=
 begin
diff --git a/src/analysis/convex/star.lean b/src/analysis/convex/star.lean
new file mode 100644
index 0000000000000..547be107fcd83
--- /dev/null
+++ b/src/analysis/convex/star.lean
@@ -0,0 +1,454 @@
+/-
+Copyright (c) 2021 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import analysis.convex.basic
+
+/-!
+# Star-convex sets
+
+This files defines star-convex sets (aka star domains, star-shaped set, radially convex set).
+
+A set is star-convex at `x` if every segment from `x` to a point in the set is contained in the set.
+
+This is the prototypical example of a contractible set in homotopy theory (by scaling every point
+towards `x`), but has wider uses.
+
+Note that this has nothing to do with star rings, `has_star` and co.
+
+## Main declarations
+
+* `star_convex 𝕜 x s`: `s` is star-convex at `x` with scalars `𝕜`.
+
+## Implementation notes
+
+Instead of saying that a set is star-convex, we say a set is star-convex *at a point*. This has the
+advantage of allowing us to talk about convexity as being "everywhere star-convexity" and of making
+the union of star-convex sets be star-convex.
+
+Incidentally, this choice means we don't need to assume a set is nonempty for it to be star-convex.
+Concretely, the empty set is star-convex at every point.
+
+## TODO
+
+Balanced sets are star-convex.
+
+The closure of a star-convex set is star-convex.
+
+Star-convex sets are contractible.
+
+A nonempty open star-convex set in `ℝ^n` is diffeomorphic to the entire space.
+-/
+
+open set
+open_locale convex pointwise
+
+variables {𝕜 E F β : Type*}
+
+section ordered_semiring
+variables [ordered_semiring 𝕜]
+
+section add_comm_monoid
+variables [add_comm_monoid E] [add_comm_monoid F]
+
+section has_scalar
+variables (𝕜) [has_scalar 𝕜 E] [has_scalar 𝕜 F] (x : E) (s : set E)
+
+/-- Star-convexity of sets. `s` is star-convex at `x` if every segment from `x` to a point in `s` is
+contained in `s`. -/
+def star_convex : Prop :=
+∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
+
+variables {𝕜 x s} {t : set E}
+
+lemma convex_iff_forall_star_convex : convex 𝕜 s ↔ ∀ x ∈ s, star_convex 𝕜 x s :=
+forall_congr $ λ x, forall_swap
+
+alias convex_iff_forall_star_convex ↔ convex.star_convex _
+
+lemma star_convex_iff_segment_subset : star_convex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s → [x -[𝕜] y] ⊆ s :=
+begin
+  split,
+  { rintro h y hy z ⟨a, b, ha, hb, hab, rfl⟩,
+    exact h hy ha hb hab },
+  { rintro h y hy a b ha hb hab,
+    exact h hy ⟨a, b, ha, hb, hab, rfl⟩ }
+end
+
+lemma star_convex.segment_subset (h : star_convex 𝕜 x s) {y : E} (hy : y ∈ s) : [x -[𝕜] y] ⊆ s :=
+star_convex_iff_segment_subset.1 h hy
+
+lemma star_convex.open_segment_subset (h : star_convex 𝕜 x s) {y : E} (hy : y ∈ s) :
+  open_segment 𝕜 x y ⊆ s :=
+(open_segment_subset_segment 𝕜 x y).trans (h.segment_subset hy)
+
+/-- Alternative definition of star-convexity, in terms of pointwise set operations. -/
+lemma star_convex_iff_pointwise_add_subset :
+  star_convex 𝕜 x s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • {x} + b • s ⊆ s :=
+begin
+  split,
+  { rintro hA a b ha hb hab w ⟨au, bv, ⟨u, (rfl : u = x), rfl⟩, ⟨v, hv, rfl⟩, rfl⟩,
+    exact hA hv ha hb hab },
+  { rintro h y hy a b ha hb hab,
+    refine h ha hb hab (add_mem_add _ ⟨_, hy, rfl⟩),
+    rw smul_singleton,
+    exact mem_singleton _ }
+end
+
+lemma star_convex_empty (x : E) : star_convex 𝕜 x ∅ := λ y hy, hy.elim
+
+lemma star_convex_univ (x : E) : star_convex 𝕜 x univ := λ _ _ _ _ _ _ _, trivial
+
+lemma star_convex.inter (hs : star_convex 𝕜 x s) (ht : star_convex 𝕜 x t) :
+  star_convex 𝕜 x (s ∩ t) :=
+λ y hy a b ha hb hab, ⟨hs hy.left ha hb hab, ht hy.right ha hb hab⟩
+
+lemma star_convex_sInter {S : set (set E)} (h : ∀ s ∈ S, star_convex 𝕜 x s) :
+  star_convex 𝕜 x (⋂₀ S) :=
+λ y hy a b ha hb hab s hs, h s hs (hy s hs) ha hb hab
+
+lemma star_convex_Inter {ι : Sort*} {s : ι → set E} (h : ∀ i, star_convex 𝕜 x (s i)) :
+  star_convex 𝕜 x (⋂ i, s i) :=
+(sInter_range s) ▸ star_convex_sInter $ forall_range_iff.2 h
+
+lemma star_convex.union (hs : star_convex 𝕜 x s) (ht : star_convex 𝕜 x t) :
+  star_convex 𝕜 x (s ∪ t) :=
+begin
+  rintro y (hy | hy) a b ha hb hab,
+  { exact or.inl (hs hy ha hb hab) },
+  { exact or.inr (ht hy ha hb hab) }
+end
+
+lemma star_convex_Union {ι : Sort*} {s : ι → set E} (hs : ∀ i, star_convex 𝕜 x (s i)) :
+  star_convex 𝕜 x (⋃ i, s i) :=
+begin
+  rintro y hy a b ha hb hab,
+  rw mem_Union at ⊢ hy,
+  obtain ⟨i, hy⟩ := hy,
+  exact ⟨i, hs i hy ha hb hab⟩,
+end
+
+lemma star_convex_sUnion {S : set (set E)} (hS : ∀ s ∈ S, star_convex 𝕜 x s) :
+  star_convex 𝕜 x (⋃₀ S) :=
+begin
+  rw sUnion_eq_Union,
+  exact star_convex_Union (λ s, hS _ s.2),
+end
+
+lemma star_convex.prod {y : F} {s : set E} {t : set F} (hs : star_convex 𝕜 x s)
+  (ht : star_convex 𝕜 y t) :
+  star_convex 𝕜 (x, y) (s.prod t) :=
+λ y hy a b ha hb hab, ⟨hs hy.1 ha hb hab, ht hy.2 ha hb hab⟩
+
+lemma star_convex_pi {ι : Type*} {E : ι → Type*} [Π i, add_comm_monoid (E i)]
+  [Π i, has_scalar 𝕜 (E i)] {x : Π i, E i} {s : set ι} {t : Π i, set (E i)}
+  (ht : ∀ i, star_convex 𝕜 (x i) (t i)) :
+  star_convex 𝕜 x (s.pi t) :=
+λ y hy a b ha hb hab i hi, ht i (hy i hi) ha hb hab
+
+end has_scalar
+
+section module
+variables [module 𝕜 E] [module 𝕜 F] {x y z : E} {s : set E}
+
+lemma star_convex.mem (hs : star_convex 𝕜 x s) (h : s.nonempty) : x ∈ s :=
+begin
+  obtain ⟨y, hy⟩ := h,
+  convert hs hy zero_le_one le_rfl (add_zero 1),
+  rw [one_smul, zero_smul, add_zero],
+end
+
+lemma convex.star_convex_iff (hs : convex 𝕜 s) (h : s.nonempty) : star_convex 𝕜 x s ↔ x ∈ s :=
+⟨λ hxs, hxs.mem h, hs.star_convex _⟩
+
+lemma star_convex_iff_forall_pos (hx : x ∈ s) :
+  star_convex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s :=
+begin
+  refine ⟨λ h y hy a b ha hb hab, h hy ha.le hb.le hab, _⟩,
+  intros h y hy a b ha hb hab,
+  obtain rfl | ha := ha.eq_or_lt,
+  { rw zero_add at hab,
+    rwa [hab, one_smul, zero_smul, zero_add] },
+  obtain rfl | hb := hb.eq_or_lt,
+  { rw add_zero at hab,
+    rwa [hab, one_smul, zero_smul, add_zero] },
+  exact h hy ha hb hab,
+end
+
+lemma star_convex_iff_forall_ne_pos (hx : x ∈ s) :
+  star_convex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 →
+    a • x + b • y ∈ s :=
+begin
+  refine ⟨λ h y hy _ a b ha hb hab, h hy ha.le hb.le hab, _⟩,
+  intros h y hy a b ha hb hab,
+  obtain rfl | ha' := ha.eq_or_lt,
+  { rw [zero_add] at hab, rwa [hab, zero_smul, one_smul, zero_add] },
+  obtain rfl | hb' := hb.eq_or_lt,
+  { rw [add_zero] at hab, rwa [hab, zero_smul, one_smul, add_zero] },
+  obtain rfl | hxy := eq_or_ne x y,
+  { rwa convex.combo_self hab },
+  exact h hy hxy ha' hb' hab,
+end
+
+lemma star_convex_iff_open_segment_subset (hx : x ∈ s) :
+  star_convex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s → open_segment 𝕜 x y ⊆ s :=
+star_convex_iff_segment_subset.trans $ forall_congr $ λ y, forall_congr $ λ hy,
+  (open_segment_subset_iff_segment_subset hx hy).symm
+
+lemma star_convex_singleton (x : E) : star_convex 𝕜 x {x} :=
+begin
+  rintro y (rfl : y = x) a b ha hb hab,
+  exact convex.combo_self hab _,
+end
+
+lemma star_convex.linear_image (hs : star_convex 𝕜 x s) (f : E →ₗ[𝕜] F) :
+  star_convex 𝕜 (f x) (s.image f) :=
+begin
+  intros y hy a b ha hb hab,
+  obtain ⟨y', hy', rfl⟩ := hy,
+  exact ⟨a • x + b • y', hs hy' ha hb hab, by rw [f.map_add, f.map_smul, f.map_smul]⟩,
+end
+
+lemma star_convex.is_linear_image (hs : star_convex 𝕜 x s) {f : E → F} (hf : is_linear_map 𝕜 f) :
+  star_convex 𝕜 (f x) (f '' s) :=
+hs.linear_image $ hf.mk' f
+
+lemma star_convex.linear_preimage {s : set F} (f : E →ₗ[𝕜] F) (hs : star_convex 𝕜 (f x) s) :
+  star_convex 𝕜 x (s.preimage f) :=
+begin
+  intros y hy a b ha hb hab,
+  rw [mem_preimage, f.map_add, f.map_smul, f.map_smul],
+  exact hs hy ha hb hab,
+end
+
+lemma star_convex.is_linear_preimage {s : set F} {f : E → F} (hs : star_convex 𝕜 (f x) s)
+  (hf : is_linear_map 𝕜 f) :
+  star_convex 𝕜 x (preimage f s) :=
+hs.linear_preimage $ hf.mk' f
+
+lemma star_convex.add {t : set E} (hs : star_convex 𝕜 x s) (ht : star_convex 𝕜 y t) :
+  star_convex 𝕜 (x + y) (s + t) :=
+by { rw ←add_image_prod, exact (hs.prod ht).is_linear_image is_linear_map.is_linear_map_add }
+
+lemma star_convex.add_left (hs : star_convex 𝕜 x s) (z : E) :
+  star_convex 𝕜 (z + x) ((λ x, z + x) '' s) :=
+begin
+  intros y hy a b ha hb hab,
+  obtain ⟨y', hy', rfl⟩ := hy,
+  refine ⟨a • x + b • y', hs hy' ha hb hab, _⟩,
+  rw [smul_add, smul_add, add_add_add_comm, ←add_smul, hab, one_smul],
+end
+
+lemma star_convex.add_right (hs : star_convex 𝕜 x s) (z : E) :
+  star_convex 𝕜 (x + z) ((λ x, x + z) '' s) :=
+begin
+  intros y hy a b ha hb hab,
+  obtain ⟨y', hy', rfl⟩ := hy,
+  refine ⟨a • x + b • y', hs hy' ha hb hab, _⟩,
+  rw [smul_add, smul_add, add_add_add_comm, ←add_smul, hab, one_smul],
+end
+
+/-- The translation of a star-convex set is also star-convex. -/
+lemma star_convex.preimage_add_right (hs : star_convex 𝕜 (z + x) s) :
+  star_convex 𝕜 x ((λ x, z + x) ⁻¹' s) :=
+begin
+  intros y hy a b ha hb hab,
+  have h := hs hy ha hb hab,
+  rwa [smul_add, smul_add, add_add_add_comm, ←add_smul, hab, one_smul] at h,
+end
+
+/-- The translation of a star-convex set is also star-convex. -/
+lemma star_convex.preimage_add_left (hs : star_convex 𝕜 (x + z) s) :
+  star_convex 𝕜 x ((λ x, x + z) ⁻¹' s) :=
+begin
+  rw add_comm at hs,
+  simpa only [add_comm] using hs.preimage_add_right,
+end
+
+end module
+end add_comm_monoid
+
+section add_comm_group
+variables [add_comm_group E] [module 𝕜 E] {x y : E}
+
+lemma star_convex.sub {s : set (E × E)} (hs : star_convex 𝕜 (x, y) s) :
+  star_convex 𝕜 (x - y) ((λ x : E × E, x.1 - x.2) '' s) :=
+hs.is_linear_image is_linear_map.is_linear_map_sub
+
+end add_comm_group
+end ordered_semiring
+
+section ordered_comm_semiring
+variables [ordered_comm_semiring 𝕜]
+
+section add_comm_monoid
+variables [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] {x : E} {s : set E}
+
+lemma star_convex.smul (hs : star_convex 𝕜 x s) (c : 𝕜) : star_convex 𝕜 (c • x) (c • s) :=
+hs.linear_image $ linear_map.lsmul _ _ c
+
+lemma star_convex.preimage_smul {c : 𝕜} (hs : star_convex 𝕜 (c • x) s) :
+  star_convex 𝕜 x ((λ z, c • z) ⁻¹' s) :=
+hs.linear_preimage (linear_map.lsmul _ _ c)
+
+lemma star_convex.affinity (hs : star_convex 𝕜 x s) (z : E) (c : 𝕜) :
+  star_convex 𝕜 (z + c • x) ((λ x, z + c • x) '' s) :=
+begin
+  have h := (hs.smul c).add_left z,
+  rwa [←image_smul, image_image] at h,
+end
+
+end add_comm_monoid
+end ordered_comm_semiring
+
+section ordered_ring
+variables [ordered_ring 𝕜]
+
+section add_comm_group
+variables [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] {x y : E} {s : set E}
+
+lemma star_convex.add_smul_mem (hs : star_convex 𝕜 x s) (hy : x + y ∈ s) {t : 𝕜} (ht₀ : 0 ≤ t)
+  (ht₁ : t ≤ 1) :
+  x + t • y ∈ s :=
+begin
+  have h : x + t • y = (1 - t) • x + t • (x + y),
+  { rw [smul_add, ←add_assoc, ←add_smul, sub_add_cancel, one_smul] },
+  rw h,
+  exact hs hy (sub_nonneg_of_le ht₁) ht₀ (sub_add_cancel _ _),
+end
+
+lemma star_convex.smul_mem (hs : star_convex 𝕜 0 s) (hx : x ∈ s) {t : 𝕜} (ht₀ : 0 ≤ t)
+  (ht₁ : t ≤ 1) :
+  t • x ∈ s :=
+by simpa using hs.add_smul_mem (by simpa using hx) ht₀ ht₁
+
+lemma star_convex.add_smul_sub_mem (hs : star_convex 𝕜 x s) (hy : y ∈ s) {t : 𝕜} (ht₀ : 0 ≤ t)
+  (ht₁ : t ≤ 1) :
+  x + t • (y - x) ∈ s :=
+begin
+  apply hs.segment_subset hy,
+  rw segment_eq_image',
+  exact mem_image_of_mem _ ⟨ht₀, ht₁⟩,
+end
+
+/-- The preimage of a star-convex set under an affine map is star-convex. -/
+lemma star_convex.affine_preimage (f : E →ᵃ[𝕜] F) {s : set F} (hs : star_convex 𝕜 (f x) s) :
+  star_convex 𝕜 x (f ⁻¹' s) :=
+begin
+  intros y hy a b ha hb hab,
+  rw [mem_preimage, convex.combo_affine_apply hab],
+  exact hs hy ha hb hab,
+end
+
+/-- The image of a star-convex set under an affine map is star-convex. -/
+lemma star_convex.affine_image (f : E →ᵃ[𝕜] F) {s : set E} (hs : star_convex 𝕜 x s) :
+  star_convex 𝕜 (f x) (f '' s) :=
+begin
+  rintro y ⟨y', ⟨hy', hy'f⟩⟩ a b ha hb hab,
+  refine ⟨a • x + b • y', ⟨hs hy' ha hb hab, _⟩⟩,
+  rw [convex.combo_affine_apply hab, hy'f],
+end
+
+lemma star_convex.neg (hs : star_convex 𝕜 x s) : star_convex 𝕜 (-x) ((λ z, -z) '' s) :=
+hs.is_linear_image is_linear_map.is_linear_map_neg
+
+lemma star_convex.neg_preimage (hs : star_convex 𝕜 (-x) s) : star_convex 𝕜 x ((λ z, -z) ⁻¹' s) :=
+hs.is_linear_preimage is_linear_map.is_linear_map_neg
+
+end add_comm_group
+end ordered_ring
+
+section linear_ordered_field
+variables [linear_ordered_field 𝕜]
+
+section add_comm_group
+variables [add_comm_group E] [module 𝕜 E] {x : E} {s : set E}
+
+/-- Alternative definition of star-convexity, using division. -/
+lemma star_convex_iff_div :
+  star_convex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b →
+    (a / (a + b)) • x + (b / (a + b)) • y ∈ s :=
+⟨λ h y hy a b ha hb hab, begin
+  apply h hy,
+  { have ha', from mul_le_mul_of_nonneg_left ha (inv_pos.2 hab).le,
+    rwa [mul_zero, ←div_eq_inv_mul] at ha' },
+  { have hb', from mul_le_mul_of_nonneg_left hb (inv_pos.2 hab).le,
+    rwa [mul_zero, ←div_eq_inv_mul] at hb' },
+  { rw ←add_div,
+    exact div_self hab.ne' }
+end, λ h y hy a b ha hb hab,
+begin
+  have h', from h hy ha hb,
+  rw [hab, div_one, div_one] at h',
+  exact h' zero_lt_one
+end⟩
+
+lemma star_convex.mem_smul (hs : star_convex 𝕜 0 s) (hx : x ∈ s) {t : 𝕜} (ht : 1 ≤ t) :
+  x ∈ t • s :=
+begin
+  rw mem_smul_set_iff_inv_smul_mem₀ (zero_lt_one.trans_le ht).ne',
+  exact hs.smul_mem hx (inv_nonneg.2 $ zero_le_one.trans ht) (inv_le_one ht),
+end
+
+end add_comm_group
+end linear_ordered_field
+
+/-!
+#### Star-convex sets in an ordered space
+
+Relates `star_convex` and `set.ord_connected`.
+-/
+
+section ord_connected
+
+lemma set.ord_connected.star_convex [ordered_semiring 𝕜] [ordered_add_comm_monoid E]
+  [module 𝕜 E] [ordered_smul 𝕜 E] {x : E} {s : set E} (hs : s.ord_connected) (hx : x ∈ s)
+  (h : ∀ y ∈ s, x ≤ y ∨ y ≤ x) :
+  star_convex 𝕜 x s :=
+begin
+  intros y hy a b ha hb hab,
+  obtain hxy | hyx := h _ hy,
+  { refine hs.out hx hy (mem_Icc.2 ⟨_, _⟩),
+    calc
+      x   = a • x + b • x : (convex.combo_self hab _).symm
+      ... ≤ a • x + b • y : add_le_add_left (smul_le_smul_of_nonneg hxy hb) _,
+    calc
+      a • x + b • y
+          ≤ a • y + b • y : add_le_add_right (smul_le_smul_of_nonneg hxy ha) _
+      ... = y             : convex.combo_self hab _ },
+  { refine hs.out hy hx (mem_Icc.2 ⟨_, _⟩),
+    calc
+      y   = a • y + b • y : (convex.combo_self hab _).symm
+      ... ≤ a • x + b • y : add_le_add_right (smul_le_smul_of_nonneg hyx ha) _,
+    calc
+      a • x + b • y
+          ≤ a • x + b • x : add_le_add_left (smul_le_smul_of_nonneg hyx hb) _
+      ... = x             : convex.combo_self hab _ }
+end
+
+lemma star_convex_iff_ord_connected [linear_ordered_field 𝕜] {x : 𝕜} {s : set 𝕜} (hx : x ∈ s) :
+  star_convex 𝕜 x s ↔ s.ord_connected :=
+by simp_rw [ord_connected_iff_interval_subset_left hx, star_convex_iff_segment_subset,
+  segment_eq_interval]
+
+alias star_convex_iff_ord_connected ↔ star_convex.ord_connected _
+
+end ord_connected
+
+/-! #### Star-convexity of submodules/subspaces -/
+
+section submodule
+open submodule
+
+lemma submodule.star_convex [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E]
+  (K : submodule 𝕜 E) :
+  star_convex 𝕜 (0 : E) K :=
+ K.convex.star_convex _ K.zero_mem
+
+lemma subspace.star_convex [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E]
+  (K : subspace 𝕜 E) :
+  star_convex 𝕜 (0 : E) K :=
+ K.convex.star_convex _ K.zero_mem
+
+end submodule
diff --git a/src/data/set/intervals/ord_connected.lean b/src/data/set/intervals/ord_connected.lean
index 51a0a0d0dcbfe..9fc914f5f2a6b 100644
--- a/src/data/set/intervals/ord_connected.lean
+++ b/src/data/set/intervals/ord_connected.lean
@@ -19,7 +19,7 @@ that all standard intervals are `ord_connected`.
 -/
 
 namespace set
-
+section preorder
 variables {α : Type*} [preorder α] {s t : set α}
 
 /--
@@ -140,19 +140,36 @@ instance [densely_ordered α] {s : set α} [hs : ord_connected s] :
     exact (hs.out a₁.2 a₂.2) (Ioo_subset_Icc_self ⟨ha₁x, hxa₂⟩),
   end ⟩
 
-variables {β : Type*} [linear_order β]
+end preorder
+
+section linear_order
+variables {α : Type*} [linear_order α] {s : set α} {x : α}
 
-@[instance] lemma ord_connected_interval {a b : β} : ord_connected (interval a b) :=
+@[instance] lemma ord_connected_interval {a b : α} : ord_connected (interval a b) :=
 ord_connected_Icc
 
-lemma ord_connected.interval_subset {s : set β} (hs : ord_connected s)
-  ⦃x⦄ (hx : x ∈ s) ⦃y⦄ (hy : y ∈ s) :
+lemma ord_connected.interval_subset (hs : ord_connected s) ⦃x⦄ (hx : x ∈ s) ⦃y⦄ (hy : y ∈ s) :
   interval x y ⊆ s :=
 by cases le_total x y; simp only [interval_of_le, interval_of_ge, *]; apply hs.out; assumption
 
-lemma ord_connected_iff_interval_subset {s : set β} :
+lemma ord_connected_iff_interval_subset :
   ord_connected s ↔ ∀ ⦃x⦄ (hx : x ∈ s) ⦃y⦄ (hy : y ∈ s), interval x y ⊆ s :=
 ⟨λ h, h.interval_subset,
   λ h, ord_connected_iff.2 $ λ x hx y hy hxy, by simpa only [interval_of_le hxy] using h hx hy⟩
 
+lemma ord_connected_iff_interval_subset_left (hx : x ∈ s) :
+  ord_connected s ↔ ∀ ⦃y⦄, y ∈ s → interval x y ⊆ s :=
+begin
+  refine ⟨λ hs, hs.interval_subset hx, λ hs, ord_connected_iff_interval_subset.2 $ λ y hy z hz, _⟩,
+  suffices h : interval y x ∪ interval x z ⊆ s,
+  { exact interval_subset_interval_union_interval.trans h },
+  rw [interval_swap, union_subset_iff],
+  exact ⟨hs hy, hs hz⟩,
+end
+
+lemma ord_connected_iff_interval_subset_right (hx : x ∈ s) :
+  ord_connected s ↔ ∀ ⦃y⦄, y ∈ s → interval y x ⊆ s :=
+by simp_rw [ord_connected_iff_interval_subset_left hx, interval_swap]
+
+end linear_order
 end set
diff --git a/src/data/set/intervals/unordered_interval.lean b/src/data/set/intervals/unordered_interval.lean
index 24c2c018fa20c..35edf1952f0a2 100644
--- a/src/data/set/intervals/unordered_interval.lean
+++ b/src/data/set/intervals/unordered_interval.lean
@@ -32,7 +32,7 @@ namespace set
 
 section linear_order
 
-variables {α : Type u} [linear_order α] {a a₁ a₂ b b₁ b₂ x : α}
+variables {α : Type u} [linear_order α] {a a₁ a₂ b b₁ b₂ c x : α}
 
 /-- `interval a b` is the set of elements lying between `a` and `b`, with `a` and `b` included. -/
 def interval (a b : α) := Icc (min a b) (max a b)
@@ -84,10 +84,10 @@ Icc_subset_interval ⟨ha, hb⟩
 lemma mem_interval_of_ge (hb : b ≤ x) (ha : x ≤ a) : x ∈ [a, b] :=
 Icc_subset_interval' ⟨hb, ha⟩
 
-lemma not_mem_interval_of_lt {c : α} (ha : c < a) (hb : c < b) : c ∉ interval a b :=
+lemma not_mem_interval_of_lt (ha : c < a) (hb : c < b) : c ∉ interval a b :=
 not_mem_Icc_of_lt $ lt_min_iff.mpr ⟨ha, hb⟩
 
-lemma not_mem_interval_of_gt {c : α} (ha : a < c) (hb : b < c) : c ∉ interval a b :=
+lemma not_mem_interval_of_gt (ha : a < c) (hb : b < c) : c ∉ interval a b :=
 not_mem_Icc_of_gt $ max_lt_iff.mpr ⟨ha, hb⟩
 
 lemma interval_subset_interval (h₁ : a₁ ∈ [a₂, b₂]) (h₂ : b₁ ∈ [a₂, b₂]) : [a₁, b₁] ⊆ [a₂, b₂] :=
@@ -109,6 +109,21 @@ interval_subset_interval h right_mem_interval
 lemma interval_subset_interval_left (h : x ∈ [a, b]) : [a, x] ⊆ [a, b] :=
 interval_subset_interval left_mem_interval h
 
+/-- A sort of triangle inequality. -/
+lemma interval_subset_interval_union_interval : [a, c] ⊆ [a, b] ∪ [b, c] :=
+begin
+  rintro x hx,
+  obtain hac | hac := le_total a c,
+  { rw interval_of_le hac at hx,
+    obtain hb | hb := le_total x b,
+    { exact or.inl (mem_interval_of_le hx.1 hb) },
+    { exact or.inr (mem_interval_of_le hb hx.2) } },
+  { rw interval_of_ge hac at hx,
+    obtain hb | hb := le_total x b,
+    { exact or.inr (mem_interval_of_ge hx.1 hb) },
+    { exact or.inl (mem_interval_of_ge hb hx.2) } }
+end
+
 lemma bdd_below_bdd_above_iff_subset_interval (s : set α) :
   bdd_below s ∧ bdd_above s ↔ ∃ a b, s ⊆ [a, b] :=
 begin