4 *) |
4 *) |
5 |
5 |
6 header {* Elementary topology in Euclidean space. *} |
6 header {* Elementary topology in Euclidean space. *} |
7 |
7 |
8 theory Topology_Euclidean_Space |
8 theory Topology_Euclidean_Space |
9 imports SEQ Euclidean_Space |
9 imports SEQ Euclidean_Space Product_Vector |
10 begin |
10 begin |
11 |
11 |
12 declare fstcart_pastecart[simp] sndcart_pastecart[simp] |
12 declare fstcart_pastecart[simp] sndcart_pastecart[simp] |
13 |
13 |
14 subsection{* General notion of a topology *} |
14 subsection{* General notion of a topology *} |
2422 } |
2422 } |
2423 hence *:"((f \<circ> r) ---> l) sequentially" unfolding o_def tendsto_iff by simp |
2423 hence *:"((f \<circ> r) ---> l) sequentially" unfolding o_def tendsto_iff by simp |
2424 with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" by auto |
2424 with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" by auto |
2425 qed |
2425 qed |
2426 |
2426 |
|
2427 lemma bounded_fst: "bounded s \<Longrightarrow> bounded (fst ` s)" |
|
2428 unfolding bounded_def |
|
2429 apply clarify |
|
2430 apply (rule_tac x="a" in exI) |
|
2431 apply (rule_tac x="e" in exI) |
|
2432 apply clarsimp |
|
2433 apply (drule (1) bspec) |
|
2434 apply (simp add: dist_Pair_Pair) |
|
2435 apply (erule order_trans [OF real_sqrt_sum_squares_ge1]) |
|
2436 done |
|
2437 |
|
2438 lemma bounded_snd: "bounded s \<Longrightarrow> bounded (snd ` s)" |
|
2439 unfolding bounded_def |
|
2440 apply clarify |
|
2441 apply (rule_tac x="b" in exI) |
|
2442 apply (rule_tac x="e" in exI) |
|
2443 apply clarsimp |
|
2444 apply (drule (1) bspec) |
|
2445 apply (simp add: dist_Pair_Pair) |
|
2446 apply (erule order_trans [OF real_sqrt_sum_squares_ge2]) |
|
2447 done |
|
2448 |
|
2449 instance "*" :: (heine_borel, heine_borel) heine_borel |
|
2450 proof |
|
2451 fix s :: "('a * 'b) set" and f :: "nat \<Rightarrow> 'a * 'b" |
|
2452 assume s: "bounded s" and f: "\<forall>n. f n \<in> s" |
|
2453 from s have s1: "bounded (fst ` s)" by (rule bounded_fst) |
|
2454 from f have f1: "\<forall>n. fst (f n) \<in> fst ` s" by simp |
|
2455 obtain l1 r1 where r1: "subseq r1" |
|
2456 and l1: "((\<lambda>n. fst (f (r1 n))) ---> l1) sequentially" |
|
2457 using bounded_imp_convergent_subsequence [OF s1 f1] |
|
2458 unfolding o_def by fast |
|
2459 from s have s2: "bounded (snd ` s)" by (rule bounded_snd) |
|
2460 from f have f2: "\<forall>n. snd (f (r1 n)) \<in> snd ` s" by simp |
|
2461 obtain l2 r2 where r2: "subseq r2" |
|
2462 and l2: "((\<lambda>n. snd (f (r1 (r2 n)))) ---> l2) sequentially" |
|
2463 using bounded_imp_convergent_subsequence [OF s2 f2] |
|
2464 unfolding o_def by fast |
|
2465 have l1': "((\<lambda>n. fst (f (r1 (r2 n)))) ---> l1) sequentially" |
|
2466 using lim_subseq [OF r2 l1] unfolding o_def . |
|
2467 have l: "((f \<circ> (r1 \<circ> r2)) ---> (l1, l2)) sequentially" |
|
2468 using tendsto_Pair [OF l1' l2] unfolding o_def by simp |
|
2469 have r: "subseq (r1 \<circ> r2)" |
|
2470 using r1 r2 unfolding subseq_def by simp |
|
2471 show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" |
|
2472 using l r by fast |
|
2473 qed |
|
2474 |
2427 subsection{* Completeness. *} |
2475 subsection{* Completeness. *} |
2428 |
2476 |
2429 lemma cauchy_def: |
2477 lemma cauchy_def: |
2430 "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)" |
2478 "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)" |
2431 unfolding Cauchy_def by blast |
2479 unfolding Cauchy_def by blast |