1401 have "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) ---> g x) sequentially" |
1401 have "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) ---> g x) sequentially" |
1402 apply(rule bchoice) unfolding convergent_eq_cauchy |
1402 apply(rule bchoice) unfolding convergent_eq_cauchy |
1403 proof |
1403 proof |
1404 fix x assume "x\<in>s" show "Cauchy (\<lambda>n. f n x)" |
1404 fix x assume "x\<in>s" show "Cauchy (\<lambda>n. f n x)" |
1405 proof(cases "x=x0") |
1405 proof(cases "x=x0") |
1406 case True thus ?thesis using convergent_imp_cauchy[OF assms(5)] by auto |
1406 case True thus ?thesis using LIMSEQ_imp_Cauchy[OF assms(5)] by auto |
1407 next |
1407 next |
1408 case False show ?thesis unfolding Cauchy_def |
1408 case False show ?thesis unfolding Cauchy_def |
1409 proof(rule,rule) |
1409 proof(rule,rule) |
1410 fix e::real assume "e>0" |
1410 fix e::real assume "e>0" |
1411 hence *:"e/2>0" "e/2/norm(x-x0)>0" |
1411 hence *:"e/2>0" "e/2/norm(x-x0)>0" |
1412 using False by (auto intro!: divide_pos_pos) |
1412 using False by (auto intro!: divide_pos_pos) |
1413 guess M using convergent_imp_cauchy[OF assms(5), unfolded Cauchy_def, rule_format,OF *(1)] .. note M=this |
1413 guess M using LIMSEQ_imp_Cauchy[OF assms(5), unfolded Cauchy_def, rule_format,OF *(1)] .. note M=this |
1414 guess N using lem1[rule_format,OF *(2)] .. note N = this |
1414 guess N using lem1[rule_format,OF *(2)] .. note N = this |
1415 show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e" |
1415 show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e" |
1416 apply(rule_tac x="max M N" in exI) |
1416 apply(rule_tac x="max M N" in exI) |
1417 proof(default+) |
1417 proof(default+) |
1418 fix m n assume as:"max M N \<le>m" "max M N\<le>n" |
1418 fix m n assume as:"max M N \<le>m" "max M N\<le>n" |