section‹Extending Continous Maps, Invariance of Domain, etc›(*FIX rename? *)
text‹Ported from HOL Light (moretop.ml) by L C Paulson›
theory Further_Topology imports Weierstrass_Theorems Polytope Complex_Transcendental Equivalence_Lebesgue_Henstock_Integration Retracts begin
subsection‹A map from a sphere to a higher dimensional sphere is nullhomotopic›
lemma spheremap_lemma1: fixes f :: "'a::euclidean_space ==> 'a::euclidean_space" assumes"subspace S""subspace T"and dimST: "dim S < dim T" and"S ⊆ T" and diff_f: "f differentiable_on sphere 0 1 ∩ S" shows"f ` (sphere 0 1 ∩ S) ≠ sphere 0 1 ∩ T" proof assume fim: "f ` (sphere 0 1 ∩ S) = sphere 0 1 ∩ T" have inS: "∧x. [x ∈ S; x ≠ 0]==> (x /🪙R norm x) ∈ S" using subspace_mul ‹subspace S›by blast have subS01: "(λx. x /🪙R norm x) ` (S - {0}) ⊆ sphere 0 1 ∩ S" using‹subspace S› subspace_mul by fastforce thenhave diff_f': "f differentiable_on (λx. x /🪙R norm x) ` (S - {0})" by (rule differentiable_on_subset [OF diff_f])
define g where"g ≡ λx. norm x *🪙R f(inverse(norm x) *🪙R x)" have gdiff: "g differentiable_on S - {0}" unfolding g_def by (rule diff_f' derivative_intros differentiable_on_compose [where f=f] | force)+ have geq: "g ` (S - {0}) = T - {0}" proof have"∧u. [u ∈ S; norm u *🪙R f (u /🪙R norm u) ∉ T]==> u = 0" by (metis (mono_tags, lifting) DiffI subS01 subspace_mul [OF ‹subspace T›] fim image_subset_iff inf_le2 singletonD) thenhave"g ∈ (S - {0}) → T" using g_def by blast moreoverhave"g ∈ (S - {0}) → UNIV - {0}" proof (clarsimp simp: g_def) fix y assume"y ∈ S"and f0: "f (y /🪙R norm y) = 0" thenhave"y ≠ 0 ==> y /🪙R norm y ∈ sphere 0 1 ∩ S" by (auto simp: subspace_mul [OF ‹subspace S›]) thenshow"y = 0" by (metis fim f0 Int_iff image_iff mem_sphere_0 norm_eq_zero zero_neq_one) qed ultimatelyshow"g ` (S - {0}) ⊆ T - {0}" by auto next have *: "sphere 0 1 ∩ T ⊆ f ` (sphere 0 1 ∩ S)" using fim by (simp add: image_subset_iff) have"x ∈ (λx. norm x *🪙R f (x /🪙R norm x)) ` (S - {0})" if"x ∈ T""x ≠ 0"for x proof - have"x /🪙R norm x ∈ T" using‹subspace T› subspace_mul that by blast thenobtain u where u: "f u ∈ T""x /🪙R norm x = f u""norm u = 1""u ∈ S" using * [THEN subsetD, of "x /🪙R norm x"] ‹x ≠ 0›by auto with that have [simp]: "norm x *🪙R f u = x" by (metis divideR_right norm_eq_zero) moreoverhave"norm x *🪙R u ∈ S - {0}" using‹subspace S› subspace_scale that(2) u by auto with u show ?thesis by (simp add: image_eqI [where x="norm x *🪙R u"]) qed thenhave"T - {0} ⊆ (λx. norm x *🪙R f (x /🪙R norm x)) ` (S - {0})" by force thenshow"T - {0} ⊆ g ` (S - {0})" by (simp add: g_def) qed
define T' where"T' ≡ {y. ∀x ∈ T. orthogonal x y}" have"subspace T'" by (simp add: subspace_orthogonal_to_vectors T'_def) have dim_eq: "dim T' + dim T = DIM('a)" using dim_subspace_orthogonal_to_vectors [of T UNIV] ‹subspace T› by (simp add: T'_def) have"∃v1 v2. v1 ∈ span T ∧ (∀w ∈ span T. orthogonal v2 w) ∧ x = v1 + v2"for x by (force intro: orthogonal_subspace_decomp_exists [of T x]) thenobtain p1 p2 where p1span: "p1 x ∈ span T" and"∧w. w ∈ span T ==> orthogonal (p2 x) w" and eq: "p1 x + p2 x = x"for x by metis thenhave p1: "∧z. p1 z ∈ T"and ortho: "∧w. w ∈ T ==> orthogonal (p2 x) w"for x using span_eq_iff ‹subspace T›by blast+ thenhave p2: "∧z. p2 z ∈ T'" by (simp add: T'_def orthogonal_commute) have p12_eq: "∧x y. [x ∈ T; y ∈ T']==> p1(x + y) = x ∧ p2(x + y) = y" proof (rule orthogonal_subspace_decomp_unique [OF eq p1span, where T=T']) show"∧x y. [x ∈ T; y ∈ T']==> p2 (x + y) ∈ span T'" using span_eq_iff p2 ‹subspace T'›by blast show"∧a b. [a ∈ T; b ∈ T']==> orthogonal a b" using T'_defby blast qed (auto simp: span_base) thenhave"∧c x. p1 (c *🪙R x) = c *🪙R p1 x ∧ p2 (c *🪙R x) = c *🪙R p2 x" proof - fix c :: real and x :: 'a have f1: "c *🪙R x = c *🪙R p1 x + c *🪙R p2 x" by (metis eq pth_6) have f2: "c *🪙R p2 x ∈ T'" by (simp add: ‹subspace T'› p2 subspace_scale) have"c *🪙R p1 x ∈ T" by (metis (full_types) assms(2) p1span span_eq_iff subspace_scale) thenshow"p1 (c *🪙R x) = c *🪙R p1 x ∧ p2 (c *🪙R x) = c *🪙R p2 x" using f2 f1 p12_eq by presburger qed moreoverhave lin_add: "∧x y. p1 (x + y) = p1 x + p1 y ∧ p2 (x + y) = p2 x + p2 y" proof (rule orthogonal_subspace_decomp_unique [OF _ p1span, where T=T']) show"∧x y. p1 (x + y) + p2 (x + y) = p1 x + p1 y + (p2 x + p2 y)" by (simp add: add.assoc add.left_commute eq) show"∧a b. [a ∈ T; b ∈ T']==> orthogonal a b" using T'_defby blast qed (auto simp: p1span p2 span_base span_add) ultimatelyhave"linear p1""linear p2" by unfold_locales auto have"g differentiable_on p1 ` {x + y |x y. x ∈ S - {0} ∧ y ∈ T'}" using p12_eq ‹S ⊆ T›by (force intro: differentiable_on_subset [OF gdiff]) thenhave"(λz. g (p1 z)) differentiable_on {x + y |x y. x ∈ S - {0} ∧ y ∈ T'}" by (rule differentiable_on_compose [OF linear_imp_differentiable_on [OF ‹linear p1›]]) thenhave diff: "(λx. g (p1 x) + p2 x) differentiable_on {x + y |x y. x ∈ S - {0} ∧y ∈ T'}" by (intro derivative_intros linear_imp_differentiable_on [OF ‹linear p2›]) have"dim {x + y |x y. x ∈ S - {0} ∧ y ∈ T'} ≤ dim {x + y |x y. x ∈ S ∧ y ∈ T'}" by (blast intro: dim_subset) alsohave"... = dim S + dim T' - dim (S ∩ T')" using dim_sums_Int [OF ‹subspace S›‹subspace T'›] by (simp add: algebra_simps) alsohave"... < DIM('a)" using dimST dim_eq by auto finallyhave neg: "negligible {x + y |x y. x ∈ S - {0} ∧ y ∈ T'}" by (rule negligible_lowdim) have"negligible ((λx. g (p1 x) + p2 x) ` {x + y |x y. x ∈ S - {0} ∧ y ∈ T'})" by (rule negligible_differentiable_image_negligible [OF order_refl neg diff]) thenhave"negligible {x + y |x y. x ∈ g ` (S - {0}) ∧ y ∈ T'}" proof (rule negligible_subset) have"[t' ∈ T'; s ∈ S; s ≠ 0] ==> g s + t' ∈ (λx. g (p1 x) + p2 x) ` {x + t' |x t'. x ∈ S ∧ x ≠ 0 ∧ t' ∈ T'}"for t' s using‹S ⊆ T› p12_eq by (rule_tac x="s + t'"in image_eqI) auto thenshow"{x + y |x y. x ∈ g ` (S - {0}) ∧ y ∈ T'} ⊆ (λx. g (p1 x) + p2 x) ` {x + y |x y. x ∈ S - {0} ∧ y ∈ T'}" by auto qed moreoverhave"- T' ⊆ {x + y |x y. x ∈ g ` (S - {0}) ∧ y ∈ T'}" proof clarsimp fix z assume"z ∉ T'" show"∃x y. z = x + y ∧ x ∈ g ` (S - {0}) ∧ y ∈ T'" by (metis Diff_iff ‹z ∉ T'› add.left_neutral eq geq p1 p2 singletonD) qed ultimatelyhave"negligible (-T')" using negligible_subset by blast moreoverhave"negligible T'" using negligible_lowdim by (metis add.commute assms(3) diff_add_inverse2 diff_self_eq_0 dim_eq le_add1 le_antisym linordered_semidom_class.add_diff_inverse not_less0) ultimatelyhave"negligible (-T' ∪ T')" by (metis negligible_Un_eq) thenshow False using negligible_Un_eq non_negligible_UNIV by simp qed
lemma spheremap_lemma2: fixes f :: "'a::euclidean_space ==> 'a::euclidean_space" assumes ST: "subspace S""subspace T""dim S < dim T" and"S ⊆ T" and contf: "continuous_on (sphere 0 1 ∩ S) f" and fim: "f ∈ (sphere 0 1 ∩ S) → sphere 0 1 ∩ T" shows"∃c. homotopic_with_canon (λx. True) (sphere 0 1 ∩ S) (sphere 0 1 ∩ T) f (λx. c)" proof - have [simp]: "∧x. [norm x = 1; x ∈ S]==> norm (f x) = 1" using fim by auto have"compact (sphere 0 1 ∩ S)" by (simp add: ‹subspace S› closed_subspace compact_Int_closed) thenobtain g where pfg: "polynomial_function g"and gim: "g ∈ (sphere 0 1 ∩ S) → T" and g12: "∧x. x ∈ sphere 0 1 ∩ S ==> norm(f x - g x) < 1/2" using Stone_Weierstrass_polynomial_function_subspace [OF _ contf _ ‹subspace T›, of "1/2"] fim by (auto simp: image_subset_iff_funcset) have gnz: "g x ≠ 0"if"x ∈ sphere 0 1 ∩ S"for x using g12 that by fastforce have diffg: "g differentiable_on sphere 0 1 ∩ S" by (metis pfg differentiable_on_polynomial_function)
define h where"h ≡ λx. inverse(norm(g x)) *🪙R g x" have h: "x ∈ sphere 0 1 ∩ S ==> h x ∈ sphere 0 1 ∩ T"for x unfolding h_def using‹subspace T› gim gnz subspace_mul by fastforce have diffh: "h differentiable_on sphere 0 1 ∩ S" unfolding h_def using gnz by (fastforce intro: derivative_intros diffg differentiable_on_compose [OF diffg]) have homfg: "homotopic_with_canon (λz. True) (sphere 0 1 ∩ S) (T - {0}) f g" proof (rule homotopic_with_linear [OF contf]) show"continuous_on (sphere 0 1 ∩ S) g" using pfg by (simp add: differentiable_imp_continuous_on diffg) next have non0fg: "0 ∉ closed_segment (f x) (g x)"if"norm x = 1""x ∈ S"for x proof - have"f x ∈ sphere 0 1" using fim that by (simp add: image_subset_iff) moreoverhave"norm(f x - g x) < 1/2" using g12 that by auto ultimatelyshow ?thesis by (auto simp: norm_minus_commute dest: segment_bound) qed show"closed_segment (f x) (g x) ⊆ T - {0}"if"x ∈ sphere 0 1 ∩ S"for x proof - have"convex T" by (simp add: ‹subspace T› subspace_imp_convex) thenhave"convex hull {f x, g x} ⊆ T" by (metis IntD2 PiE closed_segment_subset fim gim segment_convex_hull that) thenshow ?thesis using that non0fg segment_convex_hull by fastforce qed qed obtain d where d: "d ∈ (sphere 0 1 ∩ T) - h ` (sphere 0 1 ∩ S)" using h spheremap_lemma1 [OF ST ‹S ⊆ T› diffh] by force thenhave non0hd: "0 ∉ closed_segment (h x) (- d)"if"norm x = 1""x ∈ S"for x using midpoint_between [of 0 "h x""-d"] that h [of x] by (auto simp: between_mem_segment midpoint_def) have conth: "continuous_on (sphere 0 1 ∩ S) h" using differentiable_imp_continuous_on diffh by blast have hom_hd: "homotopic_with_canon (λz. True) (sphere 0 1 ∩ S) (T - {0}) h (λx. -d)" proof (rule homotopic_with_linear [OF conth continuous_on_const]) fix x assume x: "x ∈ sphere 0 1 ∩ S" have"convex hull {h x, - d} ⊆ T" proof (rule hull_minimal) show"{h x, - d} ⊆ T" using h d x by (force simp: subspace_neg [OF ‹subspace T›]) qed (simp add: subspace_imp_convex [OF ‹subspace T›]) with x segment_convex_hull show"closed_segment (h x) (- d) ⊆ T - {0}" by (auto simp add: subset_Diff_insert non0hd) qed have conT0: "continuous_on (T - {0}) (λy. inverse(norm y) *🪙R y)" by (intro continuous_intros) auto have sub0T: "(λy. y /🪙R norm y) ∈ (T - {0}) → sphere 0 1 ∩ T" by (fastforce simp: assms(2) subspace_mul) obtain c where homhc: "homotopic_with_canon (λz. True) (sphere 0 1 ∩ S) (sphere 0 1 ∩ T) h (λx. c)" proof show"homotopic_with_canon (λz. True) (sphere 0 1 ∩ S) (sphere 0 1 ∩ T) h (λx. - d)" using d by (force simp: h_def
intro: homotopic_with_eq homotopic_with_compose_continuous_left [OF hom_hd conT0 sub0T]) qed have"homotopic_with_canon (λx. True) (sphere 0 1 ∩ S) (sphere 0 1 ∩ T) f h" by (force simp: h_def
intro: homotopic_with_eq homotopic_with_compose_continuous_left [OF homfg conT0 sub0T]) thenshow ?thesis by (metis homotopic_with_trans [OF _ homhc]) qed
lemma spheremap_lemma3: assumes"bounded S""convex S""subspace U"and affSU: "aff_dim S ≤ dim U" obtains T where"subspace T""T ⊆ U""S ≠ {} ==> aff_dim T = aff_dim S" "(rel_frontier S) homeomorphic (sphere 0 1 ∩ T)" proof (cases "S = {}") case True with‹subspace U› subspace_0 show ?thesis by (rule_tac T = "{0}"in that) auto next case False thenobtain a where"a ∈ S" by auto thenhave affS: "aff_dim S = int (dim ((λx. -a+x) ` S))" by (metis hull_inc aff_dim_eq_dim) with affSU have"dim ((λx. -a+x) ` S) ≤ dim U" by linarith with choose_subspace_of_subspace obtain T where"subspace T""T ⊆ span U"and dimT: "dim T = dim ((λx. -a+x) ` S)" . show ?thesis proof (rule that [OF ‹subspace T›]) show"T ⊆ U" using span_eq_iff ‹subspace U›‹T ⊆ span U›by blast show"aff_dim T = aff_dim S" using dimT ‹subspace T› affS aff_dim_subspace by fastforce show"rel_frontier S homeomorphic sphere 0 1 ∩ T" proof - have"aff_dim (ball 0 1 ∩ T) = aff_dim (T)" by (metis IntI interior_ball ‹subspace T› aff_dim_convex_Int_nonempty_interior centre_in_ball empty_iff inf_commute subspace_0 subspace_imp_convex zero_less_one) thenhave affS_eq: "aff_dim S = aff_dim (ball 0 1 ∩ T)" using‹aff_dim T = aff_dim S›by simp have"rel_frontier S homeomorphic rel_frontier(ball 0 1 ∩ T)" using homeomorphic_rel_frontiers_convex_bounded_sets [OF ‹convex S›‹bounded S›] by (simp add: ‹subspace T› affS_eq assms bounded_Int convex_Int
homeomorphic_rel_frontiers_convex_bounded_sets subspace_imp_convex) alsohave"... = frontier (ball 0 1) ∩ T" proof (rule convex_affine_rel_frontier_Int [OF convex_ball]) show"affine T" by (simp add: ‹subspace T› subspace_imp_affine) show"interior (ball 0 1) ∩ T ≠ {}" using‹subspace T› subspace_0 by force qed alsohave"... = sphere 0 1 ∩ T" by auto finallyshow ?thesis . qed qed qed
proposition inessential_spheremap_lowdim_gen: fixes f :: "'M::euclidean_space ==> 'a::euclidean_space" assumes"convex S""bounded S""convex T""bounded T" and affST: "aff_dim S < aff_dim T" and contf: "continuous_on (rel_frontier S) f" and fim: "f ∈ (rel_frontier S) → rel_frontier T" obtains c where"homotopic_with_canon (λz. True) (rel_frontier S) (rel_frontier T) f (λx. c)" proof (cases "S = {}") case True thenshow ?thesis using homotopic_with_canon_on_empty that by auto next case False thenshow ?thesis proof (cases "T = {}") case True thenshow ?thesis by (smt (verit, best) False affST aff_dim_negative_iff) next case False obtain T':: "'a set" where"subspace T'"and affT': "aff_dim T' = aff_dim T" and homT: "rel_frontier T homeomorphic sphere 0 1 ∩ T'" using‹T ≠ {}› spheremap_lemma3 [OF ‹bounded T›‹convex T› subspace_UNIV, where 'b='a] by (force simp add: aff_dim_le_DIM) with homeomorphic_imp_homotopy_eqv have relT: "sphere 0 1 ∩ T' homotopy_eqv rel_frontier T" using homotopy_equivalent_space_sym by blast have"aff_dim S ≤ int (dim T')" using affT' ‹subspace T'› affST aff_dim_subspace by force with spheremap_lemma3 [OF ‹bounded S›‹convex S›‹subspace T'›] ‹S ≠ {}› obtain S':: "'a set"where"subspace S'""S' ⊆ T'" and affS': "aff_dim S' = aff_dim S" and homT: "rel_frontier S homeomorphic sphere 0 1 ∩ S'" by metis with homeomorphic_imp_homotopy_eqv have relS: "sphere 0 1 ∩ S' homotopy_eqv rel_frontier S" using homotopy_equivalent_space_sym by blast have dimST': "dim S' < dim T'" by (metis ‹S' ⊆ T'›‹subspace S'›‹subspace T'› affS' affST affT' less_irrefl not_le subspace_dim_equal) have"∃c. homotopic_with_canon (λz. True) (rel_frontier S) (rel_frontier T) f (λx. c)" using spheremap_lemma2 homotopy_eqv_cohomotopic_triviality_null[OF relS] using homotopy_eqv_homotopic_triviality_null_imp [OF relT contf fim] by (metis ‹S' ⊆ T'›‹subspace S'›‹subspace T'› dimST' image_subset_iff_funcset) with that show ?thesis by blast qed qed
lemma inessential_spheremap_lowdim: fixes f :: "'M::euclidean_space ==> 'a::euclidean_space" assumes "DIM('M) < DIM('a)"and f: "continuous_on (sphere a r) f""f ∈ (sphere a r) → (sphere b s)" obtains c where"homotopic_with_canon (λz. True) (sphere a r) (sphere b s) f (λx. c)" proof (cases "s ≤ 0") case True thenshow ?thesis by (meson nullhomotopic_into_contractible f contractible_sphere that) next case False show ?thesis proof (cases "r ≤ 0") case True thenshow ?thesis by (meson f nullhomotopic_from_contractible contractible_sphere that) next case False with‹¬ s ≤ 0›have"r > 0""s > 0"by auto show thesis using inessential_spheremap_lowdim_gen [of "cball a r""cball b s" f] using‹0 🚫›‹0 🚫› assms(1) that by (auto simp add: f aff_dim_cball) qed qed
subsection‹ Some technical lemmas about extending maps from cell complexes›
lemma extending_maps_Union_aux: assumes fin: "finite F" and"∧S. S ∈F==> closed S" and"∧S T. [S ∈F; T ∈F; S ≠ T]==> S ∩ T ⊆ K" and"∧S. S ∈F==>∃g. continuous_on S g ∧ g ∈ S → T ∧ (∀x ∈ S ∩ K. g x = h x)" shows"∃g. continuous_on (∪F) g ∧ g ∈ (∪F) → T ∧ (∀x ∈∪F∩ K. g x = h x)" using assms proof (inductionF) case empty show ?caseby simp next case (insert S F) thenobtain f where contf: "continuous_on S f"and fim: "f ∈ S → T"and feq: "∀x ∈ S ∩ K. f x = h x" by (metis funcset_image insert_iff) obtain g where contg: "continuous_on (∪F) g"and gim: "g ∈ (∪F) → T"and geq: "∀x ∈∪F∩ K. g x = h x" using insert by auto have fg: "f x = g x"if"x ∈ T""T ∈F""x ∈ S"for x T proof - have"T ∩ S ⊆ K ∨ S = T" using that by (metis (no_types) insert.prems(2) insertCI) thenshow ?thesis using UnionI feq geq ‹S ∉F› subsetD that by fastforce qed moreoverhave"continuous_on (S ∪∪F) (λx. if x ∈ S then f x else g x)" by (auto simp: insert closed_Union contf contg intro: fg continuous_on_cases) moreoverhave"S ∪∪F = ∪ (insert S F)" by auto ultimatelyshow ?case by (smt (verit) Int_iff Pi_iff UnE feq fim geq gim) qed
lemma extending_maps_Union: assumes fin: "finite F" and"∧S. S ∈F==>∃g. continuous_on S g ∧ g ∈ S → T ∧ (∀x ∈ S ∩ K. g x = h x)" and"∧S. S ∈F==> closed S" and K: "∧X Y. [X ∈F; Y ∈F; ¬ X ⊆ Y; ¬ Y ⊆ X]==> X ∩ Y ⊆ K" shows"∃g. continuous_on (∪F) g ∧ g ∈ (∪F) → T ∧ (∀x ∈∪F∩ K. g x = h x)" proof - have"∧S T. [S ∈F; ∀U∈F. ¬ S ⊂ U; T ∈F; ∀U∈F. ¬ T ⊂ U; S ≠ T]==> S ∩ T ⊆ K" by (metis K psubsetI) thenshow ?thesis apply (simp flip: Union_maximal_sets [OF fin]) apply (rule extending_maps_Union_aux, simp_all add: Union_maximal_sets [OF fin] assms) done qed
lemma extend_map_lemma: assumes"finite F""G⊆F""convex T""bounded T" and poly: "∧X. X ∈F==> polytope X" and aff: "∧X. X ∈F - G==> aff_dim X < aff_dim T" and face: "∧S T. [S ∈F; T ∈F]==> (S ∩ T) face_of S" and contf: "continuous_on (∪G) f"and fim: "f ∈ (∪G) → rel_frontier T" obtains g where"continuous_on (∪F) g""g ∈ (∪F) → rel_frontier T""∧x. x ∈∪G==> g x = f x" proof (cases "F - G = {}") case True show ?thesis using True assms(2) contf fim that by force next case False thenhave"0 ≤ aff_dim T" by (metis aff aff_dim_empty aff_dim_geq aff_dim_negative_iff all_not_in_conv not_less) thenobtain i::nat where i: "int i = aff_dim T" by (metis nonneg_eq_int) have Union_empty_eq: "∪{D. D = {} ∧ P D} = {}"for P :: "'a set ==> bool" by auto have face': "∧S T. [S ∈F; T ∈F]==> (S ∩ T) face_of S ∧ (S ∩ T) face_of T" by (metis face inf_commute) have extendf: "∃g. continuous_on (∪(G∪ {D. ∃C ∈F. D face_of C ∧ aff_dim D < i})) g ∧ g ` (∪ (G∪ {D. ∃C ∈F. D face_of C ∧ aff_dim D < i})) ⊆ rel_frontier T ∧ (∀x ∈∪G. g x = f x)" if"i ≤ aff_dim T"for i::nat using that proof (induction i) case 0 show ?case using 0 contf fim by (auto simp add: Union_empty_eq) next case (Suc p) with‹bounded T›have"rel_frontier T ≠ {}" by (auto simp: rel_frontier_eq_empty affine_bounded_eq_lowdim [of T]) thenobtain t where t: "t ∈ rel_frontier T"by auto have ple: "int p ≤ aff_dim T"using Suc.prems by force obtain h where conth: "continuous_on (∪(G∪ {D. ∃C ∈F. D face_of C ∧ aff_dim D < p})) h" and him: "h ` (∪ (G∪ {D. ∃C ∈F. D face_of C ∧ aff_dim D < p})) ⊆ rel_frontier T" and heq: "∧x. x ∈∪G==> h x = f x" using Suc.IH [OF ple] by auto let ?Faces = "{D. ∃C ∈F. D face_of C ∧ aff_dim D ≤ p}" have extendh: "∃g. continuous_on D g ∧ g ∈ D → rel_frontier T ∧ (∀x ∈ D ∩∪(G∪ {D. ∃C ∈F. D face_of C ∧ aff_dim D < p}). g x = h x)" if D: "D ∈G∪ ?Faces"for D proof (cases "D ⊆∪(G∪ {D. ∃C ∈F. D face_of C ∧ aff_dim D < p})") case True have"continuous_on D h" using True conth continuous_on_subset by blast moreoverhave"h ∈ D → rel_frontier T" using True him by blast ultimatelyshow ?thesis by blast next case False note notDsub = False show ?thesis proof (cases "∃a. D = {a}") case True thenobtain a where"D = {a}"by auto with notDsub t show ?thesis by (rule_tac x="λx. t"in exI) simp next case False have"D ≠ {}"using notDsub by auto have Dnotin: "D ∉G∪ {D. ∃C ∈F. D face_of C ∧ aff_dim D < p}" using notDsub by auto thenhave"D ∉G"by simp have"D ∈ ?Faces - {D. ∃C ∈F. D face_of C ∧ aff_dim D < p}" using Dnotin that by auto thenobtain C where"C ∈F""D face_of C"and affD: "aff_dim D = int p" by auto thenhave"bounded D" using face_of_polytope_polytope poly polytope_imp_bounded by blast thenhave [simp]: "¬ affine D" using affine_bounded_eq_trivial False ‹D ≠ {}›‹bounded D›by blast have"{F. F facet_of D} ⊆ {E. E face_of C ∧ aff_dim E < int p}" by clarify (metis ‹D face_of C› affD eq_iff face_of_trans facet_of_def zle_diff1_eq) moreoverhave"polyhedron D" using‹C ∈F›‹D face_of C› face_of_polytope_polytope poly polytope_imp_polyhedron by auto ultimatelyhave relf_sub: "rel_frontier D ⊆∪ {E. E face_of C ∧ aff_dim E < p}" by (simp add: rel_frontier_of_polyhedron Union_mono) thenhave him_relf: "h ∈ rel_frontier D → rel_frontier T" using‹C ∈F› him by blast have"convex D" by (simp add: ‹polyhedron D› polyhedron_imp_convex) have affD_lessT: "aff_dim D < aff_dim T" using Suc.prems affD by linarith have contDh: "continuous_on (rel_frontier D) h" using‹C ∈F› relf_sub by (blast intro: continuous_on_subset [OF conth]) thenhave *: "(∃c. homotopic_with_canon (λx. True) (rel_frontier D) (rel_frontier T) h (λx. c)) = (∃g. continuous_on UNIV g ∧ range g ⊆ rel_frontier T ∧ (∀x∈rel_frontier D. g x = h x))" by (simp add: assms image_subset_iff_funcset rel_frontier_eq_empty him_relf nullhomotopic_into_rel_frontier_extension [OF closed_rel_frontier]) have"∃c. homotopic_with_canon (λx. True) (rel_frontier D) (rel_frontier T) h (λx. c)" by (metis inessential_spheremap_lowdim_gen
[OF ‹convex D›‹bounded D›‹convex T›‹bounded T› affD_lessT contDh him_relf]) thenobtain g where contg: "continuous_on UNIV g" and gim: "range g ⊆ rel_frontier T" and gh: "∧x. x ∈ rel_frontier D ==> g x = h x" by (metis *) have"D ∩ E ⊆ rel_frontier D" if"E ∈G∪ {D. Bex F ((face_of) D) ∧ aff_dim D < int p}"for E proof (rule face_of_subset_rel_frontier) show"D ∩ E face_of D" using that proof safe assume"E ∈G" thenshow"D ∩ E face_of D" by (meson ‹C ∈F›‹D face_of C› assms(2) face' face_of_Int_subface face_of_refl_eq poly polytope_imp_convex subsetD) next fix x assume"aff_dim E < int p""x ∈F""E face_of x" thenshow"D ∩ E face_of D" by (meson ‹C ∈F›‹D face_of C› face' face_of_Int_subface that) qed show"D ∩ E ≠ D" using that notDsub by auto qed moreoverhave"continuous_on D g" using contg continuous_on_subset by blast ultimatelyshow ?thesis by (rule_tac x=g in exI) (use gh gim in fastforce) qed qed have intle: "i < 1 + int j ⟷ i ≤ int j"for i j by auto have"finite G" using‹finite F›‹G⊆F› rev_finite_subset by blast moreoverhave"finite (?Faces)" proof - have🍋: "finite (∪ {{D. D face_of C} |C. C ∈F})" by (auto simp: ‹finite F› finite_polytope_faces poly) show ?thesis by (auto intro: finite_subset [OF _ 🍋]) qed ultimatelyhave fin: "finite (G∪ ?Faces)" by simp have clo: "closed S"if"S ∈G∪ ?Faces"for S using that ‹G⊆F› face_of_polytope_polytope poly polytope_imp_closed by blast have K: "X ∩ Y ⊆∪(G∪ {D. ∃C∈F. D face_of C ∧ aff_dim D < int p})" if"X ∈G∪ ?Faces""Y ∈G∪ ?Faces""¬ Y ⊆ X"for X Y proof - have ff: "X ∩ Y face_of X ∧ X ∩ Y face_of Y" if XY: "X face_of D""Y face_of E"and DE: "D ∈F""E ∈F"for D E by (rule face_of_Int_subface [OF _ _ XY]) (auto simp: face' DE) show ?thesis using that apply clarsimp by (smt (verit) IntI face_of_aff_dim_lt face_of_imp_convex face_of_trans ff inf_commute) qed obtain g where"continuous_on (∪(G∪ ?Faces)) g" "g ` ∪(G∪ ?Faces) ⊆ rel_frontier T" "(∀x ∈∪(G∪ ?Faces) ∩ ∪(G∪ {D. ∃C∈F. D face_of C ∧ aff_dim D < p}). g x = h x)" by (rule exE [OF extending_maps_Union [OF fin extendh clo K]], blast+) thenshow ?case by (simp add: intle local.heq [symmetric], blast) qed have eq: "∪(G∪ {D. ∃C ∈F. D face_of C ∧ aff_dim D < i}) = ∪F" proof show"∪(G∪ {D. ∃C∈F. D face_of C ∧ aff_dim D < int i}) ⊆∪F" using‹G⊆F› face_of_imp_subset by fastforce show"∪F⊆∪(G∪ {D. ∃C∈F. D face_of C ∧ aff_dim D < i})" using face by (intro Union_mono) (fastforce simp: aff i) qed have"int i ≤ aff_dim T"by (simp add: i) thenshow ?thesis using extendf [of i] that unfolding eq by fastforce qed
lemma extend_map_lemma_cofinite0: assumes"finite F" and"pairwise (λS T. S ∩ T ⊆ K) F" and"∧S. S ∈F==>∃a g. a ∉ U ∧ continuous_on (S - {a}) g ∧ g ∈ (S - {a}) → T ∧ (∀x ∈ S ∩ K. g x = h x)" and"∧S. S ∈F==> closed S" shows"∃C g. finite C ∧ disjnt C U ∧ card C ≤ card F∧ continuous_on (∪F - C) g ∧ g ∈ (∪F - C) → T ∧ (∀x ∈ (∪F - C) ∩ K. g x = h x)" using assms proofinduction case empty thenshow ?case by force next case (insert X F) thenhave"closed X"and clo: "∧X. X ∈F==> closed X" andF: "∧S. S ∈F==>∃a g. a ∉ U ∧ continuous_on (S - {a}) g ∧ g ∈ (S - {a}) → T ∧ (∀x ∈ S ∩ K. g x = h x)" and pwX: "∧Y. Y ∈F∧ Y ≠ X ⟶ X ∩ Y ⊆ K ∧ Y ∩ X ⊆ K" and pwF: "pairwise (λ S T. S ∩ T ⊆ K) F" by (simp_all add: pairwise_insert) obtain C g where C: "finite C""disjnt C U""card C ≤ card F" and contg: "continuous_on (∪F - C) g" and gim: "g ∈ (∪F - C) → T" and gh: "∧x. x ∈ (∪F - C) ∩ K ==> g x = h x" using insert.IH [OF pwF F clo] by auto obtain a f where"a ∉ U" and contf: "continuous_on (X - {a}) f" and fim: "f ∈ (X - {a}) → T" and fh: "(∀x ∈ X ∩ K. f x = h x)" using insert.prems by (meson insertI1) show ?case proof (intro exI conjI) show"finite (insert a C)" by (simp add: C) show"disjnt (insert a C) U" using C ‹a ∉ U›by simp show"card (insert a C) ≤ card (insert X F)" by (simp add: C card_insert_if insert.hyps le_SucI) have"closed (∪F)" using clo insert.hyps by blast have"continuous_on (X - insert a C) f" using contf by (force simp: elim: continuous_on_subset) moreoverhave"continuous_on (∪F - insert a C) g" using contg by (force simp: elim: continuous_on_subset) ultimately have"continuous_on (X - insert a C ∪ (∪F - insert a C)) (λx. if x ∈ X then f x else g x)" apply (intro continuous_on_cases_local; simp add: closedin_closed) using‹closed X›apply blast using‹closed (∪F)›apply blast using fh gh insert.hyps pwX by fastforce thenshow"continuous_on (∪(insert X F) - insert a C) (λa. if a ∈ X then f a else g a)" by (blast intro: continuous_on_subset) show"∀x∈(∪(insert X F) - insert a C) ∩ K. (if x ∈ X then f x else g x) = h x" using gh by (auto simp: fh) show"(λa. if a ∈ X then f a else g a) ∈ (∪(insert X F) - insert a C) → T" using fim gim Pi_iff by fastforce qed qed
lemma extend_map_lemma_cofinite1: assumes"finite F" andF: "∧X. X ∈F==>∃a g. a ∉ U ∧ continuous_on (X - {a}) g ∧ g ∈ (X - {a}) → T ∧ (∀x ∈ X ∩ K. g x = h x)" and clo: "∧X. X ∈F==> closed X" and K: "∧X Y. [X ∈F; Y ∈F; ¬ X ⊆ Y; ¬ Y ⊆ X]==> X ∩ Y ⊆ K" obtains C g where"finite C""disjnt C U""card C ≤ card F""continuous_on (∪F - C) g" "g ∈ (∪F - C) → T" "∧x. x ∈ (∪F - C) ∩ K ==> g x = h x" proof - let ?F = "{X ∈F. ∀Y∈F. ¬ X ⊂ Y}" have [simp]: "∪?F = ∪F" by (simp add: Union_maximal_sets assms) have fin: "finite ?F" by (force intro: finite_subset [OF _ ‹finite F›]) have pw: "pairwise (λ S T. S ∩ T ⊆ K) ?F" by (simp add: pairwise_def) (metis K psubsetI) have"card {X ∈F. ∀Y∈F. ¬ X ⊂ Y} ≤ card F" by (simp add: ‹finite F› card_mono) moreover obtain C g where"finite C ∧ disjnt C U ∧ card C ≤ card ?F∧ continuous_on (∪?F - C) g ∧ g ∈ (∪?F - C) → T ∧ (∀x ∈ (∪?F - C) ∩ K. g x = h x)" using extend_map_lemma_cofinite0 [OF fin pw, of U T h] by (fastforce intro!: clo F) ultimatelyshow ?thesis by (rule_tac C=C and g=g in that) auto qed
lemma extend_map_lemma_cofinite: assumes"finite F""G⊆F"and T: "convex T""bounded T" and poly: "∧X. X ∈F==> polytope X" and contf: "continuous_on (∪G) f"and fim: "f ∈ (∪G) → rel_frontier T" and face: "∧X Y. [X ∈F; Y ∈F]==> (X ∩ Y) face_of X" and aff: "∧X. X ∈F - G==> aff_dim X ≤ aff_dim T" obtains C g where "finite C""disjnt C (∪G)""card C ≤ card F""continuous_on (∪F - C) g" "g ∈ (∪F - C) → rel_frontier T""∧x. x ∈∪G==> g x = f x" proof -
define Hwhere"H≡G∪ {D. ∃C ∈F - G. D face_of C ∧ aff_dim D < aff_dim T}" have"finite G" using assms finite_subset by blast have *: "finite (∪{{D. D face_of C} |C. C ∈F})" using finite_polytope_faces poly ‹finite F›by force thenhave"finite H" by (auto simp: H_def‹finite G› intro: finite_subset [OF _ *]) have face': "∧S T. [S ∈F; T ∈F]==> (S ∩ T) face_of S ∧ (S ∩ T) face_of T" by (metis face inf_commute) have *: "∧X Y. [X ∈H; Y ∈H]==> X ∩ Y face_of X" by (simp add: H_def) (smt (verit) ‹G⊆F› DiffE face' face_of_Int_subface in_mono inf.idem) obtain h where conth: "continuous_on (∪H) h"and him: "h ∈ (∪H) → rel_frontier T" and hf: "∧x. x ∈∪G==> h x = f x" proof (rule extend_map_lemma [OF ‹finite H› [unfolded H_def] Un_upper1 T]) show"∧X. [X ∈G∪ {D. ∃C∈F - G. D face_of C ∧ aff_dim D < aff_dim T}]==> polytope X" using‹G⊆F› face_of_polytope_polytope poly by fastforce qed (use * H_def contf fim in auto) have"bounded (∪G)" using‹finite G›‹G⊆F› poly polytope_imp_bounded by blast thenhave"∪G≠ UNIV" by auto thenobtain a where a: "a ∉∪G" by blast haveF: "∃a g. a ∉∪G∧ continuous_on (D - {a}) g ∧ g ∈ (D - {a}) → rel_frontier T ∧ (∀x ∈ D ∩∪H. g x = h x)" if"D ∈F"for D proof (cases "D ⊆∪H") case True thenhave"h ∈ (D - {a}) → rel_frontier T""continuous_on (D - {a}) h" using him by (blast intro!: ‹a ∉∪G› continuous_on_subset [OF conth])+ thenshow ?thesis using a by blast next case False note D_not_subset = False show ?thesis proof (cases "D ∈G") case True with D_not_subset show ?thesis by (auto simp: H_def) next case False thenhave affD: "aff_dim D ≤ aff_dim T" by (simp add: ‹D ∈F› aff) show ?thesis proof (cases "rel_interior D = {}") case True with‹D ∈F› poly a show ?thesis by (force simp: rel_interior_eq_empty polytope_imp_convex) next case False thenobtain b where brelD: "b ∈ rel_interior D" by blast have"polyhedron D" by (simp add: poly polytope_imp_polyhedron that) have"rel_frontier D retract_of affine hull D - {b}" by (simp add: rel_frontier_retract_of_punctured_affine_hull poly polytope_imp_bounded polytope_imp_convex that brelD) thenobtain r where relfD: "rel_frontier D ⊆ affine hull D - {b}" and contr: "continuous_on (affine hull D - {b}) r" and rim: "r ∈ (affine hull D - {b}) → rel_frontier D" and rid: "∧x. x ∈ rel_frontier D ==> r x = x" by (auto simp: retract_of_def retraction_def) show ?thesis proof (intro exI conjI ballI) show"b ∉∪G" proof clarify fix E assume"b ∈ E""E ∈G" thenhave"E ∩ D face_of E ∧ E ∩ D face_of D" using‹G⊆F› face' that by auto with face_of_subset_rel_frontier ‹E ∈G›‹b ∈ E› brelD rel_interior_subset [of D]
D_not_subset rel_frontier_def H_def show False by blast qed have"r ` (D - {b}) ⊆ r ` (affine hull D - {b})" by (simp add: Diff_mono hull_subset image_mono) alsohave"... ⊆ rel_frontier D" using rim by auto alsohave"... ⊆∪{E. E face_of D ∧ aff_dim E < aff_dim T}" using affD by (force simp: rel_frontier_of_polyhedron [OF ‹polyhedron D›] facet_of_def) alsohave"... ⊆∪(H)" using D_not_subset H_def that by fastforce finallyhave rsub: "r ` (D - {b}) ⊆∪(H)" . show"continuous_on (D - {b}) (h ∘ r)" proof (rule continuous_on_compose) show"continuous_on (D - {b}) r" by (meson Diff_mono continuous_on_subset contr hull_subset order_refl) show"continuous_on (r ` (D - {b})) h" by (simp add: Diff_mono hull_subset continuous_on_subset [OF conth rsub]) qed show"(h ∘ r) ∈ (D - {b}) → rel_frontier T" using brelD him rsub by fastforce show"(h ∘ r) x = h x"if x: "x ∈ D ∩∪H"for x proof -
consider A where"x ∈ D""A ∈G""x ∈ A"
| A B where"x ∈ D""A face_of B""B ∈F""B ∉G""aff_dim A < aff_dim T""x ∈ A" using x by (auto simp: H_def) thenhave xrel: "x ∈ rel_frontier D" proof cases case 1 show ?thesis proof (rule face_of_subset_rel_frontier [THEN subsetD]) show"D ∩ A face_of D" using‹A ∈G›‹G⊆F› face ‹D ∈F›by blast show"D ∩ A ≠ D" using‹A ∈G› D_not_subset H_defby blast qed (auto simp: 1) next case 2 show ?thesis proof (rule face_of_subset_rel_frontier [THEN subsetD]) have"D face_of D" by (simp add: ‹polyhedron D› polyhedron_imp_convex face_of_refl) thenshow"D ∩ A face_of D" by (meson "2"(2) "2"(3) ‹D ∈F› face' face_of_Int_Int face_of_face) show"D ∩ A ≠ D" using"2" D_not_subset H_defby blast qed (auto simp: 2) qed show ?thesis by (simp add: rid xrel) qed qed qed qed qed have clo: "∧S. S ∈F==> closed S" by (simp add: poly polytope_imp_closed) obtain C g where"finite C""disjnt C (∪G)""card C ≤ card F""continuous_on (∪F - C) g" "g ∈ (∪F - C) → rel_frontier T" and gh: "∧x. x ∈ (∪F - C) ∩∪H==> g x = h x" proof (rule extend_map_lemma_cofinite1 [OF ‹finite F›F clo]) show"X ∩ Y ⊆∪H"if XY: "X ∈F""Y ∈F"and"¬ X ⊆ Y""¬ Y ⊆ X"for X Y proof (cases "X ∈G") case True thenshow ?thesis by (auto simp: H_def) next case False have"X ∩ Y ≠ X" using‹¬ X ⊆ Y›by blast with XY show ?thesis by (clarsimp simp: H_def)
(metis Diff_iff Int_iff aff antisym_conv face face_of_aff_dim_lt face_of_refl
not_le poly polytope_imp_convex) qed qed (blast)+ with‹G⊆F›show ?thesis by (rule_tac C=C and g=g in that) (auto simp: disjnt_def hf [symmetric] H_def intro!: gh) qed
text‹The next two proofs are similar› theorem extend_map_cell_complex_to_sphere: assumes"finite F"and S: "S ⊆∪F""closed S"and T: "convex T""bounded T" and poly: "∧X. X ∈F==> polytope X" and aff: "∧X. X ∈F==> aff_dim X < aff_dim T" and face: "∧X Y. [X ∈F; Y ∈F]==> (X ∩ Y) face_of X" and contf: "continuous_on S f"and fim: "f ∈ S → rel_frontier T" obtains g where"continuous_on (∪F) g" "g ∈ (∪F) → rel_frontier T""∧x. x ∈ S ==> g x = f x" proof - obtain V g where"S ⊆ V""open V""continuous_on V g"and gim: "g ∈ V → rel_frontier T"andgf: "∧x. x ∈ S ==> g x = f x" using neighbourhood_extension_into_ANR [OF contf fim _ ‹closed S›] ANR_rel_frontier_convex T by blast have"compact S" by (meson assms compact_Union poly polytope_imp_compact seq_compact_closed_subset seq_compact_eq_compact) thenobtain d where"d > 0"and d: "∧x y. [x ∈ S; y ∈ - V]==> d ≤ dist x y" using separate_compact_closed [of S "-V"] ‹open V›‹S ⊆ V›by force obtainGwhere"finite G""∪G = ∪F" and diaG: "∧X. X ∈G==> diameter X < d" and polyG: "∧X. X ∈G==> polytope X" and affG: "∧X. X ∈G==> aff_dim X ≤ aff_dim T - 1" and faceG: "∧X Y. [X ∈G; Y ∈G]==> X ∩ Y face_of X" proof (rule cell_complex_subdivision_exists [OF ‹d>0›‹finite F› poly _ face]) show"∧X. X ∈F==> aff_dim X ≤ aff_dim T - 1" by (simp add: aff) qed auto obtain h where conth: "continuous_on (∪G) h"and him: "h ` ∪G⊆ rel_frontier T"and hg: "∧x. x ∈∪(G∩ Pow V) ==> h x = g x" proof (rule extend_map_lemma [of G"G∩ Pow V" T g]) show"continuous_on (∪(G∩ Pow V)) g" by (metis Union_Int_subset Union_Pow_eq ‹continuous_on V g› continuous_on_subset le_inf_iff) qed (use‹finite G› T polyG affG faceG gim image_subset_iff_funcset in auto) show ?thesis proof show"continuous_on (∪F) h" using‹∪G = ∪F› conth by auto show"h ∈∪F→ rel_frontier T" using‹∪G = ∪F› him by auto show"h x = f x"if"x ∈ S"for x proof - have"x ∈∪G" using‹∪G = ∪F›‹S ⊆∪F› that by auto thenobtain X where"x ∈ X""X ∈G"by blast thenhave"diameter X < d""bounded X" by (auto simp: diaG ‹X ∈G› polyG polytope_imp_bounded) thenhave"X ⊆ V"using d [OF ‹x ∈ S›] diameter_bounded_bound [OF ‹bounded X›‹x ∈ X›] by fastforce have"h x = g x" using‹X ∈G›‹X ⊆ V›‹x ∈ X› hg by auto alsohave"... = f x" by (simp add: gf that) finallyshow"h x = f x" . qed qed qed
theorem extend_map_cell_complex_to_sphere_cofinite: assumes"finite F"and S: "S ⊆∪F""closed S"and T: "convex T""bounded T" and poly: "∧X. X ∈F==> polytope X" and aff: "∧X. X ∈F==> aff_dim X ≤ aff_dim T" and face: "∧X Y. [X ∈F; Y ∈F]==> (X ∩ Y) face_of X" and contf: "continuous_on S f"and fim: "f ∈ S → rel_frontier T" obtains C g where"finite C""disjnt C S""continuous_on (∪F - C) g" "g ∈ (∪F - C) → rel_frontier T""∧x. x ∈ S ==> g x = f x" proof - obtain V g where"S ⊆ V""open V""continuous_on V g"and gim: "g ∈ V → rel_frontier T"andgf: "∧x. x ∈ S ==> g x = f x" using neighbourhood_extension_into_ANR [OF contf fim _ ‹closed S›] ANR_rel_frontier_convex T by blast have"compact S" by (meson assms compact_Union poly polytope_imp_compact seq_compact_closed_subset seq_compact_eq_compact) thenobtain d where"d > 0"and d: "∧x y. [x ∈ S; y ∈ - V]==> d ≤ dist x y" using separate_compact_closed [of S "-V"] ‹open V›‹S ⊆ V›by force obtainGwhere"finite G""∪G = ∪F" and diaG: "∧X. X ∈G==> diameter X < d" and polyG: "∧X. X ∈G==> polytope X" and affG: "∧X. X ∈G==> aff_dim X ≤ aff_dim T" and faceG: "∧X Y. [X ∈G; Y ∈G]==> X ∩ Y face_of X" by (rule cell_complex_subdivision_exists [OF ‹d>0›‹finite F› poly aff face]) auto obtain C h where"finite C"and dis: "disjnt C (∪(G∩ Pow V))" and card: "card C ≤ card G"and conth: "continuous_on (∪G - C) h" and him: "h ∈ (∪G - C) → rel_frontier T" and hg: "∧x. x ∈∪(G∩ Pow V) ==> h x = g x" proof (rule extend_map_lemma_cofinite [of G"G∩ Pow V" T g]) show"continuous_on (∪(G∩ Pow V)) g" by (metis Union_Int_subset Union_Pow_eq ‹continuous_on V g› continuous_on_subset le_inf_iff) show"g ∈∪(G∩ Pow V) → rel_frontier T" using gim by force qed (auto intro: ‹finite G› T polyG affG dest: faceG) have"S ⊆∪(G∩ Pow V)" proof fix x assume"x ∈ S" thenhave"x ∈∪G" using‹∪G = ∪F›‹S ⊆∪F›by auto thenobtain X where"x ∈ X""X ∈G"by blast thenhave"diameter X < d""bounded X" by (auto simp: diaG ‹X ∈G› polyG polytope_imp_bounded) thenhave"X ⊆ V"using d [OF ‹x ∈ S›] diameter_bounded_bound [OF ‹bounded X›‹x ∈ X›] by fastforce thenshow"x ∈∪(G∩ Pow V)" using‹X ∈G›‹x ∈ X›by blast qed thenshow ?thesis by (metis PowI Union_Pow_eq ‹∪G = ∪F›‹finite C› conth dis disjnt_Union2 gf hg him subsetD that) qed
subsection‹ Special cases and corollaries involving spheres›
proposition extend_map_affine_to_sphere_cofinite_simple: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes"compact S""convex U""bounded U" and aff: "aff_dim T ≤ aff_dim U" and"S ⊆ T"and contf: "continuous_on S f" and fim: "f ∈ S → rel_frontier U" obtains K g where"finite K""K ⊆ T""disjnt K S""continuous_on (T - K) g" "g ∈ (T - K) → rel_frontier U" "∧x. x ∈ S ==> g x = f x" proof - have"∃K g. finite K ∧ disjnt K S ∧ continuous_on (T - K) g ∧ g ∈ (T - K) → rel_frontier U ∧ (∀x ∈ S. g x = f x)" if"affine T""S ⊆ T"and aff: "aff_dim T ≤ aff_dim U"for T proof (cases "S = {}") case True show ?thesis proof (cases "rel_frontier U = {}") case True with‹bounded U›have"aff_dim U ≤ 0" using affine_bounded_eq_lowdim rel_frontier_eq_empty by auto with aff have"aff_dim T ≤ 0"by auto thenobtain a where"T ⊆ {a}" using‹affine T› affine_bounded_eq_lowdim affine_bounded_eq_trivial by auto thenshow ?thesis using‹S = {}› fim by (metis Diff_cancel contf disjnt_empty2 finite.emptyI finite_insert finite_subset) next case False thenobtain a where"a ∈ rel_frontier U" by auto thenshow ?thesis using continuous_on_const [of _ a] ‹S = {}›by force qed next case False have"bounded S" by (simp add: ‹compact S› compact_imp_bounded) thenobtain b where b: "S ⊆ cbox (-b) b" using bounded_subset_cbox_symmetric by blast
define bbox where"bbox ≡ cbox (-(b+One)) (b+One)" have"cbox (-b) b ⊆ bbox" by (auto simp: bbox_def algebra_simps intro!: subset_box_imp) with b ‹S ⊆ T›have"S ⊆ bbox ∩ T" by auto thenhave Ssub: "S ⊆∪{bbox ∩ T}" by auto thenhave"aff_dim (bbox ∩ T) ≤ aff_dim U" by (metis aff aff_dim_subset inf_commute inf_le1 order_trans) obtain K g where K: "finite K""disjnt K S" and contg: "continuous_on (∪{bbox ∩ T} - K) g" and gim: "g ∈ (∪{bbox ∩ T} - K) → rel_frontier U" and gf: "∧x. x ∈ S ==> g x = f x" proof (rule extend_map_cell_complex_to_sphere_cofinite
[OF _ Ssub _ ‹convex U›‹bounded U› _ _ _ contf fim]) show"closed S" using‹compact S› compact_eq_bounded_closed by auto show poly: "∧X. X ∈ {bbox ∩ T} ==> polytope X" by (simp add: polytope_Int_polyhedron bbox_def polytope_interval affine_imp_polyhedron ‹affine T›) show"∧X Y. [X ∈ {bbox ∩ T}; Y ∈ {bbox ∩ T}]==> X ∩ Y face_of X" by (simp add:poly face_of_refl polytope_imp_convex) show"∧X. X ∈ {bbox ∩ T} ==> aff_dim X ≤ aff_dim U" by (simp add: ‹aff_dim (bbox ∩ T) ≤ aff_dim U›) qed auto
define fro where"fro ≡ λd. frontier(cbox (-(b + d *🪙R One)) (b + d *🪙R One))" obtain d where d12: "1/2 ≤ d""d ≤ 1"and dd: "disjnt K (fro d)" proof (rule disjoint_family_elem_disjnt [OF _ ‹finite K›]) show"infinite {1/2..1::real}" by (simp add: infinite_Icc) have dis1: "disjnt (fro x) (fro y)"if"xfor x y by (auto simp: algebra_simps that subset_box_imp disjnt_Diff1 frontier_def fro_def) thenshow"disjoint_family_on fro {1/2..1}" by (auto simp: disjoint_family_on_def disjnt_def neq_iff) qed auto
define c where"c ≡ b + d *🪙R One" have cbsub: "cbox (-b) b ⊆ box (-c) c""cbox (-b) b ⊆ cbox (-c) c""cbox (-c) c ⊆ bbox" using d12 by (auto simp: algebra_simps subset_box_imp c_def bbox_def) have clo_cbT: "closed (cbox (- c) c ∩ T)" by (simp add: affine_closed closed_Int closed_cbox ‹affine T›) have cpT_ne: "cbox (- c) c ∩ T ≠ {}" using‹S ≠ {}› b cbsub(2) ‹S ⊆ T›by fastforce have"closest_point (cbox (- c) c ∩ T) x ∉ K"if"x ∈ T""x ∉ K"for x proof (cases "x ∈ cbox (-c) c") case True with that show ?thesis by (simp add: closest_point_self) next case False have int_ne: "interior (cbox (-c) c) ∩ T ≠ {}" using‹S ≠ {}›‹S ⊆ T› b ‹cbox (- b) b ⊆ box (- c) c›by force have"convex T" by (meson ‹affine T› affine_imp_convex) thenhave"x ∈ affine hull (cbox (- c) c ∩ T)" by (metis Int_commute Int_iff ‹S ≠ {}›‹S ⊆ T› cbsub(1) ‹x ∈ T› affine_hull_convex_Int_nonempty_interior all_not_in_conv b hull_inc inf.orderE interior_cbox) thenhave"x ∈ affine hull (cbox (- c) c ∩ T) - rel_interior (cbox (- c) c ∩ T)" by (meson DiffI False Int_iff rel_interior_subset subsetCE) thenhave"closest_point (cbox (- c) c ∩ T) x ∈ rel_frontier (cbox (- c) c ∩ T)" by (rule closest_point_in_rel_frontier [OF clo_cbT cpT_ne]) moreoverhave"(rel_frontier (cbox (- c) c ∩ T)) ⊆ fro d" by (subst convex_affine_rel_frontier_Int [OF _ ‹affine T› int_ne]) (auto simp: fro_def c_def) ultimatelyshow ?thesis using dd by (force simp: disjnt_def) qed thenhave cpt_subset: "closest_point (cbox (- c) c ∩ T) ` (T - K) ⊆∪{bbox ∩ T} - K" using closest_point_in_set [OF clo_cbT cpT_ne] cbsub(3) by force show ?thesis proof (intro conjI ballI exI) have"continuous_on (T - K) (closest_point (cbox (- c) c ∩ T))" proof (rule continuous_on_closest_point) show"convex (cbox (- c) c ∩ T)" by (simp add: affine_imp_convex convex_Int ‹affine T›) show"closed (cbox (- c) c ∩ T)" using clo_cbT by blast show"cbox (- c) c ∩ T ≠ {}" using‹S ≠ {}› cbsub(2) b that by auto qed thenshow"continuous_on (T - K) (g ∘ closest_point (cbox (- c) c ∩ T))" by (metis continuous_on_compose continuous_on_subset [OF contg cpt_subset]) have"(g ∘ closest_point (cbox (- c) c ∩ T)) ` (T - K) ⊆ g ` (∪{bbox ∩ T} - K)" by (metis image_comp image_mono cpt_subset) alsohave"... ⊆ rel_frontier U" using gim by blast finallyshow"(g ∘ closest_point (cbox (- c) c ∩ T)) ∈ (T - K) → rel_frontier U" by blast show"(g ∘ closest_point (cbox (- c) c ∩ T)) x = f x"if"x ∈ S"for x proof - have"(g ∘ closest_point (cbox (- c) c ∩ T)) x = g x" unfolding o_def by (metis IntI ‹S ⊆ T› b cbsub(2) closest_point_self subset_eq that) alsohave"... = f x" by (simp add: that gf) finallyshow ?thesis . qed qed (auto simp: K) qed thenobtain K g where"finite K""disjnt K S" and contg: "continuous_on (affine hull T - K) g" and gim: "g ∈ (affine hull T - K) → rel_frontier U" and gf: "∧x. x ∈ S ==> g x = f x" by (metis aff affine_affine_hull aff_dim_affine_hull
order_trans [OF ‹S ⊆ T› hull_subset [of T affine]]) thenobtain K g where"finite K""disjnt K S" and contg: "continuous_on (T - K) g" and gim: "g ∈ (T - K) → rel_frontier U" and gf: "∧x. x ∈ S ==> g x = f x" by (rule_tac K=K and g=g in that) (auto simp: hull_inc elim: continuous_on_subset) thenshow ?thesis by (rule_tac K="K ∩ T"and g=g in that) (auto simp: disjnt_iff Diff_Int contg) qed
subsection‹Extending maps to spheres›
(*Up to extend_map_affine_to_sphere_cofinite_gen*)
lemma extend_map_affine_to_sphere1: fixes f :: "'a::euclidean_space ==> 'b::topological_space" assumes"finite K""affine U"and contf: "continuous_on (U - K) f" and fim: "f ∈ (U - K) → T" and comps: "∧C. [C ∈ components(U - S); C ∩ K ≠ {}]==> C ∩ L ≠ {}" and clo: "closedin (top_of_set U) S"and K: "disjnt K S""K ⊆ U" obtains g where"continuous_on (U - L) g""g ∈ (U - L) → T""∧x. x ∈ S ==> g x = f x" proof (cases "K = {}") case True thenshow ?thesis by (metis DiffD1 Diff_empty Diff_subset PiE Pi_I contf continuous_on_subset fim that) next case False have"S ⊆ U" using clo closedin_limpt by blast thenhave"(U - S) ∩ K ≠ {}" by (metis Diff_triv False Int_Diff K disjnt_def inf.absorb_iff2 inf_commute) thenhave"∪(components (U - S)) ∩ K ≠ {}" using Union_components by simp thenobtain C0 where C0: "C0 ∈ components (U - S)""C0 ∩ K ≠ {}" by blast have"convex U" by (simp add: affine_imp_convex ‹affine U›) thenhave"locally connected U" by (rule convex_imp_locally_connected) have"∃a g. a ∈ C ∧ a ∈ L ∧ continuous_on (S ∪ (C - {a})) g ∧ g ` (S ∪ (C - {a})) ⊆ T ∧ (∀x ∈ S. g x = f x)" if C: "C ∈ components (U - S)"and CK: "C ∩ K ≠ {}"for C proof - have"C ⊆ U-S""C ∩ L ≠ {}" by (simp_all add: in_components_subset comps that) thenobtain a where a: "a ∈ C""a ∈ L"by auto have opeUC: "openin (top_of_set U) C" by (metis C ‹locally connected U› clo closedin_def locally_connected_open_component topspace_euclidean_subtopology) thenobtain d where"C ⊆ U""0 < d"and d: "cball a d ∩ U ⊆ C" using openin_contains_cball by (metis ‹a ∈ C›) thenhave"ball a d ∩ U ⊆ C" by auto obtain h k where homhk: "homeomorphism (S ∪ C) (S ∪ C) h k" and subC: "{x. (¬ (h x = x ∧ k x = x))} ⊆ C" and bou: "bounded {x. (¬ (h x = x ∧ k x = x))}" and hin: "∧x. x ∈ C ∩ K ==> h x ∈ ball a d ∩ U" proof (rule homeomorphism_grouping_points_exists_gen [of C "ball a d ∩ U""C ∩ K""S ∪C"]) show"openin (top_of_set C) (ball a d ∩ U)" by (metis open_ball ‹C ⊆ U›‹ball a d ∩ U ⊆ C› inf.absorb_iff2 inf.orderE inf_assoc open_openin openin_subtopology) show"openin (top_of_set (affine hull C)) C" by (metis ‹a ∈ C›‹openin (top_of_set U) C› affine_hull_eq affine_hull_openin all_not_in_conv ‹affine U›) show"ball a d ∩ U ≠ {}" using‹0 🚫›‹C ⊆ U›‹a ∈ C›by force show"finite (C ∩ K)" by (simp add: ‹finite K›) show"S ∪ C ⊆ affine hull C" by (metis ‹S ⊆ U›‹a ∈ C› affine_hull_eq affine_hull_openin assms(2) empty_iff hull_subset le_sup_iff opeUC) show"connected C" by (metis C in_components_connected) qed auto have a_BU: "a ∈ ball a d ∩ U" using‹0 🚫›‹C ⊆ U›‹a ∈ C›by auto have"rel_frontier (cball a d ∩ U) retract_of (affine hull (cball a d ∩ U) - {a})" proof (rule rel_frontier_retract_of_punctured_affine_hull) show"bounded (cball a d ∩ U)""convex (cball a d ∩ U)" by (auto simp: ‹convex U› convex_Int) show"a ∈ rel_interior (cball a d ∩ U)" by (metis ‹affine U› convex_cball empty_iff interior_cball a_BU rel_interior_convex_Int_affine) qed moreoverhave"rel_frontier (cball a d ∩ U) = frontier (cball a d) ∩ U" by (metis a_BU ‹affine U› convex_affine_rel_frontier_Int convex_cball equals0D interior_cball) moreoverhave"affine hull (cball a d ∩ U) = U" by (metis ‹convex U› a_BU affine_hull_convex_Int_nonempty_interior affine_hull_eq ‹affine U› equals0D inf.commute interior_cball) ultimatelyhave"frontier (cball a d) ∩ U retract_of (U - {a})" by metis thenobtain r where contr: "continuous_on (U - {a}) r" and rim: "r ∈ (U - {a}) → sphere a d""r ∈ (U - {a}) → U" and req: "∧x. x ∈ sphere a d ∩ U ==> r x = x" using‹affine U›by (force simp: retract_of_def retraction_def hull_same)
define j where"j ≡ λx. if x ∈ ball a d then r x else x" have kj: "∧x. x ∈ S ==> k (j x) = x" using‹C ⊆ U - S›‹S ⊆ U›‹ball a d ∩ U ⊆ C› j_def subC by auto have Uaeq: "U - {a} = (cball a d - {a}) ∩ U ∪ (U - ball a d)" using‹0 🚫›by auto have jim: "j ` (S ∪ (C - {a})) ⊆ (S ∪ C) - ball a d" proof clarify fix y assume"y ∈ S ∪ (C - {a})" thenhave"y ∈ U - {a}" using‹C ⊆ U - S›‹S ⊆ U›‹a ∈ C›by auto thenhave"r y ∈ sphere a d" using rim by auto thenshow"j y ∈ S ∪ C - ball a d" unfolding j_def using‹y ∈ S ∪ (C - {a})›‹y ∈ U - {a}› d rim(2) by auto qed have contj: "continuous_on (U - {a}) j" unfolding j_def Uaeq proof (intro continuous_on_cases_local continuous_on_id, simp_all add: req closedin_closed Uaeq [symmetric]) show"∃T. closed T ∧ (cball a d - {a}) ∩ U = (U - {a}) ∩ T" using affine_closed ‹affine U›by (rule_tac x="(cball a d) ∩ U"in exI) blast show"∃T. closed T ∧ U - ball a d = (U - {a}) ∩ T" using‹0 🚫›‹affine U› by (rule_tac x="U - ball a d"in exI) (force simp: affine_closed) show"continuous_on ((cball a d - {a}) ∩ U) r" by (force intro: continuous_on_subset [OF contr]) qed have fT: "x ∈ U - K ==> f x ∈ T"for x using fim by blast show ?thesis proof (intro conjI exI) show"continuous_on (S ∪ (C - {a})) (f ∘ k ∘ j)" proof (intro continuous_on_compose) have"S ∪ (C - {a}) ⊆ U - {a}" using‹C ⊆ U - S›‹S ⊆ U›‹a ∈ C›by force thenshow"continuous_on (S ∪ (C - {a})) j" by (rule continuous_on_subset [OF contj]) have"j ` (S ∪ (C - {a})) ⊆ S ∪ C" using jim ‹C ⊆ U - S›‹S ⊆ U›‹ball a d ∩ U ⊆ C› j_def by blast thenshow"continuous_on (j ` (S ∪ (C - {a}))) k" by (rule continuous_on_subset [OF homeomorphism_cont2 [OF homhk]]) show"continuous_on (k ` j ` (S ∪ (C - {a}))) f" proof (clarify intro!: continuous_on_subset [OF contf]) fix y assume"y ∈ S ∪ (C - {a})" have ky: "k y ∈ S ∪ C" using homeomorphism_image2 [OF homhk] ‹y ∈ S ∪ (C - {a})›by blast have jy: "j y ∈ S ∪ C - ball a d" using Un_iff ‹y ∈ S ∪ (C - {a})› jim by auto have"k (j y) ∈ U" using‹C ⊆ U›‹S ⊆ U› homeomorphism_image2 [OF homhk] jy by blast moreoverhave"k (j y) ∉ K" using K unfolding disjnt_iff by (metis DiffE Int_iff Un_iff hin homeomorphism_def homhk image_eqI jy) ultimatelyshow"k (j y) ∈ U - K" by blast qed qed have ST: "∧x. x ∈ S ==> (f ∘ k ∘ j) x ∈ T" proof (simp add: kj) show"∧x. x ∈ S ==> f x ∈ T" using K ‹S ⊆ U› fT unfolding disjnt_iff by auto qed moreoverhave"(f ∘ k ∘ j) x ∈ T"if"x ∈ C""x ≠ a""x ∉ S"for x proof - have rx: "r x ∈ sphere a d" using‹C ⊆ U› rim that by fastforce have jj: "j x ∈ S ∪ C - ball a d" using jim that by blast have"k (j x) = j x ⟶ k (j x) ∈ C ∨ j x ∈ C" by (metis Diff_iff Int_iff Un_iff ‹S ⊆ U› subsetD d j_def jj rx sphere_cball that(1)) thenhave kj: "k (j x) ∈ C" using homeomorphism_apply2 [OF homhk, of "j x"] ‹C ⊆ U›‹S ⊆ U› a rx by (metis (mono_tags, lifting) Diff_iff subsetD jj mem_Collect_eq subC) thenshow ?thesis by (metis DiffE DiffI IntD1 IntI ‹C ⊆ U› comp_apply fT hin homeomorphism_apply2 homhk jj kj subset_eq) qed ultimatelyshow"(f ∘ k ∘ j) ` (S ∪ (C - {a})) ⊆ T" by force show"∀x∈S. (f ∘ k ∘ j) x = f x"using kj by simp qed (auto simp: a) qed thenobtain a h where
ah: "∧C. [C ∈ components (U - S); C ∩ K ≠ {}] ==> a C ∈ C ∧ a C ∈ L ∧ continuous_on (S ∪ (C - {a C})) (h C) ∧ h C ` (S ∪ (C - {a C})) ⊆ T ∧ (∀x ∈ S. h C x = f x)" using that by metis
define F where"F ≡ {C ∈ components (U - S). C ∩ K ≠ {}}"
define G where"G ≡ {C ∈ components (U - S). C ∩ K = {}}"
define UF where"UF ≡ (∪C∈F. C - {a C})" have"C0 ∈ F" by (auto simp: F_def C0) have"finite F" proof (subst finite_image_iff [of "λC. C ∩ K" F, symmetric]) show"inj_on (λC. C ∩ K) F" unfolding F_def inj_on_def using components_nonoverlap by blast show"finite ((λC. C ∩ K) ` F)" unfolding F_def by (rule finite_subset [of _ "Pow K"]) (auto simp: ‹finite K›) qed obtain g where contg: "continuous_on (S ∪ UF) g" and gh: "∧x i. [i ∈ F; x ∈ (S ∪ UF) ∩ (S ∪ (i - {a i}))] ==> g x = h i x" proof (rule pasting_lemma_exists_closed [OF ‹finite F›]) let ?X = "top_of_set (S ∪ UF)" show"topspace ?X ⊆ (∪C∈F. S ∪ (C - {a C}))" using‹C0 ∈ F›by (force simp: UF_def) show"closedin (top_of_set (S ∪ UF)) (S ∪ (C - {a C}))" if"C ∈ F"for C proof (rule closedin_closed_subset [of U "S ∪ C"]) have"C ∈ components (U - S)" using F_def that by blast thenshow"closedin (top_of_set U) (S ∪ C)" by (rule closedin_Un_complement_component [OF ‹locally connected U› clo]) next have"x = a C'"if"C' ∈ F""x ∈ C'""x ∉ U"for x C' proof - have"∀A. x ∈∪A ∨ C' ∉ A" using‹x ∈ C'›by blast with that show"x = a C'" by (metis (lifting) DiffD1 F_def Union_components mem_Collect_eq) qed thenshow"S ∪ UF ⊆ U" using‹S ⊆ U›by (force simp: UF_def) next show"S ∪ (C - {a C}) = (S ∪ C) ∩ (S ∪ UF)" using F_def UF_def components_nonoverlap that by auto qed show"continuous_map (subtopology ?X (S ∪ (C' - {a C'}))) euclidean (h C')"if"C' ∈ F"for C' proof - have C': "C' ∈ components (U - S)""C' ∩ K ≠ {}" using F_def that by blast+ show ?thesis using ah [OF C'] by (auto simp: F_def subtopology_subtopology intro: continuous_on_subset) qed show"∧i j x. [i ∈ F; j ∈ F; x ∈ topspace ?X ∩ (S ∪ (i - {a i})) ∩ (S ∪ (j - {a j}))] ==> h i x = h j x" using components_eq by (fastforce simp: components_eq F_def ah) qed auto have SU': "S ∪∪G ∪ (S ∪ UF) ⊆ U" using‹S ⊆ U› in_components_subset by (auto simp: F_def G_def UF_def) have clo1: "closedin (top_of_set (S ∪∪G ∪ (S ∪ UF))) (S ∪∪G)" proof (rule closedin_closed_subset [OF _ SU']) have *: "∧C. C ∈ F ==> openin (top_of_set U) C" unfolding F_def by (metis (no_types, lifting) ‹locally connected U› clo closedin_def locally_connected_open_component mem_Collect_eq topspace_euclidean_subtopology) show"closedin (top_of_set U) (U - UF)" unfolding UF_def by (force intro: openin_delete *) have"(∪x∈F. x - {a x}) ∩ S = {}""∪ G ⊆ U" using in_components_subset by (auto simp: F_def G_def) moreoverhave"∪ G ∩ UF = {}" using components_nonoverlap by (fastforce simp: F_def G_def UF_def) ultimatelyshow"S ∪∪G = (U - UF) ∩ (S ∪∪G ∪ (S ∪ UF))" using UF_def ‹S ⊆ U›by auto qed have clo2: "closedin (top_of_set (S ∪∪G ∪ (S ∪ UF))) (S ∪ UF)" proof (rule closedin_closed_subset [OF _ SU']) show"closedin (top_of_set U) (∪C∈F. S ∪ C)" proof (rule closedin_Union) show"∧T. T ∈ (∪) S ` F ==> closedin (top_of_set U) T" using F_def ‹locally connected U› clo closedin_Un_complement_component by blast qed (simp add: ‹finite F›) show"S ∪ UF = (∪C∈F. S ∪ C) ∩ (S ∪∪G ∪ (S ∪ UF))" proof show"∪ ((∪) S ` F) ∩ (S ∪∪ G ∪ (S ∪ UF)) ⊆ S ∪ UF" using components_eq [of _ "U-S"] by (auto simp add: F_def G_def UF_def disjoint_iff_not_equal) qed (use UF_def ‹C0 ∈ F›in blast) qed have SUG: "S ∪∪G ⊆ U - K" using‹S ⊆ U› K in_components_subset[of _ "U-S"] by (force simp: G_def disjnt_iff) thenhave contf': "continuous_on (S ∪∪G) f" by (rule continuous_on_subset [OF contf]) have contg': "continuous_on (S ∪ UF) g" by (simp add: contg) have"∧x. [S ⊆ U; x ∈ S]==> f x = g x" by (subst gh) (auto simp: ah C0 intro: ‹C0 ∈ F›) thenhave f_eq_g: "∧x. x ∈ S ∪ UF ∧ x ∈ S ∪∪G ==> f x = g x" using‹S ⊆ U› components_eq [of _ "U-S"] by (fastforce simp add: F_def G_def UF_def) have cont: "continuous_on (S ∪∪G ∪ (S ∪ UF)) (λx. if x ∈ S ∪∪G then f x else g x)" by (blast intro: continuous_on_cases_local [OF clo1 clo2 contf' contg' f_eq_g, of "λx. x ∈ S∪∪G"]) show ?thesis proof have UF: "∪F - L ⊆ UF" unfolding F_def UF_def using ah by blast have"U - S - L = ∪(components (U - S)) - L" by simp alsohave"... = ∪F ∪∪G - L" unfolding F_def G_def by blast alsohave"... ⊆ UF ∪∪G" using UF by blast finallyhave"U - L ⊆ S ∪∪G ∪ (S ∪ UF)" by blast thenshow"continuous_on (U - L) (λx. if x ∈ S ∪∪G then f x else g x)" by (rule continuous_on_subset [OF cont]) have"((U - L) ∩ {x. x ∉ S ∧ (∀xa∈G. x ∉ xa)}) ⊆ ((U - L) ∩ (-S ∩ UF))" using‹U - L ⊆ S ∪∪G ∪ (S ∪ UF)›by auto moreoverhave"g ` ((U - L) ∩ (-S ∩ UF)) ⊆ T" proof - have"g x ∈ T"if"x ∈ U""x ∉ L""x ∉ S""C ∈ F""x ∈ C""x ≠ a C"for x C proof (subst gh) show"x ∈ (S ∪ UF) ∩ (S ∪ (C - {a C}))" using that by (auto simp: UF_def) show"h C x ∈ T" using ah that by (fastforce simp add: F_def) qed (rule that) thenshow ?thesis by (force simp: UF_def) qed ultimatelyhave"g ` ((U - L) ∩ {x. x ∉ S ∧ (∀xa∈G. x ∉ xa)}) ⊆ T" using image_mono order_trans by blast moreoverhave"f ` ((U - L) ∩ (S ∪∪G)) ⊆ T" using fim SUG by blast ultimatelyshow"(λx. if x ∈ S ∪∪G then f x else g x) ∈ (U - L) → T" by force show"∧x. x ∈ S ==> (if x ∈ S ∪∪G then f x else g x) = f x" by (simp add: F_def G_def) qed qed
lemma extend_map_affine_to_sphere2: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes"compact S""convex U""bounded U""affine T""S ⊆ T" and affTU: "aff_dim T ≤ aff_dim U" and contf: "continuous_on S f" and fim: "f ∈ S → rel_frontier U" and ovlap: "∧C. C ∈ components(T - S) ==> C ∩ L ≠ {}" obtains K g where"finite K""K ⊆ L""K ⊆ T""disjnt K S" "continuous_on (T - K) g""g ∈ (T - K) → rel_frontier U" "∧x. x ∈ S ==> g x = f x" proof - obtain K g where K: "finite K""K ⊆ T""disjnt K S" and contg: "continuous_on (T - K) g" and gim: "g ∈ (T - K) → rel_frontier U" and gf: "∧x. x ∈ S ==> g x = f x" using assms extend_map_affine_to_sphere_cofinite_simple by metis have"∃y C. C ∈ components (T - S) ∧ x ∈ C ∧ y ∈ C ∧ y ∈ L"if"x ∈ K"for x proof - have"x ∈ T-S" using‹K ⊆ T›‹disjnt K S› disjnt_def that by fastforce thenobtain C where"C ∈ components(T - S)""x ∈ C" by (metis UnionE Union_components) with ovlap [of C] show ?thesis by blast qed thenobtain ξ where ξ: "∧x. x ∈ K ==>∃C. C ∈ components (T - S) ∧ x ∈ C ∧ ξ x ∈ C ∧ ξ x ∈ L" by metis obtain h where conth: "continuous_on (T - ξ ` K) h" and him: "h ∈ (T - ξ ` K) → rel_frontier U" and hg: "∧x. x ∈ S ==> h x = g x" proof (rule extend_map_affine_to_sphere1 [OF ‹finite K›‹affine T› contg gim, of S "ξ ` K"]) show cloTS: "closedin (top_of_set T) S" by (simp add: ‹compact S›‹S ⊆ T› closed_subset compact_imp_closed) show"∧C. [C ∈ components (T - S); C ∩ K ≠ {}]==> C ∩ ξ ` K ≠ {}" using ξ components_eq by blast qed (use K in auto) show ?thesis proof show *: "ξ ` K ⊆ L" using ξ by blast show"finite (ξ ` K)" by (simp add: K) show"ξ ` K ⊆ T" by clarify (meson ξ Diff_iff contra_subsetD in_components_subset) show"continuous_on (T - ξ ` K) h" by (rule conth) show"disjnt (ξ ` K) S" using K ξ in_components_subset by (fastforce simp: disjnt_def) qed (simp_all add: him hg gf) qed
proposition extend_map_affine_to_sphere_cofinite_gen: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes SUT: "compact S""convex U""bounded U""affine T""S ⊆ T" and aff: "aff_dim T ≤ aff_dim U" and contf: "continuous_on S f" and fim: "f ∈ S → rel_frontier U" and dis: "∧C. [C ∈ components(T - S); bounded C]==> C ∩ L ≠ {}" obtains K g where"finite K""K ⊆ L""K ⊆ T""disjnt K S""continuous_on (T - K) g" "g ∈ (T - K) → rel_frontier U" "∧x. x ∈ S ==> g x = f x" proof (cases "S = {}") case True show ?thesis proof (cases "rel_frontier U = {}") case True with aff have"aff_dim T ≤ 0" using affine_bounded_eq_lowdim ‹bounded U› order_trans by (auto simp add: rel_frontier_eq_empty) with aff_dim_geq [of T] consider "aff_dim T = -1" | "aff_dim T = 0" by linarith thenshow ?thesis proof cases assume"aff_dim T = -1" thenhave"T = {}" by (simp add: aff_dim_empty) thenshow ?thesis by (rule_tac K="{}"in that) auto next assume"aff_dim T = 0" thenobtain a where"T = {a}" using aff_dim_eq_0 by blast thenhave"a ∈ L" using dis [of "{a}"] ‹S = {}›by (auto simp: in_components_self) with‹S = {}›‹T = {a}›show ?thesis by (rule_tac K="{a}"and g=f in that) auto qed next case False thenobtain y where"y ∈ rel_frontier U" by auto with‹S = {}›show ?thesis by (rule_tac K="{}"and g="λx. y"in that) (auto) qed next case False have"bounded S" by (simp add: assms compact_imp_bounded) thenobtain b where b: "S ⊆ cbox (-b) b" using bounded_subset_cbox_symmetric by blast
define LU where"LU ≡ L ∪ (∪ {C ∈ components (T - S). ¬bounded C} - cbox (-(b+One)) (b+One))" obtain K g where"finite K""K ⊆ LU""K ⊆ T""disjnt K S" and contg: "continuous_on (T - K) g" and gim: "g ∈ (T - K) → rel_frontier U" and gf: "∧x. x ∈ S ==> g x = f x" proof (rule extend_map_affine_to_sphere2 [OF SUT aff contf fim]) show"C ∩ LU ≠ {}"if"C ∈ components (T - S)"for C proof (cases "bounded C") case True with dis that show ?thesis unfolding LU_def by fastforce next case False thenhave"¬ bounded (∪{C ∈ components (T - S). ¬ bounded C})" by (metis (no_types, lifting) Sup_upper bounded_subset mem_Collect_eq that) thenshow ?thesis by (simp add: LU_def disjoint_iff) (meson False bounded_cbox bounded_subset subset_iff that) qed qed blast have *: False if"x ∈ cbox (- b - m *🪙R One) (b + m *🪙R One)" "x ∉ box (- b - n *🪙R One) (b + n *🪙R One)" "0 ≤ m""m < n""n ≤ 1"for m n x using that by (auto simp: mem_box algebra_simps) have"disjoint_family_on (λd. frontier (cbox (- b - d *🪙R One) (b + d *🪙R One))) {1 / 2..1}" by (auto simp: disjoint_family_on_def neq_iff frontier_def dest: *) thenobtain d where d12: "1/2 ≤ d""d ≤ 1" and ddis: "disjnt K (frontier (cbox (-(b + d *🪙R One)) (b + d *🪙R One)))" using disjoint_family_elem_disjnt [of "{1/2..1::real}" K "λd. frontier (cbox (-(b + d *🪙R One)) (b + d *🪙R One))"] by (auto simp: ‹finite K›)
define c where"c ≡ b + d *🪙R One" have cbsub: "cbox (-b) b ⊆ box (-c) c" "cbox (-b) b ⊆ cbox (-c) c" "cbox (-c) c ⊆ cbox (-(b+One)) (b+One)" using d12 by (simp_all add: subset_box c_def inner_diff_left inner_left_distrib) have clo_cT: "closed (cbox (- c) c ∩ T)" using affine_closed ‹affine T›by blast have cT_ne: "cbox (- c) c ∩ T ≠ {}" using‹S ≠ {}›‹S ⊆ T› b cbsub by fastforce have S_sub_cc: "S ⊆ cbox (- c) c" using‹cbox (- b) b ⊆ cbox (- c) c› b by auto show ?thesis proof show"finite (K ∩ cbox (-(b+One)) (b+One))" using‹finite K›by blast show"K ∩ cbox (- (b + One)) (b + One) ⊆ L" using‹K ⊆ LU›by (auto simp: LU_def) show"K ∩ cbox (- (b + One)) (b + One) ⊆ T" using‹K ⊆ T›by auto show"disjnt (K ∩ cbox (- (b + One)) (b + One)) S" using‹disjnt K S›by (simp add: disjnt_def disjoint_eq_subset_Compl inf.coboundedI1) have cloTK: "closest_point (cbox (- c) c ∩ T) x ∈ T - K" if"x ∈ T"and Knot: "x ∈ K ⟶ x ∉ cbox (- b - One) (b + One)"for x proof (cases "x ∈ cbox (- c) c") case True with‹x ∈ T›show ?thesis using cbsub(3) Knot by (force simp: closest_point_self) next case False have clo_in_rf: "closest_point (cbox (- c) c ∩ T) x ∈ rel_frontier (cbox (- c) c ∩ T)" proof (intro closest_point_in_rel_frontier [OF clo_cT cT_ne] DiffI notI) have"T ∩ interior (cbox (- c) c) ≠ {}" using‹S ≠ {}›‹S ⊆ T› b cbsub(1) by fastforce thenshow"x ∈ affine hull (cbox (- c) c ∩ T)" by (simp add: Int_commute affine_hull_affine_Int_nonempty_interior ‹affine T› hull_inc that(1)) next show"False"if"x ∈ rel_interior (cbox (- c) c ∩ T)" proof - have"interior (cbox (- c) c) ∩ T ≠ {}" using‹S ≠ {}›‹S ⊆ T› b cbsub(1) by fastforce thenhave"affine hull (T ∩ cbox (- c) c) = T" using affine_hull_convex_Int_nonempty_interior [of T "cbox (- c) c"] by (simp add: affine_imp_convex ‹affine T› inf_commute) thenshow ?thesis by (meson subsetD le_inf_iff rel_interior_subset that False) qed qed have"closest_point (cbox (- c) c ∩ T) x ∉ K" proof assume inK: "closest_point (cbox (- c) c ∩ T) x ∈ K" have"∧x. x ∈ K ==> x ∉ frontier (cbox (- (b + d *🪙R One)) (b + d *🪙R One))" by (metis ddis disjnt_iff) thenshow False by (metis DiffI Int_iff ‹affine T› cT_ne c_def clo_cT clo_in_rf closest_point_in_set
convex_affine_rel_frontier_Int convex_box(1) empty_iff frontier_cbox inK interior_cbox) qed thenshow ?thesis using cT_ne clo_cT closest_point_in_set by blast qed have"convex (cbox (- c) c ∩ T)" by (simp add: affine_imp_convex assms(4) convex_Int) thenshow"continuous_on (T - K ∩ cbox (- (b + One)) (b + One)) (g ∘ closest_point (cbox (-c) c ∩ T))" using cloTK clo_cT cT_ne by (intro continuous_on_compose continuous_on_closest_point continuous_on_subset [OF contg]; force) have"g (closest_point (cbox (- c) c ∩ T) x) ∈ rel_frontier U" if"x ∈ T""x ∈ K ⟶ x ∉ cbox (- b - One) (b + One)"for x using cloTK gim that by auto thenshow"(g ∘ closest_point (cbox (- c) c ∩ T)) ∈ (T - K ∩ cbox (- (b + One)) (b + One)) → rel_frontier U" by force show"∧x. x ∈ S ==> (g ∘ closest_point (cbox (- c) c ∩ T)) x = f x" by simp (metis (mono_tags, lifting) IntI ‹S ⊆ T› cT_ne clo_cT closest_point_refl gf subsetD S_sub_cc) qed qed
corollary extend_map_affine_to_sphere_cofinite: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes SUT: "compact S""affine T""S ⊆ T" and aff: "aff_dim T ≤ DIM('b)"and"0 ≤ r" and contf: "continuous_on S f" and fim: "f ∈ S → sphere a r" and dis: "∧C. [C ∈ components(T - S); bounded C]==> C ∩ L ≠ {}" obtains K g where"finite K""K ⊆ L""K ⊆ T""disjnt K S""continuous_on (T - K) g" "g ∈ (T - K) → sphere a r""∧x. x ∈ S ==> g x = f x" proof (cases "r = 0") case True with fim show ?thesis by (rule_tac K="{}"and g = "λx. a"in that) (auto) next case False show thesis proof (rule extend_map_affine_to_sphere_cofinite_gen
[OF ‹compact S› convex_cball bounded_cball ‹affine T›‹S ⊆ T› _ contf]) have"0 < r" using assms False by auto thenshow"aff_dim T ≤ aff_dim (cball a r)" by (simp add: aff aff_dim_cball) show"f ∈ S → rel_frontier (cball a r)" by (simp add: False fim) qed (use dis False that in auto) qed
corollary extend_map_UNIV_to_sphere_cofinite: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes"DIM('a) ≤ DIM('b)"and"0 ≤ r" and"compact S" and"continuous_on S f" and"f ∈ S → sphere a r" and"∧C. [C ∈ components(- S); bounded C]==> C ∩ L ≠ {}" obtains K g where"finite K""K ⊆ L""disjnt K S""continuous_on (- K) g" "g ∈ (- K) → sphere a r""∧x. x ∈ S ==> g x = f x" using assms extend_map_affine_to_sphere_cofinite [OF ‹compact S› affine_UNIV subset_UNIV] by (metis Compl_eq_Diff_UNIV aff_dim_UNIV of_nat_le_iff)
corollary extend_map_UNIV_to_sphere_no_bounded_component: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes aff: "DIM('a) ≤ DIM('b)"and"0 ≤ r" and SUT: "compact S" and contf: "continuous_on S f" and fim: "f ∈ S → sphere a r" and dis: "∧C. C ∈ components(- S) ==>¬ bounded C" obtains g where"continuous_on UNIV g""g ∈ UNIV → sphere a r""∧x. x ∈ S ==> g x = f x" using extend_map_UNIV_to_sphere_cofinite [OF aff ‹0 ≤ r›‹compact S› contf fim, of "{}"] by (metis Compl_empty_eq dis subset_empty)
theorem Borsuk_separation_theorem_gen: fixes S :: "'a::euclidean_space set" assumes"compact S" shows"(∀c ∈ components(- S). ¬bounded c) ⟷ (∀f. continuous_on S f ∧ f ∈ S → sphere (0::'a) 1 ⟶ (∃c. homotopic_with_canon (λx. True) S (sphere 0 1) f (λx. c)))"
(is"?lhs = ?rhs") proof assume L [rule_format]: ?lhs show ?rhs proof clarify fix f :: "'a ==> 'a" assume contf: "continuous_on S f"and fim: "f ∈ S → sphere 0 1" obtain g where contg: "continuous_on UNIV g"and gim: "g ∈ UNIV → sphere 0 1" and gf: "∧x. x ∈ S ==> g x = f x" by (rule extend_map_UNIV_to_sphere_no_bounded_component [OF _ _ ‹compact S› contf fim L]) auto thenobtain c where c: "homotopic_with_canon (λh. True) UNIV (sphere 0 1) g (λx. c)" by (metis contractible_UNIV nullhomotopic_from_contractible) thenshow"∃c. homotopic_with_canon (λx. True) S (sphere 0 1) f (λx. c)" by (metis assms compact_imp_closed contf contg contractible_empty fim gf gim nullhomotopic_from_contractible nullhomotopic_into_sphere_extension image_subset_iff_funcset) qed next assume R [rule_format]: ?rhs show ?lhs unfolding components_def proof clarify fix a assume"a ∉ S"and a: "bounded (connected_component_set (- S) a)" have"∀x∈S. norm (x - a) ≠ 0" using‹a ∉ S›by auto thenhave cont: "continuous_on S (λx. inverse(norm(x - a)) *🪙R (x - a))" by (intro continuous_intros) have im: "(λx. inverse(norm(x - a)) *🪙R (x - a)) ` S ⊆ sphere 0 1" by clarsimp (metis ‹a ∉ S› eq_iff_diff_eq_0 left_inverse norm_eq_zero) show False using R cont im Borsuk_map_essential_bounded_component [OF ‹compact S›‹a ∉ S›] a by blast qed qed
corollary Borsuk_separation_theorem: fixes S :: "'a::euclidean_space set" assumes"compact S"and 2: "2 ≤ DIM('a)" shows"connected(- S) ⟷ (∀f. continuous_on S f ∧ f ∈ S → sphere (0::'a) 1 ⟶ (∃c. homotopic_with_canon (λx. True) S (sphere 0 1) f (λx. c)))"
(is"?lhs = ?rhs") proof assume L: ?lhs show ?rhs proof (cases "S = {}") case True thenshow ?thesis using homotopic_with_canon_on_empty by blast next case False thenhave"(∀c∈components (- S). ¬ bounded c)" by (metis L assms(1) bounded_empty cobounded_imp_unbounded compact_imp_bounded in_components_maximal order_refl) thenshow ?thesis by (simp add: Borsuk_separation_theorem_gen [OF ‹compact S›]) qed next assume R: ?rhs thenhave"∀c∈components (- S). ¬ bounded c ==> connected (- S)" by (metis "2" assms(1) cobounded_has_bounded_component compact_imp_bounded double_complement) with R show ?lhs by (simp add: Borsuk_separation_theorem_gen [OF ‹compact S›]) qed
lemma homotopy_eqv_separation: fixes S :: "'a::euclidean_space set"and T :: "'a set" assumes"S homotopy_eqv T"and"compact S"and"compact T" shows"connected(- S) ⟷ connected(- T)" proof -
consider "DIM('a) = 1" | "2 ≤ DIM('a)" by (metis DIM_ge_Suc0 One_nat_def Suc_1 dual_order.antisym not_less_eq_eq) thenshow ?thesis proof cases case 1 thenshow ?thesis using bounded_connected_Compl_1 compact_imp_bounded homotopy_eqv_empty1 homotopy_eqv_empty2 assms by metis next case 2 with assms show ?thesis by (simp add: Borsuk_separation_theorem homotopy_eqv_cohomotopic_triviality_null) qed qed
proposition Jordan_Brouwer_separation: fixes S :: "'a::euclidean_space set"and a::'a assumes hom: "S homeomorphic sphere a r"and"0 < r" shows"¬ connected(- S)" proof - have"- sphere a r ∩ ball a r ≠ {}" using‹0 🚫›by (simp add: Int_absorb1 subset_eq) moreover have eq: "- sphere a r - ball a r = - cball a r" by auto have"- cball a r ≠ {}" proof - have"frontier (cball a r) ≠ {}" using‹0 🚫›by auto thenshow ?thesis by (metis frontier_complement frontier_empty) qed with eq have"- sphere a r - ball a r ≠ {}" by auto moreover have"connected (- S) = connected (- sphere a r)" by (meson hom compact_sphere homeomorphic_compactness homeomorphic_imp_homotopy_eqv homotopy_eqv_separation) ultimatelyshow ?thesis using connected_Int_frontier [of "- sphere a r""ball a r"] by (auto simp: ‹0 🚫›) qed
proposition Jordan_Brouwer_frontier: fixes S :: "'a::euclidean_space set"and a::'a assumes S: "S homeomorphic sphere a r"and T: "T ∈ components(- S)"and 2: "2 ≤ DIM('a)" shows"frontier T = S" proof (cases r rule: linorder_cases) assume"r < 0" with S T show ?thesis by auto next assume"r = 0" with S T card_eq_SucD obtain b where"S = {b}" by (auto simp: homeomorphic_finite [of "{a}" S]) have"components (- {b}) = { -{b}}" using T ‹S = {b}›by (auto simp: components_eq_sing_iff connected_punctured_universe 2) with T show ?thesis by (metis ‹S = {b}› cball_trivial frontier_cball frontier_complement singletonD sphere_trivial) next assume"r > 0" have"compact S" using homeomorphic_compactness compact_sphere S by blast show ?thesis proof (rule frontier_minimal_separating_closed) show"closed S" using‹compact S› compact_eq_bounded_closed by blast show"¬ connected (- S)" using Jordan_Brouwer_separation S ‹0 🚫›by blast obtain f g where hom: "homeomorphism S (sphere a r) f g" using S by (auto simp: homeomorphic_def) show"connected (- T)"if"closed T""T ⊂ S"for T proof - have"f ∈ T → sphere a r" using‹T ⊂ S› hom homeomorphism_image1 by blast moreoverhave"f ` T ≠ sphere a r" using‹T ⊂ S› hom by (metis homeomorphism_image2 homeomorphism_of_subsets order_refl psubsetE) ultimatelyhave"f ` T ⊂ sphere a r"by blast thenhave"connected (- f ` T)" by (rule psubset_sphere_Compl_connected [OF _ ‹0 🚫› 2]) moreoverhave"compact T" using‹compact S› bounded_subset compact_eq_bounded_closed that by blast moreoverthenhave"compact (f ` T)" by (meson compact_continuous_image continuous_on_subset hom homeomorphism_def psubsetE ‹T ⊂ S›) moreoverhave"T homotopy_eqv f ` T" by (meson hom homeomorphic_def homeomorphic_imp_homotopy_eqv homeomorphism_of_subsets order.refl psubsetE that(2)) ultimatelyshow ?thesis using homotopy_eqv_separation [of T "f`T"] by blast qed qed (rule T) qed
proposition Jordan_Brouwer_nonseparation: fixes S :: "'a::euclidean_space set"and a::'a assumes S: "S homeomorphic sphere a r"and"T ⊂ S"and 2: "2 ≤ DIM('a)" shows"connected(- T)" proof - have *: "connected(C ∪ (S - T))"if"C ∈ components(- S)"for C proof (rule connected_intermediate_closure) show"connected C" using in_components_connected that by auto have"S = frontier C" using"2" Jordan_Brouwer_frontier S that by blast with closure_subset show"C ∪ (S - T) ⊆ closure C" by (auto simp: frontier_def) qed auto have"components(- S) ≠ {}" by (metis S bounded_empty cobounded_imp_unbounded compact_eq_bounded_closed compact_sphere
components_eq_empty homeomorphic_compactness) thenhave"- T = (∪C ∈ components(- S). C ∪ (S - T))" using Union_components [of "-S"] ‹T ⊂ S›by auto moreoverhave"connected ..." using‹T ⊂ S›by (intro connected_Union) (auto simp: *) ultimatelyshow ?thesis by simp qed
subsection‹ Invariance of domain and corollaries›
lemma invariance_of_domain_ball: fixes f :: "'a ==> 'a::euclidean_space" assumes contf: "continuous_on (cball a r) f"and"0 < r" and inj: "inj_on f (cball a r)" shows"open(f ` ball a r)" proof (cases "DIM('a) = 1") case True obtain h::"'a==>real"and k where"linear h""linear k""h ` UNIV = UNIV""k ` UNIV = UNIV" "∧x. norm(h x) = norm x""∧x. norm(k x) = norm x" and kh: "∧x. k(h x) = x"and"∧x. h(k x) = x" proof (rule isomorphisms_UNIV_UNIV) show"DIM('a) = DIM(real)" using True by force qed (metis UNIV_I UNIV_eq_I imageI) have cont: "continuous_on S h""continuous_on T k"for S T by (simp_all add: ‹linear h›‹linear k› linear_continuous_on linear_linear) have"continuous_on (h ` cball a r) (h ∘ f ∘ k)" by (intro continuous_on_compose cont continuous_on_subset [OF contf]) (auto simp: kh) moreoverhave"is_interval (h ` cball a r)" by (simp add: is_interval_connected_1 ‹linear h› linear_continuous_on linear_linear connected_continuous_image) moreoverhave"inj_on (h ∘ f ∘ k) (h ` cball a r)" using inj by (simp add: inj_on_def) (metis ‹∧x. k (h x) = x›) ultimatelyhave *: "∧T. [open T; T ⊆ h ` cball a r]==> open ((h ∘ f ∘ k) ` T)" using injective_eq_1d_open_map_UNIV by blast have"open ((h ∘ f ∘ k) ` (h ` ball a r))" by (rule *) (auto simp: ‹linear h›‹range h = UNIV› open_surjective_linear_image) thenhave"open ((h ∘ f) ` ball a r)" by (simp add: image_comp ‹∧x. k (h x) = x› cong: image_cong) thenshow ?thesis unfolding image_comp [symmetric] by (metis open_bijective_linear_image_eq ‹linear h› kh ‹range h = UNIV› bijI inj_on_def) next case False thenhave 2: "DIM('a) ≥ 2" by (metis DIM_ge_Suc0 One_nat_def Suc_1 antisym not_less_eq_eq) have fimsub: "f ` ball a r ⊆ - f ` sphere a r" using inj by clarsimp (metis inj_onD less_eq_real_def mem_cball order_less_irrefl) have hom: "f ` sphere a r homeomorphic sphere a r" by (meson compact_sphere contf continuous_on_subset homeomorphic_compact homeomorphic_sym inj inj_on_subset sphere_cball) thenhave nconn: "¬ connected (- f ` sphere a r)" by (rule Jordan_Brouwer_separation) (auto simp: ‹0 🚫›) have"bounded (f ` sphere a r)" by (meson compact_imp_bounded compact_continuous_image_eq compact_sphere contf inj sphere_cball) thenobtain C where C: "C ∈ components (- f ` sphere a r)"and"bounded C" using cobounded_has_bounded_component [OF _ nconn] "2"by auto moreoverhave"f ` (ball a r) = C" proof have"C ≠ {}" by (rule in_components_nonempty [OF C]) show"C ⊆ f ` ball a r" proof (rule ccontr) assume nonsub: "¬ C ⊆ f ` ball a r" have"- f ` cball a r ⊆ C" proof (rule components_maximal [OF C]) have"f ` cball a r homeomorphic cball a r" using compact_cball contf homeomorphic_compact homeomorphic_sym inj by blast thenshow"connected (- f ` cball a r)" by (auto intro: connected_complement_homeomorphic_convex_compact 2) show"- f ` cball a r ⊆ - f ` sphere a r" by auto thenshow"C ∩ - f ` cball a r ≠ {}" using‹C ≠ {}› in_components_subset [OF C] nonsub using image_iff by fastforce qed thenhave"bounded (- f ` cball a r)" using bounded_subset ‹bounded C›by auto thenhave"¬ bounded (f ` cball a r)" using cobounded_imp_unbounded by blast thenshow"False" using compact_continuous_image [OF contf] compact_cball compact_imp_bounded by blast qed with‹C ≠ {}›have"C ∩ f ` ball a r ≠ {}" by (simp add: inf.absorb_iff1) thenshow"f ` ball a r ⊆ C" by (metis components_maximal [OF C _ fimsub] connected_continuous_image ball_subset_cball connected_ball contf continuous_on_subset) qed moreoverhave"open (- f ` sphere a r)" using hom compact_eq_bounded_closed compact_sphere homeomorphic_compactness by blast ultimatelyshow ?thesis using open_components by blast qed
text‹Proved by L. E. J. Brouwer (1912)› theorem invariance_of_domain: fixes f :: "'a ==> 'a::euclidean_space" assumes"continuous_on S f""open S""inj_on f S" shows"open(f ` S)" unfolding open_subopen [of "f`S"] proof clarify fix a assume"a ∈ S" obtain δ where"δ > 0"and δ: "cball a δ ⊆ S" using‹open S›‹a ∈ S› open_contains_cball_eq by blast show"∃T. open T ∧ f a ∈ T ∧ T ⊆ f ` S" proof (intro exI conjI) show"open (f ` (ball a δ))" by (meson δ ‹0 🚫δ› assms continuous_on_subset inj_on_subset invariance_of_domain_ball) show"f a ∈ f ` ball a δ" by (simp add: ‹0 🚫δ›) show"f ` ball a δ ⊆ f ` S" using δ ball_subset_cball by blast qed qed
lemma inv_of_domain_ss0: fixes f :: "'a ==> 'a::euclidean_space" assumes contf: "continuous_on U f"and injf: "inj_on f U"and fim: "f ∈ U → S" and"subspace S"and dimS: "dim S = DIM('b::euclidean_space)" and ope: "openin (top_of_set S) U" shows"openin (top_of_set S) (f ` U)" proof - have"U ⊆ S" using ope openin_imp_subset by blast have"(UNIV::'b set) homeomorphic S" by (simp add: ‹subspace S› dimS homeomorphic_subspaces) thenobtain h k where homhk: "homeomorphism (UNIV::'b set) S h k" using homeomorphic_def by blast have homkh: "homeomorphism S (k ` S) k h" using homhk homeomorphism_image2 homeomorphism_sym by fastforce have"open ((k ∘ f ∘ h) ` k ` U)" proof (rule invariance_of_domain) show"continuous_on (k ` U) (k ∘ f ∘ h)" proof (intro continuous_intros) show"continuous_on (k ` U) h" by (meson continuous_on_subset [OF homeomorphism_cont1 [OF homhk]] top_greatest) have"h ` k ` U ⊆ U" by (metis ‹U ⊆ S› dual_order.eq_iff homeomorphism_image2 homeomorphism_of_subsets homkh) thenshow"continuous_on (h ` k ` U) f" by (rule continuous_on_subset [OF contf]) have"f ` h ` k ` U ⊆ S" using‹h ` k ` U ⊆ U› fim by blast thenshow"continuous_on (f ` h ` k ` U) k" by (rule continuous_on_subset [OF homeomorphism_cont2 [OF homhk]]) qed have ope_iff: "∧T. open T ⟷ openin (top_of_set (k ` S)) T" using homhk homeomorphism_image2 open_openin by fastforce show"open (k ` U)" by (simp add: ope_iff homeomorphism_imp_open_map [OF homkh ope]) show"inj_on (k ∘ f ∘ h) (k ` U)" unfolding inj_on_def by (smt (verit, ccfv_threshold) PiE ‹U ⊆ S› assms(3) comp_apply homeomorphism_def homhk imageE inj_on_def injf subset_eq) qed moreover have eq: "f ` U = h ` (k ∘ f ∘ h ∘ k) ` U" unfolding image_comp [symmetric] using‹U ⊆ S› fim by (metis homeomorphism_image2 homeomorphism_of_subsets homhk homkh image_subset_iff_funcset top_greatest) ultimatelyshow ?thesis by (metis (no_types, opaque_lifting) homeomorphism_imp_open_map homhk image_comp open_openin subtopology_UNIV) qed
lemma inv_of_domain_ss1: fixes f :: "'a ==> 'a::euclidean_space" assumes contf: "continuous_on U f"and injf: "inj_on f U"and fim: "f ∈ U → S" and"subspace S" and ope: "openin (top_of_set S) U" shows"openin (top_of_set S) (f ` U)" proof -
define S' where"S' ≡ {y. ∀x ∈ S. orthogonal x y}" have"subspace S'" by (simp add: S'_def subspace_orthogonal_to_vectors)
define g where"g ≡ λz::'a*'a. ((f ∘ fst)z, snd z)" have"openin (top_of_set (S × S')) (g ` (U × S'))" proof (rule inv_of_domain_ss0) show"continuous_on (U × S') g" unfolding g_def by (auto intro!: continuous_intros continuous_on_compose2 [OF contf continuous_on_fst]) show"g ∈ (U × S') → S × S'" using fim by (auto simp: g_def) show"inj_on g (U × S')" using injf by (auto simp: g_def inj_on_def) show"subspace (S × S')" by (simp add: ‹subspace S'›‹subspace S› subspace_Times) show"openin (top_of_set (S × S')) (U × S')" by (simp add: openin_Times [OF ope]) have"dim (S × S') = dim S + dim S'" by (simp add: ‹subspace S'›‹subspace S› dim_Times) alsohave"... = DIM('a)" using dim_subspace_orthogonal_to_vectors [OF ‹subspace S› subspace_UNIV] by (simp add: add.commute S'_def) finallyshow"dim (S × S') = DIM('a)" . qed moreoverhave"g ` (U × S') = f ` U × S'" by (auto simp: g_def image_iff) moreoverhave"0 ∈ S'" using‹subspace S'› subspace_affine by blast ultimatelyshow ?thesis by (auto simp: openin_Times_eq) qed
corollary invariance_of_domain_subspaces: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes ope: "openin (top_of_set U) S" and"subspace U""subspace V"and VU: "dim V ≤ dim U" and contf: "continuous_on S f"and fim: "f ∈ S → V" and injf: "inj_on f S" shows"openin (top_of_set V) (f ` S)" proof - obtain V' where"subspace V'""V' ⊆ U""dim V' = dim V" using choose_subspace_of_subspace [OF VU] by (metis span_eq_iff ‹subspace U›) thenhave"V homeomorphic V'" by (simp add: ‹subspace V› homeomorphic_subspaces) thenobtain h k where homhk: "homeomorphism V V' h k" using homeomorphic_def by blast have eq: "f ` S = k ` (h ∘ f) ` S" proof - have"k ` h ` f ` S = f ` S" by (meson equalityD2 fim funcset_image homeomorphism_image2 homeomorphism_of_subsets homhk) thenshow ?thesis by (simp add: image_comp) qed show ?thesis unfolding eq proof (rule homeomorphism_imp_open_map) show homkh: "homeomorphism V' V k h" by (simp add: homeomorphism_symD homhk) have hfV': "(h ∘ f) ` S ⊆ V'" using fim homeomorphism_image1 homhk by fastforce moreoverhave"openin (top_of_set U) ((h ∘ f) ` S)" proof (rule inv_of_domain_ss1) show"continuous_on S (h ∘ f)" by (meson contf continuous_on_compose continuous_on_subset fim funcset_image homeomorphism_cont2 homkh) show"inj_on (h ∘ f) S" by (smt (verit, ccfv_SIG) Pi_iff comp_apply fim homeomorphism_apply2 homkh inj_on_def injf) show"h ∘ f ∈ S → U" using‹V' ⊆ U› hfV' by blast qed (auto simp: assms) ultimatelyshow"openin (top_of_set V') ((h ∘ f) ` S)" using openin_subset_trans ‹V' ⊆ U›by force qed qed
corollary invariance_of_dimension_subspaces: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes ope: "openin (top_of_set U) S" and"subspace U""subspace V" and contf: "continuous_on S f"and fim: "f ∈ S → V" and injf: "inj_on f S"and"S ≠ {}" shows"dim U ≤ dim V" proof - have"False"if"dim V < dim U" proof - obtain T where"subspace T""T ⊆ U""dim T = dim V" using choose_subspace_of_subspace [of "dim V" U] by (metis ‹dim V 🚫 U› assms(2) order.strict_implies_order span_eq_iff) thenhave"V homeomorphic T" by (simp add: ‹subspace V› homeomorphic_subspaces) thenobtain h k where homhk: "homeomorphism V T h k" using homeomorphic_def by blast have"continuous_on S (h ∘ f)" by (meson contf continuous_on_compose continuous_on_subset fim homeomorphism_def homhk image_subset_iff_funcset) moreoverhave"(h ∘ f) ` S ⊆ U" using‹T ⊆ U› fim homeomorphism_image1 homhk by fastforce moreoverhave"inj_on (h ∘ f) S" unfolding inj_on_def by (metis Pi_iff comp_apply fim homeomorphism_def homhk inj_on_def injf) ultimatelyhave ope_hf: "openin (top_of_set U) ((h ∘ f) ` S)" using invariance_of_domain_subspaces [OF ope ‹subspace U›‹subspace U›] by blast have"(h ∘ f) ` S ⊆ T" using fim homeomorphism_image1 homhk by fastforce thenhave"dim ((h ∘ f) ` S) ≤ dim T" by (rule dim_subset) alsohave"dim ((h ∘ f) ` S) = dim U" using‹S ≠ {}›‹subspace U› by (blast intro: dim_openin ope_hf) finallyshow False using‹dim V 🚫 U›‹dim T = dim V›by simp qed thenshow ?thesis using not_less by blast qed
corollary invariance_of_domain_affine_sets: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes ope: "openin (top_of_set U) S" and aff: "affine U""affine V""aff_dim V ≤ aff_dim U" and contf: "continuous_on S f"and fim: "f ∈ S → V" and injf: "inj_on f S" shows"openin (top_of_set V) (f ` S)" proof (cases "S = {}") case True thenshow ?thesis by auto next case False obtain a b where"a ∈ S""a ∈ U""b ∈ V" using False fim ope openin_contains_cball by fastforce have"openin (top_of_set ((+) (- b) ` V)) (((+) (- b) ∘ f ∘ (+) a) ` (+) (- a) ` S)" proof (rule invariance_of_domain_subspaces) show"openin (top_of_set ((+) (- a) ` U)) ((+) (- a) ` S)" by (metis ope homeomorphism_imp_open_map homeomorphism_translation translation_galois) show"subspace ((+) (- a) ` U)" by (simp add: ‹a ∈ U› affine_diffs_subspace_subtract ‹affine U› cong: image_cong_simp) show"subspace ((+) (- b) ` V)" by (simp add: ‹b ∈ V› affine_diffs_subspace_subtract ‹affine V› cong: image_cong_simp) show"dim ((+) (- b) ` V) ≤ dim ((+) (- a) ` U)" by (metis ‹a ∈ U›‹b ∈ V› aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff) show"continuous_on ((+) (- a) ` S) ((+) (- b) ∘ f ∘ (+) a)" by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois) show"(+) (- b) ∘ f ∘ (+) a ∈ (+) (- a) ` S → (+) (- b) ` V" using fim by auto show"inj_on ((+) (- b) ∘ f ∘ (+) a) ((+) (- a) ` S)" by (auto simp: inj_on_def) (meson inj_onD injf) qed thenshow ?thesis by (metis (no_types, lifting) homeomorphism_imp_open_map homeomorphism_translation image_comp translation_galois) qed
corollary invariance_of_dimension_affine_sets: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes ope: "openin (top_of_set U) S" and aff: "affine U""affine V" and contf: "continuous_on S f"and fim: "f ∈ S → V" and injf: "inj_on f S"and"S ≠ {}" shows"aff_dim U ≤ aff_dim V" proof - obtain a b where"a ∈ S""a ∈ U""b ∈ V" using‹S ≠ {}› fim ope openin_contains_cball by fastforce have"dim ((+) (- a) ` U) ≤ dim ((+) (- b) ` V)" proof (rule invariance_of_dimension_subspaces) show"openin (top_of_set ((+) (- a) ` U)) ((+) (- a) ` S)" by (metis ope homeomorphism_imp_open_map homeomorphism_translation translation_galois) show"subspace ((+) (- a) ` U)" by (simp add: ‹a ∈ U› affine_diffs_subspace_subtract ‹affine U› cong: image_cong_simp) show"subspace ((+) (- b) ` V)" by (simp add: ‹b ∈ V› affine_diffs_subspace_subtract ‹affine V› cong: image_cong_simp) show"continuous_on ((+) (- a) ` S) ((+) (- b) ∘ f ∘ (+) a)" by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois) show"(+) (- b) ∘ f ∘ (+) a ∈ (+) (- a) ` S → (+) (- b) ` V" using fim by auto show"inj_on ((+) (- b) ∘ f ∘ (+) a) ((+) (- a) ` S)" by (auto simp: inj_on_def) (meson inj_onD injf) qed (use‹S ≠ {}›in auto) thenshow ?thesis by (metis ‹a ∈ U›‹b ∈ V› aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff) qed
corollary invariance_of_dimension: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes contf: "continuous_on S f"and"open S" and injf: "inj_on f S"and"S ≠ {}" shows"DIM('a) ≤ DIM('b)" using invariance_of_dimension_subspaces [of UNIV S UNIV f] assms by auto
corollary continuous_injective_image_subspace_dim_le: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes"subspace S""subspace T" and contf: "continuous_on S f"and fim: "f ∈ S → T" and injf: "inj_on f S" shows"dim S ≤ dim T" using invariance_of_dimension_subspaces [of S S _ f] assms by (auto simp: subspace_affine)
lemma invariance_of_dimension_convex_domain: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes"convex S" and contf: "continuous_on S f"and fim: "f ∈ S → affine hull T" and injf: "inj_on f S" shows"aff_dim S ≤ aff_dim T" proof (cases "S = {}") case True thenshow ?thesis by (simp add: aff_dim_geq) next case False have"aff_dim (affine hull S) ≤ aff_dim (affine hull T)" proof (rule invariance_of_dimension_affine_sets) show"openin (top_of_set (affine hull S)) (rel_interior S)" by (simp add: openin_rel_interior) show"continuous_on (rel_interior S) f" using contf continuous_on_subset rel_interior_subset by blast show"f ∈ rel_interior S → affine hull T" using fim rel_interior_subset by blast show"inj_on f (rel_interior S)" using inj_on_subset injf rel_interior_subset by blast show"rel_interior S ≠ {}" by (simp add: False ‹convex S› rel_interior_eq_empty) qed auto thenshow ?thesis by simp qed
lemma homeomorphic_convex_sets_le: assumes"convex S""S homeomorphic T" shows"aff_dim S ≤ aff_dim T" proof - obtain h k where homhk: "homeomorphism S T h k" using homeomorphic_def assms by blast show ?thesis proof (rule invariance_of_dimension_convex_domain [OF ‹convex S›]) show"continuous_on S h" using homeomorphism_def homhk by blast show"h ∈ S → affine hull T" using homeomorphism_image1 homhk hull_subset by fastforce show"inj_on h S" by (meson homeomorphism_apply1 homhk inj_on_inverseI) qed qed
lemma homeomorphic_convex_sets: assumes"convex S""convex T""S homeomorphic T" shows"aff_dim S = aff_dim T" by (meson assms dual_order.antisym homeomorphic_convex_sets_le homeomorphic_sym)
lemma homeomorphic_convex_compact_sets_eq: assumes"convex S""compact S""convex T""compact T" shows"S homeomorphic T ⟷ aff_dim S = aff_dim T" by (meson assms homeomorphic_convex_compact_sets homeomorphic_convex_sets)
lemma invariance_of_domain_gen: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes"open S""continuous_on S f""inj_on f S""DIM('b) ≤ DIM('a)" shows"open(f ` S)" using invariance_of_domain_subspaces [of UNIV S UNIV f] assms by auto
lemma injective_into_1d_imp_open_map_UNIV: fixes f :: "'a::euclidean_space ==> real" assumes"open T""continuous_on S f""inj_on f S""T ⊆ S" shows"open (f ` T)" proof - have"DIM(real) ≤ DIM('a)" by simp thenshow ?thesis using invariance_of_domain_gen assms continuous_on_subset inj_on_subset by metis qed
lemma continuous_on_inverse_open: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes"open S""continuous_on S f""DIM('b) ≤ DIM('a)"and gf: "∧x. x ∈ S ==> g(f x) = x" shows"continuous_on (f ` S) g" proof (clarsimp simp add: continuous_openin_preimage_eq) fix T :: "'a set" assume"open T" have eq: "f ` S ∩ g -` T = f ` (S ∩ T)" by (auto simp: gf) have"open (f ` S)" by (rule invariance_of_domain_gen) (use assms inj_on_inverseI in auto) moreoverhave"open (f ` (S ∩ T))" using assms by (metis ‹open T› continuous_on_subset inj_onI inj_on_subset invariance_of_domain_gen openin_open openin_open_eq) ultimatelyshow"openin (top_of_set (f ` S)) (f ` S ∩ g -` T)" unfolding eq by (auto intro: open_openin_trans) qed
lemma invariance_of_domain_homeomorphism: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes"open S""continuous_on S f""DIM('b) ≤ DIM('a)""inj_on f S" obtains g where"homeomorphism S (f ` S) f g" proof show"homeomorphism S (f ` S) f (inv_into S f)" by (simp add: assms continuous_on_inverse_open homeomorphism_def) qed
corollary invariance_of_domain_homeomorphic: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes"open S""continuous_on S f""DIM('b) ≤ DIM('a)""inj_on f S" shows"S homeomorphic (f ` S)" using invariance_of_domain_homeomorphism [OF assms] by (meson homeomorphic_def)
lemma continuous_image_subset_interior: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes"continuous_on S f""inj_on f S""DIM('b) ≤ DIM('a)" shows"f ∈ (interior S) → interior(f ` S)" proof - have"open (f ` interior S)" using assms by (intro invariance_of_domain_gen) (auto simp: inj_on_subset interior_subset continuous_on_subset) thenshow ?thesis by (simp add: image_mono interiorI interior_subset) qed
lemma homeomorphic_interiors_same_dimension: fixes S :: "'a::euclidean_space set"and T :: "'b::euclidean_space set" assumes"S homeomorphic T"and dimeq: "DIM('a) = DIM('b)" shows"(interior S) homeomorphic (interior T)" using assms [unfolded homeomorphic_minimal] unfolding homeomorphic_def proof (clarify elim!: ex_forward) fix f g assume S: "∀x∈S. f x ∈ T ∧ g (f x) = x"and T: "∀y∈T. g y ∈ S ∧ f (g y) = y" and contf: "continuous_on S f"and contg: "continuous_on T g" thenhave fST: "f ` S = T"and gTS: "g ` T = S"and"inj_on f S""inj_on g T" by (auto simp: inj_on_def intro: rev_image_eqI) metis+ have fim: "f ∈ interior S → interior T" using continuous_image_subset_interior [OF contf ‹inj_on f S›] dimeq fST by simp have gim: "g ∈ interior T → interior S" using continuous_image_subset_interior [OF contg ‹inj_on g T›] dimeq gTS by simp show"homeomorphism (interior S) (interior T) f g" unfolding homeomorphism_def proof (intro conjI ballI) show"∧x. x ∈ interior S ==> g (f x) = x" by (meson ‹∀x∈S. f x ∈ T ∧ g (f x) = x› subsetD interior_subset) have"interior T ⊆ f ` interior S" proof fix x assume"x ∈ interior T" thenhave"g x ∈ interior S" using gim by blast thenshow"x ∈ f ` interior S" by (metis T ‹x ∈ interior T› image_iff interior_subset subsetCE) qed thenshow"f ` interior S = interior T" using fim by blast show"continuous_on (interior S) f" by (metis interior_subset continuous_on_subset contf) show"∧y. y ∈ interior T ==> f (g y) = y" by (meson T subsetD interior_subset) have"interior S ⊆ g ` interior T" proof fix x assume"x ∈ interior S" thenhave"f x ∈ interior T" using fim by blast thenshow"x ∈ g ` interior T" by (metis S ‹x ∈ interior S› image_iff interior_subset subsetCE) qed thenshow"g ` interior T = interior S" using gim by blast show"continuous_on (interior T) g" by (metis interior_subset continuous_on_subset contg) qed qed
proposition homeomorphic_interiors: fixes S :: "'a::euclidean_space set"and T :: "'b::euclidean_space set" assumes"S homeomorphic T""interior S = {} ⟷ interior T = {}" shows"(interior S) homeomorphic (interior T)" proof (cases "interior T = {}") case False thenhave"DIM('a) = DIM('b)" using assms apply (simp add: homeomorphic_minimal) apply (rule order_antisym; metis continuous_on_subset inj_onI inj_on_subset interior_subset invariance_of_dimension open_interior) done thenshow ?thesis by (rule homeomorphic_interiors_same_dimension [OF ‹S homeomorphic T›]) qed (use assms in auto)
lemma homeomorphic_frontiers_same_dimension: fixes S :: "'a::euclidean_space set"and T :: "'b::euclidean_space set" assumes"S homeomorphic T""closed S""closed T"and dimeq: "DIM('a) = DIM('b)" shows"(frontier S) homeomorphic (frontier T)" using assms [unfolded homeomorphic_minimal] unfolding homeomorphic_def proof (clarify elim!: ex_forward) fix f g assume S: "∀x∈S. f x ∈ T ∧ g (f x) = x"and T: "∀y∈T. g y ∈ S ∧ f (g y) = y" and contf: "continuous_on S f"and contg: "continuous_on T g" thenhave fST: "f ` S = T"and gTS: "g ` T = S"and"inj_on f S""inj_on g T" by (auto simp: inj_on_def intro: rev_image_eqI) metis+ have"g ∈ interior T → interior S" using continuous_image_subset_interior [OF contg ‹inj_on g T›] dimeq gTS by simp thenhave fim: "f ` frontier S ⊆ frontier T" unfolding frontier_def using Pi_mem S assms by fastforce have"f ∈ interior S → interior T" using continuous_image_subset_interior [OF contf ‹inj_on f S›] dimeq fST by simp thenhave gim: "g ` frontier T ⊆ frontier S" unfolding frontier_def using Pi_mem T assms by fastforce show"homeomorphism (frontier S) (frontier T) f g" unfolding homeomorphism_def proof (intro conjI ballI) show gf: "∧x. x ∈ frontier S ==> g (f x) = x" by (simp add: S assms(2) frontier_def) show fg: "∧y. y ∈ frontier T ==> f (g y) = y" by (simp add: T assms(3) frontier_def) have"frontier T ⊆ f ` frontier S" proof fix x assume"x ∈ frontier T" thenhave"g x ∈ frontier S" using gim by blast thenshow"x ∈ f ` frontier S" by (metis fg ‹x ∈ frontier T› imageI) qed thenshow"f ` frontier S = frontier T" using fim by blast show"continuous_on (frontier S) f" by (metis Diff_subset assms(2) closure_eq contf continuous_on_subset frontier_def) have"frontier S ⊆ g ` frontier T" proof fix x assume"x ∈ frontier S" thenhave"f x ∈ frontier T" using fim by blast thenshow"x ∈ g ` frontier T" by (metis gf ‹x ∈ frontier S› imageI) qed thenshow"g ` frontier T = frontier S" using gim by blast show"continuous_on (frontier T) g" by (metis Diff_subset assms(3) closure_closed contg continuous_on_subset frontier_def) qed qed
lemma homeomorphic_frontiers: fixes S :: "'a::euclidean_space set"and T :: "'b::euclidean_space set" assumes"S homeomorphic T""closed S""closed T" "interior S = {} ⟷ interior T = {}" shows"(frontier S) homeomorphic (frontier T)" proof (cases "interior T = {}") case True thenshow ?thesis by (metis Diff_empty assms closure_eq frontier_def) next case False thenhave"DIM('a) = DIM('b)" using assms homeomorphic_interiors homeomorphic_open_imp_same_dimension by blast thenshow ?thesis using assms homeomorphic_frontiers_same_dimension by blast qed
lemma continuous_image_subset_rel_interior: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes contf: "continuous_on S f"and injf: "inj_on f S"and fim: "f ∈ S → T" and TS: "aff_dim T ≤ aff_dim S" shows"f ∈ (rel_interior S) → rel_interior(f ` S)" unfolding image_subset_iff_funcset [symmetric] proof (rule rel_interior_maximal) show"f ` rel_interior S ⊆ f ` S" by(simp add: image_mono rel_interior_subset) show"openin (top_of_set (affine hull f ` S)) (f ` rel_interior S)" proof (rule invariance_of_domain_affine_sets) show"openin (top_of_set (affine hull S)) (rel_interior S)" by (simp add: openin_rel_interior) show"aff_dim (affine hull f ` S) ≤ aff_dim (affine hull S)" by (metis TS aff_dim_affine_hull aff_dim_subset fim image_subset_iff_funcset order_trans) show"f ∈ rel_interior S → affine hull f ` S" using‹f ` rel_interior S ⊆ f ` S› hull_subset by fastforce show"continuous_on (rel_interior S) f" using contf continuous_on_subset rel_interior_subset by blast show"inj_on f (rel_interior S)" using inj_on_subset injf rel_interior_subset by blast qed auto qed
lemma homeomorphic_rel_interiors_same_dimension: fixes S :: "'a::euclidean_space set"and T :: "'b::euclidean_space set" assumes"S homeomorphic T"and aff: "aff_dim S = aff_dim T" shows"(rel_interior S) homeomorphic (rel_interior T)" using assms [unfolded homeomorphic_minimal] unfolding homeomorphic_def proof (clarify elim!: ex_forward) fix f g assume S: "∀x∈S. f x ∈ T ∧ g (f x) = x"and T: "∀y∈T. g y ∈ S ∧ f (g y) = y" and contf: "continuous_on S f"and contg: "continuous_on T g" thenhave fST: "f ` S = T"and gTS: "g ` T = S"and"inj_on f S""inj_on g T" by (auto simp: inj_on_def intro: rev_image_eqI) metis+ have fim: "f ∈ rel_interior S → rel_interior T" by (smt (verit, best) PiE Pi_I S ‹inj_on f S› aff contf continuous_image_subset_rel_interior fST) have gim: "g ∈ rel_interior T → rel_interior S" by (metis T ‹inj_on g T› aff contg continuous_image_subset_rel_interior dual_order.refl funcsetI gTS) show"homeomorphism (rel_interior S) (rel_interior T) f g" unfolding homeomorphism_def proof (intro conjI ballI) show gf: "∧x. x ∈ rel_interior S ==> g (f x) = x" using S rel_interior_subset by blast show fg: "∧y. y ∈ rel_interior T ==> f (g y) = y" using T mem_rel_interior_ball by blast have"rel_interior T ⊆ f ` rel_interior S" proof fix x assume"x ∈ rel_interior T" thenhave"g x ∈ rel_interior S" using gim by blast thenshow"x ∈ f ` rel_interior S" by (metis fg ‹x ∈ rel_interior T› imageI) qed moreoverhave"f ` rel_interior S ⊆ rel_interior T" using fim by blast ultimatelyshow"f ` rel_interior S = rel_interior T" by blast show"continuous_on (rel_interior S) f" using contf continuous_on_subset rel_interior_subset by blast have"rel_interior S ⊆ g ` rel_interior T" proof fix x assume"x ∈ rel_interior S" thenhave"f x ∈ rel_interior T" using fim by blast thenshow"x ∈ g ` rel_interior T" by (metis gf ‹x ∈ rel_interior S› imageI) qed thenshow"g ` rel_interior T = rel_interior S" using gim by blast show"continuous_on (rel_interior T) g" using contg continuous_on_subset rel_interior_subset by blast qed qed
lemma homeomorphic_aff_dim_le: fixes S :: "'a::euclidean_space set" assumes"S homeomorphic T""rel_interior S ≠ {}" shows"aff_dim (affine hull S) ≤ aff_dim (affine hull T)" proof - obtain f g where S: "∀x∈S. f x ∈ T ∧ g (f x) = x"and T: "∀y∈T. g y ∈ S ∧ f (g y) = y" and contf: "continuous_on S f"and contg: "continuous_on T g" using assms [unfolded homeomorphic_minimal] by auto show ?thesis proof (rule invariance_of_dimension_affine_sets) show"continuous_on (rel_interior S) f" using contf continuous_on_subset rel_interior_subset by blast show"f ∈ rel_interior S → affine hull T" by (simp add: S hull_inc mem_rel_interior_ball) show"inj_on f (rel_interior S)" by (metis S inj_on_inverseI inj_on_subset rel_interior_subset) qed (simp_all add: openin_rel_interior assms) qed
lemma homeomorphic_rel_interiors: fixes S :: "'a::euclidean_space set"and T :: "'b::euclidean_space set" assumes"S homeomorphic T""rel_interior S = {} ⟷ rel_interior T = {}" shows"(rel_interior S) homeomorphic (rel_interior T)" proof (cases "rel_interior T = {}") case True with assms show ?thesis by auto next case False have"aff_dim (affine hull S) ≤ aff_dim (affine hull T)" using False assms homeomorphic_aff_dim_le by blast moreoverhave"aff_dim (affine hull T) ≤ aff_dim (affine hull S)" using False assms(1) homeomorphic_aff_dim_le homeomorphic_sym by auto ultimatelyhave"aff_dim S = aff_dim T"by force thenshow ?thesis by (rule homeomorphic_rel_interiors_same_dimension [OF ‹S homeomorphic T›]) qed
lemma homeomorphic_rel_boundaries_same_dimension: fixes S :: "'a::euclidean_space set"and T :: "'b::euclidean_space set" assumes"S homeomorphic T"and aff: "aff_dim S = aff_dim T" shows"(S - rel_interior S) homeomorphic (T - rel_interior T)" using assms [unfolded homeomorphic_minimal] unfolding homeomorphic_def proof (clarify elim!: ex_forward) fix f g assume S: "∀x∈S. f x ∈ T ∧ g (f x) = x"and T: "∀y∈T. g y ∈ S ∧ f (g y) = y" and contf: "continuous_on S f"and contg: "continuous_on T g" thenhave fST: "f ` S = T"and gTS: "g ` T = S"and"inj_on f S""inj_on g T" by (auto simp: inj_on_def intro: rev_image_eqI) metis+ have fim: "f ∈ rel_interior S → rel_interior T" by (metis ‹inj_on f S› aff contf continuous_image_subset_rel_interior dual_order.refl fST image_subset_iff_funcset) have gim: "g ∈ rel_interior T → rel_interior S" by (metis ‹inj_on g T› aff contg continuous_image_subset_rel_interior dual_order.refl gTS image_subset_iff_funcset) show"homeomorphism (S - rel_interior S) (T - rel_interior T) f g" unfolding homeomorphism_def proof (intro conjI ballI) show gf: "∧x. x ∈ S - rel_interior S ==> g (f x) = x" using S rel_interior_subset by blast show fg: "∧y. y ∈ T - rel_interior T ==> f (g y) = y" using T mem_rel_interior_ball by blast show"f ` (S - rel_interior S) = T - rel_interior T" using S fST fim gim image_subset_iff_funcset by fastforce show"continuous_on (S - rel_interior S) f" using contf continuous_on_subset rel_interior_subset by blast show"g ` (T - rel_interior T) = S - rel_interior S" using T gTS gim fim image_subset_iff_funcset by fastforce show"continuous_on (T - rel_interior T) g" using contg continuous_on_subset rel_interior_subset by blast qed qed
lemma homeomorphic_rel_boundaries: fixes S :: "'a::euclidean_space set"and T :: "'b::euclidean_space set" assumes"S homeomorphic T""rel_interior S = {} ⟷ rel_interior T = {}" shows"(S - rel_interior S) homeomorphic (T - rel_interior T)" proof (cases "rel_interior T = {}") case True with assms show ?thesis by auto next case False obtain f g where S: "∀x∈S. f x ∈ T ∧ g (f x) = x"and T: "∀y∈T. g y ∈ S ∧ f (g y) = y" and contf: "continuous_on S f"and contg: "continuous_on T g" using assms by (auto simp: homeomorphic_minimal) have"aff_dim (affine hull S) ≤ aff_dim (affine hull T)" using False assms homeomorphic_aff_dim_le by blast moreoverhave"aff_dim (affine hull T) ≤ aff_dim (affine hull S)" by (meson False assms(1) homeomorphic_aff_dim_le homeomorphic_sym) ultimatelyhave"aff_dim S = aff_dim T"by force thenshow ?thesis by (rule homeomorphic_rel_boundaries_same_dimension [OF ‹S homeomorphic T›]) qed
proposition uniformly_continuous_homeomorphism_UNIV_trivial: fixes f :: "'a::euclidean_space ==> 'a" assumes contf: "uniformly_continuous_on S f"and hom: "homeomorphism S UNIV f g" shows"S = UNIV" proof (cases "S = {}") case True thenshow ?thesis by (metis UNIV_I hom empty_iff homeomorphism_def image_eqI) next case False have"inj g" by (metis UNIV_I hom homeomorphism_apply2 injI) thenhave"open (g ` UNIV)" by (blast intro: invariance_of_domain hom homeomorphism_cont2) thenhave"open S" using hom homeomorphism_image2 by blast moreoverhave"complete S" unfolding complete_def proof clarify fix σ assume σ: "∀n. σ n ∈ S"and"Cauchy σ" have"Cauchy (f o σ)" using uniformly_continuous_imp_Cauchy_continuous ‹Cauchy σ› σ contf unfolding Cauchy_continuous_on_def by blast thenobtain l where"(f ∘ σ) <---- l" by (auto simp: convergent_eq_Cauchy [symmetric]) show"∃l∈S. σ <---- l" proof show"g l ∈ S" using hom homeomorphism_image2 by blast have"(g ∘ (f ∘ σ)) <---- g l" by (meson UNIV_I ‹(f ∘ σ) <---- l› continuous_on_sequentially hom homeomorphism_cont2) thenshow"σ <---- g l" proof - have"∀n. σ n = (g ∘ (f ∘ σ)) n" by (metis (no_types) σ comp_eq_dest_lhs hom homeomorphism_apply1) thenshow ?thesis by (metis (no_types) LIMSEQ_iff ‹(g ∘ (f ∘ σ)) <---- g l›) qed qed qed thenhave"closed S" by (simp add: complete_eq_closed) ultimatelyshow ?thesis using clopen [of S] False by simp qed
subsection‹Formulation of loop homotopy in terms of maps out of type complex›
lemma homotopic_circlemaps_imp_homotopic_loops: assumes"homotopic_with_canon (λh. True) (sphere 0 1) S f g" shows"homotopic_loops S (f ∘ exp ∘ (λt. 2 * of_real pi * of_real t * i)) (g ∘ exp ∘ (λt. 2 * of_real pi * of_real t * i))" proof - have"homotopic_with_canon (λf. True) {z. cmod z = 1} S f g" using assms by (auto simp: sphere_def) moreoverhave"continuous_on {0..1} (exp ∘ (λt. 2 * of_real pi * of_real t * i))" by (intro continuous_intros) moreoverhave"(exp ∘ (λt. 2 * of_real pi * of_real t * i)) ` {0..1} ⊆ {z. cmod z = 1}" by (auto simp: norm_mult) ultimately show ?thesis apply (simp add: homotopic_loops_def comp_assoc) apply (rule homotopic_with_compose_continuous_right) apply (auto simp: pathstart_def pathfinish_def) done qed
lemma homotopic_loops_imp_homotopic_circlemaps: assumes"homotopic_loops S p q" shows"homotopic_with_canon (λh. True) (sphere 0 1) S (p ∘ (λz. (Arg2pi z / (2 * pi)))) (q ∘ (λz. (Arg2pi z / (2 * pi))))" proof - obtain h where conth: "continuous_on ({0..1::real} × {0..1}) h" and him: "h ∈ ({0..1} × {0..1}) → S" and h0: "(∀x. h (0, x) = p x)" and h1: "(∀x. h (1, x) = q x)" and h01: "(∀t∈{0..1}. h (t, 1) = h (t, 0)) " using assms by (auto simp: homotopic_loops_def sphere_def homotopic_with_def pathstart_def pathfinish_def)
define j where"j ≡ λz. if 0 ≤ Im (snd z) then h (fst z, Arg2pi (snd z) / (2 * pi)) else h (fst z, 1 - Arg2pi (cnj (snd z)) / (2 * pi))" have Arg2pi_eq: "1 - Arg2pi (cnj y) / (2 * pi) = Arg2pi y / (2 * pi) ∨ Arg2pi y = 0 ∧ Arg2pi (cnj y) = 0"if"cmod y = 1"for y using that Arg2pi_eq_0_pi Arg2pi_eq_pi by (force simp: Arg2pi_cnj field_split_simps) show ?thesis proof (simp add: homotopic_with; intro conjI ballI exI) show"continuous_on ({0..1} × sphere 0 1) (λw. h (fst w, Arg2pi (snd w) / (2 * pi)))" proof (rule continuous_on_eq) show j: "j x = h (fst x, Arg2pi (snd x) / (2 * pi))"if"x ∈ {0..1} × sphere 0 1"forx using Arg2pi_eq that h01 by (force simp: j_def) have eq: "S = S ∩ (UNIV × {z. 0 ≤ Im z}) ∪ S ∩ (UNIV × {z. Im z ≤ 0})"for S :: "(real*complex)set" by auto have🍋: "Arg2pi z ≤ 2 * pi"for z by (simp add: Arg2pi order_le_less) have c1: "continuous_on ({0..1} × sphere 0 1 ∩ UNIV × {z. 0 ≤ Im z}) (λx. h (fst x, Arg2pi (snd x) / (2 * pi)))" apply (intro continuous_intros continuous_on_compose2 [OF conth] continuous_on_compose2 [OF continuous_on_upperhalf_Arg2pi]) by (auto simp: Arg2pi 🍋) have c2: "continuous_on ({0..1} × sphere 0 1 ∩ UNIV × {z. Im z ≤ 0}) (λx. h (fst x, 1 - Arg2pi (cnj (snd x)) / (2 * pi)))" apply (intro continuous_intros continuous_on_compose2 [OF conth] continuous_on_compose2 [OF continuous_on_upperhalf_Arg2pi]) by (auto simp: Arg2pi 🍋) show"continuous_on ({0..1} × sphere 0 1) j" apply (simp add: j_def) apply (subst eq) apply (rule continuous_on_cases_local) using Arg2pi_eq h01 by (force simp add: eq [symmetric] closedin_closed_Int closed_Times closed_halfspace_Im_le closed_halfspace_Im_ge c1 c2)+ qed have"(λw. h (fst w, Arg2pi (snd w) / (2 * pi))) ` ({0..1} × sphere 0 1) ⊆ h ` ({0..1} × {0..1})" by (auto simp: Arg2pi_ge_0 Arg2pi_lt_2pi less_imp_le) alsohave"... ⊆ S" using him by blast finallyshow"(λw. h (fst w, Arg2pi (snd w) / (2 * pi))) ∈ {0..1} × sphere 0 1 → S" by blast qed (auto simp: h0 h1) qed
lemma simply_connected_homotopic_loops: "simply_connected S ⟷ (∀p q. homotopic_loops S p p ∧ homotopic_loops S q q ⟶ homotopic_loops S p q)" unfolding simply_connected_def using homotopic_loops_refl by metis
lemma simply_connected_eq_homotopic_circlemaps1: fixes f :: "complex ==> 'a::topological_space"and g :: "complex ==> 'a" assumes S: "simply_connected S" and contf: "continuous_on (sphere 0 1) f"and fim: "f ∈ (sphere 0 1) → S" and contg: "continuous_on (sphere 0 1) g"and gim: "g ∈ (sphere 0 1) → S" shows"homotopic_with_canon (λh. True) (sphere 0 1) S f g" proof - let ?h = "(λt. complex_of_real (2 * pi * t) * i)" have"homotopic_loops S (f ∘ exp ∘ ?h) (f ∘ exp ∘ ?h) ∧ homotopic_loops S (g ∘ exp ∘ ?h) (g ∘ exp ∘ ?h)" by (simp add: homotopic_circlemaps_imp_homotopic_loops contf fim contg gim image_subset_iff_funcset) thenhave"homotopic_loops S (f ∘ exp ∘ ?h) (g ∘ exp ∘ ?h)" using S simply_connected_homotopic_loops by blast thenshow ?thesis apply (rule homotopic_with_eq [OF homotopic_loops_imp_homotopic_circlemaps]) apply (auto simp: o_def complex_norm_eq_1_exp mult.commute) done qed
lemma simply_connected_eq_homotopic_circlemaps2a: fixes h :: "complex ==> 'a::topological_space" assumes conth: "continuous_on (sphere 0 1) h"and him: "h ∈ sphere 0 1 → S" and hom: "∧f g::complex ==> 'a. [continuous_on (sphere 0 1) f; f ∈ (sphere 0 1) → S; continuous_on (sphere 0 1) g; g ∈ (sphere 0 1) → S] ==> homotopic_with_canon (λh. True) (sphere 0 1) S f g" shows"∃a. homotopic_with_canon (λh. True) (sphere 0 1) S h (λx. a)" by (metis conth continuous_on_const him hom image_subset_iff image_subset_iff_funcset)
lemma simply_connected_eq_homotopic_circlemaps2b: fixes S :: "'a::real_normed_vector set" assumes"∧f g::complex ==> 'a. [continuous_on (sphere 0 1) f; f ∈ (sphere 0 1) → S; continuous_on (sphere 0 1) g; g ∈ (sphere 0 1) → S] ==> homotopic_with_canon (λh. True) (sphere 0 1) S f g" shows"path_connected S" proof (clarsimp simp add: path_connected_eq_homotopic_points) fix a b assume"a ∈ S""b ∈ S" thenshow"homotopic_loops S (linepath a a) (linepath b b)" using homotopic_circlemaps_imp_homotopic_loops [OF assms [of "λx. a""λx. b"]] by (auto simp: o_def linepath_def) qed
lemma simply_connected_eq_homotopic_circlemaps3: fixes h :: "complex ==> 'a::real_normed_vector" assumes"path_connected S" and hom: "∧f::complex ==> 'a. [continuous_on (sphere 0 1) f; f `(sphere 0 1) ⊆ S] ==>∃a. homotopic_with_canon (λh. True) (sphere 0 1) S f (λx. a)" shows"simply_connected S" proof (clarsimp simp add: simply_connected_eq_contractible_loop_some assms) fix p assume p: "path p""path_image p ⊆ S""pathfinish p = pathstart p" thenhave"homotopic_loops S p p" by (simp add: homotopic_loops_refl) thenobtain a where homp: "homotopic_with_canon (λh. True) (sphere 0 1) S (p ∘ (λz. Arg2pi z / (2 * pi))) (λx. a)" by (metis homotopic_with_imp_subset2 homotopic_loops_imp_homotopic_circlemaps homotopic_with_imp_continuous hom) show"∃a. a ∈ S ∧ homotopic_loops S p (linepath a a)" proof (intro exI conjI) show"a ∈ S" using homotopic_with_imp_subset2 [OF homp] by (metis dist_0_norm image_subset_iff mem_sphere norm_one) have teq: "∧t. [0 ≤ t; t ≤ 1] ==> t = Arg2pi (exp (2 * of_real pi * of_real t * i)) / (2 * pi) ∨ t=1 ∧ Arg2pi (exp (2 * of_real pi * of_real t * i)) = 0" using Arg2pi_of_real [of 1] by (force simp: Arg2pi_exp) have"homotopic_loops S p (p ∘ (λz. Arg2pi z / (2 * pi)) ∘ exp ∘ (λt. 2 * complex_of_real pi * complex_of_real t * i))" using p teq by (fastforce simp: pathfinish_def pathstart_def intro: homotopic_loops_eq [OF p]) thenshow"homotopic_loops S p (linepath a a)" by (simp add: linepath_refl homotopic_loops_trans [OF _ homotopic_circlemaps_imp_homotopic_loops [OF homp, simplified K_record_comp]]) qed qed
proposition simply_connected_eq_homotopic_circlemaps: fixes S :: "'a::real_normed_vector set" shows"simply_connected S ⟷ (∀f g::complex ==> 'a. continuous_on (sphere 0 1) f ∧ f ∈ (sphere 0 1) → S ∧ continuous_on (sphere 0 1) g ∧ g ∈ (sphere 0 1) → S ⟶ homotopic_with_canon (λh. True) (sphere 0 1) S f g)" by (metis image_subset_iff_funcset simply_connected_eq_homotopic_circlemaps1 simply_connected_eq_homotopic_circlemaps2a
simply_connected_eq_homotopic_circlemaps2b simply_connected_eq_homotopic_circlemaps3)
proposition simply_connected_eq_contractible_circlemap: fixes S :: "'a::real_normed_vector set" shows"simply_connected S ⟷ path_connected S ∧ (∀f::complex ==> 'a. continuous_on (sphere 0 1) f ∧ f `(sphere 0 1) ⊆ S ⟶ (∃a. homotopic_with_canon (λh. True) (sphere 0 1) S f (λx. a)))" by (metis image_subset_iff_funcset simply_connected_eq_homotopic_circlemaps simply_connected_eq_homotopic_circlemaps2a
simply_connected_eq_homotopic_circlemaps3 simply_connected_imp_path_connected)
corollary homotopy_eqv_simple_connectedness: fixes S :: "'a::real_normed_vector set"and T :: "'b::real_normed_vector set" shows"S homotopy_eqv T ==> simply_connected S ⟷ simply_connected T" by (simp add: simply_connected_eq_homotopic_circlemaps homotopy_eqv_homotopic_triviality image_subset_iff_funcset)
subsection‹Homeomorphism of simple closed curves to circles›
proposition homeomorphic_simple_path_image_circle: fixes a :: complex and γ :: "real ==> 'a::t2_space" assumes"simple_path γ"and loop: "pathfinish γ = pathstart γ"and"0 < r" shows"(path_image γ) homeomorphic sphere a r" proof - have"homotopic_loops (path_image γ) γ γ" by (simp add: assms homotopic_loops_refl simple_path_imp_path) thenhave hom: "homotopic_with_canon (λh. True) (sphere 0 1) (path_image γ) (γ ∘ (λz. Arg2pi z / (2*pi))) (γ ∘ (λz. Arg2pi z / (2*pi)))" by (rule homotopic_loops_imp_homotopic_circlemaps) have"∃g. homeomorphism (sphere 0 1) (path_image γ) (γ ∘ (λz. Arg2pi z / (2*pi))) g" proof (rule homeomorphism_compact) show"continuous_on (sphere 0 1) (γ ∘ (λz. Arg2pi z / (2*pi)))" using hom homotopic_with_imp_continuous by blast show"inj_on (γ ∘ (λz. Arg2pi z / (2*pi))) (sphere 0 1)" proof fix x y assume xy: "x ∈ sphere 0 1""y ∈ sphere 0 1" and eq: "(γ ∘ (λz. Arg2pi z / (2*pi))) x = (γ ∘ (λz. Arg2pi z / (2*pi))) y" thenhave"(Arg2pi x / (2*pi)) = (Arg2pi y / (2*pi))" proof - have"(Arg2pi x / (2*pi)) ∈ {0..1}""(Arg2pi y / (2*pi)) ∈ {0..1}" using Arg2pi_ge_0 Arg2pi_lt_2pi dual_order.strict_iff_order by fastforce+ with eq show ?thesis using‹simple_path γ› Arg2pi_lt_2pi unfolding simple_path_def loop_free_def o_def by (metis eq_divide_eq_1 not_less_iff_gr_or_eq) qed with xy show"x = y" by (metis is_Arg_def Arg2pi Arg2pi_0 dist_0_norm divide_cancel_right dual_order.strict_iff_order mem_sphere) qed have"∧z. cmod z = 1 ==>∃x∈{0..1}. γ (Arg2pi z / (2*pi)) = γ x" by (metis Arg2pi_ge_0 Arg2pi_lt_2pi atLeastAtMost_iff divide_less_eq_1 less_eq_real_def zero_less_mult_iff pi_gt_zero zero_le_divide_iff zero_less_numeral) moreoverhave"∃z∈sphere 0 1. γ x = γ (Arg2pi z / (2*pi))"if"0 ≤ x""x ≤ 1"for x proof (cases "x=1") case True with Arg2pi_of_real [of 1] loop show ?thesis by (rule_tac x=1 in bexI) (auto simp: pathfinish_def pathstart_def ‹0 ≤ x›) next case False thenhave *: "(Arg2pi (exp (i*(2* of_real pi* of_real x))) / (2*pi)) = x" using that by (auto simp: Arg2pi_exp field_split_simps) show ?thesis by (rule_tac x="exp(i * of_real(2*pi*x))"in bexI) (auto simp: *) qed ultimatelyshow"(γ ∘ (λz. Arg2pi z / (2*pi))) ` sphere 0 1 = path_image γ" by (auto simp: path_image_def image_iff) qed auto thenhave"path_image γ homeomorphic sphere (0::complex) 1" using homeomorphic_def homeomorphic_sym by blast alsohave"... homeomorphic sphere a r" by (simp add: assms homeomorphic_spheres) finallyshow ?thesis . qed
subsection‹Dimension-based conditions for various homeomorphisms›
lemma homeomorphic_subspaces_eq: fixes S :: "'a::euclidean_space set"and T :: "'b::euclidean_space set" assumes"subspace S""subspace T" shows"S homeomorphic T ⟷ dim S = dim T" proof assume"S homeomorphic T" thenobtain f g where hom: "homeomorphism S T f g" using homeomorphic_def by blast show"dim S = dim T" by (metis ‹S homeomorphic T› aff_dim_subspace assms homeomorphic_convex_sets of_nat_eq_iff subspace_imp_convex) next assume"dim S = dim T" thenshow"S homeomorphic T" by (simp add: assms homeomorphic_subspaces) qed
lemma homeomorphic_affine_sets_eq: fixes S :: "'a::euclidean_space set"and T :: "'b::euclidean_space set" assumes"affine S""affine T" shows"S homeomorphic T ⟷ aff_dim S = aff_dim T" proof (cases "S = {} ∨ T = {}") case True thenshow ?thesis using assms homeomorphic_affine_sets by force next case False thenobtain a b where"a ∈ S""b ∈ T" by blast thenhave"subspace ((+) (- a) ` S)""subspace ((+) (- b) ` T)" using affine_diffs_subspace assms by blast+ thenshow ?thesis by (metis affine_imp_convex assms homeomorphic_affine_sets homeomorphic_convex_sets) qed
lemma homeomorphic_hyperplanes_eq: fixes a :: "'a::euclidean_space"and c :: "'b::euclidean_space" assumes"a ≠ 0""c ≠ 0" shows"({x. a ∙ x = b} homeomorphic {x. c ∙ x = d} ⟷ DIM('a) = DIM('b))" proof - have"DIM('a) - Suc 0 = DIM('b) - Suc 0 ==> DIM('a) = DIM('b)" by (metis DIM_positive Suc_pred) thenshow ?thesis by (auto simp: homeomorphic_affine_sets_eq affine_hyperplane assms) qed
lemma simply_connected_sphere_gen: assumes"convex S""bounded S"and 3: "3 ≤ aff_dim S" shows"simply_connected(rel_frontier S)" proof - have pa: "path_connected (rel_frontier S)" using assms by (simp add: path_connected_sphere_gen) show ?thesis proof (clarsimp simp add: simply_connected_eq_contractible_circlemap pa) fix f assume f: "continuous_on (sphere (0::complex) 1) f""f ` sphere 0 1 ⊆ rel_frontier S" have eq: "sphere (0::complex) 1 = rel_frontier(cball 0 1)" by simp have"convex (cball (0::complex) 1)" by (rule convex_cball) thenobtain c where"homotopic_with_canon (λz. True) (sphere (0::complex) 1) (rel_frontier S) f (λx. c)" apply (rule inessential_spheremap_lowdim_gen [OF _ bounded_cball ‹convex S›‹bounded S›, where f=f]) using f 3 by (auto simp: aff_dim_cball) thenshow"∃a. homotopic_with_canon (λh. True) (sphere 0 1) (rel_frontier S) f (λx. a)" by blast qed qed
subsection‹more invariance of domain›(*FIX ME title? *)
proposition invariance_of_domain_sphere_affine_set_gen: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes contf: "continuous_on S f"and injf: "inj_on f S"and fim: "f ∈ S → T" and U: "bounded U""convex U" and"affine T"and affTU: "aff_dim T < aff_dim U" and ope: "openin (top_of_set (rel_frontier U)) S" shows"openin (top_of_set T) (f ` S)" proof (cases "rel_frontier U = {}") case True thenshow ?thesis using ope openin_subset by force next case False obtain b c where b: "b ∈ rel_frontier U"and c: "c ∈ rel_frontier U"and"b ≠ c" using‹bounded U› rel_frontier_not_sing [of U] subset_singletonD False by fastforce obtain V :: "'a set"where"affine V"and affV: "aff_dim V = aff_dim U - 1" proof (rule choose_affine_subset [OF affine_UNIV]) show"- 1 ≤ aff_dim U - 1" by (metis aff_dim_empty aff_dim_geq aff_dim_negative_iff affTU diff_0 diff_right_mono not_le) show"aff_dim U - 1 ≤ aff_dim (UNIV::'a set)" by (metis aff_dim_UNIV aff_dim_le_DIM le_cases not_le zle_diff1_eq) qed auto have SU: "S ⊆ rel_frontier U" using ope openin_imp_subset by auto have homb: "rel_frontier U - {b} homeomorphic V" and homc: "rel_frontier U - {c} homeomorphic V" using homeomorphic_punctured_sphere_affine_gen [of U _ V] by (simp_all add: ‹affine V› affV U b c) thenobtain g h j k where gh: "homeomorphism (rel_frontier U - {b}) V g h" and jk: "homeomorphism (rel_frontier U - {c}) V j k" by (auto simp: homeomorphic_def) with SU have hgsub: "(h ` g ` (S - {b})) ⊆ S"and kjsub: "(k ` j ` (S - {c})) ⊆ S" by (simp_all add: homeomorphism_def subset_eq) have [simp]: "aff_dim T ≤ aff_dim V" by (simp add: affTU affV) have"openin (top_of_set T) ((f ∘ h) ` g ` (S - {b}))" proof (rule invariance_of_domain_affine_sets [OF _ ‹affine V›]) have"openin (top_of_set (rel_frontier U - {b})) (S - {b})" by (meson Diff_mono Diff_subset SU ope openin_delete openin_subset_trans order_refl) thenshow"openin (top_of_set V) (g ` (S - {b}))" by (rule homeomorphism_imp_open_map [OF gh]) show"continuous_on (g ` (S - {b})) (f ∘ h)" proof (rule continuous_on_compose) show"continuous_on (g ` (S - {b})) h" by (meson Diff_mono SU homeomorphism_def homeomorphism_of_subsets gh set_eq_subset) qed (use contf continuous_on_subset hgsub in blast) show"inj_on (f ∘ h) (g ` (S - {b}))" by (smt (verit, del_insts) SU homeomorphism_def inj_on_def injf gh Diff_iff comp_apply imageE subset_iff) show"f ∘ h ∈ g ` (S - {b}) → T" using fim hgsub by fastforce qed (auto simp: assms) moreover have"openin (top_of_set T) ((f ∘ k) ` j ` (S - {c}))" proof (rule invariance_of_domain_affine_sets [OF _ ‹affine V›]) show"openin (top_of_set V) (j ` (S - {c}))" by (meson Diff_mono Diff_subset SU ope openin_delete openin_subset_trans order_refl homeomorphism_imp_open_map [OF jk]) show"continuous_on (j ` (S - {c})) (f ∘ k)" proof (rule continuous_on_compose) show"continuous_on (j ` (S - {c})) k" by (meson Diff_mono SU homeomorphism_def homeomorphism_of_subsets jk set_eq_subset) qed (use contf continuous_on_subset kjsub in blast) show"inj_on (f ∘ k) (j ` (S - {c}))" by (smt (verit, del_insts) SU homeomorphism_def inj_on_def injf jk Diff_iff comp_apply imageE subset_iff) show"f ∘ k ∈ j ` (S - {c}) → T" using fim kjsub by fastforce qed (auto simp: assms) ultimatelyhave"openin (top_of_set T) ((f ∘ h) ` g ` (S - {b}) ∪ ((f ∘ k) ` j ` (S - {c})))" by (rule openin_Un) moreoverhave"(f ∘ h) ` g ` (S - {b}) = f ` (S - {b})" proof - have"h ` g ` (S - {b}) = (S - {b})" by (meson Diff_mono Diff_subset SU gh homeomorphism_def homeomorphism_of_subsets subset_singleton_iff) thenshow ?thesis by (metis image_comp) qed moreoverhave"(f ∘ k) ` j ` (S - {c}) = f ` (S - {c})" proof - have"k ` j ` (S - {c}) = (S - {c})" using homeomorphism_apply1 [OF jk] SU by (meson Diff_mono homeomorphism_def homeomorphism_of_subsets jk subset_refl) thenshow ?thesis by (metis image_comp) qed moreoverhave"f ` (S - {b}) ∪ f ` (S - {c}) = f ` (S)" using‹b ≠ c›by blast ultimatelyshow ?thesis by simp qed
lemma invariance_of_domain_sphere_affine_set: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes contf: "continuous_on S f"and injf: "inj_on f S"and fim: "f ∈ S → T" and"r ≠ 0""affine T"and affTU: "aff_dim T < DIM('a)" and ope: "openin (top_of_set (sphere a r)) S" shows"openin (top_of_set T) (f ` S)" proof (cases "sphere a r = {}") case True thenshow ?thesis using ope openin_subset by force next case False show ?thesis proof (rule invariance_of_domain_sphere_affine_set_gen [OF contf injf fim bounded_cball convex_cball ‹affine T›]) show"aff_dim T < aff_dim (cball a r)" by (metis False affTU aff_dim_cball assms(4) linorder_cases sphere_empty) show"openin (top_of_set (rel_frontier (cball a r))) S" by (simp add: ‹r ≠ 0› ope) qed qed
lemma no_embedding_sphere_lowdim: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes contf: "continuous_on (sphere a r) f"and injf: "inj_on f (sphere a r)"and"r > 0" shows"DIM('a) ≤ DIM('b)" proof - have"False"if"DIM('a) > DIM('b)" proof - have"compact (f ` sphere a r)" using compact_continuous_image by (simp add: compact_continuous_image contf) thenhave"¬ open (f ` sphere a r)" using compact_open by (metis assms(3) image_is_empty not_less_iff_gr_or_eq sphere_eq_empty) thenhave"r=0" by (metis Pi_I UNIV_I aff_dim_UNIV affine_UNIV contf injf invariance_of_domain_sphere_affine_set
of_nat_less_iff open_openin openin_subtopology_self subtopology_UNIV that) with‹r>0›show False by auto qed thenshow ?thesis using not_less by blast qed
lemma simply_connected_sphere: fixes a :: "'a::euclidean_space" assumes"3 ≤ DIM('a)" shows"simply_connected(sphere a r)" proof (cases rule: linorder_cases [of r 0]) case less thenshow ?thesis by simp next case equal thenshow ?thesis by (auto simp: convex_imp_simply_connected) next case greater thenshow ?thesis using simply_connected_sphere_gen [of "cball a r"] assms by (simp add: aff_dim_cball) qed
lemma simply_connected_sphere_eq: fixes a :: "'a::euclidean_space" shows"simply_connected(sphere a r) ⟷ 3 ≤ DIM('a) ∨ r ≤ 0" (is"?lhs = ?rhs") proof (cases "r ≤ 0") case True have"simply_connected (sphere a r)" using True less_eq_real_def by (auto intro: convex_imp_simply_connected) with True show ?thesis by auto next case False show ?thesis proof assume L: ?lhs have"False"if"DIM('a) = 1 ∨ DIM('a) = 2" using that proof assume"DIM('a) = 1" with L show False using connected_sphere_eq simply_connected_imp_connected by (metis False Suc_1 not_less_eq_eq order_refl) next assume"DIM('a) = 2" thenhave"sphere a r homeomorphic sphere (0::complex) 1" by (metis DIM_complex False homeomorphic_spheres_gen not_less zero_less_one) thenhave"simply_connected(sphere (0::complex) 1)" using L homeomorphic_simply_connected_eq by blast thenobtain a::complex where"homotopic_with_canon (λh. True) (sphere 0 1) (sphere 0 1) id (λx. a)" by (metis continuous_on_id' id_apply image_id subset_refl simply_connected_eq_contractible_circlemap) thenshow False using contractible_sphere contractible_def not_one_le_zero by blast qed with False show ?rhs by (metis DIM_ge_Suc0 One_nat_def Suc_1 not_less_eq_eq numeral_3_eq_3 order_antisym_conv) next assume ?rhs with False show ?lhs by (simp add: simply_connected_sphere) qed qed
lemma simply_connected_punctured_universe_eq: fixes a :: "'a::euclidean_space" shows"simply_connected(- {a}) ⟷ 3 ≤ DIM('a)" proof - have [simp]: "a ∈ rel_interior (cball a 1)" by (simp add: rel_interior_nonempty_interior) have [simp]: "affine hull cball a 1 - {a} = -{a}" by (metis Compl_eq_Diff_UNIV aff_dim_cball aff_dim_lt_full not_less_iff_gr_or_eq zero_less_one) have"sphere a 1 homotopy_eqv - {a}" using homotopy_eqv_rel_frontier_punctured_affine_hull [of "cball a 1" a] by auto thenhave"simply_connected(- {a}) ⟷ simply_connected(sphere a 1)" using homotopy_eqv_simple_connectedness by blast alsohave"... ⟷ 3 ≤ DIM('a)" by (simp add: simply_connected_sphere_eq) finallyshow ?thesis . qed
lemma not_simply_connected_circle: fixes a :: complex shows"0 < r ==>¬ simply_connected(sphere a r)" by (simp add: simply_connected_sphere_eq)
proposition simply_connected_punctured_convex: fixes a :: "'a::euclidean_space" assumes"convex S"and 3: "3 ≤ aff_dim S" shows"simply_connected(S - {a})" proof (cases "a ∈ rel_interior S") case True thenobtain e where"a ∈ S""0 < e"and e: "cball a e ∩ affine hull S ⊆ S" by (auto simp: rel_interior_cball) have con: "convex (cball a e ∩ affine hull S)" by (simp add: convex_Int) have bo: "bounded (cball a e ∩ affine hull S)" by (simp add: bounded_Int) have"affine hull S ∩ interior (cball a e) ≠ {}" using‹0 🚫›‹a ∈ S› hull_subset by fastforce thenhave"3 ≤ aff_dim (affine hull S ∩ cball a e)" by (simp add: 3 aff_dim_convex_Int_nonempty_interior [OF convex_affine_hull]) alsohave"... = aff_dim (cball a e ∩ affine hull S)" by (simp add: Int_commute) finallyhave"3 ≤ aff_dim (cball a e ∩ affine hull S)" . moreoverhave"rel_frontier (cball a e ∩ affine hull S) homotopy_eqv S - {a}" proof (rule homotopy_eqv_rel_frontier_punctured_convex) show"a ∈ rel_interior (cball a e ∩ affine hull S)" by (meson IntI Int_mono ‹a ∈ S›‹0 🚫› e ‹cball a e ∩ affine hull S ⊆ S› ball_subset_cball centre_in_cball dual_order.strict_implies_order hull_inc hull_mono mem_rel_interior_ball) have"closed (cball a e ∩ affine hull S)" by blast thenshow"rel_frontier (cball a e ∩ affine hull S) ⊆ S" by (metis Diff_subset closure_closed dual_order.trans e rel_frontier_def) show"S ⊆ affine hull (cball a e ∩ affine hull S)" by (metis (no_types, lifting) IntI ‹a ∈ S›‹0 🚫› affine_hull_convex_Int_nonempty_interior centre_in_ball convex_affine_hull empty_iff hull_subset inf_commute interior_cball subsetCE subsetI) qed (auto simp: assms con bo) ultimatelyshow ?thesis using homotopy_eqv_simple_connectedness simply_connected_sphere_gen [OF con bo] by blast next case False thenhave"rel_interior S ⊆ S - {a}" by (simp add: False rel_interior_subset subset_Diff_insert) moreoverhave"S - {a} ⊆ closure S" by (meson Diff_subset closure_subset subset_trans) ultimatelyshow ?thesis by (metis contractible_imp_simply_connected contractible_convex_tweak_boundary_points [OF ‹convex S›]) qed
corollary simply_connected_punctured_universe: fixes a :: "'a::euclidean_space" assumes"3 ≤ DIM('a)" shows"simply_connected(- {a})" proof - have [simp]: "affine hull cball a 1 = UNIV" by (simp add: aff_dim_cball affine_hull_UNIV) have"a ∈ rel_interior (cball a 1)" by (simp add: rel_interior_interior) then have"simply_connected (rel_frontier (cball a 1)) = simply_connected (affine hull cball a 1 - {a})" using homotopy_eqv_rel_frontier_punctured_affine_hull homotopy_eqv_simple_connectedness by blast thenshow ?thesis using simply_connected_sphere [of a 1, OF assms] by (auto simp: Compl_eq_Diff_UNIV) qed
subsection‹The power, squaring and exponential functions as covering maps›
proposition covering_space_power_punctured_plane: assumes"0 < n" shows"covering_space (- {0}) (λz::complex. z^n) (- {0})" proof -
consider "n = 1" | "2 ≤ n"using assms by linarith thenobtain e where"0 < e" and e: "∧w z. cmod(w - z) < e * cmod z ==> (w^n = z^n ⟷ w = z)" proof cases assume"n = 1"thenshow ?thesis by (rule_tac e=1 in that) auto next assume"2 ≤ n" have eq_if_pow_eq: "w = z"if lt: "cmod (w - z) < 2 * sin (pi / real n) * cmod z" and eq: "w^n = z^n"for w z proof (cases "z = 0") case True with eq assms show ?thesis by (auto simp: power_0_left) next case False thenhave"z ≠ 0"by auto have"(w/z)^n = 1" by (metis False divide_self_if eq power_divide power_one) thenobtain j::nat where j: "w / z = exp (2 * of_real pi * i * j / n)"and"j < n" using Suc_leI assms ‹2 ≤ n› complex_roots_unity [THEN eqset_imp_iff, of n "w/z"] by force have"cmod (w/z - 1) < 2 * sin (pi / real n)" using lt assms ‹z ≠ 0›by (simp add: field_split_simps norm_divide) thenhave"cmod (exp (i * of_real (2 * pi * j / n)) - 1) < 2 * sin (pi / real n)" by (simp add: j field_simps) thenhave"2 * ∣sin((2 * pi * j / n) / 2)∣ < 2 * sin (pi / real n)" by (simp only: dist_exp_i_1) thenhave sin_less: "sin((pi * j / n)) < sin (pi / real n)" by (simp add: field_simps) thenhave"w / z = 1" proof (cases "j = 0") case True thenshow ?thesis by (auto simp: j) next case False thenhave"sin (pi / real n) ≤ sin((pi * j / n))" proof (cases "j / n ≤ 1/2") case True show ?thesis using‹j ≠ 0›‹j 🚫› True by (intro sin_monotone_2pi_le) (auto simp: field_simps intro: order_trans [of _ 0]) next case False thenhave seq: "sin(pi * j / n) = sin(pi * (n - j) / n)" using‹j 🚫›by (simp add: algebra_simps diff_divide_distrib of_nat_diff)
show ?thesis unfolding seq proof (intro sin_monotone_2pi_le) show"- (pi / 2) ≤ pi / real n" by (smt (verit) divide_nonneg_nonneg of_nat_0_le_iff pi_ge_zero) qed (use‹j 🚫› False in‹auto simp: divide_simps›) qed with sin_less show ?thesis by force qed thenshow ?thesis by simp qed show ?thesis proof show"0 < 2 * sin (pi / real n)" by (force simp: ‹2 ≤ n› sin_pi_divide_n_gt_0) qed (meson eq_if_pow_eq) qed have zn1: "continuous_on (- {0}) (λz::complex. z^n)" by (rule continuous_intros)+ have zn2: "(λz::complex. z^n) ` (- {0}) = - {0}" using assms by (auto simp: image_def elim: exists_complex_root_nonzero [where n = n]) have zn3: "∃T. z^n ∈ T ∧ open T ∧ 0 ∉ T ∧ (∃v. ∪v = -{0} ∩ (λz. z ^ n) -` T ∧ (∀u∈v. open u ∧ 0 ∉ u) ∧ pairwise disjnt v ∧ (∀u∈v. Ex (homeomorphism u T (λz. z^n))))" if"z ≠ 0"for z::complex proof -
define d where"d ≡ min (1/2) (e/4) * norm z" have"0 < d" by (simp add: d_def ‹0 🚫›‹z ≠ 0›) have iff_x_eq_y: "x^n = y^n ⟷ x = y" if eq: "w^n = z^n"and x: "x ∈ ball w d"and y: "y ∈ ball w d"for w x y proof - have [simp]: "norm z = norm w"using that by (simp add: assms power_eq_imp_eq_norm) show ?thesis proof (cases "w = 0") case True with‹z ≠ 0› assms eq show ?thesis by (auto simp: power_0_left) next case False have"cmod (x - y) < 2*d" using x y by (simp add: dist_norm [symmetric]) (metis dist_commute mult_2 dist_triangle_less_add) alsohave"... ≤ 2 * e / 4 * norm w" using‹e > 0›by (simp add: d_def min_mult_distrib_right) alsohave"... = e * (cmod w / 2)" by simp alsohave"... ≤ e * cmod y" proof (rule mult_left_mono) have"cmod (w - y) < cmod w / 2 ==> cmod w / 2 ≤ cmod y" by (metis (no_types) dist_0_norm dist_norm norm_triangle_half_l not_le order_less_irrefl) thenshow"cmod w / 2 ≤ cmod y" using y by (simp add: dist_norm d_def min_mult_distrib_right) qed (use‹e > 0›in auto) finallyhave"cmod (x - y) < e * cmod y" . thenshow ?thesis by (rule e) qed qed thenhave inj: "inj_on (λw. w^n) (ball z d)" by (simp add: inj_on_def) have cont: "continuous_on (ball z d) (λw. w ^ n)" by (intro continuous_intros) have noncon: "¬ (λw::complex. w^n) constant_on UNIV" by (metis UNIV_I assms constant_on_def power_one zero_neq_one zero_power) have im_eq: "(λw. w^n) ` ball z' d = (λw. w^n) ` ball z d" if z': "z'^n = z^n"for z' proof - have nz': "norm z' = norm z"using that assms power_eq_imp_eq_norm by blast have"(w ∈ (λw. w^n) ` ball z' d) = (w ∈ (λw. w^n) ` ball z d)"for w proof (cases "w=0") case True with assms show ?thesis by (simp add: image_def ball_def nz') next case False have"z' ≠ 0"using‹z ≠ 0› nz' by force have 1: "(z*x / z')^n = x^n"if"x ≠ 0"for x using z' that by (simp add: field_simps ‹z ≠ 0›) have 2: "cmod (z - z * x / z') = cmod (z' - x)"if"x ≠ 0"for x proof - have"cmod (z - z * x / z') = cmod z * cmod (1 - x / z')" by (metis (no_types) ab_semigroup_mult_class.mult_ac(1) divide_complex_def mult.right_neutral norm_mult right_diff_distrib') alsohave"... = cmod z' * cmod (1 - x / z')" by (simp add: nz') alsohave"... = cmod (z' - x)" by (simp add: ‹z' ≠ 0› diff_divide_eq_iff norm_divide) finallyshow ?thesis . qed have 3: "(z'*x / z)^n = x^n"if"x ≠ 0"for x using z' that by (simp add: field_simps ‹z ≠ 0›) have 4: "cmod (z' - z' * x / z) = cmod (z - x)"if"x ≠ 0"for x proof - have"cmod (z * (1 - x * inverse z)) = cmod (z - x)" by (metis ‹z ≠ 0› diff_divide_distrib divide_complex_def divide_self_if nonzero_eq_divide_eq semiring_normalization_rules(7)) thenshow ?thesis by (metis (no_types) mult.assoc divide_complex_def mult.right_neutral norm_mult nz' right_diff_distrib') qed show ?thesis by (simp add: set_eq_iff image_def ball_def) (metis 1 2 3 4 diff_zero dist_norm nz') qed thenshow ?thesis by blast qed
have ex_ball: "∃B. (∃z'. B = ball z' d ∧ z'^n = z^n) ∧ x ∈ B" if"x ≠ 0"and eq: "x^n = w^n"and dzw: "dist z w < d"for x w proof - have"w ≠ 0"by (metis assms power_eq_0_iff that(1) that(2)) have [simp]: "cmod x = cmod w" using assms power_eq_imp_eq_norm eq by blast have [simp]: "cmod (x * z / w - x) = cmod (z - w)" proof - have"cmod (x * z / w - x) = cmod x * cmod (z / w - 1)" by (metis (no_types) mult.right_neutral norm_mult right_diff_distrib' times_divide_eq_right) alsohave"... = cmod w * cmod (z / w - 1)" by simp alsohave"... = cmod (z - w)" by (simp add: ‹w ≠ 0› divide_diff_eq_iff nonzero_norm_divide) finallyshow ?thesis . qed show ?thesis proof (intro exI conjI) show"(z / w * x) ^ n = z ^ n" by (metis ‹w ≠ 0› eq nonzero_eq_divide_eq power_mult_distrib) show"x ∈ ball (z / w * x) d" using‹d > 0› that by (simp add: ball_eq_ball_iff ‹z ≠ 0›‹w ≠ 0› field_simps) (simp add: dist_norm) qed auto qed
show ?thesis proof (rule exI, intro conjI) show"z ^ n ∈ (λw. w ^ n) ` ball z d" using‹d > 0›by simp show"open ((λw. w ^ n) ` ball z d)" by (rule invariance_of_domain [OF cont open_ball inj]) show"0 ∉ (λw. w ^ n) ` ball z d" using‹z ≠ 0› assms by (force simp: d_def) show"∃v. ∪v = - {0} ∩ (λz. z ^ n) -` (λw. w ^ n) ` ball z d ∧ (∀u∈v. open u ∧ 0 ∉ u) ∧ disjoint v ∧ (∀u∈v. Ex (homeomorphism u ((λw. w ^ n) ` ball z d) (λz. z ^ n)))" proof (rule exI, intro ballI conjI) show"∪{ball z' d |z'. z'^n = z^n} = - {0} ∩ (λz. z ^ n) -` (λw. w ^ n) ` ball z d"(is"?l = ?r") proof have"∧z'. cmod z' < d ==> z' ^ n ≠ z ^ n" by (auto simp add: assms d_def power_eq_imp_eq_norm that) thenshow"?l ⊆ ?r" by auto (metis im_eq image_eqI mem_ball) show"?r ⊆ ?l" by auto (meson ex_ball) qed show"∧u. u ∈ {ball z' d |z'. z' ^ n = z ^ n} ==> 0 ∉ u" by (force simp add: assms d_def power_eq_imp_eq_norm that)
show"disjoint {ball z' d |z'. z' ^ n = z ^ n}" proof (clarsimp simp add: pairwise_def disjnt_iff) fix ξ ζ x assume"ξ^n = z^n""ζ^n = z^n""ball ξ d ≠ ball ζ d" and"dist ξ x < d""dist ζ x < d" thenhave"dist ξ ζ < d+d" using dist_triangle_less_add by blast thenhave"cmod (ξ - ζ) < 2*d" by (simp add: dist_norm) alsohave"... ≤ e * cmod z" using mult_right_mono ‹0 🚫› that by (auto simp: d_def) finallyhave"cmod (ξ - ζ) < e * cmod z" . with e have"ξ = ζ" by (metis ‹ξ^n = z^n›‹ζ^n = z^n› assms power_eq_imp_eq_norm) thenshow"False" using‹ball ξ d ≠ ball ζ d›by blast qed show"Ex (homeomorphism u ((λw. w ^ n) ` ball z d) (λz. z ^ n))" if"u ∈ {ball z' d |z'. z' ^ n = z ^ n}"for u proof (rule invariance_of_domain_homeomorphism [of "u""λz. z^n"]) show"open u" using that by auto show"continuous_on u (λz. z ^ n)" by (intro continuous_intros) show"inj_on (λz. z ^ n) u" using that by (auto simp: iff_x_eq_y inj_on_def) show"∧g. homeomorphism u ((λz. z ^ n) ` u) (λz. z ^ n) g ==> Ex (homeomorphism u ((λw. w ^ n) ` ball z d) (λz. z ^ n))" using im_eq that by clarify metis qed auto qed auto qed qed show ?thesis using assms apply (simp add: covering_space_def zn1 zn2) apply (subst zn2 [symmetric]) apply (simp add: openin_open_eq open_Compl zn3) done qed
proposition covering_space_exp_punctured_plane: "covering_space UNIV (λz::complex. exp z) (- {0})" proof (simp add: covering_space_def, intro conjI ballI) show"continuous_on UNIV (λz::complex. exp z)" by (rule continuous_on_exp [OF continuous_on_id]) show"range exp = - {0::complex}" by auto (metis exp_Ln range_eqI) show"∃T. z ∈ T ∧ openin (top_of_set (- {0})) T ∧ (∃v. ∪v = exp -` T ∧ (∀u∈v. open u) ∧ disjoint v ∧ (∀u∈v. ∃q. homeomorphism u T exp q))" if"z ∈ - {0::complex}"for z proof - have"z ≠ 0" using that by auto have"ball (Ln z) 1 ⊆ ball (Ln z) pi" using pi_ge_two by (simp add: ball_subset_ball_iff) thenhave inj_exp: "inj_on exp (ball (Ln z) 1)" using inj_on_exp_pi inj_on_subset by blast
define twopi where"twopi ≡ λn. of_real (2 * of_int n * pi) * i"
define Vwhere"V≡ range (λn. (λx. x + twopi n) ` (ball(Ln z) 1))" have exp_eq': "exp w = exp z ⟷ (∃n::int. w = z + twopi n)"for z w by (simp add: exp_eq twopi_def) show ?thesis proof (intro exI conjI) show"z ∈ exp ` (ball(Ln z) 1)" by (metis ‹z ≠ 0› centre_in_ball exp_Ln rev_image_eqI zero_less_one) have"open (- {0::complex})" by blast with inj_exp show"openin (top_of_set (- {0})) (exp ` ball (Ln z) 1)" by (auto simp: openin_open_eq invariance_of_domain continuous_on_exp [OF continuous_on_id]) show UV: "∪V = exp -` exp ` ball (Ln z) 1" by (force simp: V_def twopi_def Complex_Transcendental.exp_eq image_iff) show"∀V∈V. open V" by (auto simp: V_def inj_on_def continuous_intros invariance_of_domain) have"2 ≤ cmod (twopi m -twopi n)"if"m ≠ n"for m n proof - have"1 ≤ abs (m - n)" using that by linarith thenhave"1 ≤ cmod (of_int m - of_int n) * 1" by (metis mult.right_neutral norm_of_int of_int_1_le_iff of_int_abs of_int_diff) alsohave"... ≤ cmod (of_int m - of_int n) * of_real pi" using pi_ge_two by (intro mult_left_mono) auto alsohave"... ≤ cmod ((of_int m - of_int n) * of_real pi * i)" by (simp add: norm_mult) alsohave"... ≤ cmod (of_int m * of_real pi * i - of_int n * of_real pi * i)" by (simp add: algebra_simps) finallyhave"1 ≤ cmod (of_int m * of_real pi * i - of_int n * of_real pi * i)" . thenhave"2 * 1 ≤ cmod (2 * (of_int m * of_real pi * i - of_int n * of_real pi * i))" by (metis mult_le_cancel_left_pos norm_mult_numeral1 zero_less_numeral) thenshow ?thesis by (simp add: algebra_simps twopi_def) qed thenshow"disjoint V" unfoldingV_def pairwise_def disjnt_iff by (smt (verit, best) add.commute add_diff_cancel_left' add_diff_eq dist_commute dist_complex_def dist_triangle imageE mem_ball) show"∀u∈V. ∃q. homeomorphism u (exp ` ball (Ln z) 1) exp q" proof fix u assume"u ∈V" thenobtain n where n: "u = (λx. x + twopi n) ` (ball(Ln z) 1)" by (auto simp: V_def) have"compact (cball (Ln z) 1)" by simp moreoverhave"continuous_on (cball (Ln z) 1) exp" by (rule continuous_on_exp [OF continuous_on_id]) moreoverhave"inj_on exp (cball (Ln z) 1)" using pi_ge_two inj_on_subset [OF inj_on_exp_pi [of "Ln z"]] by (simp add: subset_iff) ultimatelyobtain γ where hom: "homeomorphism (cball (Ln z) 1) (exp ` cball (Ln z) 1) exp γ" using homeomorphism_compact by blast have eq1: "exp ` u = exp ` ball (Ln z) 1" by (smt (verit) n exp_eq' image_cong image_image) have γexp: "γ (exp x) + twopi n = x"if"x ∈ u"for x proof - have"exp x = exp (x - twopi n)" using exp_eq' by auto thenhave"γ (exp x) = γ (exp (x - twopi n))" by simp alsohave"... = x - twopi n" using‹x ∈ u›by (auto simp: n intro: homeomorphism_apply1 [OF hom]) finallyshow ?thesis by simp qed have exp2n: "exp (γ (exp x) + twopi n) = exp x"if"dist (Ln z) x < 1"for x by (metis γexp exp_eq' imageI mem_ball n that) have"continuous_on (exp ` ball (Ln z) 1) γ" by (meson ball_subset_cball continuous_on_subset hom homeomorphism_cont2 image_mono) thenhave cont: "continuous_on (exp ` ball (Ln z) 1) (λx. γ x + twopi n)" by (intro continuous_intros) have"homeomorphism u (exp ` ball (Ln z) 1) exp ((λx. x + twopi n) ∘ γ)" unfolding homeomorphism_def apply (intro conjI ballI eq1 continuous_on_exp [OF continuous_on_id]) apply (auto simp: γexp exp2n cont n) apply (force simp: image_iff homeomorphism_apply1 [OF hom])+ done thenshow"∃q. homeomorphism u (exp ` ball (Ln z) 1) exp q"by metis qed qed qed qed
subsection‹Hence the Borsukian results about mappings into circles›(*FIX ME title *)
lemma inessential_eq_continuous_logarithm: fixes f :: "'a::real_normed_vector ==> complex" shows"(∃a. homotopic_with_canon (λh. True) S (-{0}) f (λt. a)) ⟷ (∃g. continuous_on S g ∧ (∀x ∈ S. f x = exp(g x)))"
(is"?lhs ⟷ ?rhs") proof assume ?lhs thus ?rhs by (metis covering_space_lift_inessential_function covering_space_exp_punctured_plane) next assume ?rhs thenobtain g where contg: "continuous_on S g"and f: "∧x. x ∈ S ==> f x = exp(g x)" by metis obtain a where"homotopic_with_canon (λh. True) S (- {of_real 0}) (exp ∘ g) (λx. a)" proof (rule nullhomotopic_through_contractible [OF contg _ _ _ contractible_UNIV]) show"continuous_on (UNIV::complex set) exp" by (intro continuous_intros) show"exp ∈ UNIV → -{of_real 0}" by auto qed force thenhave"homotopic_with_canon (λh. True) S (- {0}) f (λt. a)" using f homotopic_with_eq by fastforce thenshow ?lhs .. qed
corollary inessential_imp_continuous_logarithm_circle: fixes f :: "'a::real_normed_vector ==> complex" assumes"homotopic_with_canon (λh. True) S (sphere 0 1) f (λt. a)" obtains g where"continuous_on S g"and"∧x. x ∈ S ==> f x = exp(g x)" proof - have"homotopic_with_canon (λh. True) S (- {0}) f (λt. a)" using assms homotopic_with_subset_right by fastforce thenshow ?thesis by (metis inessential_eq_continuous_logarithm that) qed
lemma inessential_eq_continuous_logarithm_circle: fixes f :: "'a::real_normed_vector ==> complex" shows"(∃a. homotopic_with_canon (λh. True) S (sphere 0 1) f (λt. a)) ⟷ (∃g. continuous_on S g ∧ (∀x ∈ S. f x = exp(i * of_real(g x))))"
(is"?lhs ⟷ ?rhs") proof assume L: ?lhs thenobtain g where contg: "continuous_on S g"and g: "∧x. x ∈ S ==> f x = exp(g x)" using inessential_imp_continuous_logarithm_circle by blast have"f ∈ S → sphere 0 1" by (metis L image_subset_iff_funcset homotopic_with_imp_subset1) thenhave"∧x. x ∈ S ==> Re (g x) = 0" using g by (simp add: Pi_iff) thenshow ?rhs by (rule_tac x="Im ∘ g"in exI) (auto simp: Euler g intro: contg continuous_intros) next assume ?rhs thenobtain g where contg: "continuous_on S g"and g: "∧x. x ∈ S ==> f x = exp(i* of_real(g x))" by metis obtain a where"homotopic_with_canon (λh. True) S (sphere 0 1) ((exp ∘ (λz. i*z)) ∘ (of_real ∘ g)) (λx. a)" proof (rule nullhomotopic_through_contractible) show"continuous_on S (complex_of_real ∘ g)" by (intro conjI contg continuous_intros) show"(complex_of_real ∘ g) ∈ S →ℝ" by auto show"continuous_on ℝ (exp ∘ (*)i)" by (intro continuous_intros) show"(exp ∘ (*)i) ∈ℝ→ sphere 0 1" by (auto simp: complex_is_Real_iff) qed (auto simp: convex_Reals convex_imp_contractible) moreoverhave"∧x. x ∈ S ==> (exp ∘ (*)i∘ (complex_of_real ∘ g)) x = f x" by (simp add: g) ultimatelyhave"homotopic_with_canon (λh. True) S (sphere 0 1) f (λt. a)" using homotopic_with_eq by force thenshow ?lhs .. qed
proposition homotopic_with_sphere_times: fixes f :: "'a::real_normed_vector ==> complex" assumes hom: "homotopic_with_canon (λx. True) S (sphere 0 1) f g"and conth: "continuous_on S h" and hin: "∧x. x ∈ S ==> h x ∈ sphere 0 1" shows"homotopic_with_canon (λx. True) S (sphere 0 1) (λx. f x * h x) (λx. g x * h x)" proof - obtain k where contk: "continuous_on ({0..1::real} × S) k" and kim: "k ∈ ({0..1} × S) → sphere 0 1" and k0: "∧x. k(0, x) = f x" and k1: "∧x. k(1, x) = g x" using hom by (auto simp: homotopic_with_def) show ?thesis apply (simp add: homotopic_with) apply (rule_tac x="λz. k z * (h ∘ snd)z"in exI) using kim hin by (fastforce simp: conth norm_mult k0 k1 intro!: contk continuous_intros)+ qed
proposition homotopic_circlemaps_divide: fixes f :: "'a::real_normed_vector ==> complex" shows"homotopic_with_canon (λx. True) S (sphere 0 1) f g ⟷ continuous_on S f ∧ f ∈ S → sphere 0 1 ∧ continuous_on S g ∧ g ∈ S → sphere 0 1 ∧ (∃c. homotopic_with_canon (λx. True) S (sphere 0 1) (λx. f x / g x) (λx. c))" proof - have"homotopic_with_canon (λx. True) S (sphere 0 1) (λx. f x / g x) (λx. 1)" if"homotopic_with_canon (λx. True) S (sphere 0 1) (λx. f x / g x) (λx. c)"for c proof - have"S = {} ∨ path_component (sphere 0 1) 1 c" using homotopic_with_imp_subset2 [OF that] path_connected_sphere [of "0::complex" 1] by (auto simp: path_connected_component) with subtopology_empty_iff_trivial have"homotopic_with_canon (λx. True) S (sphere 0 1) (λx. 1) (λx. c)" by (force simp add: homotopic_constant_maps) thenshow ?thesis using homotopic_with_symD homotopic_with_trans that by blast qed thenhave *: "(∃c. homotopic_with_canon (λx. True) S (sphere 0 1) (λx. f x / g x) (λx. c)) ⟷ homotopic_with_canon (λx. True) S (sphere 0 1) (λx. f x / g x) (λx. 1)" by auto have"homotopic_with_canon (λx. True) S (sphere 0 1) f g ⟷ continuous_on S f ∧ f ∈ S → sphere 0 1 ∧ continuous_on S g ∧ g ∈ S → sphere 0 1 ∧ homotopic_with_canon (λx. True) S (sphere 0 1) (λx. f x / g x) (λx. 1)"
(is"?lhs ⟷ ?rhs") proof assume L: ?lhs have geq1 [simp]: "∧x. x ∈ S ==> cmod (g x) = 1" using homotopic_with_imp_subset2 [OF L] by (simp add: image_subset_iff) have cont: "continuous_on S (inverse ∘ g)" proof (rule continuous_intros) show"continuous_on S g" using homotopic_with_imp_continuous [OF L] by blast show"continuous_on (g ` S) inverse" by (rule continuous_on_subset [of "sphere 0 1", OF continuous_on_inverse]) auto qed have [simp]: "∧x. x ∈ S ==> g x ≠ 0" using geq1 by fastforce have"homotopic_with_canon (λx. True) S (sphere 0 1) (λx. f x / g x) (λx. 1)" using homotopic_with_eq [OF homotopic_with_sphere_times [OF L cont]] by (auto simp: divide_inverse norm_inverse) with L show ?rhs by (simp add: homotopic_with_imp_continuous homotopic_with_imp_funspace1) next assume ?rhs thenshow ?lhs by (elim conjE homotopic_with_eq [OF homotopic_with_sphere_times]; force) qed thenshow ?thesis by (simp add: *) qed
subsection‹Upper and lower hemicontinuous functions›
text‹And relation in the case of preimage map to open and closed maps, and fact that upper and lower hemicontinuity together imply continuity in the sense of the Hausdorff metric (at points where the function gives a bounded and nonempty set).›
text‹Many similar proofs below.› lemma upper_hemicontinuous: assumes"∧x. x ∈ S ==> f x ⊆ T" shows"((∀U. openin (top_of_set T) U ⟶ openin (top_of_set S) {x ∈ S. f x ⊆ U}) ⟷ (∀U. closedin (top_of_set T) U ⟶ closedin (top_of_set S) {x ∈ S. f x ∩ U ≠ {}}))"
(is"?lhs = ?rhs") proof (intro iffI allI impI) fix U assume * [rule_format]: ?lhs and"closedin (top_of_set T) U" thenhave"openin (top_of_set T) (T - U)" by (simp add: openin_diff) thenhave"openin (top_of_set S) {x ∈ S. f x ⊆ T - U}" using * [of "T-U"] by blast moreoverhave"S - {x ∈ S. f x ⊆ T - U} = {x ∈ S. f x ∩ U ≠ {}}" using assms by blast ultimatelyshow"closedin (top_of_set S) {x ∈ S. f x ∩ U ≠ {}}" by (simp add: openin_closedin_eq) next fix U assume * [rule_format]: ?rhs and"openin (top_of_set T) U" thenhave"closedin (top_of_set T) (T - U)" by (simp add: closedin_diff) thenhave"closedin (top_of_set S) {x ∈ S. f x ∩ (T - U) ≠ {}}" using * [of "T-U"] by blast moreoverhave"{x ∈ S. f x ∩ (T - U) ≠ {}} = S - {x ∈ S. f x ⊆ U}" using assms by auto ultimatelyshow"openin (top_of_set S) {x ∈ S. f x ⊆ U}" by (simp add: openin_closedin_eq) qed
lemma lower_hemicontinuous: assumes"∧x. x ∈ S ==> f x ⊆ T" shows"((∀U. closedin (top_of_set T) U ⟶ closedin (top_of_set S) {x ∈ S. f x ⊆ U}) ⟷ (∀U. openin (top_of_set T) U ⟶ openin (top_of_set S) {x ∈ S. f x ∩ U ≠ {}}))"
(is"?lhs = ?rhs") proof (intro iffI allI impI) fix U assume * [rule_format]: ?lhs and"openin (top_of_set T) U" thenhave"closedin (top_of_set T) (T - U)" by (simp add: closedin_diff) thenhave"closedin (top_of_set S) {x ∈ S. f x ⊆ T-U}" using * [of "T-U"] by blast moreoverhave"{x ∈ S. f x ⊆ T-U} = S - {x ∈ S. f x ∩ U ≠ {}}" using assms by auto ultimatelyshow"openin (top_of_set S) {x ∈ S. f x ∩ U ≠ {}}" by (simp add: openin_closedin_eq) next fix U assume * [rule_format]: ?rhs and"closedin (top_of_set T) U" thenhave"openin (top_of_set T) (T - U)" by (simp add: openin_diff) thenhave"openin (top_of_set S) {x ∈ S. f x ∩ (T - U) ≠ {}}" using * [of "T-U"] by blast moreoverhave"S - {x ∈ S. f x ∩ (T - U) ≠ {}} = {x ∈ S. f x ⊆ U}" using assms by blast ultimatelyshow"closedin (top_of_set S) {x ∈ S. f x ⊆ U}" by (simp add: openin_closedin_eq) qed
lemma open_map_iff_lower_hemicontinuous_preimage: assumes"f ∈ S → T" shows"((∀U. openin (top_of_set S) U ⟶ openin (top_of_set T) (f ` U)) ⟷ (∀U. closedin (top_of_set S) U ⟶ closedin (top_of_set T) {y ∈ T. {x. x ∈ S ∧ f x = y} ⊆ U}))"
(is"?lhs = ?rhs") proof (intro iffI allI impI) fix U assume * [rule_format]: ?lhs and"closedin (top_of_set S) U" thenhave"openin (top_of_set S) (S - U)" by (simp add: openin_diff) thenhave"openin (top_of_set T) (f ` (S - U))" using * [of "S-U"] by blast moreoverhave"T - (f ` (S - U)) = {y ∈ T. {x ∈ S. f x = y} ⊆ U}" using assms by blast ultimatelyshow"closedin (top_of_set T) {y ∈ T. {x ∈ S. f x = y} ⊆ U}" by (simp add: openin_closedin_eq) next fix U assume * [rule_format]: ?rhs and opeSU: "openin (top_of_set S) U" thenhave"closedin (top_of_set S) (S - U)" by (simp add: closedin_diff) thenhave"closedin (top_of_set T) {y ∈ T. {x ∈ S. f x = y} ⊆ S - U}" using * [of "S-U"] by blast moreoverhave"{y ∈ T. {x ∈ S. f x = y} ⊆ S - U} = T - (f ` U)" using assms openin_imp_subset [OF opeSU] by auto ultimatelyshow"openin (top_of_set T) (f ` U)" using assms openin_imp_subset [OF opeSU] by (force simp: openin_closedin_eq) qed
lemma closed_map_iff_upper_hemicontinuous_preimage: assumes"f ∈ S → T" shows"((∀U. closedin (top_of_set S) U ⟶ closedin (top_of_set T) (f ` U)) ⟷ (∀U. openin (top_of_set S) U ⟶ openin (top_of_set T) {y ∈ T. {x. x ∈ S ∧ f x = y} ⊆ U}))"
(is"?lhs = ?rhs") proof (intro iffI allI impI) fix U assume * [rule_format]: ?lhs and opeSU: "openin (top_of_set S) U" thenhave"closedin (top_of_set S) (S - U)" by (simp add: closedin_diff) thenhave"closedin (top_of_set T) (f ` (S - U))" using * [of "S-U"] by blast moreoverhave"f ` (S - U) = T - {y ∈ T. {x. x ∈ S ∧ f x = y} ⊆ U}" using assms openin_imp_subset [OF opeSU] by auto ultimatelyshow"openin (top_of_set T) {y ∈ T. {x. x ∈ S ∧ f x = y} ⊆ U}" using assms openin_imp_subset [OF opeSU] by (force simp: openin_closedin_eq) next fix U assume * [rule_format]: ?rhs and cloSU: "closedin (top_of_set S) U" thenhave"openin (top_of_set S) (S - U)" by (simp add: openin_diff) thenhave"openin (top_of_set T) {y ∈ T. {x ∈ S. f x = y} ⊆ S - U}" using * [of "S-U"] by blast moreoverhave"(f ` U) = T - {y ∈ T. {x ∈ S. f x = y} ⊆ S - U}" using assms closedin_imp_subset [OF cloSU] by auto ultimatelyshow"closedin (top_of_set T) (f ` U)" by (simp add: openin_closedin_eq) qed
proposition upper_lower_hemicontinuous_explicit: fixes T :: "('b::{real_normed_vector,heine_borel}) set" assumes fST: "∧x. x ∈ S ==> f x ⊆ T" and ope: "∧U. openin (top_of_set T) U ==> openin (top_of_set S) {x ∈ S. f x ⊆ U}" and clo: "∧U. closedin (top_of_set T) U ==> closedin (top_of_set S) {x ∈ S. f x ⊆ U}" and"x ∈ S""0 < e"and bofx: "bounded(f x)"and fx_ne: "f x ≠ {}" obtains d where"0 < d" "∧x'. [x' ∈ S; dist x x' < d] ==> (∀y ∈ f x. ∃y'. y' ∈ f x' ∧ dist y y' < e) ∧ (∀y' ∈ f x'. ∃y. y ∈ f x ∧ dist y' y < e)" proof - have"openin (top_of_set T) (T ∩ (∪a∈f x. ∪b∈ball 0 e. {a + b}))" by (auto simp: open_sums openin_open_Int) with ope have"openin (top_of_set S) {u ∈ S. f u ⊆ T ∩ (∪a∈f x. ∪b∈ball 0 e. {a + b})}"by blast with‹0 🚫›‹x ∈ S›obtain d1 where"d1 > 0"and
d1: "∧x'. [x' ∈ S; dist x' x < d1]==> f x' ⊆ T ∧ f x' ⊆ (∪a ∈ f x. ∪b ∈ ball 0 e. {a + b})" by (force simp: openin_euclidean_subtopology_iff dest: fST) have oo: "∧U. openin (top_of_set T) U ==> openin (top_of_set S) {x ∈ S. f x ∩ U ≠ {}}" using lower_hemicontinuous fST clo by blast have"compact (closure(f x))" by (simp add: bofx) moreoverhave"closure(f x) ⊆ (∪a ∈ f x. ball a (e/2))" using‹0 🚫›by (force simp: closure_approachable simp del: divide_const_simps) ultimatelyobtain C where"C ⊆ f x""finite C""closure(f x) ⊆ (∪a ∈ C. ball a (e/2))" by (meson compactE finite_subset_image Elementary_Metric_Spaces.open_ball compactE_image) thenhave fx_cover: "f x ⊆ (∪a ∈ C. ball a (e/2))" by (meson closure_subset order_trans) with fx_ne have"C ≠ {}" by blast have xin: "x ∈ (∩a ∈ C. {x ∈ S. f x ∩ T ∩ ball a (e/2) ≠ {}})" using‹x ∈ S›‹0 🚫› fST ‹C ⊆ f x›by force have"openin (top_of_set S) {x ∈ S. f x ∩ (T ∩ ball a (e/2)) ≠ {}}"for a by (simp add: openin_open_Int oo) thenhave"openin (top_of_set S) (∩a ∈ C. {x ∈ S. f x ∩ T ∩ ball a (e/2) ≠ {}})" by (simp add: Int_assoc openin_INT2 [OF ‹finite C›‹C ≠ {}›]) with xin obtain d2 where"d2>0" and d2: "∧u v. [u ∈ S; dist u x < d2; v ∈ C]==> f u ∩ T ∩ ball v (e/2) ≠ {}" unfolding openin_euclidean_subtopology_iff using xin by fastforce show ?thesis proof (intro that conjI ballI) show"0 < min d1 d2" using‹0 🚫›‹0 🚫›by linarith next fix x' y assume"x' ∈ S""dist x x' < min d1 d2""y ∈ f x" thenhave dd2: "dist x' x < d2" by (auto simp: dist_commute) obtain a where"a ∈ C""y ∈ ball a (e/2)" using fx_cover ‹y ∈ f x›by auto thenshow"∃y'. y' ∈ f x' ∧ dist y y' < e" using d2 [OF ‹x' ∈ S› dd2] dist_triangle_half_r by fastforce next fix x' y' assume"x' ∈ S""dist x x' < min d1 d2""y' ∈ f x'" thenhave"dist x' x < d1" by (auto simp: dist_commute) thenhave"y' ∈ (∪a∈f x. ∪b∈ball 0 e. {a + b})" using d1 [OF ‹x' ∈ S›] ‹y' ∈ f x'›by force thenshow"∃y. y ∈ f x ∧ dist y' y < e" by clarsimp (metis add_diff_cancel_left' dist_norm) qed qed
subsection‹Complex logs exist on various "well-behaved" sets›
lemma continuous_logarithm_on_contractible: fixes f :: "'a::real_normed_vector ==> complex" assumes"continuous_on S f""contractible S""∧z. z ∈ S ==> f z ≠ 0" obtains g where"continuous_on S g""∧x. x ∈ S ==> f x = exp(g x)" proof - obtain c where hom: "homotopic_with_canon (λh. True) S (-{0}) f (λx. c)" using nullhomotopic_from_contractible assms by (metis imageE subset_Compl_singleton image_subset_iff_funcset) thenshow ?thesis by (metis inessential_eq_continuous_logarithm that) qed
lemma continuous_logarithm_on_simply_connected: fixes f :: "'a::real_normed_vector ==> complex" assumes contf: "continuous_on S f"and S: "simply_connected S""locally path_connected S" and f: "∧z. z ∈ S ==> f z ≠ 0" obtains g where"continuous_on S g""∧x. x ∈ S ==> f x = exp(g x)" using covering_space_lift [OF covering_space_exp_punctured_plane S contf] by (metis (full_types) f imageE subset_Compl_singleton image_subset_iff_funcset)
lemma continuous_logarithm_on_cball: fixes f :: "'a::real_normed_vector ==> complex" assumes"continuous_on (cball a r) f"and"∧z. z ∈ cball a r ==> f z ≠ 0" obtains h where"continuous_on (cball a r) h""∧z. z ∈ cball a r ==> f z = exp(h z)" using assms continuous_logarithm_on_contractible convex_imp_contractible by blast
lemma continuous_logarithm_on_ball: fixes f :: "'a::real_normed_vector ==> complex" assumes"continuous_on (ball a r) f"and"∧z. z ∈ ball a r ==> f z ≠ 0" obtains h where"continuous_on (ball a r) h""∧z. z ∈ ball a r ==> f z = exp(h z)" using assms continuous_logarithm_on_contractible convex_imp_contractible by blast
lemma continuous_sqrt_on_contractible: fixes f :: "'a::real_normed_vector ==> complex" assumes"continuous_on S f""contractible S" and"∧z. z ∈ S ==> f z ≠ 0" obtains g where"continuous_on S g""∧x. x ∈ S ==> f x = (g x) ^ 2" proof - obtain g where contg: "continuous_on S g"and feq: "∧x. x ∈ S ==> f x = exp(g x)" using continuous_logarithm_on_contractible [OF assms] by blast show ?thesis proof show"continuous_on S (λz. exp (g z / 2))" by (rule continuous_on_compose2 [of UNIV exp]; intro continuous_intros contg subset_UNIV) auto show"∧x. x ∈ S ==> f x = (exp (g x / 2))🪙2" by (metis exp_double feq nonzero_mult_div_cancel_left times_divide_eq_right zero_neq_numeral) qed qed
lemma continuous_sqrt_on_simply_connected: fixes f :: "'a::real_normed_vector ==> complex" assumes contf: "continuous_on S f"and S: "simply_connected S""locally path_connected S" and f: "∧z. z ∈ S ==> f z ≠ 0" obtains g where"continuous_on S g""∧x. x ∈ S ==> f x = (g x) ^ 2" proof - obtain g where contg: "continuous_on S g"and feq: "∧x. x ∈ S ==> f x = exp(g x)" using continuous_logarithm_on_simply_connected [OF assms] by blast show ?thesis proof show"continuous_on S (λz. exp (g z / 2))" by (rule continuous_on_compose2 [of UNIV exp]; intro continuous_intros contg subset_UNIV) auto show"∧x. x ∈ S ==> f x = (exp (g x / 2))🪙2" by (metis exp_double feq nonzero_mult_div_cancel_left times_divide_eq_right zero_neq_numeral) qed qed
subsection‹Another simple case where sphere maps are nullhomotopic›
lemma inessential_spheremap_2_aux: fixes f :: "'a::euclidean_space ==> complex" assumes 2: "2 < DIM('a)"and contf: "continuous_on (sphere a r) f" and fim: "f ∈ (sphere a r) → (sphere 0 1)" obtains c where"homotopic_with_canon (λz. True) (sphere a r) (sphere 0 1) f (λx. c)" proof - obtain g where contg: "continuous_on (sphere a r) g" and feq: "∧x. x ∈ sphere a r ==> f x = exp(g x)" proof (rule continuous_logarithm_on_simply_connected [OF contf]) show"simply_connected (sphere a r)" using 2 by (simp add: simply_connected_sphere_eq) show"locally path_connected (sphere a r)" by (simp add: locally_path_connected_sphere) show"∧z. z ∈ sphere a r ==> f z ≠ 0" using fim by force qed auto have"∃g. continuous_on (sphere a r) g ∧ (∀x∈sphere a r. f x = exp (i * complex_of_real (g x)))" proof (intro exI conjI) show"continuous_on (sphere a r) (Im ∘ g)" by (intro contg continuous_intros continuous_on_compose) show"∀x∈sphere a r. f x = exp (i * complex_of_real ((Im ∘ g) x))" using exp_eq_polar feq fim norm_exp_eq_Re by (auto simp flip: image_subset_iff_funcset) qed with inessential_eq_continuous_logarithm_circle that show ?thesis by metis qed
lemma inessential_spheremap_2: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes a2: "2 < DIM('a)"and b2: "DIM('b) = 2" and contf: "continuous_on (sphere a r) f"and fim: "f ∈ (sphere a r) → (sphere b s)" obtains c where"homotopic_with_canon (λz. True) (sphere a r) (sphere b s) f (λx. c)" proof (cases "s ≤ 0") case True thenshow ?thesis using contf contractible_sphere fim nullhomotopic_into_contractible that by blast next case False thenhave"sphere b s homeomorphic sphere (0::complex) 1" using assms by (simp add: homeomorphic_spheres_gen) thenobtain h k where hk: "homeomorphism (sphere b s) (sphere (0::complex) 1) h k" by (auto simp: homeomorphic_def) thenhave conth: "continuous_on (sphere b s) h" and contk: "continuous_on (sphere 0 1) k" and him: "h ∈ sphere b s → sphere 0 1" and kim: "k ∈ sphere 0 1 → sphere b s" by (force simp: homeomorphism_def)+ obtain c where"homotopic_with_canon (λz. True) (sphere a r) (sphere 0 1) (h ∘ f) (λx. c)" proof (rule inessential_spheremap_2_aux [OF a2]) show"continuous_on (sphere a r) (h ∘ f)" by (meson contf conth continuous_on_compose continuous_on_subset fim image_subset_iff_funcset) show"(h ∘ f) ∈ sphere a r → sphere 0 1" using fim him by force qed auto thenhave"homotopic_with_canon (λf. True) (sphere a r) (sphere b s) (k ∘ (h ∘ f)) (k ∘ (λx. c))" by (rule homotopic_with_compose_continuous_left [OF _ contk kim]) moreoverhave"∧x. r = dist a x ==> f x = k (h (f x))" by (metis fim hk homeomorphism_def image_subset_iff mem_sphere image_subset_iff_funcset) ultimatelyhave"homotopic_with_canon (λz. True) (sphere a r) (sphere b s) f (λx. k c)" by (auto intro: homotopic_with_eq) thenshow ?thesis by (metis that) qed
subsection‹Holomorphic logarithms and square roots›
lemma g_imp_holomorphic_log: assumes holf: "f holomorphic_on S" and contg: "continuous_on S g"and feq: "∧x. x ∈ S ==> f x = exp (g x)" and fnz: "∧z. z ∈ S ==> f z ≠ 0" obtains g where"g holomorphic_on S""∧z. z ∈ S ==> f z = exp(g z)" proof - have contf: "continuous_on S f" by (simp add: holf holomorphic_on_imp_continuous_on) have"g field_differentiable at z within S"if"f field_differentiable at z within S""z ∈ S"for z proof - obtain f' where f': "((λy. (f y - f z) / (y - z)) ---> f') (at z within S)" using‹f field_differentiable at z within S›by (auto simp: field_differentiable_def has_field_derivative_iff) thenhave ee: "((λx. (exp(g x) - exp(g z)) / (x - z)) ---> f') (at z within S)" by (simp add: feq ‹z ∈ S› Lim_transform_within [OF _ zero_less_one]) have"(((λy. if y = g z then exp (g z) else (exp y - exp (g z)) / (y - g z)) ∘ g) ---> exp (g z)) (at z within S)" proof (rule tendsto_compose_at) show"(g ---> g z) (at z within S)" using contg continuous_on ‹z ∈ S›by blast show"(λy. if y = g z then exp (g z) else (exp y - exp (g z)) / (y - g z)) ←-g z→ exp (g z)" by (simp add: LIM_offset_zero_iff DERIV_D cong: if_cong Lim_cong_within) qed auto thenhave dd: "((λx. if g x = g z then exp(g z) else (exp(g x) - exp(g z)) / (g x - g z)) ---> exp(g z)) (at z within S)" by (simp add: o_def) have"continuous (at z within S) g" using contg continuous_on_eq_continuous_within ‹z ∈ S›by blast thenhave"(∀🪙F x in at z within S. dist (g x) (g z) < 2*pi)" by (simp add: continuous_within tendsto_iff) thenhave"∀🪙F x in at z within S. exp (g x) = exp (g z) ⟶ g x ≠ g z ⟶ x = z" by (rule eventually_mono) (auto simp: exp_eq dist_norm norm_mult) thenhave"((λy. (g y - g z) / (y - z)) ---> f' / exp (g z)) (at z within S)" by (auto intro!: Lim_transform_eventually [OF tendsto_divide [OF ee dd]]) thenshow ?thesis by (auto simp: field_differentiable_def has_field_derivative_iff) qed thenhave"g holomorphic_on S" using holf holomorphic_on_def by auto thenshow ?thesis using feq that by auto qed
lemma contractible_imp_holomorphic_log: assumes holf: "f holomorphic_on S" and S: "contractible S" and fnz: "∧z. z ∈ S ==> f z ≠ 0" obtains g where"g holomorphic_on S""∧z. z ∈ S ==> f z = exp(g z)" proof - have contf: "continuous_on S f" by (simp add: holf holomorphic_on_imp_continuous_on) obtain g where contg: "continuous_on S g"and feq: "∧x. x ∈ S ==> f x = exp (g x)" by (metis continuous_logarithm_on_contractible [OF contf S fnz]) thenshow thesis using fnz g_imp_holomorphic_log holf that by blast qed
lemma simply_connected_imp_holomorphic_log: assumes holf: "f holomorphic_on S" and S: "simply_connected S""locally path_connected S" and fnz: "∧z. z ∈ S ==> f z ≠ 0" obtains g where"g holomorphic_on S""∧z. z ∈ S ==> f z = exp(g z)" proof - have contf: "continuous_on S f" by (simp add: holf holomorphic_on_imp_continuous_on) obtain g where contg: "continuous_on S g"and feq: "∧x. x ∈ S ==> f x = exp (g x)" by (metis continuous_logarithm_on_simply_connected [OF contf S fnz]) thenshow thesis using fnz g_imp_holomorphic_log holf that by blast qed
lemma contractible_imp_holomorphic_sqrt: assumes holf: "f holomorphic_on S" and S: "contractible S" and fnz: "∧z. z ∈ S ==> f z ≠ 0" obtains g where"g holomorphic_on S""∧z. z ∈ S ==> f z = g z ^ 2" proof - obtain g where holg: "g holomorphic_on S"and feq: "∧z. z ∈ S ==> f z = exp(g z)" using contractible_imp_holomorphic_log [OF assms] by blast show ?thesis proof show"exp ∘ (λz. z / 2) ∘ g holomorphic_on S" by (intro holomorphic_on_compose holg holomorphic_intros) auto show"∧z. z ∈ S ==> f z = ((exp ∘ (λz. z / 2) ∘ g) z)🪙2" by (simp add: feq flip: exp_double) qed qed
lemma simply_connected_imp_holomorphic_sqrt: assumes holf: "f holomorphic_on S" and S: "simply_connected S""locally path_connected S" and fnz: "∧z. z ∈ S ==> f z ≠ 0" obtains g where"g holomorphic_on S""∧z. z ∈ S ==> f z = g z ^ 2" proof - obtain g where holg: "g holomorphic_on S"and feq: "∧z. z ∈ S ==> f z = exp(g z)" using simply_connected_imp_holomorphic_log [OF assms] by blast show ?thesis proof show"exp ∘ (λz. z / 2) ∘ g holomorphic_on S" by (intro holomorphic_on_compose holg holomorphic_intros) auto show"∧z. z ∈ S ==> f z = ((exp ∘ (λz. z / 2) ∘ g) z)🪙2" by (simp add: feq flip: exp_double) qed qed
text‹ Related theorems about holomorphic inverse cosines.›
lemma contractible_imp_holomorphic_arccos: assumes holf: "f holomorphic_on S"and S: "contractible S" and non1: "∧z. z ∈ S ==> f z ≠ 1 ∧ f z ≠ -1" obtains g where"g holomorphic_on S""∧z. z ∈ S ==> f z = cos(g z)" proof - have hol1f: "(λz. 1 - f z ^ 2) holomorphic_on S" by (intro holomorphic_intros holf) obtain g where holg: "g holomorphic_on S"and eq: "∧z. z ∈ S ==> 1 - (f z)🪙2 = (g z)🪙2" using contractible_imp_holomorphic_sqrt [OF hol1f S] by (metis eq_iff_diff_eq_0 non1 power2_eq_1_iff) have holfg: "(λz. f z + i*g z) holomorphic_on S" by (intro holf holg holomorphic_intros) have"∧z. z ∈ S ==> f z + i*g z ≠ 0" by (metis Arccos_body_lemma eq add.commute add.inverse_unique complex_i_mult_minus power2_csqrt power2_eq_iff) thenobtain h where holh: "h holomorphic_on S"and fgeq: "∧z. z ∈ S ==> f z + i*g z = exp (h z)" using contractible_imp_holomorphic_log [OF holfg S] by metis show ?thesis proof show"(λz. -i*h z) holomorphic_on S" by (intro holh holomorphic_intros) show"f z = cos (- i*h z)"if"z ∈ S"for z proof - have"(f z + i*g z)*(f z - i*g z) = 1" using that eq by (auto simp: algebra_simps power2_eq_square) thenhave"f z - i*g z = inverse (f z + i*g z)" using inverse_unique by force alsohave"... = exp (- h z)" by (simp add: exp_minus fgeq that) finallyhave"f z = exp (- h z) + i*g z" by (simp add: diff_eq_eq) with that show ?thesis by (simp add: cos_exp_eq flip: fgeq) qed qed qed
lemma contractible_imp_holomorphic_arccos_bounded: assumes holf: "f holomorphic_on S"and S: "contractible S"and"a ∈ S" and non1: "∧z. z ∈ S ==> f z ≠ 1 ∧ f z ≠ -1" obtains g where"g holomorphic_on S""norm(g a) ≤ pi + norm(f a)""∧z. z ∈ S ==> f z = cos(g z)" proof - obtain g where holg: "g holomorphic_on S"and feq: "∧z. z ∈ S ==> f z = cos (g z)" using contractible_imp_holomorphic_arccos [OF holf S non1] by blast obtain b where"cos b = f a""norm b ≤ pi + norm (f a)" using cos_Arccos norm_Arccos_bounded by blast thenhave"cos b = cos (g a)" by (simp add: ‹a ∈ S› feq) then consider n where"n ∈ℤ""b = g a + of_real(2*n*pi)" | n where"n ∈ℤ""b = -g a + of_real(2*n*pi)" by (auto simp: complex_cos_eq) thenshow ?thesis proof cases case 1 show ?thesis proof show"(λz. g z + of_real(2*n*pi)) holomorphic_on S" by (intro holomorphic_intros holg) show"cmod (g a + of_real(2*n*pi)) ≤ pi + cmod (f a)" using"1"‹cmod b ≤ pi + cmod (f a)›by blast show"∧z. z ∈ S ==> f z = cos (g z + complex_of_real (2*n*pi))" by (metis ‹n ∈ℤ› complex_cos_eq feq) qed next case 2 show ?thesis proof show"(λz. -g z + of_real(2*n*pi)) holomorphic_on S" by (intro holomorphic_intros holg) show"cmod (-g a + of_real(2*n*pi)) ≤ pi + cmod (f a)" using"2"‹cmod b ≤ pi + cmod (f a)›by blast show"∧z. z ∈ S ==> f z = cos (-g z + complex_of_real (2*n*pi))" by (metis ‹n ∈ℤ› complex_cos_eq feq) qed qed qed
subsection‹The "Borsukian" property of sets›
text‹This doesn't have a standard name. Kuratowski uses ``contractible with respect to ‹[S🪙1]›''
while Whyburn uses ``property b''. It's closely related to unicoherence.›
definition🍋‹tag important› Borsukian where "Borsukian S ≡ ∀f. continuous_on S f ∧ f ∈ S → (- {0::complex}) ⟶ (∃a. homotopic_with_canon (λh. True) S (- {0}) f (λx. a))"
lemma Borsukian_retraction_gen: assumes"Borsukian S""continuous_on S h""h ` S = T" "continuous_on T k""k ∈ T → S""∧y. y ∈ T ==> h(k y) = y" shows"Borsukian T" proof - interpret R: Retracts S h T k using assms by (simp add: image_subset_iff_funcset Retracts.intro) show ?thesis using assms apply (clarsimp simp add: Borsukian_def) apply (rule R.cohomotopically_trivial_retraction_null_gen [OF TrueI TrueI refl, of "-{0}"], auto) done qed
lemma retract_of_Borsukian: "[Borsukian T; S retract_of T]==> Borsukian S" by (smt (verit) Borsukian_retraction_gen retract_of_def retraction retraction_def retraction_subset image_subset_iff_funcset)
lemma homeomorphic_Borsukian: "[Borsukian S; S homeomorphic T]==> Borsukian T" using Borsukian_retraction_gen order_refl by (fastforce simp add: homeomorphism_def homeomorphic_def)
lemma homeomorphic_Borsukian_eq: "S homeomorphic T ==> Borsukian S ⟷ Borsukian T" by (meson homeomorphic_Borsukian homeomorphic_sym)
lemma Borsukian_translation: fixes S :: "'a::real_normed_vector set" shows"Borsukian (image (λx. a + x) S) ⟷ Borsukian S" using homeomorphic_Borsukian_eq homeomorphic_translation by blast
lemma Borsukian_injective_linear_image: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes"linear f""inj f" shows"Borsukian(f ` S) ⟷ Borsukian S" using assms homeomorphic_Borsukian_eq linear_homeomorphic_image by blast
lemma homotopy_eqv_Borsukianness: fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set" assumes"S homotopy_eqv T" shows"(Borsukian S ⟷ Borsukian T)" by (meson Borsukian_def assms homotopy_eqv_cohomotopic_triviality_null image_subset_iff_funcset)
lemma Borsukian_alt: fixes S :: "'a::real_normed_vector set" shows "Borsukian S ⟷ (∀f g. continuous_on S f ∧ f ∈ S → -{0} ∧ continuous_on S g ∧ g ∈ S → -{0} ⟶ homotopic_with_canon (λh. True) S (- {0::complex}) f g)" unfolding Borsukian_def homotopic_triviality by (force simp add: path_connected_punctured_universe)
lemma Borsukian_continuous_logarithm: fixes S :: "'a::real_normed_vector set" shows"Borsukian S ⟷ (∀f. continuous_on S f ∧ f ∈ S → (- {0::complex}) ⟶ (∃g. continuous_on S g ∧ (∀x ∈ S. f x = exp(g x))))" by (simp add: Borsukian_def inessential_eq_continuous_logarithm)
lemma Borsukian_continuous_logarithm_circle: fixes S :: "'a::real_normed_vector set" shows"Borsukian S ⟷ (∀f. continuous_on S f ∧ f ∈ S → sphere (0::complex) 1 ⟶ (∃g. continuous_on S g ∧ (∀x ∈ S. f x = exp(g x))))"
(is"?lhs = ?rhs") proof assume ?lhs thenshow ?rhs by (force simp: Borsukian_continuous_logarithm) next assume RHS [rule_format]: ?rhs show ?lhs proof (clarsimp simp: Borsukian_continuous_logarithm Pi_iff) fix f :: "'a ==> complex" assume contf: "continuous_on S f"and 0: "∀i∈S. f i ≠ 0" thenhave"continuous_on S (λx. f x / complex_of_real (cmod (f x)))" by (intro continuous_intros) auto moreoverhave"(λx. f x / complex_of_real (cmod (f x))) ∈ S → sphere 0 1" using 0 by (auto simp: norm_divide) ultimatelyobtain g where contg: "continuous_on S g" and fg: "∀x ∈ S. f x / complex_of_real (cmod (f x)) = exp(g x)" using RHS [of "λx. f x / of_real(norm(f x))"] by auto show"∃g. continuous_on S g ∧ (∀x∈S. f x = exp (g x))" proof (intro exI ballI conjI) show"continuous_on S (λx. (Ln ∘ of_real ∘ norm ∘ f)x + g x)" by (intro continuous_intros contf contg conjI) (use"0"in auto) show"f x = exp ((Ln ∘ complex_of_real ∘ cmod ∘ f) x + g x)"if"x ∈ S"for x using 0 that apply (simp add: exp_add) by (metis div_by_0 exp_Ln exp_not_eq_zero fg mult.commute nonzero_eq_divide_eq) qed qed qed
lemma Borsukian_continuous_logarithm_circle_real: fixes S :: "'a::real_normed_vector set" shows"Borsukian S ⟷ (∀f. continuous_on S f ∧ f ∈ S → sphere (0::complex) 1 ⟶ (∃g. continuous_on S (complex_of_real ∘ g) ∧ (∀x ∈ S. f x = exp(i * of_real(g x)))))"
(is"?lhs = ?rhs") proof assume LHS: ?lhs show ?rhs proof (clarify) fix f :: "'a ==> complex" assume"continuous_on S f"and f01: "f ∈ S → sphere 0 1" thenobtain g where contg: "continuous_on S g"and"∧x. x ∈ S ==> f x = exp(g x)" using LHS by (auto simp: Borsukian_continuous_logarithm_circle) thenhave"∀x∈S. f x = exp (i * complex_of_real ((Im ∘ g) x))" using f01 exp_eq_polar norm_exp_eq_Re by (fastforce simp: Pi_iff) thenshow"∃g. continuous_on S (complex_of_real ∘ g) ∧ (∀x∈S. f x = exp (i * complex_of_real (g x)))" by (rule_tac x="Im ∘ g"in exI) (force intro: continuous_intros contg) qed next assume RHS [rule_format]: ?rhs show ?lhs proof (clarsimp simp: Borsukian_continuous_logarithm_circle) fix f :: "'a ==> complex" assume"continuous_on S f"and f01: "f ∈ S → sphere 0 1" thenobtain g where contg: "continuous_on S (complex_of_real ∘ g)"and"∧x. x ∈ S ==> f x = exp(i * of_real(g x))" by (metis RHS) thenshow"∃g. continuous_on S g ∧ (∀x∈S. f x = exp (g x))" by (rule_tac x="λx. i* of_real(g x)"in exI) (auto simp: continuous_intros contg) qed qed
lemma Borsukian_circle: fixes S :: "'a::real_normed_vector set" shows"Borsukian S ⟷ (∀f. continuous_on S f ∧ f ∈ S → sphere (0::complex) 1 ⟶ (∃a. homotopic_with_canon (λh. True) S (sphere (0::complex) 1) f (λx. a)))" by (simp add: inessential_eq_continuous_logarithm_circle Borsukian_continuous_logarithm_circle_real)
lemma contractible_imp_Borsukian: "contractible S ==> Borsukian S" by (meson Borsukian_def nullhomotopic_from_contractible image_subset_iff_funcset)
lemma simply_connected_imp_Borsukian: fixes S :: "'a::real_normed_vector set" shows"[simply_connected S; locally path_connected S]==> Borsukian S" by (smt (verit, del_insts) continuous_logarithm_on_simply_connected Borsukian_continuous_logarithm_circle
PiE mem_sphere_0 norm_eq_zero zero_neq_one)
lemma starlike_imp_Borsukian: fixes S :: "'a::real_normed_vector set" shows"starlike S ==> Borsukian S" by (simp add: contractible_imp_Borsukian starlike_imp_contractible)
lemma Borsukian_empty: "Borsukian {}" by (auto simp: contractible_imp_Borsukian)
lemma convex_imp_Borsukian: fixes S :: "'a::real_normed_vector set" shows"convex S ==> Borsukian S" by (meson Borsukian_def convex_imp_contractible nullhomotopic_from_contractible)
proposition Borsukian_sphere: fixes a :: "'a::euclidean_space" shows"3 ≤ DIM('a) ==> Borsukian (sphere a r)" using ENR_sphere by (blast intro: simply_connected_imp_Borsukian ENR_imp_locally_path_connected simply_connected_sphere)
lemma Borsukian_Un_lemma: fixes S :: "'a::real_normed_vector set" assumes BS: "Borsukian S"and BT: "Borsukian T"and ST: "connected(S ∩ T)" and *: "∧f g::'a ==> complex. [continuous_on S f; continuous_on T g; ∧x. x ∈ S ∧ x ∈ T ==> f x = g x] ==> continuous_on (S ∪ T) (λx. if x ∈ S then f x else g x)" shows"Borsukian(S ∪ T)" proof (clarsimp simp add: Borsukian_continuous_logarithm Pi_iff) fix f :: "'a ==> complex" assume contf: "continuous_on (S ∪ T) f"and 0: "∀i∈S ∪ T. f i ≠ 0" thenhave contfS: "continuous_on S f"and contfT: "continuous_on T f" using continuous_on_subset by auto have"[continuous_on S f; f ∈ S → -{0}]==>∃g. continuous_on S g ∧ (∀x ∈ S. f x = exp(g x))" using BS by (auto simp: Borsukian_continuous_logarithm) thenobtain g where contg: "continuous_on S g"and fg: "∧x. x ∈ S ==> f x = exp(g x)" using"0" contfS by force have"[continuous_on T f; f ∈ T → -{0}]==>∃g. continuous_on T g ∧ (∀x ∈ T. f x = exp(g x))" using BT by (auto simp: Borsukian_continuous_logarithm) thenobtain h where conth: "continuous_on T h"and fh: "∧x. x ∈ T ==> f x = exp(h x)" using"0" contfT by force show"∃g. continuous_on (S ∪ T) g ∧ (∀x∈S ∪ T. f x = exp (g x))" proof (cases "S ∩ T = {}") case True show ?thesis proof (intro exI conjI) show"continuous_on (S ∪ T) (λx. if x ∈ S then g x else h x)" using True * [OF contg conth] by (meson disjoint_iff) show"∀x∈S ∪ T. f x = exp (if x ∈ S then g x else h x)" using fg fh by auto qed next case False have"(λx. g x - h x) constant_on S ∩ T" proof (rule continuous_discrete_range_constant [OF ST]) show"continuous_on (S ∩ T) (λx. g x - h x)" by (metis contg conth continuous_on_diff continuous_on_subset inf_le1 inf_le2) show"∃e>0. ∀y. y ∈ S ∩ T ∧ g y - h y ≠ g x - h x ⟶ e ≤ cmod (g y - h y - (g x - h x))" if"x ∈ S ∩ T"for x proof - have"g y - g x = h y - h x" if"y ∈ S""y ∈ T""cmod (g y - g x - (h y - h x)) < 2 * pi"for y proof (rule exp_complex_eqI) have"∣Im (g y - g x) - Im (h y - h x)∣≤ cmod (g y - g x - (h y - h x))" by (metis abs_Im_le_cmod minus_complex.simps(2)) thenshow"∣Im (g y - g x) - Im (h y - h x)∣ < 2 * pi" using that by linarith have"exp (g x) = exp (h x)""exp (g y) = exp (h y)" using fg fh that ‹x ∈ S ∩ T›by fastforce+ thenshow"exp (g y - g x) = exp (h y - h x)" by (simp add: exp_diff) qed thenshow ?thesis by (rule_tac x="2*pi"in exI) (fastforce simp add: algebra_simps) qed qed thenobtain a where a: "∧x. x ∈ S ∩ T ==> g x - h x = a" by (auto simp: constant_on_def) with False have"exp a = 1" by (metis IntI disjoint_iff_not_equal divide_self_if exp_diff exp_not_eq_zero fg fh) with a show ?thesis apply (rule_tac x="λx. if x ∈ S then g x else a + h x"in exI) apply (intro * contg conth continuous_intros conjI) apply (auto simp: algebra_simps fg fh exp_add) done qed qed
proposition Borsukian_open_Un: fixes S :: "'a::real_normed_vector set" assumes opeS: "openin (top_of_set (S ∪ T)) S" and opeT: "openin (top_of_set (S ∪ T)) T" and BS: "Borsukian S"and BT: "Borsukian T"and ST: "connected(S ∩ T)" shows"Borsukian(S ∪ T)" by (force intro: Borsukian_Un_lemma [OF BS BT ST] continuous_on_cases_local_open [OF opeS opeT])
lemma Borsukian_closed_Un: fixes S :: "'a::real_normed_vector set" assumes cloS: "closedin (top_of_set (S ∪ T)) S" and cloT: "closedin (top_of_set (S ∪ T)) T" and BS: "Borsukian S"and BT: "Borsukian T"and ST: "connected(S ∩ T)" shows"Borsukian(S ∪ T)" by (force intro: Borsukian_Un_lemma [OF BS BT ST] continuous_on_cases_local [OF cloS cloT])
lemma Borsukian_separation_compact: fixes S :: "complex set" assumes"compact S" shows"Borsukian S ⟷ connected(- S)" by (simp add: Borsuk_separation_theorem Borsukian_circle assms)
lemma Borsukian_monotone_image_compact: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes"Borsukian S"and contf: "continuous_on S f"and fim: "f ` S = T" and"compact S"and conn: "∧y. y ∈ T ==> connected {x. x ∈ S ∧ f x = y}" shows"Borsukian T" proof (clarsimp simp: Borsukian_continuous_logarithm Pi_iff) fix g :: "'b ==> complex" assume contg: "continuous_on T g"and 0: "∀i∈T. g i ≠ 0" have"continuous_on S (g ∘ f)" using contf contg continuous_on_compose fim by blast moreoverhave"(g ∘ f) ` S ⊆ -{0}" using fim 0 by auto ultimatelyobtain h where conth: "continuous_on S h"and gfh: "∧x. x ∈ S ==> (g ∘ f) x = exp(h x)" using‹Borsukian S›by (auto simp: Borsukian_continuous_logarithm) have"∧y. ∃x. y ∈ T ⟶ x ∈ S ∧ f x = y" using fim by auto thenobtain f' where f': "∧y. y ∈ T ⟶ f' y ∈ S ∧ f (f' y) = y" by metis have *: "(λx. h x - h(f' y)) constant_on {x. x ∈ S ∧ f x = y}"if"y ∈ T"for y proof (rule continuous_discrete_range_constant [OF conn [OF that], of "λx. h x - h (f' y)"], simp_all add: algebra_simps) show"continuous_on {x ∈ S. f x = y} (λx. h x - h (f' y))" by (intro continuous_intros continuous_on_subset [OF conth]) auto show"∃e>0. ∀u. u ∈ S ∧ f u = y ∧ h u ≠ h x ⟶ e ≤ cmod (h u - h x)" if x: "x ∈ S ∧ f x = y"for x proof - have"h u = h x"if"u ∈ S""f u = y""cmod (h u - h x) < 2 * pi"for u proof (rule exp_complex_eqI) have"∣Im (h u) - Im (h x)∣≤ cmod (h u - h x)" by (metis abs_Im_le_cmod minus_complex.simps(2)) thenshow"∣Im (h u) - Im (h x)∣ < 2 * pi" using that by linarith show"exp (h u) = exp (h x)" by (simp add: gfh [symmetric] x that) qed thenshow ?thesis by (rule_tac x="2*pi"in exI) (fastforce simp add: algebra_simps) qed qed show"∃h. continuous_on T h ∧ (∀x∈T. g x = exp (h x))" proof (intro exI conjI) show"continuous_on T (h ∘ f')" proof (rule continuous_from_closed_graph [of "h ` S"]) show"compact (h ` S)" by (simp add: ‹compact S› compact_continuous_image conth) show"(h ∘ f') ∈ T → h ` S" by (auto simp: f') have"h x = h (f' (f x))"if"x ∈ S"for x using * [of "f x"] fim that unfolding constant_on_def by clarsimp (metis f' imageI right_minus_eq) moreoverhave"∧x. x ∈ T ==>∃u. u ∈ S ∧ x = f u ∧ h (f' x) = h u" using f' by fastforce ultimately have eq: "((λx. (x, (h ∘ f') x)) ` T) = {p. ∃x. x ∈ S ∧ (x, p) ∈ (S × UNIV) ∩ ((λz. snd z - ((f ∘ fst) z, (h ∘ fst) z)) -` {0})}" using fim by (auto simp: image_iff) moreoverhave"closed …" apply (intro closed_compact_projection [OF ‹compact S›] continuous_closed_preimage
continuous_intros continuous_on_subset [OF contf] continuous_on_subset [OF conth]) by (auto simp: ‹compact S› closed_Times compact_imp_closed) ultimatelyshow"closed ((λx. (x, (h ∘ f') x)) ` T)" by simp qed qed (use f' gfh in fastforce) qed
lemma Borsukian_open_map_image_compact: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes"Borsukian S"and contf: "continuous_on S f"and fim: "f ` S = T"and"compact S" and ope: "∧U. openin (top_of_set S) U ==> openin (top_of_set T) (f ` U)" shows"Borsukian T" proof (clarsimp simp add: Borsukian_continuous_logarithm_circle_real) fix g :: "'b ==> complex" assume contg: "continuous_on T g"and gim: "g ∈ T → sphere 0 1" have"continuous_on S (g ∘ f)" using contf contg continuous_on_compose fim by blast moreoverhave"(g ∘ f) ∈ S → sphere 0 1" using fim gim by auto ultimatelyobtain h where cont_cxh: "continuous_on S (complex_of_real ∘ h)" and gfh: "∧x. x ∈ S ==> (g ∘ f) x = exp(i * of_real(h x))" using‹Borsukian S› Borsukian_continuous_logarithm_circle_real by metis thenhave conth: "continuous_on S h" by simp have"∃x. x ∈ S ∧ f x = y ∧ (∀x' ∈ S. f x' = y ⟶ h x ≤ h x')"if"y ∈ T"for y proof - have 1: "compact (h ` {x ∈ S. f x = y})" proof (rule compact_continuous_image) show"continuous_on {x ∈ S. f x = y} h" by (rule continuous_on_subset [OF conth]) auto have"compact (S ∩ f -` {y})" using that proper_map_from_compact [OF contf _ ‹compact S›] fim by force thenshow"compact {x ∈ S. f x = y}" by (auto simp: vimage_def Int_def) qed have 2: "h ` {x ∈ S. f x = y} ≠ {}" using fim that by auto have"∃s ∈ h ` {x ∈ S. f x = y}. ∀t ∈ h ` {x ∈ S. f x = y}. s ≤ t" using compact_attains_inf [OF 1 2] by blast thenshow ?thesis by auto qed thenobtain k where kTS: "∧y. y ∈ T ==> k y ∈ S" and fk: "∧y. y ∈ T ==> f (k y) = y " and hle: "∧x' y. [y ∈ T; x' ∈ S; f x' = y]==> h (k y) ≤ h x'" by metis have"continuous_on T (h ∘ k)" proof (clarsimp simp add: continuous_on_iff) fix y and e::real assume"y ∈ T""0 < e" moreoverhave"uniformly_continuous_on S (complex_of_real ∘ h)" using‹compact S› cont_cxh compact_uniformly_continuous by blast ultimatelyobtain d where"0 < d" and d: "∧x x'. [x∈S; x'∈S; dist x' x < d]==> dist (h x') (h x) < e" by (force simp: uniformly_continuous_on_def) obtain δ where"0 < δ"and δ: "∧x'. [x' ∈ T; dist y x' < δ] ==> (∀v ∈ {z ∈ S. f z = y}. ∃v'. v' ∈ {z ∈ S. f z = x'} ∧ dist v v' < d) ∧ (∀v' ∈ {z ∈ S. f z = x'}. ∃v. v ∈ {z ∈ S. f z = y} ∧ dist v' v < d)" proof (rule upper_lower_hemicontinuous_explicit [of T "λy. {z ∈ S. f z = y}" S]) show"∧U. openin (top_of_set S) U ==> openin (top_of_set T) {x ∈ T. {z ∈ S. f z = x} ⊆ U}" using closed_map_iff_upper_hemicontinuous_preimage [of f S T] fim contf ‹compact S› using Abstract_Topology_2.continuous_imp_closed_map by blast show"∧U. closedin (top_of_set S) U ==> closedin (top_of_set T) {x ∈ T. {z ∈ S. f z = x} ⊆ U}" using ope open_map_iff_lower_hemicontinuous_preimage[of f S T] fim [THEN equalityD1] by blast show"bounded {z ∈ S. f z = y}" by (metis (no_types, lifting) compact_imp_bounded [OF ‹compact S›] bounded_subset mem_Collect_eq subsetI) qed (use‹y ∈ T›‹0 🚫› fk kTS in‹force+›) have"dist (h (k y')) (h (k y)) < e"if"y' ∈ T""dist y y' < δ"for y' proof - have k1: "k y ∈ S""f (k y) = y"and k2: "k y' ∈ S""f (k y') = y'" by (auto simp: ‹y ∈ T›‹y' ∈ T› kTS fk) have 1: "∧v. [v ∈ S; f v = y]==>∃v'. v' ∈ {z ∈ S. f z = y'} ∧ dist v v' < d" and 2: "∧v'. [v' ∈ S; f v' = y']==>∃v. v ∈ {z ∈ S. f z = y} ∧ dist v' v < d" using δ [OF that] by auto thenobtain w' w where"w' ∈ S""f w' = y'""dist (k y) w' < d" and"w ∈ S""f w = y""dist (k y') w < d" using 1 [OF k1] 2 [OF k2] by auto thenshow ?thesis using d [of w "k y'"] d [of w' "k y"] k1 k2 ‹y' ∈ T›‹y ∈ T› hle by (fastforce simp: dist_norm abs_diff_less_iff algebra_simps) qed thenshow"∃d>0. ∀x'∈T. dist x' y < d ⟶ dist (h (k x')) (h (k y)) < e" using‹0 🚫δ›by (auto simp: dist_commute) qed thenshow"∃h. continuous_on T h ∧ (∀x∈T. g x = exp (i * complex_of_real (h x)))" using fk gfh kTS by force qed
text‹If two points are separated by a closed set, there's a minimal one.›
proposition closed_irreducible_separator: fixes a :: "'a::real_normed_vector" assumes"closed S"and ab: "¬ connected_component (- S) a b" obtains T where"T ⊆ S""closed T""T ≠ {}""¬ connected_component (- T) a b" "∧U. U ⊂ T ==> connected_component (- U) a b" proof (cases "a ∈ S ∨ b ∈ S") case True thenshow ?thesis proof assume *: "a ∈ S" show ?thesis proof show"{a} ⊆ S" using * by blast show"¬ connected_component (- {a}) a b" using connected_component_in by auto show"∧U. U ⊂ {a} ==> connected_component (- U) a b" by (metis connected_component_UNIV UNIV_I compl_bot_eq connected_component_eq_eq less_le_not_le subset_singletonD) qed auto next assume *: "b ∈ S" show ?thesis proof show"{b} ⊆ S" using * by blast show"¬ connected_component (- {b}) a b" using connected_component_in by auto show"∧U. U ⊂ {b} ==> connected_component (- U) a b" by (metis connected_component_UNIV UNIV_I compl_bot_eq connected_component_eq_eq less_le_not_le subset_singletonD) qed auto qed next case False
define A where"A ≡ connected_component_set (- S) a"
define B where"B ≡ connected_component_set (- (closure A)) b" have"a ∈ A" using False A_def by auto have"b ∈ B" unfolding A_def B_def closure_Un_frontier using ab False ‹closed S› frontier_complement frontier_of_connected_component_subset frontier_subset_closed by force have"frontier B ⊆ frontier (connected_component_set (- closure A) b)" using B_def by blast alsohave frsub: "... ⊆ frontier A" proof - have"∧A. closure (- closure (- A)) ⊆ closure A" by (metis (no_types) closure_mono closure_subset compl_le_compl_iff double_compl) thenshow ?thesis by (metis (no_types) closure_closure double_compl frontier_closures frontier_of_connected_component_subset le_inf_iff subset_trans) qed finallyhave frBA: "frontier B ⊆ frontier A" . show ?thesis proof show"frontier B ⊆ S" proof - have"frontier S ⊆ S" by (simp add: ‹closed S› frontier_subset_closed) thenshow ?thesis using frsub frontier_complement frontier_of_connected_component_subset unfolding A_def B_def by blast qed show"closed (frontier B)" by simp show"¬ connected_component (- frontier B) a b" unfolding connected_component_def proof clarify fix T assume"connected T"and TB: "T ⊆ - frontier B"and"a ∈ T"and"b ∈ T" have"a ∉ B" by (metis A_def B_def ComplD ‹a ∈ A› assms(1) closed_open connected_component_subset in_closure_connected_component subsetD) have"T ∩ B ≠ {}" using‹b ∈ B›‹b ∈ T›by blast moreoverhave"T - B ≠ {}" using‹a ∉ B›‹a ∈ T›by blast ultimatelyshow"False" using connected_Int_frontier [of T B] TB ‹connected T›by blast qed moreoverhave"connected_component (- frontier B) a b"if"frontier B = {}" using connected_component_eq_UNIV that by auto ultimatelyshow"frontier B ≠ {}" by blast show"connected_component (- U) a b"if"U ⊂ frontier B"for U proof - obtain p where Usub: "U ⊆ frontier B"and p: "p ∈ frontier B""p ∉ U" using‹U ⊂ frontier B›by blast show ?thesis unfolding connected_component_def proof (intro exI conjI) have"connected ((insert p A) ∪ (insert p B))" proof (rule connected_Un) show"connected (insert p A)" by (metis A_def IntD1 frBA ‹p ∈ frontier B› closure_insert closure_subset connected_connected_component connected_intermediate_closure frontier_closures insert_absorb subsetCE subset_insertI) show"connected (insert p B)" by (metis B_def IntD1 ‹p ∈ frontier B› closure_insert closure_subset connected_connected_component connected_intermediate_closure frontier_closures insert_absorb subset_insertI) qed blast thenshow"connected (insert p (B ∪ A))" by (simp add: sup.commute) have"A ⊆ - U" using A_def Usub ‹frontier B ⊆ S› connected_component_subset by fastforce moreoverhave"B ⊆ - U" using B_def Usub connected_component_subset frBA frontier_closures by fastforce ultimatelyshow"insert p (B ∪ A) ⊆ - U" using p by auto qed (auto simp: ‹a ∈ A›‹b ∈ B›) qed qed qed
lemma frontier_minimal_separating_closed_pointwise: fixes S :: "'a::real_normed_vector set" assumes S: "closed S""a ∉ S"and nconn: "¬ connected_component (- S) a b" and conn: "∧T. [closed T; T ⊂ S]==> connected_component (- T) a b" shows"frontier(connected_component_set (- S) a) = S" (is"?F = S") proof - have"?F ⊆ S" by (simp add: S componentsI frontier_of_components_closed_complement) moreoverhave False if"?F ⊂ S" proof - have"connected_component (- ?F) a b" by (simp add: conn that) thenobtain T where"connected T""T ⊆ -?F""a ∈ T""b ∈ T" by (auto simp: connected_component_def) moreoverhave"T ∩ ?F ≠ {}" proof (rule connected_Int_frontier [OF ‹connected T›]) show"T ∩ connected_component_set (- S) a ≠ {}" using‹a ∉ S›‹a ∈ T›by fastforce show"T - connected_component_set (- S) a ≠ {}" using‹b ∈ T› nconn by blast qed ultimatelyshow ?thesis by blast qed ultimatelyshow ?thesis by blast qed
subsection‹Unicoherence (closed)›
definition🍋‹tag important› unicoherent where "unicoherent U ≡ ∀S T. connected S ∧ connected T ∧ S ∪ T = U ∧ closedin (top_of_set U) S ∧ closedin (top_of_set U) T ⟶ connected (S ∩ T)"
lemma unicoherentI [intro?]: assumes"∧S T. [connected S; connected T; U = S ∪ T; closedin (top_of_set U) S; closedin (top_of_set U) T] ==> connected (S ∩ T)" shows"unicoherent U" using assms unfolding unicoherent_def by blast
lemma unicoherentD: assumes"unicoherent U""connected S""connected T""U = S ∪ T""closedin (top_of_set U) S""closedin (top_of_set U) T" shows"connected (S ∩ T)" using assms unfolding unicoherent_def by blast
proposition homeomorphic_unicoherent: assumes ST: "S homeomorphic T"and S: "unicoherent S" shows"unicoherent T" proof - obtain f g where gf: "∧x. x ∈ S ==> g (f x) = x"and fim: "T = f ` S"and gfim: "g ` f ` S = S" and contf: "continuous_on S f"and contg: "continuous_on (f ` S) g" using ST by (auto simp: homeomorphic_def homeomorphism_def) show ?thesis proof fix U V assume"connected U""connected V"and T: "T = U ∪ V" and cloU: "closedin (top_of_set T) U" and cloV: "closedin (top_of_set T) V" have"f ∈ (g ` U ∩ g ` V) → U""f ∈ (g ` U ∩ g ` V) → V" using gf fim T by auto (metis UnCI image_iff)+ moreoverhave"U ∩ V ⊆ f ` (g ` U ∩ g ` V)" using gf fim by (force simp: image_iff T) ultimatelyhave"U ∩ V = f ` (g ` U ∩ g ` V)"by blast moreoverhave"connected (f ` (g ` U ∩ g ` V))" proof (rule connected_continuous_image) show"continuous_on (g ` U ∩ g ` V) f" using T fim gfim by (metis Un_upper1 contf continuous_on_subset image_mono inf_le1) show"connected (g ` U ∩ g ` V)" proof (intro conjI unicoherentD [OF S]) show"connected (g ` U)""connected (g ` V)" using‹connected U› cloU ‹connected V› cloV by (metis Topological_Spaces.connected_continuous_image closedin_imp_subset contg continuous_on_subset fim)+ show"S = g ` U ∪ g ` V" using T fim gfim by auto have hom: "homeomorphism T S g f" by (simp add: contf contg fim gf gfim homeomorphism_def) have"closedin (top_of_set T) U""closedin (top_of_set T) V" by (simp_all add: cloU cloV) thenshow"closedin (top_of_set S) (g ` U)" "closedin (top_of_set S) (g ` V)" by (blast intro: homeomorphism_imp_closed_map [OF hom])+ qed qed ultimatelyshow"connected (U ∩ V)"by metis qed qed
lemma homeomorphic_unicoherent_eq: "S homeomorphic T ==> (unicoherent S ⟷ unicoherent T)" by (meson homeomorphic_sym homeomorphic_unicoherent)
lemma unicoherent_translation: fixes S :: "'a::real_normed_vector set" shows "unicoherent (image (λx. a + x) S) ⟷ unicoherent S" using homeomorphic_translation homeomorphic_unicoherent_eq by blast
lemma unicoherent_injective_linear_image: fixes f :: "'a::euclidean_space ==> 'b::euclidean_space" assumes"linear f""inj f" shows"(unicoherent(f ` S) ⟷ unicoherent S)" using assms homeomorphic_unicoherent_eq linear_homeomorphic_image by blast
lemma Borsukian_imp_unicoherent: fixes U :: "'a::euclidean_space set" assumes"Borsukian U"shows"unicoherent U" unfolding unicoherent_def proof clarify fix S T assume"connected S""connected T""U = S ∪ T" and cloS: "closedin (top_of_set (S ∪ T)) S" and cloT: "closedin (top_of_set (S ∪ T)) T" show"connected (S ∩ T)" unfolding connected_closedin_eq proof clarify fix V W assume"closedin (top_of_set (S ∩ T)) V" and"closedin (top_of_set (S ∩ T)) W" and VW: "V ∪ W = S ∩ T""V ∩ W = {}"and"V ≠ {}""W ≠ {}" thenhave cloV: "closedin (top_of_set U) V"and cloW: "closedin (top_of_set U) W" using‹U = S ∪ T› cloS cloT closedin_trans by blast+ obtain q where contq: "continuous_on U q" and q01: "∧x. x ∈ U ==> q x ∈ {0..1::real}" and qV: "∧x. x ∈ V ==> q x = 0"and qW: "∧x. x ∈ W ==> q x = 1" by (rule Urysohn_local [OF cloV cloW ‹V ∩ W = {}›, of 0 1])
(fastforce simp: closed_segment_eq_real_ivl) let ?h = "λx. if x ∈ S then exp(pi * i * q x) else 1 / exp(pi * i * q x)" have eqST: "exp(pi * i * q x) = 1 / exp(pi * i * q x)"if"x ∈ S ∩ T"for x proof - have"x ∈ V ∪ W" using that ‹V ∪ W = S ∩ T›by blast with qV qW show ?thesis by force qed obtain g where contg: "continuous_on U g" and circle: "g ∈ U → sphere 0 1" and S: "∧x. x ∈ S ==> g x = exp(pi * i * q x)" and T: "∧x. x ∈ T ==> g x = 1 / exp(pi * i * q x)" proof show"continuous_on U ?h" unfolding‹U = S ∪ T› proof (rule continuous_on_cases_local [OF cloS cloT]) show"continuous_on S (λx. exp (pi * i * q x))" proof (intro continuous_intros) show"continuous_on S q" using‹U = S ∪ T› continuous_on_subset contq by blast qed show"continuous_on T (λx. 1 / exp (pi * i * q x))" proof (intro continuous_intros) show"continuous_on T q" using‹U = S ∪ T› continuous_on_subset contq by auto qed auto qed (use eqST in auto) qed (use eqST in‹auto simp: norm_divide›) thenobtain h where conth: "continuous_on U h"and heq: "∧x. x ∈ U ==> g x = exp (h x)" by (metis Borsukian_continuous_logarithm_circle assms) obtain v w where"v ∈ V""w ∈ W" using‹V ≠ {}›‹W ≠ {}›by blast thenhave vw: "v ∈ S ∩ T""w ∈ S ∩ T" using VW by auto have iff: "2 * pi ≤ cmod (2 * of_int m * of_real pi * i - 2 * of_int n * of_real pi * i) ⟷ 1 ≤ abs (m - n)"for m n proof - have"2 * pi ≤ cmod (2 * of_int m * of_real pi * i - 2 * of_int n * of_real pi * i) ⟷ 2 * pi ≤ cmod ((2 * pi * i) * (of_int m - of_int n))" by (simp add: algebra_simps) alsohave"... ⟷ 2 * pi ≤ 2 * pi * cmod (of_int m - of_int n)" by (simp add: norm_mult) alsohave"... ⟷ 1 ≤ abs (m - n)" by simp (metis norm_of_int of_int_1_le_iff of_int_abs of_int_diff) finallyshow ?thesis . qed have *: "∃n::int. h x - (pi * i * q x) = (of_int(2*n) * pi) * i"if"x ∈ S"for x using that S ‹U = S ∪ T› heq exp_eq [symmetric] by (simp add: algebra_simps) moreoverhave"(λx. h x - (pi * i * q x)) constant_on S" proof (rule continuous_discrete_range_constant [OF ‹connected S›]) have"continuous_on S h""continuous_on S q" using‹U = S ∪ T› continuous_on_subset conth contq by blast+ thenshow"continuous_on S (λx. h x - (pi * i * q x))" by (intro continuous_intros) have"2*pi ≤ cmod (h y - (pi * i * q y) - (h x - (pi * i * q x)))" if"x ∈ S""y ∈ S"and ne: "h y - (pi * i * q y) ≠ h x - (pi * i * q x)"for x y using * [OF ‹x ∈ S›] * [OF ‹y ∈ S›] ne by (auto simp: iff) thenshow"∧x. x ∈ S ==> ∃e>0. ∀y. y ∈ S ∧ h y - (pi * i * q y) ≠ h x - (pi * i * q x) ⟶ e ≤ cmod (h y - (pi * i * q y) - (h x - (pi * i * q x)))" by (rule_tac x="2*pi"in exI) auto qed ultimately obtain m where m: "∧x. x ∈ S ==> h x - (pi * i * q x) = (of_int(2*m) * pi) * i" using vw by (force simp: constant_on_def) have *: "∃n::int. h x = - (pi * i * q x) + (of_int(2*n) * pi) * i"if"x ∈ T"for x unfolding exp_eq [symmetric] using that T ‹U = S ∪ T›by (simp add: exp_minus field_simps heq [symmetric]) moreoverhave"(λx. h x + (pi * i * q x)) constant_on T" proof (rule continuous_discrete_range_constant [OF ‹connected T›]) have"continuous_on T h""continuous_on T q" using‹U = S ∪ T› continuous_on_subset conth contq by blast+ thenshow"continuous_on T (λx. h x + (pi * i * q x))" by (intro continuous_intros) have"2*pi ≤ cmod (h y + (pi * i * q y) - (h x + (pi * i * q x)))" if"x ∈ T""y ∈ T"and ne: "h y + (pi * i * q y) ≠ h x + (pi * i * q x)"for x y using * [OF ‹x ∈ T›] * [OF ‹y ∈ T›] ne by (auto simp: iff) thenshow"∧x. x ∈ T ==> ∃e>0. ∀y. y ∈ T ∧ h y + (pi * i * q y) ≠ h x + (pi * i * q x) ⟶ e ≤ cmod (h y + (pi * i * q y) - (h x + (pi * i * q x)))" by (rule_tac x="2*pi"in exI) auto qed ultimately obtain n where n: "∧x. x ∈ T ==> h x + (pi * i * q x) = (of_int(2*n) * pi) * i" using vw by (force simp: constant_on_def) show"False" using m [of v] m [of w] n [of v] n [of w] vw by (auto simp: algebra_simps ‹v ∈ V›‹w ∈ W› qV qW) qed qed
corollary contractible_imp_unicoherent: fixes U :: "'a::euclidean_space set" assumes"contractible U"shows"unicoherent U" by (simp add: Borsukian_imp_unicoherent assms contractible_imp_Borsukian)
corollary convex_imp_unicoherent: fixes U :: "'a::euclidean_space set" assumes"convex U"shows"unicoherent U" by (simp add: Borsukian_imp_unicoherent assms convex_imp_Borsukian)
text‹If the type class constraint can be relaxed, I don't know how!› corollary unicoherent_UNIV: "unicoherent (UNIV :: 'a :: euclidean_space set)" by (simp add: convex_imp_unicoherent)
lemma unicoherent_monotone_image_compact: fixes T :: "'b :: t2_space set" assumes S: "unicoherent S""compact S"and contf: "continuous_on S f"and fim: "f ` S = T" and conn: "∧y. y ∈ T ==> connected (S ∩ f -` {y})" shows"unicoherent T" proof fix U V assume UV: "connected U""connected V""T = U ∪ V" and cloU: "closedin (top_of_set T) U" and cloV: "closedin (top_of_set T) V" moreoverhave"compact T" using‹compact S› compact_continuous_image contf fim by blast ultimatelyhave"closed U""closed V" by (auto simp: closedin_closed_eq compact_imp_closed) let ?SUV = "(S ∩ f -` U) ∩ (S ∩ f -` V)" have UV_eq: "f ` ?SUV = U ∩ V" using‹T = U ∪ V› fim by force+ have"connected (f ` ?SUV)" proof (rule connected_continuous_image) show"continuous_on ?SUV f" by (meson contf continuous_on_subset inf_le1) show"connected ?SUV" proof (rule unicoherentD [OF ‹unicoherent S›, of "S ∩ f -` U""S ∩ f -` V"]) have"∧C. closedin (top_of_set S) C ==> closedin (top_of_set T) (f ` C)" by (metis ‹compact S› closed_subset closedin_compact closedin_imp_subset compact_continuous_image compact_imp_closed contf continuous_on_subset fim image_mono) thenshow"connected (S ∩ f -` U)""connected (S ∩ f -` V)" using UV by (auto simp: conn intro: connected_closed_monotone_preimage [OF contf fim]) show"S = (S ∩ f -` U) ∪ (S ∩ f -` V)" using UV fim by blast show"closedin (top_of_set S) (S ∩ f -` U)" "closedin (top_of_set S) (S ∩ f -` V)" by (auto simp: continuous_on_imp_closedin cloU cloV contf fim) qed qed with UV_eq show"connected (U ∩ V)" by simp qed
subsection‹Several common variants of unicoherence›
lemma connected_frontier_disjoint: fixes S :: "'a :: euclidean_space set" assumes"connected S""connected T""disjnt S T"and ST: "frontier S ⊆ frontier T" shows"connected(frontier S)" proof (cases "S = UNIV") case True thenshow ?thesis by simp next case False thenhave"-S ≠ {}" by blast thenobtain C where C: "C ∈ components(- S)"and"T ⊆ C" by (metis ComplI disjnt_iff subsetI exists_component_superset ‹disjnt S T›‹connected T›) moreoverhave"frontier S = frontier C" proof - have"frontier C ⊆ frontier S" using C frontier_complement frontier_of_components_subset by blast moreoverhave"x ∈ frontier C"if"x ∈ frontier S"for x proof - have"x ∈ closure C" using that unfolding frontier_def by (metis (no_types) Diff_eq ST ‹T ⊆ C› closure_mono contra_subsetD frontier_def le_inf_iff that) moreoverhave"x ∉ interior C" using that unfolding frontier_def by (metis C Compl_eq_Diff_UNIV Diff_iff subsetD in_components_subset interior_diff interior_mono) ultimatelyshow ?thesis by (auto simp: frontier_def) qed ultimatelyshow ?thesis by blast qed ultimatelyshow ?thesis using‹connected S› connected_frontier_component_complement by auto qed
subsection‹Some separation results›
lemma separation_by_component_closed_pointwise: fixes S :: "'a :: euclidean_space set" assumes"closed S""¬ connected_component (- S) a b" obtains C where"C ∈ components S""¬ connected_component(- C) a b" proof (cases "a ∈ S ∨ b ∈ S") case True thenshow ?thesis using connected_component_in componentsI that by fastforce next case False obtain T where"T ⊆ S""closed T""T ≠ {}" and nab: "¬ connected_component (- T) a b" and conn: "∧U. U ⊂ T ==> connected_component (- U) a b" using closed_irreducible_separator [OF assms] by metis moreoverhave"connected T" proof - have ab: "frontier(connected_component_set (- T) a) = T""frontier(connected_component_set (- T) b) = T" using frontier_minimal_separating_closed_pointwise by (metis False ‹T ⊆ S›‹closed T› connected_component_sym conn connected_component_eq_empty connected_component_intermediate_subset empty_subsetI nab)+ have"connected (frontier (connected_component_set (- T) a))" proof (rule connected_frontier_disjoint) show"disjnt (connected_component_set (- T) a) (connected_component_set (- T) b)" unfolding disjnt_iff by (metis connected_component_eq connected_component_eq_empty connected_component_idemp mem_Collect_eq nab) show"frontier (connected_component_set (- T) a) ⊆ frontier (connected_component_set (- T) b)" by (simp add: ab) qed auto with ab ‹closed T›show ?thesis by simp qed ultimatelyobtain C where"C ∈ components S""T ⊆ C" using exists_component_superset [of T S] by blast thenshow ?thesis by (meson Compl_anti_mono connected_component_of_subset nab that) qed
lemma separation_by_component_closed: fixes S :: "'a :: euclidean_space set" assumes"closed S""¬ connected(- S)" obtains C where"C ∈ components S""¬ connected(- C)" proof - obtain x y where"closed S""x ∉ S""y ∉ S"and"¬ connected_component (- S) x y" using assms by (auto simp: connected_iff_connected_component) thenobtain C where"C ∈ components S""¬ connected_component(- C) x y" using separation_by_component_closed_pointwise by metis thenshow"thesis" by (metis Compl_iff ‹x ∉ S›‹y ∉ S› connected_component_eq_self in_components_subset mem_Collect_eq subsetD that) qed
lemma separation_by_Un_closed_pointwise: fixes S :: "'a :: euclidean_space set" assumes ST: "closed S""closed T""S ∩ T = {}" and conS: "connected_component (- S) a b"and conT: "connected_component (- T) a b" shows"connected_component (- (S ∪ T)) a b" proof (rule ccontr) have"a ∉ S""b ∉ S""a ∉ T""b ∉ T" using conS conT connected_component_in by auto assume"¬ connected_component (- (S ∪ T)) a b" thenobtain C where"C ∈ components (S ∪ T)"and C: "¬ connected_component(- C) a b" using separation_by_component_closed_pointwise assms by blast thenhave"C ⊆ S ∨ C ⊆ T" proof - have"connected C""C ⊆ S ∪ T" using‹C ∈ components (S ∪ T)› in_components_subset by (blast elim: componentsE)+ moreoverthenhave"C ∩ T = {} ∨ C ∩ S = {}" by (metis Int_empty_right ST inf.commute connected_closed) ultimatelyshow ?thesis by blast qed thenshow False by (meson Compl_anti_mono C conS conT connected_component_of_subset) qed
lemma separation_by_Un_closed: fixes S :: "'a :: euclidean_space set" assumes ST: "closed S""closed T""S ∩ T = {}"and conS: "connected(- S)"and conT: "connected(- T)" shows"connected(- (S ∪ T))" using assms separation_by_Un_closed_pointwise by (fastforce simp add: connected_iff_connected_component)
lemma open_unicoherent_UNIV: fixes S :: "'a :: euclidean_space set" assumes"open S""open T""connected S""connected T""S ∪ T = UNIV" shows"connected(S ∩ T)" proof - have"connected(- (-S ∪ -T))" by (metis closed_Compl compl_sup compl_top_eq double_compl separation_by_Un_closed assms) thenshow ?thesis by simp qed
lemma separation_by_component_open_aux: fixes S :: "'a :: euclidean_space set" assumes ST: "closed S""closed T""S ∩ T = {}" and"S ≠ {}""T ≠ {}" obtains C where"C ∈ components(-(S ∪ T))""C ≠ {}""frontier C ∩ S ≠ {}""frontier C ∩ T ≠ {}" proof (rule ccontr) let ?S = "S ∪∪{C ∈ components(- (S ∪ T)). frontier C ⊆ S}" let ?T = "T ∪∪{C ∈ components(- (S ∪ T)). frontier C ⊆ T}" assume"¬ thesis" with that have *: "frontier C ∩ S = {} ∨ frontier C ∩ T = {}" if C: "C ∈ components (- (S ∪ T))""C ≠ {}"for C using C by blast have"∃A B::'a set. closed A ∧ closed B ∧ UNIV ⊆ A ∪ B ∧ A ∩ B = {} ∧ A ≠ {} ∧ B ≠ {}" proof (intro exI conjI) have"frontier (∪{C ∈ components (- S ∩ - T). frontier C ⊆ S}) ⊆ S" using subset_trans [OF frontier_Union_subset_closure] by (metis (no_types, lifting) SUP_least ‹closed S› closure_minimal mem_Collect_eq) thenhave"frontier ?S ⊆ S" by (simp add: frontier_subset_eq assms subset_trans [OF frontier_Un_subset]) thenshow"closed ?S" using frontier_subset_eq by fastforce have"frontier (∪{C ∈ components (- S ∩ - T). frontier C ⊆ T}) ⊆ T" using subset_trans [OF frontier_Union_subset_closure] by (metis (no_types, lifting) SUP_least ‹closed T› closure_minimal mem_Collect_eq) thenhave"frontier ?T ⊆ T" by (simp add: frontier_subset_eq assms subset_trans [OF frontier_Un_subset]) thenshow"closed ?T" using frontier_subset_eq by fastforce have"UNIV ⊆ (S ∪ T) ∪∪(components(- (S ∪ T)))" using Union_components by blast alsohave"... ⊆ ?S ∪ ?T" proof - have"C ∈ components (-(S ∪ T)) ∧ frontier C ⊆ S ∨ C ∈ components (-(S ∪ T)) ∧ frontier C ⊆ T" if"C ∈ components (- (S ∪ T))""C ≠ {}"for C using * [OF that] that by clarify (metis (no_types, lifting) UnE ‹closed S›‹closed T› closed_Un disjoint_iff_not_equal frontier_of_components_closed_complement subsetCE) thenshow ?thesis by blast qed finallyshow"UNIV ⊆ ?S ∪ ?T" . have"∪{C ∈ components (- (S ∪ T)). frontier C ⊆ S} ∪ ∪{C ∈ components (- (S ∪ T)). frontier C ⊆ T} ⊆ - (S ∪ T)" using in_components_subset by fastforce moreoverhave"∪{C ∈ components (- (S ∪ T)). frontier C ⊆ S} ∩ ∪{C ∈ components (- (S ∪ T)). frontier C ⊆ T} = {}" proof - have"C ∩ C' = {}"if"C ∈ components (- (S ∪ T))""frontier C ⊆ S" "C' ∈ components (- (S ∪ T))""frontier C' ⊆ T"for C C' proof - have NUN: "- S ∩ - T ≠ UNIV" using‹T ≠ {}›by blast have"C ≠ C'" proof assume"C = C'" with that have"frontier C' ⊆ S ∩ T" by simp alsohave"... = {}" using‹S ∩ T = {}›by blast finallyhave"C' = {} ∨ C' = UNIV" using frontier_eq_empty by auto thenshow False using‹C = C'› NUN that by (force simp: dest: in_components_nonempty in_components_subset) qed with that show ?thesis by (simp add: components_nonoverlap [of _ "-(S ∪ T)"]) qed thenshow ?thesis by blast qed ultimatelyshow"?S ∩ ?T = {}" using ST by blast show"?S ≠ {}""?T ≠ {}" using‹S ≠ {}›‹T ≠ {}›by blast+ qed thenshow False by (metis Compl_disjoint connected_UNIV compl_bot_eq compl_unique connected_closedD inf_sup_absorb sup_compl_top_left1 top.extremum_uniqueI) qed
proposition separation_by_component_open: fixes S :: "'a :: euclidean_space set" assumes"open S"and non: "¬ connected(- S)" obtains C where"C ∈ components S""¬ connected(- C)" proof - obtain T U where"closed T""closed U"and TU: "T ∪ U = - S""T ∩ U = {}""T ≠ {}""U ≠ {}" using assms by (auto simp: connected_closed_set closed_def) thenobtain C where C: "C ∈ components(-(T ∪ U))""C ≠ {}" and"frontier C ∩ T ≠ {}""frontier C ∩ U ≠ {}" using separation_by_component_open_aux [OF ‹closed T›‹closed U›‹T ∩ U = {}›] by force show"thesis" proof show"C ∈ components S" using C(1) TU(1) by auto show"¬ connected (- C)" proof assume"connected (- C)" thenhave"connected (frontier C)" using connected_frontier_simple [of C] ‹C ∈ components S› in_components_connected by blast thenshow False unfolding connected_closed by (metis C(1) TU(2) ‹closed T›‹closed U›‹frontier C ∩ T ≠ {}›‹frontier C ∩ U ≠ {}› closed_Un frontier_of_components_closed_complement inf_bot_right inf_commute) qed qed qed
lemma separation_by_Un_open: fixes S :: "'a :: euclidean_space set" assumes"open S""open T""S ∩ T = {}"and cS: "connected(-S)"and cT: "connected(-T)" shows"connected(- (S ∪ T))" using assms unicoherent_UNIV unfolding unicoherent_def by force
lemma nonseparation_by_component_eq: fixes S :: "'a :: euclidean_space set" assumes"open S ∨ closed S" shows"((∀C ∈ components S. connected(-C)) ⟷ connected(- S))" by (metis assms component_complement_connected double_complement separation_by_component_closed separation_by_component_open)
text‹Another interesting equivalent of an inessential mapping into C-{0}›
proposition inessential_eq_extensible: fixes f :: "'a::euclidean_space ==> complex" assumes"closed S" shows"(∃a. homotopic_with_canon (λh. True) S (-{0}) f (λt. a)) ⟷ (∃g. continuous_on UNIV g ∧ (∀x ∈ S. g x = f x) ∧ (∀x. g x ≠ 0))"
(is"?lhs = ?rhs") proof assume ?lhs thenobtain a where a: "homotopic_with_canon (λh. True) S (-{0}) f (λt. a)" .. show ?rhs proof (cases "S = {}") case True with a show ?thesis by force next case False have anr: "ANR (-{0::complex})" by (simp add: ANR_delete open_Compl open_imp_ANR) obtain g where contg: "continuous_on UNIV g"and gim: "g ∈ UNIV → -{0}" and gf: "∧x. x ∈ S ==> g x = f x" proof (rule Borsuk_homotopy_extension_homotopic [OF _ _ continuous_on_const _ homotopic_with_symD [OF a]]) show"closedin (top_of_set UNIV) S" using assms by auto show"(λt. a) ∈ UNIV → - {0}" using a homotopic_with_imp_subset2 False by blast qed (use anr that in‹force+›) thenshow ?thesis by force qed next assume ?rhs thenobtain g where contg: "continuous_on UNIV g" and gf: "∧x. x ∈ S ==> g x = f x"and non0: "∧x. g x ≠ 0" by metis obtain h k::"'a==>'a"where hk: "homeomorphism (ball 0 1) UNIV h k" using homeomorphic_ball01_UNIV homeomorphic_def by blast thenhave"continuous_on (ball 0 1) (g ∘ h)" by (meson contg continuous_on_compose continuous_on_subset homeomorphism_cont1 top_greatest) thenobtain j where contj: "continuous_on (ball 0 1) j" and j: "∧z. z ∈ ball 0 1 ==> exp(j z) = (g ∘ h) z" by (metis (mono_tags, opaque_lifting) continuous_logarithm_on_ball comp_apply non0) have [simp]: "∧x. x ∈ S ==> h (k x) = x" using hk homeomorphism_apply2 by blast have"∃ζ. continuous_on S ζ∧ (∀x∈S. f x = exp (ζ x))" proof (intro exI conjI ballI) show"continuous_on S (j ∘ k)" proof (rule continuous_on_compose) show"continuous_on S k" by (meson continuous_on_subset hk homeomorphism_cont2 top_greatest) show"continuous_on (k ` S) j" by (auto intro: continuous_on_subset [OF contj] simp flip: homeomorphism_image2 [OF hk]) qed show"f x = exp ((j ∘ k) x)"if"x ∈ S"for x by (metis UNIV_I comp_apply gf hk homeomorphism_def image_eqI j that) qed thenshow ?lhs by (simp add: inessential_eq_continuous_logarithm) qed
lemma inessential_on_clopen_Union: fixesF :: "'a::euclidean_space set set" assumes T: "path_connected T" and"∧S. S ∈F==> closedin (top_of_set (∪F)) S" and"∧S. S ∈F==> openin (top_of_set (∪F)) S" and hom: "∧S. S ∈F==>∃a. homotopic_with_canon (λx. True) S T f (λx. a)" obtains a where"homotopic_with_canon (λx. True) (∪F) T f (λx. a)" proof (cases "∪F = {}") case True with that show ?thesis using homotopic_with_canon_on_empty by fastforce next case False thenobtain C where"C ∈F""C ≠ {}" by blast thenobtain a where clo: "closedin (top_of_set (∪F)) C" and ope: "openin (top_of_set (∪F)) C" and"homotopic_with_canon (λx. True) C T f (λx. a)" using assms by blast with‹C ≠ {}›have"f ∈ C → T""a ∈ T" using homotopic_with_imp_subset1 homotopic_with_imp_subset2 by blast+ have"homotopic_with_canon (λx. True) (∪F) T f (λx. a)" proof (rule homotopic_on_clopen_Union) show"∧S. S ∈F==> closedin (top_of_set (∪F)) S" "∧S. S ∈F==> openin (top_of_set (∪F)) S" by (simp_all add: assms) show"homotopic_with_canon (λx. True) S T f (λx. a)"if"S ∈F"for S proof (cases "S = {}") case False thenobtain b where"b ∈ S" by blast obtain c where c: "homotopic_with_canon (λx. True) S T f (λx. c)" using‹S ∈F› hom by blast thenhave"c ∈ T" using‹b ∈ S› homotopic_with_imp_subset2 by blast thenhave"homotopic_with_canon (λx. True) S T (λx. a) (λx. c)" using T ‹a ∈ T›by (simp add: homotopic_constant_maps path_connected_component) thenshow ?thesis using c homotopic_with_symD homotopic_with_trans by blast qed (simp add: homotopic_on_empty) qed thenshow ?thesis .. qed
proposition Janiszewski_dual: fixes S :: "complex set" assumes"compact S""compact T""connected S""connected T""connected(- (S ∪ T))" shows"connected(S ∩ T)" by (meson Borsukian_imp_unicoherent Borsukian_separation_compact assms closed_subset compact_Un
compact_imp_closed sup_ge1 sup_ge2 unicoherentD)
end
Messung V0.5 in Prozent
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.525Bemerkung:
(vorverarbeitet am 2026-05-01)
¤
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.