equal
deleted
inserted
replaced
1996 "x \<in> {x. norm (a - x) = e}" |
1996 "x \<in> {x. norm (a - x) = e}" |
1997 "2 *\<^sub>R a - x = x" |
1997 "2 *\<^sub>R a - x = x" |
1998 apply (rule retract_fixpoint_property[OF *, of "\<lambda>x. scaleR 2 a - x"]) |
1998 apply (rule retract_fixpoint_property[OF *, of "\<lambda>x. scaleR 2 a - x"]) |
1999 apply (blast intro: brouwer_ball[OF assms]) |
1999 apply (blast intro: brouwer_ball[OF assms]) |
2000 apply (intro continuous_intros) |
2000 apply (intro continuous_intros) |
2001 unfolding frontier_cball subset_eq Ball_def image_iff dist_norm |
2001 unfolding frontier_cball subset_eq Ball_def image_iff dist_norm sphere_def |
2002 apply (auto simp add: ** norm_minus_commute) |
2002 apply (auto simp add: ** norm_minus_commute) |
2003 done |
2003 done |
2004 then have "scaleR 2 a = scaleR 1 x + scaleR 1 x" |
2004 then have "scaleR 2 a = scaleR 1 x + scaleR 1 x" |
2005 by (auto simp add: algebra_simps) |
2005 by (auto simp add: algebra_simps) |
2006 then have "a = x" |
2006 then have "a = x" |