diff -r 1d477a2b1572 -r a2e9b39df938 src/HOL/Lim.thy --- a/src/HOL/Lim.thy Thu Aug 25 19:41:38 2011 -0700 +++ b/src/HOL/Lim.thy Fri Aug 26 08:12:38 2011 -0700 @@ -444,46 +444,51 @@ subsection {* Relation of LIM and LIMSEQ *} +lemma sequentially_imp_eventually_within: + fixes a :: "'a::metric_space" + assumes "\f. (\n. f n \ s \ f n \ a) \ f ----> a \ + eventually (\n. P (f n)) sequentially" + shows "eventually P (at a within s)" +proof (rule ccontr) + let ?I = "\n. inverse (real (Suc n))" + def F \ "\n::nat. SOME x. x \ s \ x \ a \ dist x a < ?I n \ \ P x" + assume "\ eventually P (at a within s)" + hence P: "\d>0. \x. x \ s \ x \ a \ dist x a < d \ \ P x" + unfolding Limits.eventually_within Limits.eventually_at by fast + hence "\n. \x. x \ s \ x \ a \ dist x a < ?I n \ \ P x" by simp + hence F: "\n. F n \ s \ F n \ a \ dist (F n) a < ?I n \ \ P (F n)" + unfolding F_def by (rule someI_ex) + hence F0: "\n. F n \ s" and F1: "\n. F n \ a" + and F2: "\n. dist (F n) a < ?I n" and F3: "\n. \ P (F n)" + by fast+ + from LIMSEQ_inverse_real_of_nat have "F ----> a" + by (rule metric_tendsto_imp_tendsto, + simp add: dist_norm F2 less_imp_le) + hence "eventually (\n. P (F n)) sequentially" + using assms F0 F1 by simp + thus "False" by (simp add: F3) +qed + +lemma sequentially_imp_eventually_at: + fixes a :: "'a::metric_space" + assumes "\f. (\n. f n \ a) \ f ----> a \ + eventually (\n. P (f n)) sequentially" + shows "eventually P (at a)" + using assms sequentially_imp_eventually_within [where s=UNIV] + unfolding within_UNIV by simp + lemma LIMSEQ_SEQ_conv1: fixes f :: "'a::topological_space \ 'b::topological_space" assumes f: "f -- a --> l" shows "\S. (\n. S n \ a) \ S ----> a \ (\n. f (S n)) ----> l" using tendsto_compose_eventually [OF f, where F=sequentially] by simp -lemma LIMSEQ_SEQ_conv2_lemma: - fixes a :: "'a::metric_space" - assumes "\S. (\n. S n \ a) \ S ----> a \ eventually (\x. P (S x)) sequentially" - shows "eventually P (at a)" -proof (rule ccontr) - let ?I = "\n. inverse (real (Suc n))" - let ?F = "\n::nat. SOME x. x \ a \ dist x a < ?I n \ \ P x" - assume "\ eventually P (at a)" - hence P: "\d>0. \x. x \ a \ dist x a < d \ \ P x" - unfolding eventually_at by simp - hence "\n. \x. x \ a \ dist x a < ?I n \ \ P x" by simp - hence F: "\n. ?F n \ a \ dist (?F n) a < ?I n \ \ P (?F n)" - by (rule someI_ex) - hence F1: "\n. ?F n \ a" - and F2: "\n. dist (?F n) a < ?I n" - and F3: "\n. \ P (?F n)" - by fast+ - have "?F ----> a" - using LIMSEQ_inverse_real_of_nat - by (rule metric_tendsto_imp_tendsto, - simp add: dist_norm F2 [THEN less_imp_le]) - moreover have "\n. ?F n \ a" - by (rule allI) (rule F1) - ultimately have "eventually (\n. P (?F n)) sequentially" - using assms by simp - thus "False" by (simp add: F3) -qed - lemma LIMSEQ_SEQ_conv2: fixes f :: "'a::metric_space \ 'b::topological_space" assumes "\S. (\n. S n \ a) \ S ----> a \ (\n. f (S n)) ----> l" shows "f -- a --> l" using assms unfolding tendsto_def [where l=l] - by (simp add: LIMSEQ_SEQ_conv2_lemma) + by (simp add: sequentially_imp_eventually_at) lemma LIMSEQ_SEQ_conv: "(\S. (\n. S n \ a) \ S ----> (a::'a::metric_space) \ (\n. X (S n)) ----> L) =