src/HOL/Analysis/Homotopy.thy
changeset 69918 eddcc7c726f3
parent 69768 7e4966eaf781
child 69922 4a9167f377b0
     1.1 --- a/src/HOL/Analysis/Homotopy.thy	Sun Mar 17 21:26:42 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Homotopy.thy	Mon Mar 18 15:35:34 2019 +0000
     1.3 @@ -3652,6 +3652,11 @@
     1.4      using \<open>S \<subseteq> box a b\<close> by auto
     1.5  qed
     1.6  
     1.7 +corollary bounded_path_connected_Compl_real:
     1.8 +  fixes S :: "real set"
     1.9 +  assumes "bounded S" "path_connected(- S)" shows "S = {}"
    1.10 +  by (simp add: assms bounded_connected_Compl_real path_connected_imp_connected)
    1.11 +
    1.12  lemma bounded_connected_Compl_1:
    1.13    fixes S :: "'a::{euclidean_space} set"
    1.14    assumes "bounded S" and conn: "connected(- S)" and 1: "DIM('a) = 1"