src/HOL/Analysis/Connected.thy
changeset 66939 04678058308f
parent 66884 c2128ab11f61
child 66953 826a5fd4d36c
     1.1 --- a/src/HOL/Analysis/Connected.thy	Sun Oct 29 19:39:03 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Connected.thy	Mon Oct 30 16:02:59 2017 +0000
     1.3 @@ -810,6 +810,10 @@
     1.4      by (auto simp: closedin_closed)
     1.5  qed
     1.6  
     1.7 +lemma closedin_component:
     1.8 +   "C \<in> components s \<Longrightarrow> closedin (subtopology euclidean s) C"
     1.9 +  using closedin_connected_component componentsE by blast
    1.10 +
    1.11  
    1.12  subsection \<open>Intersecting chains of compact sets and the Baire property\<close>
    1.13  
    1.14 @@ -3235,39 +3239,29 @@
    1.15  using assms
    1.16  by (auto simp: continuous_on_id intro: continuous_on_cases_le [where h = id, simplified])
    1.17  
    1.18 -text\<open>Some more convenient intermediate-value theorem formulations.\<close>
    1.19 +subsubsection\<open>Some more convenient intermediate-value theorem formulations.\<close>
    1.20  
    1.21  lemma connected_ivt_hyperplane:
    1.22 -  assumes "connected s"
    1.23 -    and "x \<in> s"
    1.24 -    and "y \<in> s"
    1.25 -    and "inner a x \<le> b"
    1.26 -    and "b \<le> inner a y"
    1.27 -  shows "\<exists>z \<in> s. inner a z = b"
    1.28 +  assumes "connected S" and xy: "x \<in> S" "y \<in> S" and b: "inner a x \<le> b" "b \<le> inner a y"
    1.29 +  shows "\<exists>z \<in> S. inner a z = b"
    1.30  proof (rule ccontr)
    1.31 -  assume as:"\<not> (\<exists>z\<in>s. inner a z = b)"
    1.32 +  assume as:"\<not> (\<exists>z\<in>S. inner a z = b)"
    1.33    let ?A = "{x. inner a x < b}"
    1.34    let ?B = "{x. inner a x > b}"
    1.35    have "open ?A" "open ?B"
    1.36      using open_halfspace_lt and open_halfspace_gt by auto
    1.37 -  moreover
    1.38 -  have "?A \<inter> ?B = {}" by auto
    1.39 -  moreover
    1.40 -  have "s \<subseteq> ?A \<union> ?B" using as by auto
    1.41 -  ultimately
    1.42 -  show False
    1.43 -    using assms(1)[unfolded connected_def not_ex,
    1.44 +  moreover have "?A \<inter> ?B = {}" by auto
    1.45 +  moreover have "S \<subseteq> ?A \<union> ?B" using as by auto
    1.46 +  ultimately show False
    1.47 +    using \<open>connected S\<close>[unfolded connected_def not_ex,
    1.48        THEN spec[where x="?A"], THEN spec[where x="?B"]]
    1.49 -    using assms(2-5)
    1.50 -    by auto
    1.51 +    using xy b by auto
    1.52  qed
    1.53  
    1.54  lemma connected_ivt_component:
    1.55    fixes x::"'a::euclidean_space"
    1.56 -  shows "connected s \<Longrightarrow>
    1.57 -    x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow>
    1.58 -    x\<bullet>k \<le> a \<Longrightarrow> a \<le> y\<bullet>k \<Longrightarrow> (\<exists>z\<in>s.  z\<bullet>k = a)"
    1.59 -  using connected_ivt_hyperplane[of s x y "k::'a" a]
    1.60 +  shows "connected S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x\<bullet>k \<le> a \<Longrightarrow> a \<le> y\<bullet>k \<Longrightarrow> (\<exists>z\<in>S.  z\<bullet>k = a)"
    1.61 +  using connected_ivt_hyperplane[of S x y "k::'a" a]
    1.62    by (auto simp: inner_commute)
    1.63  
    1.64  lemma image_affinity_cbox: fixes m::real
    1.65 @@ -4942,7 +4936,7 @@
    1.66  qed
    1.67  
    1.68  
    1.69 -proposition component_complement_connected:
    1.70 +proposition component_diff_connected:
    1.71    fixes S :: "'a::metric_space set"
    1.72    assumes "connected S" "connected U" "S \<subseteq> U" and C: "C \<in> components (U - S)"
    1.73    shows "connected(U - C)"