--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Sun Oct 29 19:39:03 2017 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Mon Oct 30 16:02:59 2017 +0000
@@ -2373,7 +2373,14 @@
qed
corollary connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)"
- by(simp add: convex_connected)
+ by (simp add: convex_connected)
+
+corollary component_complement_connected:
+ fixes S :: "'a::real_normed_vector set"
+ assumes "connected S" "C \<in> components (-S)"
+ shows "connected(-C)"
+ using component_diff_connected [of S UNIV] assms
+ by (auto simp: Compl_eq_Diff_UNIV)
proposition clopen:
fixes S :: "'a :: real_normed_vector set"