|
1 section \<open>Neigbourhood bases and Locally path-connected spaces\<close> |
|
2 |
|
3 theory Locally |
|
4 imports |
|
5 Path_Connected Function_Topology |
|
6 begin |
|
7 |
|
8 subsection\<open>Neigbourhood bases (useful for "local" properties of various kinds)\<close> |
|
9 |
|
10 definition neighbourhood_base_at where |
|
11 "neighbourhood_base_at x P X \<equiv> |
|
12 \<forall>W. openin X W \<and> x \<in> W |
|
13 \<longrightarrow> (\<exists>U V. openin X U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W)" |
|
14 |
|
15 definition neighbourhood_base_of where |
|
16 "neighbourhood_base_of P X \<equiv> |
|
17 \<forall>x \<in> topspace X. neighbourhood_base_at x P X" |
|
18 |
|
19 lemma neighbourhood_base_of: |
|
20 "neighbourhood_base_of P X \<longleftrightarrow> |
|
21 (\<forall>W x. openin X W \<and> x \<in> W |
|
22 \<longrightarrow> (\<exists>U V. openin X U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W))" |
|
23 unfolding neighbourhood_base_at_def neighbourhood_base_of_def |
|
24 using openin_subset by blast |
|
25 |
|
26 lemma neighbourhood_base_at_mono: |
|
27 "\<lbrakk>neighbourhood_base_at x P X; \<And>S. \<lbrakk>P S; x \<in> S\<rbrakk> \<Longrightarrow> Q S\<rbrakk> \<Longrightarrow> neighbourhood_base_at x Q X" |
|
28 unfolding neighbourhood_base_at_def |
|
29 by (meson subset_eq) |
|
30 |
|
31 lemma neighbourhood_base_of_mono: |
|
32 "\<lbrakk>neighbourhood_base_of P X; \<And>S. P S \<Longrightarrow> Q S\<rbrakk> \<Longrightarrow> neighbourhood_base_of Q X" |
|
33 unfolding neighbourhood_base_of_def |
|
34 using neighbourhood_base_at_mono by force |
|
35 |
|
36 lemma open_neighbourhood_base_at: |
|
37 "(\<And>S. \<lbrakk>P S; x \<in> S\<rbrakk> \<Longrightarrow> openin X S) |
|
38 \<Longrightarrow> neighbourhood_base_at x P X \<longleftrightarrow> (\<forall>W. openin X W \<and> x \<in> W \<longrightarrow> (\<exists>U. P U \<and> x \<in> U \<and> U \<subseteq> W))" |
|
39 unfolding neighbourhood_base_at_def |
|
40 by (meson subsetD) |
|
41 |
|
42 lemma open_neighbourhood_base_of: |
|
43 "(\<forall>S. P S \<longrightarrow> openin X S) |
|
44 \<Longrightarrow> neighbourhood_base_of P X \<longleftrightarrow> (\<forall>W x. openin X W \<and> x \<in> W \<longrightarrow> (\<exists>U. P U \<and> x \<in> U \<and> U \<subseteq> W))" |
|
45 apply (simp add: neighbourhood_base_of, safe, blast) |
|
46 by meson |
|
47 |
|
48 lemma neighbourhood_base_of_open_subset: |
|
49 "\<lbrakk>neighbourhood_base_of P X; openin X S\<rbrakk> |
|
50 \<Longrightarrow> neighbourhood_base_of P (subtopology X S)" |
|
51 apply (clarsimp simp add: neighbourhood_base_of openin_subtopology_alt image_def) |
|
52 apply (rename_tac x V) |
|
53 apply (drule_tac x="S \<inter> V" in spec) |
|
54 apply (simp add: Int_ac) |
|
55 by (metis IntI le_infI1 openin_Int) |
|
56 |
|
57 lemma neighbourhood_base_of_topology_base: |
|
58 "openin X = arbitrary union_of (\<lambda>W. W \<in> \<B>) |
|
59 \<Longrightarrow> neighbourhood_base_of P X \<longleftrightarrow> |
|
60 (\<forall>W x. W \<in> \<B> \<and> x \<in> W \<longrightarrow> (\<exists>U V. openin X U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W))" |
|
61 apply (auto simp: openin_topology_base_unique neighbourhood_base_of) |
|
62 by (meson subset_trans) |
|
63 |
|
64 lemma neighbourhood_base_at_unlocalized: |
|
65 assumes "\<And>S T. \<lbrakk>P S; openin X T; x \<in> T; T \<subseteq> S\<rbrakk> \<Longrightarrow> P T" |
|
66 shows "neighbourhood_base_at x P X |
|
67 \<longleftrightarrow> (x \<in> topspace X \<longrightarrow> (\<exists>U V. openin X U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> topspace X))" |
|
68 (is "?lhs = ?rhs") |
|
69 proof |
|
70 assume R: ?rhs show ?lhs |
|
71 unfolding neighbourhood_base_at_def |
|
72 proof clarify |
|
73 fix W |
|
74 assume "openin X W" "x \<in> W" |
|
75 then have "x \<in> topspace X" |
|
76 using openin_subset by blast |
|
77 with R obtain U V where "openin X U" "P V" "x \<in> U" "U \<subseteq> V" "V \<subseteq> topspace X" |
|
78 by blast |
|
79 then show "\<exists>U V. openin X U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W" |
|
80 by (metis IntI \<open>openin X W\<close> \<open>x \<in> W\<close> assms inf_le1 inf_le2 openin_Int) |
|
81 qed |
|
82 qed (simp add: neighbourhood_base_at_def) |
|
83 |
|
84 lemma neighbourhood_base_at_with_subset: |
|
85 "\<lbrakk>openin X U; x \<in> U\<rbrakk> |
|
86 \<Longrightarrow> (neighbourhood_base_at x P X \<longleftrightarrow> neighbourhood_base_at x (\<lambda>T. T \<subseteq> U \<and> P T) X)" |
|
87 apply (simp add: neighbourhood_base_at_def) |
|
88 apply (metis IntI Int_subset_iff openin_Int) |
|
89 done |
|
90 |
|
91 lemma neighbourhood_base_of_with_subset: |
|
92 "neighbourhood_base_of P X \<longleftrightarrow> neighbourhood_base_of (\<lambda>t. t \<subseteq> topspace X \<and> P t) X" |
|
93 using neighbourhood_base_at_with_subset |
|
94 by (fastforce simp add: neighbourhood_base_of_def) |
|
95 |
|
96 subsection\<open>Locally path-connected spaces\<close> |
|
97 |
|
98 definition weakly_locally_path_connected_at |
|
99 where "weakly_locally_path_connected_at x X \<equiv> neighbourhood_base_at x (path_connectedin X) X" |
|
100 |
|
101 definition locally_path_connected_at |
|
102 where "locally_path_connected_at x X \<equiv> |
|
103 neighbourhood_base_at x (\<lambda>U. openin X U \<and> path_connectedin X U) X" |
|
104 |
|
105 definition locally_path_connected_space |
|
106 where "locally_path_connected_space X \<equiv> neighbourhood_base_of (path_connectedin X) X" |
|
107 |
|
108 lemma locally_path_connected_space_alt: |
|
109 "locally_path_connected_space X \<longleftrightarrow> neighbourhood_base_of (\<lambda>U. openin X U \<and> path_connectedin X U) X" |
|
110 (is "?P = ?Q") |
|
111 and locally_path_connected_space_eq_open_path_component_of: |
|
112 "locally_path_connected_space X \<longleftrightarrow> |
|
113 (\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> openin X (Collect (path_component_of (subtopology X U) x)))" |
|
114 (is "?P = ?R") |
|
115 proof - |
|
116 have ?P if ?Q |
|
117 using locally_path_connected_space_def neighbourhood_base_of_mono that by auto |
|
118 moreover have ?R if P: ?P |
|
119 proof - |
|
120 show ?thesis |
|
121 proof clarify |
|
122 fix U y |
|
123 assume "openin X U" "y \<in> U" |
|
124 have "\<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> Collect (path_component_of (subtopology X U) y)" |
|
125 if "path_component_of (subtopology X U) y x" for x |
|
126 |
|
127 proof - |
|
128 have "x \<in> U" |
|
129 using path_component_of_equiv that topspace_subtopology by fastforce |
|
130 then have "\<exists>Ua. openin X Ua \<and> (\<exists>V. path_connectedin X V \<and> x \<in> Ua \<and> Ua \<subseteq> V \<and> V \<subseteq> U)" |
|
131 using P |
|
132 by (simp add: \<open>openin X U\<close> locally_path_connected_space_def neighbourhood_base_of) |
|
133 then show ?thesis |
|
134 by (metis dual_order.trans path_component_of_equiv path_component_of_maximal path_connectedin_subtopology subset_iff that) |
|
135 qed |
|
136 then show "openin X (Collect (path_component_of (subtopology X U) y))" |
|
137 using openin_subopen by force |
|
138 qed |
|
139 qed |
|
140 moreover have ?Q if ?R |
|
141 using that |
|
142 apply (simp add: open_neighbourhood_base_of) |
|
143 by (metis mem_Collect_eq openin_subset path_component_of_refl path_connectedin_path_component_of path_connectedin_subtopology that topspace_subtopology_subset) |
|
144 ultimately show "?P = ?Q" "?P = ?R" |
|
145 by blast+ |
|
146 qed |
|
147 |
|
148 lemma locally_path_connected_space: |
|
149 "locally_path_connected_space X |
|
150 \<longleftrightarrow> (\<forall>V x. openin X V \<and> x \<in> V \<longrightarrow> (\<exists>U. openin X U \<and> path_connectedin X U \<and> x \<in> U \<and> U \<subseteq> V))" |
|
151 by (simp add: locally_path_connected_space_alt open_neighbourhood_base_of) |
|
152 |
|
153 lemma locally_path_connected_space_open_path_components: |
|
154 "locally_path_connected_space X \<longleftrightarrow> |
|
155 (\<forall>U c. openin X U \<and> c \<in> path_components_of(subtopology X U) \<longrightarrow> openin X c)" |
|
156 apply (auto simp: locally_path_connected_space_eq_open_path_component_of path_components_of_def topspace_subtopology) |
|
157 by (metis imageI inf.absorb_iff2 openin_closedin_eq) |
|
158 |
|
159 lemma openin_path_component_of_locally_path_connected_space: |
|
160 "locally_path_connected_space X \<Longrightarrow> openin X (Collect (path_component_of X x))" |
|
161 apply (auto simp: locally_path_connected_space_eq_open_path_component_of) |
|
162 by (metis openin_empty openin_topspace path_component_of_eq_empty subtopology_topspace) |
|
163 |
|
164 lemma openin_path_components_of_locally_path_connected_space: |
|
165 "\<lbrakk>locally_path_connected_space X; c \<in> path_components_of X\<rbrakk> \<Longrightarrow> openin X c" |
|
166 apply (auto simp: locally_path_connected_space_eq_open_path_component_of) |
|
167 by (metis (no_types, lifting) imageE openin_topspace path_components_of_def subtopology_topspace) |
|
168 |
|
169 lemma closedin_path_components_of_locally_path_connected_space: |
|
170 "\<lbrakk>locally_path_connected_space X; c \<in> path_components_of X\<rbrakk> \<Longrightarrow> closedin X c" |
|
171 by (simp add: closedin_def complement_path_components_of_Union openin_path_components_of_locally_path_connected_space openin_clauses(3) path_components_of_subset) |
|
172 |
|
173 lemma closedin_path_component_of_locally_path_connected_space: |
|
174 assumes "locally_path_connected_space X" |
|
175 shows "closedin X (Collect (path_component_of X x))" |
|
176 proof (cases "x \<in> topspace X") |
|
177 case True |
|
178 then show ?thesis |
|
179 by (simp add: assms closedin_path_components_of_locally_path_connected_space path_component_in_path_components_of) |
|
180 next |
|
181 case False |
|
182 then show ?thesis |
|
183 by (metis closedin_empty path_component_of_eq_empty) |
|
184 qed |
|
185 |
|
186 lemma weakly_locally_path_connected_at: |
|
187 "weakly_locally_path_connected_at x X \<longleftrightarrow> |
|
188 (\<forall>V. openin X V \<and> x \<in> V |
|
189 \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> U \<subseteq> V \<and> |
|
190 (\<forall>y \<in> U. \<exists>C. path_connectedin X C \<and> C \<subseteq> V \<and> x \<in> C \<and> y \<in> C)))" |
|
191 (is "?lhs = ?rhs") |
|
192 proof |
|
193 assume ?lhs then show ?rhs |
|
194 apply (simp add: weakly_locally_path_connected_at_def neighbourhood_base_at_def) |
|
195 by (meson order_trans subsetD) |
|
196 next |
|
197 have *: "\<exists>V. path_connectedin X V \<and> U \<subseteq> V \<and> V \<subseteq> W" |
|
198 if "(\<forall>y\<in>U. \<exists>C. path_connectedin X C \<and> C \<subseteq> W \<and> x \<in> C \<and> y \<in> C)" |
|
199 for W U |
|
200 proof (intro exI conjI) |
|
201 let ?V = "(Collect (path_component_of (subtopology X W) x))" |
|
202 show "path_connectedin X (Collect (path_component_of (subtopology X W) x))" |
|
203 by (meson path_connectedin_path_component_of path_connectedin_subtopology) |
|
204 show "U \<subseteq> ?V" |
|
205 by (auto simp: path_component_of path_connectedin_subtopology that) |
|
206 show "?V \<subseteq> W" |
|
207 by (meson path_connectedin_path_component_of path_connectedin_subtopology) |
|
208 qed |
|
209 assume ?rhs |
|
210 then show ?lhs |
|
211 unfolding weakly_locally_path_connected_at_def neighbourhood_base_at_def by (metis "*") |
|
212 qed |
|
213 |
|
214 lemma locally_path_connected_space_im_kleinen: |
|
215 "locally_path_connected_space X \<longleftrightarrow> |
|
216 (\<forall>V x. openin X V \<and> x \<in> V |
|
217 \<longrightarrow> (\<exists>U. openin X U \<and> |
|
218 x \<in> U \<and> U \<subseteq> V \<and> |
|
219 (\<forall>y \<in> U. \<exists>c. path_connectedin X c \<and> |
|
220 c \<subseteq> V \<and> x \<in> c \<and> y \<in> c)))" |
|
221 apply (simp add: locally_path_connected_space_def neighbourhood_base_of_def) |
|
222 apply (simp add: weakly_locally_path_connected_at flip: weakly_locally_path_connected_at_def) |
|
223 using openin_subset apply force |
|
224 done |
|
225 |
|
226 lemma locally_path_connected_space_open_subset: |
|
227 "\<lbrakk>locally_path_connected_space X; openin X s\<rbrakk> |
|
228 \<Longrightarrow> locally_path_connected_space (subtopology X s)" |
|
229 apply (simp add: locally_path_connected_space_def neighbourhood_base_of openin_open_subtopology path_connectedin_subtopology) |
|
230 by (meson order_trans) |
|
231 |
|
232 lemma locally_path_connected_space_quotient_map_image: |
|
233 assumes f: "quotient_map X Y f" and X: "locally_path_connected_space X" |
|
234 shows "locally_path_connected_space Y" |
|
235 unfolding locally_path_connected_space_open_path_components |
|
236 proof clarify |
|
237 fix V C |
|
238 assume V: "openin Y V" and c: "C \<in> path_components_of (subtopology Y V)" |
|
239 then have sub: "C \<subseteq> topspace Y" |
|
240 using path_connectedin_path_components_of path_connectedin_subset_topspace path_connectedin_subtopology by blast |
|
241 have "openin X {x \<in> topspace X. f x \<in> C}" |
|
242 proof (subst openin_subopen, clarify) |
|
243 fix x |
|
244 assume x: "x \<in> topspace X" and "f x \<in> C" |
|
245 let ?T = "Collect (path_component_of (subtopology X {z \<in> topspace X. f z \<in> V}) x)" |
|
246 show "\<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> {x \<in> topspace X. f x \<in> C}" |
|
247 proof (intro exI conjI) |
|
248 have "\<exists>U. openin X U \<and> ?T \<in> path_components_of (subtopology X U)" |
|
249 proof (intro exI conjI) |
|
250 show "openin X ({z \<in> topspace X. f z \<in> V})" |
|
251 using V f openin_subset quotient_map_def by fastforce |
|
252 show "Collect (path_component_of (subtopology X {z \<in> topspace X. f z \<in> V}) x) |
|
253 \<in> path_components_of (subtopology X {z \<in> topspace X. f z \<in> V})" |
|
254 by (metis (no_types, lifting) Int_iff \<open>f x \<in> C\<close> c mem_Collect_eq path_component_in_path_components_of path_components_of_subset topspace_subtopology topspace_subtopology_subset x) |
|
255 qed |
|
256 with X show "openin X ?T" |
|
257 using locally_path_connected_space_open_path_components by blast |
|
258 show x: "x \<in> ?T" |
|
259 using V \<open>f x \<in> C\<close> c openin_subset path_component_of_equiv path_components_of_subset topspace_subtopology topspace_subtopology_subset x |
|
260 by fastforce |
|
261 have "f ` ?T \<subseteq> C" |
|
262 proof (rule path_components_of_maximal) |
|
263 show "C \<in> path_components_of (subtopology Y V)" |
|
264 by (simp add: c) |
|
265 show "path_connectedin (subtopology Y V) (f ` ?T)" |
|
266 proof - |
|
267 have "quotient_map (subtopology X {a \<in> topspace X. f a \<in> V}) (subtopology Y V) f" |
|
268 by (simp add: V f quotient_map_restriction) |
|
269 then show ?thesis |
|
270 by (meson path_connectedin_continuous_map_image path_connectedin_path_component_of quotient_imp_continuous_map) |
|
271 qed |
|
272 show "\<not> disjnt C (f ` ?T)" |
|
273 by (metis (no_types, lifting) \<open>f x \<in> C\<close> x disjnt_iff image_eqI) |
|
274 qed |
|
275 then show "?T \<subseteq> {x \<in> topspace X. f x \<in> C}" |
|
276 by (force simp: path_component_of_equiv topspace_subtopology) |
|
277 qed |
|
278 qed |
|
279 then show "openin Y C" |
|
280 using f sub by (simp add: quotient_map_def) |
|
281 qed |
|
282 |
|
283 lemma homeomorphic_locally_path_connected_space: |
|
284 assumes "X homeomorphic_space Y" |
|
285 shows "locally_path_connected_space X \<longleftrightarrow> locally_path_connected_space Y" |
|
286 proof - |
|
287 obtain f g where "homeomorphic_maps X Y f g" |
|
288 using assms homeomorphic_space_def by fastforce |
|
289 then show ?thesis |
|
290 by (metis (no_types) homeomorphic_map_def homeomorphic_maps_map locally_path_connected_space_quotient_map_image) |
|
291 qed |
|
292 |
|
293 lemma locally_path_connected_space_retraction_map_image: |
|
294 "\<lbrakk>retraction_map X Y r; locally_path_connected_space X\<rbrakk> |
|
295 \<Longrightarrow> locally_path_connected_space Y" |
|
296 using Abstract_Topology.retraction_imp_quotient_map locally_path_connected_space_quotient_map_image by blast |
|
297 |
|
298 lemma locally_path_connected_space_euclideanreal: "locally_path_connected_space euclideanreal" |
|
299 unfolding locally_path_connected_space_def neighbourhood_base_of |
|
300 proof clarsimp |
|
301 fix W and x :: "real" |
|
302 assume "open W" "x \<in> W" |
|
303 then obtain e where "e > 0" and e: "\<And>x'. \<bar>x' - x\<bar> < e \<longrightarrow> x' \<in> W" |
|
304 by (auto simp: open_real) |
|
305 then show "\<exists>U. open U \<and> (\<exists>V. path_connected V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W)" |
|
306 by (force intro!: convex_imp_path_connected exI [where x = "{x-e<..<x+e}"]) |
|
307 qed |
|
308 |
|
309 lemma locally_path_connected_space_discrete_topology: |
|
310 "locally_path_connected_space (discrete_topology U)" |
|
311 using locally_path_connected_space_open_path_components by fastforce |
|
312 |
|
313 lemma path_component_eq_connected_component_of: |
|
314 assumes "locally_path_connected_space X" |
|
315 shows "(path_component_of_set X x = connected_component_of_set X x)" |
|
316 proof (cases "x \<in> topspace X") |
|
317 case True |
|
318 then show ?thesis |
|
319 using connectedin_connected_component_of [of X x] |
|
320 apply (clarsimp simp add: connectedin_def connected_space_clopen_in topspace_subtopology_subset cong: conj_cong) |
|
321 apply (drule_tac x="path_component_of_set X x" in spec) |
|
322 by (metis assms closedin_closed_subtopology closedin_connected_component_of closedin_path_component_of_locally_path_connected_space inf.absorb_iff2 inf.orderE openin_path_component_of_locally_path_connected_space openin_subtopology path_component_of_eq_empty path_component_subset_connected_component_of) |
|
323 next |
|
324 case False |
|
325 then show ?thesis |
|
326 using connected_component_of_eq_empty path_component_of_eq_empty by fastforce |
|
327 qed |
|
328 |
|
329 lemma path_components_eq_connected_components_of: |
|
330 "locally_path_connected_space X \<Longrightarrow> (path_components_of X = connected_components_of X)" |
|
331 by (simp add: path_components_of_def connected_components_of_def image_def path_component_eq_connected_component_of) |
|
332 |
|
333 lemma path_connected_eq_connected_space: |
|
334 "locally_path_connected_space X |
|
335 \<Longrightarrow> path_connected_space X \<longleftrightarrow> connected_space X" |
|
336 by (metis connected_components_of_subset_sing path_components_eq_connected_components_of path_components_of_subset_singleton) |
|
337 |
|
338 lemma locally_path_connected_space_product_topology: |
|
339 "locally_path_connected_space(product_topology X I) \<longleftrightarrow> |
|
340 topspace(product_topology X I) = {} \<or> |
|
341 finite {i. i \<in> I \<and> ~path_connected_space(X i)} \<and> |
|
342 (\<forall>i \<in> I. locally_path_connected_space(X i))" |
|
343 (is "?lhs \<longleftrightarrow> ?empty \<or> ?rhs") |
|
344 proof (cases ?empty) |
|
345 case True |
|
346 then show ?thesis |
|
347 by (simp add: locally_path_connected_space_def neighbourhood_base_of openin_closedin_eq) |
|
348 next |
|
349 case False |
|
350 then obtain z where z: "z \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))" |
|
351 by auto |
|
352 have ?rhs if L: ?lhs |
|
353 proof - |
|
354 obtain U C where U: "openin (product_topology X I) U" |
|
355 and V: "path_connectedin (product_topology X I) C" |
|
356 and "z \<in> U" "U \<subseteq> C" and Csub: "C \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (X i))" |
|
357 using L apply (clarsimp simp add: locally_path_connected_space_def neighbourhood_base_of) |
|
358 by (metis openin_topspace topspace_product_topology z) |
|
359 then obtain V where finV: "finite {i \<in> I. V i \<noteq> topspace (X i)}" |
|
360 and XV: "\<And>i. i\<in>I \<Longrightarrow> openin (X i) (V i)" and "z \<in> Pi\<^sub>E I V" and subU: "Pi\<^sub>E I V \<subseteq> U" |
|
361 by (force simp: openin_product_topology_alt) |
|
362 show ?thesis |
|
363 proof (intro conjI ballI) |
|
364 have "path_connected_space (X i)" if "i \<in> I" "V i = topspace (X i)" for i |
|
365 proof - |
|
366 have pc: "path_connectedin (X i) ((\<lambda>x. x i) ` C)" |
|
367 apply (rule path_connectedin_continuous_map_image [OF _ V]) |
|
368 by (simp add: continuous_map_product_projection \<open>i \<in> I\<close>) |
|
369 moreover have "((\<lambda>x. x i) ` C) = topspace (X i)" |
|
370 proof |
|
371 show "(\<lambda>x. x i) ` C \<subseteq> topspace (X i)" |
|
372 by (simp add: pc path_connectedin_subset_topspace) |
|
373 have "V i \<subseteq> (\<lambda>x. x i) ` (\<Pi>\<^sub>E i\<in>I. V i)" |
|
374 by (metis \<open>z \<in> Pi\<^sub>E I V\<close> empty_iff image_projection_PiE order_refl that(1)) |
|
375 also have "\<dots> \<subseteq> (\<lambda>x. x i) ` U" |
|
376 using subU by blast |
|
377 finally show "topspace (X i) \<subseteq> (\<lambda>x. x i) ` C" |
|
378 using \<open>U \<subseteq> C\<close> that by blast |
|
379 qed |
|
380 ultimately show ?thesis |
|
381 by (simp add: path_connectedin_topspace) |
|
382 qed |
|
383 then have "{i \<in> I. \<not> path_connected_space (X i)} \<subseteq> {i \<in> I. V i \<noteq> topspace (X i)}" |
|
384 by blast |
|
385 with finV show "finite {i \<in> I. \<not> path_connected_space (X i)}" |
|
386 using finite_subset by blast |
|
387 next |
|
388 show "locally_path_connected_space (X i)" if "i \<in> I" for i |
|
389 apply (rule locally_path_connected_space_quotient_map_image [OF _ L, where f = "\<lambda>x. x i"]) |
|
390 by (metis False Abstract_Topology.retraction_imp_quotient_map retraction_map_product_projection that) |
|
391 qed |
|
392 qed |
|
393 moreover have ?lhs if R: ?rhs |
|
394 proof (clarsimp simp add: locally_path_connected_space_def neighbourhood_base_of) |
|
395 fix F z |
|
396 assume "openin (product_topology X I) F" and "z \<in> F" |
|
397 then obtain W where finW: "finite {i \<in> I. W i \<noteq> topspace (X i)}" |
|
398 and opeW: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (W i)" and "z \<in> Pi\<^sub>E I W" "Pi\<^sub>E I W \<subseteq> F" |
|
399 by (auto simp: openin_product_topology_alt) |
|
400 have "\<forall>i \<in> I. \<exists>U C. openin (X i) U \<and> path_connectedin (X i) C \<and> z i \<in> U \<and> U \<subseteq> C \<and> C \<subseteq> W i \<and> |
|
401 (W i = topspace (X i) \<and> |
|
402 path_connected_space (X i) \<longrightarrow> U = topspace (X i) \<and> C = topspace (X i))" |
|
403 (is "\<forall>i \<in> I. ?\<Phi> i") |
|
404 proof |
|
405 fix i assume "i \<in> I" |
|
406 have "locally_path_connected_space (X i)" |
|
407 by (simp add: R \<open>i \<in> I\<close>) |
|
408 moreover have "openin (X i) (W i) " "z i \<in> W i" |
|
409 using \<open>z \<in> Pi\<^sub>E I W\<close> opeW \<open>i \<in> I\<close> by auto |
|
410 ultimately obtain U C where UC: "openin (X i) U" "path_connectedin (X i) C" "z i \<in> U" "U \<subseteq> C" "C \<subseteq> W i" |
|
411 using \<open>i \<in> I\<close> by (force simp: locally_path_connected_space_def neighbourhood_base_of) |
|
412 show "?\<Phi> i" |
|
413 proof (cases "W i = topspace (X i) \<and> path_connected_space(X i)") |
|
414 case True |
|
415 then show ?thesis |
|
416 using \<open>z i \<in> W i\<close> path_connectedin_topspace by blast |
|
417 next |
|
418 case False |
|
419 then show ?thesis |
|
420 by (meson UC) |
|
421 qed |
|
422 qed |
|
423 then obtain U C where |
|
424 *: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (U i) \<and> path_connectedin (X i) (C i) \<and> z i \<in> (U i) \<and> (U i) \<subseteq> (C i) \<and> (C i) \<subseteq> W i \<and> |
|
425 (W i = topspace (X i) \<and> path_connected_space (X i) |
|
426 \<longrightarrow> (U i) = topspace (X i) \<and> (C i) = topspace (X i))" |
|
427 by metis |
|
428 let ?A = "{i \<in> I. \<not> path_connected_space (X i)} \<union> {i \<in> I. W i \<noteq> topspace (X i)}" |
|
429 have "{i \<in> I. U i \<noteq> topspace (X i)} \<subseteq> ?A" |
|
430 by (clarsimp simp add: "*") |
|
431 moreover have "finite ?A" |
|
432 by (simp add: that finW) |
|
433 ultimately have "finite {i \<in> I. U i \<noteq> topspace (X i)}" |
|
434 using finite_subset by auto |
|
435 then have "openin (product_topology X I) (Pi\<^sub>E I U)" |
|
436 using * by (simp add: openin_PiE_gen) |
|
437 then show "\<exists>U. openin (product_topology X I) U \<and> |
|
438 (\<exists>V. path_connectedin (product_topology X I) V \<and> z \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> F)" |
|
439 apply (rule_tac x="PiE I U" in exI, simp) |
|
440 apply (rule_tac x="PiE I C" in exI) |
|
441 using \<open>z \<in> Pi\<^sub>E I W\<close> \<open>Pi\<^sub>E I W \<subseteq> F\<close> * |
|
442 apply (simp add: path_connectedin_PiE subset_PiE PiE_iff PiE_mono dual_order.trans) |
|
443 done |
|
444 qed |
|
445 ultimately show ?thesis |
|
446 using False by blast |
|
447 qed |
|
448 |
|
449 end |