# HG changeset patch # User paulson # Date 1673456572 0 # Node ID 7ed303c024187025d7c89dd9d27a42284c1a34b4 # Parent f5a7f171d186b54d39ce54129845b0010a030ba9 More tidying of topology proofs diff -r f5a7f171d186 -r 7ed303c02418 src/HOL/Analysis/Further_Topology.thy --- a/src/HOL/Analysis/Further_Topology.thy Wed Jan 11 13:41:53 2023 +0000 +++ b/src/HOL/Analysis/Further_Topology.thy Wed Jan 11 17:02:52 2023 +0000 @@ -369,7 +369,7 @@ with \\ s \ 0\ have "r > 0" "s > 0" by auto show thesis using inessential_spheremap_lowdim_gen [of "cball a r" "cball b s" f] - using \0 < r\ \0 < s\ assms(1) that by (auto simp add: f aff_dim_cball) + using \0 < r\ \0 < s\ assms(1) that by (auto simp add: f aff_dim_cball) qed qed @@ -1538,8 +1538,7 @@ then have "\ bounded (\{C \ components (T - S). \ bounded C})" by (metis (no_types, lifting) Sup_upper bounded_subset mem_Collect_eq that) then show ?thesis - apply (clarsimp simp: LU_def Int_Un_distrib Diff_Int_distrib Int_UN_distrib) - by (metis (no_types, lifting) False Sup_upper bounded_cbox bounded_subset inf.orderE mem_Collect_eq that) + by (simp add: LU_def disjoint_iff) (meson False bounded_cbox bounded_subset subset_iff that) qed qed blast have *: False if "x \ cbox (- b - m *\<^sub>R One) (b + m *\<^sub>R One)" @@ -1611,10 +1610,11 @@ then show ?thesis using cT_ne clo_cT closest_point_in_set by blast qed - show "continuous_on (T - K \ cbox (- (b + One)) (b + One)) (g \ closest_point (cbox (-c) c \ T))" - using cloTK - apply (intro continuous_on_compose continuous_on_closest_point continuous_on_subset [OF contg]) - by (auto simp add: clo_cT affine_imp_convex \affine T\ convex_Int cT_ne) + have "convex (cbox (- c) c \ T)" + by (simp add: affine_imp_convex assms(4) convex_Int) + then show "continuous_on (T - K \ cbox (- (b + One)) (b + One)) (g \ closest_point (cbox (-c) c \ T))" + using cloTK clo_cT cT_ne + by (intro continuous_on_compose continuous_on_closest_point continuous_on_subset [OF contg]; force) 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 @@ -1646,10 +1646,9 @@ then have "aff_dim T \ aff_dim (cball a r)" by (simp add: aff aff_dim_cball) then show ?thesis - apply (rule extend_map_affine_to_sphere_cofinite_gen - [OF \compact S\ convex_cball bounded_cball \affine T\ \S \ T\ _ contf]) - using fim apply (auto simp: assms False that dest: dis) - done + 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) qed corollary extend_map_UNIV_to_sphere_cofinite: @@ -1673,9 +1672,9 @@ 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" - apply (rule extend_map_UNIV_to_sphere_cofinite [OF aff \0 \ r\ \compact S\ contf fim, of "{}"]) - apply (auto dest: dis) -done + using extend_map_UNIV_to_sphere_cofinite [OF aff \0 \ r\ \compact S\ contf fim, of "{}"] + by (metis Compl_empty_eq dis subset_empty) + theorem Borsuk_separation_theorem_gen: fixes S :: "'a::euclidean_space set" @@ -1739,11 +1738,10 @@ qed next assume R: ?rhs - then show ?lhs - apply (simp add: Borsuk_separation_theorem_gen [OF \compact S\, symmetric]) - apply (auto simp: components_def connected_iff_eq_connected_component_set) - using connected_component_in apply fastforce - using cobounded_unique_unbounded_component [OF _ 2, of "-S"] \compact S\ compact_eq_bounded_closed by fastforce + then have "\c\components (- S). \ bounded c \ connected (- S)" + by (metis "2" assms(1) cobounded_has_bounded_component compact_imp_bounded double_complement) + with R show ?lhs + by (simp add: Borsuk_separation_theorem_gen [OF \compact S\]) qed @@ -2017,8 +2015,7 @@ show "open (k ` U)" by (simp add: ope_iff homeomorphism_imp_open_map [OF homkh ope]) show "inj_on (k \ f \ h) (k ` U)" - apply (clarsimp simp: inj_on_def) - by (metis \U \ S\ fim homeomorphism_apply2 homhk image_subset_iff inj_onD injf subsetD) + by (smt (verit) comp_apply inj_on_def \U \ S\ fim homeomorphism_apply2 homhk image_iff injf subsetD) qed moreover have eq: "f ` U = h ` (k \ f \ h \ k) ` U" @@ -2102,8 +2099,7 @@ show "continuous_on S (h \ f)" by (meson contf continuous_on_compose continuous_on_subset fim homeomorphism_cont1 homhk) show "inj_on (h \ f) S" - apply (clarsimp simp: inj_on_def) - by (metis fim homeomorphism_apply2 [OF homkh] image_subset_iff inj_onD injf) + by (smt (verit, ccfv_SIG) comp_apply fim inj_on_def homeomorphism_apply2 [OF homkh] image_subset_iff injf) show "(h \ f) ` S \ U" using \V' \ U\ hfV' by auto qed (auto simp: assms) @@ -2134,8 +2130,7 @@ moreover have "(h \ f) ` S \ U" using \T \ U\ fim homeomorphism_image1 homhk by fastforce moreover have "inj_on (h \ f) S" - apply (clarsimp simp: inj_on_def) - by (metis fim homeomorphism_apply1 homhk image_subset_iff inj_onD injf) + by (smt (verit, best) comp_apply inj_on_def fim homeomorphism_apply1 homhk image_subset_iff injf) ultimately have ope_hf: "openin (top_of_set U) ((h \ f) ` S)" using invariance_of_domain_subspaces [OF ope \subspace U\ \subspace U\] by blast have "(h \ f) ` S \ T" @@ -2298,9 +2293,13 @@ lemma injective_into_1d_imp_open_map_UNIV: fixes f :: "'a::euclidean_space \ real" assumes "open T" "continuous_on S f" "inj_on f S" "T \ S" - shows "open (f ` T)" - apply (rule invariance_of_domain_gen [OF \open T\]) - using assms by (auto simp: elim: continuous_on_subset subset_inj_on) + shows "open (f ` T)" +proof - + have "DIM(real) \ DIM('a)" + by simp + then show ?thesis + using invariance_of_domain_gen assms continuous_on_subset subset_inj_on by metis +qed lemma continuous_on_inverse_open: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" @@ -2402,7 +2401,7 @@ fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "S homeomorphic T" "open S" "S \ {}" "open T" "T \ {}" shows "DIM('a) = DIM('b)" - using assms + using assms apply (simp add: homeomorphic_minimal) apply (rule order_antisym; metis inj_onI invariance_of_dimension) done @@ -2412,9 +2411,6 @@ assumes "S homeomorphic T" "interior S = {} \ interior T = {}" shows "(interior S) homeomorphic (interior T)" proof (cases "interior T = {}") - case True - with assms show ?thesis by auto -next case False then have "DIM('a) = DIM('b)" using assms @@ -2423,7 +2419,7 @@ done then show ?thesis by (rule homeomorphic_interiors_same_dimension [OF \S homeomorphic T\]) -qed +qed (use assms in auto) lemma homeomorphic_frontiers_same_dimension: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" @@ -2659,7 +2655,7 @@ obtain f g where S: "\x\S. f x \ T \ g (f x) = x" and T: "\y\T. g y \ S \ f (g y) = y" and contf: "continuous_on S f" and contg: "continuous_on T g" - using assms [unfolded homeomorphic_minimal] by auto + using assms by (auto simp: homeomorphic_minimal) have "aff_dim (affine hull S) \ aff_dim (affine hull T)" using False assms homeomorphic_aff_dim_le by blast moreover have "aff_dim (affine hull T) \ aff_dim (affine hull S)" @@ -2762,16 +2758,14 @@ using Arg2pi_eq that h01 by (force simp: j_def) have eq: "S = S \ (UNIV \ {z. 0 \ Im z}) \ S \ (UNIV \ {z. Im z \ 0})" for S :: "(real*complex)set" by auto + have \
: "Arg2pi z \ 2 * pi" for z + by (simp add: Arg2pi order_le_less) have c1: "continuous_on ({0..1} \ sphere 0 1 \ UNIV \ {z. 0 \ Im z}) (\x. h (fst x, Arg2pi (snd x) / (2 * pi)))" apply (intro continuous_intros continuous_on_compose2 [OF conth] continuous_on_compose2 [OF continuous_on_upperhalf_Arg2pi]) - apply (auto simp: Arg2pi) - apply (meson Arg2pi_lt_2pi linear not_le) - done + by (auto simp: Arg2pi \
) have c2: "continuous_on ({0..1} \ sphere 0 1 \ UNIV \ {z. Im z \ 0}) (\x. h (fst x, 1 - Arg2pi (cnj (snd x)) / (2 * pi)))" apply (intro continuous_intros continuous_on_compose2 [OF conth] continuous_on_compose2 [OF continuous_on_upperhalf_Arg2pi]) - apply (auto simp: Arg2pi) - apply (meson Arg2pi_lt_2pi linear not_le) - done + by (auto simp: Arg2pi \
) show "continuous_on ({0..1} \ sphere 0 1) j" apply (simp add: j_def) apply (subst eq) @@ -2800,10 +2794,11 @@ and contg: "continuous_on (sphere 0 1) g" and gim: "g ` (sphere 0 1) \ S" shows "homotopic_with_canon (\h. True) (sphere 0 1) S f g" proof - - have "homotopic_loops S (f \ exp \ (\t. of_real(2 * pi * t) * \)) (g \ exp \ (\t. of_real(2 * pi * t) * \))" - apply (rule S [unfolded simply_connected_homotopic_loops, rule_format]) - apply (simp add: homotopic_circlemaps_imp_homotopic_loops contf fim contg gim) - done + let ?h = "(\t. complex_of_real (2 * pi * t) * \)" + have "homotopic_loops S (f \ exp \ ?h) (f \ exp \ ?h) \ homotopic_loops S (g \ exp \ ?h) (g \ exp \ ?h)" + by (simp add: homotopic_circlemaps_imp_homotopic_loops contf fim contg gim) + then have "homotopic_loops S (f \ exp \ ?h) (g \ exp \ ?h)" + using S simply_connected_homotopic_loops by blast then show ?thesis apply (rule homotopic_with_eq [OF homotopic_loops_imp_homotopic_circlemaps]) apply (auto simp: o_def complex_norm_eq_1_exp mult.commute) @@ -2818,9 +2813,7 @@ continuous_on (sphere 0 1) g; g ` (sphere 0 1) \ S\ \ homotopic_with_canon (\h. True) (sphere 0 1) S f g" shows "\a. homotopic_with_canon (\h. True) (sphere 0 1) S h (\x. a)" - apply (rule_tac x="h 1" in exI) - apply (rule hom) - using assms by (auto) + by (metis conth continuous_on_const him hom image_subset_iff) lemma simply_connected_eq_homotopic_circlemaps2b: fixes S :: "'a::real_normed_vector set" @@ -2874,9 +2867,8 @@ continuous_on (sphere 0 1) f \ f ` (sphere 0 1) \ S \ continuous_on (sphere 0 1) g \ g ` (sphere 0 1) \ S \ homotopic_with_canon (\h. True) (sphere 0 1) S f g)" - apply (rule iffI) - apply (blast dest: simply_connected_eq_homotopic_circlemaps1) - by (simp add: simply_connected_eq_homotopic_circlemaps2a simply_connected_eq_homotopic_circlemaps2b simply_connected_eq_homotopic_circlemaps3) + by (metis simply_connected_eq_homotopic_circlemaps1 simply_connected_eq_homotopic_circlemaps2a + simply_connected_eq_homotopic_circlemaps2b simply_connected_eq_homotopic_circlemaps3) proposition simply_connected_eq_contractible_circlemap: fixes S :: "'a::real_normed_vector set" @@ -2885,9 +2877,8 @@ (\f::complex \ 'a. continuous_on (sphere 0 1) f \ f `(sphere 0 1) \ S \ (\a. homotopic_with_canon (\h. True) (sphere 0 1) S f (\x. a)))" - apply (rule iffI) - apply (simp add: simply_connected_eq_homotopic_circlemaps1 simply_connected_eq_homotopic_circlemaps2a simply_connected_eq_homotopic_circlemaps2b) - using simply_connected_eq_homotopic_circlemaps3 by blast + by (metis simply_connected_eq_homotopic_circlemaps simply_connected_eq_homotopic_circlemaps2a + simply_connected_eq_homotopic_circlemaps3 simply_connected_imp_path_connected) corollary homotopy_eqv_simple_connectedness: fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set" @@ -3004,8 +2995,12 @@ fixes a :: "'a::euclidean_space" and c :: "'b::euclidean_space" assumes "a \ 0" "c \ 0" shows "({x. a \ x = b} homeomorphic {x. c \ x = d} \ DIM('a) = DIM('b))" - apply (auto simp: homeomorphic_affine_sets_eq affine_hyperplane assms) - by (metis DIM_positive Suc_pred) +proof - + have "DIM('a) - Suc 0 = DIM('b) - Suc 0 \ DIM('a) = DIM('b)" + by (metis DIM_positive Suc_pred) + then show ?thesis + by (auto simp: homeomorphic_affine_sets_eq affine_hyperplane assms) +qed lemma homeomorphic_UNIV_UNIV: shows "(UNIV::'a set) homeomorphic (UNIV::'b set) \ @@ -3028,9 +3023,7 @@ by (rule convex_cball) then obtain c where "homotopic_with_canon (\z. True) (sphere (0::complex) 1) (rel_frontier S) f (\x. c)" apply (rule inessential_spheremap_lowdim_gen [OF _ bounded_cball \convex S\ \bounded S\, where f=f]) - using f 3 - apply (auto simp: aff_dim_cball) - done + using f 3 by (auto simp: aff_dim_cball) then show "\a. homotopic_with_canon (\h. True) (sphere 0 1) (rel_frontier S) f (\x. a)" by blast qed @@ -3086,9 +3079,7 @@ by (meson Diff_mono SU homeomorphism_def homeomorphism_of_subsets gh set_eq_subset) qed (use contf continuous_on_subset hgsub in blast) show "inj_on (f \ h) (g ` (S - {b}))" - using kjsub - apply (clarsimp simp add: inj_on_def) - by (metis SU b homeomorphism_def inj_onD injf insert_Diff insert_iff gh rev_subsetD) + by (smt (verit, del_insts) SU homeomorphism_def inj_on_def injf gh Diff_iff comp_apply imageE subset_iff) show "(f \ h) ` g ` (S - {b}) \ T" by (metis fim image_comp image_mono hgsub subset_trans) qed (auto simp: assms) @@ -3103,9 +3094,7 @@ by (meson Diff_mono SU homeomorphism_def homeomorphism_of_subsets jk set_eq_subset) qed (use contf continuous_on_subset kjsub in blast) show "inj_on (f \ k) (j ` (S - {c}))" - using kjsub - apply (clarsimp simp add: inj_on_def) - by (metis SU c homeomorphism_def inj_onD injf insert_Diff insert_iff jk rev_subsetD) + by (smt (verit, del_insts) SU homeomorphism_def inj_on_def injf jk Diff_iff comp_apply imageE subset_iff) show "(f \ k) ` j ` (S - {c}) \ T" by (metis fim image_comp image_mono kjsub subset_trans) qed (auto simp: assms) @@ -3116,11 +3105,9 @@ have "h ` g ` (S - {b}) = (S - {b})" proof show "h ` g ` (S - {b}) \ S - {b}" - using homeomorphism_apply1 [OF gh] SU - by (fastforce simp add: image_iff image_subset_iff) + using homeomorphism_apply1 [OF gh] SU by (fastforce simp add: image_iff image_subset_iff) show "S - {b} \ h ` g ` (S - {b})" - apply clarify - by (metis SU subsetD homeomorphism_apply1 [OF gh] image_iff member_remove remove_def) + by (metis Diff_mono SU gh homeomorphism_image2 homeomorphism_of_subsets set_eq_subset) qed then show ?thesis by (metis image_comp) @@ -3128,14 +3115,8 @@ moreover have "(f \ k) ` j ` (S - {c}) = f ` (S - {c})" proof - have "k ` j ` (S - {c}) = (S - {c})" - proof - show "k ` j ` (S - {c}) \ S - {c}" - using homeomorphism_apply1 [OF jk] SU - by (fastforce simp add: image_iff image_subset_iff) - show "S - {c} \ k ` j ` (S - {c})" - apply clarify - by (metis SU subsetD homeomorphism_apply1 [OF jk] image_iff member_remove remove_def) - qed + using homeomorphism_apply1 [OF jk] SU + by (meson Diff_mono homeomorphism_def homeomorphism_of_subsets jk subset_refl) then show ?thesis by (metis image_comp) qed @@ -3237,8 +3218,7 @@ using contractible_sphere contractible_def not_one_le_zero by blast qed with False show ?rhs - apply simp - by (metis DIM_ge_Suc0 le_antisym not_less_eq_eq numeral_2_eq_2 numeral_3_eq_3) + by (metis DIM_ge_Suc0 One_nat_def Suc_1 not_less_eq_eq numeral_3_eq_3 order_antisym_conv) next assume ?rhs with False show ?lhs by (simp add: simply_connected_sphere) @@ -3595,7 +3575,10 @@ using pi_ge_two by (simp add: ball_subset_ball_iff) then have inj_exp: "inj_on exp (ball (Ln z) 1)" using inj_on_exp_pi inj_on_subset by blast - define \ where "\ \ range (\n. (\x. x + of_real (2 * of_int n * pi) * \) ` (ball(Ln z) 1))" + define twopi where "twopi \ \n. of_real (2 * of_int n * pi) * \" + define \ where "\ \ range (\n. (\x. x + twopi n) ` (ball(Ln z) 1))" + have exp_eq': "exp w = exp z \ (\n::int. w = z + twopi n)" for z w + by (simp add: exp_eq twopi_def) show ?thesis proof (intro exI conjI) show "z \ exp ` (ball(Ln z) 1)" @@ -3604,80 +3587,73 @@ by blast with inj_exp show "openin (top_of_set (- {0})) (exp ` ball (Ln z) 1)" by (auto simp: openin_open_eq invariance_of_domain continuous_on_exp [OF continuous_on_id]) - show "\\ = exp -` exp ` ball (Ln z) 1" - by (force simp: \_def Complex_Transcendental.exp_eq image_iff) + show UV: "\\ = exp -` exp ` ball (Ln z) 1" + by (force simp: \_def twopi_def Complex_Transcendental.exp_eq image_iff) show "\V\\. open V" by (auto simp: \_def inj_on_def continuous_intros invariance_of_domain) - have xy: "2 \ cmod (2 * of_int x * of_real pi * \ - 2 * of_int y * of_real pi * \)" - if "x < y" for x y + have "2 \ cmod (twopi m -twopi n)" if "m \ n" for m n proof - - have "1 \ abs (x - y)" + have "1 \ abs (m - n)" using that by linarith - then have "1 \ cmod (of_int x - of_int y) * 1" + then have "1 \ cmod (of_int m - of_int n) * 1" by (metis mult.right_neutral norm_of_int of_int_1_le_iff of_int_abs of_int_diff) - also have "... \ cmod (of_int x - of_int y) * of_real pi" + also have "... \ cmod (of_int m - of_int n) * of_real pi" using pi_ge_two by (intro mult_left_mono) auto - also have "... \ cmod ((of_int x - of_int y) * of_real pi * \)" + also have "... \ cmod ((of_int m - of_int n) * of_real pi * \)" by (simp add: norm_mult) - also have "... \ cmod (of_int x * of_real pi * \ - of_int y * of_real pi * \)" + also have "... \ cmod (of_int m * of_real pi * \ - of_int n * of_real pi * \)" by (simp add: algebra_simps) - finally have "1 \ cmod (of_int x * of_real pi * \ - of_int y * of_real pi * \)" . - then have "2 * 1 \ cmod (2 * (of_int x * of_real pi * \ - of_int y * of_real pi * \))" + finally have "1 \ cmod (of_int m * of_real pi * \ - of_int n * of_real pi * \)" . + then have "2 * 1 \ cmod (2 * (of_int m * of_real pi * \ - of_int n * of_real pi * \))" by (metis mult_le_cancel_left_pos norm_mult_numeral1 zero_less_numeral) then show ?thesis - by (simp add: algebra_simps) + by (simp add: algebra_simps twopi_def) qed - show "disjoint \" - apply (clarsimp simp add: \_def pairwise_def disjnt_def add.commute [of _ "x*y" for x y] - ball_eq_ball_iff intro!: disjoint_ballI) - apply (auto simp: dist_norm neq_iff) - by (metis norm_minus_commute xy)+ + then show "disjoint \" + unfolding \_def pairwise_def disjnt_iff + by (smt (verit, best) add.commute add_diff_cancel_left' add_diff_eq dist_commute dist_complex_def dist_triangle imageE mem_ball) show "\u\\. \q. homeomorphism u (exp ` ball (Ln z) 1) exp q" proof fix u assume "u \ \" - then obtain n where n: "u = (\x. x + of_real (2 * of_int n * pi) * \) ` (ball(Ln z) 1)" + then obtain n where n: "u = (\x. x + twopi n) ` (ball(Ln z) 1)" by (auto simp: \_def) have "compact (cball (Ln z) 1)" by simp moreover have "continuous_on (cball (Ln z) 1) exp" by (rule continuous_on_exp [OF continuous_on_id]) moreover have "inj_on exp (cball (Ln z) 1)" - apply (rule inj_on_subset [OF inj_on_exp_pi [of "Ln z"]]) - using pi_ge_two by (simp add: cball_subset_ball_iff) + using pi_ge_two inj_on_subset [OF inj_on_exp_pi [of "Ln z"]] + by (simp add: subset_iff) ultimately obtain \ where hom: "homeomorphism (cball (Ln z) 1) (exp ` cball (Ln z) 1) exp \" using homeomorphism_compact by blast have eq1: "exp ` u = exp ` ball (Ln z) 1" - apply (auto simp: algebra_simps n) - apply (rule_tac x = "_ + \ * (of_int n * (of_real pi * 2))" in image_eqI) - apply (auto simp: image_iff) - done - have \exp: "\ (exp x) + 2 * of_int n * of_real pi * \ = x" if "x \ u" for x + by (smt (verit) n exp_eq' image_cong image_image) + have \exp: "\ (exp x) + twopi n = x" if "x \ u" for x proof - - have "exp x = exp (x - 2 * of_int n * of_real pi * \)" - by (simp add: exp_eq) - then have "\ (exp x) = \ (exp (x - 2 * of_int n * of_real pi * \))" + have "exp x = exp (x - twopi n)" + using exp_eq' by auto + then have "\ (exp x) = \ (exp (x - twopi n))" by simp - also have "... = x - 2 * of_int n * of_real pi * \" + also have "... = x - twopi n" using \x \ u\ by (auto simp: n intro: homeomorphism_apply1 [OF hom]) finally show ?thesis by simp qed - have exp2n: "exp (\ (exp x) + 2 * of_int n * complex_of_real pi * \) = exp x" - if "dist (Ln z) x < 1" for x - using that by (auto simp: exp_eq homeomorphism_apply1 [OF hom]) + have exp2n: "exp (\ (exp x) + twopi n) = exp x" if "dist (Ln z) x < 1" for x + by (metis \exp exp_eq' imageI mem_ball n that) have "continuous_on (exp ` ball (Ln z) 1) \" by (meson ball_subset_cball continuous_on_subset hom homeomorphism_cont2 image_mono) - then have cont: "continuous_on (exp ` ball (Ln z) 1) (\x. \ x + 2 * of_int n * complex_of_real pi * \)" + then have cont: "continuous_on (exp ` ball (Ln z) 1) (\x. \ x + twopi n)" by (intro continuous_intros) - show "\q. homeomorphism u (exp ` ball (Ln z) 1) exp q" - apply (rule_tac x="(\x. x + of_real(2 * n * pi) * \) \ \" in exI) + have "homeomorphism u (exp ` ball (Ln z) 1) exp ((\x. x + twopi n) \ \)" unfolding homeomorphism_def apply (intro conjI ballI eq1 continuous_on_exp [OF continuous_on_id]) apply (auto simp: \exp exp2n cont n) apply (force simp: image_iff homeomorphism_apply1 [OF hom])+ done + then show "\q. homeomorphism u (exp ` ball (Ln z) 1) exp q" by metis qed qed qed @@ -3772,7 +3748,7 @@ using hom by (auto simp: homotopic_with_def) show ?thesis apply (simp add: homotopic_with) - apply (rule_tac x="\z. k z*(h \ snd)z" in exI) + apply (rule_tac x="\z. k z * (h \ snd)z" in exI) using kim hin by (fastforce simp: conth norm_mult k0 k1 intro!: contk continuous_intros)+ qed @@ -3817,10 +3793,10 @@ have [simp]: "\x. x \ S \ g x \ 0" using geq1 by fastforce have "homotopic_with_canon (\x. True) S (sphere 0 1) (\x. f x / g x) (\x. 1)" - apply (rule homotopic_with_eq [OF homotopic_with_sphere_times [OF L cont]]) + using homotopic_with_eq [OF homotopic_with_sphere_times [OF L cont]] by (auto simp: divide_inverse norm_inverse) with L show ?rhs - by (auto simp: homotopic_with_imp_continuous dest: homotopic_with_imp_subset1 homotopic_with_imp_subset2) + by (simp add: homotopic_with_imp_continuous homotopic_with_imp_subset1 homotopic_with_imp_subset2) next assume ?rhs then show ?lhs by (elim conjE homotopic_with_eq [OF homotopic_with_sphere_times]; force) @@ -3983,15 +3959,13 @@ by (force simp: openin_euclidean_subtopology_iff dest: fST) have oo: "\U. openin (top_of_set T) U \ openin (top_of_set S) {x \ S. f x \ U \ {}}" - apply (rule lower_hemicontinuous [THEN iffD1, rule_format]) - using fST clo by auto + using lower_hemicontinuous fST clo by blast have "compact (closure(f x))" by (simp add: bofx) moreover have "closure(f x) \ (\a \ f x. ball a (e/2))" using \0 < e\ by (force simp: closure_approachable simp del: divide_const_simps) ultimately obtain C where "C \ f x" "finite C" "closure(f x) \ (\a \ C. ball a (e/2))" - apply (rule compactE, force) - by (metis finite_subset_image) + by (meson compactE finite_subset_image Elementary_Metric_Spaces.open_ball compactE_image) then have fx_cover: "f x \ (\a \ C. ball a (e/2))" by (meson closure_subset order_trans) with fx_ne have "C \ {}" @@ -4158,9 +4132,10 @@ 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]) - then have "homotopic_with_canon (\z. True) (sphere a r) (sphere b s) f (\x. k c)" - apply (rule homotopic_with_eq, auto) + moreover have "\x. r = dist a x \ f x = k (h (f x))" by (metis fim hk homeomorphism_def image_subset_iff mem_sphere) + 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 by (metis that) qed @@ -4303,9 +4278,8 @@ by (simp add: exp_minus fgeq that) finally have "f z = exp (- h z) + \*g z" by (simp add: diff_eq_eq) - then show ?thesis - apply (simp add: cos_exp_eq) - by (metis fgeq add.assoc mult_2_right that) + with that show ?thesis + by (simp add: cos_exp_eq flip: fgeq) qed qed qed @@ -4376,11 +4350,7 @@ qed lemma retract_of_Borsukian: "\Borsukian T; S retract_of T\ \ Borsukian S" - apply (auto simp: retract_of_def retraction_def) - apply (erule (1) Borsukian_retraction_gen) - apply (meson retraction retraction_def) - apply (auto) - done + by (smt (verit) Borsukian_retraction_gen retract_of_def retraction retraction_def retraction_subset) lemma homeomorphic_Borsukian: "\Borsukian S; S homeomorphic T\ \ Borsukian T" using Borsukian_retraction_gen order_refl @@ -4565,12 +4535,7 @@ have "(\x. g x - h x) constant_on S \ T" proof (rule continuous_discrete_range_constant [OF ST]) show "continuous_on (S \ T) (\x. g x - h x)" - proof (intro continuous_intros) - show "continuous_on (S \ T) g" - by (meson contg continuous_on_subset inf_le1) - show "continuous_on (S \ T) h" - by (meson conth continuous_on_subset inf_sup_ord(2)) - qed + by (metis contg conth continuous_on_diff continuous_on_subset inf_le1 inf_le2) show "\e>0. \y. y \ S \ T \ g y - h y \ g x - h x \ e \ cmod (g y - h y - (g x - h x))" if "x \ S \ T" for x proof - @@ -4748,7 +4713,7 @@ by (simp add: Abstract_Topology_2.continuous_imp_closed_map \compact S\ contf fim) show "\U. closedin (top_of_set S) U \ closedin (top_of_set T) {x \ T. {z \ S. f z = x} \ U}" - using ope open_map_iff_lower_hemicontinuous_preimage [OF fim [THEN equalityD1]] + using ope open_map_iff_lower_hemicontinuous_preimage [OF fim [THEN equalityD1]] by meson show "bounded {z \ S. f z = y}" by (metis (no_types, lifting) compact_imp_bounded [OF \compact S\] bounded_subset mem_Collect_eq subsetI) @@ -4768,7 +4733,7 @@ by (fastforce simp: dist_norm abs_diff_less_iff algebra_simps) qed then show "\d>0. \x'\T. dist x' y < d \ dist (h (k x')) (h (k y)) < e" - using \0 < \\ by (auto simp: dist_commute) + using \0 < \\ by (auto simp: dist_commute) qed then show "\h. continuous_on T h \ (\x\T. g x = exp (\ * complex_of_real (h x)))" using fk gfh kTS by force @@ -5522,10 +5487,6 @@ by (simp_all add: assms) show "homotopic_with_canon (\x. True) S T f (\x. a)" if "S \ \" for S proof (cases "S = {}") - case True - then show ?thesis - by auto - next case False then obtain b where "b \ S" by blast @@ -5534,11 +5495,10 @@ then have "c \ T" using \b \ S\ homotopic_with_imp_subset2 by blast then have "homotopic_with_canon (\x. True) S T (\x. a) (\x. c)" - using T \a \ T\ homotopic_constant_maps path_connected_component - by (simp add: homotopic_constant_maps path_connected_component) + using T \a \ T\ by (simp add: homotopic_constant_maps path_connected_component) then show ?thesis using c homotopic_with_symD homotopic_with_trans by blast - qed + qed auto qed then show ?thesis .. qed @@ -5553,7 +5513,7 @@ by (simp add: assms compact_Un) with Borsukian_imp_unicoherent [of "S \ T"] ST assms show ?thesis - by (auto simp: closed_subset compact_imp_closed Borsukian_separation_compact unicoherent_def) + by (simp add: Borsukian_separation_compact closed_subset compact_imp_closed unicoherentD) qed end