new material on path_component_sets, inside, outside, etc. And more default simprules
authorpaulson <lp15@cam.ac.uk>
Tue Oct 13 12:42:08 2015 +0100 (2015-10-13)
changeset 61426d53db136e8fd
parent 61425 fb95d06fb21f
child 61427 3c69ea85f8dd
new material on path_component_sets, inside, outside, etc. And more default simprules
NEWS
src/HOL/Library/Convex.thy
src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Path_Connected.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/NEWS	Tue Oct 13 09:21:21 2015 +0200
     1.2 +++ b/NEWS	Tue Oct 13 12:42:08 2015 +0100
     1.3 @@ -344,7 +344,7 @@
     1.4    - Always generate "case_transfer" theorem.
     1.5  
     1.6  * Transfer:
     1.7 -  - new methods for interactive debugging of 'transfer' and 
     1.8 +  - new methods for interactive debugging of 'transfer' and
     1.9      'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end',
    1.10      'transfer_prover_start' and 'transfer_prover_end'.
    1.11  
    1.12 @@ -408,8 +408,11 @@
    1.13      less_eq_multiset_def
    1.14      INCOMPATIBILITY
    1.15  
    1.16 -* Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals and Cauchy's integral theorem,
    1.17 -    ported from HOL Light
    1.18 +* Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals and Cauchy's
    1.19 +integral theorem, ported from HOL Light
    1.20 +
    1.21 +* Multivariate_Analysis: Added topological concepts such as connected components
    1.22 +and the inside or outside of a set.
    1.23  
    1.24  * Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef'
    1.25  command. Minor INCOMPATIBILITY, use 'function' instead.
     2.1 --- a/src/HOL/Library/Convex.thy	Tue Oct 13 09:21:21 2015 +0200
     2.2 +++ b/src/HOL/Library/Convex.thy	Tue Oct 13 12:42:08 2015 +0100
     2.3 @@ -43,7 +43,7 @@
     2.4      unfolding convex_def by auto
     2.5  qed (auto simp: convex_def)
     2.6  
     2.7 -lemma mem_convex:
     2.8 +lemma convexD_alt:
     2.9    assumes "convex s" "a \<in> s" "b \<in> s" "0 \<le> u" "u \<le> 1"
    2.10    shows "((1 - u) *\<^sub>R a + u *\<^sub>R b) \<in> s"
    2.11    using assms unfolding convex_alt by auto
     3.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Tue Oct 13 09:21:21 2015 +0200
     3.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Tue Oct 13 12:42:08 2015 +0100
     3.3 @@ -1259,7 +1259,7 @@
     3.4      shows "midpoint x y \<in> convex hull s"
     3.5  proof -
     3.6    have "(1 - inverse(2)) *\<^sub>R x + inverse(2) *\<^sub>R y \<in> convex hull s"
     3.7 -    apply (rule mem_convex)
     3.8 +    apply (rule convexD_alt)
     3.9      using assms
    3.10      apply (auto simp: convex_convex_hull)
    3.11      done
    3.12 @@ -1649,7 +1649,7 @@
    3.13      apply (simp add: segment_convex_hull)
    3.14      apply (rule convex_hull_subset)
    3.15      using assms
    3.16 -    apply (auto simp: hull_inc c' Convex.mem_convex)
    3.17 +    apply (auto simp: hull_inc c' Convex.convexD_alt)
    3.18      done
    3.19  qed
    3.20  
    3.21 @@ -1666,7 +1666,7 @@
    3.22      apply (simp_all add: segment_convex_hull)
    3.23      apply (rule_tac [!] convex_hull_subset)
    3.24      using assms
    3.25 -    apply (auto simp: hull_inc c' Convex.mem_convex)
    3.26 +    apply (auto simp: hull_inc c' Convex.convexD_alt)
    3.27      done
    3.28    show ?thesis
    3.29      apply (rule path_integral_unique)
     4.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Oct 13 09:21:21 2015 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Oct 13 12:42:08 2015 +0100
     4.3 @@ -522,9 +522,6 @@
     4.4    proof (rule complex_taylor [of "closed_segment 0 z" n 
     4.5                                   "\<lambda>k x. (-1)^(k div 2) * (if even k then sin x else cos x)" 
     4.6                                   "exp\<bar>Im z\<bar>" 0 z,  simplified])
     4.7 -  show "convex (closed_segment 0 z)"
     4.8 -    by (rule convex_segment [of 0 z])
     4.9 -  next
    4.10      fix k x
    4.11      show "((\<lambda>x. (- 1) ^ (k div 2) * (if even k then sin x else cos x)) has_field_derivative
    4.12              (- 1) ^ (Suc k div 2) * (if odd k then sin x else cos x))
    4.13 @@ -537,13 +534,6 @@
    4.14      assume "x \<in> closed_segment 0 z"
    4.15      then show "cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \<le> exp \<bar>Im z\<bar>"
    4.16        by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
    4.17 -  next
    4.18 -    show "0 \<in> closed_segment 0 z"
    4.19 -      by (auto simp: closed_segment_def)
    4.20 -  next
    4.21 -    show "z \<in> closed_segment 0 z"
    4.22 -      apply (simp add: closed_segment_def scaleR_conv_of_real)
    4.23 -      using of_real_1 zero_le_one by blast
    4.24    qed
    4.25    have **: "\<And>k. complex_of_real (sin_coeff k) * z ^ k
    4.26              = (-1)^(k div 2) * (if even k then sin 0 else cos 0) * z^k / of_nat (fact k)"
    4.27 @@ -565,9 +555,6 @@
    4.28             \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
    4.29    proof (rule complex_taylor [of "closed_segment 0 z" n "\<lambda>k x. (-1)^(Suc k div 2) * (if even k then cos x else sin x)" "exp\<bar>Im z\<bar>" 0 z,
    4.30  simplified])
    4.31 -  show "convex (closed_segment 0 z)"
    4.32 -    by (rule convex_segment [of 0 z])
    4.33 -  next
    4.34      fix k x
    4.35      assume "x \<in> closed_segment 0 z" "k \<le> n"
    4.36      show "((\<lambda>x. (- 1) ^ (Suc k div 2) * (if even k then cos x else sin x)) has_field_derivative
    4.37 @@ -581,13 +568,6 @@
    4.38      assume "x \<in> closed_segment 0 z"
    4.39      then show "cmod ((- 1) ^ Suc (n div 2) * (if odd n then cos x else sin x)) \<le> exp \<bar>Im z\<bar>"
    4.40        by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
    4.41 -  next
    4.42 -    show "0 \<in> closed_segment 0 z"
    4.43 -      by (auto simp: closed_segment_def)
    4.44 -  next
    4.45 -    show "z \<in> closed_segment 0 z"
    4.46 -      apply (simp add: closed_segment_def scaleR_conv_of_real)
    4.47 -      using of_real_1 zero_le_one by blast
    4.48    qed
    4.49    have **: "\<And>k. complex_of_real (cos_coeff k) * z ^ k
    4.50              = (-1)^(Suc k div 2) * (if even k then cos 0 else sin 0) * z^k / of_nat (fact k)"
     5.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Oct 13 09:21:21 2015 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Oct 13 12:42:08 2015 +0100
     5.3 @@ -1305,7 +1305,7 @@
     5.4  
     5.5  lemma connectedD:
     5.6    "connected S \<Longrightarrow> open A \<Longrightarrow> open B \<Longrightarrow> S \<subseteq> A \<union> B \<Longrightarrow> A \<inter> B \<inter> S = {} \<Longrightarrow> A \<inter> S = {} \<or> B \<inter> S = {}"
     5.7 -  by (metis connected_def)
     5.8 +  by (rule Topological_Spaces.topological_space_class.connectedD)
     5.9  
    5.10  lemma convex_connected:
    5.11    fixes s :: "'a::real_normed_vector set"
    5.12 @@ -1332,10 +1332,8 @@
    5.13    ultimately show False by auto
    5.14  qed
    5.15  
    5.16 -text \<open>One rather trivial consequence.\<close>
    5.17 -
    5.18 -lemma connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)"
    5.19 -  by(simp add: convex_connected convex_UNIV)
    5.20 +corollary connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)"
    5.21 +  by(simp add: convex_connected)
    5.22  
    5.23  text \<open>Balls, being convex, are connected.\<close>
    5.24  
    5.25 @@ -3318,7 +3316,7 @@
    5.26    moreover have c: "c \<in> S"
    5.27      using assms rel_interior_subset by auto
    5.28    moreover from c have "x - e *\<^sub>R (x - c) \<in> S"
    5.29 -    using mem_convex[of S x c e]
    5.30 +    using convexD_alt[of S x c e]
    5.31      apply (simp add: algebra_simps)
    5.32      using assms
    5.33      apply auto
    5.34 @@ -3920,7 +3918,7 @@
    5.35            "0 \<le> c \<and> c \<le> 1" "u \<in> s" "finite t" "t \<subseteq> s" "card t \<le> n"  "v \<in> convex hull t"
    5.36            by auto
    5.37          moreover have "(1 - c) *\<^sub>R u + c *\<^sub>R v \<in> convex hull insert u t"
    5.38 -          apply (rule mem_convex)
    5.39 +          apply (rule convexD_alt)
    5.40            using obt(2) and convex_convex_hull and hull_subset[of "insert u t" convex]
    5.41            using obt(7) and hull_mono[of t "insert u t"]
    5.42            apply auto
    5.43 @@ -4263,7 +4261,7 @@
    5.44      using closer_point_lemma[of a x y] by auto
    5.45    let ?z = "(1 - u) *\<^sub>R x + u *\<^sub>R y"
    5.46    have "?z \<in> s"
    5.47 -    using mem_convex[OF assms(1,3,4), of u] using u by auto
    5.48 +    using convexD_alt[OF assms(1,3,4), of u] using u by auto
    5.49    then show False
    5.50      using assms(5)[THEN bspec[where x="?z"]] and u(3)
    5.51      by (auto simp add: dist_commute algebra_simps)
    5.52 @@ -5486,7 +5484,7 @@
    5.53        by (simp add: dist_norm inverse_eq_divide norm_minus_commute)
    5.54      with assms(3) have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> s" ..
    5.55      with assms(1) have "(1 - u) *\<^sub>R ((y - u *\<^sub>R x) /\<^sub>R (1 - u)) + u *\<^sub>R x \<in> s"
    5.56 -      using \<open>x \<in> s\<close> \<open>0 \<le> u\<close> \<open>u < 1\<close> [THEN less_imp_le] by (rule mem_convex)
    5.57 +      using \<open>x \<in> s\<close> \<open>0 \<le> u\<close> \<open>u < 1\<close> [THEN less_imp_le] by (rule convexD_alt)
    5.58      then show "y \<in> s" using \<open>u < 1\<close>
    5.59        by simp
    5.60    qed
    5.61 @@ -6345,10 +6343,15 @@
    5.62      done
    5.63  qed
    5.64  
    5.65 -lemma convex_segment: "convex (closed_segment a b)"
    5.66 +lemma convex_segment [iff]: "convex (closed_segment a b)"
    5.67    unfolding segment_convex_hull by(rule convex_convex_hull)
    5.68  
    5.69 -lemma ends_in_segment: "a \<in> closed_segment a b" "b \<in> closed_segment a b"
    5.70 +lemma connected_segment [iff]:
    5.71 +  fixes x :: "'a :: real_normed_vector"
    5.72 +  shows "connected (closed_segment x y)"
    5.73 +  by (simp add: convex_connected)
    5.74 +
    5.75 +lemma ends_in_segment [iff]: "a \<in> closed_segment a b" "b \<in> closed_segment a b"
    5.76    unfolding segment_convex_hull
    5.77    apply (rule_tac[!] hull_subset[unfolded subset_eq, rule_format])
    5.78    apply auto
     6.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Tue Oct 13 09:21:21 2015 +0200
     6.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Tue Oct 13 12:42:08 2015 +0100
     6.3 @@ -942,6 +942,9 @@
     6.4  definition "path_component s x y \<longleftrightarrow>
     6.5    (\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)"
     6.6  
     6.7 +abbreviation
     6.8 +   "path_component_set s x \<equiv> Collect (path_component s x)"
     6.9 +
    6.10  lemmas path_defs = path_def pathstart_def pathfinish_def path_image_def path_component_def
    6.11  
    6.12  lemma path_component_mem:
    6.13 @@ -972,8 +975,7 @@
    6.14    done
    6.15  
    6.16  lemma path_component_trans:
    6.17 -  assumes "path_component s x y"
    6.18 -    and "path_component s y z"
    6.19 +  assumes "path_component s x y" and "path_component s y z"
    6.20    shows "path_component s x z"
    6.21    using assms
    6.22    unfolding path_component_def
    6.23 @@ -985,23 +987,36 @@
    6.24  lemma path_component_of_subset: "s \<subseteq> t \<Longrightarrow> path_component s x y \<Longrightarrow> path_component t x y"
    6.25    unfolding path_component_def by auto
    6.26  
    6.27 +lemma path_connected_linepath:
    6.28 +    fixes s :: "'a::real_normed_vector set"
    6.29 +    shows "closed_segment a b \<subseteq> s \<Longrightarrow> path_component s a b"
    6.30 +  apply (simp add: path_component_def)
    6.31 +  apply (rule_tac x="linepath a b" in exI, auto)
    6.32 +  done
    6.33 +
    6.34  
    6.35  text \<open>Can also consider it as a set, as the name suggests.\<close>
    6.36  
    6.37  lemma path_component_set:
    6.38 -  "{y. path_component s x y} =
    6.39 +  "path_component_set s x =
    6.40      {y. (\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)}"
    6.41 -  unfolding mem_Collect_eq path_component_def
    6.42 -  apply auto
    6.43 -  done
    6.44 +  by (auto simp: path_component_def)
    6.45  
    6.46 -lemma path_component_subset: "{y. path_component s x y} \<subseteq> s"
    6.47 +lemma path_component_subset: "path_component_set s x \<subseteq> s"
    6.48    by (auto simp add: path_component_mem(2))
    6.49  
    6.50 -lemma path_component_eq_empty: "{y. path_component s x y} = {} \<longleftrightarrow> x \<notin> s"
    6.51 +lemma path_component_eq_empty: "path_component_set s x = {} \<longleftrightarrow> x \<notin> s"
    6.52    using path_component_mem path_component_refl_eq
    6.53      by fastforce
    6.54  
    6.55 +lemma path_component_mono:
    6.56 +     "s \<subseteq> t \<Longrightarrow> (path_component_set s x) \<subseteq> (path_component_set t x)"
    6.57 +  by (simp add: Collect_mono path_component_of_subset)
    6.58 +
    6.59 +lemma path_component_eq:
    6.60 +   "y \<in> path_component_set s x \<Longrightarrow> path_component_set s y = path_component_set s x"
    6.61 +by (metis (no_types, lifting) Collect_cong mem_Collect_eq path_component_sym path_component_trans)
    6.62 +
    6.63  subsection \<open>Path connectedness of a space\<close>
    6.64  
    6.65  definition "path_connected s \<longleftrightarrow>
    6.66 @@ -1010,10 +1025,13 @@
    6.67  lemma path_connected_component: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. path_component s x y)"
    6.68    unfolding path_connected_def path_component_def by auto
    6.69  
    6.70 -lemma path_connected_component_set: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. {y. path_component s x y} = s)"
    6.71 -  unfolding path_connected_component path_component_subset
    6.72 -  apply auto
    6.73 -  using path_component_mem(2) by blast
    6.74 +lemma path_connected_component_set: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. path_component_set s x = s)"
    6.75 +  unfolding path_connected_component path_component_subset 
    6.76 +  using path_component_mem by blast
    6.77 +
    6.78 +lemma path_component_maximal:
    6.79 +     "\<lbrakk>x \<in> t; path_connected t; t \<subseteq> s\<rbrakk> \<Longrightarrow> t \<subseteq> (path_component_set s x)"
    6.80 +  by (metis path_component_mono path_connected_component_set)
    6.81  
    6.82  subsection \<open>Some useful lemmas about path-connectedness\<close>
    6.83  
    6.84 @@ -1069,11 +1087,11 @@
    6.85  lemma open_path_component:
    6.86    fixes s :: "'a::real_normed_vector set"
    6.87    assumes "open s"
    6.88 -  shows "open {y. path_component s x y}"
    6.89 +  shows "open (path_component_set s x)"
    6.90    unfolding open_contains_ball
    6.91  proof
    6.92    fix y
    6.93 -  assume as: "y \<in> {y. path_component s x y}"
    6.94 +  assume as: "y \<in> path_component_set s x"
    6.95    then have "y \<in> s"
    6.96      apply -
    6.97      apply (rule path_component_mem(2))
    6.98 @@ -1083,7 +1101,7 @@
    6.99    then obtain e where e: "e > 0" "ball y e \<subseteq> s"
   6.100      using assms[unfolded open_contains_ball]
   6.101      by auto
   6.102 -  show "\<exists>e > 0. ball y e \<subseteq> {y. path_component s x y}"
   6.103 +  show "\<exists>e > 0. ball y e \<subseteq> path_component_set s x"
   6.104      apply (rule_tac x=e in exI)
   6.105      apply (rule,rule \<open>e>0\<close>)
   6.106      apply rule
   6.107 @@ -1105,15 +1123,15 @@
   6.108  lemma open_non_path_component:
   6.109    fixes s :: "'a::real_normed_vector set"
   6.110    assumes "open s"
   6.111 -  shows "open (s - {y. path_component s x y})"
   6.112 +  shows "open (s - path_component_set s x)"
   6.113    unfolding open_contains_ball
   6.114  proof
   6.115    fix y
   6.116 -  assume as: "y \<in> s - {y. path_component s x y}"
   6.117 +  assume as: "y \<in> s - path_component_set s x"
   6.118    then obtain e where e: "e > 0" "ball y e \<subseteq> s"
   6.119      using assms [unfolded open_contains_ball]
   6.120      by auto
   6.121 -  show "\<exists>e>0. ball y e \<subseteq> s - {y. path_component s x y}"
   6.122 +  show "\<exists>e>0. ball y e \<subseteq> s - path_component_set s x"
   6.123      apply (rule_tac x=e in exI)
   6.124      apply rule
   6.125      apply (rule \<open>e>0\<close>)
   6.126 @@ -1122,8 +1140,8 @@
   6.127      defer
   6.128    proof (rule ccontr)
   6.129      fix z
   6.130 -    assume "z \<in> ball y e" "\<not> z \<notin> {y. path_component s x y}"
   6.131 -    then have "y \<in> {y. path_component s x y}"
   6.132 +    assume "z \<in> ball y e" "\<not> z \<notin> path_component_set s x"
   6.133 +    then have "y \<in> path_component_set s x"
   6.134        unfolding not_not mem_Collect_eq using \<open>e>0\<close>
   6.135        apply -
   6.136        apply (rule path_component_trans, assumption)
   6.137 @@ -1145,17 +1163,17 @@
   6.138  proof (rule, rule, rule path_component_subset, rule)
   6.139    fix x y
   6.140    assume "x \<in> s" and "y \<in> s"
   6.141 -  show "y \<in> {y. path_component s x y}"
   6.142 +  show "y \<in> path_component_set s x"
   6.143    proof (rule ccontr)
   6.144      assume "\<not> ?thesis"
   6.145 -    moreover have "{y. path_component s x y} \<inter> s \<noteq> {}"
   6.146 +    moreover have "path_component_set s x \<inter> s \<noteq> {}"
   6.147        using \<open>x \<in> s\<close> path_component_eq_empty path_component_subset[of s x]
   6.148        by auto
   6.149      ultimately
   6.150      show False
   6.151        using \<open>y \<in> s\<close> open_non_path_component[OF assms(1)] open_path_component[OF assms(1)]
   6.152        using assms(2)[unfolded connected_def not_ex, rule_format,
   6.153 -        of"{y. path_component s x y}" "s - {y. path_component s x y}"]
   6.154 +        of "path_component_set s x" "s - path_component_set s x"]
   6.155        by auto
   6.156    qed
   6.157  qed
   6.158 @@ -1239,12 +1257,91 @@
   6.159      by (rule path_component_trans)
   6.160  qed
   6.161  
   6.162 +lemma path_component_path_image_pathstart:
   6.163 +  assumes p: "path p" and x: "x \<in> path_image p"
   6.164 +  shows "path_component (path_image p) (pathstart p) x"
   6.165 +using x
   6.166 +proof (clarsimp simp add: path_image_def)
   6.167 +  fix y
   6.168 +  assume "x = p y" and y: "0 \<le> y" "y \<le> 1"
   6.169 +  show "path_component (p ` {0..1}) (pathstart p) (p y)"
   6.170 +  proof (cases "y=0")
   6.171 +    case True then show ?thesis
   6.172 +      by (simp add: path_component_refl_eq pathstart_def)
   6.173 +  next
   6.174 +    case False have "continuous_on {0..1} (p o (op*y))"
   6.175 +      apply (rule continuous_intros)+
   6.176 +      using p [unfolded path_def] y
   6.177 +      apply (auto simp: mult_le_one intro: continuous_on_subset [of _ p])
   6.178 +      done
   6.179 +    then have "path (\<lambda>u. p (y * u))"
   6.180 +      by (simp add: path_def)
   6.181 +    then show ?thesis
   6.182 +      apply (simp add: path_component_def)
   6.183 +      apply (rule_tac x = "\<lambda>u. p (y * u)" in exI)
   6.184 +      apply (intro conjI)
   6.185 +      using y False
   6.186 +      apply (auto simp: mult_le_one pathstart_def pathfinish_def path_image_def)
   6.187 +      done
   6.188 +  qed
   6.189 +qed
   6.190 +
   6.191 +lemma path_connected_path_image: "path p \<Longrightarrow> path_connected(path_image p)"
   6.192 +  unfolding path_connected_component
   6.193 +  by (meson path_component_path_image_pathstart path_component_sym path_component_trans)
   6.194 +
   6.195 +lemma path_connected_path_component:
   6.196 +   "path_connected (path_component_set s x)"
   6.197 +proof -
   6.198 +  { fix y z
   6.199 +    assume pa: "path_component s x y" "path_component s x z"
   6.200 +    then have pae: "path_component_set s x = path_component_set s y"
   6.201 +      using path_component_eq by auto
   6.202 +    have yz: "path_component s y z"
   6.203 +      using pa path_component_sym path_component_trans by blast
   6.204 +    then have "\<exists>g. path g \<and> path_image g \<subseteq> path_component_set s x \<and> pathstart g = y \<and> pathfinish g = z"
   6.205 +      apply (simp add: path_component_def, clarify)
   6.206 +      apply (rule_tac x=g in exI)
   6.207 +      by (simp add: pae path_component_maximal path_connected_path_image pathstart_in_path_image)
   6.208 +  }
   6.209 +  then show ?thesis
   6.210 +    by (simp add: path_connected_def)
   6.211 +qed
   6.212 +
   6.213 +lemma path_component: "path_component s x y \<longleftrightarrow> (\<exists>t. path_connected t \<and> t \<subseteq> s \<and> x \<in> t \<and> y \<in> t)"
   6.214 +  apply (intro iffI)
   6.215 +  apply (metis path_connected_path_image path_defs(5) pathfinish_in_path_image pathstart_in_path_image)
   6.216 +  using path_component_of_subset path_connected_component by blast
   6.217 +
   6.218 +lemma path_component_path_component [simp]:
   6.219 +   "path_component_set (path_component_set s x) x = path_component_set s x"
   6.220 +proof (cases "x \<in> s")
   6.221 +  case True show ?thesis
   6.222 +    apply (rule subset_antisym)
   6.223 +    apply (simp add: path_component_subset)
   6.224 +    by (simp add: True path_component_maximal path_component_refl path_connected_path_component)
   6.225 +next
   6.226 +  case False then show ?thesis
   6.227 +    by (metis False empty_iff path_component_eq_empty)
   6.228 +qed
   6.229 +
   6.230 +lemma path_component_subset_connected_component:
   6.231 +   "(path_component_set s x) \<subseteq> (connected_component_set s x)"
   6.232 +proof (cases "x \<in> s")
   6.233 +  case True show ?thesis
   6.234 +    apply (rule connected_component_maximal)
   6.235 +    apply (auto simp: True path_component_subset path_component_refl path_connected_imp_connected path_connected_path_component)
   6.236 +    done
   6.237 +next
   6.238 +  case False then show ?thesis
   6.239 +    using path_component_eq_empty by auto
   6.240 +qed
   6.241  
   6.242  subsection \<open>Sphere is path-connected\<close>
   6.243  
   6.244  lemma path_connected_punctured_universe:
   6.245    assumes "2 \<le> DIM('a::euclidean_space)"
   6.246 -  shows "path_connected ((UNIV::'a set) - {a})"
   6.247 +  shows "path_connected (- {a::'a})"
   6.248  proof -
   6.249    let ?A = "{x::'a. \<exists>i\<in>Basis. x \<bullet> i < a \<bullet> i}"
   6.250    let ?B = "{x::'a. \<exists>i\<in>Basis. a \<bullet> i < x \<bullet> i}"
   6.251 @@ -1287,7 +1384,7 @@
   6.252    also have "\<dots> = {x. x \<noteq> a}"
   6.253      unfolding euclidean_eq_iff [where 'a='a]
   6.254      by (simp add: Bex_def)
   6.255 -  also have "\<dots> = UNIV - {a}"
   6.256 +  also have "\<dots> = - {a}"
   6.257      by auto
   6.258    finally show ?thesis .
   6.259  qed
   6.260 @@ -1316,7 +1413,7 @@
   6.261      using r
   6.262      apply (auto simp add: scaleR_right_diff_distrib)
   6.263      done
   6.264 -  have **: "{x::'a. norm x = 1} = (\<lambda>x. (1/norm x) *\<^sub>R x) ` (UNIV - {0})"
   6.265 +  have **: "{x::'a. norm x = 1} = (\<lambda>x. (1/norm x) *\<^sub>R x) ` (- {0})"
   6.266      apply (rule set_eqI)
   6.267      apply rule
   6.268      unfolding image_iff
   6.269 @@ -1324,7 +1421,7 @@
   6.270      unfolding mem_Collect_eq
   6.271      apply (auto split: split_if_asm)
   6.272      done
   6.273 -  have "continuous_on (UNIV - {0}) (\<lambda>x::'a. 1 / norm x)"
   6.274 +  have "continuous_on (- {0}) (\<lambda>x::'a. 1 / norm x)"
   6.275      by (auto intro!: continuous_intros)
   6.276    then show ?thesis
   6.277      unfolding * **
   6.278 @@ -1332,8 +1429,630 @@
   6.279      by (auto intro!: path_connected_continuous_image continuous_intros)
   6.280  qed
   6.281  
   6.282 -lemma connected_sphere: "2 \<le> DIM('a::euclidean_space) \<Longrightarrow> connected {x::'a. norm (x - a) = r}"
   6.283 +corollary connected_sphere: "2 \<le> DIM('a::euclidean_space) \<Longrightarrow> connected {x::'a. norm (x - a) = r}"
   6.284    using path_connected_sphere path_connected_imp_connected
   6.285    by auto
   6.286  
   6.287 +corollary path_connected_complement_bounded_convex:
   6.288 +    fixes s :: "'a :: euclidean_space set"
   6.289 +    assumes "bounded s" "convex s" and 2: "2 \<le> DIM('a)"
   6.290 +    shows "path_connected (- s)"
   6.291 +proof (cases "s={}")
   6.292 +  case True then show ?thesis
   6.293 +    using convex_imp_path_connected by auto
   6.294 +next
   6.295 +  case False
   6.296 +  then obtain a where "a \<in> s" by auto
   6.297 +  { fix x y assume "x \<notin> s" "y \<notin> s"
   6.298 +    then have "x \<noteq> a" "y \<noteq> a" using `a \<in> s` by auto
   6.299 +    then have bxy: "bounded(insert x (insert y s))"
   6.300 +      by (simp add: `bounded s`)
   6.301 +    then obtain B::real where B: "0 < B" and Bx: "norm (a - x) < B" and By: "norm (a - y) < B"
   6.302 +                          and "s \<subseteq> ball a B"
   6.303 +      using bounded_subset_ballD [OF bxy, of a] by (auto simp: dist_norm)
   6.304 +    def C == "B / norm(x - a)"
   6.305 +    { fix u
   6.306 +      assume u: "(1 - u) *\<^sub>R x + u *\<^sub>R (a + C *\<^sub>R (x - a)) \<in> s" and "0 \<le> u" "u \<le> 1"
   6.307 +      have CC: "1 \<le> 1 + (C - 1) * u"
   6.308 +        using `x \<noteq> a` `0 \<le> u`
   6.309 +        apply (simp add: C_def divide_simps norm_minus_commute)
   6.310 +        by (metis Bx diff_le_iff(1) less_eq_real_def mult_nonneg_nonneg)
   6.311 +      have *: "\<And>v. (1 - u) *\<^sub>R x + u *\<^sub>R (a + v *\<^sub>R (x - a)) = a + (1 + (v - 1) * u) *\<^sub>R (x - a)"
   6.312 +        by (simp add: algebra_simps)
   6.313 +      have "a + ((1 / (1 + C * u - u)) *\<^sub>R x + ((u / (1 + C * u - u)) *\<^sub>R a + (C * u / (1 + C * u - u)) *\<^sub>R x)) =
   6.314 +            (1 + (u / (1 + C * u - u))) *\<^sub>R a + ((1 / (1 + C * u - u)) + (C * u / (1 + C * u - u))) *\<^sub>R x"
   6.315 +        by (simp add: algebra_simps)
   6.316 +      also have "... = (1 + (u / (1 + C * u - u))) *\<^sub>R a + (1 + (u / (1 + C * u - u))) *\<^sub>R x"
   6.317 +        using CC by (simp add: field_simps)
   6.318 +      also have "... = x + (1 + (u / (1 + C * u - u))) *\<^sub>R a + (u / (1 + C * u - u)) *\<^sub>R x"
   6.319 +        by (simp add: algebra_simps)
   6.320 +      also have "... = x + ((1 / (1 + C * u - u)) *\<^sub>R a +
   6.321 +              ((u / (1 + C * u - u)) *\<^sub>R x + (C * u / (1 + C * u - u)) *\<^sub>R a))"
   6.322 +        using CC by (simp add: field_simps) (simp add: add_divide_distrib scaleR_add_left)
   6.323 +      finally have xeq: "(1 - 1 / (1 + (C - 1) * u)) *\<^sub>R a + (1 / (1 + (C - 1) * u)) *\<^sub>R (a + (1 + (C - 1) * u) *\<^sub>R (x - a)) = x"
   6.324 +        by (simp add: algebra_simps)
   6.325 +      have False
   6.326 +        using `convex s`
   6.327 +        apply (simp add: convex_alt)
   6.328 +        apply (drule_tac x=a in bspec)
   6.329 +         apply (rule  `a \<in> s`)
   6.330 +        apply (drule_tac x="a + (1 + (C - 1) * u) *\<^sub>R (x - a)" in bspec)
   6.331 +         using u apply (simp add: *)
   6.332 +        apply (drule_tac x="1 / (1 + (C - 1) * u)" in spec)
   6.333 +        using `x \<noteq> a` `x \<notin> s` `0 \<le> u` CC
   6.334 +        apply (auto simp: xeq)
   6.335 +        done
   6.336 +    }
   6.337 +    then have pcx: "path_component (- s) x (a + C *\<^sub>R (x - a))"
   6.338 +      by (force simp: closed_segment_def intro!: path_connected_linepath)
   6.339 +    def D == "B / norm(y - a)"  --{*massive duplication with the proof above*}
   6.340 +    { fix u
   6.341 +      assume u: "(1 - u) *\<^sub>R y + u *\<^sub>R (a + D *\<^sub>R (y - a)) \<in> s" and "0 \<le> u" "u \<le> 1"
   6.342 +      have DD: "1 \<le> 1 + (D - 1) * u"
   6.343 +        using `y \<noteq> a` `0 \<le> u`
   6.344 +        apply (simp add: D_def divide_simps norm_minus_commute)
   6.345 +        by (metis By diff_le_iff(1) less_eq_real_def mult_nonneg_nonneg)
   6.346 +      have *: "\<And>v. (1 - u) *\<^sub>R y + u *\<^sub>R (a + v *\<^sub>R (y - a)) = a + (1 + (v - 1) * u) *\<^sub>R (y - a)"
   6.347 +        by (simp add: algebra_simps)
   6.348 +      have "a + ((1 / (1 + D * u - u)) *\<^sub>R y + ((u / (1 + D * u - u)) *\<^sub>R a + (D * u / (1 + D * u - u)) *\<^sub>R y)) =
   6.349 +            (1 + (u / (1 + D * u - u))) *\<^sub>R a + ((1 / (1 + D * u - u)) + (D * u / (1 + D * u - u))) *\<^sub>R y"
   6.350 +        by (simp add: algebra_simps)
   6.351 +      also have "... = (1 + (u / (1 + D * u - u))) *\<^sub>R a + (1 + (u / (1 + D * u - u))) *\<^sub>R y"
   6.352 +        using DD by (simp add: field_simps)
   6.353 +      also have "... = y + (1 + (u / (1 + D * u - u))) *\<^sub>R a + (u / (1 + D * u - u)) *\<^sub>R y"
   6.354 +        by (simp add: algebra_simps)
   6.355 +      also have "... = y + ((1 / (1 + D * u - u)) *\<^sub>R a +
   6.356 +              ((u / (1 + D * u - u)) *\<^sub>R y + (D * u / (1 + D * u - u)) *\<^sub>R a))"
   6.357 +        using DD by (simp add: field_simps) (simp add: add_divide_distrib scaleR_add_left)
   6.358 +      finally have xeq: "(1 - 1 / (1 + (D - 1) * u)) *\<^sub>R a + (1 / (1 + (D - 1) * u)) *\<^sub>R (a + (1 + (D - 1) * u) *\<^sub>R (y - a)) = y"
   6.359 +        by (simp add: algebra_simps)
   6.360 +      have False
   6.361 +        using `convex s`
   6.362 +        apply (simp add: convex_alt)
   6.363 +        apply (drule_tac x=a in bspec)
   6.364 +         apply (rule  `a \<in> s`)
   6.365 +        apply (drule_tac x="a + (1 + (D - 1) * u) *\<^sub>R (y - a)" in bspec)
   6.366 +         using u apply (simp add: *)
   6.367 +        apply (drule_tac x="1 / (1 + (D - 1) * u)" in spec)
   6.368 +        using `y \<noteq> a` `y \<notin> s` `0 \<le> u` DD
   6.369 +        apply (auto simp: xeq)
   6.370 +        done
   6.371 +    }
   6.372 +    then have pdy: "path_component (- s) y (a + D *\<^sub>R (y - a))"
   6.373 +      by (force simp: closed_segment_def intro!: path_connected_linepath)
   6.374 +    have pyx: "path_component (- s) (a + D *\<^sub>R (y - a)) (a + C *\<^sub>R (x - a))"
   6.375 +      apply (rule path_component_of_subset [of "{x. norm(x - a) = B}"])
   6.376 +       using `s \<subseteq> ball a B`
   6.377 +       apply (force simp: ball_def dist_norm norm_minus_commute)
   6.378 +      apply (rule path_connected_sphere [OF 2, of a B, simplified path_connected_component, rule_format])
   6.379 +      using `x \<noteq> a`  using `y \<noteq> a`  B apply (auto simp: C_def D_def)
   6.380 +      done
   6.381 +    have "path_component (- s) x y"
   6.382 +      by (metis path_component_trans path_component_sym pcx pdy pyx)
   6.383 +  }
   6.384 +  then show ?thesis
   6.385 +    by (auto simp: path_connected_component)
   6.386 +qed
   6.387 +
   6.388 +
   6.389 +lemma connected_complement_bounded_convex:
   6.390 +    fixes s :: "'a :: euclidean_space set"
   6.391 +    assumes "bounded s" "convex s" "2 \<le> DIM('a)"
   6.392 +      shows  "connected (- s)"
   6.393 +  using path_connected_complement_bounded_convex [OF assms] path_connected_imp_connected by blast
   6.394 +
   6.395 +lemma connected_diff_ball:
   6.396 +    fixes s :: "'a :: euclidean_space set"
   6.397 +    assumes "connected s" "cball a r \<subseteq> s" "2 \<le> DIM('a)"
   6.398 +      shows "connected (s - ball a r)"
   6.399 +  apply (rule connected_diff_open_from_closed [OF ball_subset_cball])
   6.400 +  using assms connected_sphere
   6.401 +  apply (auto simp: cball_diff_eq_sphere dist_norm)
   6.402 +  done
   6.403 +
   6.404 +subsection\<open>Relations between components and path components\<close>
   6.405 +
   6.406 +lemma open_connected_component:
   6.407 +  fixes s :: "'a::real_normed_vector set"
   6.408 +  shows "open s \<Longrightarrow> open (connected_component_set s x)"
   6.409 +    apply (simp add: open_contains_ball, clarify)
   6.410 +    apply (rename_tac y)
   6.411 +    apply (drule_tac x=y in bspec)
   6.412 +     apply (simp add: connected_component_in, clarify)
   6.413 +    apply (rule_tac x=e in exI)
   6.414 +    by (metis mem_Collect_eq connected_component_eq connected_component_maximal centre_in_ball connected_ball)
   6.415 +
   6.416 +corollary open_components:
   6.417 +    fixes s :: "'a::real_normed_vector set"
   6.418 +    shows "\<lbrakk>open u; s \<in> components u\<rbrakk> \<Longrightarrow> open s"
   6.419 +  by (simp add: components_iff) (metis open_connected_component)
   6.420 +
   6.421 +lemma in_closure_connected_component:
   6.422 +  fixes s :: "'a::real_normed_vector set"
   6.423 +  assumes x: "x \<in> s" and s: "open s"
   6.424 +  shows "x \<in> closure (connected_component_set s y) \<longleftrightarrow>  x \<in> connected_component_set s y"
   6.425 +proof -
   6.426 +  { assume "x \<in> closure (connected_component_set s y)"
   6.427 +    moreover have "x \<in> connected_component_set s x"
   6.428 +      using x by simp
   6.429 +    ultimately have "x \<in> connected_component_set s y"
   6.430 +      using s by (meson Compl_disjoint closure_iff_nhds_not_empty connected_component_disjoint disjoint_eq_subset_Compl open_connected_component)
   6.431 +  }
   6.432 +  then show ?thesis
   6.433 +    by (auto simp: closure_def)
   6.434 +qed
   6.435 +
   6.436 +subsection\<open>Existence of unbounded components\<close>
   6.437 +
   6.438 +lemma cobounded_unbounded_component:
   6.439 +    fixes s :: "'a :: euclidean_space set"
   6.440 +    assumes "bounded (-s)"
   6.441 +      shows "\<exists>x. x \<in> s \<and> ~ bounded (connected_component_set s x)"
   6.442 +proof -
   6.443 +  obtain i::'a where i: "i \<in> Basis"
   6.444 +    using nonempty_Basis by blast
   6.445 +  obtain B where B: "B>0" "-s \<subseteq> ball 0 B"
   6.446 +    using bounded_subset_ballD [OF assms, of 0] by auto
   6.447 +  then have *: "\<And>x. B \<le> norm x \<Longrightarrow> x \<in> s"
   6.448 +    by (force simp add: ball_def dist_norm)
   6.449 +  have unbounded_inner: "~ bounded {x. inner i x \<ge> B}"
   6.450 +    apply (auto simp: bounded_def dist_norm)
   6.451 +    apply (rule_tac x="x + (max B e + 1 + \<bar>i \<bullet> x\<bar>) *\<^sub>R i" in exI)
   6.452 +    apply simp
   6.453 +    using i
   6.454 +    apply (auto simp: algebra_simps)
   6.455 +    done
   6.456 +  have **: "{x. B \<le> i \<bullet> x} \<subseteq> connected_component_set s (B *\<^sub>R i)"
   6.457 +    apply (rule connected_component_maximal)
   6.458 +    apply (auto simp: i intro: convex_connected convex_halfspace_ge [of B])
   6.459 +    apply (rule *)
   6.460 +    apply (rule order_trans [OF _ Basis_le_norm [OF i]])
   6.461 +    by (simp add: inner_commute)
   6.462 +  have "B *\<^sub>R i \<in> s"
   6.463 +    by (rule *) (simp add: norm_Basis [OF i])
   6.464 +  then show ?thesis
   6.465 +    apply (rule_tac x="B *\<^sub>R i" in exI, clarify)
   6.466 +    apply (frule bounded_subset [of _ "{x. B \<le> i \<bullet> x}", OF _ **])
   6.467 +    using unbounded_inner apply blast
   6.468 +    done
   6.469 +qed
   6.470 +
   6.471 +lemma cobounded_unique_unbounded_component:
   6.472 +    fixes s :: "'a :: euclidean_space set"
   6.473 +    assumes bs: "bounded (-s)" and "2 \<le> DIM('a)"
   6.474 +        and bo: "~ bounded(connected_component_set s x)"
   6.475 +                "~ bounded(connected_component_set s y)"
   6.476 +      shows "connected_component_set s x = connected_component_set s y"
   6.477 +proof -
   6.478 +  obtain i::'a where i: "i \<in> Basis"
   6.479 +    using nonempty_Basis by blast
   6.480 +  obtain B where B: "B>0" "-s \<subseteq> ball 0 B"
   6.481 +    using bounded_subset_ballD [OF bs, of 0] by auto
   6.482 +  then have *: "\<And>x. B \<le> norm x \<Longrightarrow> x \<in> s"
   6.483 +    by (force simp add: ball_def dist_norm)
   6.484 +  have ccb: "connected (- ball 0 B :: 'a set)"
   6.485 +    using assms by (auto intro: connected_complement_bounded_convex)
   6.486 +  obtain x' where x': "connected_component s x x'" "norm x' > B"
   6.487 +    using bo [unfolded bounded_def dist_norm, simplified, rule_format]
   6.488 +    by (metis diff_zero norm_minus_commute not_less)
   6.489 +  obtain y' where y': "connected_component s y y'" "norm y' > B"
   6.490 +    using bo [unfolded bounded_def dist_norm, simplified, rule_format]
   6.491 +    by (metis diff_zero norm_minus_commute not_less)
   6.492 +  have x'y': "connected_component s x' y'"
   6.493 +    apply (simp add: connected_component_def)
   6.494 +    apply (rule_tac x="- ball 0 B" in exI)
   6.495 +    using x' y'
   6.496 +    apply (auto simp: ccb dist_norm *)
   6.497 +    done
   6.498 +  show ?thesis
   6.499 +    apply (rule connected_component_eq)
   6.500 +    using x' y' x'y'
   6.501 +    by (metis (no_types, lifting) connected_component_eq_empty connected_component_eq_eq connected_component_idemp connected_component_in)
   6.502 +qed
   6.503 +
   6.504 +lemma cobounded_unbounded_components:
   6.505 +    fixes s :: "'a :: euclidean_space set"
   6.506 +    shows "bounded (-s) \<Longrightarrow> \<exists>c. c \<in> components s \<and> ~bounded c"
   6.507 +  by (metis cobounded_unbounded_component components_def imageI)
   6.508 +
   6.509 +lemma cobounded_unique_unbounded_components:
   6.510 +    fixes s :: "'a :: euclidean_space set"
   6.511 +    shows  "\<lbrakk>bounded (- s); c \<in> components s; \<not> bounded c; c' \<in> components s; \<not> bounded c'; 2 \<le> DIM('a)\<rbrakk> \<Longrightarrow> c' = c"
   6.512 +  unfolding components_iff
   6.513 +  by (metis cobounded_unique_unbounded_component)
   6.514 +
   6.515 +lemma cobounded_has_bounded_component:
   6.516 +    fixes s :: "'a :: euclidean_space set"
   6.517 +    shows "\<lbrakk>bounded (- s); ~connected s; 2 \<le> DIM('a)\<rbrakk> \<Longrightarrow> \<exists>c. c \<in> components s \<and> bounded c"
   6.518 +  by (meson cobounded_unique_unbounded_components connected_eq_connected_components_eq)
   6.519 +
   6.520 +
   6.521 +subsection\<open>The "inside" and "outside" of a set\<close>
   6.522 +
   6.523 +text\<open>The inside comprises the points in a bounded connected component of the set's complement.
   6.524 +  The outside comprises the points in unbounded connected component of the complement.\<close>
   6.525 +
   6.526 +definition inside where
   6.527 +  "inside s \<equiv> {x. (x \<notin> s) \<and> bounded(connected_component_set ( - s) x)}"
   6.528 +
   6.529 +definition outside where
   6.530 +  "outside s \<equiv> -s \<inter> {x. ~ bounded(connected_component_set (- s) x)}"
   6.531 +
   6.532 +lemma outside: "outside s = {x. ~ bounded(connected_component_set (- s) x)}"
   6.533 +  by (auto simp: outside_def) (metis Compl_iff bounded_empty connected_component_eq_empty)
   6.534 +
   6.535 +lemma inside_no_overlap [simp]: "inside s \<inter> s = {}"
   6.536 +  by (auto simp: inside_def)
   6.537 +
   6.538 +lemma outside_no_overlap [simp]:
   6.539 +   "outside s \<inter> s = {}"
   6.540 +  by (auto simp: outside_def)
   6.541 +
   6.542 +lemma inside_inter_outside [simp]: "inside s \<inter> outside s = {}"
   6.543 +  by (auto simp: inside_def outside_def)
   6.544 +
   6.545 +lemma inside_union_outside [simp]: "inside s \<union> outside s = (- s)"
   6.546 +  by (auto simp: inside_def outside_def)
   6.547 +
   6.548 +lemma inside_eq_outside:
   6.549 +   "inside s = outside s \<longleftrightarrow> s = UNIV"
   6.550 +  by (auto simp: inside_def outside_def)
   6.551 +
   6.552 +lemma inside_outside: "inside s = (- (s \<union> outside s))"
   6.553 +  by (force simp add: inside_def outside)
   6.554 +
   6.555 +lemma outside_inside: "outside s = (- (s \<union> inside s))"
   6.556 +  by (auto simp: inside_outside) (metis IntI equals0D outside_no_overlap)
   6.557 +
   6.558 +lemma union_with_inside: "s \<union> inside s = - outside s"
   6.559 +  by (auto simp: inside_outside) (simp add: outside_inside)
   6.560 +
   6.561 +lemma union_with_outside: "s \<union> outside s = - inside s"
   6.562 +  by (simp add: inside_outside)
   6.563 +
   6.564 +lemma outside_mono: "s \<subseteq> t \<Longrightarrow> outside t \<subseteq> outside s"
   6.565 +  by (auto simp: outside bounded_subset connected_component_mono)
   6.566 +
   6.567 +lemma inside_mono: "s \<subseteq> t \<Longrightarrow> inside s - t \<subseteq> inside t"
   6.568 +  by (auto simp: inside_def bounded_subset connected_component_mono)
   6.569 +
   6.570 +lemma segment_bound_lemma:
   6.571 +  fixes u::real
   6.572 +  assumes "x \<ge> B" "y \<ge> B" "0 \<le> u" "u \<le> 1"
   6.573 +  shows "(1 - u) * x + u * y \<ge> B"
   6.574 +proof -
   6.575 +  obtain dx dy where "dx \<ge> 0" "dy \<ge> 0" "x = B + dx" "y = B + dy"
   6.576 +    using assms by auto (metis add.commute diff_add_cancel)
   6.577 +  with `0 \<le> u` `u \<le> 1` show ?thesis
   6.578 +    by (simp add: add_increasing2 mult_left_le field_simps)
   6.579 +qed
   6.580 +
   6.581 +lemma cobounded_outside:
   6.582 +  fixes s :: "'a :: real_normed_vector set"
   6.583 +  assumes "bounded s" shows "bounded (- outside s)"
   6.584 +proof -
   6.585 +  obtain B where B: "B>0" "s \<subseteq> ball 0 B"
   6.586 +    using bounded_subset_ballD [OF assms, of 0] by auto
   6.587 +  { fix x::'a and C::real
   6.588 +    assume Bno: "B \<le> norm x" and C: "0 < C"
   6.589 +    have "\<exists>y. connected_component (- s) x y \<and> norm y > C"
   6.590 +    proof (cases "x = 0")
   6.591 +      case True with B Bno show ?thesis by force
   6.592 +    next
   6.593 +      case False with B C show ?thesis
   6.594 +        apply (rule_tac x="((B+C)/norm x) *\<^sub>R x" in exI)
   6.595 +        apply (simp add: connected_component_def)
   6.596 +        apply (rule_tac x="closed_segment x (((B+C)/norm x) *\<^sub>R x)" in exI)
   6.597 +        apply simp
   6.598 +        apply (rule_tac y="- ball 0 B" in order_trans)
   6.599 +         prefer 2 apply force
   6.600 +        apply (simp add: closed_segment_def ball_def dist_norm, clarify)
   6.601 +        apply (simp add: real_vector_class.scaleR_add_left [symmetric] divide_simps)
   6.602 +        using segment_bound_lemma [of B "norm x" "B+C" ] Bno
   6.603 +        by (meson le_add_same_cancel1 less_eq_real_def not_le)
   6.604 +    qed
   6.605 +  }
   6.606 +  then show ?thesis
   6.607 +    apply (simp add: outside_def assms)
   6.608 +    apply (rule bounded_subset [OF bounded_ball [of 0 B]])
   6.609 +    apply (force simp add: dist_norm not_less bounded_pos)
   6.610 +    done
   6.611 +qed
   6.612 +
   6.613 +lemma unbounded_outside:
   6.614 +    fixes s :: "'a::{real_normed_vector, perfect_space} set"
   6.615 +    shows "bounded s \<Longrightarrow> ~ bounded(outside s)"
   6.616 +  using cobounded_imp_unbounded cobounded_outside by blast
   6.617 +
   6.618 +lemma bounded_inside:
   6.619 +    fixes s :: "'a::{real_normed_vector, perfect_space} set"
   6.620 +    shows "bounded s \<Longrightarrow> bounded(inside s)"
   6.621 +  by (simp add: bounded_Int cobounded_outside inside_outside)
   6.622 +
   6.623 +lemma connected_outside:
   6.624 +    fixes s :: "'a::euclidean_space set"
   6.625 +    assumes "bounded s" "2 \<le> DIM('a)"
   6.626 +      shows "connected(outside s)"
   6.627 +  apply (simp add: connected_iff_connected_component, clarify)
   6.628 +  apply (simp add: outside)
   6.629 +  apply (rule_tac s="connected_component_set (- s) x" in connected_component_of_subset)
   6.630 +  apply (metis (no_types) assms cobounded_unbounded_component cobounded_unique_unbounded_component connected_component_eq_eq connected_component_idemp double_complement mem_Collect_eq)
   6.631 +  apply clarify
   6.632 +  apply (metis connected_component_eq_eq connected_component_in)
   6.633 +  done
   6.634 +
   6.635 +lemma outside_connected_component_lt:
   6.636 +    "outside s = {x. \<forall>B. \<exists>y. B < norm(y) \<and> connected_component (- s) x y}"
   6.637 +apply (auto simp: outside bounded_def dist_norm)
   6.638 +apply (metis diff_0 norm_minus_cancel not_less)
   6.639 +by (metis less_diff_eq norm_minus_commute norm_triangle_ineq2 order.trans pinf(6))
   6.640 +
   6.641 +lemma outside_connected_component_le:
   6.642 +   "outside s =
   6.643 +            {x. \<forall>B. \<exists>y. B \<le> norm(y) \<and>
   6.644 +                         connected_component (- s) x y}"
   6.645 +apply (simp add: outside_connected_component_lt)
   6.646 +apply (simp add: Set.set_eq_iff)
   6.647 +by (meson gt_ex leD le_less_linear less_imp_le order.trans)
   6.648 +
   6.649 +lemma not_outside_connected_component_lt:
   6.650 +    fixes s :: "'a::euclidean_space set"
   6.651 +    assumes s: "bounded s" and "2 \<le> DIM('a)"
   6.652 +      shows "- (outside s) = {x. \<forall>B. \<exists>y. B < norm(y) \<and> ~ (connected_component (- s) x y)}"
   6.653 +proof -
   6.654 +  obtain B::real where B: "0 < B" and Bno: "\<And>x. x \<in> s \<Longrightarrow> norm x \<le> B"
   6.655 +    using s [simplified bounded_pos] by auto
   6.656 +  { fix y::'a and z::'a
   6.657 +    assume yz: "B < norm z" "B < norm y"
   6.658 +    have "connected_component (- cball 0 B) y z"
   6.659 +      apply (rule connected_componentI [OF _ subset_refl])
   6.660 +      apply (rule connected_complement_bounded_convex)
   6.661 +      using assms yz
   6.662 +      by (auto simp: dist_norm)
   6.663 +    then have "connected_component (- s) y z"
   6.664 +      apply (rule connected_component_of_subset)
   6.665 +      apply (metis Bno Compl_anti_mono mem_cball_0 subset_iff)
   6.666 +      done
   6.667 +  } note cyz = this
   6.668 +  show ?thesis
   6.669 +    apply (auto simp: outside)
   6.670 +    apply (metis Compl_iff bounded_iff cobounded_imp_unbounded mem_Collect_eq not_le)
   6.671 +    apply (simp add: bounded_pos)
   6.672 +    by (metis B connected_component_trans cyz not_le)
   6.673 +qed
   6.674 +
   6.675 +lemma not_outside_connected_component_le:
   6.676 +    fixes s :: "'a::euclidean_space set"
   6.677 +    assumes s: "bounded s"  "2 \<le> DIM('a)"
   6.678 +      shows "- (outside s) = {x. \<forall>B. \<exists>y. B \<le> norm(y) \<and> ~ (connected_component (- s) x y)}"
   6.679 +apply (auto intro: less_imp_le simp: not_outside_connected_component_lt [OF assms])
   6.680 +by (meson gt_ex less_le_trans)
   6.681 +
   6.682 +lemma inside_connected_component_lt:
   6.683 +    fixes s :: "'a::euclidean_space set"
   6.684 +    assumes s: "bounded s"  "2 \<le> DIM('a)"
   6.685 +      shows "inside s = {x. (x \<notin> s) \<and> (\<forall>B. \<exists>y. B < norm(y) \<and> ~(connected_component (- s) x y))}"
   6.686 +  by (auto simp: inside_outside not_outside_connected_component_lt [OF assms])
   6.687 +
   6.688 +lemma inside_connected_component_le:
   6.689 +    fixes s :: "'a::euclidean_space set"
   6.690 +    assumes s: "bounded s"  "2 \<le> DIM('a)"
   6.691 +      shows "inside s = {x. (x \<notin> s) \<and> (\<forall>B. \<exists>y. B \<le> norm(y) \<and> ~(connected_component (- s) x y))}"
   6.692 +  by (auto simp: inside_outside not_outside_connected_component_le [OF assms])
   6.693 +
   6.694 +lemma inside_subset:
   6.695 +  assumes "connected u" and "~bounded u" and "t \<union> u = - s"
   6.696 +  shows "inside s \<subseteq> t"
   6.697 +apply (auto simp: inside_def)
   6.698 +by (metis bounded_subset [of "connected_component_set (- s) _"] connected_component_maximal
   6.699 +       Compl_iff Un_iff assms subsetI)
   6.700 +
   6.701 +lemma frontier_interiors: "frontier s = - interior(s) - interior(-s)"
   6.702 +  by (simp add: Int_commute frontier_def interior_closure)
   6.703 +
   6.704 +lemma connected_inter_frontier:
   6.705 +     "\<lbrakk>connected s; s \<inter> t \<noteq> {}; s - t \<noteq> {}\<rbrakk> \<Longrightarrow> (s \<inter> frontier t \<noteq> {})"
   6.706 +  apply (simp add: frontier_interiors connected_open_in, safe)
   6.707 +  apply (drule_tac x="s \<inter> interior t" in spec, safe)
   6.708 +   apply (drule_tac [2] x="s \<inter> interior (-t)" in spec)
   6.709 +   apply (auto simp: disjoint_eq_subset_Compl dest: interior_subset [THEN subsetD])
   6.710 +  done
   6.711 +
   6.712 +lemma connected_component_UNIV:
   6.713 +    fixes x :: "'a::real_normed_vector"
   6.714 +    shows "connected_component_set UNIV x = UNIV"
   6.715 +using connected_iff_eq_connected_component_set [of "UNIV::'a set"] connected_UNIV
   6.716 +by auto
   6.717 +
   6.718 +lemma connected_component_eq_UNIV:
   6.719 +    fixes x :: "'a::real_normed_vector"
   6.720 +    shows "connected_component_set s x = UNIV \<longleftrightarrow> s = UNIV"
   6.721 +  using connected_component_in connected_component_UNIV by blast
   6.722 +
   6.723 +lemma components_univ [simp]: "components UNIV = {UNIV :: 'a::real_normed_vector set}"
   6.724 +  by (auto simp: components_eq_sing_iff)
   6.725 +
   6.726 +lemma interior_inside_frontier:
   6.727 +    fixes s :: "'a::real_normed_vector set"
   6.728 +    assumes "bounded s"
   6.729 +      shows "interior s \<subseteq> inside (frontier s)"
   6.730 +proof -
   6.731 +  { fix x y
   6.732 +    assume x: "x \<in> interior s" and y: "y \<notin> s"
   6.733 +       and cc: "connected_component (- frontier s) x y"
   6.734 +    have "connected_component_set (- frontier s) x \<inter> frontier s \<noteq> {}"
   6.735 +      apply (rule connected_inter_frontier, simp)
   6.736 +      apply (metis IntI cc connected_component_in connected_component_refl empty_iff interiorE mem_Collect_eq set_rev_mp x)
   6.737 +      using  y cc
   6.738 +      by blast
   6.739 +    then have "bounded (connected_component_set (- frontier s) x)"
   6.740 +      using connected_component_in by auto
   6.741 +  }
   6.742 +  then show ?thesis
   6.743 +    apply (auto simp: inside_def frontier_def)
   6.744 +    apply (rule classical)
   6.745 +    apply (rule bounded_subset [OF assms], blast)
   6.746 +    done
   6.747 +qed
   6.748 +
   6.749 +lemma inside_empty [simp]: "inside {} = ({} :: 'a :: {real_normed_vector, perfect_space} set)"
   6.750 +  by (simp add: inside_def connected_component_UNIV)
   6.751 +
   6.752 +lemma outside_empty [simp]: "outside {} = (UNIV :: 'a :: {real_normed_vector, perfect_space} set)"
   6.753 +using inside_empty inside_union_outside by blast
   6.754 +
   6.755 +lemma inside_same_component:
   6.756 +   "\<lbrakk>connected_component (- s) x y; x \<in> inside s\<rbrakk> \<Longrightarrow> y \<in> inside s"
   6.757 +  using connected_component_eq connected_component_in
   6.758 +  by (fastforce simp add: inside_def)
   6.759 +
   6.760 +lemma outside_same_component:
   6.761 +   "\<lbrakk>connected_component (- s) x y; x \<in> outside s\<rbrakk> \<Longrightarrow> y \<in> outside s"
   6.762 +  using connected_component_eq connected_component_in
   6.763 +  by (fastforce simp add: outside_def)
   6.764 +
   6.765 +lemma convex_in_outside:
   6.766 +  fixes s :: "'a :: {real_normed_vector, perfect_space} set"
   6.767 +  assumes s: "convex s" and z: "z \<notin> s"
   6.768 +    shows "z \<in> outside s"
   6.769 +proof (cases "s={}")
   6.770 +  case True then show ?thesis by simp
   6.771 +next
   6.772 +  case False then obtain a where "a \<in> s" by blast
   6.773 +  with z have zna: "z \<noteq> a" by auto
   6.774 +  { assume "bounded (connected_component_set (- s) z)"
   6.775 +    with bounded_pos_less obtain B where "B>0" and B: "\<And>x. connected_component (- s) z x \<Longrightarrow> norm x < B"
   6.776 +      by (metis mem_Collect_eq)
   6.777 +    def C \<equiv> "((B + 1 + norm z) / norm (z-a))"
   6.778 +    have "C > 0"
   6.779 +      using `0 < B` zna by (simp add: C_def divide_simps add_strict_increasing)
   6.780 +    have "\<bar>norm (z + C *\<^sub>R (z-a)) - norm (C *\<^sub>R (z-a))\<bar> \<le> norm z"
   6.781 +      by (metis add_diff_cancel norm_triangle_ineq3)
   6.782 +    moreover have "norm (C *\<^sub>R (z-a)) > norm z + B"
   6.783 +      using zna `B>0` by (simp add: C_def le_max_iff_disj field_simps)
   6.784 +    ultimately have C: "norm (z + C *\<^sub>R (z-a)) > B" by linarith
   6.785 +    { fix u::real
   6.786 +      assume u: "0\<le>u" "u\<le>1" and ins: "(1 - u) *\<^sub>R z + u *\<^sub>R (z + C *\<^sub>R (z - a)) \<in> s"
   6.787 +      then have Cpos: "1 + u * C > 0"
   6.788 +        by (meson `0 < C` add_pos_nonneg less_eq_real_def zero_le_mult_iff zero_less_one)
   6.789 +      then have *: "(1 / (1 + u * C)) *\<^sub>R z + (u * C / (1 + u * C)) *\<^sub>R z = z"
   6.790 +        by (simp add: scaleR_add_left [symmetric] divide_simps)
   6.791 +      then have False
   6.792 +        using convexD_alt [OF s `a \<in> s` ins, of "1/(u*C + 1)"] `C>0` `z \<notin> s` Cpos u
   6.793 +        by (simp add: * divide_simps algebra_simps)
   6.794 +    } note contra = this
   6.795 +    have "connected_component (- s) z (z + C *\<^sub>R (z-a))"
   6.796 +      apply (rule connected_componentI [OF connected_segment [of z "z + C *\<^sub>R (z-a)"]])
   6.797 +      apply (simp add: closed_segment_def)
   6.798 +      using contra
   6.799 +      apply auto
   6.800 +      done
   6.801 +    then have False
   6.802 +      using zna B [of "z + C *\<^sub>R (z-a)"] C
   6.803 +      by (auto simp: divide_simps max_mult_distrib_right)
   6.804 +  }
   6.805 +  then show ?thesis
   6.806 +    by (auto simp: outside_def z)
   6.807 +qed
   6.808 +
   6.809 +lemma outside_convex:
   6.810 +  fixes s :: "'a :: {real_normed_vector, perfect_space} set"
   6.811 +  assumes "convex s"
   6.812 +    shows "outside s = - s"
   6.813 +  by (metis ComplD assms convex_in_outside equalityI inside_union_outside subsetI sup.cobounded2)
   6.814 +
   6.815 +lemma inside_convex:
   6.816 +  fixes s :: "'a :: {real_normed_vector, perfect_space} set"
   6.817 +  shows "convex s \<Longrightarrow> inside s = {}"
   6.818 +  by (simp add: inside_outside outside_convex)
   6.819 +
   6.820 +lemma outside_subset_convex:
   6.821 +  fixes s :: "'a :: {real_normed_vector, perfect_space} set"
   6.822 +  shows "\<lbrakk>convex t; s \<subseteq> t\<rbrakk> \<Longrightarrow> - t \<subseteq> outside s"
   6.823 +  using outside_convex outside_mono by blast
   6.824 +
   6.825 +lemma outside_frontier_misses_closure:
   6.826 +    fixes s :: "'a::real_normed_vector set"
   6.827 +    assumes "bounded s"
   6.828 +    shows  "outside(frontier s) \<subseteq> - closure s"
   6.829 +  unfolding outside_inside Lattices.boolean_algebra_class.compl_le_compl_iff
   6.830 +proof -
   6.831 +  { assume "interior s \<subseteq> inside (frontier s)"
   6.832 +    hence "interior s \<union> inside (frontier s) = inside (frontier s)"
   6.833 +      by (simp add: subset_Un_eq)
   6.834 +    then have "closure s \<subseteq> frontier s \<union> inside (frontier s)"
   6.835 +      using frontier_def by auto
   6.836 +  }
   6.837 +  then show "closure s \<subseteq> frontier s \<union> inside (frontier s)"
   6.838 +    using interior_inside_frontier [OF assms] by blast
   6.839 +qed
   6.840 +
   6.841 +lemma outside_frontier_eq_complement_closure:
   6.842 +  fixes s :: "'a :: {real_normed_vector, perfect_space} set"
   6.843 +    assumes "bounded s" "convex s"
   6.844 +      shows "outside(frontier s) = - closure s"
   6.845 +by (metis Diff_subset assms convex_closure frontier_def outside_frontier_misses_closure
   6.846 +          outside_subset_convex subset_antisym)
   6.847 +
   6.848 +lemma open_inside:
   6.849 +    fixes s :: "'a::real_normed_vector set"
   6.850 +    assumes "closed s"
   6.851 +      shows "open (inside s)"
   6.852 +proof -
   6.853 +  { fix x assume x: "x \<in> inside s"
   6.854 +    have "open (connected_component_set (- s) x)"
   6.855 +      using assms open_connected_component by blast
   6.856 +    then obtain e where e: "e>0" and e: "\<And>y. dist y x < e \<longrightarrow> connected_component (- s) x y"
   6.857 +      using dist_not_less_zero
   6.858 +      apply (simp add: open_dist)
   6.859 +      by (metis (no_types, lifting) Compl_iff connected_component_refl_eq inside_def mem_Collect_eq x)
   6.860 +    then have "\<exists>e>0. ball x e \<subseteq> inside s"
   6.861 +      by (metis e dist_commute inside_same_component mem_ball subsetI x)
   6.862 +  }
   6.863 +  then show ?thesis
   6.864 +    by (simp add: open_contains_ball)
   6.865 +qed
   6.866 +
   6.867 +lemma open_outside:
   6.868 +    fixes s :: "'a::real_normed_vector set"
   6.869 +    assumes "closed s"
   6.870 +      shows "open (outside s)"
   6.871 +proof -
   6.872 +  { fix x assume x: "x \<in> outside s"
   6.873 +    have "open (connected_component_set (- s) x)"
   6.874 +      using assms open_connected_component by blast
   6.875 +    then obtain e where e: "e>0" and e: "\<And>y. dist y x < e \<longrightarrow> connected_component (- s) x y"
   6.876 +      using dist_not_less_zero
   6.877 +      apply (simp add: open_dist)
   6.878 +      by (metis Int_iff outside_def connected_component_refl_eq  x)
   6.879 +    then have "\<exists>e>0. ball x e \<subseteq> outside s"
   6.880 +      by (metis e dist_commute outside_same_component mem_ball subsetI x)
   6.881 +  }
   6.882 +  then show ?thesis
   6.883 +    by (simp add: open_contains_ball)
   6.884 +qed
   6.885 +
   6.886 +lemma closure_inside_subset:
   6.887 +    fixes s :: "'a::real_normed_vector set"
   6.888 +    assumes "closed s"
   6.889 +      shows "closure(inside s) \<subseteq> s \<union> inside s"
   6.890 +by (metis assms closure_minimal open_closed open_outside sup.cobounded2 union_with_inside)
   6.891 +
   6.892 +lemma frontier_inside_subset:
   6.893 +    fixes s :: "'a::real_normed_vector set"
   6.894 +    assumes "closed s"
   6.895 +      shows "frontier(inside s) \<subseteq> s"
   6.896 +proof -
   6.897 +  have "closure (inside s) \<inter> - inside s = closure (inside s) - interior (inside s)"
   6.898 +    by (metis (no_types) Diff_Compl assms closure_closed interior_closure open_closed open_inside)
   6.899 +  moreover have "- inside s \<inter> - outside s = s"
   6.900 +    by (metis (no_types) compl_sup double_compl inside_union_outside)
   6.901 +  moreover have "closure (inside s) \<subseteq> - outside s"
   6.902 +    by (metis (no_types) assms closure_inside_subset union_with_inside)
   6.903 +  ultimately have "closure (inside s) - interior (inside s) \<subseteq> s"
   6.904 +    by blast
   6.905 +  then show ?thesis
   6.906 +    by (simp add: frontier_def open_inside interior_open)
   6.907 +qed
   6.908 +
   6.909  end
     7.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Oct 13 09:21:21 2015 +0200
     7.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Oct 13 12:42:08 2015 +0100
     7.3 @@ -836,6 +836,9 @@
     7.4  lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s"
     7.5    by (simp add: set_eq_iff)
     7.6  
     7.7 +lemma cball_diff_eq_sphere: "cball a r - ball a r =  {x. dist x a = r}"
     7.8 +  by (auto simp: cball_def ball_def dist_commute)
     7.9 +
    7.10  lemma diff_less_iff:
    7.11    "(a::real) - b > 0 \<longleftrightarrow> a > b"
    7.12    "(a::real) - b < 0 \<longleftrightarrow> a < b"
    7.13 @@ -1806,6 +1809,10 @@
    7.14  abbreviation
    7.15     "connected_component_set s x \<equiv> Collect (connected_component s x)"
    7.16  
    7.17 +lemma connected_componentI:
    7.18 +    "\<lbrakk>connected t; t \<subseteq> s; x \<in> t; y \<in> t\<rbrakk> \<Longrightarrow> connected_component s x y"
    7.19 +  by (auto simp: connected_component_def)
    7.20 +
    7.21  lemma connected_component_in: "connected_component s x y \<Longrightarrow> x \<in> s \<and> y \<in> s"
    7.22    by (auto simp: connected_component_def)
    7.23  
    7.24 @@ -3086,8 +3093,21 @@
    7.25  definition (in metric_space) bounded :: "'a set \<Rightarrow> bool"
    7.26    where "bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)"
    7.27  
    7.28 -lemma bounded_subset_cball: "bounded S \<longleftrightarrow> (\<exists>e x. S \<subseteq> cball x e)"
    7.29 -  unfolding bounded_def subset_eq by auto
    7.30 +lemma bounded_subset_cball: "bounded S \<longleftrightarrow> (\<exists>e x. S \<subseteq> cball x e \<and> 0 \<le> e)"
    7.31 +  unfolding bounded_def subset_eq  by auto (meson order_trans zero_le_dist)
    7.32 +
    7.33 +lemma bounded_subset_ballD:
    7.34 +  assumes "bounded S" shows "\<exists>r. 0 < r \<and> S \<subseteq> ball x r"
    7.35 +proof -
    7.36 +  obtain e::real and y where "S \<subseteq> cball y e"  "0 \<le> e"
    7.37 +    using assms by (auto simp: bounded_subset_cball)
    7.38 +  then show ?thesis
    7.39 +    apply (rule_tac x="dist x y + e + 1" in exI)
    7.40 +    apply (simp add: add.commute add_pos_nonneg)
    7.41 +    apply (erule subset_trans)
    7.42 +    apply (clarsimp simp add: cball_def)
    7.43 +    by (metis add_le_cancel_right add_strict_increasing dist_commute dist_triangle_le zero_less_one)
    7.44 +qed
    7.45  
    7.46  lemma bounded_any_center: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>y\<in>S. dist a y \<le> e)"
    7.47    unfolding bounded_def
    7.48 @@ -3207,6 +3227,11 @@
    7.49    then show "\<exists>x::'a. b < norm x" ..
    7.50  qed
    7.51  
    7.52 +corollary cobounded_imp_unbounded:
    7.53 +    fixes S :: "'a::{real_normed_vector, perfect_space} set"
    7.54 +    shows "bounded (- S) \<Longrightarrow> ~ (bounded S)"
    7.55 +  using bounded_Un [of S "-S"]  by (simp add: sup_compl_top)
    7.56 +
    7.57  lemma bounded_linear_image:
    7.58    assumes "bounded S"
    7.59      and "bounded_linear f"
     8.1 --- a/src/HOL/Topological_Spaces.thy	Tue Oct 13 09:21:21 2015 +0200
     8.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Oct 13 12:42:08 2015 +0100
     8.3 @@ -1393,11 +1393,15 @@
     8.4    unfolding continuous_on_closed_invariant
     8.5    by (metis closed_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s])
     8.6  
     8.7 +corollary closed_vimage_Int[continuous_intros]:
     8.8 +  assumes "closed s" and "continuous_on t f" and t: "closed t"
     8.9 +  shows "closed (f -` s \<inter> t)"
    8.10 +  using assms unfolding continuous_on_closed_vimage [OF t]  by simp
    8.11 +
    8.12  corollary closed_vimage[continuous_intros]:
    8.13    assumes "closed s" and "continuous_on UNIV f"
    8.14    shows "closed (f -` s)"
    8.15 -  using assms unfolding continuous_on_closed_vimage [OF closed_UNIV]
    8.16 -  by simp
    8.17 +  using closed_vimage_Int [OF assms] by simp
    8.18  
    8.19  lemma continuous_on_open_Union:
    8.20    "(\<And>s. s \<in> S \<Longrightarrow> open s) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on s f) \<Longrightarrow> continuous_on (\<Union>S) f"