src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 45270 d5b5c9259afd
parent 45051 c478d1876371
child 45548 3e2722d66169
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Oct 25 16:37:11 2011 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Oct 27 07:46:57 2011 +0200
     1.3 @@ -5298,12 +5298,12 @@
     1.4      then obtain N where N:"\<forall>n\<ge>N. norm (f (x n) - f (x N)) < e * d"
     1.5        using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]] and e and mult_pos_pos[of e d] by auto
     1.6      { fix n assume "n\<ge>N"
     1.7 -      hence "norm (f (x n - x N)) < e * d" using N[THEN spec[where x=n]] unfolding f.diff[THEN sym] by auto
     1.8 -      moreover have "e * norm (x n - x N) \<le> norm (f (x n - x N))"
     1.9 +      have "e * norm (x n - x N) \<le> norm (f (x n - x N))"
    1.10          using subspace_sub[OF s, of "x n" "x N"] using xs[THEN spec[where x=N]] and xs[THEN spec[where x=n]]
    1.11          using normf[THEN bspec[where x="x n - x N"]] by auto
    1.12 -      ultimately have "norm (x n - x N) < d" using `e>0`
    1.13 -        using mult_left_less_imp_less[of e "norm (x n - x N)" d] by auto   }
    1.14 +      also have "norm (f (x n - x N)) < e * d"
    1.15 +        using `N \<le> n` N unfolding f.diff[THEN sym] by auto
    1.16 +      finally have "norm (x n - x N) < d" using `e>0` by simp }
    1.17      hence "\<exists>N. \<forall>n\<ge>N. norm (x n - x N) < d" by auto }
    1.18    thus ?thesis unfolding cauchy and dist_norm by auto
    1.19  qed