69945
|
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
|