feat(analysis/convex/star): Star-convex sets (#10524)

This defines `star_convex 𝕜 x s` to mean that a set is star-convex (aka star-shaped, radially convex, or a star domain) at `x`. This means that every segment from `x` to a point in `s` is a subset of `s`.

Author: YaelDillies

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
 

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

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