diff -r 30f69046f120 -r ffdad62bc235 src/HOL/Analysis/Path_Connected.thy --- a/src/HOL/Analysis/Path_Connected.thy Sat May 06 12:42:10 2023 +0100 +++ b/src/HOL/Analysis/Path_Connected.thy Sun May 07 14:52:53 2023 +0100 @@ -2313,6 +2313,174 @@ using assms homeomorphic_map_path_component_of by fastforce +subsection\Paths and path-connectedness\ + +lemma path_connected_space_quotient_map_image: + "\quotient_map X Y q; path_connected_space X\ \ path_connected_space Y" + by (metis path_connectedin_continuous_map_image path_connectedin_topspace quotient_imp_continuous_map quotient_imp_surjective_map) + +lemma path_connected_space_retraction_map_image: + "\retraction_map X Y r; path_connected_space X\ \ path_connected_space Y" + using path_connected_space_quotient_map_image retraction_imp_quotient_map by blast + +lemma path_connected_space_prod_topology: + "path_connected_space(prod_topology X Y) \ + topspace(prod_topology X Y) = {} \ path_connected_space X \ path_connected_space Y" +proof (cases "topspace(prod_topology X Y) = {}") + case True + then show ?thesis + by (simp add: path_connected_space_topspace_empty) +next + case False + have "path_connected_space (prod_topology X Y)" + if X: "path_connected_space X" and Y: "path_connected_space Y" + proof (clarsimp simp: path_connected_space_def) + fix x y x' y' + assume "x \ topspace X" and "y \ topspace Y" and "x' \ topspace X" and "y' \ topspace Y" + obtain f where "pathin X f" "f 0 = x" "f 1 = x'" + by (meson X \x \ topspace X\ \x' \ topspace X\ path_connected_space_def) + obtain g where "pathin Y g" "g 0 = y" "g 1 = y'" + by (meson Y \y \ topspace Y\ \y' \ topspace Y\ path_connected_space_def) + show "\h. pathin (prod_topology X Y) h \ h 0 = (x,y) \ h 1 = (x',y')" + proof (intro exI conjI) + show "pathin (prod_topology X Y) (\t. (f t, g t))" + using \pathin X f\ \pathin Y g\ by (simp add: continuous_map_paired pathin_def) + show "(\t. (f t, g t)) 0 = (x, y)" + using \f 0 = x\ \g 0 = y\ by blast + show "(\t. (f t, g t)) 1 = (x', y')" + using \f 1 = x'\ \g 1 = y'\ by blast + qed + qed + then show ?thesis + by (metis False Sigma_empty1 Sigma_empty2 topspace_prod_topology path_connected_space_retraction_map_image + retraction_map_fst retraction_map_snd) +qed + +lemma path_connectedin_Times: + "path_connectedin (prod_topology X Y) (S \ T) \ + S = {} \ T = {} \ path_connectedin X S \ path_connectedin Y T" + by (auto simp add: path_connectedin_def subtopology_Times path_connected_space_prod_topology) + + +subsection\Path components\ + +lemma path_component_of_subtopology_eq: + "path_component_of (subtopology X U) x = path_component_of X x \ path_component_of_set X x \ U" + (is "?lhs = ?rhs") +proof + show "?lhs \ ?rhs" + by (metis path_connectedin_path_component_of path_connectedin_subtopology) +next + show "?rhs \ ?lhs" + unfolding fun_eq_iff + by (metis path_connectedin_subtopology path_component_of path_component_of_aux path_component_of_mono) +qed + +lemma path_components_of_subtopology: + assumes "C \ path_components_of X" "C \ U" + shows "C \ path_components_of (subtopology X U)" + using assms path_component_of_refl path_component_of_subtopology_eq topspace_subtopology + by (smt (verit) imageE path_component_in_path_components_of path_components_of_def) + +lemma path_imp_connected_component_of: + "path_component_of X x y \ connected_component_of X x y" + by (metis in_mono mem_Collect_eq path_component_subset_connected_component_of) + +lemma finite_path_components_of_finite: + "finite(topspace X) \ finite(path_components_of X)" + by (simp add: Union_path_components_of finite_UnionD) + +lemma path_component_of_continuous_image: + "\continuous_map X X' f; path_component_of X x y\ \ path_component_of X' (f x) (f y)" + by (meson image_eqI path_component_of path_connectedin_continuous_map_image) + +lemma path_component_of_pair [simp]: + "path_component_of_set (prod_topology X Y) (x,y) = + path_component_of_set X x \ path_component_of_set Y y" (is "?lhs = ?rhs") +proof (cases "?lhs = {}") + case True + then show ?thesis + by (metis Sigma_empty1 Sigma_empty2 mem_Sigma_iff path_component_of_eq_empty topspace_prod_topology) +next + case False + then have "path_component_of X x x" "path_component_of Y y y" + using path_component_of_eq_empty path_component_of_refl by fastforce+ + moreover + have "path_connectedin (prod_topology X Y) (path_component_of_set X x \ path_component_of_set Y y)" + by (metis path_connectedin_Times path_connectedin_path_component_of) + moreover have "path_component_of X x a" "path_component_of Y y b" + if "(x, y) \ C'" "(a,b) \ C'" and "path_connectedin (prod_topology X Y) C'" for C' a b + by (smt (verit, best) that continuous_map_fst continuous_map_snd fst_conv snd_conv path_component_of path_component_of_continuous_image)+ + ultimately show ?thesis + by (intro path_component_of_unique) auto +qed + +lemma path_components_of_prod_topology: + "path_components_of (prod_topology X Y) = + (\(C,D). C \ D) ` (path_components_of X \ path_components_of Y)" + by (force simp add: image_iff path_components_of_def) + +lemma path_components_of_prod_topology': + "path_components_of (prod_topology X Y) = + {C \ D |C D. C \ path_components_of X \ D \ path_components_of Y}" + by (auto simp: path_components_of_prod_topology) + +lemma path_component_of_product_topology: + "path_component_of_set (product_topology X I) f = + (if f \ extensional I then PiE I (\i. path_component_of_set (X i) (f i)) else {})" + (is "?lhs = ?rhs") +proof (cases "path_component_of_set (product_topology X I) f = {}") + case True + then show ?thesis + by (smt (verit) PiE_eq_empty_iff PiE_iff path_component_of_eq_empty topspace_product_topology) +next + case False + then have [simp]: "f \ extensional I" + by (auto simp: path_component_of_eq_empty PiE_iff path_component_of_equiv) + show ?thesis + proof (intro path_component_of_unique) + show "f \ ?rhs" + using False path_component_of_eq_empty path_component_of_refl by force + show "path_connectedin (product_topology X I) (if f \ extensional I then \\<^sub>E i\I. path_component_of_set (X i) (f i) else {})" + by (simp add: path_connectedin_PiE path_connectedin_path_component_of) + fix C' + assume "f \ C'" and C': "path_connectedin (product_topology X I) C'" + show "C' \ ?rhs" + proof - + have "C' \ extensional I" + using PiE_def C' path_connectedin_subset_topspace by fastforce + with \f \ C'\ C' show ?thesis + apply (clarsimp simp: PiE_iff subset_iff) + by (smt (verit, ccfv_threshold) continuous_map_product_projection path_component_of path_component_of_continuous_image) + qed + qed +qed + +lemma path_components_of_product_topology: + "path_components_of (product_topology X I) = + {PiE I B |B. \i \ I. B i \ path_components_of(X i)}" (is "?lhs=?rhs") +proof + show "?lhs \ ?rhs" + apply (simp add: path_components_of_def image_subset_iff) + by (smt (verit, best) PiE_iff image_eqI path_component_of_product_topology) +next + show "?rhs \ ?lhs" + proof + fix F + assume "F \ ?rhs" + then obtain B where B: "F = Pi\<^sub>E I B" + and "\i\I. \x\topspace (X i). B i = path_component_of_set (X i) x" + by (force simp add: path_components_of_def image_iff) + then obtain f where ftop: "\i. i \ I \ f i \ topspace (X i)" + and BF: "\i. i \ I \ B i = path_component_of_set (X i) (f i)" + by metis + then have "F = path_component_of_set (product_topology X I) (restrict f I)" + by (metis (mono_tags, lifting) B PiE_cong path_component_of_product_topology restrict_apply' restrict_extensional) + then show "F \ ?lhs" + by (simp add: ftop path_component_in_path_components_of) + qed +qed + subsection \Sphere is path-connected\ lemma path_connected_punctured_universe: