src/HOL/Analysis/Further_Topology.thy
changeset 66941 c67bb79a0ceb
parent 66939 04678058308f
child 66955 289f390c4e57
     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"