1880 by (simp add: Bex_def) |
1880 by (simp add: Bex_def) |
1881 also have "\<dots> = - {a}" |
1881 also have "\<dots> = - {a}" |
1882 by auto |
1882 by auto |
1883 finally show ?thesis . |
1883 finally show ?thesis . |
1884 qed |
1884 qed |
|
1885 |
|
1886 corollary connected_punctured_universe: |
|
1887 "2 \<le> DIM('N::euclidean_space) \<Longrightarrow> connected(- {a::'N})" |
|
1888 by (simp add: path_connected_punctured_universe path_connected_imp_connected) |
1885 |
1889 |
1886 lemma path_connected_sphere: |
1890 lemma path_connected_sphere: |
1887 assumes "2 \<le> DIM('a::euclidean_space)" |
1891 assumes "2 \<le> DIM('a::euclidean_space)" |
1888 shows "path_connected {x::'a. norm (x - a) = r}" |
1892 shows "path_connected {x::'a. norm (x - a) = r}" |
1889 proof (rule linorder_cases [of r 0]) |
1893 proof (rule linorder_cases [of r 0]) |
2102 moreover have "open (S - F)" using finite_imp_closed[OF \<open>finite F\<close>] \<open>open S\<close> by auto |
2106 moreover have "open (S - F)" using finite_imp_closed[OF \<open>finite F\<close>] \<open>open S\<close> by auto |
2103 ultimately have "connected (S - F - {x})" using connected_open_delete[OF _ _ 2] by auto |
2107 ultimately have "connected (S - F - {x})" using connected_open_delete[OF _ _ 2] by auto |
2104 thus ?case by (metis Diff_insert) |
2108 thus ?case by (metis Diff_insert) |
2105 qed |
2109 qed |
2106 |
2110 |
|
2111 lemma psubset_sphere_Compl_connected: |
|
2112 fixes S :: "'a::euclidean_space set" |
|
2113 assumes S: "S \<subset> sphere a r" and "0 < r" and 2: "2 \<le> DIM('a)" |
|
2114 shows "connected(- S)" |
|
2115 proof - |
|
2116 have "S \<subseteq> sphere a r" |
|
2117 using S by blast |
|
2118 obtain b where "dist a b = r" and "b \<notin> S" |
|
2119 using S mem_sphere by blast |
|
2120 have CS: "- S = {x. dist a x \<le> r \<and> (x \<notin> S)} \<union> {x. r \<le> dist a x \<and> (x \<notin> S)}" |
|
2121 by (auto simp: ) |
|
2122 have "{x. dist a x \<le> r \<and> x \<notin> S} \<inter> {x. r \<le> dist a x \<and> x \<notin> S} \<noteq> {}" |
|
2123 using \<open>b \<notin> S\<close> \<open>dist a b = r\<close> by blast |
|
2124 moreover have "connected {x. dist a x \<le> r \<and> x \<notin> S}" |
|
2125 apply (rule connected_intermediate_closure [of "ball a r"]) |
|
2126 using assms by auto |
|
2127 moreover |
|
2128 have "connected {x. r \<le> dist a x \<and> x \<notin> S}" |
|
2129 apply (rule connected_intermediate_closure [of "- cball a r"]) |
|
2130 using assms apply (auto intro: connected_complement_bounded_convex) |
|
2131 apply (metis ComplI interior_cball interior_closure mem_ball not_less) |
|
2132 done |
|
2133 ultimately show ?thesis |
|
2134 by (simp add: CS connected_Un) |
|
2135 qed |
|
2136 |
2107 subsection\<open>Relations between components and path components\<close> |
2137 subsection\<open>Relations between components and path components\<close> |
2108 |
2138 |
2109 lemma open_connected_component: |
2139 lemma open_connected_component: |
2110 fixes s :: "'a::real_normed_vector set" |
2140 fixes s :: "'a::real_normed_vector set" |
2111 shows "open s \<Longrightarrow> open (connected_component_set s x)" |
2141 shows "open s \<Longrightarrow> open (connected_component_set s x)" |
2503 shows "frontier(connected_component_set S x) \<subseteq> frontier S" |
2533 shows "frontier(connected_component_set S x) \<subseteq> frontier S" |
2504 proof - |
2534 proof - |
2505 { fix y |
2535 { fix y |
2506 assume y1: "y \<in> closure (connected_component_set S x)" |
2536 assume y1: "y \<in> closure (connected_component_set S x)" |
2507 and y2: "y \<notin> interior (connected_component_set S x)" |
2537 and y2: "y \<notin> interior (connected_component_set S x)" |
2508 have 1: "y \<in> closure S" |
2538 have "y \<in> closure S" |
2509 using y1 closure_mono connected_component_subset by blast |
2539 using y1 closure_mono connected_component_subset by blast |
2510 have "z \<in> interior (connected_component_set S x)" |
2540 moreover have "z \<in> interior (connected_component_set S x)" |
2511 if "0 < e" "ball y e \<subseteq> interior S" "dist y z < e" for e z |
2541 if "0 < e" "ball y e \<subseteq> interior S" "dist y z < e" for e z |
2512 proof - |
2542 proof - |
2513 have "ball y e \<subseteq> connected_component_set S y" |
2543 have "ball y e \<subseteq> connected_component_set S y" |
2514 apply (rule connected_component_maximal) |
2544 apply (rule connected_component_maximal) |
2515 using that interior_subset mem_ball apply auto |
2545 using that interior_subset mem_ball apply auto |
2516 done |
2546 done |
2517 then show ?thesis |
2547 then show ?thesis |
2518 using y1 apply (simp add: closure_approachable open_contains_ball_eq [OF open_interior]) |
2548 using y1 apply (simp add: closure_approachable open_contains_ball_eq [OF open_interior]) |
2519 by (metis (no_types, hide_lams) connected_component_eq_eq connected_component_in subsetD |
2549 by (metis connected_component_eq dist_commute mem_Collect_eq mem_ball mem_interior subsetD \<open>0 < e\<close> y2) |
2520 dist_commute mem_Collect_eq mem_ball mem_interior \<open>0 < e\<close> y2) |
|
2521 qed |
2550 qed |
2522 then have 2: "y \<notin> interior S" |
2551 then have "y \<notin> interior S" |
2523 using y2 by (force simp: open_contains_ball_eq [OF open_interior]) |
2552 using y2 by (force simp: open_contains_ball_eq [OF open_interior]) |
2524 note 1 2 |
2553 ultimately have "y \<in> frontier S" |
|
2554 by (auto simp: frontier_def) |
2525 } |
2555 } |
2526 then show ?thesis by (auto simp: frontier_def) |
2556 then show ?thesis by (auto simp: frontier_def) |
2527 qed |
2557 qed |
2528 |
2558 |
2529 lemma frontier_Union_subset_closure: |
2559 lemma frontier_Union_subset_closure: |
2562 lemma frontier_Union_subset: |
2592 lemma frontier_Union_subset: |
2563 fixes F :: "'a::real_normed_vector set set" |
2593 fixes F :: "'a::real_normed_vector set set" |
2564 shows "finite F \<Longrightarrow> frontier(\<Union>F) \<subseteq> (\<Union>t \<in> F. frontier t)" |
2594 shows "finite F \<Longrightarrow> frontier(\<Union>F) \<subseteq> (\<Union>t \<in> F. frontier t)" |
2565 by (rule order_trans [OF frontier_Union_subset_closure]) |
2595 by (rule order_trans [OF frontier_Union_subset_closure]) |
2566 (auto simp: closure_subset_eq) |
2596 (auto simp: closure_subset_eq) |
|
2597 |
|
2598 lemma frontier_of_components_subset: |
|
2599 fixes S :: "'a::real_normed_vector set" |
|
2600 shows "C \<in> components S \<Longrightarrow> frontier C \<subseteq> frontier S" |
|
2601 by (metis Path_Connected.frontier_of_connected_component_subset components_iff) |
|
2602 |
|
2603 lemma frontier_of_components_closed_complement: |
|
2604 fixes S :: "'a::real_normed_vector set" |
|
2605 shows "\<lbrakk>closed S; C \<in> components (- S)\<rbrakk> \<Longrightarrow> frontier C \<subseteq> S" |
|
2606 using frontier_complement frontier_of_components_subset frontier_subset_eq by blast |
|
2607 |
|
2608 lemma frontier_minimal_separating_closed: |
|
2609 fixes S :: "'a::real_normed_vector set" |
|
2610 assumes "closed S" |
|
2611 and nconn: "~ connected(- S)" |
|
2612 and C: "C \<in> components (- S)" |
|
2613 and conn: "\<And>T. \<lbrakk>closed T; T \<subset> S\<rbrakk> \<Longrightarrow> connected(- T)" |
|
2614 shows "frontier C = S" |
|
2615 proof (rule ccontr) |
|
2616 assume "frontier C \<noteq> S" |
|
2617 then have "frontier C \<subset> S" |
|
2618 using frontier_of_components_closed_complement [OF \<open>closed S\<close> C] by blast |
|
2619 then have "connected(- (frontier C))" |
|
2620 by (simp add: conn) |
|
2621 have "\<not> connected(- (frontier C))" |
|
2622 unfolding connected_def not_not |
|
2623 proof (intro exI conjI) |
|
2624 show "open C" |
|
2625 using C \<open>closed S\<close> open_components by blast |
|
2626 show "open (- closure C)" |
|
2627 by blast |
|
2628 show "C \<inter> - closure C \<inter> - frontier C = {}" |
|
2629 using closure_subset by blast |
|
2630 show "C \<inter> - frontier C \<noteq> {}" |
|
2631 using C \<open>open C\<close> components_eq frontier_disjoint_eq by fastforce |
|
2632 show "- frontier C \<subseteq> C \<union> - closure C" |
|
2633 by (simp add: \<open>open C\<close> closed_Compl frontier_closures) |
|
2634 then show "- closure C \<inter> - frontier C \<noteq> {}" |
|
2635 by (metis (no_types, lifting) C Compl_subset_Compl_iff \<open>frontier C \<subset> S\<close> compl_sup frontier_closures in_components_subset psubsetE sup.absorb_iff2 sup.boundedE sup_bot.right_neutral sup_inf_absorb) |
|
2636 qed |
|
2637 then show False |
|
2638 using \<open>connected (- frontier C)\<close> by blast |
|
2639 qed |
2567 |
2640 |
2568 lemma connected_component_UNIV [simp]: |
2641 lemma connected_component_UNIV [simp]: |
2569 fixes x :: "'a::real_normed_vector" |
2642 fixes x :: "'a::real_normed_vector" |
2570 shows "connected_component_set UNIV x = UNIV" |
2643 shows "connected_component_set UNIV x = UNIV" |
2571 using connected_iff_eq_connected_component_set [of "UNIV::'a set"] connected_UNIV |
2644 using connected_iff_eq_connected_component_set [of "UNIV::'a set"] connected_UNIV |
6137 (\<forall>f. continuous_on T f \<and> f ` T \<subseteq> U |
6210 (\<forall>f. continuous_on T f \<and> f ` T \<subseteq> U |
6138 \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) T U f (\<lambda>x. c)))" |
6211 \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) T U f (\<lambda>x. c)))" |
6139 apply (rule iffI) |
6212 apply (rule iffI) |
6140 apply (metis assms homotopy_eqv_cohomotopic_triviality_null_imp) |
6213 apply (metis assms homotopy_eqv_cohomotopic_triviality_null_imp) |
6141 by (metis assms homotopy_eqv_cohomotopic_triviality_null_imp homotopy_eqv_sym) |
6214 by (metis assms homotopy_eqv_cohomotopic_triviality_null_imp homotopy_eqv_sym) |
|
6215 |
|
6216 lemma homotopy_eqv_homotopic_triviality_null_imp: |
|
6217 fixes S :: "'a::real_normed_vector set" |
|
6218 and T :: "'b::real_normed_vector set" |
|
6219 and U :: "'c::real_normed_vector set" |
|
6220 assumes "S homotopy_eqv T" |
|
6221 and f: "continuous_on U f" "f ` U \<subseteq> T" |
|
6222 and homSU: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S\<rbrakk> |
|
6223 \<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) U S f (\<lambda>x. c)" |
|
6224 shows "\<exists>c. homotopic_with (\<lambda>x. True) U T f (\<lambda>x. c)" |
|
6225 proof - |
|
6226 obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T" |
|
6227 and k: "continuous_on T k" "k ` T \<subseteq> S" |
|
6228 and hom: "homotopic_with (\<lambda>x. True) S S (k \<circ> h) id" |
|
6229 "homotopic_with (\<lambda>x. True) T T (h \<circ> k) id" |
|
6230 using assms by (auto simp: homotopy_eqv_def) |
|
6231 obtain c::'a where "homotopic_with (\<lambda>x. True) U S (k \<circ> f) (\<lambda>x. c)" |
|
6232 apply (rule exE [OF homSU [of "k \<circ> f"]]) |
|
6233 apply (intro continuous_on_compose h) |
|
6234 using k f apply (force elim!: continuous_on_subset)+ |
|
6235 done |
|
6236 then have "homotopic_with (\<lambda>x. True) U T (h \<circ> (k \<circ> f)) (h \<circ> (\<lambda>x. c))" |
|
6237 apply (rule homotopic_with_compose_continuous_left [where Y=S]) |
|
6238 using h by auto |
|
6239 moreover have "homotopic_with (\<lambda>x. True) U T (id \<circ> f) ((h \<circ> k) \<circ> f)" |
|
6240 apply (rule homotopic_with_compose_continuous_right [where X=T]) |
|
6241 apply (simp add: hom homotopic_with_symD) |
|
6242 using f apply auto |
|
6243 done |
|
6244 ultimately show ?thesis |
|
6245 using homotopic_with_trans by (fastforce simp add: o_def) |
|
6246 qed |
|
6247 |
|
6248 lemma homotopy_eqv_homotopic_triviality_null: |
|
6249 fixes S :: "'a::real_normed_vector set" |
|
6250 and T :: "'b::real_normed_vector set" |
|
6251 and U :: "'c::real_normed_vector set" |
|
6252 assumes "S homotopy_eqv T" |
|
6253 shows "(\<forall>f. continuous_on U f \<and> f ` U \<subseteq> S |
|
6254 \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) U S f (\<lambda>x. c))) \<longleftrightarrow> |
|
6255 (\<forall>f. continuous_on U f \<and> f ` U \<subseteq> T |
|
6256 \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) U T f (\<lambda>x. c)))" |
|
6257 apply (rule iffI) |
|
6258 apply (metis assms homotopy_eqv_homotopic_triviality_null_imp) |
|
6259 by (metis assms homotopy_eqv_homotopic_triviality_null_imp homotopy_eqv_sym) |
6142 |
6260 |
6143 lemma homotopy_eqv_contractible_sets: |
6261 lemma homotopy_eqv_contractible_sets: |
6144 fixes S :: "'a::real_normed_vector set" |
6262 fixes S :: "'a::real_normed_vector set" |
6145 and T :: "'b::real_normed_vector set" |
6263 and T :: "'b::real_normed_vector set" |
6146 assumes "contractible S" "contractible T" "S = {} \<longleftrightarrow> T = {}" |
6264 assumes "contractible S" "contractible T" "S = {} \<longleftrightarrow> T = {}" |