src/HOL/Analysis/Jordan_Curve.thy
changeset 68651 16d98ef49a2c
parent 67968 a5ad4c015d1c
     1.1 --- a/src/HOL/Analysis/Jordan_Curve.thy	Mon Apr 09 16:20:23 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)"