More topological results overlooked last time
authorpaulson <lp15@cam.ac.uk>
Mon Oct 30 17:20:56 2017 +0000 (19 months ago)
changeset 66941c67bb79a0ceb
parent 66940 e5776e8e152b
child 66951 dd4710b91277
More topological results overlooked last time
src/HOL/Analysis/Further_Topology.thy
src/HOL/Analysis/Riemann_Mapping.thy
     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>