src/HOL/Library/Topology_Euclidean_Space.thy
 author huffman Thu Jun 11 09:03:24 2009 -0700 (2009-06-11) changeset 31563 ded2364d14d4 parent 31560 88347c12e267 child 31565 da5a5589418e permissions -rw-r--r--
cleaned up some proofs
 chaieb@30262 ` 1` ```(* Title: Topology ``` chaieb@30262 ` 2` ``` Author: Amine Chaieb, University of Cambridge ``` wenzelm@30267 ` 3` ``` Author: Robert Himmelmann, TU Muenchen ``` wenzelm@30267 ` 4` ```*) ``` chaieb@30262 ` 5` chaieb@30262 ` 6` ```header {* Elementary topology in Euclidean space. *} ``` chaieb@30262 ` 7` chaieb@30262 ` 8` ```theory Topology_Euclidean_Space ``` huffman@31560 ` 9` ```imports SEQ Euclidean_Space Product_Vector ``` chaieb@30262 ` 10` ```begin ``` chaieb@30262 ` 11` chaieb@30262 ` 12` ```declare fstcart_pastecart[simp] sndcart_pastecart[simp] ``` chaieb@30262 ` 13` chaieb@30262 ` 14` ```subsection{* General notion of a topology *} ``` chaieb@30262 ` 15` chaieb@30262 ` 16` ```definition "istopology L \ {} \ L \ (\S \L. \T \L. S \ T \ L) \ (\K. K \L \ \ K \ L)" ``` huffman@30488 ` 17` ```typedef (open) 'a topology = "{L::('a set) set. istopology L}" ``` chaieb@30262 ` 18` ``` morphisms "openin" "topology" ``` chaieb@30262 ` 19` ``` unfolding istopology_def by blast ``` chaieb@30262 ` 20` chaieb@30262 ` 21` ```lemma istopology_open_in[intro]: "istopology(openin U)" ``` chaieb@30262 ` 22` ``` using openin[of U] by blast ``` chaieb@30262 ` 23` chaieb@30262 ` 24` ```lemma topology_inverse': "istopology U \ openin (topology U) = U" ``` chaieb@30262 ` 25` ``` using topology_inverse[unfolded mem_def Collect_def] . ``` chaieb@30262 ` 26` chaieb@30262 ` 27` ```lemma topology_inverse_iff: "istopology U \ openin (topology U) = U" ``` chaieb@30262 ` 28` ``` using topology_inverse[of U] istopology_open_in[of "topology U"] by auto ``` chaieb@30262 ` 29` chaieb@30262 ` 30` ```lemma topology_eq: "T1 = T2 \ (\S. openin T1 S \ openin T2 S)" ``` chaieb@30262 ` 31` ```proof- ``` chaieb@30262 ` 32` ``` {assume "T1=T2" hence "\S. openin T1 S \ openin T2 S" by simp} ``` chaieb@30262 ` 33` ``` moreover ``` chaieb@30262 ` 34` ``` {assume H: "\S. openin T1 S \ openin T2 S" ``` chaieb@30262 ` 35` ``` hence "openin T1 = openin T2" by (metis mem_def set_ext) ``` chaieb@30262 ` 36` ``` hence "topology (openin T1) = topology (openin T2)" by simp ``` chaieb@30262 ` 37` ``` hence "T1 = T2" unfolding openin_inverse .} ``` chaieb@30262 ` 38` ``` ultimately show ?thesis by blast ``` chaieb@30262 ` 39` ```qed ``` chaieb@30262 ` 40` chaieb@30262 ` 41` ```text{* Infer the "universe" from union of all sets in the topology. *} ``` chaieb@30262 ` 42` chaieb@30262 ` 43` ```definition "topspace T = \{S. openin T S}" ``` chaieb@30262 ` 44` chaieb@30262 ` 45` ```subsection{* Main properties of open sets *} ``` chaieb@30262 ` 46` chaieb@30262 ` 47` ```lemma openin_clauses: ``` chaieb@30262 ` 48` ``` fixes U :: "'a topology" ``` chaieb@30262 ` 49` ``` shows "openin U {}" ``` chaieb@30262 ` 50` ``` "\S T. openin U S \ openin U T \ openin U (S\T)" ``` chaieb@30262 ` 51` ``` "\K. (\S \ K. openin U S) \ openin U (\K)" ``` chaieb@30262 ` 52` ``` using openin[of U] unfolding istopology_def Collect_def mem_def ``` chaieb@30262 ` 53` ``` by (metis mem_def subset_eq)+ ``` chaieb@30262 ` 54` chaieb@30262 ` 55` ```lemma openin_subset[intro]: "openin U S \ S \ topspace U" ``` chaieb@30262 ` 56` ``` unfolding topspace_def by blast ``` chaieb@30262 ` 57` ```lemma openin_empty[simp]: "openin U {}" by (simp add: openin_clauses) ``` chaieb@30262 ` 58` chaieb@30262 ` 59` ```lemma openin_Int[intro]: "openin U S \ openin U T \ openin U (S \ T)" ``` chaieb@30262 ` 60` ``` by (simp add: openin_clauses) ``` chaieb@30262 ` 61` chaieb@30262 ` 62` ```lemma openin_Union[intro]: "(\S \K. openin U S) \ openin U (\ K)" by (simp add: openin_clauses) ``` chaieb@30262 ` 63` chaieb@30262 ` 64` ```lemma openin_Un[intro]: "openin U S \ openin U T \ openin U (S \ T)" ``` chaieb@30262 ` 65` ``` using openin_Union[of "{S,T}" U] by auto ``` chaieb@30262 ` 66` chaieb@30262 ` 67` ```lemma openin_topspace[intro, simp]: "openin U (topspace U)" by (simp add: openin_Union topspace_def) ``` chaieb@30262 ` 68` chaieb@30262 ` 69` ```lemma openin_subopen: "openin U S \ (\x \ S. \T. openin U T \ x \ T \ T \ S)" (is "?lhs \ ?rhs") ``` chaieb@30262 ` 70` ```proof- ``` chaieb@30262 ` 71` ``` {assume ?lhs then have ?rhs by auto } ``` chaieb@30262 ` 72` ``` moreover ``` chaieb@30262 ` 73` ``` {assume H: ?rhs ``` huffman@30488 ` 74` ``` then obtain t where t: "\x\S. openin U (t x) \ x \ t x \ t x \ S" ``` chaieb@30262 ` 75` ``` unfolding Ball_def ex_simps(6)[symmetric] choice_iff by blast ``` chaieb@30262 ` 76` ``` from t have th0: "\x\ t`S. openin U x" by auto ``` huffman@30488 ` 77` ``` have "\ t`S = S" using t by auto ``` chaieb@30262 ` 78` ``` with openin_Union[OF th0] have "openin U S" by simp } ``` chaieb@30262 ` 79` ``` ultimately show ?thesis by blast ``` chaieb@30262 ` 80` ```qed ``` chaieb@30262 ` 81` chaieb@30262 ` 82` ```subsection{* Closed sets *} ``` chaieb@30262 ` 83` chaieb@30262 ` 84` ```definition "closedin U S \ S \ topspace U \ openin U (topspace U - S)" ``` chaieb@30262 ` 85` chaieb@30262 ` 86` ```lemma closedin_subset: "closedin U S \ S \ topspace U" by (metis closedin_def) ``` chaieb@30262 ` 87` ```lemma closedin_empty[simp]: "closedin U {}" by (simp add: closedin_def) ``` huffman@30488 ` 88` ```lemma closedin_topspace[intro,simp]: ``` chaieb@30262 ` 89` ``` "closedin U (topspace U)" by (simp add: closedin_def) ``` chaieb@30262 ` 90` ```lemma closedin_Un[intro]: "closedin U S \ closedin U T \ closedin U (S \ T)" ``` chaieb@30262 ` 91` ``` by (auto simp add: Diff_Un closedin_def) ``` chaieb@30262 ` 92` chaieb@30262 ` 93` ```lemma Diff_Inter[intro]: "A - \S = \ {A - s|s. s\S}" by auto ``` chaieb@30262 ` 94` ```lemma closedin_Inter[intro]: assumes Ke: "K \ {}" and Kc: "\S \K. closedin U S" ``` chaieb@30262 ` 95` ``` shows "closedin U (\ K)" using Ke Kc unfolding closedin_def Diff_Inter by auto ``` chaieb@30262 ` 96` chaieb@30262 ` 97` ```lemma closedin_Int[intro]: "closedin U S \ closedin U T \ closedin U (S \ T)" ``` chaieb@30262 ` 98` ``` using closedin_Inter[of "{S,T}" U] by auto ``` chaieb@30262 ` 99` chaieb@30262 ` 100` ```lemma Diff_Diff_Int: "A - (A - B) = A \ B" by blast ``` chaieb@30262 ` 101` ```lemma openin_closedin_eq: "openin U S \ S \ topspace U \ closedin U (topspace U - S)" ``` chaieb@30262 ` 102` ``` apply (auto simp add: closedin_def) ``` chaieb@30262 ` 103` ``` apply (metis openin_subset subset_eq) ``` chaieb@30262 ` 104` ``` apply (auto simp add: Diff_Diff_Int) ``` chaieb@30262 ` 105` ``` apply (subgoal_tac "topspace U \ S = S") ``` chaieb@30262 ` 106` ``` by auto ``` chaieb@30262 ` 107` chaieb@30262 ` 108` ```lemma openin_closedin: "S \ topspace U \ (openin U S \ closedin U (topspace U - S))" ``` chaieb@30262 ` 109` ``` by (simp add: openin_closedin_eq) ``` chaieb@30262 ` 110` chaieb@30262 ` 111` ```lemma openin_diff[intro]: assumes oS: "openin U S" and cT: "closedin U T" shows "openin U (S - T)" ``` chaieb@30262 ` 112` ```proof- ``` chaieb@30262 ` 113` ``` have "S - T = S \ (topspace U - T)" using openin_subset[of U S] oS cT ``` chaieb@30262 ` 114` ``` by (auto simp add: topspace_def openin_subset) ``` chaieb@30262 ` 115` ``` then show ?thesis using oS cT by (auto simp add: closedin_def) ``` huffman@30488 ` 116` ```qed ``` chaieb@30262 ` 117` chaieb@30262 ` 118` ```lemma closedin_diff[intro]: assumes oS: "closedin U S" and cT: "openin U T" shows "closedin U (S - T)" ``` chaieb@30262 ` 119` ```proof- ``` huffman@30488 ` 120` ``` have "S - T = S \ (topspace U - T)" using closedin_subset[of U S] oS cT ``` chaieb@30262 ` 121` ``` by (auto simp add: topspace_def ) ``` chaieb@30262 ` 122` ``` then show ?thesis using oS cT by (auto simp add: openin_closedin_eq) ``` chaieb@30262 ` 123` ```qed ``` chaieb@30262 ` 124` chaieb@30262 ` 125` ```subsection{* Subspace topology. *} ``` chaieb@30262 ` 126` chaieb@30262 ` 127` ```definition "subtopology U V = topology {S \ V |S. openin U S}" ``` chaieb@30262 ` 128` chaieb@30262 ` 129` ```lemma istopology_subtopology: "istopology {S \ V |S. openin U S}" (is "istopology ?L") ``` chaieb@30262 ` 130` ```proof- ``` chaieb@30262 ` 131` ``` have "{} \ ?L" by blast ``` chaieb@30262 ` 132` ``` {fix A B assume A: "A \ ?L" and B: "B \ ?L" ``` chaieb@30262 ` 133` ``` from A B obtain Sa and Sb where Sa: "openin U Sa" "A = Sa \ V" and Sb: "openin U Sb" "B = Sb \ V" by blast ``` chaieb@30262 ` 134` ``` have "A\B = (Sa \ Sb) \ V" "openin U (Sa \ Sb)" using Sa Sb by blast+ ``` chaieb@30262 ` 135` ``` then have "A \ B \ ?L" by blast} ``` chaieb@30262 ` 136` ``` moreover ``` chaieb@30262 ` 137` ``` {fix K assume K: "K \ ?L" ``` huffman@30488 ` 138` ``` have th0: "?L = (\S. S \ V) ` openin U " ``` huffman@30488 ` 139` ``` apply (rule set_ext) ``` huffman@30488 ` 140` ``` apply (simp add: Ball_def image_iff) ``` chaieb@30262 ` 141` ``` by (metis mem_def) ``` chaieb@30262 ` 142` ``` from K[unfolded th0 subset_image_iff] ``` chaieb@30262 ` 143` ``` obtain Sk where Sk: "Sk \ openin U" "K = (\S. S \ V) ` Sk" by blast ``` chaieb@30262 ` 144` ``` have "\K = (\Sk) \ V" using Sk by auto ``` chaieb@30262 ` 145` ``` moreover have "openin U (\ Sk)" using Sk by (auto simp add: subset_eq mem_def) ``` chaieb@30262 ` 146` ``` ultimately have "\K \ ?L" by blast} ``` huffman@30488 ` 147` ``` ultimately show ?thesis unfolding istopology_def by blast ``` huffman@30488 ` 148` ```qed ``` huffman@30488 ` 149` huffman@30488 ` 150` ```lemma openin_subtopology: ``` chaieb@30262 ` 151` ``` "openin (subtopology U V) S \ (\ T. (openin U T) \ (S = T \ V))" ``` huffman@30488 ` 152` ``` unfolding subtopology_def topology_inverse'[OF istopology_subtopology] ``` huffman@30488 ` 153` ``` by (auto simp add: Collect_def) ``` chaieb@30262 ` 154` chaieb@30262 ` 155` ```lemma topspace_subtopology: "topspace(subtopology U V) = topspace U \ V" ``` chaieb@30262 ` 156` ``` by (auto simp add: topspace_def openin_subtopology) ``` chaieb@30262 ` 157` huffman@30488 ` 158` ```lemma closedin_subtopology: ``` chaieb@30262 ` 159` ``` "closedin (subtopology U V) S \ (\T. closedin U T \ S = T \ V)" ``` chaieb@30262 ` 160` ``` unfolding closedin_def topspace_subtopology ``` chaieb@30262 ` 161` ``` apply (simp add: openin_subtopology) ``` chaieb@30262 ` 162` ``` apply (rule iffI) ``` chaieb@30262 ` 163` ``` apply clarify ``` chaieb@30262 ` 164` ``` apply (rule_tac x="topspace U - T" in exI) ``` chaieb@30262 ` 165` ``` by auto ``` chaieb@30262 ` 166` chaieb@30262 ` 167` ```lemma openin_subtopology_refl: "openin (subtopology U V) V \ V \ topspace U" ``` chaieb@30262 ` 168` ``` unfolding openin_subtopology ``` chaieb@30262 ` 169` ``` apply (rule iffI, clarify) ``` chaieb@30262 ` 170` ``` apply (frule openin_subset[of U]) apply blast ``` chaieb@30262 ` 171` ``` apply (rule exI[where x="topspace U"]) ``` chaieb@30262 ` 172` ``` by auto ``` chaieb@30262 ` 173` huffman@30488 ` 174` ```lemma subtopology_superset: assumes UV: "topspace U \ V" ``` chaieb@30262 ` 175` ``` shows "subtopology U V = U" ``` chaieb@30262 ` 176` ```proof- ``` chaieb@30262 ` 177` ``` {fix S ``` chaieb@30262 ` 178` ``` {fix T assume T: "openin U T" "S = T \ V" ``` chaieb@30262 ` 179` ``` from T openin_subset[OF T(1)] UV have eq: "S = T" by blast ``` chaieb@30262 ` 180` ``` have "openin U S" unfolding eq using T by blast} ``` chaieb@30262 ` 181` ``` moreover ``` chaieb@30262 ` 182` ``` {assume S: "openin U S" ``` chaieb@30262 ` 183` ``` hence "\T. openin U T \ S = T \ V" ``` chaieb@30262 ` 184` ``` using openin_subset[OF S] UV by auto} ``` chaieb@30262 ` 185` ``` ultimately have "(\T. openin U T \ S = T \ V) \ openin U S" by blast} ``` chaieb@30262 ` 186` ``` then show ?thesis unfolding topology_eq openin_subtopology by blast ``` chaieb@30262 ` 187` ```qed ``` chaieb@30262 ` 188` chaieb@30262 ` 189` chaieb@30262 ` 190` ```lemma subtopology_topspace[simp]: "subtopology U (topspace U) = U" ``` chaieb@30262 ` 191` ``` by (simp add: subtopology_superset) ``` chaieb@30262 ` 192` chaieb@30262 ` 193` ```lemma subtopology_UNIV[simp]: "subtopology U UNIV = U" ``` chaieb@30262 ` 194` ``` by (simp add: subtopology_superset) ``` chaieb@30262 ` 195` chaieb@30262 ` 196` ```subsection{* The universal Euclidean versions are what we use most of the time *} ``` huffman@31418 ` 197` huffman@31285 ` 198` ```definition ``` huffman@31418 ` 199` ``` euclidean :: "'a::topological_space topology" where ``` huffman@31418 ` 200` ``` "euclidean = topology open" ``` huffman@31418 ` 201` chaieb@30262 ` 202` ```lemma open_openin: "open S \ openin euclidean S" ``` chaieb@30262 ` 203` ``` unfolding euclidean_def ``` chaieb@30262 ` 204` ``` apply (rule cong[where x=S and y=S]) ``` chaieb@30262 ` 205` ``` apply (rule topology_inverse[symmetric]) ``` chaieb@30262 ` 206` ``` apply (auto simp add: istopology_def) ``` chaieb@30262 ` 207` ``` by (auto simp add: mem_def subset_eq) ``` chaieb@30262 ` 208` chaieb@30262 ` 209` ```lemma topspace_euclidean: "topspace euclidean = UNIV" ``` chaieb@30262 ` 210` ``` apply (simp add: topspace_def) ``` chaieb@30262 ` 211` ``` apply (rule set_ext) ``` chaieb@30262 ` 212` ``` by (auto simp add: open_openin[symmetric]) ``` chaieb@30262 ` 213` chaieb@30262 ` 214` ```lemma topspace_euclidean_subtopology[simp]: "topspace (subtopology euclidean S) = S" ``` chaieb@30262 ` 215` ``` by (simp add: topspace_euclidean topspace_subtopology) ``` chaieb@30262 ` 216` chaieb@30262 ` 217` ```lemma closed_closedin: "closed S \ closedin euclidean S" ``` huffman@31490 ` 218` ``` by (simp add: closed_def closedin_def topspace_euclidean open_openin Compl_eq_Diff_UNIV) ``` chaieb@30262 ` 219` chaieb@30262 ` 220` ```lemma open_subopen: "open S \ (\x\S. \T. open T \ x \ T \ T \ S)" ``` chaieb@30262 ` 221` ``` by (simp add: open_openin openin_subopen[symmetric]) ``` chaieb@30262 ` 222` chaieb@30262 ` 223` ```subsection{* Open and closed balls. *} ``` chaieb@30262 ` 224` huffman@31285 ` 225` ```definition ``` huffman@31345 ` 226` ``` ball :: "'a::metric_space \ real \ 'a set" where ``` huffman@31285 ` 227` ``` "ball x e = {y. dist x y < e}" ``` huffman@31285 ` 228` huffman@31285 ` 229` ```definition ``` huffman@31345 ` 230` ``` cball :: "'a::metric_space \ real \ 'a set" where ``` huffman@31285 ` 231` ``` "cball x e = {y. dist x y \ e}" ``` chaieb@30262 ` 232` huffman@30488 ` 233` ```lemma mem_ball[simp]: "y \ ball x e \ dist x y < e" by (simp add: ball_def) ``` huffman@30488 ` 234` ```lemma mem_cball[simp]: "y \ cball x e \ dist x y \ e" by (simp add: cball_def) ``` huffman@31345 ` 235` huffman@31345 ` 236` ```lemma mem_ball_0 [simp]: ``` huffman@31345 ` 237` ``` fixes x :: "'a::real_normed_vector" ``` huffman@31345 ` 238` ``` shows "x \ ball 0 e \ norm x < e" ``` huffman@31345 ` 239` ``` by (simp add: dist_norm) ``` huffman@31345 ` 240` huffman@31345 ` 241` ```lemma mem_cball_0 [simp]: ``` huffman@31345 ` 242` ``` fixes x :: "'a::real_normed_vector" ``` huffman@31345 ` 243` ``` shows "x \ cball 0 e \ norm x \ e" ``` huffman@31345 ` 244` ``` by (simp add: dist_norm) ``` huffman@31345 ` 245` chaieb@30262 ` 246` ```lemma centre_in_cball[simp]: "x \ cball x e \ 0\ e" by simp ``` chaieb@30262 ` 247` ```lemma ball_subset_cball[simp,intro]: "ball x e \ cball x e" by (simp add: subset_eq) ``` chaieb@30262 ` 248` ```lemma subset_ball[intro]: "d <= e ==> ball x d \ ball x e" by (simp add: subset_eq) ``` chaieb@30262 ` 249` ```lemma subset_cball[intro]: "d <= e ==> cball x d \ cball x e" by (simp add: subset_eq) ``` chaieb@30262 ` 250` ```lemma ball_max_Un: "ball a (max r s) = ball a r \ ball a s" ``` chaieb@30262 ` 251` ``` by (simp add: expand_set_eq) arith ``` chaieb@30262 ` 252` chaieb@30262 ` 253` ```lemma ball_min_Int: "ball a (min r s) = ball a r \ ball a s" ``` huffman@30488 ` 254` ``` by (simp add: expand_set_eq) ``` chaieb@30262 ` 255` chaieb@30262 ` 256` ```subsection{* Topological properties of open balls *} ``` chaieb@30262 ` 257` huffman@30488 ` 258` ```lemma diff_less_iff: "(a::real) - b > 0 \ a > b" ``` huffman@30488 ` 259` ``` "(a::real) - b < 0 \ a < b" ``` chaieb@30262 ` 260` ``` "a - b < c \ a < c +b" "a - b > c \ a > c +b" by arith+ ``` huffman@30488 ` 261` ```lemma diff_le_iff: "(a::real) - b \ 0 \ a \ b" "(a::real) - b \ 0 \ a \ b" ``` chaieb@30262 ` 262` ``` "a - b \ c \ a \ c +b" "a - b \ c \ a \ c +b" by arith+ ``` chaieb@30262 ` 263` chaieb@30262 ` 264` ```lemma open_ball[intro, simp]: "open (ball x e)" ``` huffman@31418 ` 265` ``` unfolding open_dist ball_def Collect_def Ball_def mem_def ``` huffman@31285 ` 266` ``` unfolding dist_commute ``` chaieb@30262 ` 267` ``` apply clarify ``` chaieb@30262 ` 268` ``` apply (rule_tac x="e - dist xa x" in exI) ``` chaieb@30262 ` 269` ``` using dist_triangle_alt[where z=x] ``` chaieb@30262 ` 270` ``` apply (clarsimp simp add: diff_less_iff) ``` chaieb@30262 ` 271` ``` apply atomize ``` huffman@31492 ` 272` ``` apply (erule_tac x="y" in allE) ``` chaieb@30262 ` 273` ``` apply (erule_tac x="xa" in allE) ``` chaieb@30262 ` 274` ``` by arith ``` chaieb@30262 ` 275` huffman@31285 ` 276` ```lemma centre_in_ball[simp]: "x \ ball x e \ e > 0" by (metis mem_ball dist_self) ``` chaieb@30262 ` 277` ```lemma open_contains_ball: "open S \ (\x\S. \e>0. ball x e \ S)" ``` huffman@31418 ` 278` ``` unfolding open_dist subset_eq mem_ball Ball_def dist_commute .. ``` chaieb@30262 ` 279` chaieb@30262 ` 280` ```lemma open_contains_ball_eq: "open S \ \x. x\S \ (\e>0. ball x e \ S)" ``` chaieb@30262 ` 281` ``` by (metis open_contains_ball subset_eq centre_in_ball) ``` chaieb@30262 ` 282` chaieb@30262 ` 283` ```lemma ball_eq_empty[simp]: "ball x e = {} \ e \ 0" ``` chaieb@30262 ` 284` ``` unfolding mem_ball expand_set_eq ``` chaieb@30262 ` 285` ``` apply (simp add: not_less) ``` huffman@31285 ` 286` ``` by (metis zero_le_dist order_trans dist_self) ``` chaieb@30262 ` 287` chaieb@30262 ` 288` ```lemma ball_empty[intro]: "e \ 0 ==> ball x e = {}" by simp ``` chaieb@30262 ` 289` chaieb@30262 ` 290` ```subsection{* Basic "localization" results are handy for connectedness. *} ``` chaieb@30262 ` 291` chaieb@30262 ` 292` ```lemma openin_open: "openin (subtopology euclidean U) S \ (\T. open T \ (S = U \ T))" ``` chaieb@30262 ` 293` ``` by (auto simp add: openin_subtopology open_openin[symmetric]) ``` chaieb@30262 ` 294` chaieb@30262 ` 295` ```lemma openin_open_Int[intro]: "open S \ openin (subtopology euclidean U) (U \ S)" ``` huffman@30488 ` 296` ``` by (auto simp add: openin_open) ``` huffman@30488 ` 297` huffman@30488 ` 298` ```lemma open_openin_trans[trans]: ``` chaieb@30262 ` 299` ``` "open S \ open T \ T \ S \ openin (subtopology euclidean S) T" ``` chaieb@30262 ` 300` ``` by (metis Int_absorb1 openin_open_Int) ``` chaieb@30262 ` 301` chaieb@30262 ` 302` ```lemma open_subset: "S \ T \ open S \ openin (subtopology euclidean T) S" ``` chaieb@30262 ` 303` ``` by (auto simp add: openin_open) ``` chaieb@30262 ` 304` chaieb@30262 ` 305` ```lemma closedin_closed: "closedin (subtopology euclidean U) S \ (\T. closed T \ S = U \ T)" ``` chaieb@30262 ` 306` ``` by (simp add: closedin_subtopology closed_closedin Int_ac) ``` chaieb@30262 ` 307` chaieb@30262 ` 308` ```lemma closedin_closed_Int: "closed S ==> closedin (subtopology euclidean U) (U \ S)" ``` chaieb@30262 ` 309` ``` by (metis closedin_closed) ``` chaieb@30262 ` 310` chaieb@30262 ` 311` ```lemma closed_closedin_trans: "closed S \ closed T \ T \ S \ closedin (subtopology euclidean S) T" ``` chaieb@30262 ` 312` ``` apply (subgoal_tac "S \ T = T" ) ``` chaieb@30262 ` 313` ``` apply auto ``` chaieb@30262 ` 314` ``` apply (frule closedin_closed_Int[of T S]) ``` chaieb@30262 ` 315` ``` by simp ``` chaieb@30262 ` 316` chaieb@30262 ` 317` ```lemma closed_subset: "S \ T \ closed S \ closedin (subtopology euclidean T) S" ``` chaieb@30262 ` 318` ``` by (auto simp add: closedin_closed) ``` chaieb@30262 ` 319` huffman@31418 ` 320` ```lemma openin_euclidean_subtopology_iff: ``` huffman@31418 ` 321` ``` fixes S U :: "'a::metric_space set" ``` huffman@31418 ` 322` ``` shows "openin (subtopology euclidean U) S ``` chaieb@30262 ` 323` ``` \ S \ U \ (\x\S. \e>0. \x'\U. dist x' x < e \ x'\ S)" (is "?lhs \ ?rhs") ``` chaieb@30262 ` 324` ```proof- ``` chaieb@30262 ` 325` ``` {assume ?lhs hence ?rhs unfolding openin_subtopology open_openin[symmetric] ``` huffman@31418 ` 326` ``` by (simp add: open_dist) blast} ``` chaieb@30262 ` 327` ``` moreover ``` chaieb@30262 ` 328` ``` {assume SU: "S \ U" and H: "\x. x \ S \ \e>0. \x'\U. dist x' x < e \ x' \ S" ``` chaieb@30262 ` 329` ``` from H obtain d where d: "\x . x\ S \ d x > 0 \ (\x' \ U. dist x' x < d x \ x' \ S)" ``` chaieb@30262 ` 330` ``` by metis ``` chaieb@30262 ` 331` ``` let ?T = "\{B. \x\S. B = ball x (d x)}" ``` chaieb@30262 ` 332` ``` have oT: "open ?T" by auto ``` chaieb@30262 ` 333` ``` { fix x assume "x\S" ``` chaieb@30262 ` 334` ``` hence "x \ \{B. \x\S. B = ball x (d x)}" ``` chaieb@30262 ` 335` ``` apply simp apply(rule_tac x="ball x(d x)" in exI) apply auto ``` huffman@31285 ` 336` ``` by (rule d [THEN conjunct1]) ``` chaieb@30262 ` 337` ``` hence "x\ ?T \ U" using SU and `x\S` by auto } ``` chaieb@30262 ` 338` ``` moreover ``` chaieb@30262 ` 339` ``` { fix y assume "y\?T" ``` chaieb@30262 ` 340` ``` then obtain B where "y\B" "B\{B. \x\S. B = ball x (d x)}" by auto ``` chaieb@30262 ` 341` ``` then obtain x where "x\S" and x:"y \ ball x (d x)" by auto ``` chaieb@30262 ` 342` ``` assume "y\U" ``` huffman@31285 ` 343` ``` hence "y\S" using d[OF `x\S`] and x by(auto simp add: dist_commute) } ``` huffman@30488 ` 344` ``` ultimately have "S = ?T \ U" by blast ``` chaieb@30262 ` 345` ``` with oT have ?lhs unfolding openin_subtopology open_openin[symmetric] by blast} ``` chaieb@30262 ` 346` ``` ultimately show ?thesis by blast ``` chaieb@30262 ` 347` ```qed ``` chaieb@30262 ` 348` chaieb@30262 ` 349` ```text{* These "transitivity" results are handy too. *} ``` chaieb@30262 ` 350` huffman@30488 ` 351` ```lemma openin_trans[trans]: "openin (subtopology euclidean T) S \ openin (subtopology euclidean U) T ``` chaieb@30262 ` 352` ``` \ openin (subtopology euclidean U) S" ``` chaieb@30262 ` 353` ``` unfolding open_openin openin_open by blast ``` chaieb@30262 ` 354` chaieb@30262 ` 355` ```lemma openin_open_trans: "openin (subtopology euclidean T) S \ open T \ open S" ``` chaieb@30262 ` 356` ``` by (auto simp add: openin_open intro: openin_trans) ``` chaieb@30262 ` 357` huffman@30488 ` 358` ```lemma closedin_trans[trans]: ``` huffman@30488 ` 359` ``` "closedin (subtopology euclidean T) S \ ``` chaieb@30262 ` 360` ``` closedin (subtopology euclidean U) T ``` chaieb@30262 ` 361` ``` ==> closedin (subtopology euclidean U) S" ``` chaieb@30262 ` 362` ``` by (auto simp add: closedin_closed closed_closedin closed_Inter Int_assoc) ``` chaieb@30262 ` 363` chaieb@30262 ` 364` ```lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \ closed T \ closed S" ``` chaieb@30262 ` 365` ``` by (auto simp add: closedin_closed intro: closedin_trans) ``` chaieb@30262 ` 366` chaieb@30262 ` 367` ```subsection{* Connectedness *} ``` chaieb@30262 ` 368` chaieb@30262 ` 369` ```definition "connected S \ ``` huffman@30488 ` 370` ``` ~(\e1 e2. open e1 \ open e2 \ S \ (e1 \ e2) \ (e1 \ e2 \ S = {}) ``` chaieb@30262 ` 371` ``` \ ~(e1 \ S = {}) \ ~(e2 \ S = {}))" ``` chaieb@30262 ` 372` huffman@30488 ` 373` ```lemma connected_local: ``` chaieb@30262 ` 374` ``` "connected S \ ~(\e1 e2. ``` chaieb@30262 ` 375` ``` openin (subtopology euclidean S) e1 \ ``` chaieb@30262 ` 376` ``` openin (subtopology euclidean S) e2 \ ``` chaieb@30262 ` 377` ``` S \ e1 \ e2 \ ``` chaieb@30262 ` 378` ``` e1 \ e2 = {} \ ``` chaieb@30262 ` 379` ``` ~(e1 = {}) \ ``` chaieb@30262 ` 380` ``` ~(e2 = {}))" ``` huffman@31418 ` 381` ```unfolding connected_def openin_open by (safe, blast+) ``` chaieb@30262 ` 382` chaieb@30262 ` 383` ```lemma exists_diff: "(\S. P(UNIV - S)) \ (\S. P S)" (is "?lhs \ ?rhs") ``` chaieb@30262 ` 384` ```proof- ``` huffman@30488 ` 385` chaieb@30262 ` 386` ``` {assume "?lhs" hence ?rhs by blast } ``` chaieb@30262 ` 387` ``` moreover ``` chaieb@30262 ` 388` ``` {fix S assume H: "P S" ``` chaieb@30262 ` 389` ``` have "S = UNIV - (UNIV - S)" by auto ``` chaieb@30262 ` 390` ``` with H have "P (UNIV - (UNIV - S))" by metis } ``` chaieb@30262 ` 391` ``` ultimately show ?thesis by metis ``` chaieb@30262 ` 392` ```qed ``` chaieb@30262 ` 393` chaieb@30262 ` 394` ```lemma connected_clopen: "connected S \ ``` chaieb@30262 ` 395` ``` (\T. openin (subtopology euclidean S) T \ ``` chaieb@30262 ` 396` ``` closedin (subtopology euclidean S) T \ T = {} \ T = S)" (is "?lhs \ ?rhs") ``` chaieb@30262 ` 397` ```proof- ``` huffman@30488 ` 398` ``` have " \ connected S \ (\e1 e2. open e1 \ open (UNIV - e2) \ S \ e1 \ (UNIV - e2) \ e1 \ (UNIV - e2) \ S = {} \ e1 \ S \ {} \ (UNIV - e2) \ S \ {})" ``` huffman@30488 ` 399` ``` unfolding connected_def openin_open closedin_closed ``` chaieb@30262 ` 400` ``` apply (subst exists_diff) by blast ``` huffman@30488 ` 401` ``` hence th0: "connected S \ \ (\e2 e1. closed e2 \ open e1 \ S \ e1 \ (UNIV - e2) \ e1 \ (UNIV - e2) \ S = {} \ e1 \ S \ {} \ (UNIV - e2) \ S \ {})" ``` huffman@31490 ` 402` ``` (is " _ \ \ (\e2 e1. ?P e2 e1)") apply (simp add: closed_def Compl_eq_Diff_UNIV) by metis ``` chaieb@30262 ` 403` chaieb@30262 ` 404` ``` have th1: "?rhs \ \ (\t' t. closed t'\t = S\t' \ t\{} \ t\S \ (\t'. open t' \ t = S \ t'))" ``` chaieb@30262 ` 405` ``` (is "_ \ \ (\t' t. ?Q t' t)") ``` chaieb@30262 ` 406` ``` unfolding connected_def openin_open closedin_closed by auto ``` chaieb@30262 ` 407` ``` {fix e2 ``` chaieb@30262 ` 408` ``` {fix e1 have "?P e2 e1 \ (\t. closed e2 \ t = S\e2 \ open e1 \ t = S\e1 \ t\{} \ t\S)" ``` chaieb@30262 ` 409` ``` by auto} ``` chaieb@30262 ` 410` ``` then have "(\e1. ?P e2 e1) \ (\t. ?Q e2 t)" by metis} ``` chaieb@30262 ` 411` ``` then have "\e2. (\e1. ?P e2 e1) \ (\t. ?Q e2 t)" by blast ``` chaieb@30262 ` 412` ``` then show ?thesis unfolding th0 th1 by simp ``` chaieb@30262 ` 413` ```qed ``` chaieb@30262 ` 414` chaieb@30262 ` 415` ```lemma connected_empty[simp, intro]: "connected {}" ``` chaieb@30262 ` 416` ``` by (simp add: connected_def) ``` chaieb@30262 ` 417` chaieb@30262 ` 418` ```subsection{* Hausdorff and other separation properties *} ``` chaieb@30262 ` 419` haftmann@31457 ` 420` ```class t0_space = ``` haftmann@31457 ` 421` ``` assumes t0_space: "x \ y \ \U. open U \ \ (x \ U \ y \ U)" ``` haftmann@31457 ` 422` haftmann@31457 ` 423` ```class t1_space = ``` haftmann@31457 ` 424` ``` assumes t1_space: "x \ y \ \U V. open U \ open V \ x \ U \ y \ U \ x \ V \ y \ V" ``` haftmann@31457 ` 425` ```begin ``` haftmann@31457 ` 426` haftmann@31457 ` 427` ```subclass t0_space ``` haftmann@31457 ` 428` ```proof ``` haftmann@31457 ` 429` ```qed (fast dest: t1_space) ``` haftmann@31457 ` 430` haftmann@31457 ` 431` ```end ``` huffman@31421 ` 432` huffman@31421 ` 433` ```text {* T2 spaces are also known as Hausdorff spaces. *} ``` huffman@31421 ` 434` haftmann@31457 ` 435` ```class t2_space = ``` haftmann@31457 ` 436` ``` assumes hausdorff: "x \ y \ \U V. open U \ open V \ x \ U \ y \ V \ U \ V = {}" ``` haftmann@31457 ` 437` ```begin ``` haftmann@31457 ` 438` haftmann@31457 ` 439` ```subclass t1_space ``` haftmann@31457 ` 440` ```proof ``` haftmann@31457 ` 441` ```qed (fast dest: hausdorff) ``` haftmann@31457 ` 442` haftmann@31457 ` 443` ```end ``` huffman@31421 ` 444` huffman@31421 ` 445` ```instance metric_space \ t2_space ``` huffman@31421 ` 446` ```proof ``` huffman@31421 ` 447` ``` fix x y :: "'a::metric_space" ``` huffman@31421 ` 448` ``` assume xy: "x \ y" ``` chaieb@30262 ` 449` ``` let ?U = "ball x (dist x y / 2)" ``` chaieb@30262 ` 450` ``` let ?V = "ball y (dist x y / 2)" ``` chaieb@30262 ` 451` ``` have th0: "\d x y z. (d x z :: real) <= d x y + d y z \ d y z = d z y ``` chaieb@30262 ` 452` ``` ==> ~(d x y * 2 < d x z \ d z y * 2 < d x z)" by arith ``` huffman@31421 ` 453` ``` have "open ?U \ open ?V \ x \ ?U \ y \ ?V \ ?U \ ?V = {}" ``` huffman@31421 ` 454` ``` using dist_pos_lt[OF xy] th0[of dist,OF dist_triangle dist_commute] ``` huffman@31421 ` 455` ``` by (auto simp add: expand_set_eq) ``` huffman@31421 ` 456` ``` then show "\U V. open U \ open V \ x \ U \ y \ V \ U \ V = {}" ``` huffman@31421 ` 457` ``` by blast ``` chaieb@30262 ` 458` ```qed ``` chaieb@30262 ` 459` huffman@31418 ` 460` ```lemma separation_t2: ``` huffman@31421 ` 461` ``` fixes x y :: "'a::t2_space" ``` huffman@31418 ` 462` ``` shows "x \ y \ (\U V. open U \ open V \ x \ U \ y \ V \ U \ V = {})" ``` huffman@30488 ` 463` ``` using hausdorff[of x y] by blast ``` chaieb@30262 ` 464` huffman@31418 ` 465` ```lemma separation_t1: ``` huffman@31421 ` 466` ``` fixes x y :: "'a::t1_space" ``` huffman@31418 ` 467` ``` shows "x \ y \ (\U V. open U \ open V \ x \U \ y\ U \ x\V \ y\V)" ``` huffman@31421 ` 468` ``` using t1_space[of x y] by blast ``` chaieb@30262 ` 469` huffman@31418 ` 470` ```lemma separation_t0: ``` huffman@31421 ` 471` ``` fixes x y :: "'a::t0_space" ``` huffman@31421 ` 472` ``` shows "x \ y \ (\U. open U \ ~(x\U \ y\U))" ``` huffman@31421 ` 473` ``` using t0_space[of x y] by blast ``` chaieb@30262 ` 474` chaieb@30262 ` 475` ```subsection{* Limit points *} ``` chaieb@30262 ` 476` huffman@31345 ` 477` ```definition ``` huffman@31420 ` 478` ``` islimpt:: "'a::topological_space \ 'a set \ bool" ``` huffman@31420 ` 479` ``` (infixr "islimpt" 60) where ``` huffman@31345 ` 480` ``` "x islimpt S \ (\T. x\T \ open T \ (\y\S. y\T \ y\x))" ``` chaieb@30262 ` 481` huffman@31489 ` 482` ```lemma islimptI: ``` huffman@31489 ` 483` ``` assumes "\T. x \ T \ open T \ \y\S. y \ T \ y \ x" ``` huffman@31489 ` 484` ``` shows "x islimpt S" ``` huffman@31489 ` 485` ``` using assms unfolding islimpt_def by auto ``` huffman@31489 ` 486` huffman@31489 ` 487` ```lemma islimptE: ``` huffman@31489 ` 488` ``` assumes "x islimpt S" and "x \ T" and "open T" ``` huffman@31489 ` 489` ``` obtains y where "y \ S" and "y \ T" and "y \ x" ``` chaieb@30262 ` 490` ``` using assms unfolding islimpt_def by auto ``` chaieb@30262 ` 491` chaieb@30262 ` 492` ```lemma islimpt_subset: "x islimpt S \ S \ T ==> x islimpt T" by (auto simp add: islimpt_def) ``` huffman@31420 ` 493` huffman@31420 ` 494` ```lemma islimpt_approachable: ``` huffman@31420 ` 495` ``` fixes x :: "'a::metric_space" ``` huffman@31420 ` 496` ``` shows "x islimpt S \ (\e>0. \x'\S. x' \ x \ dist x' x < e)" ``` chaieb@30262 ` 497` ``` unfolding islimpt_def ``` chaieb@30262 ` 498` ``` apply auto ``` chaieb@30262 ` 499` ``` apply(erule_tac x="ball x e" in allE) ``` huffman@31285 ` 500` ``` apply auto ``` huffman@31285 ` 501` ``` apply(rule_tac x=y in bexI) ``` huffman@31285 ` 502` ``` apply (auto simp add: dist_commute) ``` huffman@31418 ` 503` ``` apply (simp add: open_dist, drule (1) bspec) ``` huffman@31285 ` 504` ``` apply (clarify, drule spec, drule (1) mp, auto) ``` huffman@31285 ` 505` ``` done ``` chaieb@30262 ` 506` huffman@31420 ` 507` ```lemma islimpt_approachable_le: ``` huffman@31420 ` 508` ``` fixes x :: "'a::metric_space" ``` huffman@31420 ` 509` ``` shows "x islimpt S \ (\e>0. \x'\ S. x' \ x \ dist x' x <= e)" ``` chaieb@30262 ` 510` ``` unfolding islimpt_approachable ``` chaieb@30262 ` 511` ``` using approachable_lt_le[where f="\x'. dist x' x" and P="\x'. \ (x'\S \ x'\x)"] ``` huffman@31285 ` 512` ``` by metis (* FIXME: VERY slow! *) ``` chaieb@30262 ` 513` haftmann@31457 ` 514` ```class perfect_space = ``` huffman@31420 ` 515` ``` (* FIXME: perfect_space should inherit from topological_space *) ``` haftmann@31457 ` 516` ``` assumes islimpt_UNIV [simp, intro]: "(x::'a::metric_space) islimpt UNIV" ``` huffman@31345 ` 517` huffman@31345 ` 518` ```lemma perfect_choose_dist: ``` huffman@31345 ` 519` ``` fixes x :: "'a::perfect_space" ``` huffman@31345 ` 520` ``` shows "0 < r \ \a. a \ x \ dist a x < r" ``` huffman@31345 ` 521` ```using islimpt_UNIV [of x] ``` huffman@31345 ` 522` ```by (simp add: islimpt_approachable) ``` huffman@31345 ` 523` huffman@31345 ` 524` ```instance real :: perfect_space ``` huffman@31345 ` 525` ```apply default ``` huffman@31345 ` 526` ```apply (rule islimpt_approachable [THEN iffD2]) ``` huffman@31345 ` 527` ```apply (clarify, rule_tac x="x + e/2" in bexI) ``` huffman@31345 ` 528` ```apply (auto simp add: dist_norm) ``` huffman@31345 ` 529` ```done ``` huffman@31420 ` 530` huffman@31345 ` 531` ```instance "^" :: (perfect_space, finite) perfect_space ``` huffman@31345 ` 532` ```proof ``` huffman@31345 ` 533` ``` fix x :: "'a ^ 'b" ``` chaieb@30262 ` 534` ``` { ``` huffman@31345 ` 535` ``` fix e :: real assume "0 < e" ``` huffman@31345 ` 536` ``` def a \ "x \$ arbitrary" ``` huffman@31345 ` 537` ``` have "a islimpt UNIV" by (rule islimpt_UNIV) ``` huffman@31345 ` 538` ``` with `0 < e` obtain b where "b \ a" and "dist b a < e" ``` huffman@31345 ` 539` ``` unfolding islimpt_approachable by auto ``` huffman@31345 ` 540` ``` def y \ "Cart_lambda ((Cart_nth x)(arbitrary := b))" ``` huffman@31345 ` 541` ``` from `b \ a` have "y \ x" ``` huffman@31345 ` 542` ``` unfolding a_def y_def by (simp add: Cart_eq) ``` huffman@31345 ` 543` ``` from `dist b a < e` have "dist y x < e" ``` huffman@31345 ` 544` ``` unfolding dist_vector_def a_def y_def ``` huffman@31345 ` 545` ``` apply simp ``` huffman@31345 ` 546` ``` apply (rule le_less_trans [OF setL2_le_setsum [OF zero_le_dist]]) ``` huffman@31345 ` 547` ``` apply (subst setsum_diff1' [where a=arbitrary], simp, simp, simp) ``` huffman@31345 ` 548` ``` done ``` huffman@31345 ` 549` ``` from `y \ x` and `dist y x < e` ``` huffman@31345 ` 550` ``` have "\y\UNIV. y \ x \ dist y x < e" by auto ``` huffman@31345 ` 551` ``` } ``` huffman@31345 ` 552` ``` then show "x islimpt UNIV" unfolding islimpt_approachable by blast ``` chaieb@30262 ` 553` ```qed ``` chaieb@30262 ` 554` chaieb@30262 ` 555` ```lemma closed_limpt: "closed S \ (\x. x islimpt S \ x \ S)" ``` chaieb@30262 ` 556` ``` unfolding closed_def ``` chaieb@30262 ` 557` ``` apply (subst open_subopen) ``` huffman@31490 ` 558` ``` apply (simp add: islimpt_def subset_eq Compl_eq_Diff_UNIV) ``` chaieb@30262 ` 559` ``` by (metis DiffE DiffI UNIV_I insertCI insert_absorb mem_def) ``` chaieb@30262 ` 560` chaieb@30262 ` 561` ```lemma islimpt_EMPTY[simp]: "\ x islimpt {}" ``` huffman@31420 ` 562` ``` unfolding islimpt_def by auto ``` chaieb@30262 ` 563` huffman@30582 ` 564` ```lemma closed_positive_orthant: "closed {x::real^'n::finite. \i. 0 \x\$i}" ``` chaieb@30262 ` 565` ```proof- ``` huffman@30582 ` 566` ``` let ?U = "UNIV :: 'n set" ``` huffman@30582 ` 567` ``` let ?O = "{x::real^'n. \i. x\$i\0}" ``` huffman@30582 ` 568` ``` {fix x:: "real^'n" and i::'n assume H: "\e>0. \x'\?O. x' \ x \ dist x' x < e" ``` chaieb@30262 ` 569` ``` and xi: "x\$i < 0" ``` chaieb@30262 ` 570` ``` from xi have th0: "-x\$i > 0" by arith ``` chaieb@30262 ` 571` ``` from H[rule_format, OF th0] obtain x' where x': "x' \?O" "x' \ x" "dist x' x < -x \$ i" by blast ``` chaieb@30262 ` 572` ``` have th:" \b a (x::real). abs x <= b \ b <= a ==> ~(a + x < 0)" by arith ``` chaieb@30262 ` 573` ``` have th': "\x (y::real). x < 0 \ 0 <= y ==> abs x <= abs (y - x)" by arith ``` huffman@30582 ` 574` ``` have th1: "\x\$i\ \ \(x' - x)\$i\" using x'(1) xi ``` chaieb@30262 ` 575` ``` apply (simp only: vector_component) ``` chaieb@30262 ` 576` ``` by (rule th') auto ``` huffman@30582 ` 577` ``` have th2: "\dist x x'\ \ \(x' - x)\$i\" using component_le_norm[of "x'-x" i] ``` huffman@31289 ` 578` ``` apply (simp add: dist_norm) by norm ``` huffman@31285 ` 579` ``` from th[OF th1 th2] x'(3) have False by (simp add: dist_commute) } ``` huffman@30488 ` 580` ``` then show ?thesis unfolding closed_limpt islimpt_approachable ``` chaieb@30262 ` 581` ``` unfolding not_le[symmetric] by blast ``` chaieb@30262 ` 582` ```qed ``` chaieb@30262 ` 583` huffman@31289 ` 584` ```lemma finite_set_avoid: ``` huffman@31345 ` 585` ``` fixes a :: "'a::metric_space" ``` huffman@31289 ` 586` ``` assumes fS: "finite S" shows "\d>0. \x\S. x \ a \ d <= dist a x" ``` chaieb@30262 ` 587` ```proof(induct rule: finite_induct[OF fS]) ``` chaieb@30262 ` 588` ``` case 1 thus ?case apply auto by ferrack ``` chaieb@30262 ` 589` ```next ``` huffman@30488 ` 590` ``` case (2 x F) ``` chaieb@30262 ` 591` ``` from 2 obtain d where d: "d >0" "\x\F. x\a \ d \ dist a x" by blast ``` chaieb@30262 ` 592` ``` {assume "x = a" hence ?case using d by auto } ``` chaieb@30262 ` 593` ``` moreover ``` chaieb@30262 ` 594` ``` {assume xa: "x\a" ``` chaieb@30262 ` 595` ``` let ?d = "min d (dist a x)" ``` chaieb@30262 ` 596` ``` have dp: "?d > 0" using xa d(1) using dist_nz by auto ``` chaieb@30262 ` 597` ``` from d have d': "\x\F. x\a \ ?d \ dist a x" by auto ``` chaieb@30262 ` 598` ``` with dp xa have ?case by(auto intro!: exI[where x="?d"]) } ``` chaieb@30262 ` 599` ``` ultimately show ?case by blast ``` chaieb@30262 ` 600` ```qed ``` chaieb@30262 ` 601` huffman@31420 ` 602` ```lemma islimpt_finite: ``` huffman@31420 ` 603` ``` fixes S :: "'a::metric_space set" ``` huffman@31420 ` 604` ``` assumes fS: "finite S" shows "\ a islimpt S" ``` huffman@30488 ` 605` ``` unfolding islimpt_approachable ``` huffman@31285 ` 606` ``` using finite_set_avoid[OF fS, of a] by (metis dist_commute not_le) ``` chaieb@30262 ` 607` chaieb@30262 ` 608` ```lemma islimpt_Un: "x islimpt (S \ T) \ x islimpt S \ x islimpt T" ``` chaieb@30262 ` 609` ``` apply (rule iffI) ``` chaieb@30262 ` 610` ``` defer ``` chaieb@30262 ` 611` ``` apply (metis Un_upper1 Un_upper2 islimpt_subset) ``` huffman@31420 ` 612` ``` unfolding islimpt_def ``` huffman@31420 ` 613` ``` apply (rule ccontr, clarsimp, rename_tac A B) ``` huffman@31420 ` 614` ``` apply (drule_tac x="A \ B" in spec) ``` huffman@31490 ` 615` ``` apply (auto simp add: open_Int) ``` chaieb@30262 ` 616` ``` done ``` chaieb@30262 ` 617` huffman@30488 ` 618` ```lemma discrete_imp_closed: ``` huffman@31418 ` 619` ``` fixes S :: "'a::metric_space set" ``` huffman@31345 ` 620` ``` assumes e: "0 < e" and d: "\x \ S. \y \ S. dist y x < e \ y = x" ``` chaieb@30262 ` 621` ``` shows "closed S" ``` huffman@30488 ` 622` ```proof- ``` chaieb@30262 ` 623` ``` {fix x assume C: "\e>0. \x'\S. x' \ x \ dist x' x < e" ``` chaieb@30262 ` 624` ``` from e have e2: "e/2 > 0" by arith ``` chaieb@30262 ` 625` ``` from C[rule_format, OF e2] obtain y where y: "y \ S" "y\x" "dist y x < e/2" by blast ``` chaieb@30262 ` 626` ``` let ?m = "min (e/2) (dist x y) " ``` chaieb@30262 ` 627` ``` from e2 y(2) have mp: "?m > 0" by (simp add: dist_nz[THEN sym]) ``` chaieb@30262 ` 628` ``` from C[rule_format, OF mp] obtain z where z: "z \ S" "z\x" "dist z x < ?m" by blast ``` huffman@31345 ` 629` ``` have th: "dist z y < e" using z y ``` huffman@31285 ` 630` ``` by (intro dist_triangle_lt [where z=x], simp) ``` huffman@30488 ` 631` ``` from d[rule_format, OF y(1) z(1) th] y z ``` huffman@31285 ` 632` ``` have False by (auto simp add: dist_commute)} ``` huffman@31420 ` 633` ``` then show ?thesis by (metis islimpt_approachable closed_limpt [where 'a='a]) ``` chaieb@30262 ` 634` ```qed ``` chaieb@30262 ` 635` chaieb@30262 ` 636` ```subsection{* Interior of a Set *} ``` chaieb@30262 ` 637` ```definition "interior S = {x. \T. open T \ x \ T \ T \ S}" ``` chaieb@30262 ` 638` chaieb@30262 ` 639` ```lemma interior_eq: "interior S = S \ open S" ``` chaieb@30262 ` 640` ``` apply (simp add: expand_set_eq interior_def) ``` huffman@31418 ` 641` ``` apply (subst (2) open_subopen) by (safe, blast+) ``` chaieb@30262 ` 642` chaieb@30262 ` 643` ```lemma interior_open: "open S ==> (interior S = S)" by (metis interior_eq) ``` chaieb@30262 ` 644` chaieb@30262 ` 645` ```lemma interior_empty[simp]: "interior {} = {}" by (simp add: interior_def) ``` chaieb@30262 ` 646` chaieb@30262 ` 647` ```lemma open_interior[simp, intro]: "open(interior S)" ``` chaieb@30262 ` 648` ``` apply (simp add: interior_def) ``` chaieb@30262 ` 649` ``` apply (subst open_subopen) by blast ``` chaieb@30262 ` 650` chaieb@30262 ` 651` ```lemma interior_interior[simp]: "interior(interior S) = interior S" by (metis interior_eq open_interior) ``` huffman@30488 ` 652` ```lemma interior_subset: "interior S \ S" by (auto simp add: interior_def) ``` chaieb@30262 ` 653` ```lemma subset_interior: "S \ T ==> (interior S) \ (interior T)" by (auto simp add: interior_def) ``` chaieb@30262 ` 654` ```lemma interior_maximal: "T \ S \ open T ==> T \ (interior S)" by (auto simp add: interior_def) ``` chaieb@30262 ` 655` ```lemma interior_unique: "T \ S \ open T \ (\T'. T' \ S \ open T' \ T' \ T) \ interior S = T" ``` chaieb@30262 ` 656` ``` by (metis equalityI interior_maximal interior_subset open_interior) ``` chaieb@30262 ` 657` ```lemma mem_interior: "x \ interior S \ (\e. 0 < e \ ball x e \ S)" ``` chaieb@30262 ` 658` ``` apply (simp add: interior_def) ``` chaieb@30262 ` 659` ``` by (metis open_contains_ball centre_in_ball open_ball subset_trans) ``` chaieb@30262 ` 660` chaieb@30262 ` 661` ```lemma open_subset_interior: "open S ==> S \ interior T \ S \ T" ``` chaieb@30262 ` 662` ``` by (metis interior_maximal interior_subset subset_trans) ``` chaieb@30262 ` 663` chaieb@30262 ` 664` ```lemma interior_inter[simp]: "interior(S \ T) = interior S \ interior T" ``` chaieb@30262 ` 665` ``` apply (rule equalityI, simp) ``` chaieb@30262 ` 666` ``` apply (metis Int_lower1 Int_lower2 subset_interior) ``` huffman@31490 ` 667` ``` by (metis Int_mono interior_subset open_Int open_interior open_subset_interior) ``` chaieb@30262 ` 668` huffman@31345 ` 669` ```lemma interior_limit_point [intro]: ``` huffman@31345 ` 670` ``` fixes x :: "'a::perfect_space" ``` huffman@31345 ` 671` ``` assumes x: "x \ interior S" shows "x islimpt S" ``` chaieb@30262 ` 672` ```proof- ``` chaieb@30262 ` 673` ``` from x obtain e where e: "e>0" "\x'. dist x x' < e \ x' \ S" ``` chaieb@30262 ` 674` ``` unfolding mem_interior subset_eq Ball_def mem_ball by blast ``` huffman@31345 ` 675` ``` { ``` huffman@31345 ` 676` ``` fix d::real assume d: "d>0" ``` huffman@31345 ` 677` ``` let ?m = "min d e" ``` huffman@31345 ` 678` ``` have mde2: "0 < ?m" using e(1) d(1) by simp ``` huffman@31345 ` 679` ``` from perfect_choose_dist [OF mde2, of x] ``` huffman@31345 ` 680` ``` obtain y where "y \ x" and "dist y x < ?m" by blast ``` huffman@31345 ` 681` ``` then have "dist y x < e" "dist y x < d" by simp_all ``` huffman@31345 ` 682` ``` from `dist y x < e` e(2) have "y \ S" by (simp add: dist_commute) ``` huffman@30488 ` 683` ``` have "\x'\S. x'\ x \ dist x' x < d" ``` huffman@31345 ` 684` ``` using `y \ S` `y \ x` `dist y x < d` by fast ``` huffman@31345 ` 685` ``` } ``` chaieb@30262 ` 686` ``` then show ?thesis unfolding islimpt_approachable by blast ``` chaieb@30262 ` 687` ```qed ``` chaieb@30262 ` 688` huffman@30488 ` 689` ```lemma interior_closed_Un_empty_interior: ``` chaieb@30262 ` 690` ``` assumes cS: "closed S" and iT: "interior T = {}" ``` chaieb@30262 ` 691` ``` shows "interior(S \ T) = interior S" ``` huffman@31394 ` 692` ```proof ``` huffman@31394 ` 693` ``` show "interior S \ interior (S\T)" ``` chaieb@30262 ` 694` ``` by (rule subset_interior, blast) ``` huffman@31394 ` 695` ```next ``` huffman@31394 ` 696` ``` show "interior (S \ T) \ interior S" ``` huffman@31394 ` 697` ``` proof ``` huffman@31394 ` 698` ``` fix x assume "x \ interior (S \ T)" ``` huffman@31394 ` 699` ``` then obtain R where "open R" "x \ R" "R \ S \ T" ``` huffman@31394 ` 700` ``` unfolding interior_def by fast ``` huffman@31394 ` 701` ``` show "x \ interior S" ``` huffman@31394 ` 702` ``` proof (rule ccontr) ``` huffman@31394 ` 703` ``` assume "x \ interior S" ``` huffman@31394 ` 704` ``` with `x \ R` `open R` obtain y where "y \ R - S" ``` huffman@31394 ` 705` ``` unfolding interior_def expand_set_eq by fast ``` huffman@31490 ` 706` ``` from `open R` `closed S` have "open (R - S)" by (rule open_Diff) ``` huffman@31394 ` 707` ``` from `R \ S \ T` have "R - S \ T" by fast ``` huffman@31394 ` 708` ``` from `y \ R - S` `open (R - S)` `R - S \ T` `interior T = {}` ``` huffman@31394 ` 709` ``` show "False" unfolding interior_def by fast ``` huffman@31394 ` 710` ``` qed ``` huffman@31394 ` 711` ``` qed ``` chaieb@30262 ` 712` ```qed ``` chaieb@30262 ` 713` chaieb@30262 ` 714` chaieb@30262 ` 715` ```subsection{* Closure of a Set *} ``` chaieb@30262 ` 716` chaieb@30262 ` 717` ```definition "closure S = S \ {x | x. x islimpt S}" ``` chaieb@30262 ` 718` chaieb@30262 ` 719` ```lemma closure_interior: "closure S = UNIV - interior (UNIV - S)" ``` chaieb@30262 ` 720` ```proof- ``` chaieb@30262 ` 721` ``` { fix x ``` chaieb@30262 ` 722` ``` have "x\UNIV - interior (UNIV - S) \ x \ closure S" (is "?lhs = ?rhs") ``` chaieb@30262 ` 723` ``` proof ``` chaieb@30262 ` 724` ``` let ?exT = "\ y. (\T. open T \ y \ T \ T \ UNIV - S)" ``` chaieb@30262 ` 725` ``` assume "?lhs" ``` chaieb@30262 ` 726` ``` hence *:"\ ?exT x" ``` chaieb@30262 ` 727` ``` unfolding interior_def ``` chaieb@30262 ` 728` ``` by simp ``` chaieb@30262 ` 729` ``` { assume "\ ?rhs" ``` chaieb@30262 ` 730` ``` hence False using * ``` chaieb@30262 ` 731` ``` unfolding closure_def islimpt_def ``` chaieb@30262 ` 732` ``` by blast ``` chaieb@30262 ` 733` ``` } ``` chaieb@30262 ` 734` ``` thus "?rhs" ``` chaieb@30262 ` 735` ``` by blast ``` chaieb@30262 ` 736` ``` next ``` chaieb@30262 ` 737` ``` assume "?rhs" thus "?lhs" ``` chaieb@30262 ` 738` ``` unfolding closure_def interior_def islimpt_def ``` chaieb@30262 ` 739` ``` by blast ``` chaieb@30262 ` 740` ``` qed ``` chaieb@30262 ` 741` ``` } ``` chaieb@30262 ` 742` ``` thus ?thesis ``` chaieb@30262 ` 743` ``` by blast ``` chaieb@30262 ` 744` ```qed ``` chaieb@30262 ` 745` chaieb@30262 ` 746` ```lemma interior_closure: "interior S = UNIV - (closure (UNIV - S))" ``` chaieb@30262 ` 747` ```proof- ``` chaieb@30262 ` 748` ``` { fix x ``` chaieb@30262 ` 749` ``` have "x \ interior S \ x \ UNIV - (closure (UNIV - S))" ``` chaieb@30262 ` 750` ``` unfolding interior_def closure_def islimpt_def ``` chaieb@30262 ` 751` ``` by blast ``` chaieb@30262 ` 752` ``` } ``` chaieb@30262 ` 753` ``` thus ?thesis ``` chaieb@30262 ` 754` ``` by blast ``` chaieb@30262 ` 755` ```qed ``` chaieb@30262 ` 756` chaieb@30262 ` 757` ```lemma closed_closure[simp, intro]: "closed (closure S)" ``` chaieb@30262 ` 758` ```proof- ``` chaieb@30262 ` 759` ``` have "closed (UNIV - interior (UNIV -S))" by blast ``` chaieb@30262 ` 760` ``` thus ?thesis using closure_interior[of S] by simp ``` chaieb@30262 ` 761` ```qed ``` chaieb@30262 ` 762` chaieb@30262 ` 763` ```lemma closure_hull: "closure S = closed hull S" ``` chaieb@30262 ` 764` ```proof- ``` chaieb@30262 ` 765` ``` have "S \ closure S" ``` chaieb@30262 ` 766` ``` unfolding closure_def ``` chaieb@30262 ` 767` ``` by blast ``` chaieb@30262 ` 768` ``` moreover ``` chaieb@30262 ` 769` ``` have "closed (closure S)" ``` chaieb@30262 ` 770` ``` using closed_closure[of S] ``` chaieb@30262 ` 771` ``` by assumption ``` chaieb@30262 ` 772` ``` moreover ``` chaieb@30262 ` 773` ``` { fix t ``` chaieb@30262 ` 774` ``` assume *:"S \ t" "closed t" ``` chaieb@30262 ` 775` ``` { fix x ``` chaieb@30262 ` 776` ``` assume "x islimpt S" ``` chaieb@30262 ` 777` ``` hence "x islimpt t" using *(1) ``` chaieb@30262 ` 778` ``` using islimpt_subset[of x, of S, of t] ``` chaieb@30262 ` 779` ``` by blast ``` chaieb@30262 ` 780` ``` } ``` chaieb@30262 ` 781` ``` with * have "closure S \ t" ``` chaieb@30262 ` 782` ``` unfolding closure_def ``` chaieb@30262 ` 783` ``` using closed_limpt[of t] ``` huffman@31345 ` 784` ``` by auto ``` chaieb@30262 ` 785` ``` } ``` chaieb@30262 ` 786` ``` ultimately show ?thesis ``` chaieb@30262 ` 787` ``` using hull_unique[of S, of "closure S", of closed] ``` chaieb@30262 ` 788` ``` unfolding mem_def ``` chaieb@30262 ` 789` ``` by simp ``` chaieb@30262 ` 790` ```qed ``` chaieb@30262 ` 791` chaieb@30262 ` 792` ```lemma closure_eq: "closure S = S \ closed S" ``` chaieb@30262 ` 793` ``` unfolding closure_hull ``` chaieb@30262 ` 794` ``` using hull_eq[of closed, unfolded mem_def, OF closed_Inter, of S] ``` chaieb@30262 ` 795` ``` by (metis mem_def subset_eq) ``` chaieb@30262 ` 796` chaieb@30262 ` 797` ```lemma closure_closed[simp]: "closed S \ closure S = S" ``` chaieb@30262 ` 798` ``` using closure_eq[of S] ``` chaieb@30262 ` 799` ``` by simp ``` chaieb@30262 ` 800` chaieb@30262 ` 801` ```lemma closure_closure[simp]: "closure (closure S) = closure S" ``` chaieb@30262 ` 802` ``` unfolding closure_hull ``` chaieb@30262 ` 803` ``` using hull_hull[of closed S] ``` chaieb@30262 ` 804` ``` by assumption ``` chaieb@30262 ` 805` chaieb@30262 ` 806` ```lemma closure_subset: "S \ closure S" ``` chaieb@30262 ` 807` ``` unfolding closure_hull ``` chaieb@30262 ` 808` ``` using hull_subset[of S closed] ``` chaieb@30262 ` 809` ``` by assumption ``` chaieb@30262 ` 810` chaieb@30262 ` 811` ```lemma subset_closure: "S \ T \ closure S \ closure T" ``` chaieb@30262 ` 812` ``` unfolding closure_hull ``` chaieb@30262 ` 813` ``` using hull_mono[of S T closed] ``` chaieb@30262 ` 814` ``` by assumption ``` chaieb@30262 ` 815` chaieb@30262 ` 816` ```lemma closure_minimal: "S \ T \ closed T \ closure S \ T" ``` chaieb@30262 ` 817` ``` using hull_minimal[of S T closed] ``` chaieb@30262 ` 818` ``` unfolding closure_hull mem_def ``` chaieb@30262 ` 819` ``` by simp ``` chaieb@30262 ` 820` chaieb@30262 ` 821` ```lemma closure_unique: "S \ T \ closed T \ (\ T'. S \ T' \ closed T' \ T \ T') \ closure S = T" ``` chaieb@30262 ` 822` ``` using hull_unique[of S T closed] ``` chaieb@30262 ` 823` ``` unfolding closure_hull mem_def ``` chaieb@30262 ` 824` ``` by simp ``` chaieb@30262 ` 825` chaieb@30262 ` 826` ```lemma closure_empty[simp]: "closure {} = {}" ``` chaieb@30262 ` 827` ``` using closed_empty closure_closed[of "{}"] ``` chaieb@30262 ` 828` ``` by simp ``` chaieb@30262 ` 829` chaieb@30262 ` 830` ```lemma closure_univ[simp]: "closure UNIV = UNIV" ``` chaieb@30262 ` 831` ``` using closure_closed[of UNIV] ``` chaieb@30262 ` 832` ``` by simp ``` chaieb@30262 ` 833` chaieb@30262 ` 834` ```lemma closure_eq_empty: "closure S = {} \ S = {}" ``` chaieb@30262 ` 835` ``` using closure_empty closure_subset[of S] ``` chaieb@30262 ` 836` ``` by blast ``` chaieb@30262 ` 837` chaieb@30262 ` 838` ```lemma closure_subset_eq: "closure S \ S \ closed S" ``` chaieb@30262 ` 839` ``` using closure_eq[of S] closure_subset[of S] ``` chaieb@30262 ` 840` ``` by simp ``` chaieb@30262 ` 841` chaieb@30262 ` 842` ```lemma open_inter_closure_eq_empty: ``` chaieb@30262 ` 843` ``` "open S \ (S \ closure T) = {} \ S \ T = {}" ``` chaieb@30262 ` 844` ``` using open_subset_interior[of S "UNIV - T"] ``` chaieb@30262 ` 845` ``` using interior_subset[of "UNIV - T"] ``` chaieb@30262 ` 846` ``` unfolding closure_interior ``` chaieb@30262 ` 847` ``` by auto ``` chaieb@30262 ` 848` huffman@31420 ` 849` ```lemma open_inter_closure_subset: ``` huffman@31489 ` 850` ``` "open S \ (S \ (closure T)) \ closure(S \ T)" ``` chaieb@30262 ` 851` ```proof ``` chaieb@30262 ` 852` ``` fix x ``` chaieb@30262 ` 853` ``` assume as: "open S" "x \ S \ closure T" ``` chaieb@30262 ` 854` ``` { assume *:"x islimpt T" ``` huffman@31489 ` 855` ``` have "x islimpt (S \ T)" ``` huffman@31489 ` 856` ``` proof (rule islimptI) ``` huffman@31489 ` 857` ``` fix A ``` huffman@31489 ` 858` ``` assume "x \ A" "open A" ``` huffman@31489 ` 859` ``` with as have "x \ A \ S" "open (A \ S)" ``` huffman@31490 ` 860` ``` by (simp_all add: open_Int) ``` huffman@31489 ` 861` ``` with * obtain y where "y \ T" "y \ A \ S" "y \ x" ``` huffman@31489 ` 862` ``` by (rule islimptE) ``` huffman@31489 ` 863` ``` hence "y \ S \ T" "y \ A \ y \ x" ``` huffman@31489 ` 864` ``` by simp_all ``` huffman@31489 ` 865` ``` thus "\y\(S \ T). y \ A \ y \ x" .. ``` huffman@31489 ` 866` ``` qed ``` chaieb@30262 ` 867` ``` } ``` chaieb@30262 ` 868` ``` then show "x \ closure (S \ T)" using as ``` chaieb@30262 ` 869` ``` unfolding closure_def ``` chaieb@30262 ` 870` ``` by blast ``` chaieb@30262 ` 871` ```qed ``` chaieb@30262 ` 872` chaieb@30262 ` 873` ```lemma closure_complement: "closure(UNIV - S) = UNIV - interior(S)" ``` chaieb@30262 ` 874` ```proof- ``` chaieb@30262 ` 875` ``` have "S = UNIV - (UNIV - S)" ``` chaieb@30262 ` 876` ``` by auto ``` chaieb@30262 ` 877` ``` thus ?thesis ``` chaieb@30262 ` 878` ``` unfolding closure_interior ``` chaieb@30262 ` 879` ``` by auto ``` chaieb@30262 ` 880` ```qed ``` chaieb@30262 ` 881` chaieb@30262 ` 882` ```lemma interior_complement: "interior(UNIV - S) = UNIV - closure(S)" ``` chaieb@30262 ` 883` ``` unfolding closure_interior ``` chaieb@30262 ` 884` ``` by blast ``` chaieb@30262 ` 885` chaieb@30262 ` 886` ```subsection{* Frontier (aka boundary) *} ``` chaieb@30262 ` 887` chaieb@30262 ` 888` ```definition "frontier S = closure S - interior S" ``` chaieb@30262 ` 889` chaieb@30262 ` 890` ```lemma frontier_closed: "closed(frontier S)" ``` huffman@31490 ` 891` ``` by (simp add: frontier_def closed_Diff) ``` chaieb@30262 ` 892` chaieb@30262 ` 893` ```lemma frontier_closures: "frontier S = (closure S) \ (closure(UNIV - S))" ``` chaieb@30262 ` 894` ``` by (auto simp add: frontier_def interior_closure) ``` chaieb@30262 ` 895` huffman@31420 ` 896` ```lemma frontier_straddle: ``` huffman@31420 ` 897` ``` fixes a :: "'a::metric_space" ``` huffman@31420 ` 898` ``` shows "a \ frontier S \ (\e>0. (\x\S. dist a x < e) \ (\x. x \ S \ dist a x < e))" (is "?lhs \ ?rhs") ``` chaieb@30262 ` 899` ```proof ``` chaieb@30262 ` 900` ``` assume "?lhs" ``` chaieb@30262 ` 901` ``` { fix e::real ``` chaieb@30262 ` 902` ``` assume "e > 0" ``` chaieb@30262 ` 903` ``` let ?rhse = "(\x\S. dist a x < e) \ (\x. x \ S \ dist a x < e)" ``` chaieb@30262 ` 904` ``` { assume "a\S" ``` huffman@31285 ` 905` ``` have "\x\S. dist a x < e" using `e>0` `a\S` by(rule_tac x=a in bexI) auto ``` chaieb@30262 ` 906` ``` moreover have "\x. x \ S \ dist a x < e" using `?lhs` `a\S` ``` huffman@31285 ` 907` ``` unfolding frontier_closures closure_def islimpt_def using `e>0` ``` chaieb@30262 ` 908` ``` by (auto, erule_tac x="ball a e" in allE, auto) ``` chaieb@30262 ` 909` ``` ultimately have ?rhse by auto ``` chaieb@30262 ` 910` ``` } ``` chaieb@30262 ` 911` ``` moreover ``` chaieb@30262 ` 912` ``` { assume "a\S" ``` chaieb@30262 ` 913` ``` hence ?rhse using `?lhs` ``` chaieb@30262 ` 914` ``` unfolding frontier_closures closure_def islimpt_def ``` huffman@31285 ` 915` ``` using open_ball[of a e] `e > 0` ``` huffman@31285 ` 916` ``` by (auto, erule_tac x = "ball a e" in allE, auto) (* FIXME: VERY slow! *) ``` chaieb@30262 ` 917` ``` } ``` huffman@30488 ` 918` ``` ultimately have ?rhse by auto ``` chaieb@30262 ` 919` ``` } ``` chaieb@30262 ` 920` ``` thus ?rhs by auto ``` chaieb@30262 ` 921` ```next ``` chaieb@30262 ` 922` ``` assume ?rhs ``` chaieb@30262 ` 923` ``` moreover ``` chaieb@30262 ` 924` ``` { fix T assume "a\S" and ``` chaieb@30262 ` 925` ``` as:"\e>0. (\x\S. dist a x < e) \ (\x. x \ S \ dist a x < e)" "a \ S" "a \ T" "open T" ``` chaieb@30262 ` 926` ``` from `open T` `a \ T` have "\e>0. ball a e \ T" unfolding open_contains_ball[of T] by auto ``` chaieb@30262 ` 927` ``` then obtain e where "e>0" "ball a e \ T" by auto ``` chaieb@30262 ` 928` ``` then obtain y where y:"y\S" "dist a y < e" using as(1) by auto ``` chaieb@30262 ` 929` ``` have "\y\S. y \ T \ y \ a" ``` chaieb@30262 ` 930` ``` using `dist a y < e` `ball a e \ T` unfolding ball_def using `y\S` `a\S` by auto ``` chaieb@30262 ` 931` ``` } ``` chaieb@30262 ` 932` ``` hence "a \ closure S" unfolding closure_def islimpt_def using `?rhs` by auto ``` chaieb@30262 ` 933` ``` moreover ``` chaieb@30262 ` 934` ``` { fix T assume "a \ T" "open T" "a\S" ``` chaieb@30262 ` 935` ``` then obtain e where "e>0" and balle: "ball a e \ T" unfolding open_contains_ball using `?rhs` by auto ``` chaieb@30262 ` 936` ``` obtain x where "x \ S" "dist a x < e" using `?rhs` using `e>0` by auto ``` chaieb@30262 ` 937` ``` hence "\y\UNIV - S. y \ T \ y \ a" using balle `a\S` unfolding ball_def by (rule_tac x=x in bexI)auto ``` chaieb@30262 ` 938` ``` } ``` chaieb@30262 ` 939` ``` hence "a islimpt (UNIV - S) \ a\S" unfolding islimpt_def by auto ``` chaieb@30262 ` 940` ``` ultimately show ?lhs unfolding frontier_closures using closure_def[of "UNIV - S"] by auto ``` chaieb@30262 ` 941` ```qed ``` chaieb@30262 ` 942` huffman@30488 ` 943` ```lemma frontier_subset_closed: "closed S \ frontier S \ S" ``` chaieb@30262 ` 944` ``` by (metis frontier_def closure_closed Diff_subset) ``` chaieb@30262 ` 945` chaieb@30262 ` 946` ```lemma frontier_empty: "frontier {} = {}" ``` chaieb@30262 ` 947` ``` by (simp add: frontier_def closure_empty) ``` chaieb@30262 ` 948` chaieb@30262 ` 949` ```lemma frontier_subset_eq: "frontier S \ S \ closed S" ``` chaieb@30262 ` 950` ```proof- ``` chaieb@30262 ` 951` ``` { assume "frontier S \ S" ``` chaieb@30262 ` 952` ``` hence "closure S \ S" using interior_subset unfolding frontier_def by auto ``` chaieb@30262 ` 953` ``` hence "closed S" using closure_subset_eq by auto ``` chaieb@30262 ` 954` ``` } ``` chaieb@30262 ` 955` ``` thus ?thesis using frontier_subset_closed[of S] by auto ``` chaieb@30262 ` 956` ```qed ``` chaieb@30262 ` 957` huffman@30488 ` 958` ```lemma frontier_complement: "frontier(UNIV - S) = frontier S" ``` chaieb@30262 ` 959` ``` by (auto simp add: frontier_def closure_complement interior_complement) ``` chaieb@30262 ` 960` chaieb@30262 ` 961` ```lemma frontier_disjoint_eq: "frontier S \ S = {} \ open S" ``` huffman@30488 ` 962` ``` using frontier_complement frontier_subset_eq[of "UNIV - S"] ``` huffman@31490 ` 963` ``` unfolding open_closed Compl_eq_Diff_UNIV by auto ``` chaieb@30262 ` 964` chaieb@30262 ` 965` ```subsection{* Common nets and The "within" modifier for nets. *} ``` chaieb@30262 ` 966` huffman@31285 ` 967` ```definition ``` huffman@31346 ` 968` ``` at_infinity :: "'a::real_normed_vector net" where ``` huffman@31390 ` 969` ``` "at_infinity = Abs_net (range (\r. {x. r \ norm x}))" ``` huffman@31346 ` 970` huffman@31346 ` 971` ```definition ``` huffman@31530 ` 972` ``` indirection :: "'a::real_normed_vector \ 'a \ 'a net" (infixr "indirection" 70) where ``` huffman@31530 ` 973` ``` "a indirection v = (at a) within {b. \c\0. b - a = scaleR c v}" ``` chaieb@30262 ` 974` chaieb@30262 ` 975` ```text{* Prove That They are all nets. *} ``` chaieb@30262 ` 976` huffman@31390 ` 977` ```lemma Rep_net_at_infinity: ``` huffman@31390 ` 978` ``` "Rep_net at_infinity = range (\r. {x. r \ norm x})" ``` huffman@31390 ` 979` ```unfolding at_infinity_def ``` huffman@31390 ` 980` ```apply (rule Abs_net_inverse') ``` huffman@31390 ` 981` ```apply (rule image_nonempty, simp) ``` huffman@31390 ` 982` ```apply (clarsimp, rename_tac r s) ``` huffman@31390 ` 983` ```apply (rule_tac x="max r s" in exI, auto) ``` huffman@31390 ` 984` ```done ``` huffman@31390 ` 985` huffman@31346 ` 986` ```lemma within_UNIV: "net within UNIV = net" ``` huffman@31390 ` 987` ``` by (simp add: Rep_net_inject [symmetric] Rep_net_within) ``` chaieb@30262 ` 988` chaieb@30262 ` 989` ```subsection{* Identify Trivial limits, where we can't approach arbitrarily closely. *} ``` chaieb@30262 ` 990` huffman@31346 ` 991` ```definition ``` huffman@31346 ` 992` ``` trivial_limit :: "'a net \ bool" where ``` huffman@31390 ` 993` ``` "trivial_limit net \ {} \ Rep_net net" ``` huffman@31346 ` 994` huffman@31346 ` 995` ```lemma trivial_limit_within: ``` huffman@31346 ` 996` ``` shows "trivial_limit (at a within S) \ \ a islimpt S" ``` huffman@31390 ` 997` ```proof ``` huffman@31390 ` 998` ``` assume "trivial_limit (at a within S)" ``` huffman@31390 ` 999` ``` thus "\ a islimpt S" ``` huffman@31390 ` 1000` ``` unfolding trivial_limit_def ``` huffman@31390 ` 1001` ``` unfolding Rep_net_within Rep_net_at ``` huffman@31492 ` 1002` ``` unfolding islimpt_def ``` huffman@31447 ` 1003` ``` apply (clarsimp simp add: expand_set_eq) ``` huffman@31447 ` 1004` ``` apply (rename_tac T, rule_tac x=T in exI) ``` huffman@31447 ` 1005` ``` apply (clarsimp, drule_tac x=y in spec, simp) ``` huffman@31390 ` 1006` ``` done ``` huffman@31390 ` 1007` ```next ``` huffman@31390 ` 1008` ``` assume "\ a islimpt S" ``` huffman@31390 ` 1009` ``` thus "trivial_limit (at a within S)" ``` huffman@31390 ` 1010` ``` unfolding trivial_limit_def ``` huffman@31390 ` 1011` ``` unfolding Rep_net_within Rep_net_at ``` huffman@31492 ` 1012` ``` unfolding islimpt_def ``` huffman@31447 ` 1013` ``` apply (clarsimp simp add: image_image) ``` huffman@31447 ` 1014` ``` apply (rule_tac x=T in image_eqI) ``` huffman@31390 ` 1015` ``` apply (auto simp add: expand_set_eq) ``` huffman@31390 ` 1016` ``` done ``` chaieb@30262 ` 1017` ```qed ``` chaieb@30262 ` 1018` huffman@31391 ` 1019` ```lemma trivial_limit_at_iff: "trivial_limit (at a) \ \ a islimpt UNIV" ``` huffman@31346 ` 1020` ``` using trivial_limit_within [of a UNIV] ``` huffman@31346 ` 1021` ``` by (simp add: within_UNIV) ``` huffman@31346 ` 1022` huffman@31391 ` 1023` ```lemma trivial_limit_at: ``` huffman@31391 ` 1024` ``` fixes a :: "'a::perfect_space" ``` huffman@31391 ` 1025` ``` shows "\ trivial_limit (at a)" ``` huffman@31391 ` 1026` ``` by (simp add: trivial_limit_at_iff) ``` huffman@31391 ` 1027` huffman@31346 ` 1028` ```lemma trivial_limit_at_infinity: ``` huffman@31346 ` 1029` ``` "\ trivial_limit (at_infinity :: ('a::{real_normed_vector,zero_neq_one}) net)" ``` huffman@31391 ` 1030` ``` (* FIXME: find a more appropriate type class *) ``` huffman@31390 ` 1031` ``` unfolding trivial_limit_def Rep_net_at_infinity ``` huffman@31390 ` 1032` ``` apply (clarsimp simp add: expand_set_eq) ``` huffman@31390 ` 1033` ``` apply (drule_tac x="scaleR r (sgn 1)" in spec) ``` huffman@31390 ` 1034` ``` apply (simp add: norm_scaleR norm_sgn) ``` huffman@31390 ` 1035` ``` done ``` chaieb@30262 ` 1036` huffman@31346 ` 1037` ```lemma trivial_limit_sequentially: "\ trivial_limit sequentially" ``` huffman@31390 ` 1038` ``` by (auto simp add: trivial_limit_def Rep_net_sequentially) ``` chaieb@30262 ` 1039` chaieb@30262 ` 1040` ```subsection{* Some property holds "sufficiently close" to the limit point. *} ``` chaieb@30262 ` 1041` huffman@31447 ` 1042` ```lemma eventually_at: (* FIXME: this replaces Limits.eventually_at *) ``` huffman@31390 ` 1043` ``` "eventually P (at a) \ (\d>0. \x. 0 < dist x a \ dist x a < d \ P x)" ``` huffman@31447 ` 1044` ```unfolding eventually_at dist_nz by auto ``` huffman@31390 ` 1045` huffman@31390 ` 1046` ```lemma eventually_at_infinity: ``` huffman@31390 ` 1047` ``` "eventually P at_infinity \ (\b. \x. norm x >= b \ P x)" ``` huffman@31390 ` 1048` ```unfolding eventually_def Rep_net_at_infinity by auto ``` huffman@31390 ` 1049` huffman@31346 ` 1050` ```lemma eventually_within: "eventually P (at a within S) \ ``` chaieb@30262 ` 1051` ``` (\d>0. \x\S. 0 < dist x a \ dist x a < d \ P x)" ``` huffman@31393 ` 1052` ```unfolding eventually_within eventually_at dist_nz by auto ``` huffman@31390 ` 1053` huffman@31390 ` 1054` ```lemma eventually_within_le: "eventually P (at a within S) \ ``` huffman@31390 ` 1055` ``` (\d>0. \x\S. 0 < dist x a \ dist x a <= d \ P x)" (is "?lhs = ?rhs") ``` huffman@31390 ` 1056` ```unfolding eventually_within ``` huffman@31390 ` 1057` ```apply safe ``` huffman@31390 ` 1058` ```apply (rule_tac x="d/2" in exI, simp) ``` huffman@31390 ` 1059` ```apply (rule_tac x="d" in exI, simp) ``` huffman@31390 ` 1060` ```done ``` huffman@31390 ` 1061` huffman@31390 ` 1062` ```lemma eventually_happens: "eventually P net ==> trivial_limit net \ (\x. P x)" ``` huffman@31390 ` 1063` ``` unfolding eventually_def trivial_limit_def ``` huffman@31390 ` 1064` ``` using Rep_net_nonempty [of net] by auto ``` chaieb@30262 ` 1065` huffman@31347 ` 1066` ```lemma always_eventually: "(\x. P x) ==> eventually P net" ``` huffman@31390 ` 1067` ``` unfolding eventually_def trivial_limit_def ``` huffman@31390 ` 1068` ``` using Rep_net_nonempty [of net] by auto ``` huffman@31347 ` 1069` huffman@31348 ` 1070` ```lemma trivial_limit_eventually: "trivial_limit net \ eventually P net" ``` huffman@31390 ` 1071` ``` unfolding trivial_limit_def eventually_def by auto ``` huffman@31390 ` 1072` huffman@31390 ` 1073` ```lemma eventually_False: "eventually (\x. False) net \ trivial_limit net" ``` huffman@31390 ` 1074` ``` unfolding trivial_limit_def eventually_def by auto ``` huffman@31348 ` 1075` huffman@31348 ` 1076` ```lemma trivial_limit_eq: "trivial_limit net \ (\P. eventually P net)" ``` huffman@31390 ` 1077` ``` apply (safe elim!: trivial_limit_eventually) ``` huffman@31390 ` 1078` ``` apply (simp add: eventually_False [symmetric]) ``` huffman@31390 ` 1079` ``` done ``` huffman@31348 ` 1080` chaieb@30262 ` 1081` ```text{* Combining theorems for "eventually" *} ``` chaieb@30262 ` 1082` huffman@31390 ` 1083` ```lemma eventually_conjI: ``` huffman@31390 ` 1084` ``` "\eventually (\x. P x) net; eventually (\x. Q x) net\ ``` huffman@31390 ` 1085` ``` \ eventually (\x. P x \ Q x) net" ``` huffman@31393 ` 1086` ```by (rule eventually_conj) ``` chaieb@30262 ` 1087` huffman@31390 ` 1088` ```lemma eventually_rev_mono: ``` huffman@31390 ` 1089` ``` "eventually P net \ (\x. P x \ Q x) \ eventually Q net" ``` huffman@31390 ` 1090` ```using eventually_mono [of P Q] by fast ``` huffman@31390 ` 1091` huffman@31390 ` 1092` ```lemma eventually_and: " eventually (\x. P x \ Q x) net \ eventually P net \ eventually Q net" ``` huffman@31390 ` 1093` ``` by (auto intro!: eventually_conjI elim: eventually_rev_mono) ``` huffman@31390 ` 1094` chaieb@30262 ` 1095` ```lemma eventually_false: "eventually (\x. False) net \ trivial_limit net" ``` huffman@31390 ` 1096` ``` by (auto simp add: eventually_False) ``` huffman@31390 ` 1097` huffman@31390 ` 1098` ```lemma not_eventually: "(\x. \ P x ) \ ~(trivial_limit net) ==> ~(eventually (\x. P x) net)" ``` huffman@31390 ` 1099` ``` by (simp add: eventually_False) ``` huffman@31347 ` 1100` chaieb@30262 ` 1101` ```subsection{* Limits, defined as vacuously true when the limit is trivial. *} ``` chaieb@30262 ` 1102` chaieb@30262 ` 1103` ``` text{* Notation Lim to avoid collition with lim defined in analysis *} ``` huffman@31488 ` 1104` ```definition ``` huffman@31488 ` 1105` ``` Lim :: "'a net \ ('a \ 'b::metric_space) \ 'b" where ``` huffman@31488 ` 1106` ``` "Lim net f = (THE l. (f ---> l) net)" ``` chaieb@30262 ` 1107` huffman@30488 ` 1108` ```lemma Lim: ``` chaieb@30262 ` 1109` ``` "(f ---> l) net \ ``` chaieb@30262 ` 1110` ``` trivial_limit net \ ``` huffman@31348 ` 1111` ``` (\e>0. eventually (\x. dist (f x) l < e) net)" ``` huffman@31488 ` 1112` ``` unfolding tendsto_iff trivial_limit_eq by auto ``` chaieb@30262 ` 1113` chaieb@30262 ` 1114` chaieb@30262 ` 1115` ```text{* Show that they yield usual definitions in the various cases. *} ``` chaieb@30262 ` 1116` chaieb@30262 ` 1117` ```lemma Lim_within_le: "(f ---> l)(at a within S) \ ``` chaieb@30262 ` 1118` ``` (\e>0. \d>0. \x\S. 0 < dist x a \ dist x a <= d \ dist (f x) l < e)" ``` huffman@31488 ` 1119` ``` by (auto simp add: tendsto_iff eventually_within_le) ``` chaieb@30262 ` 1120` chaieb@30262 ` 1121` ```lemma Lim_within: "(f ---> l) (at a within S) \ ``` chaieb@30262 ` 1122` ``` (\e >0. \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" ``` huffman@31488 ` 1123` ``` by (auto simp add: tendsto_iff eventually_within) ``` chaieb@30262 ` 1124` chaieb@30262 ` 1125` ```lemma Lim_at: "(f ---> l) (at a) \ ``` chaieb@30262 ` 1126` ``` (\e >0. \d>0. \x. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" ``` huffman@31488 ` 1127` ``` by (auto simp add: tendsto_iff eventually_at) ``` chaieb@30262 ` 1128` huffman@31342 ` 1129` ```lemma Lim_at_iff_LIM: "(f ---> l) (at a) \ f -- a --> l" ``` huffman@31342 ` 1130` ``` unfolding Lim_at LIM_def by (simp only: zero_less_dist_iff) ``` huffman@31342 ` 1131` chaieb@30262 ` 1132` ```lemma Lim_at_infinity: ``` huffman@31531 ` 1133` ``` "(f ---> l) at_infinity \ (\e>0. \b. \x. norm x >= b \ dist (f x) l < e)" ``` huffman@31488 ` 1134` ``` by (auto simp add: tendsto_iff eventually_at_infinity) ``` chaieb@30262 ` 1135` huffman@30488 ` 1136` ```lemma Lim_sequentially: ``` chaieb@30262 ` 1137` ``` "(S ---> l) sequentially \ ``` chaieb@30262 ` 1138` ``` (\e>0. \N. \n\N. dist (S n) l < e)" ``` huffman@31488 ` 1139` ``` by (auto simp add: tendsto_iff eventually_sequentially) ``` chaieb@30262 ` 1140` huffman@31342 ` 1141` ```lemma Lim_sequentially_iff_LIMSEQ: "(S ---> l) sequentially \ S ----> l" ``` huffman@31342 ` 1142` ``` unfolding Lim_sequentially LIMSEQ_def .. ``` huffman@31342 ` 1143` huffman@31525 ` 1144` ```lemma Lim_eventually: "eventually (\x. f x = l) net \ (f ---> l) net" ``` huffman@31525 ` 1145` ``` by (rule topological_tendstoI, auto elim: eventually_rev_mono) ``` chaieb@30262 ` 1146` chaieb@30262 ` 1147` ```text{* The expected monotonicity property. *} ``` chaieb@30262 ` 1148` huffman@31447 ` 1149` ```lemma Lim_within_empty: "(f ---> l) (net within {})" ``` huffman@31447 ` 1150` ``` unfolding tendsto_def Limits.eventually_within by simp ``` huffman@31447 ` 1151` huffman@31447 ` 1152` ```lemma Lim_within_subset: "(f ---> l) (net within S) \ T \ S \ (f ---> l) (net within T)" ``` huffman@31447 ` 1153` ``` unfolding tendsto_def Limits.eventually_within ``` huffman@31447 ` 1154` ``` by (auto elim!: eventually_elim1) ``` huffman@31447 ` 1155` huffman@31447 ` 1156` ```lemma Lim_Un: assumes "(f ---> l) (net within S)" "(f ---> l) (net within T)" ``` huffman@31447 ` 1157` ``` shows "(f ---> l) (net within (S \ T))" ``` huffman@31447 ` 1158` ``` using assms unfolding tendsto_def Limits.eventually_within ``` huffman@31447 ` 1159` ``` apply clarify ``` huffman@31492 ` 1160` ``` apply (drule spec, drule (1) mp, drule (1) mp) ``` huffman@31492 ` 1161` ``` apply (drule spec, drule (1) mp, drule (1) mp) ``` huffman@31447 ` 1162` ``` apply (auto elim: eventually_elim2) ``` huffman@31447 ` 1163` ``` done ``` chaieb@30262 ` 1164` huffman@30488 ` 1165` ```lemma Lim_Un_univ: ``` huffman@31447 ` 1166` ``` "(f ---> l) (net within S) \ (f ---> l) (net within T) \ S \ T = UNIV ``` huffman@31447 ` 1167` ``` ==> (f ---> l) net" ``` chaieb@30262 ` 1168` ``` by (metis Lim_Un within_UNIV) ``` chaieb@30262 ` 1169` chaieb@30262 ` 1170` ```text{* Interrelations between restricted and unrestricted limits. *} ``` chaieb@30262 ` 1171` huffman@31447 ` 1172` ```lemma Lim_at_within: "(f ---> l) net ==> (f ---> l)(net within S)" ``` huffman@31525 ` 1173` ``` (* FIXME: rename *) ``` huffman@31447 ` 1174` ``` unfolding tendsto_def Limits.eventually_within ``` huffman@31492 ` 1175` ``` apply (clarify, drule spec, drule (1) mp, drule (1) mp) ``` huffman@31447 ` 1176` ``` by (auto elim!: eventually_elim1) ``` chaieb@30262 ` 1177` chaieb@30262 ` 1178` ```lemma Lim_within_open: ``` huffman@31525 ` 1179` ``` fixes f :: "'a::topological_space \ 'b::topological_space" ``` chaieb@30262 ` 1180` ``` assumes"a \ S" "open S" ``` chaieb@30262 ` 1181` ``` shows "(f ---> l)(at a within S) \ (f ---> l)(at a)" (is "?lhs \ ?rhs") ``` chaieb@30262 ` 1182` ```proof ``` chaieb@30262 ` 1183` ``` assume ?lhs ``` huffman@31525 ` 1184` ``` { fix A assume "open A" "l \ A" ``` huffman@31525 ` 1185` ``` with `?lhs` have "eventually (\x. f x \ A) (at a within S)" ``` huffman@31525 ` 1186` ``` by (rule topological_tendstoD) ``` huffman@31525 ` 1187` ``` hence "eventually (\x. x \ S \ f x \ A) (at a)" ``` huffman@31447 ` 1188` ``` unfolding Limits.eventually_within . ``` huffman@31525 ` 1189` ``` then obtain T where "open T" "a \ T" "\x\T. x \ a \ x \ S \ f x \ A" ``` huffman@31492 ` 1190` ``` unfolding eventually_at_topological by fast ``` huffman@31525 ` 1191` ``` hence "open (T \ S)" "a \ T \ S" "\x\(T \ S). x \ a \ f x \ A" ``` huffman@31447 ` 1192` ``` using assms by auto ``` huffman@31525 ` 1193` ``` hence "\T. open T \ a \ T \ (\x\T. x \ a \ f x \ A)" ``` huffman@31447 ` 1194` ``` by fast ``` huffman@31525 ` 1195` ``` hence "eventually (\x. f x \ A) (at a)" ``` huffman@31492 ` 1196` ``` unfolding eventually_at_topological . ``` chaieb@30262 ` 1197` ``` } ``` huffman@31525 ` 1198` ``` thus ?rhs by (rule topological_tendstoI) ``` chaieb@30262 ` 1199` ```next ``` chaieb@30262 ` 1200` ``` assume ?rhs ``` huffman@31447 ` 1201` ``` thus ?lhs by (rule Lim_at_within) ``` chaieb@30262 ` 1202` ```qed ``` chaieb@30262 ` 1203` chaieb@30262 ` 1204` ```text{* Another limit point characterization. *} ``` chaieb@30262 ` 1205` huffman@30488 ` 1206` ```lemma islimpt_sequential: ``` huffman@31488 ` 1207` ``` fixes x :: "'a::metric_space" (* FIXME: generalize to topological_space *) ``` huffman@31488 ` 1208` ``` shows "x islimpt S \ (\f. (\n::nat. f n \ S -{x}) \ (f ---> x) sequentially)" ``` huffman@31488 ` 1209` ``` (is "?lhs = ?rhs") ``` chaieb@30262 ` 1210` ```proof ``` chaieb@30262 ` 1211` ``` assume ?lhs ``` huffman@30488 ` 1212` ``` then obtain f where f:"\y. y>0 \ f y \ S \ f y \ x \ dist (f y) x < y" ``` chaieb@30262 ` 1213` ``` unfolding islimpt_approachable using choice[of "\e y. e>0 \ y\S \ y\x \ dist y x < e"] by auto ``` chaieb@30262 ` 1214` ``` { fix n::nat ``` chaieb@30262 ` 1215` ``` have "f (inverse (real n + 1)) \ S - {x}" using f by auto ``` chaieb@30262 ` 1216` ``` } ``` chaieb@30262 ` 1217` ``` moreover ``` chaieb@30262 ` 1218` ``` { fix e::real assume "e>0" ``` chaieb@30262 ` 1219` ``` hence "\N::nat. inverse (real (N + 1)) < e" using real_arch_inv[of e] apply (auto simp add: Suc_pred') apply(rule_tac x="n - 1" in exI) by auto ``` chaieb@30262 ` 1220` ``` then obtain N::nat where "inverse (real (N + 1)) < e" by auto ``` chaieb@30262 ` 1221` ``` hence "\n\N. inverse (real n + 1) < e" by (auto, metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans real_of_nat_Suc real_of_nat_Suc_gt_zero) ``` chaieb@30262 ` 1222` ``` moreover have "\n\N. dist (f (inverse (real n + 1))) x < (inverse (real n + 1))" using f `e>0` by auto ``` chaieb@30262 ` 1223` ``` ultimately have "\N::nat. \n\N. dist (f (inverse (real n + 1))) x < e" apply(rule_tac x=N in exI) apply auto apply(erule_tac x=n in allE)+ by auto ``` chaieb@30262 ` 1224` ``` } ``` chaieb@30262 ` 1225` ``` hence " ((\n. f (inverse (real n + 1))) ---> x) sequentially" ``` chaieb@30262 ` 1226` ``` unfolding Lim_sequentially using f by auto ``` huffman@30488 ` 1227` ``` ultimately show ?rhs apply (rule_tac x="(\n::nat. f (inverse (real n + 1)))" in exI) by auto ``` chaieb@30262 ` 1228` ```next ``` chaieb@30262 ` 1229` ``` assume ?rhs ``` huffman@31345 ` 1230` ``` then obtain f::"nat\'a" where f:"(\n. f n \ S - {x})" "(\e>0. \N. \n\N. dist (f n) x < e)" unfolding Lim_sequentially by auto ``` chaieb@30262 ` 1231` ``` { fix e::real assume "e>0" ``` chaieb@30262 ` 1232` ``` then obtain N where "dist (f N) x < e" using f(2) by auto ``` chaieb@30262 ` 1233` ``` moreover have "f N\S" "f N \ x" using f(1) by auto ``` chaieb@30262 ` 1234` ``` ultimately have "\x'\S. x' \ x \ dist x' x < e" by auto ``` chaieb@30262 ` 1235` ``` } ``` chaieb@30262 ` 1236` ``` thus ?lhs unfolding islimpt_approachable by auto ``` chaieb@30262 ` 1237` ```qed ``` chaieb@30262 ` 1238` chaieb@30262 ` 1239` ```text{* Basic arithmetical combining theorems for limits. *} ``` chaieb@30262 ` 1240` huffman@30582 ` 1241` ```lemma Lim_linear: fixes f :: "('a \ real^'n::finite)" and h :: "(real^'n \ real^'m::finite)" ``` huffman@30488 ` 1242` ``` assumes "(f ---> l) net" "linear h" ``` chaieb@30262 ` 1243` ``` shows "((\x. h (f x)) ---> h l) net" ``` huffman@31529 ` 1244` ```using `linear h` `(f ---> l) net` ``` huffman@31529 ` 1245` ```unfolding linear_conv_bounded_linear ``` huffman@31529 ` 1246` ```by (rule bounded_linear.tendsto) ``` chaieb@30262 ` 1247` huffman@31558 ` 1248` ```lemma Lim_ident_at: "((\x. x) ---> a) (at a)" ``` huffman@31558 ` 1249` ``` unfolding tendsto_def Limits.eventually_at_topological by fast ``` huffman@31558 ` 1250` chaieb@30262 ` 1251` ```lemma Lim_const: "((\x. a) ---> a) net" ``` huffman@31525 ` 1252` ``` by (rule tendsto_const) ``` chaieb@30262 ` 1253` huffman@31343 ` 1254` ```lemma Lim_cmul: ``` huffman@31343 ` 1255` ``` fixes f :: "'a \ real ^ 'n::finite" ``` huffman@31343 ` 1256` ``` shows "(f ---> l) net ==> ((\x. c *s f x) ---> c *s l) net" ``` chaieb@30262 ` 1257` ``` apply (rule Lim_linear[where f = f]) ``` chaieb@30262 ` 1258` ``` apply simp ``` chaieb@30262 ` 1259` ``` apply (rule linear_compose_cmul) ``` chaieb@30262 ` 1260` ``` apply (rule linear_id[unfolded id_def]) ``` chaieb@30262 ` 1261` ``` done ``` chaieb@30262 ` 1262` huffman@31343 ` 1263` ```lemma Lim_neg: ``` huffman@31343 ` 1264` ``` fixes f :: "'a \ 'b::real_normed_vector" ``` huffman@31343 ` 1265` ``` shows "(f ---> l) net ==> ((\x. -(f x)) ---> -l) net" ``` huffman@31525 ` 1266` ``` by (rule tendsto_minus) ``` chaieb@30262 ` 1267` huffman@31343 ` 1268` ```lemma Lim_add: fixes f :: "'a \ 'b::real_normed_vector" shows ``` chaieb@30262 ` 1269` ``` "(f ---> l) net \ (g ---> m) net \ ((\x. f(x) + g(x)) ---> l + m) net" ``` huffman@31525 ` 1270` ``` by (rule tendsto_add) ``` chaieb@30262 ` 1271` huffman@31343 ` 1272` ```lemma Lim_sub: ``` huffman@31343 ` 1273` ``` fixes f :: "'a \ 'b::real_normed_vector" ``` huffman@31343 ` 1274` ``` shows "(f ---> l) net \ (g ---> m) net \ ((\x. f(x) - g(x)) ---> l - m) net" ``` huffman@31525 ` 1275` ``` by (rule tendsto_diff) ``` chaieb@30262 ` 1276` huffman@31558 ` 1277` ```lemma dist_triangle3: (* TODO: move *) ``` huffman@31558 ` 1278` ``` fixes x y :: "'a::metric_space" ``` huffman@31558 ` 1279` ``` shows "dist x y \ dist a x + dist a y" ``` huffman@31558 ` 1280` ```using dist_triangle2 [of x y a] ``` huffman@31558 ` 1281` ```by (simp add: dist_commute) ``` huffman@31558 ` 1282` huffman@31558 ` 1283` ```lemma tendsto_dist: (* TODO: move *) ``` huffman@31558 ` 1284` ``` assumes f: "(f ---> l) net" and g: "(g ---> m) net" ``` huffman@31558 ` 1285` ``` shows "((\x. dist (f x) (g x)) ---> dist l m) net" ``` huffman@31558 ` 1286` ```proof (rule tendstoI) ``` huffman@31558 ` 1287` ``` fix e :: real assume "0 < e" ``` huffman@31558 ` 1288` ``` hence e2: "0 < e/2" by simp ``` huffman@31558 ` 1289` ``` from tendstoD [OF f e2] tendstoD [OF g e2] ``` huffman@31558 ` 1290` ``` show "eventually (\x. dist (dist (f x) (g x)) (dist l m) < e) net" ``` huffman@31558 ` 1291` ``` proof (rule eventually_elim2) ``` huffman@31558 ` 1292` ``` fix x assume x: "dist (f x) l < e/2" "dist (g x) m < e/2" ``` huffman@31558 ` 1293` ``` have "dist (f x) (g x) - dist l m \ dist (f x) l + dist (g x) m" ``` huffman@31558 ` 1294` ``` using dist_triangle2 [of "f x" "g x" "l"] ``` huffman@31558 ` 1295` ``` using dist_triangle2 [of "g x" "l" "m"] ``` huffman@31558 ` 1296` ``` by arith ``` huffman@31558 ` 1297` ``` moreover ``` huffman@31558 ` 1298` ``` have "dist l m - dist (f x) (g x) \ dist (f x) l + dist (g x) m" ``` huffman@31558 ` 1299` ``` using dist_triangle3 [of "l" "m" "f x"] ``` huffman@31558 ` 1300` ``` using dist_triangle [of "f x" "m" "g x"] ``` huffman@31558 ` 1301` ``` by arith ``` huffman@31558 ` 1302` ``` ultimately ``` huffman@31558 ` 1303` ``` have "dist (dist (f x) (g x)) (dist l m) \ dist (f x) l + dist (g x) m" ``` huffman@31558 ` 1304` ``` unfolding dist_norm real_norm_def by arith ``` huffman@31558 ` 1305` ``` with x show "dist (dist (f x) (g x)) (dist l m) < e" ``` huffman@31558 ` 1306` ``` by arith ``` huffman@31558 ` 1307` ``` qed ``` huffman@31558 ` 1308` ```qed ``` huffman@31558 ` 1309` huffman@31343 ` 1310` ```lemma Lim_null: ``` huffman@31343 ` 1311` ``` fixes f :: "'a \ 'b::real_normed_vector" ``` huffman@31343 ` 1312` ``` shows "(f ---> l) net \ ((\x. f(x) - l) ---> 0) net" by (simp add: Lim dist_norm) ``` huffman@31343 ` 1313` huffman@31343 ` 1314` ```lemma Lim_null_norm: ``` huffman@31343 ` 1315` ``` fixes f :: "'a \ 'b::real_normed_vector" ``` huffman@31558 ` 1316` ``` shows "(f ---> 0) net \ ((\x. norm(f x)) ---> 0) net" ``` huffman@31558 ` 1317` ``` by (simp add: Lim dist_norm) ``` chaieb@30262 ` 1318` huffman@30488 ` 1319` ```lemma Lim_null_comparison: ``` huffman@31343 ` 1320` ``` fixes f :: "'a \ 'b::real_normed_vector" ``` huffman@31558 ` 1321` ``` assumes "eventually (\x. norm (f x) \ g x) net" "(g ---> 0) net" ``` huffman@30488 ` 1322` ``` shows "(f ---> 0) net" ``` huffman@31488 ` 1323` ```proof(simp add: tendsto_iff, rule+) ``` chaieb@30262 ` 1324` ``` fix e::real assume "0 g x" "dist (g x) 0 < e" ``` huffman@31558 ` 1327` ``` hence "dist (f x) 0 < e" by (simp add: dist_norm) ``` chaieb@30262 ` 1328` ``` } ``` huffman@30488 ` 1329` ``` thus "eventually (\x. dist (f x) 0 < e) net" ``` huffman@31558 ` 1330` ``` using eventually_and[of "\x. norm(f x) <= g x" "\x. dist (g x) 0 < e" net] ``` huffman@31558 ` 1331` ``` using eventually_mono[of "(\x. norm (f x) \ g x \ dist (g x) 0 < e)" "(\x. dist (f x) 0 < e)" net] ``` huffman@31488 ` 1332` ``` using assms `e>0` unfolding tendsto_iff by auto ``` chaieb@30262 ` 1333` ```qed ``` chaieb@30262 ` 1334` huffman@31558 ` 1335` ```lemma Lim_component: ``` huffman@31558 ` 1336` ``` fixes f :: "'a \ 'b::metric_space ^ 'n::finite" ``` huffman@31558 ` 1337` ``` shows "(f ---> l) net \ ((\a. f a \$i) ---> l\$i) net" ``` huffman@31488 ` 1338` ``` unfolding tendsto_iff ``` huffman@31558 ` 1339` ``` apply (clarify) ``` huffman@31558 ` 1340` ``` apply (drule spec, drule (1) mp) ``` huffman@31558 ` 1341` ``` apply (erule eventually_elim1) ``` huffman@31558 ` 1342` ``` apply (erule le_less_trans [OF dist_nth_le]) ``` huffman@31558 ` 1343` ``` done ``` chaieb@30262 ` 1344` huffman@30488 ` 1345` ```lemma Lim_transform_bound: ``` huffman@31343 ` 1346` ``` fixes f :: "'a \ 'b::real_normed_vector" ``` huffman@31343 ` 1347` ``` fixes g :: "'a \ 'c::real_normed_vector" ``` chaieb@30262 ` 1348` ``` assumes "eventually (\n. norm(f n) <= norm(g n)) net" "(g ---> 0) net" ``` chaieb@30262 ` 1349` ``` shows "(f ---> 0) net" ``` huffman@31525 ` 1350` ```proof (rule tendstoI) ``` chaieb@30262 ` 1351` ``` fix e::real assume "e>0" ``` chaieb@30262 ` 1352` ``` { fix x ``` chaieb@30262 ` 1353` ``` assume "norm (f x) \ norm (g x)" "dist (g x) 0 < e" ``` huffman@31343 ` 1354` ``` hence "dist (f x) 0 < e" by (simp add: dist_norm)} ``` chaieb@30262 ` 1355` ``` thus "eventually (\x. dist (f x) 0 < e) net" ``` chaieb@30262 ` 1356` ``` using eventually_and[of "\x. norm (f x) \ norm (g x)" "\x. dist (g x) 0 < e" net] ``` chaieb@30262 ` 1357` ``` using eventually_mono[of "\x. norm (f x) \ norm (g x) \ dist (g x) 0 < e" "\x. dist (f x) 0 < e" net] ``` huffman@31488 ` 1358` ``` using assms `e>0` unfolding tendsto_iff by blast ``` chaieb@30262 ` 1359` ```qed ``` chaieb@30262 ` 1360` chaieb@30262 ` 1361` ```text{* Deducing things about the limit from the elements. *} ``` chaieb@30262 ` 1362` chaieb@30262 ` 1363` ```lemma Lim_in_closed_set: ``` huffman@31525 ` 1364` ``` assumes "closed S" "eventually (\x. f(x) \ S) net" "\(trivial_limit net)" "(f ---> l) net" ``` chaieb@30262 ` 1365` ``` shows "l \ S" ``` huffman@31347 ` 1366` ```proof (rule ccontr) ``` huffman@31347 ` 1367` ``` assume "l \ S" ``` huffman@31525 ` 1368` ``` with `closed S` have "open (- S)" "l \ - S" ``` huffman@31525 ` 1369` ``` by (simp_all add: open_Compl) ``` huffman@31525 ` 1370` ``` with assms(4) have "eventually (\x. f x \ - S) net" ``` huffman@31525 ` 1371` ``` by (rule topological_tendstoD) ``` huffman@31525 ` 1372` ``` with assms(2) have "eventually (\x. False) net" ``` huffman@31525 ` 1373` ``` by (rule eventually_elim2) simp ``` huffman@31525 ` 1374` ``` with assms(3) show "False" ``` huffman@31525 ` 1375` ``` by (simp add: eventually_False) ``` chaieb@30262 ` 1376` ```qed ``` chaieb@30262 ` 1377` chaieb@30262 ` 1378` ```text{* Need to prove closed(cball(x,e)) before deducing this as a corollary. *} ``` chaieb@30262 ` 1379` huffman@31533 ` 1380` ```lemma Lim_dist_ubound: ``` huffman@31533 ` 1381` ``` assumes "\(trivial_limit net)" "(f ---> l) net" "eventually (\x. dist a (f x) <= e) net" ``` huffman@31533 ` 1382` ``` shows "dist a l <= e" ``` huffman@31533 ` 1383` ```proof (rule ccontr) ``` huffman@31533 ` 1384` ``` assume "\ dist a l \ e" ``` huffman@31533 ` 1385` ``` then have "0 < dist a l - e" by simp ``` huffman@31533 ` 1386` ``` with assms(2) have "eventually (\x. dist (f x) l < dist a l - e) net" ``` huffman@31533 ` 1387` ``` by (rule tendstoD) ``` huffman@31533 ` 1388` ``` with assms(3) have "eventually (\x. dist a (f x) \ e \ dist (f x) l < dist a l - e) net" ``` huffman@31533 ` 1389` ``` by (rule eventually_conjI) ``` huffman@31533 ` 1390` ``` then obtain w where "dist a (f w) \ e" "dist (f w) l < dist a l - e" ``` huffman@31533 ` 1391` ``` using assms(1) eventually_happens by auto ``` huffman@31533 ` 1392` ``` hence "dist a (f w) + dist (f w) l < e + (dist a l - e)" ``` huffman@31533 ` 1393` ``` by (rule add_le_less_mono) ``` huffman@31533 ` 1394` ``` hence "dist a (f w) + dist (f w) l < dist a l" ``` huffman@31533 ` 1395` ``` by simp ``` huffman@31533 ` 1396` ``` also have "\ \ dist a (f w) + dist (f w) l" ``` huffman@31533 ` 1397` ``` by (rule dist_triangle) ``` huffman@31533 ` 1398` ``` finally show False by simp ``` huffman@31533 ` 1399` ```qed ``` huffman@31533 ` 1400` huffman@30488 ` 1401` ```lemma Lim_norm_ubound: ``` huffman@31343 ` 1402` ``` fixes f :: "'a \ 'b::real_normed_vector" ``` chaieb@30262 ` 1403` ``` assumes "\(trivial_limit net)" "(f ---> l) net" "eventually (\x. norm(f x) <= e) net" ``` chaieb@30262 ` 1404` ``` shows "norm(l) <= e" ``` huffman@31347 ` 1405` ```proof (rule ccontr) ``` huffman@31347 ` 1406` ``` assume "\ norm l \ e" ``` huffman@31347 ` 1407` ``` then have "0 < norm l - e" by simp ``` huffman@31347 ` 1408` ``` with assms(2) have "eventually (\x. dist (f x) l < norm l - e) net" ``` huffman@31347 ` 1409` ``` by (rule tendstoD) ``` huffman@31347 ` 1410` ``` with assms(3) have "eventually (\x. norm (f x) \ e \ dist (f x) l < norm l - e) net" ``` huffman@31347 ` 1411` ``` by (rule eventually_conjI) ``` huffman@31347 ` 1412` ``` then obtain w where "norm (f w) \ e" "dist (f w) l < norm l - e" ``` huffman@31347 ` 1413` ``` using assms(1) eventually_happens by auto ``` huffman@31347 ` 1414` ``` hence "norm (f w - l) < norm l - e" "norm (f w) \ e" by (simp_all add: dist_norm) ``` huffman@31347 ` 1415` ``` hence "norm (f w - l) + norm (f w) < norm l" by simp ``` huffman@31347 ` 1416` ``` hence "norm (f w - l - f w) < norm l" by (rule le_less_trans [OF norm_triangle_ineq4]) ``` huffman@31347 ` 1417` ``` thus False using `\ norm l \ e` by simp ``` chaieb@30262 ` 1418` ```qed ``` chaieb@30262 ` 1419` chaieb@30262 ` 1420` ```lemma Lim_norm_lbound: ``` huffman@31343 ` 1421` ``` fixes f :: "'a \ 'b::real_normed_vector" ``` chaieb@30262 ` 1422` ``` assumes "\ (trivial_limit net)" "(f ---> l) net" "eventually (\x. e <= norm(f x)) net" ``` chaieb@30262 ` 1423` ``` shows "e \ norm l" ``` huffman@31347 ` 1424` ```proof (rule ccontr) ``` huffman@31347 ` 1425` ``` assume "\ e \ norm l" ``` huffman@31347 ` 1426` ``` then have "0 < e - norm l" by simp ``` huffman@31347 ` 1427` ``` with assms(2) have "eventually (\x. dist (f x) l < e - norm l) net" ``` huffman@31347 ` 1428` ``` by (rule tendstoD) ``` huffman@31347 ` 1429` ``` with assms(3) have "eventually (\x. e \ norm (f x) \ dist (f x) l < e - norm l) net" ``` huffman@31347 ` 1430` ``` by (rule eventually_conjI) ``` huffman@31347 ` 1431` ``` then obtain w where "e \ norm (f w)" "dist (f w) l < e - norm l" ``` huffman@31347 ` 1432` ``` using assms(1) eventually_happens by auto ``` huffman@31347 ` 1433` ``` hence "norm (f w - l) + norm l < e" "e \ norm (f w)" by (simp_all add: dist_norm) ``` huffman@31347 ` 1434` ``` hence "norm (f w - l) + norm l < norm (f w)" by (rule less_le_trans) ``` huffman@31347 ` 1435` ``` hence "norm (f w - l + l) < norm (f w)" by (rule le_less_trans [OF norm_triangle_ineq]) ``` huffman@31347 ` 1436` ``` thus False by simp ``` chaieb@30262 ` 1437` ```qed ``` chaieb@30262 ` 1438` chaieb@30262 ` 1439` ```text{* Uniqueness of the limit, when nontrivial. *} ``` chaieb@30262 ` 1440` chaieb@30262 ` 1441` ```lemma Lim_unique: ``` huffman@31397 ` 1442` ``` fixes f :: "'a \ 'b::metric_space" ``` huffman@31397 ` 1443` ``` assumes "\ trivial_limit net" "(f ---> l) net" "(f ---> l') net" ``` chaieb@30262 ` 1444` ``` shows "l = l'" ``` huffman@31397 ` 1445` ```proof (rule ccontr) ``` huffman@31397 ` 1446` ``` let ?d = "dist l l' / 2" ``` huffman@31397 ` 1447` ``` assume "l \ l'" ``` huffman@31397 ` 1448` ``` then have "0 < ?d" by (simp add: dist_nz) ``` huffman@31397 ` 1449` ``` have "eventually (\x. dist (f x) l < ?d) net" ``` huffman@31397 ` 1450` ``` using `(f ---> l) net` `0 < ?d` by (rule tendstoD) ``` huffman@31397 ` 1451` ``` moreover ``` huffman@31397 ` 1452` ``` have "eventually (\x. dist (f x) l' < ?d) net" ``` huffman@31397 ` 1453` ``` using `(f ---> l') net` `0 < ?d` by (rule tendstoD) ``` huffman@31397 ` 1454` ``` ultimately ``` huffman@31397 ` 1455` ``` have "eventually (\x. False) net" ``` huffman@31397 ` 1456` ``` proof (rule eventually_elim2) ``` huffman@31397 ` 1457` ``` fix x ``` huffman@31397 ` 1458` ``` assume *: "dist (f x) l < ?d" "dist (f x) l' < ?d" ``` huffman@31397 ` 1459` ``` have "dist l l' \ dist (f x) l + dist (f x) l'" ``` huffman@31397 ` 1460` ``` by (rule dist_triangle_alt) ``` huffman@31397 ` 1461` ``` also from * have "\ < ?d + ?d" ``` huffman@31397 ` 1462` ``` by (rule add_strict_mono) ``` huffman@31397 ` 1463` ``` also have "\ = dist l l'" by simp ``` huffman@31397 ` 1464` ``` finally show "False" by simp ``` huffman@31397 ` 1465` ``` qed ``` huffman@31397 ` 1466` ``` with `\ trivial_limit net` show "False" ``` huffman@31397 ` 1467` ``` by (simp add: eventually_False) ``` chaieb@30262 ` 1468` ```qed ``` chaieb@30262 ` 1469` huffman@30488 ` 1470` ```lemma tendsto_Lim: ``` huffman@31397 ` 1471` ``` fixes f :: "'a \ 'b::metric_space" ``` huffman@31343 ` 1472` ``` shows "~(trivial_limit net) \ (f ---> l) net ==> Lim net f = l" ``` chaieb@30262 ` 1473` ``` unfolding Lim_def using Lim_unique[of net f] by auto ``` chaieb@30262 ` 1474` huffman@31529 ` 1475` ```text{* Limit under bilinear function *} ``` chaieb@30262 ` 1476` huffman@30488 ` 1477` ```lemma Lim_bilinear: ``` huffman@30582 ` 1478` ``` fixes net :: "'a net" and h:: "real ^'m::finite \ real ^'n::finite \ real ^'p::finite" ``` chaieb@30262 ` 1479` ``` assumes "(f ---> l) net" and "(g ---> m) net" and "bilinear h" ``` chaieb@30262 ` 1480` ``` shows "((\x. h (f x) (g x)) ---> (h l m)) net" ``` huffman@31529 ` 1481` ```using `bilinear h` `(f ---> l) net` `(g ---> m) net` ``` huffman@31529 ` 1482` ```unfolding bilinear_conv_bounded_bilinear ``` huffman@31529 ` 1483` ```by (rule bounded_bilinear.tendsto) ``` chaieb@30262 ` 1484` chaieb@30262 ` 1485` ```text{* These are special for limits out of the same vector space. *} ``` chaieb@30262 ` 1486` huffman@31488 ` 1487` ```lemma Lim_within_id: "(id ---> a) (at a within s)" ``` huffman@31488 ` 1488` ``` unfolding tendsto_def Limits.eventually_within eventually_at_topological ``` huffman@31488 ` 1489` ``` by auto ``` huffman@31488 ` 1490` chaieb@30262 ` 1491` ```lemma Lim_at_id: "(id ---> a) (at a)" ``` chaieb@30262 ` 1492` ```apply (subst within_UNIV[symmetric]) by (simp add: Lim_within_id) ``` chaieb@30262 ` 1493` huffman@31346 ` 1494` ```lemma Lim_at_zero: ``` huffman@31391 ` 1495` ``` fixes a :: "'a::real_normed_vector" ``` huffman@31526 ` 1496` ``` fixes l :: "'b::topological_space" ``` huffman@31346 ` 1497` ``` shows "(f ---> l) (at a) \ ((\x. f(a + x)) ---> l) (at 0)" (is "?lhs = ?rhs") ``` chaieb@30262 ` 1498` ```proof ``` chaieb@30262 ` 1499` ``` assume "?lhs" ``` huffman@31526 ` 1500` ``` { fix S assume "open S" "l \ S" ``` huffman@31526 ` 1501` ``` with `?lhs` have "eventually (\x. f x \ S) (at a)" ``` huffman@31526 ` 1502` ``` by (rule topological_tendstoD) ``` huffman@31526 ` 1503` ``` then obtain d where d: "d>0" "\x. x \ a \ dist x a < d \ f x \ S" ``` huffman@31526 ` 1504` ``` unfolding Limits.eventually_at by fast ``` huffman@31526 ` 1505` ``` { fix x::"'a" assume "x \ 0 \ dist x 0 < d" ``` huffman@31526 ` 1506` ``` hence "f (a + x) \ S" using d ``` huffman@31526 ` 1507` ``` apply(erule_tac x="x+a" in allE) ``` huffman@31526 ` 1508` ``` by(auto simp add: comm_monoid_add.mult_commute dist_norm dist_commute) ``` chaieb@30262 ` 1509` ``` } ``` huffman@31526 ` 1510` ``` hence "\d>0. \x. x \ 0 \ dist x 0 < d \ f (a + x) \ S" ``` huffman@31526 ` 1511` ``` using d(1) by auto ``` huffman@31526 ` 1512` ``` hence "eventually (\x. f (a + x) \ S) (at 0)" ``` huffman@31526 ` 1513` ``` unfolding Limits.eventually_at . ``` chaieb@30262 ` 1514` ``` } ``` huffman@31526 ` 1515` ``` thus "?rhs" by (rule topological_tendstoI) ``` chaieb@30262 ` 1516` ```next ``` chaieb@30262 ` 1517` ``` assume "?rhs" ``` huffman@31526 ` 1518` ``` { fix S assume "open S" "l \ S" ``` huffman@31526 ` 1519` ``` with `?rhs` have "eventually (\x. f (a + x) \ S) (at 0)" ``` huffman@31526 ` 1520` ``` by (rule topological_tendstoD) ``` huffman@31526 ` 1521` ``` then obtain d where d: "d>0" "\x. x \ 0 \ dist x 0 < d \ f (a + x) \ S" ``` huffman@31526 ` 1522` ``` unfolding Limits.eventually_at by fast ``` huffman@31526 ` 1523` ``` { fix x::"'a" assume "x \ a \ dist x a < d" ``` huffman@31526 ` 1524` ``` hence "f x \ S" using d apply(erule_tac x="x-a" in allE) ``` huffman@31289 ` 1525` ``` by(auto simp add: comm_monoid_add.mult_commute dist_norm dist_commute) ``` chaieb@30262 ` 1526` ``` } ``` huffman@31526 ` 1527` ``` hence "\d>0. \x. x \ a \ dist x a < d \ f x \ S" using d(1) by auto ``` huffman@31526 ` 1528` ``` hence "eventually (\x. f x \ S) (at a)" unfolding Limits.eventually_at . ``` chaieb@30262 ` 1529` ``` } ``` huffman@31526 ` 1530` ``` thus "?lhs" by (rule topological_tendstoI) ``` chaieb@30262 ` 1531` ```qed ``` chaieb@30262 ` 1532` chaieb@30262 ` 1533` ```text{* It's also sometimes useful to extract the limit point from the net. *} ``` chaieb@30262 ` 1534` huffman@31390 ` 1535` ```definition ``` huffman@31390 ` 1536` ``` netlimit :: "'a::metric_space net \ 'a" where ``` huffman@31448 ` 1537` ``` "netlimit net = (SOME a. \r>0. eventually (\x. dist x a < r) net)" ``` huffman@31390 ` 1538` huffman@31390 ` 1539` ```lemma netlimit_within: ``` huffman@31390 ` 1540` ``` assumes "\ trivial_limit (at a within S)" ``` huffman@31390 ` 1541` ``` shows "netlimit (at a within S) = a" ``` huffman@31390 ` 1542` ```using assms ``` huffman@31390 ` 1543` ```apply (simp add: trivial_limit_within) ``` huffman@31448 ` 1544` ```apply (simp add: netlimit_def eventually_within zero_less_dist_iff) ``` huffman@31390 ` 1545` ```apply (rule some_equality, fast) ``` huffman@31390 ` 1546` ```apply (rename_tac b) ``` huffman@31390 ` 1547` ```apply (rule ccontr) ``` huffman@31390 ` 1548` ```apply (drule_tac x="dist b a / 2" in spec, drule mp, simp add: dist_nz) ``` huffman@31390 ` 1549` ```apply (clarify, rename_tac r) ``` huffman@31390 ` 1550` ```apply (simp only: islimpt_approachable) ``` huffman@31390 ` 1551` ```apply (drule_tac x="min r (dist b a / 2)" in spec, drule mp, simp add: dist_nz) ``` huffman@31390 ` 1552` ```apply (clarify) ``` huffman@31447 ` 1553` ```apply (drule_tac x=x' in bspec, simp) ``` huffman@31447 ` 1554` ```apply (drule mp, simp) ``` huffman@31390 ` 1555` ```apply (subgoal_tac "dist b a < dist b a / 2 + dist b a / 2", simp) ``` huffman@31390 ` 1556` ```apply (rule le_less_trans [OF dist_triangle3]) ``` huffman@31390 ` 1557` ```apply (erule add_strict_mono) ``` huffman@31390 ` 1558` ```apply simp ``` huffman@31390 ` 1559` ```done ``` chaieb@30262 ` 1560` huffman@31391 ` 1561` ```lemma netlimit_at: ``` huffman@31391 ` 1562` ``` fixes a :: "'a::perfect_space" ``` huffman@31391 ` 1563` ``` shows "netlimit (at a) = a" ``` chaieb@30262 ` 1564` ``` apply (subst within_UNIV[symmetric]) ``` chaieb@30262 ` 1565` ``` using netlimit_within[of a UNIV] ``` chaieb@30262 ` 1566` ``` by (simp add: trivial_limit_at within_UNIV) ``` chaieb@30262 ` 1567` chaieb@30262 ` 1568` ```text{* Transformation of limit. *} ``` chaieb@30262 ` 1569` huffman@31343 ` 1570` ```lemma Lim_transform: ``` huffman@31343 ` 1571` ``` fixes f g :: "'a::type \ 'b::real_normed_vector" ``` huffman@31343 ` 1572` ``` assumes "((\x. f x - g x) ---> 0) net" "(f ---> l) net" ``` chaieb@30262 ` 1573` ``` shows "(g ---> l) net" ``` chaieb@30262 ` 1574` ```proof- ``` chaieb@30262 ` 1575` ``` from assms have "((\x. f x - g x - f x) ---> 0 - l) net" using Lim_sub[of "\x. f x - g x" 0 net f l] by auto ``` chaieb@30262 ` 1576` ``` thus "?thesis" using Lim_neg [of "\ x. - g x" "-l" net] by auto ``` chaieb@30262 ` 1577` ```qed ``` chaieb@30262 ` 1578` huffman@31343 ` 1579` ```lemma Lim_transform_eventually: ``` huffman@31526 ` 1580` ``` "eventually (\x. f x = g x) net \ (f ---> l) net ==> (g ---> l) net" ``` huffman@31526 ` 1581` ``` apply (rule topological_tendstoI) ``` huffman@31526 ` 1582` ``` apply (drule (2) topological_tendstoD) ``` huffman@31395 ` 1583` ``` apply (erule (1) eventually_elim2, simp) ``` huffman@31395 ` 1584` ``` done ``` chaieb@30262 ` 1585` huffman@30488 ` 1586` ```lemma Lim_transform_within: ``` huffman@31488 ` 1587` ``` fixes l :: "'b::metric_space" (* TODO: generalize *) ``` chaieb@30262 ` 1588` ``` assumes "0 < d" "(\x'\S. 0 < dist x' x \ dist x' x < d \ f x' = g x')" ``` chaieb@30262 ` 1589` ``` "(f ---> l) (at x within S)" ``` chaieb@30262 ` 1590` ``` shows "(g ---> l) (at x within S)" ``` huffman@31395 ` 1591` ``` using assms(1,3) unfolding Lim_within ``` huffman@31395 ` 1592` ``` apply - ``` huffman@31395 ` 1593` ``` apply (clarify, rename_tac e) ``` huffman@31395 ` 1594` ``` apply (drule_tac x=e in spec, clarsimp, rename_tac r) ``` huffman@31395 ` 1595` ``` apply (rule_tac x="min d r" in exI, clarsimp, rename_tac y) ``` huffman@31395 ` 1596` ``` apply (drule_tac x=y in bspec, assumption, clarsimp) ``` huffman@31395 ` 1597` ``` apply (simp add: assms(2)) ``` huffman@31395 ` 1598` ``` done ``` chaieb@30262 ` 1599` huffman@31343 ` 1600` ```lemma Lim_transform_at: ``` huffman@31488 ` 1601` ``` fixes l :: "'b::metric_space" (* TODO: generalize *) ``` huffman@31343 ` 1602` ``` shows "0 < d \ (\x'. 0 < dist x' x \ dist x' x < d \ f x' = g x') \ ``` chaieb@30262 ` 1603` ``` (f ---> l) (at x) ==> (g ---> l) (at x)" ``` chaieb@30262 ` 1604` ``` apply (subst within_UNIV[symmetric]) ``` chaieb@30262 ` 1605` ``` using Lim_transform_within[of d UNIV x f g l] ``` chaieb@30262 ` 1606` ``` by (auto simp add: within_UNIV) ``` chaieb@30262 ` 1607` chaieb@30262 ` 1608` ```text{* Common case assuming being away from some crucial point like 0. *} ``` chaieb@30262 ` 1609` huffman@30488 ` 1610` ```lemma Lim_transform_away_within: ``` huffman@31447 ` 1611` ``` fixes a b :: "'a::metric_space" ``` huffman@31488 ` 1612` ``` fixes l :: "'b::metric_space" (* TODO: generalize *) ``` huffman@30488 ` 1613` ``` assumes "a\b" "\x\ S. x \ a \ x \ b \ f x = g x" ``` chaieb@30262 ` 1614` ``` and "(f ---> l) (at a within S)" ``` chaieb@30262 ` 1615` ``` shows "(g ---> l) (at a within S)" ``` chaieb@30262 ` 1616` ```proof- ``` huffman@30488 ` 1617` ``` have "\x'\S. 0 < dist x' a \ dist x' a < dist a b \ f x' = g x'" using assms(2) ``` huffman@31285 ` 1618` ``` apply auto apply(erule_tac x=x' in ballE) by (auto simp add: dist_commute) ``` chaieb@30262 ` 1619` ``` thus ?thesis using Lim_transform_within[of "dist a b" S a f g l] using assms(1,3) unfolding dist_nz by auto ``` chaieb@30262 ` 1620` ```qed ``` chaieb@30262 ` 1621` huffman@30488 ` 1622` ```lemma Lim_transform_away_at: ``` huffman@31447 ` 1623` ``` fixes a b :: "'a::metric_space" ``` huffman@31488 ` 1624` ``` fixes l :: "'b::metric_space" (* TODO: generalize *) ``` huffman@30488 ` 1625` ``` assumes ab: "a\b" and fg: "\x. x \ a \ x \ b \ f x = g x" ``` chaieb@30262 ` 1626` ``` and fl: "(f ---> l) (at a)" ``` chaieb@30262 ` 1627` ``` shows "(g ---> l) (at a)" ``` huffman@30488 ` 1628` ``` using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl ``` chaieb@30262 ` 1629` ``` by (auto simp add: within_UNIV) ``` chaieb@30262 ` 1630` chaieb@30262 ` 1631` ```text{* Alternatively, within an open set. *} ``` chaieb@30262 ` 1632` huffman@30488 ` 1633` ```lemma Lim_transform_within_open: ``` huffman@31447 ` 1634` ``` fixes a :: "'a::metric_space" ``` huffman@31488 ` 1635` ``` fixes l :: "'b::metric_space" (* TODO: generalize *) ``` chaieb@30262 ` 1636` ``` assumes "open S" "a \ S" "\x\S. x \ a \ f x = g x" "(f ---> l) (at a)" ``` chaieb@30262 ` 1637` ``` shows "(g ---> l) (at a)" ``` chaieb@30262 ` 1638` ```proof- ``` chaieb@30262 ` 1639` ``` from assms(1,2) obtain e::real where "e>0" and e:"ball a e \ S" unfolding open_contains_ball by auto ``` huffman@30488 ` 1640` ``` hence "\x'. 0 < dist x' a \ dist x' a < e \ f x' = g x'" using assms(3) ``` huffman@31285 ` 1641` ``` unfolding ball_def subset_eq apply auto apply(erule_tac x=x' in allE) apply(erule_tac x=x' in ballE) by(auto simp add: dist_commute) ``` chaieb@30262 ` 1642` ``` thus ?thesis using Lim_transform_at[of e a f g l] `e>0` assms(4) by auto ``` chaieb@30262 ` 1643` ```qed ``` chaieb@30262 ` 1644` chaieb@30262 ` 1645` ```text{* A congruence rule allowing us to transform limits assuming not at point. *} ``` chaieb@30262 ` 1646` huffman@31395 ` 1647` ```(* FIXME: Only one congruence rule for tendsto can be used at a time! *) ``` huffman@31395 ` 1648` huffman@30488 ` 1649` ```lemma Lim_cong_within[cong add]: ``` huffman@31488 ` 1650` ``` fixes a :: "'a::metric_space" ``` huffman@31488 ` 1651` ``` fixes l :: "'b::metric_space" (* TODO: generalize *) ``` huffman@31488 ` 1652` ``` shows "(\x. x \ a \ f x = g x) ==> ((\x. f x) ---> l) (at a within S) \ ((g ---> l) (at a within S))" ``` chaieb@30262 ` 1653` ``` by (simp add: Lim_within dist_nz[symmetric]) ``` chaieb@30262 ` 1654` huffman@30488 ` 1655` ```lemma Lim_cong_at[cong add]: ``` huffman@31488 ` 1656` ``` fixes a :: "'a::metric_space" ``` huffman@31488 ` 1657` ``` fixes l :: "'b::metric_space" (* TODO: generalize *) ``` huffman@31488 ` 1658` ``` shows "(\x. x \ a ==> f x = g x) ==> (((\x. f x) ---> l) (at a) \ ((g ---> l) (at a)))" ``` chaieb@30262 ` 1659` ``` by (simp add: Lim_at dist_nz[symmetric]) ``` chaieb@30262 ` 1660` chaieb@30262 ` 1661` ```text{* Useful lemmas on closure and set of possible sequential limits.*} ``` chaieb@30262 ` 1662` huffman@30488 ` 1663` ```lemma closure_sequential: ``` huffman@31488 ` 1664` ``` fixes l :: "'a::metric_space" (* TODO: generalize *) ``` huffman@31488 ` 1665` ``` shows "l \ closure S \ (\x. (\n. x n \ S) \ (x ---> l) sequentially)" (is "?lhs = ?rhs") ``` chaieb@30262 ` 1666` ```proof ``` chaieb@30262 ` 1667` ``` assume "?lhs" moreover ``` chaieb@30262 ` 1668` ``` { assume "l \ S" ``` chaieb@30262 ` 1669` ``` hence "?rhs" using Lim_const[of l sequentially] by auto ``` chaieb@30262 ` 1670` ``` } moreover ``` chaieb@30262 ` 1671` ``` { assume "l islimpt S" ``` chaieb@30262 ` 1672` ``` hence "?rhs" unfolding islimpt_sequential by auto ``` chaieb@30262 ` 1673` ``` } ultimately ``` chaieb@30262 ` 1674` ``` show "?rhs" unfolding closure_def by auto ``` chaieb@30262 ` 1675` ```next ``` chaieb@30262 ` 1676` ``` assume "?rhs" ``` chaieb@30262 ` 1677` ``` thus "?lhs" unfolding closure_def unfolding islimpt_sequential by auto ``` chaieb@30262 ` 1678` ```qed ``` chaieb@30262 ` 1679` huffman@30488 ` 1680` ```lemma closed_sequential_limits: ``` huffman@31420 ` 1681` ``` fixes S :: "'a::metric_space set" ``` huffman@31420 ` 1682` ``` shows "closed S \ (\x l. (\n. x n \ S) \ (x ---> l) sequentially \ l \ S)" ``` chaieb@30262 ` 1683` ``` unfolding closed_limpt ``` huffman@31420 ` 1684` ``` using closure_sequential [where 'a='a] closure_closed [where 'a='a] closed_limpt [where 'a='a] islimpt_sequential [where 'a='a] mem_delete [where 'a='a] ``` huffman@31420 ` 1685` ``` by metis ``` huffman@31420 ` 1686` huffman@31420 ` 1687` ```lemma closure_approachable: ``` huffman@31420 ` 1688` ``` fixes S :: "'a::metric_space set" ``` huffman@31420 ` 1689` ``` shows "x \ closure S \ (\e>0. \y\S. dist y x < e)" ``` chaieb@30262 ` 1690` ``` apply (auto simp add: closure_def islimpt_approachable) ``` huffman@31285 ` 1691` ``` by (metis dist_self) ``` chaieb@30262 ` 1692` huffman@31418 ` 1693` ```lemma closed_approachable: ``` huffman@31418 ` 1694` ``` fixes S :: "'a::metric_space set" ``` huffman@31418 ` 1695` ``` shows "closed S ==> (\e>0. \y\S. dist y x < e) \ x \ S" ``` chaieb@30262 ` 1696` ``` by (metis closure_closed closure_approachable) ``` chaieb@30262 ` 1697` chaieb@30262 ` 1698` ```text{* Some other lemmas about sequences. *} ``` chaieb@30262 ` 1699` huffman@31488 ` 1700` ```lemma seq_offset: ``` huffman@31488 ` 1701` ``` fixes l :: "'a::metric_space" (* TODO: generalize *) ``` huffman@31488 ` 1702` ``` shows "(f ---> l) sequentially ==> ((\i. f( i + k)) ---> l) sequentially" ``` chaieb@30262 ` 1703` ``` apply (auto simp add: Lim_sequentially) ``` chaieb@30262 ` 1704` ``` by (metis trans_le_add1 ) ``` chaieb@30262 ` 1705` huffman@31488 ` 1706` ```lemma seq_offset_neg: ``` huffman@31526 ` 1707` ``` "(f ---> l) sequentially ==> ((\i. f(i - k)) ---> l) sequentially" ``` huffman@31526 ` 1708` ``` apply (rule topological_tendstoI) ``` huffman@31526 ` 1709` ``` apply (drule (2) topological_tendstoD) ``` huffman@31526 ` 1710` ``` apply (simp only: eventually_sequentially) ``` chaieb@30262 ` 1711` ``` apply (subgoal_tac "\N k (n::nat). N + k <= n ==> N <= n - k") ``` chaieb@30262 ` 1712` ``` apply metis ``` chaieb@30262 ` 1713` ``` by arith ``` chaieb@30262 ` 1714` huffman@31488 ` 1715` ```lemma seq_offset_rev: ``` huffman@31526 ` 1716` ``` "((\i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially" ``` huffman@31526 ` 1717` ``` apply (rule topological_tendstoI) ``` huffman@31526 ` 1718` ``` apply (drule (2) topological_tendstoD) ``` huffman@31526 ` 1719` ``` apply (simp only: eventually_sequentially) ``` chaieb@30262 ` 1720` ``` apply (subgoal_tac "\N k (n::nat). N + k <= n ==> N <= n - k \ (n - k) + k = n") ``` chaieb@30262 ` 1721` ``` by metis arith ``` chaieb@30262 ` 1722` huffman@31558 ` 1723` ```lemma seq_harmonic: "((\n. inverse (real n)) ---> 0) sequentially" ``` chaieb@30262 ` 1724` ```proof- ``` chaieb@30262 ` 1725` ``` { fix e::real assume "e>0" ``` chaieb@30262 ` 1726` ``` hence "\N::nat. \n::nat\N. inverse (real n) < e" ``` chaieb@30262 ` 1727` ``` using real_arch_inv[of e] apply auto apply(rule_tac x=n in exI) ``` huffman@31558 ` 1728` ``` by (metis not_le le_imp_inverse_le not_less real_of_nat_gt_zero_cancel_iff real_of_nat_less_iff xt1(7)) ``` chaieb@30262 ` 1729` ``` } ``` huffman@31558 ` 1730` ``` thus ?thesis unfolding Lim_sequentially dist_norm by simp ``` chaieb@30262 ` 1731` ```qed ``` chaieb@30262 ` 1732` chaieb@30262 ` 1733` ```text{* More properties of closed balls. *} ``` chaieb@30262 ` 1734` huffman@31396 ` 1735` ```lemma closed_cball: "closed (cball x e)" ``` huffman@31526 ` 1736` ```unfolding cball_def closed_def ``` huffman@31396 ` 1737` ```unfolding Collect_neg_eq [symmetric] not_le ``` huffman@31418 ` 1738` ```apply (clarsimp simp add: open_dist, rename_tac y) ``` huffman@31396 ` 1739` ```apply (rule_tac x="dist x y - e" in exI, clarsimp) ``` huffman@31492 ` 1740` ```apply (rename_tac x') ``` huffman@31396 ` 1741` ```apply (cut_tac x=x and y=x' and z=y in dist_triangle) ``` huffman@31396 ` 1742` ```apply simp ``` huffman@31396 ` 1743` ```done ``` huffman@30488 ` 1744` chaieb@30262 ` 1745` ```lemma open_contains_cball: "open S \ (\x\S. \e>0. cball x e \ S)" ``` chaieb@30262 ` 1746` ```proof- ``` chaieb@30262 ` 1747` ``` { fix x and e::real assume "x\S" "e>0" "ball x e \ S" ``` chaieb@30262 ` 1748` ``` hence "\d>0. cball x d \ S" unfolding subset_eq by (rule_tac x="e/2" in exI, auto) ``` chaieb@30262 ` 1749` ``` } moreover ``` chaieb@30262 ` 1750` ``` { fix x and e::real assume "x\S" "e>0" "cball x e \ S" ``` chaieb@30262 ` 1751` ``` hence "\d>0. ball x d \ S" unfolding subset_eq apply(rule_tac x="e/2" in exI) by auto ``` chaieb@30262 ` 1752` ``` } ultimately ``` chaieb@30262 ` 1753` ``` show ?thesis unfolding open_contains_ball by auto ``` chaieb@30262 ` 1754` ```qed ``` chaieb@30262 ` 1755` chaieb@30262 ` 1756` ```lemma open_contains_cball_eq: "open S ==> (\x. x \ S \ (\e>0. cball x e \ S))" ``` chaieb@30262 ` 1757` ``` by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball mem_def) ``` chaieb@30262 ` 1758` chaieb@30262 ` 1759` ```lemma mem_interior_cball: "x \ interior S \ (\e>0. cball x e \ S)" ``` huffman@31345 ` 1760` ``` apply (simp add: interior_def, safe) ``` huffman@31345 ` 1761` ``` apply (force simp add: open_contains_cball) ``` huffman@31345 ` 1762` ``` apply (rule_tac x="ball x e" in exI) ``` huffman@31345 ` 1763` ``` apply (simp add: open_ball centre_in_ball subset_trans [OF ball_subset_cball]) ``` huffman@31345 ` 1764` ``` done ``` huffman@31345 ` 1765` huffman@31345 ` 1766` ```lemma islimpt_ball: ``` huffman@31345 ` 1767` ``` fixes x y :: "'a::{real_normed_vector,perfect_space}" ``` huffman@31345 ` 1768` ``` shows "y islimpt ball x e \ 0 < e \ y \ cball x e" (is "?lhs = ?rhs") ``` chaieb@30262 ` 1769` ```proof ``` chaieb@30262 ` 1770` ``` assume "?lhs" ``` chaieb@30262 ` 1771` ``` { assume "e \ 0" ``` chaieb@30262 ` 1772` ``` hence *:"ball x e = {}" using ball_eq_empty[of x e] by auto ``` huffman@30488 ` 1773` ``` have False using `?lhs` unfolding * using islimpt_EMPTY[of y] by auto ``` chaieb@30262 ` 1774` ``` } ``` huffman@31526 ` 1775` ``` hence "e > 0" by (metis not_less) ``` chaieb@30262 ` 1776` ``` moreover ``` chaieb@30262 ` 1777` ``` have "y \ cball x e" using closed_cball[of x e] islimpt_subset[of y "ball x e" "cball x e"] ball_subset_cball[of x e] `?lhs` unfolding closed_limpt by auto ``` chaieb@30262 ` 1778` ``` ultimately show "?rhs" by auto ``` chaieb@30262 ` 1779` ```next ``` chaieb@30262 ` 1780` ``` assume "?rhs" hence "e>0" by auto ``` chaieb@30262 ` 1781` ``` { fix d::real assume "d>0" ``` chaieb@30262 ` 1782` ``` have "\x'\ball x e. x' \ y \ dist x' y < d" ``` chaieb@30262 ` 1783` ``` proof(cases "d \ dist x y") ``` chaieb@30262 ` 1784` ``` case True thus "\x'\ball x e. x' \ y \ dist x' y < d" ``` chaieb@30262 ` 1785` ``` proof(cases "x=y") ``` huffman@31285 ` 1786` ``` case True hence False using `d \ dist x y` `d>0` by auto ``` chaieb@30262 ` 1787` ``` thus "\x'\ball x e. x' \ y \ dist x' y < d" by auto ``` chaieb@30262 ` 1788` ``` next ``` chaieb@30262 ` 1789` ``` case False ``` chaieb@30262 ` 1790` huffman@31345 ` 1791` ``` have "dist x (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) ``` huffman@31345 ` 1792` ``` = norm (x - y + (d / (2 * norm (y - x))) *\<^sub>R (y - x))" ``` huffman@31289 ` 1793` ``` unfolding mem_cball mem_ball dist_norm diff_diff_eq2 diff_add_eq[THEN sym] by auto ``` chaieb@30262 ` 1794` ``` also have "\ = \- 1 + d / (2 * norm (x - y))\ * norm (x - y)" ``` huffman@31345 ` 1795` ``` using scaleR_left_distrib[of "- 1" "d / (2 * norm (y - x))", THEN sym, of "y - x"] ``` huffman@31345 ` 1796` ``` unfolding scaleR_minus_left scaleR_one ``` huffman@31345 ` 1797` ``` by (auto simp add: norm_minus_commute norm_scaleR) ``` chaieb@30262 ` 1798` ``` also have "\ = \- norm (x - y) + d / 2\" ``` chaieb@30262 ` 1799` ``` unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]] ``` huffman@31289 ` 1800` ``` unfolding real_add_mult_distrib using `x\y`[unfolded dist_nz, unfolded dist_norm] by auto ``` huffman@31289 ` 1801` ``` also have "\ \ e - d/2" using `d \ dist x y` and `d>0` and `?rhs` by(auto simp add: dist_norm) ``` huffman@31345 ` 1802` ``` finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \ ball x e" using `d>0` by auto ``` chaieb@30262 ` 1803` chaieb@30262 ` 1804` ``` moreover ``` chaieb@30262 ` 1805` huffman@31345 ` 1806` ``` have "(d / (2*dist y x)) *\<^sub>R (y - x) \ 0" ``` huffman@31345 ` 1807` ``` using `x\y`[unfolded dist_nz] `d>0` unfolding scaleR_eq_0_iff by (auto simp add: dist_commute) ``` chaieb@30262 ` 1808` ``` moreover ``` huffman@31345 ` 1809` ``` have "dist (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) y < d" unfolding dist_norm apply simp unfolding norm_minus_cancel norm_scaleR ``` huffman@31285 ` 1810` ``` using `d>0` `x\y`[unfolded dist_nz] dist_commute[of x y] ``` huffman@31289 ` 1811` ``` unfolding dist_norm by auto ``` huffman@31345 ` 1812` ``` ultimately show "\x'\ball x e. x' \ y \ dist x' y < d" by (rule_tac x="y - (d / (2*dist y x)) *\<^sub>R (y - x)" in bexI) auto ``` chaieb@30262 ` 1813` ``` qed ``` chaieb@30262 ` 1814` ``` next ``` chaieb@30262 ` 1815` ``` case False hence "d > dist x y" by auto ``` chaieb@30262 ` 1816` ``` show "\x'\ball x e. x' \ y \ dist x' y < d" ``` chaieb@30262 ` 1817` ``` proof(cases "x=y") ``` chaieb@30262 ` 1818` ``` case True ``` huffman@31345 ` 1819` ``` obtain z where **: "z \ y" "dist z y < min e d" ``` huffman@31345 ` 1820` ``` using perfect_choose_dist[of "min e d" y] ``` huffman@31285 ` 1821` ``` using `d > 0` `e>0` by auto ``` huffman@30488 ` 1822` ``` show "\x'\ball x e. x' \ y \ dist x' y < d" ``` huffman@31345 ` 1823` ``` unfolding `x = y` ``` huffman@31345 ` 1824` ``` using `z \ y` ** ``` huffman@31345 ` 1825` ``` by (rule_tac x=z in bexI, auto simp add: dist_commute) ``` chaieb@30262 ` 1826` ``` next ``` chaieb@30262 ` 1827` ``` case False thus "\x'\ball x e. x' \ y \ dist x' y < d" ``` huffman@31285 ` 1828` ``` using `d>0` `d > dist x y` `?rhs` by(rule_tac x=x in bexI, auto) ``` chaieb@30262 ` 1829` ``` qed ``` chaieb@30262 ` 1830` ``` qed } ``` chaieb@30262 ` 1831` ``` thus "?lhs" unfolding mem_cball islimpt_approachable mem_ball by auto ``` chaieb@30262 ` 1832` ```qed ``` chaieb@30262 ` 1833` huffman@31526 ` 1834` ```lemma closure_ball_lemma: ``` huffman@31526 ` 1835` ``` fixes x y :: "'a::real_normed_vector" ``` huffman@31526 ` 1836` ``` assumes "x \ y" shows "y islimpt ball x (dist x y)" ``` huffman@31526 ` 1837` ```proof (rule islimptI) ``` huffman@31526 ` 1838` ``` fix T assume "y \ T" "open T" ``` huffman@31526 ` 1839` ``` then obtain r where "0 < r" "\z. dist z y < r \ z \ T" ``` huffman@31526 ` 1840` ``` unfolding open_dist by fast ``` huffman@31526 ` 1841` ``` (* choose point between x and y, within distance r of y. *) ``` huffman@31526 ` 1842` ``` def k \ "min 1 (r / (2 * dist x y))" ``` huffman@31526 ` 1843` ``` def z \ "y + scaleR k (x - y)" ``` huffman@31526 ` 1844` ``` have z_def2: "z = x + scaleR (1 - k) (y - x)" ``` huffman@31526 ` 1845` ``` unfolding z_def by (simp add: algebra_simps) ``` huffman@31526 ` 1846` ``` have "dist z y < r" ``` huffman@31526 ` 1847` ``` unfolding z_def k_def using `0 < r` ``` huffman@31526 ` 1848` ``` by (simp add: dist_norm norm_scaleR min_def) ``` huffman@31526 ` 1849` ``` hence "z \ T" using `\z. dist z y < r \ z \ T` by simp ``` huffman@31526 ` 1850` ``` have "dist x z < dist x y" ``` huffman@31526 ` 1851` ``` unfolding z_def2 dist_norm ``` huffman@31526 ` 1852` ``` apply (simp add: norm_scaleR norm_minus_commute) ``` huffman@31526 ` 1853` ``` apply (simp only: dist_norm [symmetric]) ``` huffman@31526 ` 1854` ``` apply (subgoal_tac "\1 - k\ * dist x y < 1 * dist x y", simp) ``` huffman@31526 ` 1855` ``` apply (rule mult_strict_right_mono) ``` huffman@31526 ` 1856` ``` apply (simp add: k_def divide_pos_pos zero_less_dist_iff `0 < r` `x \ y`) ``` huffman@31526 ` 1857` ``` apply (simp add: zero_less_dist_iff `x \ y`) ``` huffman@31526 ` 1858` ``` done ``` huffman@31526 ` 1859` ``` hence "z \ ball x (dist x y)" by simp ``` huffman@31526 ` 1860` ``` have "z \ y" ``` huffman@31526 ` 1861` ``` unfolding z_def k_def using `x \ y` `0 < r` ``` huffman@31526 ` 1862` ``` by (simp add: min_def) ``` huffman@31526 ` 1863` ``` show "\z\ball x (dist x y). z \ T \ z \ y" ``` huffman@31526 ` 1864` ``` using `z \ ball x (dist x y)` `z \ T` `z \ y` ``` huffman@31526 ` 1865` ``` by fast ``` huffman@31526 ` 1866` ```qed ``` huffman@31526 ` 1867` huffman@31345 ` 1868` ```lemma closure_ball: ``` huffman@31526 ` 1869` ``` fixes x :: "'a::real_normed_vector" ``` huffman@31526 ` 1870` ``` shows "0 < e \ closure (ball x e) = cball x e" ``` huffman@31526 ` 1871` ```apply (rule equalityI) ``` huffman@31526 ` 1872` ```apply (rule closure_minimal) ``` huffman@31526 ` 1873` ```apply (rule ball_subset_cball) ``` huffman@31526 ` 1874` ```apply (rule closed_cball) ``` huffman@31526 ` 1875` ```apply (rule subsetI, rename_tac y) ``` huffman@31526 ` 1876` ```apply (simp add: le_less [where 'a=real]) ``` huffman@31526 ` 1877` ```apply (erule disjE) ``` huffman@31526 ` 1878` ```apply (rule subsetD [OF closure_subset], simp) ``` huffman@31526 ` 1879` ```apply (simp add: closure_def) ``` huffman@31526 ` 1880` ```apply clarify ``` huffman@31526 ` 1881` ```apply (rule closure_ball_lemma) ``` huffman@31526 ` 1882` ```apply (simp add: zero_less_dist_iff) ``` huffman@31526 ` 1883` ```done ``` chaieb@30262 ` 1884` huffman@31345 ` 1885` ```lemma interior_cball: ``` huffman@31345 ` 1886` ``` fixes x :: "real ^ _" (* FIXME: generalize *) ``` huffman@31345 ` 1887` ``` shows "interior(cball x e) = ball x e" ``` chaieb@30262 ` 1888` ```proof(cases "e\0") ``` chaieb@30262 ` 1889` ``` case False note cs = this ``` chaieb@30262 ` 1890` ``` from cs have "ball x e = {}" using ball_empty[of e x] by auto moreover ``` chaieb@30262 ` 1891` ``` { fix y assume "y \ cball x e" ``` huffman@31285 ` 1892` ``` hence False unfolding mem_cball using dist_nz[of x y] cs by auto } ``` chaieb@30262 ` 1893` ``` hence "cball x e = {}" by auto ``` chaieb@30262 ` 1894` ``` hence "interior (cball x e) = {}" using interior_empty by auto ``` huffman@30488 ` 1895` ``` ultimately show ?thesis by blast ``` chaieb@30262 ` 1896` ```next ``` chaieb@30262 ` 1897` ``` case True note cs = this ``` chaieb@30262 ` 1898` ``` have "ball x e \ cball x e" using ball_subset_cball by auto moreover ``` chaieb@30262 ` 1899` ``` { fix S y assume as: "S \ cball x e" "open S" "y\S" ``` huffman@31418 ` 1900` ``` then obtain d where "d>0" and d:"\x'. dist x' y < d \ x' \ S" unfolding open_dist by blast ``` huffman@30488 ` 1901` huffman@30488 ` 1902` ``` then obtain xa where xa:"dist y xa = d / 2" using vector_choose_dist[of "d/2" y] by auto ``` chaieb@30262 ` 1903` ``` hence xa_y:"xa \ y" using dist_nz[of y xa] using `d>0` by auto ``` huffman@31285 ` 1904` ``` have "xa\S" using d[THEN spec[where x=xa]] using xa apply(auto simp add: dist_commute) unfolding dist_nz[THEN sym] using xa_y by auto ``` chaieb@30262 ` 1905` ``` hence xa_cball:"xa \ cball x e" using as(1) by auto ``` chaieb@30262 ` 1906` chaieb@30262 ` 1907` ``` hence "y \ ball x e" proof(cases "x = y") ``` chaieb@30262 ` 1908` ``` case True ``` huffman@31285 ` 1909` ``` hence "e>0" using xa_y[unfolded dist_nz] xa_cball[unfolded mem_cball] by (auto simp add: dist_commute) ``` chaieb@30262 ` 1910` ``` thus "y \ ball x e" using `x = y ` by simp ``` chaieb@30262 ` 1911` ``` next ``` chaieb@30262 ` 1912` ``` case False ``` huffman@31289 ` 1913` ``` have "dist (y + (d / 2 / dist y x) *s (y - x)) y < d" unfolding dist_norm ``` huffman@30488 ` 1914` ``` using `d>0` norm_ge_zero[of "y - x"] `x \ y` by auto ``` chaieb@30262 ` 1915` ``` hence *:"y + (d / 2 / dist y x) *s (y - x) \ cball x e" using d as(1)[unfolded subset_eq] by blast ``` chaieb@30262 ` 1916` ``` have "y - x \ 0" using `x \ y` by auto ``` chaieb@30262 ` 1917` ``` hence **:"d / (2 * norm (y - x)) > 0" unfolding zero_less_norm_iff[THEN sym] ``` chaieb@30262 ` 1918` ``` using `d>0` divide_pos_pos[of d "2*norm (y - x)"] by auto ``` chaieb@30262 ` 1919` chaieb@30262 ` 1920` ``` have "dist (y + (d / 2 / dist y x) *s (y - x)) x = norm (y + (d / (2 * norm (y - x))) *s y - (d / (2 * norm (y - x))) *s x - x)" ``` huffman@31289 ` 1921` ``` by (auto simp add: dist_norm vector_ssub_ldistrib add_diff_eq) ``` chaieb@30262 ` 1922` ``` also have "\ = norm ((1 + d / (2 * norm (y - x))) *s (y - x))" ``` chaieb@30262 ` 1923` ``` by (auto simp add: vector_sadd_rdistrib vector_smult_lid ring_simps vector_sadd_rdistrib vector_ssub_ldistrib) ``` chaieb@30262 ` 1924` ``` also have "\ = \1 + d / (2 * norm (y - x))\ * norm (y - x)" using ** by auto ``` huffman@31289 ` 1925` ``` also have "\ = (dist y x) + d/2"using ** by (auto simp add: left_distrib dist_norm) ``` huffman@31285 ` 1926` ``` finally have "e \ dist x y +d/2" using *[unfolded mem_cball] by (auto simp add: dist_commute) ``` chaieb@30262 ` 1927` ``` thus "y \ ball x e" unfolding mem_ball using `d>0` by auto ``` chaieb@30262 ` 1928` ``` qed } ``` chaieb@30262 ` 1929` ``` hence "\S \ cball x e. open S \ S \ ball x e" by auto ``` chaieb@30262 ` 1930` ``` ultimately show ?thesis using interior_unique[of "ball x e" "cball x e"] using open_ball[of x e] by auto ``` huffman@30488 ` 1931` ```qed ``` chaieb@30262 ` 1932` huffman@31345 ` 1933` ```lemma frontier_ball: ``` huffman@31345 ` 1934` ``` fixes a :: "real ^ _" (* FIXME: generalize *) ``` huffman@31345 ` 1935` ``` shows "0 < e ==> frontier(ball a e) = {x. dist a x = e}" ``` huffman@30488 ` 1936` ``` apply (simp add: frontier_def closure_ball interior_open open_ball order_less_imp_le) ``` chaieb@30262 ` 1937` ``` apply (simp add: expand_set_eq) ``` chaieb@30262 ` 1938` ``` by arith ``` chaieb@30262 ` 1939` huffman@31345 ` 1940` ```lemma frontier_cball: ``` huffman@31345 ` 1941` ``` fixes a :: "real ^ _" (* FIXME: generalize *) ``` huffman@31345 ` 1942` ``` shows "frontier(cball a e) = {x. dist a x = e}" ``` chaieb@30262 ` 1943` ``` apply (simp add: frontier_def interior_cball closed_cball closure_closed order_less_imp_le) ``` chaieb@30262 ` 1944` ``` apply (simp add: expand_set_eq) ``` chaieb@30262 ` 1945` ``` by arith ``` chaieb@30262 ` 1946` chaieb@30262 ` 1947` ```lemma cball_eq_empty: "(cball x e = {}) \ e < 0" ``` chaieb@30262 ` 1948` ``` apply (simp add: expand_set_eq not_le) ``` huffman@31285 ` 1949` ``` by (metis zero_le_dist dist_self order_less_le_trans) ``` chaieb@30262 ` 1950` ```lemma cball_empty: "e < 0 ==> cball x e = {}" by (simp add: cball_eq_empty) ``` chaieb@30262 ` 1951` huffman@31345 ` 1952` ```lemma cball_eq_sing: ``` huffman@31345 ` 1953` ``` fixes x :: "real ^ _" (* FIXME: generalize *) ``` huffman@31345 ` 1954` ``` shows "(cball x e = {x}) \ e = 0" ``` chaieb@30262 ` 1955` ```proof- ``` chaieb@30262 ` 1956` ``` { assume as:"\xa. (dist x xa \ e) = (xa = x)" ``` huffman@31285 ` 1957` ``` hence "e \ 0" apply (erule_tac x=x in allE) by auto ``` chaieb@30262 ` 1958` ``` then obtain y where y:"dist x y = e" using vector_choose_dist[of e] by auto ``` huffman@31285 ` 1959` ``` hence "e = 0" using as apply(erule_tac x=y in allE) by auto ``` chaieb@30262 ` 1960` ``` } ``` huffman@31285 ` 1961` ``` thus ?thesis unfolding expand_set_eq mem_cball by (auto simp add: dist_nz) ``` huffman@30488 ` 1962` ```qed ``` chaieb@30262 ` 1963` huffman@31345 ` 1964` ```lemma cball_sing: ``` huffman@31345 ` 1965` ``` fixes x :: "real ^ _" (* FIXME: generalize *) ``` huffman@31345 ` 1966` ``` shows "e = 0 ==> cball x e = {x}" by (simp add: cball_eq_sing) ``` chaieb@30262 ` 1967` chaieb@30262 ` 1968` ```text{* For points in the interior, localization of limits makes no difference. *} ``` chaieb@30262 ` 1969` huffman@31447 ` 1970` ```lemma eventually_within_interior: ``` huffman@31447 ` 1971` ``` assumes "x \ interior S" ``` chaieb@30262 ` 1972` ``` shows "eventually P (at x within S) \ eventually P (at x)" (is "?lhs = ?rhs") ``` chaieb@30262 ` 1973` ```proof- ``` huffman@31527 ` 1974` ``` from assms obtain T where T: "open T" "x \ T" "T \ S" ``` huffman@31527 ` 1975` ``` unfolding interior_def by fast ``` huffman@31527 ` 1976` ``` { assume "?lhs" ``` huffman@31527 ` 1977` ``` then obtain A where "open A" "x \ A" "\y\A. y \ x \ y \ S \ P y" ``` huffman@31527 ` 1978` ``` unfolding Limits.eventually_within Limits.eventually_at_topological ``` huffman@31527 ` 1979` ``` by auto ``` huffman@31527 ` 1980` ``` with T have "open (A \ T)" "x \ A \ T" "\y\(A \ T). y \ x \ P y" ``` huffman@31527 ` 1981` ``` by auto ``` huffman@31527 ` 1982` ``` then have "?rhs" ``` huffman@31527 ` 1983` ``` unfolding Limits.eventually_at_topological by auto ``` chaieb@30262 ` 1984` ``` } moreover ``` huffman@31527 ` 1985` ``` { assume "?rhs" hence "?lhs" ``` huffman@31527 ` 1986` ``` unfolding Limits.eventually_within ``` huffman@31527 ` 1987` ``` by (auto elim: eventually_elim1) ``` chaieb@30262 ` 1988` ``` } ultimately ``` huffman@31527 ` 1989` ``` show "?thesis" .. ``` chaieb@30262 ` 1990` ```qed ``` chaieb@30262 ` 1991` huffman@31447 ` 1992` ```lemma lim_within_interior: ``` huffman@31527 ` 1993` ``` "x \ interior S \ (f ---> l) (at x within S) \ (f ---> l) (at x)" ``` huffman@31527 ` 1994` ``` unfolding tendsto_def by (simp add: eventually_within_interior) ``` chaieb@30262 ` 1995` huffman@31346 ` 1996` ```lemma netlimit_within_interior: ``` huffman@31346 ` 1997` ``` fixes x :: "'a::{perfect_space, real_normed_vector}" ``` huffman@31346 ` 1998` ``` (* FIXME: generalize to perfect_space *) ``` huffman@31346 ` 1999` ``` assumes "x \ interior S" ``` chaieb@30262 ` 2000` ``` shows "netlimit(at x within S) = x" (is "?lhs = ?rhs") ``` chaieb@30262 ` 2001` ```proof- ``` chaieb@30262 ` 2002` ``` from assms obtain e::real where e:"e>0" "ball x e \ S" using open_interior[of S] unfolding open_contains_ball using interior_subset[of S] by auto ``` chaieb@30262 ` 2003` ``` hence "\ trivial_limit (at x within S)" using islimpt_subset[of x "ball x e" S] unfolding trivial_limit_within islimpt_ball centre_in_cball by auto ``` chaieb@30262 ` 2004` ``` thus ?thesis using netlimit_within by auto ``` chaieb@30262 ` 2005` ```qed ``` chaieb@30262 ` 2006` chaieb@30262 ` 2007` ```subsection{* Boundedness. *} ``` chaieb@30262 ` 2008` chaieb@30262 ` 2009` ``` (* FIXME: This has to be unified with BSEQ!! *) ``` huffman@31400 ` 2010` ```definition ``` huffman@31533 ` 2011` ``` bounded :: "'a::metric_space set \ bool" where ``` huffman@31533 ` 2012` ``` "bounded S \ (\x e. \y\S. dist x y \ e)" ``` huffman@31533 ` 2013` huffman@31533 ` 2014` ```lemma bounded_any_center: "bounded S \ (\e. \y\S. dist a y \ e)" ``` huffman@31533 ` 2015` ```unfolding bounded_def ``` huffman@31533 ` 2016` ```apply safe ``` huffman@31533 ` 2017` ```apply (rule_tac x="dist a x + e" in exI, clarify) ``` huffman@31533 ` 2018` ```apply (drule (1) bspec) ``` huffman@31533 ` 2019` ```apply (erule order_trans [OF dist_triangle add_left_mono]) ``` huffman@31533 ` 2020` ```apply auto ``` huffman@31533 ` 2021` ```done ``` huffman@31533 ` 2022` huffman@31533 ` 2023` ```lemma bounded_iff: "bounded S \ (\a. \x\S. norm x \ a)" ``` huffman@31533 ` 2024` ```unfolding bounded_any_center [where a=0] ``` huffman@31533 ` 2025` ```by (simp add: dist_norm) ``` chaieb@30262 ` 2026` chaieb@30262 ` 2027` ```lemma bounded_empty[simp]: "bounded {}" by (simp add: bounded_def) ``` chaieb@30262 ` 2028` ```lemma bounded_subset: "bounded T \ S \ T ==> bounded S" ``` chaieb@30262 ` 2029` ``` by (metis bounded_def subset_eq) ``` chaieb@30262 ` 2030` chaieb@30262 ` 2031` ```lemma bounded_interior[intro]: "bounded S ==> bounded(interior S)" ``` chaieb@30262 ` 2032` ``` by (metis bounded_subset interior_subset) ``` chaieb@30262 ` 2033` chaieb@30262 ` 2034` ```lemma bounded_closure[intro]: assumes "bounded S" shows "bounded(closure S)" ``` chaieb@30262 ` 2035` ```proof- ``` huffman@31533 ` 2036` ``` from assms obtain x and a where a: "\y\S. dist x y \ a" unfolding bounded_def by auto ``` huffman@31533 ` 2037` ``` { fix y assume "y \ closure S" ``` huffman@31533 ` 2038` ``` then obtain f where f: "\n. f n \ S" "(f ---> y) sequentially" ``` huffman@31533 ` 2039` ``` unfolding closure_sequential by auto ``` huffman@31533 ` 2040` ``` have "\n. f n \ S \ dist x (f n) \ a" using a by simp ``` huffman@31533 ` 2041` ``` hence "eventually (\n. dist x (f n) \ a) sequentially" ``` huffman@31533 ` 2042` ``` by (rule eventually_mono, simp add: f(1)) ``` huffman@31533 ` 2043` ``` have "dist x y \ a" ``` huffman@31533 ` 2044` ``` apply (rule Lim_dist_ubound [of sequentially f]) ``` huffman@31347 ` 2045` ``` apply (rule trivial_limit_sequentially) ``` huffman@31533 ` 2046` ``` apply (rule f(2)) ``` huffman@31347 ` 2047` ``` apply fact ``` huffman@31347 ` 2048` ``` done ``` chaieb@30262 ` 2049` ``` } ``` chaieb@30262 ` 2050` ``` thus ?thesis unfolding bounded_def by auto ``` chaieb@30262 ` 2051` ```qed ``` chaieb@30262 ` 2052` chaieb@30262 ` 2053` ```lemma bounded_cball[simp,intro]: "bounded (cball x e)" ``` chaieb@30262 ` 2054` ``` apply (simp add: bounded_def) ``` huffman@31533 ` 2055` ``` apply (rule_tac x=x in exI) ``` huffman@31533 ` 2056` ``` apply (rule_tac x=e in exI) ``` huffman@31533 ` 2057` ``` apply auto ``` huffman@31400 ` 2058` ``` done ``` chaieb@30262 ` 2059` chaieb@30262 ` 2060` ```lemma bounded_ball[simp,intro]: "bounded(ball x e)" ``` chaieb@30262 ` 2061` ``` by (metis ball_subset_cball bounded_cball bounded_subset) ``` chaieb@30262 ` 2062` chaieb@30262 ` 2063` ```lemma finite_imp_bounded[intro]: assumes "finite S" shows "bounded S" ``` chaieb@30262 ` 2064` ```proof- ``` huffman@31533 ` 2065` ``` { fix a F assume as:"bounded F" ``` huffman@31533 ` 2066` ``` then obtain x e where "\y\F. dist x y \ e" unfolding bounded_def by auto ``` huffman@31533 ` 2067` ``` hence "\y\(insert a F). dist x y \ max e (dist x a)" by auto ``` huffman@31533 ` 2068` ``` hence "bounded (insert a F)" unfolding bounded_def by (intro exI) ``` chaieb@30262 ` 2069` ``` } ``` chaieb@30262 ` 2070` ``` thus ?thesis using finite_induct[of S bounded] using bounded_empty assms by auto ``` huffman@30488 ` 2071` ```qed ``` chaieb@30262 ` 2072` chaieb@30262 ` 2073` ```lemma bounded_Un[simp]: "bounded (S \ T) \ bounded S \ bounded T" ``` chaieb@30262 ` 2074` ``` apply (auto simp add: bounded_def) ``` huffman@31533 ` 2075` ``` apply (rename_tac x y r s) ``` huffman@31533 ` 2076` ``` apply (rule_tac x=x in exI) ``` huffman@31533 ` 2077` ``` apply (rule_tac x="max r (dist x y + s)" in exI) ``` huffman@31533 ` 2078` ``` apply (rule ballI, rename_tac z, safe) ``` huffman@31533 ` 2079` ``` apply (drule (1) bspec, simp) ``` huffman@31533 ` 2080` ``` apply (drule (1) bspec) ``` huffman@31533 ` 2081` ``` apply (rule min_max.le_supI2) ``` huffman@31533 ` 2082` ``` apply (erule order_trans [OF dist_triangle add_left_mono]) ``` huffman@31533 ` 2083` ``` done ``` chaieb@30262 ` 2084` huffman@30488 ` 2085` ```lemma bounded_Union[intro]: "finite F \ (\S\F. bounded S) \ bounded(\F)" ``` chaieb@30262 ` 2086` ``` by (induct rule: finite_induct[of F], auto) ``` chaieb@30262 ` 2087` chaieb@30262 ` 2088` ```lemma bounded_pos: "bounded S \ (\b>0. \x\ S. norm x <= b)" ``` huffman@31533 ` 2089` ``` apply (simp add: bounded_iff) ``` chaieb@30262 ` 2090` ``` apply (subgoal_tac "\x (y::real). 0 < 1 + abs y \ (x <= y \ x <= 1 + abs y)") ``` chaieb@30262 ` 2091` ``` by metis arith ``` chaieb@30262 ` 2092` chaieb@30262 ` 2093` ```lemma bounded_Int[intro]: "bounded S \ bounded T \ bounded (S \ T)" ``` chaieb@30262 ` 2094` ``` by (metis Int_lower1 Int_lower2 bounded_subset) ``` chaieb@30262 ` 2095` chaieb@30262 ` 2096` ```lemma bounded_diff[intro]: "bounded S ==> bounded (S - T)" ``` chaieb@30262 ` 2097` ```apply (metis Diff_subset bounded_subset) ``` chaieb@30262 ` 2098` ```done ``` chaieb@30262 ` 2099` chaieb@30262 ` 2100` ```lemma bounded_insert[intro]:"bounded(insert x S) \ bounded S" ``` chaieb@30262 ` 2101` ``` by (metis Diff_cancel Un_empty_right Un_insert_right bounded_Un bounded_subset finite.emptyI finite_imp_bounded infinite_remove subset_insertI) ``` chaieb@30262 ` 2102` huffman@31531 ` 2103` ```lemma not_bounded_UNIV[simp, intro]: ``` huffman@31531 ` 2104` ``` "\ bounded (UNIV :: 'a::{real_normed_vector, perfect_space} set)" ``` chaieb@30262 ` 2105` ```proof(auto simp add: bounded_pos not_le) ``` huffman@31531 ` 2106` ``` obtain x :: 'a where "x \ 0" ``` huffman@31531 ` 2107` ``` using perfect_choose_dist [OF zero_less_one] by fast ``` chaieb@30262 ` 2108` ``` fix b::real assume b: "b >0" ``` chaieb@30262 ` 2109` ``` have b1: "b +1 \ 0" using b by simp ``` huffman@31531 ` 2110` ``` with `x \ 0` have "b < norm (scaleR (b + 1) (sgn x))" ``` huffman@31531 ` 2111` ``` by (simp add: norm_scaleR norm_sgn) ``` huffman@31531 ` 2112` ``` then show "\x::'a. b < norm x" .. ``` chaieb@30262 ` 2113` ```qed ``` chaieb@30262 ` 2114` huffman@30488 ` 2115` ```lemma bounded_linear_image: ``` huffman@30582 ` 2116` ``` fixes f :: "real^'m::finite \ real^'n::finite" ``` huffman@30488 ` 2117` ``` assumes "bounded S" "linear f" ``` chaieb@30262 ` 2118` ``` shows "bounded(f ` S)" ``` chaieb@30262 ` 2119` ```proof- ``` chaieb@30262 ` 2120` ``` from assms(1) obtain b where b:"b>0" "\x\S. norm x \ b" unfolding bounded_pos by auto ``` chaieb@30262 ` 2121` ``` from assms(2) obtain B where B:"B>0" "\x. norm (f x) \ B * norm x" using linear_bounded_pos by auto ``` chaieb@30262 ` 2122` ``` { fix x assume "x\S" ``` chaieb@30262 ` 2123` ``` hence "norm x \ b" using b by auto ``` chaieb@30262 ` 2124` ``` hence "norm (f x) \ B * b" using B(2) apply(erule_tac x=x in allE) ``` chaieb@30262 ` 2125` ``` by (metis B(1) B(2) real_le_trans real_mult_le_cancel_iff2) ``` chaieb@30262 ` 2126` ``` } ``` chaieb@30262 ` 2127` ``` thus ?thesis unfolding bounded_pos apply(rule_tac x="b*B" in exI) ``` chaieb@30262 ` 2128` ``` using b B real_mult_order[of b B] by (auto simp add: real_mult_commute) ``` chaieb@30262 ` 2129` ```qed ``` chaieb@30262 ` 2130` huffman@31400 ` 2131` ```lemma bounded_scaling: ``` huffman@31400 ` 2132` ``` fixes S :: "(real ^ 'n::finite) set" ``` huffman@31400 ` 2133` ``` shows "bounded S \ bounded ((\x. c *s x) ` S)" ``` chaieb@30262 ` 2134` ``` apply (rule bounded_linear_image, assumption) ``` chaieb@30262 ` 2135` ``` by (rule linear_compose_cmul, rule linear_id[unfolded id_def]) ``` chaieb@30262 ` 2136` huffman@31533 ` 2137` ```lemma bounded_translation: ``` huffman@31533 ` 2138` ``` fixes S :: "'a::real_normed_vector set" ``` huffman@31533 ` 2139` ``` assumes "bounded S" shows "bounded ((\x. a + x) ` S)" ``` chaieb@30262 ` 2140` ```proof- ``` chaieb@30262 ` 2141` ``` from assms obtain b where b:"b>0" "\x\S. norm x \ b" unfolding bounded_pos by auto ``` chaieb@30262 ` 2142` ``` { fix x assume "x\S" ``` chaieb@30262 ` 2143` ``` hence "norm (a + x) \ b + norm a" using norm_triangle_ineq[of a x] b by auto ``` chaieb@30262 ` 2144` ``` } ``` huffman@30488 ` 2145` ``` thus ?thesis unfolding bounded_pos using norm_ge_zero[of a] b(1) using add_strict_increasing[of b 0 "norm a"] ``` chaieb@30262 ` 2146` ``` by (auto intro!: add exI[of _ "b + norm a"]) ``` chaieb@30262 ` 2147` ```qed ``` chaieb@30262 ` 2148` chaieb@30262 ` 2149` chaieb@30262 ` 2150` ```text{* Some theorems on sups and infs using the notion "bounded". *} ``` chaieb@30262 ` 2151` huffman@31558 ` 2152` ```lemma bounded_real: ``` huffman@31400 ` 2153` ``` fixes S :: "real set" ``` huffman@31558 ` 2154` ``` shows "bounded S \ (\a. \x\S. abs x <= a)" ``` huffman@31558 ` 2155` ``` by (simp add: bounded_iff) ``` huffman@31558 ` 2156` huffman@31558 ` 2157` ```lemma bounded_has_rsup: assumes "bounded S" "S \ {}" ``` chaieb@30262 ` 2158` ``` shows "\x\S. x <= rsup S" and "\b. (\x\S. x <= b) \ rsup S <= b" ``` chaieb@30262 ` 2159` ```proof ``` chaieb@30262 ` 2160` ``` fix x assume "x\S" ``` huffman@31558 ` 2161` ``` from assms(1) obtain a where a:"\x\S. \x\ \ a" unfolding bounded_real by auto ``` chaieb@30262 ` 2162` ``` hence *:"S *<= a" using setleI[of S a] by (metis abs_le_interval_iff mem_def) ``` huffman@31558 ` 2163` ``` thus "x \ rsup S" using rsup[OF `S\{}`] using assms(1)[unfolded bounded_real] using isLubD2[of UNIV S "rsup S" x] using `x\S` by auto ``` chaieb@30262 ` 2164` ```next ``` chaieb@30262 ` 2165` ``` show "\b. (\x\S. x \ b) \ rsup S \ b" using assms ``` chaieb@30262 ` 2166` ``` using rsup[of S, unfolded isLub_def isUb_def leastP_def setle_def setge_def] ``` huffman@31558 ` 2167` ``` apply (auto simp add: bounded_real) ``` chaieb@30262 ` 2168` ``` by (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def) ``` chaieb@30262 ` 2169` ```qed ``` chaieb@30262 ` 2170` huffman@31558 ` 2171` ```lemma rsup_insert: assumes "bounded S" ``` chaieb@30262 ` 2172` ``` shows "rsup(insert x S) = (if S = {} then x else max x (rsup S))" ``` chaieb@30262 ` 2173` ```proof(cases "S={}") ``` chaieb@30262 ` 2174` ``` case True thus ?thesis using rsup_finite_in[of "{x}"] by auto ``` chaieb@30262 ` 2175` ```next ``` chaieb@30262 ` 2176` ``` let ?S = "insert x S" ``` chaieb@30262 ` 2177` ``` case False ``` chaieb@30262 ` 2178` ``` hence *:"\x\S. x \ rsup S" using bounded_has_rsup(1)[of S] using assms by auto ``` chaieb@30262 ` 2179` ``` hence "insert x S *<= max x (rsup S)" unfolding setle_def by auto ``` chaieb@30262 ` 2180` ``` hence "isLub UNIV ?S (rsup ?S)" using rsup[of ?S] by auto ``` chaieb@30262 ` 2181` ``` moreover ``` chaieb@30262 ` 2182` ``` have **:"isUb UNIV ?S (max x (rsup S))" unfolding isUb_def setle_def using * by auto ```