[Merged by Bors] - feat(analysis/convex/cone): lemmas about inner_dual_cone of unions

src/analysis/convex/cone.lean

@@ -620,17 +620,37 @@ lemma inner_dual_cone_le_inner_dual_cone (h : t ⊆ s) :
 lemma pointed_inner_dual_cone : s.inner_dual_cone.pointed :=
 λ x hx, by rw inner_zero_right
 
+lemma inner_dual_cone_singleton (x : H) :
+  ({x} : set H).inner_dual_cone = (convex_cone.positive_cone ℝ ℝ).comap (innerₛₗ x) :=
+convex_cone.ext $ λ i, forall_eq
+
+lemma inner_dual_cone_union (s t : set H) :
+  (s ∪ t).inner_dual_cone = s.inner_dual_cone ⊓ t.inner_dual_cone :=
+le_antisymm
+  (le_inf (λ x hx y hy, hx _ $ or.inl hy) (λ x hx y hy, hx _ $ or.inr hy))
+  (λ x hx y, or.rec (hx.1 _) (hx.2 _))
+
+lemma inner_dual_cone_insert (x : H) (s : set H) :
+  (insert x s).inner_dual_cone = set.inner_dual_cone {x} ⊓ s.inner_dual_cone :=
+by rw [insert_eq, inner_dual_cone_union]
+
+lemma inner_dual_cone_Union {ι : Sort*} (f : ι → set H) :
+  (⋃ i, f i).inner_dual_cone = ⨅ i, (f i).inner_dual_cone :=
+begin
+  refine le_antisymm (le_infi $ λ i x hx y hy, hx _ $ mem_Union_of_mem _ hy) _,
+  intros x hx y hy,
+  rw [convex_cone.mem_infi] at hx,
+  obtain ⟨j, hj⟩ := mem_Union.mp hy,
+  exact hx _ _ hj,
+end
+
+lemma inner_dual_cone_sUnion (S : set (set H)) :
+  (⋃₀ S).inner_dual_cone = Inf (set.inner_dual_cone '' S) :=
+by simp_rw [Inf_image, sUnion_eq_bUnion, inner_dual_cone_Union]
+
 /-- The dual cone of `s` equals the intersection of dual cones of the points in `s`. -/
 lemma inner_dual_cone_eq_Inter_inner_dual_cone_singleton :
   (s.inner_dual_cone : set H) = ⋂ i : s, (({i} : set H).inner_dual_cone : set H) :=
-begin
-  simp_rw [set.Inter_coe_set, subtype.coe_mk],
-  refine set.ext (λ x, iff.intro (λ hx, _) _),
-  { refine set.mem_Inter.2 (λ i, set.mem_Inter.2 (λ hi _, _)),
-    rintro ⟨ ⟩,
-    exact hx i hi },
-  { simp only [set.mem_Inter, set_like.mem_coe, mem_inner_dual_cone,
-      set.mem_singleton_iff, forall_eq, imp_self] }
-end
+by rw [←convex_cone.coe_infi, ←inner_dual_cone_Union, Union_of_singleton_coe]
 
 end dual