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))"