src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 50898 ebd9b82537e0
parent 50897 078590669527
child 50936 b28f258ebc1a
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 14 19:28:39 2013 -0800
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Jan 15 08:29:56 2013 -0800
     1.3 @@ -2339,6 +2339,16 @@
     1.4    compact_eq_heine_borel: -- "This name is used for backwards compatibility"
     1.5      "compact S \<longleftrightarrow> (\<forall>C. (\<forall>c\<in>C. open c) \<and> S \<subseteq> \<Union>C \<longrightarrow> (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
     1.6  
     1.7 +lemma compactI:
     1.8 +  assumes "\<And>C. \<forall>t\<in>C. open t \<Longrightarrow> s \<subseteq> \<Union> C \<Longrightarrow> \<exists>C'. C' \<subseteq> C \<and> finite C' \<and> s \<subseteq> \<Union> C'"
     1.9 +  shows "compact s"
    1.10 +  unfolding compact_eq_heine_borel using assms by metis
    1.11 +
    1.12 +lemma compactE:
    1.13 +  assumes "compact s" and "\<forall>t\<in>C. open t" and "s \<subseteq> \<Union>C"
    1.14 +  obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> \<Union>C'"
    1.15 +  using assms unfolding compact_eq_heine_borel by metis
    1.16 +
    1.17  subsubsection {* Bolzano-Weierstrass property *}
    1.18  
    1.19  lemma heine_borel_imp_bolzano_weierstrass:
    1.20 @@ -2537,14 +2547,32 @@
    1.21  qed
    1.22  
    1.23  lemma compact_imp_closed:
    1.24 -  fixes s :: "'a::{first_countable_topology, t2_space} set"
    1.25 -  shows "compact s \<Longrightarrow> closed s"
    1.26 -proof -
    1.27 -  assume "compact s"
    1.28 -  hence "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t)"
    1.29 -    using heine_borel_imp_bolzano_weierstrass[of s] by auto
    1.30 -  thus "closed s"
    1.31 -    by (rule bolzano_weierstrass_imp_closed)
    1.32 +  fixes s :: "'a::t2_space set"
    1.33 +  assumes "compact s" shows "closed s"
    1.34 +unfolding closed_def
    1.35 +proof (rule openI)
    1.36 +  fix y assume "y \<in> - s"
    1.37 +  let ?C = "\<Union>x\<in>s. {u. open u \<and> x \<in> u \<and> eventually (\<lambda>y. y \<notin> u) (nhds y)}"
    1.38 +  note `compact s`
    1.39 +  moreover have "\<forall>u\<in>?C. open u" by simp
    1.40 +  moreover have "s \<subseteq> \<Union>?C"
    1.41 +  proof
    1.42 +    fix x assume "x \<in> s"
    1.43 +    with `y \<in> - s` have "x \<noteq> y" by clarsimp
    1.44 +    hence "\<exists>u v. open u \<and> open v \<and> x \<in> u \<and> y \<in> v \<and> u \<inter> v = {}"
    1.45 +      by (rule hausdorff)
    1.46 +    with `x \<in> s` show "x \<in> \<Union>?C"
    1.47 +      unfolding eventually_nhds by auto
    1.48 +  qed
    1.49 +  ultimately obtain D where "D \<subseteq> ?C" and "finite D" and "s \<subseteq> \<Union>D"
    1.50 +    by (rule compactE)
    1.51 +  from `D \<subseteq> ?C` have "\<forall>x\<in>D. eventually (\<lambda>y. y \<notin> x) (nhds y)" by auto
    1.52 +  with `finite D` have "eventually (\<lambda>y. y \<notin> \<Union>D) (nhds y)"
    1.53 +    by (simp add: eventually_Ball_finite)
    1.54 +  with `s \<subseteq> \<Union>D` have "eventually (\<lambda>y. y \<notin> s) (nhds y)"
    1.55 +    by (auto elim!: eventually_mono [rotated])
    1.56 +  thus "\<exists>t. open t \<and> y \<in> t \<and> t \<subseteq> - s"
    1.57 +    by (simp add: eventually_nhds subset_eq)
    1.58  qed
    1.59  
    1.60  text{* In particular, some common special cases. *}
    1.61 @@ -2556,9 +2584,8 @@
    1.62  
    1.63  lemma compact_union [intro]:
    1.64    assumes "compact s" "compact t" shows " compact (s \<union> t)"
    1.65 -  unfolding compact_eq_heine_borel
    1.66 -proof (intro allI impI)
    1.67 -  fix f assume *: "Ball f open \<and> s \<union> t \<subseteq> \<Union>f"
    1.68 +proof (rule compactI)
    1.69 +  fix f assume *: "Ball f open" "s \<union> t \<subseteq> \<Union>f"
    1.70    from * `compact s` obtain s' where "s' \<subseteq> f \<and> finite s' \<and> s \<subseteq> \<Union>s'"
    1.71      unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f]) metis
    1.72    moreover from * `compact t` obtain t' where "t' \<subseteq> f \<and> finite t' \<and> t \<subseteq> \<Union>t'"
    1.73 @@ -2577,8 +2604,7 @@
    1.74  lemma compact_inter_closed [intro]:
    1.75    assumes "compact s" and "closed t"
    1.76    shows "compact (s \<inter> t)"
    1.77 -  unfolding compact_eq_heine_borel
    1.78 -proof safe
    1.79 +proof (rule compactI)
    1.80    fix C assume C: "\<forall>c\<in>C. open c" and cover: "s \<inter> t \<subseteq> \<Union>C"
    1.81    from C `closed t` have "\<forall>c\<in>C \<union> {-t}. open c" by auto
    1.82    moreover from cover have "s \<subseteq> \<Union>(C \<union> {-t})" by auto
    1.83 @@ -2596,7 +2622,7 @@
    1.84    by (simp add: Int_commute)
    1.85  
    1.86  lemma compact_inter [intro]:
    1.87 -  fixes s t :: "'a :: {t2_space, first_countable_topology} set"
    1.88 +  fixes s t :: "'a :: t2_space set"
    1.89    assumes "compact s" and "compact t"
    1.90    shows "compact (s \<inter> t)"
    1.91    using assms by (intro compact_inter_closed compact_imp_closed)
    1.92 @@ -4621,35 +4647,41 @@
    1.93  text {* Making a continuous function avoid some value in a neighbourhood. *}
    1.94  
    1.95  lemma continuous_within_avoid:
    1.96 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
    1.97 -  assumes "continuous (at x within s) f"  "x \<in> s"  "f x \<noteq> a"
    1.98 +  fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
    1.99 +  assumes "continuous (at x within s) f" and "f x \<noteq> a"
   1.100    shows "\<exists>e>0. \<forall>y \<in> s. dist x y < e --> f y \<noteq> a"
   1.101  proof-
   1.102 -  obtain d where "d>0" and d:"\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < dist (f x) a"
   1.103 -    using assms(1)[unfolded continuous_within Lim_within, THEN spec[where x="dist (f x) a"]] assms(3)[unfolded dist_nz] by auto
   1.104 -  { fix y assume " y\<in>s"  "dist x y < d"
   1.105 -    hence "f y \<noteq> a" using d[THEN bspec[where x=y]] assms(3)[unfolded dist_nz]
   1.106 -      apply auto unfolding dist_nz[THEN sym] by (auto simp add: dist_commute) }
   1.107 -  thus ?thesis using `d>0` by auto
   1.108 +  obtain U where "open U" and "f x \<in> U" and "a \<notin> U"
   1.109 +    using t1_space [OF `f x \<noteq> a`] by fast
   1.110 +  have "(f ---> f x) (at x within s)"
   1.111 +    using assms(1) by (simp add: continuous_within)
   1.112 +  hence "eventually (\<lambda>y. f y \<in> U) (at x within s)"
   1.113 +    using `open U` and `f x \<in> U`
   1.114 +    unfolding tendsto_def by fast
   1.115 +  hence "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
   1.116 +    using `a \<notin> U` by (fast elim: eventually_mono [rotated])
   1.117 +  thus ?thesis
   1.118 +    unfolding Limits.eventually_within Limits.eventually_at
   1.119 +    by (rule ex_forward, cut_tac `f x \<noteq> a`, auto simp: dist_commute)
   1.120  qed
   1.121  
   1.122  lemma continuous_at_avoid:
   1.123 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
   1.124 +  fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
   1.125    assumes "continuous (at x) f" and "f x \<noteq> a"
   1.126    shows "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> f y \<noteq> a"
   1.127    using assms continuous_within_avoid[of x UNIV f a] by simp
   1.128  
   1.129  lemma continuous_on_avoid:
   1.130 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   1.131 +  fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
   1.132    assumes "continuous_on s f"  "x \<in> s"  "f x \<noteq> a"
   1.133    shows "\<exists>e>0. \<forall>y \<in> s. dist x y < e \<longrightarrow> f y \<noteq> a"
   1.134 -using assms(1)[unfolded continuous_on_eq_continuous_within, THEN bspec[where x=x], OF assms(2)]  continuous_within_avoid[of x s f a]  assms(2,3) by auto
   1.135 +using assms(1)[unfolded continuous_on_eq_continuous_within, THEN bspec[where x=x], OF assms(2)]  continuous_within_avoid[of x s f a]  assms(3) by auto
   1.136  
   1.137  lemma continuous_on_open_avoid:
   1.138 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   1.139 +  fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
   1.140    assumes "continuous_on s f"  "open s"  "x \<in> s"  "f x \<noteq> a"
   1.141    shows "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> f y \<noteq> a"
   1.142 -using assms(1)[unfolded continuous_on_eq_continuous_at[OF assms(2)], THEN bspec[where x=x], OF assms(3)]  continuous_at_avoid[of x f a]  assms(3,4) by auto
   1.143 +using assms(1)[unfolded continuous_on_eq_continuous_at[OF assms(2)], THEN bspec[where x=x], OF assms(3)]  continuous_at_avoid[of x f a]  assms(4) by auto
   1.144  
   1.145  text {* Proving a function is constant by proving open-ness of level set. *}
   1.146  
   1.147 @@ -4790,23 +4822,83 @@
   1.148  
   1.149  text {* Preservation of compactness and connectedness under continuous function. *}
   1.150  
   1.151 +lemma compact_eq_openin_cover:
   1.152 +  "compact S \<longleftrightarrow>
   1.153 +    (\<forall>C. (\<forall>c\<in>C. openin (subtopology euclidean S) c) \<and> S \<subseteq> \<Union>C \<longrightarrow>
   1.154 +      (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
   1.155 +proof safe
   1.156 +  fix C
   1.157 +  assume "compact S" and "\<forall>c\<in>C. openin (subtopology euclidean S) c" and "S \<subseteq> \<Union>C"
   1.158 +  hence "\<forall>c\<in>{T. open T \<and> S \<inter> T \<in> C}. open c" and "S \<subseteq> \<Union>{T. open T \<and> S \<inter> T \<in> C}"
   1.159 +    unfolding openin_open by force+
   1.160 +  with `compact S` obtain D where "D \<subseteq> {T. open T \<and> S \<inter> T \<in> C}" and "finite D" and "S \<subseteq> \<Union>D"
   1.161 +    by (rule compactE)
   1.162 +  hence "image (\<lambda>T. S \<inter> T) D \<subseteq> C \<and> finite (image (\<lambda>T. S \<inter> T) D) \<and> S \<subseteq> \<Union>(image (\<lambda>T. S \<inter> T) D)"
   1.163 +    by auto
   1.164 +  thus "\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D" ..
   1.165 +next
   1.166 +  assume 1: "\<forall>C. (\<forall>c\<in>C. openin (subtopology euclidean S) c) \<and> S \<subseteq> \<Union>C \<longrightarrow>
   1.167 +        (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D)"
   1.168 +  show "compact S"
   1.169 +  proof (rule compactI)
   1.170 +    fix C
   1.171 +    let ?C = "image (\<lambda>T. S \<inter> T) C"
   1.172 +    assume "\<forall>t\<in>C. open t" and "S \<subseteq> \<Union>C"
   1.173 +    hence "(\<forall>c\<in>?C. openin (subtopology euclidean S) c) \<and> S \<subseteq> \<Union>?C"
   1.174 +      unfolding openin_open by auto
   1.175 +    with 1 obtain D where "D \<subseteq> ?C" and "finite D" and "S \<subseteq> \<Union>D"
   1.176 +      by metis
   1.177 +    let ?D = "inv_into C (\<lambda>T. S \<inter> T) ` D"
   1.178 +    have "?D \<subseteq> C \<and> finite ?D \<and> S \<subseteq> \<Union>?D"
   1.179 +    proof (intro conjI)
   1.180 +      from `D \<subseteq> ?C` show "?D \<subseteq> C"
   1.181 +        by (fast intro: inv_into_into)
   1.182 +      from `finite D` show "finite ?D"
   1.183 +        by (rule finite_imageI)
   1.184 +      from `S \<subseteq> \<Union>D` show "S \<subseteq> \<Union>?D"
   1.185 +        apply (rule subset_trans)
   1.186 +        apply clarsimp
   1.187 +        apply (frule subsetD [OF `D \<subseteq> ?C`, THEN f_inv_into_f])
   1.188 +        apply (erule rev_bexI, fast)
   1.189 +        done
   1.190 +    qed
   1.191 +    thus "\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D" ..
   1.192 +  qed
   1.193 +qed
   1.194 +
   1.195  lemma compact_continuous_image:
   1.196 -  fixes f :: "'a :: metric_space \<Rightarrow> 'b :: metric_space"
   1.197 -  assumes "continuous_on s f"  "compact s"
   1.198 -  shows "compact(f ` s)"
   1.199 -proof-
   1.200 -  { fix x assume x:"\<forall>n::nat. x n \<in> f ` s"
   1.201 -    then obtain y where y:"\<forall>n. y n \<in> s \<and> x n = f (y n)" unfolding image_iff Bex_def using choice[of "\<lambda>n xa. xa \<in> s \<and> x n = f xa"] by auto
   1.202 -    then obtain l r where "l\<in>s" and r:"subseq r" and lr:"((y \<circ> r) ---> l) sequentially" using assms(2)[unfolded compact_def, THEN spec[where x=y]] by auto
   1.203 -    { fix e::real assume "e>0"
   1.204 -      then obtain d where "d>0" and d:"\<forall>x'\<in>s. dist x' l < d \<longrightarrow> dist (f x') (f l) < e"
   1.205 -        using assms(1)[unfolded continuous_on_iff, THEN bspec[where x=l], OF `l\<in>s`] by auto
   1.206 -      then obtain N::nat where N:"\<forall>n\<ge>N. dist ((y \<circ> r) n) l < d" using lr[unfolded LIMSEQ_def, THEN spec[where x=d]] by auto
   1.207 -      { fix n::nat assume "n\<ge>N" hence "dist ((x \<circ> r) n) (f l) < e" using N[THEN spec[where x=n]] d[THEN bspec[where x="y (r n)"]] y[THEN spec[where x="r n"]] by auto  }
   1.208 -      hence "\<exists>N. \<forall>n\<ge>N. dist ((x \<circ> r) n) (f l) < e" by auto  }
   1.209 -    hence "\<exists>l\<in>f ` s. \<exists>r. subseq r \<and> ((x \<circ> r) ---> l) sequentially" unfolding LIMSEQ_def using r lr `l\<in>s` by auto  }
   1.210 -  thus ?thesis unfolding compact_def by auto
   1.211 -qed
   1.212 +  assumes "continuous_on s f" and "compact s"
   1.213 +  shows "compact (f ` s)"
   1.214 +using assms (* FIXME: long unstructured proof *)
   1.215 +unfolding continuous_on_open
   1.216 +unfolding compact_eq_openin_cover
   1.217 +apply clarify
   1.218 +apply (drule_tac x="image (\<lambda>t. {x \<in> s. f x \<in> t}) C" in spec)
   1.219 +apply (drule mp)
   1.220 +apply (rule conjI)
   1.221 +apply simp
   1.222 +apply clarsimp
   1.223 +apply (drule subsetD)
   1.224 +apply (erule imageI)
   1.225 +apply fast
   1.226 +apply (erule thin_rl)
   1.227 +apply clarify
   1.228 +apply (rule_tac x="image (inv_into C (\<lambda>t. {x \<in> s. f x \<in> t})) D" in exI)
   1.229 +apply (intro conjI)
   1.230 +apply clarify
   1.231 +apply (rule inv_into_into)
   1.232 +apply (erule (1) subsetD)
   1.233 +apply (erule finite_imageI)
   1.234 +apply (clarsimp, rename_tac x)
   1.235 +apply (drule (1) subsetD, clarify)
   1.236 +apply (drule (1) subsetD, clarify)
   1.237 +apply (rule rev_bexI)
   1.238 +apply assumption
   1.239 +apply (subgoal_tac "{x \<in> s. f x \<in> t} \<in> (\<lambda>t. {x \<in> s. f x \<in> t}) ` C")
   1.240 +apply (drule f_inv_into_f)
   1.241 +apply fast
   1.242 +apply (erule imageI)
   1.243 +done
   1.244  
   1.245  lemma connected_continuous_image:
   1.246    assumes "continuous_on s f"  "connected s"
   1.247 @@ -4862,25 +4954,33 @@
   1.248  text{* Continuity of inverse function on compact domain. *}
   1.249  
   1.250  lemma continuous_on_inv:
   1.251 -  fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
   1.252 -    (* TODO: can this be generalized more? *)
   1.253 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::t2_space"
   1.254    assumes "continuous_on s f"  "compact s"  "\<forall>x \<in> s. g (f x) = x"
   1.255    shows "continuous_on (f ` s) g"
   1.256 -proof-
   1.257 -  have *:"g ` f ` s = s" using assms(3) by (auto simp add: image_iff)
   1.258 -  { fix t assume t:"closedin (subtopology euclidean (g ` f ` s)) t"
   1.259 -    then obtain T where T: "closed T" "t = s \<inter> T" unfolding closedin_closed unfolding * by auto
   1.260 -    have "continuous_on (s \<inter> T) f" using continuous_on_subset[OF assms(1), of "s \<inter> t"]
   1.261 -      unfolding T(2) and Int_left_absorb by auto
   1.262 -    moreover have "compact (s \<inter> T)"
   1.263 -      using assms(2) unfolding compact_eq_bounded_closed
   1.264 -      using bounded_subset[of s "s \<inter> T"] and T(1) by auto
   1.265 -    ultimately have "closed (f ` t)" using T(1) unfolding T(2)
   1.266 -      using compact_continuous_image [of "s \<inter> T" f] unfolding compact_eq_bounded_closed by auto
   1.267 -    moreover have "{x \<in> f ` s. g x \<in> t} = f ` s \<inter> f ` t" using assms(3) unfolding T(2) by auto
   1.268 -    ultimately have "closedin (subtopology euclidean (f ` s)) {x \<in> f ` s. g x \<in> t}"
   1.269 -      unfolding closedin_closed by auto  }
   1.270 -  thus ?thesis unfolding continuous_on_closed by auto
   1.271 +unfolding continuous_on_topological
   1.272 +proof (clarsimp simp add: assms(3))
   1.273 +  fix x :: 'a and B :: "'a set"
   1.274 +  assume "x \<in> s" and "open B" and "x \<in> B"
   1.275 +  have 1: "\<forall>x\<in>s. f x \<in> f ` (s - B) \<longleftrightarrow> x \<in> s - B"
   1.276 +    using assms(3) by (auto, metis)
   1.277 +  have "continuous_on (s - B) f"
   1.278 +    using `continuous_on s f` Diff_subset
   1.279 +    by (rule continuous_on_subset)
   1.280 +  moreover have "compact (s - B)"
   1.281 +    using `open B` and `compact s`
   1.282 +    unfolding Diff_eq by (intro compact_inter_closed closed_Compl)
   1.283 +  ultimately have "compact (f ` (s - B))"
   1.284 +    by (rule compact_continuous_image)
   1.285 +  hence "closed (f ` (s - B))"
   1.286 +    by (rule compact_imp_closed)
   1.287 +  hence "open (- f ` (s - B))"
   1.288 +    by (rule open_Compl)
   1.289 +  moreover have "f x \<in> - f ` (s - B)"
   1.290 +    using `x \<in> s` and `x \<in> B` by (simp add: 1)
   1.291 +  moreover have "\<forall>y\<in>s. f y \<in> - f ` (s - B) \<longrightarrow> y \<in> B"
   1.292 +    by (simp add: 1)
   1.293 +  ultimately show "\<exists>A. open A \<and> f x \<in> A \<and> (\<forall>y\<in>s. f y \<in> A \<longrightarrow> y \<in> B)"
   1.294 +    by fast
   1.295  qed
   1.296  
   1.297  text {* A uniformly convergent limit of continuous functions is continuous. *}
   1.298 @@ -6043,7 +6143,7 @@
   1.299       (\<forall>y\<in>t. (f(g y) = y)) \<and> (g ` t = s) \<and> continuous_on t g"
   1.300  
   1.301  definition
   1.302 -  homeomorphic :: "'a::metric_space set \<Rightarrow> 'b::metric_space set \<Rightarrow> bool"
   1.303 +  homeomorphic :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
   1.304      (infixr "homeomorphic" 60) where
   1.305    homeomorphic_def: "s homeomorphic t \<equiv> (\<exists>f g. homeomorphism s t f g)"
   1.306  
   1.307 @@ -6095,8 +6195,7 @@
   1.308  text {* Relatively weak hypotheses if a set is compact. *}
   1.309  
   1.310  lemma homeomorphism_compact:
   1.311 -  fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
   1.312 -    (* class constraint due to continuous_on_inv *)
   1.313 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::t2_space"
   1.314    assumes "compact s" "continuous_on s f"  "f ` s = t"  "inj_on f s"
   1.315    shows "\<exists>g. homeomorphism s t f g"
   1.316  proof-
   1.317 @@ -6123,8 +6222,7 @@
   1.318  qed
   1.319  
   1.320  lemma homeomorphic_compact:
   1.321 -  fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
   1.322 -    (* class constraint due to continuous_on_inv *)
   1.323 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::t2_space"
   1.324    shows "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s
   1.325            \<Longrightarrow> s homeomorphic t"
   1.326    unfolding homeomorphic_def by (metis homeomorphism_compact)
   1.327 @@ -6166,12 +6264,11 @@
   1.328  qed
   1.329  
   1.330  lemma homeomorphic_balls:
   1.331 -  fixes a b ::"'a::real_normed_vector" (* FIXME: generalize to metric_space *)
   1.332 +  fixes a b ::"'a::real_normed_vector"
   1.333    assumes "0 < d"  "0 < e"
   1.334    shows "(ball a d) homeomorphic  (ball b e)" (is ?th)
   1.335          "(cball a d) homeomorphic (cball b e)" (is ?cth)
   1.336  proof-
   1.337 -  have *:"\<bar>e / d\<bar> > 0" "\<bar>d / e\<bar> >0" using assms using divide_pos_pos by auto
   1.338    show ?th unfolding homeomorphic_minimal
   1.339      apply(rule_tac x="\<lambda>x. b + (e/d) *\<^sub>R (x - a)" in exI)
   1.340      apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)
   1.341 @@ -6181,7 +6278,6 @@
   1.342      unfolding continuous_on
   1.343      by (intro ballI tendsto_intros, simp)+
   1.344  next
   1.345 -  have *:"\<bar>e / d\<bar> > 0" "\<bar>d / e\<bar> >0" using assms using divide_pos_pos by auto
   1.346    show ?cth unfolding homeomorphic_minimal
   1.347      apply(rule_tac x="\<lambda>x. b + (e/d) *\<^sub>R (x - a)" in exI)
   1.348      apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)