1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Aug 08 15:11:38 2011 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Aug 08 15:27:24 2011 -0700
1.3 @@ -2913,36 +2913,83 @@
1.4 qed
1.5
1.6 lemma sequence_infinite_lemma:
1.7 - fixes l :: "'a::metric_space" (* TODO: generalize *)
1.8 - assumes "\<forall>n::nat. (f n \<noteq> l)" "(f ---> l) sequentially"
1.9 + fixes f :: "nat \<Rightarrow> 'a::t1_space"
1.10 + assumes "\<forall>n. f n \<noteq> l" and "(f ---> l) sequentially"
1.11 shows "infinite (range f)"
1.12 proof
1.13 - let ?A = "(\<lambda>x. dist x l) ` range f"
1.14 assume "finite (range f)"
1.15 - hence **:"finite ?A" "?A \<noteq> {}" by auto
1.16 - obtain k where k:"dist (f k) l = Min ?A" using Min_in[OF **] by auto
1.17 - have "0 < Min ?A" using assms(1) unfolding dist_nz unfolding Min_gr_iff[OF **] by auto
1.18 - then obtain N where "dist (f N) l < Min ?A" using assms(2)[unfolded Lim_sequentially, THEN spec[where x="Min ?A"]] by auto
1.19 - moreover have "dist (f N) l \<in> ?A" by auto
1.20 - ultimately show False using Min_le[OF **(1), of "dist (f N) l"] by auto
1.21 -qed
1.22 -
1.23 + hence "closed (range f)" by (rule finite_imp_closed)
1.24 + hence "open (- range f)" by (rule open_Compl)
1.25 + from assms(1) have "l \<in> - range f" by auto
1.26 + from assms(2) have "eventually (\<lambda>n. f n \<in> - range f) sequentially"
1.27 + using `open (- range f)` `l \<in> - range f` by (rule topological_tendstoD)
1.28 + thus False unfolding eventually_sequentially by auto
1.29 +qed
1.30 +
1.31 +lemma closure_insert:
1.32 + fixes x :: "'a::t1_space"
1.33 + shows "closure (insert x s) = insert x (closure s)"
1.34 +apply (rule closure_unique)
1.35 +apply (rule conjI [OF insert_mono [OF closure_subset]])
1.36 +apply (rule conjI [OF closed_insert [OF closed_closure]])
1.37 +apply (simp add: closure_minimal)
1.38 +done
1.39 +
1.40 +lemma islimpt_insert:
1.41 + fixes x :: "'a::t1_space"
1.42 + shows "x islimpt (insert a s) \<longleftrightarrow> x islimpt s"
1.43 +proof
1.44 + assume *: "x islimpt (insert a s)"
1.45 + show "x islimpt s"
1.46 + proof (rule islimptI)
1.47 + fix t assume t: "x \<in> t" "open t"
1.48 + show "\<exists>y\<in>s. y \<in> t \<and> y \<noteq> x"
1.49 + proof (cases "x = a")
1.50 + case True
1.51 + obtain y where "y \<in> insert a s" "y \<in> t" "y \<noteq> x"
1.52 + using * t by (rule islimptE)
1.53 + with `x = a` show ?thesis by auto
1.54 + next
1.55 + case False
1.56 + with t have t': "x \<in> t - {a}" "open (t - {a})"
1.57 + by (simp_all add: open_Diff)
1.58 + obtain y where "y \<in> insert a s" "y \<in> t - {a}" "y \<noteq> x"
1.59 + using * t' by (rule islimptE)
1.60 + thus ?thesis by auto
1.61 + qed
1.62 + qed
1.63 +next
1.64 + assume "x islimpt s" thus "x islimpt (insert a s)"
1.65 + by (rule islimpt_subset) auto
1.66 +qed
1.67 +
1.68 +lemma islimpt_union_finite:
1.69 + fixes x :: "'a::t1_space"
1.70 + shows "finite s \<Longrightarrow> x islimpt (s \<union> t) \<longleftrightarrow> x islimpt t"
1.71 +by (induct set: finite, simp_all add: islimpt_insert)
1.72 +
1.73 lemma sequence_unique_limpt:
1.74 - fixes l :: "'a::metric_space" (* TODO: generalize *)
1.75 - assumes "\<forall>n::nat. (f n \<noteq> l)" "(f ---> l) sequentially" "l' islimpt (range f)"
1.76 + fixes f :: "nat \<Rightarrow> 'a::t2_space"
1.77 + assumes "(f ---> l) sequentially" and "l' islimpt (range f)"
1.78 shows "l' = l"
1.79 -proof(rule ccontr)
1.80 - def e \<equiv> "dist l' l"
1.81 - assume "l' \<noteq> l" hence "e>0" unfolding dist_nz e_def by auto
1.82 - then obtain N::nat where N:"\<forall>n\<ge>N. dist (f n) l < e / 2"
1.83 - using assms(2)[unfolded Lim_sequentially, THEN spec[where x="e/2"]] by auto
1.84 - def d \<equiv> "Min (insert (e/2) ((\<lambda>n. if dist (f n) l' = 0 then e/2 else dist (f n) l') ` {0 .. N}))"
1.85 - have "d>0" using `e>0` unfolding d_def e_def using zero_le_dist[of _ l', unfolded order_le_less] by auto
1.86 - obtain k where k:"f k \<noteq> l'" "dist (f k) l' < d" using `d>0` and assms(3)[unfolded islimpt_approachable, THEN spec[where x="d"]] by auto
1.87 - have "k\<ge>N" using k(1)[unfolded dist_nz] using k(2)[unfolded d_def]
1.88 - by (force simp del: Min.insert_idem)
1.89 - hence "dist l' l < e" using N[THEN spec[where x=k]] using k(2)[unfolded d_def] and dist_triangle_half_r[of "f k" l' e l] by (auto simp del: Min.insert_idem)
1.90 - thus False unfolding e_def by auto
1.91 +proof (rule ccontr)
1.92 + assume "l' \<noteq> l"
1.93 + obtain s t where "open s" "open t" "l' \<in> s" "l \<in> t" "s \<inter> t = {}"
1.94 + using hausdorff [OF `l' \<noteq> l`] by auto
1.95 + have "eventually (\<lambda>n. f n \<in> t) sequentially"
1.96 + using assms(1) `open t` `l \<in> t` by (rule topological_tendstoD)
1.97 + then obtain N where "\<forall>n\<ge>N. f n \<in> t"
1.98 + unfolding eventually_sequentially by auto
1.99 +
1.100 + have "UNIV = {..<N} \<union> {N..}" by auto
1.101 + hence "l' islimpt (f ` ({..<N} \<union> {N..}))" using assms(2) by simp
1.102 + hence "l' islimpt (f ` {..<N} \<union> f ` {N..})" by (simp add: image_Un)
1.103 + hence "l' islimpt (f ` {N..})" by (simp add: islimpt_union_finite)
1.104 + then obtain y where "y \<in> f ` {N..}" "y \<in> s" "y \<noteq> l'"
1.105 + using `l' \<in> s` `open s` by (rule islimptE)
1.106 + then obtain n where "N \<le> n" "f n \<in> s" "f n \<noteq> l'" by auto
1.107 + with `\<forall>n\<ge>N. f n \<in> t` have "f n \<in> s \<inter> t" by simp
1.108 + with `s \<inter> t = {}` show False by simp
1.109 qed
1.110
1.111 lemma bolzano_weierstrass_imp_closed: