115 shows "open X" |
116 shows "open X" |
116 using assms |
117 using assms |
117 by (simp add: topological_basis_def) |
118 by (simp add: topological_basis_def) |
118 |
119 |
119 lemma topological_basis_imp_subbasis: |
120 lemma topological_basis_imp_subbasis: |
120 assumes B: "topological_basis B" shows "open = generate_topology B" |
121 assumes B: "topological_basis B" |
|
122 shows "open = generate_topology B" |
121 proof (intro ext iffI) |
123 proof (intro ext iffI) |
122 fix S :: "'a set" assume "open S" |
124 fix S :: "'a set" |
|
125 assume "open S" |
123 with B obtain B' where "B' \<subseteq> B" "S = \<Union>B'" |
126 with B obtain B' where "B' \<subseteq> B" "S = \<Union>B'" |
124 unfolding topological_basis_def by blast |
127 unfolding topological_basis_def by blast |
125 then show "generate_topology B S" |
128 then show "generate_topology B S" |
126 by (auto intro: generate_topology.intros dest: topological_basis_open) |
129 by (auto intro: generate_topology.intros dest: topological_basis_open) |
127 next |
130 next |
128 fix S :: "'a set" assume "generate_topology B S" then show "open S" |
131 fix S :: "'a set" |
|
132 assume "generate_topology B S" |
|
133 then show "open S" |
129 by induct (auto dest: topological_basis_open[OF B]) |
134 by induct (auto dest: topological_basis_open[OF B]) |
130 qed |
135 qed |
131 |
136 |
132 lemma basis_dense: |
137 lemma basis_dense: |
133 fixes B::"'a set set" and f::"'a set \<Rightarrow> 'a" |
138 fixes B::"'a set set" |
|
139 and f::"'a set \<Rightarrow> 'a" |
134 assumes "topological_basis B" |
140 assumes "topological_basis B" |
135 assumes choosefrom_basis: "\<And>B'. B' \<noteq> {} \<Longrightarrow> f B' \<in> B'" |
141 and choosefrom_basis: "\<And>B'. B' \<noteq> {} \<Longrightarrow> f B' \<in> B'" |
136 shows "(\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>B' \<in> B. f B' \<in> X))" |
142 shows "(\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>B' \<in> B. f B' \<in> X))" |
137 proof (intro allI impI) |
143 proof (intro allI impI) |
138 fix X::"'a set" assume "open X" "X \<noteq> {}" |
144 fix X::"'a set" |
|
145 assume "open X" "X \<noteq> {}" |
139 from topological_basisE[OF `topological_basis B` `open X` choosefrom_basis[OF `X \<noteq> {}`]] |
146 from topological_basisE[OF `topological_basis B` `open X` choosefrom_basis[OF `X \<noteq> {}`]] |
140 guess B' . note B' = this |
147 guess B' . note B' = this |
141 thus "\<exists>B'\<in>B. f B' \<in> X" by (auto intro!: choosefrom_basis) |
148 then show "\<exists>B'\<in>B. f B' \<in> X" |
|
149 by (auto intro!: choosefrom_basis) |
142 qed |
150 qed |
143 |
151 |
144 end |
152 end |
145 |
153 |
146 lemma topological_basis_prod: |
154 lemma topological_basis_prod: |
147 assumes A: "topological_basis A" and B: "topological_basis B" |
155 assumes A: "topological_basis A" |
|
156 and B: "topological_basis B" |
148 shows "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))" |
157 shows "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))" |
149 unfolding topological_basis_def |
158 unfolding topological_basis_def |
150 proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[symmetric]) |
159 proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[symmetric]) |
151 fix S :: "('a \<times> 'b) set" assume "open S" |
160 fix S :: "('a \<times> 'b) set" |
|
161 assume "open S" |
152 then show "\<exists>X\<subseteq>A \<times> B. (\<Union>(a,b)\<in>X. a \<times> b) = S" |
162 then show "\<exists>X\<subseteq>A \<times> B. (\<Union>(a,b)\<in>X. a \<times> b) = S" |
153 proof (safe intro!: exI[of _ "{x\<in>A \<times> B. fst x \<times> snd x \<subseteq> S}"]) |
163 proof (safe intro!: exI[of _ "{x\<in>A \<times> B. fst x \<times> snd x \<subseteq> S}"]) |
154 fix x y assume "(x, y) \<in> S" |
164 fix x y |
|
165 assume "(x, y) \<in> S" |
155 from open_prod_elim[OF `open S` this] |
166 from open_prod_elim[OF `open S` this] |
156 obtain a b where a: "open a""x \<in> a" and b: "open b" "y \<in> b" and "a \<times> b \<subseteq> S" |
167 obtain a b where a: "open a""x \<in> a" and b: "open b" "y \<in> b" and "a \<times> b \<subseteq> S" |
157 by (metis mem_Sigma_iff) |
168 by (metis mem_Sigma_iff) |
158 moreover from topological_basisE[OF A a] guess A0 . |
169 moreover from topological_basisE[OF A a] guess A0 . |
159 moreover from topological_basisE[OF B b] guess B0 . |
170 moreover from topological_basisE[OF B b] guess B0 . |
160 ultimately show "(x, y) \<in> (\<Union>(a, b)\<in>{X \<in> A \<times> B. fst X \<times> snd X \<subseteq> S}. a \<times> b)" |
171 ultimately show "(x, y) \<in> (\<Union>(a, b)\<in>{X \<in> A \<times> B. fst X \<times> snd X \<subseteq> S}. a \<times> b)" |
161 by (intro UN_I[of "(A0, B0)"]) auto |
172 by (intro UN_I[of "(A0, B0)"]) auto |
162 qed auto |
173 qed auto |
163 qed (metis A B topological_basis_open open_Times) |
174 qed (metis A B topological_basis_open open_Times) |
164 |
175 |
|
176 |
165 subsection {* Countable Basis *} |
177 subsection {* Countable Basis *} |
166 |
178 |
167 locale countable_basis = |
179 locale countable_basis = |
168 fixes B::"'a::topological_space set set" |
180 fixes B::"'a::topological_space set set" |
169 assumes is_basis: "topological_basis B" |
181 assumes is_basis: "topological_basis B" |
211 "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)" |
225 "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)" |
212 "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<inter> b \<in> A" |
226 "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<inter> b \<in> A" |
213 proof atomize_elim |
227 proof atomize_elim |
214 from first_countable_basisE[of x] guess A' . note A' = this |
228 from first_countable_basisE[of x] guess A' . note A' = this |
215 def A \<equiv> "(\<lambda>N. \<Inter>((\<lambda>n. from_nat_into A' n) ` N)) ` (Collect finite::nat set set)" |
229 def A \<equiv> "(\<lambda>N. \<Inter>((\<lambda>n. from_nat_into A' n) ` N)) ` (Collect finite::nat set set)" |
216 thus "\<exists>A. countable A \<and> (\<forall>a. a \<in> A \<longrightarrow> x \<in> a) \<and> (\<forall>a. a \<in> A \<longrightarrow> open a) \<and> |
230 then show "\<exists>A. countable A \<and> (\<forall>a. a \<in> A \<longrightarrow> x \<in> a) \<and> (\<forall>a. a \<in> A \<longrightarrow> open a) \<and> |
217 (\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)) \<and> (\<forall>a b. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<inter> b \<in> A)" |
231 (\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)) \<and> (\<forall>a b. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<inter> b \<in> A)" |
218 proof (safe intro!: exI[where x=A]) |
232 proof (safe intro!: exI[where x=A]) |
219 show "countable A" unfolding A_def by (intro countable_image countable_Collect_finite) |
233 show "countable A" |
220 fix a assume "a \<in> A" |
234 unfolding A_def by (intro countable_image countable_Collect_finite) |
221 thus "x \<in> a" "open a" using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into) |
235 fix a |
|
236 assume "a \<in> A" |
|
237 then show "x \<in> a" "open a" |
|
238 using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into) |
222 next |
239 next |
223 let ?int = "\<lambda>N. \<Inter>(from_nat_into A' ` N)" |
240 let ?int = "\<lambda>N. \<Inter>(from_nat_into A' ` N)" |
224 fix a b assume "a \<in> A" "b \<in> A" |
241 fix a b |
225 then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)" by (auto simp: A_def) |
242 assume "a \<in> A" "b \<in> A" |
226 thus "a \<inter> b \<in> A" by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"]) |
243 then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)" |
|
244 by (auto simp: A_def) |
|
245 then show "a \<inter> b \<in> A" |
|
246 by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"]) |
227 next |
247 next |
228 fix S assume "open S" "x \<in> S" then obtain a where a: "a\<in>A'" "a \<subseteq> S" using A' by blast |
248 fix S |
229 thus "\<exists>a\<in>A. a \<subseteq> S" using a A' |
249 assume "open S" "x \<in> S" |
|
250 then obtain a where a: "a\<in>A'" "a \<subseteq> S" using A' by blast |
|
251 then show "\<exists>a\<in>A. a \<subseteq> S" using a A' |
230 by (intro bexI[where x=a]) (auto simp: A_def intro: image_eqI[where x="{to_nat_on A' a}"]) |
252 by (intro bexI[where x=a]) (auto simp: A_def intro: image_eqI[where x="{to_nat_on A' a}"]) |
231 qed |
253 qed |
232 qed |
254 qed |
233 |
255 |
234 lemma (in topological_space) first_countableI: |
256 lemma (in topological_space) first_countableI: |
235 assumes "countable A" and 1: "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a" |
257 assumes "countable A" |
236 and 2: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S" |
258 and 1: "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a" |
|
259 and 2: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S" |
237 shows "\<exists>A::nat \<Rightarrow> 'a set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))" |
260 shows "\<exists>A::nat \<Rightarrow> 'a set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))" |
238 proof (safe intro!: exI[of _ "from_nat_into A"]) |
261 proof (safe intro!: exI[of _ "from_nat_into A"]) |
|
262 fix i |
239 have "A \<noteq> {}" using 2[of UNIV] by auto |
263 have "A \<noteq> {}" using 2[of UNIV] by auto |
240 { fix i show "x \<in> from_nat_into A i" "open (from_nat_into A i)" |
264 show "x \<in> from_nat_into A i" "open (from_nat_into A i)" |
241 using range_from_nat_into_subset[OF `A \<noteq> {}`] 1 by auto } |
265 using range_from_nat_into_subset[OF `A \<noteq> {}`] 1 by auto |
242 { fix S assume "open S" "x\<in>S" from 2[OF this] show "\<exists>i. from_nat_into A i \<subseteq> S" |
266 next |
243 using subset_range_from_nat_into[OF `countable A`] by auto } |
267 fix S |
|
268 assume "open S" "x\<in>S" from 2[OF this] |
|
269 show "\<exists>i. from_nat_into A i \<subseteq> S" |
|
270 using subset_range_from_nat_into[OF `countable A`] by auto |
244 qed |
271 qed |
245 |
272 |
246 instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology |
273 instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology |
247 proof |
274 proof |
248 fix x :: "'a \<times> 'b" |
275 fix x :: "'a \<times> 'b" |
249 from first_countable_basisE[of "fst x"] guess A :: "'a set set" . note A = this |
276 from first_countable_basisE[of "fst x"] guess A :: "'a set set" . note A = this |
250 from first_countable_basisE[of "snd x"] guess B :: "'b set set" . note B = this |
277 from first_countable_basisE[of "snd x"] guess B :: "'b set set" . note B = this |
251 show "\<exists>A::nat \<Rightarrow> ('a \<times> 'b) set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))" |
278 show "\<exists>A::nat \<Rightarrow> ('a \<times> 'b) set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))" |
252 proof (rule first_countableI[of "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"], safe) |
279 proof (rule first_countableI[of "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"], safe) |
253 fix a b assume x: "a \<in> A" "b \<in> B" |
280 fix a b |
|
281 assume x: "a \<in> A" "b \<in> B" |
254 with A(2, 3)[of a] B(2, 3)[of b] show "x \<in> a \<times> b" "open (a \<times> b)" |
282 with A(2, 3)[of a] B(2, 3)[of b] show "x \<in> a \<times> b" "open (a \<times> b)" |
255 unfolding mem_Times_iff by (auto intro: open_Times) |
283 unfolding mem_Times_iff by (auto intro: open_Times) |
256 next |
284 next |
257 fix S assume "open S" "x \<in> S" |
285 fix S |
|
286 assume "open S" "x \<in> S" |
258 from open_prod_elim[OF this] guess a' b' . |
287 from open_prod_elim[OF this] guess a' b' . |
259 moreover with A(4)[of a'] B(4)[of b'] |
288 moreover with A(4)[of a'] B(4)[of b'] |
260 obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'" by auto |
289 obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'" by auto |
261 ultimately show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (A \<times> B). a \<subseteq> S" |
290 ultimately show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (A \<times> B). a \<subseteq> S" |
262 by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b]) |
291 by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b]) |
420 |
458 |
421 subsubsection {* Closed sets *} |
459 subsubsection {* Closed sets *} |
422 |
460 |
423 definition "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)" |
461 definition "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)" |
424 |
462 |
425 lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U" by (metis closedin_def) |
463 lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U" |
426 lemma closedin_empty[simp]: "closedin U {}" by (simp add: closedin_def) |
464 by (metis closedin_def) |
427 lemma closedin_topspace[intro,simp]: |
465 |
428 "closedin U (topspace U)" by (simp add: closedin_def) |
466 lemma closedin_empty[simp]: "closedin U {}" |
|
467 by (simp add: closedin_def) |
|
468 |
|
469 lemma closedin_topspace[intro, simp]: "closedin U (topspace U)" |
|
470 by (simp add: closedin_def) |
|
471 |
429 lemma closedin_Un[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<union> T)" |
472 lemma closedin_Un[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<union> T)" |
430 by (auto simp add: Diff_Un closedin_def) |
473 by (auto simp add: Diff_Un closedin_def) |
431 |
474 |
432 lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union> {A - s|s. s\<in>S}" by auto |
475 lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union> {A - s|s. s\<in>S}" |
433 lemma closedin_Inter[intro]: assumes Ke: "K \<noteq> {}" and Kc: "\<forall>S \<in>K. closedin U S" |
476 by auto |
434 shows "closedin U (\<Inter> K)" using Ke Kc unfolding closedin_def Diff_Inter by auto |
477 |
|
478 lemma closedin_Inter[intro]: |
|
479 assumes Ke: "K \<noteq> {}" |
|
480 and Kc: "\<forall>S \<in>K. closedin U S" |
|
481 shows "closedin U (\<Inter> K)" |
|
482 using Ke Kc unfolding closedin_def Diff_Inter by auto |
435 |
483 |
436 lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)" |
484 lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)" |
437 using closedin_Inter[of "{S,T}" U] by auto |
485 using closedin_Inter[of "{S,T}" U] by auto |
438 |
486 |
439 lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B" by blast |
487 lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B" |
|
488 by blast |
|
489 |
440 lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)" |
490 lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)" |
441 apply (auto simp add: closedin_def Diff_Diff_Int inf_absorb2) |
491 apply (auto simp add: closedin_def Diff_Diff_Int inf_absorb2) |
442 apply (metis openin_subset subset_eq) |
492 apply (metis openin_subset subset_eq) |
443 done |
493 done |
444 |
494 |
445 lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))" |
495 lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))" |
446 by (simp add: openin_closedin_eq) |
496 by (simp add: openin_closedin_eq) |
447 |
497 |
448 lemma openin_diff[intro]: assumes oS: "openin U S" and cT: "closedin U T" shows "openin U (S - T)" |
498 lemma openin_diff[intro]: |
449 proof- |
499 assumes oS: "openin U S" |
|
500 and cT: "closedin U T" |
|
501 shows "openin U (S - T)" |
|
502 proof - |
450 have "S - T = S \<inter> (topspace U - T)" using openin_subset[of U S] oS cT |
503 have "S - T = S \<inter> (topspace U - T)" using openin_subset[of U S] oS cT |
451 by (auto simp add: topspace_def openin_subset) |
504 by (auto simp add: topspace_def openin_subset) |
452 then show ?thesis using oS cT by (auto simp add: closedin_def) |
505 then show ?thesis using oS cT by (auto simp add: closedin_def) |
453 qed |
506 qed |
454 |
507 |
455 lemma closedin_diff[intro]: assumes oS: "closedin U S" and cT: "openin U T" shows "closedin U (S - T)" |
508 lemma closedin_diff[intro]: |
456 proof- |
509 assumes oS: "closedin U S" |
457 have "S - T = S \<inter> (topspace U - T)" using closedin_subset[of U S] oS cT |
510 and cT: "openin U T" |
458 by (auto simp add: topspace_def ) |
511 shows "closedin U (S - T)" |
459 then show ?thesis using oS cT by (auto simp add: openin_closedin_eq) |
512 proof - |
460 qed |
513 have "S - T = S \<inter> (topspace U - T)" |
|
514 using closedin_subset[of U S] oS cT |
|
515 by (auto simp add: topspace_def) |
|
516 then show ?thesis |
|
517 using oS cT by (auto simp add: openin_closedin_eq) |
|
518 qed |
|
519 |
461 |
520 |
462 subsubsection {* Subspace topology *} |
521 subsubsection {* Subspace topology *} |
463 |
522 |
464 definition "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)" |
523 definition "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)" |
465 |
524 |
466 lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)" |
525 lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)" |
467 (is "istopology ?L") |
526 (is "istopology ?L") |
468 proof- |
527 proof - |
469 have "?L {}" by blast |
528 have "?L {}" by blast |
470 {fix A B assume A: "?L A" and B: "?L B" |
529 { |
471 from A B obtain Sa and Sb where Sa: "openin U Sa" "A = Sa \<inter> V" and Sb: "openin U Sb" "B = Sb \<inter> V" by blast |
530 fix A B |
472 have "A\<inter>B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)" using Sa Sb by blast+ |
531 assume A: "?L A" and B: "?L B" |
473 then have "?L (A \<inter> B)" by blast} |
532 from A B obtain Sa and Sb where Sa: "openin U Sa" "A = Sa \<inter> V" and Sb: "openin U Sb" "B = Sb \<inter> V" |
|
533 by blast |
|
534 have "A \<inter> B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)" |
|
535 using Sa Sb by blast+ |
|
536 then have "?L (A \<inter> B)" by blast |
|
537 } |
474 moreover |
538 moreover |
475 {fix K assume K: "K \<subseteq> Collect ?L" |
539 { |
|
540 fix K assume K: "K \<subseteq> Collect ?L" |
476 have th0: "Collect ?L = (\<lambda>S. S \<inter> V) ` Collect (openin U)" |
541 have th0: "Collect ?L = (\<lambda>S. S \<inter> V) ` Collect (openin U)" |
477 apply (rule set_eqI) |
542 apply (rule set_eqI) |
478 apply (simp add: Ball_def image_iff) |
543 apply (simp add: Ball_def image_iff) |
479 by metis |
544 apply metis |
|
545 done |
480 from K[unfolded th0 subset_image_iff] |
546 from K[unfolded th0 subset_image_iff] |
481 obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk" by blast |
547 obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk" |
482 have "\<Union>K = (\<Union>Sk) \<inter> V" using Sk by auto |
548 by blast |
483 moreover have "openin U (\<Union> Sk)" using Sk by (auto simp add: subset_eq) |
549 have "\<Union>K = (\<Union>Sk) \<inter> V" |
484 ultimately have "?L (\<Union>K)" by blast} |
550 using Sk by auto |
|
551 moreover have "openin U (\<Union> Sk)" |
|
552 using Sk by (auto simp add: subset_eq) |
|
553 ultimately have "?L (\<Union>K)" by blast |
|
554 } |
485 ultimately show ?thesis |
555 ultimately show ?thesis |
486 unfolding subset_eq mem_Collect_eq istopology_def by blast |
556 unfolding subset_eq mem_Collect_eq istopology_def by blast |
487 qed |
557 qed |
488 |
558 |
489 lemma openin_subtopology: |
559 lemma openin_subtopology: "openin (subtopology U V) S \<longleftrightarrow> (\<exists>T. openin U T \<and> S = T \<inter> V)" |
490 "openin (subtopology U V) S \<longleftrightarrow> (\<exists> T. (openin U T) \<and> (S = T \<inter> V))" |
|
491 unfolding subtopology_def topology_inverse'[OF istopology_subtopology] |
560 unfolding subtopology_def topology_inverse'[OF istopology_subtopology] |
492 by auto |
561 by auto |
493 |
562 |
494 lemma topspace_subtopology: "topspace(subtopology U V) = topspace U \<inter> V" |
563 lemma topspace_subtopology: "topspace (subtopology U V) = topspace U \<inter> V" |
495 by (auto simp add: topspace_def openin_subtopology) |
564 by (auto simp add: topspace_def openin_subtopology) |
496 |
565 |
497 lemma closedin_subtopology: |
566 lemma closedin_subtopology: "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)" |
498 "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)" |
|
499 unfolding closedin_def topspace_subtopology |
567 unfolding closedin_def topspace_subtopology |
500 apply (simp add: openin_subtopology) |
568 apply (simp add: openin_subtopology) |
501 apply (rule iffI) |
569 apply (rule iffI) |
502 apply clarify |
570 apply clarify |
503 apply (rule_tac x="topspace U - T" in exI) |
571 apply (rule_tac x="topspace U - T" in exI) |
504 by auto |
572 apply auto |
|
573 done |
505 |
574 |
506 lemma openin_subtopology_refl: "openin (subtopology U V) V \<longleftrightarrow> V \<subseteq> topspace U" |
575 lemma openin_subtopology_refl: "openin (subtopology U V) V \<longleftrightarrow> V \<subseteq> topspace U" |
507 unfolding openin_subtopology |
576 unfolding openin_subtopology |
508 apply (rule iffI, clarify) |
577 apply (rule iffI, clarify) |
509 apply (frule openin_subset[of U]) apply blast |
578 apply (frule openin_subset[of U]) |
|
579 apply blast |
510 apply (rule exI[where x="topspace U"]) |
580 apply (rule exI[where x="topspace U"]) |
511 apply auto |
581 apply auto |
512 done |
582 done |
513 |
583 |
514 lemma subtopology_superset: |
584 lemma subtopology_superset: |
515 assumes UV: "topspace U \<subseteq> V" |
585 assumes UV: "topspace U \<subseteq> V" |
516 shows "subtopology U V = U" |
586 shows "subtopology U V = U" |
517 proof- |
587 proof - |
518 {fix S |
588 { |
519 {fix T assume T: "openin U T" "S = T \<inter> V" |
589 fix S |
520 from T openin_subset[OF T(1)] UV have eq: "S = T" by blast |
590 { |
521 have "openin U S" unfolding eq using T by blast} |
591 fix T |
|
592 assume T: "openin U T" "S = T \<inter> V" |
|
593 from T openin_subset[OF T(1)] UV have eq: "S = T" |
|
594 by blast |
|
595 have "openin U S" |
|
596 unfolding eq using T by blast |
|
597 } |
522 moreover |
598 moreover |
523 {assume S: "openin U S" |
599 { |
524 hence "\<exists>T. openin U T \<and> S = T \<inter> V" |
600 assume S: "openin U S" |
525 using openin_subset[OF S] UV by auto} |
601 then have "\<exists>T. openin U T \<and> S = T \<inter> V" |
526 ultimately have "(\<exists>T. openin U T \<and> S = T \<inter> V) \<longleftrightarrow> openin U S" by blast} |
602 using openin_subset[OF S] UV by auto |
527 then show ?thesis unfolding topology_eq openin_subtopology by blast |
603 } |
|
604 ultimately have "(\<exists>T. openin U T \<and> S = T \<inter> V) \<longleftrightarrow> openin U S" |
|
605 by blast |
|
606 } |
|
607 then show ?thesis |
|
608 unfolding topology_eq openin_subtopology by blast |
528 qed |
609 qed |
529 |
610 |
530 lemma subtopology_topspace[simp]: "subtopology U (topspace U) = U" |
611 lemma subtopology_topspace[simp]: "subtopology U (topspace U) = U" |
531 by (simp add: subtopology_superset) |
612 by (simp add: subtopology_superset) |
532 |
613 |
533 lemma subtopology_UNIV[simp]: "subtopology U UNIV = U" |
614 lemma subtopology_UNIV[simp]: "subtopology U UNIV = U" |
534 by (simp add: subtopology_superset) |
615 by (simp add: subtopology_superset) |
535 |
616 |
|
617 |
536 subsubsection {* The standard Euclidean topology *} |
618 subsubsection {* The standard Euclidean topology *} |
537 |
619 |
538 definition |
620 definition euclidean :: "'a::topological_space topology" |
539 euclidean :: "'a::topological_space topology" where |
621 where "euclidean = topology open" |
540 "euclidean = topology open" |
|
541 |
622 |
542 lemma open_openin: "open S \<longleftrightarrow> openin euclidean S" |
623 lemma open_openin: "open S \<longleftrightarrow> openin euclidean S" |
543 unfolding euclidean_def |
624 unfolding euclidean_def |
544 apply (rule cong[where x=S and y=S]) |
625 apply (rule cong[where x=S and y=S]) |
545 apply (rule topology_inverse[symmetric]) |
626 apply (rule topology_inverse[symmetric]) |
618 unfolding openin_open open_dist by fast |
702 unfolding openin_open open_dist by fast |
619 qed |
703 qed |
620 |
704 |
621 text {* These "transitivity" results are handy too *} |
705 text {* These "transitivity" results are handy too *} |
622 |
706 |
623 lemma openin_trans[trans]: "openin (subtopology euclidean T) S \<Longrightarrow> openin (subtopology euclidean U) T |
707 lemma openin_trans[trans]: |
624 \<Longrightarrow> openin (subtopology euclidean U) S" |
708 "openin (subtopology euclidean T) S \<Longrightarrow> openin (subtopology euclidean U) T \<Longrightarrow> |
|
709 openin (subtopology euclidean U) S" |
625 unfolding open_openin openin_open by blast |
710 unfolding open_openin openin_open by blast |
626 |
711 |
627 lemma openin_open_trans: "openin (subtopology euclidean T) S \<Longrightarrow> open T \<Longrightarrow> open S" |
712 lemma openin_open_trans: "openin (subtopology euclidean T) S \<Longrightarrow> open T \<Longrightarrow> open S" |
628 by (auto simp add: openin_open intro: openin_trans) |
713 by (auto simp add: openin_open intro: openin_trans) |
629 |
714 |
630 lemma closedin_trans[trans]: |
715 lemma closedin_trans[trans]: |
631 "closedin (subtopology euclidean T) S \<Longrightarrow> |
716 "closedin (subtopology euclidean T) S \<Longrightarrow> closedin (subtopology euclidean U) T \<Longrightarrow> |
632 closedin (subtopology euclidean U) T |
717 closedin (subtopology euclidean U) S" |
633 ==> closedin (subtopology euclidean U) S" |
|
634 by (auto simp add: closedin_closed closed_closedin closed_Inter Int_assoc) |
718 by (auto simp add: closedin_closed closed_closedin closed_Inter Int_assoc) |
635 |
719 |
636 lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S" |
720 lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S" |
637 by (auto simp add: closedin_closed intro: closedin_trans) |
721 by (auto simp add: closedin_closed intro: closedin_trans) |
638 |
722 |
639 |
723 |
640 subsection {* Open and closed balls *} |
724 subsection {* Open and closed balls *} |
641 |
725 |
642 definition |
726 definition ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" |
643 ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where |
727 where "ball x e = {y. dist x y < e}" |
644 "ball x e = {y. dist x y < e}" |
728 |
645 |
729 definition cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" |
646 definition |
730 where "cball x e = {y. dist x y \<le> e}" |
647 cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where |
|
648 "cball x e = {y. dist x y \<le> e}" |
|
649 |
731 |
650 lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e" |
732 lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e" |
651 by (simp add: ball_def) |
733 by (simp add: ball_def) |
652 |
734 |
653 lemma mem_cball [simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e" |
735 lemma mem_cball [simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e" |
667 by simp |
749 by simp |
668 |
750 |
669 lemma centre_in_cball: "x \<in> cball x e \<longleftrightarrow> 0 \<le> e" |
751 lemma centre_in_cball: "x \<in> cball x e \<longleftrightarrow> 0 \<le> e" |
670 by simp |
752 by simp |
671 |
753 |
672 lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e" by (simp add: subset_eq) |
754 lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e" |
673 lemma subset_ball[intro]: "d <= e ==> ball x d \<subseteq> ball x e" by (simp add: subset_eq) |
755 by (simp add: subset_eq) |
674 lemma subset_cball[intro]: "d <= e ==> cball x d \<subseteq> cball x e" by (simp add: subset_eq) |
756 |
|
757 lemma subset_ball[intro]: "d <= e ==> ball x d \<subseteq> ball x e" |
|
758 by (simp add: subset_eq) |
|
759 |
|
760 lemma subset_cball[intro]: "d <= e ==> cball x d \<subseteq> cball x e" |
|
761 by (simp add: subset_eq) |
|
762 |
675 lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s" |
763 lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s" |
676 by (simp add: set_eq_iff) arith |
764 by (simp add: set_eq_iff) arith |
677 |
765 |
678 lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s" |
766 lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s" |
679 by (simp add: set_eq_iff) |
767 by (simp add: set_eq_iff) |
680 |
768 |
681 lemma diff_less_iff: "(a::real) - b > 0 \<longleftrightarrow> a > b" |
769 lemma diff_less_iff: |
|
770 "(a::real) - b > 0 \<longleftrightarrow> a > b" |
682 "(a::real) - b < 0 \<longleftrightarrow> a < b" |
771 "(a::real) - b < 0 \<longleftrightarrow> a < b" |
683 "a - b < c \<longleftrightarrow> a < c +b" "a - b > c \<longleftrightarrow> a > c +b" by arith+ |
772 "a - b < c \<longleftrightarrow> a < c + b" "a - b > c \<longleftrightarrow> a > c + b" |
684 lemma diff_le_iff: "(a::real) - b \<ge> 0 \<longleftrightarrow> a \<ge> b" "(a::real) - b \<le> 0 \<longleftrightarrow> a \<le> b" |
773 by arith+ |
685 "a - b \<le> c \<longleftrightarrow> a \<le> c +b" "a - b \<ge> c \<longleftrightarrow> a \<ge> c +b" by arith+ |
774 |
|
775 lemma diff_le_iff: |
|
776 "(a::real) - b \<ge> 0 \<longleftrightarrow> a \<ge> b" |
|
777 "(a::real) - b \<le> 0 \<longleftrightarrow> a \<le> b" |
|
778 "a - b \<le> c \<longleftrightarrow> a \<le> c + b" |
|
779 "a - b \<ge> c \<longleftrightarrow> a \<ge> c + b" |
|
780 by arith+ |
686 |
781 |
687 lemma open_ball[intro, simp]: "open (ball x e)" |
782 lemma open_ball[intro, simp]: "open (ball x e)" |
688 unfolding open_dist ball_def mem_Collect_eq Ball_def |
783 unfolding open_dist ball_def mem_Collect_eq Ball_def |
689 unfolding dist_commute |
784 unfolding dist_commute |
690 apply clarify |
785 apply clarify |
728 fixes x :: "'a\<Colon>euclidean_space" |
823 fixes x :: "'a\<Colon>euclidean_space" |
729 assumes "0 < e" |
824 assumes "0 < e" |
730 shows "\<exists>a b. (\<forall>i\<in>Basis. a \<bullet> i \<in> \<rat> \<and> b \<bullet> i \<in> \<rat> ) \<and> x \<in> box a b \<and> box a b \<subseteq> ball x e" |
825 shows "\<exists>a b. (\<forall>i\<in>Basis. a \<bullet> i \<in> \<rat> \<and> b \<bullet> i \<in> \<rat> ) \<and> x \<in> box a b \<and> box a b \<subseteq> ball x e" |
731 proof - |
826 proof - |
732 def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))" |
827 def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))" |
733 then have e: "0 < e'" using assms by (auto intro!: divide_pos_pos simp: DIM_positive) |
828 then have e: "0 < e'" |
|
829 using assms by (auto intro!: divide_pos_pos simp: DIM_positive) |
734 have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i") |
830 have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i") |
735 proof |
831 proof |
736 fix i from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e show "?th i" by auto |
832 fix i |
|
833 from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e |
|
834 show "?th i" by auto |
737 qed |
835 qed |
738 from choice[OF this] guess a .. note a = this |
836 from choice[OF this] guess a .. note a = this |
739 have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" (is "\<forall>i. ?th i") |
837 have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" (is "\<forall>i. ?th i") |
740 proof |
838 proof |
741 fix i from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e show "?th i" by auto |
839 fix i |
|
840 from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e |
|
841 show "?th i" by auto |
742 qed |
842 qed |
743 from choice[OF this] guess b .. note b = this |
843 from choice[OF this] guess b .. note b = this |
744 let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i" |
844 let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i" |
745 show ?thesis |
845 show ?thesis |
746 proof (rule exI[of _ ?a], rule exI[of _ ?b], safe) |
846 proof (rule exI[of _ ?a], rule exI[of _ ?b], safe) |
747 fix y :: 'a assume *: "y \<in> box ?a ?b" |
847 fix y :: 'a |
|
848 assume *: "y \<in> box ?a ?b" |
748 have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)" |
849 have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)" |
749 unfolding setL2_def[symmetric] by (rule euclidean_dist_l2) |
850 unfolding setL2_def[symmetric] by (rule euclidean_dist_l2) |
750 also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))" |
851 also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))" |
751 proof (rule real_sqrt_less_mono, rule setsum_strict_mono) |
852 proof (rule real_sqrt_less_mono, rule setsum_strict_mono) |
752 fix i :: "'a" assume i: "i \<in> Basis" |
853 fix i :: "'a" |
753 have "a i < y\<bullet>i \<and> y\<bullet>i < b i" using * i by (auto simp: box_def) |
854 assume i: "i \<in> Basis" |
754 moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'" using a by auto |
855 have "a i < y\<bullet>i \<and> y\<bullet>i < b i" |
755 moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'" using b by auto |
856 using * i by (auto simp: box_def) |
756 ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'" by auto |
857 moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'" |
|
858 using a by auto |
|
859 moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'" |
|
860 using b by auto |
|
861 ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'" |
|
862 by auto |
757 then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))" |
863 then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))" |
758 unfolding e'_def by (auto simp: dist_real_def) |
864 unfolding e'_def by (auto simp: dist_real_def) |
759 then have "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2" |
865 then have "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2" |
760 by (rule power_strict_mono) auto |
866 by (rule power_strict_mono) auto |
761 then show "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < e\<^sup>2 / real DIM('a)" |
867 then show "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < e\<^sup>2 / real DIM('a)" |
762 by (simp add: power_divide) |
868 by (simp add: power_divide) |
763 qed auto |
869 qed auto |
764 also have "\<dots> = e" using `0 < e` by (simp add: real_eq_of_nat) |
870 also have "\<dots> = e" |
765 finally show "y \<in> ball x e" by (auto simp: ball_def) |
871 using `0 < e` by (simp add: real_eq_of_nat) |
|
872 finally show "y \<in> ball x e" |
|
873 by (auto simp: ball_def) |
766 qed (insert a b, auto simp: box_def) |
874 qed (insert a b, auto simp: box_def) |
767 qed |
875 qed |
768 |
876 |
769 lemma open_UNION_box: |
877 lemma open_UNION_box: |
770 fixes M :: "'a\<Colon>euclidean_space set" |
878 fixes M :: "'a\<Colon>euclidean_space set" |
790 |
898 |
791 |
899 |
792 subsection{* Connectedness *} |
900 subsection{* Connectedness *} |
793 |
901 |
794 lemma connected_local: |
902 lemma connected_local: |
795 "connected S \<longleftrightarrow> ~(\<exists>e1 e2. |
903 "connected S \<longleftrightarrow> |
796 openin (subtopology euclidean S) e1 \<and> |
904 \<not> (\<exists>e1 e2. |
797 openin (subtopology euclidean S) e2 \<and> |
905 openin (subtopology euclidean S) e1 \<and> |
798 S \<subseteq> e1 \<union> e2 \<and> |
906 openin (subtopology euclidean S) e2 \<and> |
799 e1 \<inter> e2 = {} \<and> |
907 S \<subseteq> e1 \<union> e2 \<and> |
800 ~(e1 = {}) \<and> |
908 e1 \<inter> e2 = {} \<and> |
801 ~(e2 = {}))" |
909 e1 \<noteq> {} \<and> |
802 unfolding connected_def openin_open by (safe, blast+) |
910 e2 \<noteq> {})" |
|
911 unfolding connected_def openin_open by (safe, blast+) |
803 |
912 |
804 lemma exists_diff: |
913 lemma exists_diff: |
805 fixes P :: "'a set \<Rightarrow> bool" |
914 fixes P :: "'a set \<Rightarrow> bool" |
806 shows "(\<exists>S. P(- S)) \<longleftrightarrow> (\<exists>S. P S)" (is "?lhs \<longleftrightarrow> ?rhs") |
915 shows "(\<exists>S. P(- S)) \<longleftrightarrow> (\<exists>S. P S)" (is "?lhs \<longleftrightarrow> ?rhs") |
807 proof- |
916 proof - |
808 {assume "?lhs" hence ?rhs by blast } |
917 { |
|
918 assume "?lhs" |
|
919 then have ?rhs by blast |
|
920 } |
809 moreover |
921 moreover |
810 {fix S assume H: "P S" |
922 { |
|
923 fix S |
|
924 assume H: "P S" |
811 have "S = - (- S)" by auto |
925 have "S = - (- S)" by auto |
812 with H have "P (- (- S))" by metis } |
926 with H have "P (- (- S))" by metis |
|
927 } |
813 ultimately show ?thesis by metis |
928 ultimately show ?thesis by metis |
814 qed |
929 qed |
815 |
930 |
816 lemma connected_clopen: "connected S \<longleftrightarrow> |
931 lemma connected_clopen: "connected S \<longleftrightarrow> |
817 (\<forall>T. openin (subtopology euclidean S) T \<and> |
932 (\<forall>T. openin (subtopology euclidean S) T \<and> |
818 closedin (subtopology euclidean S) T \<longrightarrow> T = {} \<or> T = S)" (is "?lhs \<longleftrightarrow> ?rhs") |
933 closedin (subtopology euclidean S) T \<longrightarrow> T = {} \<or> T = S)" (is "?lhs \<longleftrightarrow> ?rhs") |
819 proof- |
934 proof - |
820 have " \<not> connected S \<longleftrightarrow> (\<exists>e1 e2. open e1 \<and> open (- e2) \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})" |
935 have "\<not> connected S \<longleftrightarrow> |
|
936 (\<exists>e1 e2. open e1 \<and> open (- e2) \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})" |
821 unfolding connected_def openin_open closedin_closed |
937 unfolding connected_def openin_open closedin_closed |
822 apply (subst exists_diff) |
938 apply (subst exists_diff) |
823 apply blast |
939 apply blast |
824 done |
940 done |
825 hence th0: "connected S \<longleftrightarrow> \<not> (\<exists>e2 e1. closed e2 \<and> open e1 \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})" |
941 hence th0: "connected S \<longleftrightarrow> |
|
942 \<not> (\<exists>e2 e1. closed e2 \<and> open e1 \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})" |
826 (is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)") |
943 (is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)") |
827 apply (simp add: closed_def) |
944 apply (simp add: closed_def) |
828 apply metis |
945 apply metis |
829 done |
946 done |
830 |
|
831 have th1: "?rhs \<longleftrightarrow> \<not> (\<exists>t' t. closed t'\<and>t = S\<inter>t' \<and> t\<noteq>{} \<and> t\<noteq>S \<and> (\<exists>t'. open t' \<and> t = S \<inter> t'))" |
947 have th1: "?rhs \<longleftrightarrow> \<not> (\<exists>t' t. closed t'\<and>t = S\<inter>t' \<and> t\<noteq>{} \<and> t\<noteq>S \<and> (\<exists>t'. open t' \<and> t = S \<inter> t'))" |
832 (is "_ \<longleftrightarrow> \<not> (\<exists>t' t. ?Q t' t)") |
948 (is "_ \<longleftrightarrow> \<not> (\<exists>t' t. ?Q t' t)") |
833 unfolding connected_def openin_open closedin_closed by auto |
949 unfolding connected_def openin_open closedin_closed by auto |
834 {fix e2 |
950 { |
835 {fix e1 have "?P e2 e1 \<longleftrightarrow> (\<exists>t. closed e2 \<and> t = S\<inter>e2 \<and> open e1 \<and> t = S\<inter>e1 \<and> t\<noteq>{} \<and> t\<noteq>S)" |
951 fix e2 |
836 by auto} |
952 { |
837 then have "(\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)" by metis} |
953 fix e1 |
838 then have "\<forall>e2. (\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)" by blast |
954 have "?P e2 e1 \<longleftrightarrow> (\<exists>t. closed e2 \<and> t = S\<inter>e2 \<and> open e1 \<and> t = S\<inter>e1 \<and> t\<noteq>{} \<and> t\<noteq>S)" |
839 then show ?thesis unfolding th0 th1 by simp |
955 by auto |
|
956 } |
|
957 then have "(\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)" |
|
958 by metis |
|
959 } |
|
960 then have "\<forall>e2. (\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)" |
|
961 by blast |
|
962 then show ?thesis |
|
963 unfolding th0 th1 by simp |
840 qed |
964 qed |
841 |
965 |
842 lemma connected_empty[simp, intro]: "connected {}" (* FIXME duplicate? *) |
966 lemma connected_empty[simp, intro]: "connected {}" (* FIXME duplicate? *) |
843 by simp |
967 by simp |
844 |
968 |
845 |
969 |
846 subsection{* Limit points *} |
970 subsection{* Limit points *} |
847 |
971 |
848 definition (in topological_space) |
972 definition (in topological_space) islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60) |
849 islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60) where |
973 where "x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))" |
850 "x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))" |
|
851 |
974 |
852 lemma islimptI: |
975 lemma islimptI: |
853 assumes "\<And>T. x \<in> T \<Longrightarrow> open T \<Longrightarrow> \<exists>y\<in>S. y \<in> T \<and> y \<noteq> x" |
976 assumes "\<And>T. x \<in> T \<Longrightarrow> open T \<Longrightarrow> \<exists>y\<in>S. y \<in> T \<and> y \<noteq> x" |
854 shows "x islimpt S" |
977 shows "x islimpt S" |
855 using assms unfolding islimpt_def by auto |
978 using assms unfolding islimpt_def by auto |
905 lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}" |
1028 lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}" |
906 unfolding islimpt_def by auto |
1029 unfolding islimpt_def by auto |
907 |
1030 |
908 lemma finite_set_avoid: |
1031 lemma finite_set_avoid: |
909 fixes a :: "'a::metric_space" |
1032 fixes a :: "'a::metric_space" |
910 assumes fS: "finite S" shows "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d <= dist a x" |
1033 assumes fS: "finite S" |
911 proof(induct rule: finite_induct[OF fS]) |
1034 shows "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d <= dist a x" |
912 case 1 thus ?case by (auto intro: zero_less_one) |
1035 proof (induct rule: finite_induct[OF fS]) |
|
1036 case 1 |
|
1037 then show ?case by (auto intro: zero_less_one) |
913 next |
1038 next |
914 case (2 x F) |
1039 case (2 x F) |
915 from 2 obtain d where d: "d >0" "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> d \<le> dist a x" by blast |
1040 from 2 obtain d where d: "d >0" "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> d \<le> dist a x" |
916 {assume "x = a" hence ?case using d by auto } |
1041 by blast |
917 moreover |
1042 show ?case |
918 {assume xa: "x\<noteq>a" |
1043 proof (cases "x = a") |
|
1044 case True |
|
1045 then show ?thesis using d by auto |
|
1046 next |
|
1047 case False |
919 let ?d = "min d (dist a x)" |
1048 let ?d = "min d (dist a x)" |
920 have dp: "?d > 0" using xa d(1) using dist_nz by auto |
1049 have dp: "?d > 0" |
921 from d have d': "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> ?d \<le> dist a x" by auto |
1050 using False d(1) using dist_nz by auto |
922 with dp xa have ?case by(auto intro!: exI[where x="?d"]) } |
1051 from d have d': "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> ?d \<le> dist a x" |
923 ultimately show ?case by blast |
1052 by auto |
|
1053 with dp False show ?thesis |
|
1054 by (auto intro!: exI[where x="?d"]) |
|
1055 qed |
924 qed |
1056 qed |
925 |
1057 |
926 lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T" |
1058 lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T" |
927 by (simp add: islimpt_iff_eventually eventually_conj_iff) |
1059 by (simp add: islimpt_iff_eventually eventually_conj_iff) |
928 |
1060 |
929 lemma discrete_imp_closed: |
1061 lemma discrete_imp_closed: |
930 fixes S :: "'a::metric_space set" |
1062 fixes S :: "'a::metric_space set" |
931 assumes e: "0 < e" and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x" |
1063 assumes e: "0 < e" |
|
1064 and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x" |
932 shows "closed S" |
1065 shows "closed S" |
933 proof- |
1066 proof - |
934 {fix x assume C: "\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" |
1067 { |
|
1068 fix x |
|
1069 assume C: "\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" |
935 from e have e2: "e/2 > 0" by arith |
1070 from e have e2: "e/2 > 0" by arith |
936 from C[rule_format, OF e2] obtain y where y: "y \<in> S" "y\<noteq>x" "dist y x < e/2" by blast |
1071 from C[rule_format, OF e2] obtain y where y: "y \<in> S" "y\<noteq>x" "dist y x < e/2" |
|
1072 by blast |
937 let ?m = "min (e/2) (dist x y) " |
1073 let ?m = "min (e/2) (dist x y) " |
938 from e2 y(2) have mp: "?m > 0" by (simp add: dist_nz[THEN sym]) |
1074 from e2 y(2) have mp: "?m > 0" |
939 from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z\<noteq>x" "dist z x < ?m" by blast |
1075 by (simp add: dist_nz[THEN sym]) |
|
1076 from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z\<noteq>x" "dist z x < ?m" |
|
1077 by blast |
940 have th: "dist z y < e" using z y |
1078 have th: "dist z y < e" using z y |
941 by (intro dist_triangle_lt [where z=x], simp) |
1079 by (intro dist_triangle_lt [where z=x], simp) |
942 from d[rule_format, OF y(1) z(1) th] y z |
1080 from d[rule_format, OF y(1) z(1) th] y z |
943 have False by (auto simp add: dist_commute)} |
1081 have False by (auto simp add: dist_commute)} |
944 then show ?thesis by (metis islimpt_approachable closed_limpt [where 'a='a]) |
1082 then show ?thesis |
|
1083 by (metis islimpt_approachable closed_limpt [where 'a='a]) |
945 qed |
1084 qed |
946 |
1085 |
947 |
1086 |
948 subsection {* Interior of a Set *} |
1087 subsection {* Interior of a Set *} |
949 |
1088 |
1003 using open_contains_ball_eq [where S="interior S"] |
1142 using open_contains_ball_eq [where S="interior S"] |
1004 by (simp add: open_subset_interior) |
1143 by (simp add: open_subset_interior) |
1005 |
1144 |
1006 lemma interior_limit_point [intro]: |
1145 lemma interior_limit_point [intro]: |
1007 fixes x :: "'a::perfect_space" |
1146 fixes x :: "'a::perfect_space" |
1008 assumes x: "x \<in> interior S" shows "x islimpt S" |
1147 assumes x: "x \<in> interior S" |
|
1148 shows "x islimpt S" |
1009 using x islimpt_UNIV [of x] |
1149 using x islimpt_UNIV [of x] |
1010 unfolding interior_def islimpt_def |
1150 unfolding interior_def islimpt_def |
1011 apply (clarsimp, rename_tac T T') |
1151 apply (clarsimp, rename_tac T T') |
1012 apply (drule_tac x="T \<inter> T'" in spec) |
1152 apply (drule_tac x="T \<inter> T'" in spec) |
1013 apply (auto simp add: open_Int) |
1153 apply (auto simp add: open_Int) |
1014 done |
1154 done |
1015 |
1155 |
1016 lemma interior_closed_Un_empty_interior: |
1156 lemma interior_closed_Un_empty_interior: |
1017 assumes cS: "closed S" and iT: "interior T = {}" |
1157 assumes cS: "closed S" |
|
1158 and iT: "interior T = {}" |
1018 shows "interior (S \<union> T) = interior S" |
1159 shows "interior (S \<union> T) = interior S" |
1019 proof |
1160 proof |
1020 show "interior S \<subseteq> interior (S \<union> T)" |
1161 show "interior S \<subseteq> interior (S \<union> T)" |
1021 by (rule interior_mono, rule Un_upper1) |
1162 by (rule interior_mono) (rule Un_upper1) |
1022 next |
|
1023 show "interior (S \<union> T) \<subseteq> interior S" |
1163 show "interior (S \<union> T) \<subseteq> interior S" |
1024 proof |
1164 proof |
1025 fix x assume "x \<in> interior (S \<union> T)" |
1165 fix x |
|
1166 assume "x \<in> interior (S \<union> T)" |
1026 then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T" .. |
1167 then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T" .. |
1027 show "x \<in> interior S" |
1168 show "x \<in> interior S" |
1028 proof (rule ccontr) |
1169 proof (rule ccontr) |
1029 assume "x \<notin> interior S" |
1170 assume "x \<notin> interior S" |
1030 with `x \<in> R` `open R` obtain y where "y \<in> R - S" |
1171 with `x \<in> R` `open R` obtain y where "y \<in> R - S" |
1320 text{* The expected monotonicity property. *} |
1468 text{* The expected monotonicity property. *} |
1321 |
1469 |
1322 lemma Lim_within_empty: "(f ---> l) (at x within {})" |
1470 lemma Lim_within_empty: "(f ---> l) (at x within {})" |
1323 unfolding tendsto_def eventually_at_filter by simp |
1471 unfolding tendsto_def eventually_at_filter by simp |
1324 |
1472 |
1325 lemma Lim_Un: assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)" |
1473 lemma Lim_Un: |
|
1474 assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)" |
1326 shows "(f ---> l) (at x within (S \<union> T))" |
1475 shows "(f ---> l) (at x within (S \<union> T))" |
1327 using assms unfolding tendsto_def eventually_at_filter |
1476 using assms unfolding tendsto_def eventually_at_filter |
1328 apply clarify |
1477 apply clarify |
1329 apply (drule spec, drule (1) mp, drule (1) mp) |
1478 apply (drule spec, drule (1) mp, drule (1) mp) |
1330 apply (drule spec, drule (1) mp, drule (1) mp) |
1479 apply (drule spec, drule (1) mp, drule (1) mp) |
1331 apply (auto elim: eventually_elim2) |
1480 apply (auto elim: eventually_elim2) |
1332 done |
1481 done |
1333 |
1482 |
1334 lemma Lim_Un_univ: |
1483 lemma Lim_Un_univ: |
1335 "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow> S \<union> T = UNIV |
1484 "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow> |
1336 ==> (f ---> l) (at x)" |
1485 S \<union> T = UNIV \<Longrightarrow> (f ---> l) (at x)" |
1337 by (metis Lim_Un) |
1486 by (metis Lim_Un) |
1338 |
1487 |
1339 text{* Interrelations between restricted and unrestricted limits. *} |
1488 text{* Interrelations between restricted and unrestricted limits. *} |
1340 |
|
1341 |
1489 |
1342 lemma Lim_at_within: (* FIXME: rename *) |
1490 lemma Lim_at_within: (* FIXME: rename *) |
1343 "(f ---> l) (at x) \<Longrightarrow> (f ---> l) (at x within S)" |
1491 "(f ---> l) (at x) \<Longrightarrow> (f ---> l) (at x within S)" |
1344 by (metis order_refl filterlim_mono subset_UNIV at_le) |
1492 by (metis order_refl filterlim_mono subset_UNIV at_le) |
1345 |
1493 |
1346 lemma eventually_within_interior: |
1494 lemma eventually_within_interior: |
1347 assumes "x \<in> interior S" |
1495 assumes "x \<in> interior S" |
1348 shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" (is "?lhs = ?rhs") |
1496 shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" |
1349 proof - |
1497 (is "?lhs = ?rhs") |
|
1498 proof |
1350 from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" .. |
1499 from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" .. |
1351 { assume "?lhs" |
1500 { |
|
1501 assume "?lhs" |
1352 then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y" |
1502 then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y" |
1353 unfolding eventually_at_topological |
1503 unfolding eventually_at_topological |
1354 by auto |
1504 by auto |
1355 with T have "open (A \<inter> T)" "x \<in> A \<inter> T" "\<forall>y\<in>(A \<inter> T). y \<noteq> x \<longrightarrow> P y" |
1505 with T have "open (A \<inter> T)" "x \<in> A \<inter> T" "\<forall>y\<in>(A \<inter> T). y \<noteq> x \<longrightarrow> P y" |
1356 by auto |
1506 by auto |
1357 then have "?rhs" |
1507 then show "?rhs" |
1358 unfolding eventually_at_topological by auto |
1508 unfolding eventually_at_topological by auto |
1359 } |
1509 next |
1360 moreover |
1510 assume "?rhs" |
1361 { assume "?rhs" hence "?lhs" |
1511 then show "?lhs" |
1362 by (auto elim: eventually_elim1 simp: eventually_at_filter) |
1512 by (auto elim: eventually_elim1 simp: eventually_at_filter) |
1363 } |
1513 } |
1364 ultimately show "?thesis" .. |
|
1365 qed |
1514 qed |
1366 |
1515 |
1367 lemma at_within_interior: |
1516 lemma at_within_interior: |
1368 "x \<in> interior S \<Longrightarrow> at x within S = at x" |
1517 "x \<in> interior S \<Longrightarrow> at x within S = at x" |
1369 unfolding filter_eq_iff by (intro allI eventually_within_interior) |
1518 unfolding filter_eq_iff by (intro allI eventually_within_interior) |
1377 |
1526 |
1378 lemma Lim_right_bound: |
1527 lemma Lim_right_bound: |
1379 fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder, no_top} \<Rightarrow> |
1528 fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder, no_top} \<Rightarrow> |
1380 'b::{linorder_topology, conditionally_complete_linorder}" |
1529 'b::{linorder_topology, conditionally_complete_linorder}" |
1381 assumes mono: "\<And>a b. a \<in> I \<Longrightarrow> b \<in> I \<Longrightarrow> x < a \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b" |
1530 assumes mono: "\<And>a b. a \<in> I \<Longrightarrow> b \<in> I \<Longrightarrow> x < a \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b" |
1382 assumes bnd: "\<And>a. a \<in> I \<Longrightarrow> x < a \<Longrightarrow> K \<le> f a" |
1531 and bnd: "\<And>a. a \<in> I \<Longrightarrow> x < a \<Longrightarrow> K \<le> f a" |
1383 shows "(f ---> Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))" |
1532 shows "(f ---> Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))" |
1384 proof cases |
1533 proof cases |
1385 assume "{x<..} \<inter> I = {}" then show ?thesis by (simp add: Lim_within_empty) |
1534 assume "{x<..} \<inter> I = {}" |
|
1535 then show ?thesis by (simp add: Lim_within_empty) |
1386 next |
1536 next |
1387 assume e: "{x<..} \<inter> I \<noteq> {}" |
1537 assume e: "{x<..} \<inter> I \<noteq> {}" |
1388 show ?thesis |
1538 show ?thesis |
1389 proof (rule order_tendstoI) |
1539 proof (rule order_tendstoI) |
1390 fix a assume a: "a < Inf (f ` ({x<..} \<inter> I))" |
1540 fix a assume a: "a < Inf (f ` ({x<..} \<inter> I))" |
1391 { fix y assume "y \<in> {x<..} \<inter> I" |
1541 { |
|
1542 fix y |
|
1543 assume "y \<in> {x<..} \<inter> I" |
1392 with e bnd have "Inf (f ` ({x<..} \<inter> I)) \<le> f y" |
1544 with e bnd have "Inf (f ` ({x<..} \<inter> I)) \<le> f y" |
1393 by (auto intro: cInf_lower) |
1545 by (auto intro: cInf_lower) |
1394 with a have "a < f y" by (blast intro: less_le_trans) } |
1546 with a have "a < f y" |
|
1547 by (blast intro: less_le_trans) |
|
1548 } |
1395 then show "eventually (\<lambda>x. a < f x) (at x within ({x<..} \<inter> I))" |
1549 then show "eventually (\<lambda>x. a < f x) (at x within ({x<..} \<inter> I))" |
1396 by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one) |
1550 by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one) |
1397 next |
1551 next |
1398 fix a assume "Inf (f ` ({x<..} \<inter> I)) < a" |
1552 fix a |
1399 from cInf_lessD[OF _ this] e obtain y where y: "x < y" "y \<in> I" "f y < a" by auto |
1553 assume "Inf (f ` ({x<..} \<inter> I)) < a" |
|
1554 from cInf_lessD[OF _ this] e obtain y where y: "x < y" "y \<in> I" "f y < a" |
|
1555 by auto |
1400 then have "eventually (\<lambda>x. x \<in> I \<longrightarrow> f x < a) (at_right x)" |
1556 then have "eventually (\<lambda>x. x \<in> I \<longrightarrow> f x < a) (at_right x)" |
1401 unfolding eventually_at_right by (metis less_imp_le le_less_trans mono) |
1557 unfolding eventually_at_right by (metis less_imp_le le_less_trans mono) |
1402 then show "eventually (\<lambda>x. f x < a) (at x within ({x<..} \<inter> I))" |
1558 then show "eventually (\<lambda>x. f x < a) (at x within ({x<..} \<inter> I))" |
1403 unfolding eventually_at_filter by eventually_elim simp |
1559 unfolding eventually_at_filter by eventually_elim simp |
1404 qed |
1560 qed |
1412 (is "?lhs = ?rhs") |
1568 (is "?lhs = ?rhs") |
1413 proof |
1569 proof |
1414 assume ?lhs |
1570 assume ?lhs |
1415 from countable_basis_at_decseq[of x] guess A . note A = this |
1571 from countable_basis_at_decseq[of x] guess A . note A = this |
1416 def f \<equiv> "\<lambda>n. SOME y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y" |
1572 def f \<equiv> "\<lambda>n. SOME y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y" |
1417 { fix n |
1573 { |
|
1574 fix n |
1418 from `?lhs` have "\<exists>y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y" |
1575 from `?lhs` have "\<exists>y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y" |
1419 unfolding islimpt_def using A(1,2)[of n] by auto |
1576 unfolding islimpt_def using A(1,2)[of n] by auto |
1420 then have "f n \<in> S \<and> f n \<in> A n \<and> x \<noteq> f n" |
1577 then have "f n \<in> S \<and> f n \<in> A n \<and> x \<noteq> f n" |
1421 unfolding f_def by (rule someI_ex) |
1578 unfolding f_def by (rule someI_ex) |
1422 then have "f n \<in> S" "f n \<in> A n" "x \<noteq> f n" by auto } |
1579 then have "f n \<in> S" "f n \<in> A n" "x \<noteq> f n" by auto |
|
1580 } |
1423 then have "\<forall>n. f n \<in> S - {x}" by auto |
1581 then have "\<forall>n. f n \<in> S - {x}" by auto |
1424 moreover have "(\<lambda>n. f n) ----> x" |
1582 moreover have "(\<lambda>n. f n) ----> x" |
1425 proof (rule topological_tendstoI) |
1583 proof (rule topological_tendstoI) |
1426 fix S assume "open S" "x \<in> S" |
1584 fix S |
|
1585 assume "open S" "x \<in> S" |
1427 from A(3)[OF this] `\<And>n. f n \<in> A n` |
1586 from A(3)[OF this] `\<And>n. f n \<in> A n` |
1428 show "eventually (\<lambda>x. f x \<in> S) sequentially" by (auto elim!: eventually_elim1) |
1587 show "eventually (\<lambda>x. f x \<in> S) sequentially" |
|
1588 by (auto elim!: eventually_elim1) |
1429 qed |
1589 qed |
1430 ultimately show ?rhs by fast |
1590 ultimately show ?rhs by fast |
1431 next |
1591 next |
1432 assume ?rhs |
1592 assume ?rhs |
1433 then obtain f :: "nat \<Rightarrow> 'a" where f: "\<And>n. f n \<in> S - {x}" and lim: "f ----> x" by auto |
1593 then obtain f :: "nat \<Rightarrow> 'a" where f: "\<And>n. f n \<in> S - {x}" and lim: "f ----> x" |
|
1594 by auto |
1434 show ?lhs |
1595 show ?lhs |
1435 unfolding islimpt_def |
1596 unfolding islimpt_def |
1436 proof safe |
1597 proof safe |
1437 fix T assume "open T" "x \<in> T" |
1598 fix T |
|
1599 assume "open T" "x \<in> T" |
1438 from lim[THEN topological_tendstoD, OF this] f |
1600 from lim[THEN topological_tendstoD, OF this] f |
1439 show "\<exists>y\<in>S. y \<in> T \<and> y \<noteq> x" |
1601 show "\<exists>y\<in>S. y \<in> T \<and> y \<noteq> x" |
1440 unfolding eventually_sequentially by auto |
1602 unfolding eventually_sequentially by auto |
1441 qed |
1603 qed |
1442 qed |
1604 qed |
1443 |
1605 |
1444 lemma Lim_inv: (* TODO: delete *) |
1606 lemma Lim_inv: (* TODO: delete *) |
1445 fixes f :: "'a \<Rightarrow> real" and A :: "'a filter" |
1607 fixes f :: "'a \<Rightarrow> real" |
1446 assumes "(f ---> l) A" and "l \<noteq> 0" |
1608 and A :: "'a filter" |
|
1609 assumes "(f ---> l) A" |
|
1610 and "l \<noteq> 0" |
1447 shows "((inverse o f) ---> inverse l) A" |
1611 shows "((inverse o f) ---> inverse l) A" |
1448 unfolding o_def using assms by (rule tendsto_inverse) |
1612 unfolding o_def using assms by (rule tendsto_inverse) |
1449 |
1613 |
1450 lemma Lim_null: |
1614 lemma Lim_null: |
1451 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
1615 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
1457 assumes "eventually (\<lambda>x. norm (f x) \<le> g x) net" "(g ---> 0) net" |
1621 assumes "eventually (\<lambda>x. norm (f x) \<le> g x) net" "(g ---> 0) net" |
1458 shows "(f ---> 0) net" |
1622 shows "(f ---> 0) net" |
1459 proof (rule metric_tendsto_imp_tendsto) |
1623 proof (rule metric_tendsto_imp_tendsto) |
1460 show "(g ---> 0) net" by fact |
1624 show "(g ---> 0) net" by fact |
1461 show "eventually (\<lambda>x. dist (f x) 0 \<le> dist (g x) 0) net" |
1625 show "eventually (\<lambda>x. dist (f x) 0 \<le> dist (g x) 0) net" |
1462 using assms(1) by (rule eventually_elim1, simp add: dist_norm) |
1626 using assms(1) by (rule eventually_elim1) (simp add: dist_norm) |
1463 qed |
1627 qed |
1464 |
1628 |
1465 lemma Lim_transform_bound: |
1629 lemma Lim_transform_bound: |
1466 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
1630 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
1467 fixes g :: "'a \<Rightarrow> 'c::real_normed_vector" |
1631 and g :: "'a \<Rightarrow> 'c::real_normed_vector" |
1468 assumes "eventually (\<lambda>n. norm(f n) <= norm(g n)) net" "(g ---> 0) net" |
1632 assumes "eventually (\<lambda>n. norm(f n) <= norm(g n)) net" |
|
1633 and "(g ---> 0) net" |
1469 shows "(f ---> 0) net" |
1634 shows "(f ---> 0) net" |
1470 using assms(1) tendsto_norm_zero [OF assms(2)] |
1635 using assms(1) tendsto_norm_zero [OF assms(2)] |
1471 by (rule Lim_null_comparison) |
1636 by (rule Lim_null_comparison) |
1472 |
1637 |
1473 text{* Deducing things about the limit from the elements. *} |
1638 text{* Deducing things about the limit from the elements. *} |
1474 |
1639 |
1475 lemma Lim_in_closed_set: |
1640 lemma Lim_in_closed_set: |
1476 assumes "closed S" "eventually (\<lambda>x. f(x) \<in> S) net" "\<not>(trivial_limit net)" "(f ---> l) net" |
1641 assumes "closed S" |
|
1642 and "eventually (\<lambda>x. f(x) \<in> S) net" |
|
1643 and "\<not>(trivial_limit net)" "(f ---> l) net" |
1477 shows "l \<in> S" |
1644 shows "l \<in> S" |
1478 proof (rule ccontr) |
1645 proof (rule ccontr) |
1479 assume "l \<notin> S" |
1646 assume "l \<notin> S" |
1480 with `closed S` have "open (- S)" "l \<in> - S" |
1647 with `closed S` have "open (- S)" "l \<in> - S" |
1481 by (simp_all add: open_Compl) |
1648 by (simp_all add: open_Compl) |
1488 qed |
1655 qed |
1489 |
1656 |
1490 text{* Need to prove closed(cball(x,e)) before deducing this as a corollary. *} |
1657 text{* Need to prove closed(cball(x,e)) before deducing this as a corollary. *} |
1491 |
1658 |
1492 lemma Lim_dist_ubound: |
1659 lemma Lim_dist_ubound: |
1493 assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. dist a (f x) <= e) net" |
1660 assumes "\<not>(trivial_limit net)" |
|
1661 and "(f ---> l) net" |
|
1662 and "eventually (\<lambda>x. dist a (f x) <= e) net" |
1494 shows "dist a l <= e" |
1663 shows "dist a l <= e" |
1495 proof - |
1664 proof - |
1496 have "dist a l \<in> {..e}" |
1665 have "dist a l \<in> {..e}" |
1497 proof (rule Lim_in_closed_set) |
1666 proof (rule Lim_in_closed_set) |
1498 show "closed {..e}" by simp |
1667 show "closed {..e}" |
1499 show "eventually (\<lambda>x. dist a (f x) \<in> {..e}) net" by (simp add: assms) |
1668 by simp |
1500 show "\<not> trivial_limit net" by fact |
1669 show "eventually (\<lambda>x. dist a (f x) \<in> {..e}) net" |
1501 show "((\<lambda>x. dist a (f x)) ---> dist a l) net" by (intro tendsto_intros assms) |
1670 by (simp add: assms) |
|
1671 show "\<not> trivial_limit net" |
|
1672 by fact |
|
1673 show "((\<lambda>x. dist a (f x)) ---> dist a l) net" |
|
1674 by (intro tendsto_intros assms) |
1502 qed |
1675 qed |
1503 thus ?thesis by simp |
1676 then show ?thesis by simp |
1504 qed |
1677 qed |
1505 |
1678 |
1506 lemma Lim_norm_ubound: |
1679 lemma Lim_norm_ubound: |
1507 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
1680 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
1508 assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) <= e) net" |
1681 assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) \<le> e) net" |
1509 shows "norm(l) <= e" |
1682 shows "norm(l) \<le> e" |
1510 proof - |
1683 proof - |
1511 have "norm l \<in> {..e}" |
1684 have "norm l \<in> {..e}" |
1512 proof (rule Lim_in_closed_set) |
1685 proof (rule Lim_in_closed_set) |
1513 show "closed {..e}" by simp |
1686 show "closed {..e}" |
1514 show "eventually (\<lambda>x. norm (f x) \<in> {..e}) net" by (simp add: assms) |
1687 by simp |
1515 show "\<not> trivial_limit net" by fact |
1688 show "eventually (\<lambda>x. norm (f x) \<in> {..e}) net" |
1516 show "((\<lambda>x. norm (f x)) ---> norm l) net" by (intro tendsto_intros assms) |
1689 by (simp add: assms) |
|
1690 show "\<not> trivial_limit net" |
|
1691 by fact |
|
1692 show "((\<lambda>x. norm (f x)) ---> norm l) net" |
|
1693 by (intro tendsto_intros assms) |
1517 qed |
1694 qed |
1518 thus ?thesis by simp |
1695 then show ?thesis by simp |
1519 qed |
1696 qed |
1520 |
1697 |
1521 lemma Lim_norm_lbound: |
1698 lemma Lim_norm_lbound: |
1522 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
1699 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
1523 assumes "\<not> (trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. e <= norm(f x)) net" |
1700 assumes "\<not> (trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. e <= norm(f x)) net" |
1524 shows "e \<le> norm l" |
1701 shows "e \<le> norm l" |
1525 proof - |
1702 proof - |
1526 have "norm l \<in> {e..}" |
1703 have "norm l \<in> {e..}" |
1527 proof (rule Lim_in_closed_set) |
1704 proof (rule Lim_in_closed_set) |
1528 show "closed {e..}" by simp |
1705 show "closed {e..}" |
1529 show "eventually (\<lambda>x. norm (f x) \<in> {e..}) net" by (simp add: assms) |
1706 by simp |
1530 show "\<not> trivial_limit net" by fact |
1707 show "eventually (\<lambda>x. norm (f x) \<in> {e..}) net" |
1531 show "((\<lambda>x. norm (f x)) ---> norm l) net" by (intro tendsto_intros assms) |
1708 by (simp add: assms) |
|
1709 show "\<not> trivial_limit net" |
|
1710 by fact |
|
1711 show "((\<lambda>x. norm (f x)) ---> norm l) net" |
|
1712 by (intro tendsto_intros assms) |
1532 qed |
1713 qed |
1533 thus ?thesis by simp |
1714 then show ?thesis by simp |
1534 qed |
1715 qed |
1535 |
1716 |
1536 text{* Limit under bilinear function *} |
1717 text{* Limit under bilinear function *} |
1537 |
1718 |
1538 lemma Lim_bilinear: |
1719 lemma Lim_bilinear: |