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)"
```