src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 45548 3e2722d66169
parent 45270 d5b5c9259afd
child 45776 714100f5fda4
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Nov 17 15:07:46 2011 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Nov 17 18:31:00 2011 +0100
     1.3 @@ -3861,7 +3861,7 @@
     1.4    then obtain y e where "e>0" and e:"ball y e \<subseteq> s" and y:"x = a + y" unfolding image_iff Bex_def mem_interior by auto
     1.5    { fix z have *:"a + y - z = y + a - z" by auto
     1.6      assume "z\<in>ball x e"
     1.7 -    hence "z - a \<in> s" using e[unfolded subset_eq, THEN bspec[where x="z - a"]] unfolding mem_ball dist_norm y ab_group_add_class.diff_diff_eq2 * by auto
     1.8 +    hence "z - a \<in> s" using e[unfolded subset_eq, THEN bspec[where x="z - a"]] unfolding mem_ball dist_norm y group_add_class.diff_diff_eq2 * by auto
     1.9      hence "z \<in> op + a ` s" unfolding image_iff by(auto intro!: bexI[where x="z - a"])  }
    1.10    hence "ball x e \<subseteq> op + a ` s" unfolding subset_eq by auto
    1.11    thus "x \<in> interior (op + a ` s)" unfolding mem_interior using `e>0` by auto