src/HOL/Analysis/Riemann_Mapping.thy
changeset 66941 c67bb79a0ceb
parent 66827 c94531b5007d
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Analysis/Riemann_Mapping.thy	Mon Oct 30 16:03:21 2017 +0000
     1.2 +++ b/src/HOL/Analysis/Riemann_Mapping.thy	Mon Oct 30 17:20:56 2017 +0000
     1.3 @@ -1416,7 +1416,56 @@
     1.4  qed
     1.5  
     1.6  
     1.7 -text\<open>Finally, pick out the Riemann Mapping Theorem from the earlier chain\<close>
     1.8 +subsection\<open>More Borsukian results\<close>
     1.9 +
    1.10 +lemma Borsukian_componentwise_eq:
    1.11 +  fixes S :: "'a::euclidean_space set"
    1.12 +  assumes S: "locally connected S \<or> compact S"
    1.13 +  shows "Borsukian S \<longleftrightarrow> (\<forall>C \<in> components S. Borsukian C)"
    1.14 +proof -
    1.15 +  have *: "ANR(-{0::complex})"
    1.16 +    by (simp add: ANR_delete open_Compl open_imp_ANR)
    1.17 +  show ?thesis
    1.18 +    using cohomotopically_trivial_on_components [OF assms *] by (auto simp: Borsukian_alt)
    1.19 +qed
    1.20 +
    1.21 +lemma Borsukian_componentwise:
    1.22 +  fixes S :: "'a::euclidean_space set"
    1.23 +  assumes "locally connected S \<or> compact S" "\<And>C. C \<in> components S \<Longrightarrow> Borsukian C"
    1.24 +  shows "Borsukian S"
    1.25 +  by (metis Borsukian_componentwise_eq assms)
    1.26 +
    1.27 +lemma simply_connected_eq_Borsukian:
    1.28 +  fixes S :: "complex set"
    1.29 +  shows "open S \<Longrightarrow> (simply_connected S \<longleftrightarrow> connected S \<and> Borsukian S)"
    1.30 +  by (auto simp: simply_connected_eq_continuous_log Borsukian_continuous_logarithm)
    1.31 +
    1.32 +lemma Borsukian_eq_simply_connected:
    1.33 +  fixes S :: "complex set"
    1.34 +  shows "open S \<Longrightarrow> Borsukian S \<longleftrightarrow> (\<forall>C \<in> components S. simply_connected C)"
    1.35 +apply (auto simp: Borsukian_componentwise_eq open_imp_locally_connected)
    1.36 +  using in_components_connected open_components simply_connected_eq_Borsukian apply blast
    1.37 +  using open_components simply_connected_eq_Borsukian by blast
    1.38 +
    1.39 +lemma Borsukian_separation_open_closed:
    1.40 +  fixes S :: "complex set"
    1.41 +  assumes S: "open S \<or> closed S" and "bounded S"
    1.42 +  shows "Borsukian S \<longleftrightarrow> connected(- S)"
    1.43 +  using S
    1.44 +proof
    1.45 +  assume "open S"
    1.46 +  show ?thesis
    1.47 +    unfolding Borsukian_eq_simply_connected [OF \<open>open S\<close>]
    1.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)
    1.49 +next
    1.50 +  assume "closed S"
    1.51 +  with \<open>bounded S\<close> show ?thesis
    1.52 +    by (simp add: Borsukian_separation_compact compact_eq_bounded_closed)
    1.53 +qed
    1.54 +
    1.55 +
    1.56 +subsection\<open>Finally, the Riemann Mapping Theorem\<close>
    1.57 +
    1.58  theorem Riemann_mapping_theorem:
    1.59      "open S \<and> simply_connected S \<longleftrightarrow>
    1.60       S = {} \<or> S = UNIV \<or>