diff -r 7538b5f301ea -r 16d98ef49a2c src/HOL/Analysis/Jordan_Curve.thy --- a/src/HOL/Analysis/Jordan_Curve.thy Wed Jul 18 17:01:12 2018 +0200 +++ b/src/HOL/Analysis/Jordan_Curve.thy Tue Jul 17 12:23:37 2018 +0200 @@ -6,7 +6,6 @@ theory Jordan_Curve imports Arcwise_Connected Further_Topology - begin subsection\Janiszewski's theorem\ @@ -114,8 +113,8 @@ theorem Janiszewski: - fixes a b::complex - assumes "compact S" "closed T" and conST: "connected(S \ T)" + fixes a b :: complex + assumes "compact S" "closed T" and conST: "connected (S \ T)" and ccS: "connected_component (- S) a b" and ccT: "connected_component (- T) a b" shows "connected_component (- (S \ T)) a b" proof - @@ -166,6 +165,7 @@ using Janiszewski [OF ST] by (metis IntD1 IntD2 notST compl_sup connected_iff_connected_component) + subsection\The Jordan Curve theorem\ lemma exists_double_arc: @@ -219,7 +219,7 @@ qed -theorem Jordan_curve: +theorem%unimportant Jordan_curve: fixes c :: "real \ complex" assumes "simple_path c" and loop: "pathfinish c = pathstart c" obtains inner outer where @@ -389,7 +389,7 @@ qed -corollary Jordan_disconnected: +corollary%unimportant Jordan_disconnected: fixes c :: "real \ complex" assumes "simple_path c" "pathfinish c = pathstart c" shows "\ connected(- path_image c)"