src/HOL/Analysis/Connected.thy
 author immler Tue Jul 10 09:38:35 2018 +0200 (11 months ago) changeset 68607 67bb59e49834 parent 68527 2f4e2aab190a child 69064 5840724b1d71 permissions -rw-r--r--
make theorem, corollary, and proposition %important for HOL-Analysis manual
 lp15@66835  1 (* Author: L C Paulson, University of Cambridge  lp15@66835  2  Material split off from Topology_Euclidean_Space  lp15@66835  3 *)  lp15@66827  4 nipkow@67968  5 section \Connected Components, Homeomorphisms, Baire property, etc\  lp15@66827  6 lp15@66827  7 theory Connected  lp15@66827  8 imports Topology_Euclidean_Space  lp15@66827  9 begin  lp15@66827  10 nipkow@67968  11 subsection%unimportant \More properties of closed balls, spheres, etc\  lp15@66827  12 lp15@66827  13 lemma mem_interior_cball: "x \ interior S \ (\e>0. cball x e \ S)"  lp15@66827  14  apply (simp add: interior_def, safe)  lp15@66827  15  apply (force simp: open_contains_cball)  lp15@66827  16  apply (rule_tac x="ball x e" in exI)  lp15@66827  17  apply (simp add: subset_trans [OF ball_subset_cball])  lp15@66827  18  done  lp15@66827  19 lp15@66827  20 lemma islimpt_ball:  lp15@66827  21  fixes x y :: "'a::{real_normed_vector,perfect_space}"  lp15@66827  22  shows "y islimpt ball x e \ 0 < e \ y \ cball x e"  lp15@66827  23  (is "?lhs \ ?rhs")  lp15@66827  24 proof  lp15@66827  25  show ?rhs if ?lhs  lp15@66827  26  proof  lp15@66827  27  {  lp15@66827  28  assume "e \ 0"  lp15@66827  29  then have *: "ball x e = {}"  lp15@66827  30  using ball_eq_empty[of x e] by auto  lp15@66827  31  have False using \?lhs\  lp15@66827  32  unfolding * using islimpt_EMPTY[of y] by auto  lp15@66827  33  }  lp15@66827  34  then show "e > 0" by (metis not_less)  lp15@66827  35  show "y \ cball x e"  lp15@66827  36  using closed_cball[of x e] islimpt_subset[of y "ball x e" "cball x e"]  lp15@66827  37  ball_subset_cball[of x e] \?lhs\  lp15@66827  38  unfolding closed_limpt by auto  lp15@66827  39  qed  lp15@66827  40  show ?lhs if ?rhs  lp15@66827  41  proof -  lp15@66827  42  from that have "e > 0" by auto  lp15@66827  43  {  lp15@66827  44  fix d :: real  lp15@66827  45  assume "d > 0"  lp15@66827  46  have "\x'\ball x e. x' \ y \ dist x' y < d"  lp15@66827  47  proof (cases "d \ dist x y")  lp15@66827  48  case True  lp15@66827  49  then show "\x'\ball x e. x' \ y \ dist x' y < d"  lp15@66827  50  proof (cases "x = y")  lp15@66827  51  case True  lp15@66827  52  then have False  lp15@66827  53  using \d \ dist x y\ \d>0\ by auto  lp15@66827  54  then show "\x'\ball x e. x' \ y \ dist x' y < d"  lp15@66827  55  by auto  lp15@66827  56  next  lp15@66827  57  case False  lp15@66827  58  have "dist x (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) =  lp15@66827  59  norm (x - y + (d / (2 * norm (y - x))) *\<^sub>R (y - x))"  lp15@66827  60  unfolding mem_cball mem_ball dist_norm diff_diff_eq2 diff_add_eq[symmetric]  lp15@66827  61  by auto  lp15@66827  62  also have "\ = \- 1 + d / (2 * norm (x - y))\ * norm (x - y)"  lp15@66827  63  using scaleR_left_distrib[of "- 1" "d / (2 * norm (y - x))", symmetric, of "y - x"]  lp15@66827  64  unfolding scaleR_minus_left scaleR_one  lp15@66827  65  by (auto simp: norm_minus_commute)  lp15@66827  66  also have "\ = \- norm (x - y) + d / 2\"  lp15@66827  67  unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]  lp15@66827  68  unfolding distrib_right using \x\y\ by auto  lp15@66827  69  also have "\ \ e - d/2" using \d \ dist x y\ and \d>0\ and \?rhs\  lp15@66827  70  by (auto simp: dist_norm)  lp15@66827  71  finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \ ball x e" using \d>0\  lp15@66827  72  by auto  lp15@66827  73  moreover  lp15@66827  74  have "(d / (2*dist y x)) *\<^sub>R (y - x) \ 0"  lp15@66827  75  using \x\y$unfolded dist_nz] \d>0\ unfolding scaleR_eq_0_iff  lp15@66827  76  by (auto simp: dist_commute)  lp15@66827  77  moreover  lp15@66827  78  have "dist (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) y < d"  lp15@66827  79  unfolding dist_norm  lp15@66827  80  apply simp  lp15@66827  81  unfolding norm_minus_cancel  lp15@66827  82  using \d > 0\ \x\y\[unfolded dist_nz] dist_commute[of x y]  lp15@66827  83  unfolding dist_norm  lp15@66827  84  apply auto  lp15@66827  85  done  lp15@66827  86  ultimately show "\x'\ball x e. x' \ y \ dist x' y < d"  lp15@66827  87  apply (rule_tac x = "y - (d / (2*dist y x)) *\<^sub>R (y - x)" in bexI)  lp15@66827  88  apply auto  lp15@66827  89  done  lp15@66827  90  qed  lp15@66827  91  next  lp15@66827  92  case False  lp15@66827  93  then have "d > dist x y" by auto  lp15@66827  94  show "\x' \ ball x e. x' \ y \ dist x' y < d"  lp15@66827  95  proof (cases "x = y")  lp15@66827  96  case True  lp15@66827  97  obtain z where **: "z \ y" "dist z y < min e d"  lp15@66827  98  using perfect_choose_dist[of "min e d" y]  lp15@66827  99  using \d > 0\ \e>0\ by auto  lp15@66827  100  show "\x'\ball x e. x' \ y \ dist x' y < d"  lp15@66827  101  unfolding \x = y\  lp15@66827  102  using \z \ y\ **  lp15@66827  103  apply (rule_tac x=z in bexI)  lp15@66827  104  apply (auto simp: dist_commute)  lp15@66827  105  done  lp15@66827  106  next  lp15@66827  107  case False  lp15@66827  108  then show "\x'\ball x e. x' \ y \ dist x' y < d"  lp15@66827  109  using \d>0\ \d > dist x y\ \?rhs\  lp15@66827  110  apply (rule_tac x=x in bexI, auto)  lp15@66827  111  done  lp15@66827  112  qed  lp15@66827  113  qed  lp15@66827  114  }  lp15@66827  115  then show ?thesis  lp15@66827  116  unfolding mem_cball islimpt_approachable mem_ball by auto  lp15@66827  117  qed  lp15@66827  118 qed  lp15@66827  119 lp15@66827  120 lemma closure_ball_lemma:  lp15@66827  121  fixes x y :: "'a::real_normed_vector"  lp15@66827  122  assumes "x \ y"  lp15@66827  123  shows "y islimpt ball x (dist x y)"  lp15@66827  124 proof (rule islimptI)  lp15@66827  125  fix T  lp15@66827  126  assume "y \ T" "open T"  lp15@66827  127  then obtain r where "0 < r" "\z. dist z y < r \ z \ T"  lp15@66827  128  unfolding open_dist by fast  lp15@66827  129  (* choose point between x and y, within distance r of y. *)  lp15@66827  130  define k where "k = min 1 (r / (2 * dist x y))"  lp15@66827  131  define z where "z = y + scaleR k (x - y)"  lp15@66827  132  have z_def2: "z = x + scaleR (1 - k) (y - x)"  lp15@66827  133  unfolding z_def by (simp add: algebra_simps)  lp15@66827  134  have "dist z y < r"  lp15@66827  135  unfolding z_def k_def using \0 < r\  lp15@66827  136  by (simp add: dist_norm min_def)  lp15@66827  137  then have "z \ T"  lp15@66827  138  using \\z. dist z y < r \ z \ T\ by simp  lp15@66827  139  have "dist x z < dist x y"  lp15@66827  140  unfolding z_def2 dist_norm  lp15@66827  141  apply (simp add: norm_minus_commute)  lp15@66827  142  apply (simp only: dist_norm [symmetric])  lp15@66827  143  apply (subgoal_tac "\1 - k\ * dist x y < 1 * dist x y", simp)  lp15@66827  144  apply (rule mult_strict_right_mono)  lp15@66827  145  apply (simp add: k_def \0 < r\ \x \ y\)  lp15@66827  146  apply (simp add: \x \ y\)  lp15@66827  147  done  lp15@66827  148  then have "z \ ball x (dist x y)"  lp15@66827  149  by simp  lp15@66827  150  have "z \ y"  lp15@66827  151  unfolding z_def k_def using \x \ y\ \0 < r\  lp15@66827  152  by (simp add: min_def)  lp15@66827  153  show "\z\ball x (dist x y). z \ T \ z \ y"  lp15@66827  154  using \z \ ball x (dist x y)\ \z \ T\ \z \ y\  lp15@66827  155  by fast  lp15@66827  156 qed  lp15@66827  157 wl302@67706  158 lemma at_within_ball_bot_iff:  wl302@67706  159  fixes x y :: "'a::{real_normed_vector,perfect_space}"  wl302@67706  160  shows "at x within ball y r = bot \ (r=0 \ x \ cball y r)"  wl302@67706  161  unfolding trivial_limit_within  wl302@67706  162 apply (auto simp add:trivial_limit_within islimpt_ball )  wl302@67706  163 by (metis le_less_trans less_eq_real_def zero_le_dist)  wl302@67706  164 lp15@66827  165 lemma closure_ball [simp]:  lp15@66827  166  fixes x :: "'a::real_normed_vector"  lp15@66827  167  shows "0 < e \ closure (ball x e) = cball x e"  lp15@66827  168  apply (rule equalityI)  lp15@66827  169  apply (rule closure_minimal)  lp15@66827  170  apply (rule ball_subset_cball)  lp15@66827  171  apply (rule closed_cball)  lp15@66827  172  apply (rule subsetI, rename_tac y)  lp15@66827  173  apply (simp add: le_less [where 'a=real])  lp15@66827  174  apply (erule disjE)  lp15@66827  175  apply (rule subsetD [OF closure_subset], simp)  lp15@66827  176  apply (simp add: closure_def, clarify)  lp15@66827  177  apply (rule closure_ball_lemma)  haftmann@66953  178  apply simp  lp15@66827  179  done  lp15@66827  180 lp15@66827  181 (* In a trivial vector space, this fails for e = 0. *)  lp15@66827  182 lemma interior_cball [simp]:  lp15@66827  183  fixes x :: "'a::{real_normed_vector, perfect_space}"  lp15@66827  184  shows "interior (cball x e) = ball x e"  lp15@66827  185 proof (cases "e \ 0")  lp15@66827  186  case False note cs = this  lp15@66827  187  from cs have null: "ball x e = {}"  lp15@66827  188  using ball_empty[of e x] by auto  lp15@66827  189  moreover  lp15@66827  190  {  lp15@66827  191  fix y  lp15@66827  192  assume "y \ cball x e"  lp15@66827  193  then have False  lp15@66827  194  by (metis ball_eq_empty null cs dist_eq_0_iff dist_le_zero_iff empty_subsetI mem_cball subset_antisym subset_ball)  lp15@66827  195  }  lp15@66827  196  then have "cball x e = {}" by auto  lp15@66827  197  then have "interior (cball x e) = {}"  lp15@66827  198  using interior_empty by auto  lp15@66827  199  ultimately show ?thesis by blast  lp15@66827  200 next  lp15@66827  201  case True note cs = this  lp15@66827  202  have "ball x e \ cball x e"  lp15@66827  203  using ball_subset_cball by auto  lp15@66827  204  moreover  lp15@66827  205  {  lp15@66827  206  fix S y  lp15@66827  207  assume as: "S \ cball x e" "open S" "y\S"  lp15@66827  208  then obtain d where "d>0" and d: "\x'. dist x' y < d \ x' \ S"  lp15@66827  209  unfolding open_dist by blast  lp15@66827  210  then obtain xa where xa_y: "xa \ y" and xa: "dist xa y < d"  lp15@66827  211  using perfect_choose_dist [of d] by auto  lp15@66827  212  have "xa \ S"  lp15@66827  213  using d[THEN spec[where x = xa]]  lp15@66827  214  using xa by (auto simp: dist_commute)  lp15@66827  215  then have xa_cball: "xa \ cball x e"  lp15@66827  216  using as(1) by auto  lp15@66827  217  then have "y \ ball x e"  lp15@66827  218  proof (cases "x = y")  lp15@66827  219  case True  lp15@66827  220  then have "e > 0" using cs order.order_iff_strict xa_cball xa_y by fastforce  lp15@66827  221  then show "y \ ball x e"  lp15@66827  222  using \x = y \ by simp  lp15@66827  223  next  lp15@66827  224  case False  lp15@66827  225  have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) y < d"  lp15@66827  226  unfolding dist_norm  lp15@66827  227  using \d>0\ norm_ge_zero[of "y - x"] \x \ y\ by auto  lp15@66827  228  then have *: "y + (d / 2 / dist y x) *\<^sub>R (y - x) \ cball x e"  lp15@66827  229  using d as(1)[unfolded subset_eq] by blast  lp15@66827  230  have "y - x \ 0" using \x \ y\ by auto  lp15@66827  231  hence **:"d / (2 * norm (y - x)) > 0"  lp15@66827  232  unfolding zero_less_norm_iff[symmetric] using \d>0\ by auto  lp15@66827  233  have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) x =  lp15@66827  234  norm (y + (d / (2 * norm (y - x))) *\<^sub>R y - (d / (2 * norm (y - x))) *\<^sub>R x - x)"  lp15@66827  235  by (auto simp: dist_norm algebra_simps)  lp15@66827  236  also have "\ = norm ((1 + d / (2 * norm (y - x))) *\<^sub>R (y - x))"  lp15@66827  237  by (auto simp: algebra_simps)  lp15@66827  238  also have "\ = \1 + d / (2 * norm (y - x))\ * norm (y - x)"  lp15@66827  239  using ** by auto  lp15@66827  240  also have "\ = (dist y x) + d/2"  lp15@66827  241  using ** by (auto simp: distrib_right dist_norm)  lp15@66827  242  finally have "e \ dist x y +d/2"  lp15@66827  243  using *[unfolded mem_cball] by (auto simp: dist_commute)  lp15@66827  244  then show "y \ ball x e"  lp15@66827  245  unfolding mem_ball using \d>0\ by auto  lp15@66827  246  qed  lp15@66827  247  }  lp15@66827  248  then have "\S \ cball x e. open S \ S \ ball x e"  lp15@66827  249  by auto  lp15@66827  250  ultimately show ?thesis  lp15@66827  251  using interior_unique[of "ball x e" "cball x e"]  lp15@66827  252  using open_ball[of x e]  lp15@66827  253  by auto  lp15@66827  254 qed  lp15@66827  255 lp15@66827  256 lemma interior_ball [simp]: "interior (ball x e) = ball x e"  lp15@66827  257  by (simp add: interior_open)  lp15@66827  258 lp15@66827  259 lemma frontier_ball [simp]:  lp15@66827  260  fixes a :: "'a::real_normed_vector"  lp15@66827  261  shows "0 < e \ frontier (ball a e) = sphere a e"  lp15@66827  262  by (force simp: frontier_def)  lp15@66827  263 lp15@66827  264 lemma frontier_cball [simp]:  lp15@66827  265  fixes a :: "'a::{real_normed_vector, perfect_space}"  lp15@66827  266  shows "frontier (cball a e) = sphere a e"  lp15@66827  267  by (force simp: frontier_def)  lp15@66827  268 lp15@66827  269 lemma cball_eq_empty [simp]: "cball x e = {} \ e < 0"  lp15@66827  270  apply (simp add: set_eq_iff not_le)  lp15@66827  271  apply (metis zero_le_dist dist_self order_less_le_trans)  lp15@66827  272  done  lp15@66827  273 lp15@66827  274 lemma cball_empty [simp]: "e < 0 \ cball x e = {}"  lp15@66827  275  by simp  lp15@66827  276 lp15@66827  277 lemma cball_eq_sing:  lp15@66827  278  fixes x :: "'a::{metric_space,perfect_space}"  lp15@66827  279  shows "cball x e = {x} \ e = 0"  lp15@66827  280 proof (rule linorder_cases)  lp15@66827  281  assume e: "0 < e"  lp15@66827  282  obtain a where "a \ x" "dist a x < e"  lp15@66827  283  using perfect_choose_dist [OF e] by auto  lp15@66827  284  then have "a \ x" "dist x a \ e"  lp15@66827  285  by (auto simp: dist_commute)  lp15@66827  286  with e show ?thesis by (auto simp: set_eq_iff)  lp15@66827  287 qed auto  lp15@66827  288 lp15@66827  289 lemma cball_sing:  lp15@66827  290  fixes x :: "'a::metric_space"  lp15@66827  291  shows "e = 0 \ cball x e = {x}"  lp15@66827  292  by (auto simp: set_eq_iff)  lp15@66827  293 lp15@66827  294 lemma ball_divide_subset: "d \ 1 \ ball x (e/d) \ ball x e"  lp15@66827  295  apply (cases "e \ 0")  lp15@66827  296  apply (simp add: ball_empty divide_simps)  lp15@66827  297  apply (rule subset_ball)  lp15@66827  298  apply (simp add: divide_simps)  lp15@66827  299  done  lp15@66827  300 lp15@66827  301 lemma ball_divide_subset_numeral: "ball x (e / numeral w) \ ball x e"  lp15@66827  302  using ball_divide_subset one_le_numeral by blast  lp15@66827  303 lp15@66827  304 lemma cball_divide_subset: "d \ 1 \ cball x (e/d) \ cball x e"  lp15@66827  305  apply (cases "e < 0")  lp15@66827  306  apply (simp add: divide_simps)  lp15@66827  307  apply (rule subset_cball)  lp15@66827  308  apply (metis div_by_1 frac_le not_le order_refl zero_less_one)  lp15@66827  309  done  lp15@66827  310 lp15@66827  311 lemma cball_divide_subset_numeral: "cball x (e / numeral w) \ cball x e"  lp15@66827  312  using cball_divide_subset one_le_numeral by blast  lp15@66827  313 lp15@66827  314 lemma compact_cball[simp]:  lp15@66827  315  fixes x :: "'a::heine_borel"  lp15@66827  316  shows "compact (cball x e)"  lp15@66827  317  using compact_eq_bounded_closed bounded_cball closed_cball  lp15@66827  318  by blast  lp15@66827  319 lp15@66827  320 lemma compact_frontier_bounded[intro]:  lp15@66827  321  fixes S :: "'a::heine_borel set"  lp15@66827  322  shows "bounded S \ compact (frontier S)"  lp15@66827  323  unfolding frontier_def  lp15@66827  324  using compact_eq_bounded_closed  lp15@66827  325  by blast  lp15@66827  326 lp15@66827  327 lemma compact_frontier[intro]:  lp15@66827  328  fixes S :: "'a::heine_borel set"  lp15@66827  329  shows "compact S \ compact (frontier S)"  lp15@66827  330  using compact_eq_bounded_closed compact_frontier_bounded  lp15@66827  331  by blast  lp15@66827  332 lp15@66827  333 corollary compact_sphere [simp]:  lp15@66827  334  fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"  lp15@66827  335  shows "compact (sphere a r)"  lp15@66827  336 using compact_frontier [of "cball a r"] by simp  lp15@66827  337 lp15@66827  338 corollary bounded_sphere [simp]:  lp15@66827  339  fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"  lp15@66827  340  shows "bounded (sphere a r)"  lp15@66827  341 by (simp add: compact_imp_bounded)  lp15@66827  342 lp15@66827  343 corollary closed_sphere [simp]:  lp15@66827  344  fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"  lp15@66827  345  shows "closed (sphere a r)"  lp15@66827  346 by (simp add: compact_imp_closed)  lp15@66827  347 immler@67962  348 subsection%unimportant \Connectedness\  lp15@66827  349 lp15@66827  350 lemma connected_local:  lp15@66827  351  "connected S \  lp15@66827  352  \ (\e1 e2.  lp15@66827  353  openin (subtopology euclidean S) e1 \  lp15@66827  354  openin (subtopology euclidean S) e2 \  lp15@66827  355  S \ e1 \ e2 \  lp15@66827  356  e1 \ e2 = {} \  lp15@66827  357  e1 \ {} \  lp15@66827  358  e2 \ {})"  lp15@66827  359  unfolding connected_def openin_open  lp15@66827  360  by safe blast+  lp15@66827  361 lp15@66827  362 lemma exists_diff:  lp15@66827  363  fixes P :: "'a set \ bool"  lp15@66827  364  shows "(\S. P (- S)) \ (\S. P S)"  lp15@66827  365  (is "?lhs \ ?rhs")  lp15@66827  366 proof -  lp15@66827  367  have ?rhs if ?lhs  lp15@66827  368  using that by blast  lp15@66827  369  moreover have "P (- (- S))" if "P S" for S  lp15@66827  370  proof -  lp15@66827  371  have "S = - (- S)" by simp  lp15@66827  372  with that show ?thesis by metis  lp15@66827  373  qed  lp15@66827  374  ultimately show ?thesis by metis  lp15@66827  375 qed  lp15@66827  376 lp15@66827  377 lemma connected_clopen: "connected S \  lp15@66827  378  (\T. openin (subtopology euclidean S) T \  lp15@66827  379  closedin (subtopology euclidean S) T \ T = {} \ T = S)" (is "?lhs \ ?rhs")  lp15@66827  380 proof -  lp15@66827  381  have "\ connected S \  lp15@66827  382  (\e1 e2. open e1 \ open (- e2) \ S \ e1 \ (- e2) \ e1 \ (- e2) \ S = {} \ e1 \ S \ {} \ (- e2) \ S \ {})"  lp15@66827  383  unfolding connected_def openin_open closedin_closed  lp15@66827  384  by (metis double_complement)  lp15@66827  385  then have th0: "connected S \  lp15@66827  386  \ (\e2 e1. closed e2 \ open e1 \ S \ e1 \ (- e2) \ e1 \ (- e2) \ S = {} \ e1 \ S \ {} \ (- e2) \ S \ {})"  lp15@66827  387  (is " _ \ \ (\e2 e1. ?P e2 e1)")  lp15@66827  388  by (simp add: closed_def) metis  lp15@66827  389  have th1: "?rhs \ \ (\t' t. closed t'\t = S\t' \ t\{} \ t\S \ (\t'. open t' \ t = S \ t'))"  lp15@66827  390  (is "_ \ \ (\t' t. ?Q t' t)")  lp15@66827  391  unfolding connected_def openin_open closedin_closed by auto  lp15@66827  392  have "(\e1. ?P e2 e1) \ (\t. ?Q e2 t)" for e2  lp15@66827  393  proof -  lp15@66827  394  have "?P e2 e1 \ (\t. closed e2 \ t = S\e2 \ open e1 \ t = S\e1 \ t\{} \ t \ S)" for e1  lp15@66827  395  by auto  lp15@66827  396  then show ?thesis  lp15@66827  397  by metis  lp15@66827  398  qed  lp15@66827  399  then have "\e2. (\e1. ?P e2 e1) \ (\t. ?Q e2 t)"  lp15@66827  400  by blast  lp15@66827  401  then show ?thesis  lp15@66827  402  by (simp add: th0 th1)  lp15@66827  403 qed  lp15@66827  404 lp15@66827  405 lemma connected_linear_image:  lp15@66827  406  fixes f :: "'a::euclidean_space \ 'b::real_normed_vector"  lp15@66827  407  assumes "linear f" and "connected s"  lp15@66827  408  shows "connected (f  s)"  lp15@66827  409 using connected_continuous_image assms linear_continuous_on linear_conv_bounded_linear by blast  lp15@66827  410 lp15@66827  411 subsection \Connected components, considered as a connectedness relation or a set\  lp15@66827  412 immler@67962  413 definition%important "connected_component s x y \ \t. connected t \ t \ s \ x \ t \ y \ t"  lp15@66827  414 lp15@66827  415 abbreviation "connected_component_set s x \ Collect (connected_component s x)"  lp15@66827  416 lp15@66827  417 lemma connected_componentI:  lp15@66827  418  "connected t \ t \ s \ x \ t \ y \ t \ connected_component s x y"  lp15@66827  419  by (auto simp: connected_component_def)  lp15@66827  420 lp15@66827  421 lemma connected_component_in: "connected_component s x y \ x \ s \ y \ s"  lp15@66827  422  by (auto simp: connected_component_def)  lp15@66827  423 lp15@66827  424 lemma connected_component_refl: "x \ s \ connected_component s x x"  lp15@66827  425  by (auto simp: connected_component_def) (use connected_sing in blast)  lp15@66827  426 lp15@66827  427 lemma connected_component_refl_eq [simp]: "connected_component s x x \ x \ s"  lp15@66827  428  by (auto simp: connected_component_refl) (auto simp: connected_component_def)  lp15@66827  429 lp15@66827  430 lemma connected_component_sym: "connected_component s x y \ connected_component s y x"  lp15@66827  431  by (auto simp: connected_component_def)  lp15@66827  432 lp15@66827  433 lemma connected_component_trans:  lp15@66827  434  "connected_component s x y \ connected_component s y z \ connected_component s x z"  lp15@66827  435  unfolding connected_component_def  lp15@66827  436  by (metis Int_iff Un_iff Un_subset_iff equals0D connected_Un)  lp15@66827  437 lp15@66827  438 lemma connected_component_of_subset:  lp15@66827  439  "connected_component s x y \ s \ t \ connected_component t x y"  lp15@66827  440  by (auto simp: connected_component_def)  lp15@66827  441 lp15@66827  442 lemma connected_component_Union: "connected_component_set s x = \{t. connected t \ x \ t \ t \ s}"  lp15@66827  443  by (auto simp: connected_component_def)  lp15@66827  444 lp15@66827  445 lemma connected_connected_component [iff]: "connected (connected_component_set s x)"  lp15@66827  446  by (auto simp: connected_component_Union intro: connected_Union)  lp15@66827  447 lp15@66827  448 lemma connected_iff_eq_connected_component_set:  lp15@66827  449  "connected s \ (\x \ s. connected_component_set s x = s)"  lp15@66827  450 proof (cases "s = {}")  lp15@66827  451  case True  lp15@66827  452  then show ?thesis by simp  lp15@66827  453 next  lp15@66827  454  case False  lp15@66827  455  then obtain x where "x \ s" by auto  lp15@66827  456  show ?thesis  lp15@66827  457  proof  lp15@66827  458  assume "connected s"  lp15@66827  459  then show "\x \ s. connected_component_set s x = s"  lp15@66827  460  by (force simp: connected_component_def)  lp15@66827  461  next  lp15@66827  462  assume "\x \ s. connected_component_set s x = s"  lp15@66827  463  then show "connected s"  lp15@66827  464  by (metis \x \ s\ connected_connected_component)  lp15@66827  465  qed  lp15@66827  466 qed  lp15@66827  467 lp15@66827  468 lemma connected_component_subset: "connected_component_set s x \ s"  lp15@66827  469  using connected_component_in by blast  lp15@66827  470 lp15@66827  471 lemma connected_component_eq_self: "connected s \ x \ s \ connected_component_set s x = s"  lp15@66827  472  by (simp add: connected_iff_eq_connected_component_set)  lp15@66827  473 lp15@66827  474 lemma connected_iff_connected_component:  lp15@66827  475  "connected s \ (\x \ s. \y \ s. connected_component s x y)"  lp15@66827  476  using connected_component_in by (auto simp: connected_iff_eq_connected_component_set)  lp15@66827  477 lp15@66827  478 lemma connected_component_maximal:  lp15@66827  479  "x \ t \ connected t \ t \ s \ t \ (connected_component_set s x)"  lp15@66827  480  using connected_component_eq_self connected_component_of_subset by blast  lp15@66827  481 lp15@66827  482 lemma connected_component_mono:  lp15@66827  483  "s \ t \ connected_component_set s x \ connected_component_set t x"  lp15@66827  484  by (simp add: Collect_mono connected_component_of_subset)  lp15@66827  485 lp15@66827  486 lemma connected_component_eq_empty [simp]: "connected_component_set s x = {} \ x \ s"  lp15@66827  487  using connected_component_refl by (fastforce simp: connected_component_in)  lp15@66827  488 lp15@66827  489 lemma connected_component_set_empty [simp]: "connected_component_set {} x = {}"  lp15@66827  490  using connected_component_eq_empty by blast  lp15@66827  491 lp15@66827  492 lemma connected_component_eq:  lp15@66827  493  "y \ connected_component_set s x \ (connected_component_set s y = connected_component_set s x)"  lp15@66827  494  by (metis (no_types, lifting)  lp15@66827  495  Collect_cong connected_component_sym connected_component_trans mem_Collect_eq)  lp15@66827  496 lp15@66827  497 lemma closed_connected_component:  lp15@66827  498  assumes s: "closed s"  lp15@66827  499  shows "closed (connected_component_set s x)"  lp15@66827  500 proof (cases "x \ s")  lp15@66827  501  case False  lp15@66827  502  then show ?thesis  lp15@66827  503  by (metis connected_component_eq_empty closed_empty)  lp15@66827  504 next  lp15@66827  505  case True  lp15@66827  506  show ?thesis  lp15@66827  507  unfolding closure_eq [symmetric]  lp15@66827  508  proof  lp15@66827  509  show "closure (connected_component_set s x) \ connected_component_set s x"  lp15@66827  510  apply (rule connected_component_maximal)  lp15@66827  511  apply (simp add: closure_def True)  lp15@66827  512  apply (simp add: connected_imp_connected_closure)  lp15@66827  513  apply (simp add: s closure_minimal connected_component_subset)  lp15@66827  514  done  lp15@66827  515  next  lp15@66827  516  show "connected_component_set s x \ closure (connected_component_set s x)"  lp15@66827  517  by (simp add: closure_subset)  lp15@66827  518  qed  lp15@66827  519 qed  lp15@66827  520 lp15@66827  521 lemma connected_component_disjoint:  lp15@66827  522  "connected_component_set s a \ connected_component_set s b = {} \  lp15@66827  523  a \ connected_component_set s b"  lp15@66827  524  apply (auto simp: connected_component_eq)  lp15@66827  525  using connected_component_eq connected_component_sym  lp15@66827  526  apply blast  lp15@66827  527  done  lp15@66827  528 lp15@66827  529 lemma connected_component_nonoverlap:  lp15@66827  530  "connected_component_set s a \ connected_component_set s b = {} \  lp15@66827  531  a \ s \ b \ s \ connected_component_set s a \ connected_component_set s b"  lp15@66827  532  apply (auto simp: connected_component_in)  lp15@66827  533  using connected_component_refl_eq  lp15@66827  534  apply blast  lp15@66827  535  apply (metis connected_component_eq mem_Collect_eq)  lp15@66827  536  apply (metis connected_component_eq mem_Collect_eq)  lp15@66827  537  done  lp15@66827  538 lp15@66827  539 lemma connected_component_overlap:  lp15@66827  540  "connected_component_set s a \ connected_component_set s b \ {} \  lp15@66827  541  a \ s \ b \ s \ connected_component_set s a = connected_component_set s b"  lp15@66827  542  by (auto simp: connected_component_nonoverlap)  lp15@66827  543 lp15@66827  544 lemma connected_component_sym_eq: "connected_component s x y \ connected_component s y x"  lp15@66827  545  using connected_component_sym by blast  lp15@66827  546 lp15@66827  547 lemma connected_component_eq_eq:  lp15@66827  548  "connected_component_set s x = connected_component_set s y \  lp15@66827  549  x \ s \ y \ s \ x \ s \ y \ s \ connected_component s x y"  lp15@66827  550  apply (cases "y \ s", simp)  lp15@66827  551  apply (metis connected_component_eq connected_component_eq_empty connected_component_refl_eq mem_Collect_eq)  lp15@66827  552  apply (cases "x \ s", simp)  lp15@66827  553  apply (metis connected_component_eq_empty)  lp15@66827  554  using connected_component_eq_empty  lp15@66827  555  apply blast  lp15@66827  556  done  lp15@66827  557 lp15@66827  558 lemma connected_iff_connected_component_eq:  lp15@66827  559  "connected s \ (\x \ s. \y \ s. connected_component_set s x = connected_component_set s y)"  lp15@66827  560  by (simp add: connected_component_eq_eq connected_iff_connected_component)  lp15@66827  561 lp15@66827  562 lemma connected_component_idemp:  lp15@66827  563  "connected_component_set (connected_component_set s x) x = connected_component_set s x"  lp15@66827  564  apply (rule subset_antisym)  lp15@66827  565  apply (simp add: connected_component_subset)  lp15@66827  566  apply (metis connected_component_eq_empty connected_component_maximal  lp15@66827  567  connected_component_refl_eq connected_connected_component mem_Collect_eq set_eq_subset)  lp15@66827  568  done  lp15@66827  569 lp15@66827  570 lemma connected_component_unique:  lp15@66827  571  "\x \ c; c \ s; connected c;  lp15@66827  572  \c'. x \ c' \ c' \ s \ connected c'  lp15@66827  573  \ c' \ c\  lp15@66827  574  \ connected_component_set s x = c"  lp15@66827  575 apply (rule subset_antisym)  lp15@66827  576 apply (meson connected_component_maximal connected_component_subset connected_connected_component contra_subsetD)  lp15@66827  577 by (simp add: connected_component_maximal)  lp15@66827  578 lp15@66827  579 lemma joinable_connected_component_eq:  lp15@66827  580  "\connected t; t \ s;  lp15@66827  581  connected_component_set s x \ t \ {};  lp15@66827  582  connected_component_set s y \ t \ {}\  lp15@66827  583  \ connected_component_set s x = connected_component_set s y"  lp15@66827  584 apply (simp add: ex_in_conv [symmetric])  lp15@66827  585 apply (rule connected_component_eq)  lp15@66827  586 by (metis (no_types, hide_lams) connected_component_eq_eq connected_component_in connected_component_maximal subsetD mem_Collect_eq)  lp15@66827  587 lp15@66827  588 lp15@66827  589 lemma Union_connected_component: "$$connected_component_set s  s) = s"  lp15@66827  590  apply (rule subset_antisym)  lp15@66827  591  apply (simp add: SUP_least connected_component_subset)  lp15@66827  592  using connected_component_refl_eq  lp15@66827  593  by force  lp15@66827  594 lp15@66827  595 lp15@66827  596 lemma complement_connected_component_unions:  lp15@66827  597  "s - connected_component_set s x =  lp15@66827  598  \(connected_component_set s  s - {connected_component_set s x})"  lp15@66827  599  apply (subst Union_connected_component [symmetric], auto)  lp15@66827  600  apply (metis connected_component_eq_eq connected_component_in)  lp15@66827  601  by (metis connected_component_eq mem_Collect_eq)  lp15@66827  602 lp15@66827  603 lemma connected_component_intermediate_subset:  lp15@66827  604  "\connected_component_set u a \ t; t \ u\  lp15@66827  605  \ connected_component_set t a = connected_component_set u a"  lp15@66827  606  apply (case_tac "a \ u")  lp15@66827  607  apply (simp add: connected_component_maximal connected_component_mono subset_antisym)  lp15@66827  608  using connected_component_eq_empty by blast  lp15@66827  609 lp15@66827  610 lp15@66827  611 subsection \The set of connected components of a set\  lp15@66827  612 immler@67962  613 definition%important components:: "'a::topological_space set \ 'a set set"  lp15@66827  614  where "components s \ connected_component_set s  s"  lp15@66827  615 lp15@66827  616 lemma components_iff: "s \ components u \ (\x. x \ u \ s = connected_component_set u x)"  lp15@66827  617  by (auto simp: components_def)  lp15@66827  618 lp15@66827  619 lemma componentsI: "x \ u \ connected_component_set u x \ components u"  lp15@66827  620  by (auto simp: components_def)  lp15@66827  621 lp15@66827  622 lemma componentsE:  lp15@66827  623  assumes "s \ components u"  lp15@66827  624  obtains x where "x \ u" "s = connected_component_set u x"  lp15@66827  625  using assms by (auto simp: components_def)  lp15@66827  626 lp15@66827  627 lemma Union_components [simp]: "\(components u) = u"  lp15@66827  628  apply (rule subset_antisym)  lp15@66827  629  using Union_connected_component components_def apply fastforce  lp15@66827  630  apply (metis Union_connected_component components_def set_eq_subset)  lp15@66827  631  done  lp15@66827  632 lp15@66827  633 lemma pairwise_disjoint_components: "pairwise (\X Y. X \ Y = {}) (components u)"  lp15@66827  634  apply (simp add: pairwise_def)  lp15@66827  635  apply (auto simp: components_iff)  lp15@66827  636  apply (metis connected_component_eq_eq connected_component_in)+  lp15@66827  637  done  lp15@66827  638 lp15@66827  639 lemma in_components_nonempty: "c \ components s \ c \ {}"  lp15@66827  640  by (metis components_iff connected_component_eq_empty)  lp15@66827  641 lp15@66827  642 lemma in_components_subset: "c \ components s \ c \ s"  lp15@66827  643  using Union_components by blast  lp15@66827  644 lp15@66827  645 lemma in_components_connected: "c \ components s \ connected c"  lp15@66827  646  by (metis components_iff connected_connected_component)  lp15@66827  647 lp15@66827  648 lemma in_components_maximal:  lp15@66827  649  "c \ components s \  lp15@66827  650  c \ {} \ c \ s \ connected c \ (\d. d \ {} \ c \ d \ d \ s \ connected d \ d = c)"  lp15@66827  651  apply (rule iffI)  lp15@66827  652  apply (simp add: in_components_nonempty in_components_connected)  lp15@66827  653  apply (metis (full_types) components_iff connected_component_eq_self connected_component_intermediate_subset connected_component_refl in_components_subset mem_Collect_eq rev_subsetD)  lp15@66827  654  apply (metis bot.extremum_uniqueI components_iff connected_component_eq_empty connected_component_maximal connected_component_subset connected_connected_component subset_emptyI)  lp15@66827  655  done  lp15@66827  656 lp15@66827  657 lemma joinable_components_eq:  lp15@66827  658  "connected t \ t \ s \ c1 \ components s \ c2 \ components s \ c1 \ t \ {} \ c2 \ t \ {} \ c1 = c2"  lp15@66827  659  by (metis (full_types) components_iff joinable_connected_component_eq)  lp15@66827  660 lp15@66827  661 lemma closed_components: "\closed s; c \ components s\ \ closed c"  lp15@66827  662  by (metis closed_connected_component components_iff)  lp15@66827  663 lp15@66827  664 lemma compact_components:  lp15@66827  665  fixes s :: "'a::heine_borel set"  lp15@66827  666  shows "\compact s; c \ components s\ \ compact c"  lp15@66827  667 by (meson bounded_subset closed_components in_components_subset compact_eq_bounded_closed)  lp15@66827  668 lp15@66827  669 lemma components_nonoverlap:  lp15@66827  670  "\c \ components s; c' \ components s\ \ (c \ c' = {}) \ (c \ c')"  lp15@66827  671  apply (auto simp: in_components_nonempty components_iff)  lp15@66827  672  using connected_component_refl apply blast  lp15@66827  673  apply (metis connected_component_eq_eq connected_component_in)  lp15@66827  674  by (metis connected_component_eq mem_Collect_eq)  lp15@66827  675 lp15@66827  676 lemma components_eq: "\c \ components s; c' \ components s\ \ (c = c' \ c \ c' \ {})"  lp15@66827  677  by (metis components_nonoverlap)  lp15@66827  678 lp15@66827  679 lemma components_eq_empty [simp]: "components s = {} \ s = {}"  lp15@66827  680  by (simp add: components_def)  lp15@66827  681 lp15@66827  682 lemma components_empty [simp]: "components {} = {}"  lp15@66827  683  by simp  lp15@66827  684 lp15@66827  685 lemma connected_eq_connected_components_eq: "connected s \ (\c \ components s. \c' \ components s. c = c')"  lp15@66827  686  by (metis (no_types, hide_lams) components_iff connected_component_eq_eq connected_iff_connected_component)  lp15@66827  687 lp15@66827  688 lemma components_eq_sing_iff: "components s = {s} \ connected s \ s \ {}"  lp15@66827  689  apply (rule iffI)  lp15@66827  690  using in_components_connected apply fastforce  lp15@66827  691  apply safe  lp15@66827  692  using Union_components apply fastforce  lp15@66827  693  apply (metis components_iff connected_component_eq_self)  lp15@66827  694  using in_components_maximal  lp15@66827  695  apply auto  lp15@66827  696  done  lp15@66827  697 lp15@66827  698 lemma components_eq_sing_exists: "(\a. components s = {a}) \ connected s \ s \ {}"  lp15@66827  699  apply (rule iffI)  lp15@66827  700  using connected_eq_connected_components_eq apply fastforce  lp15@66827  701  apply (metis components_eq_sing_iff)  lp15@66827  702  done  lp15@66827  703 lp15@66827  704 lemma connected_eq_components_subset_sing: "connected s \ components s \ {s}"  lp15@66827  705  by (metis Union_components components_empty components_eq_sing_iff connected_empty insert_subset order_refl subset_singletonD)  lp15@66827  706 lp15@66827  707 lemma connected_eq_components_subset_sing_exists: "connected s \ (\a. components s \ {a})"  lp15@66827  708  by (metis components_eq_sing_exists connected_eq_components_subset_sing empty_iff subset_iff subset_singletonD)  lp15@66827  709 lp15@66827  710 lemma in_components_self: "s \ components s \ connected s \ s \ {}"  lp15@66827  711  by (metis components_empty components_eq_sing_iff empty_iff in_components_connected insertI1)  lp15@66827  712 lp15@66827  713 lemma components_maximal: "\c \ components s; connected t; t \ s; c \ t \ {}\ \ t \ c"  lp15@66827  714  apply (simp add: components_def ex_in_conv [symmetric], clarify)  lp15@66827  715  by (meson connected_component_def connected_component_trans)  lp15@66827  716 lp15@66827  717 lemma exists_component_superset: "\t \ s; s \ {}; connected t\ \ \c. c \ components s \ t \ c"  lp15@66827  718  apply (cases "t = {}", force)  lp15@66827  719  apply (metis components_def ex_in_conv connected_component_maximal contra_subsetD image_eqI)  lp15@66827  720  done  lp15@66827  721 lp15@66827  722 lemma components_intermediate_subset: "\s \ components u; s \ t; t \ u\ \ s \ components t"  lp15@66827  723  apply (auto simp: components_iff)  lp15@66827  724  apply (metis connected_component_eq_empty connected_component_intermediate_subset)  lp15@66827  725  done  lp15@66827  726 lp15@66827  727 lemma in_components_unions_complement: "c \ components s \ s - c = \(components s - {c})"  lp15@66827  728  by (metis complement_connected_component_unions components_def components_iff)  lp15@66827  729 lp15@66827  730 lemma connected_intermediate_closure:  lp15@66827  731  assumes cs: "connected s" and st: "s \ t" and ts: "t \ closure s"  lp15@66827  732  shows "connected t"  lp15@66827  733 proof (rule connectedI)  lp15@66827  734  fix A B  lp15@66827  735  assume A: "open A" and B: "open B" and Alap: "A \ t \ {}" and Blap: "B \ t \ {}"  lp15@66827  736  and disj: "A \ B \ t = {}" and cover: "t \ A \ B"  lp15@66827  737  have disjs: "A \ B \ s = {}"  lp15@66827  738  using disj st by auto  lp15@66827  739  have "A \ closure s \ {}"  lp15@66827  740  using Alap Int_absorb1 ts by blast  lp15@66827  741  then have Alaps: "A \ s \ {}"  lp15@66827  742  by (simp add: A open_Int_closure_eq_empty)  lp15@66827  743  have "B \ closure s \ {}"  lp15@66827  744  using Blap Int_absorb1 ts by blast  lp15@66827  745  then have Blaps: "B \ s \ {}"  lp15@66827  746  by (simp add: B open_Int_closure_eq_empty)  lp15@66827  747  then show False  lp15@66827  748  using cs [unfolded connected_def] A B disjs Alaps Blaps cover st  lp15@66827  749  by blast  lp15@66827  750 qed  lp15@66827  751 lp15@66827  752 lemma closedin_connected_component: "closedin (subtopology euclidean s) (connected_component_set s x)"  lp15@66827  753 proof (cases "connected_component_set s x = {}")  lp15@66827  754  case True  lp15@66827  755  then show ?thesis  lp15@66827  756  by (metis closedin_empty)  lp15@66827  757 next  lp15@66827  758  case False  lp15@66827  759  then obtain y where y: "connected_component s x y"  lp15@66827  760  by blast  lp15@66827  761  have *: "connected_component_set s x \ s \ closure (connected_component_set s x)"  lp15@66827  762  by (auto simp: closure_def connected_component_in)  lp15@66827  763  have "connected_component s x y \ s \ closure (connected_component_set s x) \ connected_component_set s x"  lp15@66827  764  apply (rule connected_component_maximal, simp)  lp15@66827  765  using closure_subset connected_component_in apply fastforce  lp15@66827  766  using * connected_intermediate_closure apply blast+  lp15@66827  767  done  lp15@66827  768  with y * show ?thesis  lp15@66827  769  by (auto simp: closedin_closed)  lp15@66827  770 qed  lp15@66827  771 lp15@66939  772 lemma closedin_component:  lp15@66939  773  "C \ components s \ closedin (subtopology euclidean s) C"  lp15@66939  774  using closedin_connected_component componentsE by blast  lp15@66939  775 lp15@66827  776 lp15@66827  777 subsection \Intersecting chains of compact sets and the Baire property\  lp15@66827  778 immler@68607  779 proposition bounded_closed_chain:  lp15@66827  780  fixes \ :: "'a::heine_borel set set"  lp15@66827  781  assumes "B \ \" "bounded B" and \: "\S. S \ \ \ closed S" and "{} \ \"  lp15@66827  782  and chain: "\S T. S \ \ \ T \ \ \ S \ T \ T \ S"  lp15@66827  783  shows "\\ \ {}"  immler@68607  784 proof -  lp15@66827  785  have "B \ \\ \ {}"  lp15@66827  786  proof (rule compact_imp_fip)  lp15@66827  787  show "compact B" "\T. T \ \ \ closed T"  lp15@66827  788  by (simp_all add: assms compact_eq_bounded_closed)  lp15@66827  789  show "\finite \; \ \ \\ \ B \ \\ \ {}" for \  lp15@66827  790  proof (induction \ rule: finite_induct)  lp15@66827  791  case empty  lp15@66827  792  with assms show ?case by force  lp15@66827  793  next  lp15@66827  794  case (insert U$$  lp15@66827  795  then have "U \ \" and ne: "B \ \\ \ {}" by auto  lp15@66827  796  then consider "B \ U" | "U \ B"  lp15@66827  797  using \B \ \\ chain by blast  lp15@66827  798  then show ?case  lp15@66827  799  proof cases  lp15@66827  800  case 1  lp15@66827  801  then show ?thesis  lp15@66827  802  using Int_left_commute ne by auto  lp15@66827  803  next  lp15@66827  804  case 2  lp15@66827  805  have "U \ {}"  lp15@66827  806  using \U \ \\ \{} \ \\ by blast  lp15@66827  807  moreover  lp15@66827  808  have False if "\x. x \ U \ \Y\\. x \ Y"  lp15@66827  809  proof -  lp15@66827  810  have "\x. x \ U \ \Y\\. Y \ U"  lp15@66827  811  by (metis chain contra_subsetD insert.prems insert_subset that)  lp15@66827  812  then obtain Y where "Y \ \" "Y \ U"  lp15@66827  813  by (metis all_not_in_conv \U \ {}\)  lp15@66827  814  moreover obtain x where "x \ \\"  lp15@66827  815  by (metis Int_emptyI ne)  lp15@66827  816  ultimately show ?thesis  lp15@66827  817  by (metis Inf_lower subset_eq that)  lp15@66827  818  qed  lp15@66827  819  with 2 show ?thesis  lp15@66827  820  by blast  lp15@66827  821  qed  lp15@66827  822  qed  lp15@66827  823  qed  lp15@66827  824  then show ?thesis by blast  lp15@66827  825 qed  lp15@66827  826 immler@68607  827 corollary compact_chain:  lp15@66827  828  fixes \ :: "'a::heine_borel set set"  lp15@66827  829  assumes "\S. S \ \ \ compact S" "{} \ \"  lp15@66827  830  "\S T. S \ \ \ T \ \ \ S \ T \ T \ S"  lp15@66827  831  shows "\ \ \ {}"  immler@68607  832 proof (cases "\ = {}")  lp15@66827  833  case True  lp15@66827  834  then show ?thesis by auto  lp15@66827  835 next  lp15@66827  836  case False  lp15@66827  837  show ?thesis  lp15@66827  838  by (metis False all_not_in_conv assms compact_imp_bounded compact_imp_closed bounded_closed_chain)  lp15@66827  839 qed  lp15@66827  840 lp15@66827  841 lemma compact_nest:  lp15@66827  842  fixes F :: "'a::linorder \ 'b::heine_borel set"  lp15@66827  843  assumes F: "\n. compact(F n)" "\n. F n \ {}" and mono: "\m n. m \ n \ F n \ F m"  lp15@66827  844  shows "\range F \ {}"  lp15@66827  845 proof -  lp15@66827  846  have *: "\S T. S \ range F \ T \ range F \ S \ T \ T \ S"  lp15@66827  847  by (metis mono image_iff le_cases)  lp15@66827  848  show ?thesis  lp15@66827  849  apply (rule compact_chain [OF _ _ *])  lp15@66827  850  using F apply (blast intro: dest: *)+  lp15@66827  851  done  lp15@66827  852 qed  lp15@66827  853 lp15@66827  854 text\The Baire property of dense sets\  immler@68607  855 theorem Baire:  lp15@66827  856  fixes S::"'a::{real_normed_vector,heine_borel} set"  lp15@66827  857  assumes "closed S" "countable \"  lp15@66827  858  and ope: "\T. T \ \ \ openin (subtopology euclidean S) T \ S \ closure T"  lp15@66827  859  shows "S \ closure(\\)"  immler@68607  860 proof (cases "\ = {}")  lp15@66827  861  case True  lp15@66827  862  then show ?thesis  lp15@66827  863  using closure_subset by auto  lp15@66827  864 next  lp15@66827  865  let ?g = "from_nat_into \"  lp15@66827  866  case False  lp15@66827  867  then have gin: "?g n \ \" for n  lp15@66827  868  by (simp add: from_nat_into)  lp15@66827  869  show ?thesis  lp15@66827  870  proof (clarsimp simp: closure_approachable)  lp15@66827  871  fix x and e::real  lp15@66827  872  assume "x \ S" "0 < e"  lp15@66827  873  obtain TF where opeF: "\n. openin (subtopology euclidean S) (TF n)"  lp15@66827  874  and ne: "\n. TF n \ {}"  lp15@66827  875  and subg: "\n. S \ closure(TF n) \ ?g n"  lp15@66827  876  and subball: "\n. closure(TF n) \ ball x e"  lp15@66827  877  and decr: "\n. TF(Suc n) \ TF n"  lp15@66827  878  proof -  lp15@66827  879  have *: "\Y. (openin (subtopology euclidean S) Y \ Y \ {} \  lp15@66827  880  S \ closure Y \ ?g n \ closure Y \ ball x e) \ Y \ U"  lp15@66827  881  if opeU: "openin (subtopology euclidean S) U" and "U \ {}" and cloU: "closure U \ ball x e" for U n  lp15@66827  882  proof -  lp15@66827  883  obtain T where T: "open T" "U = T \ S"  lp15@66827  884  using \openin (subtopology euclidean S) U\ by (auto simp: openin_subtopology)  lp15@66827  885  with \U \ {}\ have "T \ closure (?g n) \ {}"  lp15@66827  886  using gin ope by fastforce  lp15@66827  887  then have "T \ ?g n \ {}"  lp15@66827  888  using \open T\ open_Int_closure_eq_empty by blast  lp15@66827  889  then obtain y where "y \ U" "y \ ?g n"  lp15@66827  890  using T ope [of "?g n", OF gin] by (blast dest: openin_imp_subset)  lp15@66827  891  moreover have "openin (subtopology euclidean S) (U \ ?g n)"  lp15@66827  892  using gin ope opeU by blast  lp15@66827  893  ultimately obtain d where U: "U \ ?g n \ S" and "d > 0" and d: "ball y d \ S \ U \ ?g n"  lp15@66827  894  by (force simp: openin_contains_ball)  lp15@66827  895  show ?thesis  lp15@66827  896  proof (intro exI conjI)  lp15@66827  897  show "openin (subtopology euclidean S) (S \ ball y (d/2))"  lp15@66827  898  by (simp add: openin_open_Int)  lp15@66827  899  show "S \ ball y (d/2) \ {}"  lp15@66827  900  using \0 < d\ \y \ U\ opeU openin_imp_subset by fastforce  lp15@66827  901  have "S \ closure (S \ ball y (d/2)) \ S \ closure (ball y (d/2))"  lp15@66827  902  using closure_mono by blast  lp15@66827  903  also have "... \ ?g n"  lp15@66827  904  using \d > 0\ d by force  lp15@66827  905  finally show "S \ closure (S \ ball y (d/2)) \ ?g n" .  lp15@66827  906  have "closure (S \ ball y (d/2)) \ S \ ball y d"  lp15@66827  907  proof -  lp15@66827  908  have "closure (ball y (d/2)) \ ball y d"  lp15@66827  909  using \d > 0\ by auto  lp15@66827  910  then have "closure (S \ ball y (d/2)) \ ball y d"  lp15@66827  911  by (meson closure_mono inf.cobounded2 subset_trans)  lp15@66827  912  then show ?thesis  lp15@66827  913  by (simp add: \closed S\ closure_minimal)  lp15@66827  914  qed  lp15@66827  915  also have "... \ ball x e"  lp15@66827  916  using cloU closure_subset d by blast  lp15@66827  917  finally show "closure (S \ ball y (d/2)) \ ball x e" .  lp15@66827  918  show "S \ ball y (d/2) \ U"  lp15@66827  919  using ball_divide_subset_numeral d by blast  lp15@66827  920  qed  lp15@66827  921  qed  lp15@66827  922  let ?\ = "\n X. openin (subtopology euclidean S) X \ X \ {} \  lp15@66827  923  S \ closure X \ ?g n \ closure X \ ball x e"  lp15@66827  924  have "closure (S \ ball x (e / 2)) \ closure(ball x (e/2))"  lp15@66827  925  by (simp add: closure_mono)  lp15@66827  926  also have "... \ ball x e"  lp15@66827  927  using \e > 0\ by auto  lp15@66827  928  finally have "closure (S \ ball x (e / 2)) \ ball x e" .  lp15@66827  929  moreover have"openin (subtopology euclidean S) (S \ ball x (e / 2))" "S \ ball x (e / 2) \ {}"  lp15@66827  930  using \0 < e\ \x \ S\ by auto  lp15@66827  931  ultimately obtain Y where Y: "?\ 0 Y \ Y \ S \ ball x (e / 2)"  lp15@66827  932  using * [of "S \ ball x (e/2)" 0] by metis  lp15@66827  933  show thesis  lp15@66827  934  proof (rule exE [OF dependent_nat_choice [of ?\ "\n X Y. Y \ X"]])  lp15@66827  935  show "\x. ?\ 0 x"  lp15@66827  936  using Y by auto  lp15@66827  937  show "\Y. ?\ (Suc n) Y \ Y \ X" if "?\ n X" for X n  lp15@66827  938  using that by (blast intro: *)  lp15@66827  939  qed (use that in metis)  lp15@66827  940  qed  lp15@66827  941  have "(\n. S \ closure (TF n)) \ {}"  lp15@66827  942  proof (rule compact_nest)  lp15@66827  943  show "\n. compact (S \ closure (TF n))"  lp15@66827  944  by (metis closed_closure subball bounded_subset_ballI compact_eq_bounded_closed closed_Int_compact [OF \closed S$)  lp15@66827  945  show "\n. S \ closure (TF n) \ {}"  lp15@66827  946  by (metis Int_absorb1 opeF \closed S\ closure_eq_empty closure_minimal ne openin_imp_subset)  lp15@66827  947  show "\m n. m \ n \ S \ closure (TF n) \ S \ closure (TF m)"  lp15@66827  948  by (meson closure_mono decr dual_order.refl inf_mono lift_Suc_antimono_le)  lp15@66827  949  qed  lp15@66827  950  moreover have "(\n. S \ closure (TF n)) \ {y \ \\. dist y x < e}"  lp15@66827  951  proof (clarsimp, intro conjI)  lp15@66827  952  fix y  lp15@66827  953  assume "y \ S" and y: "\n. y \ closure (TF n)"  lp15@66827  954  then show "\T\\. y \ T"  lp15@66827  955  by (metis Int_iff from_nat_into_surj [OF \countable \\] set_mp subg)  lp15@66827  956  show "dist y x < e"  lp15@66827  957  by (metis y dist_commute mem_ball subball subsetCE)  lp15@66827  958  qed  lp15@66827  959  ultimately show "\y \ \\. dist y x < e"  lp15@66827  960  by auto  lp15@66827  961  qed  lp15@66827  962 qed  lp15@66827  963 nipkow@67968  964 subsection%unimportant \Some theorems on sups and infs using the notion "bounded"\  lp15@66827  965 lp15@66827  966 lemma bounded_real: "bounded (S::real set) \ (\a. \x\S. \x\ \ a)"  lp15@66827  967  by (simp add: bounded_iff)  lp15@66827  968 lp15@66827  969 lemma bounded_imp_bdd_above: "bounded S \ bdd_above (S :: real set)"  lp15@66827  970  by (auto simp: bounded_def bdd_above_def dist_real_def)  lp15@66827  971  (metis abs_le_D1 abs_minus_commute diff_le_eq)  lp15@66827  972 lp15@66827  973 lemma bounded_imp_bdd_below: "bounded S \ bdd_below (S :: real set)"  lp15@66827  974  by (auto simp: bounded_def bdd_below_def dist_real_def)  lp15@66827  975  (metis abs_le_D1 add.commute diff_le_eq)  lp15@66827  976 lp15@66827  977 lemma bounded_inner_imp_bdd_above:  lp15@66827  978  assumes "bounded s"  lp15@66827  979  shows "bdd_above ((\x. x \ a)  s)"  lp15@66827  980 by (simp add: assms bounded_imp_bdd_above bounded_linear_image bounded_linear_inner_left)  lp15@66827  981 lp15@66827  982 lemma bounded_inner_imp_bdd_below:  lp15@66827  983  assumes "bounded s"  lp15@66827  984  shows "bdd_below ((\x. x \ a)  s)"  lp15@66827  985 by (simp add: assms bounded_imp_bdd_below bounded_linear_image bounded_linear_inner_left)  lp15@66827  986 lp15@66827  987 lemma bounded_has_Sup:  lp15@66827  988  fixes S :: "real set"  lp15@66827  989  assumes "bounded S"  lp15@66827  990  and "S \ {}"  lp15@66827  991  shows "\x\S. x \ Sup S"  lp15@66827  992  and "\b. (\x\S. x \ b) \ Sup S \ b"  lp15@66827  993 proof  lp15@66827  994  show "\b. (\x\S. x \ b) \ Sup S \ b"  lp15@66827  995  using assms by (metis cSup_least)  lp15@66827  996 qed (metis cSup_upper assms(1) bounded_imp_bdd_above)  lp15@66827  997 lp15@66827  998 lemma Sup_insert:  lp15@66827  999  fixes S :: "real set"  lp15@66827  1000  shows "bounded S \ Sup (insert x S) = (if S = {} then x else max x (Sup S))"  lp15@66827  1001  by (auto simp: bounded_imp_bdd_above sup_max cSup_insert_If)  lp15@66827  1002 lp15@66827  1003 lemma Sup_insert_finite:  lp15@66827  1004  fixes S :: "'a::conditionally_complete_linorder set"  lp15@66827  1005  shows "finite S \ Sup (insert x S) = (if S = {} then x else max x (Sup S))"  lp15@66827  1006 by (simp add: cSup_insert sup_max)  lp15@66827  1007 lp15@66827  1008 lemma bounded_has_Inf:  lp15@66827  1009  fixes S :: "real set"  lp15@66827  1010  assumes "bounded S"  lp15@66827  1011  and "S \ {}"  lp15@66827  1012  shows "\x\S. x \ Inf S"  lp15@66827  1013  and "\b. (\x\S. x \ b) \ Inf S \ b"  lp15@66827  1014 proof  lp15@66827  1015  show "\b. (\x\S. x \ b) \ Inf S \ b"  lp15@66827  1016  using assms by (metis cInf_greatest)  lp15@66827  1017 qed (metis cInf_lower assms(1) bounded_imp_bdd_below)  lp15@66827  1018 lp15@66827  1019 lemma Inf_insert:  lp15@66827  1020  fixes S :: "real set"  lp15@66827  1021  shows "bounded S \ Inf (insert x S) = (if S = {} then x else min x (Inf S))"  lp15@66827  1022  by (auto simp: bounded_imp_bdd_below inf_min cInf_insert_If)  lp15@66827  1023 lp15@66827  1024 lemma Inf_insert_finite:  lp15@66827  1025  fixes S :: "'a::conditionally_complete_linorder set"  lp15@66827  1026  shows "finite S \ Inf (insert x S) = (if S = {} then x else min x (Inf S))"  lp15@66827  1027 by (simp add: cInf_eq_Min)  lp15@66827  1028 lp15@66827  1029 lemma finite_imp_less_Inf:  lp15@66827  1030  fixes a :: "'a::conditionally_complete_linorder"  lp15@66827  1031  shows "\finite X; x \ X; \x. x\X \ a < x\ \ a < Inf X"  lp15@66827  1032  by (induction X rule: finite_induct) (simp_all add: cInf_eq_Min Inf_insert_finite)  lp15@66827  1033 lp15@66827  1034 lemma finite_less_Inf_iff:  lp15@66827  1035  fixes a :: "'a :: conditionally_complete_linorder"  lp15@66827  1036  shows "\finite X; X \ {}\ \ a < Inf X \ (\x \ X. a < x)"  lp15@66827  1037  by (auto simp: cInf_eq_Min)  lp15@66827  1038 lp15@66827  1039 lemma finite_imp_Sup_less:  lp15@66827  1040  fixes a :: "'a::conditionally_complete_linorder"  lp15@66827  1041  shows "\finite X; x \ X; \x. x\X \ a > x\ \ a > Sup X"  lp15@66827  1042  by (induction X rule: finite_induct) (simp_all add: cSup_eq_Max Sup_insert_finite)  lp15@66827  1043 lp15@66827  1044 lemma finite_Sup_less_iff:  lp15@66827  1045  fixes a :: "'a :: conditionally_complete_linorder"  lp15@66827  1046  shows "\finite X; X \ {}\ \ a > Sup X \ (\x \ X. a > x)"  lp15@66827  1047  by (auto simp: cSup_eq_Max)  lp15@66827  1048 lp15@66827  1049 proposition is_interval_compact:  lp15@66827  1050  "is_interval S \ compact S \ (\a b. S = cbox a b)" (is "?lhs = ?rhs")  lp15@66827  1051 proof (cases "S = {}")  lp15@66827  1052  case True  lp15@66827  1053  with empty_as_interval show ?thesis by auto  lp15@66827  1054 next  lp15@66827  1055  case False  lp15@66827  1056  show ?thesis  lp15@66827  1057  proof  lp15@66827  1058  assume L: ?lhs  lp15@66827  1059  then have "is_interval S" "compact S" by auto  lp15@66827  1060  define a where "a \ \i\Basis. (INF x:S. x \ i) *\<^sub>R i"  lp15@66827  1061  define b where "b \ \i\Basis. (SUP x:S. x \ i) *\<^sub>R i"  lp15@66827  1062  have 1: "\x i. \x \ S; i \ Basis\ \ (INF x:S. x \ i) \ x \ i"  lp15@66827  1063  by (simp add: cInf_lower bounded_inner_imp_bdd_below compact_imp_bounded L)  lp15@66827  1064  have 2: "\x i. \x \ S; i \ Basis\ \ x \ i \ (SUP x:S. x \ i)"  lp15@66827  1065  by (simp add: cSup_upper bounded_inner_imp_bdd_above compact_imp_bounded L)  lp15@66827  1066  have 3: "x \ S" if inf: "\i. i \ Basis \ (INF x:S. x \ i) \ x \ i"  lp15@66827  1067  and sup: "\i. i \ Basis \ x \ i \ (SUP x:S. x \ i)" for x  lp15@66827  1068  proof (rule mem_box_componentwiseI [OF \is_interval S\])  lp15@66827  1069  fix i::'a  lp15@66827  1070  assume i: "i \ Basis"  lp15@66827  1071  have cont: "continuous_on S (\x. x \ i)"  lp15@66827  1072  by (intro continuous_intros)  lp15@66827  1073  obtain a where "a \ S" and a: "\y. y\S \ a \ i \ y \ i"  lp15@66827  1074  using continuous_attains_inf [OF \compact S\ False cont] by blast  lp15@66827  1075  obtain b where "b \ S" and b: "\y. y\S \ y \ i \ b \ i"  lp15@66827  1076  using continuous_attains_sup [OF \compact S\ False cont] by blast  lp15@66827  1077  have "a \ i \ (INF x:S. x \ i)"  lp15@66827  1078  by (simp add: False a cINF_greatest)  lp15@66827  1079  also have "\ \ x \ i"  lp15@66827  1080  by (simp add: i inf)  lp15@66827  1081  finally have ai: "a \ i \ x \ i" .  lp15@66827  1082  have "x \ i \ (SUP x:S. x \ i)"  lp15@66827  1083  by (simp add: i sup)  lp15@66827  1084  also have "(SUP x:S. x \ i) \ b \ i"  lp15@66827  1085  by (simp add: False b cSUP_least)  lp15@66827  1086  finally have bi: "x \ i \ b \ i" .  lp15@66827  1087  show "x \ i \ (\x. x \ i)  S"  lp15@66827  1088  apply (rule_tac x="\j\Basis. (if j = i then x \ i else a \ j) *\<^sub>R j" in image_eqI)  lp15@66827  1089  apply (simp add: i)  lp15@66827  1090  apply (rule mem_is_intervalI [OF \is_interval S\ \a \ S\ \b \ S\])  lp15@66827  1091  using i ai bi apply force  lp15@66827  1092  done  lp15@66827  1093  qed  lp15@66827  1094  have "S = cbox a b"  lp15@66827  1095  by (auto simp: a_def b_def mem_box intro: 1 2 3)  lp15@66827  1096  then show ?rhs  lp15@66827  1097  by blast  lp15@66827  1098  next  lp15@66827  1099  assume R: ?rhs  lp15@66827  1100  then show ?lhs  lp15@66827  1101  using compact_cbox is_interval_cbox by blast  lp15@66827  1102  qed  lp15@66827  1103 qed  lp15@66827  1104 immler@67685  1105 text \Hence some handy theorems on distance, diameter etc. of/from a set.\  immler@67685  1106 immler@67685  1107 lemma distance_attains_sup:  immler@67685  1108  assumes "compact s" "s \ {}"  immler@67685  1109  shows "\x\s. \y\s. dist a y \ dist a x"  immler@67685  1110 proof (rule continuous_attains_sup [OF assms])  immler@67685  1111  {  immler@67685  1112  fix x  immler@67685  1113  assume "x\s"  immler@67685  1114  have "(dist a \ dist a x) (at x within s)"  immler@67685  1115  by (intro tendsto_dist tendsto_const tendsto_ident_at)  immler@67685  1116  }  immler@67685  1117  then show "continuous_on s (dist a)"  immler@67685  1118  unfolding continuous_on ..  immler@67685  1119 qed  immler@67685  1120 immler@67685  1121 text \For \emph{minimal} distance, we only need closure, not compactness.\  immler@67685  1122 immler@67685  1123 lemma distance_attains_inf:  immler@67685  1124  fixes a :: "'a::heine_borel"  immler@67685  1125  assumes "closed s" and "s \ {}"  immler@67685  1126  obtains x where "x\s" "\y. y \ s \ dist a x \ dist a y"  immler@67685  1127 proof -  immler@67685  1128  from assms obtain b where "b \ s" by auto  immler@67685  1129  let ?B = "s \ cball a (dist b a)"  immler@67685  1130  have "?B \ {}" using \b \ s\  immler@67685  1131  by (auto simp: dist_commute)  immler@67685  1132  moreover have "continuous_on ?B (dist a)"  immler@67685  1133  by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)  immler@67685  1134  moreover have "compact ?B"  immler@67685  1135  by (intro closed_Int_compact \closed s\ compact_cball)  immler@67685  1136  ultimately obtain x where "x \ ?B" "\y\?B. dist a x \ dist a y"  immler@67685  1137  by (metis continuous_attains_inf)  immler@67685  1138  with that show ?thesis by fastforce  immler@67685  1139 qed  immler@67685  1140 immler@67685  1141 nipkow@67968  1142 subsection%unimportant\Relations among convergence and absolute convergence for power series\  lp15@66827  1143 lp15@66827  1144 lemma summable_imp_bounded:  lp15@66827  1145  fixes f :: "nat \ 'a::real_normed_vector"  lp15@66827  1146  shows "summable f \ bounded (range f)"  lp15@66827  1147 by (frule summable_LIMSEQ_zero) (simp add: convergent_imp_bounded)  lp15@66827  1148 lp15@66827  1149 lemma summable_imp_sums_bounded:  lp15@66827  1150  "summable f \ bounded (range (\n. sum f {.. 'a::{real_normed_div_algebra,banach}" and w :: 'a  lp15@66827  1155  assumes sum: "summable (\n. a n * z ^ n)" and no: "norm w < norm z"  lp15@66827  1156  shows "summable (\n. of_real(norm(a n)) * w ^ n)"  lp15@66827  1157 proof -  lp15@66827  1158  obtain M where M: "\x. norm (a x * z ^ x) \ M"  lp15@66827  1159  using summable_imp_bounded [OF sum] by (force simp: bounded_iff)  lp15@66827  1160  then have *: "summable (\n. norm (a n) * norm w ^ n)"  lp15@66827  1161  by (rule_tac M=M in Abel_lemma) (auto simp: norm_mult norm_power intro: no)  lp15@66827  1162  show ?thesis  lp15@66827  1163  apply (rule series_comparison_complex [of "(\n. of_real(norm(a n) * norm w ^ n))"])  lp15@66827  1164  apply (simp only: summable_complex_of_real *)  lp15@66827  1165  apply (auto simp: norm_mult norm_power)  lp15@66827  1166  done  lp15@66827  1167 qed  lp15@66827  1168 immler@67962  1169 subsection%unimportant \Bounded closed nest property (proof does not use Heine-Borel)\  lp15@66827  1170 lp15@66827  1171 lemma bounded_closed_nest:  lp15@68302  1172  fixes S :: "nat \ ('a::heine_borel) set"  lp15@68302  1173  assumes "\n. closed (S n)"  lp15@68302  1174  and "\n. S n \ {}"  lp15@68302  1175  and "\m n. m \ n \ S n \ S m"  lp15@68302  1176  and "bounded (S 0)"  lp15@68302  1177  obtains a where "\n. a \ S n"  lp15@66827  1178 proof -  lp15@68302  1179  from assms(2) obtain x where x: "\n. x n \ S n"  lp15@68302  1180  using choice[of "\n x. x \ S n"] by auto  lp15@68302  1181  from assms(4,1) have "seq_compact (S 0)"  lp15@66827  1182  by (simp add: bounded_closed_imp_seq_compact)  lp15@68302  1183  then obtain l r where lr: "l \ S 0" "strict_mono r" "(x \ r) \ l"  lp15@66827  1184  using x and assms(3) unfolding seq_compact_def by blast  lp15@68302  1185  have "\n. l \ S n"  lp15@66827  1186  proof  lp15@66827  1187  fix n :: nat  lp15@68302  1188  have "closed (S n)"  lp15@66827  1189  using assms(1) by simp  lp15@68302  1190  moreover have "\i. (x \ r) i \ S i"  lp15@66827  1191  using x and assms(3) and lr(2) [THEN seq_suble] by auto  lp15@68302  1192  then have "\i. (x \ r) (i + n) \ S n"  lp15@66827  1193  using assms(3) by (fast intro!: le_add2)  lp15@66827  1194  moreover have "(\i. (x \ r) (i + n)) \ l"  lp15@66827  1195  using lr(3) by (rule LIMSEQ_ignore_initial_segment)  lp15@68302  1196  ultimately show "l \ S n"  lp15@66827  1197  by (rule closed_sequentially)  lp15@66827  1198  qed  lp15@68302  1199  then show ?thesis  lp15@68302  1200  using that by blast  lp15@66827  1201 qed  lp15@66827  1202 lp15@66827  1203 text \Decreasing case does not even need compactness, just completeness.\  lp15@66827  1204 lp15@66827  1205 lemma decreasing_closed_nest:  lp15@68302  1206  fixes S :: "nat \ ('a::complete_space) set"  lp15@68302  1207  assumes "\n. closed (S n)"  lp15@68302  1208  "\n. S n \ {}"  lp15@68302  1209  "\m n. m \ n \ S n \ S m"  lp15@68302  1210  "\e. e>0 \ \n. \x\S n. \y\S n. dist x y < e"  lp15@68302  1211  obtains a where "\n. a \ S n"  lp15@66827  1212 proof -  lp15@68302  1213  have "\n. \x. x \ S n"  lp15@66827  1214  using assms(2) by auto  lp15@68302  1215  then have "\t. \n. t n \ S n"  lp15@68302  1216  using choice[of "\n x. x \ S n"] by auto  lp15@68302  1217  then obtain t where t: "\n. t n \ S n" by auto  lp15@66827  1218  {  lp15@66827  1219  fix e :: real  lp15@66827  1220  assume "e > 0"  lp15@68302  1221  then obtain N where N: "\x\S N. \y\S N. dist x y < e"  lp15@68302  1222  using assms(4) by blast  lp15@66827  1223  {  lp15@66827  1224  fix m n :: nat  lp15@66827  1225  assume "N \ m \ N \ n"  lp15@68302  1226  then have "t m \ S N" "t n \ S N"  lp15@66827  1227  using assms(3) t unfolding subset_eq t by blast+  lp15@66827  1228  then have "dist (t m) (t n) < e"  lp15@66827  1229  using N by auto  lp15@66827  1230  }  lp15@66827  1231  then have "\N. \m n. N \ m \ N \ n \ dist (t m) (t n) < e"  lp15@66827  1232  by auto  lp15@66827  1233  }  lp15@66827  1234  then have "Cauchy t"  lp15@66827  1235  unfolding cauchy_def by auto  lp15@66827  1236  then obtain l where l:"(t \ l) sequentially"  lp15@66827  1237  using complete_UNIV unfolding complete_def by auto  lp15@68302  1238  { fix n :: nat  lp15@68302  1239  { fix e :: real  lp15@66827  1240  assume "e > 0"  lp15@66827  1241  then obtain N :: nat where N: "\n\N. dist (t n) l < e"  lp15@66827  1242  using l[unfolded lim_sequentially] by auto  lp15@68302  1243  have "t (max n N) \ S n"  lp15@66835  1244  by (meson assms(3) contra_subsetD max.cobounded1 t)  lp15@68302  1245  then have "\y\S n. dist y l < e"  lp15@66835  1246  using N max.cobounded2 by blast  lp15@66827  1247  }  lp15@68302  1248  then have "l \ S n"  lp15@68302  1249  using closed_approachable[of "S n" l] assms(1) by auto  lp15@66827  1250  }  lp15@68302  1251  then show ?thesis  lp15@68302  1252  using that by blast  lp15@66827  1253 qed  lp15@66827  1254 lp15@66827  1255 text \Strengthen it to the intersection actually being a singleton.\  lp15@66827  1256 lp15@66827  1257 lemma decreasing_closed_nest_sing:  lp15@68302  1258  fixes S :: "nat \ 'a::complete_space set"  lp15@68302  1259  assumes "\n. closed(S n)"  lp15@68302  1260  "\n. S n \ {}"  lp15@68302  1261  "\m n. m \ n \ S n \ S m"  lp15@68302  1262  "\e. e>0 \ \n. \x \ (S n). \ y$$S n). dist x y < e"  lp15@68302  1263  shows "\a. \(range S) = {a}"  lp15@66827  1264 proof -  lp15@68302  1265  obtain a where a: "\n. a \ S n"  lp15@68302  1266  using decreasing_closed_nest[of S] using assms by auto  lp15@68302  1267  { fix b  lp15@68302  1268  assume b: "b \ \(range S)"  lp15@68302  1269  { fix e :: real  lp15@66827  1270  assume "e > 0"  lp15@66827  1271  then have "dist a b < e"  lp15@66827  1272  using assms(4) and b and a by blast  lp15@66827  1273  }  lp15@66827  1274  then have "dist a b = 0"  lp15@66827  1275  by (metis dist_eq_0_iff dist_nz less_le)  lp15@66827  1276  }  lp15@68302  1277  with a have "\(range S) = {a}"  lp15@66827  1278  unfolding image_def by auto  lp15@66827  1279  then show ?thesis ..  lp15@66827  1280 qed  lp15@66827  1281 lp15@66827  1282 lp15@66827  1283 subsection \Infimum Distance\  lp15@66827  1284 immler@67962  1285 definition%important "infdist x A = (if A = {} then 0 else INF a:A. dist x a)"  lp15@66827  1286 nipkow@67459  1287 lemma bdd_below_image_dist[intro, simp]: "bdd_below (dist x  A)"  lp15@66827  1288  by (auto intro!: zero_le_dist)  lp15@66827  1289 lp15@66827  1290 lemma infdist_notempty: "A \ {} \ infdist x A = (INF a:A. dist x a)"  lp15@66827  1291  by (simp add: infdist_def)  lp15@66827  1292 lp15@66827  1293 lemma infdist_nonneg: "0 \ infdist x A"  lp15@66827  1294  by (auto simp: infdist_def intro: cINF_greatest)  lp15@66827  1295 lp15@66827  1296 lemma infdist_le: "a \ A \ infdist x A \ dist x a"  lp15@66827  1297  by (auto intro: cINF_lower simp add: infdist_def)  lp15@66827  1298 lp15@66827  1299 lemma infdist_le2: "a \ A \ dist x a \ d \ infdist x A \ d"  lp15@66827  1300  by (auto intro!: cINF_lower2 simp add: infdist_def)  lp15@66827  1301 lp15@66827  1302 lemma infdist_zero[simp]: "a \ A \ infdist a A = 0"  lp15@66827  1303  by (auto intro!: antisym infdist_nonneg infdist_le2)  lp15@66827  1304 lp15@66827  1305 lemma infdist_triangle: "infdist x A \ infdist y A + dist x y"  lp15@66827  1306 proof (cases "A = {}")  lp15@66827  1307  case True  lp15@66827  1308  then show ?thesis by (simp add: infdist_def)  lp15@66827  1309 next  lp15@66827  1310  case False  lp15@66827  1311  then obtain a where "a \ A" by auto  lp15@66827  1312  have "infdist x A \ Inf {dist x y + dist y a |a. a \ A}"  lp15@66827  1313  proof (rule cInf_greatest)  lp15@66827  1314  from \A \ {}\ show "{dist x y + dist y a |a. a \ A} \ {}"  lp15@66827  1315  by simp  lp15@66827  1316  fix d  lp15@66827  1317  assume "d \ {dist x y + dist y a |a. a \ A}"  lp15@66827  1318  then obtain a where d: "d = dist x y + dist y a" "a \ A"  lp15@66827  1319  by auto  lp15@66827  1320  show "infdist x A \ d"  lp15@66827  1321  unfolding infdist_notempty[OF \A \ {}\]  lp15@66827  1322  proof (rule cINF_lower2)  lp15@66827  1323  show "a \ A" by fact  lp15@66827  1324  show "dist x a \ d"  lp15@66827  1325  unfolding d by (rule dist_triangle)  lp15@66827  1326  qed simp  lp15@66827  1327  qed  lp15@66827  1328  also have "\ = dist x y + infdist y A"  lp15@66827  1329  proof (rule cInf_eq, safe)  lp15@66827  1330  fix a  lp15@66827  1331  assume "a \ A"  lp15@66827  1332  then show "dist x y + infdist y A \ dist x y + dist y a"  lp15@66827  1333  by (auto intro: infdist_le)  lp15@66827  1334  next  lp15@66827  1335  fix i  lp15@66827  1336  assume inf: "\d. d \ {dist x y + dist y a |a. a \ A} \ i \ d"  lp15@66827  1337  then have "i - dist x y \ infdist y A"  lp15@66827  1338  unfolding infdist_notempty[OF \A \ {}\] using \a \ A\  lp15@66827  1339  by (intro cINF_greatest) (auto simp: field_simps)  lp15@66827  1340  then show "i \ dist x y + infdist y A"  lp15@66827  1341  by simp  lp15@66827  1342  qed  lp15@66827  1343  finally show ?thesis by simp  lp15@66827  1344 qed  lp15@66827  1345 lp15@66827  1346 lemma in_closure_iff_infdist_zero:  lp15@66827  1347  assumes "A \ {}"  lp15@66827  1348  shows "x \ closure A \ infdist x A = 0"  lp15@66827  1349 proof  lp15@66827  1350  assume "x \ closure A"  lp15@66827  1351  show "infdist x A = 0"  lp15@66827  1352  proof (rule ccontr)  lp15@66827  1353  assume "infdist x A \ 0"  lp15@66827  1354  with infdist_nonneg[of x A] have "infdist x A > 0"  lp15@66827  1355  by auto  lp15@66827  1356  then have "ball x (infdist x A) \ closure A = {}"  lp15@66827  1357  apply auto  lp15@66827  1358  apply (metis \x \ closure A\ closure_approachable dist_commute infdist_le not_less)  lp15@66827  1359  done  lp15@66827  1360  then have "x \ closure A"  lp15@66827  1361  by (metis \0 < infdist x A\ centre_in_ball disjoint_iff_not_equal)  lp15@66827  1362  then show False using \x \ closure A\ by simp  lp15@66827  1363  qed  lp15@66827  1364 next  lp15@66827  1365  assume x: "infdist x A = 0"  lp15@66827  1366  then obtain a where "a \ A"  lp15@66827  1367  by atomize_elim (metis all_not_in_conv assms)  lp15@66827  1368  show "x \ closure A"  lp15@66827  1369  unfolding closure_approachable  lp15@66827  1370  apply safe  lp15@66827  1371  proof (rule ccontr)  lp15@66827  1372  fix e :: real  lp15@66827  1373  assume "e > 0"  lp15@66827  1374  assume "\ (\y\A. dist y x < e)"  lp15@66827  1375  then have "infdist x A \ e" using \a \ A\  lp15@66827  1376  unfolding infdist_def  lp15@66827  1377  by (force simp: dist_commute intro: cINF_greatest)  lp15@66827  1378  with x \e > 0\ show False by auto  lp15@66827  1379  qed  lp15@66827  1380 qed  lp15@66827  1381 lp15@66827  1382 lemma in_closed_iff_infdist_zero:  lp15@66827  1383  assumes "closed A" "A \ {}"  lp15@66827  1384  shows "x \ A \ infdist x A = 0"  lp15@66827  1385 proof -  lp15@66827  1386  have "x \ closure A \ infdist x A = 0"  lp15@66827  1387  by (rule in_closure_iff_infdist_zero) fact  lp15@66827  1388  with assms show ?thesis by simp  lp15@66827  1389 qed  lp15@66827  1390 nipkow@67455  1391 lemma infdist_pos_not_in_closed:  nipkow@67455  1392  assumes "closed S" "S \ {}" "x \ S"  nipkow@67455  1393  shows "infdist x S > 0"  nipkow@67455  1394 using in_closed_iff_infdist_zero[OF assms(1) assms(2), of x] assms(3) infdist_nonneg le_less by fastforce  nipkow@67455  1395 immler@67685  1396 lemma  immler@67685  1397  infdist_attains_inf:  immler@67685  1398  fixes X::"'a::heine_borel set"  immler@67685  1399  assumes "closed X"  immler@67685  1400  assumes "X \ {}"  immler@67685  1401  obtains x where "x \ X" "infdist y X = dist y x"  immler@67685  1402 proof -  immler@67685  1403  have "bdd_below (dist y  X)"  immler@67685  1404  by auto  immler@67685  1405  from distance_attains_inf[OF assms, of y]  immler@67685  1406  obtain x where INF: "x \ X" "\z. z \ X \ dist y x \ dist y z" by auto  immler@67685  1407  have "infdist y X = dist y x"  immler@67685  1408  by (auto simp: infdist_def assms  immler@67685  1409  intro!: antisym cINF_lower[OF _ \x \ X\] cINF_greatest[OF assms(2) INF(2)])  immler@67685  1410  with \x \ X\ show ?thesis ..  immler@67685  1411 qed  immler@67685  1412 immler@67685  1413 nipkow@67455  1414 text \Every metric space is a T4 space:\  nipkow@67455  1415 nipkow@67455  1416 instance metric_space \ t4_space  nipkow@67455  1417 proof  nipkow@67455  1418  fix S T::"'a set" assume H: "closed S" "closed T" "S \ T = {}"  nipkow@67455  1419  consider "S = {}" | "T = {}" | "S \ {} \ T \ {}" by auto  nipkow@67455  1420  then show "\U V. open U \ open V \ S \ U \ T \ V \ U \ V = {}"  nipkow@67455  1421  proof (cases)  nipkow@67455  1422  case 1  nipkow@67455  1423  show ?thesis  nipkow@67455  1424  apply (rule exI[of _ "{}"], rule exI[of _ UNIV]) using 1 by auto  nipkow@67455  1425  next  nipkow@67455  1426  case 2  nipkow@67455  1427  show ?thesis  nipkow@67455  1428  apply (rule exI[of _ UNIV], rule exI[of _ "{}"]) using 2 by auto  nipkow@67455  1429  next  nipkow@67455  1430  case 3  nipkow@67455  1431  define U where "U = (\x\S. ball x ((infdist x T)/2))"  nipkow@67455  1432  have A: "open U" unfolding U_def by auto  nipkow@67455  1433  have "infdist x T > 0" if "x \ S" for x  nipkow@67455  1434  using H that 3 by (auto intro!: infdist_pos_not_in_closed)  nipkow@67455  1435  then have B: "S \ U" unfolding U_def by auto  nipkow@67455  1436  define V where "V = (\x\T. ball x ((infdist x S)/2))"  nipkow@67455  1437  have C: "open V" unfolding V_def by auto  nipkow@67455  1438  have "infdist x S > 0" if "x \ T" for x  nipkow@67455  1439  using H that 3 by (auto intro!: infdist_pos_not_in_closed)  nipkow@67455  1440  then have D: "T \ V" unfolding V_def by auto  nipkow@67455  1441 nipkow@67455  1442  have "(ball x ((infdist x T)/2)) \ (ball y ((infdist y S)/2)) = {}" if "x \ S" "y \ T" for x y  nipkow@67455  1443  proof (auto)  nipkow@67455  1444  fix z assume H: "dist x z * 2 < infdist x T" "dist y z * 2 < infdist y S"  nipkow@67455  1445  have "2 * dist x y \ 2 * dist x z + 2 * dist y z"  nipkow@67455  1446  using dist_triangle[of x y z] by (auto simp add: dist_commute)  nipkow@67455  1447  also have "... < infdist x T + infdist y S"  nipkow@67455  1448  using H by auto  nipkow@67455  1449  finally have "dist x y < infdist x T \ dist x y < infdist y S"  nipkow@67455  1450  by auto  nipkow@67455  1451  then show False  nipkow@67455  1452  using infdist_le[OF \x \ S\, of y] infdist_le[OF \y \ T\, of x] by (auto simp add: dist_commute)  nipkow@67455  1453  qed  nipkow@67455  1454  then have E: "U \ V = {}"  nipkow@67455  1455  unfolding U_def V_def by auto  nipkow@67455  1456  show ?thesis  nipkow@67455  1457  apply (rule exI[of _ U], rule exI[of _ V]) using A B C D E by auto  nipkow@67455  1458  qed  nipkow@67455  1459 qed  nipkow@67455  1460 lp15@66827  1461 lemma tendsto_infdist [tendsto_intros]:  lp15@66827  1462  assumes f: "(f \ l) F"  lp15@66827  1463  shows "((\x. infdist (f x) A) \ infdist l A) F"  lp15@66827  1464 proof (rule tendstoI)  lp15@66827  1465  fix e ::real  lp15@66827  1466  assume "e > 0"  lp15@66827  1467  from tendstoD[OF f this]  lp15@66827  1468  show "eventually (\x. dist (infdist (f x) A) (infdist l A) < e) F"  lp15@66827  1469  proof (eventually_elim)  lp15@66827  1470  fix x  lp15@66827  1471  from infdist_triangle[of l A "f x"] infdist_triangle[of "f x" A l]  lp15@66827  1472  have "dist (infdist (f x) A) (infdist l A) \ dist (f x) l"  lp15@66827  1473  by (simp add: dist_commute dist_real_def)  lp15@66827  1474  also assume "dist (f x) l < e"  lp15@66827  1475  finally show "dist (infdist (f x) A) (infdist l A) < e" .  lp15@66827  1476  qed  lp15@66827  1477 qed  lp15@66827  1478 lp15@66827  1479 lemma continuous_infdist[continuous_intros]:  lp15@66827  1480  assumes "continuous F f"  lp15@66827  1481  shows "continuous F (\x. infdist (f x) A)"  lp15@66827  1482  using assms unfolding continuous_def by (rule tendsto_infdist)  lp15@66827  1483 immler@67685  1484 lemma compact_infdist_le:  immler@67685  1485  fixes A::"'a::heine_borel set"  immler@67685  1486  assumes "A \ {}"  immler@67685  1487  assumes "compact A"  immler@67685  1488  assumes "e > 0"  immler@67685  1489  shows "compact {x. infdist x A \ e}"  immler@67685  1490 proof -  immler@67685  1491  from continuous_closed_vimage[of "{0..e}" "\x. infdist x A"]  immler@67685  1492  continuous_infdist[OF continuous_ident, of _ UNIV A]  immler@67685  1493  have "closed {x. infdist x A \ e}" by (auto simp: vimage_def infdist_nonneg)  immler@67685  1494  moreover  immler@67685  1495  from assms obtain x0 b where b: "\x. x \ A \ dist x0 x \ b" "closed A"  immler@67685  1496  by (auto simp: compact_eq_bounded_closed bounded_def)  immler@67685  1497  {  immler@67685  1498  fix y  immler@67685  1499  assume le: "infdist y A \ e"  immler@67685  1500  from infdist_attains_inf[OF \closed A\ \A \ {}\, of y]  immler@67685  1501  obtain z where z: "z \ A" "infdist y A = dist y z" by blast  immler@67685  1502  have "dist x0 y \ dist y z + dist x0 z"  immler@67685  1503  by (metis dist_commute dist_triangle)  immler@67685  1504  also have "dist y z \ e" using le z by simp  immler@67685  1505  also have "dist x0 z \ b" using b z by simp  immler@67685  1506  finally have "dist x0 y \ b + e" by arith  immler@67685  1507  } then  immler@67685  1508  have "bounded {x. infdist x A \ e}"  immler@67685  1509  by (auto simp: bounded_any_center[where a=x0] intro!: exI[where x="b + e"])  immler@67685  1510  ultimately show "compact {x. infdist x A \ e}"  immler@67685  1511  by (simp add: compact_eq_bounded_closed)  immler@67685  1512 qed  immler@67685  1513 nipkow@67968  1514 subsection%unimportant \Equality of continuous functions on closure and related results\  lp15@66827  1515 lp15@66827  1516 lemma continuous_closedin_preimage_constant:  lp15@66827  1517  fixes f :: "_ \ 'b::t1_space"  lp15@66884  1518  shows "continuous_on S f \ closedin (subtopology euclidean S) {x \ S. f x = a}"  lp15@66884  1519  using continuous_closedin_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)  lp15@66827  1520 lp15@66827  1521 lemma continuous_closed_preimage_constant:  lp15@66827  1522  fixes f :: "_ \ 'b::t1_space"  lp15@66884  1523  shows "continuous_on S f \ closed S \ closed {x \ S. f x = a}"  lp15@66884  1524  using continuous_closed_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)  lp15@66827  1525 lp15@66827  1526 lemma continuous_constant_on_closure:  lp15@66827  1527  fixes f :: "_ \ 'b::t1_space"  lp15@66827  1528  assumes "continuous_on (closure S) f"  lp15@66827  1529  and "\x. x \ S \ f x = a"  lp15@66827  1530  and "x \ closure S"  lp15@66827  1531  shows "f x = a"  lp15@66827  1532  using continuous_closed_preimage_constant[of "closure S" f a]  lp15@66827  1533  assms closure_minimal[of S "{x \ closure S. f x = a}"] closure_subset  lp15@66827  1534  unfolding subset_eq  lp15@66827  1535  by auto  lp15@66827  1536 lp15@66827  1537 lemma image_closure_subset:  lp15@66884  1538  assumes contf: "continuous_on (closure S) f"  lp15@66884  1539  and "closed T"  lp15@66884  1540  and "(f  S) \ T"  lp15@66884  1541  shows "f  (closure S) \ T"  lp15@66827  1542 proof -  lp15@66884  1543  have "S \ {x \ closure S. f x \ T}"  lp15@66827  1544  using assms(3) closure_subset by auto  lp15@66884  1545  moreover have "closed (closure S \ f - T)"  lp15@66884  1546  using continuous_closed_preimage[OF contf] \closed T\ by auto  lp15@66884  1547  ultimately have "closure S = (closure S \ f - T)"  lp15@66884  1548  using closure_minimal[of S "(closure S \ f - T)"] by auto  lp15@66827  1549  then show ?thesis by auto  lp15@66827  1550 qed  lp15@66827  1551 lp15@66827  1552 lemma continuous_on_closure_norm_le:  lp15@66827  1553  fixes f :: "'a::metric_space \ 'b::real_normed_vector"  lp15@66827  1554  assumes "continuous_on (closure s) f"  lp15@66827  1555  and "\y \ s. norm(f y) \ b"  lp15@66827  1556  and "x \ (closure s)"  lp15@66827  1557  shows "norm (f x) \ b"  lp15@66827  1558 proof -  lp15@66827  1559  have *: "f  s \ cball 0 b"  lp15@66827  1560  using assms(2)[unfolded mem_cball_0[symmetric]] by auto  lp15@66827  1561  show ?thesis  lp15@66835  1562  by (meson "*" assms(1) assms(3) closed_cball image_closure_subset image_subset_iff mem_cball_0)  lp15@66827  1563 qed  lp15@66827  1564 lp15@66827  1565 lemma isCont_indicator:  lp15@66827  1566  fixes x :: "'a::t2_space"  lp15@66827  1567  shows "isCont (indicator A :: 'a \ real) x = (x \ frontier A)"  lp15@66827  1568 proof auto  lp15@66827  1569  fix x  lp15@66827  1570  assume cts_at: "isCont (indicator A :: 'a \ real) x" and fr: "x \ frontier A"  lp15@66827  1571  with continuous_at_open have 1: "\V::real set. open V \ indicator A x \ V \  lp15@66827  1572  (\U::'a set. open U \ x \ U \ (\y\U. indicator A y \ V))" by auto  lp15@66827  1573  show False  lp15@66827  1574  proof (cases "x \ A")  lp15@66827  1575  assume x: "x \ A"  lp15@66827  1576  hence "indicator A x \ ({0<..<2} :: real set)" by simp  lp15@66827  1577  hence "\U. open U \ x \ U \ (\y\U. indicator A y \ ({0<..<2} :: real set))"  lp15@66827  1578  using 1 open_greaterThanLessThan by blast  lp15@66827  1579  then guess U .. note U = this  lp15@66827  1580  hence "\y\U. indicator A y > (0::real)"  lp15@66827  1581  unfolding greaterThanLessThan_def by auto  lp15@66827  1582  hence "U \ A" using indicator_eq_0_iff by force  lp15@66827  1583  hence "x \ interior A" using U interiorI by auto  lp15@66827  1584  thus ?thesis using fr unfolding frontier_def by simp  lp15@66827  1585  next  lp15@66827  1586  assume x: "x \ A"  lp15@66827  1587  hence "indicator A x \ ({-1<..<1} :: real set)" by simp  lp15@66827  1588  hence "\U. open U \ x \ U \ (\y\U. indicator A y \ ({-1<..<1} :: real set))"  lp15@66827  1589  using 1 open_greaterThanLessThan by blast  lp15@66827  1590  then guess U .. note U = this  lp15@66827  1591  hence "\y\U. indicator A y < (1::real)"  lp15@66827  1592  unfolding greaterThanLessThan_def by auto  lp15@66827  1593  hence "U \ -A" by auto  lp15@66827  1594  hence "x \ interior (-A)" using U interiorI by auto  lp15@66827  1595  thus ?thesis using fr interior_complement unfolding frontier_def by auto  lp15@66827  1596  qed  lp15@66827  1597 next  lp15@66827  1598  assume nfr: "x \ frontier A"  lp15@66827  1599  hence "x \ interior A \ x \ interior (-A)"  lp15@66827  1600  by (auto simp: frontier_def closure_interior)  lp15@66827  1601  thus "isCont ((indicator A)::'a \ real) x"  lp15@66827  1602  proof  lp15@66827  1603  assume int: "x \ interior A"  lp15@66827  1604  then obtain U where U: "open U" "x \ U" "U \ A" unfolding interior_def by auto  lp15@66827  1605  hence "\y\U. indicator A y = (1::real)" unfolding indicator_def by auto  lp15@66827  1606  hence "continuous_on U (indicator A)" by (simp add: continuous_on_const indicator_eq_1_iff)  lp15@66827  1607  thus ?thesis using U continuous_on_eq_continuous_at by auto  lp15@66827  1608  next  lp15@66827  1609  assume ext: "x \ interior (-A)"  lp15@66827  1610  then obtain U where U: "open U" "x \ U" "U \ -A" unfolding interior_def by auto  lp15@66827  1611  then have "continuous_on U (indicator A)"  lp15@66827  1612  using continuous_on_topological by (auto simp: subset_iff)  lp15@66827  1613  thus ?thesis using U continuous_on_eq_continuous_at by auto  lp15@66827  1614  qed  lp15@66827  1615 qed  lp15@66827  1616 immler@67962  1617 subsection%unimportant \A function constant on a set\  lp15@66827  1618 lp15@66827  1619 definition constant_on (infixl "(constant'_on)" 50)  lp15@66827  1620  where "f constant_on A \ \y. \x\A. f x = y"  lp15@66827  1621 lp15@66827  1622 lemma constant_on_subset: "\f constant_on A; B \ A\ \ f constant_on B"  lp15@66827  1623  unfolding constant_on_def by blast  lp15@66827  1624 lp15@66827  1625 lemma injective_not_constant:  lp15@66827  1626  fixes S :: "'a::{perfect_space} set"  lp15@66827  1627  shows "\open S; inj_on f S; f constant_on S\ \ S = {}"  lp15@66827  1628 unfolding constant_on_def  lp15@66827  1629 by (metis equals0I inj_on_contraD islimpt_UNIV islimpt_def)  lp15@66827  1630 lp15@66827  1631 lemma constant_on_closureI:  lp15@66827  1632  fixes f :: "_ \ 'b::t1_space"  lp15@66827  1633  assumes cof: "f constant_on S" and contf: "continuous_on (closure S) f"  lp15@66827  1634  shows "f constant_on (closure S)"  lp15@66827  1635 using continuous_constant_on_closure [OF contf] cof unfolding constant_on_def  lp15@66827  1636 by metis  lp15@66827  1637 immler@67962  1638 subsection%unimportant\Relating linear images to open/closed/interior/closure\  lp15@66827  1639 lp15@66827  1640 proposition open_surjective_linear_image:  lp15@66827  1641  fixes f :: "'a::real_normed_vector \ 'b::euclidean_space"  lp15@66827  1642  assumes "open A" "linear f" "surj f"  lp15@66827  1643  shows "open(f  A)"  lp15@66827  1644 unfolding open_dist  lp15@66827  1645 proof clarify  lp15@66827  1646  fix x  lp15@66827  1647  assume "x \ A"  lp15@66827  1648  have "bounded (inv f  Basis)"  lp15@66827  1649  by (simp add: finite_imp_bounded)  lp15@66827  1650  with bounded_pos obtain B where "B > 0" and B: "\x. x \ inv f  Basis \ norm x \ B"  lp15@66827  1651  by metis  lp15@66827  1652  obtain e where "e > 0" and e: "\z. dist z x < e \ z \ A"  lp15@66827  1653  by (metis open_dist \x \ A\ \open A$$  lp15@66827  1654  define \ where "\ \ e / B / DIM('b)"  lp15@66827  1655  show "\e>0. \y. dist y (f x) < e \ y \ f  A"  lp15@66827  1656  proof (intro exI conjI)  lp15@66827  1657  show "\ > 0"  lp15@66827  1658  using \e > 0\ \B > 0\ by (simp add: \_def divide_simps)  lp15@66827  1659  have "y \ f  A" if "dist y (f x) * (B * real DIM('b)) < e" for y  lp15@66827  1660  proof -  lp15@66827  1661  define u where "u \ y - f x"  lp15@66827  1662  show ?thesis  lp15@66827  1663  proof (rule image_eqI)  lp15@66827  1664  show "y = f (x + (\i\Basis. (u \ i) *\<^sub>R inv f i))"  lp15@66827  1665  apply (simp add: linear_add linear_sum linear.scaleR \linear f\ surj_f_inv_f \surj f\)  lp15@66827  1666  apply (simp add: euclidean_representation u_def)  lp15@66827  1667  done  lp15@66827  1668  have "dist (x + (\i\Basis. (u \ i) *\<^sub>R inv f i)) x \ (\i\Basis. norm ((u \ i) *\<^sub>R inv f i))"  lp15@66827  1669  by (simp add: dist_norm sum_norm_le)  lp15@66827  1670  also have "... = (\i\Basis. \u \ i\ * norm (inv f i))"  lp15@66827  1671  by simp  lp15@66827  1672  also have "... \ (\i\Basis. \u \ i\) * B"  lp15@66827  1673  by (simp add: B sum_distrib_right sum_mono mult_left_mono)  lp15@66827  1674  also have "... \ DIM('b) * dist y (f x) * B"  lp15@66827  1675  apply (rule mult_right_mono [OF sum_bounded_above])  lp15@66827  1676  using \0 < B\ by (auto simp: Basis_le_norm dist_norm u_def)  lp15@66827  1677  also have "... < e"  lp15@66827  1678  by (metis mult.commute mult.left_commute that)  lp15@66827  1679  finally show "x + (\i\Basis. (u \ i) *\<^sub>R inv f i) \ A"  lp15@66827  1680  by (rule e)  lp15@66827  1681  qed  lp15@66827  1682  qed  lp15@66827  1683  then show "\y. dist y (f x) < \ \ y \ f  A"  lp15@66827  1684  using \e > 0\ \B > 0\  lp15@66827  1685  by (auto simp: \_def divide_simps mult_less_0_iff)  lp15@66827  1686  qed  lp15@66827  1687 qed  lp15@66827  1688 lp15@66827  1689 corollary open_bijective_linear_image_eq:  lp15@66827  1690  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"  lp15@66827  1691  assumes "linear f" "bij f"  lp15@66827  1692  shows "open(f  A) \ open A"  lp15@66827  1693 proof  lp15@66827  1694  assume "open(f  A)"  lp15@66827  1695  then have "open(f - (f  A))"  lp15@66827  1696  using assms by (force simp: linear_continuous_at linear_conv_bounded_linear continuous_open_vimage)  lp15@66827  1697  then show "open A"  lp15@66827  1698  by (simp add: assms bij_is_inj inj_vimage_image_eq)  lp15@66827  1699 next  lp15@66827  1700  assume "open A"  lp15@66827  1701  then show "open(f  A)"  lp15@66827  1702  by (simp add: assms bij_is_surj open_surjective_linear_image)  lp15@66827  1703 qed  lp15@66827  1704 lp15@66827  1705 corollary interior_bijective_linear_image:  lp15@66827  1706  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"  lp15@66827  1707  assumes "linear f" "bij f"  lp15@66827  1708  shows "interior (f  S) = f  interior S" (is "?lhs = ?rhs")  lp15@66827  1709 proof safe  lp15@66827  1710  fix x  lp15@66827  1711  assume x: "x \ ?lhs"  lp15@66827  1712  then obtain T where "open T" and "x \ T" and "T \ f  S"  lp15@66827  1713  by (metis interiorE)  lp15@66827  1714  then show "x \ ?rhs"  lp15@66827  1715  by (metis (no_types, hide_lams) assms subsetD interior_maximal open_bijective_linear_image_eq subset_image_iff)  lp15@66827  1716 next  lp15@66827  1717  fix x  lp15@66827  1718  assume x: "x \ interior S"  lp15@66827  1719  then show "f x \ interior (f  S)"  lp15@66827  1720  by (meson assms imageI image_mono interiorI interior_subset open_bijective_linear_image_eq open_interior)  lp15@66827  1721 qed  lp15@66827  1722 lp15@66827  1723 lemma interior_injective_linear_image:  lp15@66827  1724  fixes f :: "'a::euclidean_space \ 'a::euclidean_space"  lp15@66827  1725  assumes "linear f" "inj f"  lp15@66827  1726  shows "interior(f  S) = f  (interior S)"  lp15@66827  1727  by (simp add: linear_injective_imp_surjective assms bijI interior_bijective_linear_image)  lp15@66827  1728 lp15@66827  1729 lemma interior_surjective_linear_image:  lp15@66827  1730  fixes f :: "'a::euclidean_space \ 'a::euclidean_space"  lp15@66827  1731  assumes "linear f" "surj f"  lp15@66827  1732  shows "interior(f  S) = f  (interior S)"  lp15@66827  1733  by (simp add: assms interior_injective_linear_image linear_surjective_imp_injective)  lp15@66827  1734 lp15@66827  1735 lemma interior_negations:  lp15@66827  1736  fixes S :: "'a::euclidean_space set"  lp15@66827  1737  shows "interior(uminus  S) = image uminus (interior S)"  lp15@66827  1738  by (simp add: bij_uminus interior_bijective_linear_image linear_uminus)  lp15@66827  1739 lp15@66827  1740 text \Preservation of compactness and connectedness under continuous function.\  lp15@66827  1741 lp15@66827  1742 lemma compact_eq_openin_cover:  lp15@66827  1743  "compact S \  lp15@66827  1744  (\C. (\c\C. openin (subtopology euclidean S) c) \ S \ \C \  lp15@66827  1745  (\D\C. finite D \ S \ \D))"  lp15@66827  1746 proof safe  lp15@66827  1747  fix C  lp15@66827  1748  assume "compact S" and "\c\C. openin (subtopology euclidean S) c" and "S \ \C"  lp15@66827  1749  then have "\c\{T. open T \ S \ T \ C}. open c" and "S \ \{T. open T \ S \ T \ C}"  lp15@66827  1750  unfolding openin_open by force+  lp15@66827  1751  with \compact S\ obtain D where "D \ {T. open T \ S \ T \ C}" and "finite D" and "S \ \D"  lp15@66827  1752  by (meson compactE)  lp15@66827  1753  then have "image (\T. S \ T) D \ C \ finite (image (\T. S \ T) D) \ S \ $$image (\T. S \ T) D)"  lp15@66827  1754  by auto  lp15@66827  1755  then show "\D\C. finite D \ S \ \D" ..  lp15@66827  1756 next  lp15@66827  1757  assume 1: "\C. (\c\C. openin (subtopology euclidean S) c) \ S \ \C \  lp15@66827  1758  (\D\C. finite D \ S \ \D)"  lp15@66827  1759  show "compact S"  lp15@66827  1760  proof (rule compactI)  lp15@66827  1761  fix C  lp15@66827  1762  let ?C = "image (\T. S \ T) C"  lp15@66827  1763  assume "\t\C. open t" and "S \ \C"  lp15@66827  1764  then have "(\c\?C. openin (subtopology euclidean S) c) \ S \ \?C"  lp15@66827  1765  unfolding openin_open by auto  lp15@66827  1766  with 1 obtain D where "D \ ?C" and "finite D" and "S \ \D"  lp15@66827  1767  by metis  lp15@66827  1768  let ?D = "inv_into C (\T. S \ T)  D"  lp15@66827  1769  have "?D \ C \ finite ?D \ S \ \?D"  lp15@66827  1770  proof (intro conjI)  lp15@66827  1771  from \D \ ?C\ show "?D \ C"  lp15@66827  1772  by (fast intro: inv_into_into)  lp15@66827  1773  from \finite D\ show "finite ?D"  lp15@66827  1774  by (rule finite_imageI)  lp15@66827  1775  from \S \ \D\ show "S \ \?D"  lp15@66827  1776  apply (rule subset_trans, clarsimp)  lp15@66827  1777  apply (frule subsetD [OF \D \ ?C\, THEN f_inv_into_f])  lp15@66827  1778  apply (erule rev_bexI, fast)  lp15@66827  1779  done  lp15@66827  1780  qed  lp15@66827  1781  then show "\D\C. finite D \ S \ \D" ..  lp15@66827  1782  qed  lp15@66827  1783 qed  lp15@66827  1784 immler@67962  1785 subsection%unimportant\ Theorems relating continuity and uniform continuity to closures\  lp15@66827  1786 lp15@66827  1787 lemma continuous_on_closure:  lp15@66827  1788  "continuous_on (closure S) f \  lp15@66827  1789  (\x e. x \ closure S \ 0 < e  lp15@66827  1790  \ (\d. 0 < d \ (\y. y \ S \ dist y x < d \ dist (f y) (f x) < e)))"  lp15@66827  1791  (is "?lhs = ?rhs")  lp15@66827  1792 proof  lp15@66827  1793  assume ?lhs then show ?rhs  lp15@66827  1794  unfolding continuous_on_iff by (metis Un_iff closure_def)  lp15@66827  1795 next  lp15@66827  1796  assume R [rule_format]: ?rhs  lp15@66827  1797  show ?lhs  lp15@66827  1798  proof  lp15@66827  1799  fix x and e::real  lp15@66827  1800  assume "0 < e" and x: "x \ closure S"  lp15@66827  1801  obtain \::real where "\ > 0"  lp15@66827  1802  and \: "\y. \y \ S; dist y x < \\ \ dist (f y) (f x) < e/2"  lp15@66827  1803  using R [of x "e/2"] \0 < e\ x by auto  lp15@66827  1804  have "dist (f y) (f x) \ e" if y: "y \ closure S" and dyx: "dist y x < \/2" for y  lp15@66827  1805  proof -  lp15@66827  1806  obtain \'::real where "\' > 0"  lp15@66827  1807  and \': "\z. \z \ S; dist z y < \'\ \ dist (f z) (f y) < e/2"  lp15@66827  1808  using R [of y "e/2"] \0 < e\ y by auto  lp15@66827  1809  obtain z where "z \ S" and z: "dist z y < min \' \ / 2"  lp15@66827  1810  using closure_approachable y  lp15@66827  1811  by (metis \0 < \'\ \0 < \\ divide_pos_pos min_less_iff_conj zero_less_numeral)  lp15@66827  1812  have "dist (f z) (f y) < e/2"  lp15@66827  1813  apply (rule \' [OF \z \ S\])  lp15@66827  1814  using z \0 < \'\ by linarith  lp15@66827  1815  moreover have "dist (f z) (f x) < e/2"  lp15@66827  1816  apply (rule \ [OF \z \ S\])  lp15@66827  1817  using z \0 < \\ dist_commute[of y z] dist_triangle_half_r [of y] dyx by auto  lp15@66827  1818  ultimately show ?thesis  lp15@66827  1819  by (metis dist_commute dist_triangle_half_l less_imp_le)  lp15@66827  1820  qed  lp15@66827  1821  then show "\d>0. \x'\closure S. dist x' x < d \ dist (f x') (f x) \ e"  lp15@66827  1822  by (rule_tac x="\/2" in exI) (simp add: \\ > 0$$  lp15@66827  1823  qed  lp15@66827  1824 qed  lp15@66827  1825 lp15@66827  1826 lemma continuous_on_closure_sequentially:  lp15@66827  1827  fixes f :: "'a::metric_space \ 'b :: metric_space"  lp15@66827  1828  shows  lp15@66827  1829  "continuous_on (closure S) f \  lp15@66827  1830  (\x a. a \ closure S \ (\n. x n \ S) \ x \ a \ (f \ x) \ f a)"  lp15@66827  1831  (is "?lhs = ?rhs")  lp15@66827  1832 proof -  lp15@66827  1833  have "continuous_on (closure S) f \  lp15@66827  1834  (\x \ closure S. continuous (at x within S) f)"  lp15@66827  1835  by (force simp: continuous_on_closure continuous_within_eps_delta)  lp15@66827  1836  also have "... = ?rhs"  lp15@66827  1837  by (force simp: continuous_within_sequentially)  lp15@66827  1838  finally show ?thesis .  lp15@66827  1839 qed  lp15@66827  1840 lp15@66827  1841 lemma uniformly_continuous_on_closure:  lp15@66827  1842  fixes f :: "'a::metric_space \ 'b::metric_space"  lp15@66827  1843  assumes ucont: "uniformly_continuous_on S f"  lp15@66827  1844  and cont: "continuous_on (closure S) f"  lp15@66827  1845  shows "uniformly_continuous_on (closure S) f"  lp15@66827  1846 unfolding uniformly_continuous_on_def  lp15@66827  1847 proof (intro allI impI)  lp15@66827  1848  fix e::real  lp15@66827  1849  assume "0 < e"  lp15@66827  1850  then obtain d::real  lp15@66827  1851  where "d>0"  lp15@66827  1852  and d: "\x x'. \x\S; x'\S; dist x' x < d\ \ dist (f x') (f x) < e/3"  lp15@66827  1853  using ucont [unfolded uniformly_continuous_on_def, rule_format, of "e/3"] by auto  lp15@66827  1854  show "\d>0. \x\closure S. \x'\closure S. dist x' x < d \ dist (f x') (f x) < e"  lp15@66827  1855  proof (rule exI [where x="d/3"], clarsimp simp: \d > 0\)  lp15@66827  1856  fix x y  lp15@66827  1857  assume x: "x \ closure S" and y: "y \ closure S" and dyx: "dist y x * 3 < d"  lp15@66827  1858  obtain d1::real where "d1 > 0"  lp15@66827  1859  and d1: "\w. \w \ closure S; dist w x < d1\ \ dist (f w) (f x) < e/3"  lp15@66827  1860  using cont [unfolded continuous_on_iff, rule_format, of "x" "e/3"] \0 < e\ x by auto  lp15@66827  1861  obtain x' where "x' \ S" and x': "dist x' x < min d1 (d / 3)"  lp15@66827  1862  using closure_approachable [of x S]  lp15@66827  1863  by (metis \0 < d1\ \0 < d\ divide_pos_pos min_less_iff_conj x zero_less_numeral)  lp15@66827  1864  obtain d2::real where "d2 > 0"  lp15@66827  1865  and d2: "\w \ closure S. dist w y < d2 \ dist (f w) (f y) < e/3"  lp15@66827  1866  using cont [unfolded continuous_on_iff, rule_format, of "y" "e/3"] \0 < e\ y by auto  lp15@66827  1867  obtain y' where "y' \ S" and y': "dist y' y < min d2 (d / 3)"  lp15@66827  1868  using closure_approachable [of y S]  lp15@66827  1869  by (metis \0 < d2\ \0 < d\ divide_pos_pos min_less_iff_conj y zero_less_numeral)  lp15@66827  1870  have "dist x' x < d/3" using x' by auto  lp15@66827  1871  moreover have "dist x y < d/3"  lp15@66827  1872  by (metis dist_commute dyx less_divide_eq_numeral1(1))  lp15@66827  1873  moreover have "dist y y' < d/3"  lp15@66827  1874  by (metis (no_types) dist_commute min_less_iff_conj y')  lp15@66827  1875  ultimately have "dist x' y' < d/3 + d/3 + d/3"  lp15@66827  1876  by (meson dist_commute_lessI dist_triangle_lt add_strict_mono)  lp15@66827  1877  then have "dist x' y' < d" by simp  lp15@66827  1878  then have "dist (f x') (f y') < e/3"  lp15@66827  1879  by (rule d [OF \y' \ S\ \x' \ S\])  lp15@66827  1880  moreover have "dist (f x') (f x) < e/3" using \x' \ S\ closure_subset x' d1  lp15@66827  1881  by (simp add: closure_def)  lp15@66827  1882  moreover have "dist (f y') (f y) < e/3" using \y' \ S\ closure_subset y' d2  lp15@66827  1883  by (simp add: closure_def)  lp15@66827  1884  ultimately have "dist (f y) (f x) < e/3 + e/3 + e/3"  lp15@66827  1885  by (meson dist_commute_lessI dist_triangle_lt add_strict_mono)  lp15@66827  1886  then show "dist (f y) (f x) < e" by simp  lp15@66827  1887  qed  lp15@66827  1888 qed  lp15@66827  1889 lp15@66827  1890 lemma uniformly_continuous_on_extension_at_closure:  lp15@66827  1891  fixes f::"'a::metric_space \ 'b::complete_space"  lp15@66827  1892  assumes uc: "uniformly_continuous_on X f"  lp15@66827  1893  assumes "x \ closure X"  lp15@66827  1894  obtains l where "(f \ l) (at x within X)"  lp15@66827  1895 proof -  lp15@66827  1896  from assms obtain xs where xs: "xs \ x" "\n. xs n \ X"  lp15@66827  1897  by (auto simp: closure_sequential)  lp15@66827  1898 lp15@66827  1899  from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF xs]  lp15@66827  1900  obtain l where l: "(\n. f (xs n)) \ l"  lp15@66827  1901  by atomize_elim (simp only: convergent_eq_Cauchy)  lp15@66827  1902 lp15@66827  1903  have "(f \ l) (at x within X)"  lp15@66827  1904  proof (safe intro!: Lim_within_LIMSEQ)  lp15@66827  1905  fix xs'  lp15@66827  1906  assume "\n. xs' n \ x \ xs' n \ X"  lp15@66827  1907  and xs': "xs' \ x"  lp15@66827  1908  then have "xs' n \ x" "xs' n \ X" for n by auto  lp15@66827  1909 lp15@66827  1910  from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF \xs' \ x\ \xs' _ \ X\]  lp15@66827  1911  obtain l' where l': "(\n. f (xs' n)) \ l'"  lp15@66827  1912  by atomize_elim (simp only: convergent_eq_Cauchy)  lp15@66827  1913 lp15@66827  1914  show "(\n. f (xs' n)) \ l"  lp15@66827  1915  proof (rule tendstoI)  lp15@66827  1916  fix e::real assume "e > 0"  lp15@66827  1917  define e' where "e' \ e / 2"  lp15@66827  1918  have "e' > 0" using \e > 0\ by (simp add: e'_def)  lp15@66827  1919 lp15@66827  1920  have "\\<^sub>F n in sequentially. dist (f (xs n)) l < e'"  lp15@66827  1921  by (simp add: \0 < e'\ l tendstoD)  lp15@66827  1922  moreover  lp15@66827  1923  from uc[unfolded uniformly_continuous_on_def, rule_format, OF \e' > 0\]  lp15@66827  1924  obtain d where d: "d > 0" "\x x'. x \ X \ x' \ X \ dist x x' < d \ dist (f x) (f x') < e'"  lp15@66827  1925  by auto  lp15@66827  1926  have "\\<^sub>F n in sequentially. dist (xs n) (xs' n) < d"  lp15@66827  1927  by (auto intro!: \0 < d\ order_tendstoD tendsto_eq_intros xs xs')  lp15@66827  1928  ultimately  lp15@66827  1929  show "\\<^sub>F n in sequentially. dist (f (xs' n)) l < e"  lp15@66827  1930  proof eventually_elim  lp15@66827  1931  case (elim n)  lp15@66827  1932  have "dist (f (xs' n)) l \ dist (f (xs n)) (f (xs' n)) + dist (f (xs n)) l"  lp15@66827  1933  by (metis dist_triangle dist_commute)  lp15@66827  1934  also have "dist (f (xs n)) (f (xs' n)) < e'"  lp15@66827  1935  by (auto intro!: d xs \xs' _ \ _\ elim)  lp15@66827  1936  also note \dist (f (xs n)) l < e'\  lp15@66827  1937  also have "e' + e' = e" by (simp add: e'_def)  lp15@66827  1938  finally show ?case by simp  lp15@66827  1939  qed  lp15@66827  1940  qed  lp15@66827  1941  qed  lp15@66827  1942  thus ?thesis ..  lp15@66827  1943 qed  lp15@66827  1944 lp15@66827  1945 lemma uniformly_continuous_on_extension_on_closure:  lp15@66827  1946  fixes f::"'a::metric_space \ 'b::complete_space"  lp15@66827  1947  assumes uc: "uniformly_continuous_on X f"  lp15@66827  1948  obtains g where "uniformly_continuous_on (closure X) g" "\x. x \ X \ f x = g x"  lp15@66827  1949  "\Y h x. X \ Y \ Y \ closure X \ continuous_on Y h \ (\x. x \ X \ f x = h x) \ x \ Y \ h x = g x"  lp15@66827  1950 proof -  lp15@66827  1951  from uc have cont_f: "continuous_on X f"  lp15@66827  1952  by (simp add: uniformly_continuous_imp_continuous)  lp15@66827  1953  obtain y where y: "(f \ y x) (at x within X)" if "x \ closure X" for x  lp15@66827  1954  apply atomize_elim  lp15@66827  1955  apply (rule choice)  lp15@66827  1956  using uniformly_continuous_on_extension_at_closure[OF assms]  lp15@66827  1957  by metis  lp15@66827  1958  let ?g = "\x. if x \ X then f x else y x"  lp15@66827  1959 lp15@66827  1960  have "uniformly_continuous_on (closure X) ?g"  lp15@66827  1961  unfolding uniformly_continuous_on_def  lp15@66827  1962  proof safe  lp15@66827  1963  fix e::real assume "e > 0"  lp15@66827  1964  define e' where "e' \ e / 3"  lp15@66827  1965  have "e' > 0" using \e > 0\ by (simp add: e'_def)  lp15@66827  1966  from uc[unfolded uniformly_continuous_on_def, rule_format, OF \0 < e'\]  lp15@66827  1967  obtain d where "d > 0" and d: "\x x'. x \ X \ x' \ X \ dist x' x < d \ dist (f x') (f x) < e'"  lp15@66827  1968  by auto  lp15@66827  1969  define d' where "d' = d / 3"  lp15@66827  1970  have "d' > 0" using \d > 0\ by (simp add: d'_def)  lp15@66827  1971  show "\d>0. \x\closure X. \x'\closure X. dist x' x < d \ dist (?g x') (?g x) < e"  lp15@66827  1972  proof (safe intro!: exI[where x=d'] \d' > 0\)  lp15@66827  1973  fix x x' assume x: "x \ closure X" and x': "x' \ closure X" and dist: "dist x' x < d'"  lp15@66827  1974  then obtain xs xs' where xs: "xs \ x" "\n. xs n \ X"  lp15@66827  1975  and xs': "xs' \ x'" "\n. xs' n \ X"  lp15@66827  1976  by (auto simp: closure_sequential)  lp15@66827  1977  have "\\<^sub>F n in sequentially. dist (xs' n) x' < d'"  lp15@66827  1978  and "\\<^sub>F n in sequentially. dist (xs n) x < d'"  lp15@66827  1979  by (auto intro!: \0 < d'\ order_tendstoD tendsto_eq_intros xs xs')  lp15@66827  1980  moreover  lp15@66827  1981  have "(\x. f (xs x)) \ y x" if "x \ closure X" "x \ X" "xs \ x" "\n. xs n \ X" for xs x  lp15@66827  1982  using that not_eventuallyD  lp15@66827  1983  by (force intro!: filterlim_compose[OF y[OF \x \ closure X\]] simp: filterlim_at)  lp15@66827  1984  then have "(\x. f (xs' x)) \ ?g x'" "(\x. f (xs x)) \ ?g x"  lp15@66827  1985  using x x'  lp15@66827  1986  by (auto intro!: continuous_on_tendsto_compose[OF cont_f] simp: xs' xs)  lp15@66827  1987  then have "\\<^sub>F n in sequentially. dist (f (xs' n)) (?g x') < e'"  lp15@66827  1988  "\\<^sub>F n in sequentially. dist (f (xs n)) (?g x) < e'"  lp15@66827  1989  by (auto intro!: \0 < e'\ order_tendstoD tendsto_eq_intros)  lp15@66827  1990  ultimately  lp15@66827  1991  have "\\<^sub>F n in sequentially. dist (?g x') (?g x) < e"  lp15@66827  1992  proof eventually_elim  lp15@66827  1993  case (elim n)  lp15@66827  1994  have "dist (?g x') (?g x) \  lp15@66827  1995  dist (f (xs' n)) (?g x') + dist (f (xs' n)) (f (xs n)) + dist (f (xs n)) (?g x)"  lp15@66827  1996  by (metis add.commute add_le_cancel_left dist_commute dist_triangle dist_triangle_le)  lp15@66827  1997  also  lp15@66827  1998  {  lp15@66827  1999  have "dist (xs' n) (xs n) \ dist (xs' n) x' + dist x' x + dist (xs n) x"  lp15@66827  2000  by (metis add.commute add_le_cancel_left dist_triangle dist_triangle_le)  lp15@66827  2001  also note \dist (xs' n) x' < d'\  lp15@66827  2002  also note \dist x' x < d'\  lp15@66827  2003  also note \dist (xs n) x < d'\  lp15@66827  2004  finally have "dist (xs' n) (xs n) < d" by (simp add: d'_def)  lp15@66827  2005  }  lp15@66827  2006  with \xs _ \ X\ \xs' _ \ X\ have "dist (f (xs' n)) (f (xs n)) < e'"  lp15@66827  2007  by (rule d)  lp15@66827  2008  also note \dist (f (xs' n)) (?g x') < e'\  lp15@66827  2009  also note \dist (f (xs n)) (?g x) < e'\  lp15@66827  2010  finally show ?case by (simp add: e'_def)  lp15@66827  2011  qed  lp15@66827  2012  then show "dist (?g x') (?g x) < e" by simp  lp15@66827  2013  qed  lp15@66827  2014  qed  lp15@66827  2015  moreover have "f x = ?g x" if "x \ X" for x using that by simp  lp15@66827  2016  moreover  lp15@66827  2017  {  lp15@66827  2018  fix Y h x  lp15@66827  2019  assume Y: "x \ Y" "X \ Y" "Y \ closure X" and cont_h: "continuous_on Y h"  lp15@66827  2020  and extension: "(\x. x \ X \ f x = h x)"  lp15@66827  2021  {  lp15@66827  2022  assume "x \ X"  lp15@66827  2023  have "x \ closure X" using Y by auto  lp15@66827  2024  then obtain xs where xs: "xs \ x" "\n. xs n \ X"  lp15@66827  2025  by (auto simp: closure_sequential)  lp15@66827  2026  from continuous_on_tendsto_compose[OF cont_h xs(1)] xs(2) Y  lp15@66827  2027  have hx: "(\x. f (xs x)) \ h x"  lp15@66827  2028  by (auto simp: set_mp extension)  lp15@66827  2029  then have "(\x. f (xs x)) \ y x"  lp15@66827  2030  using \x \ X\ not_eventuallyD xs(2)  lp15@66827  2031  by (force intro!: filterlim_compose[OF y[OF \x \ closure X\]] simp: filterlim_at xs)  lp15@66827  2032  with hx have "h x = y x" by (rule LIMSEQ_unique)  lp15@66827  2033  } then  lp15@66827  2034  have "h x = ?g x"  lp15@66827  2035  using extension by auto  lp15@66827  2036  }  lp15@66827  2037  ultimately show ?thesis ..  lp15@66827  2038 qed  lp15@66827  2039 lp15@66827  2040 lemma bounded_uniformly_continuous_image:  lp15@66827  2041  fixes f :: "'a :: heine_borel \ 'b :: heine_borel"  lp15@66827  2042  assumes "uniformly_continuous_on S f" "bounded S"  lp15@66884  2043  shows "bounded(f  S)"  lp15@66827  2044  by (metis (no_types, lifting) assms bounded_closure_image compact_closure compact_continuous_image compact_eq_bounded_closed image_cong uniformly_continuous_imp_continuous uniformly_continuous_on_extension_on_closure)  lp15@66827  2045 nipkow@67968  2046 subsection%unimportant \Making a continuous function avoid some value in a neighbourhood\  lp15@66827  2047 lp15@66827  2048 lemma continuous_within_avoid:  lp15@66827  2049  fixes f :: "'a::metric_space \ 'b::t1_space"  lp15@66827  2050  assumes "continuous (at x within s) f"  lp15@66827  2051  and "f x \ a"  lp15@66827  2052  shows "\e>0. \y \ s. dist x y < e --> f y \ a"  lp15@66827  2053 proof -  lp15@66827  2054  obtain U where "open U" and "f x \ U" and "a \ U"  lp15@66827  2055  using t1_space [OF \f x \ a\] by fast  lp15@66827  2056  have "(f \ f x) (at x within s)"  lp15@66827  2057  using assms(1) by (simp add: continuous_within)  lp15@66827  2058  then have "eventually (\y. f y \ U) (at x within s)"  lp15@66827  2059  using \open U\ and \f x \ U\  lp15@66827  2060  unfolding tendsto_def by fast  lp15@66827  2061  then have "eventually (\y. f y \ a) (at x within s)"  lp15@66827  2062  using \a \ U\ by (fast elim: eventually_mono)  lp15@66827  2063  then show ?thesis  haftmann@66953  2064  using \f x \ a\ by (auto simp: dist_commute eventually_at)  lp15@66827  2065 qed  lp15@66827  2066 lp15@66827  2067 lemma continuous_at_avoid:  lp15@66827  2068  fixes f :: "'a::metric_space \ 'b::t1_space"  lp15@66827  2069  assumes "continuous (at x) f"  lp15@66827  2070  and "f x \ a"  lp15@66827  2071  shows "\e>0. \y. dist x y < e \ f y \ a"  lp15@66827  2072  using assms continuous_within_avoid[of x UNIV f a] by simp  lp15@66827  2073 lp15@66827  2074 lemma continuous_on_avoid:  lp15@66827  2075  fixes f :: "'a::metric_space \ 'b::t1_space"  lp15@66827  2076  assumes "continuous_on s f"  lp15@66827  2077  and "x \ s"  lp15@66827  2078  and "f x \ a"  lp15@66827  2079  shows "\e>0. \y \ s. dist x y < e \ f y \ a"  lp15@66827  2080  using assms(1)[unfolded continuous_on_eq_continuous_within, THEN bspec[where x=x],  lp15@66827  2081  OF assms(2)] continuous_within_avoid[of x s f a]  lp15@66827  2082  using assms(3)  lp15@66827  2083  by auto  lp15@66827  2084 lp15@66827  2085 lemma continuous_on_open_avoid:  lp15@66827  2086  fixes f :: "'a::metric_space \ 'b::t1_space"  lp15@66827  2087  assumes "continuous_on s f"  lp15@66827  2088  and "open s"  lp15@66827  2089  and "x \ s"  lp15@66827  2090  and "f x \ a"  lp15@66827  2091  shows "\e>0. \y. dist x y < e \ f y \ a"  lp15@66827  2092  using assms(1)[unfolded continuous_on_eq_continuous_at[OF assms(2)], THEN bspec[where x=x], OF assms(3)]  lp15@66827  2093  using continuous_at_avoid[of x f a] assms(4)  lp15@66827  2094  by auto  lp15@66827  2095 immler@67962  2096 subsection%unimportant\Quotient maps\  lp15@66827  2097 lp15@66827  2098 lemma quotient_map_imp_continuous_open:  lp15@66884  2099  assumes T: "f  S \ T"  lp15@66884  2100  and ope: "\U. U \ T  lp15@66884  2101  \ (openin (subtopology euclidean S) (S \ f - U) \  lp15@66884  2102  openin (subtopology euclidean T) U)"  lp15@66884  2103  shows "continuous_on S f"  lp15@66827  2104 proof -  lp15@66884  2105  have [simp]: "S \ f - f  S = S" by auto  lp15@66827  2106  show ?thesis  lp15@66884  2107  using ope [OF T]  lp15@66827  2108  apply (simp add: continuous_on_open)  lp15@66884  2109  by (meson ope openin_imp_subset openin_trans)  lp15@66827  2110 qed  lp15@66827  2111 lp15@66827  2112 lemma quotient_map_imp_continuous_closed:  lp15@66884  2113  assumes T: "f  S \ T"  lp15@66884  2114  and ope: "\U. U \ T  lp15@66884  2115  \ (closedin (subtopology euclidean S) (S \ f - U) \  lp15@66884  2116  closedin (subtopology euclidean T) U)"  lp15@66884  2117  shows "continuous_on S f"  lp15@66827  2118 proof -  lp15@66884  2119  have [simp]: "S \ f - f  S = S" by auto  lp15@66827  2120  show ?thesis  lp15@66884  2121  using ope [OF T]  lp15@66827  2122  apply (simp add: continuous_on_closed)  lp15@66884  2123  by (metis (no_types, lifting) ope closedin_imp_subset closedin_trans)  lp15@66827  2124 qed  lp15@66827  2125 lp15@66827  2126 lemma open_map_imp_quotient_map:  lp15@66884  2127  assumes contf: "continuous_on S f"  lp15@66884  2128  and T: "T \<`