src/HOL/Analysis/Jordan_Curve.thy
 changeset 68651 16d98ef49a2c parent 67968 a5ad4c015d1c child 69508 2a4c8a2a3f8e
```     1.1 --- a/src/HOL/Analysis/Jordan_Curve.thy	Wed Jul 18 17:01:12 2018 +0200
1.2 +++ b/src/HOL/Analysis/Jordan_Curve.thy	Tue Jul 17 12:23:37 2018 +0200
1.3 @@ -6,7 +6,6 @@
1.4
1.5  theory Jordan_Curve
1.6    imports Arcwise_Connected Further_Topology
1.7 -
1.8  begin
1.9
1.10  subsection\<open>Janiszewski's theorem\<close>
1.11 @@ -114,8 +113,8 @@
1.12
1.13
1.14  theorem Janiszewski:
1.15 -  fixes a b::complex
1.16 -  assumes "compact S" "closed T" and conST: "connected(S \<inter> T)"
1.17 +  fixes a b :: complex
1.18 +  assumes "compact S" "closed T" and conST: "connected (S \<inter> T)"
1.19        and ccS: "connected_component (- S) a b" and ccT: "connected_component (- T) a b"
1.20      shows "connected_component (- (S \<union> T)) a b"
1.21  proof -
1.22 @@ -166,6 +165,7 @@
1.23  using Janiszewski [OF ST]
1.24  by (metis IntD1 IntD2 notST compl_sup connected_iff_connected_component)
1.25
1.26 +
1.27  subsection\<open>The Jordan Curve theorem\<close>
1.28
1.29  lemma exists_double_arc:
1.30 @@ -219,7 +219,7 @@
1.31  qed
1.32
1.33
1.34 -theorem Jordan_curve:
1.35 +theorem%unimportant Jordan_curve:
1.36    fixes c :: "real \<Rightarrow> complex"
1.37    assumes "simple_path c" and loop: "pathfinish c = pathstart c"
1.38    obtains inner outer where
1.39 @@ -389,7 +389,7 @@
1.40  qed
1.41
1.42
1.43 -corollary Jordan_disconnected:
1.44 +corollary%unimportant Jordan_disconnected:
1.45    fixes c :: "real \<Rightarrow> complex"
1.46    assumes "simple_path c" "pathfinish c = pathstart c"
1.47      shows "\<not> connected(- path_image c)"
```