src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 50937 d249ef928ae1 parent 50936 b28f258ebc1a child 50938 5b193d3dd6b6
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 11:59:12 2013 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 12:09:21 2013 +0100
1.3 @@ -3016,26 +3016,10 @@
1.4      using `l \<in> s` r l by blast
1.5  qed
1.6
1.7 -lemma subseq_bigger: assumes "subseq r" shows "n \<le> r n"
1.8 -proof(induct n)
1.9 -  show "0 \<le> r 0" by auto
1.10 -next
1.11 -  fix n assume "n \<le> r n"
1.12 -  moreover have "r n < r (Suc n)"
1.13 -    using assms [unfolded subseq_def] by auto
1.14 -  ultimately show "Suc n \<le> r (Suc n)" by auto
1.15 -qed
1.16 -
1.17 -lemma eventually_subseq:
1.18 -  assumes r: "subseq r"
1.19 -  shows "eventually P sequentially \<Longrightarrow> eventually (\<lambda>n. P (r n)) sequentially"
1.20 -unfolding eventually_sequentially
1.21 -by (metis subseq_bigger [OF r] le_trans)
1.22 -
1.23  lemma lim_subseq:
1.24    "subseq r \<Longrightarrow> (s ---> l) sequentially \<Longrightarrow> ((s o r) ---> l) sequentially"
1.25  unfolding tendsto_def eventually_sequentially o_def
1.26 -by (metis subseq_bigger le_trans)
1.27 +by (metis seq_suble le_trans)
1.28
1.29  lemma num_Axiom: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
1.30    unfolding Ex1_def
1.31 @@ -3292,7 +3276,7 @@
1.32    { fix f assume as: "(\<forall>n::nat. f n \<in> s)" "Cauchy f"
1.33      from as(1) obtain l r where lr: "l\<in>s" "subseq r" "((f \<circ> r) ---> l) sequentially" using assms unfolding seq_compact_def by blast
1.34
1.35 -    note lr' = subseq_bigger [OF lr(2)]
1.36 +    note lr' = seq_suble [OF lr(2)]
1.37
1.38      { fix e::real assume "e>0"
1.39        from as(2) obtain N where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (f m) (f n) < e/2" unfolding cauchy_def using `e>0` apply (erule_tac x="e/2" in allE) by auto
1.40 @@ -3431,7 +3415,7 @@
1.41    obtain N2::nat where N2:"N2>0" "inverse (real N2) < e /2" using real_arch_inv[of "e/2"] and `e>0` by auto
1.42    have N2':"inverse (real (r (N1 + N2) +1 )) < e/2"
1.43      apply(rule order_less_trans) apply(rule less_imp_inverse_less) using N2
1.44 -    using subseq_bigger[OF r, of "N1 + N2"] by auto
1.45 +    using seq_suble[OF r, of "N1 + N2"] by auto
1.46
1.47    def x \<equiv> "(f (r (N1 + N2)))"
1.48    have x:"\<not> ball x (inverse (real (r (N1 + N2) + 1))) \<subseteq> b" unfolding x_def
1.49 @@ -3771,7 +3755,7 @@
1.50        with lr(3) obtain N where N:"\<forall>m\<ge>N. dist ((x \<circ> r) m) l < e" unfolding LIMSEQ_def by auto
1.51        hence "dist ((x \<circ> r) (max N n)) l < e" by auto
1.52        moreover
1.53 -      have "r (max N n) \<ge> n" using lr(2) using subseq_bigger[of r "max N n"] by auto
1.54 +      have "r (max N n) \<ge> n" using lr(2) using seq_suble[of r "max N n"] by auto
1.55        hence "(x \<circ> r) (max N n) \<in> s n"
1.56          using x apply(erule_tac x=n in allE)
1.57          using x apply(erule_tac x="r (max N n)" in allE)
1.58 @@ -6784,7 +6768,7 @@
1.59        moreover
1.60        have "dist (f (r (Na + Nb + n)) x - f (r (Na + Nb + n)) y) (a - b) \<ge> dist a b - dist (f n x) (f n y)"
1.61          using distf[of n "r (Na+Nb+n)", OF _ `x\<in>s` `y\<in>s`]
1.62 -        using subseq_bigger[OF r, of "Na+Nb+n"]
1.63 +        using seq_suble[OF r, of "Na+Nb+n"]
1.64          using *[of "f (r (Na + Nb + n)) x" "f (r (Na + Nb + n)) y" "f n x" "f n y"] by auto
1.65        ultimately have False by simp
1.66      }
```