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
```