2505 moreover have "\<forall>n. f n \<in> closure (range f)" |
2505 moreover have "\<forall>n. f n \<in> closure (range f)" |
2506 using closure_subset [of "range f"] by auto |
2506 using closure_subset [of "range f"] by auto |
2507 ultimately have "\<exists>l\<in>closure (range f). (f ---> l) sequentially" |
2507 ultimately have "\<exists>l\<in>closure (range f). (f ---> l) sequentially" |
2508 using `Cauchy f` unfolding complete_def by auto |
2508 using `Cauchy f` unfolding complete_def by auto |
2509 then show "convergent f" |
2509 then show "convergent f" |
2510 unfolding convergent_def LIMSEQ_conv_tendsto [symmetric] by auto |
2510 unfolding convergent_def by auto |
2511 qed |
2511 qed |
2512 |
2512 |
2513 lemma complete_univ: "complete (UNIV :: 'a::complete_space set)" |
2513 lemma complete_univ: "complete (UNIV :: 'a::complete_space set)" |
2514 proof(simp add: complete_def, rule, rule) |
2514 proof(simp add: complete_def, rule, rule) |
2515 fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f" |
2515 fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f" |
2516 hence "convergent f" by (rule Cauchy_convergent) |
2516 hence "convergent f" by (rule Cauchy_convergent) |
2517 hence "\<exists>l. f ----> l" unfolding convergent_def . |
2517 thus "\<exists>l. f ----> l" unfolding convergent_def . |
2518 thus "\<exists>l. (f ---> l) sequentially" unfolding LIMSEQ_conv_tendsto . |
|
2519 qed |
2518 qed |
2520 |
2519 |
2521 lemma complete_imp_closed: assumes "complete s" shows "closed s" |
2520 lemma complete_imp_closed: assumes "complete s" shows "closed s" |
2522 proof - |
2521 proof - |
2523 { fix x assume "x islimpt s" |
2522 { fix x assume "x islimpt s" |