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