tuned;
authorwenzelm
Fri Jul 12 18:16:50 2013 +0200 (2013-07-12)
changeset 52625b74bf6c0e5a1
parent 52624 8a7b59a81088
child 52626 79a4e7f8d758
tuned;
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jul 12 17:43:18 2013 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jul 12 18:16:50 2013 +0200
     1.3 @@ -5736,24 +5736,30 @@
     1.4    have "open ?A" "open ?B" using open_halfspace_lt and open_halfspace_gt by auto
     1.5    moreover have "?A \<inter> ?B = {}" by auto
     1.6    moreover have "s \<subseteq> ?A \<union> ?B" using as by auto
     1.7 -  ultimately show False using assms(1)[unfolded connected_def not_ex, THEN spec[where x="?A"], THEN spec[where x="?B"]] and assms(2-5) by auto
     1.8 -qed
     1.9 -
    1.10 -lemma connected_ivt_component: fixes x::"'a::euclidean_space" shows
    1.11 - "connected s \<Longrightarrow> x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x\<bullet>k \<le> a \<Longrightarrow> a \<le> y\<bullet>k \<Longrightarrow> (\<exists>z\<in>s.  z\<bullet>k = a)"
    1.12 -  using connected_ivt_hyperplane[of s x y "k::'a" a] by (auto simp: inner_commute)
    1.13 +  ultimately show False
    1.14 +    using assms(1)[unfolded connected_def not_ex, THEN spec[where x="?A"], THEN spec[where x="?B"]] and assms(2-5)
    1.15 +    by auto
    1.16 +qed
    1.17 +
    1.18 +lemma connected_ivt_component:
    1.19 +  fixes x::"'a::euclidean_space"
    1.20 +  shows "connected s \<Longrightarrow>
    1.21 +    x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow>
    1.22 +    x\<bullet>k \<le> a \<Longrightarrow> a \<le> y\<bullet>k \<Longrightarrow> (\<exists>z\<in>s.  z\<bullet>k = a)"
    1.23 +  using connected_ivt_hyperplane[of s x y "k::'a" a]
    1.24 +  by (auto simp: inner_commute)
    1.25  
    1.26  
    1.27  subsection {* Homeomorphisms *}
    1.28  
    1.29 -definition "homeomorphism s t f g \<equiv>
    1.30 -     (\<forall>x\<in>s. (g(f x) = x)) \<and> (f ` s = t) \<and> continuous_on s f \<and>
    1.31 -     (\<forall>y\<in>t. (f(g y) = y)) \<and> (g ` t = s) \<and> continuous_on t g"
    1.32 +definition "homeomorphism s t f g \<longleftrightarrow>
    1.33 +  (\<forall>x\<in>s. (g(f x) = x)) \<and> (f ` s = t) \<and> continuous_on s f \<and>
    1.34 +  (\<forall>y\<in>t. (f(g y) = y)) \<and> (g ` t = s) \<and> continuous_on t g"
    1.35  
    1.36  definition
    1.37    homeomorphic :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
    1.38      (infixr "homeomorphic" 60) where
    1.39 -  homeomorphic_def: "s homeomorphic t \<equiv> (\<exists>f g. homeomorphism s t f g)"
    1.40 +  "s homeomorphic t \<equiv> (\<exists>f g. homeomorphism s t f g)"
    1.41  
    1.42  lemma homeomorphic_refl: "s homeomorphic s"
    1.43    unfolding homeomorphic_def
    1.44 @@ -5761,44 +5767,81 @@
    1.45    using continuous_on_id
    1.46    apply(rule_tac x = "(\<lambda>x. x)" in exI)
    1.47    apply(rule_tac x = "(\<lambda>x. x)" in exI)
    1.48 -  by blast
    1.49 -
    1.50 -lemma homeomorphic_sym:
    1.51 - "s homeomorphic t \<longleftrightarrow> t homeomorphic s"
    1.52 -unfolding homeomorphic_def
    1.53 -unfolding homeomorphism_def
    1.54 -by blast 
    1.55 +  apply blast
    1.56 +  done
    1.57 +
    1.58 +lemma homeomorphic_sym: "s homeomorphic t \<longleftrightarrow> t homeomorphic s"
    1.59 +  unfolding homeomorphic_def
    1.60 +  unfolding homeomorphism_def
    1.61 +  by blast 
    1.62  
    1.63  lemma homeomorphic_trans:
    1.64 -  assumes "s homeomorphic t" "t homeomorphic u" shows "s homeomorphic u"
    1.65 +  assumes "s homeomorphic t" "t homeomorphic u"
    1.66 +  shows "s homeomorphic u"
    1.67  proof-
    1.68 -  obtain f1 g1 where fg1:"\<forall>x\<in>s. g1 (f1 x) = x"  "f1 ` s = t" "continuous_on s f1" "\<forall>y\<in>t. f1 (g1 y) = y" "g1 ` t = s" "continuous_on t g1"
    1.69 +  obtain f1 g1 where fg1:"\<forall>x\<in>s. g1 (f1 x) = x"  "f1 ` s = t"
    1.70 +      "continuous_on s f1" "\<forall>y\<in>t. f1 (g1 y) = y" "g1 ` t = s" "continuous_on t g1"
    1.71      using assms(1) unfolding homeomorphic_def homeomorphism_def by auto
    1.72 -  obtain f2 g2 where fg2:"\<forall>x\<in>t. g2 (f2 x) = x"  "f2 ` t = u" "continuous_on t f2" "\<forall>y\<in>u. f2 (g2 y) = y" "g2 ` u = t" "continuous_on u g2"
    1.73 +  obtain f2 g2 where fg2:"\<forall>x\<in>t. g2 (f2 x) = x"  "f2 ` t = u" "continuous_on t f2"
    1.74 +      "\<forall>y\<in>u. f2 (g2 y) = y" "g2 ` u = t" "continuous_on u g2"
    1.75      using assms(2) unfolding homeomorphic_def homeomorphism_def by auto
    1.76  
    1.77 -  { fix x assume "x\<in>s" hence "(g1 \<circ> g2) ((f2 \<circ> f1) x) = x" using fg1(1)[THEN bspec[where x=x]] and fg2(1)[THEN bspec[where x="f1 x"]] and fg1(2) by auto }
    1.78 -  moreover have "(f2 \<circ> f1) ` s = u" using fg1(2) fg2(2) by auto
    1.79 -  moreover have "continuous_on s (f2 \<circ> f1)" using continuous_on_compose[OF fg1(3)] and fg2(3) unfolding fg1(2) by auto
    1.80 -  moreover { fix y assume "y\<in>u" hence "(f2 \<circ> f1) ((g1 \<circ> g2) y) = y" using fg2(4)[THEN bspec[where x=y]] and fg1(4)[THEN bspec[where x="g2 y"]] and fg2(5) by auto }
    1.81 +  {
    1.82 +    fix x
    1.83 +    assume "x\<in>s"
    1.84 +    hence "(g1 \<circ> g2) ((f2 \<circ> f1) x) = x"
    1.85 +      using fg1(1)[THEN bspec[where x=x]] and fg2(1)[THEN bspec[where x="f1 x"]] and fg1(2)
    1.86 +      by auto
    1.87 +  }
    1.88 +  moreover have "(f2 \<circ> f1) ` s = u"
    1.89 +    using fg1(2) fg2(2) by auto
    1.90 +  moreover have "continuous_on s (f2 \<circ> f1)"
    1.91 +    using continuous_on_compose[OF fg1(3)] and fg2(3) unfolding fg1(2) by auto
    1.92 +  moreover {
    1.93 +    fix y
    1.94 +    assume "y\<in>u"
    1.95 +    hence "(f2 \<circ> f1) ((g1 \<circ> g2) y) = y"
    1.96 +      using fg2(4)[THEN bspec[where x=y]] and fg1(4)[THEN bspec[where x="g2 y"]] and fg2(5)
    1.97 +      by auto
    1.98 +  }
    1.99    moreover have "(g1 \<circ> g2) ` u = s" using fg1(5) fg2(5) by auto
   1.100 -  moreover have "continuous_on u (g1 \<circ> g2)" using continuous_on_compose[OF fg2(6)] and fg1(6)  unfolding fg2(5) by auto
   1.101 -  ultimately show ?thesis unfolding homeomorphic_def homeomorphism_def apply(rule_tac x="f2 \<circ> f1" in exI) apply(rule_tac x="g1 \<circ> g2" in exI) by auto
   1.102 +  moreover have "continuous_on u (g1 \<circ> g2)"
   1.103 +    using continuous_on_compose[OF fg2(6)] and fg1(6)
   1.104 +    unfolding fg2(5)
   1.105 +    by auto
   1.106 +  ultimately show ?thesis
   1.107 +    unfolding homeomorphic_def homeomorphism_def
   1.108 +    apply (rule_tac x="f2 \<circ> f1" in exI)
   1.109 +    apply (rule_tac x="g1 \<circ> g2" in exI)
   1.110 +    apply auto
   1.111 +    done
   1.112  qed
   1.113  
   1.114  lemma homeomorphic_minimal:
   1.115 - "s homeomorphic t \<longleftrightarrow>
   1.116 +  "s homeomorphic t \<longleftrightarrow>
   1.117      (\<exists>f g. (\<forall>x\<in>s. f(x) \<in> t \<and> (g(f(x)) = x)) \<and>
   1.118             (\<forall>y\<in>t. g(y) \<in> s \<and> (f(g(y)) = y)) \<and>
   1.119             continuous_on s f \<and> continuous_on t g)"
   1.120 -unfolding homeomorphic_def homeomorphism_def
   1.121 -apply auto apply (rule_tac x=f in exI) apply (rule_tac x=g in exI)
   1.122 -apply auto apply (rule_tac x=f in exI) apply (rule_tac x=g in exI) apply auto
   1.123 -unfolding image_iff
   1.124 -apply(erule_tac x="g x" in ballE) apply(erule_tac x="x" in ballE)
   1.125 -apply auto apply(rule_tac x="g x" in bexI) apply auto
   1.126 -apply(erule_tac x="f x" in ballE) apply(erule_tac x="x" in ballE)
   1.127 -apply auto apply(rule_tac x="f x" in bexI) by auto
   1.128 +  unfolding homeomorphic_def homeomorphism_def
   1.129 +  apply auto
   1.130 +  apply (rule_tac x=f in exI)
   1.131 +  apply (rule_tac x=g in exI)
   1.132 +  apply auto
   1.133 +  apply (rule_tac x=f in exI)
   1.134 +  apply (rule_tac x=g in exI)
   1.135 +  apply auto
   1.136 +  unfolding image_iff
   1.137 +  apply (erule_tac x="g x" in ballE)
   1.138 +  apply (erule_tac x="x" in ballE)
   1.139 +  apply auto
   1.140 +  apply (rule_tac x="g x" in bexI)
   1.141 +  apply auto
   1.142 +  apply (erule_tac x="f x" in ballE)
   1.143 +  apply (erule_tac x="x" in ballE)
   1.144 +  apply auto
   1.145 +  apply (rule_tac x="f x" in bexI)
   1.146 +  apply auto
   1.147 +  done
   1.148  
   1.149  text {* Relatively weak hypotheses if a set is compact. *}
   1.150  
   1.151 @@ -5808,25 +5851,44 @@
   1.152    shows "\<exists>g. homeomorphism s t f g"
   1.153  proof-
   1.154    def g \<equiv> "\<lambda>x. SOME y. y\<in>s \<and> f y = x"
   1.155 -  have g:"\<forall>x\<in>s. g (f x) = x" using assms(3) assms(4)[unfolded inj_on_def] unfolding g_def by auto
   1.156 -  { fix y assume "y\<in>t"
   1.157 +  have g: "\<forall>x\<in>s. g (f x) = x"
   1.158 +    using assms(3) assms(4)[unfolded inj_on_def] unfolding g_def by auto
   1.159 +  {
   1.160 +    fix y assume "y\<in>t"
   1.161      then obtain x where x:"f x = y" "x\<in>s" using assms(3) by auto
   1.162      hence "g (f x) = x" using g by auto
   1.163 -    hence "f (g y) = y" unfolding x(1)[THEN sym] by auto  }
   1.164 +    hence "f (g y) = y" unfolding x(1)[THEN sym] by auto
   1.165 +  }
   1.166    hence g':"\<forall>x\<in>t. f (g x) = x" by auto
   1.167    moreover
   1.168 -  { fix x
   1.169 -    have "x\<in>s \<Longrightarrow> x \<in> g ` t" using g[THEN bspec[where x=x]] unfolding image_iff using assms(3) by(auto intro!: bexI[where x="f x"])
   1.170 +  {
   1.171 +    fix x
   1.172 +    have "x\<in>s \<Longrightarrow> x \<in> g ` t"
   1.173 +      using g[THEN bspec[where x=x]]
   1.174 +      unfolding image_iff
   1.175 +      using assms(3)
   1.176 +      by (auto intro!: bexI[where x="f x"])
   1.177      moreover
   1.178 -    { assume "x\<in>g ` t"
   1.179 +    {
   1.180 +      assume "x\<in>g ` t"
   1.181        then obtain y where y:"y\<in>t" "g y = x" by auto
   1.182 -      then obtain x' where x':"x'\<in>s" "f x' = y" using assms(3) by auto
   1.183 -      hence "x \<in> s" unfolding g_def using someI2[of "\<lambda>b. b\<in>s \<and> f b = y" x' "\<lambda>x. x\<in>s"] unfolding y(2)[THEN sym] and g_def by auto }
   1.184 -    ultimately have "x\<in>s \<longleftrightarrow> x \<in> g ` t" ..  }
   1.185 +      then obtain x' where x':"x'\<in>s" "f x' = y"
   1.186 +        using assms(3) by auto
   1.187 +      hence "x \<in> s"
   1.188 +        unfolding g_def
   1.189 +        using someI2[of "\<lambda>b. b\<in>s \<and> f b = y" x' "\<lambda>x. x\<in>s"]
   1.190 +        unfolding y(2)[THEN sym] and g_def
   1.191 +        by auto
   1.192 +    }
   1.193 +    ultimately have "x\<in>s \<longleftrightarrow> x \<in> g ` t" ..
   1.194 +  }
   1.195    hence "g ` t = s" by auto
   1.196 -  ultimately
   1.197 -  show ?thesis unfolding homeomorphism_def homeomorphic_def
   1.198 -    apply(rule_tac x=g in exI) using g and assms(3) and continuous_on_inv[OF assms(2,1), of g, unfolded assms(3)] and assms(2) by auto
   1.199 +  ultimately show ?thesis
   1.200 +    unfolding homeomorphism_def homeomorphic_def
   1.201 +    apply (rule_tac x=g in exI)
   1.202 +    using g and assms(3) and continuous_on_inv[OF assms(2,1), of g, unfolded assms(3)] and assms(2)
   1.203 +    apply auto
   1.204 +    done
   1.205  qed
   1.206  
   1.207  lemma homeomorphic_compact:
   1.208 @@ -5837,10 +5899,9 @@
   1.209  
   1.210  text{* Preservation of topological properties.                                   *}
   1.211  
   1.212 -lemma homeomorphic_compactness:
   1.213 - "s homeomorphic t ==> (compact s \<longleftrightarrow> compact t)"
   1.214 -unfolding homeomorphic_def homeomorphism_def
   1.215 -by (metis compact_continuous_image)
   1.216 +lemma homeomorphic_compactness: "s homeomorphic t \<Longrightarrow> (compact s \<longleftrightarrow> compact t)"
   1.217 +  unfolding homeomorphic_def homeomorphism_def
   1.218 +  by (metis compact_continuous_image)
   1.219  
   1.220  text{* Results on translation, scaling etc.                                      *}
   1.221  
   1.222 @@ -5848,27 +5909,34 @@
   1.223    fixes s :: "'a::real_normed_vector set"
   1.224    assumes "c \<noteq> 0"  shows "s homeomorphic ((\<lambda>x. c *\<^sub>R x) ` s)"
   1.225    unfolding homeomorphic_minimal
   1.226 -  apply(rule_tac x="\<lambda>x. c *\<^sub>R x" in exI)
   1.227 -  apply(rule_tac x="\<lambda>x. (1 / c) *\<^sub>R x" in exI)
   1.228 -  using assms by (auto simp add: continuous_on_intros)
   1.229 +  apply (rule_tac x="\<lambda>x. c *\<^sub>R x" in exI)
   1.230 +  apply (rule_tac x="\<lambda>x. (1 / c) *\<^sub>R x" in exI)
   1.231 +  using assms
   1.232 +  apply (auto simp add: continuous_on_intros)
   1.233 +  done
   1.234  
   1.235  lemma homeomorphic_translation:
   1.236    fixes s :: "'a::real_normed_vector set"
   1.237    shows "s homeomorphic ((\<lambda>x. a + x) ` s)"
   1.238    unfolding homeomorphic_minimal
   1.239 -  apply(rule_tac x="\<lambda>x. a + x" in exI)
   1.240 -  apply(rule_tac x="\<lambda>x. -a + x" in exI)
   1.241 -  using continuous_on_add[OF continuous_on_const continuous_on_id] by auto
   1.242 +  apply (rule_tac x="\<lambda>x. a + x" in exI)
   1.243 +  apply (rule_tac x="\<lambda>x. -a + x" in exI)
   1.244 +  using continuous_on_add[OF continuous_on_const continuous_on_id]
   1.245 +  apply auto
   1.246 +  done
   1.247  
   1.248  lemma homeomorphic_affinity:
   1.249    fixes s :: "'a::real_normed_vector set"
   1.250 -  assumes "c \<noteq> 0"  shows "s homeomorphic ((\<lambda>x. a + c *\<^sub>R x) ` s)"
   1.251 +  assumes "c \<noteq> 0"
   1.252 +  shows "s homeomorphic ((\<lambda>x. a + c *\<^sub>R x) ` s)"
   1.253  proof-
   1.254 -  have *:"op + a ` op *\<^sub>R c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto
   1.255 +  have *: "op + a ` op *\<^sub>R c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto
   1.256    show ?thesis
   1.257      using homeomorphic_trans
   1.258      using homeomorphic_scaling[OF assms, of s]
   1.259 -    using homeomorphic_translation[of "(\<lambda>x. c *\<^sub>R x) ` s" a] unfolding * by auto
   1.260 +    using homeomorphic_translation[of "(\<lambda>x. c *\<^sub>R x) ` s" a]
   1.261 +    unfolding *
   1.262 +    by auto
   1.263  qed
   1.264  
   1.265  lemma homeomorphic_balls:
   1.266 @@ -5882,7 +5950,7 @@
   1.267      apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)
   1.268      using assms
   1.269      apply (auto intro!: continuous_on_intros
   1.270 -                simp: dist_commute dist_norm pos_divide_less_eq mult_strict_left_mono)
   1.271 +      simp: dist_commute dist_norm pos_divide_less_eq mult_strict_left_mono)
   1.272      done
   1.273  next
   1.274    show ?cth unfolding homeomorphic_minimal
   1.275 @@ -5890,7 +5958,7 @@
   1.276      apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)
   1.277      using assms
   1.278      apply (auto intro!: continuous_on_intros
   1.279 -                simp: dist_commute dist_norm pos_divide_le_eq mult_strict_left_mono)
   1.280 +      simp: dist_commute dist_norm pos_divide_le_eq mult_strict_left_mono)
   1.281      done
   1.282  qed
   1.283  
   1.284 @@ -5898,30 +5966,49 @@
   1.285  
   1.286  lemma cauchy_isometric:
   1.287    fixes x :: "nat \<Rightarrow> 'a::euclidean_space"
   1.288 -  assumes e:"0 < e" and s:"subspace s" and f:"bounded_linear f" and normf:"\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" and xs:"\<forall>n::nat. x n \<in> s" and cf:"Cauchy(f o x)"
   1.289 +  assumes e: "0 < e"
   1.290 +    and s: "subspace s"
   1.291 +    and f: "bounded_linear f"
   1.292 +    and normf: "\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)"
   1.293 +    and xs: "\<forall>n::nat. x n \<in> s"
   1.294 +    and cf: "Cauchy(f o x)"
   1.295    shows "Cauchy x"
   1.296 -proof-
   1.297 +proof -
   1.298    interpret f: bounded_linear f by fact
   1.299 -  { fix d::real assume "d>0"
   1.300 +  {
   1.301 +    fix d::real assume "d>0"
   1.302      then obtain N where N:"\<forall>n\<ge>N. norm (f (x n) - f (x N)) < e * d"
   1.303 -      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.304 -    { fix n assume "n\<ge>N"
   1.305 +      using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]] and e and mult_pos_pos[of e d]
   1.306 +      by auto
   1.307 +    {
   1.308 +      fix n
   1.309 +      assume "n\<ge>N"
   1.310        have "e * norm (x n - x N) \<le> norm (f (x n - x N))"
   1.311 -        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.312 -        using normf[THEN bspec[where x="x n - x N"]] by auto
   1.313 +        using subspace_sub[OF s, of "x n" "x N"]
   1.314 +        using xs[THEN spec[where x=N]] and xs[THEN spec[where x=n]]
   1.315 +        using normf[THEN bspec[where x="x n - x N"]]
   1.316 +        by auto
   1.317        also have "norm (f (x n - x N)) < e * d"
   1.318          using `N \<le> n` N unfolding f.diff[THEN sym] by auto
   1.319 -      finally have "norm (x n - x N) < d" using `e>0` by simp }
   1.320 -    hence "\<exists>N. \<forall>n\<ge>N. norm (x n - x N) < d" by auto }
   1.321 +      finally have "norm (x n - x N) < d" using `e>0` by simp
   1.322 +    }
   1.323 +    hence "\<exists>N. \<forall>n\<ge>N. norm (x n - x N) < d" by auto
   1.324 +  }
   1.325    thus ?thesis unfolding cauchy and dist_norm by auto
   1.326  qed
   1.327  
   1.328  lemma complete_isometric_image:
   1.329    fixes f :: "'a::euclidean_space => 'b::euclidean_space"
   1.330 -  assumes "0 < e" and s:"subspace s" and f:"bounded_linear f" and normf:"\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" and cs:"complete s"
   1.331 +  assumes "0 < e"
   1.332 +    and s: "subspace s"
   1.333 +    and f: "bounded_linear f"
   1.334 +    and normf: "\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)"
   1.335 +    and cs: "complete s"
   1.336    shows "complete(f ` s)"
   1.337 -proof-
   1.338 -  { fix g assume as:"\<forall>n::nat. g n \<in> f ` s" and cfg:"Cauchy g"
   1.339 +proof -
   1.340 +  {
   1.341 +    fix g
   1.342 +    assume as:"\<forall>n::nat. g n \<in> f ` s" and cfg:"Cauchy g"
   1.343      then obtain x where "\<forall>n. x n \<in> s \<and> g n = f (x n)" 
   1.344        using choice[of "\<lambda> n xa. xa \<in> s \<and> g n = f xa"] by auto
   1.345      hence x:"\<forall>n. x n \<in> s"  "\<forall>n. g n = f (x n)" by auto
   1.346 @@ -5931,19 +6018,25 @@
   1.347        using cauchy_isometric[OF `0<e` s f normf] and cfg and x(1) by auto
   1.348      hence "\<exists>l\<in>f ` s. (g ---> l) sequentially"
   1.349        using linear_continuous_at[OF f, unfolded continuous_at_sequentially, THEN spec[where x=x], of l]
   1.350 -      unfolding `f \<circ> x = g` by auto  }
   1.351 +      unfolding `f \<circ> x = g` by auto
   1.352 +  }
   1.353    thus ?thesis unfolding complete_def by auto
   1.354  qed
   1.355  
   1.356 -lemma injective_imp_isometric: fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   1.357 -  assumes s:"closed s"  "subspace s"  and f:"bounded_linear f" "\<forall>x\<in>s. (f x = 0) \<longrightarrow> (x = 0)"
   1.358 +lemma injective_imp_isometric:
   1.359 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   1.360 +  assumes s: "closed s" "subspace s"
   1.361 +    and f: "bounded_linear f" "\<forall>x\<in>s. (f x = 0) \<longrightarrow> (x = 0)"
   1.362    shows "\<exists>e>0. \<forall>x\<in>s. norm (f x) \<ge> e * norm(x)"
   1.363 -proof(cases "s \<subseteq> {0::'a}")
   1.364 +proof (cases "s \<subseteq> {0::'a}")
   1.365    case True
   1.366 -  { fix x assume "x \<in> s"
   1.367 +  {
   1.368 +    fix x
   1.369 +    assume "x \<in> s"
   1.370      hence "x = 0" using True by auto
   1.371 -    hence "norm x \<le> norm (f x)" by auto  }
   1.372 -  thus ?thesis by(auto intro!: exI[where x=1])
   1.373 +    hence "norm x \<le> norm (f x)" by auto
   1.374 +  }
   1.375 +  thus ?thesis by (auto intro!: exI[where x=1])
   1.376  next
   1.377    interpret f: bounded_linear f by fact
   1.378    case False
   1.379 @@ -5953,37 +6046,58 @@
   1.380    let ?S' = "{x::'a. x\<in>s \<and> norm x = norm a}"
   1.381    let ?S'' = "{x::'a. norm x = norm a}"
   1.382  
   1.383 -  have "?S'' = frontier(cball 0 (norm a))" unfolding frontier_cball and dist_norm by auto
   1.384 -  hence "compact ?S''" using compact_frontier[OF compact_cball, of 0 "norm a"] by auto
   1.385 +  have "?S'' = frontier(cball 0 (norm a))"
   1.386 +    unfolding frontier_cball and dist_norm by auto
   1.387 +  hence "compact ?S''"
   1.388 +    using compact_frontier[OF compact_cball, of 0 "norm a"] by auto
   1.389    moreover have "?S' = s \<inter> ?S''" by auto
   1.390 -  ultimately have "compact ?S'" using closed_inter_compact[of s ?S''] using s(1) by auto
   1.391 +  ultimately have "compact ?S'"
   1.392 +    using closed_inter_compact[of s ?S''] using s(1) by auto
   1.393    moreover have *:"f ` ?S' = ?S" by auto
   1.394 -  ultimately have "compact ?S" using compact_continuous_image[OF linear_continuous_on[OF f(1)], of ?S'] by auto
   1.395 +  ultimately have "compact ?S"
   1.396 +    using compact_continuous_image[OF linear_continuous_on[OF f(1)], of ?S'] by auto
   1.397    hence "closed ?S" using compact_imp_closed by auto
   1.398    moreover have "?S \<noteq> {}" using a by auto
   1.399 -  ultimately obtain b' where "b'\<in>?S" "\<forall>y\<in>?S. norm b' \<le> norm y" using distance_attains_inf[of ?S 0] unfolding dist_0_norm by auto
   1.400 -  then obtain b where "b\<in>s" and ba:"norm b = norm a" and b:"\<forall>x\<in>{x \<in> s. norm x = norm a}. norm (f b) \<le> norm (f x)" unfolding *[THEN sym] unfolding image_iff by auto
   1.401 +  ultimately obtain b' where "b'\<in>?S" "\<forall>y\<in>?S. norm b' \<le> norm y"
   1.402 +    using distance_attains_inf[of ?S 0] unfolding dist_0_norm by auto
   1.403 +  then obtain b where "b\<in>s" and ba:"norm b = norm a"
   1.404 +      and b:"\<forall>x\<in>{x \<in> s. norm x = norm a}. norm (f b) \<le> norm (f x)"
   1.405 +    unfolding *[THEN sym] unfolding image_iff by auto
   1.406  
   1.407    let ?e = "norm (f b) / norm b"
   1.408    have "norm b > 0" using ba and a and norm_ge_zero by auto
   1.409 -  moreover have "norm (f b) > 0" using f(2)[THEN bspec[where x=b], OF `b\<in>s`] using `norm b >0` unfolding zero_less_norm_iff by auto
   1.410 -  ultimately have "0 < norm (f b) / norm b" by(simp only: divide_pos_pos)
   1.411 +  moreover have "norm (f b) > 0"
   1.412 +    using f(2)[THEN bspec[where x=b], OF `b\<in>s`]
   1.413 +    using `norm b >0`
   1.414 +    unfolding zero_less_norm_iff
   1.415 +    by auto
   1.416 +  ultimately have "0 < norm (f b) / norm b"
   1.417 +    by (simp only: divide_pos_pos)
   1.418    moreover
   1.419 -  { fix x assume "x\<in>s"
   1.420 +  {
   1.421 +    fix x
   1.422 +    assume "x\<in>s"
   1.423      hence "norm (f b) / norm b * norm x \<le> norm (f x)"
   1.424 -    proof(cases "x=0")
   1.425 -      case True thus "norm (f b) / norm b * norm x \<le> norm (f x)" by auto
   1.426 +    proof (cases "x=0")
   1.427 +      case True
   1.428 +      thus "norm (f b) / norm b * norm x \<le> norm (f x)" by auto
   1.429      next
   1.430        case False
   1.431 -      hence *:"0 < norm a / norm x" using `a\<noteq>0` unfolding zero_less_norm_iff[THEN sym] by(simp only: divide_pos_pos)
   1.432 -      have "\<forall>c. \<forall>x\<in>s. c *\<^sub>R x \<in> s" using s[unfolded subspace_def] by auto
   1.433 -      hence "(norm a / norm x) *\<^sub>R x \<in> {x \<in> s. norm x = norm a}" using `x\<in>s` and `x\<noteq>0` by auto
   1.434 -      thus "norm (f b) / norm b * norm x \<le> norm (f x)" using b[THEN bspec[where x="(norm a / norm x) *\<^sub>R x"]]
   1.435 +      hence *:"0 < norm a / norm x"
   1.436 +        using `a\<noteq>0`
   1.437 +        unfolding zero_less_norm_iff[THEN sym]
   1.438 +        by (simp only: divide_pos_pos)
   1.439 +      have "\<forall>c. \<forall>x\<in>s. c *\<^sub>R x \<in> s"
   1.440 +        using s[unfolded subspace_def] by auto
   1.441 +      hence "(norm a / norm x) *\<^sub>R x \<in> {x \<in> s. norm x = norm a}"
   1.442 +        using `x\<in>s` and `x\<noteq>0` by auto
   1.443 +      thus "norm (f b) / norm b * norm x \<le> norm (f x)"
   1.444 +        using b[THEN bspec[where x="(norm a / norm x) *\<^sub>R x"]]
   1.445          unfolding f.scaleR and ba using `x\<noteq>0` `a\<noteq>0`
   1.446          by (auto simp add: mult_commute pos_le_divide_eq pos_divide_le_eq)
   1.447 -    qed }
   1.448 -  ultimately
   1.449 -  show ?thesis by auto
   1.450 +    qed
   1.451 +  }
   1.452 +  ultimately show ?thesis by auto
   1.453  qed
   1.454  
   1.455  lemma closed_injective_image_subspace:
   1.456 @@ -5991,8 +6105,10 @@
   1.457    assumes "subspace s" "bounded_linear f" "\<forall>x\<in>s. f x = 0 --> x = 0" "closed s"
   1.458    shows "closed(f ` s)"
   1.459  proof-
   1.460 -  obtain e where "e>0" and e:"\<forall>x\<in>s. e * norm x \<le> norm (f x)" using injective_imp_isometric[OF assms(4,1,2,3)] by auto
   1.461 -  show ?thesis using complete_isometric_image[OF `e>0` assms(1,2) e] and assms(4)
   1.462 +  obtain e where "e>0" and e:"\<forall>x\<in>s. e * norm x \<le> norm (f x)"
   1.463 +    using injective_imp_isometric[OF assms(4,1,2,3)] by auto
   1.464 +  show ?thesis
   1.465 +    using complete_isometric_image[OF `e>0` assms(1,2) e] and assms(4)
   1.466      unfolding complete_eq_closed[THEN sym] by auto
   1.467  qed
   1.468  
   1.469 @@ -6004,8 +6120,8 @@
   1.470    unfolding subspace_def by (auto simp: inner_add_left)
   1.471  
   1.472  lemma closed_substandard:
   1.473 - "closed {x::'a::euclidean_space. \<forall>i\<in>Basis. P i --> x\<bullet>i = 0}" (is "closed ?A")
   1.474 -proof-
   1.475 +  "closed {x::'a::euclidean_space. \<forall>i\<in>Basis. P i --> x\<bullet>i = 0}" (is "closed ?A")
   1.476 +proof -
   1.477    let ?D = "{i\<in>Basis. P i}"
   1.478    have "closed (\<Inter>i\<in>?D. {x::'a. x\<bullet>i = 0})"
   1.479      by (simp add: closed_INT closed_Collect_eq)
   1.480 @@ -6014,18 +6130,25 @@
   1.481    finally show "closed ?A" .
   1.482  qed
   1.483  
   1.484 -lemma dim_substandard: assumes d: "d \<subseteq> Basis"
   1.485 +lemma dim_substandard:
   1.486 +  assumes d: "d \<subseteq> Basis"
   1.487    shows "dim {x::'a::euclidean_space. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0} = card d" (is "dim ?A = _")
   1.488 -proof-
   1.489 +proof -
   1.490    let ?D = "Basis :: 'a set"
   1.491    have "d \<subseteq> ?A" using d by (auto simp: inner_Basis)
   1.492    moreover
   1.493 -  { fix x::"'a" assume "x \<in> ?A"
   1.494 +  {
   1.495 +    fix x::"'a" assume "x \<in> ?A"
   1.496      hence "finite d" "x \<in> ?A" using assms by(auto intro: finite_subset[OF _ finite_Basis])
   1.497      from this d have "x \<in> span d"
   1.498 -    proof(induct d arbitrary: x)
   1.499 -      case empty hence "x=0" apply(rule_tac euclidean_eqI) by auto
   1.500 -      thus ?case using subspace_0[OF subspace_span[of "{}"]] by auto
   1.501 +    proof (induct d arbitrary: x)
   1.502 +      case empty
   1.503 +      hence "x=0"
   1.504 +        apply (rule_tac euclidean_eqI)
   1.505 +        apply auto
   1.506 +        done
   1.507 +      thus ?case
   1.508 +        using subspace_0[OF subspace_span[of "{}"]] by auto
   1.509      next
   1.510        case (insert k F)
   1.511        hence *:"\<forall>i\<in>Basis. i \<notin> insert k F \<longrightarrow> x \<bullet> i = 0" by auto
   1.512 @@ -6050,8 +6173,13 @@
   1.513    }
   1.514    hence "?A \<subseteq> span d" by auto
   1.515    moreover
   1.516 -  { fix x assume "x \<in> d" hence "x \<in> ?D" using assms by auto  }
   1.517 -  hence "independent d" using independent_mono[OF independent_Basis, of d] and assms by auto
   1.518 +  {
   1.519 +    fix x
   1.520 +    assume "x \<in> d"
   1.521 +    hence "x \<in> ?D" using assms by auto
   1.522 +  }
   1.523 +  hence "independent d"
   1.524 +    using independent_mono[OF independent_Basis, of d] and assms by auto
   1.525    moreover
   1.526    have "d \<subseteq> ?D" unfolding subset_eq using assms by auto
   1.527    ultimately show ?thesis using dim_unique[of d ?A] by auto
   1.528 @@ -6069,41 +6197,55 @@
   1.529      by (auto simp: bij_betw_def card_image)
   1.530    then show ?thesis by blast
   1.531  next
   1.532 -  assume "\<not> finite A" with `n \<le> card A` show ?thesis by force
   1.533 -qed
   1.534 -
   1.535 -lemma closed_subspace: fixes s::"('a::euclidean_space) set"
   1.536 -  assumes "subspace s" shows "closed s"
   1.537 -proof-
   1.538 -  have "dim s \<le> card (Basis :: 'a set)" using dim_subset_UNIV by auto
   1.539 -  with ex_card[OF this] obtain d :: "'a set" where t: "card d = dim s" and d: "d \<subseteq> Basis" by auto
   1.540 +  assume "\<not> finite A"
   1.541 +  with `n \<le> card A` show ?thesis by force
   1.542 +qed
   1.543 +
   1.544 +lemma closed_subspace:
   1.545 +  fixes s::"('a::euclidean_space) set"
   1.546 +  assumes "subspace s"
   1.547 +  shows "closed s"
   1.548 +proof -
   1.549 +  have "dim s \<le> card (Basis :: 'a set)"
   1.550 +    using dim_subset_UNIV by auto
   1.551 +  with ex_card[OF this] obtain d :: "'a set" where t: "card d = dim s" and d: "d \<subseteq> Basis"
   1.552 +    by auto
   1.553    let ?t = "{x::'a. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}"
   1.554    have "\<exists>f. linear f \<and> f ` {x::'a. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0} = s \<and>
   1.555        inj_on f {x::'a. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0}"
   1.556      using dim_substandard[of d] t d assms
   1.557      by (intro subspace_isomorphism[OF subspace_substandard[of "\<lambda>i. i \<notin> d"]]) (auto simp: inner_Basis)
   1.558    then guess f by (elim exE conjE) note f = this
   1.559 -  interpret f: bounded_linear f using f unfolding linear_conv_bounded_linear by auto
   1.560 -  { fix x have "x\<in>?t \<Longrightarrow> f x = 0 \<Longrightarrow> x = 0" using f.zero d f(3)[THEN inj_onD, of x 0] by auto }
   1.561 +  interpret f: bounded_linear f
   1.562 +    using f unfolding linear_conv_bounded_linear by auto
   1.563 +  {
   1.564 +    fix x
   1.565 +    have "x\<in>?t \<Longrightarrow> f x = 0 \<Longrightarrow> x = 0"
   1.566 +      using f.zero d f(3)[THEN inj_onD, of x 0] by auto
   1.567 +  }
   1.568    moreover have "closed ?t" using closed_substandard .
   1.569    moreover have "subspace ?t" using subspace_substandard .
   1.570 -  ultimately show ?thesis using closed_injective_image_subspace[of ?t f]
   1.571 +  ultimately show ?thesis
   1.572 +    using closed_injective_image_subspace[of ?t f]
   1.573      unfolding f(2) using f(1) unfolding linear_conv_bounded_linear by auto
   1.574  qed
   1.575  
   1.576  lemma complete_subspace:
   1.577 -  fixes s :: "('a::euclidean_space) set" shows "subspace s ==> complete s"
   1.578 -  using complete_eq_closed closed_subspace
   1.579 -  by auto
   1.580 +  fixes s :: "('a::euclidean_space) set"
   1.581 +  shows "subspace s \<Longrightarrow> complete s"
   1.582 +  using complete_eq_closed closed_subspace by auto
   1.583  
   1.584  lemma dim_closure:
   1.585    fixes s :: "('a::euclidean_space) set"
   1.586    shows "dim(closure s) = dim s" (is "?dc = ?d")
   1.587 -proof-
   1.588 +proof -
   1.589    have "?dc \<le> ?d" using closure_minimal[OF span_inc, of s]
   1.590      using closed_subspace[OF subspace_span, of s]
   1.591 -    using dim_subset[of "closure s" "span s"] unfolding dim_span by auto
   1.592 -  thus ?thesis using dim_subset[OF closure_subset, of s] by auto
   1.593 +    using dim_subset[of "closure s" "span s"]
   1.594 +    unfolding dim_span
   1.595 +    by auto
   1.596 +  thus ?thesis using dim_subset[OF closure_subset, of s]
   1.597 +    by auto
   1.598  qed
   1.599  
   1.600  
   1.601 @@ -6189,34 +6331,46 @@
   1.602    def z \<equiv> "\<lambda>n. (f ^^ n) z0"
   1.603    { fix n::nat
   1.604      have "z n \<in> s" unfolding z_def
   1.605 -    proof(induct n) case 0 thus ?case using `z0 \<in>s` by auto
   1.606 -    next case Suc thus ?case using f by auto qed }
   1.607 -  note z_in_s = this
   1.608 +    proof (induct n)
   1.609 +      case 0
   1.610 +      thus ?case using `z0 \<in>s` by auto
   1.611 +    next
   1.612 +      case Suc
   1.613 +      thus ?case using f by auto qed
   1.614 +  } note z_in_s = this
   1.615  
   1.616    def d \<equiv> "dist (z 0) (z 1)"
   1.617  
   1.618    have fzn:"\<And>n. f (z n) = z (Suc n)" unfolding z_def by auto
   1.619 -  { fix n::nat
   1.620 +  {
   1.621 +    fix n::nat
   1.622      have "dist (z n) (z (Suc n)) \<le> (c ^ n) * d"
   1.623 -    proof(induct n)
   1.624 -      case 0 thus ?case unfolding d_def by auto
   1.625 +    proof (induct n)
   1.626 +      case 0 thus ?case
   1.627 +        unfolding d_def by auto
   1.628      next
   1.629        case (Suc m)
   1.630        hence "c * dist (z m) (z (Suc m)) \<le> c ^ Suc m * d"
   1.631 -        using `0 \<le> c` using mult_left_mono[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by auto
   1.632 -      thus ?case using lipschitz[THEN bspec[where x="z m"], OF z_in_s, THEN bspec[where x="z (Suc m)"], OF z_in_s]
   1.633 -        unfolding fzn and mult_le_cancel_left by auto
   1.634 +        using `0 \<le> c`
   1.635 +        using mult_left_mono[of "dist (z m) (z (Suc m))" "c ^ m * d" c]
   1.636 +        by auto
   1.637 +      thus ?case
   1.638 +        using lipschitz[THEN bspec[where x="z m"], OF z_in_s, THEN bspec[where x="z (Suc m)"], OF z_in_s]
   1.639 +        unfolding fzn and mult_le_cancel_left
   1.640 +        by auto
   1.641      qed
   1.642    } note cf_z = this
   1.643  
   1.644 -  { fix n m::nat
   1.645 +  {
   1.646 +    fix n m::nat
   1.647      have "(1 - c) * dist (z m) (z (m+n)) \<le> (c ^ m) * d * (1 - c ^ n)"
   1.648 -    proof(induct n)
   1.649 +    proof (induct n)
   1.650        case 0 show ?case by auto
   1.651      next
   1.652        case (Suc k)
   1.653 -      have "(1 - c) * dist (z m) (z (m + Suc k)) \<le> (1 - c) * (dist (z m) (z (m + k)) + dist (z (m + k)) (z (Suc (m + k))))"
   1.654 -        using dist_triangle and c by(auto simp add: dist_triangle)
   1.655 +      have "(1 - c) * dist (z m) (z (m + Suc k)) \<le>
   1.656 +          (1 - c) * (dist (z m) (z (m + k)) + dist (z (m + k)) (z (Suc (m + k))))"
   1.657 +        using dist_triangle and c by (auto simp add: dist_triangle)
   1.658        also have "\<dots> \<le> (1 - c) * (dist (z m) (z (m + k)) + c ^ (m + k) * d)"
   1.659          using cf_z[of "m + k"] and c by auto
   1.660        also have "\<dots> \<le> c ^ m * d * (1 - c ^ k) + (1 - c) * c ^ (m + k) * d"
   1.661 @@ -6228,9 +6382,11 @@
   1.662        finally show ?case by auto
   1.663      qed
   1.664    } note cf_z2 = this
   1.665 -  { fix e::real assume "e>0"
   1.666 +  {
   1.667 +    fix e::real
   1.668 +    assume "e>0"
   1.669      hence "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (z m) (z n) < e"
   1.670 -    proof(cases "d = 0")
   1.671 +    proof (cases "d = 0")
   1.672        case True
   1.673        have *: "\<And>x. ((1 - c) * x \<le> 0) = (x \<le> 0)" using `1 - c > 0`
   1.674          by (metis mult_zero_left mult_commute real_mult_le_cancel_iff1)
   1.675 @@ -6238,21 +6394,31 @@
   1.676          by (simp add: *)
   1.677        thus ?thesis using `e>0` by auto
   1.678      next
   1.679 -      case False hence "d>0" unfolding d_def using zero_le_dist[of "z 0" "z 1"]
   1.680 +      case False
   1.681 +      hence "d>0" unfolding d_def using zero_le_dist[of "z 0" "z 1"]
   1.682          by (metis False d_def less_le)
   1.683 -      hence "0 < e * (1 - c) / d" using `e>0` and `1-c>0`
   1.684 -        using divide_pos_pos[of "e * (1 - c)" d] and mult_pos_pos[of e "1 - c"] by auto
   1.685 -      then obtain N where N:"c ^ N < e * (1 - c) / d" using real_arch_pow_inv[of "e * (1 - c) / d" c] and c by auto
   1.686 -      { fix m n::nat assume "m>n" and as:"m\<ge>N" "n\<ge>N"
   1.687 -        have *:"c ^ n \<le> c ^ N" using `n\<ge>N` and c using power_decreasing[OF `n\<ge>N`, of c] by auto
   1.688 -        have "1 - c ^ (m - n) > 0" using c and power_strict_mono[of c 1 "m - n"] using `m>n` by auto
   1.689 +      hence "0 < e * (1 - c) / d"
   1.690 +        using `e>0` and `1-c>0`
   1.691 +        using divide_pos_pos[of "e * (1 - c)" d] and mult_pos_pos[of e "1 - c"]
   1.692 +        by auto
   1.693 +      then obtain N where N:"c ^ N < e * (1 - c) / d"
   1.694 +        using real_arch_pow_inv[of "e * (1 - c) / d" c] and c by auto
   1.695 +      {
   1.696 +        fix m n::nat
   1.697 +        assume "m>n" and as:"m\<ge>N" "n\<ge>N"
   1.698 +        have *:"c ^ n \<le> c ^ N" using `n\<ge>N` and c
   1.699 +          using power_decreasing[OF `n\<ge>N`, of c] by auto
   1.700 +        have "1 - c ^ (m - n) > 0"
   1.701 +          using c and power_strict_mono[of c 1 "m - n"] using `m>n` by auto
   1.702          hence **:"d * (1 - c ^ (m - n)) / (1 - c) > 0"
   1.703            using mult_pos_pos[OF `d>0`, of "1 - c ^ (m - n)"]
   1.704            using divide_pos_pos[of "d * (1 - c ^ (m - n))" "1 - c"]
   1.705 -          using `0 < 1 - c` by auto
   1.706 +          using `0 < 1 - c`
   1.707 +          by auto
   1.708  
   1.709          have "dist (z m) (z n) \<le> c ^ n * d * (1 - c ^ (m - n)) / (1 - c)"
   1.710 -          using cf_z2[of n "m - n"] and `m>n` unfolding pos_le_divide_eq[OF `1-c>0`]
   1.711 +          using cf_z2[of n "m - n"] and `m>n`
   1.712 +          unfolding pos_le_divide_eq[OF `1-c>0`]
   1.713            by (auto simp add: mult_commute dist_commute)
   1.714          also have "\<dots> \<le> c ^ N * d * (1 - c ^ (m - n)) / (1 - c)"
   1.715            using mult_right_mono[OF * order_less_imp_le[OF **]]
   1.716 @@ -6263,44 +6429,66 @@
   1.717          also have "\<dots> \<le> e" using c and `1 - c ^ (m - n) > 0` and `e>0` using mult_right_le_one_le[of e "1 - c ^ (m - n)"] by auto
   1.718          finally have  "dist (z m) (z n) < e" by auto
   1.719        } note * = this
   1.720 -      { fix m n::nat assume as:"N\<le>m" "N\<le>n"
   1.721 +      {
   1.722 +        fix m n::nat
   1.723 +        assume as:"N\<le>m" "N\<le>n"
   1.724          hence "dist (z n) (z m) < e"
   1.725 -        proof(cases "n = m")
   1.726 -          case True thus ?thesis using `e>0` by auto
   1.727 +        proof (cases "n = m")
   1.728 +          case True
   1.729 +          thus ?thesis using `e>0` by auto
   1.730          next
   1.731 -          case False thus ?thesis using as and *[of n m] *[of m n] unfolding nat_neq_iff by (auto simp add: dist_commute)
   1.732 -        qed }
   1.733 +          case False
   1.734 +          thus ?thesis using as and *[of n m] *[of m n]
   1.735 +            unfolding nat_neq_iff by (auto simp add: dist_commute)
   1.736 +        qed
   1.737 +      }
   1.738        thus ?thesis by auto
   1.739      qed
   1.740    }
   1.741    hence "Cauchy z" unfolding cauchy_def by auto
   1.742 -  then obtain x where "x\<in>s" and x:"(z ---> x) sequentially" using s(1)[unfolded compact_def complete_def, THEN spec[where x=z]] and z_in_s by auto
   1.743 +  then obtain x where "x\<in>s" and x:"(z ---> x) sequentially"
   1.744 +    using s(1)[unfolded compact_def complete_def, THEN spec[where x=z]] and z_in_s by auto
   1.745  
   1.746    def e \<equiv> "dist (f x) x"
   1.747 -  have "e = 0" proof(rule ccontr)
   1.748 -    assume "e \<noteq> 0" hence "e>0" unfolding e_def using zero_le_dist[of "f x" x]
   1.749 +  have "e = 0"
   1.750 +  proof (rule ccontr)
   1.751 +    assume "e \<noteq> 0"
   1.752 +    hence "e>0" unfolding e_def using zero_le_dist[of "f x" x]
   1.753        by (metis dist_eq_0_iff dist_nz e_def)
   1.754      then obtain N where N:"\<forall>n\<ge>N. dist (z n) x < e / 2"
   1.755        using x[unfolded LIMSEQ_def, THEN spec[where x="e/2"]] by auto
   1.756      hence N':"dist (z N) x < e / 2" by auto
   1.757  
   1.758 -    have *:"c * dist (z N) x \<le> dist (z N) x" unfolding mult_le_cancel_right2
   1.759 +    have *:"c * dist (z N) x \<le> dist (z N) x"
   1.760 +      unfolding mult_le_cancel_right2
   1.761        using zero_le_dist[of "z N" x] and c
   1.762        by (metis dist_eq_0_iff dist_nz order_less_asym less_le)
   1.763 -    have "dist (f (z N)) (f x) \<le> c * dist (z N) x" using lipschitz[THEN bspec[where x="z N"], THEN bspec[where x=x]]
   1.764 -      using z_in_s[of N] `x\<in>s` using c by auto
   1.765 -    also have "\<dots> < e / 2" using N' and c using * by auto
   1.766 -    finally show False unfolding fzn
   1.767 +    have "dist (f (z N)) (f x) \<le> c * dist (z N) x"
   1.768 +      using lipschitz[THEN bspec[where x="z N"], THEN bspec[where x=x]]
   1.769 +      using z_in_s[of N] `x\<in>s`
   1.770 +      using c
   1.771 +      by auto
   1.772 +    also have "\<dots> < e / 2"
   1.773 +      using N' and c using * by auto
   1.774 +    finally show False
   1.775 +      unfolding fzn
   1.776        using N[THEN spec[where x="Suc N"]] and dist_triangle_half_r[of "z (Suc N)" "f x" e x]
   1.777 -      unfolding e_def by auto
   1.778 +      unfolding e_def
   1.779 +      by auto
   1.780    qed
   1.781    hence "f x = x" unfolding e_def by auto
   1.782    moreover
   1.783 -  { fix y assume "f y = y" "y\<in>s"
   1.784 -    hence "dist x y \<le> c * dist x y" using lipschitz[THEN bspec[where x=x], THEN bspec[where x=y]]
   1.785 -      using `x\<in>s` and `f x = x` by auto
   1.786 -    hence "dist x y = 0" unfolding mult_le_cancel_right1
   1.787 -      using c and zero_le_dist[of x y] by auto
   1.788 +  {
   1.789 +    fix y
   1.790 +    assume "f y = y" "y\<in>s"
   1.791 +    hence "dist x y \<le> c * dist x y"
   1.792 +      using lipschitz[THEN bspec[where x=x], THEN bspec[where x=y]]
   1.793 +      using `x\<in>s` and `f x = x`
   1.794 +      by auto
   1.795 +    hence "dist x y = 0"
   1.796 +      unfolding mult_le_cancel_right1
   1.797 +      using c and zero_le_dist[of x y]
   1.798 +      by auto
   1.799      hence "y = x" by auto
   1.800    }
   1.801    ultimately show ?thesis using `x\<in>s` by blast+
   1.802 @@ -6310,8 +6498,9 @@
   1.803  
   1.804  lemma edelstein_fix:
   1.805    fixes s :: "'a::metric_space set"
   1.806 -  assumes s:"compact s" "s \<noteq> {}" and gs:"(g ` s) \<subseteq> s"
   1.807 -      and dist:"\<forall>x\<in>s. \<forall>y\<in>s. x \<noteq> y \<longrightarrow> dist (g x) (g y) < dist x y"
   1.808 +  assumes s: "compact s" "s \<noteq> {}"
   1.809 +    and gs: "(g ` s) \<subseteq> s"
   1.810 +    and dist: "\<forall>x\<in>s. \<forall>y\<in>s. x \<noteq> y \<longrightarrow> dist (g x) (g y) < dist x y"
   1.811    shows "\<exists>!x\<in>s. g x = x"
   1.812  proof -
   1.813    let ?D = "(\<lambda>x. (x, x)) ` s"