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