equal
deleted
inserted
replaced
2797 unfolding complete_def |
2797 unfolding complete_def |
2798 proof clarify |
2798 proof clarify |
2799 fix \<sigma> |
2799 fix \<sigma> |
2800 assume \<sigma>: "\<forall>n. \<sigma> n \<in> S" and "Cauchy \<sigma>" |
2800 assume \<sigma>: "\<forall>n. \<sigma> n \<in> S" and "Cauchy \<sigma>" |
2801 have "Cauchy (f o \<sigma>)" |
2801 have "Cauchy (f o \<sigma>)" |
2802 using uniformly_continuous_imp_Cauchy_continuous \<open>Cauchy \<sigma>\<close> \<sigma> contf by blast |
2802 using uniformly_continuous_imp_Cauchy_continuous \<open>Cauchy \<sigma>\<close> \<sigma> contf |
|
2803 unfolding Cauchy_continuous_on_def by blast |
2803 then obtain l where "(f \<circ> \<sigma>) \<longlonglongrightarrow> l" |
2804 then obtain l where "(f \<circ> \<sigma>) \<longlonglongrightarrow> l" |
2804 by (auto simp: convergent_eq_Cauchy [symmetric]) |
2805 by (auto simp: convergent_eq_Cauchy [symmetric]) |
2805 show "\<exists>l\<in>S. \<sigma> \<longlonglongrightarrow> l" |
2806 show "\<exists>l\<in>S. \<sigma> \<longlonglongrightarrow> l" |
2806 proof |
2807 proof |
2807 show "g l \<in> S" |
2808 show "g l \<in> S" |