src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 66939 04678058308f
parent 66884 c2128ab11f61
child 67135 1a94352812f4
     1.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sun Oct 29 19:39:03 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Oct 30 16:02:59 2017 +0000
     1.3 @@ -2373,7 +2373,14 @@
     1.4  qed
     1.5  
     1.6  corollary connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)"
     1.7 -  by(simp add: convex_connected)
     1.8 +  by (simp add: convex_connected)
     1.9 +
    1.10 +corollary component_complement_connected:
    1.11 +  fixes S :: "'a::real_normed_vector set"
    1.12 +  assumes "connected S" "C \<in> components (-S)"
    1.13 +  shows "connected(-C)"
    1.14 +  using component_diff_connected [of S UNIV] assms
    1.15 +  by (auto simp: Compl_eq_Diff_UNIV)
    1.16  
    1.17  proposition clopen:
    1.18    fixes S :: "'a :: real_normed_vector set"