src/HOL/Lim.thy
 changeset 44532 a2e9b39df938 parent 44314 dbad46932536 child 44568 e6f291cb5810
equal inserted replaced
44531:1d477a2b1572 44532:a2e9b39df938
`   442 by (rule isUCont [THEN isUCont_Cauchy])`
`   442 by (rule isUCont [THEN isUCont_Cauchy])`
`   443 `
`   443 `
`   444 `
`   444 `
`   445 subsection {* Relation of LIM and LIMSEQ *}`
`   445 subsection {* Relation of LIM and LIMSEQ *}`
`   446 `
`   446 `
`       `
`   447 lemma sequentially_imp_eventually_within:`
`       `
`   448   fixes a :: "'a::metric_space"`
`       `
`   449   assumes "\<forall>f. (\<forall>n. f n \<in> s \<and> f n \<noteq> a) \<and> f ----> a \<longrightarrow>`
`       `
`   450     eventually (\<lambda>n. P (f n)) sequentially"`
`       `
`   451   shows "eventually P (at a within s)"`
`       `
`   452 proof (rule ccontr)`
`       `
`   453   let ?I = "\<lambda>n. inverse (real (Suc n))"`
`       `
`   454   def F \<equiv> "\<lambda>n::nat. SOME x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"`
`       `
`   455   assume "\<not> eventually P (at a within s)"`
`       `
`   456   hence P: "\<forall>d>0. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < d \<and> \<not> P x"`
`       `
`   457     unfolding Limits.eventually_within Limits.eventually_at by fast`
`       `
`   458   hence "\<And>n. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp`
`       `
`   459   hence F: "\<And>n. F n \<in> s \<and> F n \<noteq> a \<and> dist (F n) a < ?I n \<and> \<not> P (F n)"`
`       `
`   460     unfolding F_def by (rule someI_ex)`
`       `
`   461   hence F0: "\<forall>n. F n \<in> s" and F1: "\<forall>n. F n \<noteq> a"`
`       `
`   462     and F2: "\<forall>n. dist (F n) a < ?I n" and F3: "\<forall>n. \<not> P (F n)"`
`       `
`   463     by fast+`
`       `
`   464   from LIMSEQ_inverse_real_of_nat have "F ----> a"`
`       `
`   465     by (rule metric_tendsto_imp_tendsto,`
`       `
`   466       simp add: dist_norm F2 less_imp_le)`
`       `
`   467   hence "eventually (\<lambda>n. P (F n)) sequentially"`
`       `
`   468     using assms F0 F1 by simp`
`       `
`   469   thus "False" by (simp add: F3)`
`       `
`   470 qed`
`       `
`   471 `
`       `
`   472 lemma sequentially_imp_eventually_at:`
`       `
`   473   fixes a :: "'a::metric_space"`
`       `
`   474   assumes "\<forall>f. (\<forall>n. f n \<noteq> a) \<and> f ----> a \<longrightarrow>`
`       `
`   475     eventually (\<lambda>n. P (f n)) sequentially"`
`       `
`   476   shows "eventually P (at a)"`
`       `
`   477   using assms sequentially_imp_eventually_within [where s=UNIV]`
`       `
`   478   unfolding within_UNIV by simp`
`       `
`   479 `
`   447 lemma LIMSEQ_SEQ_conv1:`
`   480 lemma LIMSEQ_SEQ_conv1:`
`   448   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"`
`   481   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"`
`   449   assumes f: "f -- a --> l"`
`   482   assumes f: "f -- a --> l"`
`   450   shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"`
`   483   shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"`
`   451   using tendsto_compose_eventually [OF f, where F=sequentially] by simp`
`   484   using tendsto_compose_eventually [OF f, where F=sequentially] by simp`
`   452 `
`   485 `
`   481 lemma LIMSEQ_SEQ_conv2:`
`   486 lemma LIMSEQ_SEQ_conv2:`
`   482   fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"`
`   487   fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"`
`   483   assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"`
`   488   assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"`
`   484   shows "f -- a --> l"`
`   489   shows "f -- a --> l"`
`   485   using assms unfolding tendsto_def [where l=l]`
`   490   using assms unfolding tendsto_def [where l=l]`
`   486   by (simp add: LIMSEQ_SEQ_conv2_lemma)`
`   491   by (simp add: sequentially_imp_eventually_at)`
`   487 `
`   492 `
`   488 lemma LIMSEQ_SEQ_conv:`
`   493 lemma LIMSEQ_SEQ_conv:`
`   489   "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =`
`   494   "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =`
`   490    (X -- a --> (L::'b::topological_space))"`
`   495    (X -- a --> (L::'b::topological_space))"`
`   491   using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..`
`   496   using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..`