# HG changeset patch # User paulson # Date 1483628617 0 # Node ID 6440577e34eee461ffc4c537980a769bc84f2191 # Parent 19f3d4af7a7d52f6ec7fc876e9826bdbd9305194 connectedness, circles not simply connected , punctured universe diff -r 19f3d4af7a7d -r 6440577e34ee src/HOL/Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Thu Jan 05 14:18:24 2017 +0000 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Thu Jan 05 15:03:37 2017 +0000 @@ -2021,6 +2021,55 @@ done qed +lemma connected_sphere_eq: + fixes a :: "'a :: euclidean_space" + shows "connected(sphere a r) \ 2 \ DIM('a) \ r \ 0" + (is "?lhs = ?rhs") +proof (cases r "0::real" rule: linorder_cases) + case less + then show ?thesis by auto +next + case equal + then show ?thesis by auto +next + case greater + show ?thesis + proof + assume L: ?lhs + have "False" if 1: "DIM('a) = 1" + proof - + obtain x y where xy: "sphere a r = {x,y}" "x \ y" + using sphere_1D_doubleton [OF 1 greater] + by (metis dist_self greater insertI1 less_add_same_cancel1 mem_sphere mult_2 not_le zero_le_dist) + then have "finite (sphere a r)" + by auto + with L \r > 0\ show "False" + apply (auto simp: connected_finite_iff_sing) + using xy by auto + qed + with greater show ?rhs + by (metis DIM_ge_Suc0 One_nat_def Suc_1 le_antisym not_less_eq_eq) + next + assume ?rhs + then show ?lhs + using connected_sphere greater by auto + qed +qed + +lemma path_connected_sphere_eq: + fixes a :: "'a :: euclidean_space" + shows "path_connected(sphere a r) \ 2 \ DIM('a) \ r \ 0" + (is "?lhs = ?rhs") +proof + assume ?lhs + then show ?rhs + using connected_sphere_eq path_connected_imp_connected by blast +next + assume R: ?rhs + then show ?lhs + by (auto simp: contractible_imp_path_connected contractible_sphere path_connected_sphere) +qed + proposition frontier_subset_retraction: fixes S :: "'a::euclidean_space set" assumes "bounded S" and fros: "frontier S \ T" @@ -2073,7 +2122,7 @@ ultimately show False by simp qed -subsection\Retractions\ +subsection\More Properties of Retractions\ lemma retraction: "retraction s t r \ @@ -2272,6 +2321,60 @@ using assms by (auto simp: retract_of_def retraction intro!: retraction_imp_quotient_map elim!: locally_path_connected_quotient_image) +subsubsection\A few simple lemmas about deformation retracts\ + +lemma deformation_retract_imp_homotopy_eqv: + fixes S :: "'a::euclidean_space set" + assumes "homotopic_with (\x. True) S S id r" "retraction S T r" + shows "S homotopy_eqv T" + apply (simp add: homotopy_eqv_def) + apply (rule_tac x=r in exI) + using assms apply (simp add: retraction_def) + apply (rule_tac x=id in exI) + apply (auto simp: continuous_on_id) + apply (metis homotopic_with_symD) + by (metis continuous_on_id' homotopic_with_equal homotopic_with_symD id_apply image_id subset_refl) + +lemma deformation_retract: + fixes S :: "'a::euclidean_space set" + shows "(\r. homotopic_with (\x. True) S S id r \ retraction S T r) \ + T retract_of S \ (\f. homotopic_with (\x. True) S S id f \ f ` S \ T)" + (is "?lhs = ?rhs") +proof + assume ?lhs + then show ?rhs + by (auto simp: retract_of_def retraction_def) +next + assume ?rhs + then show ?lhs + apply (clarsimp simp add: retract_of_def retraction_def) + apply (rule_tac x=r in exI, simp) + apply (rule homotopic_with_trans, assumption) + apply (rule_tac f = "r \ f" and g="r \ id" in homotopic_with_eq) + apply (rule_tac Y=S in homotopic_compose_continuous_left) + apply (auto simp: homotopic_with_sym) + done +qed + +lemma deformation_retract_of_contractible_sing: + fixes S :: "'a::euclidean_space set" + assumes "contractible S" "a \ S" + obtains r where "homotopic_with (\x. True) S S id r" "retraction S {a} r" +proof - + have "{a} retract_of S" + by (simp add: \a \ S\) + moreover have "homotopic_with (\x. True) S S id (\x. a)" + using assms + apply (clarsimp simp add: contractible_def) + apply (rule homotopic_with_trans, assumption) + by (metis assms(1) contractible_imp_path_connected homotopic_constant_maps homotopic_with_sym homotopic_with_trans insert_absorb insert_not_empty path_component_mem(1) path_connected_component) + moreover have "(\x. a) ` S \ {a}" + by (simp add: image_subsetI) + ultimately show ?thesis + using that deformation_retract by metis +qed + + subsection\Punctured affine hulls, etc.\ lemma continuous_on_compact_surface_projection_aux: @@ -2493,6 +2596,23 @@ by (metis assms closure_closed compact_eq_bounded_closed rel_frontier_def rel_frontier_retract_of_punctured_affine_hull) +lemma homotopy_eqv_rel_frontier_punctured_convex: + fixes S :: "'a::euclidean_space set" + assumes "convex S" "bounded S" "a \ rel_interior S" "convex T" "rel_frontier S \ T" "T \ affine hull S" + shows "(rel_frontier S) homotopy_eqv (T - {a})" + apply (rule rel_frontier_deformation_retract_of_punctured_convex [of S T]) + using assms + apply auto + apply (subst homotopy_eqv_sym) + using deformation_retract_imp_homotopy_eqv by blast + +lemma homotopy_eqv_rel_frontier_punctured_affine_hull: + fixes S :: "'a::euclidean_space set" + assumes "convex S" "bounded S" "a \ rel_interior S" + shows "(rel_frontier S) homotopy_eqv (affine hull S - {a})" +apply (rule homotopy_eqv_rel_frontier_punctured_convex) + using assms rel_frontier_affine_hull by force+ + lemma path_connected_sphere_gen: assumes "convex S" "bounded S" "aff_dim S \ 1" shows "path_connected(rel_frontier S)" diff -r 19f3d4af7a7d -r 6440577e34ee src/HOL/Analysis/Further_Topology.thy --- a/src/HOL/Analysis/Further_Topology.thy Thu Jan 05 14:18:24 2017 +0000 +++ b/src/HOL/Analysis/Further_Topology.thy Thu Jan 05 15:03:37 2017 +0000 @@ -2976,6 +2976,72 @@ by (simp add: aff_dim_cball) qed +lemma simply_connected_sphere_eq: + fixes a :: "'a::euclidean_space" + shows "simply_connected(sphere a r) \ 3 \ DIM('a) \ r \ 0" (is "?lhs = ?rhs") +proof (cases "r \ 0") + case True + have "simply_connected (sphere a r)" + apply (rule convex_imp_simply_connected) + using True less_eq_real_def by auto + with True show ?thesis by auto +next + case False + show ?thesis + proof + assume L: ?lhs + have "False" if "DIM('a) = 1 \ DIM('a) = 2" + using that + proof + assume "DIM('a) = 1" + with L show False + using connected_sphere_eq simply_connected_imp_connected + by (metis False Suc_1 not_less_eq_eq order_refl) + next + assume "DIM('a) = 2" + then have "sphere a r homeomorphic sphere (0::complex) 1" + by (metis DIM_complex False homeomorphic_spheres_gen not_less zero_less_one) + then have "simply_connected(sphere (0::complex) 1)" + using L homeomorphic_simply_connected_eq by blast + then obtain a::complex where "homotopic_with (\h. True) (sphere 0 1) (sphere 0 1) id (\x. a)" + apply (simp add: simply_connected_eq_contractible_circlemap) + by (metis continuous_on_id' id_apply image_id subset_refl) + then show False + 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) + next + assume ?rhs + with False show ?lhs by (simp add: simply_connected_sphere) + qed +qed + + +lemma simply_connected_punctured_universe_eq: + fixes a :: "'a::euclidean_space" + shows "simply_connected(- {a}) \ 3 \ DIM('a)" +proof - + have [simp]: "a \ rel_interior (cball a 1)" + by (simp add: rel_interior_nonempty_interior) + have [simp]: "affine hull cball a 1 - {a} = -{a}" + by (metis Compl_eq_Diff_UNIV aff_dim_cball aff_dim_lt_full not_less_iff_gr_or_eq zero_less_one) + have "simply_connected(- {a}) \ simply_connected(sphere a 1)" + apply (rule sym) + apply (rule homotopy_eqv_simple_connectedness) + using homotopy_eqv_rel_frontier_punctured_affine_hull [of "cball a 1" a] apply auto + done + also have "... \ 3 \ DIM('a)" + by (simp add: simply_connected_sphere_eq) + finally show ?thesis . +qed + +lemma not_simply_connected_circle: + fixes a :: complex + shows "0 < r \ \ simply_connected(sphere a r)" +by (simp add: simply_connected_sphere_eq) + subsection\The power, squaring and exponential functions as covering maps\ diff -r 19f3d4af7a7d -r 6440577e34ee src/HOL/Analysis/Homeomorphism.thy --- a/src/HOL/Analysis/Homeomorphism.thy Thu Jan 05 14:18:24 2017 +0000 +++ b/src/HOL/Analysis/Homeomorphism.thy Thu Jan 05 15:03:37 2017 +0000 @@ -8,6 +8,34 @@ imports Path_Connected begin +lemma homeomorphic_spheres': + fixes a ::"'a::euclidean_space" and b ::"'b::euclidean_space" + assumes "0 < \" and dimeq: "DIM('a) = DIM('b)" + shows "(sphere a \) homeomorphic (sphere b \)" +proof - + obtain f :: "'a\'b" and g where "linear f" "linear g" + and fg: "\x. norm(f x) = norm x" "\y. norm(g y) = norm y" "\x. g(f x) = x" "\y. f(g y) = y" + by (blast intro: isomorphisms_UNIV_UNIV [OF dimeq]) + then have "continuous_on UNIV f" "continuous_on UNIV g" + using linear_continuous_on linear_linear by blast+ + then show ?thesis + unfolding homeomorphic_minimal + apply(rule_tac x="\x. b + f(x - a)" in exI) + apply(rule_tac x="\x. a + g(x - b)" in exI) + using assms + apply (force intro: continuous_intros + continuous_on_compose2 [of _ f] continuous_on_compose2 [of _ g] simp: dist_commute dist_norm fg) + done +qed + +lemma homeomorphic_spheres_gen: + fixes a :: "'a::euclidean_space" and b :: "'b::euclidean_space" + assumes "0 < r" "0 < s" "DIM('a::euclidean_space) = DIM('b::euclidean_space)" + shows "(sphere a r homeomorphic sphere b s)" + apply (rule homeomorphic_trans [OF homeomorphic_spheres homeomorphic_spheres']) + using assms apply auto + done + subsection \Homeomorphism of all convex compact sets with nonempty interior\ proposition ray_to_rel_frontier: