1077 have "continuous_on U (\<lambda>x. (x, One /\<^sub>R setdist {x} (- U)))" |
1077 have "continuous_on U (\<lambda>x. (x, One /\<^sub>R setdist {x} (- U)))" |
1078 apply (intro continuous_intros continuous_on_setdist) |
1078 apply (intro continuous_intros continuous_on_setdist) |
1079 by (simp add: Ucomp setdist_eq_0_sing_1) |
1079 by (simp add: Ucomp setdist_eq_0_sing_1) |
1080 then have homU: "homeomorphism U (f`U) f fst" |
1080 then have homU: "homeomorphism U (f`U) f fst" |
1081 by (auto simp: f_def homeomorphism_def image_iff continuous_intros) |
1081 by (auto simp: f_def homeomorphism_def image_iff continuous_intros) |
1082 have cloS: "closedin (subtopology euclidean U) S" |
1082 have cloS: "closedin (top_of_set U) S" |
1083 by (metis US closed_closure closedin_closed_Int) |
1083 by (metis US closed_closure closedin_closed_Int) |
1084 have cont: "isCont ((\<lambda>x. setdist {x} (- U)) o fst) z" for z :: "'a \<times> 'b" |
1084 have cont: "isCont ((\<lambda>x. setdist {x} (- U)) o fst) z" for z :: "'a \<times> 'b" |
1085 by (rule continuous_at_compose continuous_intros continuous_at_setdist)+ |
1085 by (rule continuous_at_compose continuous_intros continuous_at_setdist)+ |
1086 have setdist1D: "setdist {a} (- U) *\<^sub>R b = One \<Longrightarrow> setdist {a} (- U) \<noteq> 0" for a::'a and b::'b |
1086 have setdist1D: "setdist {a} (- U) *\<^sub>R b = One \<Longrightarrow> setdist {a} (- U) \<noteq> 0" for a::'a and b::'b |
1087 by force |
1087 by force |
1273 definition%important covering_space |
1273 definition%important covering_space |
1274 :: "'a::topological_space set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b::topological_space set \<Rightarrow> bool" |
1274 :: "'a::topological_space set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b::topological_space set \<Rightarrow> bool" |
1275 where |
1275 where |
1276 "covering_space c p S \<equiv> |
1276 "covering_space c p S \<equiv> |
1277 continuous_on c p \<and> p ` c = S \<and> |
1277 continuous_on c p \<and> p ` c = S \<and> |
1278 (\<forall>x \<in> S. \<exists>T. x \<in> T \<and> openin (subtopology euclidean S) T \<and> |
1278 (\<forall>x \<in> S. \<exists>T. x \<in> T \<and> openin (top_of_set S) T \<and> |
1279 (\<exists>v. \<Union>v = c \<inter> p -` T \<and> |
1279 (\<exists>v. \<Union>v = c \<inter> p -` T \<and> |
1280 (\<forall>u \<in> v. openin (subtopology euclidean c) u) \<and> |
1280 (\<forall>u \<in> v. openin (top_of_set c) u) \<and> |
1281 pairwise disjnt v \<and> |
1281 pairwise disjnt v \<and> |
1282 (\<forall>u \<in> v. \<exists>q. homeomorphism u T p q)))" |
1282 (\<forall>u \<in> v. \<exists>q. homeomorphism u T p q)))" |
1283 |
1283 |
1284 lemma covering_space_imp_continuous: "covering_space c p S \<Longrightarrow> continuous_on c p" |
1284 lemma covering_space_imp_continuous: "covering_space c p S \<Longrightarrow> continuous_on c p" |
1285 by (simp add: covering_space_def) |
1285 by (simp add: covering_space_def) |
1293 apply (rule_tac x="{S}" in exI, auto) |
1293 apply (rule_tac x="{S}" in exI, auto) |
1294 done |
1294 done |
1295 |
1295 |
1296 lemma covering_space_local_homeomorphism: |
1296 lemma covering_space_local_homeomorphism: |
1297 assumes "covering_space c p S" "x \<in> c" |
1297 assumes "covering_space c p S" "x \<in> c" |
1298 obtains T u q where "x \<in> T" "openin (subtopology euclidean c) T" |
1298 obtains T u q where "x \<in> T" "openin (top_of_set c) T" |
1299 "p x \<in> u" "openin (subtopology euclidean S) u" |
1299 "p x \<in> u" "openin (top_of_set S) u" |
1300 "homeomorphism T u p q" |
1300 "homeomorphism T u p q" |
1301 using assms |
1301 using assms |
1302 apply (simp add: covering_space_def, clarify) |
1302 apply (simp add: covering_space_def, clarify) |
1303 apply (drule_tac x="p x" in bspec, force) |
1303 apply (drule_tac x="p x" in bspec, force) |
1304 by (metis IntI UnionE vimage_eq) |
1304 by (metis IntI UnionE vimage_eq) |
1305 |
1305 |
1306 |
1306 |
1307 lemma covering_space_local_homeomorphism_alt: |
1307 lemma covering_space_local_homeomorphism_alt: |
1308 assumes p: "covering_space c p S" and "y \<in> S" |
1308 assumes p: "covering_space c p S" and "y \<in> S" |
1309 obtains x T U q where "p x = y" |
1309 obtains x T U q where "p x = y" |
1310 "x \<in> T" "openin (subtopology euclidean c) T" |
1310 "x \<in> T" "openin (top_of_set c) T" |
1311 "y \<in> U" "openin (subtopology euclidean S) U" |
1311 "y \<in> U" "openin (top_of_set S) U" |
1312 "homeomorphism T U p q" |
1312 "homeomorphism T U p q" |
1313 proof - |
1313 proof - |
1314 obtain x where "p x = y" "x \<in> c" |
1314 obtain x where "p x = y" "x \<in> c" |
1315 using assms covering_space_imp_surjective by blast |
1315 using assms covering_space_imp_surjective by blast |
1316 show ?thesis |
1316 show ?thesis |
1318 using that \<open>p x = y\<close> by blast |
1318 using that \<open>p x = y\<close> by blast |
1319 qed |
1319 qed |
1320 |
1320 |
1321 proposition covering_space_open_map: |
1321 proposition covering_space_open_map: |
1322 fixes S :: "'a :: metric_space set" and T :: "'b :: metric_space set" |
1322 fixes S :: "'a :: metric_space set" and T :: "'b :: metric_space set" |
1323 assumes p: "covering_space c p S" and T: "openin (subtopology euclidean c) T" |
1323 assumes p: "covering_space c p S" and T: "openin (top_of_set c) T" |
1324 shows "openin (subtopology euclidean S) (p ` T)" |
1324 shows "openin (top_of_set S) (p ` T)" |
1325 proof - |
1325 proof - |
1326 have pce: "p ` c = S" |
1326 have pce: "p ` c = S" |
1327 and covs: |
1327 and covs: |
1328 "\<And>x. x \<in> S \<Longrightarrow> |
1328 "\<And>x. x \<in> S \<Longrightarrow> |
1329 \<exists>X VS. x \<in> X \<and> openin (subtopology euclidean S) X \<and> |
1329 \<exists>X VS. x \<in> X \<and> openin (top_of_set S) X \<and> |
1330 \<Union>VS = c \<inter> p -` X \<and> |
1330 \<Union>VS = c \<inter> p -` X \<and> |
1331 (\<forall>u \<in> VS. openin (subtopology euclidean c) u) \<and> |
1331 (\<forall>u \<in> VS. openin (top_of_set c) u) \<and> |
1332 pairwise disjnt VS \<and> |
1332 pairwise disjnt VS \<and> |
1333 (\<forall>u \<in> VS. \<exists>q. homeomorphism u X p q)" |
1333 (\<forall>u \<in> VS. \<exists>q. homeomorphism u X p q)" |
1334 using p by (auto simp: covering_space_def) |
1334 using p by (auto simp: covering_space_def) |
1335 have "T \<subseteq> c" by (metis openin_euclidean_subtopology_iff T) |
1335 have "T \<subseteq> c" by (metis openin_euclidean_subtopology_iff T) |
1336 have "\<exists>X. openin (subtopology euclidean S) X \<and> y \<in> X \<and> X \<subseteq> p ` T" |
1336 have "\<exists>X. openin (top_of_set S) X \<and> y \<in> X \<and> X \<subseteq> p ` T" |
1337 if "y \<in> p ` T" for y |
1337 if "y \<in> p ` T" for y |
1338 proof - |
1338 proof - |
1339 have "y \<in> S" using \<open>T \<subseteq> c\<close> pce that by blast |
1339 have "y \<in> S" using \<open>T \<subseteq> c\<close> pce that by blast |
1340 obtain U VS where "y \<in> U" and U: "openin (subtopology euclidean S) U" |
1340 obtain U VS where "y \<in> U" and U: "openin (top_of_set S) U" |
1341 and VS: "\<Union>VS = c \<inter> p -` U" |
1341 and VS: "\<Union>VS = c \<inter> p -` U" |
1342 and openVS: "\<forall>V \<in> VS. openin (subtopology euclidean c) V" |
1342 and openVS: "\<forall>V \<in> VS. openin (top_of_set c) V" |
1343 and homVS: "\<And>V. V \<in> VS \<Longrightarrow> \<exists>q. homeomorphism V U p q" |
1343 and homVS: "\<And>V. V \<in> VS \<Longrightarrow> \<exists>q. homeomorphism V U p q" |
1344 using covs [OF \<open>y \<in> S\<close>] by auto |
1344 using covs [OF \<open>y \<in> S\<close>] by auto |
1345 obtain x where "x \<in> c" "p x \<in> U" "x \<in> T" "p x = y" |
1345 obtain x where "x \<in> c" "p x \<in> U" "x \<in> T" "p x = y" |
1346 apply simp |
1346 apply simp |
1347 using T [unfolded openin_euclidean_subtopology_iff] \<open>y \<in> U\<close> \<open>y \<in> p ` T\<close> by blast |
1347 using T [unfolded openin_euclidean_subtopology_iff] \<open>y \<in> U\<close> \<open>y \<in> p ` T\<close> by blast |
1348 with VS obtain V where "x \<in> V" "V \<in> VS" by auto |
1348 with VS obtain V where "x \<in> V" "V \<in> VS" by auto |
1349 then obtain q where q: "homeomorphism V U p q" using homVS by blast |
1349 then obtain q where q: "homeomorphism V U p q" using homVS by blast |
1350 then have ptV: "p ` (T \<inter> V) = U \<inter> q -` (T \<inter> V)" |
1350 then have ptV: "p ` (T \<inter> V) = U \<inter> q -` (T \<inter> V)" |
1351 using VS \<open>V \<in> VS\<close> by (auto simp: homeomorphism_def) |
1351 using VS \<open>V \<in> VS\<close> by (auto simp: homeomorphism_def) |
1352 have ocv: "openin (subtopology euclidean c) V" |
1352 have ocv: "openin (top_of_set c) V" |
1353 by (simp add: \<open>V \<in> VS\<close> openVS) |
1353 by (simp add: \<open>V \<in> VS\<close> openVS) |
1354 have "openin (subtopology euclidean U) (U \<inter> q -` (T \<inter> V))" |
1354 have "openin (top_of_set U) (U \<inter> q -` (T \<inter> V))" |
1355 apply (rule continuous_on_open [THEN iffD1, rule_format]) |
1355 apply (rule continuous_on_open [THEN iffD1, rule_format]) |
1356 using homeomorphism_def q apply blast |
1356 using homeomorphism_def q apply blast |
1357 using openin_subtopology_Int_subset [of c] q T unfolding homeomorphism_def |
1357 using openin_subtopology_Int_subset [of c] q T unfolding homeomorphism_def |
1358 by (metis inf.absorb_iff2 Int_commute ocv openin_euclidean_subtopology_iff) |
1358 by (metis inf.absorb_iff2 Int_commute ocv openin_euclidean_subtopology_iff) |
1359 then have os: "openin (subtopology euclidean S) (U \<inter> q -` (T \<inter> V))" |
1359 then have os: "openin (top_of_set S) (U \<inter> q -` (T \<inter> V))" |
1360 using openin_trans [of U] by (simp add: Collect_conj_eq U) |
1360 using openin_trans [of U] by (simp add: Collect_conj_eq U) |
1361 show ?thesis |
1361 show ?thesis |
1362 apply (rule_tac x = "p ` (T \<inter> V)" in exI) |
1362 apply (rule_tac x = "p ` (T \<inter> V)" in exI) |
1363 apply (rule conjI) |
1363 apply (rule conjI) |
1364 apply (simp only: ptV os) |
1364 apply (simp only: ptV os) |
1384 have "U \<subseteq> T" by (rule in_components_subset [OF u_compt]) |
1384 have "U \<subseteq> T" by (rule in_components_subset [OF u_compt]) |
1385 define G12 where "G12 \<equiv> {x \<in> U. g1 x - g2 x = 0}" |
1385 define G12 where "G12 \<equiv> {x \<in> U. g1 x - g2 x = 0}" |
1386 have "connected U" by (rule in_components_connected [OF u_compt]) |
1386 have "connected U" by (rule in_components_connected [OF u_compt]) |
1387 have contu: "continuous_on U g1" "continuous_on U g2" |
1387 have contu: "continuous_on U g1" "continuous_on U g2" |
1388 using \<open>U \<subseteq> T\<close> continuous_on_subset g1 g2 by blast+ |
1388 using \<open>U \<subseteq> T\<close> continuous_on_subset g1 g2 by blast+ |
1389 have o12: "openin (subtopology euclidean U) G12" |
1389 have o12: "openin (top_of_set U) G12" |
1390 unfolding G12_def |
1390 unfolding G12_def |
1391 proof (subst openin_subopen, clarify) |
1391 proof (subst openin_subopen, clarify) |
1392 fix z |
1392 fix z |
1393 assume z: "z \<in> U" "g1 z - g2 z = 0" |
1393 assume z: "z \<in> U" "g1 z - g2 z = 0" |
1394 obtain v w q where "g1 z \<in> v" and ocv: "openin (subtopology euclidean c) v" |
1394 obtain v w q where "g1 z \<in> v" and ocv: "openin (top_of_set c) v" |
1395 and "p (g1 z) \<in> w" and osw: "openin (subtopology euclidean S) w" |
1395 and "p (g1 z) \<in> w" and osw: "openin (top_of_set S) w" |
1396 and hom: "homeomorphism v w p q" |
1396 and hom: "homeomorphism v w p q" |
1397 apply (rule_tac x = "g1 z" in covering_space_local_homeomorphism [OF cov]) |
1397 apply (rule_tac x = "g1 z" in covering_space_local_homeomorphism [OF cov]) |
1398 using \<open>U \<subseteq> T\<close> \<open>z \<in> U\<close> g1(2) apply blast+ |
1398 using \<open>U \<subseteq> T\<close> \<open>z \<in> U\<close> g1(2) apply blast+ |
1399 done |
1399 done |
1400 have "g2 z \<in> v" using \<open>g1 z \<in> v\<close> z by auto |
1400 have "g2 z \<in> v" using \<open>g1 z \<in> v\<close> z by auto |
1401 have gg: "U \<inter> g -` v = U \<inter> g -` (v \<inter> g ` U)" for g |
1401 have gg: "U \<inter> g -` v = U \<inter> g -` (v \<inter> g ` U)" for g |
1402 by auto |
1402 by auto |
1403 have "openin (subtopology euclidean (g1 ` U)) (v \<inter> g1 ` U)" |
1403 have "openin (top_of_set (g1 ` U)) (v \<inter> g1 ` U)" |
1404 using ocv \<open>U \<subseteq> T\<close> g1 by (fastforce simp add: openin_open) |
1404 using ocv \<open>U \<subseteq> T\<close> g1 by (fastforce simp add: openin_open) |
1405 then have 1: "openin (subtopology euclidean U) (U \<inter> g1 -` v)" |
1405 then have 1: "openin (top_of_set U) (U \<inter> g1 -` v)" |
1406 unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format]) |
1406 unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format]) |
1407 have "openin (subtopology euclidean (g2 ` U)) (v \<inter> g2 ` U)" |
1407 have "openin (top_of_set (g2 ` U)) (v \<inter> g2 ` U)" |
1408 using ocv \<open>U \<subseteq> T\<close> g2 by (fastforce simp add: openin_open) |
1408 using ocv \<open>U \<subseteq> T\<close> g2 by (fastforce simp add: openin_open) |
1409 then have 2: "openin (subtopology euclidean U) (U \<inter> g2 -` v)" |
1409 then have 2: "openin (top_of_set U) (U \<inter> g2 -` v)" |
1410 unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format]) |
1410 unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format]) |
1411 show "\<exists>T. openin (subtopology euclidean U) T \<and> z \<in> T \<and> T \<subseteq> {z \<in> U. g1 z - g2 z = 0}" |
1411 show "\<exists>T. openin (top_of_set U) T \<and> z \<in> T \<and> T \<subseteq> {z \<in> U. g1 z - g2 z = 0}" |
1412 using z |
1412 using z |
1413 apply (rule_tac x = "(U \<inter> g1 -` v) \<inter> (U \<inter> g2 -` v)" in exI) |
1413 apply (rule_tac x = "(U \<inter> g1 -` v) \<inter> (U \<inter> g2 -` v)" in exI) |
1414 apply (intro conjI) |
1414 apply (intro conjI) |
1415 apply (rule openin_Int [OF 1 2]) |
1415 apply (rule openin_Int [OF 1 2]) |
1416 using \<open>g1 z \<in> v\<close> \<open>g2 z \<in> v\<close> apply (force simp:, clarify) |
1416 using \<open>g1 z \<in> v\<close> \<open>g2 z \<in> v\<close> apply (force simp:, clarify) |
1417 apply (metis \<open>U \<subseteq> T\<close> subsetD eq_iff_diff_eq_0 fg1 fg2 hom homeomorphism_def) |
1417 apply (metis \<open>U \<subseteq> T\<close> subsetD eq_iff_diff_eq_0 fg1 fg2 hom homeomorphism_def) |
1418 done |
1418 done |
1419 qed |
1419 qed |
1420 have c12: "closedin (subtopology euclidean U) G12" |
1420 have c12: "closedin (top_of_set U) G12" |
1421 unfolding G12_def |
1421 unfolding G12_def |
1422 by (intro continuous_intros continuous_closedin_preimage_constant contu) |
1422 by (intro continuous_intros continuous_closedin_preimage_constant contu) |
1423 have "G12 = {} \<or> G12 = U" |
1423 have "G12 = {} \<or> G12 = U" |
1424 by (intro connected_clopen [THEN iffD1, rule_format] \<open>connected U\<close> conjI o12 c12) |
1424 by (intro connected_clopen [THEN iffD1, rule_format] \<open>connected U\<close> conjI o12 c12) |
1425 with eq \<open>a \<in> U\<close> have "\<And>x. x \<in> U \<Longrightarrow> g1 x - g2 x = 0" by (auto simp: G12_def) |
1425 with eq \<open>a \<in> U\<close> have "\<And>x. x \<in> U \<Longrightarrow> g1 x - g2 x = 0" by (auto simp: G12_def) |
1466 proof |
1466 proof |
1467 assume L: ?lhs |
1467 assume L: ?lhs |
1468 show ?rhs |
1468 show ?rhs |
1469 proof (rule locallyI) |
1469 proof (rule locallyI) |
1470 fix V x |
1470 fix V x |
1471 assume V: "openin (subtopology euclidean C) V" and "x \<in> V" |
1471 assume V: "openin (top_of_set C) V" and "x \<in> V" |
1472 have "p x \<in> p ` C" |
1472 have "p x \<in> p ` C" |
1473 by (metis IntE V \<open>x \<in> V\<close> imageI openin_open) |
1473 by (metis IntE V \<open>x \<in> V\<close> imageI openin_open) |
1474 then obtain T \<V> where "p x \<in> T" |
1474 then obtain T \<V> where "p x \<in> T" |
1475 and opeT: "openin (subtopology euclidean S) T" |
1475 and opeT: "openin (top_of_set S) T" |
1476 and veq: "\<Union>\<V> = C \<inter> p -` T" |
1476 and veq: "\<Union>\<V> = C \<inter> p -` T" |
1477 and ope: "\<forall>U\<in>\<V>. openin (subtopology euclidean C) U" |
1477 and ope: "\<forall>U\<in>\<V>. openin (top_of_set C) U" |
1478 and hom: "\<forall>U\<in>\<V>. \<exists>q. homeomorphism U T p q" |
1478 and hom: "\<forall>U\<in>\<V>. \<exists>q. homeomorphism U T p q" |
1479 using cov unfolding covering_space_def by (blast intro: that) |
1479 using cov unfolding covering_space_def by (blast intro: that) |
1480 have "x \<in> \<Union>\<V>" |
1480 have "x \<in> \<Union>\<V>" |
1481 using V veq \<open>p x \<in> T\<close> \<open>x \<in> V\<close> openin_imp_subset by fastforce |
1481 using V veq \<open>p x \<in> T\<close> \<open>x \<in> V\<close> openin_imp_subset by fastforce |
1482 then obtain U where "x \<in> U" "U \<in> \<V>" |
1482 then obtain U where "x \<in> U" "U \<in> \<V>" |
1483 by blast |
1483 by blast |
1484 then obtain q where opeU: "openin (subtopology euclidean C) U" and q: "homeomorphism U T p q" |
1484 then obtain q where opeU: "openin (top_of_set C) U" and q: "homeomorphism U T p q" |
1485 using ope hom by blast |
1485 using ope hom by blast |
1486 with V have "openin (subtopology euclidean C) (U \<inter> V)" |
1486 with V have "openin (top_of_set C) (U \<inter> V)" |
1487 by blast |
1487 by blast |
1488 then have UV: "openin (subtopology euclidean S) (p ` (U \<inter> V))" |
1488 then have UV: "openin (top_of_set S) (p ` (U \<inter> V))" |
1489 using cov covering_space_open_map by blast |
1489 using cov covering_space_open_map by blast |
1490 obtain W W' where opeW: "openin (subtopology euclidean S) W" and "\<psi> W'" "p x \<in> W" "W \<subseteq> W'" and W'sub: "W' \<subseteq> p ` (U \<inter> V)" |
1490 obtain W W' where opeW: "openin (top_of_set S) W" and "\<psi> W'" "p x \<in> W" "W \<subseteq> W'" and W'sub: "W' \<subseteq> p ` (U \<inter> V)" |
1491 using locallyE [OF L UV] \<open>x \<in> U\<close> \<open>x \<in> V\<close> by blast |
1491 using locallyE [OF L UV] \<open>x \<in> U\<close> \<open>x \<in> V\<close> by blast |
1492 then have "W \<subseteq> T" |
1492 then have "W \<subseteq> T" |
1493 by (metis Int_lower1 q homeomorphism_image1 image_Int_subset order_trans) |
1493 by (metis Int_lower1 q homeomorphism_image1 image_Int_subset order_trans) |
1494 show "\<exists>U Z. openin (subtopology euclidean C) U \<and> |
1494 show "\<exists>U Z. openin (top_of_set C) U \<and> |
1495 \<phi> Z \<and> x \<in> U \<and> U \<subseteq> Z \<and> Z \<subseteq> V" |
1495 \<phi> Z \<and> x \<in> U \<and> U \<subseteq> Z \<and> Z \<subseteq> V" |
1496 proof (intro exI conjI) |
1496 proof (intro exI conjI) |
1497 have "openin (subtopology euclidean T) W" |
1497 have "openin (top_of_set T) W" |
1498 by (meson opeW opeT openin_imp_subset openin_subset_trans \<open>W \<subseteq> T\<close>) |
1498 by (meson opeW opeT openin_imp_subset openin_subset_trans \<open>W \<subseteq> T\<close>) |
1499 then have "openin (subtopology euclidean U) (q ` W)" |
1499 then have "openin (top_of_set U) (q ` W)" |
1500 by (meson homeomorphism_imp_open_map homeomorphism_symD q) |
1500 by (meson homeomorphism_imp_open_map homeomorphism_symD q) |
1501 then show "openin (subtopology euclidean C) (q ` W)" |
1501 then show "openin (top_of_set C) (q ` W)" |
1502 using opeU openin_trans by blast |
1502 using opeU openin_trans by blast |
1503 show "\<phi> (q ` W')" |
1503 show "\<phi> (q ` W')" |
1504 by (metis (mono_tags, lifting) Int_subset_iff UV W'sub \<open>\<psi> W'\<close> continuous_on_subset dual_order.trans homeomorphism_def image_Int_subset openin_imp_subset q qim) |
1504 by (metis (mono_tags, lifting) Int_subset_iff UV W'sub \<open>\<psi> W'\<close> continuous_on_subset dual_order.trans homeomorphism_def image_Int_subset openin_imp_subset q qim) |
1505 show "x \<in> q ` W" |
1505 show "x \<in> q ` W" |
1506 by (metis \<open>p x \<in> W\<close> \<open>x \<in> U\<close> homeomorphism_def imageI q) |
1506 by (metis \<open>p x \<in> W\<close> \<open>x \<in> U\<close> homeomorphism_def imageI q) |
1573 obtains k where "continuous_on ({0..1} \<times> U) k" |
1573 obtains k where "continuous_on ({0..1} \<times> U) k" |
1574 "k ` ({0..1} \<times> U) \<subseteq> C" |
1574 "k ` ({0..1} \<times> U) \<subseteq> C" |
1575 "\<And>y. y \<in> U \<Longrightarrow> k(0, y) = f y" |
1575 "\<And>y. y \<in> U \<Longrightarrow> k(0, y) = f y" |
1576 "\<And>z. z \<in> {0..1} \<times> U \<Longrightarrow> h z = p(k z)" |
1576 "\<And>z. z \<in> {0..1} \<times> U \<Longrightarrow> h z = p(k z)" |
1577 proof - |
1577 proof - |
1578 have "\<exists>V k. openin (subtopology euclidean U) V \<and> y \<in> V \<and> |
1578 have "\<exists>V k. openin (top_of_set U) V \<and> y \<in> V \<and> |
1579 continuous_on ({0..1} \<times> V) k \<and> k ` ({0..1} \<times> V) \<subseteq> C \<and> |
1579 continuous_on ({0..1} \<times> V) k \<and> k ` ({0..1} \<times> V) \<subseteq> C \<and> |
1580 (\<forall>z \<in> V. k(0, z) = f z) \<and> (\<forall>z \<in> {0..1} \<times> V. h z = p(k z))" |
1580 (\<forall>z \<in> V. k(0, z) = f z) \<and> (\<forall>z \<in> {0..1} \<times> V. h z = p(k z))" |
1581 if "y \<in> U" for y |
1581 if "y \<in> U" for y |
1582 proof - |
1582 proof - |
1583 obtain UU where UU: "\<And>s. s \<in> S \<Longrightarrow> s \<in> (UU s) \<and> openin (subtopology euclidean S) (UU s) \<and> |
1583 obtain UU where UU: "\<And>s. s \<in> S \<Longrightarrow> s \<in> (UU s) \<and> openin (top_of_set S) (UU s) \<and> |
1584 (\<exists>\<V>. \<Union>\<V> = C \<inter> p -` UU s \<and> |
1584 (\<exists>\<V>. \<Union>\<V> = C \<inter> p -` UU s \<and> |
1585 (\<forall>U \<in> \<V>. openin (subtopology euclidean C) U) \<and> |
1585 (\<forall>U \<in> \<V>. openin (top_of_set C) U) \<and> |
1586 pairwise disjnt \<V> \<and> |
1586 pairwise disjnt \<V> \<and> |
1587 (\<forall>U \<in> \<V>. \<exists>q. homeomorphism U (UU s) p q))" |
1587 (\<forall>U \<in> \<V>. \<exists>q. homeomorphism U (UU s) p q))" |
1588 using cov unfolding covering_space_def by (metis (mono_tags)) |
1588 using cov unfolding covering_space_def by (metis (mono_tags)) |
1589 then have ope: "\<And>s. s \<in> S \<Longrightarrow> s \<in> (UU s) \<and> openin (subtopology euclidean S) (UU s)" |
1589 then have ope: "\<And>s. s \<in> S \<Longrightarrow> s \<in> (UU s) \<and> openin (top_of_set S) (UU s)" |
1590 by blast |
1590 by blast |
1591 have "\<exists>k n i. open k \<and> open n \<and> |
1591 have "\<exists>k n i. open k \<and> open n \<and> |
1592 t \<in> k \<and> y \<in> n \<and> i \<in> S \<and> h ` (({0..1} \<inter> k) \<times> (U \<inter> n)) \<subseteq> UU i" if "t \<in> {0..1}" for t |
1592 t \<in> k \<and> y \<in> n \<and> i \<in> S \<and> h ` (({0..1} \<inter> k) \<times> (U \<inter> n)) \<subseteq> UU i" if "t \<in> {0..1}" for t |
1593 proof - |
1593 proof - |
1594 have hinS: "h (t, y) \<in> S" |
1594 have hinS: "h (t, y) \<in> S" |
1595 using \<open>y \<in> U\<close> him that by blast |
1595 using \<open>y \<in> U\<close> him that by blast |
1596 then have "(t,y) \<in> ({0..1} \<times> U) \<inter> h -` UU(h(t, y))" |
1596 then have "(t,y) \<in> ({0..1} \<times> U) \<inter> h -` UU(h(t, y))" |
1597 using \<open>y \<in> U\<close> \<open>t \<in> {0..1}\<close> by (auto simp: ope) |
1597 using \<open>y \<in> U\<close> \<open>t \<in> {0..1}\<close> by (auto simp: ope) |
1598 moreover have ope_01U: "openin (subtopology euclidean ({0..1} \<times> U)) (({0..1} \<times> U) \<inter> h -` UU(h(t, y)))" |
1598 moreover have ope_01U: "openin (top_of_set ({0..1} \<times> U)) (({0..1} \<times> U) \<inter> h -` UU(h(t, y)))" |
1599 using hinS ope continuous_on_open_gen [OF him] conth by blast |
1599 using hinS ope continuous_on_open_gen [OF him] conth by blast |
1600 ultimately obtain V W where opeV: "open V" and "t \<in> {0..1} \<inter> V" "t \<in> {0..1} \<inter> V" |
1600 ultimately obtain V W where opeV: "open V" and "t \<in> {0..1} \<inter> V" "t \<in> {0..1} \<inter> V" |
1601 and opeW: "open W" and "y \<in> U" "y \<in> W" |
1601 and opeW: "open W" and "y \<in> U" "y \<in> W" |
1602 and VW: "({0..1} \<inter> V) \<times> (U \<inter> W) \<subseteq> (({0..1} \<times> U) \<inter> h -` UU(h(t, y)))" |
1602 and VW: "({0..1} \<inter> V) \<times> (U \<inter> W) \<subseteq> (({0..1} \<times> U) \<inter> h -` UU(h(t, y)))" |
1603 by (rule Times_in_interior_subtopology) (auto simp: openin_open) |
1603 by (rule Times_in_interior_subtopology) (auto simp: openin_open) |
1639 qed auto |
1639 qed auto |
1640 obtain N::nat where N: "N > 1 / \<delta>" |
1640 obtain N::nat where N: "N > 1 / \<delta>" |
1641 using reals_Archimedean2 by blast |
1641 using reals_Archimedean2 by blast |
1642 then have "N > 0" |
1642 then have "N > 0" |
1643 using \<open>0 < \<delta>\<close> order.asym by force |
1643 using \<open>0 < \<delta>\<close> order.asym by force |
1644 have *: "\<exists>V k. openin (subtopology euclidean U) V \<and> y \<in> V \<and> |
1644 have *: "\<exists>V k. openin (top_of_set U) V \<and> y \<in> V \<and> |
1645 continuous_on ({0..of_nat n / N} \<times> V) k \<and> |
1645 continuous_on ({0..of_nat n / N} \<times> V) k \<and> |
1646 k ` ({0..of_nat n / N} \<times> V) \<subseteq> C \<and> |
1646 k ` ({0..of_nat n / N} \<times> V) \<subseteq> C \<and> |
1647 (\<forall>z\<in>V. k (0, z) = f z) \<and> |
1647 (\<forall>z\<in>V. k (0, z) = f z) \<and> |
1648 (\<forall>z\<in>{0..of_nat n / N} \<times> V. h z = p (k z))" if "n \<le> N" for n |
1648 (\<forall>z\<in>{0..of_nat n / N} \<times> V. h z = p (k z))" if "n \<le> N" for n |
1649 using that |
1649 using that |
1674 using \<open>0 < \<delta>\<close> N by (auto simp: divide_simps algebra_simps) |
1674 using \<open>0 < \<delta>\<close> N by (auto simp: divide_simps algebra_simps) |
1675 qed blast |
1675 qed blast |
1676 have t01: "t \<in> {0..1}" |
1676 have t01: "t \<in> {0..1}" |
1677 using \<open>t \<in> tk\<close> \<open>tk \<subseteq> {0..1}\<close> by blast |
1677 using \<open>t \<in> tk\<close> \<open>tk \<subseteq> {0..1}\<close> by blast |
1678 obtain \<V> where \<V>: "\<Union>\<V> = C \<inter> p -` UU (X t)" |
1678 obtain \<V> where \<V>: "\<Union>\<V> = C \<inter> p -` UU (X t)" |
1679 and opeC: "\<And>U. U \<in> \<V> \<Longrightarrow> openin (subtopology euclidean C) U" |
1679 and opeC: "\<And>U. U \<in> \<V> \<Longrightarrow> openin (top_of_set C) U" |
1680 and "pairwise disjnt \<V>" |
1680 and "pairwise disjnt \<V>" |
1681 and homuu: "\<And>U. U \<in> \<V> \<Longrightarrow> \<exists>q. homeomorphism U (UU (X t)) p q" |
1681 and homuu: "\<And>U. U \<in> \<V> \<Longrightarrow> \<exists>q. homeomorphism U (UU (X t)) p q" |
1682 using inUS [OF t01] UU by meson |
1682 using inUS [OF t01] UU by meson |
1683 have n_div_N_in: "real n / real N \<in> {real n / real N .. (1 + real n) / real N}" |
1683 have n_div_N_in: "real n / real N \<in> {real n / real N .. (1 + real n) / real N}" |
1684 using N by (auto simp: divide_simps algebra_simps) |
1684 using N by (auto simp: divide_simps algebra_simps) |
1701 qed |
1701 qed |
1702 with \<V> have "k (real n / real N, y) \<in> \<Union>\<V>" |
1702 with \<V> have "k (real n / real N, y) \<in> \<Union>\<V>" |
1703 by blast |
1703 by blast |
1704 then obtain W where W: "k (real n / real N, y) \<in> W" and "W \<in> \<V>" |
1704 then obtain W where W: "k (real n / real N, y) \<in> W" and "W \<in> \<V>" |
1705 by blast |
1705 by blast |
1706 then obtain p' where opeC': "openin (subtopology euclidean C) W" |
1706 then obtain p' where opeC': "openin (top_of_set C) W" |
1707 and hom': "homeomorphism W (UU (X t)) p p'" |
1707 and hom': "homeomorphism W (UU (X t)) p p'" |
1708 using homuu opeC by blast |
1708 using homuu opeC by blast |
1709 then have "W \<subseteq> C" |
1709 then have "W \<subseteq> C" |
1710 using openin_imp_subset by blast |
1710 using openin_imp_subset by blast |
1711 define W' where "W' = UU(X t)" |
1711 define W' where "W' = UU(X t)" |
1712 have opeVW: "openin (subtopology euclidean V) (V \<inter> (k \<circ> Pair (n / N)) -` W)" |
1712 have opeVW: "openin (top_of_set V) (V \<inter> (k \<circ> Pair (n / N)) -` W)" |
1713 apply (rule continuous_openin_preimage [OF _ _ opeC']) |
1713 apply (rule continuous_openin_preimage [OF _ _ opeC']) |
1714 apply (intro continuous_intros continuous_on_subset [OF contk]) |
1714 apply (intro continuous_intros continuous_on_subset [OF contk]) |
1715 using kim apply (auto simp: \<open>y \<in> V\<close> W) |
1715 using kim apply (auto simp: \<open>y \<in> V\<close> W) |
1716 done |
1716 done |
1717 obtain N' where opeUN': "openin (subtopology euclidean U) N'" |
1717 obtain N' where opeUN': "openin (top_of_set U) N'" |
1718 and "y \<in> N'" and kimw: "k ` ({(real n / real N)} \<times> N') \<subseteq> W" |
1718 and "y \<in> N'" and kimw: "k ` ({(real n / real N)} \<times> N') \<subseteq> W" |
1719 apply (rule_tac N' = "(V \<inter> (k \<circ> Pair (n / N)) -` W)" in that) |
1719 apply (rule_tac N' = "(V \<inter> (k \<circ> Pair (n / N)) -` W)" in that) |
1720 apply (fastforce simp: \<open>y \<in> V\<close> W intro!: openin_trans [OF opeVW opeUV])+ |
1720 apply (fastforce simp: \<open>y \<in> V\<close> W intro!: openin_trans [OF opeVW opeUV])+ |
1721 done |
1721 done |
1722 obtain Q Q' where opeUQ: "openin (subtopology euclidean U) Q" |
1722 obtain Q Q' where opeUQ: "openin (top_of_set U) Q" |
1723 and cloUQ': "closedin (subtopology euclidean U) Q'" |
1723 and cloUQ': "closedin (top_of_set U) Q'" |
1724 and "y \<in> Q" "Q \<subseteq> Q'" |
1724 and "y \<in> Q" "Q \<subseteq> Q'" |
1725 and Q': "Q' \<subseteq> (U \<inter> NN(t)) \<inter> N' \<inter> V" |
1725 and Q': "Q' \<subseteq> (U \<inter> NN(t)) \<inter> N' \<inter> V" |
1726 proof - |
1726 proof - |
1727 obtain VO VX where "open VO" "open VX" and VO: "V = U \<inter> VO" and VX: "N' = U \<inter> VX" |
1727 obtain VO VX where "open VO" "open VX" and VO: "V = U \<inter> VO" and VX: "N' = U \<inter> VX" |
1728 using opeUV opeUN' by (auto simp: openin_open) |
1728 using opeUV opeUN' by (auto simp: openin_open) |
1730 using NN t01 by blast |
1730 using NN t01 by blast |
1731 then obtain e where "e > 0" and e: "cball y e \<subseteq> NN(t) \<inter> VO \<inter> VX" |
1731 then obtain e where "e > 0" and e: "cball y e \<subseteq> NN(t) \<inter> VO \<inter> VX" |
1732 by (metis Int_iff \<open>N' = U \<inter> VX\<close> \<open>V = U \<inter> VO\<close> \<open>y \<in> N'\<close> \<open>y \<in> V\<close> inUS open_contains_cball t01) |
1732 by (metis Int_iff \<open>N' = U \<inter> VX\<close> \<open>V = U \<inter> VO\<close> \<open>y \<in> N'\<close> \<open>y \<in> V\<close> inUS open_contains_cball t01) |
1733 show ?thesis |
1733 show ?thesis |
1734 proof |
1734 proof |
1735 show "openin (subtopology euclidean U) (U \<inter> ball y e)" |
1735 show "openin (top_of_set U) (U \<inter> ball y e)" |
1736 by blast |
1736 by blast |
1737 show "closedin (subtopology euclidean U) (U \<inter> cball y e)" |
1737 show "closedin (top_of_set U) (U \<inter> cball y e)" |
1738 using e by (auto simp: closedin_closed) |
1738 using e by (auto simp: closedin_closed) |
1739 qed (use \<open>y \<in> U\<close> \<open>e > 0\<close> VO VX e in auto) |
1739 qed (use \<open>y \<in> U\<close> \<open>e > 0\<close> VO VX e in auto) |
1740 qed |
1740 qed |
1741 then have "y \<in> Q'" "Q \<subseteq> (U \<inter> NN(t)) \<inter> N' \<inter> V" |
1741 then have "y \<in> Q'" "Q \<subseteq> (U \<inter> NN(t)) \<inter> N' \<inter> V" |
1742 by blast+ |
1742 by blast+ |
1747 by blast |
1747 by blast |
1748 have cont: "continuous_on ({0..(1 + real n) / real N} \<times> Q') |
1748 have cont: "continuous_on ({0..(1 + real n) / real N} \<times> Q') |
1749 (\<lambda>x. if x \<in> {0..real n / real N} \<times> Q' then k x else (p' \<circ> h) x)" |
1749 (\<lambda>x. if x \<in> {0..real n / real N} \<times> Q' then k x else (p' \<circ> h) x)" |
1750 unfolding neqQ' [symmetric] |
1750 unfolding neqQ' [symmetric] |
1751 proof (rule continuous_on_cases_local, simp_all add: neqQ' del: comp_apply) |
1751 proof (rule continuous_on_cases_local, simp_all add: neqQ' del: comp_apply) |
1752 show "closedin (subtopology euclidean ({0..(1 + real n) / real N} \<times> Q')) |
1752 show "closedin (top_of_set ({0..(1 + real n) / real N} \<times> Q')) |
1753 ({0..real n / real N} \<times> Q')" |
1753 ({0..real n / real N} \<times> Q')" |
1754 apply (simp add: closedin_closed) |
1754 apply (simp add: closedin_closed) |
1755 apply (rule_tac x="{0 .. real n / real N} \<times> UNIV" in exI) |
1755 apply (rule_tac x="{0 .. real n / real N} \<times> UNIV" in exI) |
1756 using n_div_N_in apply (auto simp: closed_Times) |
1756 using n_div_N_in apply (auto simp: closed_Times) |
1757 done |
1757 done |
1758 show "closedin (subtopology euclidean ({0..(1 + real n) / real N} \<times> Q')) |
1758 show "closedin (top_of_set ({0..(1 + real n) / real N} \<times> Q')) |
1759 ({real n / real N..(1 + real n) / real N} \<times> Q')" |
1759 ({real n / real N..(1 + real n) / real N} \<times> Q')" |
1760 apply (simp add: closedin_closed) |
1760 apply (simp add: closedin_closed) |
1761 apply (rule_tac x="{real n / real N .. (1 + real n) / real N} \<times> UNIV" in exI) |
1761 apply (rule_tac x="{real n / real N .. (1 + real n) / real N} \<times> UNIV" in exI) |
1762 apply (auto simp: closed_Times) |
1762 apply (auto simp: closed_Times) |
1763 by (meson divide_nonneg_nonneg of_nat_0_le_iff order_trans) |
1763 by (meson divide_nonneg_nonneg of_nat_0_le_iff order_trans) |
1843 qed (auto simp: \<open>y \<in> Q\<close> opeUQ) |
1843 qed (auto simp: \<open>y \<in> Q\<close> opeUQ) |
1844 qed |
1844 qed |
1845 show ?thesis |
1845 show ?thesis |
1846 using*[OF order_refl] N \<open>0 < \<delta>\<close> by (simp add: split: if_split_asm) |
1846 using*[OF order_refl] N \<open>0 < \<delta>\<close> by (simp add: split: if_split_asm) |
1847 qed |
1847 qed |
1848 then obtain V fs where opeV: "\<And>y. y \<in> U \<Longrightarrow> openin (subtopology euclidean U) (V y)" |
1848 then obtain V fs where opeV: "\<And>y. y \<in> U \<Longrightarrow> openin (top_of_set U) (V y)" |
1849 and V: "\<And>y. y \<in> U \<Longrightarrow> y \<in> V y" |
1849 and V: "\<And>y. y \<in> U \<Longrightarrow> y \<in> V y" |
1850 and contfs: "\<And>y. y \<in> U \<Longrightarrow> continuous_on ({0..1} \<times> V y) (fs y)" |
1850 and contfs: "\<And>y. y \<in> U \<Longrightarrow> continuous_on ({0..1} \<times> V y) (fs y)" |
1851 and *: "\<And>y. y \<in> U \<Longrightarrow> (fs y) ` ({0..1} \<times> V y) \<subseteq> C \<and> |
1851 and *: "\<And>y. y \<in> U \<Longrightarrow> (fs y) ` ({0..1} \<times> V y) \<subseteq> C \<and> |
1852 (\<forall>z \<in> V y. fs y (0, z) = f z) \<and> |
1852 (\<forall>z \<in> V y. fs y (0, z) = f z) \<and> |
1853 (\<forall>z \<in> {0..1} \<times> V y. h z = p(fs y z))" |
1853 (\<forall>z \<in> {0..1} \<times> V y. h z = p(fs y z))" |
1855 then have VU: "\<And>y. y \<in> U \<Longrightarrow> V y \<subseteq> U" |
1855 then have VU: "\<And>y. y \<in> U \<Longrightarrow> V y \<subseteq> U" |
1856 by (meson openin_imp_subset) |
1856 by (meson openin_imp_subset) |
1857 obtain k where contk: "continuous_on ({0..1} \<times> U) k" |
1857 obtain k where contk: "continuous_on ({0..1} \<times> U) k" |
1858 and k: "\<And>x i. \<lbrakk>i \<in> U; x \<in> {0..1} \<times> U \<inter> {0..1} \<times> V i\<rbrakk> \<Longrightarrow> k x = fs i x" |
1858 and k: "\<And>x i. \<lbrakk>i \<in> U; x \<in> {0..1} \<times> U \<inter> {0..1} \<times> V i\<rbrakk> \<Longrightarrow> k x = fs i x" |
1859 proof (rule pasting_lemma_exists) |
1859 proof (rule pasting_lemma_exists) |
1860 show "{0..1} \<times> U \<subseteq> (\<Union>i\<in>U. {0..1} \<times> V i)" |
1860 let ?X = "top_of_set ({0..1::real} \<times> U)" |
1861 apply auto |
1861 show "topspace ?X \<subseteq> (\<Union>i\<in>U. {0..1} \<times> V i)" |
1862 using V by blast |
1862 using V by force |
1863 show "\<And>i. i \<in> U \<Longrightarrow> openin (subtopology euclidean ({0..1} \<times> U)) ({0..1} \<times> V i)" |
1863 show "\<And>i. i \<in> U \<Longrightarrow> openin (top_of_set ({0..1} \<times> U)) ({0..1} \<times> V i)" |
1864 by (simp add: opeV openin_Times) |
1864 by (simp add: opeV openin_Times) |
1865 show "\<And>i. i \<in> U \<Longrightarrow> continuous_on ({0..1} \<times> V i) (fs i)" |
1865 show "\<And>i. i \<in> U \<Longrightarrow> continuous_map |
1866 using contfs by blast |
1866 (subtopology (top_of_set ({0..1} \<times> U)) ({0..1} \<times> V i)) euclidean (fs i)" |
1867 show "fs i x = fs j x" if "i \<in> U" "j \<in> U" and x: "x \<in> {0..1} \<times> U \<inter> {0..1} \<times> V i \<inter> {0..1} \<times> V j" |
1867 using contfs |
|
1868 apply simp |
|
1869 by (metis continuous_map_iff_continuous continuous_on_subset openin_imp_subset openin_subtopology_self subtopology_subtopology) |
|
1870 show "fs i x = fs j x" if "i \<in> U" "j \<in> U" and x: "x \<in> topspace ?X \<inter> {0..1} \<times> V i \<inter> {0..1} \<times> V j" |
1868 for i j x |
1871 for i j x |
1869 proof - |
1872 proof - |
1870 obtain u y where "x = (u, y)" "y \<in> V i" "y \<in> V j" "0 \<le> u" "u \<le> 1" |
1873 obtain u y where "x = (u, y)" "y \<in> V i" "y \<in> V j" "0 \<le> u" "u \<le> 1" |
1871 using x by auto |
1874 using x by auto |
1872 show ?thesis |
1875 show ?thesis |
2280 using*[OF \<open>y \<in> U\<close>] by (metis l atLeastAtMost_iff order_refl pathfinish_def zero_le_one) |
2283 using*[OF \<open>y \<in> U\<close>] by (metis l atLeastAtMost_iff order_refl pathfinish_def zero_le_one) |
2281 show "l z = a" |
2284 show "l z = a" |
2282 using l [of "linepath z z" z "linepath a a"] by (auto simp: assms) |
2285 using l [of "linepath z z" z "linepath a a"] by (auto simp: assms) |
2283 show LC: "l ` U \<subseteq> C" |
2286 show LC: "l ` U \<subseteq> C" |
2284 by (clarify dest!: *) (metis (full_types) l pathfinish_in_path_image subsetCE) |
2287 by (clarify dest!: *) (metis (full_types) l pathfinish_in_path_image subsetCE) |
2285 have "\<exists>T. openin (subtopology euclidean U) T \<and> y \<in> T \<and> T \<subseteq> U \<inter> l -` X" |
2288 have "\<exists>T. openin (top_of_set U) T \<and> y \<in> T \<and> T \<subseteq> U \<inter> l -` X" |
2286 if X: "openin (subtopology euclidean C) X" and "y \<in> U" "l y \<in> X" for X y |
2289 if X: "openin (top_of_set C) X" and "y \<in> U" "l y \<in> X" for X y |
2287 proof - |
2290 proof - |
2288 have "X \<subseteq> C" |
2291 have "X \<subseteq> C" |
2289 using X openin_euclidean_subtopology_iff by blast |
2292 using X openin_euclidean_subtopology_iff by blast |
2290 have "f y \<in> S" |
2293 have "f y \<in> S" |
2291 using fim \<open>y \<in> U\<close> by blast |
2294 using fim \<open>y \<in> U\<close> by blast |
2292 then obtain W \<V> |
2295 then obtain W \<V> |
2293 where WV: "f y \<in> W \<and> openin (subtopology euclidean S) W \<and> |
2296 where WV: "f y \<in> W \<and> openin (top_of_set S) W \<and> |
2294 (\<Union>\<V> = C \<inter> p -` W \<and> |
2297 (\<Union>\<V> = C \<inter> p -` W \<and> |
2295 (\<forall>U \<in> \<V>. openin (subtopology euclidean C) U) \<and> |
2298 (\<forall>U \<in> \<V>. openin (top_of_set C) U) \<and> |
2296 pairwise disjnt \<V> \<and> |
2299 pairwise disjnt \<V> \<and> |
2297 (\<forall>U \<in> \<V>. \<exists>q. homeomorphism U W p q))" |
2300 (\<forall>U \<in> \<V>. \<exists>q. homeomorphism U W p q))" |
2298 using cov by (force simp: covering_space_def) |
2301 using cov by (force simp: covering_space_def) |
2299 then have "l y \<in> \<Union>\<V>" |
2302 then have "l y \<in> \<Union>\<V>" |
2300 using \<open>X \<subseteq> C\<close> pleq that by auto |
2303 using \<open>X \<subseteq> C\<close> pleq that by auto |
2301 then obtain W' where "l y \<in> W'" and "W' \<in> \<V>" |
2304 then obtain W' where "l y \<in> W'" and "W' \<in> \<V>" |
2302 by blast |
2305 by blast |
2303 with WV obtain p' where opeCW': "openin (subtopology euclidean C) W'" |
2306 with WV obtain p' where opeCW': "openin (top_of_set C) W'" |
2304 and homUW': "homeomorphism W' W p p'" |
2307 and homUW': "homeomorphism W' W p p'" |
2305 by blast |
2308 by blast |
2306 then have contp': "continuous_on W p'" and p'im: "p' ` W \<subseteq> W'" |
2309 then have contp': "continuous_on W p'" and p'im: "p' ` W \<subseteq> W'" |
2307 using homUW' homeomorphism_image2 homeomorphism_cont2 by fastforce+ |
2310 using homUW' homeomorphism_image2 homeomorphism_cont2 by fastforce+ |
2308 obtain V where "y \<in> V" "y \<in> U" and fimW: "f ` V \<subseteq> W" "V \<subseteq> U" |
2311 obtain V where "y \<in> V" "y \<in> U" and fimW: "f ` V \<subseteq> W" "V \<subseteq> U" |
2309 and "path_connected V" and opeUV: "openin (subtopology euclidean U) V" |
2312 and "path_connected V" and opeUV: "openin (top_of_set U) V" |
2310 proof - |
2313 proof - |
2311 have "openin (subtopology euclidean U) (U \<inter> f -` W)" |
2314 have "openin (top_of_set U) (U \<inter> f -` W)" |
2312 using WV contf continuous_on_open_gen fim by auto |
2315 using WV contf continuous_on_open_gen fim by auto |
2313 then show ?thesis |
2316 then show ?thesis |
2314 using U WV |
2317 using U WV |
2315 apply (auto simp: locally_path_connected) |
2318 apply (auto simp: locally_path_connected) |
2316 apply (drule_tac x="U \<inter> f -` W" in spec) |
2319 apply (drule_tac x="U \<inter> f -` W" in spec) |
2322 using opeCW' WV openin_imp_subset by auto |
2325 using opeCW' WV openin_imp_subset by auto |
2323 have p'im: "p' ` W \<subseteq> W'" |
2326 have p'im: "p' ` W \<subseteq> W'" |
2324 using homUW' homeomorphism_image2 by fastforce |
2327 using homUW' homeomorphism_image2 by fastforce |
2325 show ?thesis |
2328 show ?thesis |
2326 proof (intro exI conjI) |
2329 proof (intro exI conjI) |
2327 have "openin (subtopology euclidean S) (W \<inter> p' -` (W' \<inter> X))" |
2330 have "openin (top_of_set S) (W \<inter> p' -` (W' \<inter> X))" |
2328 proof (rule openin_trans) |
2331 proof (rule openin_trans) |
2329 show "openin (subtopology euclidean W) (W \<inter> p' -` (W' \<inter> X))" |
2332 show "openin (top_of_set W) (W \<inter> p' -` (W' \<inter> X))" |
2330 apply (rule continuous_openin_preimage [OF contp' p'im]) |
2333 apply (rule continuous_openin_preimage [OF contp' p'im]) |
2331 using X \<open>W' \<subseteq> C\<close> apply (auto simp: openin_open) |
2334 using X \<open>W' \<subseteq> C\<close> apply (auto simp: openin_open) |
2332 done |
2335 done |
2333 show "openin (subtopology euclidean S) W" |
2336 show "openin (top_of_set S) W" |
2334 using WV by blast |
2337 using WV by blast |
2335 qed |
2338 qed |
2336 then show "openin (subtopology euclidean U) (V \<inter> (U \<inter> (f -` (W \<inter> (p' -` (W' \<inter> X))))))" |
2339 then show "openin (top_of_set U) (V \<inter> (U \<inter> (f -` (W \<inter> (p' -` (W' \<inter> X))))))" |
2337 by (blast intro: opeUV openin_subtopology_self continuous_openin_preimage [OF contf fim]) |
2340 by (blast intro: opeUV openin_subtopology_self continuous_openin_preimage [OF contf fim]) |
2338 have "p' (f y) \<in> X" |
2341 have "p' (f y) \<in> X" |
2339 using \<open>l y \<in> W'\<close> homeomorphism_apply1 [OF homUW'] pleq \<open>y \<in> U\<close> \<open>l y \<in> X\<close> by fastforce |
2342 using \<open>l y \<in> W'\<close> homeomorphism_apply1 [OF homUW'] pleq \<open>y \<in> U\<close> \<open>l y \<in> X\<close> by fastforce |
2340 then show "y \<in> V \<inter> (U \<inter> f -` (W \<inter> p' -` (W' \<inter> X)))" |
2343 then show "y \<in> V \<inter> (U \<inter> f -` (W \<inter> p' -` (W' \<inter> X)))" |
2341 using \<open>y \<in> U\<close> \<open>y \<in> V\<close> WV p'im by auto |
2344 using \<open>y \<in> U\<close> \<open>y \<in> V\<close> WV p'im by auto |