88 \<Longrightarrow> continuous_map X (Euclidean_space n) (\<lambda>x i. f x i - g x i)" |
88 \<Longrightarrow> continuous_map X (Euclidean_space n) (\<lambda>x i. f x i - g x i)" |
89 unfolding Euclidean_space_def continuous_map_in_subtopology |
89 unfolding Euclidean_space_def continuous_map_in_subtopology |
90 by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_diff) |
90 by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_diff) |
91 |
91 |
92 lemma continuous_map_Euclidean_space_iff: |
92 lemma continuous_map_Euclidean_space_iff: |
93 "continuous_map (Euclidean_space m) euclideanreal g |
93 "continuous_map (Euclidean_space m) euclidean g |
94 = continuous_on (topspace (Euclidean_space m)) g" |
94 = continuous_on (topspace (Euclidean_space m)) g" |
95 proof |
95 proof |
96 assume "continuous_map (Euclidean_space m) euclideanreal g" |
96 assume "continuous_map (Euclidean_space m) euclidean g" |
97 then have "continuous_map (top_of_set {f. \<forall>n\<ge>m. f n = 0}) euclideanreal g" |
97 then have "continuous_map (top_of_set {f. \<forall>n\<ge>m. f n = 0}) euclidean g" |
98 by (simp add: Euclidean_space_def euclidean_product_topology) |
98 by (simp add: Euclidean_space_def euclidean_product_topology) |
99 then show "continuous_on (topspace (Euclidean_space m)) g" |
99 then show "continuous_on (topspace (Euclidean_space m)) g" |
100 by (metis continuous_map_subtopology_eu subtopology_topspace topspace_Euclidean_space) |
100 by (metis continuous_map_subtopology_eu subtopology_topspace topspace_Euclidean_space) |
101 next |
101 next |
102 assume "continuous_on (topspace (Euclidean_space m)) g" |
102 assume "continuous_on (topspace (Euclidean_space m)) g" |
103 then have "continuous_map (top_of_set {f. \<forall>n\<ge>m. f n = 0}) euclideanreal g" |
103 then have "continuous_map (top_of_set {f. \<forall>n\<ge>m. f n = 0}) euclidean g" |
104 by (metis (lifting) continuous_map_into_fulltopology continuous_map_subtopology_eu order_refl topspace_Euclidean_space) |
104 by (metis (lifting) continuous_map_into_fulltopology continuous_map_subtopology_eu order_refl topspace_Euclidean_space) |
105 then show "continuous_map (Euclidean_space m) euclideanreal g" |
105 then show "continuous_map (Euclidean_space m) euclidean g" |
106 by (simp add: Euclidean_space_def euclidean_product_topology) |
106 by (simp add: Euclidean_space_def euclidean_product_topology) |
107 qed |
107 qed |
108 |
108 |
109 lemma cm_Euclidean_space_iff_continuous_on: |
109 lemma cm_Euclidean_space_iff_continuous_on: |
110 "continuous_map (subtopology (Euclidean_space m) S) (Euclidean_space n) f |
110 "continuous_map (subtopology (Euclidean_space m) S) (Euclidean_space n) f |
197 have "({x. (\<Sum>i\<le>n. (x i)\<^sup>2) + (x (Suc n))\<^sup>2 = 1 \<and> (\<forall>i>Suc n. x i = 0)} \<inter> {x. x (Suc n) = 0}) |
197 have "({x. (\<Sum>i\<le>n. (x i)\<^sup>2) + (x (Suc n))\<^sup>2 = 1 \<and> (\<forall>i>Suc n. x i = 0)} \<inter> {x. x (Suc n) = 0}) |
198 = {x. (\<Sum>i\<le>n. (x i)\<^sup>2) = 1 \<and> (\<forall>i>n. x i = (0::real))}" |
198 = {x. (\<Sum>i\<le>n. (x i)\<^sup>2) = 1 \<and> (\<forall>i>n. x i = (0::real))}" |
199 using Suc_lessI [of n] by (fastforce simp: set_eq_iff) |
199 using Suc_lessI [of n] by (fastforce simp: set_eq_iff) |
200 then show ?thesis |
200 then show ?thesis |
201 by (simp add: nsphere subtopology_subtopology) |
201 by (simp add: nsphere subtopology_subtopology) |
|
202 qed |
|
203 |
|
204 lemma topspace_nsphere_minus1: |
|
205 assumes x: "x \<in> topspace (nsphere n)" and "x n = 0" |
|
206 shows "x \<in> topspace (nsphere (n - Suc 0))" |
|
207 proof (cases "n = 0") |
|
208 case True |
|
209 then show ?thesis |
|
210 using x by auto |
|
211 next |
|
212 case False |
|
213 have subt_eq: "nsphere (n - Suc 0) = subtopology (nsphere n) {x. x n = 0}" |
|
214 by (metis False Suc_pred le_zero_eq not_le subtopology_nsphere_equator) |
|
215 with x show ?thesis |
|
216 by (simp add: assms) |
202 qed |
217 qed |
203 |
218 |
204 lemma continuous_map_nsphere_reflection: |
219 lemma continuous_map_nsphere_reflection: |
205 "continuous_map (nsphere n) (nsphere n) (\<lambda>x i. if i = k then -x i else x i)" |
220 "continuous_map (nsphere n) (nsphere n) (\<lambda>x i. if i = k then -x i else x i)" |
206 proof - |
221 proof - |