author  hoelzl 
Thu, 17 Jan 2013 11:57:17 +0100  
changeset 50935  cfdf19d3ca32 
parent 50884  2b21b4e2d7cb 
child 51478  270b21f3ae0a 
permissions  rwrr 
41959  1 
(* Title: HOL/Multivariate_Analysis/Path_Connected.thy 
36583  2 
Author: Robert Himmelmann, TU Muenchen 
3 
*) 

4 

5 
header {* Continuous paths and pathconnected sets *} 

6 

7 
theory Path_Connected 

37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

8 
imports Convex_Euclidean_Space 
36583  9 
begin 
10 

11 
subsection {* Paths. *} 

12 

49653  13 
definition path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool" 
36583  14 
where "path g \<longleftrightarrow> continuous_on {0 .. 1} g" 
15 

49653  16 
definition pathstart :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a" 
36583  17 
where "pathstart g = g 0" 
18 

49653  19 
definition pathfinish :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a" 
36583  20 
where "pathfinish g = g 1" 
21 

49653  22 
definition path_image :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a set" 
36583  23 
where "path_image g = g ` {0 .. 1}" 
24 

49653  25 
definition reversepath :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> (real \<Rightarrow> 'a)" 
36583  26 
where "reversepath g = (\<lambda>x. g(1  x))" 
27 

49653  28 
definition joinpaths :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a)" 
36583  29 
(infixr "+++" 75) 
30 
where "g1 +++ g2 = (\<lambda>x. if x \<le> 1/2 then g1 (2 * x) else g2 (2 * x  1))" 

31 

49653  32 
definition simple_path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool" 
36583  33 
where "simple_path g \<longleftrightarrow> 
49653  34 
(\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. g x = g y \<longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0)" 
36583  35 

49653  36 
definition injective_path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool" 
36583  37 
where "injective_path g \<longleftrightarrow> (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. g x = g y \<longrightarrow> x = y)" 
38 

49653  39 

36583  40 
subsection {* Some lemmas about these concepts. *} 
41 

49653  42 
lemma injective_imp_simple_path: "injective_path g \<Longrightarrow> simple_path g" 
36583  43 
unfolding injective_path_def simple_path_def by auto 
44 

45 
lemma path_image_nonempty: "path_image g \<noteq> {}" 

46 
unfolding path_image_def image_is_empty interval_eq_empty by auto 

47 

48 
lemma pathstart_in_path_image[intro]: "(pathstart g) \<in> path_image g" 

49 
unfolding pathstart_def path_image_def by auto 

50 

51 
lemma pathfinish_in_path_image[intro]: "(pathfinish g) \<in> path_image g" 

52 
unfolding pathfinish_def path_image_def by auto 

53 

54 
lemma connected_path_image[intro]: "path g \<Longrightarrow> connected(path_image g)" 

55 
unfolding path_def path_image_def 

56 
apply (erule connected_continuous_image) 

49653  57 
apply (rule convex_connected, rule convex_real_interval) 
58 
done 

36583  59 

50935
cfdf19d3ca32
generalize compact_path_image to topological_space
hoelzl
parents:
50884
diff
changeset

60 
lemma compact_path_image[intro]: "path g \<Longrightarrow> compact(path_image g)" 
36583  61 
unfolding path_def path_image_def 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36583
diff
changeset

62 
by (erule compact_continuous_image, rule compact_interval) 
36583  63 

64 
lemma reversepath_reversepath[simp]: "reversepath(reversepath g) = g" 

65 
unfolding reversepath_def by auto 

66 

67 
lemma pathstart_reversepath[simp]: "pathstart(reversepath g) = pathfinish g" 

68 
unfolding pathstart_def reversepath_def pathfinish_def by auto 

69 

70 
lemma pathfinish_reversepath[simp]: "pathfinish(reversepath g) = pathstart g" 

71 
unfolding pathstart_def reversepath_def pathfinish_def by auto 

72 

49653  73 
lemma pathstart_join[simp]: "pathstart (g1 +++ g2) = pathstart g1" 
36583  74 
unfolding pathstart_def joinpaths_def pathfinish_def by auto 
75 

49653  76 
lemma pathfinish_join[simp]: "pathfinish (g1 +++ g2) = pathfinish g2" 
36583  77 
unfolding pathstart_def joinpaths_def pathfinish_def by auto 
78 

49653  79 
lemma path_image_reversepath[simp]: "path_image(reversepath g) = path_image g" 
80 
proof  

81 
have *: "\<And>g. path_image(reversepath g) \<subseteq> path_image g" 

82 
unfolding path_image_def subset_eq reversepath_def Ball_def image_iff 

83 
apply(rule,rule,erule bexE) 

84 
apply(rule_tac x="1  xa" in bexI) 

85 
apply auto 

86 
done 

87 
show ?thesis 

88 
using *[of g] *[of "reversepath g"] 

89 
unfolding reversepath_reversepath by auto 

90 
qed 

36583  91 

49653  92 
lemma path_reversepath[simp]: "path (reversepath g) \<longleftrightarrow> path g" 
93 
proof  

94 
have *: "\<And>g. path g \<Longrightarrow> path (reversepath g)" 

95 
unfolding path_def reversepath_def 

96 
apply (rule continuous_on_compose[unfolded o_def, of _ "\<lambda>x. 1  x"]) 

97 
apply (intro continuous_on_intros) 

98 
apply (rule continuous_on_subset[of "{0..1}"], assumption) 

99 
apply auto 

100 
done 

101 
show ?thesis 

102 
using *[of "reversepath g"] *[of g] 

103 
unfolding reversepath_reversepath 

104 
by (rule iffI) 

105 
qed 

106 

107 
lemmas reversepath_simps = 

108 
path_reversepath path_image_reversepath pathstart_reversepath pathfinish_reversepath 

36583  109 

49653  110 
lemma path_join[simp]: 
111 
assumes "pathfinish g1 = pathstart g2" 

112 
shows "path (g1 +++ g2) \<longleftrightarrow> path g1 \<and> path g2" 

113 
unfolding path_def pathfinish_def pathstart_def 

114 
apply rule defer 

115 
apply(erule conjE) 

116 
proof  

117 
assume as: "continuous_on {0..1} (g1 +++ g2)" 

118 
have *: "g1 = (\<lambda>x. g1 (2 *\<^sub>R x)) \<circ> (\<lambda>x. (1/2) *\<^sub>R x)" 

119 
"g2 = (\<lambda>x. g2 (2 *\<^sub>R x  1)) \<circ> (\<lambda>x. (1/2) *\<^sub>R (x + 1))" 

36583  120 
unfolding o_def by (auto simp add: add_divide_distrib) 
49653  121 
have "op *\<^sub>R (1 / 2) ` {0::real..1} \<subseteq> {0..1}" 
122 
"(\<lambda>x. (1 / 2) *\<^sub>R (x + 1)) ` {(0::real)..1} \<subseteq> {0..1}" 

36583  123 
by auto 
49653  124 
then show "continuous_on {0..1} g1 \<and> continuous_on {0..1} g2" 
125 
apply  

126 
apply rule 

127 
apply (subst *) defer 

128 
apply (subst *) 

129 
apply (rule_tac[!] continuous_on_compose) 

44531
1d477a2b1572
replace some continuous_on lemmas with more general versions
huffman
parents:
44170
diff
changeset

130 
apply (intro continuous_on_intros) defer 
1d477a2b1572
replace some continuous_on lemmas with more general versions
huffman
parents:
44170
diff
changeset

131 
apply (intro continuous_on_intros) 
49653  132 
apply (rule_tac[!] continuous_on_eq[of _ "g1 +++ g2"]) defer prefer 3 
133 
apply (rule_tac[12] continuous_on_subset[of "{0 .. 1}"]) 

134 
apply (rule as, assumption, rule as, assumption) 

135 
apply rule defer 

136 
apply rule 

137 
proof  

138 
fix x 

139 
assume "x \<in> op *\<^sub>R (1 / 2) ` {0::real..1}" 

49654  140 
then have "x \<le> 1 / 2" unfolding image_iff by auto 
141 
then show "(g1 +++ g2) x = g1 (2 *\<^sub>R x)" unfolding joinpaths_def by auto 

49653  142 
next 
143 
fix x 

144 
assume "x \<in> (\<lambda>x. (1 / 2) *\<^sub>R (x + 1)) ` {0::real..1}" 

49654  145 
then have "x \<ge> 1 / 2" unfolding image_iff by auto 
146 
then show "(g1 +++ g2) x = g2 (2 *\<^sub>R x  1)" 

49653  147 
proof (cases "x = 1 / 2") 
148 
case True 

49654  149 
then have "x = (1/2) *\<^sub>R 1" by auto 
150 
then show ?thesis 

49653  151 
unfolding joinpaths_def 
152 
using assms[unfolded pathstart_def pathfinish_def] 

153 
by (auto simp add: mult_ac) 

154 
qed (auto simp add:le_less joinpaths_def) 

155 
qed 

156 
next 

157 
assume as:"continuous_on {0..1} g1" "continuous_on {0..1} g2" 

158 
have *: "{0 .. 1::real} = {0.. (1/2)*\<^sub>R 1} \<union> {(1/2) *\<^sub>R 1 .. 1}" by auto 

159 
have **: "op *\<^sub>R 2 ` {0..(1 / 2) *\<^sub>R 1} = {0..1::real}" 

160 
apply (rule set_eqI, rule) 

161 
unfolding image_iff 

162 
defer 

163 
apply (rule_tac x="(1/2)*\<^sub>R x" in bexI) 

164 
apply auto 

165 
done 

166 
have ***: "(\<lambda>x. 2 *\<^sub>R x  1) ` {(1 / 2) *\<^sub>R 1..1} = {0..1::real}" 

36583  167 
apply (auto simp add: image_def) 
168 
apply (rule_tac x="(x + 1) / 2" in bexI) 

169 
apply (auto simp add: add_divide_distrib) 

170 
done 

49653  171 
show "continuous_on {0..1} (g1 +++ g2)" 
172 
unfolding * 

173 
apply (rule continuous_on_union) 

174 
apply (rule closed_real_atLeastAtMost)+ 

175 
proof  

176 
show "continuous_on {0..(1 / 2) *\<^sub>R 1} (g1 +++ g2)" 

177 
apply (rule continuous_on_eq[of _ "\<lambda>x. g1 (2 *\<^sub>R x)"]) defer 

178 
unfolding o_def[THEN sym] 

179 
apply (rule continuous_on_compose) 

180 
apply (intro continuous_on_intros) 

181 
unfolding ** 

182 
apply (rule as(1)) 

183 
unfolding joinpaths_def 

184 
apply auto 

185 
done 

186 
next 

187 
show "continuous_on {(1/2)*\<^sub>R1..1} (g1 +++ g2)" 

188 
apply (rule continuous_on_eq[of _ "g2 \<circ> (\<lambda>x. 2 *\<^sub>R x  1)"]) defer 

189 
apply (rule continuous_on_compose) 

190 
apply (intro continuous_on_intros) 

191 
unfolding *** o_def joinpaths_def 

192 
apply (rule as(2)) 

193 
using assms[unfolded pathstart_def pathfinish_def] 

194 
apply (auto simp add: mult_ac) 

195 
done 

196 
qed 

197 
qed 

36583  198 

49653  199 
lemma path_image_join_subset: "path_image(g1 +++ g2) \<subseteq> (path_image g1 \<union> path_image g2)" 
200 
proof 

201 
fix x 

202 
assume "x \<in> path_image (g1 +++ g2)" 

36583  203 
then obtain y where y:"y\<in>{0..1}" "x = (if y \<le> 1 / 2 then g1 (2 *\<^sub>R y) else g2 (2 *\<^sub>R y  1))" 
204 
unfolding path_image_def image_iff joinpaths_def by auto 

49654  205 
then show "x \<in> path_image g1 \<union> path_image g2" 
49653  206 
apply (cases "y \<le> 1/2") 
207 
apply (rule_tac UnI1) defer 

208 
apply (rule_tac UnI2) 

209 
unfolding y(2) path_image_def 

210 
using y(1) 

211 
apply (auto intro!: imageI) 

212 
done 

213 
qed 

36583  214 

215 
lemma subset_path_image_join: 

49653  216 
assumes "path_image g1 \<subseteq> s" "path_image g2 \<subseteq> s" 
217 
shows "path_image(g1 +++ g2) \<subseteq> s" 

36583  218 
using path_image_join_subset[of g1 g2] and assms by auto 
219 

220 
lemma path_image_join: 

221 
assumes "path g1" "path g2" "pathfinish g1 = pathstart g2" 

222 
shows "path_image(g1 +++ g2) = (path_image g1) \<union> (path_image g2)" 

49653  223 
apply (rule, rule path_image_join_subset, rule) 
224 
unfolding Un_iff 

225 
proof (erule disjE) 

226 
fix x 

227 
assume "x \<in> path_image g1" 

228 
then obtain y where y: "y\<in>{0..1}" "x = g1 y" 

229 
unfolding path_image_def image_iff by auto 

49654  230 
then show "x \<in> path_image (g1 +++ g2)" 
49653  231 
unfolding joinpaths_def path_image_def image_iff 
232 
apply (rule_tac x="(1/2) *\<^sub>R y" in bexI) 

233 
apply auto 

234 
done 

235 
next 

236 
fix x 

237 
assume "x \<in> path_image g2" 

238 
then obtain y where y: "y\<in>{0..1}" "x = g2 y" 

239 
unfolding path_image_def image_iff by auto 

240 
then show "x \<in> path_image (g1 +++ g2)" 

241 
unfolding joinpaths_def path_image_def image_iff 

242 
apply(rule_tac x="(1/2) *\<^sub>R (y + 1)" in bexI) 

243 
using assms(3)[unfolded pathfinish_def pathstart_def] 

244 
apply (auto simp add: add_divide_distrib) 

245 
done 

246 
qed 

36583  247 

248 
lemma not_in_path_image_join: 

49653  249 
assumes "x \<notin> path_image g1" "x \<notin> path_image g2" 
250 
shows "x \<notin> path_image(g1 +++ g2)" 

36583  251 
using assms and path_image_join_subset[of g1 g2] by auto 
252 

49653  253 
lemma simple_path_reversepath: 
254 
assumes "simple_path g" 

255 
shows "simple_path (reversepath g)" 

256 
using assms 

257 
unfolding simple_path_def reversepath_def 

258 
apply  

259 
apply (rule ballI)+ 

260 
apply (erule_tac x="1x" in ballE, erule_tac x="1y" in ballE) 

261 
apply auto 

262 
done 

36583  263 

264 
lemma simple_path_join_loop: 

265 
assumes "injective_path g1" "injective_path g2" "pathfinish g2 = pathstart g1" 

49653  266 
"(path_image g1 \<inter> path_image g2) \<subseteq> {pathstart g1,pathstart g2}" 
36583  267 
shows "simple_path(g1 +++ g2)" 
49653  268 
unfolding simple_path_def 
269 
proof ((rule ballI)+, rule impI) 

270 
let ?g = "g1 +++ g2" 

36583  271 
note inj = assms(1,2)[unfolded injective_path_def, rule_format] 
49653  272 
fix x y :: real 
273 
assume xy: "x \<in> {0..1}" "y \<in> {0..1}" "?g x = ?g y" 

274 
show "x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0" 

275 
proof (case_tac "x \<le> 1/2", case_tac[!] "y \<le> 1/2", unfold not_le) 

276 
assume as: "x \<le> 1 / 2" "y \<le> 1 / 2" 

49654  277 
then have "g1 (2 *\<^sub>R x) = g1 (2 *\<^sub>R y)" 
49653  278 
using xy(3) unfolding joinpaths_def by auto 
279 
moreover 

280 
have "2 *\<^sub>R x \<in> {0..1}" "2 *\<^sub>R y \<in> {0..1}" using xy(1,2) as 

36583  281 
by auto 
49653  282 
ultimately 
283 
show ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] by auto 

284 
next 

285 
assume as:"x > 1 / 2" "y > 1 / 2" 

49654  286 
then have "g2 (2 *\<^sub>R x  1) = g2 (2 *\<^sub>R y  1)" 
49653  287 
using xy(3) unfolding joinpaths_def by auto 
288 
moreover 

289 
have "2 *\<^sub>R x  1 \<in> {0..1}" "2 *\<^sub>R y  1 \<in> {0..1}" 

290 
using xy(1,2) as by auto 

291 
ultimately 

292 
show ?thesis using inj(2)[of "2*\<^sub>R x  1" "2*\<^sub>R y  1"] by auto 

293 
next 

294 
assume as:"x \<le> 1 / 2" "y > 1 / 2" 

49654  295 
then have "?g x \<in> path_image g1" "?g y \<in> path_image g2" 
49653  296 
unfolding path_image_def joinpaths_def 
36583  297 
using xy(1,2) by auto 
49653  298 
moreover 
299 
have "?g y \<noteq> pathstart g2" using as(2) unfolding pathstart_def joinpaths_def 

36583  300 
using inj(2)[of "2 *\<^sub>R y  1" 0] and xy(2) 
301 
by (auto simp add: field_simps) 

49653  302 
ultimately 
303 
have *:"?g x = pathstart g1" using assms(4) unfolding xy(3) by auto 

49654  304 
then have "x = 0" unfolding pathstart_def joinpaths_def using as(1) and xy(1) 
36583  305 
using inj(1)[of "2 *\<^sub>R x" 0] by auto 
49653  306 
moreover 
307 
have "y = 1" using * unfolding xy(3) assms(3)[THEN sym] 

36583  308 
unfolding joinpaths_def pathfinish_def using as(2) and xy(2) 
309 
using inj(2)[of "2 *\<^sub>R y  1" 1] by auto 

310 
ultimately show ?thesis by auto 

49653  311 
next 
312 
assume as: "x > 1 / 2" "y \<le> 1 / 2" 

49654  313 
then have "?g x \<in> path_image g2" "?g y \<in> path_image g1" 
49653  314 
unfolding path_image_def joinpaths_def 
36583  315 
using xy(1,2) by auto 
49653  316 
moreover 
317 
have "?g x \<noteq> pathstart g2" using as(1) unfolding pathstart_def joinpaths_def 

36583  318 
using inj(2)[of "2 *\<^sub>R x  1" 0] and xy(1) 
319 
by (auto simp add: field_simps) 

49653  320 
ultimately 
321 
have *: "?g y = pathstart g1" using assms(4) unfolding xy(3) by auto 

49654  322 
then have "y = 0" unfolding pathstart_def joinpaths_def using as(2) and xy(2) 
36583  323 
using inj(1)[of "2 *\<^sub>R y" 0] by auto 
49653  324 
moreover 
325 
have "x = 1" using * unfolding xy(3)[THEN sym] assms(3)[THEN sym] 

36583  326 
unfolding joinpaths_def pathfinish_def using as(1) and xy(1) 
327 
using inj(2)[of "2 *\<^sub>R x  1" 1] by auto 

49653  328 
ultimately show ?thesis by auto 
329 
qed 

330 
qed 

36583  331 

332 
lemma injective_path_join: 

333 
assumes "injective_path g1" "injective_path g2" "pathfinish g1 = pathstart g2" 

49653  334 
"(path_image g1 \<inter> path_image g2) \<subseteq> {pathstart g2}" 
36583  335 
shows "injective_path(g1 +++ g2)" 
49653  336 
unfolding injective_path_def 
337 
proof (rule, rule, rule) 

338 
let ?g = "g1 +++ g2" 

36583  339 
note inj = assms(1,2)[unfolded injective_path_def, rule_format] 
49653  340 
fix x y 
341 
assume xy: "x \<in> {0..1}" "y \<in> {0..1}" "(g1 +++ g2) x = (g1 +++ g2) y" 

342 
show "x = y" 

343 
proof (cases "x \<le> 1/2", case_tac[!] "y \<le> 1/2", unfold not_le) 

344 
assume "x \<le> 1 / 2" "y \<le> 1 / 2" 

49654  345 
then show ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] and xy 
36583  346 
unfolding joinpaths_def by auto 
49653  347 
next 
348 
assume "x > 1 / 2" "y > 1 / 2" 

49654  349 
then show ?thesis using inj(2)[of "2*\<^sub>R x  1" "2*\<^sub>R y  1"] and xy 
36583  350 
unfolding joinpaths_def by auto 
49653  351 
next 
352 
assume as: "x \<le> 1 / 2" "y > 1 / 2" 

49654  353 
then have "?g x \<in> path_image g1" "?g y \<in> path_image g2" 
49653  354 
unfolding path_image_def joinpaths_def 
36583  355 
using xy(1,2) by auto 
49654  356 
then have "?g x = pathfinish g1" "?g y = pathstart g2" 
49653  357 
using assms(4) unfolding assms(3) xy(3) by auto 
49654  358 
then show ?thesis 
49653  359 
using as and inj(1)[of "2 *\<^sub>R x" 1] inj(2)[of "2 *\<^sub>R y  1" 0] and xy(1,2) 
36583  360 
unfolding pathstart_def pathfinish_def joinpaths_def 
361 
by auto 

49653  362 
next 
363 
assume as:"x > 1 / 2" "y \<le> 1 / 2" 

49654  364 
then have "?g x \<in> path_image g2" "?g y \<in> path_image g1" 
49653  365 
unfolding path_image_def joinpaths_def 
36583  366 
using xy(1,2) by auto 
49654  367 
then have "?g x = pathstart g2" "?g y = pathfinish g1" 
49653  368 
using assms(4) unfolding assms(3) xy(3) by auto 
49654  369 
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) 
36583  370 
unfolding pathstart_def pathfinish_def joinpaths_def 
49653  371 
by auto 
372 
qed 

373 
qed 

36583  374 

375 
lemmas join_paths_simps = path_join path_image_join pathstart_join pathfinish_join 

376 

49653  377 

36583  378 
subsection {* Reparametrizing a closed curve to start at some chosen point. *} 
379 

380 
definition "shiftpath a (f::real \<Rightarrow> 'a::topological_space) = 

381 
(\<lambda>x. if (a + x) \<le> 1 then f(a + x) else f(a + x  1))" 

382 

383 
lemma pathstart_shiftpath: "a \<le> 1 \<Longrightarrow> pathstart(shiftpath a g) = g a" 

384 
unfolding pathstart_def shiftpath_def by auto 

385 

49653  386 
lemma pathfinish_shiftpath: 
387 
assumes "0 \<le> a" "pathfinish g = pathstart g" 

36583  388 
shows "pathfinish(shiftpath a g) = g a" 
389 
using assms unfolding pathstart_def pathfinish_def shiftpath_def 

390 
by auto 

391 

392 
lemma endpoints_shiftpath: 

393 
assumes "pathfinish g = pathstart g" "a \<in> {0 .. 1}" 

394 
shows "pathfinish(shiftpath a g) = g a" "pathstart(shiftpath a g) = g a" 

395 
using assms by(auto intro!:pathfinish_shiftpath pathstart_shiftpath) 

396 

397 
lemma closed_shiftpath: 

398 
assumes "pathfinish g = pathstart g" "a \<in> {0..1}" 

399 
shows "pathfinish(shiftpath a g) = pathstart(shiftpath a g)" 

400 
using endpoints_shiftpath[OF assms] by auto 

401 

402 
lemma path_shiftpath: 

403 
assumes "path g" "pathfinish g = pathstart g" "a \<in> {0..1}" 

49653  404 
shows "path(shiftpath a g)" 
405 
proof  

406 
have *: "{0 .. 1} = {0 .. 1a} \<union> {1a .. 1}" using assms(3) by auto 

407 
have **: "\<And>x. x + a = 1 \<Longrightarrow> g (x + a  1) = g (x + a)" 

36583  408 
using assms(2)[unfolded pathfinish_def pathstart_def] by auto 
49653  409 
show ?thesis 
410 
unfolding path_def shiftpath_def * 

411 
apply (rule continuous_on_union) 

412 
apply (rule closed_real_atLeastAtMost)+ 

413 
apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a + x)"]) prefer 3 

414 
apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a  1 + x)"]) defer prefer 3 

415 
apply (rule continuous_on_intros)+ prefer 2 

416 
apply (rule continuous_on_intros)+ 

417 
apply (rule_tac[12] continuous_on_subset[OF assms(1)[unfolded path_def]]) 

418 
using assms(3) and ** 

419 
apply (auto, auto simp add: field_simps) 

420 
done 

421 
qed 

36583  422 

49653  423 
lemma shiftpath_shiftpath: 
424 
assumes "pathfinish g = pathstart g" "a \<in> {0..1}" "x \<in> {0..1}" 

36583  425 
shows "shiftpath (1  a) (shiftpath a g) x = g x" 
426 
using assms unfolding pathfinish_def pathstart_def shiftpath_def by auto 

427 

428 
lemma path_image_shiftpath: 

429 
assumes "a \<in> {0..1}" "pathfinish g = pathstart g" 

49653  430 
shows "path_image(shiftpath a g) = path_image g" 
431 
proof  

432 
{ fix x 

433 
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)" 

49654  434 
then have "\<exists>y\<in>{0..1} \<inter> {x. a + x \<le> 1}. g x = g (a + y)" 
49653  435 
proof (cases "a \<le> x") 
436 
case False 

49654  437 
then show ?thesis 
49653  438 
apply (rule_tac x="1 + x  a" in bexI) 
36583  439 
using as(1,2) and as(3)[THEN bspec[where x="1 + x  a"]] and assms(1) 
49653  440 
apply (auto simp add: field_simps atomize_not) 
441 
done 

442 
next 

443 
case True 

49654  444 
then show ?thesis using as(12) and assms(1) apply(rule_tac x="x  a" in bexI) 
49653  445 
by(auto simp add: field_simps) 
446 
qed 

447 
} 

49654  448 
then show ?thesis 
49653  449 
using assms unfolding shiftpath_def path_image_def pathfinish_def pathstart_def 
450 
by(auto simp add: image_iff) 

451 
qed 

452 

36583  453 

454 
subsection {* Special case of straightline paths. *} 

455 

49653  456 
definition linepath :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> real \<Rightarrow> 'a" 
457 
where "linepath a b = (\<lambda>x. (1  x) *\<^sub>R a + x *\<^sub>R b)" 

36583  458 

459 
lemma pathstart_linepath[simp]: "pathstart(linepath a b) = a" 

460 
unfolding pathstart_def linepath_def by auto 

461 

462 
lemma pathfinish_linepath[simp]: "pathfinish(linepath a b) = b" 

463 
unfolding pathfinish_def linepath_def by auto 

464 

465 
lemma continuous_linepath_at[intro]: "continuous (at x) (linepath a b)" 

466 
unfolding linepath_def by (intro continuous_intros) 

467 

468 
lemma continuous_on_linepath[intro]: "continuous_on s (linepath a b)" 

469 
using continuous_linepath_at by(auto intro!: continuous_at_imp_continuous_on) 

470 

471 
lemma path_linepath[intro]: "path(linepath a b)" 

472 
unfolding path_def by(rule continuous_on_linepath) 

473 

474 
lemma path_image_linepath[simp]: "path_image(linepath a b) = (closed_segment a b)" 

49653  475 
unfolding path_image_def segment linepath_def 
476 
apply (rule set_eqI, rule) defer 

477 
unfolding mem_Collect_eq image_iff 

478 
apply(erule exE) 

479 
apply(rule_tac x="u *\<^sub>R 1" in bexI) 

480 
apply auto 

481 
done 

482 

483 
lemma reversepath_linepath[simp]: "reversepath(linepath a b) = linepath b a" 

484 
unfolding reversepath_def linepath_def 

36583  485 
by auto 
486 

487 
lemma injective_path_linepath: 

49653  488 
assumes "a \<noteq> b" 
489 
shows "injective_path (linepath a b)" 

36583  490 
proof  
491 
{ fix x y :: "real" 

492 
assume "x *\<^sub>R b + y *\<^sub>R a = x *\<^sub>R a + y *\<^sub>R b" 

49654  493 
then have "(x  y) *\<^sub>R a = (x  y) *\<^sub>R b" by (simp add: algebra_simps) 
36583  494 
with assms have "x = y" by simp } 
49654  495 
then show ?thesis 
49653  496 
unfolding injective_path_def linepath_def 
497 
by (auto simp add: algebra_simps) 

498 
qed 

36583  499 

49653  500 
lemma simple_path_linepath[intro]: "a \<noteq> b \<Longrightarrow> simple_path(linepath a b)" 
501 
by(auto intro!: injective_imp_simple_path injective_path_linepath) 

502 

36583  503 

504 
subsection {* Bounding a point away from a path. *} 

505 

506 
lemma not_on_path_ball: 

507 
fixes g :: "real \<Rightarrow> 'a::heine_borel" 

508 
assumes "path g" "z \<notin> path_image g" 

49653  509 
shows "\<exists>e > 0. ball z e \<inter> (path_image g) = {}" 
510 
proof  

511 
obtain a where "a \<in> path_image g" "\<forall>y \<in> path_image g. dist z a \<le> dist z y" 

36583  512 
using distance_attains_inf[OF _ path_image_nonempty, of g z] 
513 
using compact_path_image[THEN compact_imp_closed, OF assms(1)] by auto 

49654  514 
then show ?thesis 
49653  515 
apply (rule_tac x="dist z a" in exI) 
516 
using assms(2) 

517 
apply (auto intro!: dist_pos_lt) 

518 
done 

519 
qed 

36583  520 

521 
lemma not_on_path_cball: 

522 
fixes g :: "real \<Rightarrow> 'a::heine_borel" 

523 
assumes "path g" "z \<notin> path_image g" 

49653  524 
shows "\<exists>e>0. cball z e \<inter> (path_image g) = {}" 
525 
proof  

526 
obtain e where "ball z e \<inter> path_image g = {}" "e>0" 

527 
using not_on_path_ball[OF assms] by auto 

36583  528 
moreover have "cball z (e/2) \<subseteq> ball z e" using `e>0` by auto 
49653  529 
ultimately show ?thesis apply(rule_tac x="e/2" in exI) by auto 
530 
qed 

531 

36583  532 

533 
subsection {* Path component, considered as a "joinability" relation (from Tom Hales). *} 

534 

49653  535 
definition "path_component s x y \<longleftrightarrow> 
536 
(\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)" 

36583  537 

538 
lemmas path_defs = path_def pathstart_def pathfinish_def path_image_def path_component_def 

539 

49653  540 
lemma path_component_mem: 
541 
assumes "path_component s x y" 

542 
shows "x \<in> s" "y \<in> s" 

36583  543 
using assms unfolding path_defs by auto 
544 

49653  545 
lemma path_component_refl: 
546 
assumes "x \<in> s" 

547 
shows "path_component s x x" 

548 
unfolding path_defs 

549 
apply (rule_tac x="\<lambda>u. x" in exI) 

550 
using assms apply (auto intro!:continuous_on_intros) done 

36583  551 

552 
lemma path_component_refl_eq: "path_component s x x \<longleftrightarrow> x \<in> s" 

49653  553 
by (auto intro!: path_component_mem path_component_refl) 
36583  554 

555 
lemma path_component_sym: "path_component s x y \<Longrightarrow> path_component s y x" 

49653  556 
using assms 
557 
unfolding path_component_def 

558 
apply (erule exE) 

559 
apply (rule_tac x="reversepath g" in exI) 

560 
apply auto 

561 
done 

36583  562 

49653  563 
lemma path_component_trans: 
564 
assumes "path_component s x y" "path_component s y z" 

565 
shows "path_component s x z" 

566 
using assms 

567 
unfolding path_component_def 

568 
apply  

569 
apply (erule exE)+ 

570 
apply (rule_tac x="g +++ ga" in exI) 

571 
apply (auto simp add: path_image_join) 

572 
done 

36583  573 

574 
lemma path_component_of_subset: "s \<subseteq> t \<Longrightarrow> path_component s x y \<Longrightarrow> path_component t x y" 

575 
unfolding path_component_def by auto 

576 

49653  577 

36583  578 
subsection {* Can also consider it as a set, as the name suggests. *} 
579 

49653  580 
lemma path_component_set: 
581 
"{y. path_component s x y} = 

582 
{y. (\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)}" 

583 
apply (rule set_eqI) 

584 
unfolding mem_Collect_eq 

585 
unfolding path_component_def 

586 
apply auto 

587 
done 

36583  588 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
41959
diff
changeset

589 
lemma path_component_subset: "{y. path_component s x y} \<subseteq> s" 
49653  590 
apply (rule, rule path_component_mem(2)) 
591 
apply auto 

592 
done 

36583  593 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
41959
diff
changeset

594 
lemma path_component_eq_empty: "{y. path_component s x y} = {} \<longleftrightarrow> x \<notin> s" 
49653  595 
apply rule 
596 
apply (drule equals0D[of _ x]) defer 

597 
apply (rule equals0I) 

598 
unfolding mem_Collect_eq 

599 
apply (drule path_component_mem(1)) 

600 
using path_component_refl 

601 
apply auto 

602 
done 

603 

36583  604 

605 
subsection {* Path connectedness of a space. *} 

606 

49653  607 
definition "path_connected s \<longleftrightarrow> 
608 
(\<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)" 

36583  609 

610 
lemma path_connected_component: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. path_component s x y)" 

611 
unfolding path_connected_def path_component_def by auto 

612 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
41959
diff
changeset

613 
lemma path_connected_component_set: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. {y. path_component s x y} = s)" 
49653  614 
unfolding path_connected_component 
615 
apply (rule, rule, rule, rule path_component_subset) 

616 
unfolding subset_eq mem_Collect_eq Ball_def 

617 
apply auto 

618 
done 

619 

36583  620 

621 
subsection {* Some useful lemmas about pathconnectedness. *} 

622 

623 
lemma convex_imp_path_connected: 

624 
fixes s :: "'a::real_normed_vector set" 

625 
assumes "convex s" shows "path_connected s" 

49653  626 
unfolding path_connected_def 
627 
apply (rule, rule, rule_tac x = "linepath x y" in exI) 

628 
unfolding path_image_linepath 

629 
using assms [unfolded convex_contains_segment] 

630 
apply auto 

631 
done 

36583  632 

49653  633 
lemma path_connected_imp_connected: 
634 
assumes "path_connected s" 

635 
shows "connected s" 

636 
unfolding connected_def not_ex 

637 
apply (rule, rule, rule ccontr) 

638 
unfolding not_not 

639 
apply (erule conjE)+ 

640 
proof  

641 
fix e1 e2 

642 
assume as: "open e1" "open e2" "s \<subseteq> e1 \<union> e2" "e1 \<inter> e2 \<inter> s = {}" "e1 \<inter> s \<noteq> {}" "e2 \<inter> s \<noteq> {}" 

36583  643 
then obtain x1 x2 where obt:"x1\<in>e1\<inter>s" "x2\<in>e2\<inter>s" by auto 
644 
then obtain g where g:"path g" "path_image g \<subseteq> s" "pathstart g = x1" "pathfinish g = x2" 

645 
using assms[unfolded path_connected_def,rule_format,of x1 x2] by auto 

49653  646 
have *: "connected {0..1::real}" 
647 
by (auto intro!: convex_connected convex_real_interval) 

648 
have "{0..1} \<subseteq> {x \<in> {0..1}. g x \<in> e1} \<union> {x \<in> {0..1}. g x \<in> e2}" 

649 
using as(3) g(2)[unfolded path_defs] by blast 

650 
moreover have "{x \<in> {0..1}. g x \<in> e1} \<inter> {x \<in> {0..1}. g x \<in> e2} = {}" 

651 
using as(4) g(2)[unfolded path_defs] unfolding subset_eq by auto 

652 
moreover have "{x \<in> {0..1}. g x \<in> e1} \<noteq> {} \<and> {x \<in> {0..1}. g x \<in> e2} \<noteq> {}" 

653 
using g(3,4)[unfolded path_defs] using obt 

36583  654 
by (simp add: ex_in_conv [symmetric], metis zero_le_one order_refl) 
49653  655 
ultimately show False 
656 
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}"] 

36583  657 
using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(1)] 
49653  658 
using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(2)] 
659 
by auto 

660 
qed 

36583  661 

662 
lemma open_path_component: 

663 
fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*) 

49653  664 
assumes "open s" 
665 
shows "open {y. path_component s x y}" 

666 
unfolding open_contains_ball 

667 
proof 

668 
fix y 

669 
assume as: "y \<in> {y. path_component s x y}" 

49654  670 
then have "y \<in> s" 
49653  671 
apply  
672 
apply (rule path_component_mem(2)) 

673 
unfolding mem_Collect_eq 

674 
apply auto 

675 
done 

676 
then obtain e where e:"e>0" "ball y e \<subseteq> s" 

677 
using assms[unfolded open_contains_ball] by auto 

678 
show "\<exists>e > 0. ball y e \<subseteq> {y. path_component s x y}" 

679 
apply (rule_tac x=e in exI) 

680 
apply (rule,rule `e>0`, rule) 

681 
unfolding mem_ball mem_Collect_eq 

682 
proof  

683 
fix z 

684 
assume "dist y z < e" 

49654  685 
then show "path_component s x z" 
49653  686 
apply (rule_tac path_component_trans[of _ _ y]) defer 
687 
apply (rule path_component_of_subset[OF e(2)]) 

688 
apply (rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format]) 

689 
using `e>0` as 

690 
apply auto 

691 
done 

692 
qed 

693 
qed 

36583  694 

695 
lemma open_non_path_component: 

696 
fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*) 

49653  697 
assumes "open s" 
698 
shows "open(s  {y. path_component s x y})" 

699 
unfolding open_contains_ball 

700 
proof 

701 
fix y 

702 
assume as: "y\<in>s  {y. path_component s x y}" 

703 
then obtain e where e:"e>0" "ball y e \<subseteq> s" 

704 
using assms [unfolded open_contains_ball] by auto 

705 
show "\<exists>e>0. ball y e \<subseteq> s  {y. path_component s x y}" 

706 
apply (rule_tac x=e in exI) 

707 
apply (rule, rule `e>0`, rule, rule) defer 

708 
proof (rule ccontr) 

709 
fix z 

710 
assume "z \<in> ball y e" "\<not> z \<notin> {y. path_component s x y}" 

49654  711 
then have "y \<in> {y. path_component s x y}" 
49653  712 
unfolding not_not mem_Collect_eq using `e>0` 
713 
apply  

714 
apply (rule path_component_trans, assumption) 

715 
apply (rule path_component_of_subset[OF e(2)]) 

716 
apply (rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format]) 

717 
apply auto 

718 
done 

49654  719 
then show False using as by auto 
49653  720 
qed (insert e(2), auto) 
721 
qed 

36583  722 

723 
lemma connected_open_path_connected: 

724 
fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*) 

49653  725 
assumes "open s" "connected s" 
726 
shows "path_connected s" 

727 
unfolding path_connected_component_set 

728 
proof (rule, rule, rule path_component_subset, rule) 

729 
fix x y 

730 
assume "x \<in> s" "y \<in> s" 

731 
show "y \<in> {y. path_component s x y}" 

732 
proof (rule ccontr) 

733 
assume "y \<notin> {y. path_component s x y}" 

734 
moreover 

735 
have "{y. path_component s x y} \<inter> s \<noteq> {}" 

736 
using `x\<in>s` path_component_eq_empty path_component_subset[of s x] by auto 

737 
ultimately 

738 
show False 

739 
using `y\<in>s` open_non_path_component[OF assms(1)] open_path_component[OF assms(1)] 

740 
using assms(2)[unfolded connected_def not_ex, rule_format, of"{y. path_component s x y}" "s  {y. path_component s x y}"] 

741 
by auto 

742 
qed 

743 
qed 

36583  744 

745 
lemma path_connected_continuous_image: 

49653  746 
assumes "continuous_on s f" "path_connected s" 
747 
shows "path_connected (f ` s)" 

748 
unfolding path_connected_def 

749 
proof (rule, rule) 

750 
fix x' y' 

751 
assume "x' \<in> f ` s" "y' \<in> f ` s" 

752 
then obtain x y where xy: "x\<in>s" "y\<in>s" "x' = f x" "y' = f y" by auto 

753 
guess g using assms(2)[unfolded path_connected_def, rule_format, OF xy(1,2)] .. 

49654  754 
then show "\<exists>g. path g \<and> path_image g \<subseteq> f ` s \<and> pathstart g = x' \<and> pathfinish g = y'" 
49653  755 
unfolding xy 
756 
apply (rule_tac x="f \<circ> g" in exI) 

757 
unfolding path_defs 

758 
using assms(1) 

759 
apply (auto intro!: continuous_on_compose continuous_on_subset[of _ _ "g ` {0..1}"]) 

760 
done 

761 
qed 

36583  762 

763 
lemma homeomorphic_path_connectedness: 

764 
"s homeomorphic t \<Longrightarrow> (path_connected s \<longleftrightarrow> path_connected t)" 

49653  765 
unfolding homeomorphic_def homeomorphism_def 
766 
apply (erule exEerule conjE)+ 

767 
apply rule 

768 
apply (drule_tac f=f in path_connected_continuous_image) prefer 3 

769 
apply (drule_tac f=g in path_connected_continuous_image) 

770 
apply auto 

771 
done 

36583  772 

773 
lemma path_connected_empty: "path_connected {}" 

774 
unfolding path_connected_def by auto 

775 

776 
lemma path_connected_singleton: "path_connected {a}" 

777 
unfolding path_connected_def pathstart_def pathfinish_def path_image_def 

778 
apply (clarify, rule_tac x="\<lambda>x. a" in exI, simp add: image_constant_conv) 

779 
apply (simp add: path_def continuous_on_const) 

780 
done 

781 

49653  782 
lemma path_connected_Un: 
783 
assumes "path_connected s" "path_connected t" "s \<inter> t \<noteq> {}" 

784 
shows "path_connected (s \<union> t)" 

785 
unfolding path_connected_component 

786 
proof (rule, rule) 

787 
fix x y 

788 
assume as: "x \<in> s \<union> t" "y \<in> s \<union> t" 

36583  789 
from assms(3) obtain z where "z \<in> s \<inter> t" by auto 
49654  790 
then show "path_component (s \<union> t) x y" 
49653  791 
using as and assms(12)[unfolded path_connected_component] 
792 
apply  

793 
apply (erule_tac[!] UnE)+ 

794 
apply (rule_tac[23] path_component_trans[of _ _ z]) 

795 
apply (auto simp add:path_component_of_subset [OF Un_upper1] path_component_of_subset[OF Un_upper2]) 

796 
done 

797 
qed 

36583  798 

37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

799 
lemma path_connected_UNION: 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

800 
assumes "\<And>i. i \<in> A \<Longrightarrow> path_connected (S i)" 
49653  801 
and "\<And>i. i \<in> A \<Longrightarrow> z \<in> S i" 
37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

802 
shows "path_connected (\<Union>i\<in>A. S i)" 
49653  803 
unfolding path_connected_component 
804 
proof clarify 

37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

805 
fix x i y j 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

806 
assume *: "i \<in> A" "x \<in> S i" "j \<in> A" "y \<in> S j" 
49654  807 
then have "path_component (S i) x z" and "path_component (S j) z y" 
37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

808 
using assms by (simp_all add: path_connected_component) 
49654  809 
then have "path_component (\<Union>i\<in>A. S i) x z" and "path_component (\<Union>i\<in>A. S i) z y" 
48125
602dc0215954
tuned proofs  prefer direct "rotated" instead of oldstyle COMP;
wenzelm
parents:
44647
diff
changeset

810 
using *(1,3) by (auto elim!: path_component_of_subset [rotated]) 
49654  811 
then show "path_component (\<Union>i\<in>A. S i) x y" 
37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

812 
by (rule path_component_trans) 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

813 
qed 
36583  814 

49653  815 

37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

816 
subsection {* sphere is pathconnected. *} 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36583
diff
changeset

817 

36583  818 
lemma path_connected_punctured_universe: 
37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

819 
assumes "2 \<le> DIM('a::euclidean_space)" 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

820 
shows "path_connected((UNIV::'a::euclidean_space set)  {a})" 
49653  821 
proof  
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

822 
let ?A = "{x::'a. \<exists>i\<in>Basis. x \<bullet> i < a \<bullet> i}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

823 
let ?B = "{x::'a. \<exists>i\<in>Basis. a \<bullet> i < x \<bullet> i}" 
36583  824 

49653  825 
have A: "path_connected ?A" 
826 
unfolding Collect_bex_eq 

37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

827 
proof (rule path_connected_UNION) 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

828 
fix i :: 'a 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

829 
assume "i \<in> Basis" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

830 
then show "(\<Sum>i\<in>Basis. (a \<bullet> i  1)*\<^sub>R i) \<in> {x::'a. x \<bullet> i < a \<bullet> i}" by simp 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

831 
show "path_connected {x. x \<bullet> i < a \<bullet> i}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

832 
using convex_imp_path_connected [OF convex_halfspace_lt, of i "a \<bullet> i"] 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

833 
by (simp add: inner_commute) 
37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

834 
qed 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

835 
have B: "path_connected ?B" unfolding Collect_bex_eq 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

836 
proof (rule path_connected_UNION) 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

837 
fix i :: 'a 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

838 
assume "i \<in> Basis" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

839 
then show "(\<Sum>i\<in>Basis. (a \<bullet> i + 1) *\<^sub>R i) \<in> {x::'a. a \<bullet> i < x \<bullet> i}" by simp 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

840 
show "path_connected {x. a \<bullet> i < x \<bullet> i}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

841 
using convex_imp_path_connected [OF convex_halfspace_gt, of "a \<bullet> i" i] 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

842 
by (simp add: inner_commute) 
37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

843 
qed 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

844 
obtain S :: "'a set" where "S \<subseteq> Basis" "card S = Suc (Suc 0)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

845 
using ex_card[OF assms] by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

846 
then obtain b0 b1 :: 'a where "b0 \<in> Basis" "b1 \<in> Basis" "b0 \<noteq> b1" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

847 
unfolding card_Suc_eq by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

848 
then have "a + b0  b1 \<in> ?A \<inter> ?B" by (auto simp: inner_simps inner_Basis) 
49654  849 
then have "?A \<inter> ?B \<noteq> {}" by fast 
37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

850 
with A B have "path_connected (?A \<union> ?B)" 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

851 
by (rule path_connected_Un) 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

852 
also have "?A \<union> ?B = {x. \<exists>i\<in>Basis. x \<bullet> i \<noteq> a \<bullet> i}" 
37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

853 
unfolding neq_iff bex_disj_distrib Collect_disj_eq .. 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

854 
also have "\<dots> = {x. x \<noteq> a}" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

855 
unfolding euclidean_eq_iff [where 'a='a] by (simp add: Bex_def) 
37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

856 
also have "\<dots> = UNIV  {a}" by auto 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

857 
finally show ?thesis . 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

858 
qed 
36583  859 

37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

860 
lemma path_connected_sphere: 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

861 
assumes "2 \<le> DIM('a::euclidean_space)" 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

862 
shows "path_connected {x::'a::euclidean_space. norm(x  a) = r}" 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

863 
proof (rule linorder_cases [of r 0]) 
49653  864 
assume "r < 0" 
49654  865 
then have "{x::'a. norm(x  a) = r} = {}" by auto 
866 
then show ?thesis using path_connected_empty by simp 

37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

867 
next 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

868 
assume "r = 0" 
49654  869 
then show ?thesis using path_connected_singleton by simp 
37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

870 
next 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

871 
assume r: "0 < r" 
49654  872 
then have *: "{x::'a. norm(x  a) = r} = (\<lambda>x. a + r *\<^sub>R x) ` {x. norm x = 1}" 
49653  873 
apply  
874 
apply (rule set_eqI, rule) 

875 
unfolding image_iff 

876 
apply (rule_tac x="(1/r) *\<^sub>R (x  a)" in bexI) 

877 
unfolding mem_Collect_eq norm_scaleR 

878 
apply (auto simp add: scaleR_right_diff_distrib) 

879 
done 

880 
have **: "{x::'a. norm x = 1} = (\<lambda>x. (1/norm x) *\<^sub>R x) ` (UNIV  {0})" 

881 
apply (rule set_eqI,rule) 

882 
unfolding image_iff 

883 
apply (rule_tac x=x in bexI) 

884 
unfolding mem_Collect_eq 

885 
apply (auto split:split_if_asm) 

886 
done 

44647
e4de7750cdeb
modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents:
44531
diff
changeset

887 
have "continuous_on (UNIV  {0}) (\<lambda>x::'a. 1 / norm x)" 
e4de7750cdeb
modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents:
44531
diff
changeset

888 
unfolding field_divide_inverse by (simp add: continuous_on_intros) 
49654  889 
then show ?thesis unfolding * ** using path_connected_punctured_universe[OF assms] 
49653  890 
by (auto intro!: path_connected_continuous_image continuous_on_intros) 
37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

891 
qed 
36583  892 

37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

893 
lemma connected_sphere: "2 \<le> DIM('a::euclidean_space) \<Longrightarrow> connected {x::'a. norm(x  a) = r}" 
36583  894 
using path_connected_sphere path_connected_imp_connected by auto 
895 

896 
end 