86 lemma continuous_map_Euclidean_space_diff [continuous_intros]: |
86 lemma continuous_map_Euclidean_space_diff [continuous_intros]: |
87 "\<lbrakk>continuous_map X (Euclidean_space n) f; continuous_map X (Euclidean_space n) g\<rbrakk> |
87 "\<lbrakk>continuous_map X (Euclidean_space n) f; continuous_map X (Euclidean_space n) g\<rbrakk> |
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 |
|
92 lemma continuous_map_Euclidean_space_iff: |
|
93 "continuous_map (Euclidean_space m) euclideanreal g |
|
94 = continuous_on (topspace (Euclidean_space m)) g" |
|
95 proof |
|
96 assume "continuous_map (Euclidean_space m) euclideanreal g" |
|
97 then have "continuous_map (top_of_set {f. \<forall>n\<ge>m. f n = 0}) euclideanreal g" |
|
98 by (simp add: Euclidean_space_def euclidean_product_topology) |
|
99 then show "continuous_on (topspace (Euclidean_space m)) g" |
|
100 by (metis continuous_map_subtopology_eu subtopology_topspace topspace_Euclidean_space) |
|
101 next |
|
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" |
|
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" |
|
106 by (simp add: Euclidean_space_def euclidean_product_topology) |
|
107 qed |
|
108 |
|
109 lemma cm_Euclidean_space_iff_continuous_on: |
|
110 "continuous_map (subtopology (Euclidean_space m) S) (Euclidean_space n) f |
|
111 \<longleftrightarrow> continuous_on (topspace (subtopology (Euclidean_space m) S)) f \<and> |
|
112 f ` (topspace (subtopology (Euclidean_space m) S)) \<subseteq> topspace (Euclidean_space n)" |
|
113 (is "?P \<longleftrightarrow> ?Q \<and> ?R") |
|
114 proof - |
|
115 have ?Q if ?P |
|
116 proof - |
|
117 have "\<And>n. Euclidean_space n = top_of_set {f. \<forall>m\<ge>n. f m = 0}" |
|
118 by (simp add: Euclidean_space_def euclidean_product_topology) |
|
119 with that show ?thesis |
|
120 by (simp add: subtopology_subtopology) |
|
121 qed |
|
122 moreover |
|
123 have ?R if ?P |
|
124 using that by (simp add: image_subset_iff continuous_map_def) |
|
125 moreover |
|
126 have ?P if ?Q ?R |
|
127 proof - |
|
128 have "continuous_map (top_of_set (topspace (subtopology (subtopology (powertop_real UNIV) {f. \<forall>n\<ge>m. f n = 0}) S))) (top_of_set (topspace (subtopology (powertop_real UNIV) {f. \<forall>na\<ge>n. f na = 0}))) f" |
|
129 using Euclidean_space_def that by auto |
|
130 then show ?thesis |
|
131 by (simp add: Euclidean_space_def euclidean_product_topology subtopology_subtopology) |
|
132 qed |
|
133 ultimately show ?thesis |
|
134 by auto |
|
135 qed |
91 |
136 |
92 lemma homeomorphic_Euclidean_space_product_topology: |
137 lemma homeomorphic_Euclidean_space_product_topology: |
93 "Euclidean_space n homeomorphic_space product_topology (\<lambda>i. euclideanreal) {..<n}" |
138 "Euclidean_space n homeomorphic_space product_topology (\<lambda>i. euclideanreal) {..<n}" |
94 proof - |
139 proof - |
95 have cm: "continuous_map (product_topology (\<lambda>i. euclideanreal) {..<n}) |
140 have cm: "continuous_map (product_topology (\<lambda>i. euclideanreal) {..<n}) |
122 using locally_path_connected_space_euclideanreal by auto |
167 using locally_path_connected_space_euclideanreal by auto |
123 |
168 |
124 lemma compact_Euclidean_space: |
169 lemma compact_Euclidean_space: |
125 "compact_space (Euclidean_space n) \<longleftrightarrow> n = 0" |
170 "compact_space (Euclidean_space n) \<longleftrightarrow> n = 0" |
126 by (auto simp: homeomorphic_compact_space [OF homeomorphic_Euclidean_space_product_topology] compact_space_product_topology) |
171 by (auto simp: homeomorphic_compact_space [OF homeomorphic_Euclidean_space_product_topology] compact_space_product_topology) |
|
172 |
127 |
173 |
128 subsection\<open>n-dimensional spheres\<close> |
174 subsection\<open>n-dimensional spheres\<close> |
129 |
175 |
130 definition nsphere where |
176 definition nsphere where |
131 "nsphere n \<equiv> subtopology (Euclidean_space (Suc n)) { x. (\<Sum>i\<le>n. x i ^ 2) = 1 }" |
177 "nsphere n \<equiv> subtopology (Euclidean_space (Suc n)) { x. (\<Sum>i\<le>n. x i ^ 2) = 1 }" |