src/HOL/Analysis/Jordan_Curve.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (2 months ago) changeset 69981 3dced198b9ec parent 69922 4a9167f377b0 child 69986 f2d327275065 permissions -rw-r--r--
more strict AFP properties;
```     1 (*  Title:      HOL/Analysis/Jordan_Curve.thy
```
```     2     Authors:    LC Paulson, based on material from HOL Light
```
```     3 *)
```
```     4
```
```     5 section \<open>The Jordan Curve Theorem and Applications\<close>
```
```     6
```
```     7 theory Jordan_Curve
```
```     8   imports Arcwise_Connected Further_Topology
```
```     9 begin
```
```    10
```
```    11 subsection\<open>Janiszewski's theorem\<close>
```
```    12
```
```    13 lemma Janiszewski_weak:
```
```    14   fixes a b::complex
```
```    15   assumes "compact S" "compact T" and conST: "connected(S \<inter> T)"
```
```    16       and ccS: "connected_component (- S) a b" and ccT: "connected_component (- T) a b"
```
```    17     shows "connected_component (- (S \<union> T)) a b"
```
```    18 proof -
```
```    19   have [simp]: "a \<notin> S" "a \<notin> T" "b \<notin> S" "b \<notin> T"
```
```    20     by (meson ComplD ccS ccT connected_component_in)+
```
```    21   have clo: "closedin (top_of_set (S \<union> T)) S" "closedin (top_of_set (S \<union> T)) T"
```
```    22     by (simp_all add: assms closed_subset compact_imp_closed)
```
```    23   obtain g where contg: "continuous_on S g"
```
```    24              and g: "\<And>x. x \<in> S \<Longrightarrow> exp (\<i>* of_real (g x)) = (x - a) /\<^sub>R cmod (x - a) / ((x - b) /\<^sub>R cmod (x - b))"
```
```    25     using ccS \<open>compact S\<close>
```
```    26     apply (simp add: Borsuk_maps_homotopic_in_connected_component_eq [symmetric])
```
```    27     apply (subst (asm) homotopic_circlemaps_divide)
```
```    28     apply (auto simp: inessential_eq_continuous_logarithm_circle)
```
```    29     done
```
```    30   obtain h where conth: "continuous_on T h"
```
```    31              and h: "\<And>x. x \<in> T \<Longrightarrow> exp (\<i>* of_real (h x)) = (x - a) /\<^sub>R cmod (x - a) / ((x - b) /\<^sub>R cmod (x - b))"
```
```    32     using ccT \<open>compact T\<close>
```
```    33     apply (simp add: Borsuk_maps_homotopic_in_connected_component_eq [symmetric])
```
```    34     apply (subst (asm) homotopic_circlemaps_divide)
```
```    35     apply (auto simp: inessential_eq_continuous_logarithm_circle)
```
```    36     done
```
```    37   have "continuous_on (S \<union> T) (\<lambda>x. (x - a) /\<^sub>R cmod (x - a))" "continuous_on (S \<union> T) (\<lambda>x. (x - b) /\<^sub>R cmod (x - b))"
```
```    38     by (intro continuous_intros; force)+
```
```    39   moreover have "(\<lambda>x. (x - a) /\<^sub>R cmod (x - a)) ` (S \<union> T) \<subseteq> sphere 0 1" "(\<lambda>x. (x - b) /\<^sub>R cmod (x - b)) ` (S \<union> T) \<subseteq> sphere 0 1"
```
```    40     by (auto simp: divide_simps)
```
```    41   moreover have "\<exists>g. continuous_on (S \<union> T) g \<and>
```
```    42                      (\<forall>x\<in>S \<union> T. (x - a) /\<^sub>R cmod (x - a) / ((x - b) /\<^sub>R cmod (x - b)) = exp (\<i>*complex_of_real (g x)))"
```
```    43   proof (cases "S \<inter> T = {}")
```
```    44     case True
```
```    45     have "continuous_on (S \<union> T) (\<lambda>x. if x \<in> S then g x else h x)"
```
```    46       apply (rule continuous_on_cases_local [OF clo contg conth])
```
```    47       using True by auto
```
```    48     then show ?thesis
```
```    49       by (rule_tac x="(\<lambda>x. if x \<in> S then g x else h x)" in exI) (auto simp: g h)
```
```    50   next
```
```    51     case False
```
```    52     have diffpi: "\<exists>n. g x = h x + 2* of_int n*pi" if "x \<in> S \<inter> T" for x
```
```    53     proof -
```
```    54       have "exp (\<i>* of_real (g x)) = exp (\<i>* of_real (h x))"
```
```    55         using that by (simp add: g h)
```
```    56       then obtain n where "complex_of_real (g x) = complex_of_real (h x) + 2* of_int n*complex_of_real pi"
```
```    57         apply (auto simp: exp_eq)
```
```    58         by (metis complex_i_not_zero distrib_left mult.commute mult_cancel_left)
```
```    59       then show ?thesis
```
```    60         apply (rule_tac x=n in exI)
```
```    61         using of_real_eq_iff by fastforce
```
```    62     qed
```
```    63     have contgh: "continuous_on (S \<inter> T) (\<lambda>x. g x - h x)"
```
```    64       by (intro continuous_intros continuous_on_subset [OF contg] continuous_on_subset [OF conth]) auto
```
```    65     moreover have disc:
```
```    66           "\<exists>e>0. \<forall>y. y \<in> S \<inter> T \<and> g y - h y \<noteq> g x - h x \<longrightarrow> e \<le> norm ((g y - h y) - (g x - h x))"
```
```    67           if "x \<in> S \<inter> T" for x
```
```    68     proof -
```
```    69       obtain nx where nx: "g x = h x + 2* of_int nx*pi"
```
```    70         using \<open>x \<in> S \<inter> T\<close> diffpi by blast
```
```    71       have "2*pi \<le> norm (g y - h y - (g x - h x))" if y: "y \<in> S \<inter> T" and neq: "g y - h y \<noteq> g x - h x" for y
```
```    72       proof -
```
```    73         obtain ny where ny: "g y = h y + 2* of_int ny*pi"
```
```    74           using \<open>y \<in> S \<inter> T\<close> diffpi by blast
```
```    75         { assume "nx \<noteq> ny"
```
```    76           then have "1 \<le> \<bar>real_of_int ny - real_of_int nx\<bar>"
```
```    77             by linarith
```
```    78           then have "(2*pi)*1 \<le> (2*pi)*\<bar>real_of_int ny - real_of_int nx\<bar>"
```
```    79             by simp
```
```    80           also have "... = \<bar>2*real_of_int ny*pi - 2*real_of_int nx*pi\<bar>"
```
```    81             by (simp add: algebra_simps abs_if)
```
```    82           finally have "2*pi \<le> \<bar>2*real_of_int ny*pi - 2*real_of_int nx*pi\<bar>" by simp
```
```    83         }
```
```    84         with neq show ?thesis
```
```    85           by (simp add: nx ny)
```
```    86       qed
```
```    87       then show ?thesis
```
```    88         by (rule_tac x="2*pi" in exI) auto
```
```    89     qed
```
```    90     ultimately have "(\<lambda>x. g x - h x) constant_on S \<inter> T"
```
```    91       using continuous_discrete_range_constant [OF conST contgh] by blast
```
```    92     then obtain z where z: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = z"
```
```    93       by (auto simp: constant_on_def)
```
```    94     obtain w where "exp(\<i> * of_real(h w)) = exp (\<i> * of_real(z + h w))"
```
```    95       using disc z False
```
```    96       by auto (metis diff_add_cancel g h of_real_add)
```
```    97     then have [simp]: "exp (\<i>* of_real z) = 1"
```
```    98       by (metis cis_conv_exp cis_mult exp_not_eq_zero mult_cancel_right1)
```
```    99     show ?thesis
```
```   100     proof (intro exI conjI)
```
```   101       show "continuous_on (S \<union> T) (\<lambda>x. if x \<in> S then g x else z + h x)"
```
```   102         apply (intro continuous_intros continuous_on_cases_local [OF clo contg] conth)
```
```   103         using z by fastforce
```
```   104     qed (auto simp: g h algebra_simps exp_add)
```
```   105   qed
```
```   106   ultimately have *: "homotopic_with (\<lambda>x. True) (S \<union> T) (sphere 0 1)
```
```   107                           (\<lambda>x. (x - a) /\<^sub>R cmod (x - a))  (\<lambda>x. (x - b) /\<^sub>R cmod (x - b))"
```
```   108     by (subst homotopic_circlemaps_divide) (auto simp: inessential_eq_continuous_logarithm_circle)
```
```   109   show ?thesis
```
```   110     apply (rule Borsuk_maps_homotopic_in_connected_component_eq [THEN iffD1])
```
```   111     using assms by (auto simp: *)
```
```   112 qed
```
```   113
```
```   114
```
```   115 theorem Janiszewski:
```
```   116   fixes a b :: complex
```
```   117   assumes "compact S" "closed T" and conST: "connected (S \<inter> T)"
```
```   118       and ccS: "connected_component (- S) a b" and ccT: "connected_component (- T) a b"
```
```   119     shows "connected_component (- (S \<union> T)) a b"
```
```   120 proof -
```
```   121   have "path_component(- T) a b"
```
```   122     by (simp add: \<open>closed T\<close> ccT open_Compl open_path_connected_component)
```
```   123   then obtain g where g: "path g" "path_image g \<subseteq> - T" "pathstart g = a" "pathfinish g = b"
```
```   124     by (auto simp: path_component_def)
```
```   125   obtain C where C: "compact C" "connected C" "a \<in> C" "b \<in> C" "C \<inter> T = {}"
```
```   126   proof
```
```   127     show "compact (path_image g)"
```
```   128       by (simp add: \<open>path g\<close> compact_path_image)
```
```   129     show "connected (path_image g)"
```
```   130       by (simp add: \<open>path g\<close> connected_path_image)
```
```   131   qed (use g in auto)
```
```   132   obtain r where "0 < r" and r: "C \<union> S \<subseteq> ball 0 r"
```
```   133     by (metis \<open>compact C\<close> \<open>compact S\<close> bounded_Un compact_imp_bounded bounded_subset_ballD)
```
```   134   have "connected_component (- (S \<union> (T \<inter> cball 0 r \<union> sphere 0 r))) a b"
```
```   135   proof (rule Janiszewski_weak [OF \<open>compact S\<close>])
```
```   136     show comT': "compact ((T \<inter> cball 0 r) \<union> sphere 0 r)"
```
```   137       by (simp add: \<open>closed T\<close> closed_Int_compact compact_Un)
```
```   138     have "S \<inter> (T \<inter> cball 0 r \<union> sphere 0 r) = S \<inter> T"
```
```   139       using r by auto
```
```   140     with conST show "connected (S \<inter> (T \<inter> cball 0 r \<union> sphere 0 r))"
```
```   141       by simp
```
```   142     show "connected_component (- (T \<inter> cball 0 r \<union> sphere 0 r)) a b"
```
```   143       using conST C r
```
```   144       apply (simp add: connected_component_def)
```
```   145       apply (rule_tac x=C in exI)
```
```   146       by auto
```
```   147   qed (simp add: ccS)
```
```   148   then obtain U where U: "connected U" "U \<subseteq> - S" "U \<subseteq> - T \<union> - cball 0 r" "U \<subseteq> - sphere 0 r" "a \<in> U" "b \<in> U"
```
```   149     by (auto simp: connected_component_def)
```
```   150   show ?thesis
```
```   151     unfolding connected_component_def
```
```   152   proof (intro exI conjI)
```
```   153     show "U \<subseteq> - (S \<union> T)"
```
```   154       using U r \<open>0 < r\<close> \<open>a \<in> C\<close> connected_Int_frontier [of U "cball 0 r"]
```
```   155       apply simp
```
```   156       by (metis ball_subset_cball compl_inf disjoint_eq_subset_Compl disjoint_iff_not_equal inf.orderE inf_sup_aci(3) subsetCE)
```
```   157   qed (auto simp: U)
```
```   158 qed
```
```   159
```
```   160 lemma Janiszewski_connected:
```
```   161   fixes S :: "complex set"
```
```   162   assumes ST: "compact S" "closed T" "connected(S \<inter> T)"
```
```   163       and notST: "connected (- S)" "connected (- T)"
```
```   164     shows "connected(- (S \<union> T))"
```
```   165 using Janiszewski [OF ST]
```
```   166 by (metis IntD1 IntD2 notST compl_sup connected_iff_connected_component)
```
```   167
```
```   168
```
```   169 subsection\<open>The Jordan Curve theorem\<close>
```
```   170
```
```   171 lemma exists_double_arc:
```
```   172   fixes g :: "real \<Rightarrow> 'a::real_normed_vector"
```
```   173   assumes "simple_path g" "pathfinish g = pathstart g" "a \<in> path_image g" "b \<in> path_image g" "a \<noteq> b"
```
```   174   obtains u d where "arc u" "arc d" "pathstart u = a" "pathfinish u = b"
```
```   175                     "pathstart d = b" "pathfinish d = a"
```
```   176                     "(path_image u) \<inter> (path_image d) = {a,b}"
```
```   177                     "(path_image u) \<union> (path_image d) = path_image g"
```
```   178 proof -
```
```   179   obtain u where u: "0 \<le> u" "u \<le> 1" "g u = a"
```
```   180     using assms by (auto simp: path_image_def)
```
```   181   define h where "h \<equiv> shiftpath u g"
```
```   182   have "simple_path h"
```
```   183     using \<open>simple_path g\<close> simple_path_shiftpath \<open>0 \<le> u\<close> \<open>u \<le> 1\<close> assms(2) h_def by blast
```
```   184   have "pathstart h = g u"
```
```   185     by (simp add: \<open>u \<le> 1\<close> h_def pathstart_shiftpath)
```
```   186   have "pathfinish h = g u"
```
```   187     by (simp add: \<open>0 \<le> u\<close> assms h_def pathfinish_shiftpath)
```
```   188   have pihg: "path_image h = path_image g"
```
```   189     by (simp add: \<open>0 \<le> u\<close> \<open>u \<le> 1\<close> assms h_def path_image_shiftpath)
```
```   190   then obtain v where v: "0 \<le> v" "v \<le> 1" "h v = b"
```
```   191     using assms by (metis (mono_tags, lifting) atLeastAtMost_iff imageE path_image_def)
```
```   192   show ?thesis
```
```   193   proof
```
```   194     show "arc (subpath 0 v h)"
```
```   195       by (metis (no_types) \<open>pathstart h = g u\<close> \<open>simple_path h\<close> arc_simple_path_subpath \<open>a \<noteq> b\<close> atLeastAtMost_iff zero_le_one order_refl pathstart_def u(3) v)
```
```   196     show "arc (subpath v 1 h)"
```
```   197       by (metis (no_types) \<open>pathfinish h = g u\<close> \<open>simple_path h\<close> arc_simple_path_subpath \<open>a \<noteq> b\<close> atLeastAtMost_iff zero_le_one order_refl pathfinish_def u(3) v)
```
```   198     show "pathstart (subpath 0 v h) = a"
```
```   199       by (metis \<open>pathstart h = g u\<close> pathstart_def pathstart_subpath u(3))
```
```   200     show "pathfinish (subpath 0 v h) = b"  "pathstart (subpath v 1 h) = b"
```
```   201       by (simp_all add: v(3))
```
```   202     show "pathfinish (subpath v 1 h) = a"
```
```   203       by (metis \<open>pathfinish h = g u\<close> pathfinish_def pathfinish_subpath u(3))
```
```   204     show "path_image (subpath 0 v h) \<inter> path_image (subpath v 1 h) = {a, b}"
```
```   205     proof
```
```   206       show "path_image (subpath 0 v h) \<inter> path_image (subpath v 1 h) \<subseteq> {a, b}"
```
```   207         using v  \<open>pathfinish (subpath v 1 h) = a\<close> \<open>simple_path h\<close>
```
```   208           apply (auto simp: simple_path_def path_image_subpath image_iff Ball_def)
```
```   209         by (metis (full_types) less_eq_real_def less_irrefl less_le_trans)
```
```   210       show "{a, b} \<subseteq> path_image (subpath 0 v h) \<inter> path_image (subpath v 1 h)"
```
```   211         using v \<open>pathstart (subpath 0 v h) = a\<close> \<open>pathfinish (subpath v 1 h) = a\<close>
```
```   212         apply (auto simp: path_image_subpath image_iff)
```
```   213         by (metis atLeastAtMost_iff order_refl)
```
```   214     qed
```
```   215     show "path_image (subpath 0 v h) \<union> path_image (subpath v 1 h) = path_image g"
```
```   216       using v apply (simp add: path_image_subpath pihg [symmetric])
```
```   217       using path_image_def by fastforce
```
```   218   qed
```
```   219 qed
```
```   220
```
```   221
```
```   222 theorem%unimportant Jordan_curve:
```
```   223   fixes c :: "real \<Rightarrow> complex"
```
```   224   assumes "simple_path c" and loop: "pathfinish c = pathstart c"
```
```   225   obtains inner outer where
```
```   226                 "inner \<noteq> {}" "open inner" "connected inner"
```
```   227                 "outer \<noteq> {}" "open outer" "connected outer"
```
```   228                 "bounded inner" "\<not> bounded outer" "inner \<inter> outer = {}"
```
```   229                 "inner \<union> outer = - path_image c"
```
```   230                 "frontier inner = path_image c"
```
```   231                 "frontier outer = path_image c"
```
```   232 proof -
```
```   233   have "path c"
```
```   234     by (simp add: assms simple_path_imp_path)
```
```   235   have hom: "(path_image c) homeomorphic (sphere(0::complex) 1)"
```
```   236     by (simp add: assms homeomorphic_simple_path_image_circle)
```
```   237   with Jordan_Brouwer_separation have "\<not> connected (- (path_image c))"
```
```   238     by fastforce
```
```   239   then obtain inner where inner: "inner \<in> components (- path_image c)" and "bounded inner"
```
```   240     using cobounded_has_bounded_component [of "- (path_image c)"]
```
```   241     using \<open>\<not> connected (- path_image c)\<close> \<open>simple_path c\<close> bounded_simple_path_image by force
```
```   242   obtain outer where outer: "outer \<in> components (- path_image c)" and "\<not> bounded outer"
```
```   243     using cobounded_unbounded_components [of "- (path_image c)"]
```
```   244     using \<open>path c\<close> bounded_path_image by auto
```
```   245   show ?thesis
```
```   246   proof
```
```   247     show "inner \<noteq> {}"
```
```   248       using inner in_components_nonempty by auto
```
```   249     show "open inner"
```
```   250       by (meson \<open>simple_path c\<close> compact_imp_closed compact_simple_path_image inner open_Compl open_components)
```
```   251     show "connected inner"
```
```   252       using in_components_connected inner by blast
```
```   253     show "outer \<noteq> {}"
```
```   254       using outer in_components_nonempty by auto
```
```   255     show "open outer"
```
```   256       by (meson \<open>simple_path c\<close> compact_imp_closed compact_simple_path_image outer open_Compl open_components)
```
```   257     show "connected outer"
```
```   258       using in_components_connected outer by blast
```
```   259     show "inner \<inter> outer = {}"
```
```   260       by (meson \<open>\<not> bounded outer\<close> \<open>bounded inner\<close> \<open>connected outer\<close> bounded_subset components_maximal in_components_subset inner outer)
```
```   261     show fro_inner: "frontier inner = path_image c"
```
```   262       by (simp add: Jordan_Brouwer_frontier [OF hom inner])
```
```   263     show fro_outer: "frontier outer = path_image c"
```
```   264       by (simp add: Jordan_Brouwer_frontier [OF hom outer])
```
```   265     have False if m: "middle \<in> components (- path_image c)" and "middle \<noteq> inner" "middle \<noteq> outer" for middle
```
```   266     proof -
```
```   267       have "frontier middle = path_image c"
```
```   268         by (simp add: Jordan_Brouwer_frontier [OF hom] that)
```
```   269       have middle: "open middle" "connected middle" "middle \<noteq> {}"
```
```   270         apply (meson \<open>simple_path c\<close> compact_imp_closed compact_simple_path_image m open_Compl open_components)
```
```   271         using in_components_connected in_components_nonempty m by blast+
```
```   272       obtain a0 b0 where "a0 \<in> path_image c" "b0 \<in> path_image c" "a0 \<noteq> b0"
```
```   273         using simple_path_image_uncountable [OF \<open>simple_path c\<close>]
```
```   274         by (metis Diff_cancel countable_Diff_eq countable_empty insert_iff subsetI subset_singleton_iff)
```
```   275       obtain a b g where ab: "a \<in> path_image c" "b \<in> path_image c" "a \<noteq> b"
```
```   276                      and "arc g" "pathstart g = a" "pathfinish g = b"
```
```   277                      and pag_sub: "path_image g - {a,b} \<subseteq> middle"
```
```   278       proof (rule dense_accessible_frontier_point_pairs [OF \<open>open middle\<close> \<open>connected middle\<close>, of "path_image c \<inter> ball a0 (dist a0 b0)" "path_image c \<inter> ball b0 (dist a0 b0)"])
```
```   279         show "openin (top_of_set (frontier middle)) (path_image c \<inter> ball a0 (dist a0 b0))"
```
```   280              "openin (top_of_set (frontier middle)) (path_image c \<inter> ball b0 (dist a0 b0))"
```
```   281           by (simp_all add: \<open>frontier middle = path_image c\<close> openin_open_Int)
```
```   282         show "path_image c \<inter> ball a0 (dist a0 b0) \<noteq> path_image c \<inter> ball b0 (dist a0 b0)"
```
```   283           using \<open>a0 \<noteq> b0\<close> \<open>b0 \<in> path_image c\<close> by auto
```
```   284         show "path_image c \<inter> ball a0 (dist a0 b0) \<noteq> {}"
```
```   285           using \<open>a0 \<in> path_image c\<close> \<open>a0 \<noteq> b0\<close> by auto
```
```   286         show "path_image c \<inter> ball b0 (dist a0 b0) \<noteq> {}"
```
```   287           using \<open>b0 \<in> path_image c\<close> \<open>a0 \<noteq> b0\<close> by auto
```
```   288       qed (use arc_distinct_ends arc_imp_simple_path simple_path_endless that in fastforce)
```
```   289       obtain u d where "arc u" "arc d"
```
```   290                    and "pathstart u = a" "pathfinish u = b" "pathstart d = b" "pathfinish d = a"
```
```   291                    and ud_ab: "(path_image u) \<inter> (path_image d) = {a,b}"
```
```   292                    and ud_Un: "(path_image u) \<union> (path_image d) = path_image c"
```
```   293         using exists_double_arc [OF assms ab] by blast
```
```   294       obtain x y where "x \<in> inner" "y \<in> outer"
```
```   295         using \<open>inner \<noteq> {}\<close> \<open>outer \<noteq> {}\<close> by auto
```
```   296       have "inner \<inter> middle = {}" "middle \<inter> outer = {}"
```
```   297         using components_nonoverlap inner outer m that by blast+
```
```   298       have "connected_component (- (path_image u \<union> path_image g \<union> (path_image d \<union> path_image g))) x y"
```
```   299       proof (rule Janiszewski)
```
```   300         show "compact (path_image u \<union> path_image g)"
```
```   301           by (simp add: \<open>arc g\<close> \<open>arc u\<close> compact_Un compact_arc_image)
```
```   302         show "closed (path_image d \<union> path_image g)"
```
```   303           by (simp add: \<open>arc d\<close> \<open>arc g\<close> closed_Un closed_arc_image)
```
```   304         show "connected ((path_image u \<union> path_image g) \<inter> (path_image d \<union> path_image g))"
```
```   305           by (metis Un_Diff_cancel \<open>arc g\<close> \<open>path_image u \<inter> path_image d = {a, b}\<close> \<open>pathfinish g = b\<close> \<open>pathstart g = a\<close> connected_arc_image insert_Diff1 pathfinish_in_path_image pathstart_in_path_image sup_bot.right_neutral sup_commute sup_inf_distrib1)
```
```   306         show "connected_component (- (path_image u \<union> path_image g)) x y"
```
```   307           unfolding connected_component_def
```
```   308         proof (intro exI conjI)
```
```   309           have "connected ((inner \<union> (path_image c - path_image u)) \<union> (outer \<union> (path_image c - path_image u)))"
```
```   310           proof (rule connected_Un)
```
```   311             show "connected (inner \<union> (path_image c - path_image u))"
```
```   312               apply (rule connected_intermediate_closure [OF \<open>connected inner\<close>])
```
```   313               using fro_inner [symmetric]  apply (auto simp: closure_subset frontier_def)
```
```   314               done
```
```   315             show "connected (outer \<union> (path_image c - path_image u))"
```
```   316               apply (rule connected_intermediate_closure [OF \<open>connected outer\<close>])
```
```   317               using fro_outer [symmetric]  apply (auto simp: closure_subset frontier_def)
```
```   318               done
```
```   319             have "(inner \<inter> outer) \<union> (path_image c - path_image u) \<noteq> {}"
```
```   320               by (metis \<open>arc d\<close>  ud_ab Diff_Int Diff_cancel Un_Diff \<open>inner \<inter> outer = {}\<close> \<open>pathfinish d = a\<close> \<open>pathstart d = b\<close> arc_simple_path insert_commute nonempty_simple_path_endless sup_bot_left ud_Un)
```
```   321             then show "(inner \<union> (path_image c - path_image u)) \<inter> (outer \<union> (path_image c - path_image u)) \<noteq> {}"
```
```   322               by auto
```
```   323           qed
```
```   324           then show "connected (inner \<union> outer \<union> (path_image c - path_image u))"
```
```   325             by (metis sup.right_idem sup_assoc sup_commute)
```
```   326           have "inner \<subseteq> - path_image u" "outer \<subseteq> - path_image u"
```
```   327             using in_components_subset inner outer ud_Un by auto
```
```   328           moreover have "inner \<subseteq> - path_image g" "outer \<subseteq> - path_image g"
```
```   329             using \<open>inner \<inter> middle = {}\<close> \<open>inner \<subseteq> - path_image u\<close>
```
```   330             using \<open>middle \<inter> outer = {}\<close> \<open>outer \<subseteq> - path_image u\<close> pag_sub ud_ab by fastforce+
```
```   331           moreover have "path_image c - path_image u \<subseteq> - path_image g"
```
```   332             using in_components_subset m pag_sub ud_ab by fastforce
```
```   333           ultimately show "inner \<union> outer \<union> (path_image c - path_image u) \<subseteq> - (path_image u \<union> path_image g)"
```
```   334             by force
```
```   335           show "x \<in> inner \<union> outer \<union> (path_image c - path_image u)"
```
```   336             by (auto simp: \<open>x \<in> inner\<close>)
```
```   337           show "y \<in> inner \<union> outer \<union> (path_image c - path_image u)"
```
```   338             by (auto simp: \<open>y \<in> outer\<close>)
```
```   339         qed
```
```   340         show "connected_component (- (path_image d \<union> path_image g)) x y"
```
```   341           unfolding connected_component_def
```
```   342         proof (intro exI conjI)
```
```   343           have "connected ((inner \<union> (path_image c - path_image d)) \<union> (outer \<union> (path_image c - path_image d)))"
```
```   344           proof (rule connected_Un)
```
```   345             show "connected (inner \<union> (path_image c - path_image d))"
```
```   346               apply (rule connected_intermediate_closure [OF \<open>connected inner\<close>])
```
```   347               using fro_inner [symmetric]  apply (auto simp: closure_subset frontier_def)
```
```   348               done
```
```   349             show "connected (outer \<union> (path_image c - path_image d))"
```
```   350               apply (rule connected_intermediate_closure [OF \<open>connected outer\<close>])
```
```   351               using fro_outer [symmetric]  apply (auto simp: closure_subset frontier_def)
```
```   352               done
```
```   353             have "(inner \<inter> outer) \<union> (path_image c - path_image d) \<noteq> {}"
```
```   354               using \<open>arc u\<close> \<open>pathfinish u = b\<close> \<open>pathstart u = a\<close> arc_imp_simple_path nonempty_simple_path_endless ud_Un ud_ab by fastforce
```
```   355             then show "(inner \<union> (path_image c - path_image d)) \<inter> (outer \<union> (path_image c - path_image d)) \<noteq> {}"
```
```   356               by auto
```
```   357           qed
```
```   358           then show "connected (inner \<union> outer \<union> (path_image c - path_image d))"
```
```   359             by (metis sup.right_idem sup_assoc sup_commute)
```
```   360           have "inner \<subseteq> - path_image d" "outer \<subseteq> - path_image d"
```
```   361             using in_components_subset inner outer ud_Un by auto
```
```   362           moreover have "inner \<subseteq> - path_image g" "outer \<subseteq> - path_image g"
```
```   363             using \<open>inner \<inter> middle = {}\<close> \<open>inner \<subseteq> - path_image d\<close>
```
```   364             using \<open>middle \<inter> outer = {}\<close> \<open>outer \<subseteq> - path_image d\<close> pag_sub ud_ab by fastforce+
```
```   365           moreover have "path_image c - path_image d \<subseteq> - path_image g"
```
```   366             using in_components_subset m pag_sub ud_ab by fastforce
```
```   367           ultimately show "inner \<union> outer \<union> (path_image c - path_image d) \<subseteq> - (path_image d \<union> path_image g)"
```
```   368             by force
```
```   369           show "x \<in> inner \<union> outer \<union> (path_image c - path_image d)"
```
```   370             by (auto simp: \<open>x \<in> inner\<close>)
```
```   371           show "y \<in> inner \<union> outer \<union> (path_image c - path_image d)"
```
```   372             by (auto simp: \<open>y \<in> outer\<close>)
```
```   373         qed
```
```   374       qed
```
```   375       then have "connected_component (- (path_image u \<union> path_image d \<union> path_image g)) x y"
```
```   376         by (simp add: Un_ac)
```
```   377       moreover have "\<not>(connected_component (- (path_image c)) x y)"
```
```   378         by (metis (no_types, lifting) \<open>\<not> bounded outer\<close> \<open>bounded inner\<close> \<open>x \<in> inner\<close> \<open>y \<in> outer\<close> componentsE connected_component_eq inner mem_Collect_eq outer)
```
```   379       ultimately show False
```
```   380         by (auto simp: ud_Un [symmetric] connected_component_def)
```
```   381     qed
```
```   382     then have "components (- path_image c) = {inner,outer}"
```
```   383       using inner outer by blast
```
```   384     then have "Union (components (- path_image c)) = inner \<union> outer"
```
```   385       by simp
```
```   386     then show "inner \<union> outer = - path_image c"
```
```   387       by auto
```
```   388   qed (auto simp: \<open>bounded inner\<close> \<open>\<not> bounded outer\<close>)
```
```   389 qed
```
```   390
```
```   391
```
```   392 corollary%unimportant Jordan_disconnected:
```
```   393   fixes c :: "real \<Rightarrow> complex"
```
```   394   assumes "simple_path c" "pathfinish c = pathstart c"
```
```   395     shows "\<not> connected(- path_image c)"
```
```   396 using Jordan_curve [OF assms]
```
```   397   by (metis Jordan_Brouwer_separation assms homeomorphic_simple_path_image_circle zero_less_one)
```
```   398
```
```   399
```
```   400 corollary Jordan_inside_outside:
```
```   401   fixes c :: "real \<Rightarrow> complex"
```
```   402   assumes "simple_path c" "pathfinish c = pathstart c"
```
```   403     shows "inside(path_image c) \<noteq> {} \<and>
```
```   404           open(inside(path_image c)) \<and>
```
```   405           connected(inside(path_image c)) \<and>
```
```   406           outside(path_image c) \<noteq> {} \<and>
```
```   407           open(outside(path_image c)) \<and>
```
```   408           connected(outside(path_image c)) \<and>
```
```   409           bounded(inside(path_image c)) \<and>
```
```   410           \<not> bounded(outside(path_image c)) \<and>
```
```   411           inside(path_image c) \<inter> outside(path_image c) = {} \<and>
```
```   412           inside(path_image c) \<union> outside(path_image c) =
```
```   413           - path_image c \<and>
```
```   414           frontier(inside(path_image c)) = path_image c \<and>
```
```   415           frontier(outside(path_image c)) = path_image c"
```
```   416 proof -
```
```   417   obtain inner outer
```
```   418     where *: "inner \<noteq> {}" "open inner" "connected inner"
```
```   419              "outer \<noteq> {}" "open outer" "connected outer"
```
```   420              "bounded inner" "\<not> bounded outer" "inner \<inter> outer = {}"
```
```   421              "inner \<union> outer = - path_image c"
```
```   422              "frontier inner = path_image c"
```
```   423              "frontier outer = path_image c"
```
```   424     using Jordan_curve [OF assms] by blast
```
```   425   then have inner: "inside(path_image c) = inner"
```
```   426     by (metis dual_order.antisym inside_subset interior_eq interior_inside_frontier)
```
```   427   have outer: "outside(path_image c) = outer"
```
```   428     using \<open>inner \<union> outer = - path_image c\<close> \<open>inside (path_image c) = inner\<close>
```
```   429           outside_inside \<open>inner \<inter> outer = {}\<close> by auto
```
```   430   show ?thesis
```
```   431     using * by (auto simp: inner outer)
```
```   432 qed
```
```   433
```
```   434 subsubsection\<open>Triple-curve or "theta-curve" theorem\<close>
```
```   435
```
```   436 text\<open>Proof that there is no fourth component taken from
```
```   437      Kuratowski's Topology vol 2, para 61, II.\<close>
```
```   438
```
```   439 theorem split_inside_simple_closed_curve:
```
```   440   fixes c :: "real \<Rightarrow> complex"
```
```   441   assumes "simple_path c1" and c1: "pathstart c1 = a" "pathfinish c1 = b"
```
```   442       and "simple_path c2" and c2: "pathstart c2 = a" "pathfinish c2 = b"
```
```   443       and "simple_path c"  and c: "pathstart c = a" "pathfinish c = b"
```
```   444       and "a \<noteq> b"
```
```   445       and c1c2: "path_image c1 \<inter> path_image c2 = {a,b}"
```
```   446       and c1c: "path_image c1 \<inter> path_image c = {a,b}"
```
```   447       and c2c: "path_image c2 \<inter> path_image c = {a,b}"
```
```   448       and ne_12: "path_image c \<inter> inside(path_image c1 \<union> path_image c2) \<noteq> {}"
```
```   449   obtains "inside(path_image c1 \<union> path_image c) \<inter> inside(path_image c2 \<union> path_image c) = {}"
```
```   450           "inside(path_image c1 \<union> path_image c) \<union> inside(path_image c2 \<union> path_image c) \<union>
```
```   451            (path_image c - {a,b}) = inside(path_image c1 \<union> path_image c2)"
```
```   452 proof -
```
```   453   let ?\<Theta> = "path_image c"  let ?\<Theta>1 = "path_image c1"  let ?\<Theta>2 = "path_image c2"
```
```   454   have sp: "simple_path (c1 +++ reversepath c2)" "simple_path (c1 +++ reversepath c)" "simple_path (c2 +++ reversepath c)"
```
```   455     using assms by (auto simp: simple_path_join_loop_eq arc_simple_path simple_path_reversepath)
```
```   456   then have op_in12: "open (inside (?\<Theta>1 \<union> ?\<Theta>2))"
```
```   457      and op_out12: "open (outside (?\<Theta>1 \<union> ?\<Theta>2))"
```
```   458      and op_in1c: "open (inside (?\<Theta>1 \<union> ?\<Theta>))"
```
```   459      and op_in2c: "open (inside (?\<Theta>2 \<union> ?\<Theta>))"
```
```   460      and op_out1c: "open (outside (?\<Theta>1 \<union> ?\<Theta>))"
```
```   461      and op_out2c: "open (outside (?\<Theta>2 \<union> ?\<Theta>))"
```
```   462      and co_in1c: "connected (inside (?\<Theta>1 \<union> ?\<Theta>))"
```
```   463      and co_in2c: "connected (inside (?\<Theta>2 \<union> ?\<Theta>))"
```
```   464      and co_out12c: "connected (outside (?\<Theta>1 \<union> ?\<Theta>2))"
```
```   465      and co_out1c: "connected (outside (?\<Theta>1 \<union> ?\<Theta>))"
```
```   466      and co_out2c: "connected (outside (?\<Theta>2 \<union> ?\<Theta>))"
```
```   467      and pa_c: "?\<Theta> - {pathstart c, pathfinish c} \<subseteq> - ?\<Theta>1"
```
```   468                "?\<Theta> - {pathstart c, pathfinish c} \<subseteq> - ?\<Theta>2"
```
```   469      and pa_c1: "?\<Theta>1 - {pathstart c1, pathfinish c1} \<subseteq> - ?\<Theta>2"
```
```   470                 "?\<Theta>1 - {pathstart c1, pathfinish c1} \<subseteq> - ?\<Theta>"
```
```   471      and pa_c2: "?\<Theta>2 - {pathstart c2, pathfinish c2} \<subseteq> - ?\<Theta>1"
```
```   472                 "?\<Theta>2 - {pathstart c2, pathfinish c2} \<subseteq> - ?\<Theta>"
```
```   473      and co_c: "connected(?\<Theta> - {pathstart c,pathfinish c})"
```
```   474      and co_c1: "connected(?\<Theta>1 - {pathstart c1,pathfinish c1})"
```
```   475      and co_c2: "connected(?\<Theta>2 - {pathstart c2,pathfinish c2})"
```
```   476      and fr_in: "frontier(inside(?\<Theta>1 \<union> ?\<Theta>2)) = ?\<Theta>1 \<union> ?\<Theta>2"
```
```   477               "frontier(inside(?\<Theta>2 \<union> ?\<Theta>)) = ?\<Theta>2 \<union> ?\<Theta>"
```
```   478               "frontier(inside(?\<Theta>1 \<union> ?\<Theta>)) = ?\<Theta>1 \<union> ?\<Theta>"
```
```   479      and fr_out: "frontier(outside(?\<Theta>1 \<union> ?\<Theta>2)) = ?\<Theta>1 \<union> ?\<Theta>2"
```
```   480               "frontier(outside(?\<Theta>2 \<union> ?\<Theta>)) = ?\<Theta>2 \<union> ?\<Theta>"
```
```   481               "frontier(outside(?\<Theta>1 \<union> ?\<Theta>)) = ?\<Theta>1 \<union> ?\<Theta>"
```
```   482     using Jordan_inside_outside [of "c1 +++ reversepath c2"]
```
```   483     using Jordan_inside_outside [of "c1 +++ reversepath c"]
```
```   484     using Jordan_inside_outside [of "c2 +++ reversepath c"] assms
```
```   485               apply (simp_all add: path_image_join closed_Un closed_simple_path_image open_inside open_outside)
```
```   486       apply (blast elim: | metis connected_simple_path_endless)+
```
```   487     done
```
```   488   have inout_12: "inside (?\<Theta>1 \<union> ?\<Theta>2) \<inter> (?\<Theta> - {pathstart c, pathfinish c}) \<noteq> {}"
```
```   489     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)
```
```   490   have pi_disjoint:  "?\<Theta> \<inter> outside(?\<Theta>1 \<union> ?\<Theta>2) = {}"
```
```   491   proof (rule ccontr)
```
```   492     assume "?\<Theta> \<inter> outside (?\<Theta>1 \<union> ?\<Theta>2) \<noteq> {}"
```
```   493     then show False
```
```   494       using connectedD [OF co_c, of "inside(?\<Theta>1 \<union> ?\<Theta>2)" "outside(?\<Theta>1 \<union> ?\<Theta>2)"]
```
```   495       using c c1c2 pa_c op_in12 op_out12 inout_12
```
```   496       apply auto
```
```   497       apply (metis Un_Diff_cancel2 Un_iff compl_sup disjoint_insert(1) inf_commute inf_compl_bot_left2 inside_Un_outside mk_disjoint_insert sup_inf_absorb)
```
```   498       done
```
```   499   qed
```
```   500   have out_sub12: "outside(?\<Theta>1 \<union> ?\<Theta>2) \<subseteq> outside(?\<Theta>1 \<union> ?\<Theta>)" "outside(?\<Theta>1 \<union> ?\<Theta>2) \<subseteq> outside(?\<Theta>2 \<union> ?\<Theta>)"
```
```   501     by (metis Un_commute pi_disjoint outside_Un_outside_Un)+
```
```   502   have pa1_disj_in2: "?\<Theta>1 \<inter> inside (?\<Theta>2 \<union> ?\<Theta>) = {}"
```
```   503   proof (rule ccontr)
```
```   504     assume ne: "?\<Theta>1 \<inter> inside (?\<Theta>2 \<union> ?\<Theta>) \<noteq> {}"
```
```   505     have 1: "inside (?\<Theta> \<union> ?\<Theta>2) \<inter> ?\<Theta> = {}"
```
```   506       by (metis (no_types) Diff_Int_distrib Diff_cancel inf_sup_absorb inf_sup_aci(3) inside_no_overlap)
```
```   507     have 2: "outside (?\<Theta> \<union> ?\<Theta>2) \<inter> ?\<Theta> = {}"
```
```   508       by (metis (no_types) Int_empty_right Int_left_commute inf_sup_absorb outside_no_overlap)
```
```   509     have "outside (?\<Theta>2 \<union> ?\<Theta>) \<subseteq> outside (?\<Theta>1 \<union> ?\<Theta>2)"
```
```   510       apply (subst Un_commute, rule outside_Un_outside_Un)
```
```   511       using connectedD [OF co_c1, of "inside(?\<Theta>2 \<union> ?\<Theta>)" "outside(?\<Theta>2 \<union> ?\<Theta>)"]
```
```   512         pa_c1 op_in2c op_out2c ne c1 c2c 1 2 by (auto simp: inf_sup_aci)
```
```   513     with out_sub12
```
```   514     have "outside(?\<Theta>1 \<union> ?\<Theta>2) = outside(?\<Theta>2 \<union> ?\<Theta>)" by blast
```
```   515     then have "frontier(outside(?\<Theta>1 \<union> ?\<Theta>2)) = frontier(outside(?\<Theta>2 \<union> ?\<Theta>))"
```
```   516       by simp
```
```   517     then show False
```
```   518       using inout_12 pi_disjoint c c1c c2c fr_out by auto
```
```   519   qed
```
```   520   have pa2_disj_in1: "?\<Theta>2 \<inter> inside(?\<Theta>1 \<union> ?\<Theta>) = {}"
```
```   521   proof (rule ccontr)
```
```   522     assume ne: "?\<Theta>2 \<inter> inside (?\<Theta>1 \<union> ?\<Theta>) \<noteq> {}"
```
```   523     have 1: "inside (?\<Theta> \<union> ?\<Theta>1) \<inter> ?\<Theta> = {}"
```
```   524       by (metis (no_types) Diff_Int_distrib Diff_cancel inf_sup_absorb inf_sup_aci(3) inside_no_overlap)
```
```   525     have 2: "outside (?\<Theta> \<union> ?\<Theta>1) \<inter> ?\<Theta> = {}"
```
```   526       by (metis (no_types) Int_empty_right Int_left_commute inf_sup_absorb outside_no_overlap)
```
```   527     have "outside (?\<Theta>1 \<union> ?\<Theta>) \<subseteq> outside (?\<Theta>1 \<union> ?\<Theta>2)"
```
```   528       apply (rule outside_Un_outside_Un)
```
```   529       using connectedD [OF co_c2, of "inside(?\<Theta>1 \<union> ?\<Theta>)" "outside(?\<Theta>1 \<union> ?\<Theta>)"]
```
```   530         pa_c2 op_in1c op_out1c ne c2 c1c 1 2 by (auto simp: inf_sup_aci)
```
```   531     with out_sub12
```
```   532     have "outside(?\<Theta>1 \<union> ?\<Theta>2) = outside(?\<Theta>1 \<union> ?\<Theta>)"
```
```   533       by blast
```
```   534     then have "frontier(outside(?\<Theta>1 \<union> ?\<Theta>2)) = frontier(outside(?\<Theta>1 \<union> ?\<Theta>))"
```
```   535       by simp
```
```   536     then show False
```
```   537       using inout_12 pi_disjoint c c1c c2c fr_out by auto
```
```   538   qed
```
```   539   have in_sub_in1: "inside(?\<Theta>1 \<union> ?\<Theta>) \<subseteq> inside(?\<Theta>1 \<union> ?\<Theta>2)"
```
```   540     using pa2_disj_in1 out_sub12 by (auto simp: inside_outside)
```
```   541   have in_sub_in2: "inside(?\<Theta>2 \<union> ?\<Theta>) \<subseteq> inside(?\<Theta>1 \<union> ?\<Theta>2)"
```
```   542     using pa1_disj_in2 out_sub12 by (auto simp: inside_outside)
```
```   543   have in_sub_out12: "inside(?\<Theta>1 \<union> ?\<Theta>) \<subseteq> outside(?\<Theta>2 \<union> ?\<Theta>)"
```
```   544   proof
```
```   545     fix x
```
```   546     assume x: "x \<in> inside (?\<Theta>1 \<union> ?\<Theta>)"
```
```   547     then have xnot: "x \<notin> ?\<Theta>"
```
```   548       by (simp add: inside_def)
```
```   549     obtain z where zim: "z \<in> ?\<Theta>1" and zout: "z \<in> outside(?\<Theta>2 \<union> ?\<Theta>)"
```
```   550       apply (auto simp: outside_inside)
```
```   551       using nonempty_simple_path_endless [OF \<open>simple_path c1\<close>]
```
```   552       by (metis Diff_Diff_Int Diff_iff ex_in_conv c1 c1c c1c2 pa1_disj_in2)
```
```   553     obtain e where "e > 0" and e: "ball z e \<subseteq> outside(?\<Theta>2 \<union> ?\<Theta>)"
```
```   554       using zout op_out2c open_contains_ball_eq by blast
```
```   555     have "z \<in> frontier (inside (?\<Theta>1 \<union> ?\<Theta>))"
```
```   556       using zim by (auto simp: fr_in)
```
```   557     then obtain w where w1: "w \<in> inside (?\<Theta>1 \<union> ?\<Theta>)" and dwz: "dist w z < e"
```
```   558       using zim \<open>e > 0\<close> by (auto simp: frontier_def closure_approachable)
```
```   559     then have w2: "w \<in> outside (?\<Theta>2 \<union> ?\<Theta>)"
```
```   560       by (metis e dist_commute mem_ball subsetCE)
```
```   561     then have "connected_component (- ?\<Theta>2 \<inter> - ?\<Theta>) z w"
```
```   562       apply (simp add: connected_component_def)
```
```   563       apply (rule_tac x = "outside(?\<Theta>2 \<union> ?\<Theta>)" in exI)
```
```   564       using zout apply (auto simp: co_out2c)
```
```   565        apply (simp_all add: outside_inside)
```
```   566       done
```
```   567     moreover have "connected_component (- ?\<Theta>2 \<inter> - ?\<Theta>) w x"
```
```   568       unfolding connected_component_def
```
```   569       using pa2_disj_in1 co_in1c x w1 union_with_outside by fastforce
```
```   570     ultimately have eq: "connected_component_set (- ?\<Theta>2 \<inter> - ?\<Theta>) x =
```
```   571                          connected_component_set (- ?\<Theta>2 \<inter> - ?\<Theta>) z"
```
```   572       by (metis (mono_tags, lifting) connected_component_eq mem_Collect_eq)
```
```   573     show "x \<in> outside (?\<Theta>2 \<union> ?\<Theta>)"
```
```   574       using zout x pa2_disj_in1 by (auto simp: outside_def eq xnot)
```
```   575   qed
```
```   576   have in_sub_out21: "inside(?\<Theta>2 \<union> ?\<Theta>) \<subseteq> outside(?\<Theta>1 \<union> ?\<Theta>)"
```
```   577   proof
```
```   578     fix x
```
```   579     assume x: "x \<in> inside (?\<Theta>2 \<union> ?\<Theta>)"
```
```   580     then have xnot: "x \<notin> ?\<Theta>"
```
```   581       by (simp add: inside_def)
```
```   582     obtain z where zim: "z \<in> ?\<Theta>2" and zout: "z \<in> outside(?\<Theta>1 \<union> ?\<Theta>)"
```
```   583       apply (auto simp: outside_inside)
```
```   584       using nonempty_simple_path_endless [OF \<open>simple_path c2\<close>]
```
```   585       by (metis (no_types, hide_lams) Diff_Diff_Int Diff_iff c1c2 c2 c2c ex_in_conv pa2_disj_in1)
```
```   586     obtain e where "e > 0" and e: "ball z e \<subseteq> outside(?\<Theta>1 \<union> ?\<Theta>)"
```
```   587       using zout op_out1c open_contains_ball_eq by blast
```
```   588     have "z \<in> frontier (inside (?\<Theta>2 \<union> ?\<Theta>))"
```
```   589       using zim by (auto simp: fr_in)
```
```   590     then obtain w where w2: "w \<in> inside (?\<Theta>2 \<union> ?\<Theta>)" and dwz: "dist w z < e"
```
```   591       using zim \<open>e > 0\<close> by (auto simp: frontier_def closure_approachable)
```
```   592     then have w1: "w \<in> outside (?\<Theta>1 \<union> ?\<Theta>)"
```
```   593       by (metis e dist_commute mem_ball subsetCE)
```
```   594     then have "connected_component (- ?\<Theta>1 \<inter> - ?\<Theta>) z w"
```
```   595       apply (simp add: connected_component_def)
```
```   596       apply (rule_tac x = "outside(?\<Theta>1 \<union> ?\<Theta>)" in exI)
```
```   597       using zout apply (auto simp: co_out1c)
```
```   598        apply (simp_all add: outside_inside)
```
```   599       done
```
```   600     moreover have "connected_component (- ?\<Theta>1 \<inter> - ?\<Theta>) w x"
```
```   601       unfolding connected_component_def
```
```   602       using pa1_disj_in2 co_in2c x w2 union_with_outside by fastforce
```
```   603     ultimately have eq: "connected_component_set (- ?\<Theta>1 \<inter> - ?\<Theta>) x =
```
```   604                            connected_component_set (- ?\<Theta>1 \<inter> - ?\<Theta>) z"
```
```   605       by (metis (no_types, lifting) connected_component_eq mem_Collect_eq)
```
```   606     show "x \<in> outside (?\<Theta>1 \<union> ?\<Theta>)"
```
```   607       using zout x pa1_disj_in2 by (auto simp: outside_def eq xnot)
```
```   608   qed
```
```   609   show ?thesis
```
```   610   proof
```
```   611     show "inside (?\<Theta>1 \<union> ?\<Theta>) \<inter> inside (?\<Theta>2 \<union> ?\<Theta>) = {}"
```
```   612       by (metis Int_Un_distrib in_sub_out12 bot_eq_sup_iff disjoint_eq_subset_Compl outside_inside)
```
```   613     have *: "outside (?\<Theta>1 \<union> ?\<Theta>) \<inter> outside (?\<Theta>2 \<union> ?\<Theta>) \<subseteq> outside (?\<Theta>1 \<union> ?\<Theta>2)"
```
```   614     proof (rule components_maximal)
```
```   615       show out_in: "outside (?\<Theta>1 \<union> ?\<Theta>2) \<in> components (- (?\<Theta>1 \<union> ?\<Theta>2))"
```
```   616         apply (simp only: outside_in_components co_out12c)
```
```   617         by (metis bounded_empty fr_out(1) frontier_empty unbounded_outside)
```
```   618       have conn_U: "connected (- (closure (inside (?\<Theta>1 \<union> ?\<Theta>)) \<union> closure (inside (?\<Theta>2 \<union> ?\<Theta>))))"
```
```   619       proof (rule Janiszewski_connected, simp_all)
```
```   620         show "bounded (inside (?\<Theta>1 \<union> ?\<Theta>))"
```
```   621           by (simp add: \<open>simple_path c1\<close> \<open>simple_path c\<close> bounded_inside bounded_simple_path_image)
```
```   622         have if1: "- (inside (?\<Theta>1 \<union> ?\<Theta>) \<union> frontier (inside (?\<Theta>1 \<union> ?\<Theta>))) = - ?\<Theta>1 \<inter> - ?\<Theta> \<inter> - inside (?\<Theta>1 \<union> ?\<Theta>)"
```
```   623           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))
```
```   624         then show "connected (- closure (inside (?\<Theta>1 \<union> ?\<Theta>)))"
```
```   625           by (metis Compl_Un outside_inside co_out1c closure_Un_frontier)
```
```   626         have if2: "- (inside (?\<Theta>2 \<union> ?\<Theta>) \<union> frontier (inside (?\<Theta>2 \<union> ?\<Theta>))) = - ?\<Theta>2 \<inter> - ?\<Theta> \<inter> - inside (?\<Theta>2 \<union> ?\<Theta>)"
```
```   627           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 closure_Un_frontier fr_out(2))
```
```   628         then show "connected (- closure (inside (?\<Theta>2 \<union> ?\<Theta>)))"
```
```   629           by (metis Compl_Un outside_inside co_out2c closure_Un_frontier)
```
```   630         have "connected(?\<Theta>)"
```
```   631           by (metis \<open>simple_path c\<close> connected_simple_path_image)
```
```   632         moreover
```
```   633         have "closure (inside (?\<Theta>1 \<union> ?\<Theta>)) \<inter> closure (inside (?\<Theta>2 \<union> ?\<Theta>)) = ?\<Theta>"
```
```   634           (is "?lhs = ?rhs")
```
```   635         proof
```
```   636           show "?lhs \<subseteq> ?rhs"
```
```   637           proof clarify
```
```   638             fix x
```
```   639             assume x: "x \<in> closure (inside (?\<Theta>1 \<union> ?\<Theta>))" "x \<in> closure (inside (?\<Theta>2 \<union> ?\<Theta>))"
```
```   640             then have "x \<notin> inside (?\<Theta>1 \<union> ?\<Theta>)"
```
```   641               by (meson closure_iff_nhds_not_empty in_sub_out12 inside_Int_outside op_in1c)
```
```   642             with fr_in x show "x \<in> ?\<Theta>"
```
```   643               by (metis c1c c1c2 closure_Un_frontier pa1_disj_in2 Int_iff Un_iff insert_disjoint(2) insert_subset subsetI subset_antisym)
```
```   644           qed
```
```   645           show "?rhs \<subseteq> ?lhs"
```
```   646             using if1 if2 closure_Un_frontier by fastforce
```
```   647         qed
```
```   648         ultimately
```
```   649         show "connected (closure (inside (?\<Theta>1 \<union> ?\<Theta>)) \<inter> closure (inside (?\<Theta>2 \<union> ?\<Theta>)))"
```
```   650           by auto
```
```   651       qed
```
```   652       show "connected (outside (?\<Theta>1 \<union> ?\<Theta>) \<inter> outside (?\<Theta>2 \<union> ?\<Theta>))"
```
```   653         using fr_in conn_U  by (simp add: closure_Un_frontier outside_inside Un_commute)
```
```   654       show "outside (?\<Theta>1 \<union> ?\<Theta>) \<inter> outside (?\<Theta>2 \<union> ?\<Theta>) \<subseteq> - (?\<Theta>1 \<union> ?\<Theta>2)"
```
```   655         by clarify (metis Diff_Compl Diff_iff Un_iff inf_sup_absorb outside_inside)
```
```   656       show "outside (?\<Theta>1 \<union> ?\<Theta>2) \<inter>
```
```   657             (outside (?\<Theta>1 \<union> ?\<Theta>) \<inter> outside (?\<Theta>2 \<union> ?\<Theta>)) \<noteq> {}"
```
```   658         by (metis Int_assoc out_in inf.orderE out_sub12(1) out_sub12(2) outside_in_components)
```
```   659     qed
```
```   660     show "inside (?\<Theta>1 \<union> ?\<Theta>) \<union> inside (?\<Theta>2 \<union> ?\<Theta>) \<union> (?\<Theta> - {a, b}) = inside (?\<Theta>1 \<union> ?\<Theta>2)"
```
```   661       (is "?lhs = ?rhs")
```
```   662     proof
```
```   663       show "?lhs \<subseteq> ?rhs"
```
```   664         apply (simp add: in_sub_in1 in_sub_in2)
```
```   665         using c1c c2c inside_outside pi_disjoint by fastforce
```
```   666       have "inside (?\<Theta>1 \<union> ?\<Theta>2) \<subseteq> inside (?\<Theta>1 \<union> ?\<Theta>) \<union> inside (?\<Theta>2 \<union> ?\<Theta>) \<union> (?\<Theta>)"
```
```   667         using Compl_anti_mono [OF *] by (force simp: inside_outside)
```
```   668       moreover have "inside (?\<Theta>1 \<union> ?\<Theta>2) \<subseteq> -{a,b}"
```
```   669         using c1 union_with_outside by fastforce
```
```   670       ultimately show "?rhs \<subseteq> ?lhs" by auto
```
```   671     qed
```
```   672   qed
```
```   673 qed
```
```   674
```
```   675 end
```