# HG changeset patch # User paulson # Date 1688399197 -3600 # Node ID 1260be3f33a4359108ef63d87d322506d2c9d782 # Parent d4125fc10c0c2ef42494a2197a6cf689873b8b50# Parent 740b23f1138a4cb339ba1f60a04b695510ee188b merged diff -r d4125fc10c0c -r 1260be3f33a4 src/HOL/Analysis/Abstract_Metric_Spaces.thy --- a/src/HOL/Analysis/Abstract_Metric_Spaces.thy Sun Jul 02 20:41:07 2023 +0200 +++ b/src/HOL/Analysis/Abstract_Metric_Spaces.thy Mon Jul 03 16:46:37 2023 +0100 @@ -2645,7 +2645,7 @@ lemma continuous_map_uniform_limit_alt: assumes contf: "\\<^sub>F \ in F. continuous_map X mtopology (f \)" - and gim: "g ` (topspace X) \ M" + and gim: "g \ topspace X \ M" and dfg: "\\. 0 < \ \ \\<^sub>F \ in F. \x \ topspace X. d (f \ x) (g x) < \" and nontriv: "\ trivial_limit F" shows "continuous_map X mtopology g" @@ -2653,7 +2653,7 @@ fix \ :: real assume "\ > 0" with gim dfg show "\\<^sub>F \ in F. \x\topspace X. g x \ M \ d (f \ x) (g x) < \" - by (simp add: image_subset_iff) + by (simp add: Pi_iff) qed (use nontriv in auto) @@ -2800,14 +2800,16 @@ lemma completely_metrizable_space_cbox: "completely_metrizable_space (top_of_set (cbox a b))" using closed_closedin completely_metrizable_space_closedin completely_metrizable_space_euclidean by blast + lemma homeomorphic_completely_metrizable_space_aux: assumes homXY: "X homeomorphic_space Y" and X: "completely_metrizable_space X" shows "completely_metrizable_space Y" proof - obtain f g where hmf: "homeomorphic_map X Y f" and hmg: "homeomorphic_map Y X g" - and fg: "(\x \ topspace X. g(f x) = x) \ (\y \ topspace Y. f(g y) = y)" - and fim: "f ` (topspace X) = topspace Y" and gim: "g ` (topspace Y) = topspace X" - by (smt (verit, best) homXY homeomorphic_imp_surjective_map homeomorphic_maps_map homeomorphic_space_def) + and fg: "\x. x \ topspace X \ g(f x) = x" "\y. y \ topspace Y \ f(g y) = y" + and fim: "f \ topspace X \ topspace Y" and gim: "g \ topspace Y \ topspace X" + using homXY + using homeomorphic_space_unfold by blast obtain M d where Md: "Metric_space M d" "Metric_space.mcomplete M d" and Xeq: "X = Metric_space.mtopology M d" using X by (auto simp: completely_metrizable_space_def) then interpret MX: Metric_space M d by metis @@ -2816,7 +2818,7 @@ proof show "(D x y = 0) \ (x = y)" if "x \ topspace Y" "y \ topspace Y" for x y unfolding D_def - by (metis that MX.topspace_mtopology MX.zero Xeq fg gim imageI) + by (metis that MX.topspace_mtopology MX.zero Xeq fg gim Pi_iff) show "D x z \ D x y +D y z" if "x \ topspace Y" "y \ topspace Y" "z \ topspace Y" for x y z using that MX.triangle Xeq gim by (auto simp: D_def) @@ -2828,8 +2830,8 @@ show "Metric_space (topspace Y) D" using MY.Metric_space_axioms by blast have gball: "g ` MY.mball y r = MX.mball (g y) r" if "y \ topspace Y" for y r - using that MX.topspace_mtopology Xeq gim - unfolding MX.mball_def MY.mball_def by (auto simp: subset_iff image_iff D_def) + using that MX.topspace_mtopology Xeq gim hmg homeomorphic_imp_surjective_map + unfolding MX.mball_def MY.mball_def by (fastforce simp: D_def) have "\r>0. MY.mball y r \ S" if "openin Y S" and "y \ S" for S y proof - have "openin X (g`S)" @@ -3783,16 +3785,16 @@ definition Lipschitz_continuous_map where "Lipschitz_continuous_map \ - \m1 m2 f. f ` mspace m1 \ mspace m2 \ + \m1 m2 f. f \ mspace m1 \ mspace m2 \ (\B. \x \ mspace m1. \y \ mspace m1. mdist m2 (f x) (f y) \ B * mdist m1 x y)" lemma Lipschitz_continuous_map_image: - "Lipschitz_continuous_map m1 m2 f \ f ` mspace m1 \ mspace m2" + "Lipschitz_continuous_map m1 m2 f \ f \ mspace m1 \ mspace m2" by (simp add: Lipschitz_continuous_map_def) lemma Lipschitz_continuous_map_pos: "Lipschitz_continuous_map m1 m2 f \ - f ` mspace m1 \ mspace m2 \ + f \ mspace m1 \ mspace m2 \ (\B>0. \x \ mspace m1. \y \ mspace m1. mdist m2 (f x) (f y) \ B * mdist m1 x y)" proof - have "B * mdist m1 x y \ (\B\ + 1) * mdist m1 x y" "\B\ + 1 > 0" for x y B @@ -3805,15 +3807,14 @@ lemma Lipschitz_continuous_map_eq: assumes "Lipschitz_continuous_map m1 m2 f" "\x. x \ mspace m1 \ f x = g x" shows "Lipschitz_continuous_map m1 m2 g" - using Lipschitz_continuous_map_def assms - by (metis (no_types, opaque_lifting) image_subset_iff) + using Lipschitz_continuous_map_def assms by (simp add: Lipschitz_continuous_map_pos Pi_iff) lemma Lipschitz_continuous_map_from_submetric: assumes "Lipschitz_continuous_map m1 m2 f" shows "Lipschitz_continuous_map (submetric m1 S) m2 f" unfolding Lipschitz_continuous_map_def proof - show "f ` mspace (submetric m1 S) \ mspace m2" + show "f \ mspace (submetric m1 S) \ mspace m2" using Lipschitz_continuous_map_pos assms by fastforce qed (use assms in \fastforce simp: Lipschitz_continuous_map_def\) @@ -3824,37 +3825,36 @@ lemma Lipschitz_continuous_map_into_submetric: "Lipschitz_continuous_map m1 (submetric m2 S) f \ - f ` mspace m1 \ S \ Lipschitz_continuous_map m1 m2 f" + f \ mspace m1 \ S \ Lipschitz_continuous_map m1 m2 f" by (auto simp: Lipschitz_continuous_map_def) lemma Lipschitz_continuous_map_const: "Lipschitz_continuous_map m1 m2 (\x. c) \ mspace m1 = {} \ c \ mspace m2" - unfolding Lipschitz_continuous_map_def image_subset_iff + unfolding Lipschitz_continuous_map_def Pi_iff by (metis all_not_in_conv mdist_nonneg mdist_zero mult_1) lemma Lipschitz_continuous_map_id: "Lipschitz_continuous_map m1 m1 (\x. x)" - by (metis Lipschitz_continuous_map_def image_ident mult_1 order_refl) + unfolding Lipschitz_continuous_map_def by (metis funcset_id mult_1 order_refl) lemma Lipschitz_continuous_map_compose: assumes f: "Lipschitz_continuous_map m1 m2 f" and g: "Lipschitz_continuous_map m2 m3 g" shows "Lipschitz_continuous_map m1 m3 (g \ f)" - unfolding Lipschitz_continuous_map_def image_subset_iff + unfolding Lipschitz_continuous_map_def proof - show "\x\mspace m1. (g \ f) x \ mspace m3" - by (metis Lipschitz_continuous_map_def assms comp_apply image_subset_iff) + show "g \ f \ mspace m1 \ mspace m3" + by (smt (verit, best) Lipschitz_continuous_map_image Pi_iff comp_apply f g) obtain B where B: "\x\mspace m1. \y\mspace m1. mdist m2 (f x) (f y) \ B * mdist m1 x y" using assms unfolding Lipschitz_continuous_map_def by presburger obtain C where "C>0" and C: "\x\mspace m2. \y\mspace m2. mdist m3 (g x) (g y) \ C * mdist m2 x y" using assms unfolding Lipschitz_continuous_map_pos by metis show "\B. \x\mspace m1. \y\mspace m1. mdist m3 ((g \ f) x) ((g \ f) y) \ B * mdist m1 x y" - apply (rule_tac x="C*B" in exI) - proof clarify + proof (intro strip exI) fix x y assume \
: "x \ mspace m1" "y \ mspace m1" then have "mdist m3 ((g \ f) x) ((g \ f) y) \ C * mdist m2 (f x) (f y)" - by (metis C Lipschitz_continuous_map_def f comp_apply image_subset_iff) + using C Lipschitz_continuous_map_image f by fastforce also have "\ \ C * B * mdist m1 x y" by (simp add: "\
" B \0 < C\) finally show "mdist m3 ((g \ f) x) ((g \ f) y) \ C * B * mdist m1 x y" . @@ -3865,12 +3865,12 @@ definition uniformly_continuous_map where "uniformly_continuous_map \ - \m1 m2 f. f ` mspace m1 \ mspace m2 \ + \m1 m2 f. f \ mspace m1 \ mspace m2 \ (\\>0. \\>0. \x \ mspace m1. \y \ mspace m1. mdist m1 y x < \ \ mdist m2 (f y) (f x) < \)" -lemma uniformly_continuous_map_image: - "uniformly_continuous_map m1 m2 f \ f ` mspace m1 \ mspace m2" +lemma uniformly_continuous_map_funspace: + "uniformly_continuous_map m1 m2 f \ f \ mspace m1 \ mspace m2" by (simp add: uniformly_continuous_map_def) lemma ucmap_A: @@ -3898,7 +3898,7 @@ assumes \
: "\\ \ \. \\ > 0; range \ \ mspace m1; range \ \ mspace m1; ((\n. mdist m1 (\ n) (\ n)) \ 0)\ \ \n. mdist m2 (f (\ n)) (f (\ n)) < \" - and fim: "f ` mspace m1 \ mspace m2" + and fim: "f \ mspace m1 \ mspace m2" shows "uniformly_continuous_map m1 m2 f" proof - {assume "\ (\\>0. \\>0. \x\mspace m1. \y\mspace m1. mdist m1 y x < \ \ mdist m2 (f y) (f x) < \)" @@ -3921,13 +3921,13 @@ lemma uniformly_continuous_map_sequentially: "uniformly_continuous_map m1 m2 f \ - f ` mspace m1 \ mspace m2 \ + f \ mspace m1 \ mspace m2 \ (\\ \. range \ \ mspace m1 \ range \ \ mspace m1 \ (\n. mdist m1 (\ n) (\ n)) \ 0 \ (\n. mdist m2 (f (\ n)) (f (\ n))) \ 0)" (is "?lhs \ ?rhs") proof show "?lhs \ ?rhs" - by (simp add: ucmap_A uniformly_continuous_map_image) + by (simp add: ucmap_A uniformly_continuous_map_funspace) show "?rhs \ ?lhs" by (intro ucmap_B ucmap_C) auto qed @@ -3935,14 +3935,14 @@ lemma uniformly_continuous_map_sequentially_alt: "uniformly_continuous_map m1 m2 f \ - f ` mspace m1 \ mspace m2 \ + f \ mspace m1 \ mspace m2 \ (\\>0. \\ \. range \ \ mspace m1 \ range \ \ mspace m1 \ ((\n. mdist m1 (\ n) (\ n)) \ 0) \ (\n. mdist m2 (f (\ n)) (f (\ n)) < \))" (is "?lhs \ ?rhs") proof show "?lhs \ ?rhs" - using uniformly_continuous_map_image by (intro conjI strip ucmap_B | force simp: ucmap_A)+ + using uniformly_continuous_map_funspace by (intro conjI strip ucmap_B | fastforce simp: ucmap_A)+ show "?rhs \ ?lhs" by (intro ucmap_C) auto qed @@ -3951,14 +3951,14 @@ lemma uniformly_continuous_map_eq: "\\x. x \ mspace m1 \ f x = g x; uniformly_continuous_map m1 m2 f\ \ uniformly_continuous_map m1 m2 g" - by (simp add: uniformly_continuous_map_def) + by (simp add: uniformly_continuous_map_def Pi_iff) lemma uniformly_continuous_map_from_submetric: assumes "uniformly_continuous_map m1 m2 f" shows "uniformly_continuous_map (submetric m1 S) m2 f" unfolding uniformly_continuous_map_def proof - show "f ` mspace (submetric m1 S) \ mspace m2" + show "f \ mspace (submetric m1 S) \ mspace m2" using assms by (auto simp: uniformly_continuous_map_def) qed (use assms in \force simp: uniformly_continuous_map_def\) @@ -3969,23 +3969,23 @@ lemma uniformly_continuous_map_into_submetric: "uniformly_continuous_map m1 (submetric m2 S) f \ - f ` mspace m1 \ S \ uniformly_continuous_map m1 m2 f" + f \ mspace m1 \ S \ uniformly_continuous_map m1 m2 f" by (auto simp: uniformly_continuous_map_def) lemma uniformly_continuous_map_const: "uniformly_continuous_map m1 m2 (\x. c) \ mspace m1 = {} \ c \ mspace m2" - unfolding uniformly_continuous_map_def image_subset_iff + unfolding uniformly_continuous_map_def Pi_iff by (metis empty_iff equals0I mdist_zero) lemma uniformly_continuous_map_id [simp]: "uniformly_continuous_map m1 m1 (\x. x)" - by (metis image_ident order_refl uniformly_continuous_map_def) + by (metis funcset_id uniformly_continuous_map_def) lemma uniformly_continuous_map_compose: assumes f: "uniformly_continuous_map m1 m2 f" and g: "uniformly_continuous_map m2 m3 g" shows "uniformly_continuous_map m1 m3 (g \ f)" - by (smt (verit, ccfv_threshold) comp_apply f g image_subset_iff uniformly_continuous_map_def) + by (smt (verit, ccfv_threshold) comp_apply f g Pi_iff uniformly_continuous_map_def) lemma uniformly_continuous_map_real_const [simp]: "uniformly_continuous_map m euclidean_metric (\x. c)" @@ -4009,9 +4009,9 @@ = Cauchy_continuous_on S f" by (auto simp add: Cauchy_continuous_map_def Cauchy_continuous_on_def Cauchy_def Met_TC.subspace Metric_space.MCauchy_def) -lemma Cauchy_continuous_map_image: +lemma Cauchy_continuous_map_funspace: assumes "Cauchy_continuous_map m1 m2 f" - shows "f ` mspace m1 \ mspace m2" + shows "f \ mspace m1 \ mspace m2" proof clarsimp fix x assume "x \ mspace m1" @@ -4042,14 +4042,14 @@ lemma Cauchy_continuous_map_into_submetric: "Cauchy_continuous_map m1 (submetric m2 S) f \ - f ` mspace m1 \ S \ Cauchy_continuous_map m1 m2 f" (is "?lhs \ ?rhs") + f \ mspace m1 \ S \ Cauchy_continuous_map m1 m2 f" (is "?lhs \ ?rhs") proof - have "?lhs \ Cauchy_continuous_map m1 m2 f" by (simp add: Cauchy_continuous_map_def Metric_space.MCauchy_def [OF Metric_space_mspace_mdist]) moreover have "?rhs \ ?lhs" - by (bestsimp simp add: Cauchy_continuous_map_def Metric_space.MCauchy_def [OF Metric_space_mspace_mdist]) + by (auto simp: Cauchy_continuous_map_def Metric_space.MCauchy_def [OF Metric_space_mspace_mdist]) ultimately show ?thesis - by (metis Cauchy_continuous_map_image le_inf_iff mspace_submetric) + by (metis Cauchy_continuous_map_funspace Int_iff funcsetI funcset_mem mspace_submetric) qed lemma Cauchy_continuous_map_const [simp]: @@ -4060,7 +4060,7 @@ moreover have "c \ mspace m2 \ Cauchy_continuous_map m1 m2 (\x. c)" by (simp add: Cauchy_continuous_map_def o_def Metric_space.MCauchy_const [OF Metric_space_mspace_mdist]) ultimately show ?thesis - using Cauchy_continuous_map_image by blast + using Cauchy_continuous_map_funspace by blast qed lemma Cauchy_continuous_map_id [simp]: @@ -4076,7 +4076,7 @@ assumes "Lipschitz_continuous_map m1 m2 f" shows "uniformly_continuous_map m1 m2 f" proof - - have "f ` mspace m1 \ mspace m2" + have "f \ mspace m1 \ mspace m2" by (simp add: Lipschitz_continuous_map_image assms) moreover have "\\>0. \x\mspace m1. \y\mspace m1. mdist m1 y x < \ \ mdist m2 (f y) (f x) < \" if "\ > 0" for \ @@ -4097,7 +4097,7 @@ "uniformly_continuous_map m1 m2 f \ Cauchy_continuous_map m1 m2 f" unfolding uniformly_continuous_map_def Cauchy_continuous_map_def apply (simp add: image_subset_iff o_def Metric_space.MCauchy_def [OF Metric_space_mspace_mdist]) - by meson + by (metis funcset_mem) lemma locally_Cauchy_continuous_map: assumes "\ > 0" @@ -4137,7 +4137,7 @@ then have "\ n \ mball_of m1 (\ n) \" by (simp add: Metric_space.centre_in_mball_iff Metric_space_mspace_mdist assms(1) mball_of_def) then show "(f \ \) n \ mspace m2" - using Cauchy_continuous_map_image [OF \
[of "\ n"]] \\ n \ mspace m1\ by auto + using Cauchy_continuous_map_funspace [OF \
[of "\ n"]] \\ n \ mspace m1\ by auto qed qed @@ -4154,7 +4154,7 @@ unfolding limit_atin_sequentially proof (intro conjI strip) show "f x \ M2" - using Cauchy_continuous_map_image \x \ M1\ assms by fastforce + using Cauchy_continuous_map_funspace \x \ M1\ assms by fastforce fix \ assume "range \ \ M1 - {x} \ limitin M1.mtopology \ x sequentially" then have "M1.MCauchy (\n. if even n then \ (n div 2) else x)" @@ -4221,8 +4221,8 @@ shows "uniformly_continuous_map m1 m2 f" unfolding uniformly_continuous_map_sequentially_alt imp_conjL proof (intro conjI strip) - show "f ` mspace m1 \ mspace m2" - by (simp add: Cauchy_continuous_map_image f) + show "f \ mspace m1 \ mspace m2" + by (simp add: Cauchy_continuous_map_funspace f) interpret M1: Metric_space "mspace m1" "mdist m1" by (simp add: Metric_space_mspace_mdist) interpret M2: Metric_space "mspace m2" "mdist m2" @@ -4286,7 +4286,7 @@ lemma Lipschitz_continuous_map_projections: "Lipschitz_continuous_map (prod_metric m1 m2) m1 fst" "Lipschitz_continuous_map (prod_metric m1 m2) m2 snd" - by (simp add: Lipschitz_continuous_map_def prod_dist_def; + by (simp add: Lipschitz_continuous_map_def prod_dist_def fst_Pi snd_Pi; metis mult_numeral_1 real_sqrt_sum_squares_ge1 real_sqrt_sum_squares_ge2)+ lemma Lipschitz_continuous_map_pairwise: @@ -4308,11 +4308,11 @@ show ?thesis unfolding Lipschitz_continuous_map_pos proof (intro exI conjI strip) - have f1im: "f1 ` mspace m \ mspace m1" + have f1im: "f1 \ mspace m \ mspace m1" by (simp add: Lipschitz_continuous_map_image f1) - moreover have f2im: "f2 ` mspace m \ mspace m2" + moreover have f2im: "f2 \ mspace m \ mspace m2" by (simp add: Lipschitz_continuous_map_image f2) - ultimately show "(\x. (f1 x, f2 x)) ` mspace m \ mspace (prod_metric m1 m2)" + ultimately show "(\x. (f1 x, f2 x)) \ mspace m \ mspace (prod_metric m1 m2)" by auto show "B1+B2 > 0" using \0 < B1\ \0 < B2\ by linarith @@ -4343,11 +4343,11 @@ show ?thesis unfolding uniformly_continuous_map_def proof (intro conjI strip) - have f1im: "f1 ` mspace m \ mspace m1" - by (simp add: uniformly_continuous_map_image f1) - moreover have f2im: "f2 ` mspace m \ mspace m2" - by (simp add: uniformly_continuous_map_image f2) - ultimately show "(\x. (f1 x, f2 x)) ` mspace m \ mspace (prod_metric m1 m2)" + have f1im: "f1 \ mspace m \ mspace m1" + by (simp add: uniformly_continuous_map_funspace f1) + moreover have f2im: "f2 \ mspace m \ mspace m2" + by (simp add: uniformly_continuous_map_funspace f2) + ultimately show "(\x. (f1 x, f2 x)) \ mspace m \ mspace (prod_metric m1 m2)" by auto fix \:: real assume "\ > 0" @@ -4402,9 +4402,9 @@ assumes f: "Lipschitz_continuous_map m1 m2 f" and S: "Metric_space.mbounded (mspace m1) (mdist m1) S" shows "Metric_space.mbounded (mspace m2) (mdist m2) (f`S)" proof - - obtain B where fim: "f ` mspace m1 \ mspace m2" + obtain B where fim: "f \ mspace m1 \ mspace m2" and "B>0" and B: "\x y. \x \ mspace m1; y \ mspace m1\ \ mdist m2 (f x) (f y) \ B * mdist m1 x y" - by (meson Lipschitz_continuous_map_pos f) + by (metis Lipschitz_continuous_map_pos f) show ?thesis unfolding Metric_space.mbounded_alt_pos [OF Metric_space_mspace_mdist] proof @@ -4429,7 +4429,7 @@ have "S \ mspace m1" using S by (simp add: Metric_space.mtotally_bounded_sequentially[OF Metric_space_mspace_mdist]) then show "f ` S \ mspace m2" - using Cauchy_continuous_map_image f by blast + using Cauchy_continuous_map_funspace f by blast fix \ :: "nat \ 'b" assume "range \ \ f ` S" then have "\n. \x. \ n = f x \ x \ S" @@ -4448,11 +4448,11 @@ lemma Lipschitz_coefficient_pos: assumes "x \ mspace m" "y \ mspace m" "f x \ f y" - and "f ` mspace m \ mspace m2" + and "f \ mspace m \ mspace m2" and "\x y. \x \ mspace m; y \ mspace m\ \ mdist m2 (f x) (f y) \ k * mdist m x y" shows "0 < k" - using assms by (smt (verit, best) image_subset_iff mdist_nonneg mdist_zero mult_nonpos_nonneg) + using assms by (smt (verit, best) Pi_iff mdist_nonneg mdist_zero mult_nonpos_nonneg) lemma Lipschitz_continuous_map_metric: "Lipschitz_continuous_map (prod_metric m m) euclidean_metric (\(x,y). mdist m x y)" @@ -4563,7 +4563,7 @@ subsection \Isometries\ lemma (in Metric_space12) isometry_imp_embedding_map: - assumes fim: "f ` M1 \ M2" and d: "\x y. \x \ M1; y \ M1\ \ d2 (f x) (f y) = d1 x y" + assumes fim: "f \ M1 \ M2" and d: "\x y. \x \ M1; y \ M1\ \ d2 (f x) (f y) = d1 x y" shows "embedding_map M1.mtopology M2.mtopology f" proof - have "inj_on f M1" @@ -4574,7 +4574,10 @@ unfolding homeomorphic_maps_def proof (intro conjI; clarsimp) show "continuous_map M1.mtopology (subtopology M2.mtopology (f ` M1)) f" - by (metis M1.metric_continuous_map M1.topspace_mtopology M2.Metric_space_axioms continuous_map_into_subtopology d fim order_refl) + proof (rule continuous_map_into_subtopology) + show "continuous_map M1.mtopology M2.mtopology f" + by (metis M1.metric_continuous_map M2.Metric_space_axioms d fim image_subset_iff_funcset) + qed simp have "Lipschitz_continuous_map (submetric (metric(M2,d2)) (f ` M1)) (metric(M1,d1)) g" unfolding Lipschitz_continuous_map_def proof (intro conjI exI strip; simp) @@ -4595,7 +4598,8 @@ lemma (in Metric_space12) isometry_imp_homeomorphic_map: assumes fim: "f ` M1 = M2" and d: "\x y. \x \ M1; y \ M1\ \ d2 (f x) (f y) = d1 x y" shows "homeomorphic_map M1.mtopology M2.mtopology f" - by (metis M1.topspace_mtopology M2.subtopology_mspace d embedding_map_def fim isometry_imp_embedding_map subsetI) + by (metis image_eqI M1.topspace_mtopology M2.subtopology_mspace d embedding_map_def fim isometry_imp_embedding_map Pi_iff) + subsection\"Capped" equivalent bounded metrics and general product metrics\ definition (in Metric_space) capped_dist where @@ -5132,6 +5136,5 @@ "locally_connected_space(Euclidean_space n)" by (simp add: locally_path_connected_Euclidean_space locally_path_connected_imp_locally_connected_space) - end diff -r d4125fc10c0c -r 1260be3f33a4 src/HOL/Analysis/Abstract_Topological_Spaces.thy --- a/src/HOL/Analysis/Abstract_Topological_Spaces.thy Sun Jul 02 20:41:07 2023 +0200 +++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy Mon Jul 03 16:46:37 2023 +0100 @@ -1819,13 +1819,13 @@ qed moreover { assume R: ?rhs - then have fgim: "f ` topspace X \ topspace X'" "g ` topspace Y \ topspace Y'" + then have fgim: "f \ topspace X \ topspace X'" "g \ topspace Y \ topspace Y'" and cm: "closed_map X X' f" "closed_map Y Y' g" by (auto simp: proper_map_def closed_map_imp_subset_topspace) have "closed_map (prod_topology X Y) (prod_topology X' Y') h" unfolding closed_map_fibre_neighbourhood imp_conjL proof (intro conjI strip) - show "h ` topspace (prod_topology X Y) \ topspace (prod_topology X' Y')" + show "h \ topspace (prod_topology X Y) \ topspace (prod_topology X' Y')" unfolding h_def using fgim by auto fix W w assume W: "openin (prod_topology X Y) W" @@ -1960,7 +1960,7 @@ "\perfect_map X Z (g \ f); f ` topspace X = topspace Y; continuous_map X Y f; continuous_map Y Z g; inj_on g (topspace Y)\ \ perfect_map X Y f" - by (meson continuous_map_image_subset_topspace perfect_map_def proper_map_from_composition_right_inj) + by (meson continuous_map_openin_preimage_eq perfect_map_def proper_map_from_composition_right_inj) subsection \Regular spaces\ @@ -2285,7 +2285,7 @@ fix C assume "closedin Z C" then have "C \ topspace Z" by (simp add: closedin_subset) - have "f ` topspace Z \ topspace X" "g ` topspace Z \ topspace Y" + have "f \ topspace Z \ topspace X" "g \ topspace Z \ topspace Y" by (simp_all add: assms closed_map_imp_subset_topspace) show "closedin (prod_topology X Y) ((\x. (f x, g x)) ` C)" unfolding closedin_def topspace_prod_topology @@ -2293,7 +2293,7 @@ have "closedin Y (g ` C)" using \closedin Z C\ assms(3) closed_map_def by blast with assms show "(\x. (f x, g x)) ` C \ topspace X \ topspace Y" - using \C \ topspace Z\ \f ` topspace Z \ topspace X\ continuous_map_closedin subsetD by fastforce + by (smt (verit) SigmaI \closedin Z C\ closed_map_def closedin_subset image_subset_iff) have *: "\T. openin (prod_topology X Y) T \ (y1,y2) \ T \ T \ topspace X \ topspace Y - (\x. (f x, g x)) ` C" if "(y1,y2) \ (\x. (f x, g x)) ` C" and y1: "y1 \ topspace X" and y2: "y2 \ topspace Y" for y1 y2 @@ -5157,7 +5157,7 @@ qed lemma closed_map_into_k_space: - assumes "k_space Y" and fim: "f ` (topspace X) \ topspace Y" + assumes "k_space Y" and fim: "f \ (topspace X) \ topspace Y" and f: "\K. compactin Y K \ closed_map(subtopology X {x \ topspace X. f x \ K}) (subtopology Y K) f" shows "closed_map X Y f" @@ -5176,13 +5176,13 @@ qed then show "closedin Y (f ` C)" using \k_space Y\ unfolding k_space - by (meson \closedin X C\ closedin_subset dual_order.trans fim image_mono) + by (meson \closedin X C\ closedin_subset order.trans fim funcset_image subset_image_iff) qed text \Essentially the same proof\ lemma open_map_into_k_space: - assumes "k_space Y" and fim: "f ` (topspace X) \ topspace Y" + assumes "k_space Y" and fim: "f \ (topspace X) \ topspace Y" and f: "\K. compactin Y K \ open_map (subtopology X {x \ topspace X. f x \ K}) (subtopology Y K) f" shows "open_map X Y f" @@ -5201,7 +5201,7 @@ qed then show "openin Y (f ` C)" using \k_space Y\ unfolding k_space_open - by (meson \openin X C\ openin_subset dual_order.trans fim image_mono) + by (meson \openin X C\ openin_subset order.trans fim funcset_image subset_image_iff) qed lemma quotient_map_into_k_space: @@ -5255,7 +5255,7 @@ lemma open_map_into_k_space_eq: assumes "k_space Y" shows "open_map X Y f \ - f ` (topspace X) \ topspace Y \ + f \ (topspace X) \ topspace Y \ (\k. compactin Y k \ open_map (subtopology X {x \ topspace X. f x \ k}) (subtopology Y k) f)" (is "?lhs=?rhs") @@ -5269,7 +5269,7 @@ lemma closed_map_into_k_space_eq: assumes "k_space Y" shows "closed_map X Y f \ - f ` (topspace X) \ topspace Y \ + f \ (topspace X) \ topspace Y \ (\k. compactin Y k \ closed_map (subtopology X {x \ topspace X. f x \ k}) (subtopology Y k) f)" (is "?lhs \ ?rhs") @@ -5281,7 +5281,7 @@ qed lemma proper_map_into_k_space: - assumes "k_space Y" and fim: "f ` (topspace X) \ topspace Y" + assumes "k_space Y" and fim: "f \ (topspace X) \ topspace Y" and f: "\K. compactin Y K \ proper_map (subtopology X {x \ topspace X. f x \ K}) (subtopology Y K) f" @@ -5297,7 +5297,7 @@ lemma proper_map_into_k_space_eq: assumes "k_space Y" shows "proper_map X Y f \ - f ` (topspace X) \ topspace Y \ + f \ (topspace X) \ topspace Y \ (\K. compactin Y K \ proper_map (subtopology X {x \ topspace X. f x \ K}) (subtopology Y K) f)" (is "?lhs \ ?rhs") @@ -5305,11 +5305,11 @@ show "?lhs \ ?rhs" by (simp add: proper_map_imp_subset_topspace proper_map_restriction) show "?rhs \ ?lhs" - by (simp add: assms proper_map_into_k_space) + by (simp add: assms funcset_image proper_map_into_k_space) qed lemma compact_imp_proper_map: - assumes "k_space Y" "kc_space Y" and fim: "f ` (topspace X) \ topspace Y" + assumes "k_space Y" "kc_space Y" and fim: "f \ (topspace X) \ topspace Y" and f: "continuous_map X Y f \ kc_space X" and comp: "\K. compactin Y K \ compactin X {x \ topspace X. f x \ K}" shows "proper_map X Y f" @@ -5325,12 +5325,12 @@ assumes "k_space Y" "kc_space Y" and f: "continuous_map X Y f \ kc_space X" shows "proper_map X Y f \ - f ` (topspace X) \ topspace Y \ + f \ (topspace X) \ topspace Y \ (\K. compactin Y K \ compactin X {x \ topspace X. f x \ K})" (is "?lhs \ ?rhs") proof show "?lhs \ ?rhs" - by (simp add: proper_map_alt proper_map_imp_subset_topspace) + using \k_space Y\ compactin_proper_map_preimage proper_map_into_k_space_eq by blast qed (use assms compact_imp_proper_map in auto) lemma compact_imp_perfect_map: @@ -5338,7 +5338,7 @@ and "continuous_map X Y f" and "\K. compactin Y K \ compactin X {x \ topspace X. f x \ K}" shows "perfect_map X Y f" - by (simp add: assms compact_imp_proper_map perfect_map_def) + by (simp add: assms compact_imp_proper_map perfect_map_def flip: image_subset_iff_funcset) end diff -r d4125fc10c0c -r 1260be3f33a4 src/HOL/Analysis/Abstract_Topology.thy --- a/src/HOL/Analysis/Abstract_Topology.thy Sun Jul 02 20:41:07 2023 +0200 +++ b/src/HOL/Analysis/Abstract_Topology.thy Mon Jul 03 16:46:37 2023 +0100 @@ -1703,24 +1703,24 @@ lemma continuous_map_from_subtopology: - "continuous_map X X' f \ continuous_map (subtopology X S) X' f" + "continuous_map X Y f \ continuous_map (subtopology X S) Y f" by (auto simp: continuous_map openin_subtopology) lemma continuous_map_into_fulltopology: - "continuous_map X (subtopology X' T) f \ continuous_map X X' f" + "continuous_map X (subtopology Y T) f \ continuous_map X Y f" by (auto simp: continuous_map_in_subtopology) lemma continuous_map_into_subtopology: - "\continuous_map X X' f; f ` topspace X \ T\ \ continuous_map X (subtopology X' T) f" + "\continuous_map X Y f; f \ topspace X \ T\ \ continuous_map X (subtopology Y T) f" by (auto simp: continuous_map_in_subtopology) lemma continuous_map_from_subtopology_mono: - "\continuous_map (subtopology X T) X' f; S \ T\ - \ continuous_map (subtopology X S) X' f" + "\continuous_map (subtopology X T) Y f; S \ T\ + \ continuous_map (subtopology X S) Y f" by (metis inf.absorb_iff2 continuous_map_from_subtopology subtopology_subtopology) lemma continuous_map_from_discrete_topology [simp]: - "continuous_map (discrete_topology U) X f \ f ` U \ topspace X" + "continuous_map (discrete_topology U) X f \ f \ U \ topspace X" by (auto simp: continuous_map_def) lemma continuous_map_iff_continuous [simp]: "continuous_map (top_of_set S) euclidean g = continuous_on S g" @@ -1731,12 +1731,12 @@ lemma continuous_map_openin_preimage_eq: "continuous_map X Y f \ - f ` (topspace X) \ topspace Y \ (\U. openin Y U \ openin X (topspace X \ f -` U))" + f \ (topspace X) \ topspace Y \ (\U. openin Y U \ openin X (topspace X \ f -` U))" by (auto simp: continuous_map_def vimage_def Int_def) lemma continuous_map_closedin_preimage_eq: "continuous_map X Y f \ - f ` (topspace X) \ topspace Y \ (\U. closedin Y U \ closedin X (topspace X \ f -` U))" + f \ (topspace X) \ topspace Y \ (\U. closedin Y U \ closedin X (topspace X \ f -` U))" by (auto simp: continuous_map_closedin vimage_def Int_def) lemma continuous_map_square_root: "continuous_map euclideanreal euclideanreal sqrt" @@ -1759,7 +1759,7 @@ lemma\<^marker>\tag important\ continuous_map_alt: "continuous_map T1 T2 f - = ((\U. openin T2 U \ openin T1 (f -` U \ topspace T1)) \ f ` topspace T1 \ topspace T2)" + = ((\U. openin T2 U \ openin T1 (f -` U \ topspace T1)) \ f \ topspace T1 \ topspace T2)" by (auto simp: continuous_map_def vimage_def image_def Collect_conj_eq inf_commute) lemma continuous_map_open [intro]: @@ -1782,8 +1782,8 @@ where "closed_map X1 X2 f \ \U. closedin X1 U \ closedin X2 (f ` U)" lemma open_map_imp_subset_topspace: - "open_map X1 X2 f \ f ` (topspace X1) \ topspace X2" - unfolding open_map_def by (simp add: openin_subset) + "open_map X1 X2 f \ f \ (topspace X1) \ topspace X2" + unfolding open_map_def using openin_subset by fastforce lemma open_map_on_empty: "topspace X = {} \ open_map X Y f" @@ -1798,8 +1798,8 @@ by (metis closed_map_def closed_map_on_empty closedin_empty closedin_topspace image_constant_conv) lemma open_map_imp_subset: - "\open_map X1 X2 f; S \ topspace X1\ \ f ` S \ topspace X2" - by (meson order_trans open_map_imp_subset_topspace subset_image_iff) + "\open_map X1 X2 f; S \ topspace X1\ \ f \ S \ topspace X2" + using open_map_imp_subset_topspace by fastforce lemma topology_finer_open_id: "(\S. openin X S \ openin X' S) \ open_map X X' id" @@ -1826,11 +1826,11 @@ by (metis (no_types, lifting) image_comp open_map_def) lemma closed_map_imp_subset_topspace: - "closed_map X1 X2 f \ f ` (topspace X1) \ topspace X2" - by (simp add: closed_map_def closedin_subset) + "closed_map X1 X2 f \ f \ (topspace X1) \ topspace X2" + by (simp add: closed_map_def closedin_def image_subset_iff_funcset) lemma closed_map_imp_subset: - "\closed_map X1 X2 f; S \ topspace X1\ \ f ` S \ topspace X2" + "\closed_map X1 X2 f; S \ topspace X1\ \ f \ S \ topspace X2" using closed_map_imp_subset_topspace by blast lemma topology_finer_closed_id: @@ -1863,21 +1863,21 @@ by (simp add: closed_map_inclusion_eq closedin_Int) lemma open_map_into_subtopology: - "\open_map X X' f; f ` topspace X \ S\ \ open_map X (subtopology X' S) f" + "\open_map X X' f; f \ topspace X \ S\ \ open_map X (subtopology X' S) f" unfolding open_map_def openin_subtopology using openin_subset by fastforce lemma closed_map_into_subtopology: - "\closed_map X X' f; f ` topspace X \ S\ \ closed_map X (subtopology X' S) f" + "\closed_map X X' f; f \ topspace X \ S\ \ closed_map X (subtopology X' S) f" unfolding closed_map_def closedin_subtopology using closedin_subset by fastforce lemma open_map_into_discrete_topology: - "open_map X (discrete_topology U) f \ f ` (topspace X) \ U" + "open_map X (discrete_topology U) f \ f \ (topspace X) \ U" unfolding open_map_def openin_discrete_topology using openin_subset by blast lemma closed_map_into_discrete_topology: - "closed_map X (discrete_topology U) f \ f ` (topspace X) \ U" + "closed_map X (discrete_topology U) f \ f \ (topspace X) \ U" unfolding closed_map_def closedin_discrete_topology using closedin_subset by blast lemma bijective_open_imp_closed_map: @@ -1930,8 +1930,8 @@ lemma closed_map_closure_of_image: "closed_map X Y f \ - f ` topspace X \ topspace Y \ - (\S. S \ topspace X \ Y closure_of (f ` S) \ image f (X closure_of S))" (is "?lhs=?rhs") + f \ topspace X \ topspace Y \ + (\S. S \ topspace X \ Y closure_of (f ` S) \ f ` (X closure_of S))" (is "?lhs=?rhs") proof assume ?lhs then show ?rhs @@ -1953,12 +1953,12 @@ lemma open_map_interior_of_image_subset_gen: "open_map X Y f \ - (f ` topspace X \ topspace Y \ (\S. f ` (X interior_of S) \ Y interior_of f ` S))" - by (meson open_map_imp_subset_topspace open_map_interior_of_image_subset) + (f \ topspace X \ topspace Y \ (\S. f ` (X interior_of S) \ Y interior_of f ` S))" + by (metis open_map_imp_subset_topspace open_map_interior_of_image_subset) lemma open_map_preimage_neighbourhood: "open_map X Y f \ - (f ` topspace X \ topspace Y \ + (f \ topspace X \ topspace Y \ (\U T. closedin X U \ T \ topspace Y \ {x \ topspace X. f x \ T} \ U \ (\V. closedin Y V \ T \ V \ {x \ topspace X. f x \ V} \ U)))" (is "?lhs=?rhs") @@ -1966,7 +1966,7 @@ assume L: ?lhs show ?rhs proof (intro conjI strip) - show "f ` topspace X \ topspace Y" + show "f \ topspace X \ topspace Y" by (simp add: \open_map X Y f\ open_map_imp_subset_topspace) next fix U T @@ -2000,7 +2000,7 @@ lemma closed_map_preimage_neighbourhood: "closed_map X Y f \ - image f (topspace X) \ topspace Y \ + f \ topspace X \ topspace Y \ (\U T. openin X U \ T \ topspace Y \ {x \ topspace X. f x \ T} \ U \ (\V. openin Y V \ T \ V \ @@ -2009,7 +2009,7 @@ assume L: ?lhs show ?rhs proof (intro conjI strip) - show "f ` topspace X \ topspace Y" + show "f \ topspace X \ topspace Y" by (simp add: L closed_map_imp_subset_topspace) next fix U T @@ -2042,13 +2042,13 @@ lemma closed_map_fibre_neighbourhood: "closed_map X Y f \ - f ` (topspace X) \ topspace Y \ + f \ (topspace X) \ topspace Y \ (\U y. openin X U \ y \ topspace Y \ {x \ topspace X. f x = y} \ U \ (\V. openin Y V \ y \ V \ {x \ topspace X. f x \ V} \ U))" unfolding closed_map_preimage_neighbourhood proof (intro conj_cong refl all_cong1) fix U - assume "f ` topspace X \ topspace Y" + assume "f \ topspace X \ topspace Y" show "(\T. openin X U \ T \ topspace Y \ {x \ topspace X. f x \ T} \ U \ (\V. openin Y V \ T \ V \ {x \ topspace X. f x \ V} \ U)) = (\y. openin X U \ y \ topspace Y \ {x \ topspace X. f x = y} \ U @@ -2083,8 +2083,8 @@ lemma open_map_in_subtopology: "openin Y S - \ (open_map X (subtopology Y S) f \ open_map X Y f \ f ` (topspace X) \ S)" - by (metis le_inf_iff open_map_def open_map_imp_subset_topspace open_map_into_subtopology openin_trans_full topspace_subtopology) + \ open_map X (subtopology Y S) f \ open_map X Y f \ f \ topspace X \ S" + by (metis image_subset_iff_funcset open_map_def open_map_into_subtopology openin_imp_subset openin_topspace openin_trans_full) lemma open_map_from_open_subtopology: "\openin Y S; open_map X (subtopology Y S) f\ \ open_map X Y f" @@ -2092,7 +2092,7 @@ lemma closed_map_in_subtopology: "closedin Y S - \ closed_map X (subtopology Y S) f \ (closed_map X Y f \ f ` topspace X \ S)" + \ closed_map X (subtopology Y S) f \ (closed_map X Y f \ f \ topspace X \ S)" by (metis closed_map_def closed_map_imp_subset_topspace closed_map_into_subtopology closedin_closed_subtopology closedin_subset topspace_subtopology_subset) @@ -2138,7 +2138,7 @@ qed lemma closed_map_from_composition_right: - assumes cmf: "closed_map X Z (g \ f)" "f ` topspace X \ topspace Y" "continuous_map Y Z g" "inj_on g (topspace Y)" + assumes cmf: "closed_map X Z (g \ f)" "f \ topspace X \ topspace Y" "continuous_map Y Z g" "inj_on g (topspace Y)" shows "closed_map X Y f" unfolding closed_map_def proof (intro strip) @@ -2156,7 +2156,7 @@ text \identical proof as the above\ lemma open_map_from_composition_right: - assumes "open_map X Z (g \ f)" "f ` topspace X \ topspace Y" "continuous_map Y Z g" "inj_on g (topspace Y)" + assumes "open_map X Z (g \ f)" "f \ topspace X \ topspace Y" "continuous_map Y Z g" "inj_on g (topspace Y)" shows "open_map X Y f" unfolding open_map_def proof (intro strip) @@ -2733,8 +2733,8 @@ by (simp add: homeomorphic_eq_everything_map) lemma homeomorphic_imp_surjective_map: - "homeomorphic_map X Y f \ f ` (topspace X) = topspace Y" - by (simp add: homeomorphic_eq_everything_map) + "homeomorphic_map X Y f \ f ` topspace X = topspace Y" + using homeomorphic_eq_everything_map by fastforce lemma homeomorphic_imp_injective_map: "homeomorphic_map X Y f \ inj_on f (topspace X)" @@ -2899,13 +2899,13 @@ lemma all_openin_homeomorphic_image: assumes "homeomorphic_map X Y f" - shows "(\V. openin Y V \ P V) \ (\U. openin X U \ P(f ` U))" - by (metis (no_types, lifting) assms homeomorphic_imp_surjective_map homeomorphic_map_openness openin_subset subset_image_iff) + shows "(\V. openin Y V \ P V) \ (\U. openin X U \ P(f ` U))" + by (metis (no_types, lifting) assms homeomorphic_eq_everything_map homeomorphic_map_openness openin_subset subset_image_iff) lemma all_closedin_homeomorphic_image: assumes "homeomorphic_map X Y f" - shows "(\V. closedin Y V \ P V) \ (\U. closedin X U \ P(f ` U))" (is "?lhs = ?rhs") - by (metis (no_types, lifting) assms homeomorphic_imp_surjective_map homeomorphic_map_closedness closedin_subset subset_image_iff) + shows "(\V. closedin Y V \ P V) \ (\U. closedin X U \ P(f ` U))" + by (metis (no_types, lifting) assms closedin_subset homeomorphic_eq_everything_map homeomorphic_map_closedness subset_image_iff) lemma homeomorphic_map_derived_set_of: @@ -3059,7 +3059,7 @@ lemma homeomorphic_empty_space: "X homeomorphic_space Y \ topspace X = {} \ topspace Y = {}" - by (metis homeomorphic_imp_surjective_map homeomorphic_space image_is_empty) + by (metis homeomorphic_eq_everything_map homeomorphic_space image_is_empty) lemma homeomorphic_empty_space_eq: assumes "topspace X = {}" @@ -3067,6 +3067,14 @@ unfolding homeomorphic_maps_def homeomorphic_space_def by (metis assms continuous_map_on_empty continuous_map_closedin ex_in_conv) +lemma homeomorphic_space_unfold: + assumes "X homeomorphic_space Y" + obtains f g where "homeomorphic_map X Y f" "homeomorphic_map Y X g" + and "\x. x \ topspace X \ g(f x) = x" "\y. y \ topspace Y \ f(g y) = y" + and "f \ topspace X \ topspace Y" "g \ topspace Y \ topspace X" + using assms unfolding homeomorphic_space_def homeomorphic_maps_map + by (smt (verit, best) Pi_I homeomorphic_imp_surjective_map image_eqI) + subsection\Connected topological spaces\ definition connected_space :: "'a topology \ bool" where @@ -3923,9 +3931,9 @@ have hm: "homeomorphic_map X (subtopology X' (f ` topspace X)) f" "homeomorphic_map X' (subtopology X'' (g ` topspace X')) g" using assms by (auto simp: embedding_map_def) then obtain C where "g ` topspace X' \ C = (g \ f) ` topspace X" - by (metis homeomorphic_imp_surjective_map image_comp image_mono inf.absorb_iff2 topspace_subtopology) + using continuous_map_image_subset_topspace homeomorphic_imp_continuous_map by fastforce then have "homeomorphic_map (subtopology X' (f ` topspace X)) (subtopology X'' ((g \ f) ` topspace X)) g" - by (metis hm homeomorphic_imp_surjective_map homeomorphic_map_subtopologies image_comp subtopology_subtopology topspace_subtopology) + by (metis hm homeomorphic_eq_everything_map homeomorphic_map_subtopologies image_comp subtopology_subtopology topspace_subtopology) then show ?thesis unfolding embedding_map_def using hm(1) homeomorphic_map_compose by blast @@ -3945,14 +3953,15 @@ lemma injective_open_imp_embedding_map: "\continuous_map X Y f; open_map X Y f; inj_on f (topspace X)\ \ embedding_map X Y f" - unfolding embedding_map_def - by (simp add: continuous_map_in_subtopology continuous_open_quotient_map eq_iff homeomorphic_map_def open_map_imp_subset open_map_into_subtopology) + unfolding embedding_map_def homeomorphic_map_def + by (simp add: image_subset_iff_funcset continuous_map_in_subtopology continuous_open_quotient_map eq_iff + open_map_imp_subset open_map_into_subtopology) lemma injective_closed_imp_embedding_map: "\continuous_map X Y f; closed_map X Y f; inj_on f (topspace X)\ \ embedding_map X Y f" - unfolding embedding_map_def + unfolding embedding_map_def homeomorphic_map_def by (simp add: closed_map_imp_subset closed_map_into_subtopology continuous_closed_quotient_map - continuous_map_in_subtopology dual_order.eq_iff homeomorphic_map_def) + continuous_map_in_subtopology dual_order.eq_iff image_subset_iff_funcset) lemma embedding_map_imp_homeomorphic_space: "embedding_map X Y f \ X homeomorphic_space (subtopology Y (f ` (topspace X)))" @@ -4098,7 +4107,7 @@ lemma continuous_map_euclidean_top_of_set: assumes eq: "f -` S = UNIV" and cont: "continuous_on UNIV f" shows "continuous_map euclidean (top_of_set S) f" - by (simp add: cont continuous_map_into_subtopology eq image_subset_iff_subset_vimage) + by (simp add: cont continuous_map_in_subtopology eq image_subset_iff_subset_vimage) subsection\<^marker>\tag unimportant\ \Half-global and completely global cases\ @@ -4256,36 +4265,32 @@ qed lemma continuous_on_open_gen: - assumes "f ` S \ T" + assumes "f \ S \ T" shows "continuous_on S f \ (\U. openin (top_of_set T) U \ openin (top_of_set S) (S \ f -` U))" (is "?lhs = ?rhs") proof assume ?lhs - then show ?rhs - by (clarsimp simp add: continuous_openin_preimage_eq openin_open) - (metis Int_assoc assms image_subset_iff_subset_vimage inf.absorb_iff1) + with assms show ?rhs + apply (simp add: Pi_iff continuous_openin_preimage_eq openin_open) + by (metis inf.orderE inf_assoc subsetI vimageI vimage_Int) next assume R [rule_format]: ?rhs show ?lhs proof (clarsimp simp add: continuous_openin_preimage_eq) - fix U::"'a set" - assume "open U" - then have "openin (top_of_set S) (S \ f -` (U \ T))" - by (metis R inf_commute openin_open) - then show "openin (top_of_set S) (S \ f -` U)" - by (metis Int_assoc Int_commute assms image_subset_iff_subset_vimage inf.absorb_iff2 vimage_Int) + show "\T. open T \ openin (top_of_set S) (S \ f -` T)" + by (metis (no_types) R assms image_subset_iff_funcset image_subset_iff_subset_vimage inf.orderE inf_assoc openin_open_Int vimage_Int) qed qed lemma continuous_openin_preimage: - "\continuous_on S f; f ` S \ T; openin (top_of_set T) U\ + "\continuous_on S f; f \ S \ T; openin (top_of_set T) U\ \ openin (top_of_set S) (S \ f -` U)" by (simp add: continuous_on_open_gen) lemma continuous_on_closed_gen: - assumes "f ` S \ T" + assumes "f \ S \ T" shows "continuous_on S f \ (\U. closedin (top_of_set T) U \ closedin (top_of_set S) (S \ f -` U))" @@ -4298,7 +4303,7 @@ qed lemma continuous_closedin_preimage_gen: - assumes "continuous_on S f" "f ` S \ T" "closedin (top_of_set T) U" + assumes "continuous_on S f" "f \ S \ T" "closedin (top_of_set T) U" shows "closedin (top_of_set S) (S \ f -` U)" using assms continuous_on_closed_gen by blast @@ -4825,7 +4830,7 @@ by (simp add: proper_map_def) lemma proper_map_imp_subset_topspace: - "proper_map X Y f \ f ` (topspace X) \ topspace Y" + "proper_map X Y f \ f \ (topspace X) \ topspace Y" by (simp add: closed_map_imp_subset_topspace proper_map_def) lemma proper_map_restriction: @@ -4868,7 +4873,7 @@ assumes f: "proper_map X Y f" and "compactin Y K" shows "compactin X {x. x \ topspace X \ f x \ K}" proof - - have "f ` (topspace X) \ topspace Y" + have "f \ (topspace X) \ topspace Y" by (simp add: f proper_map_imp_subset_topspace) have *: "\y. y \ topspace Y \ compactin X {x \ topspace X. f x = y}" using f by (auto simp: proper_map_def) @@ -5009,7 +5014,7 @@ by (metis closed_Int_compactin closed_map_inclusion_eq inf.absorb_iff2 inj_on_id injective_imp_proper_eq_closed_map) lemma proper_map_into_subtopology: - "\proper_map X Y f; f ` topspace X \ C\ \ proper_map X (subtopology Y C) f" + "\proper_map X Y f; f \ topspace X \ C\ \ proper_map X (subtopology Y C) f" by (simp add: closed_map_into_subtopology compactin_subtopology proper_map_alt) lemma proper_map_from_composition_left: @@ -5031,7 +5036,7 @@ qed lemma proper_map_from_composition_right_inj: - assumes gf: "proper_map X Z (g \ f)" and fim: "f ` topspace X \ topspace Y" + assumes gf: "proper_map X Z (g \ f)" and fim: "f \ topspace X \ topspace Y" and contf: "continuous_map Y Z g" and inj: "inj_on g (topspace Y)" shows "proper_map X Y f" unfolding proper_map_def @@ -5041,7 +5046,7 @@ fix y assume "y \ topspace Y" with fim inj have eq: "{x \ topspace X. f x = y} = {x \ topspace X. (g \ f) x = g y}" - by (auto simp: image_subset_iff inj_onD) + by (auto simp: Pi_iff inj_onD) show "compactin X {x \ topspace X. f x = y}" unfolding eq by (smt (verit) Collect_cong \y \ topspace Y\ contf continuous_map_closedin gf proper_map_def) diff -r d4125fc10c0c -r 1260be3f33a4 src/HOL/Analysis/Abstract_Topology_2.thy --- a/src/HOL/Analysis/Abstract_Topology_2.thy Sun Jul 02 20:41:07 2023 +0200 +++ b/src/HOL/Analysis/Abstract_Topology_2.thy Mon Jul 03 16:46:37 2023 +0100 @@ -575,7 +575,7 @@ subsection\<^marker>\tag unimportant\\Quotient maps\ lemma quotient_map_imp_continuous_open: - assumes T: "f ` S \ T" + assumes T: "f \ S \ T" and ope: "\U. U \ T \ (openin (top_of_set S) (S \ f -` U) \ openin (top_of_set T) U)" @@ -587,7 +587,7 @@ qed lemma quotient_map_imp_continuous_closed: - assumes T: "f ` S \ T" + assumes T: "f \ S \ T" and ope: "\U. U \ T \ (closedin (top_of_set S) (S \ f -` U) \ closedin (top_of_set T) U)" @@ -635,8 +635,8 @@ qed lemma continuous_right_inverse_imp_quotient_map: - assumes contf: "continuous_on S f" and imf: "f ` S \ T" - and contg: "continuous_on T g" and img: "g ` T \ S" + assumes contf: "continuous_on S f" and imf: "f \ S \ T" + and contg: "continuous_on T g" and img: "g \ T \ S" and fg [simp]: "\y. y \ T \ f(g y) = y" and U: "U \ T" shows "openin (top_of_set S) (S \ f -` U) \ @@ -657,13 +657,13 @@ finally have eq: "T \ g -` (g ` T \ (S \ f -` U)) = U" . assume ?lhs then have *: "openin (top_of_set (g ` T)) (g ` T \ (S \ f -` U))" - by (meson img openin_Int openin_subtopology_Int_subset openin_subtopology_self) + by (meson img openin_Int openin_subtopology_Int_subset openin_subtopology_self image_subset_iff_funcset) show ?rhs using g [OF *] eq by auto next assume rhs: ?rhs show ?lhs - by (metis f fg image_eqI image_subset_iff imf img openin_subopen openin_subtopology_self openin_trans rhs) + using assms continuous_openin_preimage rhs by blast qed qed @@ -696,7 +696,7 @@ shows "continuous_map X Y g" unfolding continuous_map_openin_preimage_eq proof (intro conjI allI impI) - show "g ` topspace X \ topspace Y" + show "g \ topspace X \ topspace Y" using g cont continuous_map_image_subset_topspace by fastforce next fix U @@ -737,7 +737,7 @@ shows "continuous_map X Y g" unfolding continuous_map_closedin_preimage_eq proof (intro conjI allI impI) - show "g ` topspace X \ topspace Y" + show "g \ topspace X \ topspace Y" using g cont continuous_map_image_subset_topspace by fastforce next fix U @@ -885,7 +885,7 @@ definition\<^marker>\tag important\ retraction :: "('a::topological_space) set \ 'a set \ ('a \ 'a) \ bool" where "retraction S T r \ - T \ S \ continuous_on S r \ r ` S \ T \ (\x\T. r x = x)" + T \ S \ continuous_on S r \ r \ S \ T \ (\x\T. r x = x)" definition\<^marker>\tag important\ retract_of (infixl "retract'_of" 50) where "T retract_of S \ (\r. retraction S T r)" @@ -899,20 +899,20 @@ fixes S :: "'a::topological_space set" and T :: "'b::topological_space set" assumes contt: "continuous_on T i" - and "i ` T \ S" + and "i \ T \ S" and contr: "continuous_on S r" - and "r ` S \ T" + and "r \ S \ T" and ri: "\y. y \ T \ r (i y) = y" - and FP: "\f. \continuous_on S f; f ` S \ S\ \ \x\S. f x = x" + and FP: "\f. \continuous_on S f; f \ S \ S\ \ \x\S. f x = x" and contg: "continuous_on T g" - and "g ` T \ T" + and "g \ T \ T" obtains y where "y \ T" and "g y = y" proof - have "\x\S. (i \ g \ r) x = x" proof (rule FP) show "continuous_on S (i \ g \ r)" - by (meson contt contr assms(4) contg assms(8) continuous_on_compose continuous_on_subset) - show "(i \ g \ r) ` S \ S" + by (metis assms(4) assms(8) contg continuous_on_compose continuous_on_subset contr contt funcset_image) + show "(i \ g \ r) \ S \ S" using assms(2,4,8) by force qed then obtain x where x: "x \ S" "(i \ g \ r) x = x" .. @@ -928,8 +928,8 @@ fixes S :: "'a::topological_space set" and T :: "'b::topological_space set" assumes "S homeomorphic T" - shows "(\f. continuous_on S f \ f ` S \ S \ (\x\S. f x = x)) \ - (\g. continuous_on T g \ g ` T \ T \ (\y\T. g y = y))" + shows "(\f. continuous_on S f \ f \ S \ S \ (\x\S. f x = x)) \ + (\g. continuous_on T g \ g \ T \ T \ (\y\T. g y = y))" (is "?lhs = ?rhs") proof - obtain r i where r: @@ -940,11 +940,11 @@ proof assume ?lhs with r show ?rhs - by (metis invertible_fixpoint_property[of T i S r] order_refl) + by (smt (verit, del_insts) Pi_iff image_eqI invertible_fixpoint_property[of T i S r]) next assume ?rhs with r show ?lhs - by (metis invertible_fixpoint_property[of S r T i] order_refl) + by (smt (verit, del_insts) Pi_iff image_eqI invertible_fixpoint_property[of S r T i]) qed qed @@ -952,9 +952,9 @@ fixes f :: "'a::topological_space \ 'b::topological_space" and S :: "'a set" assumes "T retract_of S" - and FP: "\f. \continuous_on S f; f ` S \ S\ \ \x\S. f x = x" + and FP: "\f. \continuous_on S f; f \ S \ S\ \ \x\S. f x = x" and contg: "continuous_on T g" - and "g ` T \ T" + and "g \ T \ T" obtains y where "y \ T" and "g y = y" proof - obtain h where "retraction S T h" @@ -962,23 +962,24 @@ then show ?thesis unfolding retraction_def using invertible_fixpoint_property[OF continuous_on_id _ _ _ _ FP] - by (metis assms(4) contg image_ident that) + by (smt (verit, del_insts) Pi_iff assms(4) contg subsetD that) qed lemma retraction: - "retraction S T r \ - T \ S \ continuous_on S r \ r ` S = T \ (\x \ T. r x = x)" - by (force simp: retraction_def) + "retraction S T r \ T \ S \ continuous_on S r \ r ` S = T \ (\x \ T. r x = x)" + by (force simp: retraction_def simp flip: image_subset_iff_funcset) lemma retractionE: \ \yields properties normalized wrt. simp -- less likely to loop\ assumes "retraction S T r" - obtains "T = r ` S" "r ` S \ S" "continuous_on S r" "\x. x \ S \ r (r x) = r x" + obtains "T = r ` S" "r \ S \ S" "continuous_on S r" "\x. x \ S \ r (r x) = r x" proof (rule that) from retraction [of S T r] assms have "T \ S" "continuous_on S r" "r ` S = T" and "\x \ T. r x = x" by simp_all - then show "T = r ` S" "r ` S \ S" "continuous_on S r" - by simp_all + then show "r \ S \ S" "continuous_on S r" + by auto + then show "T = r ` S" + using \r ` S = T\ by blast from \\x \ T. r x = x\ have "r x = x" if "x \ T" for x using that by simp with \r ` S = T\ show "r (r x) = r x" if "x \ S" for x @@ -987,7 +988,7 @@ lemma retract_ofE: \ \yields properties normalized wrt. simp -- less likely to loop\ assumes "T retract_of S" - obtains r where "T = r ` S" "r ` S \ S" "continuous_on S r" "\x. x \ S \ r (r x) = r x" + obtains r where "T = r ` S" "r \ S \ S" "continuous_on S r" "\x. x \ S \ r (r x) = r x" proof - from assms obtain r where "retraction S T r" by (auto simp add: retract_of_def) @@ -996,30 +997,31 @@ qed lemma retract_of_imp_extensible: - assumes "S retract_of T" and "continuous_on S f" and "f ` S \ U" - obtains g where "continuous_on T g" "g ` T \ U" "\x. x \ S \ g x = f x" + assumes "S retract_of T" and "continuous_on S f" and "f \ S \ U" + obtains g where "continuous_on T g" "g \ T \ U" "\x. x \ S \ g x = f x" proof - from \S retract_of T\ obtain r where "retraction T S r" by (auto simp add: retract_of_def) - show thesis - by (rule that [of "f \ r"]) - (use \continuous_on S f\ \f ` S \ U\ \retraction T S r\ in \auto simp: continuous_on_compose2 retraction\) + then have "continuous_on T (f \ r)" + by (metis assms(2) continuous_on_compose retraction) + then show thesis + by (smt (verit, best) Pi_iff \retraction T S r\ assms(3) comp_apply retraction_def that) qed lemma idempotent_imp_retraction: - assumes "continuous_on S f" and "f ` S \ S" and "\x. x \ S \ f(f x) = f x" + assumes "continuous_on S f" and "f \ S \ S" and "\x. x \ S \ f(f x) = f x" shows "retraction S (f ` S) f" -by (simp add: assms retraction) + by (simp add: assms funcset_image retraction) lemma retraction_subset: - assumes "retraction S T r" and "T \ s'" and "s' \ S" - shows "retraction s' T r" + assumes "retraction S T r" and "T \ S'" and "S' \ S" + shows "retraction S' T r" unfolding retraction_def - by (metis assms continuous_on_subset image_mono retraction) + by (metis assms continuous_on_subset image_mono image_subset_iff_funcset retraction) lemma retract_of_subset: - assumes "T retract_of S" and "T \ s'" and "s' \ S" - shows "T retract_of s'" + assumes "T retract_of S" and "T \ S'" and "S' \ S" + shows "T retract_of S'" by (meson assms retract_of_def retraction_subset) lemma retraction_refl [simp]: "retraction S S (\x. x)" @@ -1054,10 +1056,10 @@ assumes "S retract_of T" shows "closedin (top_of_set T) S" proof - - obtain r where r: "S \ T" "continuous_on T r" "r ` T \ S" "\x. x \ S \ r x = x" + obtain r where r: "S \ T" "continuous_on T r" "r \ T \ S" "\x. x \ S \ r x = x" using assms by (auto simp: retract_of_def retraction_def) have "S = {x\T. x = r x}" - using r by auto + using r by force also have "\ = T \ ((\x. (x, r x)) -` ({y. \x. y = (x, x)}))" unfolding vimage_def mem_Times_iff fst_conv snd_conv using r @@ -1088,14 +1090,14 @@ shows "openin (top_of_set S) (S \ r -` U) \ openin (top_of_set T) U" (is "?lhs = ?rhs") proof show "?lhs \ ?rhs" - using r retraction_def retractionE - by (smt (verit, best) continuous_right_inverse_imp_quotient_map retraction_subset \U \ T\) + using r + by (smt (verit, del_insts) assms(2) continuous_right_inverse_imp_quotient_map image_subset_iff_funcset r retractionE retraction_def retraction_subset) show "?rhs \ ?lhs" - by (meson continuous_openin_preimage r retraction_def) + by (metis continuous_on_open r retraction) qed lemma retract_of_Times: - "\S retract_of s'; T retract_of t'\ \ (S \ T) retract_of (s' \ t')" + "\S retract_of S'; T retract_of T'\ \ (S \ T) retract_of (S' \ T')" apply (simp add: retract_of_def retraction_def Sigma_mono, clarify) apply (rename_tac f g) apply (rule_tac x="\z. ((f \ fst) z, (g \ snd) z)" in exI) @@ -1238,7 +1240,7 @@ lemma path_finish_in_topspace: "pathin X g \ g 1 \ topspace X" by (force simp: pathin_def continuous_map) -lemma path_image_subset_topspace: "pathin X g \ g ` ({0..1}) \ topspace X" +lemma path_image_subset_topspace: "pathin X g \ g \ ({0..1}) \ topspace X" by (force simp: pathin_def continuous_map) definition path_connected_space :: "'a topology \ bool" @@ -1262,9 +1264,9 @@ lemma path_connectedin: "path_connectedin X S \ S \ topspace X \ - (\x \ S. \y \ S. \g. pathin X g \ g ` {0..1} \ S \ g 0 = x \ g 1 = y)" + (\x \ S. \y \ S. \g. pathin X g \ g \ {0..1} \ S \ g 0 = x \ g 1 = y)" unfolding path_connectedin_def path_connected_space_def pathin_def continuous_map_in_subtopology - by (intro conj_cong refl ball_cong) (simp_all add: inf.absorb_iff2) + by (intro conj_cong refl ball_cong) (simp_all add: inf.absorb_iff2 flip: image_subset_iff_funcset) lemma path_connectedin_topspace: "path_connectedin X (topspace X) \ path_connected_space X" @@ -1310,21 +1312,21 @@ assumes f: "continuous_map X Y f" and S: "path_connectedin X S" shows "path_connectedin Y (f ` S)" proof - - have fX: "f ` (topspace X) \ topspace Y" - by (metis f continuous_map_image_subset_topspace) + have fX: "f \ (topspace X) \ topspace Y" + using continuous_map_def f by fastforce show ?thesis unfolding path_connectedin proof (intro conjI ballI; clarify?) fix x assume "x \ S" show "f x \ topspace Y" - by (meson S fX \x \ S\ image_subset_iff path_connectedin_subset_topspace set_mp) + using S \x \ S\ fX path_connectedin_subset_topspace by fastforce next fix x y assume "x \ S" and "y \ S" - then obtain g where g: "pathin X g" "g ` {0..1} \ S" "g 0 = x" "g 1 = y" + then obtain g where g: "pathin X g" "g \ {0..1} \ S" "g 0 = x" "g 1 = y" using S by (force simp: path_connectedin) - show "\g. pathin Y g \ g ` {0..1} \ f ` S \ g 0 = f x \ g 1 = f y" + show "\g. pathin Y g \ g \ {0..1} \ f ` S \ g 0 = f x \ g 1 = f y" proof (intro exI conjI) show "pathin Y (f \ g)" using \pathin X g\ f pathin_compose by auto @@ -1361,7 +1363,7 @@ shows "path_connectedin Y (f ` U) \ path_connectedin X U" unfolding path_connectedin_def proof (intro conj_cong homeomorphic_path_connected_space) - show "(f ` U \ topspace Y) = (U \ topspace X)" + show "f ` U \ topspace Y \ (U \ topspace X)" using assms homeomorphic_imp_surjective_map by blast next assume "U \ topspace X" diff -r d4125fc10c0c -r 1260be3f33a4 src/HOL/Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Sun Jul 02 20:41:07 2023 +0200 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Mon Jul 03 16:46:37 2023 +0100 @@ -24,7 +24,7 @@ assumes "contractible T" "S retract_of T" shows "contractible S" using assms -apply (clarsimp simp add: retract_of_def contractible_def retraction_def homotopic_with) +apply (clarsimp simp add: retract_of_def contractible_def retraction_def homotopic_with image_subset_iff_funcset) apply (rule_tac x="r a" in exI) apply (rule_tac x="r \ h" in exI) apply (intro conjI continuous_intros continuous_on_compose) @@ -126,8 +126,8 @@ by (metis eq_id_iff homotopic_with_id2 topspace_euclidean_subtopology) ultimately show ?thesis - unfolding homotopy_equivalent_space_def - by (metis (no_types, lifting) continuous_map_subtopology_eu continuous_on_id' id_def image_id r retraction_def) + unfolding homotopy_equivalent_space_def + by (smt (verit, del_insts) continuous_map_id continuous_map_subtopology_eu id_def r retraction retraction_comp subset_refl) qed lemma deformation_retract: @@ -1807,7 +1807,7 @@ and "convex S" and "interior S \ {}" and "continuous_on S f" - and "f ` S \ S" + and "f \ S \ S" obtains x where "x \ S" and "f x = x" proof - let ?U = "cbox 0 One :: 'a set" @@ -1824,8 +1824,7 @@ then have *: "interior ?U \ {}" by fast have *: "?U homeomorphic S" using homeomorphic_convex_compact[OF convex_box(1) compact_cbox * assms(2,1,3)] . - have "\f. continuous_on ?U f \ f ` ?U \ ?U \ - (\x\?U. f x = x)" + have "\f. continuous_on ?U f \ f \ ?U \ ?U \ (\x\?U. f x = x)" using brouwer_cube by auto then show ?thesis unfolding homeomorphic_fixpoint_property[OF *] @@ -1839,7 +1838,7 @@ fixes f :: "'a::euclidean_space \ 'a" assumes "e > 0" and "continuous_on (cball a e) f" - and "f ` cball a e \ cball a e" + and "f \ cball a e \ cball a e" obtains x where "x \ cball a e" and "f x = x" using brouwer_weak[OF compact_cball convex_cball, of a e f] unfolding interior_cball ball_eq_empty @@ -1851,7 +1850,7 @@ fixes f :: "'a::euclidean_space \ 'a" assumes S: "compact S" "convex S" "S \ {}" and contf: "continuous_on S f" - and fim: "f ` S \ S" + and fim: "f \ S \ S" obtains x where "x \ S" and "f x = x" proof - have "\e>0. S \ cball 0 e" @@ -1864,12 +1863,12 @@ show "continuous_on (cball 0 e) (f \ closest_point S)" by (meson assms closest_point_in_set compact_eq_bounded_closed contf continuous_on_closest_point continuous_on_compose continuous_on_subset image_subsetI) - show "(f \ closest_point S) ` cball 0 e \ cball 0 e" - by clarsimp (metis S fim closest_point_exists(1) compact_eq_bounded_closed e(2) image_subset_iff mem_cball_0 subsetCE) + show "f \ closest_point S \ cball 0 e \ cball 0 e" + by (smt (verit) Pi_iff assms(1) assms(3) closest_point_in_set comp_apply compact_eq_bounded_closed e(2) fim subset_eq) qed (use assms in auto) then obtain x where x: "x \ cball 0 e" "(f \ closest_point S) x = x" .. - have "x \ S" - by (metis closest_point_in_set comp_apply compact_imp_closed fim image_eqI S(1) S(3) subset_iff x(2)) + with S have "x \ S" + by (metis PiE closest_point_in_set comp_apply compact_imp_closed fim) then have *: "closest_point S x = x" by (rule closest_point_self) show thesis @@ -1877,7 +1876,7 @@ show "closest_point S x \ S" by (simp add: "*" \x \ S\) show "f (closest_point S x) = closest_point S x" - using "*" x(2) by auto + using "*" x by auto qed qed @@ -1897,14 +1896,13 @@ proof (rule retract_fixpoint_property[OF *, of "\x. scaleR 2 a - x"]) show "continuous_on (frontier (cball a e)) ((-) (2 *\<^sub>R a))" by (intro continuous_intros) - show "(-) (2 *\<^sub>R a) ` frontier (cball a e) \ frontier (cball a e)" + show "(-) (2 *\<^sub>R a) \ frontier (cball a e) \ frontier (cball a e)" by clarsimp (metis "**" dist_norm norm_minus_cancel) qed (auto simp: dist_norm intro: brouwer_ball[OF assms]) then have "scaleR 2 a = scaleR 1 x + scaleR 1 x" by (auto simp: algebra_simps) then have "a = x" - unfolding scaleR_left_distrib[symmetric] - by auto + unfolding scaleR_left_distrib[symmetric] by auto then show False using x assms by auto qed @@ -1977,7 +1975,7 @@ fixes S :: "'a::euclidean_space set" assumes "bounded S" and fros: "frontier S \ T" and contf: "continuous_on (closure S) f" - and fim: "f ` S \ T" + and fim: "f \ S \ T" and fid: "\x. x \ T \ f x = x" shows "S \ T" proof (rule ccontr) @@ -1995,7 +1993,7 @@ using \bounded S\ bounded_subset_ballD by blast have notga: "g x \ a" for x unfolding g_def using fros fim \a \ T\ - by (metis Un_iff \a \ S\ closure_Un_frontier fid imageI subset_eq) + by (metis PiE Un_iff \a \ S\ closure_Un_frontier fid subsetD) define h where "h \ (\y. a + (B / norm(y - a)) *\<^sub>R (y - a)) \ g" have "\ (frontier (cball a B) retract_of (cball a B))" by (metis no_retraction_cball \0 < B\) @@ -2009,12 +2007,12 @@ show "continuous_on (cball a B) h" unfolding h_def by (intro continuous_intros) (use contg continuous_on_subset notga in auto) - show "h ` cball a B \ frontier (cball a B)" + show "h \ cball a B \ frontier (cball a B)" using \0 < B\ by (auto simp: h_def notga dist_norm) show "\x. x \ frontier (cball a B) \ h x = x" - apply (auto simp: h_def algebra_simps) - apply (simp add: vector_add_divide_simps notga) - by (metis (no_types, opaque_lifting) B add.commute dist_commute dist_norm g_def mem_ball not_less_iff_gr_or_eq subset_eq) + using notga \0 < B\ + apply (simp add: g_def h_def field_simps) + by (metis B dist_commute dist_norm mem_ball order_less_irrefl subset_eq) qed ultimately show False by simp qed @@ -2131,7 +2129,7 @@ using arelS relS rel_frontier_def by fastforce show "continuous_on (T - {a}) (\x. a + dd (x - a) *\<^sub>R (x - a))" using contdd by (simp add: o_def) - show "(\x. a + dd (x - a) *\<^sub>R (x - a)) ` (T - {a}) \ rel_frontier S" + show "(\x. a + dd (x - a) *\<^sub>R (x - a)) \ (T - {a}) \ rel_frontier S" apply (auto simp: rel_frontier_def) apply (metis Diff_subset add.commute affS dd1 diff_add_cancel eq_iff_diff_eq_0 rel_frontier_def subset_iff) by (metis DiffE add.commute affS dd1 diff_add_cancel eq_iff_diff_eq_0 rel_frontier_def rev_subsetD) @@ -2216,20 +2214,25 @@ subsubsection\Borsuk-style characterization of separation\ lemma continuous_on_Borsuk_map: - "a \ s \ continuous_on s (\x. inverse(norm (x - a)) *\<^sub>R (x - a))" + "a \ S \ continuous_on S (\x. inverse(norm (x - a)) *\<^sub>R (x - a))" by (rule continuous_intros | force)+ lemma Borsuk_map_into_sphere: - "(\x. inverse(norm (x - a)) *\<^sub>R (x - a)) ` s \ sphere 0 1 \ (a \ s)" - by auto (metis eq_iff_diff_eq_0 left_inverse norm_eq_zero) + "(\x. inverse(norm (x - a)) *\<^sub>R (x - a)) \ S \ sphere 0 1 \ (a \ S)" +proof - + have "\x. \a \ S; x \ S\ \ inverse (norm (x - a)) * norm (x - a) = 1" + by (metis left_inverse norm_eq_zero right_minus_eq) + then show ?thesis + by force +qed lemma Borsuk_maps_homotopic_in_path_component: - assumes "path_component (- s) a b" - shows "homotopic_with_canon (\x. True) s (sphere 0 1) + assumes "path_component (- S) a b" + shows "homotopic_with_canon (\x. True) S (sphere 0 1) (\x. inverse(norm(x - a)) *\<^sub>R (x - a)) (\x. inverse(norm(x - b)) *\<^sub>R (x - b))" proof - - obtain g where "path g" "path_image g \ -s" "pathstart g = a" "pathfinish g = b" + obtain g where "path g" "path_image g \ -S" "pathstart g = a" "pathfinish g = b" using assms by (auto simp: path_component_def) then show ?thesis apply (simp add: path_def path_image_def pathstart_def pathfinish_def homotopic_with_def) @@ -2240,61 +2243,59 @@ lemma non_extensible_Borsuk_map: fixes a :: "'a :: euclidean_space" - assumes "compact s" and cin: "c \ components(- s)" and boc: "bounded c" and "a \ c" - shows "\ (\g. continuous_on (s \ c) g \ - g ` (s \ c) \ sphere 0 1 \ - (\x \ s. g x = inverse(norm(x - a)) *\<^sub>R (x - a)))" + assumes "compact S" and cin: "C \ components(- S)" and boc: "bounded C" and "a \ C" + shows "\ (\g. continuous_on (S \ C) g \ + g \ (S \ C) \ sphere 0 1 \ + (\x \ S. g x = inverse(norm(x - a)) *\<^sub>R (x - a)))" proof - - have "closed s" using assms by (simp add: compact_imp_closed) - have "c \ -s" + have "closed S" using assms by (simp add: compact_imp_closed) + have "C \ -S" using assms by (simp add: in_components_subset) - with \a \ c\ have "a \ s" by blast - then have ceq: "c = connected_component_set (- s) a" - by (metis \a \ c\ cin components_iff connected_component_eq) - then have "bounded (s \ connected_component_set (- s) a)" - using \compact s\ boc compact_imp_bounded by auto - with bounded_subset_ballD obtain r where "0 < r" and r: "(s \ connected_component_set (- s) a) \ ball a r" + with \a \ C\ have "a \ S" by blast + then have ceq: "C = connected_component_set (- S) a" + by (metis \a \ C\ cin components_iff connected_component_eq) + then have "bounded (S \ connected_component_set (- S) a)" + using \compact S\ boc compact_imp_bounded by auto + with bounded_subset_ballD obtain r where "0 < r" and r: "(S \ connected_component_set (- S) a) \ ball a r" by blast { fix g - assume "continuous_on (s \ c) g" - "g ` (s \ c) \ sphere 0 1" - and [simp]: "\x. x \ s \ g x = (x - a) /\<^sub>R norm (x - a)" - then have [simp]: "\x. x \ s \ c \ norm (g x) = 1" + assume "continuous_on (S \ C) g" + "g \ (S \ C) \ sphere 0 1" + and [simp]: "\x. x \ S \ g x = (x - a) /\<^sub>R norm (x - a)" + then have norm_g1[simp]: "\x. x \ S \ C \ norm (g x) = 1" by force - have cb_eq: "cball a r = (s \ connected_component_set (- s) a) \ - (cball a r - connected_component_set (- s) a)" + have cb_eq: "cball a r = (S \ connected_component_set (- S) a) \ + (cball a r - connected_component_set (- S) a)" using ball_subset_cball [of a r] r by auto - have cont1: "continuous_on (s \ connected_component_set (- s) a) + have cont1: "continuous_on (S \ connected_component_set (- S) a) (\x. a + r *\<^sub>R g x)" - using \continuous_on (s \ c) g\ ceq + using \continuous_on (S \ C) g\ ceq by (intro continuous_intros) blast - have cont2: "continuous_on (cball a r - connected_component_set (- s) a) + have cont2: "continuous_on (cball a r - connected_component_set (- S) a) (\x. a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))" - by (rule continuous_intros | force simp: \a \ s\)+ + by (rule continuous_intros | force simp: \a \ S\)+ have 1: "continuous_on (cball a r) - (\x. if connected_component (- s) a x + (\x. if connected_component (- S) a x then a + r *\<^sub>R g x else a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))" apply (subst cb_eq) apply (rule continuous_on_cases [OF _ _ cont1 cont2]) - using \closed s\ ceq cin + using \closed S\ ceq cin by (force simp: closed_Diff open_Compl closed_Un_complement_component open_connected_component)+ - have 2: "(\x. a + r *\<^sub>R g x) ` (cball a r \ connected_component_set (- s) a) + have 2: "(\x. a + r *\<^sub>R g x) ` (cball a r \ connected_component_set (- S) a) \ sphere a r " using \0 < r\ by (force simp: dist_norm ceq) have "retraction (cball a r) (sphere a r) - (\x. if x \ connected_component_set (- s) a + (\x. if x \ connected_component_set (- S) a then a + r *\<^sub>R g x else a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))" - using \0 < r\ - apply (simp add: retraction_def dist_norm 1 2, safe) - apply (force simp: dist_norm abs_if mult_less_0_iff divide_simps \a \ s\) - using r - by (auto simp: dist_norm norm_minus_commute) + using \0 < r\ \a \ S\ \a \ C\ r + by (auto simp: norm_minus_commute retraction_def Pi_iff ceq dist_norm abs_if + mult_less_0_iff divide_simps 1 2) then have False using no_retraction_cball [OF \0 < r\, of a, unfolded retract_of_def, simplified, rule_format, - of "\x. if x \ connected_component_set (- s) a + of "\x. if x \ connected_component_set (- S) a then a + r *\<^sub>R g x else a + r *\<^sub>R inverse(norm(x - a)) *\<^sub>R (x - a)"] by blast diff -r d4125fc10c0c -r 1260be3f33a4 src/HOL/Analysis/Fashoda_Theorem.thy --- a/src/HOL/Analysis/Fashoda_Theorem.thy Sun Jul 02 20:41:07 2023 +0200 +++ b/src/HOL/Analysis/Fashoda_Theorem.thy Mon Jul 03 16:46:37 2023 +0100 @@ -174,8 +174,8 @@ "(negatex \ sqprojection \ (\w. (f \ (\x. x $ 1)) w - (g \ (\x. x $ 2)) w)) x = x" apply (rule brouwer_weak[of "cbox (- 1) (1::real^2)" "negatex \ sqprojection \ ?F"]) apply (rule compact_cbox convex_box)+ - unfolding interior_cbox - apply (rule 1 2 3)+ + unfolding interior_cbox image_subset_iff_funcset [symmetric] + apply (rule 1 2 3)+ apply blast done have "?F x \ 0" diff -r d4125fc10c0c -r 1260be3f33a4 src/HOL/Analysis/Further_Topology.thy --- a/src/HOL/Analysis/Further_Topology.thy Sun Jul 02 20:41:07 2023 +0200 +++ b/src/HOL/Analysis/Further_Topology.thy Mon Jul 03 16:46:37 2023 +0100 @@ -231,7 +231,7 @@ qed have conT0: "continuous_on (T - {0}) (\y. inverse(norm y) *\<^sub>R y)" by (intro continuous_intros) auto - have sub0T: "(\y. y /\<^sub>R norm y) ` (T - {0}) \ sphere 0 1 \ T" + have sub0T: "(\y. y /\<^sub>R norm y) \ (T - {0}) \ sphere 0 1 \ T" by (fastforce simp: assms(2) subspace_mul) obtain c where homhc: "homotopic_with_canon (\z. True) (sphere 0 1 \ S) (sphere 0 1 \ T) h (\x. c)" proof @@ -307,7 +307,7 @@ assumes "convex S" "bounded S" "convex T" "bounded T" and affST: "aff_dim S < aff_dim T" and contf: "continuous_on (rel_frontier S) f" - and fim: "f ` (rel_frontier S) \ rel_frontier T" + and fim: "f \ (rel_frontier S) \ rel_frontier T" obtains c where "homotopic_with_canon (\z. True) (rel_frontier S) (rel_frontier T) f (\x. c)" proof (cases "S = {}") case True @@ -319,7 +319,7 @@ proof (cases "T = {}") case True then show ?thesis - using fim that by auto + using fim that by (simp add: Pi_iff) next case False obtain T':: "'a set" @@ -345,7 +345,7 @@ have "\c. homotopic_with_canon (\z. True) (rel_frontier S) (rel_frontier T) f (\x. c)" using spheremap_lemma2 homotopy_eqv_cohomotopic_triviality_null[OF relS] using homotopy_eqv_homotopic_triviality_null_imp [OF relT contf fim] - by (metis \S' \ T'\ \subspace S'\ \subspace T'\ dimST') + by (metis \S' \ T'\ \subspace S'\ \subspace T'\ dimST' image_subset_iff_funcset) with that show ?thesis by blast qed qed @@ -353,7 +353,7 @@ lemma inessential_spheremap_lowdim: fixes f :: "'M::euclidean_space \ 'a::euclidean_space" assumes - "DIM('M) < DIM('a)" and f: "continuous_on (sphere a r) f" "f ` (sphere a r) \ (sphere b s)" + "DIM('M) < DIM('a)" and f: "continuous_on (sphere a r) f" "f \ (sphere a r) \ (sphere b s)" obtains c where "homotopic_with_canon (\z. True) (sphere a r) (sphere b s) f (\x. c)" proof (cases "s \ 0") case True then show ?thesis @@ -505,7 +505,7 @@ using \C \ \\ \D face_of C\ face_of_polytope_polytope poly polytope_imp_polyhedron by auto ultimately have relf_sub: "rel_frontier D \ \ {E. E face_of C \ aff_dim E < p}" by (simp add: rel_frontier_of_polyhedron Union_mono) - then have him_relf: "h ` rel_frontier D \ rel_frontier T" + then have him_relf: "h \ rel_frontier D \ rel_frontier T" using \C \ \\ him by blast have "convex D" by (simp add: \polyhedron D\ polyhedron_imp_convex) @@ -516,9 +516,9 @@ then have *: "(\c. homotopic_with_canon (\x. True) (rel_frontier D) (rel_frontier T) h (\x. c)) = (\g. continuous_on UNIV g \ range g \ rel_frontier T \ (\x\rel_frontier D. g x = h x))" - by (simp add: assms rel_frontier_eq_empty him_relf nullhomotopic_into_rel_frontier_extension [OF closed_rel_frontier]) - have "(\c. homotopic_with_canon (\x. True) (rel_frontier D) (rel_frontier T) h (\x. c))" - by (metis inessential_spheremap_lowdim_gen + by (simp add: assms image_subset_iff_funcset rel_frontier_eq_empty him_relf nullhomotopic_into_rel_frontier_extension [OF closed_rel_frontier]) + have "\c. homotopic_with_canon (\x. True) (rel_frontier D) (rel_frontier T) h (\x. c)" + by (metis inessential_spheremap_lowdim_gen [OF \convex D\ \bounded D\ \convex T\ \bounded T\ affD_lessT contDh him_relf]) then obtain g where contg: "continuous_on UNIV g" and gim: "range g \ rel_frontier T" @@ -852,11 +852,11 @@ and poly: "\X. X \ \ \ polytope X" and aff: "\X. X \ \ \ aff_dim X < aff_dim T" and face: "\X Y. \X \ \; Y \ \\ \ (X \ Y) face_of X" - and contf: "continuous_on S f" and fim: "f ` S \ rel_frontier T" + and contf: "continuous_on S f" and fim: "f \ S \ rel_frontier T" obtains g where "continuous_on (\\) g" "g ` (\\) \ rel_frontier T" "\x. x \ S \ g x = f x" proof - - obtain V g where "S \ V" "open V" "continuous_on V g" and gim: "g ` V \ rel_frontier T" and gf: "\x. x \ S \ g x = f x" + obtain V g where "S \ V" "open V" "continuous_on V g" and gim: "g \ V \ rel_frontier T" and gf: "\x. x \ S \ g x = f x" using neighbourhood_extension_into_ANR [OF contf fim _ \closed S\] ANR_rel_frontier_convex T by blast have "compact S" by (meson assms compact_Union poly polytope_imp_compact seq_compact_closed_subset seq_compact_eq_compact) @@ -906,11 +906,11 @@ and poly: "\X. X \ \ \ polytope X" and aff: "\X. X \ \ \ aff_dim X \ aff_dim T" and face: "\X Y. \X \ \; Y \ \\ \ (X \ Y) face_of X" - and contf: "continuous_on S f" and fim: "f ` S \ rel_frontier T" + and contf: "continuous_on S f" and fim: "f \ S \ rel_frontier T" obtains C g where "finite C" "disjnt C S" "continuous_on (\\ - C) g" "g ` (\\ - C) \ rel_frontier T" "\x. x \ S \ g x = f x" proof - - obtain V g where "S \ V" "open V" "continuous_on V g" and gim: "g ` V \ rel_frontier T" and gf: "\x. x \ S \ g x = f x" + obtain V g where "S \ V" "open V" "continuous_on V g" and gim: "g \ V \ rel_frontier T" and gf: "\x. x \ S \ g x = f x" using neighbourhood_extension_into_ANR [OF contf fim _ \closed S\] ANR_rel_frontier_convex T by blast have "compact S" by (meson assms compact_Union poly polytope_imp_compact seq_compact_closed_subset seq_compact_eq_compact) @@ -974,13 +974,13 @@ assumes "compact S" "convex U" "bounded U" and aff: "aff_dim T \ aff_dim U" and "S \ T" and contf: "continuous_on S f" - and fim: "f ` S \ rel_frontier U" + and fim: "f \ S \ rel_frontier U" obtains K g where "finite K" "K \ T" "disjnt K S" "continuous_on (T - K) g" - "g ` (T - K) \ rel_frontier U" + "g \ (T - K) \ rel_frontier U" "\x. x \ S \ g x = f x" proof - have "\K g. finite K \ disjnt K S \ continuous_on (T - K) g \ - g ` (T - K) \ rel_frontier U \ (\x \ S. g x = f x)" + g \ (T - K) \ rel_frontier U \ (\x \ S. g x = f x)" if "affine T" "S \ T" and aff: "aff_dim T \ aff_dim U" for T proof (cases "S = {}") case True @@ -1089,7 +1089,8 @@ by (metis image_comp image_mono cpt_subset) also have "... \ rel_frontier U" by (rule gim) - finally show "(g \ closest_point (cbox (- c) c \ T)) ` (T - K) \ rel_frontier U" . + finally show "(g \ closest_point (cbox (- c) c \ T)) \ (T - K) \ rel_frontier U" + by blast show "(g \ closest_point (cbox (- c) c \ T)) x = f x" if "x \ S" for x proof - have "(g \ closest_point (cbox (- c) c \ T)) x = g x" @@ -1103,7 +1104,7 @@ qed then obtain K g where "finite K" "disjnt K S" and contg: "continuous_on (affine hull T - K) g" - and gim: "g ` (affine hull T - K) \ rel_frontier U" + and gim: "g \ (affine hull T - K) \ rel_frontier U" and gf: "\x. x \ S \ g x = f x" by (metis aff affine_affine_hull aff_dim_affine_hull order_trans [OF \S \ T\ hull_subset [of T affine]]) @@ -1123,14 +1124,14 @@ lemma extend_map_affine_to_sphere1: fixes f :: "'a::euclidean_space \ 'b::topological_space" assumes "finite K" "affine U" and contf: "continuous_on (U - K) f" - and fim: "f ` (U - K) \ T" + and fim: "f \ (U - K) \ T" and comps: "\C. \C \ components(U - S); C \ K \ {}\ \ C \ L \ {}" and clo: "closedin (top_of_set U) S" and K: "disjnt K S" "K \ U" - obtains g where "continuous_on (U - L) g" "g ` (U - L) \ T" "\x. x \ S \ g x = f x" + obtains g where "continuous_on (U - L) g" "g \ (U - L) \ T" "\x. x \ S \ g x = f x" proof (cases "K = {}") case True then show ?thesis - by (metis Diff_empty Diff_subset contf fim continuous_on_subset image_subsetI image_eqI subset_iff that) + by (metis DiffD1 Diff_empty Diff_subset PiE Pi_I contf continuous_on_subset fim that) next case False have "S \ U" @@ -1194,7 +1195,7 @@ then obtain r where contr: "continuous_on (U - {a}) r" and rim: "r ` (U - {a}) \ sphere a d" "r ` (U - {a}) \ U" and req: "\x. x \ sphere a d \ U \ r x = x" - using \affine U\ by (auto simp: retract_of_def retraction_def hull_same) + using \affine U\ by (force simp: retract_of_def retraction_def hull_same) define j where "j \ \x. if x \ ball a d then r x else x" have kj: "\x. x \ S \ k (j x) = x" using \C \ U - S\ \S \ U\ \ball a d \ U \ C\ j_def subC by auto @@ -1256,7 +1257,7 @@ have ST: "\x. x \ S \ (f \ k \ j) x \ T" proof (simp add: kj) show "\x. x \ S \ f x \ T" - using K unfolding disjnt_iff by (metis DiffI \S \ U\ subsetD fim image_subset_iff) + using K \S \ U\ fT unfolding disjnt_iff by auto qed moreover have "(f \ k \ j) x \ T" if "x \ C" "x \ a" "x \ S" for x proof - @@ -1410,7 +1411,7 @@ using image_mono order_trans by blast moreover have "f ` ((U - L) \ (S \ \G)) \ T" using fim SUG by blast - ultimately show "(\x. if x \ S \ \G then f x else g x) ` (U - L) \ T" + ultimately show "(\x. if x \ S \ \G then f x else g x) \ (U - L) \ T" by force show "\x. x \ S \ (if x \ S \ \G then f x else g x) = f x" by (simp add: F_def G_def) @@ -1423,15 +1424,15 @@ assumes "compact S" "convex U" "bounded U" "affine T" "S \ T" and affTU: "aff_dim T \ aff_dim U" and contf: "continuous_on S f" - and fim: "f ` S \ rel_frontier U" + and fim: "f \ S \ rel_frontier U" and ovlap: "\C. C \ components(T - S) \ C \ L \ {}" obtains K g where "finite K" "K \ L" "K \ T" "disjnt K S" - "continuous_on (T - K) g" "g ` (T - K) \ rel_frontier U" + "continuous_on (T - K) g" "g \ (T - K) \ rel_frontier U" "\x. x \ S \ g x = f x" proof - obtain K g where K: "finite K" "K \ T" "disjnt K S" and contg: "continuous_on (T - K) g" - and gim: "g ` (T - K) \ rel_frontier U" + and gim: "g \ (T - K) \ rel_frontier U" and gf: "\x. x \ S \ g x = f x" using assms extend_map_affine_to_sphere_cofinite_simple by metis have "(\y C. C \ components (T - S) \ x \ C \ y \ C \ y \ L)" if "x \ K" for x @@ -1446,7 +1447,7 @@ then obtain \ where \: "\x. x \ K \ \C. C \ components (T - S) \ x \ C \ \ x \ C \ \ x \ L" by metis obtain h where conth: "continuous_on (T - \ ` K) h" - and him: "h ` (T - \ ` K) \ rel_frontier U" + and him: "h \ (T - \ ` K) \ rel_frontier U" and hg: "\x. x \ S \ h x = g x" proof (rule extend_map_affine_to_sphere1 [OF \finite K\ \affine T\ contg gim, of S "\ ` K"]) show cloTS: "closedin (top_of_set T) S" @@ -1475,10 +1476,10 @@ assumes SUT: "compact S" "convex U" "bounded U" "affine T" "S \ T" and aff: "aff_dim T \ aff_dim U" and contf: "continuous_on S f" - and fim: "f ` S \ rel_frontier U" + and fim: "f \ S \ rel_frontier U" and dis: "\C. \C \ components(T - S); bounded C\ \ C \ L \ {}" obtains K g where "finite K" "K \ L" "K \ T" "disjnt K S" "continuous_on (T - K) g" - "g ` (T - K) \ rel_frontier U" + "g \ (T - K) \ rel_frontier U" "\x. x \ S \ g x = f x" proof (cases "S = {}") case True @@ -1615,8 +1616,8 @@ have "g (closest_point (cbox (- c) c \ T) x) \ rel_frontier U" if "x \ T" "x \ K \ x \ cbox (- b - One) (b + One)" for x using gim [THEN subsetD] that cloTK by blast - then show "(g \ closest_point (cbox (- c) c \ T)) ` (T - K \ cbox (- (b + One)) (b + One)) - \ rel_frontier U" + then show "(g \ closest_point (cbox (- c) c \ T)) \ (T - K \ cbox (- (b + One)) (b + One)) + \ rel_frontier U" by force show "\x. x \ S \ (g \ closest_point (cbox (- c) c \ T)) x = f x" by simp (metis (mono_tags, lifting) IntI \S \ T\ cT_ne clo_cT closest_point_refl gf subsetD S_sub_cc) @@ -1629,23 +1630,26 @@ assumes SUT: "compact S" "affine T" "S \ T" and aff: "aff_dim T \ DIM('b)" and "0 \ r" and contf: "continuous_on S f" - and fim: "f ` S \ sphere a r" + and fim: "f \ S \ sphere a r" and dis: "\C. \C \ components(T - S); bounded C\ \ C \ L \ {}" obtains K g where "finite K" "K \ L" "K \ T" "disjnt K S" "continuous_on (T - K) g" - "g ` (T - K) \ sphere a r" "\x. x \ S \ g x = f x" + "g \ (T - K) \ sphere a r" "\x. x \ S \ g x = f x" proof (cases "r = 0") case True with fim show ?thesis by (rule_tac K="{}" and g = "\x. a" in that) (auto) next case False - with assms have "0 < r" by auto - then have "aff_dim T \ aff_dim (cball a r)" - by (simp add: aff aff_dim_cball) - then show ?thesis - using extend_map_affine_to_sphere_cofinite_gen - [OF \compact S\ convex_cball bounded_cball \affine T\ \S \ T\ _ contf] - using fim by (fastforce simp: assms False that dest: dis) + show thesis + proof (rule extend_map_affine_to_sphere_cofinite_gen + [OF \compact S\ convex_cball bounded_cball \affine T\ \S \ T\ _ contf]) + have "0 < r" + using assms False by auto + then show "aff_dim T \ aff_dim (cball a r)" + by (simp add: aff aff_dim_cball) + show "f \ S \ rel_frontier (cball a r)" + by (simp add: False fim) + qed (use dis False that in auto) qed corollary extend_map_UNIV_to_sphere_cofinite: @@ -1653,10 +1657,10 @@ assumes "DIM('a) \ DIM('b)" and "0 \ r" and "compact S" and "continuous_on S f" - and "f ` S \ sphere a r" + and "f \ S \ sphere a r" and "\C. \C \ components(- S); bounded C\ \ C \ L \ {}" obtains K g where "finite K" "K \ L" "disjnt K S" "continuous_on (- K) g" - "g ` (- K) \ sphere a r" "\x. x \ S \ g x = f x" + "g \ (- K) \ sphere a r" "\x. x \ S \ g x = f x" using extend_map_affine_to_sphere_cofinite [OF \compact S\ affine_UNIV subset_UNIV] assms by (metis Compl_eq_Diff_UNIV aff_dim_UNIV of_nat_le_iff) @@ -1666,9 +1670,9 @@ assumes aff: "DIM('a) \ DIM('b)" and "0 \ r" and SUT: "compact S" and contf: "continuous_on S f" - and fim: "f ` S \ sphere a r" + and fim: "f \ S \ sphere a r" and dis: "\C. C \ components(- S) \ \ bounded C" - obtains g where "continuous_on UNIV g" "g ` UNIV \ sphere a r" "\x. x \ S \ g x = f x" + obtains g where "continuous_on UNIV g" "g \ UNIV \ sphere a r" "\x. x \ S \ g x = f x" using extend_map_UNIV_to_sphere_cofinite [OF aff \0 \ r\ \compact S\ contf fim, of "{}"] by (metis Compl_empty_eq dis subset_empty) @@ -1677,7 +1681,7 @@ fixes S :: "'a::euclidean_space set" assumes "compact S" shows "(\c \ components(- S). \bounded c) \ - (\f. continuous_on S f \ f ` S \ sphere (0::'a) 1 + (\f. continuous_on S f \ f \ S \ sphere (0::'a) 1 \ (\c. homotopic_with_canon (\x. True) S (sphere 0 1) f (\x. c)))" (is "?lhs = ?rhs") proof @@ -1685,14 +1689,14 @@ show ?rhs proof clarify fix f :: "'a \ 'a" - assume contf: "continuous_on S f" and fim: "f ` S \ sphere 0 1" - obtain g where contg: "continuous_on UNIV g" and gim: "range g \ sphere 0 1" + assume contf: "continuous_on S f" and fim: "f \ S \ sphere 0 1" + obtain g where contg: "continuous_on UNIV g" and gim: "g \ UNIV \ sphere 0 1" and gf: "\x. x \ S \ g x = f x" by (rule extend_map_UNIV_to_sphere_no_bounded_component [OF _ _ \compact S\ contf fim L]) auto then obtain c where c: "homotopic_with_canon (\h. True) UNIV (sphere 0 1) g (\x. c)" - using contractible_UNIV nullhomotopic_from_contractible by blast + by (metis contractible_UNIV nullhomotopic_from_contractible) then show "\c. homotopic_with_canon (\x. True) S (sphere 0 1) f (\x. c)" - by (metis assms compact_imp_closed contf contg contractible_empty fim gf gim nullhomotopic_from_contractible nullhomotopic_into_sphere_extension) + by (metis assms compact_imp_closed contf contg contractible_empty fim gf gim nullhomotopic_from_contractible nullhomotopic_into_sphere_extension image_subset_iff_funcset) qed next assume R [rule_format]: ?rhs @@ -1717,7 +1721,7 @@ fixes S :: "'a::euclidean_space set" assumes "compact S" and 2: "2 \ DIM('a)" shows "connected(- S) \ - (\f. continuous_on S f \ f ` S \ sphere (0::'a) 1 + (\f. continuous_on S f \ f \ S \ sphere (0::'a) 1 \ (\c. homotopic_with_canon (\x. True) S (sphere 0 1) f (\x. c)))" (is "?lhs = ?rhs") proof @@ -2881,7 +2885,7 @@ corollary homotopy_eqv_simple_connectedness: fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set" shows "S homotopy_eqv T \ simply_connected S \ simply_connected T" - by (simp add: simply_connected_eq_homotopic_circlemaps homotopy_eqv_homotopic_triviality) + by (simp add: simply_connected_eq_homotopic_circlemaps homotopy_eqv_homotopic_triviality image_subset_iff_funcset) subsection\Homeomorphism of simple closed curves to circles\ @@ -3673,10 +3677,10 @@ then obtain g where contg: "continuous_on S g" and f: "\x. x \ S \ f x = exp(g x)" by metis obtain a where "homotopic_with_canon (\h. True) S (- {of_real 0}) (exp \ g) (\x. a)" - proof (rule nullhomotopic_through_contractible [OF contg subset_UNIV _ _ contractible_UNIV]) + proof (rule nullhomotopic_through_contractible [OF contg _ _ _ contractible_UNIV]) show "continuous_on (UNIV::complex set) exp" by (intro continuous_intros) - show "range exp \ - {0}" + show "exp \ UNIV \ -{of_real 0}" by auto qed force then have "homotopic_with_canon (\h. True) S (- {0}) f (\t. a)" @@ -3719,11 +3723,11 @@ proof (rule nullhomotopic_through_contractible) show "continuous_on S (complex_of_real \ g)" by (intro conjI contg continuous_intros) - show "(complex_of_real \ g) ` S \ \" + show "(complex_of_real \ g) \ S \ \" by auto show "continuous_on \ (exp \ (*)\)" by (intro continuous_intros) - show "(exp \ (*)\) ` \ \ sphere 0 1" + show "(exp \ (*)\) \ \ \ sphere 0 1" by (auto simp: complex_is_Real_iff) qed (auto simp: convex_Reals convex_imp_contractible) moreover have "\x. x \ S \ (exp \ (*)\ \ (complex_of_real \ g)) x = f x" @@ -4012,7 +4016,7 @@ proof - obtain c where hom: "homotopic_with_canon (\h. True) S (-{0}) f (\x. c)" using nullhomotopic_from_contractible assms - by (metis imageE subset_Compl_singleton) + by (metis imageE subset_Compl_singleton image_subset_iff_funcset) then show ?thesis by (metis inessential_eq_continuous_logarithm that) qed @@ -4023,7 +4027,7 @@ and f: "\z. z \ S \ f z \ 0" obtains g where "continuous_on S g" "\x. x \ S \ f x = exp(g x)" using covering_space_lift [OF covering_space_exp_punctured_plane S contf] - by (metis (full_types) f imageE subset_Compl_singleton) + by (metis (full_types) f imageE subset_Compl_singleton image_subset_iff_funcset) lemma continuous_logarithm_on_cball: fixes f :: "'a::real_normed_vector \ complex" @@ -4077,7 +4081,7 @@ lemma inessential_spheremap_2_aux: fixes f :: "'a::euclidean_space \ complex" assumes 2: "2 < DIM('a)" and contf: "continuous_on (sphere a r) f" - and fim: "f `(sphere a r) \ (sphere 0 1)" + and fim: "f \ (sphere a r) \ (sphere 0 1)" obtains c where "homotopic_with_canon (\z. True) (sphere a r) (sphere 0 1) f (\x. c)" proof - obtain g where contg: "continuous_on (sphere a r) g" @@ -4095,7 +4099,8 @@ show "continuous_on (sphere a r) (Im \ g)" by (intro contg continuous_intros continuous_on_compose) show "\x\sphere a r. f x = exp (\ * complex_of_real ((Im \ g) x))" - using exp_eq_polar feq fim norm_exp_eq_Re by auto + using exp_eq_polar feq fim norm_exp_eq_Re + by (auto simp flip: image_subset_iff_funcset) qed with inessential_eq_continuous_logarithm_circle that show ?thesis by metis @@ -4104,7 +4109,7 @@ lemma inessential_spheremap_2: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes a2: "2 < DIM('a)" and b2: "DIM('b) = 2" - and contf: "continuous_on (sphere a r) f" and fim: "f `(sphere a r) \ (sphere b s)" + and contf: "continuous_on (sphere a r) f" and fim: "f \ (sphere a r) \ (sphere b s)" obtains c where "homotopic_with_canon (\z. True) (sphere a r) (sphere b s) f (\x. c)" proof (cases "s \ 0") case True @@ -4118,20 +4123,20 @@ by (auto simp: homeomorphic_def) then have conth: "continuous_on (sphere b s) h" and contk: "continuous_on (sphere 0 1) k" - and him: "h ` sphere b s \ sphere 0 1" - and kim: "k ` sphere 0 1 \ sphere b s" - by (simp_all add: homeomorphism_def) + and him: "h \ sphere b s \ sphere 0 1" + and kim: "k \ sphere 0 1 \ sphere b s" + by (force simp: homeomorphism_def)+ obtain c where "homotopic_with_canon (\z. True) (sphere a r) (sphere 0 1) (h \ f) (\x. c)" proof (rule inessential_spheremap_2_aux [OF a2]) show "continuous_on (sphere a r) (h \ f)" - by (meson continuous_on_compose [OF contf] conth continuous_on_subset fim) - show "(h \ f) ` sphere a r \ sphere 0 1" + by (meson contf conth continuous_on_compose continuous_on_subset fim image_subset_iff_funcset) + show "(h \ f) \ sphere a r \ sphere 0 1" using fim him by force qed auto then have "homotopic_with_canon (\f. True) (sphere a r) (sphere b s) (k \ (h \ f)) (k \ (\x. c))" by (rule homotopic_with_compose_continuous_left [OF _ contk kim]) moreover have "\x. r = dist a x \ f x = k (h (f x))" - by (metis fim hk homeomorphism_def image_subset_iff mem_sphere) + by (metis fim hk homeomorphism_def image_subset_iff mem_sphere image_subset_iff_funcset) ultimately have "homotopic_with_canon (\z. True) (sphere a r) (sphere b s) f (\x. k c)" by (auto intro: homotopic_with_eq) then show ?thesis @@ -4330,16 +4335,16 @@ definition\<^marker>\tag important\ Borsukian where "Borsukian S \ - \f. continuous_on S f \ f ` S \ (- {0::complex}) + \f. continuous_on S f \ f \ S \ (- {0::complex}) \ (\a. homotopic_with_canon (\h. True) S (- {0}) f (\x. a))" lemma Borsukian_retraction_gen: assumes "Borsukian S" "continuous_on S h" "h ` S = T" - "continuous_on T k" "k ` T \ S" "\y. y \ T \ h(k y) = y" + "continuous_on T k" "k \ T \ S" "\y. y \ T \ h(k y) = y" shows "Borsukian T" proof - interpret R: Retracts S h T k - using assms by (simp add: Retracts.intro) + using assms by (simp add: image_subset_iff_funcset Retracts.intro) show ?thesis using assms apply (clarsimp simp add: Borsukian_def) @@ -4348,7 +4353,7 @@ qed lemma retract_of_Borsukian: "\Borsukian T; S retract_of T\ \ Borsukian S" - by (smt (verit) Borsukian_retraction_gen retract_of_def retraction retraction_def retraction_subset) + by (smt (verit) Borsukian_retraction_gen retract_of_def retraction retraction_def retraction_subset image_subset_iff_funcset) lemma homeomorphic_Borsukian: "\Borsukian S; S homeomorphic T\ \ Borsukian T" using Borsukian_retraction_gen order_refl @@ -4374,29 +4379,29 @@ and T :: "'b::real_normed_vector set" assumes "S homotopy_eqv T" shows "(Borsukian S \ Borsukian T)" - by (meson Borsukian_def assms homotopy_eqv_cohomotopic_triviality_null) + by (meson Borsukian_def assms homotopy_eqv_cohomotopic_triviality_null image_subset_iff_funcset) lemma Borsukian_alt: fixes S :: "'a::real_normed_vector set" shows "Borsukian S \ - (\f g. continuous_on S f \ f ` S \ -{0} \ - continuous_on S g \ g ` S \ -{0} + (\f g. continuous_on S f \ f \ S \ -{0} \ + continuous_on S g \ g \ S \ -{0} \ homotopic_with_canon (\h. True) S (- {0::complex}) f g)" unfolding Borsukian_def homotopic_triviality - by (simp add: path_connected_punctured_universe) + by (force simp add: path_connected_punctured_universe) lemma Borsukian_continuous_logarithm: fixes S :: "'a::real_normed_vector set" shows "Borsukian S \ - (\f. continuous_on S f \ f ` S \ (- {0::complex}) + (\f. continuous_on S f \ f \ S \ (- {0::complex}) \ (\g. continuous_on S g \ (\x \ S. f x = exp(g x))))" by (simp add: Borsukian_def inessential_eq_continuous_logarithm) lemma Borsukian_continuous_logarithm_circle: fixes S :: "'a::real_normed_vector set" shows "Borsukian S \ - (\f. continuous_on S f \ f ` S \ sphere (0::complex) 1 + (\f. continuous_on S f \ f \ S \ sphere (0::complex) 1 \ (\g. continuous_on S g \ (\x \ S. f x = exp(g x))))" (is "?lhs = ?rhs") proof @@ -4405,12 +4410,12 @@ next assume RHS [rule_format]: ?rhs show ?lhs - proof (clarsimp simp: Borsukian_continuous_logarithm) + proof (clarsimp simp: Borsukian_continuous_logarithm Pi_iff) fix f :: "'a \ complex" - assume contf: "continuous_on S f" and 0: "0 \ f ` S" + assume contf: "continuous_on S f" and 0: "\i\S. f i \ 0" then have "continuous_on S (\x. f x / complex_of_real (cmod (f x)))" by (intro continuous_intros) auto - moreover have "(\x. f x / complex_of_real (cmod (f x))) ` S \ sphere 0 1" + moreover have "(\x. f x / complex_of_real (cmod (f x))) \ S \ sphere 0 1" using 0 by (auto simp: norm_divide) ultimately obtain g where contg: "continuous_on S g" and fg: "\x \ S. f x / complex_of_real (cmod (f x)) = exp(g x)" @@ -4431,7 +4436,7 @@ lemma Borsukian_continuous_logarithm_circle_real: fixes S :: "'a::real_normed_vector set" shows "Borsukian S \ - (\f. continuous_on S f \ f ` S \ sphere (0::complex) 1 + (\f. continuous_on S f \ f \ S \ sphere (0::complex) 1 \ (\g. continuous_on S (complex_of_real \ g) \ (\x \ S. f x = exp(\ * of_real(g x)))))" (is "?lhs = ?rhs") proof @@ -4439,11 +4444,11 @@ show ?rhs proof (clarify) fix f :: "'a \ complex" - assume "continuous_on S f" and f01: "f ` S \ sphere 0 1" + assume "continuous_on S f" and f01: "f \ S \ sphere 0 1" then obtain g where contg: "continuous_on S g" and "\x. x \ S \ f x = exp(g x)" using LHS by (auto simp: Borsukian_continuous_logarithm_circle) then have "\x\S. f x = exp (\ * complex_of_real ((Im \ g) x))" - using f01 exp_eq_polar norm_exp_eq_Re by auto + using f01 exp_eq_polar norm_exp_eq_Re by (fastforce simp: Pi_iff) then show "\g. continuous_on S (complex_of_real \ g) \ (\x\S. f x = exp (\ * complex_of_real (g x)))" by (rule_tac x="Im \ g" in exI) (force intro: continuous_intros contg) qed @@ -4452,7 +4457,7 @@ show ?lhs proof (clarsimp simp: Borsukian_continuous_logarithm_circle) fix f :: "'a \ complex" - assume "continuous_on S f" and f01: "f ` S \ sphere 0 1" + assume "continuous_on S f" and f01: "f \ S \ sphere 0 1" then obtain g where contg: "continuous_on S (complex_of_real \ g)" and "\x. x \ S \ f x = exp(\ * of_real(g x))" by (metis RHS) then show "\g. continuous_on S g \ (\x\S. f x = exp (g x))" @@ -4463,17 +4468,18 @@ lemma Borsukian_circle: fixes S :: "'a::real_normed_vector set" shows "Borsukian S \ - (\f. continuous_on S f \ f ` S \ sphere (0::complex) 1 + (\f. continuous_on S f \ f \ S \ sphere (0::complex) 1 \ (\a. homotopic_with_canon (\h. True) S (sphere (0::complex) 1) f (\x. a)))" by (simp add: inessential_eq_continuous_logarithm_circle Borsukian_continuous_logarithm_circle_real) lemma contractible_imp_Borsukian: "contractible S \ Borsukian S" - by (meson Borsukian_def nullhomotopic_from_contractible) + by (meson Borsukian_def nullhomotopic_from_contractible image_subset_iff_funcset) lemma simply_connected_imp_Borsukian: fixes S :: "'a::real_normed_vector set" shows "\simply_connected S; locally path_connected S\ \ Borsukian S" - by (metis (no_types, lifting) Borsukian_continuous_logarithm continuous_logarithm_on_simply_connected image_eqI subset_Compl_singleton) + by (smt (verit, del_insts) continuous_logarithm_on_simply_connected Borsukian_continuous_logarithm_circle + PiE mem_sphere_0 norm_eq_zero zero_neq_one) lemma starlike_imp_Borsukian: fixes S :: "'a::real_normed_vector set" @@ -4504,19 +4510,19 @@ \continuous_on S f; continuous_on T g; \x. x \ S \ x \ T \ f x = g x\ \ continuous_on (S \ T) (\x. if x \ S then f x else g x)" shows "Borsukian(S \ T)" -proof (clarsimp simp add: Borsukian_continuous_logarithm) +proof (clarsimp simp add: Borsukian_continuous_logarithm Pi_iff) fix f :: "'a \ complex" - assume contf: "continuous_on (S \ T) f" and 0: "0 \ f ` (S \ T)" + assume contf: "continuous_on (S \ T) f" and 0: "\i\S \ T. f i \ 0" then have contfS: "continuous_on S f" and contfT: "continuous_on T f" using continuous_on_subset by auto have "\continuous_on S f; f ` S \ -{0}\ \ \g. continuous_on S g \ (\x \ S. f x = exp(g x))" using BS by (auto simp: Borsukian_continuous_logarithm) then obtain g where contg: "continuous_on S g" and fg: "\x. x \ S \ f x = exp(g x)" - using "0" contfS by blast + using "0" contfS by force have "\continuous_on T f; f ` T \ -{0}\ \ \g. continuous_on T g \ (\x \ T. f x = exp(g x))" using BT by (auto simp: Borsukian_continuous_logarithm) then obtain h where conth: "continuous_on T h" and fh: "\x. x \ T \ f x = exp(h x)" - using "0" contfT by blast + using "0" contfT by force show "\g. continuous_on (S \ T) g \ (\x\S \ T. f x = exp (g x))" proof (cases "S \ T = {}") case True @@ -4592,9 +4598,9 @@ assumes "Borsukian S" and contf: "continuous_on S f" and fim: "f ` S = T" and "compact S" and conn: "\y. y \ T \ connected {x. x \ S \ f x = y}" shows "Borsukian T" -proof (clarsimp simp add: Borsukian_continuous_logarithm) +proof (clarsimp simp: Borsukian_continuous_logarithm Pi_iff) fix g :: "'b \ complex" - assume contg: "continuous_on T g" and 0: "0 \ g ` T" + assume contg: "continuous_on T g" and 0: "\i\T. g i \ 0" have "continuous_on S (g \ f)" using contf contg continuous_on_compose fim by blast moreover have "(g \ f) ` S \ -{0}" @@ -4631,7 +4637,7 @@ proof (rule continuous_from_closed_graph [of "h ` S"]) show "compact (h ` S)" by (simp add: \compact S\ compact_continuous_image conth) - show "(h \ f') ` T \ h ` S" + show "(h \ f') \ T \ h ` S" by (auto simp: f') have "h x = h (f' (f x))" if "x \ S" for x using * [of "f x"] fim that unfolding constant_on_def by clarsimp (metis f' imageI right_minus_eq) @@ -4660,10 +4666,10 @@ shows "Borsukian T" proof (clarsimp simp add: Borsukian_continuous_logarithm_circle_real) fix g :: "'b \ complex" - assume contg: "continuous_on T g" and gim: "g ` T \ sphere 0 1" + assume contg: "continuous_on T g" and gim: "g \ T \ sphere 0 1" have "continuous_on S (g \ f)" using contf contg continuous_on_compose fim by blast - moreover have "(g \ f) ` S \ sphere 0 1" + moreover have "(g \ f) \ S \ sphere 0 1" using fim gim by auto ultimately obtain h where cont_cxh: "continuous_on S (complex_of_real \ h)" and gfh: "\x. x \ S \ (g \ f) x = exp(\ * of_real(h x))" @@ -4677,7 +4683,8 @@ show "continuous_on {x \ S. f x = y} h" by (rule continuous_on_subset [OF conth]) auto have "compact (S \ f -` {y})" - by (rule proper_map_from_compact [OF contf _ \compact S\, of T]) (simp_all add: fim that) + using that proper_map_from_compact [OF contf _ \compact S\] fim + by force then show "compact {x \ S. f x = y}" by (auto simp: vimage_def Int_def) qed @@ -4985,7 +4992,7 @@ with qV qW show ?thesis by force qed obtain g where contg: "continuous_on U g" - and circle: "g ` U \ sphere 0 1" + and circle: "g \ U \ sphere 0 1" and S: "\x. x \ S \ g x = exp(pi * \ * q x)" and T: "\x. x \ T \ g x = 1 / exp(pi * \ * q x)" proof @@ -5415,7 +5422,7 @@ proof (rule Borsuk_homotopy_extension_homotopic [OF _ _ continuous_on_const _ homotopic_with_symD [OF a]]) show "closedin (top_of_set UNIV) S" using assms by auto - show "range (\t. a) \ - {0}" + show "(\t. a) \ UNIV \ - {0}" using a homotopic_with_imp_subset2 False by blast qed (use anr that in \force+\) then show ?thesis diff -r d4125fc10c0c -r 1260be3f33a4 src/HOL/Analysis/Homeomorphism.thy --- a/src/HOL/Analysis/Homeomorphism.thy Sun Jul 02 20:41:07 2023 +0200 +++ b/src/HOL/Analysis/Homeomorphism.thy Mon Jul 03 16:46:37 2023 +0100 @@ -1112,10 +1112,10 @@ fixes g1 :: "'a \ 'c::real_normed_vector" assumes cov: "covering_space c p S" and eq: "g1 a = g2 a" - and f: "continuous_on T f" "f ` T \ S" - and g1: "continuous_on T g1" "g1 ` T \ c" + and f: "continuous_on T f" "f \ T \ S" + and g1: "continuous_on T g1" "g1 \ T \ c" and fg1: "\x. x \ T \ f x = p(g1 x)" - and g2: "continuous_on T g2" "g2 ` T \ c" + and g2: "continuous_on T g2" "g2 \ T \ c" and fg2: "\x. x \ T \ f x = p(g2 x)" and u_compt: "U \ components T" and "a \ U" "x \ U" shows "g1 x = g2 x" @@ -1175,9 +1175,9 @@ fixes g1 :: "'a \ 'c::real_normed_vector" assumes "covering_space c p S" "g1 a = g2 a" - "continuous_on T f" "f ` T \ S" - "continuous_on T g1" "g1 ` T \ c" "\x. x \ T \ f x = p(g1 x)" - "continuous_on T g2" "g2 ` T \ c" "\x. x \ T \ f x = p(g2 x)" + "continuous_on T f" "f \ T \ S" + "continuous_on T g1" "g1 \ T \ c" "\x. x \ T \ f x = p(g1 x)" + "continuous_on T g2" "g2 \ T \ c" "\x. x \ T \ f x = p(g2 x)" "connected T" "a \ T" "x \ T" shows "g1 x = g2 x" using covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv @@ -1315,11 +1315,11 @@ and h :: "real \ 'c::real_normed_vector \ 'b" assumes cov: "covering_space C p S" and conth: "continuous_on ({0..1} \ U) h" - and him: "h ` ({0..1} \ U) \ S" + and him: "h \ ({0..1} \ U) \ S" and heq: "\y. y \ U \ h (0,y) = p(f y)" - and contf: "continuous_on U f" and fim: "f ` U \ C" + and contf: "continuous_on U f" and fim: "f \ U \ C" obtains k where "continuous_on ({0..1} \ U) k" - "k ` ({0..1} \ U) \ C" + "k \ ({0..1} \ U) \ C" "\y. y \ U \ k(0, y) = f y" "\z. z \ {0..1} \ U \ h z = p(k z)" proof - @@ -1459,7 +1459,7 @@ proof (rule continuous_openin_preimage [OF _ _ opeC']) show "continuous_on V (k \ Pair (n/N))" by (intro continuous_intros continuous_on_subset [OF contk], auto) - show "(k \ Pair (n/N)) ` V \ C" + show "(k \ Pair (n/N)) \ V \ C" using kim by (auto simp: \y \ V\ W) qed obtain N' where opeUN': "openin (top_of_set U) N'" @@ -1633,19 +1633,19 @@ using*V by (simp add: \y \ V i\ \y \ V j\ that) show conth_y: "continuous_on ({0..1} \ {y}) h" using VU \y \ V j\ that by (auto intro: continuous_on_subset [OF conth]) - show "h ` ({0..1} \ {y}) \ S" + show "h \ ({0..1} \ {y}) \ S" using \y \ V i\ assms(3) VU that by fastforce show "continuous_on ({0..1} \ {y}) (fs i)" using continuous_on_subset [OF contfs] \i \ U\ by (simp add: \y \ V i\ subset_iff) - show "fs i ` ({0..1} \ {y}) \ C" + show "fs i \ ({0..1} \ {y}) \ C" using "*" \y \ V i\ \i \ U\ by fastforce show "\x. x \ {0..1} \ {y} \ h x = p (fs i x)" using "*" \y \ V i\ \i \ U\ by blast show "continuous_on ({0..1} \ {y}) (fs j)" using continuous_on_subset [OF contfs] \j \ U\ by (simp add: \y \ V j\ subset_iff) - show "fs j ` ({0..1} \ {y}) \ C" + show "fs j \ ({0..1} \ {y}) \ C" using "*" \y \ V j\ \j \ U\ by fastforce show "\x. x \ {0..1} \ {y} \ h x = p (fs j x)" using "*" \y \ V j\ \j \ U\ by blast @@ -1660,7 +1660,7 @@ qed force show ?thesis proof - show "k ` ({0..1} \ U) \ C" + show "k \ ({0..1} \ U) \ C" using V*k VU by fastforce show "\y. y \ U \ k (0, y) = f y" by (simp add: V*k) @@ -1674,11 +1674,11 @@ and h :: "'c::real_normed_vector \ real \ 'b" assumes cov: "covering_space C p S" and conth: "continuous_on (U \ {0..1}) h" - and him: "h ` (U \ {0..1}) \ S" + and him: "h \ (U \ {0..1}) \ S" and heq: "\y. y \ U \ h (y,0) = p(f y)" - and contf: "continuous_on U f" and fim: "f ` U \ C" + and contf: "continuous_on U f" and fim: "f \ U \ C" obtains k where "continuous_on (U \ {0..1}) k" - "k ` (U \ {0..1}) \ C" + "k \ (U \ {0..1}) \ C" "\y. y \ U \ k(y, 0) = f y" "\z. z \ U \ {0..1} \ h z = p(k z)" proof - @@ -1701,13 +1701,13 @@ fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector" and g:: "'c::real_normed_vector \ 'a" assumes cov: "covering_space C p S" and contg: "continuous_on U g" - and gim: "g ` U \ C" + and gim: "g \ U \ C" and pgeq: "\y. y \ U \ p(g y) = f y" and hom: "homotopic_with_canon (\x. True) U S f f'" obtains g' where "continuous_on U g'" "image g' U \ C" "\y. y \ U \ p(g' y) = f' y" proof - obtain h where conth: "continuous_on ({0..1::real} \ U) h" - and him: "h ` ({0..1} \ U) \ S" + and him: "h \ ({0..1} \ U) \ S" and h0: "\x. h(0, x) = f x" and h1: "\x. h(1, x) = f' x" using hom by (auto simp: homotopic_with_def) @@ -1717,7 +1717,7 @@ and kim: "k ` ({0..1} \ U) \ C" and k0: "\y. y \ U \ k(0, y) = g y" and heq: "\z. z \ {0..1} \ U \ h z = p(k z)" - using covering_space_lift_homotopy [OF cov conth him _ contg gim] by metis + using covering_space_lift_homotopy [OF cov conth him _ contg gim] by (metis image_subset_iff_funcset) show ?thesis proof show "continuous_on U (k \ Pair 1)" @@ -1743,7 +1743,7 @@ then obtain b where b: "b \ C" "p b = a" using covering_space_imp_surjective [OF cov] homotopic_with_imp_subset2 [OF hom] by auto - then have gim: "(\y. b) ` U \ C" + then have gim: "(\y. b) \ U \ C" by blast show ?thesis proof (rule covering_space_lift_homotopic_function [OF cov continuous_on_const gim]) @@ -1770,7 +1770,7 @@ proof (rule covering_space_lift_homotopy [OF cov, of "{undefined}" "g \ fst"]) show "continuous_on ({0..1::real} \ {undefined::'c}) (g \ fst)" using \path g\ by (intro continuous_intros) (simp add: path_def) - show "(g \ fst) ` ({0..1} \ {undefined}) \ S" + show "(g \ fst) \ ({0..1} \ {undefined}) \ S" using pag by (auto simp: path_image_def) show "(g \ fst) (0, y) = p a" if "y \ {undefined}" for y::'c by (metis comp_def fst_conv pas pathstart_def) @@ -1815,13 +1815,13 @@ proof - obtain h :: "real \ real \ 'b" where conth: "continuous_on ({0..1} \ {0..1}) h" - and him: "h ` ({0..1} \ {0..1}) \ S" + and him: "h \ ({0..1} \ {0..1}) \ S" and h0: "\x. h (0, x) = g1 x" and h1: "\x. h (1, x) = g2 x" and heq0: "\t. t \ {0..1} \ h (t, 0) = g1 0" and heq1: "\t. t \ {0..1} \ h (t, 1) = g1 1" - using hom by (auto simp: homotopic_paths_def homotopic_with_def pathstart_def pathfinish_def) + using hom by (auto simp: homotopic_paths_def homotopic_with_def pathstart_def pathfinish_def image_subset_iff_funcset) obtain k where contk: "continuous_on ({0..1} \ {0..1}) k" - and kim: "k ` ({0..1} \ {0..1}) \ C" + and kim: "k \ ({0..1} \ {0..1}) \ C" and kh2: "\y. y \ {0..1} \ k (y, 0) = h2 0" and hpk: "\z. z \ {0..1} \ {0..1} \ h z = p (k z)" proof (rule covering_space_lift_homotopy_alt [OF cov conth him]) @@ -1830,11 +1830,11 @@ qed (use path_image_def pih2 in \fastforce+\) have contg1: "continuous_on {0..1} g1" and contg2: "continuous_on {0..1} g2" using \path g1\ \path g2\ path_def by blast+ - have g1im: "g1 ` {0..1} \ S" and g2im: "g2 ` {0..1} \ S" + have g1im: "g1 \ {0..1} \ S" and g2im: "g2 \ {0..1} \ S" using path_image_def pig1 pig2 by auto have conth1: "continuous_on {0..1} h1" and conth2: "continuous_on {0..1} h2" using \path h1\ \path h2\ path_def by blast+ - have h1im: "h1 ` {0..1} \ C" and h2im: "h2 ` {0..1} \ C" + have h1im: "h1 \ {0..1} \ C" and h2im: "h2 \ {0..1} \ C" using path_image_def pih1 pih2 by auto show ?thesis unfolding homotopic_paths pathstart_def pathfinish_def @@ -1911,13 +1911,13 @@ and f :: "'c::real_normed_vector \ 'b" assumes cov: "covering_space C p S" and "a \ C" "z \ U" and U: "path_connected U" "locally path_connected U" - and contf: "continuous_on U f" and fim: "f ` U \ S" + and contf: "continuous_on U f" and fim: "f \ U \ S" and feq: "f z = p a" and hom: "\r. \path r; path_image r \ U; pathstart r = z; pathfinish r = z\ \ \q. path q \ path_image q \ C \ pathstart q = a \ pathfinish q = a \ homotopic_paths S (f \ r) (p \ q)" - obtains g where "continuous_on U g" "g ` U \ C" "g z = a" "\y. y \ U \ p(g y) = f y" + obtains g where "continuous_on U g" "g \ U \ C" "g z = a" "\y. y \ U \ p(g y) = f y" proof - have *: "\g h. path g \ path_image g \ U \ pathstart g = z \ pathfinish g = y \ @@ -1934,7 +1934,7 @@ show "path (f \ g)" using \path g\ \path_image g \ U\ contf continuous_on_subset path_continuous_image by blast show "path_image (f \ g) \ S" - by (metis \path_image g \ U\ fim image_mono path_image_compose subset_trans) + by (metis \path_image g \ U\ fim image_mono path_image_compose subset_trans image_subset_iff_funcset) show "pathstart (f \ g) = p a" by (simp add: feq pastg pathstart_compose) qed auto @@ -1975,11 +1975,11 @@ show "g ` (*\<^sub>R) 2 ` {0..1/2} \ U" using g path_image_def by fastforce qed auto - show "(f \ g \ (*\<^sub>R) 2) ` {0..1/2} \ S" - using g(2) path_image_def fim by fastforce - show "(h \ (*\<^sub>R) 2) ` {0..1/2} \ C" + show "(f \ g \ (*\<^sub>R) 2) \ {0..1/2} \ S" + using g(2) fim by (fastforce simp: path_image_def image_subset_iff_funcset) + show "(h \ (*\<^sub>R) 2) \ {0..1/2} \ C" using h path_image_def by fastforce - show "q' ` {0..1/2} \ C" + show "q' \ {0..1/2} \ C" using \path_image q' \ C\ path_image_def by fastforce show "\x. x \ {0..1/2} \ (f \ g \ (*\<^sub>R) 2) x = p (q' x)" by (auto simp: joinpaths_def pq'_eq) @@ -2000,11 +2000,11 @@ show "reversepath g' ` (\t. 2 *\<^sub>R t - 1) ` {1/2<..1} \ U" using g' by (auto simp: path_image_def reversepath_def) qed (use g' in auto) - show "(f \ reversepath g' \ (\t. 2 *\<^sub>R t - 1)) ` {1/2<..1} \ S" + show "(f \ reversepath g' \ (\t. 2 *\<^sub>R t - 1)) \ {1/2<..1} \ S" using g'(2) path_image_def fim by (auto simp: image_subset_iff path_image_def reversepath_def) - show "q' ` {1/2<..1} \ C" + show "q' \ {1/2<..1} \ C" using \path_image q' \ C\ path_image_def by fastforce - show "(reversepath h' \ (\t. 2 *\<^sub>R t - 1)) ` {1/2<..1} \ C" + show "(reversepath h' \ (\t. 2 *\<^sub>R t - 1)) \ {1/2<..1} \ C" using h' by (simp add: path_image_def reversepath_def subset_eq) show "\x. x \ {1/2<..1} \ (f \ reversepath g' \ (\t. 2 *\<^sub>R t - 1)) x = p (q' x)" by (auto simp: joinpaths_def pq'_eq) @@ -2036,7 +2036,7 @@ using*[OF \y \ U\] by (metis l atLeastAtMost_iff order_refl pathfinish_def zero_le_one) show "l z = a" using l [of "linepath z z" z "linepath a a"] by (auto simp: assms) - show LC: "l ` U \ C" + show LC: "l \ U \ C" by (clarify dest!: *) (metis (full_types) l pathfinish_in_path_image subsetCE) have "\T. openin (top_of_set U) T \ y \ T \ T \ U \ l -` X" if X: "openin (top_of_set C) X" and "y \ U" "l y \ X" for X y @@ -2080,7 +2080,8 @@ have "openin (top_of_set S) (W \ p' -` (W' \ X))" proof (rule openin_trans) show "openin (top_of_set W) (W \ p' -` (W' \ X))" - using X \W' \ C\ by (intro continuous_openin_preimage [OF contp' p'im]) (auto simp: openin_open) + using X \W' \ C\ + by (metis continuous_on_open contp' homUW' homeomorphism_image2 inf.assoc inf.orderE openin_open) show "openin (top_of_set S) W" using WV by blast qed @@ -2154,6 +2155,7 @@ qed qed then show "continuous_on U l" + using vimage_eq openin_subopen continuous_on_open_gen [OF LC] by (metis IntD1 IntD2 vimage_eq openin_subopen continuous_on_open_gen [OF LC]) qed qed @@ -2163,11 +2165,11 @@ and f :: "'c::real_normed_vector \ 'b" assumes cov: "covering_space C p S" "a \ C" "z \ U" and U: "path_connected U" "locally path_connected U" - and contf: "continuous_on U f" and fim: "f ` U \ S" + and contf: "continuous_on U f" and fim: "f \ U \ S" and feq: "f z = p a" and hom: "\r. \path r; path_image r \ U; pathstart r = z; pathfinish r = z\ \ \b. homotopic_paths S (f \ r) (linepath b b)" - obtains g where "continuous_on U g" "g ` U \ C" "g z = a" "\y. y \ U \ p(g y) = f y" + obtains g where "continuous_on U g" "g \ U \ C" "g z = a" "\y. y \ U \ p(g y) = f y" proof (rule covering_space_lift_general [OF cov U contf fim feq]) fix r assume "path r" "path_image r \ U" "pathstart r = z" "pathfinish r = z" @@ -2190,9 +2192,9 @@ and f :: "'c::real_normed_vector \ 'b" assumes cov: "covering_space C p S" "a \ C" "z \ U" and scU: "simply_connected U" and lpcU: "locally path_connected U" - and contf: "continuous_on U f" and fim: "f ` U \ S" + and contf: "continuous_on U f" and fim: "f \ U \ S" and feq: "f z = p a" - obtains g where "continuous_on U g" "g ` U \ C" "g z = a" "\y. y \ U \ p(g y) = f y" + obtains g where "continuous_on U g" "g \ U \ C" "g z = a" "\y. y \ U \ p(g y) = f y" proof (rule covering_space_lift_stronger [OF cov _ lpcU contf fim feq]) show "path_connected U" using scU simply_connected_eq_contractible_loop_some by blast @@ -2211,8 +2213,8 @@ and f :: "'c::real_normed_vector \ 'b" assumes cov: "covering_space C p S" and U: "simply_connected U" "locally path_connected U" - and contf: "continuous_on U f" and fim: "f ` U \ S" - obtains g where "continuous_on U g" "g ` U \ C" "\y. y \ U \ p(g y) = f y" + and contf: "continuous_on U f" and fim: "f \ U \ S" + obtains g where "continuous_on U g" "g \ U \ C" "\y. y \ U \ p(g y) = f y" proof (cases "U = {}") case True with that show ?thesis by auto @@ -2220,7 +2222,7 @@ case False then obtain z where "z \ U" by blast then obtain a where "a \ C" "f z = p a" - by (metis cov covering_space_imp_surjective fim image_iff image_subset_iff) + by (metis cov covering_space_imp_surjective fim image_iff Pi_iff) then show ?thesis by (metis that covering_space_lift_strong [OF cov _ \z \ U\ U contf fim]) qed diff -r d4125fc10c0c -r 1260be3f33a4 src/HOL/Analysis/Homotopy.thy --- a/src/HOL/Analysis/Homotopy.thy Sun Jul 02 20:41:07 2023 +0200 +++ b/src/HOL/Analysis/Homotopy.thy Mon Jul 03 16:46:37 2023 +0100 @@ -124,6 +124,14 @@ "homotopic_with_canon P X Y f g \ g ` X \ Y" by (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps) +lemma homotopic_with_imp_funspace1: + "homotopic_with_canon P X Y f g \ f \ X \ Y" + using homotopic_with_imp_subset1 by blast + +lemma homotopic_with_imp_funspace2: + "homotopic_with_canon P X Y f g \ g \ X \ Y" + using homotopic_with_imp_subset2 by blast + lemma homotopic_with_subset_left: "\homotopic_with_canon P X Y f g; Z \ X\ \ homotopic_with_canon P Z Y f g" unfolding homotopic_with_def by (auto elim!: continuous_on_subset ex_forward) @@ -150,7 +158,7 @@ have *: "continuous_map (prod_topology ?I01 X) (prod_topology ?I01 X) ?j" proof - have "continuous_map (prod_topology ?I01 X) (subtopology (prod_topology euclideanreal X) ({0..1} \ topspace X)) ?j" - by (simp add: continuous_map_into_subtopology [OF 1] image_subset_iff) + by (simp add: continuous_map_into_subtopology [OF 1] image_subset_iff flip: image_subset_iff_funcset) then show ?thesis by (simp add: prod_topology_subtopology(1)) qed @@ -262,14 +270,14 @@ by (metis assms homotopic_with_compose_continuous_map_left homotopic_with_compose_continuous_map_right homotopic_with_imp_continuous_maps homotopic_with_trans) proposition homotopic_with_compose_continuous_right: - "\homotopic_with_canon (\f. p (f \ h)) X Y f g; continuous_on W h; h ` W \ X\ + "\homotopic_with_canon (\f. p (f \ h)) X Y f g; continuous_on W h; h \ W \ X\ \ homotopic_with_canon p W Y (f \ h) (g \ h)" - by (simp add: homotopic_with_compose_continuous_map_right) + by (simp add: homotopic_with_compose_continuous_map_right image_subset_iff_funcset) proposition homotopic_with_compose_continuous_left: - "\homotopic_with_canon (\f. p (h \ f)) X Y f g; continuous_on Y h; h ` Y \ Z\ + "\homotopic_with_canon (\f. p (h \ f)) X Y f g; continuous_on Y h; h \ Y \ Z\ \ homotopic_with_canon p X Z (h \ f) (h \ g)" - by (simp add: homotopic_with_compose_continuous_map_left) + by (simp add: homotopic_with_compose_continuous_map_left image_subset_iff_funcset) lemma homotopic_from_subtopology: "homotopic_with P X X' f g \ homotopic_with P (subtopology X S) X' f g" @@ -397,15 +405,15 @@ text\Homotopic triviality implicitly incorporates path-connectedness.\ lemma homotopic_triviality: - shows "(\f g. continuous_on S f \ f ` S \ T \ - continuous_on S g \ g ` S \ T + shows "(\f g. continuous_on S f \ f \ S \ T \ + continuous_on S g \ g \ S \ T \ homotopic_with_canon (\x. True) S T f g) \ (S = {} \ path_connected T) \ - (\f. continuous_on S f \ f ` S \ T \ (\c. homotopic_with_canon (\x. True) S T f (\x. c)))" + (\f. continuous_on S f \ f \ S \ T \ (\c. homotopic_with_canon (\x. True) S T f (\x. c)))" (is "?lhs = ?rhs") proof (cases "S = {} \ T = {}") case True then show ?thesis - by (auto simp: homotopic_on_emptyI) + by (auto simp: homotopic_on_emptyI simp flip: image_subset_iff_funcset) next case False show ?thesis proof @@ -418,7 +426,7 @@ using False homotopic_constant_maps [of "top_of_set S" "top_of_set T" a b] by auto qed moreover - have "\c. homotopic_with_canon (\x. True) S T f (\x. c)" if "continuous_on S f" "f ` S \ T" for f + have "\c. homotopic_with_canon (\x. True) S T f (\x. c)" if "continuous_on S f" "f \ S \ T" for f using False LHS continuous_on_const that by blast ultimately show ?rhs by (simp add: path_connected_component) @@ -429,9 +437,9 @@ show ?lhs proof clarify fix f g - assume "continuous_on S f" "f ` S \ T" "continuous_on S g" "g ` S \ T" + assume "continuous_on S f" "f \ S \ T" "continuous_on S g" "g \ S \ T" obtain c d where c: "homotopic_with_canon (\x. True) S T f (\x. c)" and d: "homotopic_with_canon (\x. True) S T g (\x. d)" - using False \continuous_on S f\ \f ` S \ T\ RHS \continuous_on S g\ \g ` S \ T\ by blast + using RHS \continuous_on S f\ \continuous_on S g\ \f \ S \ T\ \g \ S \ T\ by presburger with T have "path_component T c d" by (metis False ex_in_conv homotopic_with_imp_subset2 image_subset_iff path_connected_component) then have "homotopic_with_canon (\x. True) S T (\x. c) (\x. d)" @@ -454,7 +462,7 @@ lemma homotopic_paths: "homotopic_paths S p q \ (\h. continuous_on ({0..1} \ {0..1}) h \ - h ` ({0..1} \ {0..1}) \ S \ + h \ ({0..1} \ {0..1}) \ S \ (\x \ {0..1}. h(0,x) = p x) \ (\x \ {0..1}. h(1,x) = q x) \ (\t \ {0..1::real}. pathstart(h \ Pair t) = pathstart p \ @@ -500,7 +508,7 @@ assumes "path p" and pips: "path_image p \ S" and contf: "continuous_on {0..1} f" - and f01:"f ` {0..1} \ {0..1}" + and f01 :"f \ {0..1} \ {0..1}" and [simp]: "f(0) = 0" "f(1) = 1" and q: "\t. t \ {0..1} \ q(t) = p(f t)" shows "homotopic_paths S p q" @@ -508,15 +516,15 @@ have contp: "continuous_on {0..1} p" by (metis \path p\ path_def) then have "continuous_on {0..1} (p \ f)" - using contf continuous_on_compose continuous_on_subset f01 by blast + by (meson assms(4) contf continuous_on_compose continuous_on_subset image_subset_iff_funcset) then have "path q" by (simp add: path_def) (metis q continuous_on_cong) have piqs: "path_image q \ S" - by (metis (no_types, opaque_lifting) pips f01 image_subset_iff path_image_def q) + by (smt (verit, ccfv_threshold) Pi_iff assms(2) assms(4) assms(7) image_subset_iff path_defs(4)) have fb0: "\a b. \0 \ a; a \ 1; 0 \ b; b \ 1\ \ 0 \ (1 - a) * f b + a * b" using f01 by force have fb1: "\0 \ a; a \ 1; 0 \ b; b \ 1\ \ (1 - a) * f b + a * b \ 1" for a b - using f01 [THEN subsetD, of "f b"] by (simp add: convex_bound_le) + by (intro convex_bound_le) (use f01 in auto) have "homotopic_paths S q p" proof (rule homotopic_paths_trans) show "homotopic_paths S q (p \ f)" @@ -585,9 +593,9 @@ done proposition homotopic_paths_continuous_image: - "\homotopic_paths S f g; continuous_on S h; h ` S \ t\ \ homotopic_paths t (h \ f) (h \ g)" + "\homotopic_paths S f g; continuous_on S h; h \ S \ t\ \ homotopic_paths t (h \ f) (h \ g)" unfolding homotopic_paths_def - by (simp add: homotopic_with_compose_continuous_map_left pathfinish_compose pathstart_compose) + by (simp add: homotopic_with_compose_continuous_map_left pathfinish_compose pathstart_compose image_subset_iff_funcset) subsection\Group properties for homotopy of paths\ @@ -711,9 +719,9 @@ by (auto intro: homotopic_with_eq [OF homotopic_with_refl [where f = p, THEN iffD2]]) proposition homotopic_loops_continuous_image: - "\homotopic_loops S f g; continuous_on S h; h ` S \ t\ \ homotopic_loops t (h \ f) (h \ g)" + "\homotopic_loops S f g; continuous_on S h; h \ S \ t\ \ homotopic_loops t (h \ f) (h \ g)" unfolding homotopic_loops_def - by (simp add: homotopic_with_compose_continuous_map_left pathfinish_def pathstart_def) + by (simp add: homotopic_with_compose_continuous_map_left pathfinish_def pathstart_def image_subset_iff_funcset) subsection\Relations between the two variants of homotopy\ @@ -731,11 +739,11 @@ have pip: "path_image p \ S" by (metis assms homotopic_loops_imp_subset) let ?A = "{0..1::real} \ {0..1::real}" obtain h where conth: "continuous_on ?A h" - and hs: "h ` ?A \ S" + and hs: "h \ ?A \ S" and h0[simp]: "\x. x \ {0..1} \ h(0,x) = p x" and h1[simp]: "\x. x \ {0..1} \ h(1,x) = a" and ends: "\t. t \ {0..1} \ pathfinish (h \ Pair t) = pathstart (h \ Pair t)" - using assms by (auto simp: homotopic_loops homotopic_with) + using assms by (auto simp: homotopic_loops homotopic_with image_subset_iff_funcset) have conth0: "path (\u. h (u, 0))" unfolding path_def proof (rule continuous_on_compose [of _ _ h, unfolded o_def]) @@ -783,12 +791,13 @@ +++ subpath (fst y) 0 (\u. h (u, 0))) (snd y)" have "continuous_on ?A ?h" by (intro continuous_on_homotopic_join_lemma; simp add: path_defs joinpaths_def subpath_def conth c1 c2) - moreover have "?h ` ?A \ S" + moreover have "?h \ ?A \ S" + using hs unfolding joinpaths_def subpath_def - by (force simp: algebra_simps mult_le_one mult_left_le intro: hs [THEN subsetD] adhoc_le) + by (force simp: algebra_simps mult_le_one mult_left_le intro: adhoc_le) ultimately show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1})) (top_of_set S) ?h" - by (simp add: subpath_reversepath) + by (simp add: subpath_reversepath image_subset_iff_funcset) qed (use ploop in \simp_all add: reversepath_def path_defs joinpaths_def o_def subpath_def conth c1 c2\) moreover have "homotopic_paths S ((\u. h (u, 0)) +++ linepath a a +++ reversepath (\u. h (u, 0))) (linepath (pathstart p) (pathstart p))" @@ -999,7 +1008,7 @@ show "continuous_on {0..1} ?f" unfolding split_01 by (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def dest!: t2)+ - show "?f ` {0..1} \ {0..1}" + show "?f \ {0..1} \ {0..1}" using False assms by (force simp: field_simps not_le mult_left_mono affine_ineq dest!: 1 2) show "(subpath u v g +++ subpath v w g) t = subpath u w g (?f t)" if "t \ {0..1}" for t @@ -1057,12 +1066,12 @@ assumes "path_component S a b" shows "homotopic_loops S (linepath a a) (linepath b b)" proof - - obtain g :: "real \ 'a" where g: "continuous_on {0..1} g" "g ` {0..1} \ S" "g 0 = a" "g 1 = b" + obtain g :: "real \ 'a" where g: "continuous_on {0..1} g" "g \ {0..1} \ S" "g 0 = a" "g 1 = b" using assms by (auto simp: path_defs) then have "continuous_on ({0..1} \ {0..1}) (g \ fst)" by (fastforce intro!: continuous_intros)+ with g show ?thesis - by (auto simp: homotopic_loops_def homotopic_with_def path_defs image_subset_iff) + by (auto simp: homotopic_loops_def homotopic_with_def path_defs Pi_iff) qed lemma homotopic_loops_imp_path_component_value: @@ -1289,39 +1298,39 @@ lemma nullhomotopic_through_contractible: fixes S :: "_::topological_space set" - assumes f: "continuous_on S f" "f ` S \ T" - and g: "continuous_on T g" "g ` T \ U" + assumes f: "continuous_on S f" "f \ S \ T" + and g: "continuous_on T g" "g \ T \ U" and T: "contractible T" obtains c where "homotopic_with_canon (\h. True) S U (g \ f) (\x. c)" proof - obtain b where b: "homotopic_with_canon (\x. True) T T id (\x. b)" using assms by (force simp: contractible_def) have "homotopic_with_canon (\f. True) T U (g \ id) (g \ (\x. b))" - by (metis Abstract_Topology.continuous_map_subtopology_eu b g homotopic_with_compose_continuous_map_left) + by (metis b continuous_map_subtopology_eu g homotopic_with_compose_continuous_map_left image_subset_iff_funcset) then have "homotopic_with_canon (\f. True) S U (g \ id \ f) (g \ (\x. b) \ f)" - by (simp add: f homotopic_with_compose_continuous_map_right) + by (simp add: f homotopic_with_compose_continuous_map_right image_subset_iff_funcset) then show ?thesis by (simp add: comp_def that) qed lemma nullhomotopic_into_contractible: - assumes f: "continuous_on S f" "f ` S \ T" + assumes f: "continuous_on S f" "f \ S \ T" and T: "contractible T" obtains c where "homotopic_with_canon (\h. True) S T f (\x. c)" by (rule nullhomotopic_through_contractible [OF f, of id T]) (use assms in auto) lemma nullhomotopic_from_contractible: - assumes f: "continuous_on S f" "f ` S \ T" + assumes f: "continuous_on S f" "f \ S \ T" and S: "contractible S" obtains c where "homotopic_with_canon (\h. True) S T f (\x. c)" by (auto simp: comp_def intro: nullhomotopic_through_contractible [OF continuous_on_id _ f S]) lemma homotopic_through_contractible: fixes S :: "_::real_normed_vector set" - assumes "continuous_on S f1" "f1 ` S \ T" - "continuous_on T g1" "g1 ` T \ U" - "continuous_on S f2" "f2 ` S \ T" - "continuous_on T g2" "g2 ` T \ U" + assumes "continuous_on S f1" "f1 \ S \ T" + "continuous_on T g1" "g1 \ T \ U" + "continuous_on S f2" "f2 \ S \ T" + "continuous_on T g2" "g2 \ T \ U" "contractible T" "path_connected U" shows "homotopic_with_canon (\h. True) S U (g1 \ f1) (g2 \ f2)" proof - @@ -1346,8 +1355,8 @@ lemma homotopic_into_contractible: fixes S :: "'a::real_normed_vector set" and T:: "'b::real_normed_vector set" - assumes f: "continuous_on S f" "f ` S \ T" - and g: "continuous_on S g" "g ` S \ T" + assumes f: "continuous_on S f" "f \ S \ T" + and g: "continuous_on S g" "g \ S \ T" and T: "contractible T" shows "homotopic_with_canon (\h. True) S T f g" using homotopic_through_contractible [of S f T id T g id] @@ -1355,8 +1364,8 @@ lemma homotopic_from_contractible: fixes S :: "'a::real_normed_vector set" and T:: "'b::real_normed_vector set" - assumes f: "continuous_on S f" "f ` S \ T" - and g: "continuous_on S g" "g ` S \ T" + assumes f: "continuous_on S f" "f \ S \ T" + and g: "continuous_on S g" "g \ S \ T" and "contractible S" "path_connected T" shows "homotopic_with_canon (\h. True) S T f g" using homotopic_through_contractible [of S id S f T id g] @@ -1478,15 +1487,15 @@ shows "contractible (S \ T)" proof - obtain a h where conth: "continuous_on ({0..1} \ S) h" - and hsub: "h ` ({0..1} \ S) \ S" + and hsub: "h \ ({0..1} \ S) \ S" and [simp]: "\x. x \ S \ h (0, x) = x" and [simp]: "\x. x \ S \ h (1::real, x) = a" - using S by (auto simp: contractible_def homotopic_with) + using S by (force simp: contractible_def homotopic_with) obtain b k where contk: "continuous_on ({0..1} \ T) k" - and ksub: "k ` ({0..1} \ T) \ T" + and ksub: "k \ ({0..1} \ T) \ T" and [simp]: "\x. x \ T \ k (0, x) = x" and [simp]: "\x. x \ T \ k (1::real, x) = b" - using T by (auto simp: contractible_def homotopic_with) + using T by (force simp: contractible_def homotopic_with) show ?thesis apply (simp add: contractible_def homotopic_with) apply (rule exI [where x=a]) @@ -3210,7 +3219,7 @@ by (rule hom) then have "homotopic_with_canon Q U t (h \ (k \ f)) (h \ (k \ g))" apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono]) - using Q by (auto simp: conth imh) + using Q conth imh by force+ then show ?thesis proof (rule homotopic_with_eq; simp) show "\h k. (\x. x \ U \ h x = k x) \ Q h = Q k" @@ -3240,7 +3249,7 @@ by (metis hom) then have "homotopic_with_canon Q U t (h \ (k \ f)) (h \ (\x. c))" apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono]) - using Q by (auto simp: conth imh) + using Q conth imh by force+ then have "homotopic_with_canon Q U t f (\x. h c)" proof (rule homotopic_with_eq) show "\x. x \ topspace (top_of_set U) \ f x = (h \ (k \ f)) x" @@ -3281,7 +3290,7 @@ by (rule hom) then have "homotopic_with_canon Q t U (f \ h \ k) (g \ h \ k)" apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono]) - using Q by (auto simp: contk imk) + using Q contk imk by force+ then show ?thesis proof (rule homotopic_with_eq) show "f x = (f \ h \ k) x" "g x = (g \ h \ k) x" @@ -3312,7 +3321,7 @@ proof (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono]) show "\h. \continuous_map (top_of_set S) (top_of_set U) h; P h\ \ Q (h \ k)" using Q by auto - qed (auto simp: contk imk) + qed (use contk imk in force)+ moreover have "homotopic_with_canon Q t U f (\x. c)" using homotopic_with_eq [OF \
] feq Qeq by fastforce ultimately show ?thesis @@ -3789,15 +3798,10 @@ (infix "homotopy'_eqv" 50) where "S homotopy_eqv T \ top_of_set S homotopy_equivalent_space top_of_set T" - - - - lemma homeomorphic_imp_homotopy_eqv: "S homeomorphic T \ S homotopy_eqv T" unfolding homeomorphic_def homeomorphism_def homotopy_equivalent_space_def by (metis continuous_map_subtopology_eu homotopic_with_id2 openin_imp_subset openin_subtopology_self topspace_euclidean_subtopology) - lemma homotopy_eqv_inj_linear_image: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "linear f" "inj f" @@ -3814,25 +3818,25 @@ and T :: "'b::real_normed_vector set" and U :: "'c::real_normed_vector set" assumes "S homotopy_eqv T" - and f: "continuous_on U f" "f ` U \ T" - and g: "continuous_on U g" "g ` U \ T" - and homUS: "\f g. \continuous_on U f; f ` U \ S; - continuous_on U g; g ` U \ S\ + and f: "continuous_on U f" "f \ U \ T" + and g: "continuous_on U g" "g \ U \ T" + and homUS: "\f g. \continuous_on U f; f \ U \ S; + continuous_on U g; g \ U \ S\ \ homotopic_with_canon (\x. True) U S f g" shows "homotopic_with_canon (\x. True) U T f g" proof - - obtain h k where h: "continuous_on S h" "h ` S \ T" - and k: "continuous_on T k" "k ` T \ S" + obtain h k where h: "continuous_on S h" "h \ S \ T" + and k: "continuous_on T k" "k \ T \ S" and hom: "homotopic_with_canon (\x. True) S S (k \ h) id" "homotopic_with_canon (\x. True) T T (h \ k) id" - using assms by (auto simp: homotopy_equivalent_space_def) + using assms by (force simp: homotopy_equivalent_space_def image_subset_iff_funcset) have "homotopic_with_canon (\f. True) U S (k \ f) (k \ g)" proof (rule homUS) show "continuous_on U (k \ f)" "continuous_on U (k \ g)" - using continuous_on_compose continuous_on_subset f g k by blast+ + using continuous_on_compose continuous_on_subset f g k by (metis funcset_image)+ qed (use f g k in \(force simp: o_def)+\ ) then have "homotopic_with_canon (\x. True) U T (h \ (k \ f)) (h \ (k \ g))" - by (rule homotopic_with_compose_continuous_left; simp add: h) + by (simp add: h homotopic_with_compose_continuous_map_left image_subset_iff_funcset) moreover have "homotopic_with_canon (\x. True) U T (h \ k \ f) (id \ f)" by (rule homotopic_with_compose_continuous_right [where X=T and Y=T]; simp add: hom f) moreover have "homotopic_with_canon (\x. True) U T (h \ k \ g) (id \ g)" @@ -3847,11 +3851,11 @@ and T :: "'b::real_normed_vector set" and U :: "'c::real_normed_vector set" assumes "S homotopy_eqv T" - shows "(\f g. continuous_on U f \ f ` U \ S \ - continuous_on U g \ g ` U \ S + shows "(\f g. continuous_on U f \ f \ U \ S \ + continuous_on U g \ g \ U \ S \ homotopic_with_canon (\x. True) U S f g) \ - (\f g. continuous_on U f \ f ` U \ T \ - continuous_on U g \ g ` U \ T + (\f g. continuous_on U f \ f \ U \ T \ + continuous_on U g \ g \ U \ T \ homotopic_with_canon (\x. True) U T f g)" (is "?lhs = ?rhs") proof @@ -3873,20 +3877,20 @@ and T :: "'b::real_normed_vector set" and U :: "'c::real_normed_vector set" assumes "S homotopy_eqv T" - and f: "continuous_on T f" "f ` T \ U" - and homSU: "\f. \continuous_on S f; f ` S \ U\ + and f: "continuous_on T f" "f \ T \ U" + and homSU: "\f. \continuous_on S f; f \ S \ U\ \ \c. homotopic_with_canon (\x. True) S U f (\x. c)" obtains c where "homotopic_with_canon (\x. True) T U f (\x. c)" proof - - obtain h k where h: "continuous_on S h" "h ` S \ T" - and k: "continuous_on T k" "k ` T \ S" + obtain h k where h: "continuous_on S h" "h \ S \ T" + and k: "continuous_on T k" "k \ T \ S" and hom: "homotopic_with_canon (\x. True) S S (k \ h) id" "homotopic_with_canon (\x. True) T T (h \ k) id" - using assms by (auto simp: homotopy_equivalent_space_def) + using assms by (force simp: homotopy_equivalent_space_def image_subset_iff_funcset) obtain c where "homotopic_with_canon (\x. True) S U (f \ h) (\x. c)" proof (rule exE [OF homSU]) show "continuous_on S (f \ h)" - using continuous_on_compose continuous_on_subset f h by blast + by (metis continuous_on_compose continuous_on_subset f h funcset_image) qed (use f h in force) then have "homotopic_with_canon (\x. True) T U ((f \ h) \ k) ((\x. c) \ k)" by (rule homotopic_with_compose_continuous_right [where X=S]) (use k in auto) @@ -3902,9 +3906,9 @@ and T :: "'b::real_normed_vector set" and U :: "'c::real_normed_vector set" assumes "S homotopy_eqv T" - shows "(\f. continuous_on S f \ f ` S \ U + shows "(\f. continuous_on S f \ f \ S \ U \ (\c. homotopic_with_canon (\x. True) S U f (\x. c))) \ - (\f. continuous_on T f \ f ` T \ U + (\f. continuous_on T f \ f \ T \ U \ (\c. homotopic_with_canon (\x. True) T U f (\x. c)))" by (rule iffI; metis assms homotopy_eqv_cohomotopic_triviality_null_imp homotopy_equivalent_space_sym) @@ -3914,20 +3918,20 @@ and T :: "'b::real_normed_vector set" and U :: "'c::real_normed_vector set" assumes "S homotopy_eqv T" - and f: "continuous_on U f" "f ` U \ T" - and homSU: "\f. \continuous_on U f; f ` U \ S\ + and f: "continuous_on U f" "f \ U \ T" + and homSU: "\f. \continuous_on U f; f \ U \ S\ \ \c. homotopic_with_canon (\x. True) U S f (\x. c)" shows "\c. homotopic_with_canon (\x. True) U T f (\x. c)" proof - - obtain h k where h: "continuous_on S h" "h ` S \ T" - and k: "continuous_on T k" "k ` T \ S" + obtain h k where h: "continuous_on S h" "h \ S \ T" + and k: "continuous_on T k" "k \ T \ S" and hom: "homotopic_with_canon (\x. True) S S (k \ h) id" "homotopic_with_canon (\x. True) T T (h \ k) id" - using assms by (auto simp: homotopy_equivalent_space_def) + using assms by (force simp: homotopy_equivalent_space_def image_subset_iff_funcset) obtain c::'a where "homotopic_with_canon (\x. True) U S (k \ f) (\x. c)" proof (rule exE [OF homSU [of "k \ f"]]) show "continuous_on U (k \ f)" - using continuous_on_compose continuous_on_subset f k by blast + using continuous_on_compose continuous_on_subset f k by (metis funcset_image) qed (use f k in force) then have "homotopic_with_canon (\x. True) U T (h \ (k \ f)) (h \ (\x. c))" by (rule homotopic_with_compose_continuous_left [where Y=S]) (use h in auto) @@ -3943,9 +3947,9 @@ and T :: "'b::real_normed_vector set" and U :: "'c::real_normed_vector set" assumes "S homotopy_eqv T" - shows "(\f. continuous_on U f \ f ` U \ S + shows "(\f. continuous_on U f \ f \ U \ S \ (\c. homotopic_with_canon (\x. True) U S f (\x. c))) \ - (\f. continuous_on U f \ f ` U \ T + (\f. continuous_on U f \ f \ U \ T \ (\c. homotopic_with_canon (\x. True) U T f (\x. c)))" by (rule iffI; metis assms homotopy_eqv_homotopic_triviality_null_imp homotopy_equivalent_space_sym) diff -r d4125fc10c0c -r 1260be3f33a4 src/HOL/Analysis/Lindelof_Spaces.thy --- a/src/HOL/Analysis/Lindelof_Spaces.thy Sun Jul 02 20:41:07 2023 +0200 +++ b/src/HOL/Analysis/Lindelof_Spaces.thy Mon Jul 03 16:46:37 2023 +0100 @@ -253,7 +253,7 @@ show "x \ \ (\ (\ ` I))" if "x \ topspace X" for x proof - have "f x \ topspace Y" - by (meson f image_subset_iff proper_map_imp_subset_topspace that) + using f proper_map_imp_subset_topspace that by fastforce then show ?thesis using that I by auto qed diff -r d4125fc10c0c -r 1260be3f33a4 src/HOL/Analysis/Lipschitz.thy --- a/src/HOL/Analysis/Lipschitz.thy Sun Jul 02 20:41:07 2023 +0200 +++ b/src/HOL/Analysis/Lipschitz.thy Mon Jul 03 16:46:37 2023 +0100 @@ -125,8 +125,8 @@ proof show "?lhs \ ?rhs" by (force simp add: Lipschitz_continuous_map_pos lipschitz_on_def less_le_not_le) - show "?rhs \ ?lhs" - by (metis Lipschitz_continuous_map_def lipschitz_onD mdist_euclidean_metric mspace_euclidean_metric top_greatest) + show "?rhs \ ?lhs" + by (auto simp: Lipschitz_continuous_map_def lipschitz_on_def) qed subsubsection \Continuity\ diff -r d4125fc10c0c -r 1260be3f33a4 src/HOL/Analysis/Path_Connected.thy --- a/src/HOL/Analysis/Path_Connected.thy Sun Jul 02 20:41:07 2023 +0200 +++ b/src/HOL/Analysis/Path_Connected.thy Mon Jul 03 16:46:37 2023 +0100 @@ -1484,7 +1484,7 @@ lemma path_connectedin_iff_path_connected_real [simp]: "path_connectedin euclideanreal S \ path_connected S" - by (simp add: path_connectedin path_connected_def path_defs) + by (simp add: path_connectedin path_connected_def path_defs image_subset_iff_funcset) lemma path_connected_component: "path_connected S \ (\x\S. \y\S. path_component S x y)" unfolding path_connected_def path_component_def by auto @@ -1929,12 +1929,12 @@ definition path_components_of :: "'a topology \ 'a set set" where "path_components_of X \ path_component_of_set X ` topspace X" -lemma pathin_canon_iff: "pathin (top_of_set T) g \ path g \ g ` {0..1} \ T" - by (simp add: path_def pathin_def) +lemma pathin_canon_iff: "pathin (top_of_set T) g \ path g \ g \ {0..1} \ T" + by (simp add: path_def pathin_def image_subset_iff_funcset) lemma path_component_of_canon_iff [simp]: "path_component_of (top_of_set T) a b \ path_component T a b" - by (simp add: path_component_of_def pathin_canon_iff path_defs) + by (simp add: path_component_of_def pathin_canon_iff path_defs image_subset_iff_funcset) lemma path_component_in_topspace: "path_component_of X x y \ x \ topspace X \ y \ topspace X" diff -r d4125fc10c0c -r 1260be3f33a4 src/HOL/Analysis/Retracts.thy --- a/src/HOL/Analysis/Retracts.thy Sun Jul 02 20:41:07 2023 +0200 +++ b/src/HOL/Analysis/Retracts.thy Mon Jul 03 16:46:37 2023 +0100 @@ -100,7 +100,7 @@ proof (simp add: retraction_def retract_of_def, intro exI conjI) show "continuous_on U (g \ h')" by (meson continuous_on_compose continuous_on_subset h' hom homeomorphism_cont1) - show "(g \ h') ` U \ S'" + show "(g \ h') \ U \ S'" using h' by clarsimp (metis hom subsetD homeomorphism_def imageI) show "\x\S'. (g \ h') x = x" by clarsimp (metis h'h hom homeomorphism_def) @@ -136,7 +136,7 @@ proof (simp add: retraction_def retract_of_def, intro exI conjI) show "continuous_on U (g \ h')" by (meson continuous_on_compose continuous_on_subset h' hom homeomorphism_cont1) - show "(g \ h') ` U \ T" + show "(g \ h') \ U \ T" using h' by clarsimp (metis hom subsetD homeomorphism_def imageI) show "\x\T. (g \ h') x = x" by clarsimp (metis h'h hom homeomorphism_def) @@ -173,11 +173,11 @@ lemma ANR_imp_absolute_neighbourhood_extensor: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" - assumes "ANR S" and contf: "continuous_on T f" and "f ` T \ S" + assumes "ANR S" and contf: "continuous_on T f" and "f \ T \ S" and cloUT: "closedin (top_of_set U) T" obtains V g where "T \ V" "openin (top_of_set U) V" "continuous_on V g" - "g ` V \ S" "\x. x \ T \ g x = f x" + "g \ V \ S" "\x. x \ T \ g x = f x" proof - have "aff_dim S < int (DIM('b \ real))" using aff_dim_le_DIM [of S] by simp @@ -194,7 +194,7 @@ obtain g h where homgh: "homeomorphism S S' g h" using hom by (force simp: homeomorphic_def) have "continuous_on (f ` T) g" - by (meson \f ` T \ S\ continuous_on_subset homeomorphism_def homgh) + by (metis PiE assms(3) continuous_on_subset homeomorphism_cont1 homgh image_subset_iff) then have contgf: "continuous_on T (g \ f)" by (intro continuous_on_compose contf) have gfTC: "(g \ f) ` T \ C" @@ -202,7 +202,7 @@ have "g ` S = S'" by (metis (no_types) homeomorphism_def homgh) then show ?thesis - by (metis (no_types) assms(3) cloCS closedin_def image_comp image_mono order.trans topspace_euclidean_subtopology) + by (metis PiE assms(3) cloCS closedin_def image_comp image_mono image_subset_iff order.trans topspace_euclidean_subtopology) qed obtain f' where contf': "continuous_on U f'" and "f' ` U \ C" @@ -211,10 +211,10 @@ show ?thesis proof (rule_tac V = "U \ f' -` D" and g = "h \ r \ f'" in that) show "T \ U \ f' -` D" - using cloUT closedin_imp_subset \S' \ D\ \f ` T \ S\ eq homeomorphism_image1 homgh + using cloUT closedin_imp_subset \S' \ D\ \f \ T \ S\ eq homeomorphism_image1 homgh by fastforce show ope: "openin (top_of_set U) (U \ f' -` D)" - using \f' ` U \ C\ by (auto simp: opD contf' continuous_openin_preimage) + by (meson \f' ` U \ C\ contf' continuous_openin_preimage image_subset_iff_funcset opD) have conth: "continuous_on (r ` f' ` (U \ f' -` D)) h" proof (rule continuous_on_subset [of S']) show "continuous_on S' h" @@ -222,12 +222,12 @@ qed (use \r ` D \ S'\ in blast) show "continuous_on (U \ f' -` D) (h \ r \ f')" by (blast intro: continuous_on_compose conth continuous_on_subset [OF contr] continuous_on_subset [OF contf']) - show "(h \ r \ f') ` (U \ f' -` D) \ S" + show "(h \ r \ f') \ (U \ f' -` D) \ S" using \homeomorphism S S' g h\ \f' ` U \ C\ \r ` D \ S'\ by (auto simp: homeomorphism_def) show "\x. x \ T \ (h \ r \ f') x = f x" - using \homeomorphism S S' g h\ \f ` T \ S\ eq - by (auto simp: rid homeomorphism_def) + using \homeomorphism S S' g h\ \f \ T \ S\ eq + by (metis PiE comp_apply homeomorphism_def image_iff rid) qed qed @@ -240,7 +240,7 @@ proof - obtain g h where hom: "homeomorphism S S' g h" using assms by (force simp: homeomorphic_def) - obtain h: "continuous_on S' h" " h ` S' \ S" + obtain h: "continuous_on S' h" " h \ S' \ S" using hom homeomorphism_def by blast from ANR_imp_absolute_neighbourhood_extensor [OF \ANR S\ h clo] obtain V h' where "S' \ V" and opUV: "openin (top_of_set U) V" @@ -251,7 +251,7 @@ proof (simp add: retraction_def retract_of_def, intro exI conjI \S' \ V\) show "continuous_on V (g \ h')" by (meson continuous_on_compose continuous_on_subset h'(1) h'(2) hom homeomorphism_cont1) - show "(g \ h') ` V \ S'" + show "(g \ h') \ V \ S'" using h' by clarsimp (metis hom subsetD homeomorphism_def imageI) show "\x\S'. (g \ h') x = x" by clarsimp (metis h'h hom homeomorphism_def) @@ -269,29 +269,29 @@ corollary neighbourhood_extension_into_ANR: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" - assumes contf: "continuous_on S f" and fim: "f ` S \ T" and "ANR T" "closed S" + assumes contf: "continuous_on S f" and fim: "f \ S \ T" and "ANR T" "closed S" obtains V g where "S \ V" "open V" "continuous_on V g" - "g ` V \ T" "\x. x \ S \ g x = f x" + "g \ V \ T" "\x. x \ S \ g x = f x" using ANR_imp_absolute_neighbourhood_extensor [OF \ANR T\ contf fim] by (metis \closed S\ closed_closedin open_openin subtopology_UNIV) lemma absolute_neighbourhood_extensor_imp_ANR: fixes S :: "'a::euclidean_space set" assumes "\f :: 'a * real \ 'a. - \U T. \continuous_on T f; f ` T \ S; + \U T. \continuous_on T f; f \ T \ S; closedin (top_of_set U) T\ \ \V g. T \ V \ openin (top_of_set U) V \ - continuous_on V g \ g ` V \ S \ (\x \ T. g x = f x)" + continuous_on V g \ g \ V \ S \ (\x \ T. g x = f x)" shows "ANR S" proof (clarsimp simp: ANR_def) fix U and T :: "('a * real) set" assume "S homeomorphic T" and clo: "closedin (top_of_set U) T" then obtain g h where hom: "homeomorphism S T g h" by (force simp: homeomorphic_def) - obtain h: "continuous_on T h" " h ` T \ S" + obtain h: "continuous_on T h" " h \ T \ S" using hom homeomorphism_def by blast obtain V h' where "T \ V" and opV: "openin (top_of_set U) V" - and h': "continuous_on V h'" "h' ` V \ S" + and h': "continuous_on V h'" "h' \ V \ S" and h'h: "\x\T. h' x = h x" using assms [OF h clo] by blast have [simp]: "T \ U" @@ -299,9 +299,9 @@ have "T retract_of V" proof (simp add: retraction_def retract_of_def, intro exI conjI \T \ V\) show "continuous_on V (g \ h')" - by (meson continuous_on_compose continuous_on_subset h' hom homeomorphism_cont1) - show "(g \ h') ` V \ T" - using h' by clarsimp (metis hom subsetD homeomorphism_def imageI) + by (meson continuous_on_compose continuous_on_subset h' hom homeomorphism_def image_subset_iff_funcset) + show "(g \ h') \ V \ T" + using h' hom homeomorphism_image1 by fastforce show "\x\T. (g \ h') x = x" by clarsimp (metis h'h hom homeomorphism_def) qed @@ -313,10 +313,10 @@ fixes S :: "'a::euclidean_space set" shows "ANR S \ (\f :: 'a * real \ 'a. - \U T. continuous_on T f \ f ` T \ S \ + \U T. continuous_on T f \ f \ T \ S \ closedin (top_of_set U) T \ (\V g. T \ V \ openin (top_of_set U) V \ - continuous_on V g \ g ` V \ S \ (\x \ T. g x = f x)))" (is "_ = ?rhs") + continuous_on V g \ g \ V \ S \ (\x \ T. g x = f x)))" (is "_ = ?rhs") proof assume "ANR S" then show ?rhs by (metis ANR_imp_absolute_neighbourhood_extensor) @@ -431,7 +431,7 @@ by (metis \retraction X S r\ image_mono image_subset_iff_subset_vimage inf_le2 retraction) qed qed - show "(f \ r \ h) ` (W \ h -` X) \ S'" + show "(f \ r \ h) \ (W \ h -` X) \ S'" using \retraction X S r\ hom by (auto simp: retraction_def homeomorphism_def) show "\x\S'. (f \ r \ h) x = x" @@ -529,15 +529,15 @@ by (auto simp: contractible_def homotopic_with_def) then have "a \ S" by (metis all_not_in_conv atLeastAtMost_iff image_subset_iff mem_Sigma_iff order_refl zero_le_one) - have "\g. continuous_on W g \ g ` W \ S \ (\x\T. g x = f x)" - if f: "continuous_on T f" "f ` T \ S" + have "\g. continuous_on W g \ g \ W \ S \ (\x\T. g x = f x)" + if f: "continuous_on T f" "f \ T \ S" and WT: "closedin (top_of_set W) T" for W T and f :: "'a \ real \ 'a" proof - obtain U g where "T \ U" and WU: "openin (top_of_set W) U" and contg: "continuous_on U g" - and "g ` U \ S" and gf: "\x. x \ T \ g x = f x" + and "g \ U \ S" and gf: "\x. x \ T \ g x = f x" using iffD1 [OF ANR_eq_absolute_neighbourhood_extensor \ANR S\, rule_format, OF f WT] by auto have WWU: "closedin (top_of_set W) (W - U)" @@ -570,7 +570,7 @@ show "continuous_on (W - V') g" by (metis Diff_subset_conv \W - U \ V'\ contg continuous_on_subset Un_commute) show "(\x. (j x, g x)) ` (W - V') \ {0..1} \ S" - using j \g ` U \ S\ \W - U \ V'\ by fastforce + using j \g \ U \ S\ \W - U \ V'\ by fastforce qed show "continuous_on W (\x. if x \ W - V then a else h (j x, g x))" proof (subst Weq, rule continuous_on_cases_local) @@ -583,12 +583,12 @@ have "j(x, y) \ {0..1}" using j that by blast moreover have "g(x, y) \ S" - using \V' \ V = {}\ \W - U \ V'\ \g ` U \ S\ that by fastforce + using \V' \ V = {}\ \W - U \ V'\ \g \ U \ S\ that by fastforce ultimately show ?thesis using hS by blast qed - with \a \ S\ \g ` U \ S\ - show "(\x. if x \ W - V then a else h (j x, g x)) ` W \ S" + with \a \ S\ \g \ U \ S\ + show "(\x. if x \ W - V then a else h (j x, g x)) \ W \ S" by auto next show "\x\T. (if x \ W - V then a else h (j x, g x)) = f x" @@ -596,7 +596,7 @@ qed qed then show ?lhs - by (simp add: AR_eq_absolute_extensor) + by (simp add: AR_eq_absolute_extensor image_subset_iff_funcset) qed @@ -606,17 +606,17 @@ shows "ANR S" proof (clarsimp simp add: ANR_eq_absolute_neighbourhood_extensor) fix f::"'a \ real \ 'a" and U W - assume W: "continuous_on W f" "f ` W \ S" "closedin (top_of_set U) W" - then obtain r where "S \ T" and r: "continuous_on T r" "r ` T \ S" "\x\S. r x = x" "continuous_on W f" "f ` W \ S" + assume W: "continuous_on W f" "f \ W \ S" "closedin (top_of_set U) W" + then obtain r where "S \ T" and r: "continuous_on T r" "r \ T \ S" "\x\S. r x = x" "continuous_on W f" "f \ W \ S" "closedin (top_of_set U) W" - by (meson ST retract_of_def retraction_def) + by (metis ST retract_of_def retraction_def) then have "f ` W \ T" by blast - with W obtain V g where V: "W \ V" "openin (top_of_set U) V" "continuous_on V g" "g ` V \ T" "\x\W. g x = f x" - by (metis ANR_imp_absolute_neighbourhood_extensor \ANR T\) - with r have "continuous_on V (r \ g) \ (r \ g) ` V \ S \ (\x\W. (r \ g) x = f x)" - by (metis (no_types, lifting) comp_apply continuous_on_compose continuous_on_subset image_subset_iff) - then show "\V. W \ V \ openin (top_of_set U) V \ (\g. continuous_on V g \ g ` V \ S \ (\x\W. g x = f x))" + with W obtain V g where V: "W \ V" "openin (top_of_set U) V" "continuous_on V g" "g \ V \ T" "\x\W. g x = f x" + by (smt (verit) ANR_imp_absolute_neighbourhood_extensor Pi_I assms(1) funcset_mem image_subset_iff_funcset) + with r have "continuous_on V (r \ g) \ (r \ g) \ V \ S \ (\x\W. (r \ g) x = f x)" + by (smt (verit, del_insts) Pi_iff comp_apply continuous_on_compose continuous_on_subset image_subset_iff_funcset) + then show "\V. W \ V \ openin (top_of_set U) V \ (\g. continuous_on V g \ g \ V \ S \ (\x\W. g x = f x))" by (meson V) qed @@ -775,7 +775,8 @@ show ?thesis apply (simp add: retract_of_def retraction_def \S \ U\ \T \ U\) apply (rule_tac x="\x. if x \ S' then g x else h x" in exI) - using ST UST \S \ S'\ \S' \ T' = W\ \T \ T'\ cont geqr heqr r_def by auto + using ST UST \S \ S'\ \S' \ T' = W\ \T \ T'\ cont geqr heqr r_def + by (smt (verit, del_insts) IntI Pi_I Un_iff image_subset_iff r0 subsetD) qed @@ -883,14 +884,14 @@ have "W0 \ U" using \W \ U\ cloWW0 closedin_subset by fastforce obtain r0 - where "S \ T \ W0" and contr0: "continuous_on W0 r0" and "r0 ` W0 \ S \ T" + where "S \ T \ W0" and contr0: "continuous_on W0 r0" and "r0 \ W0 \ S \ T" and r0 [simp]: "\x. x \ S \ T \ r0 x = x" using ret by (force simp: retract_of_def retraction_def) have ST: "x \ W \ x \ S \ x \ T" for x using assms by (auto simp: W_def setdist_sing_in_set dest!: setdist_eq_0_closedin) define r where "r \ \x. if x \ W0 then r0 x else x" have "r ` (W0 \ S) \ S" "r ` (W0 \ T) \ T" - using \r0 ` W0 \ S \ T\ r_def by auto + using \r0 \ W0 \ S \ T\ r_def by auto have contr: "continuous_on (W0 \ (S \ T)) r" unfolding r_def proof (rule continuous_on_cases_local [OF _ _ contr0 continuous_on_id]) @@ -907,21 +908,21 @@ closedin_Un closedin_imp_subset closedin_trans) obtain W1 g where "W0 \ S \ W1" and contg: "continuous_on W1 g" and opeSW1: "openin (top_of_set S') W1" - and "g ` W1 \ S" and geqr: "\x. x \ W0 \ S \ g x = r x" - proof (rule ANR_imp_absolute_neighbourhood_extensor [OF \ANR S\ _ \r ` (W0 \ S) \ S\ cloS'WS]) + and "g \ W1 \ S" and geqr: "\x. x \ W0 \ S \ g x = r x" + proof (rule ANR_imp_absolute_neighbourhood_extensor [OF \ANR S\ _ _ cloS'WS]) show "continuous_on (W0 \ S) r" using continuous_on_subset contr sup_assoc by blast - qed auto + qed (use \r ` (W0 \ S) \ S\ in auto) have cloT'WT: "closedin (top_of_set T') (W0 \ T)" by (meson closedin_subset_trans UT cloUT' \T \ T'\ \W \ T'\ cloUW cloWW0 closedin_Un closedin_imp_subset closedin_trans) obtain W2 h where "W0 \ T \ W2" and conth: "continuous_on W2 h" and opeSW2: "openin (top_of_set T') W2" and "h ` W2 \ T" and heqr: "\x. x \ W0 \ T \ h x = r x" - proof (rule ANR_imp_absolute_neighbourhood_extensor [OF \ANR T\ _ \r ` (W0 \ T) \ T\ cloT'WT]) + proof (rule ANR_imp_absolute_neighbourhood_extensor [OF \ANR T\ _ _ cloT'WT]) show "continuous_on (W0 \ T) r" using continuous_on_subset contr sup_assoc by blast - qed auto + qed (use \r ` (W0 \ T) \ T\ in auto) have "S' \ T' = W" by (force simp: S'_def T'_def W_def) obtain O1 O2 where O12: "open O1" "W1 = S' \ O1" "open O2" "W2 = T' \ O2" @@ -961,12 +962,12 @@ using continuous_on_cases_local [OF cloW1 cloW2 continuous_on_subset [OF contg] continuous_on_subset [OF conth]] by simp show "?gh ` (?WW1 \ ?WW2) \ S \ T" - using \W1 = S' \ O1\ \W2 = T' \ O2\ \S' \ T' = W\ \g ` W1 \ S\ \h ` W2 \ T\ \U0 \ W \ W0\ \W0 \ S \ W1\ + using \W1 = S' \ O1\ \W2 = T' \ O2\ \S' \ T' = W\ \g \ W1 \ S\ \h ` W2 \ T\ \U0 \ W \ W0\ \W0 \ S \ W1\ by (auto simp add: image_subset_iff) qed then show "S \ T retract_of ?WW1 \ ?WW2" using \W0 \ S \ W1\ \W0 \ T \ W2\ ST opeUU0 U0 - by (auto simp: retract_of_def retraction_def) + by (auto simp: retract_of_def retraction_def image_subset_iff_funcset) qed qed @@ -1025,17 +1026,17 @@ shows "ANR S" proof (clarsimp simp only: ANR_eq_absolute_neighbourhood_extensor) fix f :: "'a \ real \ 'a" and U C - assume contf: "continuous_on C f" and fim: "f ` C \ S" + assume contf: "continuous_on C f" and fim: "f \ C \ S" and cloUC: "closedin (top_of_set U) C" - have "f ` C \ T" + have "f \ C \ T" using fim opeTS openin_imp_subset by blast obtain W g where "C \ W" and UW: "openin (top_of_set U) W" and contg: "continuous_on W g" - and gim: "g ` W \ T" + and gim: "g \ W \ T" and geq: "\x. x \ C \ g x = f x" - using ANR_imp_absolute_neighbourhood_extensor [OF \ANR T\ contf \f ` C \ T\ cloUC] fim by auto - show "\V g. C \ V \ openin (top_of_set U) V \ continuous_on V g \ g ` V \ S \ (\x\C. g x = f x)" + using ANR_imp_absolute_neighbourhood_extensor [OF \ANR T\ contf \f \ C \ T\ cloUC] fim by auto + show "\V g. C \ V \ openin (top_of_set U) V \ continuous_on V g \ g \ V \ S \ (\x\C. g x = f x)" proof (intro exI conjI) show "C \ W \ g -` S" using \C \ W\ fim geq by blast @@ -1043,7 +1044,7 @@ by (metis (mono_tags, lifting) UW contg continuous_openin_preimage gim opeTS openin_trans) show "continuous_on (W \ g -` S) g" by (blast intro: continuous_on_subset [OF contg]) - show "g ` (W \ g -` S) \ S" + show "g \ (W \ g -` S) \ S" using gim by blast show "\x\C. g x = f x" using geq by blast @@ -1217,7 +1218,7 @@ assumes "ANR S" "ANR T" shows "ANR(S \ T)" proof (clarsimp simp only: ANR_eq_absolute_neighbourhood_extensor) fix f :: " ('a \ 'b) \ real \ 'a \ 'b" and U C - assume "continuous_on C f" and fim: "f ` C \ S \ T" + assume "continuous_on C f" and fim: "f \ C \ S \ T" and cloUC: "closedin (top_of_set U) C" have contf1: "continuous_on C (fst \ f)" by (simp add: \continuous_on C f\ continuous_on_fst) @@ -1227,23 +1228,23 @@ and gim: "g ` W1 \ S" and geq: "\x. x \ C \ g x = (fst \ f) x" proof (rule ANR_imp_absolute_neighbourhood_extensor [OF \ANR S\ contf1 _ cloUC]) - show "(fst \ f) ` C \ S" - using fim by auto + show "(fst \ f) \ C \ S" + using fim by force qed auto have contf2: "continuous_on C (snd \ f)" by (simp add: \continuous_on C f\ continuous_on_snd) obtain W2 h where "C \ W2" and UW2: "openin (top_of_set U) W2" and conth: "continuous_on W2 h" - and him: "h ` W2 \ T" + and him: "h \ W2 \ T" and heq: "\x. x \ C \ h x = (snd \ f) x" proof (rule ANR_imp_absolute_neighbourhood_extensor [OF \ANR T\ contf2 _ cloUC]) - show "(snd \ f) ` C \ T" - using fim by auto + show "(snd \ f) \ C \ T" + using fim by force qed auto show "\V g. C \ V \ openin (top_of_set U) V \ - continuous_on V g \ g ` V \ S \ T \ (\x\C. g x = f x)" + continuous_on V g \ g \ V \ S \ T \ (\x\C. g x = f x)" proof (intro exI conjI) show "C \ W1 \ W2" by (simp add: \C \ W1\ \C \ W2\) @@ -1251,7 +1252,7 @@ by (simp add: UW1 UW2 openin_Int) show "continuous_on (W1 \ W2) (\x. (g x, h x))" by (metis (no_types) contg conth continuous_on_Pair continuous_on_subset inf_commute inf_le1) - show "(\x. (g x, h x)) ` (W1 \ W2) \ S \ T" + show "(\x. (g x, h x)) \ (W1 \ W2) \ S \ T" using gim him by blast show "(\x\C. (g x, h x) = f x)" using geq heq by auto @@ -1710,7 +1711,7 @@ assumes cloTS: "closedin (top_of_set T) S" and anr: "(ANR S \ ANR T) \ ANR U" and contf: "continuous_on T f" - and "f ` T \ U" + and "f \ T \ U" and "homotopic_with_canon (\x. True) S U f g" obtains g' where "homotopic_with_canon (\x. True) T U f g'" "continuous_on T g'" "image g' T \ U" @@ -1718,9 +1719,9 @@ proof - have "S \ T" using assms closedin_imp_subset by blast obtain h where conth: "continuous_on ({0..1} \ S) h" - and him: "h ` ({0..1} \ S) \ U" + and him: "h \ ({0..1} \ S) \ U" and [simp]: "\x. h(0, x) = f x" "\x. h(1::real, x) = g x" - using assms by (auto simp: homotopic_with_def) + using assms by (fastforce simp: homotopic_with_def) define h' where "h' \ \z. if snd z \ S then h z else (f \ snd) z" define B where "B \ {0::real} \ T \ {0..1} \ S" have clo0T: "closedin (top_of_set ({0..1} \ T)) ({0::real} \ T)" @@ -1744,9 +1745,9 @@ then have conth': "continuous_on B h'" by (simp add: h'_def B_def Un_commute [of "{0} \ T"]) have "image h' B \ U" - using \f ` T \ U\ him by (auto simp: h'_def B_def) + using \f \ T \ U\ him by (auto simp: h'_def B_def) obtain V k where "B \ V" and opeTV: "openin (top_of_set ({0..1} \ T)) V" - and contk: "continuous_on V k" and kim: "k ` V \ U" + and contk: "continuous_on V k" and kim: "k \ V \ U" and keq: "\x. x \ B \ k x = h' x" using anr proof @@ -1770,14 +1771,15 @@ moreover have "(h' \ r) ` V \ U" by (metis \h' ` B \ U\ image_comp retractionE that(2)) ultimately show ?thesis - using Vk [of V "h' \ r"] by (metis comp_apply retraction that) + using Vk [of V "h' \ r"] by (metis comp_apply retraction image_subset_iff_funcset that) qed show thesis by (meson "*" ANR_imp_neighbourhood_retract \ANR B\ clo0TB retract_of_def) next assume "ANR U" - with ANR_imp_absolute_neighbourhood_extensor \h' ` B \ U\ clo0TB conth' that - show ?thesis by blast + with ANR_imp_absolute_neighbourhood_extensor \h' ` B \ U\ clo0TB conth' image_subset_iff_funcset that + show ?thesis + by (smt (verit) Pi_I funcset_mem) qed define S' where "S' \ {x. \u::real. u \ {0..1} \ (u, x::'a) \ {0..1} \ T - V}" have "closedin (top_of_set T) S'" @@ -1827,7 +1829,7 @@ fix t assume "t \ T" show "k (a t, t) \ U" - by (metis \t \ T\ image_subset_iff inV kim not_one_le_zero linear mult_cancel_right1) + by (metis \t \ T\ image_subset_iff inV kim not_one_le_zero linear mult_cancel_right1 image_subset_iff_funcset) qed show "\x. x \ S \ k (a x, x) = g x" by (simp add: B_def a1 h'_def keq) @@ -1854,7 +1856,7 @@ then obtain g where "continuous_on UNIV g" "range g \ T" "\x. x \ S \ g x = f x" proof (rule Borsuk_homotopy_extension_homotopic) - show "range (\x. c) \ T" + show "(\x. c) \ UNIV \ T" using \S \ {}\ c homotopic_with_imp_subset1 by fastforce qed (use assms c in auto) then show ?rhs by blast @@ -1956,7 +1958,7 @@ by (metis convex_imp_contractible convex_ball) show "continuous_on (ball 0 r) (\x. inverse(norm (x - b)) *\<^sub>R (x - b))" by (rule continuous_on_Borsuk_map [OF bnot]) - show "(\x. (x - b) /\<^sub>R norm (x - b)) ` ball 0 r \ sphere 0 1" + show "(\x. (x - b) /\<^sub>R norm (x - b)) \ ball 0 r \ sphere 0 1" using bnot Borsuk_map_into_sphere by blast qed blast ultimately have "homotopic_with_canon (\x. True) S (sphere 0 1) (\x. (x - a) /\<^sub>R norm (x - a)) (\x. c)" @@ -1979,9 +1981,10 @@ assume notcc: "\ connected_component (- S) a b" let ?T = "S \ connected_component_set (- S) a" have "\g. continuous_on (S \ connected_component_set (- S) a) g \ - g ` (S \ connected_component_set (- S) a) \ sphere 0 1 \ + g \ (S \ connected_component_set (- S) a) \ sphere 0 1 \ (\x\S. g x = (x - a) /\<^sub>R norm (x - a))" - by (simp add: \a \ S\ componentsI non_extensible_Borsuk_map [OF \compact S\ _ boc]) + using non_extensible_Borsuk_map [OF \compact S\ _ boc] \a \ S\ + by (simp add: componentsI) moreover obtain g where "continuous_on (S \ connected_component_set (- S) a) g" "g ` (S \ connected_component_set (- S) a) \ sphere 0 1" "\x. x \ S \ g x = (x - a) /\<^sub>R norm (x - a)" @@ -1990,7 +1993,7 @@ by (simp add: \compact S\ closed_subset compact_imp_closed) show "continuous_on ?T (\x. (x - b) /\<^sub>R norm (x - b))" by (simp add: \b \ S\ notcc continuous_on_Borsuk_map) - show "(\x. (x - b) /\<^sub>R norm (x - b)) ` ?T \ sphere 0 1" + show "(\x. (x - b) /\<^sub>R norm (x - b)) \ ?T \ sphere 0 1" by (simp add: \b \ S\ notcc Borsuk_map_into_sphere) show "homotopic_with_canon (\x. True) S (sphere 0 1) (\x. (x - b) /\<^sub>R norm (x - b)) (\x. (x - a) /\<^sub>R norm (x - a))" @@ -2073,12 +2076,12 @@ lemma extension_from_component: fixes f :: "'a :: euclidean_space \ 'b :: euclidean_space" assumes S: "locally connected S \ compact S" and "ANR U" - and C: "C \ components S" and contf: "continuous_on C f" and fim: "f ` C \ U" - obtains g where "continuous_on S g" "g ` S \ U" "\x. x \ C \ g x = f x" + and C: "C \ components S" and contf: "continuous_on C f" and fim: "f \ C \ U" + obtains g where "continuous_on S g" "g \ S \ U" "\x. x \ C \ g x = f x" proof - obtain T g where ope: "openin (top_of_set S) T" and clo: "closedin (top_of_set S) T" - and "C \ T" and contg: "continuous_on T g" and gim: "g ` T \ U" + and "C \ T" and contg: "continuous_on T g" and gim: "g \ T \ U" and gf: "\x. x \ C \ g x = f x" using S proof @@ -2089,7 +2092,7 @@ assume "compact S" then obtain W g where "C \ W" and opeW: "openin (top_of_set S) W" and contg: "continuous_on W g" - and gim: "g ` W \ U" and gf: "\x. x \ C \ g x = f x" + and gim: "g \ W \ U" and gf: "\x. x \ C \ g x = f x" using ANR_imp_absolute_neighbourhood_extensor [of U C f S] C \ANR U\ closedin_component contf fim by blast then obtain V where "open V" and V: "W = S \ V" by (auto simp: openin_open) @@ -2103,13 +2106,13 @@ by (meson \compact K\ \compact S\ closedin_compact_eq opeK openin_imp_subset) show "continuous_on K g" by (metis Int_subset_iff V \K \ V\ contg continuous_on_subset opeK openin_subtopology subset_eq) - show "g ` K \ U" + show "g \ K \ U" using V \K \ V\ gim opeK openin_imp_subset by fastforce qed (use opeK gf \C \ K\ in auto) qed - obtain h where "continuous_on S h" "h ` S \ U" "\x. x \ T \ h x = g x" + obtain h where "continuous_on S h" "h \ S \ U" "\x. x \ T \ h x = g x" using extension_from_clopen - by (metis C bot.extremum_uniqueI clo contg gim fim image_is_empty in_components_nonempty ope) + by (metis C bot.extremum_uniqueI clo contg gim fim image_is_empty in_components_nonempty ope image_subset_iff_funcset) then show ?thesis by (metis \C \ T\ gf subset_eq that) qed @@ -2198,9 +2201,9 @@ obtain W k where W: "({0,1} \ S) \ ({0..1} \ T) \ W" and opeW: "openin (top_of_set ({0..1} \ S)) W" and contk: "continuous_on W k" - and kim: "k ` W \ U" + and kim: "k \ W \ U" and kh': "\x. x \ ({0,1} \ S) \ ({0..1} \ T) \ k x = h' x" - by (metis ANR_imp_absolute_neighbourhood_extensor [OF \ANR U\, of "({0,1} \ S) \ ({0..1} \ T)" h' "{0..1} \ S"]) + by (metis ANR_imp_absolute_neighbourhood_extensor [OF \ANR U\, of "({0,1} \ S) \ ({0..1} \ T)" h' "{0..1} \ S"] image_subset_iff_funcset) obtain T' where opeT': "openin (top_of_set S) T'" and "T \ T'" and TW: "{0..1} \ T' \ W" using tube_lemma_gen [of "{0..1::real}" T S W] W \T \ S\ opeW by auto @@ -2377,11 +2380,11 @@ fixes S :: "'a :: euclidean_space set" and T :: "'b :: euclidean_space set" assumes S: "locally connected S \ compact S" and "ANR T" shows - "(\f g. continuous_on S f \ f ` S \ T \ continuous_on S g \ g ` S \ T \ + "(\f g. continuous_on S f \ f \ S \ T \ continuous_on S g \ g \ S \ T \ homotopic_with_canon (\x. True) S T f g) \ (\C\components S. - \f g. continuous_on C f \ f ` C \ T \ continuous_on C g \ g ` C \ T \ + \f g. continuous_on C f \ f \ C \ T \ continuous_on C g \ g \ C \ T \ homotopic_with_canon (\x. True) C T f g)" (is "?lhs = ?rhs") proof @@ -2389,11 +2392,11 @@ show ?rhs proof clarify fix C f g - assume contf: "continuous_on C f" and fim: "f ` C \ T" - and contg: "continuous_on C g" and gim: "g ` C \ T" and C: "C \ components S" - obtain f' where contf': "continuous_on S f'" and f'im: "f' ` S \ T" and f'f: "\x. x \ C \ f' x = f x" + assume contf: "continuous_on C f" and fim: "f \ C \ T" + and contg: "continuous_on C g" and gim: "g \ C \ T" and C: "C \ components S" + obtain f' where contf': "continuous_on S f'" and f'im: "f' \ S \ T" and f'f: "\x. x \ C \ f' x = f x" using extension_from_component [OF S \ANR T\ C contf fim] by metis - obtain g' where contg': "continuous_on S g'" and g'im: "g' ` S \ T" and g'g: "\x. x \ C \ g' x = g x" + obtain g' where contg': "continuous_on S g'" and g'im: "g' \ S \ T" and g'g: "\x. x \ C \ g' x = g x" using extension_from_component [OF S \ANR T\ C contg gim] by metis have "homotopic_with_canon (\x. True) C T f' g'" using L [OF contf' f'im contg' g'im] homotopic_with_subset_left C in_components_subset by fastforce @@ -2405,11 +2408,11 @@ show ?lhs proof clarify fix f g - assume contf: "continuous_on S f" and fim: "f ` S \ T" - and contg: "continuous_on S g" and gim: "g ` S \ T" + assume contf: "continuous_on S f" and fim: "f \ S \ T" + and contg: "continuous_on S g" and gim: "g \ S \ T" moreover have "homotopic_with_canon (\x. True) C T f g" if "C \ components S" for C - using R [OF that] - by (meson contf contg continuous_on_subset fim gim image_mono in_components_subset order.trans that) + using R [OF that] contf contg continuous_on_subset fim gim in_components_subset + by (smt (verit, del_insts) Pi_anti_mono subsetD that) ultimately show "homotopic_with_canon (\x. True) S T f g" by (subst homotopic_on_components_eq [OF S \ANR T\]) auto qed diff -r d4125fc10c0c -r 1260be3f33a4 src/HOL/Analysis/Starlike.thy --- a/src/HOL/Analysis/Starlike.thy Sun Jul 02 20:41:07 2023 +0200 +++ b/src/HOL/Analysis/Starlike.thy Mon Jul 03 16:46:37 2023 +0100 @@ -4202,7 +4202,7 @@ lemma proper_map_from_compact: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" - assumes contf: "continuous_on S f" and imf: "f ` S \ T" and "compact S" + assumes contf: "continuous_on S f" and imf: "f \ S \ T" and "compact S" "closedin (top_of_set T) K" shows "compact (S \ f -` K)" by (rule closedin_compact [OF \compact S\] continuous_closedin_preimage_gen assms)+ @@ -5820,7 +5820,7 @@ lemma continuous_closed_graph_eq: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" - assumes "compact T" and fim: "f ` S \ T" + assumes "compact T" and fim: "f \ S \ T" shows "continuous_on S f \ closedin (top_of_set (S \ T)) ((\x. Pair x (f x)) ` S)" (is "?lhs = ?rhs") @@ -5848,7 +5848,7 @@ lemma continuous_from_closed_graph: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" - assumes "compact T" and fim: "f ` S \ T" and clo: "closed ((\x. Pair x (f x)) ` S)" + assumes "compact T" and fim: "f \ S \ T" and clo: "closed ((\x. Pair x (f x)) ` S)" shows "continuous_on S f" using fim clo by (auto intro: closed_subset simp: continuous_closed_graph_eq [OF \compact T\ fim]) diff -r d4125fc10c0c -r 1260be3f33a4 src/HOL/Analysis/Urysohn.thy --- a/src/HOL/Analysis/Urysohn.thy Sun Jul 02 20:41:07 2023 +0200 +++ b/src/HOL/Analysis/Urysohn.thy Mon Jul 03 16:46:37 2023 +0100 @@ -2516,8 +2516,9 @@ show ?thesis unfolding Lipschitz_continuous_map_pos proof - show "f ` mspace (submetric m1 T) \ mspace m2" - by (metis cmf Metric_space.metric_continuous_map Metric_space_mspace_mdist mtopology_of_def mtopology_of_submetric) + show "f \ mspace (submetric m1 T) \ mspace m2" + by (metis cmf Metric_space.metric_continuous_map Metric_space_mspace_mdist mtopology_of_def + mtopology_of_submetric image_subset_iff_funcset) define X where "X \ prod_topology (subtopology L.M1.mtopology T) (subtopology L.M1.mtopology T)" obtain B::real where "B > 0" and B: "\(x,y) \ S\S. mdist m2 (f x) (f y) \ B * mdist m1 x y" using lcf \S \ mspace m1\ by (force simp: Lipschitz_continuous_map_pos) @@ -2608,8 +2609,9 @@ show ?thesis unfolding uniformly_continuous_map_def proof (intro conjI strip) - show "f ` mspace (submetric m1 T) \ mspace m2" - by (metis cmf Metric_space.metric_continuous_map Metric_space_mspace_mdist mtopology_of_def mtopology_of_submetric) + show "f \ mspace (submetric m1 T) \ mspace m2" + by (metis cmf Metric_space.metric_continuous_map Metric_space_mspace_mdist + mtopology_of_def mtopology_of_submetric image_subset_iff_funcset) fix \::real assume "\ > 0" then obtain \ where "\>0" and \: "\(x,y) \ S\S. mdist m1 x y < \ \ mdist m2 (f x) (f y) \ \/2" @@ -3143,7 +3145,7 @@ lemma mspace_cfunspace [simp]: "mspace (cfunspace X m) = - {f. f ` topspace X \ mspace m \ f \ extensional (topspace X) \ + {f. f \ topspace X \ mspace m \ f \ extensional (topspace X) \ Metric_space.mbounded (mspace m) (mdist m) (f ` (topspace X)) \ continuous_map X (mtopology_of m) f}" by (auto simp: cfunspace_def Metric_space.fspace_def) @@ -3278,7 +3280,7 @@ assume g: "range \ \ mspace (cfunspace X Self) \ limitin F.mtopology \ g sequentially" show "g \ mspace (cfunspace X Self)" proof (simp add: mtopology_of_def, intro conjI) - show "g ` topspace X \ M" "g \ extensional (topspace X)" "mbounded (g ` topspace X)" + show "g \ topspace X \ M" "g \ extensional (topspace X)" "mbounded (g ` topspace X)" using g F.limitin_mspace by (force simp: fspace_def)+ show "continuous_map X mtopology g" using * g by blast @@ -3296,7 +3298,7 @@ obtains f :: "['a,'a] \ real" and S where "S \ mspace(funspace M euclidean_metric)" "mcomplete_of (submetric (funspace M euclidean_metric) S)" - "f ` M \ S" + "f \ M \ S" "mtopology_of(funspace M euclidean_metric) closure_of f ` M = S" "\x y. \x \ M; y \ M\ \ mdist (funspace M euclidean_metric) (f x) (f y) = d x y" @@ -3337,7 +3339,7 @@ using Metric_space.mcomplete_funspace Met_TC.Metric_space_axioms by (fastforce simp: mcomplete_of_def) ultimately show "mcomplete_of (submetric (funspace M euclidean_metric) S)" by (simp add: S.closedin_eq_mcomplete mcomplete_of_def) - show "f ` M \ S" + show "f \ M \ S" using S_def fim in_closure_of m'_def by fastforce show "mtopology_of (funspace M euclidean_metric) closure_of f ` M = S" by (auto simp: f_def S_def mtopology_of_def) @@ -3363,14 +3365,14 @@ lemma (in Metric_space) metric_completion: obtains f :: "['a,'a] \ real" and m' where "mcomplete_of m'" - "f ` M \ mspace m' " + "f \ M \ mspace m' " "mtopology_of m' closure_of f ` M = mspace m'" "\x y. \x \ M; y \ M\ \ mdist m' (f x) (f y) = d x y" proof - obtain f :: "['a,'a] \ real" and S where Ssub: "S \ mspace(funspace M euclidean_metric)" and mcom: "mcomplete_of (submetric (funspace M euclidean_metric) S)" - and fim: "f ` M \ S" + and fim: "f \ M \ S" and eqS: "mtopology_of(funspace M euclidean_metric) closure_of f ` M = S" and eqd: "\x y. \x \ M; y \ M\ \ mdist (funspace M euclidean_metric) (f x) (f y) = d x y" using metric_completion_explicit by metis @@ -3379,11 +3381,11 @@ proof show "mcomplete_of m'" by (simp add: mcom m'_def) - show "f ` M \ mspace m'" + show "f \ M \ mspace m'" using Ssub fim m'_def by auto show "mtopology_of m' closure_of f ` M = mspace m'" using eqS fim Ssub - by (force simp: m'_def mtopology_of_submetric closure_of_subtopology Int_absorb1) + by (force simp: m'_def mtopology_of_submetric closure_of_subtopology Int_absorb1 image_subset_iff_funcset) show "mdist m' (f x) (f y) = d x y" if "x \ M" and "y \ M" for x y using that eqd m'_def by force qed @@ -3400,10 +3402,10 @@ then interpret Metric_space M d by simp obtain f :: "['a,'a] \ real" and m' where "mcomplete_of m'" - and fim: "f ` M \ mspace m' " + and fim: "f \ M \ mspace m' " and m': "mtopology_of m' closure_of f ` M = mspace m'" and eqd: "\x y. \x \ M; y \ M\ \ mdist m' (f x) (f y) = d x y" - by (meson metric_completion) + by (metis metric_completion) show thesis proof show "completely_metrizable_space (mtopology_of m')" @@ -3412,7 +3414,8 @@ by (metis Metric_space_mspace_mdist) show "embedding_map X (mtopology_of m') f" using Metric_space12.isometry_imp_embedding_map - by (metis Metric_space12_def Metric_space_axioms Metric_space_mspace_mdist Xeq eqd fim mtopology_of_def) + by (metis Metric_space12_def Metric_space_axioms Metric_space_mspace_mdist Xeq eqd fim + mtopology_of_def) show "(mtopology_of m') closure_of f ` topspace X = topspace (mtopology_of m')" by (simp add: Xeq m') qed @@ -3424,7 +3427,7 @@ lemma (in Metric_space) contraction_imp_unique_fixpoint: assumes "f x = x" "f y = y" - and "f ` M \ M" + and "f \ M \ M" and "k < 1" and "\x y. \x \ M; y \ M\ \ d (f x) (f y) \ k * d x y" and "x \ M" "y \ M" @@ -3433,7 +3436,7 @@ text \Banach Fixed-Point Theorem (aka, Contraction Mapping Principle)\ lemma (in Metric_space) Banach_fixedpoint_thm: - assumes mcomplete and "M \ {}" and fim: "f ` M \ M" + assumes mcomplete and "M \ {}" and fim: "f \ M \ M" and "k < 1" and con: "\x y. \x \ M; y \ M\ \ d (f x) (f y) \ k * d x y" obtains x where "x \ M" "f x = x" @@ -3444,7 +3447,7 @@ proof (cases "\x \ M. f x = f a") case True then show ?thesis - by (metis \a \ M\ fim image_subset_iff that) + by (metis \a \ M\ fim image_subset_iff image_subset_iff_funcset that) next case False then obtain b where "b \ M" and b: "f b \ f a" @@ -3472,7 +3475,7 @@ fix \::real assume "\>0" with \k < 1\ \f a \ a\ \a \ M\ fim have gt0: "((1 - k) * \) / d a (f a) > 0" - by (fastforce simp: divide_simps) + by (fastforce simp: divide_simps Pi_iff) obtain N where "k^N < ((1-k) * \) / d a (f a)" using real_arch_pow_inv [OF gt0 \k < 1\] by blast then have N: "\n. n \ N \ k^n < ((1-k) * \) / d a (f a)" @@ -3992,11 +3995,11 @@ shows "embedding_map X (product_topology (\f. top_of_set {0..1::real}) (mspace (submetric (cfunspace X euclidean_metric) - {f. f ` topspace X \ {0..1}})) ) - (\x. \f \ mspace (submetric (cfunspace X euclidean_metric) {f. f ` topspace X \ {0..1}}). + {f. f \ topspace X \ {0..1}})) ) + (\x. \f \ mspace (submetric (cfunspace X euclidean_metric) {f. f \ topspace X \ {0..1}}). f x)" proof - - define K where "K \ mspace(submetric (cfunspace X euclidean_metric) {f. f ` topspace X \ {0..1::real}})" + define K where "K \ mspace(submetric (cfunspace X euclidean_metric) {f. f \ topspace X \ {0..1::real}})" define e where "e \ \x. \f\K. f x" have "e x \ e y" if xy: "x \ y" "x \ topspace X" "y \ topspace X" for x y proof - @@ -4023,14 +4026,14 @@ assume "e x \ K \\<^sub>E {0..1}" and "x \ topspace X" and "openin X U" and "x \ U" then obtain g where contg: "continuous_map X (top_of_set {0..1}) g" and "g x = 0" and gim: "g ` (topspace X - U) \ {1::real}" - using \completely_regular_space X\ unfolding completely_regular_space_def + using \completely_regular_space X\ unfolding completely_regular_space_def by (metis Diff_iff openin_closedin_eq) then have "bounded (g ` topspace X)" by (meson bounded_closed_interval bounded_subset continuous_map_in_subtopology) - moreover have "g ` topspace X \ {0..1}" - using contg by (simp add: continuous_map_in_subtopology) + moreover have "g \ topspace X \ {0..1}" + using contg by (simp add: continuous_map_def) ultimately have g_in_K: "restrict g (topspace X) \ K" - using contg by (simp add: K_def continuous_map_in_subtopology) + using contg by (force simp add: K_def continuous_map_in_subtopology) have "openin (top_of_set {0..1}) {0..<1::real}" using open_real_greaterThanLessThan[of "-1" 1] by (force simp: openin_open) moreover have "e x \ (\\<^sub>E f\K. if f = restrict g (topspace X) then {0..<1} else {0..1})" diff -r d4125fc10c0c -r 1260be3f33a4 src/HOL/Complex_Analysis/Conformal_Mappings.thy --- a/src/HOL/Complex_Analysis/Conformal_Mappings.thy Sun Jul 02 20:41:07 2023 +0200 +++ b/src/HOL/Complex_Analysis/Conformal_Mappings.thy Mon Jul 03 16:46:37 2023 +0100 @@ -1145,7 +1145,7 @@ lemma covering_space_lift_is_holomorphic: assumes cov: "covering_space C p S" and C: "open C" "p holomorphic_on C" - and holf: "f holomorphic_on U" and fim: "f ` U \ S" and gim: "g ` U \ C" + and holf: "f holomorphic_on U" and fim: "f \ U \ S" and gim: "g \ U \ C" and contg: "continuous_on U g" and pg_f: "\x. x \ U \ p(g x) = f x" shows "g holomorphic_on U" unfolding holomorphic_on_def @@ -1161,7 +1161,7 @@ then have "\W. W \ \ \ open W \ W \ C" by (metis \open C\ inf_le1 open_Int openin_open) then obtain V where "V \ \" "g z \ V" "open V" "V \ C" - by (metis IntI UnionE image_subset_iff vimageI UV \f z \ T\ \z \ U\ gim pg_f) + by (metis IntI UnionE image_subset_iff vimageI UV \f z \ T\ \z \ U\ gim pg_f image_subset_iff_funcset) have holp: "p holomorphic_on V" using \V \ C\ \p holomorphic_on C\ holomorphic_on_subset by blast moreover have injp: "inj_on p V" @@ -1201,15 +1201,14 @@ lemma covering_space_lift_holomorphic: assumes cov: "covering_space C p S" and C: "open C" "p holomorphic_on C" - and f: "f holomorphic_on U" "f ` U \ S" + and f: "f holomorphic_on U" "f \ U \ S" and U: "simply_connected U" "locally path_connected U" - obtains g where "g holomorphic_on U" "g ` U \ C" "\y. y \ U \ p(g y) = f y" + obtains g where "g holomorphic_on U" "g \ U \ C" "\y. y \ U \ p(g y) = f y" proof - - obtain g where "continuous_on U g" "g ` U \ C" "\y. y \ U \ p(g y) = f y" - using covering_space_lift [OF cov U] - using f holomorphic_on_imp_continuous_on by blast + obtain g where "continuous_on U g" "g \ U \ C" "\y. y \ U \ p(g y) = f y" + using covering_space_lift [OF cov U] f holomorphic_on_imp_continuous_on by blast then show ?thesis - by (metis C cov covering_space_lift_is_holomorphic f that) + by (metis C cov covering_space_lift_is_holomorphic f image_subset_iff_funcset that) qed subsection\The Schwarz Lemma\ diff -r d4125fc10c0c -r 1260be3f33a4 src/HOL/Complex_Analysis/Riemann_Mapping.thy --- a/src/HOL/Complex_Analysis/Riemann_Mapping.thy Sun Jul 02 20:41:07 2023 +0200 +++ b/src/HOL/Complex_Analysis/Riemann_Mapping.thy Mon Jul 03 16:46:37 2023 +0100 @@ -1624,7 +1624,7 @@ qed show "continuous_on UNIV (\w. \ + exp w)" by (rule continuous_intros)+ - show "range (\w. \ + exp w) \ -{\}" + show "(\w. \ + exp w) \ UNIV \ -{\}" by auto qed then have "homotopic_with_canon (\r. pathfinish r = pathstart r) {0..1} (-{\}) p (\x. \ + 1)" diff -r d4125fc10c0c -r 1260be3f33a4 src/HOL/Library/FuncSet.thy --- a/src/HOL/Library/FuncSet.thy Sun Jul 02 20:41:07 2023 +0200 +++ b/src/HOL/Library/FuncSet.thy Mon Jul 03 16:46:37 2023 +0100 @@ -148,9 +148,10 @@ by (auto simp: Pi_def) lemma Pi_fupd_iff: "i \ I \ f \ Pi I (B(i := A)) \ f \ Pi (I - {i}) B \ f i \ A" - apply auto - apply (metis PiE fun_upd_apply) - by force + using mk_disjoint_insert by fastforce + +lemma fst_Pi: "fst \ A \ B \ A" and snd_Pi: "snd \ A \ B \ B" + by auto subsection \Composition With a Restricted Domain: \<^term>\compose\\