src/HOL/Topological_Spaces.thy
changeset 61306 9dd394c866fc
parent 61245 b77bf45efe21
child 61342 b98cd131e2b5
     1.1 --- a/src/HOL/Topological_Spaces.thy	Thu Oct 01 23:26:31 2015 +0200
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Oct 02 15:07:41 2015 +0100
     1.3 @@ -1826,7 +1826,10 @@
     1.4    \<Longrightarrow> connected U"
     1.5    by (auto simp: connected_def)
     1.6  
     1.7 -lemma connected_empty[simp]: "connected {}"
     1.8 +lemma connected_empty [simp]: "connected {}"
     1.9 +  by (auto intro!: connectedI)
    1.10 +
    1.11 +lemma connected_sing [simp]: "connected {x}"
    1.12    by (auto intro!: connectedI)
    1.13  
    1.14  lemma connectedD:
    1.15 @@ -1835,6 +1838,78 @@
    1.16  
    1.17  end
    1.18  
    1.19 +lemma connected_closed:
    1.20 +    "connected s \<longleftrightarrow>
    1.21 +     ~ (\<exists>A B. closed A \<and> closed B \<and> s \<subseteq> A \<union> B \<and> A \<inter> B \<inter> s = {} \<and> A \<inter> s \<noteq> {} \<and> B \<inter> s \<noteq> {})"
    1.22 +apply (simp add: connected_def del: ex_simps, safe)
    1.23 +apply (drule_tac x="-A" in spec)
    1.24 +apply (drule_tac x="-B" in spec)
    1.25 +apply (fastforce simp add: closed_def [symmetric])
    1.26 +apply (drule_tac x="-A" in spec)
    1.27 +apply (drule_tac x="-B" in spec)
    1.28 +apply (fastforce simp add: open_closed [symmetric])
    1.29 +done
    1.30 +
    1.31 +
    1.32 +lemma connected_Union:
    1.33 +  assumes cs: "\<And>s. s \<in> S \<Longrightarrow> connected s" and ne: "\<Inter>S \<noteq> {}"
    1.34 +    shows "connected(\<Union>S)"
    1.35 +proof (rule connectedI)
    1.36 +  fix A B
    1.37 +  assume A: "open A" and B: "open B" and Alap: "A \<inter> \<Union>S \<noteq> {}" and Blap: "B \<inter> \<Union>S \<noteq> {}"
    1.38 +     and disj: "A \<inter> B \<inter> \<Union>S = {}" and cover: "\<Union>S \<subseteq> A \<union> B"
    1.39 +  have disjs:"\<And>s. s \<in> S \<Longrightarrow> A \<inter> B \<inter> s = {}"
    1.40 +    using disj by auto
    1.41 +  obtain sa where sa: "sa \<in> S" "A \<inter> sa \<noteq> {}"
    1.42 +    using Alap by auto
    1.43 +  obtain sb where sb: "sb \<in> S" "B \<inter> sb \<noteq> {}"
    1.44 +    using Blap by auto
    1.45 +  obtain x where x: "\<And>s. s \<in> S \<Longrightarrow> x \<in> s"
    1.46 +    using ne by auto
    1.47 +  then have "x \<in> \<Union>S"
    1.48 +    using `sa \<in> S` by blast
    1.49 +  then have "x \<in> A \<or> x \<in> B"
    1.50 +    using cover by auto
    1.51 +  then show False
    1.52 +    using cs [unfolded connected_def]
    1.53 +    by (metis A B IntI Sup_upper sa sb disjs x cover empty_iff subset_trans)
    1.54 +qed
    1.55 +
    1.56 +lemma connected_Un: "\<lbrakk>connected s; connected t; s \<inter> t \<noteq> {}\<rbrakk> \<Longrightarrow> connected (s \<union> t)"
    1.57 +  using connected_Union [of "{s,t}"] by auto
    1.58 +
    1.59 +lemma connected_diff_open_from_closed:
    1.60 +  assumes st: "s \<subseteq> t" and tu: "t \<subseteq> u" and s: "open s"
    1.61 +      and t: "closed t" and u: "connected u" and ts: "connected (t - s)"
    1.62 +  shows "connected(u - s)"
    1.63 +proof (rule connectedI)
    1.64 +  fix A B
    1.65 +  assume AB: "open A" "open B" "A \<inter> (u - s) \<noteq> {}" "B \<inter> (u - s) \<noteq> {}"
    1.66 +     and disj: "A \<inter> B \<inter> (u - s) = {}" and cover: "u - s \<subseteq> A \<union> B"
    1.67 +  then consider "A \<inter> (t - s) = {}" | "B \<inter> (t - s) = {}"
    1.68 +    using st ts tu connectedD [of "t-s" "A" "B"]
    1.69 +    by auto
    1.70 +  then show False
    1.71 +  proof cases
    1.72 +    case 1
    1.73 +    then have "(A - t) \<inter> (B \<union> s) \<inter> u = {}"
    1.74 +      using disj st by auto
    1.75 +    moreover have  "u \<subseteq> (A - t) \<union> (B \<union> s)" using 1 cover by auto
    1.76 +    ultimately show False
    1.77 +      using connectedD [of u "A - t" "B \<union> s"] AB s t 1 u
    1.78 +      by auto
    1.79 +  next
    1.80 +    case 2
    1.81 +    then have "(A \<union> s) \<inter> (B - t) \<inter> u = {}"
    1.82 +      using disj st
    1.83 +      by auto
    1.84 +    moreover have "u \<subseteq> (A \<union> s) \<union> (B - t)" using 2 cover by auto
    1.85 +    ultimately show False
    1.86 +      using connectedD [of u "A \<union> s" "B - t"] AB s t 2 u
    1.87 +      by auto
    1.88 +  qed
    1.89 +qed
    1.90 +
    1.91  lemma connected_iff_const:
    1.92    fixes S :: "'a::topological_space set"
    1.93    shows "connected S \<longleftrightarrow> (\<forall>P::'a \<Rightarrow> bool. continuous_on S P \<longrightarrow> (\<exists>c. \<forall>s\<in>S. P s = c))"
    1.94 @@ -1938,7 +2013,8 @@
    1.95      by auto
    1.96  qed
    1.97  
    1.98 -section \<open>Connectedness\<close>
    1.99 +
   1.100 +section \<open>Linear Continuum Topologies\<close>
   1.101  
   1.102  class linear_continuum_topology = linorder_topology + linear_continuum
   1.103  begin