(* Title: HOL/Analysis/Jordan_Curve.thy Authors: LC Paulson, based on material from HOL Light *) section ‹The Jordan Curve Theorem and Applications› theory Jordan_Curve imports Arcwise_Connected Further_Topology begin subsection‹Janiszewski's theorem› lemma Janiszewski_weak: fixes a b::complex assumes "compact S" "compact T" and conST: "connected(S ∩ T)" and ccS: "connected_component (- S) a b" and ccT: "connected_component (- T) a b" shows "connected_component (- (S ∪ T)) a b" proof - have [simp]: "a ∉ S" "a ∉ T" "b ∉ S" "b ∉ T" by (meson ComplD ccS ccT connected_component_in)+ have clo: "closedin (top_of_set (S ∪ T)) S" "closedin (top_of_set (S ∪ T)) T" by (simp_all add: assms closed_subset compact_imp_closed) obtain g where contg: "continuous_on S g" and g: "⋀x. x ∈ S ⟹ exp (𝗂* of_real (g x)) = (x - a) /⇩_{R}cmod (x - a) / ((x - b) /⇩_{R}cmod (x - b))" using ccS ‹compact S› apply (simp add: Borsuk_maps_homotopic_in_connected_component_eq [symmetric]) apply (subst (asm) homotopic_circlemaps_divide) apply (auto simp: inessential_eq_continuous_logarithm_circle) done obtain h where conth: "continuous_on T h" and h: "⋀x. x ∈ T ⟹ exp (𝗂* of_real (h x)) = (x - a) /⇩_{R}cmod (x - a) / ((x - b) /⇩_{R}cmod (x - b))" using ccT ‹compact T› apply (simp add: Borsuk_maps_homotopic_in_connected_component_eq [symmetric]) apply (subst (asm) homotopic_circlemaps_divide) apply (auto simp: inessential_eq_continuous_logarithm_circle) done have "continuous_on (S ∪ T) (λx. (x - a) /⇩_{R}cmod (x - a))" "continuous_on (S ∪ T) (λx. (x - b) /⇩_{R}cmod (x - b))" by (intro continuous_intros; force)+ moreover have "(λx. (x - a) /⇩_{R}cmod (x - a)) ` (S ∪ T) ⊆ sphere 0 1" "(λx. (x - b) /⇩_{R}cmod (x - b)) ` (S ∪ T) ⊆ sphere 0 1" by (auto simp: divide_simps) moreover have "∃g. continuous_on (S ∪ T) g ∧ (∀x∈S ∪ T. (x - a) /⇩_{R}cmod (x - a) / ((x - b) /⇩_{R}cmod (x - b)) = exp (𝗂*complex_of_real (g x)))" proof (cases "S ∩ T = {}") case True then have "continuous_on (S ∪ T) (λx. if x ∈ S then g x else h x)" using continuous_on_cases_local [OF clo contg conth] by (meson disjoint_iff) then show ?thesis by (rule_tac x="(λx. if x ∈ S then g x else h x)" in exI) (auto simp: g h) next case False have diffpi: "∃n. g x = h x + 2* of_int n*pi" if "x ∈ S ∩ T" for x proof - have "exp (𝗂* of_real (g x)) = exp (𝗂* of_real (h x))" using that by (simp add: g h) then obtain n where "complex_of_real (g x) = complex_of_real (h x) + 2* of_int n*complex_of_real pi" apply (simp add: exp_eq) by (metis complex_i_not_zero distrib_left mult.commute mult_cancel_left) then show ?thesis using of_real_eq_iff by (fastforce intro!: exI [where x=n]) qed have contgh: "continuous_on (S ∩ T) (λx. g x - h x)" by (intro continuous_intros continuous_on_subset [OF contg] continuous_on_subset [OF conth]) auto moreover have disc: "∃e>0. ∀y. y ∈ S ∩ T ∧ g y - h y ≠ g x - h x ⟶ e ≤ norm ((g y - h y) - (g x - h x))" if "x ∈ S ∩ T" for x proof - obtain nx where nx: "g x = h x + 2* of_int nx*pi" using ‹x ∈ S ∩ T› diffpi by blast have "2*pi ≤ norm (g y - h y - (g x - h x))" if y: "y ∈ S ∩ T" and neq: "g y - h y ≠ g x - h x" for y proof - obtain ny where ny: "g y = h y + 2* of_int ny*pi" using ‹y ∈ S ∩ T› diffpi by blast { assume "nx ≠ ny" then have "1 ≤ ¦real_of_int ny - real_of_int nx¦" by linarith then have "(2*pi)*1 ≤ (2*pi)*¦real_of_int ny - real_of_int nx¦" by simp also have "... = ¦2*real_of_int ny*pi - 2*real_of_int nx*pi¦" by (simp add: algebra_simps abs_if) finally have "2*pi ≤ ¦2*real_of_int ny*pi - 2*real_of_int nx*pi¦" by simp } with neq show ?thesis by (simp add: nx ny) qed then show ?thesis by (rule_tac x="2*pi" in exI) auto qed ultimately have "(λx. g x - h x) constant_on S ∩ T" using continuous_discrete_range_constant [OF conST contgh] by blast then obtain z where z: "⋀x. x ∈ S ∩ T ⟹ g x - h x = z" by (auto simp: constant_on_def) obtain w where "exp(𝗂 * of_real(h w)) = exp (𝗂 * of_real(z + h w))" using disc z False by auto (metis diff_add_cancel g h of_real_add) then have [simp]: "exp (𝗂* of_real z) = 1" by (metis cis_conv_exp cis_mult exp_not_eq_zero mult_cancel_right1) show ?thesis proof (intro exI conjI) show "continuous_on (S ∪ T) (λx. if x ∈ S then g x else z + h x)" by (intro continuous_intros continuous_on_cases_local [OF clo contg] conth) (use z in force) qed (auto simp: g h algebra_simps exp_add) qed ultimately have "homotopic_with_canon (λx. True) (S ∪ T) (sphere 0 1) (λx. (x - a) /⇩_{R}cmod (x - a)) (λx. (x - b) /⇩_{R}cmod (x - b))" by (subst homotopic_circlemaps_divide) (auto simp: inessential_eq_continuous_logarithm_circle) moreover have "compact (S ∪ T)" using assms by blast ultimately show ?thesis using assms Borsuk_maps_homotopic_in_connected_component_eq by fastforce qed theorem Janiszewski: fixes a b :: complex assumes "compact S" "closed T" and conST: "connected (S ∩ T)" and ccS: "connected_component (- S) a b" and ccT: "connected_component (- T) a b" shows "connected_component (- (S ∪ T)) a b" proof - have "path_component(- T) a b" by (simp add: ‹closed T› ccT open_Compl open_path_connected_component) then obtain g where g: "path g" "path_image g ⊆ - T" "pathstart g = a" "pathfinish g = b" by (auto simp: path_component_def) then obtain C where C: "compact C" "connected C" "a ∈ C" "b ∈ C" "C ∩ T = {}" by fastforce obtain r where "0 < r" and r: "C ∪ S ⊆ ball 0 r" by (metis ‹compact C› ‹compact S› bounded_Un compact_imp_bounded bounded_subset_ballD) have "connected_component (- (S ∪ (T ∩ cball 0 r ∪ sphere 0 r))) a b" proof (rule Janiszewski_weak [OF ‹compact S›]) show comT': "compact ((T ∩ cball 0 r) ∪ sphere 0 r)" by (simp add: ‹closed T› closed_Int_compact compact_Un) have "S ∩ (T ∩ cball 0 r ∪ sphere 0 r) = S ∩ T" using r by auto with conST show "connected (S ∩ (T ∩ cball 0 r ∪ sphere 0 r))" by simp show "connected_component (- (T ∩ cball 0 r ∪ sphere 0 r)) a b" using conST C r apply (simp add: connected_component_def) apply (rule_tac x=C in exI) by auto qed (simp add: ccS) then obtain U where U: "connected U" "U ⊆ - S" "U ⊆ - T ∪ - cball 0 r" "U ⊆ - sphere 0 r" "a ∈ U" "b ∈ U" by (auto simp: connected_component_def) show ?thesis unfolding connected_component_def proof (intro exI conjI) show "U ⊆ - (S ∪ T)" using U r ‹0 < r› ‹a ∈ C› connected_Int_frontier [of U "cball 0 r"] apply simp by (metis ball_subset_cball compl_inf disjoint_eq_subset_Compl disjoint_iff_not_equal inf.orderE inf_sup_aci(3) subsetCE) qed (auto simp: U) qed lemma Janiszewski_connected: fixes S :: "complex set" assumes ST: "compact S" "closed T" "connected(S ∩ T)" and notST: "connected (- S)" "connected (- T)" shows "connected(- (S ∪ T))" using Janiszewski [OF ST] by (metis IntD1 IntD2 notST compl_sup connected_iff_connected_component) subsection‹The Jordan Curve theorem› lemma exists_double_arc: fixes g :: "real ⇒ 'a::real_normed_vector" assumes "simple_path g" "pathfinish g = pathstart g" "a ∈ path_image g" "b ∈ path_image g" "a ≠ b" obtains u d where "arc u" "arc d" "pathstart u = a" "pathfinish u = b" "pathstart d = b" "pathfinish d = a" "(path_image u) ∩ (path_image d) = {a,b}" "(path_image u) ∪ (path_image d) = path_image g" proof - obtain u where u: "0 ≤ u" "u ≤ 1" "g u = a" using assms by (auto simp: path_image_def) define h where "h ≡ shiftpath u g" have "simple_path h" using ‹simple_path g› simple_path_shiftpath ‹0 ≤ u› ‹u ≤ 1› assms(2) h_def by blast have "pathstart h = g u" by (simp add: ‹u ≤ 1› h_def pathstart_shiftpath) have "pathfinish h = g u" by (simp add: ‹0 ≤ u› assms h_def pathfinish_shiftpath) have pihg: "path_image h = path_image g" by (simp add: ‹0 ≤ u› ‹u ≤ 1› assms h_def path_image_shiftpath) then obtain v where v: "0 ≤ v" "v ≤ 1" "h v = b" using assms by (metis (mono_tags, lifting) atLeastAtMost_iff imageE path_image_def) show ?thesis proof show "arc (subpath 0 v h)" by (metis (no_types) ‹pathstart h = g u› ‹simple_path h› arc_simple_path_subpath ‹a ≠ b› atLeastAtMost_iff zero_le_one order_refl pathstart_def u(3) v) show "arc (subpath v 1 h)" by (metis (no_types) ‹pathfinish h = g u› ‹simple_path h› arc_simple_path_subpath ‹a ≠ b› atLeastAtMost_iff zero_le_one order_refl pathfinish_def u(3) v) show "pathstart (subpath 0 v h) = a" by (metis ‹pathstart h = g u› pathstart_def pathstart_subpath u(3)) show "pathfinish (subpath 0 v h) = b" "pathstart (subpath v 1 h) = b" by (simp_all add: v(3)) show "pathfinish (subpath v 1 h) = a" by (metis ‹pathfinish h = g u› pathfinish_def pathfinish_subpath u(3)) show "path_image (subpath 0 v h) ∩ path_image (subpath v 1 h) = {a, b}" proof have "loop_free h" using ‹simple_path h› simple_path_def by blast then show "path_image (subpath 0 v h) ∩ path_image (subpath v 1 h) ⊆ {a, b}" using v ‹pathfinish (subpath v 1 h) = a› apply (clarsimp simp add: loop_free_def path_image_subpath Ball_def) by (smt (verit)) show "{a, b} ⊆ path_image (subpath 0 v h) ∩ path_image (subpath v 1 h)" using v ‹pathstart (subpath 0 v h) = a› ‹pathfinish (subpath v 1 h) = a› by (auto simp: path_image_subpath image_iff Bex_def) qed show "path_image (subpath 0 v h) ∪ path_image (subpath v 1 h) = path_image g" using v path_image_subpath pihg path_image_def by (metis (full_types) image_Un ivl_disj_un_two_touch(4)) qed qed theorem✐‹tag unimportant› Jordan_curve: fixes c :: "real ⇒ complex" assumes "simple_path c" and loop: "pathfinish c = pathstart c" obtains inner outer where "inner ≠ {}" "open inner" "connected inner" "outer ≠ {}" "open outer" "connected outer" "bounded inner" "¬ bounded outer" "inner ∩ outer = {}" "inner ∪ outer = - path_image c" "frontier inner = path_image c" "frontier outer = path_image c" proof - have "path c" by (simp add: assms simple_path_imp_path) have hom: "(path_image c) homeomorphic (sphere(0::complex) 1)" by (simp add: assms homeomorphic_simple_path_image_circle) with Jordan_Brouwer_separation have "¬ connected (- (path_image c))" by fastforce then obtain inner where inner: "inner ∈ components (- path_image c)" and "bounded inner" using cobounded_has_bounded_component [of "- (path_image c)"] using ‹¬ connected (- path_image c)› ‹simple_path c› bounded_simple_path_image by force obtain outer where outer: "outer ∈ components (- path_image c)" and "¬ bounded outer" using cobounded_unbounded_components [of "- (path_image c)"] using ‹path c› bounded_path_image by auto show ?thesis proof show "inner ≠ {}" using inner in_components_nonempty by auto show "open inner" by (meson ‹simple_path c› compact_imp_closed compact_simple_path_image inner open_Compl open_components) show "connected inner" using in_components_connected inner by blast show "outer ≠ {}" using outer in_components_nonempty by auto show "open outer" by (meson ‹simple_path c› compact_imp_closed compact_simple_path_image outer open_Compl open_components) show "connected outer" using in_components_connected outer by blast show inner_outer: "inner ∩ outer = {}" by (meson ‹¬ bounded outer› ‹bounded inner› ‹connected outer› bounded_subset components_maximal in_components_subset inner outer) show fro_inner: "frontier inner = path_image c" by (simp add: Jordan_Brouwer_frontier [OF hom inner]) show fro_outer: "frontier outer = path_image c" by (simp add: Jordan_Brouwer_frontier [OF hom outer]) have False if m: "middle ∈ components (- path_image c)" and "middle ≠ inner" "middle ≠ outer" for middle proof - have "frontier middle = path_image c" by (simp add: Jordan_Brouwer_frontier [OF hom] that) obtain middle: "open middle" "connected middle" "middle ≠ {}" by (metis fro_inner frontier_closed in_components_maximal m open_Compl open_components) obtain a0 b0 where "a0 ∈ path_image c" "b0 ∈ path_image c" "a0 ≠ b0" using simple_path_image_uncountable [OF ‹simple_path c›] by (metis Diff_cancel countable_Diff_eq countable_empty insert_iff subsetI subset_singleton_iff) obtain a b g where ab: "a ∈ path_image c" "b ∈ path_image c" "a ≠ b" and g: "arc g" "pathstart g = a" "pathfinish g = b" and pag_sub: "path_image g - {a,b} ⊆ middle" proof (rule dense_accessible_frontier_point_pairs [OF ‹open middle› ‹connected middle›, of "path_image c ∩ ball a0 (dist a0 b0)" "path_image c ∩ ball b0 (dist a0 b0)"]) show "openin (top_of_set (frontier middle)) (path_image c ∩ ball a0 (dist a0 b0))" "openin (top_of_set (frontier middle)) (path_image c ∩ ball b0 (dist a0 b0))" by (simp_all add: ‹frontier middle = path_image c› openin_open_Int) show "path_image c ∩ ball a0 (dist a0 b0) ≠ path_image c ∩ ball b0 (dist a0 b0)" using ‹a0 ≠ b0› ‹b0 ∈ path_image c› by auto show "path_image c ∩ ball a0 (dist a0 b0) ≠ {}" using ‹a0 ∈ path_image c› ‹a0 ≠ b0› by auto show "path_image c ∩ ball b0 (dist a0 b0) ≠ {}" using ‹b0 ∈ path_image c› ‹a0 ≠ b0› by auto qed (use arc_distinct_ends arc_imp_simple_path simple_path_endless that in fastforce) obtain u d where "arc u" "arc d" and "pathstart u = a" "pathfinish u = b" "pathstart d = b" "pathfinish d = a" and ud_ab: "(path_image u) ∩ (path_image d) = {a,b}" and ud_Un: "(path_image u) ∪ (path_image d) = path_image c" using exists_double_arc [OF assms ab] by blast obtain x y where "x ∈ inner" "y ∈ outer" using ‹inner ≠ {}› ‹outer ≠ {}› by auto have "inner ∩ middle = {}" "middle ∩ outer = {}" using components_nonoverlap inner outer m that by blast+ have "connected_component (- (path_image u ∪ path_image g ∪ (path_image d ∪ path_image g))) x y" proof (rule Janiszewski) show "compact (path_image u ∪ path_image g)" by (simp add: ‹arc g› ‹arc u› compact_Un compact_arc_image) show "closed (path_image d ∪ path_image g)" by (simp add: ‹arc d› ‹arc g› closed_Un closed_arc_image) show "connected ((path_image u ∪ path_image g) ∩ (path_image d ∪ path_image g))" using ud_ab by (metis Un_insert_left g connected_arc_image insert_absorb pathfinish_in_path_image pathstart_in_path_image sup_bot_left sup_commute sup_inf_distrib1) show "connected_component (- (path_image u ∪ path_image g)) x y" unfolding connected_component_def proof (intro exI conjI) have "connected ((inner ∪ (path_image c - path_image u)) ∪ (outer ∪ (path_image c - path_image u)))" proof (rule connected_Un) show "connected (inner ∪ (path_image c - path_image u))" using connected_intermediate_closure [OF ‹connected inner›] by (metis Diff_subset closure_Un_frontier dual_order.refl fro_inner sup.mono sup_ge1) show "connected (outer ∪ (path_image c - path_image u))" using connected_intermediate_closure [OF ‹connected outer›] by (simp add: Diff_eq closure_Un_frontier fro_outer sup_inf_distrib1) have "(inner ∩ outer) ∪ (path_image c - path_image u) ≠ {}" using ‹arc d› ‹pathfinish d = a› ‹pathstart d = b› arc_imp_simple_path nonempty_simple_path_endless ud_Un ud_ab by fastforce then show "(inner ∪ (path_image c - path_image u)) ∩ (outer ∪ (path_image c - path_image u)) ≠ {}" by auto qed then show "connected (inner ∪ outer ∪ (path_image c - path_image u))" by (metis sup.right_idem sup_assoc sup_commute) have "inner ⊆ - path_image u" "outer ⊆ - path_image u" using in_components_subset inner outer ud_Un by auto moreover have "inner ⊆ - path_image g" "outer ⊆ - path_image g" using ‹inner ∩ middle = {}› ‹inner ⊆ - path_image u› using ‹middle ∩ outer = {}› ‹outer ⊆ - path_image u› pag_sub ud_ab by fastforce+ moreover have "path_image c - path_image u ⊆ - path_image g" using in_components_subset m pag_sub ud_ab by fastforce ultimately show "inner ∪ outer ∪ (path_image c - path_image u) ⊆ - (path_image u ∪ path_image g)" by force show "x ∈ inner ∪ outer ∪ (path_image c - path_image u)" by (auto simp: ‹x ∈ inner›) show "y ∈ inner ∪ outer ∪ (path_image c - path_image u)" by (auto simp: ‹y ∈ outer›) qed show "connected_component (- (path_image d ∪ path_image g)) x y" unfolding connected_component_def proof (intro exI conjI) have "connected ((inner ∪ (path_image c - path_image d)) ∪ (outer ∪ (path_image c - path_image d)))" proof (rule connected_Un) show "connected (inner ∪ (path_image c - path_image d))" using connected_intermediate_closure [OF ‹connected inner›] fro_inner by (simp add: closure_Un_frontier sup.coboundedI2) show "connected (outer ∪ (path_image c - path_image d))" using connected_intermediate_closure [OF ‹connected outer›] by (simp add: closure_Un_frontier fro_outer sup.coboundedI2) have "(inner ∩ outer) ∪ (path_image c - path_image d) ≠ {}" using ‹arc u› ‹pathfinish u = b› ‹pathstart u = a› arc_imp_simple_path nonempty_simple_path_endless ud_Un ud_ab by fastforce then show "(inner ∪ (path_image c - path_image d)) ∩ (outer ∪ (path_image c - path_image d)) ≠ {}" by auto qed then show "connected (inner ∪ outer ∪ (path_image c - path_image d))" by (metis sup.right_idem sup_assoc sup_commute) have "inner ⊆ - path_image d" "outer ⊆ - path_image d" using in_components_subset inner outer ud_Un by auto moreover have "inner ⊆ - path_image g" "outer ⊆ - path_image g" using ‹inner ∩ middle = {}› ‹inner ⊆ - path_image d› using ‹middle ∩ outer = {}› ‹outer ⊆ - path_image d› pag_sub ud_ab by fastforce+ moreover have "path_image c - path_image d ⊆ - path_image g" using in_components_subset m pag_sub ud_ab by fastforce ultimately show "inner ∪ outer ∪ (path_image c - path_image d) ⊆ - (path_image d ∪ path_image g)" by force show "x ∈ inner ∪ outer ∪ (path_image c - path_image d)" by (auto simp: ‹x ∈ inner›) show "y ∈ inner ∪ outer ∪ (path_image c - path_image d)" by (auto simp: ‹y ∈ outer›) qed qed then have "connected_component (- (path_image u ∪ path_image d ∪ path_image g)) x y" by (simp add: Un_ac) moreover have "¬(connected_component (- (path_image c)) x y)" by (metis (no_types, lifting) ‹¬ bounded outer› ‹bounded inner› ‹x ∈ inner› ‹y ∈ outer› componentsE connected_component_eq inner mem_Collect_eq outer) ultimately show False by (auto simp: ud_Un [symmetric] connected_component_def) qed then have "components (- path_image c) = {inner,outer}" using inner outer by blast then have "Union (components (- path_image c)) = inner ∪ outer" by simp then show "inner ∪ outer = - path_image c" by auto qed (auto simp: ‹bounded inner› ‹¬ bounded outer›) qed corollary✐‹tag unimportant› Jordan_disconnected: fixes c :: "real ⇒ complex" assumes "simple_path c" "pathfinish c = pathstart c" shows "¬ connected(- path_image c)" using Jordan_curve [OF assms] by (metis Jordan_Brouwer_separation assms homeomorphic_simple_path_image_circle zero_less_one) corollary Jordan_inside_outside: fixes c :: "real ⇒ complex" assumes "simple_path c" "pathfinish c = pathstart c" shows "inside(path_image c) ≠ {} ∧ open(inside(path_image c)) ∧ connected(inside(path_image c)) ∧ outside(path_image c) ≠ {} ∧ open(outside(path_image c)) ∧ connected(outside(path_image c)) ∧ bounded(inside(path_image c)) ∧ ¬ bounded(outside(path_image c)) ∧ inside(path_image c) ∩ outside(path_image c) = {} ∧ inside(path_image c) ∪ outside(path_image c) = - path_image c ∧ frontier(inside(path_image c)) = path_image c ∧ frontier(outside(path_image c)) = path_image c" proof - obtain inner outer where *: "inner ≠ {}" "open inner" "connected inner" "outer ≠ {}" "open outer" "connected outer" "bounded inner" "¬ bounded outer" "inner ∩ outer = {}" "inner ∪ outer = - path_image c" "frontier inner = path_image c" "frontier outer = path_image c" using Jordan_curve [OF assms] by blast then have inner: "inside(path_image c) = inner" by (metis dual_order.antisym inside_subset interior_eq interior_inside_frontier) have outer: "outside(path_image c) = outer" using ‹inner ∪ outer = - path_image c› ‹inside (path_image c) = inner› outside_inside ‹inner ∩ outer = {}› by auto show ?thesis using * by (auto simp: inner outer) qed subsubsection‹Triple-curve or "theta-curve" theorem› text‹Proof that there is no fourth component taken from Kuratowski's Topology vol 2, para 61, II.› theorem split_inside_simple_closed_curve: fixes c :: "real ⇒ complex" assumes "simple_path c1" and c1: "pathstart c1 = a" "pathfinish c1 = b" and "simple_path c2" and c2: "pathstart c2 = a" "pathfinish c2 = b" and "simple_path c" and c: "pathstart c = a" "pathfinish c = b" and "a ≠ b" and c1c2: "path_image c1 ∩ path_image c2 = {a,b}" and c1c: "path_image c1 ∩ path_image c = {a,b}" and c2c: "path_image c2 ∩ path_image c = {a,b}" and ne_12: "path_image c ∩ inside(path_image c1 ∪ path_image c2) ≠ {}" obtains "inside(path_image c1 ∪ path_image c) ∩ inside(path_image c2 ∪ path_image c) = {}" "inside(path_image c1 ∪ path_image c) ∪ inside(path_image c2 ∪ path_image c) ∪ (path_image c - {a,b}) = inside(path_image c1 ∪ path_image c2)" proof - let ?Θ = "path_image c" let ?Θ1 = "path_image c1" let ?Θ2 = "path_image c2" have sp: "simple_path (c1 +++ reversepath c2)" "simple_path (c1 +++ reversepath c)" "simple_path (c2 +++ reversepath c)" using assms by (auto simp: simple_path_join_loop_eq arc_simple_path simple_path_reversepath) then have op_in12: "open (inside (?Θ1 ∪ ?Θ2))" and op_out12: "open (outside (?Θ1 ∪ ?Θ2))" and op_in1c: "open (inside (?Θ1 ∪ ?Θ))" and op_in2c: "open (inside (?Θ2 ∪ ?Θ))" and op_out1c: "open (outside (?Θ1 ∪ ?Θ))" and op_out2c: "open (outside (?Θ2 ∪ ?Θ))" and co_in1c: "connected (inside (?Θ1 ∪ ?Θ))" and co_in2c: "connected (inside (?Θ2 ∪ ?Θ))" and co_out12c: "connected (outside (?Θ1 ∪ ?Θ2))" and co_out1c: "connected (outside (?Θ1 ∪ ?Θ))" and co_out2c: "connected (outside (?Θ2 ∪ ?Θ))" and pa_c: "?Θ - {pathstart c, pathfinish c} ⊆ - ?Θ1" "?Θ - {pathstart c, pathfinish c} ⊆ - ?Θ2" and pa_c1: "?Θ1 - {pathstart c1, pathfinish c1} ⊆ - ?Θ2" "?Θ1 - {pathstart c1, pathfinish c1} ⊆ - ?Θ" and pa_c2: "?Θ2 - {pathstart c2, pathfinish c2} ⊆ - ?Θ1" "?Θ2 - {pathstart c2, pathfinish c2} ⊆ - ?Θ" and co_c: "connected(?Θ - {pathstart c,pathfinish c})" and co_c1: "connected(?Θ1 - {pathstart c1,pathfinish c1})" and co_c2: "connected(?Θ2 - {pathstart c2,pathfinish c2})" and fr_in: "frontier(inside(?Θ1 ∪ ?Θ2)) = ?Θ1 ∪ ?Θ2" "frontier(inside(?Θ2 ∪ ?Θ)) = ?Θ2 ∪ ?Θ" "frontier(inside(?Θ1 ∪ ?Θ)) = ?Θ1 ∪ ?Θ" and fr_out: "frontier(outside(?Θ1 ∪ ?Θ2)) = ?Θ1 ∪ ?Θ2" "frontier(outside(?Θ2 ∪ ?Θ)) = ?Θ2 ∪ ?Θ" "frontier(outside(?Θ1 ∪ ?Θ)) = ?Θ1 ∪ ?Θ" using Jordan_inside_outside [of "c1 +++ reversepath c2"] using Jordan_inside_outside [of "c1 +++ reversepath c"] using Jordan_inside_outside [of "c2 +++ reversepath c"] assms apply (simp_all add: path_image_join closed_Un closed_simple_path_image open_inside open_outside) apply (blast | metis connected_simple_path_endless)+ done have inout_12: "inside (?Θ1 ∪ ?Θ2) ∩ (?Θ - {pathstart c, pathfinish c}) ≠ {}" by (metis (no_types, lifting) c c1c ne_12 Diff_Int_distrib Diff_empty Int_empty_right Int_left_commute inf_sup_absorb inf_sup_aci(1) inside_no_overlap) have pi_disjoint: "?Θ ∩ outside(?Θ1 ∪ ?Θ2) = {}" proof (rule ccontr) assume "?Θ ∩ outside (?Θ1 ∪ ?Θ2) ≠ {}" then show False using connectedD [OF co_c, of "inside(?Θ1 ∪ ?Θ2)" "outside(?Θ1 ∪ ?Θ2)"] using c c1c2 pa_c op_in12 op_out12 inout_12 apply clarsimp by (smt (verit, ccfv_threshold) Diff_Int_distrib Diff_cancel Diff_empty Int_assoc inf_sup_absorb inf_sup_aci(1) outside_no_overlap) qed have out_sub12: "outside(?Θ1 ∪ ?Θ2) ⊆ outside(?Θ1 ∪ ?Θ)" "outside(?Θ1 ∪ ?Θ2) ⊆ outside(?Θ2 ∪ ?Θ)" by (metis Un_commute pi_disjoint outside_Un_outside_Un)+ have pa1_disj_in2: "?Θ1 ∩ inside (?Θ2 ∪ ?Θ) = {}" proof (rule ccontr) assume ne: "?Θ1 ∩ inside (?Θ2 ∪ ?Θ) ≠ {}" have 1: "inside (?Θ ∪ ?Θ2) ∩ ?Θ = {}" by (metis (no_types) Diff_Int_distrib Diff_cancel inf_sup_absorb inf_sup_aci(3) inside_no_overlap) have 2: "outside (?Θ ∪ ?Θ2) ∩ ?Θ = {}" by (metis (no_types) Int_empty_right Int_left_commute inf_sup_absorb outside_no_overlap) have "path_image c1 ∩ outside (path_image c2 ∪ path_image c) = {}" using connectedD [OF co_c1, of "inside(?Θ2 ∪ ?Θ)" "outside(?Θ2 ∪ ?Θ)"] pa_c1 op_in2c op_out2c ne c1 c2c 1 2 by (auto simp: inf_sup_aci) then have "outside (?Θ2 ∪ ?Θ) ⊆ outside (?Θ1 ∪ ?Θ2)" by (metis outside_Un_outside_Un sup_commute) with out_sub12 have "outside(?Θ1 ∪ ?Θ2) = outside(?Θ2 ∪ ?Θ)" by blast then have "frontier(outside(?Θ1 ∪ ?Θ2)) = frontier(outside(?Θ2 ∪ ?Θ))" by simp then show False using inout_12 pi_disjoint c c1c c2c fr_out by auto qed have pa2_disj_in1: "?Θ2 ∩ inside(?Θ1 ∪ ?Θ) = {}" proof (rule ccontr) assume ne: "?Θ2 ∩ inside (?Θ1 ∪ ?Θ) ≠ {}" have 1: "inside (?Θ ∪ ?Θ1) ∩ ?Θ = {}" by (metis (no_types) Diff_Int_distrib Diff_cancel inf_sup_absorb inf_sup_aci(3) inside_no_overlap) have 2: "outside (?Θ ∪ ?Θ1) ∩ ?Θ = {}" by (metis (no_types) Int_empty_right Int_left_commute inf_sup_absorb outside_no_overlap) have "outside (?Θ1 ∪ ?Θ) ⊆ outside (?Θ1 ∪ ?Θ2)" apply (rule outside_Un_outside_Un) using connectedD [OF co_c2, of "inside(?Θ1 ∪ ?Θ)" "outside(?Θ1 ∪ ?Θ)"] pa_c2 op_in1c op_out1c ne c2 c1c 1 2 by (auto simp: inf_sup_aci) with out_sub12 have "outside(?Θ1 ∪ ?Θ2) = outside(?Θ1 ∪ ?Θ)" by blast then have "frontier(outside(?Θ1 ∪ ?Θ2)) = frontier(outside(?Θ1 ∪ ?Θ))" by simp then show False using inout_12 pi_disjoint c c1c c2c fr_out by auto qed have in_sub_in1: "inside(?Θ1 ∪ ?Θ) ⊆ inside(?Θ1 ∪ ?Θ2)" using pa2_disj_in1 out_sub12 by (auto simp: inside_outside) have in_sub_in2: "inside(?Θ2 ∪ ?Θ) ⊆ inside(?Θ1 ∪ ?Θ2)" using pa1_disj_in2 out_sub12 by (auto simp: inside_outside) have in_sub_out12: "inside(?Θ1 ∪ ?Θ) ⊆ outside(?Θ2 ∪ ?Θ)" proof fix x assume x: "x ∈ inside (?Θ1 ∪ ?Θ)" then have xnot: "x ∉ ?Θ" by (simp add: inside_def) obtain z where zim: "z ∈ ?Θ1" and zout: "z ∈ outside(?Θ2 ∪ ?Θ)" unfolding outside_inside using nonempty_simple_path_endless [OF ‹simple_path c1›] c1 c1c c1c2 pa1_disj_in2 by auto obtain e where "e > 0" and e: "ball z e ⊆ outside(?Θ2 ∪ ?Θ)" using zout op_out2c open_contains_ball_eq by blast have "z ∈ frontier (inside (?Θ1 ∪ ?Θ))" using zim by (auto simp: fr_in) then obtain w where w1: "w ∈ inside (?Θ1 ∪ ?Θ)" and dwz: "dist w z < e" using zim ‹e > 0› by (auto simp: frontier_def closure_approachable) then have w2: "w ∈ outside (?Θ2 ∪ ?Θ)" by (metis e dist_commute mem_ball subsetCE) then have "connected_component (- ?Θ2 ∩ - ?Θ) z w" unfolding connected_component_def by (metis co_out2c compl_sup inside_Un_outside sup_ge2 zout) moreover have "connected_component (- ?Θ2 ∩ - ?Θ) w x" unfolding connected_component_def using pa2_disj_in1 co_in1c x w1 union_with_outside by fastforce ultimately have eq: "connected_component_set (- ?Θ2 ∩ - ?Θ) x = connected_component_set (- ?Θ2 ∩ - ?Θ) z" by (metis (mono_tags, lifting) connected_component_eq mem_Collect_eq) show "x ∈ outside (?Θ2 ∪ ?Θ)" using zout x pa2_disj_in1 by (auto simp: outside_def eq xnot) qed have in_sub_out21: "inside(?Θ2 ∪ ?Θ) ⊆ outside(?Θ1 ∪ ?Θ)" proof fix x assume x: "x ∈ inside (?Θ2 ∪ ?Θ)" then have xnot: "x ∉ ?Θ" by (simp add: inside_def) obtain z where zim: "z ∈ ?Θ2" and zout: "z ∈ outside(?Θ1 ∪ ?Θ)" unfolding outside_inside using nonempty_simple_path_endless [OF ‹simple_path c2›] c1c2 c2 c2c pa2_disj_in1 by auto obtain e where "e > 0" and e: "ball z e ⊆ outside(?Θ1 ∪ ?Θ)" using zout op_out1c open_contains_ball_eq by blast have "z ∈ frontier (inside (?Θ2 ∪ ?Θ))" using zim by (auto simp: fr_in) then obtain w where w2: "w ∈ inside (?Θ2 ∪ ?Θ)" and dwz: "dist w z < e" using zim ‹e > 0› by (auto simp: frontier_def closure_approachable) then have w1: "w ∈ outside (?Θ1 ∪ ?Θ)" by (metis e dist_commute mem_ball subsetCE) then have "connected_component (- ?Θ1 ∩ - ?Θ) z w" unfolding connected_component_def by (metis Compl_Un co_out1c inside_Un_outside sup_ge2 zout) moreover have "connected_component (- ?Θ1 ∩ - ?Θ) w x" unfolding connected_component_def using pa1_disj_in2 co_in2c x w2 union_with_outside by fastforce ultimately have eq: "connected_component_set (- ?Θ1 ∩ - ?Θ) x = connected_component_set (- ?Θ1 ∩ - ?Θ) z" by (metis (no_types, lifting) connected_component_eq mem_Collect_eq) show "x ∈ outside (?Θ1 ∪ ?Θ)" using zout x pa1_disj_in2 by (auto simp: outside_def eq xnot) qed show ?thesis proof show "inside (?Θ1 ∪ ?Θ) ∩ inside (?Θ2 ∪ ?Θ) = {}" by (metis Int_Un_distrib in_sub_out12 bot_eq_sup_iff disjoint_eq_subset_Compl outside_inside) have *: "outside (?Θ1 ∪ ?Θ) ∩ outside (?Θ2 ∪ ?Θ) ⊆ outside (?Θ1 ∪ ?Θ2)" proof (rule components_maximal) show out_in: "outside (?Θ1 ∪ ?Θ2) ∈ components (- (?Θ1 ∪ ?Θ2))" unfolding outside_in_components co_out12c using co_out12c fr_out(1) by force have conn_U: "connected (- (closure (inside (?Θ1 ∪ ?Θ)) ∪ closure (inside (?Θ2 ∪ ?Θ))))" proof (rule Janiszewski_connected, simp_all) show "bounded (inside (?Θ1 ∪ ?Θ))" by (simp add: ‹simple_path c1› ‹simple_path c› bounded_inside bounded_simple_path_image) have if1: "- (inside (?Θ1 ∪ ?Θ) ∪ frontier (inside (?Θ1 ∪ ?Θ))) = - ?Θ1 ∩ - ?Θ ∩ - inside (?Θ1 ∪ ?Θ)" by (metis (no_types, lifting) Int_commute Jordan_inside_outside c c1 compl_sup path_image_join path_image_reversepath pathfinish_join pathfinish_reversepath pathstart_join pathstart_reversepath sp(2) closure_Un_frontier fr_out(3)) then show "connected (- closure (inside (?Θ1 ∪ ?Θ)))" by (metis Compl_Un outside_inside co_out1c closure_Un_frontier) have if2: "- (inside (?Θ2 ∪ ?Θ) ∪ frontier (inside (?Θ2 ∪ ?Θ))) = - ?Θ2 ∩ - ?Θ ∩ - inside (?Θ2 ∪ ?Θ)" by (metis (no_types, lifting) Int_commute Jordan_inside_outside c c2 compl_sup path_image_join path_image_reversepath pathfinish_join pathfinish_reversepath pathstart_join pathstart_reversepath sp(3) closure_Un_frontier fr_out(2)) then show "connected (- closure (inside (?Θ2 ∪ ?Θ)))" by (metis Compl_Un outside_inside co_out2c closure_Un_frontier) have "connected(?Θ)" by (metis ‹simple_path c› connected_simple_path_image) moreover have "closure (inside (?Θ1 ∪ ?Θ)) ∩ closure (inside (?Θ2 ∪ ?Θ)) = ?Θ" (is "?lhs = ?rhs") proof show "?lhs ⊆ ?rhs" proof clarify fix x assume x: "x ∈ closure (inside (?Θ1 ∪ ?Θ))" "x ∈ closure (inside (?Θ2 ∪ ?Θ))" then have "x ∉ inside (?Θ1 ∪ ?Θ)" by (meson closure_iff_nhds_not_empty in_sub_out12 inside_Int_outside op_in1c) with fr_in x show "x ∈ ?Θ" by (metis c1c c1c2 closure_Un_frontier pa1_disj_in2 Int_iff Un_iff insert_disjoint(2) insert_subset subsetI subset_antisym) qed show "?rhs ⊆ ?lhs" using if1 if2 closure_Un_frontier by fastforce qed ultimately show "connected (closure (inside (?Θ1 ∪ ?Θ)) ∩ closure (inside (?Θ2 ∪ ?Θ)))" by auto qed show "connected (outside (?Θ1 ∪ ?Θ) ∩ outside (?Θ2 ∪ ?Θ))" using fr_in conn_U by (simp add: closure_Un_frontier outside_inside Un_commute) show "outside (?Θ1 ∪ ?Θ) ∩ outside (?Θ2 ∪ ?Θ) ⊆ - (?Θ1 ∪ ?Θ2)" by clarify (metis Diff_Compl Diff_iff Un_iff inf_sup_absorb outside_inside) show "outside (?Θ1 ∪ ?Θ2) ∩ (outside (?Θ1 ∪ ?Θ) ∩ outside (?Θ2 ∪ ?Θ)) ≠ {}" by (metis Int_assoc out_in inf.orderE out_sub12(1) out_sub12(2) outside_in_components) qed show "inside (?Θ1 ∪ ?Θ) ∪ inside (?Θ2 ∪ ?Θ) ∪ (?Θ - {a, b}) = inside (?Θ1 ∪ ?Θ2)" (is "?lhs = ?rhs") proof have " path_image c - {a, b} ⊆ inside (path_image c1 ∪ path_image c2)" using c1c c2c inside_outside pi_disjoint by fastforce then show "?lhs ⊆ ?rhs" by (simp add: in_sub_in1 in_sub_in2) have "inside (?Θ1 ∪ ?Θ2) ⊆ inside (?Θ1 ∪ ?Θ) ∪ inside (?Θ2 ∪ ?Θ) ∪ (?Θ)" using Compl_anti_mono [OF *] by (force simp: inside_outside) moreover have "inside (?Θ1 ∪ ?Θ2) ⊆ -{a,b}" using c1 union_with_outside by fastforce ultimately show "?rhs ⊆ ?lhs" by auto qed qed qed end