# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1509384056 0
# Node ID c67bb79a0ceb85982db035b0d547fa4aeba580db
# Parent  e5776e8e152b0aef1534269e4c4e3463e52ce29b
More topological results overlooked last time

diff -r e5776e8e152b -r c67bb79a0ceb src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Mon Oct 30 16:03:21 2017 +0000
+++ b/src/HOL/Analysis/Further_Topology.thy	Mon Oct 30 17:20:56 2017 +0000
@@ -4972,7 +4972,6 @@
 qed
 
 
-
 subsection\<open>Several common variants of unicoherence\<close>
 
 lemma connected_frontier_simple:
@@ -5025,6 +5024,9 @@
     using \<open>connected S\<close> connected_frontier_component_complement by auto
 qed
 
+
+subsection\<open>Some separation results\<close>
+
 lemma separation_by_component_closed_pointwise:
   fixes S :: "'a :: euclidean_space set"
   assumes "closed S" "\<not> connected_component (- S) a b"
diff -r e5776e8e152b -r c67bb79a0ceb src/HOL/Analysis/Riemann_Mapping.thy
--- a/src/HOL/Analysis/Riemann_Mapping.thy	Mon Oct 30 16:03:21 2017 +0000
+++ b/src/HOL/Analysis/Riemann_Mapping.thy	Mon Oct 30 17:20:56 2017 +0000
@@ -1416,7 +1416,56 @@
 qed
 
 
-text\<open>Finally, pick out the Riemann Mapping Theorem from the earlier chain\<close>
+subsection\<open>More Borsukian results\<close>
+
+lemma Borsukian_componentwise_eq:
+  fixes S :: "'a::euclidean_space set"
+  assumes S: "locally connected S \<or> compact S"
+  shows "Borsukian S \<longleftrightarrow> (\<forall>C \<in> components S. Borsukian C)"
+proof -
+  have *: "ANR(-{0::complex})"
+    by (simp add: ANR_delete open_Compl open_imp_ANR)
+  show ?thesis
+    using cohomotopically_trivial_on_components [OF assms *] by (auto simp: Borsukian_alt)
+qed
+
+lemma Borsukian_componentwise:
+  fixes S :: "'a::euclidean_space set"
+  assumes "locally connected S \<or> compact S" "\<And>C. C \<in> components S \<Longrightarrow> Borsukian C"
+  shows "Borsukian S"
+  by (metis Borsukian_componentwise_eq assms)
+
+lemma simply_connected_eq_Borsukian:
+  fixes S :: "complex set"
+  shows "open S \<Longrightarrow> (simply_connected S \<longleftrightarrow> connected S \<and> Borsukian S)"
+  by (auto simp: simply_connected_eq_continuous_log Borsukian_continuous_logarithm)
+
+lemma Borsukian_eq_simply_connected:
+  fixes S :: "complex set"
+  shows "open S \<Longrightarrow> Borsukian S \<longleftrightarrow> (\<forall>C \<in> components S. simply_connected C)"
+apply (auto simp: Borsukian_componentwise_eq open_imp_locally_connected)
+  using in_components_connected open_components simply_connected_eq_Borsukian apply blast
+  using open_components simply_connected_eq_Borsukian by blast
+
+lemma Borsukian_separation_open_closed:
+  fixes S :: "complex set"
+  assumes S: "open S \<or> closed S" and "bounded S"
+  shows "Borsukian S \<longleftrightarrow> connected(- S)"
+  using S
+proof
+  assume "open S"
+  show ?thesis
+    unfolding Borsukian_eq_simply_connected [OF \<open>open S\<close>]
+    by (meson \<open>open S\<close> \<open>bounded S\<close> bounded_subset in_components_connected in_components_subset nonseparation_by_component_eq open_components simply_connected_iff_simple)
+next
+  assume "closed S"
+  with \<open>bounded S\<close> show ?thesis
+    by (simp add: Borsukian_separation_compact compact_eq_bounded_closed)
+qed
+
+
+subsection\<open>Finally, the Riemann Mapping Theorem\<close>
+
 theorem Riemann_mapping_theorem:
     "open S \<and> simply_connected S \<longleftrightarrow>
      S = {} \<or> S = UNIV \<or>