feat(analysis/convex/basic): missing lemmas (#7946)

- the union of a set/indexed family of convex sets is convex
- `open_segment a b` is convex
- a set is nonempty iff its convex hull is

src/analysis/convex/basic.lean

@@ -10,7 +10,6 @@ import linear_algebra.affine_space.affine_map
 import algebra.module.ordered
 import order.closure
 
-
 /-!
 # Convex sets and functions on real vector spaces
 
@@ -320,7 +319,7 @@ lemma convex_sInter {S : set (set E)} (h : ∀ s ∈ S, convex s) : convex (⋂
 assume x y hx hy a b ha hb hab s hs,
 h s hs (hx s hs) (hy s hs) ha hb hab
 
-lemma convex_Inter {ι : Sort*} {s: ι → set E} (h: ∀ i : ι, convex (s i)) : convex (⋂ i, s i) :=
+lemma convex_Inter {ι : Sort*} {s : ι → set E} (h : ∀ i : ι, convex (s i)) : convex (⋂ i, s i) :=
 (sInter_range s) ▸ convex_sInter $ forall_range_iff.2 h
 
 lemma convex.prod {s : set E} {t : set F} (hs : convex s) (ht : convex t) :
@@ -332,6 +331,26 @@ begin
         ht (mem_prod.1 hx).2 (mem_prod.1 hy).2 ha hb hab⟩
 end
 
+lemma directed.convex_Union {ι : Sort*} {s : ι → set E} (hdir : directed has_subset.subset s)
+  (hc : ∀ ⦃i : ι⦄, convex (s i)) :
+  convex (⋃ i, s i) :=
+begin
+  rintro x y hx hy a b ha hb hab,
+  rw mem_Union at ⊢ hx hy,
+  obtain ⟨i, hx⟩ := hx,
+  obtain ⟨j, hy⟩ := hy,
+  obtain ⟨k, hik, hjk⟩ := hdir i j,
+  exact ⟨k, hc (hik hx) (hjk hy) ha hb hab⟩,
+end
+
+lemma directed_on.convex_sUnion {c : set (set E)} (hdir : directed_on has_subset.subset c)
+  (hc : ∀ ⦃A : set E⦄, A ∈ c → convex A) :
+  convex (⋃₀c) :=
+begin
+  rw sUnion_eq_Union,
+  exact (directed_on_iff_directed.1 hdir).convex_Union (λ A, hc A.2),
+end
+
 lemma convex.combo_to_vadd {a b : ℝ} {x y : E} (h : a + b = 1) :
   a • x + b • y = b • (y - x) + x :=
 calc
@@ -437,12 +456,20 @@ lemma convex_interval (r : ℝ) (s : ℝ) : convex (interval r s) := ord_connect
 
 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,
+  have : (λ (t : ℝ), a + t • (b - a)) = (λ z : E, a + z) ∘ (λ t : ℝ, t • (b - a)) := rfl,
   rw [segment_eq_image', this, image_comp],
   refine ((convex_Icc _ _).is_linear_image _).translate _,
   exact is_linear_map.is_linear_map_smul' _
 end
 
+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],
+  refine ((convex_Ioo _ _).is_linear_image _).translate _,
+  exact is_linear_map.is_linear_map_smul' _,
+end
+
 lemma convex_halfspace_lt {f : E → ℝ} (h : is_linear_map ℝ f) (r : ℝ) :
   convex {w | f w < r} :=
 (convex_Iio r).is_linear_preimage h
@@ -1316,6 +1343,13 @@ begin
     exact convex_hull_empty }
 end
 
+@[simp] lemma convex_hull_nonempty_iff :
+  (convex_hull s).nonempty ↔ s.nonempty :=
+begin
+  rw [←ne_empty_iff_nonempty, ←ne_empty_iff_nonempty, ne.def, ne.def],
+  exact not_congr convex_hull_empty_iff,
+end
+
 @[simp]
 lemma convex_hull_singleton {x : E} : convex_hull ({x} : set E) = {x} :=
 (convex_singleton x).convex_hull_eq