(* Title: HOL/Analysis/Path_Connected.thy Authors: LC Paulson and Robert Himmelmann (TU Muenchen), based on material from HOL Light *)
section‹Homotopy of Maps›
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. We often just want to require that ‹P›fixes some subset, but to include the case of a loop homotopy, it 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🍋‹tag important›‹%whitespace›
proposition homotopic_with: assumes"∧h k. (∧x. x ∈ topspace X ==> h x = k x) ==> (P h ⟷ P k)" shows"homotopic_with P X Y p q ⟷ (∃h. continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y h ∧ (∀x ∈ topspace X. h(0,x) = p x) ∧ (∀x ∈ topspace X. h(1,x) = q x) ∧ (∀t ∈ {0..1}. P(λx. h(t, x))))" unfolding homotopic_with_def apply (rule iffI, blast, clarify) apply (rule_tac x="λ(u,v). if v ∈ topspace X then h(u,v) else if u = 0 then p v else q v"in exI) apply simp by (smt (verit, best) SigmaE assms case_prod_conv continuous_map_eq topspace_prod_topology)
lemma homotopic_with_mono: assumes hom: "homotopic_with P X Y f g" and Q: "∧h. [continuous_map X Y h; P h]==> Q h" shows"homotopic_with Q X Y f g" using hom unfolding homotopic_with_def by (force simp: o_def dest: continuous_map_o_Pair intro: Q)
lemma homotopic_with_imp_continuous_maps: assumes"homotopic_with P X Y f g" shows"continuous_map X Y f ∧ continuous_map X Y g" proof - obtain h :: "real × 'a ==> 'b" where conth: "continuous_map (prod_topology (top_of_set {0..1}) X) Y h" and h: "∀x. h (0, x) = f x""∀x. h (1, x) = g x" using assms by (auto simp: homotopic_with_def) have *: "t ∈ {0..1} ==> continuous_map X Y (h ∘ (λx. (t,x)))"for t by (rule continuous_map_compose [OF _ conth]) (simp add: o_def continuous_map_pairwise) show ?thesis using h *[of 0] *[of 1] by (simp add: continuous_map_eq) qed
lemma homotopic_with_imp_continuous: assumes"homotopic_with_canon P X Y f g" shows"continuous_on X f ∧ continuous_on X g" by (meson assms continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)
lemma homotopic_with_imp_property: assumes"homotopic_with P X Y f g" shows"P f ∧ P g" proof obtain h where h: "∧x. h(0, x) = f x""∧x. h(1, x) = g x"and P: "∧t. t ∈ {0..1::real} ==> P(λx. h(t,x))" using assms by (force simp: homotopic_with_def) show"P f""P g" using P [of 0] P [of 1] by (force simp: h)+ qed
lemma homotopic_with_equal: assumes"P f""P g"and contf: "continuous_map X Y f"and fg: "∧x. x ∈ topspace X ==> f x = g x" shows"homotopic_with P X Y f g" unfolding homotopic_with_def proof (intro exI conjI allI ballI) let ?h = "λ(t::real,x). if t = 1 then g x else f x" show"continuous_map (prod_topology (top_of_set {0..1}) X) Y ?h" proof (rule continuous_map_eq) show"continuous_map (prod_topology (top_of_set {0..1}) X) Y (f ∘ snd)" by (simp add: contf continuous_map_of_snd) qed (auto simp: fg) show"P (λx. ?h (t, x))"if"t ∈ {0..1}"for t by (cases "t = 1") (simp_all add: assms) qed auto
lemma homotopic_with_imp_funspace1: "homotopic_with_canon P X Y f g ==> f ∈ X → Y" using homotopic_with_imp_continuous_maps by fastforce
lemma homotopic_with_imp_subset1: "homotopic_with_canon P X Y f g ==> f ` X ⊆ Y" using homotopic_with_imp_funspace1 by blast
lemma homotopic_with_imp_funspace2: "homotopic_with_canon P X Y f g ==> g ∈ X → Y" using homotopic_with_imp_continuous_maps by force
lemma homotopic_with_imp_subset2: "homotopic_with_canon P X Y f g ==> g ` X ⊆ Y" using homotopic_with_imp_funspace2 by blast
lemma homotopic_with_subset_left: "[homotopic_with_canon P X Y f g; Z ⊆ X]==> homotopic_with_canon P Z Y f g" unfolding homotopic_with_def by (auto elim!: continuous_on_subset ex_forward)
lemma homotopic_with_subset_right: "[homotopic_with_canon P X Y f g; Y ⊆ Z]==> homotopic_with_canon P X Z f g" unfolding homotopic_with_def by (auto elim!: continuous_on_subset ex_forward)
subsection‹Homotopy with P is an equivalence relation›
text‹(on continuous functions mapping X into Y that satisfy P, though this only affects reflexivity)›
lemma homotopic_with_refl [simp]: "homotopic_with P X Y f f ⟷ continuous_map X Y f ∧ P f" by (metis homotopic_with_equal homotopic_with_imp_continuous_maps homotopic_with_imp_property)
lemma homotopic_with_symD: assumes"homotopic_with P X Y f g" shows"homotopic_with P X Y g f" proof - let ?I01 = "subtopology euclideanreal {0..1}" let ?j = "λy. (1 - fst y, snd y)" have 1: "continuous_map (prod_topology ?I01 X) (prod_topology euclideanreal X) ?j" by (intro continuous_intros; simp add: continuous_map_subtopology_fst prod_topology_subtopology) have *: "continuous_map (prod_topology ?I01 X) (prod_topology ?I01 X) ?j" proof - have"continuous_map (prod_topology ?I01 X) (subtopology (prod_topology euclideanreal X) ({0..1} × topspace X)) ?j" by (simp add: continuous_map_into_subtopology [OF 1] image_subset_iff flip: image_subset_iff_funcset) thenshow ?thesis by (simp add: prod_topology_subtopology(1)) qed show ?thesis using assms apply (clarsimp simp: homotopic_with_def)
subgoal for h by (rule_tac x="h ∘ (λy. (1 - fst y, snd y))"in exI) (simp add: continuous_map_compose [OF *]) done qed
lemma homotopic_with_sym: "homotopic_with P X Y f g ⟷ homotopic_with P X Y g f" by (metis homotopic_with_symD)
proposition homotopic_with_trans: assumes"homotopic_with P X Y f g""homotopic_with P X Y g h" shows"homotopic_with P X Y f h" proof - let ?X01 = "prod_topology (subtopology euclideanreal {0..1}) X" obtain k1 k2 where contk1: "continuous_map ?X01 Y k1"and contk2: "continuous_map ?X01 Y k2" and k12: "∀x. k1 (1, x) = g x""∀x. k2 (0, x) = g x" "∀x. k1 (0, x) = f x""∀x. k2 (1, x) = h x" and P: "∀t∈{0..1}. P (λx. k1 (t, x))""∀t∈{0..1}. P (λx. k2 (t, x))" using assms by (auto simp: homotopic_with_def)
define k where"k ≡ λy. if fst y ≤ 1/2 then (k1 ∘ (λx. (2 *🪙R fst x, snd x))) y else (k2 ∘ (λx. (2 *🪙R fst x -1, snd x))) y" have keq: "k1 (2 * u, v) = k2 (2 * u -1, v)"if"u = 1/2"for u v by (simp add: k12 that) show ?thesis unfolding homotopic_with_def proof (intro exI conjI) show"continuous_map ?X01 Y k" unfolding k_def proof (rule continuous_map_cases_le) show fst: "continuous_map ?X01 euclideanreal fst" using continuous_map_fst continuous_map_in_subtopology by blast show"continuous_map ?X01 euclideanreal (λx. 1/2)" by simp show"continuous_map (subtopology ?X01 {y ∈ topspace ?X01. fst y ≤ 1/2}) Y (k1 ∘ (λx. (2 *🪙R fst x, snd x)))" apply (intro fst continuous_map_compose [OF _ contk1] continuous_intros continuous_map_into_subtopology continuous_map_from_subtopology | simp)+ by (force simp: prod_topology_subtopology) show"continuous_map (subtopology ?X01 {y ∈ topspace ?X01. 1/2 ≤ fst y}) Y (k2 ∘ (λx. (2 *🪙R fst x -1, snd x)))" apply (intro fst continuous_map_compose [OF _ contk2] continuous_intros continuous_map_into_subtopology continuous_map_from_subtopology | simp)+ by (force simp: prod_topology_subtopology) show"(k1 ∘ (λx. (2 *🪙R fst x, snd x))) y = (k2 ∘ (λx. (2 *🪙R fst x -1, snd x))) y" if"y ∈ topspace ?X01"and"fst y = 1/2"for y using that by (simp add: keq) qed show"∀x. k (0, x) = f x" by (simp add: k12 k_def) show"∀x. k (1, x) = h x" by (simp add: k12 k_def) show"∀t∈{0..1}. P (λx. k (t, x))" proof fix t show"t∈{0..1} ==> P (λx. k (t, x))" by (cases "t ≤ 1/2") (auto simp: k_def P) qed qed qed
lemma homotopic_with_id2: "(∧x. x ∈ topspace X ==> g (f x) = x) ==> homotopic_with (λx. True) X X (g ∘ f) id" by (metis comp_apply continuous_map_id eq_id_iff homotopic_with_equal homotopic_with_symD)
subsection‹Continuity lemmas›
lemma homotopic_with_compose_continuous_map_left: "[homotopic_with p X1 X2 f g; continuous_map X2 X3 h; ∧j. p j ==> q(h ∘ j)] ==> homotopic_with q X1 X3 (h ∘ f) (h ∘ g)" unfolding homotopic_with_def apply clarify
subgoal for k by (rule_tac x="h ∘ k"in exI) (rule conjI continuous_map_compose | simp add: o_def)+ done
lemma homotopic_with_compose_continuous_map_right: assumes hom: "homotopic_with p X2 X3 f g"and conth: "continuous_map X1 X2 h" and q: "∧j. p j ==> q(j ∘ h)" shows"homotopic_with q X1 X3 (f ∘ h) (g ∘ h)" proof - obtain k where contk: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X2) X3 k" and k: "∀x. k (0, x) = f x""∀x. k (1, x) = g x"and p: "∧t. t∈{0..1} ==> p (λx. k (t, x))" using hom unfolding homotopic_with_def by blast have hsnd: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) X2 (h ∘ snd)" by (rule continuous_map_compose [OF continuous_map_snd conth]) let ?h = "k ∘ (λ(t,x). (t,h x))" show ?thesis unfolding homotopic_with_def proof (intro exI conjI allI ballI) have"continuous_map (prod_topology (top_of_set {0..1}) X1) (prod_topology (top_of_set {0..1::real}) X2) (λ(t, x). (t, h x))" by (metis (mono_tags, lifting) case_prod_beta' comp_def continuous_map_eq continuous_map_fst continuous_map_pairedI hsnd) thenshow"continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) X3 ?h" by (intro conjI continuous_map_compose [OF _ contk]) show"q (λx. ?h (t, x))"if"t ∈ {0..1}"for t using q [OF p [OF that]] by (simp add: o_def) qed (auto simp: k) qed
corollary homotopic_compose: assumes"homotopic_with (λx. True) X Y f f'""homotopic_with (λx. True) Y Z g g'" shows"homotopic_with (λx. True) X Z (g ∘ f) (g' ∘ f')" by (metis assms homotopic_with_compose_continuous_map_left homotopic_with_compose_continuous_map_right homotopic_with_imp_continuous_maps homotopic_with_trans)
proposition homotopic_with_compose_continuous_right: "[homotopic_with_canon (λf. p (f ∘ h)) X Y f g; continuous_on W h; h ∈ W → X] ==> homotopic_with_canon p W Y (f ∘ h) (g ∘ h)" by (simp add: homotopic_with_compose_continuous_map_right image_subset_iff_funcset)
proposition homotopic_with_compose_continuous_left: "[homotopic_with_canon (λf. p (h ∘ f)) X Y f g; continuous_on Y h; h ∈ Y → Z] ==> homotopic_with_canon p X Z (h ∘ f) (h ∘ g)" by (simp add: homotopic_with_compose_continuous_map_left image_subset_iff_funcset)
lemma homotopic_from_subtopology: "homotopic_with P X X' f g ==> homotopic_with P (subtopology X S) X' f g" by (metis continuous_map_id_subt homotopic_with_compose_continuous_map_right o_id)
lemma homotopic_on_emptyI: assumes"P f""P g" shows"homotopic_with P trivial_topology X f g" by (metis assms continuous_map_on_empty empty_iff homotopic_with_equal topspace_discrete_topology)
lemma homotopic_on_empty: "(homotopic_with P trivial_topology X f g ⟷ P f ∧ P g)" using homotopic_on_emptyI homotopic_with_imp_property by metis
lemma homotopic_with_canon_on_empty: "homotopic_with_canon (λx. True) {} t f g" by (auto intro: homotopic_with_equal)
lemma homotopic_constant_maps: "homotopic_with (λx. True) X X' (λx. a) (λx. b) ⟷ X = trivial_topology ∨ path_component_of X' a b" (is"?lhs = ?rhs") proof (cases "X = trivial_topology") case False thenobtain c where c: "c ∈ topspace X" by fastforce have"∃g. continuous_map (top_of_set {0..1::real}) X' g ∧ g 0 = a ∧ g 1 = b" if"x ∈ topspace X"and hom: "homotopic_with (λx. True) X X' (λx. a) (λx. b)"for x proof - obtain h :: "real × 'a ==> 'b" where conth: "continuous_map (prod_topology (top_of_set {0..1}) X) X' h" and h: "∧x. h (0, x) = a""∧x. h (1, x) = b" using hom by (auto simp: homotopic_with_def) have cont: "continuous_map (top_of_set {0..1}) X' (h ∘ (λt. (t, c)))" by (rule continuous_map_compose [OF _ conth] continuous_intros | simp add: c)+ thenshow ?thesis by (force simp: h) qed moreoverhave"homotopic_with (λx. True) X X' (λx. g 0) (λx. g 1)" if"x ∈ topspace X""a = g 0""b = g 1""continuous_map (top_of_set {0..1}) X' g" for x and g :: "real ==> 'b" unfolding homotopic_with_def by (force intro!: continuous_map_compose continuous_intros c that) ultimatelyshow ?thesis using False by (metis c path_component_of_set pathin_def) qed (simp add: homotopic_on_empty)
proposition homotopic_with_eq: assumes h: "homotopic_with P X Y f g" and f': "∧x. x ∈ topspace X ==> f' x = f x" and g': "∧x. x ∈ topspace X ==> g' x = g x" and P: "(∧h k. (∧x. x ∈ topspace X ==> h x = k x) ==> P h ⟷ P k)" shows"homotopic_with P X Y f' g'" by (smt (verit, ccfv_SIG) assms homotopic_with)
lemma homotopic_with_prod_topology: assumes"homotopic_with p X1 Y1 f f'"and"homotopic_with q X2 Y2 g g'" and r: "∧i j. [p i; q j]==> r(λ(x,y). (i x, j y))" shows"homotopic_with r (prod_topology X1 X2) (prod_topology Y1 Y2) (λz. (f(fst z),g(snd z))) (λz. (f'(fst z), g'(snd z)))" proof - obtain h where h: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) Y1 h" and h0: "∧x. h (0, x) = f x" and h1: "∧x. h (1, x) = f' x" and p: "∧t. [0 ≤ t; t ≤ 1]==> p (λx. h (t,x))" using assms unfolding homotopic_with_def by auto obtain k where k: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X2) Y2 k" and k0: "∧x. k (0, x) = g x" and k1: "∧x. k (1, x) = g' x" and q: "∧t. [0 ≤ t; t ≤ 1]==> q (λx. k (t,x))" using assms unfolding homotopic_with_def by auto let ?hk = "λ(t,x,y). (h(t,x), k(t,y))" show ?thesis unfolding homotopic_with_def proof (intro conjI allI exI) show"continuous_map (prod_topology (subtopology euclideanreal {0..1}) (prod_topology X1 X2)) (prod_topology Y1 Y2) ?hk" unfolding continuous_map_pairwise case_prod_unfold by (rule conjI continuous_map_pairedI continuous_intros continuous_map_id [unfolded id_def]
continuous_map_fst_of [unfolded o_def] continuous_map_snd_of [unfolded o_def]
continuous_map_compose [OF _ h, unfolded o_def]
continuous_map_compose [OF _ k, unfolded o_def])+ next fix x show"?hk (0, x) = (f (fst x), g (snd x))""?hk (1, x) = (f' (fst x), g' (snd x))" by (auto simp: case_prod_beta h0 k0 h1 k1) qed (auto simp: p q r) qed
lemma homotopic_with_product_topology: assumes ht: "∧i. i ∈ I ==> homotopic_with (p i) (X i) (Y i) (f i) (g i)" and pq: "∧h. (∧i. i ∈ I ==> p i (h i)) ==> q(λx. (λi∈I. h i (x i)))" shows"homotopic_with q (product_topology X I) (product_topology Y I) (λz. (λi∈I. (f i) (z i))) (λz. (λi∈I. (g i) (z i)))" proof - obtain h where h: "∧i. i ∈ I ==> continuous_map (prod_topology (subtopology euclideanreal {0..1}) (X i)) (Y i) (h i)" and h0: "∧i x. i ∈ I ==> h i (0, x) = f i x" and h1: "∧i x. i ∈ I ==> h i (1, x) = g i x" and p: "∧i t. [i ∈ I; t ∈ {0..1}]==> p i (λx. h i (t,x))" using ht unfolding homotopic_with_def by metis show ?thesis unfolding homotopic_with_def proof (intro conjI allI exI) let ?h = "λ(t,z). λi∈I. h i (t,z i)" have"continuous_map (prod_topology (subtopology euclideanreal {0..1}) (product_topology X I)) (Y i) (λx. h i (fst x, snd x i))"if"i ∈ I"for i proof - have🍋: "continuous_map (prod_topology (top_of_set {0..1}) (product_topology X I)) (X i) (λx. snd x i)" using continuous_map_componentwise continuous_map_snd that by fastforce show ?thesis unfolding continuous_map_pairwise case_prod_unfold by (intro conjI that 🍋 continuous_intros continuous_map_compose [OF _ h, unfolded o_def]) qed thenshow"continuous_map (prod_topology (subtopology euclideanreal {0..1}) (product_topology X I)) (product_topology Y I) ?h" by (auto simp: continuous_map_componentwise case_prod_beta) show"?h (0, x) = (λi∈I. f i (x i))""?h (1, x) = (λi∈I. g i (x i))"for x by (auto simp: case_prod_beta h0 h1) show"∀t∈{0..1}. q (λx. ?h (t, x))" by (force intro: p pq) qed qed
text‹Homotopic triviality implicitly incorporates path-connectedness.› lemma homotopic_triviality: shows"(∀f g. continuous_on S f ∧ f ∈ S → T ∧ continuous_on S g ∧ g ∈ S → T ⟶ homotopic_with_canon (λx. True) S T f g) ⟷ (S = {} ∨ path_connected T) ∧ (∀f. continuous_on S f ∧ f ∈ S → T ⟶ (∃c. homotopic_with_canon (λx. True) S T f (λx. c)))"
(is"?lhs = ?rhs") proof (cases "S = {} ∨ T = {}") case True thenshow ?thesis by (auto simp: homotopic_on_emptyI simp flip: image_subset_iff_funcset) next case False show ?thesis proof assume LHS [rule_format]: ?lhs have pab: "path_component T a b"if"a ∈ T""b ∈ T"for a b proof - have"homotopic_with_canon (λx. True) S T (λx. a) (λx. b)" by (simp add: LHS image_subset_iff that) thenshow ?thesis using False homotopic_constant_maps [of "top_of_set S""top_of_set T" a b] by (metis path_component_of_canon_iff topspace_discrete_topology topspace_euclidean_subtopology) qed moreover have"∃c. homotopic_with_canon (λx. True) S T f (λx. c)"if"continuous_on S f""f ∈ S→ T"for f using False LHS continuous_on_const that by blast ultimatelyshow ?rhs by (simp add: path_connected_component) next assume RHS: ?rhs with False have T: "path_connected T" by blast show ?lhs proof clarify fix f g assume"continuous_on S f""f ∈ S → T""continuous_on S g""g ∈ S → T" obtain c d where c: "homotopic_with_canon (λx. True) S T f (λx. c)"and d: "homotopic_with_canon (λx. True) S T g (λx. d)" using RHS ‹continuous_on S f›‹continuous_on S g›‹f ∈ S → T›‹g ∈ S → T›by presburger with T have"path_component T c d" by (metis False ex_in_conv homotopic_with_imp_subset2 image_subset_iff path_connected_component) thenhave"homotopic_with_canon (λx. True) S T (λx. c) (λx. d)" by (simp add: homotopic_constant_maps) with c d show"homotopic_with_canon (λx. True) S T f g" by (meson homotopic_with_symD homotopic_with_trans) qed qed qed
subsection‹Homotopy of paths, maintaining the same endpoints›
definition🍋‹tag important› homotopic_paths :: "['a set, real ==> 'a, real ==> 'a::topological_space] ==> bool" where "homotopic_paths S p q ≡ homotopic_with_canon (λr. pathstart r = pathstart p ∧ pathfinish r = pathfinish p) {0..1} S p q"
lemma homotopic_paths: "homotopic_paths S p q ⟷ (∃h. continuous_on ({0..1} × {0..1}) h ∧ h ∈ ({0..1} × {0..1}) → S ∧ (∀x ∈ {0..1}. h(0,x) = p x) ∧ (∀x ∈ {0..1}. h(1,x) = q x) ∧ (∀t ∈ {0..1::real}. pathstart(h ∘ Pair t) = pathstart p ∧ pathfinish(h ∘ Pair t) = pathfinish p))" by (auto simp: homotopic_paths_def homotopic_with pathstart_def pathfinish_def)
proposition homotopic_paths_imp_pathstart: "homotopic_paths S p q ==> pathstart p = pathstart q" by (metis (mono_tags, lifting) homotopic_paths_def homotopic_with_imp_property)
proposition homotopic_paths_imp_pathfinish: "homotopic_paths S p q ==> pathfinish p = pathfinish q" by (metis (mono_tags, lifting) homotopic_paths_def homotopic_with_imp_property)
lemma homotopic_paths_imp_path: "homotopic_paths S p q ==> path p ∧ path q" using homotopic_paths_def homotopic_with_imp_continuous_maps path_def continuous_map_subtopology_eu by blast
lemma homotopic_paths_imp_subset: "homotopic_paths S p q ==> path_image p ⊆ S ∧ path_image q ⊆ S" by (simp add: homotopic_paths_def homotopic_with_imp_subset1 homotopic_with_imp_subset2
path_image_def)
proposition homotopic_paths_refl [simp]: "homotopic_paths S p p ⟷ path p ∧ path_image p ⊆ S" by (auto simp add: homotopic_paths_def path_def path_image_def)
proposition homotopic_paths_sym: "homotopic_paths S p q ==> homotopic_paths S q p" by (metis (mono_tags) homotopic_paths_def homotopic_paths_imp_pathfinish homotopic_paths_imp_pathstart homotopic_with_symD)
proposition homotopic_paths_sym_eq: "homotopic_paths S p q ⟷ homotopic_paths S q p" by (metis homotopic_paths_sym)
proposition homotopic_paths_trans [trans]: assumes"homotopic_paths S p q""homotopic_paths S q r" shows"homotopic_paths S p r" using assms homotopic_paths_imp_pathfinish homotopic_paths_imp_pathstart unfolding homotopic_paths_def by (smt (verit, ccfv_SIG) homotopic_with_mono homotopic_with_trans)
proposition homotopic_paths_eq: "[path p; path_image p ⊆ S; ∧t. t ∈ {0..1} ==> p t = q t]==> homotopic_paths S p q" by (smt (verit, best) homotopic_paths homotopic_paths_refl)
proposition homotopic_paths_reparametrize: assumes"path p" and pips: "path_image p ⊆ S" and contf: "continuous_on {0..1} f" and f01 :"f ∈ {0..1} → {0..1}" and [simp]: "f(0) = 0""f(1) = 1" and q: "∧t. t ∈ {0..1} ==> q(t) = p(f t)" shows"homotopic_paths S p q" proof - have contp: "continuous_on {0..1} p" by (metis ‹path p› path_def) thenhave"continuous_on {0..1} (p ∘ f)" by (meson assms(4) contf continuous_on_compose continuous_on_subset image_subset_iff_funcset) thenhave"path q" by (simp add: path_def) (metis q continuous_on_cong) have piqs: "path_image q ⊆ S" by (smt (verit, ccfv_threshold) Pi_iff assms(2) assms(4) assms(7) image_subset_iff path_defs(4)) have fb0: "∧a b. [0 ≤ a; a ≤ 1; 0 ≤ b; b ≤ 1]==> 0 ≤ (1 - a) * f b + a * b" using f01 by force have fb1: "[0 ≤ a; a ≤ 1; 0 ≤ b; b ≤ 1]==> (1 - a) * f b + a * b ≤ 1"for a b by (intro convex_bound_le) (use f01 in auto) have"homotopic_paths S q p" proof (rule homotopic_paths_trans) show"homotopic_paths S q (p ∘ f)" using q by (force intro: homotopic_paths_eq [OF ‹path q› piqs]) next show"homotopic_paths S (p ∘ f) p" using pips [unfolded path_image_def] apply (simp add: homotopic_paths_def homotopic_with_def) apply (rule_tac x="p ∘ (λy. (1 - (fst y)) *🪙R ((f ∘ snd) y) + (fst y) *🪙R snd y)"in exI) apply (rule conjI contf continuous_intros continuous_on_subset [OF contp] | simp)+ by (auto simp: fb0 fb1 pathstart_def pathfinish_def) qed thenshow ?thesis by (simp add: homotopic_paths_sym) qed
lemma homotopic_paths_subset: "[homotopic_paths S p q; S ⊆ t]==> homotopic_paths t p q" unfolding homotopic_paths by fast
text‹ A slightly ad-hoc but useful lemma in constructing homotopies.› lemma continuous_on_homotopic_join_lemma: fixes q :: "[real,real] ==> 'a::topological_space" assumes p: "continuous_on ({0..1} × {0..1}) (λy. p (fst y) (snd y))" (is"continuous_on ?A ?p") and q: "continuous_on ({0..1} × {0..1}) (λy. q (fst y) (snd y))" (is"continuous_on ?A ?q") and pf: "∧t. t ∈ {0..1} ==> pathfinish(p t) = pathstart(q t)" shows"continuous_on ({0..1} × {0..1}) (λy. (p(fst y) +++ q(fst y)) (snd y))" proof - have🍋: "(λt. p (fst t) (2 * snd t)) = ?p ∘ (λy. (fst y, 2 * snd y))" "(λt. q (fst t) (2 * snd t - 1)) = ?q ∘ (λy. (fst y, 2 * snd y - 1))" by force+ show ?thesis unfolding joinpaths_def proof (rule continuous_on_cases_le) show"continuous_on {y ∈ ?A. snd y ≤ 1/2} (λt. p (fst t) (2 * snd t))" "continuous_on {y ∈ ?A. 1/2 ≤ snd y} (λt. q (fst t) (2 * snd t - 1))" "continuous_on ?A snd" unfolding🍋 by (rule continuous_intros continuous_on_subset [OF p] continuous_on_subset [OF q] | force)+ qed (use pf in‹auto simp: mult.commute pathstart_def pathfinish_def›) qed
text‹ Congruence properties of homotopy w.r.t. path-combining operations.›
proposition homotopic_paths_reversepath: "homotopic_paths S (reversepath p) (reversepath q) ⟷ homotopic_paths S p q" using homotopic_paths_reversepath_D by force
proposition homotopic_paths_continuous_image: "[homotopic_paths S f g; continuous_on S h; h ∈ S → t]==> homotopic_paths t (h ∘ f) (h ∘ g)" unfolding homotopic_paths_def by (simp add: homotopic_with_compose_continuous_map_left pathfinish_compose pathstart_compose image_subset_iff_funcset)
subsection‹Group properties for homotopy of paths›
text🍋‹tag important›\<open>So taking equivalence classes under homotopy would give the fundamental group›
proposition homotopic_paths_rid: assumes"path p""path_image p ⊆ S" shows"homotopic_paths S (p +++ linepath (pathfinish p) (pathfinish p)) p" proof - have🍋: "continuous_on {0..1} (λt::real. if t ≤ 1/2 then 2 *🪙R t else 1)" unfolding split_01 by (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def)+ show ?thesis apply (rule homotopic_paths_sym) using assms unfolding pathfinish_def joinpaths_def by (intro 🍋 continuous_on_cases continuous_intros homotopic_paths_reparametrize [where f = "λt. if t ≤ 1/2 then 2 *🪙R t else 1"]; force) qed
proposition homotopic_paths_lid: "[path p; path_image p ⊆ S]==> homotopic_paths S (linepath (pathstart p) (pathstart p) +++ p) p" using homotopic_paths_rid [of "reversepath p" S] by (metis homotopic_paths_reversepath path_image_reversepath path_reversepath pathfinish_linepath
pathfinish_reversepath reversepath_joinpaths reversepath_linepath)
lemma homotopic_paths_rid': assumes"path p""path_image p ⊆ s""x = pathfinish p" shows"homotopic_paths s (p +++ linepath x x) p" using homotopic_paths_rid[of p s] assms by simp
lemma homotopic_paths_lid': "[path p; path_image p ⊆ s; x = pathstart p]==> homotopic_paths s (linepath x x +++ p) p" using homotopic_paths_lid[of p s] by simp
proposition homotopic_paths_assoc: "[path p; path_image p ⊆ S; path q; path_image q ⊆ S; path r; path_image r ⊆ S; pathfinish p = pathstart q; pathfinish q = pathstart r] ==> homotopic_paths S (p +++ (q +++ r)) ((p +++ q) +++ r)" apply (subst homotopic_paths_sym) apply (rule homotopic_paths_reparametrize
[where f = "λt. if t ≤ 1/2 then inverse 2 *🪙R t else if t ≤ 3 / 4 then t - (1 / 4) else 2 *🪙R t - 1"]) apply (simp_all del: le_divide_eq_numeral1 add: subset_path_image_join) apply (rule continuous_on_cases_1 continuous_intros | auto simp: joinpaths_def)+ done
proposition homotopic_paths_rinv: assumes"path p""path_image p ⊆ S" shows"homotopic_paths S (p +++ reversepath p) (linepath (pathstart p) (pathstart p))" proof - have p: "continuous_on {0..1} p" using assms by (auto simp: path_def) let ?A = "{0..1} × {0..1}" have"continuous_on ?A (λx. (subpath 0 (fst x) p +++ reversepath (subpath 0 (fst x) p)) (snd x))" unfolding joinpaths_def subpath_def reversepath_def path_def add_0_right diff_0_right proof (rule continuous_on_cases_le) show"continuous_on {x ∈ ?A. snd x ≤ 1/2} (λt. p (fst t * (2 * snd t)))" "continuous_on {x ∈ ?A. 1/2 ≤ snd x} (λt. p (fst t * (1 - (2 * snd t - 1))))" "continuous_on ?A snd" by (intro continuous_on_compose2 [OF p] continuous_intros; auto simp: mult_le_one)+ qed (auto simp: algebra_simps) thenshow ?thesis using assms apply (subst homotopic_paths_sym_eq) unfolding homotopic_paths_def homotopic_with_def apply (rule_tac x="(λy. (subpath 0 (fst y) p +++ reversepath(subpath 0 (fst y) p)) (snd y))"in exI) apply (force simp: mult_le_one path_defs joinpaths_def subpath_def reversepath_def) done qed
proposition homotopic_paths_linv: assumes"path p""path_image p ⊆ S" shows"homotopic_paths S (reversepath p +++ p) (linepath (pathfinish p) (pathfinish p))" using homotopic_paths_rinv [of "reversepath p" S] assms by simp
subsection‹Homotopy of loops without requiring preservation of endpoints›
definition🍋‹tag important› homotopic_loops :: "'a::topological_space set ==> (real ==> 'a) ==> (real ==> 'a) ==> bool"where "homotopic_loops S p q ≡ homotopic_with_canon (λr. pathfinish r = pathstart r) {0..1} S p q"
lemma homotopic_loops: "homotopic_loops S p q ⟷ (∃h. continuous_on ({0..1::real} × {0..1}) h ∧ h ∈ ({0..1} × {0..1}) → S ∧ (∀x ∈ {0..1}. h(0,x) = p x) ∧ (∀x ∈ {0..1}. h(1,x) = q x) ∧ (∀t ∈ {0..1}. pathfinish(h ∘ Pair t) = pathstart(h ∘ Pair t)))" by (simp add: homotopic_loops_def pathstart_def pathfinish_def homotopic_with)
proposition homotopic_loops_imp_loop: "homotopic_loops S p q ==> pathfinish p = pathstart p ∧ pathfinish q = pathstart q" using homotopic_with_imp_property homotopic_loops_def by blast
proposition homotopic_loops_imp_path: "homotopic_loops S p q ==> path p ∧ path q" unfolding homotopic_loops_def path_def using homotopic_with_imp_continuous_maps continuous_map_subtopology_eu by blast
proposition homotopic_loops_imp_subset: "homotopic_loops S p q ==> path_image p ⊆ S ∧ path_image q ⊆ S" unfolding homotopic_loops_def path_image_def by (simp add: homotopic_with_imp_subset1 homotopic_with_imp_subset2)
proposition homotopic_loops_refl: "homotopic_loops S p p ⟷ path p ∧ path_image p ⊆ S ∧ pathfinish p = pathstart p" by (metis (mono_tags, lifting) homotopic_loops_def homotopic_paths_def
homotopic_paths_refl homotopic_with_refl)
proposition homotopic_loops_sym: "homotopic_loops S p q ==> homotopic_loops S q p" by (simp add: homotopic_loops_def homotopic_with_sym)
proposition homotopic_loops_sym_eq: "homotopic_loops S p q ⟷ homotopic_loops S q p" by (metis homotopic_loops_sym)
proposition homotopic_loops_trans: "[homotopic_loops S p q; homotopic_loops S q r]==> homotopic_loops S p r" unfolding homotopic_loops_def by (blast intro: homotopic_with_trans)
proposition homotopic_loops_subset: "[homotopic_loops S p q; S ⊆ t]==> homotopic_loops t p q" by (fastforce simp: homotopic_loops)
proposition homotopic_loops_eq: "[path p; path_image p ⊆ S; pathfinish p = pathstart p; ∧t. t ∈ {0..1} ==> p(t) = q(t)] ==> homotopic_loops S p q" unfolding homotopic_loops_def path_image_def path_def pathstart_def pathfinish_def image_subset_iff_funcset using homotopic_with_eq [OF homotopic_with_refl [where f = p, THEN iffD2]] by fastforce
proposition homotopic_loops_continuous_image: "[homotopic_loops S f g; continuous_on S h; h ∈ S → t]==> homotopic_loops t (h ∘ f) (h ∘ g)" unfolding homotopic_loops_def by (simp add: homotopic_with_compose_continuous_map_left pathfinish_def pathstart_def image_subset_iff_funcset)
subsection‹Relations between the two variants of homotopy›
proposition homotopic_paths_imp_homotopic_loops: "[homotopic_paths S p q; pathfinish p = pathstart p; pathfinish q = pathstart p]==> homotopic_loops S p q" by (auto simp: homotopic_with_def homotopic_paths_def homotopic_loops_def)
proposition homotopic_loops_imp_homotopic_paths_null: assumes"homotopic_loops S p (linepath a a)" shows"homotopic_paths S p (linepath (pathstart p) (pathstart p))" proof - have"path p"by (metis assms homotopic_loops_imp_path) have ploop: "pathfinish p = pathstart p"by (metis assms homotopic_loops_imp_loop) have pip: "path_image p ⊆ S"by (metis assms homotopic_loops_imp_subset) let ?A = "{0..1::real} × {0..1::real}" obtain h where conth: "continuous_on ?A h" and hs: "h ∈ ?A → S" and h0[simp]: "∧x. x ∈ {0..1} ==> h(0,x) = p x" and h1[simp]: "∧x. x ∈ {0..1} ==> h(1,x) = a" and ends: "∧t. t ∈ {0..1} ==> pathfinish (h ∘ Pair t) = pathstart (h ∘ Pair t)" using assms by (auto simp: homotopic_loops homotopic_with image_subset_iff_funcset) have conth0: "path (λu. h (u, 0))" unfolding path_def proof (rule continuous_on_compose [of _ _ h, unfolded o_def]) show"continuous_on ((λx. (x, 0)) ` {0..1}) h" by (force intro: continuous_on_subset [OF conth]) qed (force intro: continuous_intros) have pih0: "path_image (λu. h (u, 0)) ⊆ S" using hs by (force simp: path_image_def) have c1: "continuous_on ?A (λx. h (fst x * snd x, 0))" proof (rule continuous_on_compose [of _ _ h, unfolded o_def]) show"continuous_on ((λx. (fst x * snd x, 0)) ` ?A) h" by (force simp: mult_le_one intro: continuous_on_subset [OF conth]) qed (force intro: continuous_intros)+ have c2: "continuous_on ?A (λx. h (fst x - fst x * snd x, 0))" proof (rule continuous_on_compose [of _ _ h, unfolded o_def]) show"continuous_on ((λx. (fst x - fst x * snd x, 0)) ` ?A) h" by (auto simp: algebra_simps add_increasing2 mult_left_le intro: continuous_on_subset [OF conth]) qed (force intro: continuous_intros) have [simp]: "∧t. [0 ≤ t ∧ t ≤ 1]==> h (t, 1) = h (t, 0)" using ends by (simp add: pathfinish_def pathstart_def) have adhoc_le: "c * 4 ≤ 1 + c * (d * 4)"if"¬ d * 4 ≤ 3""0 ≤ c""c ≤ 1"for c d::real proof - have"c * 3 ≤ c * (d * 4)"using that less_eq_real_def by auto with‹c ≤ 1›show ?thesis by fastforce qed have *: "∧p x. [path p ∧ path(reversepath p); path_image p ⊆ S ∧ path_image(reversepath p) ⊆ S; pathfinish p = pathstart(linepath a a +++ reversepath p) ∧ pathstart(reversepath p) = a ∧ pathstart p = x] ==> homotopic_paths S (p +++ linepath a a +++ reversepath p) (linepath x x)" by (metis homotopic_paths_lid homotopic_paths_join
homotopic_paths_trans homotopic_paths_sym homotopic_paths_rinv) have 1: "homotopic_paths S p (p +++ linepath (pathfinish p) (pathfinish p))" using‹path p› homotopic_paths_rid homotopic_paths_sym pip by blast moreoverhave"homotopic_paths S (p +++ linepath (pathfinish p) (pathfinish p)) (linepath (pathstart p) (pathstart p) +++ p +++ linepath (pathfinish p) (pathfinish p))" using homotopic_paths_lid [of "p +++ linepath (pathfinish p) (pathfinish p)" S] by (metis 1 homotopic_paths_imp_path homotopic_paths_imp_subset homotopic_paths_sym pathstart_join) moreover have"homotopic_paths S (linepath (pathstart p) (pathstart p) +++ p +++ linepath (pathfinish p) (pathfinish p)) ((λu. h (u, 0)) +++ linepath a a +++ reversepath (λu. h (u, 0)))" unfolding homotopic_paths_def homotopic_with_def proof (intro exI strip conjI) let ?h = "λy. (subpath 0 (fst y) (λu. h (u, 0)) +++ (λu. h (Pair (fst y) u)) +++ subpath (fst y) 0 (λu. h (u, 0))) (snd y)" have"continuous_on ?A ?h" by (intro continuous_on_homotopic_join_lemma; simp add: path_defs joinpaths_def subpath_def conth c1 c2) moreoverhave"?h ∈ ?A → S" using hs unfolding joinpaths_def subpath_def by (force simp: algebra_simps mult_le_one mult_left_le intro: adhoc_le) ultimatelyshow"continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1})) (top_of_set S) ?h" by (simp add: subpath_reversepath image_subset_iff_funcset) qed (use ploop in‹simp_all add: reversepath_def path_defs joinpaths_def o_def subpath_def conth c1 c2›) moreoverhave"homotopic_paths S ((λu. h (u, 0)) +++ linepath a a +++ reversepath (λu. h (u, 0))) (linepath (pathstart p) (pathstart p))" by (rule *; simp add: pih0 pathstart_def pathfinish_def conth0; simp add: reversepath_def joinpaths_def) ultimatelyshow ?thesis by (blast intro: homotopic_paths_trans) qed
proposition homotopic_loops_conjugate: fixes S :: "'a::real_normed_vector set" assumes"path p""path q"and pip: "path_image p ⊆ S"and piq: "path_image q ⊆ S" and pq: "pathfinish p = pathstart q"and qloop: "pathfinish q = pathstart q" shows"homotopic_loops S (p +++ q +++ reversepath p) q" proof - have contp: "continuous_on {0..1} p"using‹path p› [unfolded path_def] by blast have contq: "continuous_on {0..1} q"using‹path q› [unfolded path_def] by blast let ?A = "{0..1::real} × {0..1::real}" have c1: "continuous_on ?A (λx. p ((1 - fst x) * snd x + fst x))" proof (rule continuous_on_compose [of _ _ p, unfolded o_def]) show"continuous_on ((λx. (1 - fst x) * snd x + fst x) ` ?A) p" by (auto intro: continuous_on_subset [OF contp] simp: algebra_simps add_increasing2 mult_right_le_one_le sum_le_prod1) qed (force intro: continuous_intros) have c2: "continuous_on ?A (λx. p ((fst x - 1) * snd x + 1))" proof (rule continuous_on_compose [of _ _ p, unfolded o_def]) show"continuous_on ((λx. (fst x - 1) * snd x + 1) ` ?A) p" by (auto intro: continuous_on_subset [OF contp] simp: algebra_simps add_increasing2 mult_left_le_one_le) qed (force intro: continuous_intros)
have ps1: "∧a b. [b * 2 ≤ 1; 0 ≤ b; 0 ≤ a; a ≤ 1]==> p ((1 - a) * (2 * b) + a) ∈S" using sum_le_prod1 by (force simp: algebra_simps add_increasing2 mult_left_le intro: pip [unfolded path_image_def, THEN subsetD]) have ps2: "∧a b. [¬ 4 * b ≤ 3; b ≤ 1; 0 ≤ a; a ≤ 1]==> p ((a - 1) * (4 * b - 3) + 1) ∈ S" apply (rule pip [unfolded path_image_def, THEN subsetD]) apply (rule image_eqI, blast) apply (simp add: algebra_simps) by (metis add_mono affine_ineq linear mult.commute mult.left_neutral mult_right_mono
add.commute zero_le_numeral) have qs: "∧a b. [4 * b ≤ 3; ¬ b * 2 ≤ 1]==> q (4 * b - 2) ∈ S" using path_image_def piq by fastforce have"homotopic_loops S (p +++ q +++ reversepath p) (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q))" unfolding homotopic_loops_def homotopic_with_def proof (intro exI strip conjI) let ?h = "(λy. (subpath (fst y) 1 p +++ q +++ subpath 1 (fst y) p) (snd y))" have"continuous_on ?A (λy. q (snd y))" by (force simp: contq intro: continuous_on_compose [of _ _ q, unfolded o_def] continuous_on_id continuous_on_snd) thenhave"continuous_on ?A ?h" using pq qloop by (intro continuous_on_homotopic_join_lemma) (auto simp: path_defs joinpaths_def subpath_def c1 c2) thenshow"continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1})) (top_of_set S) ?h" by (auto simp: joinpaths_def subpath_def ps1 ps2 qs) show"?h (1,x) = (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q)) x"for x using pq by (simp add: pathfinish_def subpath_refl) qed (auto simp: subpath_reversepath) moreoverhave"homotopic_loops S (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q)) q" proof - have"homotopic_paths S (linepath (pathfinish q) (pathfinish q) +++ q) q" using‹path q› homotopic_paths_lid qloop piq by auto hence 1: "∧f. homotopic_paths S f q ∨¬ homotopic_paths S f (linepath (pathfinish q) (pathfinish q) +++ q)" using homotopic_paths_trans by blast hence"homotopic_paths S (linepath (pathfinish q) (pathfinish q) +++ q +++ linepath (pathfinish q) (pathfinish q)) q" by (smt (verit, best) ‹path q› homotopic_paths_imp_path homotopic_paths_imp_subset homotopic_paths_lid
homotopic_paths_rid homotopic_paths_trans pathstart_join piq qloop) thus ?thesis by (metis (no_types) qloop homotopic_loops_sym homotopic_paths_imp_homotopic_loops homotopic_paths_imp_pathfinish homotopic_paths_sym) qed ultimatelyshow ?thesis by (blast intro: homotopic_loops_trans) qed
lemma homotopic_paths_loop_parts: assumes loops: "homotopic_loops S (p +++ reversepath q) (linepath a a)"and"path q" shows"homotopic_paths S p q" proof - have paths: "homotopic_paths S (p +++ reversepath q) (linepath (pathstart p) (pathstart p))" using homotopic_loops_imp_homotopic_paths_null [OF loops] by simp thenhave"path p" using‹path q› homotopic_loops_imp_path loops path_join path_join_path_ends path_reversepath by blast show ?thesis proof (cases "pathfinish p = pathfinish q") case True obtain pipq: "path_image p ⊆ S""path_image q ⊆ S" by (metis Un_subset_iff paths ‹path p›‹path q› homotopic_loops_imp_subset homotopic_paths_imp_path loops
path_image_join path_image_reversepath path_imp_reversepath path_join_eq) have"homotopic_paths S p (p +++ (linepath (pathfinish p) (pathfinish p)))" using‹path p›‹path_image p ⊆ S› homotopic_paths_rid homotopic_paths_sym by blast moreoverhave"homotopic_paths S (p +++ (linepath (pathfinish p) (pathfinish p))) (p +++ (reversepath q +++ q))" by (simp add: True ‹path p›‹path q› pipq homotopic_paths_join homotopic_paths_linv homotopic_paths_sym) moreoverhave"homotopic_paths S (p +++ (reversepath q +++ q)) ((p +++ reversepath q) +++ q)" by (simp add: True ‹path p›‹path q› homotopic_paths_assoc pipq) moreoverhave"homotopic_paths S ((p +++ reversepath q) +++ q) (linepath (pathstart p) (pathstart p) +++ q)" by (simp add: ‹path q› homotopic_paths_join paths pipq) ultimatelyshow ?thesis by (metis ‹path q› homotopic_paths_imp_path homotopic_paths_lid homotopic_paths_trans path_join_path_ends pathfinish_linepath pipq(2)) next case False thenshow ?thesis using‹path q› homotopic_loops_imp_path loops path_join_path_ends by fastforce qed qed
subsection🍋‹tag unimportant›\<open>Homotopy of "nearby"function, paths and loops›
lemma homotopic_with_linear: fixes f g :: "_ ==> 'b::real_normed_vector" assumes contf: "continuous_on S f" and contg:"continuous_on S g" and sub: "∧x. x ∈ S ==> closed_segment (f x) (g x) ⊆ t" shows"homotopic_with_canon (λz. True) S t f g" unfolding homotopic_with_def apply (rule_tac x="λy. ((1 - (fst y)) *🪙R f(snd y) + (fst y) *🪙R g(snd y))"in exI) using sub closed_segment_def by (fastforce intro: continuous_intros continuous_on_subset [OF contf] continuous_on_compose2 [where g=f]
continuous_on_subset [OF contg] continuous_on_compose2 [where g=g])
lemma homotopic_paths_linear: fixes g h :: "real ==> 'a::real_normed_vector" assumes"path g""path h""pathstart h = pathstart g""pathfinish h = pathfinish g" "∧t. t ∈ {0..1} ==> closed_segment (g t) (h t) ⊆ S" shows"homotopic_paths S g h" using assms unfolding path_def apply (simp add: closed_segment_def pathstart_def pathfinish_def homotopic_paths_def homotopic_with_def) apply (rule_tac x="λy. ((1 - (fst y)) *🪙R (g ∘ snd) y + (fst y) *🪙R (h ∘ snd) y)"in exI) apply (intro conjI subsetI continuous_intros; force) done
lemma homotopic_loops_linear: fixes g h :: "real ==> 'a::real_normed_vector" assumes"path g""path h""pathfinish g = pathstart g""pathfinish h = pathstart h" "∧t x. t ∈ {0..1} ==> closed_segment (g t) (h t) ⊆ S" shows"homotopic_loops S g h" using assms unfolding path_defs homotopic_loops_def homotopic_with_def apply (rule_tac x="λy. ((1 - (fst y)) *🪙R g(snd y) + (fst y) *🪙R h(snd y))"in exI) by (force simp: closed_segment_def intro!: continuous_intros intro: continuous_on_compose2 [where g=g] continuous_on_compose2 [where g=h])
lemma homotopic_paths_nearby_explicit: assumes🍋: "path g""path h""pathstart h = pathstart g""pathfinish h = pathfinish g" and no: "∧t x. [t ∈ {0..1}; x ∉ S]==> norm(h t - g t) < norm(g t - x)" shows"homotopic_paths S g h" using homotopic_paths_linear [OF 🍋] by (metis linorder_not_le no norm_minus_commute segment_bound1 subsetI)
lemma homotopic_loops_nearby_explicit: assumes🍋: "path g""path h""pathfinish g = pathstart g""pathfinish h = pathstart h" and no: "∧t x. [t ∈ {0..1}; x ∉ S]==> norm(h t - g t) < norm(g t - x)" shows"homotopic_loops S g h" using homotopic_loops_linear [OF 🍋] by (metis linorder_not_le no norm_minus_commute segment_bound1 subsetI)
lemma homotopic_nearby_paths: fixes g h :: "real ==> 'a::euclidean_space" assumes"path g""open S""path_image g ⊆ S" shows"∃e. 0 < e ∧ (∀h. path h ∧ pathstart h = pathstart g ∧ pathfinish h = pathfinish g ∧ (∀t ∈ {0..1}. norm(h t - g t) < e) ⟶ homotopic_paths S g h)" proof - obtain e where"e > 0"and e: "∧x y. x ∈ path_image g ==> y ∈ - S ==> e ≤ dist x y" using separate_compact_closed [of "path_image g""-S"] assms by force show ?thesis using e [unfolded dist_norm] ‹e > 0› by (fastforce simp: path_image_def intro!: homotopic_paths_nearby_explicit assms exI) qed
lemma homotopic_nearby_loops: fixes g h :: "real ==> 'a::euclidean_space" assumes"path g""open S""path_image g ⊆ S""pathfinish g = pathstart g" shows"∃e. 0 < e ∧ (∀h. path h ∧ pathfinish h = pathstart h ∧ (∀t ∈ {0..1}. norm(h t - g t) < e) ⟶ homotopic_loops S g h)" proof - obtain e where"e > 0"and e: "∧x y. x ∈ path_image g ==> y ∈ - S ==> e ≤ dist x y" using separate_compact_closed [of "path_image g""-S"] assms by force show ?thesis using e [unfolded dist_norm] ‹e > 0› by (fastforce simp: path_image_def intro!: homotopic_loops_nearby_explicit assms exI) qed
subsection‹ Homotopy and subpaths›
lemma homotopic_join_subpaths1: assumes"path g"and pag: "path_image g ⊆ S" and u: "u ∈ {0..1}"and v: "v ∈ {0..1}"and w: "w ∈ {0..1}""u ≤ v""v ≤ w" shows"homotopic_paths S (subpath u v g +++ subpath v w g) (subpath u w g)" proof - have 1: "t * 2 ≤ 1 ==> u + t * (v * 2) ≤ v + t * (u * 2)"for t using affine_ineq ‹u ≤ v›by fastforce have 2: "t * 2 > 1 ==> u + (2*t - 1) * v ≤ v + (2*t - 1) * w"for t by (metis add_mono_thms_linordered_semiring(1) diff_gt_0_iff_gt less_eq_real_def mult.commute mult_right_mono ‹u ≤ v›‹v ≤ w›) have t2: "∧t::real. t*2 = 1 ==> t = 1/2"by auto have"homotopic_paths (path_image g) (subpath u v g +++ subpath v w g) (subpath u w g)" proof (cases "w = u") case True thenshow ?thesis by (metis ‹path g› homotopic_paths_rinv path_image_subpath_subset path_subpath pathstart_subpath reversepath_subpath subpath_refl u v) next case False let ?f = "λt. if t ≤ 1/2 then inverse((w - u)) *🪙R (2 * (v - u)) *🪙R t else inverse((w - u)) *🪙R ((v - u) + (w - v) *🪙R (2 *🪙R t - 1))" show ?thesis proof (rule homotopic_paths_sym [OF homotopic_paths_reparametrize [where f = ?f]]) show"path (subpath u w g)" using assms(1) path_subpath u w(1) by blast show"path_image (subpath u w g) ⊆ path_image g" by (meson path_image_subpath_subset u w(1)) show"continuous_on {0..1} ?f" unfolding split_01 by (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def dest!: t2)+ show"?f ∈ {0..1} → {0..1}" using False assms by (force simp: field_simps not_le mult_left_mono affine_ineq dest!: 1 2) show"(subpath u v g +++ subpath v w g) t = subpath u w g (?f t)"if"t ∈ {0..1}"for t using assms unfolding joinpaths_def subpath_def by (auto simp: divide_simps add.commute mult.commute mult.left_commute) qed (use False in auto) qed thenshow ?thesis by (rule homotopic_paths_subset [OF _ pag]) qed
lemma homotopic_join_subpaths2: assumes"homotopic_paths S (subpath u v g +++ subpath v w g) (subpath u w g)" shows"homotopic_paths S (subpath w v g +++ subpath v u g) (subpath w u g)" by (metis assms homotopic_paths_reversepath_D pathfinish_subpath pathstart_subpath reversepath_joinpaths reversepath_subpath)
lemma homotopic_join_subpaths3: assumes hom: "homotopic_paths S (subpath u v g +++ subpath v w g) (subpath u w g)" and"path g"and pag: "path_image g ⊆ S" and u: "u ∈ {0..1}"and v: "v ∈ {0..1}"and w: "w ∈ {0..1}" shows"homotopic_paths S (subpath v w g +++ subpath w u g) (subpath v u g)" proof - obtain wvg: "path (subpath w v g)""path_image (subpath w v g) ⊆ S" and wug: "path (subpath w u g)""path_image (subpath w u g) ⊆ S" and vug: "path (subpath v u g)""path_image (subpath v u g) ⊆ S" by (meson ‹path g› pag path_image_subpath_subset path_subpath subset_trans u v w) have"homotopic_paths S (subpath u w g +++ subpath w v g) ((subpath u v g +++ subpath v w g) +++ subpath w v g)" by (simp add: hom homotopic_paths_join homotopic_paths_sym wvg) alsohave"homotopic_paths S … (subpath u v g +++ subpath v w g +++ subpath w v g)" using wvg vug ‹path g› by (metis homotopic_paths_assoc homotopic_paths_sym path_image_subpath_commute path_subpath
pathfinish_subpath pathstart_subpath u v w) alsohave"homotopic_paths S … (subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g)))" using wvg vug ‹path g› by (metis homotopic_paths_join homotopic_paths_linv homotopic_paths_refl path_image_subpath_commute
path_subpath pathfinish_subpath pathstart_join pathstart_subpath reversepath_subpath u v) alsohave"homotopic_paths S … (subpath u v g)" using vug ‹path g›by (metis homotopic_paths_rid path_image_subpath_commute path_subpath u v) finallyhave"homotopic_paths S (subpath u w g +++ subpath w v g) (subpath u v g)". thenshow ?thesis using homotopic_join_subpaths2 by blast qed
proposition homotopic_join_subpaths: "[path g; path_image g ⊆ S; u ∈ {0..1}; v ∈ {0..1}; w ∈ {0..1}] ==> homotopic_paths S (subpath u v g +++ subpath v w g) (subpath u w g)" by (smt (verit, del_insts) homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3)
text‹Relating homotopy of trivial loops to path-connectedness.›
lemma path_component_imp_homotopic_points: assumes"path_component S a b" shows"homotopic_loops S (linepath a a) (linepath b b)" proof - obtain g :: "real ==> 'a"where g: "continuous_on {0..1} g""g ∈ {0..1} → S""g 0 = a""g 1 = b" using assms by (auto simp: path_defs) thenhave"continuous_on ({0..1} × {0..1}) (g ∘ fst)" by (fastforce intro!: continuous_intros)+ with g show ?thesis by (auto simp: homotopic_loops_def homotopic_with_def path_defs Pi_iff) qed
lemma homotopic_loops_imp_path_component_value: "[homotopic_loops S p q; 0 ≤ t; t ≤ 1]==> path_component S (p t) (q t)" apply (clarsimp simp: homotopic_loops_def homotopic_with_def path_defs) apply (rule_tac x="h ∘ (λu. (u, t))"in exI) apply (fastforce elim!: continuous_on_subset intro!: continuous_intros) done
lemma homotopic_points_eq_path_component: "homotopic_loops S (linepath a a) (linepath b b) ⟷ path_component S a b" using homotopic_loops_imp_path_component_value path_component_imp_homotopic_points by fastforce
lemma path_connected_eq_homotopic_points: "path_connected S ⟷ (∀a b. a ∈ S ∧ b ∈ S ⟶ homotopic_loops S (linepath a a) (linepath b b))" by (auto simp: path_connected_def path_component_def homotopic_points_eq_path_component)
subsection‹Simply connected sets›
text🍋‹tag important›\<open>defined as "all loops are homotopic (as loops)›
definition🍋‹tag important› simply_connected where "simply_connected S ≡ ∀p q. path p ∧ pathfinish p = pathstart p ∧ path_image p ⊆ S ∧
path q ∧ pathfinish q = pathstart q ∧ path_image q ⊆ S ⟶ homotopic_loops S p q"
lemma simply_connected_empty [iff]: "simply_connected {}" by (simp add: simply_connected_def)
lemma simply_connected_imp_path_connected: fixes S :: "_::real_normed_vector set" shows "simply_connected S ==> path_connected S" by (simp add: simply_connected_def path_connected_eq_homotopic_points)
lemma simply_connected_imp_connected: fixes S :: "_::real_normed_vector set" shows "simply_connected S ==> connected S" by (simp add: path_connected_imp_connected simply_connected_imp_path_connected)
lemma simply_connected_eq_contractible_loop_any: fixes S :: "_::real_normed_vector set" shows "simply_connected S ⟷
(∀p a. path p ∧ path_image p ⊆ S ∧ pathfinish p = pathstart p ∧ a ∈ S ⟶ homotopic_loops S p (linepath a a))" (is "?lhs = ?rhs") proof assume ?rhs then show ?lhs unfolding simply_connected_def by (metis pathfinish_in_path_image subsetD homotopic_loops_trans homotopic_loops_sym) qed (force simp: simply_connected_def)
lemma simply_connected_eq_contractible_loop_some: fixes S :: "_::real_normed_vector set" shows "simply_connected S ⟷
path_connected S ∧
(∀p. path p ∧ path_image p ⊆ S ∧ pathfinish p = pathstart p ⟶ (∃a. a ∈ S ∧ homotopic_loops S p (linepath a a)))" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs using simply_connected_eq_contractible_loop_any by (blast intro: simply_connected_imp_path_connected) next assume ?rhs then show ?lhs by (meson homotopic_loops_trans path_connected_eq_homotopic_points simply_connected_eq_contractible_loop_any) qed
lemma simply_connected_eq_contractible_loop_all: fixes S :: "_::real_normed_vector set" shows "simply_connected S ⟷
S = {} ∨
(∃a ∈ S. ∀p. path p ∧ path_image p ⊆ S ∧ pathfinish p = pathstart p ⟶ homotopic_loops S p (linepath a a))" by (meson ex_in_conv homotopic_loops_sym homotopic_loops_trans simply_connected_def simply_connected_eq_contractible_loop_any)
lemma simply_connected_eq_contractible_path: fixes S :: "_::real_normed_vector set" shows "simply_connected S ⟷
path_connected S ∧
(∀p. path p ∧ path_image p ⊆ S ∧ pathfinish p = pathstart p ⟶ homotopic_paths S p (linepath (pathstart p) (pathstart p)))" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs unfolding simply_connected_imp_path_connected by (metis simply_connected_eq_contractible_loop_some homotopic_loops_imp_homotopic_paths_null) next assume ?rhs then show ?lhs using homotopic_paths_imp_homotopic_loops simply_connected_eq_contractible_loop_some by fastforce qed
lemma simply_connected_eq_homotopic_paths: fixes S :: "_::real_normed_vector set" shows "simply_connected S ⟷
path_connected S ∧
(∀p q. path p ∧ path_image p ⊆ S ∧
path q ∧ path_image q ⊆ S ∧
pathstart q = pathstart p ∧ pathfinish q = pathfinish p ⟶ homotopic_paths S p q)" (is "?lhs = ?rhs") proof assume ?lhs then have pc: "path_connected S" and *: "∧p. [path p; path_image p ⊆ S;
pathfinish p = pathstart p] ==> homotopic_paths S p (linepath (pathstart p) (pathstart p))" by (auto simp: simply_connected_eq_contractible_path) have "homotopic_paths S p q" if "path p" "path_image p ⊆ S" "path q" "path_image q ⊆ S" "pathstart q = pathstart p" "pathfinish q = pathfinish p" for p q proof - have "homotopic_paths S p (p +++ reversepath q +++ q)" using that by (smt (verit, best) homotopic_paths_join homotopic_paths_linv homotopic_paths_rid homotopic_paths_sym homotopic_paths_trans pathstart_linepath) also have "homotopic_paths S … ((p +++ reversepath q) +++ q)" by (simp add: that homotopic_paths_assoc) also have "homotopic_paths S … (linepath (pathstart q) (pathstart q) +++ q)" using * [of "p +++ reversepath q"] that by (simp add: homotopic_paths_assoc homotopic_paths_join path_image_join) also have "homotopic_paths S … q" using that homotopic_paths_lid by blast finally show ?thesis . qed then show ?rhs by (blast intro: pc *) next assume ?rhs then show ?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›]) moreover have "path_image (fst ∘ p) ⊆ S" using that by (force simp: path_image_def) ultimately have 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›]) moreover have "path_image (snd ∘ p) ⊆ T" using that by (force simp: path_image_def) ultimately have 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 subgoal for 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 then show ?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) then have "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) then have "homotopic_with_canon (λf. True) S U (g ∘ id ∘ f) (g ∘ (λx. b) ∘ f)" by (simp add: f homotopic_with_compose_continuous_map_right image_subset_iff_funcset) then show ?thesis by (simp add: comp_def that) qed
lemma nullhomotopic_into_contractible: assumes f: "continuous_on S f" "f ∈ S → T" 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 then show ?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 then have "homotopic_with_canon (λh. True) S U (λx. c2) (λx. c1)" by (auto simp: path_component homotopic_constant_maps) then show ?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) then have "∀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]) then show ?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)) then have "(λy. (1 - fst y) *🪙R snd y + fst y *🪙R a) ` ({0..1} × S) ⊆ S" using a [unfolded closed_segment_def] by force then have "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 then show ?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 then show ?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" then obtain 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) then have "S ∩ T ∩ (U1 ∩ U2) ⊆ V1 ∩ V2" "V1 ∩ V2 ⊆ S ∩ T ∩ A" "x ∈ S ∩ T ∩ (U1 ∩ U2)" by blast+ moreover have "P (V1 ∩ V2)" by (simp add: P ‹P V1›‹P V2›) ultimately show "∃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" then obtain 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 then obtain 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) then have "openin (top_of_set (S × T)) (U1 × V1)" by (simp add: openin_Times) moreover have "R (U2 × V2)" by (simp add: R opeS opeT) moreover have "U1 × V1 ⊆ U2 × V2 ∧ U2 × V2 ⊆ W" using opeS opeT ‹U × V ⊆ W› by auto ultimately show "∃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" then obtain A where T: "open A" "W = T ∩ A" by (force simp: openin_open) then have "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 then obtain 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) then have "openin (top_of_set T) (T ∩ g -` U)" using ‹continuous_on T g› continuous_on_open [THEN iffD1] by blast moreover have "∃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 then have 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) then have 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 ultimately show "∃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" then have "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]) then obtain x where "x ∈ S" "f x = y" using ‹W ⊆ f ` S›‹y ∈ W› by blast then obtain 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) then have "openin (top_of_set (f ` S)) (f ` U)" by (simp add: oo) then show "∃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) moreover have "S ⊆ ?A ∪ ?B" by clarsimp (meson opI) moreover have "openin (top_of_set S) ?A" by (subst openin_subopen, blast) moreover have "openin (top_of_set S) ?B" by (subst openin_subopen, blast) ultimately have "?A = {} ∨ ?B = {}" by (metis (no_types, lifting) ‹connected S› connected_openin) then show ?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) then show ?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) then show ?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) then show ?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 then show ?rhs by (smt (verit, del_insts) assms constant_on_def locally_constant_imp_constant locally_def openin_subtopology_self subset_iff) next assume ?rhs then show ?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 then show ?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 then have "∧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" then obtain e where "e>0" and "compact (cball x e ∩ S)" by (metis Int_commute compact_Int_closed compact_cball inf.right_idem R) moreover have "∀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) moreover have "openin (top_of_set S) (ball x e ∩ S)" by (simp add: inf_commute openin_open_Int) ultimately show "∃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 then obtain 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) moreover have "∀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) moreover have "K ⊆∪((λx. K ∩ u x) ` K)" using that by clarsimp (meson subsetCE uv) ultimately obtain D where "D ⊆ (λx. K ∩ u x) ` K" "finite D" "K ⊆∪D" by metis then obtain 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) ultimately show ?thesis using T by auto qed show ?rhs by (blast intro: *) next assume ?rhs then show ?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 then show ?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 then show ?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 moreover obtain e2 where "e2 > 0" and e2: "cball x e2 ∩ (S ∪ T) ⊆ S" by (meson ‹x ∈ S› opS openin_contains_cball) then have "cball x e2 ∩ (S ∪ T) = cball x e2 ∩ S" by force ultimately have "closed (cball x (min e1 e2) ∩ (S ∪ T))" by (metis (no_types, lifting) cball_min_Int closed_Int closed_cball inf_assoc inf_commute) then show ?thesis by (metis ‹0 < e1›‹0 < e2› min_def) qed moreover have "∃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 moreover obtain e2 where "e2 > 0" and e2: "cball x e2 ∩ (S ∪ T) ⊆ T" by (meson ‹x ∈ T› opT openin_contains_cball) then have "cball x e2 ∩ (S ∪ T) = cball x e2 ∩ T" by force moreover have "closed (cball x e1 ∩ (cball x e2 ∩ T))" by (metis closed_Int closed_cball e1 inf_left_commute) ultimately show ?thesis by (rule_tac x="min e1 e2" in exI) (simp add: ‹0 < e2› cball_min_Int inf_assoc) qed ultimately show ?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 moreover have "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) ultimately show ?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) then have "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 then show ?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) then have "closed (cball x (min e1 e2) ∩ (S ∪ T))" by (simp add: cball_min_Int inf_commute) ultimately show ?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) then have "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) then have "closed (cball x (min e1 e2) ∩ (S ∪ T))" by (auto simp: cball_min_Int) ultimately show ?thesis using ‹0 < e2› by (rule_tac x="min e1 e2" in exI) linarith qed ultimately show ?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 then show ?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) then show "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+ then obtain 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" and F: "F⊆ ?T" for F 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 F by blast then show "closedin (top_of_set S) (∩F)" by (meson cloTF closed_Inter closed_subset openin_imp_subset subset_eq) show "C ⊆∩F" using F by 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) moreover have "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+) ultimately have cloDV1: "closedin (top_of_set D) (D ∩ V1)" and cloDV2: "closedin (top_of_set D) (D ∩ V2)" by metis+ then obtain 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 = {}" then have *: "C ⊆ D ∩ V2" using D1 DV12 ‹C ⊆ D› by auto have 1: "openin (top_of_set S) (D ∩ V2)" by (simp add: ‹open V2› opeD openin_Int_open) have 2: "closedin (top_of_set S) (D ∩ V2)" using cloD cloDV2 closedin_trans by blast have "∩ ?T⊆ D ∩ V2" by (rule Inter_lower) (use * 1 2 in simp) then show False using K1 V12 ‹K1 ≠ {}›‹K1 ⊆ V1› closedin_imp_subset by blast qed moreover have "D ∩ U2 ∩ C ≠ {}" proof assume "D ∩ U2 ∩ C = {}" then have *: "C ⊆ D ∩ V1" using D2 DV12 ‹C ⊆ D› by auto have 1: "openin (top_of_set S) (D ∩ V1)" by (simp add: ‹open V1› opeD openin_Int_open) have 2: "closedin (top_of_set S) (D ∩ V1)" using cloD cloDV1 closedin_trans by blast have "∩?T⊆ D ∩ V1" by (rule Inter_lower) (use * 1 2 in simp) then show False using K2 V12 ‹K2 ≠ {}›‹K2 ⊆ V2› closedin_imp_subset by blast qed ultimately show 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 then show "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) then have 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" and F: "F⊆ ?T" for F 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 = {}" then have FUW: "∩F⊆ U ∩ W" by blast have "C ⊆∩F" using F by auto moreover have "compact (∩F)" by (metis (no_types, lifting) compact_Inter False mem_Collect_eq subsetCE F) moreover have "∩F⊆ K" using False that(2) by fastforce moreover have opeKF: "openin (top_of_set K) (∩F)" using False F‹finite F› by blast then have opeVF: "openin (top_of_set V) (∩F)" using W ‹K ⊆ S›‹V ⊆ K› opeKF ‹∩F⊆ K› FUW openin_subset_trans by fastforce then have "openin (top_of_set S) (∩F)" by (metis opeSV openin_trans) moreover have "∩F⊆ U" by (meson ‹V ⊆ U› opeVF dual_order.trans openin_imp_subset) ultimately show 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 then show ?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 then show 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" assume 1: "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" then have "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 then obtain 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 then have *: "openin ?SS (F y t) ∧ connected (G y t) ∧ y ∈ F y t ∧ F y t ⊆ G y t ∧ G y t ⊆ t" using 1 ‹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) then have "∃A. openin ?SS A ∧ y ∈ A ∧ A ⊆ connected_component_set t x" by (metis (no_types) * connected_component_eq dual_order.trans y) } then show ?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" assume 1: "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" then have "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 then obtain 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 then have *: "openin ?SS (F y t) ∧ path_connected (G y t) ∧ y ∈ F y t ∧ F y t ⊆ G y t ∧ G y t ⊆ t" using 1 ‹y ∈ t› by presburger have "G y t ⊆ path_component_set t y" using * path_component_maximal rev_subsetD by blast then have "∃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) } then show ?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) then show ?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 then show ?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 then have 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)) then show ?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 then show ?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 then show ?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" then obtain T e where "V = S ∩ T" "x ∈ S" "0 < e" "ball x e ⊆ T" by (metis Int_iff openE openin_open) then have "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) then show "∃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) moreover have "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) ultimately have *: "path_component_set S x = connected_component_set S x" by (metis connected_connected_component connected_clopen True path_component_eq_empty) then show ?thesis by blast next case False then show ?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" then have "C ⊆ U" "U ⊆ f ` S" by (meson in_components_subset openin_imp_subset)+ then have "openin (top_of_set (f ` S)) C ⟷
openin (top_of_set S) (S ∩ f -` C)" by (auto simp: oo) moreover have "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)" then have "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) then have "continuous_on (connected_component_set (S ∩ f -` U) x) f" by (meson connected_component_subset continuous_on_subset inf.boundedE) then have "connected (f ` connected_component_set (S ∩ f -` U) x)" by (rule connected_continuous_image [OF _ connected_connected_component]) moreover have "f ` connected_component_set (S ∩ f -` U) x ⊆ U" using connected_component_in by blast moreover have "C ∩ f ` connected_component_set (S ∩ f -` U) x ≠ {}" using ‹C ⊆ U›‹f x ∈ C›‹x ∈ S› by fastforce ultimately have 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" then have ?thesis using cUC connected_component_idemp connected_component_mono by blast } then show ?thesis using connected_component_eq_empty by auto qed also have "…⊆ (S ∩ f -` C)" by (rule connected_component_subset) finally show "connected_component_set (S ∩ f -` U) x ⊆ (S ∩ f -` C)" . qed qed ultimately show "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" then have "path_component_set U y ⊆ U" "U ⊆ f ` S" by (meson path_component_subset openin_imp_subset)+ then have "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 then show ?thesis using oo by blast qed moreover have "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)" then have "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)" then have "x ∉ (S ∩ f -` U)" by (metis (no_types, lifting) ‹U ⊆ f ` S› opefSU lcS oo locally_path_connected_open_path_component) then show 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) then have "continuous_on (path_component_set (S ∩ f -` U) x) f" by (meson Int_lower1 continuous_on_subset path_component_subset) then have "path_connected (f ` path_component_set (S ∩ f -` U) x)" by (simp add: path_connected_continuous_image) moreover have "f ` path_component_set (S ∩ f -` U) x ⊆ U" using path_component_mem by fastforce moreover have "f x ∈ f ` path_component_set (S ∩ f -` U) x" by (force simp: ‹x ∈ S›‹f x ∈ U› path_component_refl_eq) ultimately have "f ` (path_component_set (S ∩ f -` U) x) ⊆ path_component_set U (f x)" by (meson path_component_maximal) also have "…⊆ path_component_set U y" by (simp add: Uyfx path_component_maximal path_component_subset path_component_sym) finally have 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 then show ?thesis using path_component_path_component by blast qed also have "…⊆ (S ∩ f -` path_component_set U y)" by (rule path_component_subset) finally show "path_component_set (S ∩ f -` U) x ⊆ (S ∩ f -` path_component_set U y)" . qed qed ultimately show "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
lemma continuous_on_components: fixes f :: "'a::topological_space ==> 'b::topological_space" assumes "locally connected S " "∧C. C ∈ components S ==> continuous_on C f" shows "continuous_on S f" proof (rule continuous_on_components_gen) fix C assume "C ∈ components S" then show "openin (top_of_set S) C ∧ continuous_on C f" by (simp add: assms openin_components_locally_connected) qed
lemma continuous_on_components_eq: "locally connected S ==> (continuous_on S f ⟷ (∀c ∈ components S. continuous_on c f))" by (meson continuous_on_components continuous_on_subset in_components_subset)
lemma continuous_on_components_open: fixes S :: "'a::real_normed_vector set" assumes "open S " "∧c. c ∈ components S ==> continuous_on c f" shows "continuous_on S f" using continuous_on_components open_imp_locally_connected assms by blast
lemma continuous_on_components_open_eq: fixes S :: "'a::real_normed_vector set" shows "open S ==> (continuous_on S f ⟷ (∀c ∈ components S. continuous_on c f))" using continuous_on_subset in_components_subset by (blast intro: continuous_on_components_open)
lemma closedin_union_complement_components: assumes U: "locally connected U" and S: "closedin (top_of_set U) S" and cuS: "c ⊆ components(U - S)" shows "closedin (top_of_set U) (S ∪∪c)" proof - have di: "(∧S T. S ∈ c ∧ T ∈ c' ==> disjnt S T) ==> disjnt (∪ c) (∪ c')" for c' by (simp add: disjnt_def) blast have "S ⊆ U" using S closedin_imp_subset by blast moreover have "U - S = ∪c ∪∪(components (U - S) - c)" by (metis Diff_partition Union_components Union_Un_distrib assms(3)) moreover have "disjnt (∪c) (∪(components (U - S) - c))" apply (rule di) by (metis di DiffD1 DiffD2 assms(3) components_nonoverlap disjnt_def subsetCE) ultimately have eq: "S ∪∪c = U - (∪(components(U - S) - c))" by (auto simp: disjnt_def) have *: "openin (top_of_set U) (∪(components (U - S) - c))" proof (rule openin_Union [OF openin_trans [of "U - S"]]) show "openin (top_of_set (U - S)) T" if "T ∈ components (U - S) - c" for T using that by (simp add: U S locally_diff_closed openin_components_locally_connected) show "openin (top_of_set U) (U - S)" if "T ∈ components (U - S) - c" for T using that by (simp add: openin_diff S) qed have "closedin (top_of_set U) (U - ∪ (components (U - S) - c))" by (metis closedin_diff closedin_topspace topspace_euclidean_subtopology *) then have "openin (top_of_set U) (U - (U - ∪(components (U - S) - c)))" by (simp add: openin_diff) then show ?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) then show ?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]) then show ?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) then have 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) then have "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) also have "… = (∑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 also have "… = norm x ^2" by (simp add: x pairwise_ortho_scaleR Borth norm_sum_Pythagorean [OF ‹finite B›]) finally show ?thesis by (simp add: norm_eq_sqrt_inner) qed then show ?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) then have 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" then have 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) then have "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 also have "… = (∑v ∈ B. a v *🪙R f v)" by (simp add: f.sum f.scale) also have "… = (∑v ∈ B. a v *🪙R fb v)" by (simp add: ffb cong: sum.cong) finally have *: "f x = (∑v∈B. a v *🪙R fb v)" . then have "(norm (f x))🪙2 = (norm (∑v∈B. a v *🪙R fb v))🪙2" by simp also have "… = (∑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 also have "… = (norm x)🪙2" by (simp add: x pairwise_ortho_scaleR Borth norm_sum_Pythagorean [OF ‹finite B›]) finally show "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: *) also have "… = (∑v∈B. g (a v *🪙R fb v))" by (simp add: g.sum g.scale) also have "… = (∑v∈B. a v *🪙R g (fb v))" by (simp add: g.scale) also have "… = (∑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 also have "… = x" using x by blast finally show "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) also have "… = (∑v ∈ C. a v *🪙R g v)" by (simp add: g.scale) also have "… = (∑v ∈ C. a v *🪙R gb v)" by (simp add: ggb cong: sum.cong) finally have "f (g x) = f (∑v∈C. a v *🪙R gb v)" by simp also have "… = (∑v∈C. f (a v *🪙R gb v))" by (simp add: f.scale f.sum) also have "… = (∑v∈C. a v *🪙R f (gb v))" by (simp add: f.scale f.sum) also have "… = (∑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) also have "… = x" using x by blast finally show "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
corollary isomorphisms_UNIV_UNIV: assumes "DIM('M) = DIM('N)" obtains f::"'M::euclidean_space ==>'N::euclidean_space" and g where "linear f" "linear g" "∧x. norm(f x) = norm x" "∧y. norm(g y) = norm y" "∧x. g (f x) = x" "∧y. f(g y) = y" using assms by (auto intro: isometries_subspaces [of "UNIV::'M set" "UNIV::'N set"])
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]) then show ?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 then obtain a b where ab: "a ∈ S" "b ∈ T" by auto then have 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) also have "… homeomorphic ((+) (- b) ` T)" by (rule homeomorphic_subspaces [OF ss dd]) also have "… homeomorphic T" using homeomorphic_translation [of T "- b"] by (simp add: homeomorphic_sym [of T]) finally show ?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) moreover have "(k ∘ f) ` U ⊆ S" using imf imk by fastforce moreover have "P (k ∘ f)" by (simp add: P Qf contf imf) moreover have "continuous_on U (k ∘ g)" by (meson contg continuous_on_compose continuous_on_subset contk funcset_image img) moreover have "(k ∘ g) ` U ⊆ S" using img imk by fastforce moreover have "P (k ∘ g)" by (simp add: P Qg contg img) ultimately have "homotopic_with_canon P U S (k ∘ f) (k ∘ g)" by (simp add: hom image_subset_iff) then have "homotopic_with_canon Q U t (h ∘ (k ∘ f)) (h ∘ (k ∘ g))" apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono]) using Q conth imh by force+ then show ?thesis proof (rule homotopic_with_eq; simp) show "∧h k. (∧x. x ∈ U ==> h x = k x) ==> Q h = Q k" 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) moreover have "(k ∘ f) ∈ U → S" using imf imk by fastforce moreover have "P (k ∘ f)" by (simp add: P Qf contf imf) ultimately obtain c where "homotopic_with_canon P U S (k ∘ f) (λx. c)" by (metis hom) then have "homotopic_with_canon Q U t (h ∘ (k ∘ f)) (h ∘ (λx. c))" apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono]) using Q conth imh by force+ then have "homotopic_with_canon Q U t f (λx. h c)" proof (rule homotopic_with_eq) show "∧x. x ∈ topspace (top_of_set U) ==> f x = (h ∘ (k ∘ f)) x" 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 then show ?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 moreover have "(f ∘ h) ∈ S → U" using imf imh by fastforce moreover have "P (f ∘ h)" by (simp add: P Qf contf imf) moreover have "continuous_on S (g ∘ h)" using contg continuous_on_compose continuous_on_subset conth imh by blast moreover have "(g ∘ h) ∈ S → U" using img imh by fastforce moreover have "P (g ∘ h)" by (simp add: P Qg contg img) ultimately have "homotopic_with_canon P S U (f ∘ h) (g ∘ h)" by (simp add: hom) then have "homotopic_with_canon Q t U (f ∘ h ∘ k) (g ∘ h ∘ k)" apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono]) using Q contk imk by force+ then show ?thesis proof (rule homotopic_with_eq) show "f x = (f ∘ h ∘ k) x" "g x = (g ∘ h ∘ k) x" 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 moreover have "(f ∘ h) ∈ S → U" using imf imh by fastforce moreover have "P (f ∘ h)" by (simp add: P Qf contf imf) ultimately obtain c where "homotopic_with_canon P S U (f ∘ h) (λx. c)" by (metis hom) then have 🍋: "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)+ moreover have "homotopic_with_canon Q t U f (λx. c)" using homotopic_with_eq [OF 🍋] feq Qeq by fastforce ultimately show ?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]: assumes 1: "X homotopy_equivalent_space Y" and 2: "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" using 1 by (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" using 2 by (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 then have "homotopic_with (λf. True) X Y (g2 ∘ (f2 ∘ f1)) (id ∘ f1)" by (simp add: o_assoc) then have "homotopic_with (λx. True) X X
(g1 ∘ (g2 ∘ (f2 ∘ f1))) (g1 ∘ (id ∘ f1))" by (simp add: g1 homotopic_with_compose_continuous_map_left) moreover have "homotopic_with (λx. True) X X (g1 ∘ id ∘ f1) id" using hom1 by simp ultimately have 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 then have "homotopic_with (λf. True) U Y (f1 ∘ (g1 ∘ g2)) (id ∘ g2)" by (simp add: o_assoc) then have "homotopic_with (λx. True) U U
(f2 ∘ (f1 ∘ (g1 ∘ g2))) (f2 ∘ (id ∘ g2))" by (simp add: f2 homotopic_with_compose_continuous_map_left) moreover have "homotopic_with (λx. True) U U (f2 ∘ id ∘ g2) id" using hom2 by simp ultimately have 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 moreover have "(∃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 then show "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›) ultimately show ?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) is a little cryptic because we don't in fact assume that the constant "a" is in the space. This 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 then show ?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) then show ?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 then obtain 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 then show ?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 then have "homotopic_with (λx. True) Y Y id (λx. c)" using homotopic_with_trans [OF _ hom] homotopic_with_symD by blast then show ?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 then obtain a where a: "homotopic_with (λx. True) X X id (λx. a)" by (auto simp: contractible_space_def) then have "a ∈ topspace X" by (metis False continuous_map_const homotopic_with_imp_continuous_maps) then have "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 then have "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 then show ?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) then show ?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 then have "(prod_topology X Y) = trivial_topology" by simp then show ?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) then show "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) then show "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 have 1: "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 have 2: "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) then show ?thesis by (auto simp: contractible_space_def) qed show ?thesis using False 1 2 by (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 then have "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) then show ?rhs by (simp add: is_interval_path_connected_1) next assume ?rhs then have "convex S" by (simp add: is_interval_convex_1) show ?lhs proof (cases "S = {}") case False then obtain 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 then show ?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)+› ) then have "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) moreover have "homotopic_with_canon (λx. True) U T (h ∘ k ∘ f) (id ∘ f)" by (rule homotopic_with_compose_continuous_right [where X=T and Y=T]; simp add: hom f) moreover have "homotopic_with_canon (λx. True) U T (h ∘ k ∘ g) (id ∘ g)" by (rule homotopic_with_compose_continuous_right [where X=T and Y=T]; simp add: hom g) ultimately show "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 then show ?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 ultimately show ?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) then have "homotopic_with_canon (λx. True) T U ((f ∘ h) ∘ k) ((λx. c) ∘ k)" by (rule homotopic_with_compose_continuous_right [where X=S]) (use k in auto) moreover have "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›) ultimately show ?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) then have "homotopic_with_canon (λx. True) U T (h ∘ (k ∘ f)) (h ∘ (λx. c))" by (rule homotopic_with_compose_continuous_left [where Y=S]) (use h in auto) moreover have "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›) ultimately show ?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 then show ?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 then show ?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›\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) then have "a ∉ S" "b ∉ S" by auto then have "∀x. a ≤ x ∧ x ≤ b ⟶ x ∈ - S" by (meson Compl_iff conn connected_iff_interval) then show ?thesis using ‹S ⊆ box a b› by auto qed
lemma bounded_connected_Compl_1: fixes S :: "'a::{euclidean_space} set" assumes "bounded S" and conn: "connected(- S)" and 1: "DIM('a) = 1" shows "S = {}" proof - have "DIM('a) = DIM(real)" by (simp add: "1") then obtain f::"'a ==> real" and g where "linear f" "∧x. norm(f x) = norm x" and fg: "∧x. g(f x) = x" "∧y. f(g y) = y" by (rule isomorphisms_UNIV_UNIV) blast with ‹bounded S› have "bounded (f ` S)" using bounded_linear_image linear_linear by blast have "bij f" by (metis fg bijI') have "connected (f ` (-S))" using connected_linear_image assms ‹linear f› by blast moreover have "f ` (-S) = - (f ` S)" by (simp add: ‹bij f› bij_image_Compl_eq) finally have "connected (- (f ` S))" by simp then have "f ` S = {}" using ‹bounded (f ` S)› bounded_connected_Compl_real by blast then show ?thesis by blast qed
lemma connected_card_eq_iff_nontrivial: fixes S :: "'a::metric_space set" shows "connected S ==> uncountable S ⟷¬(∃a. S ⊆ {a})" by (metis connected_uncountable finite.emptyI finite.insertI rev_finite_subset singleton_iff subsetI uncountable_infinite)
lemma connected_finite_iff_sing: fixes S :: "'a::metric_space set" assumes "connected S" shows "finite S ⟷ S = {} ∨ (∃a. S = {a})" using assms connected_uncountable countable_finite by blast
subsection🍋‹tag unimportant›\ Some simple positive connection theorems›
proposition path_connected_convex_diff_countable: fixes U :: "'a::euclidean_space set" assumes "convex U" "¬ collinear U" "countable S" shows "path_connected(U - S)" proof (clarsimp simp: path_connected_def) fix a b assume "a ∈ U" "a ∉ S" "b ∈ U" "b ∉ S" let ?m = "midpoint a b" show "∃g. path g ∧ path_image g ⊆ U - S ∧ pathstart g = a ∧ pathfinish g = b" proof (cases "a = b") case True then show ?thesis by (metis DiffI ‹a ∈ U›‹a ∉ S› path_component_def path_component_refl) next case False then have "a ≠ ?m" "b ≠ ?m" using midpoint_eq_endpoint by fastforce+ have "?m ∈ U" using ‹a ∈ U›‹b ∈ U›‹convex U› convex_contains_segment by force obtain c where "c ∈ U" and nc_abc: "¬ collinear {a,b,c}" by (metis False ‹a ∈ U›‹b ∈ U›‹¬ collinear U› collinear_triples insert_absorb) have ncoll_mca: "¬ collinear {?m,c,a}" by (metis (full_types) ‹a ≠ ?m› collinear_3_trans collinear_midpoint insert_commute nc_abc) have ncoll_mcb: "¬ collinear {?m,c,b}" by (metis (full_types) ‹b ≠ ?m› collinear_3_trans collinear_midpoint insert_commute nc_abc) have "c ≠ ?m" by (metis collinear_midpoint insert_commute nc_abc) then have "closed_segment ?m c ⊆ U" by (simp add: ‹c ∈ U›‹?m ∈ U›‹convex U› closed_segment_subset) then obtain z where z: "z ∈ closed_segment ?m c" and disjS: "(closed_segment a z ∪ closed_segment z b) ∩ S = {}" proof - have False if "closed_segment ?m c ⊆ {z. (closed_segment a z ∪ closed_segment z b) ∩ S ≠ {}}" proof - have closb: "closed_segment ?m c ⊆
{z ∈ closed_segment ?m c. closed_segment a z ∩ S ≠ {}} ∪ {z ∈ closed_segment ?m c. closed_segment z b ∩ S ≠ {}}" using that by blast have *: "countable {z ∈ closed_segment ?m c. closed_segment z u ∩ S ≠ {}}" if "u ∈ U" "u ∉ S" and ncoll: "¬ collinear {?m, c, u}" for u proof - have **: False if x1: "x1 ∈ closed_segment ?m c" and x2: "x2 ∈ closed_segment ?m c" and "x1 ≠ x2" "x1 ≠ u" and w: "w ∈ closed_segment x1 u" "w ∈ closed_segment x2 u" and "w ∈ S" for x1 x2 w proof - have "x1 ∈ affine hull {?m,c}" "x2 ∈ affine hull {?m,c}" using segment_as_ball x1 x2 by auto then have coll_x1: "collinear {x1, ?m, c}" and coll_x2: "collinear {?m, c, x2}" by (simp_all add: affine_hull_3_imp_collinear) (metis affine_hull_3_imp_collinear insert_commute) have "¬ collinear {x1, u, x2}" proof assume "collinear {x1, u, x2}" then have "collinear {?m, c, u}" by (metis (full_types) ‹c ≠ ?m› coll_x1 coll_x2 collinear_3_trans insert_commute ncoll ‹x1 ≠ x2›) with ncoll show False .. qed then have "closed_segment x1 u ∩ closed_segment u x2 = {u}" by (blast intro!: Int_closed_segment) then have "w = u" using closed_segment_commute w by auto show ?thesis using ‹u ∉ S›‹w = u› that(7) by auto qed then have disj: "disjoint ((∪z∈closed_segment ?m c. {closed_segment z u ∩ S}))" by (fastforce simp: pairwise_def disjnt_def) have cou: "countable ((∪z ∈ closed_segment ?m c. {closed_segment z u ∩ S}) - {{}})" apply (rule pairwise_disjnt_countable_Union [OF _ pairwise_subset [OF disj]]) apply (rule countable_subset [OF _ ‹countable S›], auto) done define f where "f ≡ λX. (THE z. z ∈ closed_segment ?m c ∧ X = closed_segment z u ∩ S)" show ?thesis proof (rule countable_subset [OF _ countable_image [OF cou, where f=f]], clarify) fix x assume x: "x ∈ closed_segment ?m c" "closed_segment x u ∩ S ≠ {}" show "x ∈ f ` ((∪z∈closed_segment ?m c. {closed_segment z u ∩ S}) - {{}})" proof (rule_tac x="closed_segment x u ∩ S" in image_eqI) show "x = f (closed_segment x u ∩ S)" unfolding f_def by (rule the_equality [symmetric]) (use x in ‹auto dest: **›) qed (use x in auto) qed qed have "uncountable (closed_segment ?m c)" by (metis ‹c ≠ ?m› uncountable_closed_segment) then show False using closb * [OF ‹a ∈ U›‹a ∉ S› ncoll_mca] * [OF ‹b ∈ U›‹b ∉ S› ncoll_mcb] by (simp add: closed_segment_commute countable_subset) qed then show ?thesis by (force intro: that) qed show ?thesis proof (intro exI conjI) have "path_image (linepath a z +++ linepath z b) ⊆ U" by (metis ‹a ∈ U›‹b ∈ U›‹closed_segment ?m c ⊆ U› z ‹convex U› closed_segment_subset contra_subsetD path_image_linepath subset_path_image_join) with disjS show "path_image (linepath a z +++ linepath z b) ⊆ U - S" by (force simp: path_image_join) qed auto qed qed
lemma path_connected_punctured_convex: assumes "convex S" and aff: "aff_dim S ≠ 1" shows "path_connected(S - {a})" proof - consider "aff_dim S = -1" | "aff_dim S = 0" | "aff_dim S ≥ 2" using assms aff_dim_geq [of S] by linarith then show ?thesis proof cases assume "aff_dim S = -1" then show ?thesis by (metis aff_dim_empty empty_Diff path_connected_empty) next assume "aff_dim S = 0" then show ?thesis by (metis aff_dim_eq_0 Diff_cancel Diff_empty Diff_insert0 convex_empty convex_imp_path_connected path_connected_singleton singletonD) next assume ge2: "aff_dim S ≥ 2" then have "¬ collinear S" proof (clarsimp simp: collinear_affine_hull) fix u v assume "S ⊆ affine hull {u, v}" then have "aff_dim S ≤ aff_dim {u, v}" by (metis (no_types) aff_dim_affine_hull aff_dim_subset) with ge2 show False by (metis (no_types) aff_dim_2 antisym aff not_numeral_le_zero one_le_numeral order_trans) qed moreover have "countable {a}" by simp ultimately show ?thesis by (metis path_connected_convex_diff_countable [OF ‹convex S›]) qed qed
lemma connected_punctured_convex: shows "[convex S; aff_dim S ≠ 1]==> connected(S - {a})" using path_connected_imp_connected path_connected_punctured_convex by blast
lemma path_connected_complement_countable: fixes S :: "'a::euclidean_space set" assumes "2 ≤ DIM('a)" "countable S" shows "path_connected(- S)" proof - have "¬ collinear (UNIV::'a set)" using assms by (auto simp: collinear_aff_dim [of "UNIV :: 'a set"]) then have "path_connected(UNIV - S)" by (simp add: ‹countable S› path_connected_convex_diff_countable) then show ?thesis by (simp add: Compl_eq_Diff_UNIV) qed
proposition path_connected_openin_diff_countable: fixes S :: "'a::euclidean_space set" assumes "connected S" and ope: "openin (top_of_set (affine hull S)) S" and "¬ collinear S" "countable T" shows "path_connected(S - T)" proof (clarsimp simp: path_connected_component) fix x y assume xy: "x ∈ S" "x ∉ T" "y ∈ S" "y ∉ T" show "path_component (S - T) x y" proof (rule connected_equivalence_relation_gen [OF ‹connected S›, where P = "λx. x ∉ T"]) show "∃z. z ∈ U ∧ z ∉ T" if opeU: "openin (top_of_set S) U" and "x ∈ U" for U x proof - have "openin (top_of_set (affine hull S)) U" using opeU ope openin_trans by blast with ‹x ∈ U› obtain r where Usub: "U ⊆ affine hull S" and "r > 0" and subU: "ball x r ∩ affine hull S ⊆ U" by (auto simp: openin_contains_ball) with ‹x ∈ U› have x: "x ∈ ball x r ∩ affine hull S" by auto have "¬ S ⊆ {x}" using ‹¬ collinear S› collinear_subset by blast then obtain x' where "x' ≠ x" "x' ∈ S" by blast obtain y where y: "y ≠ x" "y ∈ ball x r ∩ affine hull S" proof show "x + (r / 2 / norm(x' - x)) *🪙R (x' - x) ≠ x" using ‹x' ≠ x›‹r > 0› by auto show "x + (r / 2 / norm (x' - x)) *🪙R (x' - x) ∈ ball x r ∩ affine hull S" using ‹x' ≠ x›‹r > 0›‹x' ∈ S› x by (simp add: dist_norm mem_affine_3_minus hull_inc) qed have "convex (ball x r ∩ affine hull S)" by (simp add: affine_imp_convex convex_Int) with x y subU have "uncountable U" by (meson countable_subset uncountable_convex) then have "¬ U ⊆ T" using ‹countable T› countable_subset by blast then show ?thesis by blast qed show "∃U. openin (top_of_set S) U ∧ x ∈ U ∧
(∀x∈U. ∀y∈U. x ∉ T ∧ y ∉ T ⟶ path_component (S - T) x y)" if "x ∈ S" for x proof - obtain r where Ssub: "S ⊆ affine hull S" and "r > 0" and subS: "ball x r ∩ affine hull S ⊆ S" using ope ‹x ∈ S› by (auto simp: openin_contains_ball) then have conv: "convex (ball x r ∩ affine hull S)" by (simp add: affine_imp_convex convex_Int) have "¬ aff_dim (affine hull S) ≤ 1" using ‹¬ collinear S› collinear_aff_dim by auto then have "¬ aff_dim (ball x r ∩ affine hull S) ≤ 1" by (metis (no_types, opaque_lifting) aff_dim_convex_Int_open IntI open_ball ‹0 < r› aff_dim_affine_hull affine_affine_hull affine_imp_convex centre_in_ball empty_iff hull_subset inf_commute subsetCE that) then have "¬ collinear (ball x r ∩ affine hull S)" by (simp add: collinear_aff_dim) then have *: "path_connected ((ball x r ∩ affine hull S) - T)" by (rule path_connected_convex_diff_countable [OF conv _ ‹countable T›]) have ST: "ball x r ∩ affine hull S - T ⊆ S - T" using subS by auto show ?thesis proof (intro exI conjI) show "x ∈ ball x r ∩ affine hull S" using ‹x ∈ S›‹r > 0› by (simp add: hull_inc) have "openin (top_of_set (affine hull S)) (ball x r ∩ affine hull S)" by (subst inf.commute) (simp add: openin_Int_open) then show "openin (top_of_set S) (ball x r ∩ affine hull S)" by (rule openin_subset_trans [OF _ subS Ssub]) qed (use * path_component_trans in ‹auto simp: path_connected_component path_component_of_subset [OF ST]›) qed qed (use xy path_component_trans in auto) qed
corollary connected_openin_diff_countable: fixes S :: "'a::euclidean_space set" assumes "connected S" and ope: "openin (top_of_set (affine hull S)) S" and "¬ collinear S" "countable T" shows "connected(S - T)" by (metis path_connected_imp_connected path_connected_openin_diff_countable [OF assms])
corollary path_connected_open_diff_countable: fixes S :: "'a::euclidean_space set" assumes "2 ≤ DIM('a)" "open S" "connected S" "countable T" shows "path_connected(S - T)" proof (cases "S = {}") case True then show ?thesis by (simp) next case False show ?thesis proof (rule path_connected_openin_diff_countable) show "openin (top_of_set (affine hull S)) S" by (simp add: assms hull_subset open_subset) show "¬ collinear S" using assms False by (simp add: collinear_aff_dim aff_dim_open) qed (simp_all add: assms) qed
lemma homeomorphism_moving_point_1: fixes a :: "'a::euclidean_space" assumes "affine T" "a ∈ T" and u: "u ∈ ball a r ∩ T" obtains f g where "homeomorphism (cball a r ∩ T) (cball a r ∩ T) f g" "f a = u" "∧x. x ∈ sphere a r ==> f x = x" proof - have nou: "norm (u - a) < r" and "u ∈ T" using u by (auto simp: dist_norm norm_minus_commute) then have "0 < r" by (metis DiffD1 Diff_Diff_Int ball_eq_empty centre_in_ball not_le u) define f where "f ≡ λx. (1 - norm(x - a) / r) *🪙R (u - a) + x" have *: "False" if eq: "x + (norm y / r) *🪙R u = y + (norm x / r) *🪙R u" and nou: "norm u < r" and yx: "norm y < norm x" for x y and u::'a proof - have "x = y + (norm x / r - (norm y / r)) *🪙R u" using eq by (simp add: algebra_simps) then have "norm x = norm (y + ((norm x - norm y) / r) *🪙R u)" by (metis diff_divide_distrib) also have "…≤ norm y + norm(((norm x - norm y) / r) *🪙R u)" using norm_triangle_ineq by blast also have "… = norm y + (norm x - norm y) * (norm u / r)" using yx ‹r > 0› by (simp add: field_split_simps) also have "… < norm y + (norm x - norm y) * 1" proof (subst add_less_cancel_left) show "(norm x - norm y) * (norm u / r) < (norm x - norm y) * 1" proof (rule mult_strict_left_mono) show "norm u / r < 1" using ‹0 < r› divide_less_eq_1_pos nou by blast qed (simp add: yx) qed also have "… = norm x" by simp finally show False by simp qed have "inj f" unfolding f_def proof (clarsimp simp: inj_on_def) fix x y assume "(1 - norm (x - a) / r) *🪙R (u - a) + x =
(1 - norm (y - a) / r) *🪙R (u - a) + y" then have eq: "(x - a) + (norm (y - a) / r) *🪙R (u - a) = (y - a) + (norm (x - a) / r) *🪙R (u - a)" by (auto simp: algebra_simps) show "x=y" proof (cases "norm (x - a) = norm (y - a)") case True then show ?thesis using eq by auto next case False then consider "norm (x - a) < norm (y - a)" | "norm (x - a) > norm (y - a)" by linarith then have "False" proof cases case 1 show False using * [OF _ nou 1] eq by simp next case 2 with * [OF eq nou] show False by auto qed then show "x=y" .. qed qed then have inj_onf: "inj_on f (cball a r ∩ T)" using inj_on_Int by fastforce have contf: "continuous_on (cball a r ∩ T) f" unfolding f_def using ‹0 < r› by (intro continuous_intros) blast have fim: "f ` (cball a r ∩ T) = cball a r ∩ T" proof have *: "norm (y + (1 - norm y / r) *🪙R u) ≤ r" if "norm y ≤ r" "norm u < r" for y u::'a proof - have "norm (y + (1 - norm y / r) *🪙R u) ≤ norm y + norm((1 - norm y / r) *🪙R u)" using norm_triangle_ineq by blast also have "… = norm y + abs(1 - norm y / r) * norm u" by simp also have "…≤ r" proof - have "(r - norm u) * (r - norm y) ≥ 0" using that by auto then have "r * norm u + r * norm y ≤ r * r + norm u * norm y" by (simp add: algebra_simps) then show ?thesis using that ‹0 < r› by (simp add: abs_if field_simps) qed finally show ?thesis . qed have "f ` (cball a r) ⊆ cball a r" using * nou apply (clarsimp simp: dist_norm norm_minus_commute f_def) by (metis diff_add_eq diff_diff_add diff_diff_eq2 norm_minus_commute) moreover have "f ` T ⊆ T" unfolding f_def using ‹affine T›‹a ∈ T›‹u ∈ T› by (force simp: add.commute mem_affine_3_minus) ultimately show "f ` (cball a r ∩ T) ⊆ cball a r ∩ T" by blast next show "cball a r ∩ T ⊆ f ` (cball a r ∩ T)" proof (clarsimp simp: dist_norm norm_minus_commute) fix x assume x: "norm (x - a) ≤ r" and "x ∈ T" have "∃v ∈ {0..1}. ((1 - v) * r - norm ((x - a) - v *🪙R (u - a))) ∙ 1 = 0" by (rule ivt_decreasing_component_on_1) (auto simp: x continuous_intros) then obtain v where "0 ≤ v" "v ≤ 1" and v: "(1 - v) * r = norm ((x - a) - v *🪙R (u - a))" by auto then have n: "norm (a - (x - v *🪙R (u - a))) = r - r * v" by (simp add: field_simps norm_minus_commute) show "x ∈ f ` (cball a r ∩ T)" proof (rule image_eqI) show "x = f (x - v *🪙R (u - a))" using ‹r > 0› v by (simp add: f_def) (simp add: field_simps) have "x - v *🪙R (u - a) ∈ cball a r" using ‹r > 0›\0 ≤ v› by (simp add: dist_norm n) moreover have "x - v *🪙R (u - a) ∈ T" by (simp add: f_def ‹u ∈ T›‹x ∈ T› assms mem_affine_3_minus2) ultimately show "x - v *🪙R (u - a) ∈ cball a r ∩ T" by blast qed qed qed have "compact (cball a r ∩ T)" by (simp add: affine_closed compact_Int_closed ‹affine T›) then obtain g where "homeomorphism (cball a r ∩ T) (cball a r ∩ T) f g" by (metis homeomorphism_compact [OF _ contf fim inj_onf]) then show thesis apply (rule_tac f=f in that) using ‹r > 0› by (simp_all add: f_def dist_norm norm_minus_commute) qed
corollary🍋‹tag unimportant› homeomorphism_moving_point_2: fixes a :: "'a::euclidean_space" assumes "affine T" "a ∈ T" and u: "u ∈ ball a r ∩ T" and v: "v ∈ ball a r ∩ T" obtains f g where "homeomorphism (cball a r ∩ T) (cball a r ∩ T) f g" "f u = v" "∧x. [x ∈ sphere a r; x ∈ T]==> f x = x" proof - have "0 < r" by (metis DiffD1 Diff_Diff_Int ball_eq_empty centre_in_ball not_le u) obtain f1 g1 where hom1: "homeomorphism (cball a r ∩ T) (cball a r ∩ T) f1 g1" and "f1 a = u" and f1: "∧x. x ∈ sphere a r ==> f1 x = x" using homeomorphism_moving_point_1 [OF ‹affine T›‹a ∈ T› u] by blast obtain f2 g2 where hom2: "homeomorphism (cball a r ∩ T) (cball a r ∩ T) f2 g2" and "f2 a = v" and f2: "∧x. x ∈ sphere a r ==> f2 x = x" using homeomorphism_moving_point_1 [OF ‹affine T›‹a ∈ T› v] by blast show ?thesis proof show "homeomorphism (cball a r ∩ T) (cball a r ∩ T) (f2 ∘ g1) (f1 ∘ g2)" by (metis homeomorphism_compose homeomorphism_symD hom1 hom2) have "g1 u = a" using ‹0 < r›‹f1 a = u› assms hom1 homeomorphism_apply1 by fastforce then show "(f2 ∘ g1) u = v" by (simp add: ‹f2 a = v›) show "∧x. [x ∈ sphere a r; x ∈ T]==> (f2 ∘ g1) x = x" using f1 f2 hom1 homeomorphism_apply1 by fastforce qed qed
corollary🍋‹tag unimportant› homeomorphism_moving_point_3: fixes a :: "'a::euclidean_space" assumes "affine T" "a ∈ T" and ST: "ball a r ∩ T ⊆ S" "S ⊆ T" and u: "u ∈ ball a r ∩ T" and v: "v ∈ ball a r ∩ T" obtains f g where "homeomorphism S S f g" "f u = v" "{x. ¬ (f x = x ∧ g x = x)} ⊆ ball a r ∩ T" proof - obtain f g where hom: "homeomorphism (cball a r ∩ T) (cball a r ∩ T) f g" and "f u = v" and fid: "∧x. [x ∈ sphere a r; x ∈ T]==> f x = x" using homeomorphism_moving_point_2 [OF ‹affine T›‹a ∈ T› u v] by blast have gid: "∧x. [x ∈ sphere a r; x ∈ T]==> g x = x" using fid hom homeomorphism_apply1 by fastforce define ff where "ff ≡ λx. if x ∈ ball a r ∩ T then f x else x" define gg where "gg ≡ λx. if x ∈ ball a r ∩ T then g x else x" show ?thesis proof show "homeomorphism S S ff gg" proof (rule homeomorphismI) have "continuous_on ((cball a r ∩ T) ∪ (T - ball a r)) ff" unfolding ff_def using homeomorphism_cont1 [OF hom] by (intro continuous_on_cases) (auto simp: affine_closed ‹affine T› fid) then show "continuous_on S ff" by (rule continuous_on_subset) (use ST in auto) have "continuous_on ((cball a r ∩ T) ∪ (T - ball a r)) gg" unfolding gg_def using homeomorphism_cont2 [OF hom] by (intro continuous_on_cases) (auto simp: affine_closed ‹affine T› gid) then show "continuous_on S gg" by (rule continuous_on_subset) (use ST in auto) show "ff ` S ⊆ S" proof (clarsimp simp: ff_def) fix x assume "x ∈ S" and x: "dist a x < r" and "x ∈ T" then have "f x ∈ cball a r ∩ T" using homeomorphism_image1 [OF hom] by force then show "f x ∈ S" using ST(1) ‹x ∈ T› gid hom homeomorphism_def x by fastforce qed show "gg ` S ⊆ S" proof (clarsimp simp: gg_def) fix x assume "x ∈ S" and x: "dist a x < r" and "x ∈ T" then have "g x ∈ cball a r ∩ T" using homeomorphism_image2 [OF hom] by force then have "g x ∈ ball a r" using homeomorphism_apply2 [OF hom] by (metis Diff_Diff_Int Diff_iff ‹x ∈ T› cball_def fid le_less mem_Collect_eq mem_ball mem_sphere x) then show "g x ∈ S" using ST(1) ‹g x ∈ cball a r ∩ T› by force qed show "∧x. x ∈ S ==> gg (ff x) = x" unfolding ff_def gg_def using homeomorphism_apply1 [OF hom] homeomorphism_image1 [OF hom] by simp (metis Int_iff homeomorphism_apply1 [OF hom] fid image_eqI less_eq_real_def mem_cball mem_sphere) show "∧x. x ∈ S ==> ff (gg x) = x" unfolding ff_def gg_def using homeomorphism_apply2 [OF hom] homeomorphism_image2 [OF hom] by simp (metis Int_iff fid image_eqI less_eq_real_def mem_cball mem_sphere) qed show "ff u = v" using u by (auto simp: ff_def ‹f u = v›) show "{x. ¬ (ff x = x ∧ gg x = x)} ⊆ ball a r ∩ T" by (auto simp: ff_def gg_def) qed qed
proposition🍋‹tag unimportant› homeomorphism_moving_point: fixes a :: "'a::euclidean_space" assumes ope: "openin (top_of_set (affine hull S)) S" and "S ⊆ T" and TS: "T ⊆ affine hull S" and S: "connected S" "a ∈ S" "b ∈ S" obtains f g where "homeomorphism T T f g" "f a = b" "{x. ¬ (f x = x ∧ g x = x)} ⊆ S" "bounded {x. ¬ (f x = x ∧ g x = x)}" proof - have 1: "∃h k. homeomorphism T T h k ∧ h (f d) = d ∧
{x. ¬ (h x = x ∧ k x = x)} ⊆ S ∧ bounded {x. ¬ (h x = x ∧ k x = x)}" if "d ∈ S" "f d ∈ S" and homfg: "homeomorphism T T f g" and S: "{x. ¬ (f x = x ∧ g x = x)} ⊆ S" and bo: "bounded {x. ¬ (f x = x ∧ g x = x)}" for d f g proof (intro exI conjI) show homgf: "homeomorphism T T g f" by (metis homeomorphism_symD homfg) then show "g (f d) = d" by (meson ‹S ⊆ T› homeomorphism_def subsetD ‹d ∈ S›) show "{x. ¬ (g x = x ∧ f x = x)} ⊆ S" using S by blast show "bounded {x. ¬ (g x = x ∧ f x = x)}" using bo by (simp add: conj_commute) qed have 2: "∃f g. homeomorphism T T f g ∧ f x = f2 (f1 x) ∧
{x. ¬ (f x = x ∧ g x = x)} ⊆ S ∧ bounded {x. ¬ (f x = x ∧ g x = x)}" if "x ∈ S" "f1 x ∈ S" "f2 (f1 x) ∈ S" and hom: "homeomorphism T T f1 g1" "homeomorphism T T f2 g2" and sub: "{x. ¬ (f1 x = x ∧ g1 x = x)} ⊆ S" "{x. ¬ (f2 x = x ∧ g2 x = x)} ⊆ S" and bo: "bounded {x. ¬ (f1 x = x ∧ g1 x = x)}" "bounded {x. ¬ (f2 x = x ∧ g2 x = x)}" for x f1 f2 g1 g2 proof (intro exI conjI) show homgf: "homeomorphism T T (f2 ∘ f1) (g1 ∘ g2)" by (metis homeomorphism_compose hom) then show "(f2 ∘ f1) x = f2 (f1 x)" by force show "{x. ¬ ((f2 ∘ f1) x = x ∧ (g1 ∘ g2) x = x)} ⊆ S" using sub by force have "bounded ({x. ¬(f1 x = x ∧ g1 x = x)} ∪ {x. ¬(f2 x = x ∧ g2 x = x)})" using bo by simp then show "bounded {x. ¬ ((f2 ∘ f1) x = x ∧ (g1 ∘ g2) x = x)}" by (rule bounded_subset) auto qed have 3: "∃U. openin (top_of_set S) U ∧
d ∈ U ∧
(∀x∈U. ∃f g. homeomorphism T T f g ∧ f d = x ∧
{x. ¬ (f x = x ∧ g x = x)} ⊆ S ∧
bounded {x. ¬ (f x = x ∧ g x = x)})" if "d ∈ S" for d proof - obtain r where "r > 0" and r: "ball d r ∩ affine hull S ⊆ S" by (metis ‹d ∈ S› ope openin_contains_ball) have *: "∃f g. homeomorphism T T f g ∧ f d = e ∧
{x. ¬ (f x = x ∧ g x = x)} ⊆ S ∧
bounded {x. ¬ (f x = x ∧ g x = x)}" if "e ∈ S" "e ∈ ball d r" for e apply (rule homeomorphism_moving_point_3 [of "affine hull S" d r T d e]) using r ‹S ⊆ T› TS that apply (auto simp: ‹d ∈ S›‹0 < r› hull_inc) using bounded_subset by blast show ?thesis by (rule_tac x="S ∩ ball d r" in exI) (fastforce simp: openin_open_Int ‹0 < r› 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: 1 2 3) then show ?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 then show ?case by (force simp: homeomorphism_ident) next case (insert i K) then have 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) then have "∃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) then show ?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) then show "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 then show "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" assumes 2: "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 then show ?thesis using KS homeomorphism_ident that by fastforce next case False then have affS: "affine hull S = UNIV" by (simp add: affine_hull_open ‹open S›) then have ope: "openin (top_of_set (affine hull S)) S" using ‹open S› open_openin by auto have "2 ≤ DIM('a)" by (rule 2) also have "… = aff_dim (UNIV :: 'a set)" by simp also have "…≤ aff_dim S" by (metis aff_dim_UNIV aff_dim_affine_hull aff_dim_le_DIM affS) finally have "2 ≤ aff_dim S" by linarith then show ?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) then show "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 then obtain g where "homeomorphism (cbox a b) (cbox c d) f g" .. then show ?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 then have 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+ then show "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) moreover have "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) moreover have "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) ultimately show ?thesis using le eq by simp qed have "inj_on f1 (cbox a b)" by (metis (full_types) hom_ab homeomorphism_def inj_onI) moreover have "inj_on f2 (cbox b c)" by (metis (full_types) hom_bc homeomorphism_def inj_onI) ultimately show "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 then obtain g where "homeomorphism (cbox a c) (cbox u w) f g" .. then show ?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 where 1: "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 where 2: "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 where 3: "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 where 4: "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 1 2] 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 4 3] 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 then obtain e where "e > 0" "cball u e ⊆ U" using ‹open U› open_contains_cball by blast then show ?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 then show ?thesis using ‹box c d ≠ {}›‹cbox c d ⊆ U›‹U ⊆ S› that by blast next case False then obtain 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 moreover have "c ∈ S" "d ∈ S" using ‹box c d ≠ {}›‹cbox c d ⊆ U›‹U ⊆ S› by force+ ultimately have "min a c ∈ S" "max b d ∈ S" by linarith+ then obtain 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 then have *: "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 moreover have "∧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)+ then show "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 then obtain P where "P ⊆ U" "finite P" "card K = card P" using infinite_arbitrarily_large by metis then obtain γ 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) then show ?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) then obtain 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+) ultimately show "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 then obtain P where "P ⊆ U" "finite P" "card K = card P" using infinite_arbitrarily_large by metis then obtain γ 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 then show ?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 then show ?thesis proof cases assume "aff_dim S = -1" then have "S = {}" using aff_dim_empty by blast then have "False" using ‹U ≠ {}›‹K ⊆ S› openin_imp_subset [OF opeU] by blast then show ?thesis .. next assume "aff_dim S = 0" then obtain a where "S = {a}" using aff_dim_eq_0 by blast then have "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" then have "affine hull S homeomorphic (UNIV :: real set)" by (auto simp: homeomorphic_affine_sets) then obtain h::"'a==>real" and j where homhj: "homeomorphism (affine hull S) UNIV h j" using homeomorphic_def by blast then have 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) then 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_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 then show "continuous_on T f'" apply (rule continuous_on_eq) using ‹T ⊆ affine hull S› f'_def by auto have "continuous_on T (j ∘ g ∘ h)" using hom homeomorphism_def by (intro continuous_on_compose cont_hj) blast then show "continuous_on T g'" apply (rule continuous_on_eq) using ‹T ⊆ affine hull S› g'_def by auto show "f' ` T ⊆ T" proof (clarsimp simp: f'_def) fix x assume "x ∈ T" then have "f (h x) ∈ h ` T" by (metis (no_types) hom homeomorphism_def image_subset_iff subset_refl) then show "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" then have "g (h x) ∈ h ` T" by (metis (no_types) hom homeomorphism_def image_subset_iff subset_refl) then show "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) then have "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) ultimately have "bounded {x ∈ affine hull S. j (f (h x)) ≠ x ∨ j (g (h x)) ≠ x}" by metis then show "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 then have "j (f (h x)) ∈ U" using f h hull_subset that by fastforce then show "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. This even works out in the degenerate cases when the radius is ‹≤› 0 we also don't need to explicitly assume continuity since it's already implicit in 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 then show ?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 then show "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 then show ?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) then have "continuous_on (cball a r) (λx. h (0, a))" "(λx. h (0, a)) ` cball a r ⊆ S" by (auto simp: equal) then show ?rhs using h(3) local.equal by force next assume ?rhs then show ?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)" then have contf: "continuous_on (sphere a r) f" by (metis homotopic_with_imp_continuous) moreover have 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 moreover have ?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)" then have "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 moreover have ?thesis if ?P proof assume ?lhs then obtain c where "homotopic_with_canon (λx. True) (sphere a r) S (λx. c) f" using homotopic_with_sym by blast then obtain 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 then have "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) then show "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) also have "… < e" using greater ‹0 < d›‹b1 ∈ Basis› that by (intro d) (simp_all add: dist_norm, simp add: field_simps) finally show ?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 then obtain 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) ultimately have "homotopic_with_canon (λx. True) (sphere a r) S (λx. g a) f" by (auto simp: homotopic_with) then show ?lhs using homotopic_with_symD by blast qed ultimately show ?thesis by meson qed
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.558 Sekunden
(vorverarbeitet am 2026-05-03)
¤
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.