3247 unfolding cauchy_def |
3247 unfolding cauchy_def |
3248 using dist_triangle_half_l |
3248 using dist_triangle_half_l |
3249 by blast |
3249 by blast |
3250 qed |
3250 qed |
3251 |
3251 |
3252 lemma convergent_imp_cauchy: |
|
3253 "(s ---> l) sequentially ==> Cauchy s" |
|
3254 proof(simp only: cauchy_def, rule, rule) |
|
3255 fix e::real assume "e>0" "(s ---> l) sequentially" |
|
3256 then obtain N::nat where N:"\<forall>n\<ge>N. dist (s n) l < e/2" unfolding LIMSEQ_def by(erule_tac x="e/2" in allE) auto |
|
3257 thus "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < e" using dist_triangle_half_l[of _ l e _] by (rule_tac x=N in exI) auto |
|
3258 qed |
|
3259 |
|
3260 lemma cauchy_imp_bounded: assumes "Cauchy s" shows "bounded (range s)" |
3252 lemma cauchy_imp_bounded: assumes "Cauchy s" shows "bounded (range s)" |
3261 proof- |
3253 proof- |
3262 from assms obtain N::nat where "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < 1" unfolding cauchy_def apply(erule_tac x= 1 in allE) by auto |
3254 from assms obtain N::nat where "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < 1" unfolding cauchy_def apply(erule_tac x= 1 in allE) by auto |
3263 hence N:"\<forall>n. N \<le> n \<longrightarrow> dist (s N) (s n) < 1" by auto |
3255 hence N:"\<forall>n. N \<le> n \<longrightarrow> dist (s N) (s n) < 1" by auto |
3264 moreover |
3256 moreover |
3321 proof - |
3313 proof - |
3322 { fix x assume "x islimpt s" |
3314 { fix x assume "x islimpt s" |
3323 then obtain f where f: "\<forall>n. f n \<in> s - {x}" "(f ---> x) sequentially" |
3315 then obtain f where f: "\<forall>n. f n \<in> s - {x}" "(f ---> x) sequentially" |
3324 unfolding islimpt_sequential by auto |
3316 unfolding islimpt_sequential by auto |
3325 then obtain l where l: "l\<in>s" "(f ---> l) sequentially" |
3317 then obtain l where l: "l\<in>s" "(f ---> l) sequentially" |
3326 using `complete s`[unfolded complete_def] using convergent_imp_cauchy[of f x] by auto |
3318 using `complete s`[unfolded complete_def] using LIMSEQ_imp_Cauchy[of f x] by auto |
3327 hence "x \<in> s" using tendsto_unique[of sequentially f l x] trivial_limit_sequentially f(2) by auto |
3319 hence "x \<in> s" using tendsto_unique[of sequentially f l x] trivial_limit_sequentially f(2) by auto |
3328 } |
3320 } |
3329 thus "closed s" unfolding closed_limpt by auto |
3321 thus "closed s" unfolding closed_limpt by auto |
3330 qed |
3322 qed |
3331 |
3323 |
3348 unfolding Cauchy_convergent_iff convergent_def .. |
3340 unfolding Cauchy_convergent_iff convergent_def .. |
3349 |
3341 |
3350 lemma convergent_imp_bounded: |
3342 lemma convergent_imp_bounded: |
3351 fixes s :: "nat \<Rightarrow> 'a::metric_space" |
3343 fixes s :: "nat \<Rightarrow> 'a::metric_space" |
3352 shows "(s ---> l) sequentially \<Longrightarrow> bounded (range s)" |
3344 shows "(s ---> l) sequentially \<Longrightarrow> bounded (range s)" |
3353 by (intro cauchy_imp_bounded convergent_imp_cauchy) |
3345 by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy) |
3354 |
3346 |
3355 subsubsection{* Total boundedness *} |
3347 subsubsection{* Total boundedness *} |
3356 |
3348 |
3357 fun helper_1::"('a::metric_space set) \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> 'a" where |
3349 fun helper_1::"('a::metric_space set) \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> 'a" where |
3358 "helper_1 s e n = (SOME y::'a. y \<in> s \<and> (\<forall>m<n. \<not> (dist (helper_1 s e m) y < e)))" |
3350 "helper_1 s e n = (SOME y::'a. y \<in> s \<and> (\<forall>m<n. \<not> (dist (helper_1 s e m) y < e)))" |
3375 apply(rule someI2[where a=z]) unfolding x_def[symmetric] and Q_def using z by auto |
3367 apply(rule someI2[where a=z]) unfolding x_def[symmetric] and Q_def using z by auto |
3376 thus "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)" unfolding Q_def by auto |
3368 thus "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)" unfolding Q_def by auto |
3377 qed } |
3369 qed } |
3378 hence "\<forall>n::nat. x n \<in> s" and x:"\<forall>n. \<forall>m < n. \<not> (dist (x m) (x n) < e)" by blast+ |
3370 hence "\<forall>n::nat. x n \<in> s" and x:"\<forall>n. \<forall>m < n. \<not> (dist (x m) (x n) < e)" by blast+ |
3379 then obtain l r where "l\<in>s" and r:"subseq r" and "((x \<circ> r) ---> l) sequentially" using assms(1)[unfolded seq_compact_def, THEN spec[where x=x]] by auto |
3371 then obtain l r where "l\<in>s" and r:"subseq r" and "((x \<circ> r) ---> l) sequentially" using assms(1)[unfolded seq_compact_def, THEN spec[where x=x]] by auto |
3380 from this(3) have "Cauchy (x \<circ> r)" using convergent_imp_cauchy by auto |
3372 from this(3) have "Cauchy (x \<circ> r)" using LIMSEQ_imp_Cauchy by auto |
3381 then obtain N::nat where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e" unfolding cauchy_def using `e>0` by auto |
3373 then obtain N::nat where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e" unfolding cauchy_def using `e>0` by auto |
3382 show False |
3374 show False |
3383 using N[THEN spec[where x=N], THEN spec[where x="N+1"]] |
3375 using N[THEN spec[where x=N], THEN spec[where x="N+1"]] |
3384 using r[unfolded subseq_def, THEN spec[where x=N], THEN spec[where x="N+1"]] |
3376 using r[unfolded subseq_def, THEN spec[where x=N], THEN spec[where x="N+1"]] |
3385 using x[THEN spec[where x="r (N+1)"], THEN spec[where x="r (N)"]] by auto |
3377 using x[THEN spec[where x="r (N+1)"], THEN spec[where x="r (N)"]] by auto |