author paulson Mon Oct 30 17:20:56 2017 +0000 (19 months ago) changeset 66941 c67bb79a0ceb parent 66940 e5776e8e152b child 66951 dd4710b91277
More topological results overlooked last time
```     1.1 --- a/src/HOL/Analysis/Further_Topology.thy	Mon Oct 30 16:03:21 2017 +0000
1.2 +++ b/src/HOL/Analysis/Further_Topology.thy	Mon Oct 30 17:20:56 2017 +0000
1.3 @@ -4972,7 +4972,6 @@
1.4  qed
1.5
1.6
1.7 -
1.8  subsection\<open>Several common variants of unicoherence\<close>
1.9
1.10  lemma connected_frontier_simple:
1.11 @@ -5025,6 +5024,9 @@
1.12      using \<open>connected S\<close> connected_frontier_component_complement by auto
1.13  qed
1.14
1.15 +
1.16 +subsection\<open>Some separation results\<close>
1.17 +
1.18  lemma separation_by_component_closed_pointwise:
1.19    fixes S :: "'a :: euclidean_space set"
1.20    assumes "closed S" "\<not> connected_component (- S) a b"
```
```     2.1 --- a/src/HOL/Analysis/Riemann_Mapping.thy	Mon Oct 30 16:03:21 2017 +0000
2.2 +++ b/src/HOL/Analysis/Riemann_Mapping.thy	Mon Oct 30 17:20:56 2017 +0000
2.3 @@ -1416,7 +1416,56 @@
2.4  qed
2.5
2.6
2.7 -text\<open>Finally, pick out the Riemann Mapping Theorem from the earlier chain\<close>
2.8 +subsection\<open>More Borsukian results\<close>
2.9 +
2.10 +lemma Borsukian_componentwise_eq:
2.11 +  fixes S :: "'a::euclidean_space set"
2.12 +  assumes S: "locally connected S \<or> compact S"
2.13 +  shows "Borsukian S \<longleftrightarrow> (\<forall>C \<in> components S. Borsukian C)"
2.14 +proof -
2.15 +  have *: "ANR(-{0::complex})"
2.16 +    by (simp add: ANR_delete open_Compl open_imp_ANR)
2.17 +  show ?thesis
2.18 +    using cohomotopically_trivial_on_components [OF assms *] by (auto simp: Borsukian_alt)
2.19 +qed
2.20 +
2.21 +lemma Borsukian_componentwise:
2.22 +  fixes S :: "'a::euclidean_space set"
2.23 +  assumes "locally connected S \<or> compact S" "\<And>C. C \<in> components S \<Longrightarrow> Borsukian C"
2.24 +  shows "Borsukian S"
2.25 +  by (metis Borsukian_componentwise_eq assms)
2.26 +
2.27 +lemma simply_connected_eq_Borsukian:
2.28 +  fixes S :: "complex set"
2.29 +  shows "open S \<Longrightarrow> (simply_connected S \<longleftrightarrow> connected S \<and> Borsukian S)"
2.30 +  by (auto simp: simply_connected_eq_continuous_log Borsukian_continuous_logarithm)
2.31 +
2.32 +lemma Borsukian_eq_simply_connected:
2.33 +  fixes S :: "complex set"
2.34 +  shows "open S \<Longrightarrow> Borsukian S \<longleftrightarrow> (\<forall>C \<in> components S. simply_connected C)"
2.35 +apply (auto simp: Borsukian_componentwise_eq open_imp_locally_connected)
2.36 +  using in_components_connected open_components simply_connected_eq_Borsukian apply blast
2.37 +  using open_components simply_connected_eq_Borsukian by blast
2.38 +
2.39 +lemma Borsukian_separation_open_closed:
2.40 +  fixes S :: "complex set"
2.41 +  assumes S: "open S \<or> closed S" and "bounded S"
2.42 +  shows "Borsukian S \<longleftrightarrow> connected(- S)"
2.43 +  using S
2.44 +proof
2.45 +  assume "open S"
2.46 +  show ?thesis
2.47 +    unfolding Borsukian_eq_simply_connected [OF \<open>open S\<close>]
2.48 +    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)
2.49 +next
2.50 +  assume "closed S"
2.51 +  with \<open>bounded S\<close> show ?thesis
2.52 +    by (simp add: Borsukian_separation_compact compact_eq_bounded_closed)
2.53 +qed
2.54 +
2.55 +
2.56 +subsection\<open>Finally, the Riemann Mapping Theorem\<close>
2.57 +
2.58  theorem Riemann_mapping_theorem:
2.59      "open S \<and> simply_connected S \<longleftrightarrow>
2.60       S = {} \<or> S = UNIV \<or>
```