114 proof safe |
129 proof safe |
115 assume cont: "continuous_on {0..1} (g1 +++ g2)" |
130 assume cont: "continuous_on {0..1} (g1 +++ g2)" |
116 have g1: "continuous_on {0..1} g1 \<longleftrightarrow> continuous_on {0..1} ((g1 +++ g2) \<circ> (\<lambda>x. x / 2))" |
131 have g1: "continuous_on {0..1} g1 \<longleftrightarrow> continuous_on {0..1} ((g1 +++ g2) \<circ> (\<lambda>x. x / 2))" |
117 by (intro continuous_on_cong refl) (auto simp: joinpaths_def) |
132 by (intro continuous_on_cong refl) (auto simp: joinpaths_def) |
118 have g2: "continuous_on {0..1} g2 \<longleftrightarrow> continuous_on {0..1} ((g1 +++ g2) \<circ> (\<lambda>x. x / 2 + 1/2))" |
133 have g2: "continuous_on {0..1} g2 \<longleftrightarrow> continuous_on {0..1} ((g1 +++ g2) \<circ> (\<lambda>x. x / 2 + 1/2))" |
119 using assms by (intro continuous_on_cong refl) (auto simp: joinpaths_def pathfinish_def pathstart_def) |
134 using assms |
120 show "continuous_on {0..1} g1" "continuous_on {0..1} g2" |
135 by (intro continuous_on_cong refl) (auto simp: joinpaths_def pathfinish_def pathstart_def) |
|
136 show "continuous_on {0..1} g1" and "continuous_on {0..1} g2" |
121 unfolding g1 g2 |
137 unfolding g1 g2 |
122 by (auto intro!: continuous_on_intros continuous_on_subset[OF cont] simp del: o_apply) |
138 by (auto intro!: continuous_on_intros continuous_on_subset[OF cont] simp del: o_apply) |
123 next |
139 next |
124 assume g1g2: "continuous_on {0..1} g1" "continuous_on {0..1} g2" |
140 assume g1g2: "continuous_on {0..1} g1" "continuous_on {0..1} g2" |
125 have 01: "{0 .. 1} = {0..1/2} \<union> {1/2 .. 1::real}" |
141 have 01: "{0 .. 1} = {0..1/2} \<union> {1/2 .. 1::real}" |
126 by auto |
142 by auto |
127 { fix x :: real assume "0 \<le> x" "x \<le> 1" then have "x \<in> (\<lambda>x. x * 2) ` {0..1 / 2}" |
143 { |
128 by (intro image_eqI[where x="x/2"]) auto } |
144 fix x :: real |
|
145 assume "0 \<le> x" and "x \<le> 1" |
|
146 then have "x \<in> (\<lambda>x. x * 2) ` {0..1 / 2}" |
|
147 by (intro image_eqI[where x="x/2"]) auto |
|
148 } |
129 note 1 = this |
149 note 1 = this |
130 { fix x :: real assume "0 \<le> x" "x \<le> 1" then have "x \<in> (\<lambda>x. x * 2 - 1) ` {1 / 2..1}" |
150 { |
131 by (intro image_eqI[where x="x/2 + 1/2"]) auto } |
151 fix x :: real |
|
152 assume "0 \<le> x" and "x \<le> 1" |
|
153 then have "x \<in> (\<lambda>x. x * 2 - 1) ` {1 / 2..1}" |
|
154 by (intro image_eqI[where x="x/2 + 1/2"]) auto |
|
155 } |
132 note 2 = this |
156 note 2 = this |
133 show "continuous_on {0..1} (g1 +++ g2)" |
157 show "continuous_on {0..1} (g1 +++ g2)" |
134 using assms unfolding joinpaths_def 01 |
158 using assms |
135 by (intro continuous_on_cases closed_atLeastAtMost g1g2[THEN continuous_on_compose2] continuous_on_intros) |
159 unfolding joinpaths_def 01 |
136 (auto simp: field_simps pathfinish_def pathstart_def intro!: 1 2) |
160 apply (intro continuous_on_cases closed_atLeastAtMost g1g2[THEN continuous_on_compose2] continuous_on_intros) |
137 qed |
161 apply (auto simp: field_simps pathfinish_def pathstart_def intro!: 1 2) |
138 |
162 done |
139 lemma path_image_join_subset: "path_image(g1 +++ g2) \<subseteq> (path_image g1 \<union> path_image g2)" |
163 qed |
140 unfolding path_image_def joinpaths_def by auto |
164 |
|
165 lemma path_image_join_subset: "path_image (g1 +++ g2) \<subseteq> path_image g1 \<union> path_image g2" |
|
166 unfolding path_image_def joinpaths_def |
|
167 by auto |
141 |
168 |
142 lemma subset_path_image_join: |
169 lemma subset_path_image_join: |
143 assumes "path_image g1 \<subseteq> s" "path_image g2 \<subseteq> s" |
170 assumes "path_image g1 \<subseteq> s" |
144 shows "path_image(g1 +++ g2) \<subseteq> s" |
171 and "path_image g2 \<subseteq> s" |
145 using path_image_join_subset[of g1 g2] and assms by auto |
172 shows "path_image (g1 +++ g2) \<subseteq> s" |
|
173 using path_image_join_subset[of g1 g2] and assms |
|
174 by auto |
146 |
175 |
147 lemma path_image_join: |
176 lemma path_image_join: |
148 assumes "pathfinish g1 = pathstart g2" |
177 assumes "pathfinish g1 = pathstart g2" |
149 shows "path_image(g1 +++ g2) = (path_image g1) \<union> (path_image g2)" |
178 shows "path_image (g1 +++ g2) = path_image g1 \<union> path_image g2" |
150 apply (rule, rule path_image_join_subset, rule) |
179 apply rule |
|
180 apply (rule path_image_join_subset) |
|
181 apply rule |
151 unfolding Un_iff |
182 unfolding Un_iff |
152 proof (erule disjE) |
183 proof (erule disjE) |
153 fix x |
184 fix x |
154 assume "x \<in> path_image g1" |
185 assume "x \<in> path_image g1" |
155 then obtain y where y: "y\<in>{0..1}" "x = g1 y" |
186 then obtain y where y: "y \<in> {0..1}" "x = g1 y" |
156 unfolding path_image_def image_iff by auto |
187 unfolding path_image_def image_iff by auto |
157 then show "x \<in> path_image (g1 +++ g2)" |
188 then show "x \<in> path_image (g1 +++ g2)" |
158 unfolding joinpaths_def path_image_def image_iff |
189 unfolding joinpaths_def path_image_def image_iff |
159 apply (rule_tac x="(1/2) *\<^sub>R y" in bexI) |
190 apply (rule_tac x="(1/2) *\<^sub>R y" in bexI) |
160 apply auto |
191 apply auto |
161 done |
192 done |
162 next |
193 next |
163 fix x |
194 fix x |
164 assume "x \<in> path_image g2" |
195 assume "x \<in> path_image g2" |
165 then obtain y where y: "y\<in>{0..1}" "x = g2 y" |
196 then obtain y where y: "y \<in> {0..1}" "x = g2 y" |
166 unfolding path_image_def image_iff by auto |
197 unfolding path_image_def image_iff by auto |
167 then show "x \<in> path_image (g1 +++ g2)" |
198 then show "x \<in> path_image (g1 +++ g2)" |
168 unfolding joinpaths_def path_image_def image_iff |
199 unfolding joinpaths_def path_image_def image_iff |
169 apply(rule_tac x="(1/2) *\<^sub>R (y + 1)" in bexI) |
200 apply (rule_tac x="(1/2) *\<^sub>R (y + 1)" in bexI) |
170 using assms(1)[unfolded pathfinish_def pathstart_def] |
201 using assms(1)[unfolded pathfinish_def pathstart_def] |
171 apply (auto simp add: add_divide_distrib) |
202 apply (auto simp add: add_divide_distrib) |
172 done |
203 done |
173 qed |
204 qed |
174 |
205 |
175 lemma not_in_path_image_join: |
206 lemma not_in_path_image_join: |
176 assumes "x \<notin> path_image g1" "x \<notin> path_image g2" |
207 assumes "x \<notin> path_image g1" |
177 shows "x \<notin> path_image(g1 +++ g2)" |
208 and "x \<notin> path_image g2" |
178 using assms and path_image_join_subset[of g1 g2] by auto |
209 shows "x \<notin> path_image (g1 +++ g2)" |
|
210 using assms and path_image_join_subset[of g1 g2] |
|
211 by auto |
179 |
212 |
180 lemma simple_path_reversepath: |
213 lemma simple_path_reversepath: |
181 assumes "simple_path g" |
214 assumes "simple_path g" |
182 shows "simple_path (reversepath g)" |
215 shows "simple_path (reversepath g)" |
183 using assms |
216 using assms |
184 unfolding simple_path_def reversepath_def |
217 unfolding simple_path_def reversepath_def |
185 apply - |
218 apply - |
186 apply (rule ballI)+ |
219 apply (rule ballI)+ |
187 apply (erule_tac x="1-x" in ballE, erule_tac x="1-y" in ballE) |
220 apply (erule_tac x="1-x" in ballE) |
|
221 apply (erule_tac x="1-y" in ballE) |
188 apply auto |
222 apply auto |
189 done |
223 done |
190 |
224 |
191 lemma simple_path_join_loop: |
225 lemma simple_path_join_loop: |
192 assumes "injective_path g1" "injective_path g2" "pathfinish g2 = pathstart g1" |
226 assumes "injective_path g1" |
193 "(path_image g1 \<inter> path_image g2) \<subseteq> {pathstart g1,pathstart g2}" |
227 and "injective_path g2" |
194 shows "simple_path(g1 +++ g2)" |
228 and "pathfinish g2 = pathstart g1" |
|
229 and "path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g1, pathstart g2}" |
|
230 shows "simple_path (g1 +++ g2)" |
195 unfolding simple_path_def |
231 unfolding simple_path_def |
196 proof ((rule ballI)+, rule impI) |
232 proof (intro ballI impI) |
197 let ?g = "g1 +++ g2" |
233 let ?g = "g1 +++ g2" |
198 note inj = assms(1,2)[unfolded injective_path_def, rule_format] |
234 note inj = assms(1,2)[unfolded injective_path_def, rule_format] |
199 fix x y :: real |
235 fix x y :: real |
200 assume xy: "x \<in> {0..1}" "y \<in> {0..1}" "?g x = ?g y" |
236 assume xy: "x \<in> {0..1}" "y \<in> {0..1}" "?g x = ?g y" |
201 show "x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0" |
237 show "x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0" |
202 proof (case_tac "x \<le> 1/2", case_tac[!] "y \<le> 1/2", unfold not_le) |
238 proof (cases "x \<le> 1/2", case_tac[!] "y \<le> 1/2", unfold not_le) |
203 assume as: "x \<le> 1 / 2" "y \<le> 1 / 2" |
239 assume as: "x \<le> 1 / 2" "y \<le> 1 / 2" |
204 then have "g1 (2 *\<^sub>R x) = g1 (2 *\<^sub>R y)" |
240 then have "g1 (2 *\<^sub>R x) = g1 (2 *\<^sub>R y)" |
205 using xy(3) unfolding joinpaths_def by auto |
241 using xy(3) |
206 moreover |
242 unfolding joinpaths_def |
207 have "2 *\<^sub>R x \<in> {0..1}" "2 *\<^sub>R y \<in> {0..1}" using xy(1,2) as |
243 by auto |
208 by auto |
244 moreover have "2 *\<^sub>R x \<in> {0..1}" "2 *\<^sub>R y \<in> {0..1}" |
209 ultimately |
245 using xy(1,2) as |
210 show ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] by auto |
246 by auto |
|
247 ultimately show ?thesis |
|
248 using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] |
|
249 by auto |
211 next |
250 next |
212 assume as:"x > 1 / 2" "y > 1 / 2" |
251 assume as: "x > 1 / 2" "y > 1 / 2" |
213 then have "g2 (2 *\<^sub>R x - 1) = g2 (2 *\<^sub>R y - 1)" |
252 then have "g2 (2 *\<^sub>R x - 1) = g2 (2 *\<^sub>R y - 1)" |
214 using xy(3) unfolding joinpaths_def by auto |
253 using xy(3) |
215 moreover |
254 unfolding joinpaths_def |
216 have "2 *\<^sub>R x - 1 \<in> {0..1}" "2 *\<^sub>R y - 1 \<in> {0..1}" |
255 by auto |
217 using xy(1,2) as by auto |
256 moreover have "2 *\<^sub>R x - 1 \<in> {0..1}" "2 *\<^sub>R y - 1 \<in> {0..1}" |
218 ultimately |
257 using xy(1,2) as |
219 show ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] by auto |
258 by auto |
|
259 ultimately show ?thesis |
|
260 using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] by auto |
220 next |
261 next |
221 assume as:"x \<le> 1 / 2" "y > 1 / 2" |
262 assume as: "x \<le> 1 / 2" "y > 1 / 2" |
222 then have "?g x \<in> path_image g1" "?g y \<in> path_image g2" |
263 then have "?g x \<in> path_image g1" "?g y \<in> path_image g2" |
223 unfolding path_image_def joinpaths_def |
264 unfolding path_image_def joinpaths_def |
224 using xy(1,2) by auto |
265 using xy(1,2) by auto |
225 moreover |
266 moreover have "?g y \<noteq> pathstart g2" |
226 have "?g y \<noteq> pathstart g2" using as(2) unfolding pathstart_def joinpaths_def |
267 using as(2) |
|
268 unfolding pathstart_def joinpaths_def |
227 using inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(2) |
269 using inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(2) |
228 by (auto simp add: field_simps) |
270 by (auto simp add: field_simps) |
229 ultimately |
271 ultimately have *: "?g x = pathstart g1" |
230 have *:"?g x = pathstart g1" using assms(4) unfolding xy(3) by auto |
272 using assms(4) |
231 then have "x = 0" unfolding pathstart_def joinpaths_def using as(1) and xy(1) |
273 unfolding xy(3) |
232 using inj(1)[of "2 *\<^sub>R x" 0] by auto |
274 by auto |
233 moreover |
275 then have "x = 0" |
234 have "y = 1" using * unfolding xy(3) assms(3)[THEN sym] |
276 unfolding pathstart_def joinpaths_def |
235 unfolding joinpaths_def pathfinish_def using as(2) and xy(2) |
277 using as(1) and xy(1) |
236 using inj(2)[of "2 *\<^sub>R y - 1" 1] by auto |
278 using inj(1)[of "2 *\<^sub>R x" 0] |
237 ultimately show ?thesis by auto |
279 by auto |
|
280 moreover have "y = 1" |
|
281 using * |
|
282 unfolding xy(3) assms(3)[symmetric] |
|
283 unfolding joinpaths_def pathfinish_def |
|
284 using as(2) and xy(2) |
|
285 using inj(2)[of "2 *\<^sub>R y - 1" 1] |
|
286 by auto |
|
287 ultimately show ?thesis |
|
288 by auto |
238 next |
289 next |
239 assume as: "x > 1 / 2" "y \<le> 1 / 2" |
290 assume as: "x > 1 / 2" "y \<le> 1 / 2" |
240 then have "?g x \<in> path_image g2" "?g y \<in> path_image g1" |
291 then have "?g x \<in> path_image g2" and "?g y \<in> path_image g1" |
241 unfolding path_image_def joinpaths_def |
292 unfolding path_image_def joinpaths_def |
242 using xy(1,2) by auto |
293 using xy(1,2) by auto |
243 moreover |
294 moreover have "?g x \<noteq> pathstart g2" |
244 have "?g x \<noteq> pathstart g2" using as(1) unfolding pathstart_def joinpaths_def |
295 using as(1) |
|
296 unfolding pathstart_def joinpaths_def |
245 using inj(2)[of "2 *\<^sub>R x - 1" 0] and xy(1) |
297 using inj(2)[of "2 *\<^sub>R x - 1" 0] and xy(1) |
246 by (auto simp add: field_simps) |
298 by (auto simp add: field_simps) |
247 ultimately |
299 ultimately have *: "?g y = pathstart g1" |
248 have *: "?g y = pathstart g1" using assms(4) unfolding xy(3) by auto |
300 using assms(4) |
249 then have "y = 0" unfolding pathstart_def joinpaths_def using as(2) and xy(2) |
301 unfolding xy(3) |
250 using inj(1)[of "2 *\<^sub>R y" 0] by auto |
302 by auto |
251 moreover |
303 then have "y = 0" |
252 have "x = 1" using * unfolding xy(3)[THEN sym] assms(3)[THEN sym] |
304 unfolding pathstart_def joinpaths_def |
|
305 using as(2) and xy(2) |
|
306 using inj(1)[of "2 *\<^sub>R y" 0] |
|
307 by auto |
|
308 moreover have "x = 1" |
|
309 using * |
|
310 unfolding xy(3)[symmetric] assms(3)[symmetric] |
253 unfolding joinpaths_def pathfinish_def using as(1) and xy(1) |
311 unfolding joinpaths_def pathfinish_def using as(1) and xy(1) |
254 using inj(2)[of "2 *\<^sub>R x - 1" 1] by auto |
312 using inj(2)[of "2 *\<^sub>R x - 1" 1] |
255 ultimately show ?thesis by auto |
313 by auto |
|
314 ultimately show ?thesis |
|
315 by auto |
256 qed |
316 qed |
257 qed |
317 qed |
258 |
318 |
259 lemma injective_path_join: |
319 lemma injective_path_join: |
260 assumes "injective_path g1" "injective_path g2" "pathfinish g1 = pathstart g2" |
320 assumes "injective_path g1" |
261 "(path_image g1 \<inter> path_image g2) \<subseteq> {pathstart g2}" |
321 and "injective_path g2" |
262 shows "injective_path(g1 +++ g2)" |
322 and "pathfinish g1 = pathstart g2" |
|
323 and "path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g2}" |
|
324 shows "injective_path (g1 +++ g2)" |
263 unfolding injective_path_def |
325 unfolding injective_path_def |
264 proof (rule, rule, rule) |
326 proof (rule, rule, rule) |
265 let ?g = "g1 +++ g2" |
327 let ?g = "g1 +++ g2" |
266 note inj = assms(1,2)[unfolded injective_path_def, rule_format] |
328 note inj = assms(1,2)[unfolded injective_path_def, rule_format] |
267 fix x y |
329 fix x y |
268 assume xy: "x \<in> {0..1}" "y \<in> {0..1}" "(g1 +++ g2) x = (g1 +++ g2) y" |
330 assume xy: "x \<in> {0..1}" "y \<in> {0..1}" "(g1 +++ g2) x = (g1 +++ g2) y" |
269 show "x = y" |
331 show "x = y" |
270 proof (cases "x \<le> 1/2", case_tac[!] "y \<le> 1/2", unfold not_le) |
332 proof (cases "x \<le> 1/2", case_tac[!] "y \<le> 1/2", unfold not_le) |
271 assume "x \<le> 1 / 2" "y \<le> 1 / 2" |
333 assume "x \<le> 1 / 2" and "y \<le> 1 / 2" |
272 then show ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] and xy |
334 then show ?thesis |
|
335 using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] and xy |
273 unfolding joinpaths_def by auto |
336 unfolding joinpaths_def by auto |
274 next |
337 next |
275 assume "x > 1 / 2" "y > 1 / 2" |
338 assume "x > 1 / 2" and "y > 1 / 2" |
276 then show ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] and xy |
339 then show ?thesis |
|
340 using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] and xy |
277 unfolding joinpaths_def by auto |
341 unfolding joinpaths_def by auto |
278 next |
342 next |
279 assume as: "x \<le> 1 / 2" "y > 1 / 2" |
343 assume as: "x \<le> 1 / 2" "y > 1 / 2" |
280 then have "?g x \<in> path_image g1" "?g y \<in> path_image g2" |
344 then have "?g x \<in> path_image g1" and "?g y \<in> path_image g2" |
281 unfolding path_image_def joinpaths_def |
345 unfolding path_image_def joinpaths_def |
282 using xy(1,2) by auto |
346 using xy(1,2) |
283 then have "?g x = pathfinish g1" "?g y = pathstart g2" |
347 by auto |
284 using assms(4) unfolding assms(3) xy(3) by auto |
348 then have "?g x = pathfinish g1" and "?g y = pathstart g2" |
|
349 using assms(4) |
|
350 unfolding assms(3) xy(3) |
|
351 by auto |
285 then show ?thesis |
352 then show ?thesis |
286 using as and inj(1)[of "2 *\<^sub>R x" 1] inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(1,2) |
353 using as and inj(1)[of "2 *\<^sub>R x" 1] inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(1,2) |
287 unfolding pathstart_def pathfinish_def joinpaths_def |
354 unfolding pathstart_def pathfinish_def joinpaths_def |
288 by auto |
355 by auto |
289 next |
356 next |
290 assume as:"x > 1 / 2" "y \<le> 1 / 2" |
357 assume as:"x > 1 / 2" "y \<le> 1 / 2" |
291 then have "?g x \<in> path_image g2" "?g y \<in> path_image g1" |
358 then have "?g x \<in> path_image g2" and "?g y \<in> path_image g1" |
292 unfolding path_image_def joinpaths_def |
359 unfolding path_image_def joinpaths_def |
293 using xy(1,2) by auto |
360 using xy(1,2) |
294 then have "?g x = pathstart g2" "?g y = pathfinish g1" |
361 by auto |
295 using assms(4) unfolding assms(3) xy(3) by auto |
362 then have "?g x = pathstart g2" and "?g y = pathfinish g1" |
|
363 using assms(4) |
|
364 unfolding assms(3) xy(3) |
|
365 by auto |
296 then show ?thesis using as and inj(2)[of "2 *\<^sub>R x - 1" 0] inj(1)[of "2 *\<^sub>R y" 1] and xy(1,2) |
366 then show ?thesis using as and inj(2)[of "2 *\<^sub>R x - 1" 0] inj(1)[of "2 *\<^sub>R y" 1] and xy(1,2) |
297 unfolding pathstart_def pathfinish_def joinpaths_def |
367 unfolding pathstart_def pathfinish_def joinpaths_def |
298 by auto |
368 by auto |
299 qed |
369 qed |
300 qed |
370 qed |
301 |
371 |
302 lemmas join_paths_simps = path_join path_image_join pathstart_join pathfinish_join |
372 lemmas join_paths_simps = path_join path_image_join pathstart_join pathfinish_join |
303 |
373 |
304 |
374 |
305 subsection {* Reparametrizing a closed curve to start at some chosen point. *} |
375 subsection {* Reparametrizing a closed curve to start at some chosen point *} |
306 |
376 |
307 definition "shiftpath a (f::real \<Rightarrow> 'a::topological_space) = |
377 definition shiftpath :: "real \<Rightarrow> (real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a" |
308 (\<lambda>x. if (a + x) \<le> 1 then f(a + x) else f(a + x - 1))" |
378 where "shiftpath a f = (\<lambda>x. if (a + x) \<le> 1 then f (a + x) else f (a + x - 1))" |
309 |
379 |
310 lemma pathstart_shiftpath: "a \<le> 1 \<Longrightarrow> pathstart(shiftpath a g) = g a" |
380 lemma pathstart_shiftpath: "a \<le> 1 \<Longrightarrow> pathstart (shiftpath a g) = g a" |
311 unfolding pathstart_def shiftpath_def by auto |
381 unfolding pathstart_def shiftpath_def by auto |
312 |
382 |
313 lemma pathfinish_shiftpath: |
383 lemma pathfinish_shiftpath: |
314 assumes "0 \<le> a" "pathfinish g = pathstart g" |
384 assumes "0 \<le> a" |
315 shows "pathfinish(shiftpath a g) = g a" |
385 and "pathfinish g = pathstart g" |
316 using assms unfolding pathstart_def pathfinish_def shiftpath_def |
386 shows "pathfinish (shiftpath a g) = g a" |
|
387 using assms |
|
388 unfolding pathstart_def pathfinish_def shiftpath_def |
317 by auto |
389 by auto |
318 |
390 |
319 lemma endpoints_shiftpath: |
391 lemma endpoints_shiftpath: |
320 assumes "pathfinish g = pathstart g" "a \<in> {0 .. 1}" |
392 assumes "pathfinish g = pathstart g" |
321 shows "pathfinish(shiftpath a g) = g a" "pathstart(shiftpath a g) = g a" |
393 and "a \<in> {0 .. 1}" |
322 using assms by(auto intro!:pathfinish_shiftpath pathstart_shiftpath) |
394 shows "pathfinish (shiftpath a g) = g a" |
|
395 and "pathstart (shiftpath a g) = g a" |
|
396 using assms |
|
397 by (auto intro!: pathfinish_shiftpath pathstart_shiftpath) |
323 |
398 |
324 lemma closed_shiftpath: |
399 lemma closed_shiftpath: |
325 assumes "pathfinish g = pathstart g" "a \<in> {0..1}" |
400 assumes "pathfinish g = pathstart g" |
326 shows "pathfinish(shiftpath a g) = pathstart(shiftpath a g)" |
401 and "a \<in> {0..1}" |
327 using endpoints_shiftpath[OF assms] by auto |
402 shows "pathfinish (shiftpath a g) = pathstart (shiftpath a g)" |
|
403 using endpoints_shiftpath[OF assms] |
|
404 by auto |
328 |
405 |
329 lemma path_shiftpath: |
406 lemma path_shiftpath: |
330 assumes "path g" "pathfinish g = pathstart g" "a \<in> {0..1}" |
407 assumes "path g" |
331 shows "path(shiftpath a g)" |
408 and "pathfinish g = pathstart g" |
|
409 and "a \<in> {0..1}" |
|
410 shows "path (shiftpath a g)" |
332 proof - |
411 proof - |
333 have *: "{0 .. 1} = {0 .. 1-a} \<union> {1-a .. 1}" using assms(3) by auto |
412 have *: "{0 .. 1} = {0 .. 1-a} \<union> {1-a .. 1}" |
|
413 using assms(3) by auto |
334 have **: "\<And>x. x + a = 1 \<Longrightarrow> g (x + a - 1) = g (x + a)" |
414 have **: "\<And>x. x + a = 1 \<Longrightarrow> g (x + a - 1) = g (x + a)" |
335 using assms(2)[unfolded pathfinish_def pathstart_def] by auto |
415 using assms(2)[unfolded pathfinish_def pathstart_def] |
|
416 by auto |
336 show ?thesis |
417 show ?thesis |
337 unfolding path_def shiftpath_def * |
418 unfolding path_def shiftpath_def * |
338 apply (rule continuous_on_union) |
419 apply (rule continuous_on_union) |
339 apply (rule closed_real_atLeastAtMost)+ |
420 apply (rule closed_real_atLeastAtMost)+ |
340 apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a + x)"]) prefer 3 |
421 apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a + x)"]) |
341 apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a - 1 + x)"]) defer prefer 3 |
422 prefer 3 |
342 apply (rule continuous_on_intros)+ prefer 2 |
423 apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a - 1 + x)"]) |
|
424 defer |
|
425 prefer 3 |
|
426 apply (rule continuous_on_intros)+ |
|
427 prefer 2 |
343 apply (rule continuous_on_intros)+ |
428 apply (rule continuous_on_intros)+ |
344 apply (rule_tac[1-2] continuous_on_subset[OF assms(1)[unfolded path_def]]) |
429 apply (rule_tac[1-2] continuous_on_subset[OF assms(1)[unfolded path_def]]) |
345 using assms(3) and ** |
430 using assms(3) and ** |
346 apply (auto, auto simp add: field_simps) |
431 apply auto |
|
432 apply (auto simp add: field_simps) |
347 done |
433 done |
348 qed |
434 qed |
349 |
435 |
350 lemma shiftpath_shiftpath: |
436 lemma shiftpath_shiftpath: |
351 assumes "pathfinish g = pathstart g" "a \<in> {0..1}" "x \<in> {0..1}" |
437 assumes "pathfinish g = pathstart g" |
|
438 and "a \<in> {0..1}" |
|
439 and "x \<in> {0..1}" |
352 shows "shiftpath (1 - a) (shiftpath a g) x = g x" |
440 shows "shiftpath (1 - a) (shiftpath a g) x = g x" |
353 using assms unfolding pathfinish_def pathstart_def shiftpath_def by auto |
441 using assms |
|
442 unfolding pathfinish_def pathstart_def shiftpath_def |
|
443 by auto |
354 |
444 |
355 lemma path_image_shiftpath: |
445 lemma path_image_shiftpath: |
356 assumes "a \<in> {0..1}" "pathfinish g = pathstart g" |
446 assumes "a \<in> {0..1}" |
357 shows "path_image(shiftpath a g) = path_image g" |
447 and "pathfinish g = pathstart g" |
|
448 shows "path_image (shiftpath a g) = path_image g" |
358 proof - |
449 proof - |
359 { fix x |
450 { fix x |
360 assume as:"g 1 = g 0" "x \<in> {0..1::real}" " \<forall>y\<in>{0..1} \<inter> {x. \<not> a + x \<le> 1}. g x \<noteq> g (a + y - 1)" |
451 assume as: "g 1 = g 0" "x \<in> {0..1::real}" " \<forall>y\<in>{0..1} \<inter> {x. \<not> a + x \<le> 1}. g x \<noteq> g (a + y - 1)" |
361 then have "\<exists>y\<in>{0..1} \<inter> {x. a + x \<le> 1}. g x = g (a + y)" |
452 then have "\<exists>y\<in>{0..1} \<inter> {x. a + x \<le> 1}. g x = g (a + y)" |
362 proof (cases "a \<le> x") |
453 proof (cases "a \<le> x") |
363 case False |
454 case False |
364 then show ?thesis |
455 then show ?thesis |
365 apply (rule_tac x="1 + x - a" in bexI) |
456 apply (rule_tac x="1 + x - a" in bexI) |
366 using as(1,2) and as(3)[THEN bspec[where x="1 + x - a"]] and assms(1) |
457 using as(1,2) and as(3)[THEN bspec[where x="1 + x - a"]] and assms(1) |
367 apply (auto simp add: field_simps atomize_not) |
458 apply (auto simp add: field_simps atomize_not) |
368 done |
459 done |
369 next |
460 next |
370 case True |
461 case True |
371 then show ?thesis using as(1-2) and assms(1) apply(rule_tac x="x - a" in bexI) |
462 then show ?thesis |
372 by(auto simp add: field_simps) |
463 using as(1-2) and assms(1) |
|
464 apply (rule_tac x="x - a" in bexI) |
|
465 apply (auto simp add: field_simps) |
|
466 done |
373 qed |
467 qed |
374 } |
468 } |
375 then show ?thesis |
469 then show ?thesis |
376 using assms unfolding shiftpath_def path_image_def pathfinish_def pathstart_def |
470 using assms |
377 by(auto simp add: image_iff) |
471 unfolding shiftpath_def path_image_def pathfinish_def pathstart_def |
378 qed |
472 by (auto simp add: image_iff) |
379 |
473 qed |
380 |
474 |
381 subsection {* Special case of straight-line paths. *} |
475 |
|
476 subsection {* Special case of straight-line paths *} |
382 |
477 |
383 definition linepath :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> real \<Rightarrow> 'a" |
478 definition linepath :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> real \<Rightarrow> 'a" |
384 where "linepath a b = (\<lambda>x. (1 - x) *\<^sub>R a + x *\<^sub>R b)" |
479 where "linepath a b = (\<lambda>x. (1 - x) *\<^sub>R a + x *\<^sub>R b)" |
385 |
480 |
386 lemma pathstart_linepath[simp]: "pathstart(linepath a b) = a" |
481 lemma pathstart_linepath[simp]: "pathstart (linepath a b) = a" |
387 unfolding pathstart_def linepath_def by auto |
482 unfolding pathstart_def linepath_def |
388 |
483 by auto |
389 lemma pathfinish_linepath[simp]: "pathfinish(linepath a b) = b" |
484 |
390 unfolding pathfinish_def linepath_def by auto |
485 lemma pathfinish_linepath[simp]: "pathfinish (linepath a b) = b" |
|
486 unfolding pathfinish_def linepath_def |
|
487 by auto |
391 |
488 |
392 lemma continuous_linepath_at[intro]: "continuous (at x) (linepath a b)" |
489 lemma continuous_linepath_at[intro]: "continuous (at x) (linepath a b)" |
393 unfolding linepath_def by (intro continuous_intros) |
490 unfolding linepath_def |
|
491 by (intro continuous_intros) |
394 |
492 |
395 lemma continuous_on_linepath[intro]: "continuous_on s (linepath a b)" |
493 lemma continuous_on_linepath[intro]: "continuous_on s (linepath a b)" |
396 using continuous_linepath_at by(auto intro!: continuous_at_imp_continuous_on) |
494 using continuous_linepath_at |
397 |
495 by (auto intro!: continuous_at_imp_continuous_on) |
398 lemma path_linepath[intro]: "path(linepath a b)" |
496 |
399 unfolding path_def by(rule continuous_on_linepath) |
497 lemma path_linepath[intro]: "path (linepath a b)" |
400 |
498 unfolding path_def |
401 lemma path_image_linepath[simp]: "path_image(linepath a b) = (closed_segment a b)" |
499 by (rule continuous_on_linepath) |
|
500 |
|
501 lemma path_image_linepath[simp]: "path_image (linepath a b) = closed_segment a b" |
402 unfolding path_image_def segment linepath_def |
502 unfolding path_image_def segment linepath_def |
403 apply (rule set_eqI, rule) defer |
503 apply (rule set_eqI) |
|
504 apply rule |
|
505 defer |
404 unfolding mem_Collect_eq image_iff |
506 unfolding mem_Collect_eq image_iff |
405 apply(erule exE) |
507 apply (erule exE) |
406 apply(rule_tac x="u *\<^sub>R 1" in bexI) |
508 apply (rule_tac x="u *\<^sub>R 1" in bexI) |
407 apply auto |
509 apply auto |
408 done |
510 done |
409 |
511 |
410 lemma reversepath_linepath[simp]: "reversepath(linepath a b) = linepath b a" |
512 lemma reversepath_linepath[simp]: "reversepath (linepath a b) = linepath b a" |
411 unfolding reversepath_def linepath_def |
513 unfolding reversepath_def linepath_def |
412 by auto |
514 by auto |
413 |
515 |
414 lemma injective_path_linepath: |
516 lemma injective_path_linepath: |
415 assumes "a \<noteq> b" |
517 assumes "a \<noteq> b" |
416 shows "injective_path (linepath a b)" |
518 shows "injective_path (linepath a b)" |
417 proof - |
519 proof - |
418 { fix x y :: "real" |
520 { |
|
521 fix x y :: "real" |
419 assume "x *\<^sub>R b + y *\<^sub>R a = x *\<^sub>R a + y *\<^sub>R b" |
522 assume "x *\<^sub>R b + y *\<^sub>R a = x *\<^sub>R a + y *\<^sub>R b" |
420 then have "(x - y) *\<^sub>R a = (x - y) *\<^sub>R b" by (simp add: algebra_simps) |
523 then have "(x - y) *\<^sub>R a = (x - y) *\<^sub>R b" |
421 with assms have "x = y" by simp } |
524 by (simp add: algebra_simps) |
|
525 with assms have "x = y" |
|
526 by simp |
|
527 } |
422 then show ?thesis |
528 then show ?thesis |
423 unfolding injective_path_def linepath_def |
529 unfolding injective_path_def linepath_def |
424 by (auto simp add: algebra_simps) |
530 by (auto simp add: algebra_simps) |
425 qed |
531 qed |
426 |
532 |
427 lemma simple_path_linepath[intro]: "a \<noteq> b \<Longrightarrow> simple_path(linepath a b)" |
533 lemma simple_path_linepath[intro]: "a \<noteq> b \<Longrightarrow> simple_path (linepath a b)" |
428 by(auto intro!: injective_imp_simple_path injective_path_linepath) |
534 by (auto intro!: injective_imp_simple_path injective_path_linepath) |
429 |
535 |
430 |
536 |
431 subsection {* Bounding a point away from a path. *} |
537 subsection {* Bounding a point away from a path *} |
432 |
538 |
433 lemma not_on_path_ball: |
539 lemma not_on_path_ball: |
434 fixes g :: "real \<Rightarrow> 'a::heine_borel" |
540 fixes g :: "real \<Rightarrow> 'a::heine_borel" |
435 assumes "path g" "z \<notin> path_image g" |
541 assumes "path g" |
436 shows "\<exists>e > 0. ball z e \<inter> (path_image g) = {}" |
542 and "z \<notin> path_image g" |
|
543 shows "\<exists>e > 0. ball z e \<inter> path_image g = {}" |
437 proof - |
544 proof - |
438 obtain a where "a \<in> path_image g" "\<forall>y \<in> path_image g. dist z a \<le> dist z y" |
545 obtain a where "a \<in> path_image g" "\<forall>y \<in> path_image g. dist z a \<le> dist z y" |
439 using distance_attains_inf[OF _ path_image_nonempty, of g z] |
546 using distance_attains_inf[OF _ path_image_nonempty, of g z] |
440 using compact_path_image[THEN compact_imp_closed, OF assms(1)] by auto |
547 using compact_path_image[THEN compact_imp_closed, OF assms(1)] by auto |
441 then show ?thesis |
548 then show ?thesis |
512 unfolding path_component_def |
628 unfolding path_component_def |
513 apply auto |
629 apply auto |
514 done |
630 done |
515 |
631 |
516 lemma path_component_subset: "{y. path_component s x y} \<subseteq> s" |
632 lemma path_component_subset: "{y. path_component s x y} \<subseteq> s" |
517 apply (rule, rule path_component_mem(2)) |
633 apply rule |
|
634 apply (rule path_component_mem(2)) |
518 apply auto |
635 apply auto |
519 done |
636 done |
520 |
637 |
521 lemma path_component_eq_empty: "{y. path_component s x y} = {} \<longleftrightarrow> x \<notin> s" |
638 lemma path_component_eq_empty: "{y. path_component s x y} = {} \<longleftrightarrow> x \<notin> s" |
522 apply rule |
639 apply rule |
523 apply (drule equals0D[of _ x]) defer |
640 apply (drule equals0D[of _ x]) |
|
641 defer |
524 apply (rule equals0I) |
642 apply (rule equals0I) |
525 unfolding mem_Collect_eq |
643 unfolding mem_Collect_eq |
526 apply (drule path_component_mem(1)) |
644 apply (drule path_component_mem(1)) |
527 using path_component_refl |
645 using path_component_refl |
528 apply auto |
646 apply auto |
529 done |
647 done |
530 |
648 |
531 |
649 |
532 subsection {* Path connectedness of a space. *} |
650 subsection {* Path connectedness of a space *} |
533 |
651 |
534 definition "path_connected s \<longleftrightarrow> |
652 definition "path_connected s \<longleftrightarrow> |
535 (\<forall>x\<in>s. \<forall>y\<in>s. \<exists>g. path g \<and> (path_image g) \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)" |
653 (\<forall>x\<in>s. \<forall>y\<in>s. \<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)" |
536 |
654 |
537 lemma path_connected_component: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. path_component s x y)" |
655 lemma path_connected_component: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. path_component s x y)" |
538 unfolding path_connected_def path_component_def by auto |
656 unfolding path_connected_def path_component_def by auto |
539 |
657 |
540 lemma path_connected_component_set: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. {y. path_component s x y} = s)" |
658 lemma path_connected_component_set: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. {y. path_component s x y} = s)" |
541 unfolding path_connected_component |
659 unfolding path_connected_component |
542 apply (rule, rule, rule, rule path_component_subset) |
660 apply rule |
|
661 apply rule |
|
662 apply rule |
|
663 apply (rule path_component_subset) |
543 unfolding subset_eq mem_Collect_eq Ball_def |
664 unfolding subset_eq mem_Collect_eq Ball_def |
544 apply auto |
665 apply auto |
545 done |
666 done |
546 |
667 |
547 |
668 |
548 subsection {* Some useful lemmas about path-connectedness. *} |
669 subsection {* Some useful lemmas about path-connectedness *} |
549 |
670 |
550 lemma convex_imp_path_connected: |
671 lemma convex_imp_path_connected: |
551 fixes s :: "'a::real_normed_vector set" |
672 fixes s :: "'a::real_normed_vector set" |
552 assumes "convex s" shows "path_connected s" |
673 assumes "convex s" |
|
674 shows "path_connected s" |
553 unfolding path_connected_def |
675 unfolding path_connected_def |
554 apply (rule, rule, rule_tac x = "linepath x y" in exI) |
676 apply rule |
|
677 apply rule |
|
678 apply (rule_tac x = "linepath x y" in exI) |
555 unfolding path_image_linepath |
679 unfolding path_image_linepath |
556 using assms [unfolded convex_contains_segment] |
680 using assms [unfolded convex_contains_segment] |
557 apply auto |
681 apply auto |
558 done |
682 done |
559 |
683 |
560 lemma path_connected_imp_connected: |
684 lemma path_connected_imp_connected: |
561 assumes "path_connected s" |
685 assumes "path_connected s" |
562 shows "connected s" |
686 shows "connected s" |
563 unfolding connected_def not_ex |
687 unfolding connected_def not_ex |
564 apply (rule, rule, rule ccontr) |
688 apply rule |
|
689 apply rule |
|
690 apply (rule ccontr) |
565 unfolding not_not |
691 unfolding not_not |
566 apply (erule conjE)+ |
692 apply (elim conjE) |
567 proof - |
693 proof - |
568 fix e1 e2 |
694 fix e1 e2 |
569 assume as: "open e1" "open e2" "s \<subseteq> e1 \<union> e2" "e1 \<inter> e2 \<inter> s = {}" "e1 \<inter> s \<noteq> {}" "e2 \<inter> s \<noteq> {}" |
695 assume as: "open e1" "open e2" "s \<subseteq> e1 \<union> e2" "e1 \<inter> e2 \<inter> s = {}" "e1 \<inter> s \<noteq> {}" "e2 \<inter> s \<noteq> {}" |
570 then obtain x1 x2 where obt:"x1\<in>e1\<inter>s" "x2\<in>e2\<inter>s" by auto |
696 then obtain x1 x2 where obt:"x1 \<in> e1 \<inter> s" "x2 \<in> e2 \<inter> s" |
571 then obtain g where g:"path g" "path_image g \<subseteq> s" "pathstart g = x1" "pathfinish g = x2" |
697 by auto |
|
698 then obtain g where g: "path g" "path_image g \<subseteq> s" "pathstart g = x1" "pathfinish g = x2" |
572 using assms[unfolded path_connected_def,rule_format,of x1 x2] by auto |
699 using assms[unfolded path_connected_def,rule_format,of x1 x2] by auto |
573 have *: "connected {0..1::real}" |
700 have *: "connected {0..1::real}" |
574 by (auto intro!: convex_connected convex_real_interval) |
701 by (auto intro!: convex_connected convex_real_interval) |
575 have "{0..1} \<subseteq> {x \<in> {0..1}. g x \<in> e1} \<union> {x \<in> {0..1}. g x \<in> e2}" |
702 have "{0..1} \<subseteq> {x \<in> {0..1}. g x \<in> e1} \<union> {x \<in> {0..1}. g x \<in> e2}" |
576 using as(3) g(2)[unfolded path_defs] by blast |
703 using as(3) g(2)[unfolded path_defs] by blast |
577 moreover have "{x \<in> {0..1}. g x \<in> e1} \<inter> {x \<in> {0..1}. g x \<in> e2} = {}" |
704 moreover have "{x \<in> {0..1}. g x \<in> e1} \<inter> {x \<in> {0..1}. g x \<in> e2} = {}" |
578 using as(4) g(2)[unfolded path_defs] unfolding subset_eq by auto |
705 using as(4) g(2)[unfolded path_defs] |
|
706 unfolding subset_eq |
|
707 by auto |
579 moreover have "{x \<in> {0..1}. g x \<in> e1} \<noteq> {} \<and> {x \<in> {0..1}. g x \<in> e2} \<noteq> {}" |
708 moreover have "{x \<in> {0..1}. g x \<in> e1} \<noteq> {} \<and> {x \<in> {0..1}. g x \<in> e2} \<noteq> {}" |
580 using g(3,4)[unfolded path_defs] using obt |
709 using g(3,4)[unfolded path_defs] |
|
710 using obt |
581 by (simp add: ex_in_conv [symmetric], metis zero_le_one order_refl) |
711 by (simp add: ex_in_conv [symmetric], metis zero_le_one order_refl) |
582 ultimately show False |
712 ultimately show False |
583 using *[unfolded connected_local not_ex, rule_format, of "{x\<in>{0..1}. g x \<in> e1}" "{x\<in>{0..1}. g x \<in> e2}"] |
713 using *[unfolded connected_local not_ex, rule_format, |
|
714 of "{x\<in>{0..1}. g x \<in> e1}" "{x\<in>{0..1}. g x \<in> e2}"] |
584 using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(1)] |
715 using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(1)] |
585 using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(2)] |
716 using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(2)] |
586 by auto |
717 by auto |
587 qed |
718 qed |
588 |
719 |
641 apply (rule path_component_trans, assumption) |
780 apply (rule path_component_trans, assumption) |
642 apply (rule path_component_of_subset[OF e(2)]) |
781 apply (rule path_component_of_subset[OF e(2)]) |
643 apply (rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format]) |
782 apply (rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format]) |
644 apply auto |
783 apply auto |
645 done |
784 done |
646 then show False using as by auto |
785 then show False |
|
786 using as by auto |
647 qed (insert e(2), auto) |
787 qed (insert e(2), auto) |
648 qed |
788 qed |
649 |
789 |
650 lemma connected_open_path_connected: |
790 lemma connected_open_path_connected: |
651 fixes s :: "'a::real_normed_vector set" |
791 fixes s :: "'a::real_normed_vector set" |
652 assumes "open s" "connected s" |
792 assumes "open s" |
|
793 and "connected s" |
653 shows "path_connected s" |
794 shows "path_connected s" |
654 unfolding path_connected_component_set |
795 unfolding path_connected_component_set |
655 proof (rule, rule, rule path_component_subset, rule) |
796 proof (rule, rule, rule path_component_subset, rule) |
656 fix x y |
797 fix x y |
657 assume "x \<in> s" "y \<in> s" |
798 assume "x \<in> s" and "y \<in> s" |
658 show "y \<in> {y. path_component s x y}" |
799 show "y \<in> {y. path_component s x y}" |
659 proof (rule ccontr) |
800 proof (rule ccontr) |
660 assume "y \<notin> {y. path_component s x y}" |
801 assume "\<not> ?thesis" |
661 moreover |
802 moreover have "{y. path_component s x y} \<inter> s \<noteq> {}" |
662 have "{y. path_component s x y} \<inter> s \<noteq> {}" |
803 using `x \<in> s` path_component_eq_empty path_component_subset[of s x] |
663 using `x\<in>s` path_component_eq_empty path_component_subset[of s x] by auto |
804 by auto |
664 ultimately |
805 ultimately |
665 show False |
806 show False |
666 using `y\<in>s` open_non_path_component[OF assms(1)] open_path_component[OF assms(1)] |
807 using `y \<in> s` open_non_path_component[OF assms(1)] open_path_component[OF assms(1)] |
667 using assms(2)[unfolded connected_def not_ex, rule_format, of"{y. path_component s x y}" "s - {y. path_component s x y}"] |
808 using assms(2)[unfolded connected_def not_ex, rule_format, |
|
809 of"{y. path_component s x y}" "s - {y. path_component s x y}"] |
668 by auto |
810 by auto |
669 qed |
811 qed |
670 qed |
812 qed |
671 |
813 |
672 lemma path_connected_continuous_image: |
814 lemma path_connected_continuous_image: |
673 assumes "continuous_on s f" "path_connected s" |
815 assumes "continuous_on s f" |
|
816 and "path_connected s" |
674 shows "path_connected (f ` s)" |
817 shows "path_connected (f ` s)" |
675 unfolding path_connected_def |
818 unfolding path_connected_def |
676 proof (rule, rule) |
819 proof (rule, rule) |
677 fix x' y' |
820 fix x' y' |
678 assume "x' \<in> f ` s" "y' \<in> f ` s" |
821 assume "x' \<in> f ` s" "y' \<in> f ` s" |
679 then obtain x y where xy: "x\<in>s" "y\<in>s" "x' = f x" "y' = f y" by auto |
822 then obtain x y where x: "x \<in> s" and y: "y \<in> s" and x': "x' = f x" and y': "y' = f y" |
680 guess g using assms(2)[unfolded path_connected_def, rule_format, OF xy(1,2)] .. |
823 by auto |
|
824 from x y obtain g where "path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y" |
|
825 using assms(2)[unfolded path_connected_def] by fast |
681 then show "\<exists>g. path g \<and> path_image g \<subseteq> f ` s \<and> pathstart g = x' \<and> pathfinish g = y'" |
826 then show "\<exists>g. path g \<and> path_image g \<subseteq> f ` s \<and> pathstart g = x' \<and> pathfinish g = y'" |
682 unfolding xy |
827 unfolding x' y' |
683 apply (rule_tac x="f \<circ> g" in exI) |
828 apply (rule_tac x="f \<circ> g" in exI) |
684 unfolding path_defs |
829 unfolding path_defs |
685 apply (intro conjI continuous_on_compose continuous_on_subset[OF assms(1)]) |
830 apply (intro conjI continuous_on_compose continuous_on_subset[OF assms(1)]) |
686 apply auto |
831 apply auto |
687 done |
832 done |
688 qed |
833 qed |
689 |
834 |
690 lemma homeomorphic_path_connectedness: |
835 lemma homeomorphic_path_connectedness: |
691 "s homeomorphic t \<Longrightarrow> (path_connected s \<longleftrightarrow> path_connected t)" |
836 "s homeomorphic t \<Longrightarrow> path_connected s \<longleftrightarrow> path_connected t" |
692 unfolding homeomorphic_def homeomorphism_def |
837 unfolding homeomorphic_def homeomorphism_def |
693 apply (erule exE|erule conjE)+ |
838 apply (erule exE|erule conjE)+ |
694 apply rule |
839 apply rule |
695 apply (drule_tac f=f in path_connected_continuous_image) prefer 3 |
840 apply (drule_tac f=f in path_connected_continuous_image) |
|
841 prefer 3 |
696 apply (drule_tac f=g in path_connected_continuous_image) |
842 apply (drule_tac f=g in path_connected_continuous_image) |
697 apply auto |
843 apply auto |
698 done |
844 done |
699 |
845 |
700 lemma path_connected_empty: "path_connected {}" |
846 lemma path_connected_empty: "path_connected {}" |
701 unfolding path_connected_def by auto |
847 unfolding path_connected_def by auto |
702 |
848 |
703 lemma path_connected_singleton: "path_connected {a}" |
849 lemma path_connected_singleton: "path_connected {a}" |
704 unfolding path_connected_def pathstart_def pathfinish_def path_image_def |
850 unfolding path_connected_def pathstart_def pathfinish_def path_image_def |
705 apply (clarify, rule_tac x="\<lambda>x. a" in exI, simp add: image_constant_conv) |
851 apply clarify |
|
852 apply (rule_tac x="\<lambda>x. a" in exI) |
|
853 apply (simp add: image_constant_conv) |
706 apply (simp add: path_def continuous_on_const) |
854 apply (simp add: path_def continuous_on_const) |
707 done |
855 done |
708 |
856 |
709 lemma path_connected_Un: |
857 lemma path_connected_Un: |
710 assumes "path_connected s" "path_connected t" "s \<inter> t \<noteq> {}" |
858 assumes "path_connected s" |
|
859 and "path_connected t" |
|
860 and "s \<inter> t \<noteq> {}" |
711 shows "path_connected (s \<union> t)" |
861 shows "path_connected (s \<union> t)" |
712 unfolding path_connected_component |
862 unfolding path_connected_component |
713 proof (rule, rule) |
863 proof (rule, rule) |
714 fix x y |
864 fix x y |
715 assume as: "x \<in> s \<union> t" "y \<in> s \<union> t" |
865 assume as: "x \<in> s \<union> t" "y \<in> s \<union> t" |
716 from assms(3) obtain z where "z \<in> s \<inter> t" by auto |
866 from assms(3) obtain z where "z \<in> s \<inter> t" |
|
867 by auto |
717 then show "path_component (s \<union> t) x y" |
868 then show "path_component (s \<union> t) x y" |
718 using as and assms(1-2)[unfolded path_connected_component] |
869 using as and assms(1-2)[unfolded path_connected_component] |
719 apply - |
870 apply - |
720 apply (erule_tac[!] UnE)+ |
871 apply (erule_tac[!] UnE)+ |
721 apply (rule_tac[2-3] path_component_trans[of _ _ z]) |
872 apply (rule_tac[2-3] path_component_trans[of _ _ z]) |
722 apply (auto simp add:path_component_of_subset [OF Un_upper1] path_component_of_subset[OF Un_upper2]) |
873 apply (auto simp add:path_component_of_subset [OF Un_upper1] path_component_of_subset[OF Un_upper2]) |
723 done |
874 done |
724 qed |
875 qed |
738 then show "path_component (\<Union>i\<in>A. S i) x y" |
889 then show "path_component (\<Union>i\<in>A. S i) x y" |
739 by (rule path_component_trans) |
890 by (rule path_component_trans) |
740 qed |
891 qed |
741 |
892 |
742 |
893 |
743 subsection {* sphere is path-connected. *} |
894 subsection {* Sphere is path-connected *} |
744 |
895 |
745 lemma path_connected_punctured_universe: |
896 lemma path_connected_punctured_universe: |
746 assumes "2 \<le> DIM('a::euclidean_space)" |
897 assumes "2 \<le> DIM('a::euclidean_space)" |
747 shows "path_connected((UNIV::'a::euclidean_space set) - {a})" |
898 shows "path_connected ((UNIV::'a set) - {a})" |
748 proof - |
899 proof - |
749 let ?A = "{x::'a. \<exists>i\<in>Basis. x \<bullet> i < a \<bullet> i}" |
900 let ?A = "{x::'a. \<exists>i\<in>Basis. x \<bullet> i < a \<bullet> i}" |
750 let ?B = "{x::'a. \<exists>i\<in>Basis. a \<bullet> i < x \<bullet> i}" |
901 let ?B = "{x::'a. \<exists>i\<in>Basis. a \<bullet> i < x \<bullet> i}" |
751 |
902 |
752 have A: "path_connected ?A" |
903 have A: "path_connected ?A" |
753 unfolding Collect_bex_eq |
904 unfolding Collect_bex_eq |
754 proof (rule path_connected_UNION) |
905 proof (rule path_connected_UNION) |
755 fix i :: 'a |
906 fix i :: 'a |
756 assume "i \<in> Basis" |
907 assume "i \<in> Basis" |
757 then show "(\<Sum>i\<in>Basis. (a \<bullet> i - 1)*\<^sub>R i) \<in> {x::'a. x \<bullet> i < a \<bullet> i}" by simp |
908 then show "(\<Sum>i\<in>Basis. (a \<bullet> i - 1)*\<^sub>R i) \<in> {x::'a. x \<bullet> i < a \<bullet> i}" |
|
909 by simp |
758 show "path_connected {x. x \<bullet> i < a \<bullet> i}" |
910 show "path_connected {x. x \<bullet> i < a \<bullet> i}" |
759 using convex_imp_path_connected [OF convex_halfspace_lt, of i "a \<bullet> i"] |
911 using convex_imp_path_connected [OF convex_halfspace_lt, of i "a \<bullet> i"] |
760 by (simp add: inner_commute) |
912 by (simp add: inner_commute) |
761 qed |
913 qed |
762 have B: "path_connected ?B" unfolding Collect_bex_eq |
914 have B: "path_connected ?B" |
|
915 unfolding Collect_bex_eq |
763 proof (rule path_connected_UNION) |
916 proof (rule path_connected_UNION) |
764 fix i :: 'a |
917 fix i :: 'a |
765 assume "i \<in> Basis" |
918 assume "i \<in> Basis" |
766 then show "(\<Sum>i\<in>Basis. (a \<bullet> i + 1) *\<^sub>R i) \<in> {x::'a. a \<bullet> i < x \<bullet> i}" by simp |
919 then show "(\<Sum>i\<in>Basis. (a \<bullet> i + 1) *\<^sub>R i) \<in> {x::'a. a \<bullet> i < x \<bullet> i}" |
|
920 by simp |
767 show "path_connected {x. a \<bullet> i < x \<bullet> i}" |
921 show "path_connected {x. a \<bullet> i < x \<bullet> i}" |
768 using convex_imp_path_connected [OF convex_halfspace_gt, of "a \<bullet> i" i] |
922 using convex_imp_path_connected [OF convex_halfspace_gt, of "a \<bullet> i" i] |
769 by (simp add: inner_commute) |
923 by (simp add: inner_commute) |
770 qed |
924 qed |
771 obtain S :: "'a set" where "S \<subseteq> Basis" "card S = Suc (Suc 0)" |
925 obtain S :: "'a set" where "S \<subseteq> Basis" and "card S = Suc (Suc 0)" |
772 using ex_card[OF assms] by auto |
926 using ex_card[OF assms] |
773 then obtain b0 b1 :: 'a where "b0 \<in> Basis" "b1 \<in> Basis" "b0 \<noteq> b1" |
927 by auto |
|
928 then obtain b0 b1 :: 'a where "b0 \<in> Basis" and "b1 \<in> Basis" and "b0 \<noteq> b1" |
774 unfolding card_Suc_eq by auto |
929 unfolding card_Suc_eq by auto |
775 then have "a + b0 - b1 \<in> ?A \<inter> ?B" by (auto simp: inner_simps inner_Basis) |
930 then have "a + b0 - b1 \<in> ?A \<inter> ?B" |
776 then have "?A \<inter> ?B \<noteq> {}" by fast |
931 by (auto simp: inner_simps inner_Basis) |
|
932 then have "?A \<inter> ?B \<noteq> {}" |
|
933 by fast |
777 with A B have "path_connected (?A \<union> ?B)" |
934 with A B have "path_connected (?A \<union> ?B)" |
778 by (rule path_connected_Un) |
935 by (rule path_connected_Un) |
779 also have "?A \<union> ?B = {x. \<exists>i\<in>Basis. x \<bullet> i \<noteq> a \<bullet> i}" |
936 also have "?A \<union> ?B = {x. \<exists>i\<in>Basis. x \<bullet> i \<noteq> a \<bullet> i}" |
780 unfolding neq_iff bex_disj_distrib Collect_disj_eq .. |
937 unfolding neq_iff bex_disj_distrib Collect_disj_eq .. |
781 also have "\<dots> = {x. x \<noteq> a}" |
938 also have "\<dots> = {x. x \<noteq> a}" |
782 unfolding euclidean_eq_iff [where 'a='a] by (simp add: Bex_def) |
939 unfolding euclidean_eq_iff [where 'a='a] |
783 also have "\<dots> = UNIV - {a}" by auto |
940 by (simp add: Bex_def) |
|
941 also have "\<dots> = UNIV - {a}" |
|
942 by auto |
784 finally show ?thesis . |
943 finally show ?thesis . |
785 qed |
944 qed |
786 |
945 |
787 lemma path_connected_sphere: |
946 lemma path_connected_sphere: |
788 assumes "2 \<le> DIM('a::euclidean_space)" |
947 assumes "2 \<le> DIM('a::euclidean_space)" |
789 shows "path_connected {x::'a::euclidean_space. norm(x - a) = r}" |
948 shows "path_connected {x::'a. norm (x - a) = r}" |
790 proof (rule linorder_cases [of r 0]) |
949 proof (rule linorder_cases [of r 0]) |
791 assume "r < 0" |
950 assume "r < 0" |
792 then have "{x::'a. norm(x - a) = r} = {}" by auto |
951 then have "{x::'a. norm(x - a) = r} = {}" |
793 then show ?thesis using path_connected_empty by simp |
952 by auto |
|
953 then show ?thesis |
|
954 using path_connected_empty by simp |
794 next |
955 next |
795 assume "r = 0" |
956 assume "r = 0" |
796 then show ?thesis using path_connected_singleton by simp |
957 then show ?thesis |
|
958 using path_connected_singleton by simp |
797 next |
959 next |
798 assume r: "0 < r" |
960 assume r: "0 < r" |
799 then have *: "{x::'a. norm(x - a) = r} = (\<lambda>x. a + r *\<^sub>R x) ` {x. norm x = 1}" |
961 have *: "{x::'a. norm(x - a) = r} = (\<lambda>x. a + r *\<^sub>R x) ` {x. norm x = 1}" |
800 apply - |
962 apply (rule set_eqI) |
801 apply (rule set_eqI, rule) |
963 apply rule |
802 unfolding image_iff |
964 unfolding image_iff |
803 apply (rule_tac x="(1/r) *\<^sub>R (x - a)" in bexI) |
965 apply (rule_tac x="(1/r) *\<^sub>R (x - a)" in bexI) |
804 unfolding mem_Collect_eq norm_scaleR |
966 unfolding mem_Collect_eq norm_scaleR |
|
967 using r |
805 apply (auto simp add: scaleR_right_diff_distrib) |
968 apply (auto simp add: scaleR_right_diff_distrib) |
806 done |
969 done |
807 have **: "{x::'a. norm x = 1} = (\<lambda>x. (1/norm x) *\<^sub>R x) ` (UNIV - {0})" |
970 have **: "{x::'a. norm x = 1} = (\<lambda>x. (1/norm x) *\<^sub>R x) ` (UNIV - {0})" |
808 apply (rule set_eqI,rule) |
971 apply (rule set_eqI) |
|
972 apply rule |
809 unfolding image_iff |
973 unfolding image_iff |
810 apply (rule_tac x=x in bexI) |
974 apply (rule_tac x=x in bexI) |
811 unfolding mem_Collect_eq |
975 unfolding mem_Collect_eq |
812 apply (auto split:split_if_asm) |
976 apply (auto split: split_if_asm) |
813 done |
977 done |
814 have "continuous_on (UNIV - {0}) (\<lambda>x::'a. 1 / norm x)" |
978 have "continuous_on (UNIV - {0}) (\<lambda>x::'a. 1 / norm x)" |
815 unfolding field_divide_inverse by (simp add: continuous_on_intros) |
979 unfolding field_divide_inverse |
816 then show ?thesis unfolding * ** using path_connected_punctured_universe[OF assms] |
980 by (simp add: continuous_on_intros) |
|
981 then show ?thesis |
|
982 unfolding * ** |
|
983 using path_connected_punctured_universe[OF assms] |
817 by (auto intro!: path_connected_continuous_image continuous_on_intros) |
984 by (auto intro!: path_connected_continuous_image continuous_on_intros) |
818 qed |
985 qed |
819 |
986 |
820 lemma connected_sphere: "2 \<le> DIM('a::euclidean_space) \<Longrightarrow> connected {x::'a. norm(x - a) = r}" |
987 lemma connected_sphere: "2 \<le> DIM('a::euclidean_space) \<Longrightarrow> connected {x::'a. norm (x - a) = r}" |
821 using path_connected_sphere path_connected_imp_connected by auto |
988 using path_connected_sphere path_connected_imp_connected |
|
989 by auto |
822 |
990 |
823 end |
991 end |