src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 53015 a1119cf551e8 parent 52625 b74bf6c0e5a1 child 53255 addd7b9b2bff
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 13 14:20:22 2013 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 13 16:25:47 2013 +0200
1.3 @@ -745,7 +745,7 @@
1.4    show ?thesis
1.5    proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
1.6      fix y :: 'a assume *: "y \<in> box ?a ?b"
1.7 -    have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<twosuperior>)"
1.8 +    have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
1.9        unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
1.10      also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
1.11      proof (rule real_sqrt_less_mono, rule setsum_strict_mono)
1.12 @@ -756,9 +756,9 @@
1.13        ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'" by auto
1.14        then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))"
1.15          unfolding e'_def by (auto simp: dist_real_def)
1.16 -      then have "(dist (x \<bullet> i) (y \<bullet> i))\<twosuperior> < (e/sqrt (real (DIM('a))))\<twosuperior>"
1.17 +      then have "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2"
1.18          by (rule power_strict_mono) auto
1.19 -      then show "(dist (x \<bullet> i) (y \<bullet> i))\<twosuperior> < e\<twosuperior> / real DIM('a)"
1.20 +      then show "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < e\<^sup>2 / real DIM('a)"
1.21          by (simp add: power_divide)
1.22      qed auto
1.23      also have "\<dots> = e" using `0 < e` by (simp add: real_eq_of_nat)
1.24 @@ -771,7 +771,7 @@
1.25    assumes "open M"
1.26    defines "a' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
1.27    defines "b' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
1.28 -  defines "I \<equiv> {f\<in>Basis \<rightarrow>\<^isub>E \<rat> \<times> \<rat>. box (a' f) (b' f) \<subseteq> M}"
1.29 +  defines "I \<equiv> {f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. box (a' f) (b' f) \<subseteq> M}"
1.30    shows "M = (\<Union>f\<in>I. box (a' f) (b' f))"
1.31  proof -
1.32    {
1.33 @@ -4747,7 +4747,7 @@
1.34  proof-
1.35    obtain x y a b where "\<forall>z\<in>s. dist x z \<le> a" "\<forall>z\<in>t. dist y z \<le> b"
1.36      using assms [unfolded bounded_def] by auto
1.37 -  then have "\<forall>z\<in>s \<times> t. dist (x, y) z \<le> sqrt (a\<twosuperior> + b\<twosuperior>)"
1.38 +  then have "\<forall>z\<in>s \<times> t. dist (x, y) z \<le> sqrt (a\<^sup>2 + b\<^sup>2)"
1.39      by (auto simp add: dist_Pair_Pair real_sqrt_le_mono add_mono power_mono)
1.40    thus ?thesis unfolding bounded_any_center [where a="(x, y)"] by auto
1.41  qed
1.42 @@ -5500,7 +5500,7 @@
1.43    then have a: "\<And>f. (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i) = a f" by simp
1.44    def b \<equiv> "\<lambda>f :: 'a \<Rightarrow> (real \<times> real). \<Sum>i\<in>Basis. snd (f i) *\<^sub>R i"
1.45    then have b: "\<And>f. (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i) = b f" by simp
1.46 -  def B \<equiv> "(\<lambda>f. box (a f) (b f)) ` (Basis \<rightarrow>\<^isub>E (\<rat> \<times> \<rat>))"
1.47 +  def B \<equiv> "(\<lambda>f. box (a f) (b f)) ` (Basis \<rightarrow>\<^sub>E (\<rat> \<times> \<rat>))"
1.48
1.49    have "Ball B open" by (simp add: B_def open_box)
1.50    moreover have "(\<forall>A. open A \<longrightarrow> (\<exists>B'\<subseteq>B. \<Union>B' = A))"
```