# HG changeset patch # User paulson # Date 1684167138 -3600 # Node ID 37894dff0111101415bedcc88781707580944b06 # Parent 2594319ad9eec33e6736cf87e7383364302a4ebb More material from the HOL Light metric space library diff -r 2594319ad9ee -r 37894dff0111 src/HOL/Analysis/Abstract_Topological_Spaces.thy --- a/src/HOL/Analysis/Abstract_Topological_Spaces.thy Thu May 11 22:12:43 2023 +0200 +++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy Mon May 15 17:12:18 2023 +0100 @@ -71,69 +71,6 @@ by (simp add: Hausdorff_imp_t1_space connectedin_imp_perfect_gen) -proposition connected_space_prod_topology: - "connected_space(prod_topology X Y) \ - topspace(prod_topology X Y) = {} \ connected_space X \ connected_space Y" (is "?lhs=?rhs") -proof (cases "topspace(prod_topology X Y) = {}") - case True - then show ?thesis - using connected_space_topspace_empty by blast -next - case False - then have nonempty: "topspace X \ {}" "topspace Y \ {}" - by force+ - show ?thesis - proof - assume ?lhs - then show ?rhs - by (meson connected_space_quotient_map_image nonempty quotient_map_fst quotient_map_snd) - next - assume ?rhs - then have conX: "connected_space X" and conY: "connected_space Y" - using False by blast+ - have False - if "openin (prod_topology X Y) U" and "openin (prod_topology X Y) V" - and UV: "topspace X \ topspace Y \ U \ V" "U \ V = {}" - and "U \ {}" and "V \ {}" - for U V - proof - - have Usub: "U \ topspace X \ topspace Y" and Vsub: "V \ topspace X \ topspace Y" - using that by (metis openin_subset topspace_prod_topology)+ - obtain a b where ab: "(a,b) \ U" and a: "a \ topspace X" and b: "b \ topspace Y" - using \U \ {}\ Usub by auto - have "\ topspace X \ topspace Y \ U" - using Usub Vsub \U \ V = {}\ \V \ {}\ by auto - then obtain x y where x: "x \ topspace X" and y: "y \ topspace Y" and "(x,y) \ U" - by blast - have oX: "openin X {x \ topspace X. (x,y) \ U}" "openin X {x \ topspace X. (x,y) \ V}" - and oY: "openin Y {y \ topspace Y. (a,y) \ U}" "openin Y {y \ topspace Y. (a,y) \ V}" - by (force intro: openin_continuous_map_preimage [where Y = "prod_topology X Y"] - simp: that continuous_map_pairwise o_def x y a)+ - have 1: "topspace Y \ {y \ topspace Y. (a,y) \ U} \ {y \ topspace Y. (a,y) \ V}" - using a that(3) by auto - have 2: "{y \ topspace Y. (a,y) \ U} \ {y \ topspace Y. (a,y) \ V} = {}" - using that(4) by auto - have 3: "{y \ topspace Y. (a,y) \ U} \ {}" - using ab b by auto - have 4: "{y \ topspace Y. (a,y) \ V} \ {}" - proof - - show ?thesis - using connected_spaceD [OF conX oX] UV \(x,y) \ U\ a x y - disjoint_iff_not_equal by blast - qed - show ?thesis - using connected_spaceD [OF conY oY 1 2 3 4] by auto - qed - then show ?lhs - unfolding connected_space_def topspace_prod_topology by blast - qed -qed - -lemma connectedin_Times: - "connectedin (prod_topology X Y) (S \ T) \ - S = {} \ T = {} \ connectedin X S \ connectedin Y T" - by (force simp: connectedin_def subtopology_Times connected_space_prod_topology) - subsection\The notion of "separated between" (complement of "connected between)"\ diff -r 2594319ad9ee -r 37894dff0111 src/HOL/Analysis/Abstract_Topology.thy --- a/src/HOL/Analysis/Abstract_Topology.thy Thu May 11 22:12:43 2023 +0200 +++ b/src/HOL/Analysis/Abstract_Topology.thy Mon May 15 17:12:18 2023 +0100 @@ -296,6 +296,10 @@ unfolding closedin_def topspace_subtopology by (auto simp: openin_subtopology) +lemma closedin_subset_topspace: + "\closedin X S; S \ T\ \ closedin (subtopology X T) S" + using closedin_subtopology by fastforce + lemma closedin_relative_to: "(closedin X relative_to S) = closedin (subtopology X S)" by (force simp: relative_to_def closedin_subtopology) @@ -3378,6 +3382,10 @@ qed qed +lemma connected_space_quotient_map_image: + "\quotient_map X X' q; connected_space X\ \ connected_space X'" + by (metis connectedin_continuous_map_image connectedin_topspace quotient_imp_continuous_map quotient_imp_surjective_map) + lemma homeomorphic_connected_space: "X homeomorphic_space Y \ connected_space X \ connected_space Y" unfolding homeomorphic_space_def homeomorphic_maps_def diff -r 2594319ad9ee -r 37894dff0111 src/HOL/Analysis/Abstract_Topology_2.thy --- a/src/HOL/Analysis/Abstract_Topology_2.thy Thu May 11 22:12:43 2023 +0200 +++ b/src/HOL/Analysis/Abstract_Topology_2.thy Mon May 15 17:12:18 2023 +0100 @@ -1639,4 +1639,53 @@ (\x. x / (1 + \x\)) (\y. y / (1 - \y\))" by (force simp: homeomorphic_maps_def continuous_map_real_shrink continuous_on_real_grow divide_simps) +lemma real_shrink_Galois: + fixes x::real + shows "(x / (1 + \x\) = y) \ (\y\ < 1 \ y / (1 - \y\) = x)" + using real_grow_shrink by (fastforce simp add: distrib_left) + +lemma real_shrink_lt: + fixes x::real + shows "x / (1 + \x\) < y / (1 + \y\) \ x < y" + using zero_less_mult_iff [of x y] by (auto simp: field_simps abs_if not_less) + +lemma real_shrink_le: + fixes x::real + shows "x / (1 + \x\) \ y / (1 + \y\) \ x \ y" + by (meson linorder_not_le real_shrink_lt) + +lemma real_shrink_grow: + fixes x::real + shows "\x\ < 1 \ x / (1 - \x\) / (1 + \x / (1 - \x\)\) = x" + using real_shrink_Galois by blast + +lemma continuous_shrink: + "continuous_on UNIV (\x::real. x / (1 + \x\))" + by (intro continuous_intros) auto + +lemma strict_mono_shrink: + "strict_mono (\x::real. x / (1 + \x\))" + by (simp add: monotoneI real_shrink_lt) + +lemma shrink_range: "(\x::real. x / (1 + \x\)) ` S \ {-1<..<1}" + by (auto simp: divide_simps) + +text \Note: connected sets of real numbers are the same thing as intervals\ +lemma connected_shrink: + fixes S :: "real set" + shows "connected ((\x. x / (1 + \x\)) ` S) \ connected S" (is "?lhs = ?rhs") +proof + assume "?lhs" + then have "connected ((\x. x / (1 - \x\)) ` (\x. x / (1 + \x\)) ` S)" + by (metis continuous_on_real_grow shrink_range connected_continuous_image + continuous_on_subset) + then show "?rhs" + using real_grow_shrink by (force simp add: image_comp) +next + assume ?rhs + then show ?lhs + using connected_continuous_image + by (metis continuous_on_subset continuous_shrink subset_UNIV) +qed + end \ No newline at end of file diff -r 2594319ad9ee -r 37894dff0111 src/HOL/Analysis/Elementary_Metric_Spaces.thy --- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Thu May 11 22:12:43 2023 +0200 +++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Mon May 15 17:12:18 2023 +0100 @@ -437,6 +437,9 @@ by (meson ball_subset_cball interior_subset mem_interior open_contains_cball open_interior subset_trans) +lemma ball_iff_cball: "(\r>0. ball x r \ U) \ (\r>0. cball x r \ U)" + by (meson mem_interior mem_interior_cball) + subsection \Frontier\ diff -r 2594319ad9ee -r 37894dff0111 src/HOL/Analysis/Locally.thy --- a/src/HOL/Analysis/Locally.thy Thu May 11 22:12:43 2023 +0200 +++ b/src/HOL/Analysis/Locally.thy Mon May 15 17:12:18 2023 +0100 @@ -2,7 +2,7 @@ theory Locally imports - Path_Connected Function_Topology + Path_Connected Function_Topology Sum_Topology begin subsection\Neighbourhood Bases\ @@ -448,4 +448,525 @@ using False by blast qed +lemma locally_path_connected_is_realinterval: + assumes "is_interval S" + shows "locally_path_connected_space(subtopology euclideanreal S)" + unfolding locally_path_connected_space_def +proof (clarsimp simp add: neighbourhood_base_of openin_subtopology_alt) + fix a U + assume "a \ S" and "a \ U" and "open U" + then obtain r where "r > 0" and r: "ball a r \ U" + by (metis open_contains_ball_eq) + show "\W. open W \ (\V. path_connectedin (top_of_set S) V \ a \ W \ S \ W \ V \ V \ S \ V \ U)" + proof (intro exI conjI) + show "path_connectedin (top_of_set S) (S \ ball a r)" + by (simp add: assms is_interval_Int is_interval_ball_real is_interval_path_connected path_connectedin_subtopology) + show "a \ ball a r" + by (simp add: \0 < r\) + qed (use \0 < r\ r in auto) +qed + +lemma locally_path_connected_real_interval: + "locally_path_connected_space (subtopology euclideanreal{a..b})" + "locally_path_connected_space (subtopology euclideanreal{a<.. + topspace (prod_topology X Y) = {} \ + locally_path_connected_space X \ locally_path_connected_space Y" (is "?lhs=?rhs") +proof (cases "topspace(prod_topology X Y) = {}") + case True + then show ?thesis + by (metis equals0D locally_path_connected_space_def neighbourhood_base_of_def) +next + case False + then have ne: "topspace X \ {}" "topspace Y \ {}" + by simp_all + show ?thesis + proof + assume ?lhs then show ?rhs + by (metis ne locally_path_connected_space_retraction_map_image retraction_map_fst retraction_map_snd) + next + assume ?rhs + with False have X: "locally_path_connected_space X" and Y: "locally_path_connected_space Y" + by auto + show ?lhs + unfolding locally_path_connected_space_def neighbourhood_base_of + proof clarify + fix UV x y + assume UV: "openin (prod_topology X Y) UV" and "(x,y) \ UV" + obtain A B where W12: "openin X A \ openin Y B \ x \ A \ y \ B \ A \ B \ UV" + using X Y by (metis UV \(x,y) \ UV\ openin_prod_topology_alt) + then obtain C D K L + where "openin X C" "path_connectedin X K" "x \ C" "C \ K" "K \ A" + "openin Y D" "path_connectedin Y L" "y \ D" "D \ L" "L \ B" + by (metis X Y locally_path_connected_space) + with W12 \openin X C\ \openin Y D\ + show "\U V. openin (prod_topology X Y) U \ path_connectedin (prod_topology X Y) V \ (x, y) \ U \ U \ V \ V \ UV" + apply (rule_tac x="C \ D" in exI) + apply (rule_tac x="K \ L" in exI) + apply (auto simp: openin_prod_Times_iff path_connectedin_Times) + done + qed + qed +qed + +lemma locally_path_connected_space_sum_topology: + "locally_path_connected_space(sum_topology X I) \ + (\i \ I. locally_path_connected_space (X i))" (is "?lhs=?rhs") +proof + assume ?lhs then show ?rhs + by (smt (verit) homeomorphic_locally_path_connected_space locally_path_connected_space_open_subset topological_property_of_sum_component) +next + assume R: ?rhs + show ?lhs + proof (clarsimp simp add: locally_path_connected_space_def neighbourhood_base_of forall_openin_sum_topology imp_conjL) + fix W i x + assume ope: "\i\I. openin (X i) (W i)" + and "i \ I" and "x \ W i" + then obtain U V where U: "openin (X i) U" and V: "path_connectedin (X i) V" + and "x \ U" "U \ V" "V \ W i" + by (metis R \i \ I\ \x \ W i\ locally_path_connected_space) + show "\U. openin (sum_topology X I) U \ (\V. path_connectedin (sum_topology X I) V \ (i, x) \ U \ U \ V \ V \ Sigma I W)" + proof (intro exI conjI) + show "openin (sum_topology X I) (Pair i ` U)" + by (meson U \i \ I\ open_map_component_injection open_map_def) + show "path_connectedin (sum_topology X I) (Pair i ` V)" + by (meson V \i \ I\ continuous_map_component_injection path_connectedin_continuous_map_image) + show "Pair i ` V \ Sigma I W" + using \V \ W i\ \i \ I\ by force + qed (use \x \ U\ \U \ V\ in auto) + qed +qed + + +subsection\Locally connected spaces\ + +definition weakly_locally_connected_at + where "weakly_locally_connected_at x X \ neighbourhood_base_at x (connectedin X) X" + +definition locally_connected_at + where "locally_connected_at x X \ + neighbourhood_base_at x (\U. openin X U \ connectedin X U ) X" + +definition locally_connected_space + where "locally_connected_space X \ neighbourhood_base_of (connectedin X) X" + + +lemma locally_connected_A: "(\U x. openin X U \ x \ U + \ openin X (connected_component_of_set (subtopology X U) x)) + \ neighbourhood_base_of (\U. openin X U \ connectedin X U) X" + by (smt (verit, best) connected_component_of_refl connectedin_connected_component_of connectedin_subtopology mem_Collect_eq neighbourhood_base_of openin_subset topspace_subtopology_subset) + +lemma locally_connected_B: "locally_connected_space X \ + (\U x. openin X U \ x \ U \ openin X (connected_component_of_set (subtopology X U) x))" + unfolding locally_connected_space_def neighbourhood_base_of + apply (erule all_forward) + apply clarify + apply (subst openin_subopen) + by (smt (verit, ccfv_threshold) Ball_Collect connected_component_of_def connected_component_of_equiv connectedin_subtopology in_mono mem_Collect_eq) + +lemma locally_connected_C: "neighbourhood_base_of (\U. openin X U \ connectedin X U) X \ locally_connected_space X" + using locally_connected_space_def neighbourhood_base_of_mono by auto + + +lemma locally_connected_space_alt: + "locally_connected_space X \ neighbourhood_base_of (\U. openin X U \ connectedin X U) X" + using locally_connected_A locally_connected_B locally_connected_C by blast + +lemma locally_connected_space_eq_open_connected_component_of: + "locally_connected_space X \ + (\U x. openin X U \ x \ U + \ openin X (connected_component_of_set (subtopology X U) x))" + by (meson locally_connected_A locally_connected_B locally_connected_C) + +lemma locally_connected_space: + "locally_connected_space X \ + (\V x. openin X V \ x \ V \ (\U. openin X U \ connectedin X U \ x \ U \ U \ V))" + by (simp add: locally_connected_space_alt open_neighbourhood_base_of) + +lemma locally_path_connected_imp_locally_connected_space: + "locally_path_connected_space X \ locally_connected_space X" + by (simp add: locally_connected_space_def locally_path_connected_space_def neighbourhood_base_of_mono path_connectedin_imp_connectedin) + +lemma locally_connected_space_open_connected_components: + "locally_connected_space X \ + (\U C. openin X U \ C \ connected_components_of(subtopology X U) \ openin X C)" + apply (simp add: locally_connected_space_eq_open_connected_component_of connected_components_of_def) + by (smt (verit) imageE image_eqI inf.orderE inf_commute openin_subset) + +lemma openin_connected_component_of_locally_connected_space: + "locally_connected_space X \ openin X (connected_component_of_set X x)" + by (metis connected_component_of_eq_empty locally_connected_space_eq_open_connected_component_of openin_empty openin_topspace subtopology_topspace) + +lemma openin_connected_components_of_locally_connected_space: + "\locally_connected_space X; C \ connected_components_of X\ \ openin X C" + by (metis locally_connected_space_open_connected_components openin_topspace subtopology_topspace) + +lemma weakly_locally_connected_at: + "weakly_locally_connected_at x X \ + (\V. openin X V \ x \ V + \ (\U. openin X U \ x \ U \ U \ V \ + (\y \ U. \C. connectedin X C \ C \ V \ x \ C \ y \ C)))" (is "?lhs=?rhs") +proof + assume ?lhs then show ?rhs + unfolding neighbourhood_base_at_def weakly_locally_connected_at_def + by (meson subsetD subset_trans) +next + assume R: ?rhs + show ?lhs + unfolding neighbourhood_base_at_def weakly_locally_connected_at_def + proof clarify + fix V + assume "openin X V" and "x \ V" + then obtain U where "openin X U" "x \ U" "U \ V" + and U: "\y\U. \C. connectedin X C \ C \ V \ x \ C \ y \ C" + using R by force + show "\A B. openin X A \ connectedin X B \ x \ A \ A \ B \ B \ V" + proof (intro conjI exI) + show "connectedin X (connected_component_of_set (subtopology X V) x)" + by (meson connectedin_connected_component_of connectedin_subtopology) + show "U \ connected_component_of_set (subtopology X V) x" + using connected_component_of_maximal U + by (simp add: connected_component_of_def connectedin_subtopology subsetI) + show "connected_component_of_set (subtopology X V) x \ V" + using connected_component_of_subset_topspace by fastforce + qed (auto simp: \x \ U\ \openin X U\) + qed +qed + +lemma locally_connected_space_iff_weak: + "locally_connected_space X \ (\x \ topspace X. weakly_locally_connected_at x X)" + by (simp add: locally_connected_space_def neighbourhood_base_of_def weakly_locally_connected_at_def) + +lemma locally_connected_space_im_kleinen: + "locally_connected_space X \ + (\V x. openin X V \ x \ V + \ (\U. openin X U \ x \ U \ U \ V \ + (\y \ U. \C. connectedin X C \ C \ V \ x \ C \ y \ C)))" + unfolding locally_connected_space_iff_weak weakly_locally_connected_at + using openin_subset subsetD by fastforce + +lemma locally_connected_space_open_subset: + "\locally_connected_space X; openin X S\ \ locally_connected_space (subtopology X S)" + apply (simp add: locally_connected_space_def) + by (smt (verit, ccfv_threshold) connectedin_subtopology neighbourhood_base_of openin_open_subtopology subset_trans) + +lemma locally_connected_space_quotient_map_image: + assumes X: "locally_connected_space X" and f: "quotient_map X Y f" + shows "locally_connected_space Y" + unfolding locally_connected_space_open_connected_components +proof clarify + fix V C + assume "openin Y V" and C: "C \ connected_components_of (subtopology Y V)" + then have "C \ topspace Y" + using connected_components_of_subset by force + have ope1: "openin X {a \ topspace X. f a \ V}" + using \openin Y V\ f openin_continuous_map_preimage quotient_imp_continuous_map by blast + define Vf where "Vf \ {z \ topspace X. f z \ V}" + have "openin X {x \ topspace X. f x \ C}" + proof (clarsimp simp: openin_subopen [where S = "{x \ topspace X. f x \ C}"]) + fix x + assume "x \ topspace X" and "f x \ C" + show "\T. openin X T \ x \ T \ T \ {x \ topspace X. f x \ C}" + proof (intro exI conjI) + show "openin X (connected_component_of_set (subtopology X Vf) x)" + by (metis Vf_def X connected_component_of_eq_empty locally_connected_B ope1 openin_empty + openin_subset topspace_subtopology_subset) + show x_in_conn: "x \ connected_component_of_set (subtopology X Vf) x" + using C Vf_def \f x \ C\ \x \ topspace X\ connected_component_of_refl connected_components_of_subset by fastforce + have "connected_component_of_set (subtopology X Vf) x \ topspace X \ Vf" + using connected_component_of_subset_topspace by fastforce + moreover + have "f ` connected_component_of_set (subtopology X Vf) x \ C" + proof (rule connected_components_of_maximal [where X = "subtopology Y V"]) + show "C \ connected_components_of (subtopology Y V)" + by (simp add: C) + have \
: "quotient_map (subtopology X Vf) (subtopology Y V) f" + by (simp add: Vf_def \openin Y V\ f quotient_map_restriction) + then show "connectedin (subtopology Y V) (f ` connected_component_of_set (subtopology X Vf) x)" + by (metis connectedin_connected_component_of connectedin_continuous_map_image quotient_imp_continuous_map) + show "\ disjnt C (f ` connected_component_of_set (subtopology X Vf) x)" + using \f x \ C\ x_in_conn by (auto simp: disjnt_iff) + qed + ultimately + show "connected_component_of_set (subtopology X Vf) x \ {x \ topspace X. f x \ C}" + by blast + qed + qed + then show "openin Y C" + using \C \ topspace Y\ f quotient_map_def by fastforce +qed + + +lemma locally_connected_space_retraction_map_image: + "\retraction_map X Y r; locally_connected_space X\ + \ locally_connected_space Y" + using locally_connected_space_quotient_map_image retraction_imp_quotient_map by blast + +lemma homeomorphic_locally_connected_space: + "X homeomorphic_space Y \ locally_connected_space X \ locally_connected_space Y" + by (meson homeomorphic_map_def homeomorphic_space homeomorphic_space_sym locally_connected_space_quotient_map_image) + +lemma locally_connected_space_euclideanreal: "locally_connected_space euclideanreal" + by (simp add: locally_path_connected_imp_locally_connected_space locally_path_connected_space_euclideanreal) + +lemma locally_connected_is_realinterval: + "is_interval S \ locally_connected_space(subtopology euclideanreal S)" + by (simp add: locally_path_connected_imp_locally_connected_space locally_path_connected_is_realinterval) + +lemma locally_connected_real_interval: + "locally_connected_space (subtopology euclideanreal{a..b})" + "locally_connected_space (subtopology euclideanreal{a<.. locally_connected_at x X" + by (simp add: locally_connected_at_def locally_path_connected_at_def neighbourhood_base_at_mono path_connectedin_imp_connectedin) + +lemma weakly_locally_path_connected_imp_weakly_locally_connected_at: + "weakly_locally_path_connected_at x X + \ weakly_locally_connected_at x X" + by (simp add: neighbourhood_base_at_mono path_connectedin_imp_connectedin weakly_locally_connected_at_def weakly_locally_path_connected_at_def) + + +lemma interior_of_locally_connected_subspace_component: + assumes X: "locally_connected_space X" + and C: "C \ connected_components_of (subtopology X S)" + shows "X interior_of C = C \ X interior_of S" +proof - + obtain Csub: "C \ topspace X" "C \ S" + by (meson C connectedin_connected_components_of connectedin_subset_topspace connectedin_subtopology) + show ?thesis + proof + show "X interior_of C \ C \ X interior_of S" + by (simp add: Csub interior_of_mono interior_of_subset) + have eq: "X interior_of S = \ (connected_components_of (subtopology X (X interior_of S)))" + by (metis Union_connected_components_of interior_of_subset_topspace topspace_subtopology_subset) + moreover have "C \ D \ X interior_of C" + if "D \ connected_components_of (subtopology X (X interior_of S))" for D + proof (cases "C \ D = {}") + case False + have "D \ X interior_of C" + proof (rule interior_of_maximal) + have "connectedin (subtopology X S) D" + by (meson connectedin_connected_components_of connectedin_subtopology interior_of_subset subset_trans that) + then show "D \ C" + by (meson C False connected_components_of_maximal disjnt_def) + show "openin X D" + using X locally_connected_space_open_connected_components openin_interior_of that by blast + qed + then show ?thesis + by blast + qed auto + ultimately show "C \ X interior_of S \ X interior_of C" + by blast + qed +qed + + +lemma frontier_of_locally_connected_subspace_component: + assumes X: "locally_connected_space X" and "closedin X S" + and C: "C \ connected_components_of (subtopology X S)" + shows "X frontier_of C = C \ X frontier_of S" +proof - + obtain Csub: "C \ topspace X" "C \ S" + by (meson C connectedin_connected_components_of connectedin_subset_topspace connectedin_subtopology) + then have "X closure_of C - X interior_of C = C \ X closure_of S - C \ X interior_of S" + using assms + apply (simp add: closure_of_closedin flip: interior_of_locally_connected_subspace_component) + by (metis closedin_connected_components_of closedin_trans_full closure_of_eq inf.orderE) + then show ?thesis + by (simp add: Diff_Int_distrib frontier_of_def) +qed + +(*Similar proof to locally_connected_space_prod_topology*) +lemma locally_connected_space_prod_topology: + "locally_connected_space (prod_topology X Y) \ + topspace (prod_topology X Y) = {} \ + locally_connected_space X \ locally_connected_space Y" (is "?lhs=?rhs") +proof (cases "topspace(prod_topology X Y) = {}") + case True + then show ?thesis + using locally_connected_space_iff_weak by force +next + case False + then have ne: "topspace X \ {}" "topspace Y \ {}" + by simp_all + show ?thesis + proof + assume ?lhs then show ?rhs + by (metis locally_connected_space_quotient_map_image ne quotient_map_fst quotient_map_snd) + next + assume ?rhs + with False have X: "locally_connected_space X" and Y: "locally_connected_space Y" + by auto + show ?lhs + unfolding locally_connected_space_def neighbourhood_base_of + proof clarify + fix UV x y + assume UV: "openin (prod_topology X Y) UV" and "(x,y) \ UV" + + obtain A B where W12: "openin X A \ openin Y B \ x \ A \ y \ B \ A \ B \ UV" + using X Y by (metis UV \(x,y) \ UV\ openin_prod_topology_alt) + then obtain C D K L + where "openin X C" "connectedin X K" "x \ C" "C \ K" "K \ A" + "openin Y D" "connectedin Y L" "y \ D" "D \ L" "L \ B" + by (metis X Y locally_connected_space) + with W12 \openin X C\ \openin Y D\ + show "\U V. openin (prod_topology X Y) U \ connectedin (prod_topology X Y) V \ (x, y) \ U \ U \ V \ V \ UV" + apply (rule_tac x="C \ D" in exI) + apply (rule_tac x="K \ L" in exI) + apply (auto simp: openin_prod_Times_iff connectedin_Times) + done + qed + qed +qed + +(*Same proof as locally_path_connected_space_product_topology*) +lemma locally_connected_space_product_topology: + "locally_connected_space(product_topology X I) \ + topspace(product_topology X I) = {} \ + finite {i. i \ I \ ~connected_space(X i)} \ + (\i \ I. locally_connected_space(X i))" + (is "?lhs \ ?empty \ ?rhs") +proof (cases ?empty) + case True + then show ?thesis + by (simp add: locally_connected_space_def neighbourhood_base_of openin_closedin_eq) +next + case False + then obtain z where z: "z \ (\\<^sub>E i\I. topspace (X i))" + by auto + have ?rhs if L: ?lhs + proof - + obtain U C where U: "openin (product_topology X I) U" + and V: "connectedin (product_topology X I) C" + and "z \ U" "U \ C" and Csub: "C \ (\\<^sub>E i\I. topspace (X i))" + using L apply (clarsimp simp add: locally_connected_space_def neighbourhood_base_of) + by (metis openin_topspace topspace_product_topology z) + then obtain V where finV: "finite {i \ I. V i \ topspace (X i)}" + and XV: "\i. i\I \ openin (X i) (V i)" and "z \ Pi\<^sub>E I V" and subU: "Pi\<^sub>E I V \ U" + by (force simp: openin_product_topology_alt) + show ?thesis + proof (intro conjI ballI) + have "connected_space (X i)" if "i \ I" "V i = topspace (X i)" for i + proof - + have pc: "connectedin (X i) ((\x. x i) ` C)" + apply (rule connectedin_continuous_map_image [OF _ V]) + by (simp add: continuous_map_product_projection \i \ I\) + moreover have "((\x. x i) ` C) = topspace (X i)" + proof + show "(\x. x i) ` C \ topspace (X i)" + by (simp add: pc connectedin_subset_topspace) + have "V i \ (\x. x i) ` (\\<^sub>E i\I. V i)" + by (metis \z \ Pi\<^sub>E I V\ empty_iff image_projection_PiE order_refl that(1)) + also have "\ \ (\x. x i) ` U" + using subU by blast + finally show "topspace (X i) \ (\x. x i) ` C" + using \U \ C\ that by blast + qed + ultimately show ?thesis + by (simp add: connectedin_topspace) + qed + then have "{i \ I. \ connected_space (X i)} \ {i \ I. V i \ topspace (X i)}" + by blast + with finV show "finite {i \ I. \ connected_space (X i)}" + using finite_subset by blast + next + show "locally_connected_space (X i)" if "i \ I" for i + by (meson False L locally_connected_space_quotient_map_image quotient_map_product_projection that) + qed + qed + moreover have ?lhs if R: ?rhs + proof (clarsimp simp add: locally_connected_space_def neighbourhood_base_of) + fix F z + assume "openin (product_topology X I) F" and "z \ F" + then obtain W where finW: "finite {i \ I. W i \ topspace (X i)}" + and opeW: "\i. i \ I \ openin (X i) (W i)" and "z \ Pi\<^sub>E I W" "Pi\<^sub>E I W \ F" + by (auto simp: openin_product_topology_alt) + have "\i \ I. \U C. openin (X i) U \ connectedin (X i) C \ z i \ U \ U \ C \ C \ W i \ + (W i = topspace (X i) \ + connected_space (X i) \ U = topspace (X i) \ C = topspace (X i))" + (is "\i \ I. ?\ i") + proof + fix i assume "i \ I" + have "locally_connected_space (X i)" + by (simp add: R \i \ I\) + moreover have "openin (X i) (W i) " "z i \ W i" + using \z \ Pi\<^sub>E I W\ opeW \i \ I\ by auto + ultimately obtain U C where UC: "openin (X i) U" "connectedin (X i) C" "z i \ U" "U \ C" "C \ W i" + using \i \ I\ by (force simp: locally_connected_space_def neighbourhood_base_of) + show "?\ i" + proof (cases "W i = topspace (X i) \ connected_space(X i)") + case True + then show ?thesis + using \z i \ W i\ connectedin_topspace by blast + next + case False + then show ?thesis + by (meson UC) + qed + qed + then obtain U C where + *: "\i. i \ I \ openin (X i) (U i) \ connectedin (X i) (C i) \ z i \ (U i) \ (U i) \ (C i) \ (C i) \ W i \ + (W i = topspace (X i) \ connected_space (X i) + \ (U i) = topspace (X i) \ (C i) = topspace (X i))" + by metis + let ?A = "{i \ I. \ connected_space (X i)} \ {i \ I. W i \ topspace (X i)}" + have "{i \ I. U i \ topspace (X i)} \ ?A" + by (clarsimp simp add: "*") + moreover have "finite ?A" + by (simp add: that finW) + ultimately have "finite {i \ I. U i \ topspace (X i)}" + using finite_subset by auto + then have "openin (product_topology X I) (Pi\<^sub>E I U)" + using * by (simp add: openin_PiE_gen) + then show "\U. openin (product_topology X I) U \ + (\V. connectedin (product_topology X I) V \ z \ U \ U \ V \ V \ F)" + apply (rule_tac x="PiE I U" in exI, simp) + apply (rule_tac x="PiE I C" in exI) + using \z \ Pi\<^sub>E I W\ \Pi\<^sub>E I W \ F\ * + apply (simp add: connectedin_PiE subset_PiE PiE_iff PiE_mono dual_order.trans) + done + qed + ultimately show ?thesis + using False by blast +qed + +lemma locally_connected_space_sum_topology: + "locally_connected_space(sum_topology X I) \ + (\i \ I. locally_connected_space (X i))" (is "?lhs=?rhs") +proof + assume ?lhs then show ?rhs + by (smt (verit) homeomorphic_locally_connected_space locally_connected_space_open_subset topological_property_of_sum_component) +next + assume R: ?rhs + show ?lhs + proof (clarsimp simp add: locally_connected_space_def neighbourhood_base_of forall_openin_sum_topology imp_conjL) + fix W i x + assume ope: "\i\I. openin (X i) (W i)" + and "i \ I" and "x \ W i" + then obtain U V where U: "openin (X i) U" and V: "connectedin (X i) V" + and "x \ U" "U \ V" "V \ W i" + by (metis R \i \ I\ \x \ W i\ locally_connected_space) + show "\U. openin (sum_topology X I) U \ (\V. connectedin (sum_topology X I) V \ (i,x) \ U \ U \ V \ V \ Sigma I W)" + proof (intro exI conjI) + show "openin (sum_topology X I) (Pair i ` U)" + by (meson U \i \ I\ open_map_component_injection open_map_def) + show "connectedin (sum_topology X I) (Pair i ` V)" + by (meson V \i \ I\ continuous_map_component_injection connectedin_continuous_map_image) + show "Pair i ` V \ Sigma I W" + using \V \ W i\ \i \ I\ by force + qed (use \x \ U\ \U \ V\ in auto) + qed +qed + + end diff -r 2594319ad9ee -r 37894dff0111 src/HOL/Analysis/Product_Topology.thy --- a/src/HOL/Analysis/Product_Topology.thy Thu May 11 22:12:43 2023 +0200 +++ b/src/HOL/Analysis/Product_Topology.thy Mon May 15 17:12:18 2023 +0100 @@ -576,5 +576,68 @@ by (metis prod.collapse) qed +proposition connected_space_prod_topology: + "connected_space(prod_topology X Y) \ + topspace(prod_topology X Y) = {} \ connected_space X \ connected_space Y" (is "?lhs=?rhs") +proof (cases "topspace(prod_topology X Y) = {}") + case True + then show ?thesis + using connected_space_topspace_empty by blast +next + case False + then have nonempty: "topspace X \ {}" "topspace Y \ {}" + by force+ + show ?thesis + proof + assume ?lhs + then show ?rhs + by (meson connected_space_quotient_map_image nonempty quotient_map_fst quotient_map_snd) + next + assume ?rhs + then have conX: "connected_space X" and conY: "connected_space Y" + using False by blast+ + have False + if "openin (prod_topology X Y) U" and "openin (prod_topology X Y) V" + and UV: "topspace X \ topspace Y \ U \ V" "U \ V = {}" + and "U \ {}" and "V \ {}" + for U V + proof - + have Usub: "U \ topspace X \ topspace Y" and Vsub: "V \ topspace X \ topspace Y" + using that by (metis openin_subset topspace_prod_topology)+ + obtain a b where ab: "(a,b) \ U" and a: "a \ topspace X" and b: "b \ topspace Y" + using \U \ {}\ Usub by auto + have "\ topspace X \ topspace Y \ U" + using Usub Vsub \U \ V = {}\ \V \ {}\ by auto + then obtain x y where x: "x \ topspace X" and y: "y \ topspace Y" and "(x,y) \ U" + by blast + have oX: "openin X {x \ topspace X. (x,y) \ U}" "openin X {x \ topspace X. (x,y) \ V}" + and oY: "openin Y {y \ topspace Y. (a,y) \ U}" "openin Y {y \ topspace Y. (a,y) \ V}" + by (force intro: openin_continuous_map_preimage [where Y = "prod_topology X Y"] + simp: that continuous_map_pairwise o_def x y a)+ + have 1: "topspace Y \ {y \ topspace Y. (a,y) \ U} \ {y \ topspace Y. (a,y) \ V}" + using a that(3) by auto + have 2: "{y \ topspace Y. (a,y) \ U} \ {y \ topspace Y. (a,y) \ V} = {}" + using that(4) by auto + have 3: "{y \ topspace Y. (a,y) \ U} \ {}" + using ab b by auto + have 4: "{y \ topspace Y. (a,y) \ V} \ {}" + proof - + show ?thesis + using connected_spaceD [OF conX oX] UV \(x,y) \ U\ a x y + disjoint_iff_not_equal by blast + qed + show ?thesis + using connected_spaceD [OF conY oY 1 2 3 4] by auto + qed + then show ?lhs + unfolding connected_space_def topspace_prod_topology by blast + qed +qed + +lemma connectedin_Times: + "connectedin (prod_topology X Y) (S \ T) \ + S = {} \ T = {} \ connectedin X S \ connectedin Y T" + by (force simp: connectedin_def subtopology_Times connected_space_prod_topology) + end diff -r 2594319ad9ee -r 37894dff0111 src/HOL/Analysis/Starlike.thy --- a/src/HOL/Analysis/Starlike.thy Thu May 11 22:12:43 2023 +0200 +++ b/src/HOL/Analysis/Starlike.thy Mon May 15 17:12:18 2023 +0100 @@ -882,6 +882,11 @@ convex_rel_interior_closure[of S] assms by auto +lemma open_subset_closure_of_interval: + assumes "open U" "is_interval S" + shows "U \ closure S \ U \ interior S" + by (metis assms convex_interior_closure is_interval_convex open_subset_interior) + lemma closure_eq_rel_interior_eq: fixes S1 S2 :: "'n::euclidean_space set" assumes "convex S1" diff -r 2594319ad9ee -r 37894dff0111 src/HOL/Analysis/Sum_Topology.thy --- a/src/HOL/Analysis/Sum_Topology.thy Thu May 11 22:12:43 2023 +0200 +++ b/src/HOL/Analysis/Sum_Topology.thy Mon May 15 17:12:18 2023 +0100 @@ -143,4 +143,20 @@ by (metis injective_open_imp_embedding_map continuous_map_component_injection open_map_component_injection inj_onI prod.inject) +lemma topological_property_of_sum_component: + assumes major: "P (sum_topology X I)" + and minor: "\X S. \P X; closedin X S; openin X S\ \ P(subtopology X S)" + and PQ: "\X Y. X homeomorphic_space Y \ (P X \ Q Y)" + shows "(\i \ I. Q(X i))" +proof - + have "Q(X i)" if "i \ I" for i + proof - + have "P(subtopology (sum_topology X I) (Pair i ` topspace (X i)))" + by (meson closed_map_component_injection closed_map_def closedin_topspace major minor open_map_component_injection open_map_def openin_topspace that) + then show ?thesis + by (metis PQ embedding_map_component_injection embedding_map_imp_homeomorphic_space homeomorphic_space_sym that) + qed + then show ?thesis by metis +qed + end