theory Homotopy imports Path_Connected Product_Topology Uncountable_Sets begin
definition✐‹tag important› homotopic_with where "homotopic_with P X Y f g ≡ (∃h. continuous_map (prod_topology (top_of_set {0..1::real}) X) Y h ∧ (∀x. h(0, x) = f x) ∧ (∀x. h(1, x) = g x) ∧ (∀t ∈ {0..1}. P(λx. h(t,x))))"
text‹‹p›, ‹q› are functions ‹X → Y›, and the property ‹P› restricts all intermediate maps.
often just want to require that ‹P› fixes some subset, but to include the case of a loop homotopy,
is convenient to have a general property ‹P›.›
abbreviation homotopic_with_canon :: "[('a::topological_space → 'b::topological_space) → bool, 'a set, 'b set, 'a → 'b, 'a → 'b] → bool" where "homotopic_with_canon P S T p q ≡ homotopic_with P (top_of_set S) (top_of_set T) p q"
lemma split_01: "{0..1::real} = {0..1/2} ∪ {1/2..1}" by force
lemma split_01_prod: "{0..1::real} × X = ({0..1/2} × X) ∪ ({1/2..1} × X)" by force
lemma image_Pair_const: "(λx. (x, c)) ` A = A × {c}" by auto
lemma fst_o_paired [simp]: "fst ∘ (λ(x,y). (f x y, g x y)) = (λ(x,y). f x y)" by auto
lemma snd_o_paired [simp]: "snd ∘ (λ(x,y). (f x y, g x y)) = (λ(x,y). g x y)" by auto
lemma continuous_on_o_Pair: "[continuous_on (T × X) h; t ∈ T]==> continuous_on X (h ∘ Pair t)" by (fast intro: continuous_intros elim!: continuous_on_subset)
lemma continuous_map_o_Pair: assumes h: "continuous_map (prod_topology X Y) Z h"and t: "t ∈ topspace X" shows"continuous_map Y Z (h ∘ Pair t)" by (intro continuous_map_compose [OF _ h] continuous_intros; simp add: t)
text‹We often want to just localize the ending function equality or whatever.› text\<^marker>\<open>tagimportant\<close>\<open>%whitespace\<close> propositionhomotopic_with: assumes"\<And>hk.(\<And>x.x\<in>topspaceX\<Longrightarrow>hx=kx)\<Longrightarrow>(Ph\<longleftrightarrow>Pk)" shows"homotopic_withPXYpq\<longleftrightarrow> (\<exists>h.continuous_map(prod_topology(subtopologyeuclideanreal{0..1})X)Yh\<and> (\<forall>x\<in>topspaceX.h(0,x)=px)\<and> (\<forall>x\<in>topspaceX.h(1,x)=qx)\<and> (\<forall>t\<in>{0..1}.P(\<lambda>x.h(t,x))))" unfoldinghomotopic_with_def apply(ruleiffI,blast,clarify) apply(rule_tacx="\<lambda>(u,v).ifv\<in>topspaceXthenh(u,v)elseifu=0thenpvelseqv"inexI) applysimp by(smt(verit,best)SigmaEassmscase_prod_convcontinuous_map_eqtopspace_prod_topology)
definition\<^marker>\<open>tagimportant\<close>homotopic_paths::"['aset,real\<Rightarrow>'a,real\<Rightarrow>'a::topological_space]\<Rightarrow>bool" where "homotopic_pathsSpq\<equiv> homotopic_with_canon(\<lambda>r.pathstartr=pathstartp\<and>pathfinishr=pathfinishp){0..1}Spq"
lemmasimply_connected_eq_contractible_path: fixesS::"_::real_normed_vectorset" shows"simply_connectedS\<longleftrightarrow> path_connectedS\<and> (\<forall>p.pathp\<and>path_imagep\<subseteq>S\<and>pathfinishp=pathstartp \<longrightarrow>homotopic_pathsSp(linepath(pathstartp)(pathstartp)))" (is"?lhs=?rhs") proof assume?lhs thenshow?rhs unfoldingsimply_connected_imp_path_connected by(metissimply_connected_eq_contractible_loop_somehomotopic_loops_imp_homotopic_paths_null) next assume?rhs thenshow?lhs usinghomotopic_paths_imp_homotopic_loopssimply_connected_eq_contractible_loop_somebyfastforce qed
lemmasimply_connected_eq_homotopic_paths: fixesS::"_::real_normed_vectorset" shows"simply_connectedS\<longleftrightarrow> path_connectedS\<and> (\<forall>pq.pathp\<and>path_imagep\<subseteq>S\<and> pathq\<and>path_imageq\<subseteq>S\<and> pathstartq=pathstartp\<and>pathfinishq=pathfinishp \<longrightarrow>homotopic_pathsSpq)" (is"?lhs=?rhs") proof assume?lhs thenhavepc:"path_connectedS" and*:"\<And>p.\<lbrakk>pathp;path_imagep\<subseteq>S; pathfinishp=pathstartp\<rbrakk> \<Longrightarrow>homotopic_pathsSp(linepath(pathstartp)(pathstartp))" by(autosimp:simply_connected_eq_contractible_path) have"homotopic_pathsSpq" if"pathp""path_imagep\<subseteq>S""pathq" "path_imageq\<subseteq>S""pathstartq=pathstartp" "pathfinishq=pathfinishp"forpq proof- have"homotopic_pathsSp(p+++reversepathq+++q)" usingthat by(smt(verit,best)homotopic_paths_joinhomotopic_paths_linvhomotopic_paths_ridhomotopic_paths_sym homotopic_paths_transpathstart_linepath) alsohave"homotopic_pathsS\<dots>((p+++reversepathq)+++q)" by(simpadd:thathomotopic_paths_assoc) alsohave"homotopic_pathsS\<dots>(linepath(pathstartq)(pathstartq)+++q)" using*[of"p+++reversepathq"]that by(simpadd:homotopic_paths_assochomotopic_paths_joinpath_image_join) alsohave"homotopic_pathsS\<dots>q" usingthathomotopic_paths_lidbyblast finallyshow?thesis. qed thenshow?rhs
by (blast intro: pc *) next assume ?rhs thenshow ?lhs by (force simp: simply_connected_eq_contractible_path) qed
proposition simply_connected_Times: fixes S :: "'a::real_normed_vector set"and T :: "'b::real_normed_vector set" assumes S: "simply_connected S"and T: "simply_connected T" shows"simply_connected(S × T)" proof - have"homotopic_loops (S × T) p (linepath (a, b) (a, b))" if"path p""path_image p ⊆ S × T""p 1 = p 0""a ∈ S""b ∈ T" for p a b proof - have"path (fst ∘ p)" by (simp add: continuous_on_fst Path_Connected.path_continuous_image [OF ‹path p›]) moreoverhave"path_image (fst ∘ p) ⊆ S" using that by (force simp: path_image_def) ultimatelyhave p1: "homotopic_loops S (fst ∘ p) (linepath a a)" using S that by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def) have"path (snd ∘ p)" by (simp add: continuous_on_snd Path_Connected.path_continuous_image [OF ‹path p›]) moreoverhave"path_image (snd ∘ p) ⊆ T" using that by (force simp: path_image_def) ultimatelyhave p2: "homotopic_loops T (snd ∘ p) (linepath b b)" using T that by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def) show ?thesis using p1 p2 unfolding homotopic_loops apply clarify subgoalfor h k by (rule_tac x="λz. (h z, k z)"in exI) (auto intro: continuous_intros simp: path_defs) done qed with assms show ?thesis by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def) qed
subsection‹Contractible sets›
definition✐‹tag important› contractible where "contractible S ≡∃a. homotopic_with_canon (λx. True) S S id (λx. a)"
proposition contractible_imp_simply_connected: fixes S :: "_::real_normed_vector set" assumes"contractible S"shows"simply_connected S" proof (cases "S = {}") case True thenshow ?thesis by force next case False obtain a where a: "homotopic_with_canon (λx. True) S S id (λx. a)" using assms by (force simp: contractible_def) thenhave"a ∈ S" using False homotopic_with_imp_funspace2 by fastforce have"∀p. path p ∧ path_image p ⊆ S ∧ pathfinish p = pathstart p ⟶ homotopic_loops S p (linepath a a)" using a apply (clarsimp simp: homotopic_loops_def homotopic_with_def path_defs) apply (rule_tac x="(h ∘ (λy. (fst y, (p ∘ snd) y)))"in exI) apply (intro conjI continuous_on_compose continuous_intros; force elim: continuous_on_subset) done with‹a ∈ S›show ?thesis by (auto simp: simply_connected_eq_contractible_loop_all False) qed
corollary contractible_imp_connected: fixes S :: "_::real_normed_vector set" shows"contractible S ==> connected S" by (simp add: contractible_imp_simply_connected simply_connected_imp_connected)
lemma contractible_imp_path_connected: fixes S :: "_::real_normed_vector set" shows"contractible S ==> path_connected S" by (simp add: contractible_imp_simply_connected simply_connected_imp_path_connected)
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" 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 b continuous_map_subtopology_eu g homotopic_with_compose_continuous_map_left image_subset_iff_funcset) thenhave"homotopic_with_canon (λf. True) S U (g ∘ id ∘ f) (g ∘ (λx. b) ∘ f)" by (simp add: f homotopic_with_compose_continuous_map_right image_subset_iff_funcset) thenshow ?thesis by (simp add: comp_def that) qed
lemma nullhomotopic_into_contractible: 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" 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" "contractible T""path_connected U" shows"homotopic_with_canon (λh. True) S U (g1 ∘ f1) (g2 ∘ f2)" proof - obtain c1 where c1: "homotopic_with_canon (λh. True) S U (g1 ∘ f1) (λx. c1)" by (rule nullhomotopic_through_contractible [of S f1 T g1 U]) (use assms in auto) obtain c2 where c2: "homotopic_with_canon (λh. True) S U (g2 ∘ f2) (λx. c2)" by (rule nullhomotopic_through_contractible [of S f2 T g2 U]) (use assms in auto) have"S = {} ∨ (∃t. path_connected t ∧ t ⊆ U ∧ c2 ∈ t ∧ c1 ∈ t)" proof (cases "S = {}") case True thenshow ?thesis by force next case False with c1 c2 have"c1 ∈ U""c2 ∈ U" using homotopic_with_imp_continuous_maps by (metis PiE equals0I homotopic_with_imp_funspace2)+ with‹path_connected U›show ?thesis by blast qed thenhave"homotopic_with_canon (λh. True) S U (λx. c2) (λx. c1)" by (auto simp: path_component homotopic_constant_maps) thenshow ?thesis using c1 c2 homotopic_with_symD homotopic_with_trans by blast qed
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" 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] by (simp add: assms contractible_imp_path_connected)
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" 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] by (simp add: assms contractible_imp_path_connected)
subsection‹Starlike sets›
definition✐‹tag important›"starlike S ⟷ (∃a∈S. ∀x∈S. closed_segment a x ⊆ S)"
lemma starlike_UNIV [simp]: "starlike UNIV" by (simp add: starlike_def)
lemma convex_imp_starlike: "convex S ==> S ≠ {} ==> starlike S" unfolding convex_contains_segment starlike_def by auto
lemma starlike_convex_tweak_boundary_points: fixes S :: "'a::euclidean_space set" assumes"convex S""S ≠ {}"and ST: "rel_interior S ⊆ T"and TS: "T ⊆ closure S" shows"starlike T" proof - have"rel_interior S ≠ {}" by (simp add: assms rel_interior_eq_empty) with ST obtain a where a: "a ∈ rel_interior S"and"a ∈ T"by blast have"∧x. x ∈ T ==> open_segment a x ⊆ rel_interior S" by (rule rel_interior_closure_convex_segment [OF ‹convex S› a]) (use assms in auto) thenhave"∀x∈T. a ∈ T ∧ open_segment a x ⊆ T" using ST by (blast intro: a ‹a ∈ T› rel_interior_closure_convex_segment [OF ‹convex S› a]) thenshow ?thesis unfolding starlike_def using bexI [OF _ ‹a ∈ T›] by (simp add: closed_segment_eq_open) qed
lemma starlike_imp_contractible_gen: fixes S :: "'a::real_normed_vector set" assumes S: "starlike S" and P: "∧a T. [a ∈ S; 0 ≤ T; T ≤ 1]==> P(λx. (1 - T) *R x + T *R a)" obtains a where"homotopic_with_canon P S S (λx. x) (λx. a)" proof - obtain a where"a ∈ S"and a: "∧x. x ∈ S ==> closed_segment a x ⊆ S" using S by (auto simp: starlike_def) have"∧t b. 0 ≤ t ∧ t ≤ 1 ==> ∃u. (1 - t) *R b + t *R a = (1 - u) *R a + u *R b ∧ 0 ≤ u ∧ u ≤ 1" by (metis add_diff_cancel_right' diff_ge_0_iff_ge le_add_diff_inverse pth_c(1)) thenhave"(λy. (1 - fst y) *R snd y + fst y *R a) ` ({0..1} × S) ⊆ S" using a [unfolded closed_segment_def] by force thenhave"homotopic_with_canon P S S (λx. x) (λx. a)" using‹a ∈ S› unfolding homotopic_with_def apply (rule_tac x="λy. (1 - (fst y)) *R snd y + (fst y) *R a"in exI) apply (force simp: P intro: continuous_intros) done thenshow ?thesis using that by blast qed
lemma starlike_imp_contractible: fixes S :: "'a::real_normed_vector set" shows"starlike S ==> contractible S" using starlike_imp_contractible_gen contractible_def by (fastforce simp: id_def)
lemma starlike_imp_simply_connected: fixes S :: "'a::real_normed_vector set" shows"starlike S ==> simply_connected S" by (simp add: contractible_imp_simply_connected starlike_imp_contractible)
lemma convex_imp_simply_connected: fixes S :: "'a::real_normed_vector set" shows"convex S ==> simply_connected S" using convex_imp_starlike starlike_imp_simply_connected by blast
lemma starlike_imp_path_connected: fixes S :: "'a::real_normed_vector set" shows"starlike S ==> path_connected S" by (simp add: simply_connected_imp_path_connected starlike_imp_simply_connected)
lemma starlike_imp_connected: fixes S :: "'a::real_normed_vector set" shows"starlike S ==> connected S" by (simp add: path_connected_imp_connected starlike_imp_path_connected)
lemma is_interval_simply_connected_1: fixes S :: "real set" shows"is_interval S ⟷ simply_connected S" by (meson convex_imp_simply_connected is_interval_connected_1 is_interval_convex_1 simply_connected_imp_connected)
lemma complex_slot_left_eq: "complex_of_real ` {..c} = {z. Re z ≤ c ∧ Im z = 0}" by (auto simp: image_iff complex_eq_iff)
lemma complex_slot_right_eq: "complex_of_real ` {c..} = {z. Re z ≥ c ∧ Im z = 0}" by (auto simp: image_iff complex_eq_iff)
lemma complex_double_slot_eq: "complex_of_real ` ({..c1} ∪ {c2..}) = {z. Im z = 0 ∧ (Re z ≤ c1 ∨ Re z ≥ c2)}" by (auto simp: image_iff complex_eq_iff)
lemma starlike_slotted_complex_plane_left_aux: assumes z: "z ∈ -(complex_of_real ` {..c})"and c: "c < c'" shows"closed_segment (complex_of_real c') z ⊆ -(complex_of_real ` {..c})" proof - show"closed_segment c' z ⊆ -of_real ` {..c}" proof (cases "Im z = 0") case True thus ?thesis using z c by (auto simp: closed_segment_same_Im closed_segment_eq_real_ivl complex_slot_left_eq) next case False show ?thesis proof fix x assume x: "x ∈ closed_segment (of_real c') z"
consider "x = of_real c'" | "x = z" | "x ∈ open_segment (of_real c') z" unfolding open_segment_def using x by blast thus"x ∈ -complex_of_real ` {..c}" proof cases assume"x ∈ open_segment (of_real c') z" hence"Im x ∈ open_segment (Im (complex_of_real c')) (Im z)" by (intro in_open_segment_imp_Im_in_open_segment) (use False in auto) hence"Im x ≠ 0" by (auto simp: open_segment_eq_real_ivl split: if_splits) thus ?thesis by (auto simp: complex_slot_right_eq) qed (use z c in‹auto simp: complex_slot_left_eq›) qed qed qed
lemma starlike_slotted_complex_plane_left: "starlike (-(complex_of_real ` {..c}))" unfolding starlike_def proof (rule bexI[of _ "of_real c + 1"]; (intro ballI)?) show"complex_of_real c + 1 ∈ -complex_of_real ` {..c}" by (auto simp: complex_eq_iff) show"closed_segment (complex_of_real c + 1) z ⊆ - complex_of_real ` {..c}" if"z ∈ - complex_of_real ` {..c}"for z using starlike_slotted_complex_plane_left_aux[OF that, of "c + 1"] by simp qed
lemma starlike_slotted_complex_plane_right_aux: assumes z: "z ∈ -(complex_of_real ` {c..})"and c: "c > c'" shows"closed_segment (complex_of_real c') z ⊆ -(complex_of_real ` {c..})" proof - show"closed_segment c' z ⊆ -of_real ` {c..}" proof (cases "Im z = 0") case True thus ?thesis using z c by (auto simp: closed_segment_same_Im closed_segment_eq_real_ivl complex_slot_right_eq) next case False show ?thesis proof fix x assume x: "x ∈ closed_segment (of_real c') z"
consider "x = of_real c'" | "x = z" | "x ∈ open_segment (of_real c') z" unfolding open_segment_def using x by blast thus"x ∈ -complex_of_real ` {c..}" proof cases assume"x ∈ open_segment (of_real c') z" hence"Im x ∈ open_segment (Im (complex_of_real c')) (Im z)" by (intro in_open_segment_imp_Im_in_open_segment) (use False in auto) hence"Im x ≠ 0" by (auto simp: open_segment_eq_real_ivl split: if_splits) thus ?thesis by (auto simp: complex_slot_right_eq) qed (use z c in‹auto simp: complex_slot_right_eq›) qed qed qed
lemma starlike_slotted_complex_plane_right: "starlike (-(complex_of_real ` {c..}))" unfolding starlike_def proof (rule bexI[of _ "of_real c - 1"]; (intro ballI)?) show"complex_of_real c - 1 ∈ -complex_of_real ` {c..}" by (auto simp: complex_eq_iff) show"closed_segment (complex_of_real c - 1) z ⊆ - complex_of_real ` {c..}" if"z ∈ - complex_of_real ` {c..}"for z using starlike_slotted_complex_plane_right_aux[OF that, of "c - 1"] by simp qed
lemma starlike_doubly_slotted_complex_plane_aux: assumes z: "z ∈ -(complex_of_real ` ({..c1} ∪ {c2..}))"and c: "c1 < c""c < c2" shows"closed_segment (complex_of_real c) z ⊆ -(complex_of_real ` ({..c1} ∪ {c2..}))" proof - show"closed_segment c z ⊆ -of_real ` ({..c1} ∪ {c2..})" proof (cases "Im z = 0") case True thus ?thesis using z c by (auto simp: closed_segment_same_Im closed_segment_eq_real_ivl complex_double_slot_eq) next case False show ?thesis proof fix x assume x: "x ∈ closed_segment (of_real c) z"
consider "x = of_real c" | "x = z" | "x ∈ open_segment (of_real c) z" unfolding open_segment_def using x by blast thus"x ∈ -complex_of_real ` ({..c1} ∪ {c2..})" proof cases assume"x ∈ open_segment (of_real c) z" hence"Im x ∈ open_segment (Im (complex_of_real c)) (Im z)" by (intro in_open_segment_imp_Im_in_open_segment) (use False in auto) hence"Im x ≠ 0" by (auto simp: open_segment_eq_real_ivl split: if_splits) thus ?thesis by (auto simp: complex_slot_right_eq) qed (use z c in‹auto simp: complex_slot_right_eq›) qed qed qed
lemma starlike_doubly_slotted_complex_plane: assumes"c1 < c2" shows"starlike (-(complex_of_real ` ({..c1} ∪ {c2..})))" proof - from assms obtain c where c: "c1 < c""c < c2" using dense by blast show ?thesis unfolding starlike_def proof (rule bexI[of _ "of_real c"]; (intro ballI)?) show"complex_of_real c ∈ -complex_of_real ` ({..c1} ∪ {c2..})" using c by (auto simp: complex_eq_iff) show"closed_segment (complex_of_real c) z ⊆ - complex_of_real ` ({..c1} ∪ {c2..})" if"z ∈ - complex_of_real ` ({..c1} ∪ {c2..})"for z using starlike_doubly_slotted_complex_plane_aux[OF that, of c] c by simp qed qed
lemma simply_connected_slotted_complex_plane_left: "simply_connected (-(complex_of_real ` {..c}))" by (intro starlike_imp_simply_connected starlike_slotted_complex_plane_left)
lemma simply_connected_slotted_complex_plane_right: "simply_connected (-(complex_of_real ` {c..}))" by (intro starlike_imp_simply_connected starlike_slotted_complex_plane_right)
lemma contractible_empty [simp]: "contractible {}" by (simp add: contractible_def homotopic_on_emptyI)
lemma contractible_convex_tweak_boundary_points: fixes S :: "'a::euclidean_space set" assumes"convex S"and TS: "rel_interior S ⊆ T""T ⊆ closure S" shows"contractible T" by (metis assms closure_eq_empty contractible_empty empty_subsetI
starlike_convex_tweak_boundary_points starlike_imp_contractible subset_antisym)
lemma convex_imp_contractible: fixes S :: "'a::real_normed_vector set" shows"convex S ==> contractible S" using contractible_empty convex_imp_starlike starlike_imp_contractible by blast
lemma contractible_sing [simp]: fixes a :: "'a::real_normed_vector" shows"contractible {a}" by (rule convex_imp_contractible [OF convex_singleton])
lemma is_interval_contractible_1: fixes S :: "real set" shows"is_interval S ⟷ contractible S" using contractible_imp_simply_connected convex_imp_contractible is_interval_convex_1
is_interval_simply_connected_1 by auto
lemma contractible_Times: fixes S :: "'a::euclidean_space set"and T :: "'b::euclidean_space set" assumes S: "contractible S"and T: "contractible T" shows"contractible (S × T)" proof - obtain a h where conth: "continuous_on ({0..1} × S) h" 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 (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 [simp]: "∧x. x ∈ T ==> k (0, x) = x" and [simp]: "∧x. x ∈ T ==> k (1::real, x) = b" using T by (force simp: contractible_def homotopic_with) show ?thesis apply (simp add: contractible_def homotopic_with) apply (rule exI [where x=a]) apply (rule exI [where x=b]) apply (rule exI [where x = "λz. (h (fst z, fst(snd z)), k (fst z, snd(snd z)))"]) using hsub ksub apply (fastforce intro!: continuous_intros continuous_on_compose2 [OF conth] continuous_on_compose2 [OF contk]) done qed
subsection‹Local versions of topological properties in general›
definition✐‹tag important› locally :: "('a::topological_space set → bool) → 'a set →bool" where "locally P S ≡ ∀w x. openin (top_of_set S) w ∧ x ∈ w ⟶ (∃U V. openin (top_of_set S) U ∧ P V ∧ x ∈ U ∧ U ⊆ V ∧ V ⊆ w)"
lemma locallyI: assumes"∧w x. [openin (top_of_set S) w; x ∈ w] ==>∃U V. openin (top_of_set S) U ∧ P V ∧ x ∈ U ∧ U ⊆ V ∧ V ⊆ w" shows"locally P S" using assms by (force simp: locally_def)
lemma locallyE: assumes"locally P S""openin (top_of_set S) w""x ∈ w" obtains U V where"openin (top_of_set S) U""P V""x ∈ U""U ⊆ V""V ⊆ w" using assms unfolding locally_def by meson
lemma locally_mono: assumes"locally P S""∧T. P T ==> Q T" shows"locally Q S" by (metis assms locally_def)
lemma locally_open_subset: assumes"locally P S""openin (top_of_set S) t" shows"locally P t" by (smt (verit, ccfv_SIG) assms order.trans locally_def openin_imp_subset openin_subset_trans openin_trans)
lemma locally_diff_closed: "[locally P S; closedin (top_of_set S) t]==> locally P (S - t)" using locally_open_subset closedin_def by fastforce
lemma locally_empty [iff]: "locally P {}" by (simp add: locally_def openin_subtopology)
lemma locally_singleton [iff]: fixes a :: "'a::metric_space" shows"locally P {a} ⟷ P {a}" proof - have"∀x::real. ¬ 0 < x ==> P {a}" using zero_less_one by blast thenshow ?thesis unfolding locally_def by (auto simp: openin_euclidean_subtopology_iff subset_singleton_iff conj_disj_distribR) qed
lemma locally_iff: "locally P S ⟷ (∀T x. open T ∧ x ∈ S ∩ T ⟶ (∃U. open U ∧ (∃V. P V ∧ x ∈ S ∩ U ∧ S ∩ U ⊆ V ∧ V ⊆ S ∩ T)))" by (smt (verit) locally_def openin_open)
lemma locally_Int: assumes S: "locally P S"and T: "locally P T" and P: "∧S T. P S ∧ P T ==> P(S ∩ T)" shows"locally P (S ∩ T)" unfolding locally_iff proof clarify fix A x assume"open A""x ∈ A""x ∈ S""x ∈ T" thenobtain U1 V1 U2 V2 where"open U1""P V1""x ∈ S ∩ U1""S ∩ U1 ⊆ V1 ∧ V1 ⊆ S ∩ A" "open U2""P V2""x ∈ T ∩ U2""T ∩ U2 ⊆ V2 ∧ V2 ⊆ T ∩ A" using S T unfolding locally_iff by (meson IntI) thenhave"S ∩ T ∩ (U1 ∩ U2) ⊆ V1 ∩ V2""V1 ∩ V2 ⊆ S ∩ T ∩ A""x ∈ S ∩ T ∩ (U1 ∩ U2)" by blast+ moreoverhave"P (V1 ∩ V2)" by (simp add: P ‹P V1›‹P V2›) ultimatelyshow"∃U. open U ∧ (∃V. P V ∧ x ∈ S ∩ T ∩ U ∧ S ∩ T ∩ U ⊆ V ∧ V ⊆ S ∩ T∩ A)" using‹open U1›‹open U2›by blast qed
lemma locally_Times: fixes S :: "('a::metric_space) set"and T :: "('b::metric_space) set" assumes PS: "locally P S"and QT: "locally Q T"and R: "∧S T. P S ∧ Q T ==> R(S × T)" shows"locally R (S × T)" unfolding locally_def proof (clarify) fix W x y assume W: "openin (top_of_set (S × T)) W"and xy: "(x, y) ∈ W" thenobtain U V where"openin (top_of_set S) U""x ∈ U" "openin (top_of_set T) V""y ∈ V""U × V ⊆ W" using Times_in_interior_subtopology by metis thenobtain U1 U2 V1 V2 where opeS: "openin (top_of_set S) U1 ∧ P U2 ∧ x ∈ U1 ∧ U1 ⊆ U2 ∧ U2 ⊆ U" and opeT: "openin (top_of_set T) V1 ∧ Q V2 ∧ y ∈ V1 ∧ V1 ⊆ V2 ∧ V2 ⊆ V" by (meson PS QT locallyE) thenhave"openin (top_of_set (S × T)) (U1 × V1)" by (simp add: openin_Times) moreoverhave"R (U2 × V2)" by (simp add: R opeS opeT) moreoverhave"U1 × V1 ⊆ U2 × V2 ∧ U2 × V2 ⊆ W" using opeS opeT ‹U × V ⊆ W›by auto ultimatelyshow"∃U V. openin (top_of_set (S × T)) U ∧ R V ∧ (x,y) ∈ U ∧ U ⊆ V ∧ V⊆ W" using opeS opeT by auto qed
proposition homeomorphism_locally_imp: fixes S :: "'a::metric_space set"and T :: "'b::t2_space set" assumes S: "locally P S"and hom: "homeomorphism S T f g" and Q: "∧S S'. [P S; homeomorphism S S' f g]==> Q S'" shows"locally Q T" proof (clarsimp simp: locally_def) fix W y assume"y ∈ W"and"openin (top_of_set T) W" thenobtain A where T: "open A""W = T ∩ A" by (force simp: openin_open) thenhave"W ⊆ T"by auto have f: "∧x. x ∈ S ==> g(f x) = x""f ` S = T""continuous_on S f" and g: "∧y. y ∈ T ==> f(g y) = y""g ` T = S""continuous_on T g" using hom by (auto simp: homeomorphism_def) have gw: "g ` W = S ∩ f -` W" using‹W ⊆ T› g by force have"openin (top_of_set S) (g ` W)" using‹openin (top_of_set T) W› continuous_on_open f gw by auto thenobtain U V where osu: "openin (top_of_set S) U"and uv: "P V""g y ∈ U""U ⊆ V""V ⊆ g ` W" by (metis S ‹y ∈ W› image_eqI locallyE) have"V ⊆ S"using uv by (simp add: gw) have fv: "f ` V = T ∩ {x. g x ∈ V}" using‹f ` S = T› f ‹V ⊆ S›by auto have contvf: "continuous_on V f" using‹V ⊆ S› continuous_on_subset f(3) by blast have"openin (top_of_set (g ` T)) U" using‹g ` T = S›by (simp add: osu) thenhave"openin (top_of_set T) (T ∩ g -` U)" using‹continuous_on T g› continuous_on_open [THEN iffD1] by blast moreoverhave"∃V. Q V ∧ y ∈ (T ∩ g -` U) ∧ (T ∩ g -` U) ⊆ V ∧ V ⊆ W" proof (intro exI conjI) show"f ` V ⊆ W" using uv using Int_lower2 gw image_subsetI mem_Collect_eq subset_iff by auto thenhave contvg: "continuous_on (f ` V) g" using‹W ⊆ T› continuous_on_subset [OF g(3)] by blast have"V ⊆ g ` f ` V" by (metis ‹V ⊆ S› hom homeomorphism_def homeomorphism_of_subsets order_refl) thenhave homv: "homeomorphism V (f ` V) f g" using‹V ⊆ S› f by (auto simp: homeomorphism_def contvf contvg) show"Q (f ` V)" using Q homv ‹P V›by blast show"y ∈ T ∩ g -` U" using T(2) ‹y ∈ W›‹g y ∈ U›by blast show"T ∩ g -` U ⊆ f ` V" using g(1) image_iff uv(3) by fastforce qed ultimatelyshow"∃U. openin (top_of_set T) U ∧ (∃v. Q v ∧ y ∈ U ∧ U ⊆ v ∧ v ⊆ W)" by meson qed
lemma homeomorphism_locally: fixes f:: "'a::metric_space → 'b::metric_space" assumes"homeomorphism S T f g" and"∧S T. homeomorphism S T f g ==> (P S ⟷ Q T)" shows"locally P S ⟷ locally Q T" by (smt (verit) assms homeomorphism_locally_imp homeomorphism_symD)
lemma homeomorphic_locally: fixes S:: "'a::metric_space set"and T:: "'b::metric_space set" assumes hom: "S homeomorphic T" and iff: "∧X Y. X homeomorphic Y ==> (P X ⟷ Q Y)" shows"locally P S ⟷ locally Q T" by (smt (verit, ccfv_SIG) hom homeomorphic_def homeomorphism_locally homeomorphism_locally_imp iff)
lemma homeomorphic_local_compactness: fixes S:: "'a::metric_space set"and T:: "'b::metric_space set" shows"S homeomorphic T ==> locally compact S ⟷ locally compact T" by (simp add: homeomorphic_compactness homeomorphic_locally)
lemma locally_translation: fixes P :: "'a :: real_normed_vector set → bool" shows"(∧S. P ((+) a ` S) = P S) ==> locally P ((+) a ` S) = locally P S" using homeomorphism_locally [OF homeomorphism_translation] by (metis (full_types) homeomorphism_image2)
lemma locally_injective_linear_image: fixes f :: "'a::euclidean_space → 'b::euclidean_space" assumes f: "linear f""inj f"and iff: "∧S. P (f ` S) ⟷ Q S" shows"locally P (f ` S) ⟷ locally Q S" by (smt (verit) f homeomorphism_image2 homeomorphism_locally iff linear_homeomorphism_image)
lemma locally_open_map_image: fixes f :: "'a::real_normed_vector → 'b::real_normed_vector" assumes P: "locally P S" and f: "continuous_on S f" and oo: "∧T. openin (top_of_set S) T ==> openin (top_of_set (f ` S)) (f ` T)" and Q: "∧T. [T ⊆ S; P T]==> Q(f ` T)" shows"locally Q (f ` S)" proof (clarsimp simp: locally_def) fix W y assume oiw: "openin (top_of_set (f ` S)) W"and"y ∈ W" thenhave"W ⊆ f ` S"by (simp add: openin_euclidean_subtopology_iff) have oivf: "openin (top_of_set S) (S ∩ f -` W)" by (rule continuous_on_open [THEN iffD1, rule_format, OF f oiw]) thenobtain x where"x ∈ S""f x = y" using‹W ⊆ f ` S›‹y ∈ W›by blast thenobtain U V where"openin (top_of_set S) U""P V""x ∈ U""U ⊆ V""V ⊆ S ∩ f -` W" by (metis IntI P ‹y ∈ W› locallyE oivf vimageI) thenhave"openin (top_of_set (f ` S)) (f ` U)" by (simp add: oo) thenshow"∃X. openin (top_of_set (f ` S)) X ∧ (∃Y. Q Y ∧ y ∈ X ∧ X ⊆ Y ∧ Y ⊆ W)" using Q ‹P V›‹U ⊆ V›‹V ⊆ S ∩ f -` W›‹f x = y›‹x ∈ U›by blast qed
subsection‹An induction principle for connected sets›
proposition connected_induction: assumes"connected S" and opD: "∧T a. [openin (top_of_set S) T; a ∈ T]==>∃z. z ∈ T ∧ P z" and opI: "∧a. a ∈ S ==>∃T. openin (top_of_set S) T ∧ a ∈ T ∧ (∀x ∈ T. ∀y ∈ T. P x ∧ P y ∧ Q x ⟶ Q y)" and etc: "a ∈ S""b ∈ S""P a""P b""Q a" shows"Q b" proof - let ?A = "{b. ∃T. openin (top_of_set S) T ∧ b ∈ T ∧ (∀x∈T. P x ⟶ Q x)}" let ?B = "{b. ∃T. openin (top_of_set S) T ∧ b ∈ T ∧ (∀x∈T. P x ⟶¬ Q x)}" have"?A ∩ ?B = {}" by (clarsimp simp: set_eq_iff) (metis (no_types, opaque_lifting) Int_iff opD openin_Int) moreoverhave"S ⊆ ?A ∪ ?B" by clarsimp (meson opI) moreoverhave"openin (top_of_set S) ?A" by (subst openin_subopen, blast) moreoverhave"openin (top_of_set S) ?B" by (subst openin_subopen, blast) ultimatelyhave"?A = {} ∨ ?B = {}" by (metis (no_types, lifting) ‹connected S› connected_openin) thenshow ?thesis by clarsimp (meson opI etc) qed
lemma connected_equivalence_relation_gen: assumes"connected S" and etc: "a ∈ S""b ∈ S""P a""P b" and trans: "∧x y z. [R x y; R y z]==> R x z" and opD: "∧T a. [openin (top_of_set S) T; a ∈ T]==>∃z. z ∈ T ∧ P z" and opI: "∧a. a ∈ S ==>∃T. openin (top_of_set S) T ∧ a ∈ T ∧ (∀x ∈ T. ∀y ∈ T. P x ∧ P y ⟶ R x y)" shows"R a b" proof - have"∧a b c. [a ∈ S; P a; b ∈ S; c ∈ S; P b; P c; R a b]==> R a c" apply (rule connected_induction [OF ‹connected S› opD], simp_all) by (meson trans opI) thenshow ?thesis by (metis etc opI) qed
lemma connected_induction_simple: assumes"connected S" and etc: "a ∈ S""b ∈ S""P a" and opI: "∧a. a ∈ S ==>∃T. openin (top_of_set S) T ∧ a ∈ T ∧ (∀x ∈ T. ∀y ∈ T. P x ⟶ P y)" shows"P b" by (rule connected_induction [OF ‹connected S› _, where P = "λx. True"])
(use opI etc in auto)
lemma connected_equivalence_relation: assumes"connected S" and etc: "a ∈ S""b ∈ S" and sym: "∧x y. [R x y; x ∈ S; y ∈ S]==> R y x" and trans: "∧x y z. [R x y; R y z; x ∈ S; y ∈ S; z ∈ S]==> R x z" and opI: "∧a. a ∈ S ==>∃T. openin (top_of_set S) T ∧ a ∈ T ∧ (∀x ∈ T. R a x)" shows"R a b" proof - have"∧a b c. [a ∈ S; b ∈ S; c ∈ S; R a b]==> R a c" by (smt (verit, ccfv_threshold) connected_induction_simple [OF ‹connected S›]
assms openin_imp_subset subset_eq) thenshow ?thesis by (metis etc opI) qed
lemma locally_constant_imp_constant: assumes"connected S" and opI: "∧a. a ∈ S ==>∃T. openin (top_of_set S) T ∧ a ∈ T ∧ (∀x ∈ T. f x = f a)" shows"f constant_on S" proof - have"∧x y. x ∈ S ==> y ∈ S ==> f x = f y" apply (rule connected_equivalence_relation [OF ‹connected S›], simp_all) by (metis opI) thenshow ?thesis by (metis constant_on_def) qed
lemma locally_constant: assumes"connected S" shows"locally (λU. f constant_on U) S ⟷ f constant_on S" (is"?lhs = ?rhs") proof assume ?lhs thenshow ?rhs by (smt (verit, del_insts) assms constant_on_def locally_constant_imp_constant locally_def openin_subtopology_self subset_iff) next assume ?rhs thenshow ?lhs by (metis constant_on_subset locallyI openin_imp_subset order_refl) qed
subsection‹Basic properties of local compactness›
proposition locally_compact: fixes S :: "'a :: metric_space set" shows "locally compact S ⟷ (∀x ∈ S. ∃u v. x ∈ u ∧ u ⊆ v ∧ v ⊆ S ∧ openin (top_of_set S) u ∧ compact v)"
(is"?lhs = ?rhs") proof assume ?lhs thenshow ?rhs by (meson locallyE openin_subtopology_self) next assume r [rule_format]: ?rhs have *: "∃u v. openin (top_of_set S) u ∧ compact v ∧ x ∈ u ∧ u ⊆ v ∧ v ⊆ S ∩ T" if"open T""x ∈ S""x ∈ T"for x T proof - obtain U V where uv: "x ∈ U""U ⊆ V""V ⊆ S""compact V""openin (top_of_set S) U" using r [OF ‹x ∈ S›] by auto obtain e where"e>0"and e: "cball x e ⊆ T" using open_contains_cball ‹open T›‹x ∈ T›by blast show ?thesis apply (rule_tac x="(S ∩ ball x e) ∩ U"in exI) apply (rule_tac x="cball x e ∩ V"in exI) using that ‹e > 0› e uv apply auto done qed show ?lhs by (rule locallyI) (metis "*" Int_iff openin_open) qed
lemma locally_compactE: fixes S :: "'a :: metric_space set" assumes"locally compact S" obtains u v where"∧x. x ∈ S ==> x ∈ u x ∧ u x ⊆ v x ∧ v x ⊆ S ∧ openin (top_of_set S) (u x) ∧ compact (v x)" using assms unfolding locally_compact by metis
lemma locally_compact_alt: fixes S :: "'a :: heine_borel set" shows"locally compact S ⟷ (∀x ∈ S. ∃U. x ∈ U ∧ openin (top_of_set S) U ∧ compact(closure U) ∧ closure U ⊆ S)" by (smt (verit, ccfv_threshold) bounded_subset closure_closed closure_mono closure_subset
compact_closure compact_imp_closed order.trans locally_compact)
lemma locally_compact_Int_cball: fixes S :: "'a :: heine_borel set" shows"locally compact S ⟷ (∀x ∈ S. ∃e. 0 < e ∧ closed(cball x e ∩ S))"
(is"?lhs = ?rhs") proof assume L: ?lhs thenhave"∧x U V e. [U ⊆ V; V ⊆ S; compact V; 0 < e; cball x e ∩ S ⊆ U] ==> closed (cball x e ∩ S)" by (metis compact_Int compact_cball compact_imp_closed inf.absorb_iff2 inf.assoc inf.orderE) with L show ?rhs by (meson locally_compactE openin_contains_cball) next assume R: ?rhs show ?lhs unfolding locally_compact proof fix x assume"x ∈ S" thenobtain e where"e>0"and"compact (cball x e ∩ S)" by (metis Int_commute compact_Int_closed compact_cball inf.right_idem R) moreoverhave"∀y∈ball x e ∩ S. ∃ε>0. cball y ε ∩ S ⊆ ball x e" by (meson Elementary_Metric_Spaces.open_ball IntD1 le_infI1 open_contains_cball_eq) moreoverhave"openin (top_of_set S) (ball x e ∩ S)" by (simp add: inf_commute openin_open_Int) ultimatelyshow"∃U V. x ∈ U ∧ U ⊆ V ∧ V ⊆ S ∧ openin (top_of_set S) U ∧ compact V" by (metis Int_iff ‹0 < e›‹x ∈ S› ball_subset_cball centre_in_ball inf_commute inf_le1 inf_mono order_refl) qed qed
lemma locally_compact_compact: fixes S :: "'a :: heine_borel set" shows"locally compact S ⟷ (∀K. K ⊆ S ∧ compact K ⟶ (∃U V. K ⊆ U ∧ U ⊆ V ∧ V ⊆ S ∧ openin (top_of_set S) U ∧ compact V))"
(is"?lhs = ?rhs") proof assume ?lhs thenobtain u v where
uv: "∧x. x ∈ S ==> x ∈ u x ∧ u x ⊆ v x ∧ v x ⊆ S ∧ openin (top_of_set S) (u x) ∧ compact (v x)" by (metis locally_compactE) have *: "∃U V. K ⊆ U ∧ U ⊆ V ∧ V ⊆ S ∧ openin (top_of_set S) U ∧ compact V" if"K ⊆ S""compact K"for K proof - have"∧C. (∀c∈C. openin (top_of_set K) c) ∧ K ⊆∪C ==> ∃D⊆C. finite D ∧ K ⊆∪D" using that by (simp add: compact_eq_openin_cover) moreoverhave"∀c ∈ (λx. K ∩ u x) ` K. openin (top_of_set K) c" using that by clarify (metis subsetD inf.absorb_iff2 openin_subset openin_subtopology_Int_subset topspace_euclidean_subtopology uv) moreoverhave"K ⊆∪((λx. K ∩ u x) ` K)" using that by clarsimp (meson subsetCE uv) ultimatelyobtain D where"D ⊆ (λx. K ∩ u x) ` K""finite D""K ⊆∪D" by metis thenobtain T where T: "T ⊆ K""finite T""K ⊆∪((λx. K ∩ u x) ` T)" by (metis finite_subset_image) have Tuv: "∪(u ` T) ⊆∪(v ` T)" using T that by (force dest!: uv) moreover have"openin (top_of_set S) (∪ (u ` T))" using T that uv by fastforce moreover obtain"compact (∪ (v ` T))""∪ (v ` T) ⊆ S" by (metis T UN_subset_iff ‹K ⊆ S› compact_UN subset_iff uv) ultimatelyshow ?thesis using T by auto qed show ?rhs by (blast intro: *) next assume ?rhs thenshow ?lhs apply (clarsimp simp: locally_compact) apply (drule_tac x="{x}"in spec, simp) done qed
lemma open_imp_locally_compact: fixes S :: "'a :: heine_borel set" assumes"open S" shows"locally compact S" proof - have *: "∃U V. x ∈ U ∧ U ⊆ V ∧ V ⊆ S ∧ openin (top_of_set S) U ∧ compact V" if"x ∈ S"for x proof - obtain e where"e>0"and e: "cball x e ⊆ S" using open_contains_cball assms ‹x ∈ S›by blast have ope: "openin (top_of_set S) (ball x e)" by (meson e open_ball ball_subset_cball dual_order.trans open_subset) show ?thesis by (meson ‹0 < e› ball_subset_cball centre_in_ball compact_cball e ope) qed show ?thesis unfolding locally_compact by (blast intro: *) qed
lemma closed_imp_locally_compact: fixes S :: "'a :: heine_borel set" assumes"closed S" shows"locally compact S" proof - have *: "∃U V. x ∈ U ∧ U ⊆ V ∧ V ⊆ S ∧ openin (top_of_set S) U ∧ compact V" if"x ∈ S"for x apply (rule_tac x = "S ∩ ball x 1"in exI, rule_tac x = "S ∩ cball x 1"in exI) using‹x ∈ S› assms by auto show ?thesis unfolding locally_compact by (blast intro: *) qed
lemma locally_compact_UNIV: "locally compact (UNIV :: 'a :: heine_borel set)" by (simp add: closed_imp_locally_compact)
lemma locally_compact_Int: fixes S :: "'a :: t2_space set" shows"[locally compact S; locally compact T]==> locally compact (S ∩ T)" by (simp add: compact_Int locally_Int)
lemma locally_compact_closedin: fixes S :: "'a :: heine_borel set" shows"[closedin (top_of_set S) T; locally compact S] ==> locally compact T" unfolding closedin_closed using closed_imp_locally_compact locally_compact_Int by blast
lemma locally_compact_delete: fixes S :: "'a :: t1_space set" shows"locally compact S ==> locally compact (S - {a})" by (auto simp: openin_delete locally_open_subset)
lemma locally_closed: fixes S :: "'a :: heine_borel set" shows"locally closed S ⟷ locally compact S"
(is"?lhs = ?rhs") proof assume ?lhs thenshow ?rhs unfolding locally_def apply (elim all_forward imp_forward asm_rl exE) apply (rename_tac U V) apply (rule_tac x = "U ∩ ball x 1"in exI) apply (rule_tac x = "V ∩ cball x 1"in exI) apply (force intro: openin_trans) done next assume ?rhs thenshow ?lhs using compact_eq_bounded_closed locally_mono by blast qed
lemma locally_compact_openin_Un: fixes S :: "'a::euclidean_space set" assumes LCS: "locally compact S"and LCT: "locally compact T" and opS: "openin (top_of_set (S ∪ T)) S" and opT: "openin (top_of_set (S ∪ T)) T" shows"locally compact (S ∪ T)" proof - have"∃e>0. closed (cball x e ∩ (S ∪ T))"if"x ∈ S"for x proof - obtain e1 where"e1 > 0"and e1: "closed (cball x e1 ∩ S)" using LCS ‹x ∈ S›unfolding locally_compact_Int_cball by blast moreoverobtain e2 where"e2 > 0"and e2: "cball x e2 ∩ (S ∪ T) ⊆ S" by (meson ‹x ∈ S› opS openin_contains_cball) thenhave"cball x e2 ∩ (S ∪ T) = cball x e2 ∩ S" by force ultimatelyhave"closed (cball x (min e1 e2) ∩ (S ∪ T))" by (metis (no_types, lifting) cball_min_Int closed_Int closed_cball inf_assoc inf_commute) thenshow ?thesis by (metis ‹0 < e1›‹0 < e2› min_def) qed moreoverhave"∃e>0. closed (cball x e ∩ (S ∪ T))"if"x ∈ T"for x proof - obtain e1 where"e1 > 0"and e1: "closed (cball x e1 ∩ T)" using LCT ‹x ∈ T›unfolding locally_compact_Int_cball by blast moreoverobtain e2 where"e2 > 0"and e2: "cball x e2 ∩ (S ∪ T) ⊆ T" by (meson ‹x ∈ T› opT openin_contains_cball) thenhave"cball x e2 ∩ (S ∪ T) = cball x e2 ∩ T" by force moreoverhave"closed (cball x e1 ∩ (cball x e2 ∩ T))" by (metis closed_Int closed_cball e1 inf_left_commute) ultimatelyshow ?thesis by (rule_tac x="min e1 e2"in exI) (simp add: ‹0 < e2› cball_min_Int inf_assoc) qed ultimatelyshow ?thesis by (force simp: locally_compact_Int_cball) qed
lemma locally_compact_closedin_Un: fixes S :: "'a::euclidean_space set" assumes LCS: "locally compact S"and LCT:"locally compact T" and clS: "closedin (top_of_set (S ∪ T)) S" and clT: "closedin (top_of_set (S ∪ T)) T" shows"locally compact (S ∪ T)" proof - have"∃e>0. closed (cball x e ∩ (S ∪ T))"if"x ∈ S""x ∈ T"for x proof - obtain e1 where"e1 > 0"and e1: "closed (cball x e1 ∩ S)" using LCS ‹x ∈ S›unfolding locally_compact_Int_cball by blast moreover obtain e2 where"e2 > 0"and e2: "closed (cball x e2 ∩ T)" using LCT ‹x ∈ T›unfolding locally_compact_Int_cball by blast moreoverhave"closed (cball x (min e1 e2) ∩ (S ∪ T))" by (smt (verit) Int_Un_distrib2 Int_commute cball_min_Int closed_Int closed_Un closed_cball e1 e2 inf_left_commute) ultimatelyshow ?thesis by (rule_tac x="min e1 e2"in exI) linarith qed moreover have"∃e>0. closed (cball x e ∩ (S ∪ T))"if x: "x ∈ S""x ∉ T"for x proof - obtain e1 where"e1 > 0"and e1: "closed (cball x e1 ∩ S)" using LCS ‹x ∈ S›unfolding locally_compact_Int_cball by blast moreover obtain e2 where"e2>0"and"cball x e2 ∩ (S ∪ T) ⊆ S - T" using clT x by (fastforce simp: openin_contains_cball closedin_def) thenhave"closed (cball x e2 ∩ T)" proof - have"{} = T - (T - cball x e2)" using Diff_subset Int_Diff ‹cball x e2 ∩ (S ∪ T) ⊆ S - T›by auto thenshow ?thesis by (simp add: Diff_Diff_Int inf_commute) qed with e1 have"closed ((cball x e1 ∩ cball x e2) ∩ (S ∪ T))" apply (simp add: inf_commute inf_sup_distrib2) by (metis closed_Int closed_Un closed_cball inf_assoc inf_left_commute) thenhave"closed (cball x (min e1 e2) ∩ (S ∪ T))" by (simp add: cball_min_Int inf_commute) ultimatelyshow ?thesis using‹0 < e2›by (rule_tac x="min e1 e2"in exI) linarith qed moreover have"∃e>0. closed (cball x e ∩ (S ∪ T))"if x: "x ∉ S""x ∈ T"for x proof - obtain e1 where"e1 > 0"and e1: "closed (cball x e1 ∩ T)" using LCT ‹x ∈ T›unfolding locally_compact_Int_cball by blast moreover obtain e2 where"e2>0"and"cball x e2 ∩ (S ∪ T) ⊆ S ∪ T - S" using clS x by (fastforce simp: openin_contains_cball closedin_def) thenhave"closed (cball x e2 ∩ S)" by (metis Diff_disjoint Int_empty_right closed_empty inf.left_commute inf.orderE inf_sup_absorb) with e1 have"closed ((cball x e1 ∩ cball x e2) ∩ (S ∪ T))" apply (simp add: inf_commute inf_sup_distrib2) by (metis closed_Int closed_Un closed_cball inf_assoc inf_left_commute) thenhave"closed (cball x (min e1 e2) ∩ (S ∪ T))" by (auto simp: cball_min_Int) ultimatelyshow ?thesis using‹0 < e2›by (rule_tac x="min e1 e2"in exI) linarith qed ultimatelyshow ?thesis by (auto simp: locally_compact_Int_cball) qed
lemma locally_compact_Times: fixes S :: "'a::euclidean_space set"and T :: "'b::euclidean_space set" shows"[locally compact S; locally compact T]==> locally compact (S × T)" by (auto simp: compact_Times locally_Times)
lemma locally_compact_compact_subopen: fixes S :: "'a :: heine_borel set" shows "locally compact S ⟷ (∀K T. K ⊆ S ∧ compact K ∧ open T ∧ K ⊆ T ⟶ (∃U V. K ⊆ U ∧ U ⊆ V ∧ U ⊆ T ∧ V ⊆ S ∧ openin (top_of_set S) U ∧ compact V))"
(is"?lhs = ?rhs") proof assume L: ?lhs show ?rhs proof clarify fix K :: "'a set"and T :: "'a set" assume"K ⊆ S"and"compact K"and"open T"and"K ⊆ T" obtain U V where"K ⊆ U""U ⊆ V""V ⊆ S""compact V" and ope: "openin (top_of_set S) U" using L unfolding locally_compact_compact by (meson ‹K ⊆ S›‹compact K›) show"∃U V. K ⊆ U ∧ U ⊆ V ∧ U ⊆ T ∧ V ⊆ S ∧ openin (top_of_set S) U ∧ compact V" proof (intro exI conjI) show"K ⊆ U ∩ T" by (simp add: ‹K ⊆ T›‹K ⊆ U›) show"U ∩ T ⊆ closure(U ∩ T)" by (rule closure_subset) show"closure (U ∩ T) ⊆ S" by (metis ‹U ⊆ V›‹V ⊆ S›‹compact V› closure_closed closure_mono compact_imp_closed inf.cobounded1 subset_trans) show"openin (top_of_set S) (U ∩ T)" by (simp add: ‹open T› ope openin_Int_open) show"compact (closure (U ∩ T))" by (meson Int_lower1 ‹U ⊆ V›‹compact V› bounded_subset compact_closure compact_eq_bounded_closed) qed auto qed next assume ?rhs thenshow ?lhs unfolding locally_compact_compact by (metis open_openin openin_topspace subtopology_superset top.extremum topspace_euclidean_subtopology) qed
subsection‹Sura-Bura's results about compact components of sets›
proposition Sura_Bura_compact: fixes S :: "'a::euclidean_space set" assumes"compact S"and C: "C ∈ components S" shows"C = ∩{T. C ⊆ T ∧ openin (top_of_set S) T ∧ closedin (top_of_set S) T}"
(is"C = ∩?T") proof obtain x where x: "C = connected_component_set S x"and"x ∈ S" using C by (auto simp: components_def) have"C ⊆ S" by (simp add: C in_components_subset) have"∩?T⊆ connected_component_set S x" proof (rule connected_component_maximal) have"x ∈ C" by (simp add: ‹x ∈ S› x) thenshow"x ∈∩?T" by blast have clo: "closed (∩?T)" by (simp add: ‹compact S› closed_Inter closedin_compact_eq compact_imp_closed) have False if K1: "closedin (top_of_set (∩?T)) K1"and
K2: "closedin (top_of_set (∩?T)) K2"and
K12_Int: "K1 ∩ K2 = {}"and K12_Un: "K1 ∪ K2 = ∩?T"and"K1 ≠ {}""K2 ≠ {}" for K1 K2 proof - have"closed K1""closed K2" using closedin_closed_trans clo K1 K2 by blast+ thenobtain V1 V2 where"open V1""open V2""K1 ⊆ V1""K2 ⊆ V2"and V12: "V1 ∩ V2 = {}" using separation_normal ‹K1 ∩ K2 = {}›by metis have SV12_ne: "(S - (V1 ∪ V2)) ∩ (∩?T) ≠ {}" proof (rule compact_imp_fip) show"compact (S - (V1 ∪ V2))" by (simp add: ‹open V1›‹open V2›‹compact S› compact_diff open_Un) show cloT: "closed T"if"T ∈ ?T"for T using that ‹compact S› by (force intro: closedin_closed_trans simp add: compact_imp_closed) show"(S - (V1 ∪ V2)) ∩∩F≠ {}"if"finite F"andF: "F⊆ ?T"forF proof assume djo: "(S - (V1 ∪ V2)) ∩∩F = {}" obtain D where opeD: "openin (top_of_set S) D" and cloD: "closedin (top_of_set S) D" and"C ⊆ D"and DV12: "D ⊆ V1 ∪ V2" proof (cases "F = {}") case True with‹C ⊆ S› djo that show ?thesis by force next case False show ?thesis proof show ope: "openin (top_of_set S) (∩F)" using openin_Inter ‹finite F› False Fby blast thenshow"closedin (top_of_set S) (∩F)" by (meson cloTF closed_Inter closed_subset openin_imp_subset subset_eq) show"C ⊆∩F" usingFby auto show"∩F⊆ V1 ∪ V2" using ope djo openin_imp_subset by fastforce qed qed have"connected C" by (simp add: x) have"closed D" using‹compact S› cloD closedin_closed_trans compact_imp_closed by blast have cloV1: "closedin (top_of_set D) (D ∩ closure V1)" and cloV2: "closedin (top_of_set D) (D ∩ closure V2)" by (simp_all add: closedin_closed_Int) moreoverhave"D ∩ closure V1 = D ∩ V1""D ∩ closure V2 = D ∩ V2" using‹D ⊆ V1 ∪ V2›‹open V1›‹open V2› V12 by (auto simp: closure_subset [THEN subsetD] closure_iff_nhds_not_empty, blast+) ultimatelyhave cloDV1: "closedin (top_of_set D) (D ∩ V1)" and cloDV2: "closedin (top_of_set D) (D ∩ V2)" by metis+ thenobtain U1 U2 where"closed U1""closed U2" and D1: "D ∩ V1 = D ∩ U1"and D2: "D ∩ V2 = D ∩ U2" by (auto simp: closedin_closed) have"D ∩ U1 ∩ C ≠ {}" proof assume"D ∩ U1 ∩ C = {}" thenhave *: "C ⊆ D ∩ V2" using D1 DV12 ‹C ⊆ D›by auto have1: "openin (top_of_set S) (D ∩ V2)" by (simp add: ‹open V2› opeD openin_Int_open) have2: "closedin (top_of_set S) (D ∩ V2)" using cloD cloDV2 closedin_trans by blast have"∩ ?T⊆ D ∩ V2" by (rule Inter_lower) (use * 12in simp) thenshow False using K1 V12 ‹K1 ≠ {}›‹K1 ⊆ V1› closedin_imp_subset by blast qed moreoverhave"D ∩ U2 ∩ C ≠ {}" proof assume"D ∩ U2 ∩ C = {}" thenhave *: "C ⊆ D ∩ V1" using D2 DV12 ‹C ⊆ D›by auto have1: "openin (top_of_set S) (D ∩ V1)" by (simp add: ‹open V1› opeD openin_Int_open) have2: "closedin (top_of_set S) (D ∩ V1)" using cloD cloDV1 closedin_trans by blast have"∩?T⊆ D ∩ V1" by (rule Inter_lower) (use * 12in simp) thenshow False using K2 V12 ‹K2 ≠ {}›‹K2 ⊆ V2› closedin_imp_subset by blast qed ultimatelyshow False using‹connected C› [unfolded connected_closed, simplified, rule_format, of concl: "D ∩ U1""D ∩ U2"] using‹C ⊆ D› D1 D2 V12 DV12 ‹closed U1›‹closed U2›‹closed D› by blast qed qed show False by (metis (full_types) DiffE UnE Un_upper2 SV12_ne ‹K1 ⊆ V1›‹K2 ⊆ V2› disjoint_iff_not_equal subsetCE sup_ge1 K12_Un) qed thenshow"connected (∩?T)" by (auto simp: connected_closedin_eq) show"∩?T⊆ S" by (fastforce simp: C in_components_subset) qed with x show"∩?T⊆ C"by simp qed auto
corollary Sura_Bura_clopen_subset: fixes S :: "'a::euclidean_space set" assumes S: "locally compact S"and C: "C ∈ components S"and"compact C" and U: "open U""C ⊆ U" obtains K where"openin (top_of_set S) K""compact K""C ⊆ K""K ⊆ U" proof (rule ccontr) assume"¬ thesis" with that have neg: "∄K. openin (top_of_set S) K ∧ compact K ∧ C ⊆ K ∧ K ⊆ U" by metis obtain V K where"C ⊆ V""V ⊆ U""V ⊆ K""K ⊆ S""compact K" and opeSV: "openin (top_of_set S) V" using S U ‹compact C›by (meson C in_components_subset locally_compact_compact_subopen) let ?T = "{T. C ⊆ T ∧ openin (top_of_set K) T ∧ compact T ∧ T ⊆ K}" have CK: "C ∈ components K" by (meson C ‹C ⊆ V›‹K ⊆ S›‹V ⊆ K› components_intermediate_subset subset_trans) with‹compact K› have"C = ∩{T. C ⊆ T ∧ openin (top_of_set K) T ∧ closedin (top_of_set K) T}" by (simp add: Sura_Bura_compact) thenhave Ceq: "C = ∩?T" by (simp add: closedin_compact_eq ‹compact K›) obtain W where"open W"and W: "V = S ∩ W" using opeSV by (auto simp: openin_open) have"-(U ∩ W) ∩∩?T≠ {}" proof (rule closed_imp_fip_compact) show"- (U ∩ W) ∩∩F≠ {}" if"finite F"andF: "F⊆ ?T"forF proof (cases "F = {}") case True have False if"U = UNIV""W = UNIV" proof - have"V = S" by (simp add: W ‹W = UNIV›) with neg show False using‹C ⊆ V›‹K ⊆ S›‹V ⊆ K›‹V ⊆ U›‹compact K›by auto qed with True show ?thesis by auto next case False show ?thesis proof assume"- (U ∩ W) ∩∩F = {}" thenhave FUW: "∩F⊆ U ∩ W" by blast have"C ⊆∩F" usingFby auto moreoverhave"compact (∩F)" by (metis (no_types, lifting) compact_Inter False mem_Collect_eq subsetCE F) moreoverhave"∩F⊆ K" using False that(2) by fastforce moreoverhave opeKF: "openin (top_of_set K) (∩F)" using False F‹finite F›by blast thenhave opeVF: "openin (top_of_set V) (∩F)" using W ‹K ⊆ S›‹V ⊆ K› opeKF ‹∩F⊆ K› FUW openin_subset_trans by fastforce thenhave"openin (top_of_set S) (∩F)" by (metis opeSV openin_trans) moreoverhave"∩F⊆ U" by (meson ‹V ⊆ U› opeVF dual_order.trans openin_imp_subset) ultimatelyshow False using neg by blast qed qed qed (use‹open W›‹open U›in auto) with W Ceq ‹C ⊆ V›‹C ⊆ U›show False by auto qed
corollary Sura_Bura_clopen_subset_alt: fixes S :: "'a::euclidean_space set" assumes S: "locally compact S"and C: "C ∈ components S"and"compact C" and opeSU: "openin (top_of_set S) U"and"C ⊆ U" obtains K where"openin (top_of_set S) K""compact K""C ⊆ K""K ⊆ U" proof - obtain V where"open V""U = S ∩ V" using opeSU by (auto simp: openin_open) with‹C ⊆ U›have"C ⊆ V" by auto thenshow ?thesis using Sura_Bura_clopen_subset [OF S C ‹compact C›‹open V›] by (metis ‹U = S ∩ V› inf.bounded_iff openin_imp_subset that) qed
corollary Sura_Bura: fixes S :: "'a::euclidean_space set" assumes"locally compact S""C ∈ components S""compact C" shows"C = ∩ {K. C ⊆ K ∧ compact K ∧ openin (top_of_set S) K}"
(is"C = ?rhs") proof show"?rhs ⊆ C" proof (clarsimp, rule ccontr) fix x assume *: "∀X. C ⊆ X ∧ compact X ∧ openin (top_of_set S) X ⟶ x ∈ X" and"x ∉ C" obtain U V where"open U""open V""{x} ⊆ U""C ⊆ V""U ∩ V = {}" using separation_normal [of "{x}" C] by (metis Int_empty_left ‹x ∉ C›‹compact C› closed_empty closed_insert compact_imp_closed insert_disjoint(1)) have"x ∉ V" using‹U ∩ V = {}›‹{x} ⊆ U›by blast thenshow False by (meson "*" Sura_Bura_clopen_subset ‹C ⊆ V›‹open V› assms(1) assms(2) assms(3) subsetCE) qed qed blast
subsection‹Special cases of local connectedness and path connectedness›
lemma locally_connected_1: assumes "∧V x. [openin (top_of_set S) V; x ∈ V]==>∃U. openin (top_of_set S) U ∧ connected U ∧ x ∈ U ∧ U ⊆ V" shows"locally connected S" by (metis assms locally_def)
lemma locally_connected_2: assumes"locally connected S" "openin (top_of_set S) t" "x ∈ t" shows"openin (top_of_set S) (connected_component_set t x)" proof -
{ fix y :: 'a let ?SS = "top_of_set S" assume1: "openin ?SS t" "∀w x. openin ?SS w ∧ x ∈ w ⟶ (∃u. openin ?SS u ∧ (∃v. connected v ∧ x ∈ u ∧ u ⊆ v ∧ v ⊆ w))" and"connected_component t x y" thenhave"y ∈ t"and y: "y ∈ connected_component_set t x" using connected_component_subset by blast+ obtain F where "∀x y. (∃w. openin ?SS w ∧ (∃u. connected u ∧ x ∈ w ∧ w ⊆ u ∧ u ⊆ y)) = (openin ?SS (F x y) ∧ (∃u. connected u ∧ x ∈ F x y ∧ F x y ⊆ u ∧ u ⊆ y))" by moura thenobtain G where "∀a A. (∃U. openin ?SS U ∧ (∃V. connected V ∧ a ∈ U ∧ U ⊆ V ∧ V ⊆ A)) = (openin ?SS (F a A) ∧ connected (G a A) ∧ a ∈ F a A ∧ F a A ⊆ G a A ∧ G a A ⊆ A)" by moura thenhave *: "openin ?SS (F y t) ∧ connected (G y t) ∧ y ∈ F y t ∧ F y t ⊆ G y t ∧G y t ⊆ t" using1‹y ∈ t›by presburger have"G y t ⊆ connected_component_set t y" by (metis (no_types) * connected_component_eq_self connected_component_mono contra_subsetD) thenhave"∃A. openin ?SS A ∧ y ∈ A ∧ A ⊆ connected_component_set t x" by (metis (no_types) * connected_component_eq dual_order.trans y)
} thenshow ?thesis using assms openin_subopen by (force simp: locally_def) qed
lemma locally_connected_3: assumes"∧t x. [openin (top_of_set S) t; x ∈ t] ==> openin (top_of_set S) (connected_component_set t x)" "openin (top_of_set S) v""x ∈ v" shows"∃u. openin (top_of_set S) u ∧ connected u ∧ x ∈ u ∧ u ⊆ v" using assms connected_component_subset by fastforce
lemma locally_connected: "locally connected S ⟷ (∀v x. openin (top_of_set S) v ∧ x ∈ v ⟶ (∃u. openin (top_of_set S) u ∧ connected u ∧ x ∈ u ∧ u ⊆ v))" by (metis locally_connected_1 locally_connected_2 locally_connected_3)
lemma locally_connected_open_connected_component: "locally connected S ⟷ (∀t x. openin (top_of_set S) t ∧ x ∈ t ⟶ openin (top_of_set S) (connected_component_set t x))" by (metis locally_connected_1 locally_connected_2 locally_connected_3)
lemma locally_path_connected_1: assumes "∧v x. [openin (top_of_set S) v; x ∈ v] ==>∃u. openin (top_of_set S) u ∧ path_connected u ∧ x ∈ u ∧ u ⊆ v" shows"locally path_connected S" by (force simp: locally_def dest: assms)
lemma locally_path_connected_2: assumes"locally path_connected S" "openin (top_of_set S) t" "x ∈ t" shows"openin (top_of_set S) (path_component_set t x)" proof -
{ fix y :: 'a let ?SS = "top_of_set S" assume1: "openin ?SS t" "∀w x. openin ?SS w ∧ x ∈ w ⟶ (∃u. openin ?SS u ∧ (∃v. path_connected v ∧ x ∈ u ∧ u ⊆ v ∧ v ⊆ w))" and"path_component t x y" thenhave"y ∈ t"and y: "y ∈ path_component_set t x" using path_component_mem(2) by blast+ obtain F where "∀x y. (∃w. openin ?SS w ∧ (∃u. path_connected u ∧ x ∈ w ∧ w ⊆ u ∧ u ⊆ y)) = (openin ?SS (F x y) ∧ (∃u. path_connected u ∧ x ∈ F x y ∧ F x y ⊆ u ∧ u ⊆ y))" by moura thenobtain G where "∀a A. (∃U. openin ?SS U ∧ (∃V. path_connected V ∧ a ∈ U ∧ U ⊆ V ∧ V ⊆ A)) = (openin ?SS (F a A) ∧ path_connected (G a A) ∧ a ∈ F a A ∧ F a A ⊆ G a A ∧ G a A ⊆ A)" by moura thenhave *: "openin ?SS (F y t) ∧ path_connected (G y t) ∧ y ∈ F y t ∧ F y t ⊆ G y t ∧ G y t ⊆ t" using1‹y ∈ t›by presburger have"G y t ⊆ path_component_set t y" using * path_component_maximal rev_subsetD by blast thenhave"∃A. openin ?SS A ∧ y ∈ A ∧ A ⊆ path_component_set t x" by (metis "*"‹G y t ⊆ path_component_set t y› dual_order.trans path_component_eq y)
} thenshow ?thesis using assms openin_subopen by (force simp: locally_def) qed
lemma locally_path_connected_3: assumes"∧t x. [openin (top_of_set S) t; x ∈ t] ==> openin (top_of_set S) (path_component_set t x)" "openin (top_of_set S) v""x ∈ v" shows"∃u. openin (top_of_set S) u ∧ path_connected u ∧ x ∈ u ∧ u ⊆ v" proof - have"path_component v x x" by (meson assms(3) path_component_refl) thenshow ?thesis by (metis assms mem_Collect_eq path_component_subset path_connected_path_component) qed
proposition locally_path_connected: "locally path_connected S ⟷ (∀V x. openin (top_of_set S) V ∧ x ∈ V ⟶ (∃U. openin (top_of_set S) U ∧ path_connected U ∧ x ∈ U ∧ U ⊆ V))" by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
proposition locally_path_connected_open_path_component: "locally path_connected S ⟷ (∀t x. openin (top_of_set S) t ∧ x ∈ t ⟶ openin (top_of_set S) (path_component_set t x))" by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
lemma locally_connected_open_component: "locally connected S ⟷ (∀t c. openin (top_of_set S) t ∧ c ∈ components t ⟶ openin (top_of_set S) c)" by (metis components_iff locally_connected_open_connected_component)
proposition locally_connected_im_kleinen: "locally connected S ⟷ (∀v x. openin (top_of_set S) v ∧ x ∈ v ⟶ (∃u. openin (top_of_set S) u ∧ x ∈ u ∧ u ⊆ v ∧ (∀y. y ∈ u ⟶ (∃c. connected c ∧ c ⊆ v ∧ x ∈ c ∧ y ∈ c))))"
(is"?lhs = ?rhs") proof assume ?lhs thenshow ?rhs by (fastforce simp: locally_connected) next assume ?rhs have *: "∃T. openin (top_of_set S) T ∧ x ∈ T ∧ T ⊆ c" if"openin (top_of_set S) t"and c: "c ∈ components t"and"x ∈ c"for t c x proof - from that ‹?rhs› [rule_format, of t x] obtain u where u: "openin (top_of_set S) u ∧ x ∈ u ∧ u ⊆ t ∧ (∀y. y ∈ u ⟶ (∃c. connected c ∧ c ⊆ t ∧ x ∈ c ∧ y ∈ c))" using in_components_subset by auto obtain F :: "'a set → 'a set → 'a"where "∀x y. (∃z. z ∈ x ∧ y = connected_component_set x z) = (F x y ∈ x ∧ y = connected_component_set x (F x y))" by moura thenhave F: "F t c ∈ t ∧ c = connected_component_set t (F t c)" by (meson components_iff c) obtain G :: "'a set → 'a set → 'a"where
G: "∀x y. (∃z. z ∈ y ∧ z ∉ x) = (G x y ∈ y ∧ G x y ∉ x)" by moura have"G c u ∉ u ∨ G c u ∈ c" using F by (metis (full_types) u connected_componentI connected_component_eq mem_Collect_eq that(3)) thenshow ?thesis using G u by auto qed show ?lhs unfolding locally_connected_open_component by (meson "*" openin_subopen) qed
proposition locally_path_connected_im_kleinen: "locally path_connected S ⟷ (∀v x. openin (top_of_set S) v ∧ x ∈ v ⟶ (∃u. openin (top_of_set S) u ∧ x ∈ u ∧ u ⊆ v ∧ (∀y. y ∈ u ⟶ (∃p. path p ∧ path_image p ⊆ v ∧ pathstart p = x ∧ pathfinish p = y))))"
(is"?lhs = ?rhs") proof assume ?lhs thenshow ?rhs apply (simp add: locally_path_connected path_connected_def) apply (erule all_forward ex_forward imp_forward conjE | simp)+ by (meson dual_order.trans) next assume ?rhs have *: "∃T. openin (top_of_set S) T ∧ x ∈ T ∧ T ⊆ path_component_set u z" if"openin (top_of_set S) u"and"z ∈ u"and c: "path_component u z x"for u z x proof - have"x ∈ u" by (meson c path_component_mem(2)) with that ‹?rhs› [rule_format, of u x] obtain U where U: "openin (top_of_set S) U ∧ x ∈ U ∧ U ⊆ u ∧ (∀y. y ∈ U ⟶ (∃p. path p ∧ path_image p ⊆ u ∧ pathstart p = x ∧ pathfinish p = y))" by blast show ?thesis by (metis U c mem_Collect_eq path_component_def path_component_eq subsetI) qed show ?lhs unfolding locally_path_connected_open_path_component using"*" openin_subopen by fastforce qed
lemma locally_path_connected_imp_locally_connected: "locally path_connected S ==> locally connected S" using locally_mono path_connected_imp_connected by blast
lemma locally_connected_components: "[locally connected S; c ∈ components S]==> locally connected c" by (meson locally_connected_open_component locally_open_subset openin_subtopology_self)
lemma locally_path_connected_components: "[locally path_connected S; c ∈ components S]==> locally path_connected c" by (meson locally_connected_open_component locally_open_subset locally_path_connected_imp_locally_connected openin_subtopology_self)
lemma locally_path_connected_connected_component: "locally path_connected S ==> locally path_connected (connected_component_set S x)" by (metis components_iff connected_component_eq_empty locally_empty locally_path_connected_components)
lemma open_imp_locally_path_connected: fixes S :: "'a :: real_normed_vector set" assumes"open S" shows"locally path_connected S" proof (rule locally_mono) show"locally convex S" using assms unfolding locally_def by (meson open_ball centre_in_ball convex_ball openE open_subset openin_imp_subset openin_open_trans subset_trans) show"∧T::'a set. convex T ==> path_connected T" using convex_imp_path_connected by blast qed
lemma open_imp_locally_connected: fixes S :: "'a :: real_normed_vector set" shows"open S ==> locally connected S" by (simp add: locally_path_connected_imp_locally_connected open_imp_locally_path_connected)
lemma openin_connected_component_locally_connected: "locally connected S ==> openin (top_of_set S) (connected_component_set S x)" by (metis connected_component_eq_empty locally_connected_2 openin_empty openin_subtopology_self)
lemma openin_components_locally_connected: "[locally connected S; c ∈ components S]==> openin (top_of_set S) c" using locally_connected_open_component openin_subtopology_self by blast
lemma openin_path_component_locally_path_connected: "locally path_connected S ==> openin (top_of_set S) (path_component_set S x)" by (metis (no_types) empty_iff locally_path_connected_2 openin_subopen openin_subtopology_self path_component_eq_empty)
lemma closedin_path_component_locally_path_connected: assumes"locally path_connected S" shows"closedin (top_of_set S) (path_component_set S x)" proof - have"openin (top_of_set S) (∪ ({path_component_set S y |y. y ∈ S} - {path_component_set S x}))" using locally_path_connected_2 assms by fastforce thenshow ?thesis by (simp add: closedin_def path_component_subset complement_path_component_Union) qed
lemma convex_imp_locally_path_connected: fixes S :: "'a:: real_normed_vector set" assumes"convex S" shows"locally path_connected S" proof (clarsimp simp: locally_path_connected) fix V x assume"openin (top_of_set S) V"and"x ∈ V" thenobtain T e where"V = S ∩ T""x ∈ S""0 < e""ball x e ⊆ T" by (metis Int_iff openE openin_open) thenhave"openin (top_of_set S) (S ∩ ball x e)""path_connected (S ∩ ball x e)" by (simp_all add: assms convex_Int convex_imp_path_connected openin_open_Int) thenshow"∃U. openin (top_of_set S) U ∧ path_connected U ∧ x ∈ U ∧ U ⊆ V" using‹0 < e›‹V = S ∩ T›‹ball x e ⊆ T›‹x ∈ S›by auto qed
lemma convex_imp_locally_connected: fixes S :: "'a:: real_normed_vector set" shows"convex S ==> locally connected S" by (simp add: locally_path_connected_imp_locally_connected convex_imp_locally_path_connected)
subsection‹Relations between components and path components›
lemma path_component_eq_connected_component: assumes"locally path_connected S" shows"(path_component S x = connected_component S x)" proof (cases "x ∈ S") case True have"openin (top_of_set (connected_component_set S x)) (path_component_set S x)" proof (rule openin_subset_trans) show"openin (top_of_set S) (path_component_set S x)" by (simp add: True assms locally_path_connected_2) show"connected_component_set S x ⊆ S" by (simp add: connected_component_subset) qed (simp add: path_component_subset_connected_component) moreoverhave"closedin (top_of_set (connected_component_set S x)) (path_component_set S x)" proof (rule closedin_subset_trans [of S]) show"closedin (top_of_set S) (path_component_set S x)" by (simp add: assms closedin_path_component_locally_path_connected) show"connected_component_set S x ⊆ S" by (simp add: connected_component_subset) qed (simp add: path_component_subset_connected_component) ultimatelyhave *: "path_component_set S x = connected_component_set S x" by (metis connected_connected_component connected_clopen True path_component_eq_empty) thenshow ?thesis by blast next case False thenshow ?thesis by (metis Collect_empty_eq_bot connected_component_eq_empty path_component_eq_empty) qed
lemma path_component_eq_connected_component_set: "locally path_connected S ==> (path_component_set S x = connected_component_set S x)" by (simp add: path_component_eq_connected_component)
lemma locally_path_connected_path_component: "locally path_connected S ==> locally path_connected (path_component_set S x)" using locally_path_connected_connected_component path_component_eq_connected_component by fastforce
lemma open_path_connected_component: fixes S :: "'a :: real_normed_vector set" shows"open S ==> path_component S x = connected_component S x" by (simp add: path_component_eq_connected_component open_imp_locally_path_connected)
lemma open_path_connected_component_set: fixes S :: "'a :: real_normed_vector set" shows"open S ==> path_component_set S x = connected_component_set S x" by (simp add: open_path_connected_component)
proposition locally_connected_quotient_image: assumes lcS: "locally connected S" and oo: "∧T. T ⊆ f ` S ==> openin (top_of_set S) (S ∩ f -` T) ⟷ openin (top_of_set (f ` S)) T" shows"locally connected (f ` S)" proof (clarsimp simp: locally_connected_open_component) fix U C assume opefSU: "openin (top_of_set (f ` S)) U"and"C ∈ components U" thenhave"C ⊆ U""U ⊆ f ` S" by (meson in_components_subset openin_imp_subset)+ thenhave"openin (top_of_set (f ` S)) C ⟷ openin (top_of_set S) (S ∩ f -` C)" by (auto simp: oo) moreoverhave"openin (top_of_set S) (S ∩ f -` C)" proof (subst openin_subopen, clarify) fix x assume"x ∈ S""f x ∈ C" show"∃T. openin (top_of_set S) T ∧ x ∈ T ∧ T ⊆ (S ∩ f -` C)" proof (intro conjI exI) show"openin (top_of_set S) (connected_component_set (S ∩ f -` U) x)" proof (rule ccontr) assume **: "¬ openin (top_of_set S) (connected_component_set (S ∩ f -` U) x)" thenhave"x ∉ (S ∩ f -` U)" using‹U ⊆ f ` S› opefSU lcS locally_connected_2 oo by blast with ** show False by (metis (no_types) connected_component_eq_empty empty_iff openin_subopen) qed next show"x ∈ connected_component_set (S ∩ f -` U) x" using‹C ⊆ U›‹f x ∈ C›‹x ∈ S›by auto next have contf: "continuous_on S f" by (simp add: continuous_on_open oo openin_imp_subset) thenhave"continuous_on (connected_component_set (S ∩ f -` U) x) f" by (meson connected_component_subset continuous_on_subset inf.boundedE) thenhave"connected (f ` connected_component_set (S ∩ f -` U) x)" by (rule connected_continuous_image [OF _ connected_connected_component]) moreoverhave"f ` connected_component_set (S ∩ f -` U) x ⊆ U" using connected_component_in by blast moreoverhave"C ∩ f ` connected_component_set (S ∩ f -` U) x ≠ {}" using‹C ⊆ U›‹f x ∈ C›‹x ∈ S›by fastforce ultimatelyhave fC: "f ` (connected_component_set (S ∩ f -` U) x) ⊆ C" by (rule components_maximal [OF ‹C ∈ components U›]) have cUC: "connected_component_set (S ∩ f -` U) x ⊆ (S ∩ f -` C)" using connected_component_subset fC by blast have"connected_component_set (S ∩ f -` U) x ⊆ connected_component_set (S ∩ f -` C) x" proof -
{ assume"x ∈ connected_component_set (S ∩ f -` U) x" thenhave ?thesis using cUC connected_component_idemp connected_component_mono by blast } thenshow ?thesis using connected_component_eq_empty by auto qed alsohave"…⊆ (S ∩ f -` C)" by (rule connected_component_subset) finallyshow"connected_component_set (S ∩ f -` U) x ⊆ (S ∩ f -` C)" . qed qed ultimatelyshow"openin (top_of_set (f ` S)) C" by metis qed
text‹The proof resembles that above but is not identical!›
proposition locally_path_connected_quotient_image: assumes lcS: "locally path_connected S" and oo: "∧T. T ⊆ f ` S ==> openin (top_of_set S) (S ∩ f -` T) ⟷ openin (top_of_set (f ` S)) T" shows"locally path_connected (f ` S)" proof (clarsimp simp: locally_path_connected_open_path_component) fix U y assume opefSU: "openin (top_of_set (f ` S)) U"and"y ∈ U" thenhave"path_component_set U y ⊆ U""U ⊆ f ` S" by (meson path_component_subset openin_imp_subset)+ thenhave"openin (top_of_set (f ` S)) (path_component_set U y) ⟷ openin (top_of_set S) (S ∩ f -` path_component_set U y)" proof - have"path_component_set U y ⊆ f ` S" using‹U ⊆ f ` S›‹path_component_set U y ⊆ U›by blast thenshow ?thesis using oo by blast qed moreoverhave"openin (top_of_set S) (S ∩ f -` path_component_set U y)" proof (subst openin_subopen, clarify) fix x assume"x ∈ S"and Uyfx: "path_component U y (f x)" thenhave"f x ∈ U" using path_component_mem by blast show"∃T. openin (top_of_set S) T ∧ x ∈ T ∧ T ⊆ (S ∩ f -` path_component_set U y)" proof (intro conjI exI) show"openin (top_of_set S) (path_component_set (S ∩ f -` U) x)" proof (rule ccontr) assume **: "¬ openin (top_of_set S) (path_component_set (S ∩ f -` U) x)" thenhave"x ∉ (S ∩ f -` U)" by (metis (no_types, lifting) ‹U ⊆ f ` S› opefSU lcS oo locally_path_connected_open_path_component) thenshow False using ** ‹path_component_set U y ⊆ U›‹x ∈ S›‹path_component U y (f x)›by blast qed next show"x ∈ path_component_set (S ∩ f -` U) x" by (simp add: ‹f x ∈ U›‹x ∈ S› path_component_refl) next have contf: "continuous_on S f" by (simp add: continuous_on_open oo openin_imp_subset) thenhave"continuous_on (path_component_set (S ∩ f -` U) x) f" by (meson Int_lower1 continuous_on_subset path_component_subset) thenhave"path_connected (f ` path_component_set (S ∩ f -` U) x)" by (simp add: path_connected_continuous_image) moreoverhave"f ` path_component_set (S ∩ f -` U) x ⊆ U" using path_component_mem by fastforce moreoverhave"f x ∈ f ` path_component_set (S ∩ f -` U) x" by (force simp: ‹x ∈ S›‹f x ∈ U› path_component_refl_eq) ultimatelyhave"f ` (path_component_set (S ∩ f -` U) x) ⊆ path_component_set U (f x)" by (meson path_component_maximal) alsohave"…⊆ path_component_set U y" by (simp add: Uyfx path_component_maximal path_component_subset path_component_sym) finallyhave fC: "f ` (path_component_set (S ∩ f -` U) x) ⊆ path_component_set U y". have cUC: "path_component_set (S ∩ f -` U) x ⊆ (S ∩ f -` path_component_set U y)" using path_component_subset fC by blast have"path_component_set (S ∩ f -` U) x ⊆ path_component_set (S ∩ f -` path_component_set U y) x" proof - have"∧a. path_component_set (path_component_set (S ∩ f -` U) x) a ⊆ path_component_set (S ∩ f -` path_component_set U y) a" using cUC path_component_mono by blast thenshow ?thesis using path_component_path_component by blast qed alsohave"…⊆ (S ∩ f -` path_component_set U y)" by (rule path_component_subset) finallyshow"path_component_set (S ∩ f -` U) x ⊆ (S ∩ f -` path_component_set U y)" . qed qed ultimatelyshow"openin (top_of_set (f ` S)) (path_component_set U y)" by metis qed
lemma continuous_on_components_gen: fixes f :: "'a::topological_space → 'b::topological_space" assumes"∧C. C ∈ components S ==> openin (top_of_set S) C ∧ continuous_on C f" shows"continuous_on S f" proof (clarsimp simp: continuous_openin_preimage_eq) fix t :: "'b set" assume"open t" have *: "S ∩ f -` t = (∪c ∈ components S. c ∩ f -` t)" by auto show"openin (top_of_set S) (S ∩ f -` t)" unfolding * using‹open t› assms continuous_openin_preimage_gen openin_trans openin_Union by blast qed
lemmacontinuous_on_components: fixesf::"'a::topological_space\<Rightarrow>'b::topological_space" assumes"locallyconnectedS""\<And>C.C\<in>componentsS\<Longrightarrow>continuous_onCf" shows"continuous_onSf" proof(rulecontinuous_on_components_gen) fixC assume"C\<in>componentsS" thenshow"openin(top_of_setS)C\<and>continuous_onCf" by(simpadd:assmsopenin_components_locally_connected) qed
lemmaclosedin_union_complement_components: assumesU:"locallyconnectedU" andS:"closedin(top_of_setU)S" andcuS:"c\<subseteq>components(U-S)" shows"closedin(top_of_setU)(S\<union>\<Union>c)" proof- havedi:"(\<And>ST.S\<in>c\<and>T\<in>c'\<Longrightarrow>disjntST)\<Longrightarrow>disjnt(\<Union>c)(\<Union>c')"forc' by(simpadd:disjnt_def)blast have"S\<subseteq>U" usingSclosedin_imp_subsetbyblast moreoverhave"U-S=\<Union>c\<union>\<Union>(components(U-S)-c)" by(metisDiff_partitionUnion_componentsUnion_Un_distribassms(3)) moreoverhave"disjnt(\<Union>c)(\<Union>(components(U-S)-c))" apply(ruledi) by(metisdiDiffD1DiffD2assms(3)components_nonoverlapdisjnt_defsubsetCE) ultimatelyhaveeq:"S\<union>\<Union>c=U-(\<Union>(components(U-S)-c))" by(autosimp:disjnt_def) have*:"openin(top_of_setU)(\<Union>(components(U-S)-c))" proof(ruleopenin_Union[OFopenin_trans[of"U-S"]]) show"openin(top_of_set(U-S))T"if"T\<in>components(U-S)-c"forT usingthatby(simpadd:USlocally_diff_closedopenin_components_locally_connected) show"openin(top_of_setU)(U-S)"if"T\<in>components(U-S)-c"forT usingthatby(simpadd:openin_diffS) qed have"closedin(top_of_setU)(U-\<Union>(components(U-S)-c))"
by (metis closedin_diff closedin_topspace topspace_euclidean_subtopology *) thenhave"openin (top_of_set U) (U - (U - ∪(components (U - S) - c)))" by (simp add: openin_diff) thenshow ?thesis by (force simp: eq closedin_def) qed
lemma closed_union_complement_components: fixes S :: "'a::real_normed_vector set" assumes S: "closed S"and c: "c ⊆ components(- S)" shows"closed(S ∪∪ c)" proof - have"closedin (top_of_set UNIV) (S ∪∪c)" by (metis Compl_eq_Diff_UNIV S c closed_closedin closedin_union_complement_components locally_connected_UNIV subtopology_UNIV) thenshow ?thesis by simp qed
lemma closedin_Un_complement_component: fixes S :: "'a::real_normed_vector set" assumes u: "locally connected u" and S: "closedin (top_of_set u) S" and c: " c ∈ components(u - S)" shows"closedin (top_of_set u) (S ∪ c)" proof - have"closedin (top_of_set u) (S ∪∪{c})" using c by (blast intro: closedin_union_complement_components [OF u S]) thenshow ?thesis by simp qed
lemma closed_Un_complement_component: fixes S :: "'a::real_normed_vector set" assumes S: "closed S"and c: " c ∈ components(-S)" shows"closed (S ∪ c)" by (metis Compl_eq_Diff_UNIV S c closed_closedin closedin_Un_complement_component
locally_connected_UNIV subtopology_UNIV)
subsection‹Existence of isometry between subspaces of same dimension›
lemma isometry_subset_subspace: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes S: "subspace S" and T: "subspace T" and d: "dim S ≤ dim T" obtains f where"linear f""f ∈ S → T""∧x. x ∈ S ==> norm(f x) = norm x" proof - obtain B where"B ⊆ S"and Borth: "pairwise orthogonal B" and B1: "∧x. x ∈ B ==> norm x = 1" and"independent B""finite B""card B = dim S""span B = S" by (metis orthonormal_basis_subspace [OF S] independent_imp_finite) obtain C where"C ⊆ T"and Corth: "pairwise orthogonal C" and C1:"∧x. x ∈ C ==> norm x = 1" and"independent C""finite C""card C = dim T""span C = T" by (metis orthonormal_basis_subspace [OF T] independent_imp_finite) obtain fb where"fb ` B ⊆ C""inj_on fb B" by (metis ‹card B = dim S›‹card C = dim T›‹finite B›‹finite C› card_le_inj d) thenhave pairwise_orth_fb: "pairwise (λv j. orthogonal (fb v) (fb j)) B" using Corth unfolding pairwise_def inj_on_def by (blast intro: orthogonal_clauses) obtain f where"linear f"and ffb: "∧x. x ∈ B ==> f x = fb x" using linear_independent_extend ‹independent B›by fastforce have"span (f ` B) ⊆ span C" by (metis ‹fb ` B ⊆ C› ffb image_cong span_mono) thenhave"f ` S ⊆ T" unfolding‹span B = S›‹span C = T› span_linear_image[OF ‹linear f›] . have [simp]: "∧x. x ∈ B ==> norm (fb x) = norm x" using B1 C1 ‹fb ` B ⊆ C›by auto have"norm (f x) = norm x"if"x ∈ S"for x proof - interpret linear f by fact obtain a where x: "x = (∑v ∈ B. a v *R v)" using‹finite B›‹span B = S›‹x ∈ S› span_finite by fastforce have"norm (f x)^2 = norm (∑v∈B. a v *R fb v)^2"by (simp add: sum scale ffb x) alsohave"… = (∑v∈B. norm ((a v *R fb v))^2)" proof (rule norm_sum_Pythagorean [OF ‹finite B›]) show"pairwise (λv j. orthogonal (a v *R fb v) (a j *R fb j)) B" by (rule pairwise_ortho_scaleR [OF pairwise_orth_fb]) qed alsohave"… = norm x ^2" by (simp add: x pairwise_ortho_scaleR Borth norm_sum_Pythagorean [OF ‹finite B›]) finallyshow ?thesis by (simp add: norm_eq_sqrt_inner) qed thenshow ?thesis by (meson ‹f ` S ⊆ T›‹linear f› image_subset_iff_funcset that) qed
proposition isometries_subspaces: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes S: "subspace S" and T: "subspace T" and d: "dim S = dim T" obtains f g where"linear f""linear g""f ` S = T""g ` T = S" "∧x. x ∈ S ==> norm(f x) = norm x" "∧x. x ∈ T ==> norm(g x) = norm x" "∧x. x ∈ S ==> g(f x) = x" "∧x. x ∈ T ==> f(g x) = x" proof - obtain B where"B ⊆ S"and Borth: "pairwise orthogonal B" and B1: "∧x. x ∈ B ==> norm x = 1" and"independent B""finite B""card B = dim S""span B = S" by (metis orthonormal_basis_subspace [OF S] independent_imp_finite) obtain C where"C ⊆ T"and Corth: "pairwise orthogonal C" and C1:"∧x. x ∈ C ==> norm x = 1" and"independent C""finite C""card C = dim T""span C = T" by (metis orthonormal_basis_subspace [OF T] independent_imp_finite) obtain fb where"bij_betw fb B C" by (metis ‹finite B›‹finite C› bij_betw_iff_card ‹card B = dim S›‹card C = dim T› d) thenhave pairwise_orth_fb: "pairwise (λv j. orthogonal (fb v) (fb j)) B" using Corth unfolding pairwise_def inj_on_def bij_betw_def by (blast intro: orthogonal_clauses) obtain f where"linear f"and ffb: "∧x. x ∈ B ==> f x = fb x" using linear_independent_extend ‹independent B›by fastforce interpret f: linear f by fact define gb where"gb ≡ inv_into B fb" thenhave pairwise_orth_gb: "pairwise (λv j. orthogonal (gb v) (gb j)) C" using Borth ‹bij_betw fb B C›unfolding pairwise_def bij_betw_def by force obtain g where"linear g"and ggb: "∧x. x ∈ C ==> g x = gb x" using linear_independent_extend ‹independent C›by fastforce interpret g: linear g by fact have"span (f ` B) ⊆ span C" by (metis ‹bij_betw fb B C› bij_betw_imp_surj_on eq_iff ffb image_cong) thenhave"f ` S ⊆ T" unfolding‹span B = S›‹span C = T› span_linear_image[OF ‹linear f›] . have [simp]: "∧x. x ∈ B ==> norm (fb x) = norm x" using B1 C1 ‹bij_betw fb B C› bij_betw_imp_surj_on by fastforce have f [simp]: "norm (f x) = norm x""g (f x) = x"if"x ∈ S"for x proof - obtain a where x: "x = (∑v ∈ B. a v *R v)" using‹finite B›‹span B = S›‹x ∈ S› span_finite by fastforce have"f x = (∑v ∈ B. f (a v *R v))" using linear_sum [OF ‹linear f›] x by auto alsohave"… = (∑v ∈ B. a v *R f v)" by (simp add: f.sum f.scale) alsohave"… = (∑v ∈ B. a v *R fb v)" by (simp add: ffb cong: sum.cong) finallyhave *: "f x = (∑v∈B. a v *R fb v)" . thenhave"(norm (f x))2 = (norm (∑v∈B. a v *R fb v))2"by simp alsohave"… = (∑v∈B. norm ((a v *R fb v))^2)" proof (rule norm_sum_Pythagorean [OF ‹finite B›]) show"pairwise (λv j. orthogonal (a v *R fb v) (a j *R fb j)) B" by (rule pairwise_ortho_scaleR [OF pairwise_orth_fb]) qed alsohave"… = (norm x)2" by (simp add: x pairwise_ortho_scaleR Borth norm_sum_Pythagorean [OF ‹finite B›]) finallyshow"norm (f x) = norm x" by (simp add: norm_eq_sqrt_inner) have"g (f x) = g (∑v∈B. a v *R fb v)"by (simp add: *) alsohave"… = (∑v∈B. g (a v *R fb v))" by (simp add: g.sum g.scale) alsohave"… = (∑v∈B. a v *R g (fb v))" by (simp add: g.scale) alsohave"… = (∑v∈B. a v *R v)" proof (rule sum.cong [OF refl]) show"a x *R g (fb x) = a x *R x"if"x ∈ B"for x using that ‹bij_betw fb B C› bij_betwE bij_betw_inv_into_left gb_def ggb by fastforce qed alsohave"… = x" using x by blast finallyshow"g (f x) = x" . qed have [simp]: "∧x. x ∈ C ==> norm (gb x) = norm x" by (metis B1 C1 ‹bij_betw fb B C› bij_betw_imp_surj_on gb_def inv_into_into) have g [simp]: "f (g x) = x"if"x ∈ T"for x proof - obtain a where x: "x = (∑v ∈ C. a v *R v)" using‹finite C›‹span C = T›‹x ∈ T› span_finite by fastforce have"g x = (∑v ∈ C. g (a v *R v))" by (simp add: x g.sum) alsohave"… = (∑v ∈ C. a v *R g v)" by (simp add: g.scale) alsohave"… = (∑v ∈ C. a v *R gb v)" by (simp add: ggb cong: sum.cong) finallyhave"f (g x) = f (∑v∈C. a v *R gb v)"by simp alsohave"… = (∑v∈C. f (a v *R gb v))" by (simp add: f.scale f.sum) alsohave"… = (∑v∈C. a v *R f (gb v))" by (simp add: f.scale f.sum) alsohave"… = (∑v∈C. a v *R v)" using‹bij_betw fb B C› by (simp add: bij_betw_def gb_def bij_betw_inv_into_right ffb inv_into_into) alsohave"… = x" using x by blast finallyshow"f (g x) = x" . qed have gim: "g ` T = S" by (metis (full_types) S T ‹f ` S ⊆ T› d dim_eq_span dim_image_le f(2) g.linear_axioms
image_iff linear_subspace_image span_eq_iff subset_iff) have fim: "f ` S = T" using‹g ` T = S› image_iff by fastforce have [simp]: "norm (g x) = norm x"if"x ∈ T"for x using fim that by auto show ?thesis by (rule that [OF ‹linear f›‹linear g›]) (simp_all add: fim gim) qed
corollary isometry_subspaces: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes S: "subspace S" and T: "subspace T" and d: "dim S = dim T" obtains f where"linear f""f ` S = T""∧x. x ∈ S ==> norm(f x) = norm x" using isometries_subspaces [OF assms] by metis
lemma homeomorphic_subspaces: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes S: "subspace S" and T: "subspace T" and d: "dim S = dim T" shows"S homeomorphic T" proof - obtain f g where"linear f""linear g""f ` S = T""g ` T = S" "∧x. x ∈ S ==> g(f x) = x""∧x. x ∈ T ==> f(g x) = x" by (blast intro: isometries_subspaces [OF assms]) thenshow ?thesis unfolding homeomorphic_def homeomorphism_def apply (rule_tac x=f in exI, rule_tac x=g in exI) apply (auto simp: linear_continuous_on linear_conv_bounded_linear) done qed
lemma homeomorphic_affine_sets: assumes"affine S""affine T""aff_dim S = aff_dim T" shows"S homeomorphic T" proof (cases "S = {} ∨ T = {}") case True with assms aff_dim_empty homeomorphic_empty show ?thesis by metis next case False thenobtain a b where ab: "a ∈ S""b ∈ T"by auto thenhave ss: "subspace ((+) (- a) ` S)""subspace ((+) (- b) ` T)" using affine_diffs_subspace assms by blast+ have dd: "dim ((+) (- a) ` S) = dim ((+) (- b) ` T)" using assms ab by (simp add: aff_dim_eq_dim [OF hull_inc] image_def) have"S homeomorphic ((+) (- a) ` S)" by (fact homeomorphic_translation) alsohave"… homeomorphic ((+) (- b) ` T)" by (rule homeomorphic_subspaces [OF ss dd]) alsohave"… homeomorphic T" using homeomorphic_translation [of T "- b"] by (simp add: homeomorphic_sym [of T]) finallyshow ?thesis . qed
subsection‹Retracts, in a general sense, preserve (co)homotopic triviality)›
locale✐‹tag important› Retracts = fixes S h t k assumes conth: "continuous_on S h" and imh: "h ` S = t" and contk: "continuous_on t k" and imk: "k ∈ t → S" and idhk: "∧y. y ∈ t ==> h(k y) = y"
begin
lemma homotopically_trivial_retraction_gen: assumes P: "∧f. [continuous_on U f; f ∈ U → t; Q f]==> P(k ∘ f)" and Q: "∧f. [continuous_on U f; f ∈ U → S; P f]==> Q(h ∘ f)" and Qeq: "∧h k. (∧x. x ∈ U ==> h x = k x) ==> Q h = Q k" and hom: "∧f g. [continuous_on U f; f ∈ U → S; P f; continuous_on U g; g ∈ U → S; P g] ==> homotopic_with_canon P U S f g" and contf: "continuous_on U f"and imf: "f ∈ U → t"and Qf: "Q f" and contg: "continuous_on U g"and img: "g ∈ U → t"and Qg: "Q g" shows"homotopic_with_canon Q U t f g" proof - have"continuous_on U (k ∘ f)" by (meson contf continuous_on_compose continuous_on_subset contk funcset_image imf) moreoverhave"(k ∘ f) ` U ⊆ S" using imf imk by fastforce moreoverhave"P (k ∘ f)" by (simp add: P Qf contf imf) moreoverhave"continuous_on U (k ∘ g)" by (meson contg continuous_on_compose continuous_on_subset contk funcset_image img) moreoverhave"(k ∘ g) ` U ⊆ S" using img imk by fastforce moreoverhave"P (k ∘ g)" by (simp add: P Qg contg img) ultimatelyhave"homotopic_with_canon P U S (k ∘ f) (k ∘ g)" by (simp add: hom image_subset_iff) thenhave"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 conth imh by force+ thenshow ?thesis proof (rule homotopic_with_eq; simp) show"∧h k. (∧x. x ∈ U ==> h x = k x) ==> Q h = Q k" using Qeq topspace_euclidean_subtopology by blast show"∧x. x ∈ U ==> f x = h (k (f x))""∧x. x ∈ U ==> g x = h (k (g x))" using idhk imf img by fastforce+ qed qed
lemma homotopically_trivial_retraction_null_gen: assumes P: "∧f. [continuous_on U f; f ∈ U → t; Q f]==> P(k ∘ f)" and Q: "∧f. [continuous_on U f; f ∈ U → S; P f]==> Q(h ∘ f)" and Qeq: "∧h k. (∧x. x ∈ U ==> h x = k x) ==> Q h = Q k" and hom: "∧f. [continuous_on U f; f ∈ U → S; P f] ==>∃c. homotopic_with_canon P U S f (λx. c)" and contf: "continuous_on U f"and imf:"f ∈ U → t"and Qf: "Q f" obtains c where"homotopic_with_canon Q U t f (λx. c)" proof - have feq: "∧x. x ∈ U ==> (h ∘ (k ∘ f)) x = f x"using idhk imf by auto have"continuous_on U (k ∘ f)" by (meson contf continuous_on_compose continuous_on_subset contk funcset_image imf) moreoverhave"(k ∘ f) ∈ U → S" using imf imk by fastforce moreoverhave"P (k ∘ f)" by (simp add: P Qf contf imf) ultimatelyobtain c where"homotopic_with_canon P U S (k ∘ f) (λx. c)" by (metis hom) thenhave"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 conth imh by force+ thenhave"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" using feq by auto show"∧h k. (∧x. x ∈ topspace (top_of_set U) ==> h x = k x) ==> Q h = Q k" using Qeq topspace_euclidean_subtopology by blast qed auto thenshow ?thesis using that by blast qed
lemma cohomotopically_trivial_retraction_gen: assumes P: "∧f. [continuous_on t f; f ∈ t → U; Q f]==> P(f ∘ h)" and Q: "∧f. [continuous_on S f; f ∈ S → U; P f]==> Q(f ∘ k)" and Qeq: "∧h k. (∧x. x ∈ t ==> h x = k x) ==> Q h = Q k" and hom: "∧f g. [continuous_on S f; f ∈ S → U; P f; continuous_on S g; g ∈ S → U; P g] ==> homotopic_with_canon P S U f g" and contf: "continuous_on t f"and imf: "f ∈ t → U"and Qf: "Q f" and contg: "continuous_on t g"and img: "g ∈ t → U"and Qg: "Q g" shows"homotopic_with_canon Q t U f g" proof - have feq: "∧x. x ∈ t ==> (f ∘ h ∘ k) x = f x"using idhk imf by auto have geq: "∧x. x ∈ t ==> (g ∘ h ∘ k) x = g x"using idhk img by auto have"continuous_on S (f ∘ h)" using contf conth continuous_on_compose imh by blast moreoverhave"(f ∘ h) ∈ S → U" using imf imh by fastforce moreoverhave"P (f ∘ h)" by (simp add: P Qf contf imf) moreoverhave"continuous_on S (g ∘ h)" using contg continuous_on_compose continuous_on_subset conth imh by blast moreoverhave"(g ∘ h) ∈ S → U" using img imh by fastforce moreoverhave"P (g ∘ h)" by (simp add: P Qg contg img) ultimatelyhave"homotopic_with_canon P S U (f ∘ h) (g ∘ h)" by (simp add: hom) thenhave"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 contk imk by force+ thenshow ?thesis proof (rule homotopic_with_eq) show"f x = (f ∘ h ∘ k) x""g x = (g ∘ h ∘ k) x" if"x ∈ topspace (top_of_set t)"for x using feq geq that by force+ qed (use Qeq topspace_euclidean_subtopology in blast) qed
lemma cohomotopically_trivial_retraction_null_gen: assumes P: "∧f. [continuous_on t f; f ∈ t → U; Q f]==> P(f ∘ h)" and Q: "∧f. [continuous_on S f; f ∈ S → U; P f]==> Q(f ∘ k)" and Qeq: "∧h k. (∧x. x ∈ t ==> h x = k x) ==> Q h = Q k" and hom: "∧f g. [continuous_on S f; f ∈ S → U; P f] ==>∃c. homotopic_with_canon P S U f (λx. c)" and contf: "continuous_on t f"and imf: "f ∈ t → U"and Qf: "Q f" obtains c where"homotopic_with_canon Q t U f (λx. c)" proof - have feq: "∧x. x ∈ t ==> (f ∘ h ∘ k) x = f x"using idhk imf by auto have"continuous_on S (f ∘ h)" using contf conth continuous_on_compose imh by blast moreoverhave"(f ∘ h) ∈ S → U" using imf imh by fastforce moreoverhave"P (f ∘ h)" by (simp add: P Qf contf imf) ultimatelyobtain c where"homotopic_with_canon P S U (f ∘ h) (λx. c)" by (metis hom) thenhave§: "homotopic_with_canon Q t U (f ∘ h ∘ k) ((λx. c) ∘ k)" 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 (use contk imk in force)+ moreoverhave"homotopic_with_canon Q t U f (λx. c)" using homotopic_with_eq [OF §] feq Qeq by fastforce ultimatelyshow ?thesis using that by blast qed
end
lemma simply_connected_retraction_gen: shows"[simply_connected S; continuous_on S h; h ` S = T; continuous_on T k; k ∈ T → S; ∧y. y ∈ T ==> h(k y) = y] ==> simply_connected T" apply (simp add: simply_connected_def path_def path_image_def homotopic_loops_def, clarify) apply (rule Retracts.homotopically_trivial_retraction_gen
[of S h _ k _ "λp. pathfinish p = pathstart p""λp. pathfinish p = pathstart p"]) apply (simp_all add: Retracts_def pathfinish_def pathstart_def image_subset_iff_funcset) done
lemma homeomorphic_simply_connected_eq: "S homeomorphic T ==> (simply_connected S ⟷ simply_connected T)" by (metis homeomorphic_simply_connected homeomorphic_sym)
subsection‹Homotopy equivalence›
subsection‹Homotopy equivalence of topological spaces.›
definition✐‹tag important› homotopy_equivalent_space
(infix‹homotopy'_equivalent'_space›50) where"X homotopy_equivalent_space Y ≡ (∃f g. continuous_map X Y f ∧ continuous_map Y X g ∧ homotopic_with (λx. True) X X (g ∘ f) id ∧ homotopic_with (λx. True) Y Y (f ∘ g) id)"
lemma homeomorphic_imp_homotopy_equivalent_space: "X homeomorphic_space Y ==> X homotopy_equivalent_space Y" unfolding homeomorphic_space_def homotopy_equivalent_space_def apply (erule ex_forward)+ by (simp add: homotopic_with_equal homotopic_with_sym homeomorphic_maps_def)
lemma homotopy_equivalent_space_refl: "X homotopy_equivalent_space X" by (simp add: homeomorphic_imp_homotopy_equivalent_space homeomorphic_space_refl)
lemma homotopy_equivalent_space_sym: "X homotopy_equivalent_space Y ⟷ Y homotopy_equivalent_space X" by (meson homotopy_equivalent_space_def)
lemma homotopy_eqv_trans [trans]: assumes1: "X homotopy_equivalent_space Y"and2: "Y homotopy_equivalent_space U" shows"X homotopy_equivalent_space U" proof - obtain f1 g1 where f1: "continuous_map X Y f1" and g1: "continuous_map Y X g1" and hom1: "homotopic_with (λx. True) X X (g1 ∘ f1) id" "homotopic_with (λx. True) Y Y (f1 ∘ g1) id" using1by (auto simp: homotopy_equivalent_space_def) obtain f2 g2 where f2: "continuous_map Y U f2" and g2: "continuous_map U Y g2" and hom2: "homotopic_with (λx. True) Y Y (g2 ∘ f2) id" "homotopic_with (λx. True) U U (f2 ∘ g2) id" using2by (auto simp: homotopy_equivalent_space_def) have"homotopic_with (λf. True) X Y (g2 ∘ f2 ∘ f1) (id ∘ f1)" using f1 hom2(1) homotopic_with_compose_continuous_map_right by metis thenhave"homotopic_with (λf. True) X Y (g2 ∘ (f2 ∘ f1)) (id ∘ f1)" by (simp add: o_assoc) thenhave"homotopic_with (λx. True) X X (g1 ∘ (g2 ∘ (f2 ∘ f1))) (g1 ∘ (id ∘ f1))" by (simp add: g1 homotopic_with_compose_continuous_map_left) moreoverhave"homotopic_with (λx. True) X X (g1 ∘ id ∘ f1) id" using hom1 by simp ultimatelyhave SS: "homotopic_with (λx. True) X X (g1 ∘ g2 ∘ (f2 ∘ f1)) id" by (metis comp_assoc homotopic_with_trans id_comp) have"homotopic_with (λf. True) U Y (f1 ∘ g1 ∘ g2) (id ∘ g2)" using g2 hom1(2) homotopic_with_compose_continuous_map_right by fastforce thenhave"homotopic_with (λf. True) U Y (f1 ∘ (g1 ∘ g2)) (id ∘ g2)" by (simp add: o_assoc) thenhave"homotopic_with (λx. True) U U (f2 ∘ (f1 ∘ (g1 ∘ g2))) (f2 ∘ (id ∘ g2))" by (simp add: f2 homotopic_with_compose_continuous_map_left) moreoverhave"homotopic_with (λx. True) U U (f2 ∘ id ∘ g2) id" using hom2 by simp ultimatelyhave UU: "homotopic_with (λx. True) U U (f2 ∘ f1 ∘ (g1 ∘ g2)) id" by (simp add: fun.map_comp hom2(2) homotopic_with_trans) show ?thesis unfolding homotopy_equivalent_space_def by (blast intro: f1 f2 g1 g2 continuous_map_compose SS UU) qed
lemma deformation_retraction_imp_homotopy_equivalent_space: "[homotopic_with (λx. True) X X (S ∘ r) id; retraction_maps X Y r S] ==> X homotopy_equivalent_space Y" unfolding homotopy_equivalent_space_def retraction_maps_def using homotopic_with_id2 by fastforce
lemma deformation_retract_imp_homotopy_equivalent_space: "[homotopic_with (λx. True) X X r id; retraction_maps X Y r id] ==> X homotopy_equivalent_space Y" using deformation_retraction_imp_homotopy_equivalent_space by force
lemma deformation_retract_of_space: "S ⊆ topspace X ∧ (∃r. homotopic_with (λx. True) X X id r ∧ retraction_maps X (subtopology X S) r id) ⟷ S retract_of_space X ∧ (∃f. homotopic_with (λx. True) X X id f ∧ f ` (topspace X)⊆ S)" proof (cases "S ⊆ topspace X") case True moreoverhave"(∃r. homotopic_with (λx. True) X X id r ∧ retraction_maps X (subtopology X S) r id) ⟷ (S retract_of_space X ∧ (∃f. homotopic_with (λx. True) X X id f ∧ f ` topspace X ⊆ S))" unfolding retract_of_space_def proof safe fix f r assume f: "homotopic_with (λx. True) X X id f" and fS: "f ` topspace X ⊆ S" and r: "continuous_map X (subtopology X S) r" and req: "∀x∈S. r x = x" show"∃r. homotopic_with (λx. True) X X id r ∧ retraction_maps X (subtopology X S) r id" proof (intro exI conjI) have"homotopic_with (λx. True) X X f r" proof (rule homotopic_with_eq) show"homotopic_with (λx. True) X X (r ∘ f) (r ∘ id)" by (metis continuous_map_into_fulltopology f homotopic_with_compose_continuous_map_left homotopic_with_symD r) show"f x = (r ∘ f) x"if"x ∈ topspace X"for x using that fS req by auto qed auto thenshow"homotopic_with (λx. True) X X id r" by (rule homotopic_with_trans [OF f]) next show"retraction_maps X (subtopology X S) r id" by (simp add: r req retraction_maps_def) qed qed (use True in‹auto simp: retraction_maps_def topspace_subtopology_subset continuous_map_in_subtopology›) ultimatelyshow ?thesis by simp qed (auto simp: retract_of_space_def retraction_maps_def)
subsection‹Contractible spaces›
text‹The definition (which agrees with "contractible" on subsets of Euclidean space)
a little cryptic because we don't in fact assume that the constant "a" is in the space.
forces the convention that the empty space / set is contractible, avoiding some special cases. ›
definition contractible_space where "contractible_space X ≡∃a. homotopic_with (λx. True) X X id (λx. a)"
lemma contractible_space_empty [simp]: "contractible_space trivial_topology" unfolding contractible_space_def homotopic_with_def apply (rule_tac x=undefined in exI) apply (rule_tac x="λ(t,x). if t = 0 then x else undefined"in exI) apply (auto simp: continuous_map_on_empty) done
lemma contractible_space_singleton [simp]: "contractible_space (discrete_topology{a})" unfolding contractible_space_def homotopic_with_def apply (rule_tac x=a in exI) apply (rule_tac x="λ(t,x). if t = 0 then x else a"in exI) apply (auto intro: continuous_map_eq [where f = "λz. a"]) done
lemma contractible_space_subset_singleton: "topspace X ⊆ {a} ==> contractible_space X" by (metis contractible_space_empty contractible_space_singleton null_topspace_iff_trivial subset_singletonD subtopology_eq_discrete_topology_sing)
lemma contractible_space_subtopology_singleton [simp]: "contractible_space (subtopology X {a})" by (meson contractible_space_subset_singleton insert_subset path_connectedin_singleton path_connectedin_subtopology subsetI)
lemma contractible_space: "contractible_space X ⟷ X = trivial_topology ∨ (∃a ∈ topspace X. homotopic_with (λx. True) X X id (λx. a))" proof (cases "X = trivial_topology") case False thenshow ?thesis using homotopic_with_imp_continuous_maps by (fastforce simp: contractible_space_def) qed (simp add: contractible_space_empty)
lemma contractible_imp_path_connected_space: assumes"contractible_space X"shows"path_connected_space X" proof (cases "X = trivial_topology") case False have *: "path_connected_space X" if"a ∈ topspace X"and conth: "continuous_map (prod_topology (top_of_set {0..1}) X) X h" and h: "∀x. h (0, x) = x""∀x. h (1, x) = a" for a and h :: "real × 'a → 'a" proof - have"path_component_of X b a"if"b ∈ topspace X"for b unfolding path_component_of_def proof (intro exI conjI) let ?g = "h ∘ (λx. (x,b))" show"pathin X ?g" unfolding pathin_def proof (rule continuous_map_compose [OF _ conth]) show"continuous_map (top_of_set {0..1}) (prod_topology (top_of_set {0..1}) X) (λx. (x, b))" using that by (auto intro!: continuous_intros) qed qed (use h in auto) thenshow ?thesis by (metis path_component_of_equiv path_connected_space_iff_path_component) qed show ?thesis using assms False by (auto simp: contractible_space homotopic_with_def *) qed (simp add: path_connected_space_topspace_empty)
lemma contractible_imp_connected_space: "contractible_space X ==> connected_space X" by (simp add: contractible_imp_path_connected_space path_connected_imp_connected_space)
lemma contractible_space_alt: "contractible_space X ⟷ (∀a ∈ topspace X. homotopic_with (λx. True) X X id (λx. a))" (is"?lhs = ?rhs") proof assume X: ?lhs thenobtain a where a: "homotopic_with (λx. True) X X id (λx. a)" by (auto simp: contractible_space_def) show ?rhs proof show"homotopic_with (λx. True) X X id (λx. b)"if"b ∈ topspace X"for b proof (rule homotopic_with_trans [OF a]) show"homotopic_with (λx. True) X X (λx. a) (λx. b)" using homotopic_constant_maps path_connected_space_imp_path_component_of by (metis X a contractible_imp_path_connected_space homotopic_with_sym homotopic_with_trans path_component_of_equiv that) qed qed next assume R: ?rhs thenshow ?lhs using contractible_space_def by fastforce qed
lemma compose_const [simp]: "f ∘ (λx. a) = (λx. f a)""(λx. a) ∘ g = (λx. a)" by (simp_all add: o_def)
lemma nullhomotopic_through_contractible_space: assumes f: "continuous_map X Y f"and g: "continuous_map Y Z g"and Y: "contractible_space Y" obtains c where"homotopic_with (λh. True) X Z (g ∘ f) (λx. c)" proof - obtain b where b: "homotopic_with (λx. True) Y Y id (λx. b)" using Y by (auto simp: contractible_space_def) show thesis using homotopic_with_compose_continuous_map_right
[OF homotopic_with_compose_continuous_map_left [OF b g] f] by (force simp: that) qed
lemma nullhomotopic_into_contractible_space: assumes f: "continuous_map X Y f"and Y: "contractible_space Y" obtains c where"homotopic_with (λh. True) X Y f (λx. c)" using nullhomotopic_through_contractible_space [OF f _ Y] by (metis continuous_map_id id_comp)
lemma nullhomotopic_from_contractible_space: assumes f: "continuous_map X Y f"and X: "contractible_space X" obtains c where"homotopic_with (λh. True) X Y f (λx. c)" using nullhomotopic_through_contractible_space [OF _ f X] by (metis comp_id continuous_map_id)
lemma homotopy_dominated_contractibility: assumes f: "continuous_map X Y f"and g: "continuous_map Y X g" and hom: "homotopic_with (λx. True) Y Y (f ∘ g) id"and X: "contractible_space X" shows"contractible_space Y" proof - obtain c where c: "homotopic_with (λh. True) X Y f (λx. c)" using nullhomotopic_from_contractible_space [OF f X] . have"homotopic_with (λx. True) Y Y (f ∘ g) (λx. c)" using homotopic_with_compose_continuous_map_right [OF c g] by fastforce thenhave"homotopic_with (λx. True) Y Y id (λx. c)" using homotopic_with_trans [OF _ hom] homotopic_with_symD by blast thenshow ?thesis unfolding contractible_space_def .. qed
lemma homotopy_equivalent_space_contractibility: "X homotopy_equivalent_space Y ==> (contractible_space X ⟷ contractible_space Y)" unfolding homotopy_equivalent_space_def by (blast intro: homotopy_dominated_contractibility)
lemma homeomorphic_space_contractibility: "X homeomorphic_space Y ==> (contractible_space X ⟷ contractible_space Y)" by (simp add: homeomorphic_imp_homotopy_equivalent_space homotopy_equivalent_space_contractibility)
lemma homotopic_through_contractible_space: "continuous_map X Y f ∧ continuous_map X Y f' ∧ continuous_map Y Z g ∧ continuous_map Y Z g' ∧ contractible_space Y ∧ path_connected_space Z ==> homotopic_with (λh. True) X Z (g ∘ f) (g' ∘ f')" using nullhomotopic_through_contractible_space [of X Y f Z g] using nullhomotopic_through_contractible_space [of X Y f' Z g'] by (smt (verit) continuous_map_const homotopic_constant_maps homotopic_with_imp_continuous_maps
homotopic_with_symD homotopic_with_trans path_connected_space_imp_path_component_of)
lemma homotopic_from_contractible_space: "continuous_map X Y f ∧ continuous_map X Y g ∧ contractible_space X ∧ path_connected_space Y ==> homotopic_with (λx. True) X Y f g" by (metis comp_id continuous_map_id homotopic_through_contractible_space)
lemma homotopic_into_contractible_space: "continuous_map X Y f ∧ continuous_map X Y g ∧ contractible_space Y ==> homotopic_with (λx. True) X Y f g" by (metis continuous_map_id contractible_imp_path_connected_space homotopic_through_contractible_space id_comp)
lemma contractible_eq_homotopy_equivalent_singleton_subtopology: "contractible_space X ⟷ X = trivial_topology ∨ (∃a ∈ topspace X. X homotopy_equivalent_space (subtopology X {a}))"(is"?lhs = ?rhs") proof (cases "X = trivial_topology") case False show ?thesis proof assume ?lhs thenobtain a where a: "homotopic_with (λx. True) X X id (λx. a)" by (auto simp: contractible_space_def) thenhave"a ∈ topspace X" by (metis False continuous_map_const homotopic_with_imp_continuous_maps) thenhave"homotopic_with (λx. True) (subtopology X {a}) (subtopology X {a}) id (λx. a)" using connectedin_absolute connectedin_sing contractible_space_alt contractible_space_subtopology_singleton by fastforce thenhave"X homotopy_equivalent_space subtopology X {a}" unfolding homotopy_equivalent_space_def using‹a ∈ topspace X› by (metis (full_types) a comp_id continuous_map_const continuous_map_id_subt empty_subsetI homotopic_with_symD
id_comp insertI1 insert_subset topspace_subtopology_subset) with‹a ∈ topspace X›show ?rhs by blast next assume ?rhs thenshow ?lhs by (meson False contractible_space_subtopology_singleton homotopy_equivalent_space_contractibility) qed qed (simp add: contractible_space_empty)
lemma contractible_space_retraction_map_image: assumes"retraction_map X Y f"and X: "contractible_space X" shows"contractible_space Y" proof - obtain g where f: "continuous_map X Y f"and g: "continuous_map Y X g"and fg: "∀y ∈ topspace Y. f(g y) = y" using assms by (auto simp: retraction_map_def retraction_maps_def) obtain a where a: "homotopic_with (λx. True) X X id (λx. a)" using X by (auto simp: contractible_space_def) have"homotopic_with (λx. True) Y Y id (λx. f a)" proof (rule homotopic_with_eq) show"homotopic_with (λx. True) Y Y (f ∘ id ∘ g) (f ∘ (λx. a) ∘ g)" using f g a homotopic_with_compose_continuous_map_left homotopic_with_compose_continuous_map_right by metis qed (use fg in auto) thenshow ?thesis unfolding contractible_space_def by blast qed
lemma contractible_space_prod_topology: "contractible_space(prod_topology X Y) ⟷ X = trivial_topology ∨ Y = trivial_topology ∨ contractible_space X ∧ contractible_space Y" proof (cases "X = trivial_topology ∨ Y = trivial_topology") case True thenhave"(prod_topology X Y) = trivial_topology" by simp thenshow ?thesis by (auto simp: contractible_space_empty) next case False have"contractible_space(prod_topology X Y) ⟷ contractible_space X ∧ contractible_space Y" proof safe assume XY: "contractible_space (prod_topology X Y)" with False have"retraction_map (prod_topology X Y) X fst" by (auto simp: contractible_space False retraction_map_fst) thenshow"contractible_space X" by (rule contractible_space_retraction_map_image [OF _ XY]) have"retraction_map (prod_topology X Y) Y snd" using False XY by (auto simp: contractible_space False retraction_map_snd) thenshow"contractible_space Y" by (rule contractible_space_retraction_map_image [OF _ XY]) next assume"contractible_space X"and"contractible_space Y" with False obtain a b where"a ∈ topspace X"and a: "homotopic_with (λx. True) X X id (λx. a)" and"b ∈ topspace Y"and b: "homotopic_with (λx. True) Y Y id (λx. b)" by (auto simp: contractible_space) with False show"contractible_space (prod_topology X Y)" apply (simp add: contractible_space) apply (rule_tac x=a in bexI) apply (rule_tac x=b in bexI) using homotopic_with_prod_topology [OF a b] apply (metis (no_types, lifting) case_prod_Pair case_prod_beta' eq_id_iff) apply auto done qed with False show ?thesis by auto qed
lemma contractible_space_product_topology: "contractible_space(product_topology X I) ⟷ (product_topology X I) = trivial_topology ∨ (∀i ∈ I. contractible_space(X i))" proof (cases "(product_topology X I) = trivial_topology") case False have1: "contractible_space (X i)" if XI: "contractible_space (product_topology X I)"and"i ∈ I" for i proof (rule contractible_space_retraction_map_image [OF _ XI]) show"retraction_map (product_topology X I) (X i) (λx. x i)" using False by (simp add: retraction_map_product_projection ‹i ∈ I›) qed have2: "contractible_space (product_topology X I)" if"x ∈ topspace (product_topology X I)"and cs: "∀i∈I. contractible_space (X i)" for x :: "'a → 'b" proof - obtain f where f: "∧i. i∈I ==> homotopic_with (λx. True) (X i) (X i) id (λx. f i)" using cs unfolding contractible_space_def by metis have"homotopic_with (λx. True) (product_topology X I) (product_topology X I) id (λx. restrict f I)" by (rule homotopic_with_eq [OF homotopic_with_product_topology [OF f]]) (auto) thenshow ?thesis by (auto simp: contractible_space_def) qed show ?thesis using False 12by (meson equals0I subtopology_eq_discrete_topology_empty) qed auto
lemma contractible_space_subtopology_euclideanreal [simp]: "contractible_space(subtopology euclideanreal S) ⟷ is_interval S"
(is"?lhs = ?rhs") proof assume ?lhs thenhave"path_connectedin (subtopology euclideanreal S) S" using contractible_imp_path_connected_space path_connectedin_topspace path_connectedin_absolute by (simp add: contractible_imp_path_connected) thenshow ?rhs by (simp add: is_interval_path_connected_1) next assume ?rhs thenhave"convex S" by (simp add: is_interval_convex_1) show ?lhs proof (cases "S = {}") case False thenobtain z where"z ∈ S" by blast show ?thesis unfolding contractible_space_def homotopic_with_def proof (intro exI conjI allI) note§ = convexD [OF ‹convex S›, simplified] show"continuous_map (prod_topology (top_of_set {0..1}) (top_of_set S)) (top_of_set S) (λ(t,x). (1 - t) * x + t * z)" using‹z ∈ S› by (auto simp: case_prod_unfold intro!: continuous_intros §) qed auto qed (simp add: contractible_space_empty) qed
corollary contractible_space_euclideanreal: "contractible_space euclideanreal" proof - have"contractible_space (subtopology euclideanreal UNIV)" using contractible_space_subtopology_euclideanreal by blast thenshow ?thesis by simp qed
abbreviation✐‹tag important› homotopy_eqv :: "'a::topological_space set → 'b::topological_space set → bool"
(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 apply (erule ex_forward)+ by (metis continuous_map_subtopology_eu homotopic_with_id2 openin_imp_subset openin_subtopology_self topspace_euclidean_subtopology
image_subset_iff_funcset)
lemma homotopy_eqv_translation: fixes S :: "'a::real_normed_vector set" shows"(+) a ` S homotopy_eqv S" using homeomorphic_imp_homotopy_eqv homeomorphic_translation homeomorphic_sym by blast
lemma homotopy_eqv_homotopic_triviality_imp: fixes S :: "'a::real_normed_vector set" 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] ==> 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" 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 (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 (metis funcset_image)+ qed (use f g k in‹(force simp: o_def)+› ) thenhave"homotopic_with_canon (λx. True) U T (h ∘ (k ∘ f)) (h ∘ (k ∘ g))" by (simp add: h homotopic_with_compose_continuous_map_left image_subset_iff_funcset) moreoverhave"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) moreoverhave"homotopic_with_canon (λx. True) U T (h ∘ k ∘ g) (id ∘ g)" by (rule homotopic_with_compose_continuous_right [where X=T and Y=T]; simp add: hom g) ultimatelyshow"homotopic_with_canon (λx. True) U T f g" unfolding o_assoc by (metis homotopic_with_trans homotopic_with_sym id_comp) qed
lemma homotopy_eqv_homotopic_triviality: fixes S :: "'a::real_normed_vector set" 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 ⟶ 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 ⟶ homotopic_with_canon (λx. True) U T f g)"
(is"?lhs = ?rhs") proof assume ?lhs thenshow ?rhs by (metis assms homotopy_eqv_homotopic_triviality_imp) next assume ?rhs moreover have"T homotopy_eqv S" using assms homotopy_equivalent_space_sym by blast ultimatelyshow ?lhs by (blast intro: homotopy_eqv_homotopic_triviality_imp) qed
lemma homotopy_eqv_cohomotopic_triviality_null_imp: fixes S :: "'a::real_normed_vector set" 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] ==>∃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" 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 (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)" by (metis continuous_on_compose continuous_on_subset f h funcset_image) qed (use f h in force) thenhave"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) moreoverhave"homotopic_with_canon (λx. True) T U (f ∘ id) (f ∘ (h ∘ k))" by (rule homotopic_with_compose_continuous_left [where Y=T])
(use f in‹auto simp: hom homotopic_with_symD›) ultimatelyshow ?thesis using that homotopic_with_trans by (fastforce simp: o_def) qed
lemma homotopy_eqv_cohomotopic_triviality_null: fixes S :: "'a::real_normed_vector set" 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 ⟶ (∃c. homotopic_with_canon (λx. True) S U f (λx. c))) ⟷ (∀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)
text‹Similar to the proof above› lemma homotopy_eqv_homotopic_triviality_null_imp: fixes S :: "'a::real_normed_vector set" 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] ==>∃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" 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 (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 (metis funcset_image) qed (use f k in force) thenhave"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) moreoverhave"homotopic_with_canon (λx. True) U T (id ∘ f) ((h ∘ k) ∘ f)" by (rule homotopic_with_compose_continuous_right [where X=T])
(use f in‹auto simp: hom homotopic_with_symD›) ultimatelyshow ?thesis using homotopic_with_trans by (fastforce simp: o_def) qed
lemma homotopy_eqv_homotopic_triviality_null: fixes S :: "'a::real_normed_vector set" 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 ⟶ (∃c. homotopic_with_canon (λx. True) U S f (λx. c))) ⟷ (∀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)
lemma homotopy_eqv_contractible_sets: fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set" assumes"contractible S""contractible T""S = {} ⟷ T = {}" shows"S homotopy_eqv T" proof (cases "S = {}") case True with assms show ?thesis using homeomorphic_imp_homotopy_eqv by fastforce next case False with assms obtain a b where"a ∈ S""b ∈ T" by auto thenshow ?thesis unfolding homotopy_equivalent_space_def apply (rule_tac x="λx. b"in exI, rule_tac x="λx. a"in exI) apply (intro assms conjI continuous_on_id' homotopic_into_contractible; force) done qed
lemma homotopy_eqv_empty1 [simp]: fixes S :: "'a::real_normed_vector set" shows"S homotopy_eqv ({}::'b::real_normed_vector set) ⟷ S = {}" (is"?lhs = ?rhs") proof assume ?lhs thenshow ?rhs by (meson continuous_map_subtopology_eu equals0D equals0I funcset_mem
homotopy_equivalent_space_def) qed (use homeomorphic_imp_homotopy_eqv in force)
lemma homotopy_eqv_empty2 [simp]: fixes S :: "'a::real_normed_vector set" shows"({}::'b::real_normed_vector set) homotopy_eqv S ⟷ S = {}" using homotopy_equivalent_space_sym homotopy_eqv_empty1 by blast
lemma homotopy_eqv_contractibility: fixes S :: "'a::real_normed_vector set"and T :: "'b::real_normed_vector set" shows"S homotopy_eqv T ==> (contractible S ⟷ contractible T)" by (meson contractible_space_top_of_set homotopy_equivalent_space_contractibility)
lemma homotopy_eqv_sing: fixes S :: "'a::real_normed_vector set"and a :: "'b::real_normed_vector" shows"S homotopy_eqv {a} ⟷ S ≠ {} ∧ contractible S" by (metis contractible_sing empty_not_insert homotopy_eqv_contractibility homotopy_eqv_contractible_sets homotopy_eqv_empty2)
lemma homeomorphic_contractible_eq: fixes S :: "'a::real_normed_vector set"and T :: "'b::real_normed_vector set" shows"S homeomorphic T ==> (contractible S ⟷ contractible T)" by (simp add: homeomorphic_imp_homotopy_eqv homotopy_eqv_contractibility)
lemma homeomorphic_contractible: fixes S :: "'a::real_normed_vector set"and T :: "'b::real_normed_vector set" shows"[contractible S; S homeomorphic T]==> contractible T" by (metis homeomorphic_contractible_eq)
subsection✐‹tag unimportant›\<open>Misc other results›
lemma bounded_connected_Compl_real: fixes S :: "real set" assumes"bounded S"and conn: "connected(- S)" shows"S = {}" proof - obtain a b where"S ⊆ box a b" by (meson assms bounded_subset_box_symmetric) thenhave"a ∉ S""b ∉ S" by auto thenhave"∀x. a ≤ x ∧ x ≤ b ⟶ x ∈ - S" by (meson Compl_iff conn connected_iff_interval) thenshow ?thesis using‹S ⊆ box a b› by auto qed
proposition\<^marker>\<open>tagunimportant\<close>homeomorphism_moving_point: fixesa::"'a::euclidean_space" assumesope:"openin(top_of_set(affinehullS))S" and"S\<subseteq>T" andTS:"T\<subseteq>affinehullS" andS:"connectedS""a\<in>S""b\<in>S" obtainsfgwhere"homeomorphismTTfg""fa=b" "{x.\<not>(fx=x\<and>gx=x)}\<subseteq>S" "bounded{x.\<not>(fx=x\<and>gx=x)}" proof- have1:"\<exists>hk.homeomorphismTThk\<and>h(fd)=d\<and> {x.\<not>(hx=x\<and>kx=x)}\<subseteq>S\<and>bounded{x.\<not>(hx=x\<and>kx=x)}" if"d\<in>S""fd\<in>S"andhomfg:"homeomorphismTTfg" andS:"{x.\<not>(fx=x\<and>gx=x)}\<subseteq>S" andbo:"bounded{x.\<not>(fx=x\<and>gx=x)}"fordfg proof(introexIconjI) showhomgf:"homeomorphismTTgf" by(metishomeomorphism_symDhomfg) thenshow"g(fd)=d" by(meson\<open>S\<subseteq>T\<close>homeomorphism_defsubsetD\<open>d\<in>S\<close>) show"{x.\<not>(gx=x\<and>fx=x)}\<subseteq>S" usingSbyblast show"bounded{x.\<not>(gx=x\<and>fx=x)}" usingboby(simpadd:conj_commute) qed have2:"\<exists>fg.homeomorphismTTfg\<and>fx=f2(f1x)\<and> {x.\<not>(fx=x\<and>gx=x)}\<subseteq>S\<and>bounded{x.\<not>(fx=x\<and>gx=x)}" if"x\<in>S""f1x\<in>S""f2(f1x)\<in>S" andhom:"homeomorphismTTf1g1""homeomorphismTTf2g2" andsub:"{x.\<not>(f1x=x\<and>g1x=x)}\<subseteq>S""{x.\<not>(f2x=x\<and>g2x=x)}\<subseteq>S" andbo:"bounded{x.\<not>(f1x=x\<and>g1x=x)}""bounded{x.\<not>(f2x=x\<and>g2x=x)}" forxf1f2g1g2 proof(introexIconjI) showhomgf:"homeomorphismTT(f2\<circ>f1)(g1\<circ>g2)" by(metishomeomorphism_composehom) thenshow"(f2\<circ>f1)x=f2(f1x)" byforce show"{x.\<not>((f2\<circ>f1)x=x\<and>(g1\<circ>g2)x=x)}\<subseteq>S" usingsubbyforce have"bounded({x.\<not>(f1x=x\<and>g1x=x)}\<union>{x.\<not>(f2x=x\<and>g2x=x)})" usingbobysimp thenshow"bounded{x.\<not>((f2\<circ>f1)x=x\<and>(g1\<circ>g2)x=x)}" by(rulebounded_subset)auto qed have3:"\<exists>U.openin(top_of_setS)U\<and> d\<in>U\<and> (\<forall>x\<in>U. \<exists>fg.homeomorphismTTfg\<and>fd=x\<and> {x.\<not>(fx=x\<and>gx=x)}\<subseteq>S\<and> bounded{x.\<not>(fx=x\<and>gx=x)})" if"d\<in>S"ford proof- obtainrwhere"r>0"andr:"balldr\<inter>affinehullS\<subseteq>S" by(metis\<open>d\<in>S\<close>opeopenin_contains_ball) have*:"\<exists>fg.homeomorphismTTfg\<and>fd=e\<and> {x.\<not>(fx=x\<and>gx=x)}\<subseteq>S\<and> bounded{x.\<not>(fx=x\<and>gx=x)}"if"e\<in>S""e\<in>balldr"fore apply(rulehomeomorphism_moving_point_3[of"affinehullS"drTde]) usingr\<open>S\<subseteq>T\<close>TSthat apply(autosimp:\<open>d\<in>S\<close>\<open>0<r\<close>hull_inc) usingbounded_subsetbyblast show?thesis
by (rule_tac x="S \<inter> ball d r" in exI) (fastforce simp: openin_open_Int \<open>0 < r\<close> that intro: *) qed have"∃f g. homeomorphism T T f g ∧ f a = b ∧ {x. ¬ (f x = x ∧ g x = x)} ⊆ S ∧ bounded {x. ¬ (f x = x ∧ g x = x)}" by (rule connected_equivalence_relation [OF S]; blast intro: 123) thenshow ?thesis using that by auto qed
lemma homeomorphism_moving_points_exists_gen: assumes K: "finite K""∧i. i ∈ K ==> x i ∈ S ∧ y i ∈ S" "pairwise (λi j. (x i ≠ x j) ∧ (y i ≠ y j)) K" and"2 ≤ aff_dim S" and ope: "openin (top_of_set (affine hull S)) S" and"S ⊆ T""T ⊆ affine hull S""connected S" shows"∃f g. homeomorphism T T f g ∧ (∀i ∈ K. f(x i) = y i) ∧ {x. ¬ (f x = x ∧ g x = x)} ⊆ S ∧ bounded {x. ¬ (f x = x ∧ g x = x)}" using assms proof (induction K) case empty thenshow ?case by (force simp: homeomorphism_ident) next case (insert i K) thenhave xney: "∧j. [j ∈ K; j ≠ i]==> x i ≠ x j ∧ y i ≠ y j" and pw: "pairwise (λi j. x i ≠ x j ∧ y i ≠ y j) K" and"x i ∈ S""y i ∈ S" and xyS: "∧i. i ∈ K ==> x i ∈ S ∧ y i ∈ S" by (simp_all add: pairwise_insert) obtain f g where homfg: "homeomorphism T T f g"and feq: "∧i. i ∈ K ==> f(x i) = y i" and fg_sub: "{x. ¬ (f x = x ∧ g x = x)} ⊆ S" and bo_fg: "bounded {x. ¬ (f x = x ∧ g x = x)}" using insert.IH [OF xyS pw] insert.prems by (blast intro: that) thenhave"∃f g. homeomorphism T T f g ∧ (∀i ∈ K. f(x i) = y i) ∧ {x. ¬ (f x = x ∧ g x = x)} ⊆ S ∧ bounded {x. ¬ (f x = x ∧ g x = x)}" using insert by blast have aff_eq: "affine hull (S - y ` K) = affine hull S" proof (rule affine_hull_Diff [OF ope]) show"finite (y ` K)" by (simp add: insert.hyps(1)) show"y ` K ⊂ S" using‹y i ∈ S› insert.hyps(2) xney xyS by fastforce qed have f_in_S: "f x ∈ S"if"x ∈ S"for x using homfg fg_sub homeomorphism_apply1 ‹S ⊆ T› proof - have"(f (f x) ≠ f x ∨ g (f x) ≠ f x) ∨ f x ∈ S" by (metis ‹S ⊆ T› homfg subsetD homeomorphism_apply1 that) thenshow ?thesis using fg_sub by force qed obtain h k where homhk: "homeomorphism T T h k"and heq: "h (f (x i)) = y i" and hk_sub: "{x. ¬ (h x = x ∧ k x = x)} ⊆ S - y ` K" and bo_hk: "bounded {x. ¬ (h x = x ∧ k x = x)}" proof (rule homeomorphism_moving_point [of "S - y`K" T "f(x i)""y i"]) show"openin (top_of_set (affine hull (S - y ` K))) (S - y ` K)" by (simp add: aff_eq openin_diff finite_imp_closedin image_subset_iff hull_inc insert xyS) show"S - y ` K ⊆ T" using‹S ⊆ T›by auto show"T ⊆ affine hull (S - y ` K)" using insert by (simp add: aff_eq) show"connected (S - y ` K)" proof (rule connected_openin_diff_countable [OF ‹connected S› ope]) show"¬ collinear S" using collinear_aff_dim ‹2 ≤ aff_dim S›by force show"countable (y ` K)" using countable_finite insert.hyps(1) by blast qed have"∧k. [f (x i) = y k; k ∈ K]==> False" by (metis feq homfg ‹x i ∈ S› homeomorphism_def ‹S ⊆ T›‹i ∉ K› subsetCE xney xyS) thenshow"f (x i) ∈ S - y ` K" by (auto simp: f_in_S ‹x i ∈ S›) show"y i ∈ S - y ` K" using insert.hyps xney by (auto simp: ‹y i ∈ S›) qed blast show ?case proof (intro exI conjI) show"homeomorphism T T (h ∘ f) (g ∘ k)" using homfg homhk homeomorphism_compose by blast show"∀i ∈ insert i K. (h ∘ f) (x i) = y i" using feq hk_sub by (auto simp: heq) show"{x. ¬ ((h ∘ f) x = x ∧ (g ∘ k) x = x)} ⊆ S" using fg_sub hk_sub by force have"bounded ({x. ¬(f x = x ∧ g x = x)} ∪ {x. ¬(h x = x ∧ k x = x)})" using bo_fg bo_hk bounded_Un by blast thenshow"bounded {x. ¬ ((h ∘ f) x = x ∧ (g ∘ k) x = x)}" by (rule bounded_subset) auto qed qed
proposition✐‹tag unimportant› homeomorphism_moving_points_exists: fixes S :: "'a::euclidean_space set" assumes2: "2 ≤ DIM('a)""open S""connected S""S ⊆ T""finite K" and KS: "∧i. i ∈ K ==> x i ∈ S ∧ y i ∈ S" and pw: "pairwise (λi j. (x i ≠ x j) ∧ (y i ≠ y j)) K" and S: "S ⊆ T""T ⊆ affine hull S""connected S" obtains f g where"homeomorphism T T f g""∧i. i ∈ K ==> f(x i) = y i" "{x. ¬ (f x = x ∧ g x = x)} ⊆ S""bounded {x. (¬ (f x = x ∧ g x = x))}" proof (cases "S = {}") case True thenshow ?thesis using KS homeomorphism_ident that by fastforce next case False thenhave affS: "affine hull S = UNIV" by (simp add: affine_hull_open ‹open S›) thenhave ope: "openin (top_of_set (affine hull S)) S" using‹open S› open_openin by auto have"2 ≤ DIM('a)"by (rule 2) alsohave"… = aff_dim (UNIV :: 'a set)" by simp alsohave"…≤ aff_dim S" by (metis aff_dim_UNIV aff_dim_affine_hull aff_dim_le_DIM affS) finallyhave"2 ≤ aff_dim S" by linarith thenshow ?thesis using homeomorphism_moving_points_exists_gen [OF ‹finite K› KS pw _ ope S] that by fastforce qed
lemma homeomorphism_grouping_point_1: fixes a::real and c::real assumes"a < b""c < d" obtains f g where"homeomorphism (cbox a b) (cbox c d) f g""f a = c""f b = d" proof - define f where"f ≡ λx. ((d - c) / (b - a)) * x + (c - a * ((d - c) / (b - a)))" have"∃g. homeomorphism (cbox a b) (cbox c d) f g" proof (rule homeomorphism_compact) show"continuous_on (cbox a b) f" unfolding f_def by (intro continuous_intros) have"f ` {a..b} = {c..d}" unfolding f_def image_affinity_atLeastAtMost using assms sum_sqs_eq by (auto simp: field_split_simps) thenshow"f ` cbox a b = cbox c d" by auto show"inj_on f (cbox a b)" unfolding f_def inj_on_def using assms by auto qed auto thenobtain g where"homeomorphism (cbox a b) (cbox c d) f g" .. thenshow ?thesis proof show"f a = c" by (simp add: f_def) show"f b = d" using assms sum_sqs_eq [of a b] by (auto simp: f_def field_split_simps) qed qed
lemma homeomorphism_grouping_point_2: fixes a::real and w::real assumes hom_ab: "homeomorphism (cbox a b) (cbox u v) f1 g1" and hom_bc: "homeomorphism (cbox b c) (cbox v w) f2 g2" and"b ∈ cbox a c""v ∈ cbox u w" and eq: "f1 a = u""f1 b = v""f2 b = v""f2 c = w" obtains f g where"homeomorphism (cbox a c) (cbox u w) f g""f a = u""f c = w" "∧x. x ∈ cbox a b ==> f x = f1 x""∧x. x ∈ cbox b c ==> f x = f2 x" proof - have le: "a ≤ b""b ≤ c""u ≤ v""v ≤ w" using assms by simp_all thenhave ac: "cbox a c = cbox a b ∪ cbox b c"and uw: "cbox u w = cbox u v ∪ cbox v w" by auto define f where"f ≡ λx. if x ≤ b then f1 x else f2 x" have"∃g. homeomorphism (cbox a c) (cbox u w) f g" proof (rule homeomorphism_compact) have cf1: "continuous_on (cbox a b) f1" using hom_ab homeomorphism_cont1 by blast have cf2: "continuous_on (cbox b c) f2" using hom_bc homeomorphism_cont1 by blast show"continuous_on (cbox a c) f" unfolding f_def using le eq by (force intro: continuous_on_cases_le [OF continuous_on_subset [OF cf1] continuous_on_subset [OF cf2]]) have"f ` cbox a b = f1 ` cbox a b""f ` cbox b c = f2 ` cbox b c" unfolding f_def using eq by force+ thenshow"f ` cbox a c = cbox u w" unfolding ac uw image_Un by (metis hom_ab hom_bc homeomorphism_def) have neq12: "f1 x ≠ f2 y"if x: "a ≤ x""x ≤ b"and y: "b < y""y ≤ c"for x y proof - have"f1 x ∈ cbox u v" by (metis hom_ab homeomorphism_def image_eqI mem_box_real(2) x) moreoverhave"f2 y ∈ cbox v w" by (metis (full_types) hom_bc homeomorphism_def image_subset_iff mem_box_real(2) not_le not_less_iff_gr_or_eq order_refl y) moreoverhave"f2 y ≠ f2 b" by (metis cancel_comm_monoid_add_class.diff_cancel diff_gt_0_iff_gt hom_bc homeomorphism_def le(2) less_imp_le less_numeral_extra(3) mem_box_real(2) order_refl y) ultimatelyshow ?thesis using le eq by simp qed have"inj_on f1 (cbox a b)" by (metis (full_types) hom_ab homeomorphism_def inj_onI) moreoverhave"inj_on f2 (cbox b c)" by (metis (full_types) hom_bc homeomorphism_def inj_onI) ultimatelyshow"inj_on f (cbox a c)" apply (simp (no_asm) add: inj_on_def) apply (simp add: f_def inj_on_eq_iff) using neq12 by force qed auto thenobtain g where"homeomorphism (cbox a c) (cbox u w) f g" .. thenshow ?thesis using eq f_def le that by force qed
lemma homeomorphism_grouping_point_3: fixes a::real assumes cbox_sub: "cbox c d ⊆ box a b""cbox u v ⊆ box a b" and box_ne: "box c d ≠ {}""box u v ≠ {}" obtains f g where"homeomorphism (cbox a b) (cbox a b) f g""f a = a""f b = b" "∧x. x ∈ cbox c d ==> f x ∈ cbox u v" proof - have less: "a < c""a < u""d < b""v < b""c < d""u < v""cbox c d ≠ {}" using assms by (simp_all add: cbox_sub subset_eq) obtain f1 g1 where1: "homeomorphism (cbox a c) (cbox a u) f1 g1" and f1_eq: "f1 a = a""f1 c = u" using homeomorphism_grouping_point_1 [OF ‹a < c›‹a < u›] . obtain f2 g2 where2: "homeomorphism (cbox c d) (cbox u v) f2 g2" and f2_eq: "f2 c = u""f2 d = v" using homeomorphism_grouping_point_1 [OF ‹c < d›‹u < v›] . obtain f3 g3 where3: "homeomorphism (cbox d b) (cbox v b) f3 g3" and f3_eq: "f3 d = v""f3 b = b" using homeomorphism_grouping_point_1 [OF ‹d < b›‹v < b›] . obtain f4 g4 where4: "homeomorphism (cbox a d) (cbox a v) f4 g4"and"f4 a = a""f4 d = v" and f4_eq: "∧x. x ∈ cbox a c ==> f4 x = f1 x""∧x. x ∈ cbox c d ==> f4 x = f2 x" using homeomorphism_grouping_point_2 [OF 12] less by (auto simp: f1_eq f2_eq) obtain f g where fg: "homeomorphism (cbox a b) (cbox a b) f g""f a = a""f b = b" and f_eq: "∧x. x ∈ cbox a d ==> f x = f4 x""∧x. x ∈ cbox d b ==> f x = f3 x" using homeomorphism_grouping_point_2 [OF 43] less by (auto simp: f4_eq f3_eq f2_eq f1_eq) show ?thesis proof (rule that [OF fg]) show"f x ∈ cbox u v"if"x ∈ cbox c d"for x using that f4_eq f_eq homeomorphism_image1 [OF 2] by (metis atLeastAtMost_iff box_real(2) image_eqI less(1) less_eq_real_def order_trans) qed qed
lemma homeomorphism_grouping_point_4: fixes T :: "real set" assumes"open U""open S""connected S""U ≠ {}""finite K""K ⊆ S""U ⊆ S""S ⊆ T" obtains f g where"homeomorphism T T f g" "∧x. x ∈ K ==> f x ∈ U""{x. (¬ (f x = x ∧ g x = x))} ⊆ S" "bounded {x. (¬ (f x = x ∧ g x = x))}" proof - obtain c d where"box c d ≠ {}""cbox c d ⊆ U" proof - obtain u where"u ∈ U" using‹U ≠ {}›by blast thenobtain e where"e > 0""cball u e ⊆ U" using‹open U› open_contains_cball by blast thenshow ?thesis by (rule_tac c=u and d="u+e"in that) (auto simp: dist_norm subset_iff) qed have"compact K" by (simp add: ‹finite K› finite_imp_compact) obtain a b where"box a b ≠ {}""K ⊆ cbox a b""cbox a b ⊆ S" proof (cases "K = {}") case True thenshow ?thesis using‹box c d ≠ {}›‹cbox c d ⊆ U›‹U ⊆ S› that by blast next case False thenobtain a b where"a ∈ K""b ∈ K" and a: "∧x. x ∈ K ==> a ≤ x"and b: "∧x. x ∈ K ==> x ≤ b" using compact_attains_inf compact_attains_sup by (metis ‹compact K›)+ obtain e where"e > 0""cball b e ⊆ S" using‹open S› open_contains_cball by (metis ‹b ∈ K›‹K ⊆ S› subsetD) show ?thesis proof show"box a (b + e) ≠ {}" using‹0 < e›‹b ∈ K› a by force show"K ⊆ cbox a (b + e)" using‹0 < e› a b by fastforce have"a ∈ S" using‹a ∈ K› assms(6) by blast have"b + e ∈ S" using‹0 < e›‹cball b e ⊆ S›by (force simp: dist_norm) show"cbox a (b + e) ⊆ S" using‹a ∈ S›‹b + e ∈ S›‹connected S› connected_contains_Icc by auto qed qed obtain w z where"cbox w z ⊆ S"and sub_wz: "cbox a b ∪ cbox c d ⊆ box w z" proof - have"a ∈ S""b ∈ S" using‹box a b ≠ {}›‹cbox a b ⊆ S›by auto moreoverhave"c ∈ S""d ∈ S" using‹box c d ≠ {}›‹cbox c d ⊆ U›‹U ⊆ S›by force+ ultimatelyhave"min a c ∈ S""max b d ∈ S" by linarith+ thenobtain e1 e2 where"e1 > 0""cball (min a c) e1 ⊆ S""e2 > 0""cball (max b d) e2 ⊆ S" using‹open S› open_contains_cball by metis thenhave *: "min a c - e1 ∈ S""max b d + e2 ∈ S" by (auto simp: dist_norm) show ?thesis proof show"cbox (min a c - e1) (max b d+ e2) ⊆ S" using * ‹connected S› connected_contains_Icc by auto show"cbox a b ∪ cbox c d ⊆ box (min a c - e1) (max b d + e2)" using‹0 < e1›‹0 < e2›by auto qed qed then obtain f g where hom: "homeomorphism (cbox w z) (cbox w z) f g" and"f w = w""f z = z" and fin: "∧x. x ∈ cbox a b ==> f x ∈ cbox c d" using homeomorphism_grouping_point_3 [of a b w z c d] using‹box a b ≠ {}›‹box c d ≠ {}›by blast have contfg: "continuous_on (cbox w z) f""continuous_on (cbox w z) g" using hom homeomorphism_def by blast+ define f' where"f' ≡ λx. if x ∈ cbox w z then f x else x" define g' where"g' ≡ λx. if x ∈ cbox w z then g x else x" show ?thesis proof have T: "cbox w z ∪ (T - box w z) = T" using‹cbox w z ⊆ S›‹S ⊆ T›by auto show"homeomorphism T T f' g'" proof have clo: "closedin (top_of_set (cbox w z ∪ (T - box w z))) (T - box w z)" by (metis Diff_Diff_Int Diff_subset T closedin_def open_box openin_open_Int topspace_euclidean_subtopology) have"∧x. [w ≤ x ∧ x ≤ z; w < x ⟶¬ x < z]==> f x = x" using‹f w = w›‹f z = z›by auto moreoverhave"∧x. [w ≤ x ∧ x ≤ z; w < x ⟶¬ x < z]==> g x = x" using‹f w = w›‹f z = z› hom homeomorphism_apply1 by fastforce ultimately have"continuous_on (cbox w z ∪ (T - box w z)) f'""continuous_on (cbox w z ∪ (T - box w z)) g'" unfolding f'_def g'_def by (intro continuous_on_cases_local contfg continuous_on_id clo; auto simp: closed_subset)+ thenshow"continuous_on T f'""continuous_on T g'" by (simp_all only: T) show"f' ` T ⊆ T" unfolding f'_def by clarsimp (metis ‹cbox w z ⊆ S›‹S ⊆ T› subsetD hom homeomorphism_def imageI mem_box_real(2)) show"g' ` T ⊆ T" unfolding g'_def by clarsimp (metis ‹cbox w z ⊆ S›‹S ⊆ T› subsetD hom homeomorphism_def imageI mem_box_real(2)) show"∧x. x ∈ T ==> g' (f' x) = x" unfolding f'_def g'_def using homeomorphism_apply1 [OF hom] homeomorphism_image1 [OF hom] by fastforce show"∧y. y ∈ T ==> f' (g' y) = y" unfolding f'_def g'_def using homeomorphism_apply2 [OF hom] homeomorphism_image2 [OF hom] by fastforce qed show"∧x. x ∈ K ==> f' x ∈ U" using fin sub_wz ‹K ⊆ cbox a b›‹cbox c d ⊆ U›by (force simp: f'_def) show"{x. ¬ (f' x = x ∧ g' x = x)} ⊆ S" using‹cbox w z ⊆ S›by (auto simp: f'_def g'_def) show"bounded {x. ¬ (f' x = x ∧ g' x = x)}" proof (rule bounded_subset [of "cbox w z"]) show"bounded (cbox w z)" using bounded_cbox by blast show"{x. ¬ (f' x = x ∧ g' x = x)} ⊆ cbox w z" by (auto simp: f'_def g'_def) qed qed qed
proposition✐‹tag unimportant› homeomorphism_grouping_points_exists: fixes S :: "'a::euclidean_space set" assumes"open U""open S""connected S""U ≠ {}""finite K""K ⊆ S""U ⊆ S""S ⊆ T" obtains f g where"homeomorphism T T f g""{x. (¬ (f x = x ∧ g x = x))} ⊆ S" "bounded {x. (¬ (f x = x ∧ g x = x))}""∧x. x ∈ K ==> f x ∈ U" proof (cases "2 ≤ DIM('a)") case True have TS: "T ⊆ affine hull S" using affine_hull_open assms by blast have"infinite U" using‹open U›‹U ≠ {}› finite_imp_not_open by blast thenobtain P where"P ⊆ U""finite P""card K = card P" using infinite_arbitrarily_large by metis thenobtain γ where γ: "bij_betw γ K P" using‹finite K› finite_same_card_bij by blast obtain f g where"homeomorphism T T f g""∧i. i ∈ K ==> f (id i) = γ i""{x. ¬ (f x = x∧ g x = x)} ⊆ S""bounded {x. ¬ (f x = x ∧ g x = x)}" proof (rule homeomorphism_moving_points_exists [OF True ‹open S›‹connected S›‹S ⊆ T›‹finite K›]) show"∧i. i ∈ K ==> id i ∈ S ∧ γ i ∈ S" using‹P ⊆ U›‹bij_betw γ K P›‹K ⊆ S›‹U ⊆ S› bij_betwE by blast show"pairwise (λi j. id i ≠ id j ∧ γ i ≠ γ j) K" using γ by (auto simp: pairwise_def bij_betw_def inj_on_def) qed (use affine_hull_open assms that in auto) thenshow ?thesis using γ ‹P ⊆ U› bij_betwE by (fastforce simp: intro!: that) next case False with DIM_positive have"DIM('a) = 1" by (simp add: dual_order.antisym) thenobtain h::"'a →real"and j where"linear h""linear j" and noh: "∧x. norm(h x) = norm x"and noj: "∧y. norm(j y) = norm y" and hj: "∧x. j(h x) = x""∧y. h(j y) = y" and ranh: "surj h" using isomorphisms_UNIV_UNIV by (metis (mono_tags, opaque_lifting) DIM_real UNIV_eq_I range_eqI) obtain f g where hom: "homeomorphism (h ` T) (h ` T) f g" and f: "∧x. x ∈ h ` K ==> f x ∈ h ` U" and sub: "{x. ¬ (f x = x ∧ g x = x)} ⊆ h ` S" and bou: "bounded {x. ¬ (f x = x ∧ g x = x)}" apply (rule homeomorphism_grouping_point_4 [of "h ` U""h ` S""h ` K""h ` T"]) by (simp_all add: assms image_mono ‹linear h› open_surjective_linear_image connected_linear_image ranh) have jf: "j (f (h x)) = x ⟷ f (h x) = h x"for x by (metis hj) have jg: "j (g (h x)) = x ⟷ g (h x) = h x"for x by (metis hj) have cont_hj: "continuous_on X h""continuous_on Y j"for X Y by (simp_all add: ‹linear h›‹linear j› linear_linear linear_continuous_on) show ?thesis proof show"homeomorphism T T (j ∘ f ∘ h) (j ∘ g ∘ h)" proof show"continuous_on T (j ∘ f ∘ h)""continuous_on T (j ∘ g ∘ h)" using hom homeomorphism_def by (blast intro: continuous_on_compose cont_hj)+ show"(j ∘ f ∘ h) ` T ⊆ T""(j ∘ g ∘ h) ` T ⊆ T" by auto (metis (mono_tags, opaque_lifting) hj(1) hom homeomorphism_def imageE imageI)+ show"∧x. x ∈ T ==> (j ∘ g ∘ h) ((j ∘ f ∘ h) x) = x" using hj hom homeomorphism_apply1 by fastforce show"∧y. y ∈ T ==> (j ∘ f ∘ h) ((j ∘ g ∘ h) y) = y" using hj hom homeomorphism_apply2 by fastforce qed show"{x. ¬ ((j ∘ f ∘ h) x = x ∧ (j ∘ g ∘ h) x = x)} ⊆ S" proof (clarsimp simp: jf jg hj) show"f (h x) = h x ⟶ g (h x) ≠ h x ==> x ∈ S"for x using sub [THEN subsetD, of "h x"] hj by simp (metis imageE) qed have"bounded (j ` {x. (¬ (f x = x ∧ g x = x))})" by (rule bounded_linear_image [OF bou]) (use‹linear j› linear_conv_bounded_linear in auto) moreover have *: "{x. ¬((j ∘ f ∘ h) x = x ∧ (j ∘ g ∘ h) x = x)} = j ` {x. (¬ (f x = x ∧ g x = x))}" using hj by (auto simp: jf jg image_iff, metis+) ultimatelyshow"bounded {x. ¬ ((j ∘ f ∘ h) x = x ∧ (j ∘ g ∘ h) x = x)}" by metis show"∧x. x ∈ K ==> (j ∘ f ∘ h) x ∈ U" using f hj by fastforce qed qed
proposition✐‹tag unimportant› homeomorphism_grouping_points_exists_gen: fixes S :: "'a::euclidean_space set" assumes opeU: "openin (top_of_set S) U" and opeS: "openin (top_of_set (affine hull S)) S" and"U ≠ {}""finite K""K ⊆ S"and S: "S ⊆ T""T ⊆ affine hull S""connected S" obtains f g where"homeomorphism T T f g""{x. (¬ (f x = x ∧ g x = x))} ⊆ S" "bounded {x. (¬ (f x = x ∧ g x = x))}""∧x. x ∈ K ==> f x ∈ U" proof (cases "2 ≤ aff_dim S") case True have opeU': "openin (top_of_set (affine hull S)) U" using opeS opeU openin_trans by blast obtain u where"u ∈ U""u ∈ S" using‹U ≠ {}› opeU openin_imp_subset by fastforce+ have"infinite U" proof (rule infinite_openin [OF opeU ‹u ∈ U›]) show"u islimpt S" using True ‹u ∈ S› assms(8) connected_imp_perfect_aff_dim by fastforce qed thenobtain P where"P ⊆ U""finite P""card K = card P" using infinite_arbitrarily_large by metis thenobtain γ where γ: "bij_betw γ K P" using‹finite K› finite_same_card_bij by blast have"∃f g. homeomorphism T T f g ∧ (∀i ∈ K. f(id i) = γ i) ∧ {x. ¬ (f x = x ∧ g x = x)} ⊆ S ∧ bounded {x. ¬ (f x = x ∧ g x = x)}" proof (rule homeomorphism_moving_points_exists_gen [OF ‹finite K› _ _ True opeS S]) show"∧i. i ∈ K ==> id i ∈ S ∧ γ i ∈ S" by (metis id_apply opeU openin_contains_cball subsetCE ‹P ⊆ U›‹bij_betw γ K P›‹K ⊆ S› bij_betwE) show"pairwise (λi j. id i ≠ id j ∧ γ i ≠ γ j) K" using γ by (auto simp: pairwise_def bij_betw_def inj_on_def) qed thenshow ?thesis using γ ‹P ⊆ U› bij_betwE by (fastforce simp: intro!: that) next case False with aff_dim_geq [of S] consider "aff_dim S = -1" | "aff_dim S = 0" | "aff_dim S = 1"by linarith thenshow ?thesis proof cases assume"aff_dim S = -1" thenhave"S = {}" using aff_dim_empty by blast thenhave"False" using‹U ≠ {}›‹K ⊆ S› openin_imp_subset [OF opeU] by blast thenshow ?thesis .. next assume"aff_dim S = 0" thenobtain a where"S = {a}" using aff_dim_eq_0 by blast thenhave"K ⊆ U" using‹U ≠ {}›‹K ⊆ S› openin_imp_subset [OF opeU] by blast show ?thesis using‹K ⊆ U›by (intro that [of id id]) (auto intro: homeomorphismI) next assume"aff_dim S = 1" thenhave"affine hull S homeomorphic (UNIV :: real set)" by (auto simp: homeomorphic_affine_sets) thenobtain h::"'a→real"and j where homhj: "homeomorphism (affine hull S) UNIV h j" using homeomorphic_def by blast thenhave h: "∧x. x ∈ affine hull S ==> j(h(x)) = x"and j: "∧y. j y ∈ affine hull S ∧ h(j y) = y" by (auto simp: homeomorphism_def) have connh: "connected (h ` S)" by (meson Topological_Spaces.connected_continuous_image ‹connected S› homeomorphism_cont1 homeomorphism_of_subsets homhj hull_subset top_greatest) have hUS: "h ` U ⊆ h ` S" by (meson homeomorphism_imp_open_map homeomorphism_of_subsets homhj hull_subset opeS opeU open_UNIV openin_open_eq) have opn: "openin (top_of_set (affine hull S)) U ==> open (h ` U)"for U using homeomorphism_imp_open_map [OF homhj] by simp have"open (h ` U)""open (h ` S)" by (auto intro: opeS opeU openin_trans opn) thenobtain f g where hom: "homeomorphism (h ` T) (h ` T) f g" and f: "∧x. x ∈ h ` K ==> f x ∈ h ` U" and sub: "{x. ¬ (f x = x ∧ g x = x)} ⊆ h ` S" and bou: "bounded {x. ¬ (f x = x ∧ g x = x)}" apply (rule homeomorphism_grouping_points_exists [of "h ` U""h ` S""h ` K""h ` T"]) using assms by (auto simp: connh hUS) have jf: "∧x. x ∈ affine hull S ==> j (f (h x)) = x ⟷ f (h x) = h x" by (metis h j) have jg: "∧x. x ∈ affine hull S ==> j (g (h x)) = x ⟷ g (h x) = h x" by (metis h j) have cont_hj: "continuous_on T h""continuous_on Y j"for Y proof (rule continuous_on_subset [OF _ ‹T ⊆ affine hull S›]) show"continuous_on (affine hull S) h" using homeomorphism_def homhj by blast qed (meson continuous_on_subset homeomorphism_def homhj top_greatest) define f' where"f' ≡ λx. if x ∈ affine hull S then (j ∘ f ∘ h) x else x" define g' where"g' ≡ λx. if x ∈ affine hull S then (j ∘ g ∘ h) x else x" show ?thesis proof show"homeomorphism T T f' g'" proof have"continuous_on T (j ∘ f ∘ h)" using hom homeomorphism_def by (intro continuous_on_compose cont_hj) blast thenshow"continuous_on T f'" apply (rule continuous_on_eq) using‹T ⊆ affine hull S› f'_defby auto have"continuous_on T (j ∘ g ∘ h)" using hom homeomorphism_def by (intro continuous_on_compose cont_hj) blast thenshow"continuous_on T g'" apply (rule continuous_on_eq) using‹T ⊆ affine hull S› g'_defby auto show"f' ` T ⊆ T" proof (clarsimp simp: f'_def) fix x assume"x ∈ T" thenhave"f (h x) ∈ h ` T" by (metis (no_types) hom homeomorphism_def image_subset_iff subset_refl) thenshow"j (f (h x)) ∈ T" using‹T ⊆ affine hull S› h by auto qed show"g' ` T ⊆ T" proof (clarsimp simp: g'_def) fix x assume"x ∈ T" thenhave"g (h x) ∈ h ` T" by (metis (no_types) hom homeomorphism_def image_subset_iff subset_refl) thenshow"j (g (h x)) ∈ T" using‹T ⊆ affine hull S› h by auto qed show"∧x. x ∈ T ==> g' (f' x) = x" using h j hom homeomorphism_apply1 by (fastforce simp: f'_def g'_def) show"∧y. y ∈ T ==> f' (g' y) = y" using h j hom homeomorphism_apply2 by (fastforce simp: f'_def g'_def) qed next have§: "∧x y. [x ∈ affine hull S; h x = h y; y ∈ S]==> x ∈ S" by (metis h hull_inc) show"{x. ¬ (f' x = x ∧ g' x = x)} ⊆ S" using sub by (simp add: f'_def g'_def jf jg) (force elim: §) next have"compact (j ` closure {x. ¬ (f x = x ∧ g x = x)})" using bou by (auto simp: compact_continuous_image cont_hj) thenhave"bounded (j ` {x. ¬ (f x = x ∧ g x = x)})" by (rule bounded_closure_image [OF compact_imp_bounded]) moreover have *: "{x ∈ affine hull S. j (f (h x)) ≠ x ∨ j (g (h x)) ≠ x} = j ` {x. (¬ (f x = x ∧ g x = x))}" using h j by (auto simp: image_iff; metis) ultimatelyhave"bounded {x ∈ affine hull S. j (f (h x)) ≠ x ∨ j (g (h x)) ≠ x}" by metis thenshow"bounded {x. ¬ (f' x = x ∧ g' x = x)}" by (simp add: f'_def g'_def Collect_mono bounded_subset) next show"f' x ∈ U"if"x ∈ K"for x proof - have"U ⊆ S" using opeU openin_imp_subset by blast thenhave"j (f (h x)) ∈ U" using f h hull_subset that by fastforce thenshow"f' x ∈ U" using‹K ⊆ S› S f'_def that by auto qed qed qed qed
subsection‹Nullhomotopic mappings›
text‹ A mapping out of a sphere is nullhomotopic iff it extends to the ball.
even works out in the degenerate cases when the radius is ‹≤› 0, and
also don't need to explicitly assume continuity since it's already implicit
both sides of the equivalence.›
lemma nullhomotopic_from_lemma: assumes contg: "continuous_on (cball a r - {a}) g" and fa: "∧e. 0 < e ==>∃d. 0 < d ∧ (∀x. x ≠ a ∧ norm(x - a) < d ⟶ norm(g x - f a) < e)" and r: "∧x. x ∈ cball a r ∧ x ≠ a ==> f x = g x" shows"continuous_on (cball a r) f" proof (clarsimp simp: continuous_on_eq_continuous_within Ball_def) fix x assume x: "dist a x ≤ r" show"continuous (at x within cball a r) f" proof (cases "x=a") case True thenshow ?thesis by (metis continuous_within_eps_delta fa dist_norm dist_self r) next case False show ?thesis proof (rule continuous_transform_within [where f=g and δ = "norm(x-a)"]) have"∃d>0. ∀x'∈cball a r. dist x' x < d ⟶ dist (g x') (g x) < e" if"e>0"for e proof - obtain d where"d > 0" and d: "∧y. [dist y a ≤ r; y ≠ a; dist y x < d]==> dist (g y) (g x) < e" using contg False x ‹e>0› unfolding continuous_on_iff by (fastforce simp: dist_commute intro: that) show ?thesis using‹d > 0›‹x ≠ a› by (rule_tac x="min d (norm(x - a))"in exI)
(auto simp: dist_commute dist_norm [symmetric] intro!: d) qed thenshow"continuous (at x within cball a r) g" using contg False by (auto simp: continuous_within_eps_delta) show"0 < norm (x - a)" using False by force show"x ∈ cball a r" by (simp add: x) show"∧x'. [x' ∈ cball a r; dist x' x < norm (x - a)] ==> g x' = f x'" by (metis dist_commute dist_norm less_le r) qed qed qed
proposition nullhomotopic_from_sphere_extension: fixes f :: "'M::euclidean_space → 'a::real_normed_vector" shows"(∃c. homotopic_with_canon (λx. True) (sphere a r) S f (λx. c)) ⟷ (∃g. continuous_on (cball a r) g ∧ g ` (cball a r) ⊆ S ∧ (∀x ∈ sphere a r. g x = f x))"
(is"?lhs = ?rhs") proof (cases r "0::real" rule: linorder_cases) case less thenshow ?thesis by (simp add: homotopic_on_emptyI) next case equal show ?thesis proof assume L: ?lhs with equal have [simp]: "f a ∈ S" using homotopic_with_imp_subset1 by fastforce obtain h:: "real × 'M → 'a" where h: "continuous_on ({0..1} × {a}) h""h ` ({0..1} × {a}) ⊆ S""h (0, a) = f a" using L equal by (auto simp: homotopic_with) thenhave"continuous_on (cball a r) (λx. h (0, a))""(λx. h (0, a)) ` cball a r ⊆ S" by (auto simp: equal) thenshow ?rhs using h(3) local.equal by force next assume ?rhs thenshow ?lhs using equal continuous_on_const by (force simp: homotopic_with) qed next case greater let ?P = "continuous_on {x. norm(x - a) = r} f ∧ f ` {x. norm(x - a) = r} ⊆ S" have ?P if ?lhs using that proof fix c assume c: "homotopic_with_canon (λx. True) (sphere a r) S f (λx. c)" thenhave contf: "continuous_on (sphere a r) f" by (metis homotopic_with_imp_continuous) moreoverhave fim: "f ∈ sphere a r → S" using homotopic_with_imp_subset1 that by blast show ?P using contf fim by (auto simp: sphere_def dist_norm norm_minus_commute) qed moreoverhave ?P if ?rhs using that proof fix g assume g: "continuous_on (cball a r) g ∧ g ` cball a r ⊆ S ∧ (∀xa∈sphere a r. g xa = f xa)" thenhave"f ` {x. norm (x - a) = r} ⊆ S" using sphere_cball [of a r] unfolding image_subset_iff sphere_def by (metis dist_commute dist_norm mem_Collect_eq subset_eq) with g show ?P by (auto simp: dist_norm norm_minus_commute elim!: continuous_on_eq [OF continuous_on_subset]) qed moreoverhave ?thesis if ?P proof assume ?lhs thenobtain c where"homotopic_with_canon (λx. True) (sphere a r) S (λx. c) f" using homotopic_with_sym by blast thenobtain h where conth: "continuous_on ({0..1::real} × sphere a r) h" and him: "h ` ({0..1} × sphere a r) ⊆ S" and h: "∧x. h(0, x) = c""∧x. h(1, x) = f x" by (auto simp: homotopic_with_def) obtain b1::'M where"b1 ∈ Basis" using SOME_Basis by auto have"c ∈ h ` ({0..1} × sphere a r)" proof show"c = h (0, a + r *R b1)" by (simp add: h) show"(0, a + r *R b1) ∈ {0..1::real} × sphere a r" using greater ‹b1 ∈ Basis›by (auto simp: dist_norm) qed thenhave"c ∈ S" using him by blast have uconth: "uniformly_continuous_on ({0..1::real} × (sphere a r)) h" by (force intro: compact_Times conth compact_uniformly_continuous) let ?g = "λx. h (norm (x - a)/r, a + (if x = a then r *R b1 else (r / norm(x - a)) *R (x - a)))" let ?g' = "λx. h (norm (x - a)/r, a + (r / norm(x - a)) *R (x - a))" show ?rhs proof (intro exI conjI) have"continuous_on (cball a r - {a}) ?g'" using greater by (force simp: dist_norm norm_minus_commute intro: continuous_on_compose2 [OF conth] continuous_intros) thenshow"continuous_on (cball a r) ?g" proof (rule nullhomotopic_from_lemma) show"∃d>0. ∀x. x ≠ a ∧ norm (x - a) < d ⟶ norm (?g' x - ?g a) < e"if"0 < e"for e proof - obtain d where"0 < d" and d: "∧x x'. [x ∈ {0..1} × sphere a r; x' ∈ {0..1} × sphere a r; norm ( x' - x) < d] ==> norm (h x' - h x) < e" using uniformly_continuous_onE [OF uconth ‹0 < e›] by (auto simp: dist_norm) have *: "norm (h (norm (x - a) / r, a + (r / norm (x - a)) *R (x - a)) - h (0, a + r *R b1)) < e" (is"norm (?ha - ?hb) < e") if"x ≠ a""norm (x - a) < r""norm (x - a) < d * r"for x proof - have"norm (?ha - ?hb) = norm (?ha - h (0, a + (r / norm (x - a)) *R (x - a)))" by (simp add: h) alsohave"… < e" using greater ‹0 < d›‹b1 ∈ Basis› that by (intro d) (simp_all add: dist_norm, simp add: field_simps) finallyshow ?thesis . qed show ?thesis using greater ‹0 < d› by (rule_tac x = "min r (d * r)"in exI) (auto simp: *) qed show"∧x. x ∈ cball a r ∧ x ≠ a ==> ?g x = ?g' x" by auto qed next show"?g ` cball a r ⊆ S" using greater him ‹c ∈ S› by (force simp: h dist_norm norm_minus_commute) next show"∀x∈sphere a r. ?g x = f x" using greater by (auto simp: h dist_norm norm_minus_commute) qed next assume ?rhs thenobtain g where contg: "continuous_on (cball a r) g" and gim: "g ` cball a r ⊆ S" and gf: "∀x ∈ sphere a r. g x = f x" by auto let ?h = "λy. g (a + (fst y) *R (snd y - a))" have"continuous_on ({0..1} × sphere a r) ?h" proof (rule continuous_on_compose2 [OF contg]) show"continuous_on ({0..1} × sphere a r) (λx. a + fst x *R (snd x - a))" by (intro continuous_intros) qed (auto simp: dist_norm norm_minus_commute mult_left_le_one_le) moreover have"?h ∈ ({0..1} × sphere a r) → S" by (auto simp: dist_norm norm_minus_commute mult_left_le_one_le gim [THEN subsetD]) moreover have"∀x∈sphere a r. ?h (0, x) = g a""∀x∈sphere a r. ?h (1, x) = f x" by (auto simp: dist_norm norm_minus_commute mult_left_le_one_le gf) ultimatelyhave"homotopic_with_canon (λx. True) (sphere a r) S (λx. g a) f" by (auto simp: homotopic_with) thenshow ?lhs using homotopic_with_symD by blast qed ultimately show ?thesis by meson qed
end
Messung V0.5 in Prozent
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.1.410Bemerkung:
(vorverarbeitet am 2026-06-29)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.