src/HOL/Analysis/Connected.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 months ago)
changeset 69981 3dced198b9ec
parent 69922 4a9167f377b0
child 70136 f03a01a18c6e
permissions -rw-r--r--
more strict AFP properties;
     1 (*  Author:     L C Paulson, University of Cambridge
     2     Material split off from Topology_Euclidean_Space
     3 *)
     4 
     5 section \<open>Connected Components\<close>
     6 
     7 theory Connected
     8   imports
     9     Abstract_Topology_2
    10 begin
    11 
    12 subsection%unimportant \<open>Connectedness\<close>
    13 
    14 lemma connected_local:
    15  "connected S \<longleftrightarrow>
    16   \<not> (\<exists>e1 e2.
    17       openin (top_of_set S) e1 \<and>
    18       openin (top_of_set S) e2 \<and>
    19       S \<subseteq> e1 \<union> e2 \<and>
    20       e1 \<inter> e2 = {} \<and>
    21       e1 \<noteq> {} \<and>
    22       e2 \<noteq> {})"
    23   unfolding connected_def openin_open
    24   by safe blast+
    25 
    26 lemma exists_diff:
    27   fixes P :: "'a set \<Rightarrow> bool"
    28   shows "(\<exists>S. P (- S)) \<longleftrightarrow> (\<exists>S. P S)"
    29     (is "?lhs \<longleftrightarrow> ?rhs")
    30 proof -
    31   have ?rhs if ?lhs
    32     using that by blast
    33   moreover have "P (- (- S))" if "P S" for S
    34   proof -
    35     have "S = - (- S)" by simp
    36     with that show ?thesis by metis
    37   qed
    38   ultimately show ?thesis by metis
    39 qed
    40 
    41 lemma connected_clopen: "connected S \<longleftrightarrow>
    42   (\<forall>T. openin (top_of_set S) T \<and>
    43      closedin (top_of_set S) T \<longrightarrow> T = {} \<or> T = S)" (is "?lhs \<longleftrightarrow> ?rhs")
    44 proof -
    45   have "\<not> connected S \<longleftrightarrow>
    46     (\<exists>e1 e2. open e1 \<and> open (- e2) \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
    47     unfolding connected_def openin_open closedin_closed
    48     by (metis double_complement)
    49   then have th0: "connected S \<longleftrightarrow>
    50     \<not> (\<exists>e2 e1. closed e2 \<and> open e1 \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
    51     (is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)")
    52     by (simp add: closed_def) metis
    53   have th1: "?rhs \<longleftrightarrow> \<not> (\<exists>t' t. closed t'\<and>t = S\<inter>t' \<and> t\<noteq>{} \<and> t\<noteq>S \<and> (\<exists>t'. open t' \<and> t = S \<inter> t'))"
    54     (is "_ \<longleftrightarrow> \<not> (\<exists>t' t. ?Q t' t)")
    55     unfolding connected_def openin_open closedin_closed by auto
    56   have "(\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)" for e2
    57   proof -
    58     have "?P e2 e1 \<longleftrightarrow> (\<exists>t. closed e2 \<and> t = S\<inter>e2 \<and> open e1 \<and> t = S\<inter>e1 \<and> t\<noteq>{} \<and> t \<noteq> S)" for e1
    59       by auto
    60     then show ?thesis
    61       by metis
    62   qed
    63   then have "\<forall>e2. (\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)"
    64     by blast
    65   then show ?thesis
    66     by (simp add: th0 th1)
    67 qed
    68 
    69 subsection \<open>Connected components, considered as a connectedness relation or a set\<close>
    70 
    71 definition%important "connected_component s x y \<equiv> \<exists>t. connected t \<and> t \<subseteq> s \<and> x \<in> t \<and> y \<in> t"
    72 
    73 abbreviation "connected_component_set s x \<equiv> Collect (connected_component s x)"
    74 
    75 lemma connected_componentI:
    76   "connected t \<Longrightarrow> t \<subseteq> s \<Longrightarrow> x \<in> t \<Longrightarrow> y \<in> t \<Longrightarrow> connected_component s x y"
    77   by (auto simp: connected_component_def)
    78 
    79 lemma connected_component_in: "connected_component s x y \<Longrightarrow> x \<in> s \<and> y \<in> s"
    80   by (auto simp: connected_component_def)
    81 
    82 lemma connected_component_refl: "x \<in> s \<Longrightarrow> connected_component s x x"
    83   by (auto simp: connected_component_def) (use connected_sing in blast)
    84 
    85 lemma connected_component_refl_eq [simp]: "connected_component s x x \<longleftrightarrow> x \<in> s"
    86   by (auto simp: connected_component_refl) (auto simp: connected_component_def)
    87 
    88 lemma connected_component_sym: "connected_component s x y \<Longrightarrow> connected_component s y x"
    89   by (auto simp: connected_component_def)
    90 
    91 lemma connected_component_trans:
    92   "connected_component s x y \<Longrightarrow> connected_component s y z \<Longrightarrow> connected_component s x z"
    93   unfolding connected_component_def
    94   by (metis Int_iff Un_iff Un_subset_iff equals0D connected_Un)
    95 
    96 lemma connected_component_of_subset:
    97   "connected_component s x y \<Longrightarrow> s \<subseteq> t \<Longrightarrow> connected_component t x y"
    98   by (auto simp: connected_component_def)
    99 
   100 lemma connected_component_Union: "connected_component_set s x = \<Union>{t. connected t \<and> x \<in> t \<and> t \<subseteq> s}"
   101   by (auto simp: connected_component_def)
   102 
   103 lemma connected_connected_component [iff]: "connected (connected_component_set s x)"
   104   by (auto simp: connected_component_Union intro: connected_Union)
   105 
   106 lemma connected_iff_eq_connected_component_set:
   107   "connected s \<longleftrightarrow> (\<forall>x \<in> s. connected_component_set s x = s)"
   108 proof (cases "s = {}")
   109   case True
   110   then show ?thesis by simp
   111 next
   112   case False
   113   then obtain x where "x \<in> s" by auto
   114   show ?thesis
   115   proof
   116     assume "connected s"
   117     then show "\<forall>x \<in> s. connected_component_set s x = s"
   118       by (force simp: connected_component_def)
   119   next
   120     assume "\<forall>x \<in> s. connected_component_set s x = s"
   121     then show "connected s"
   122       by (metis \<open>x \<in> s\<close> connected_connected_component)
   123   qed
   124 qed
   125 
   126 lemma connected_component_subset: "connected_component_set s x \<subseteq> s"
   127   using connected_component_in by blast
   128 
   129 lemma connected_component_eq_self: "connected s \<Longrightarrow> x \<in> s \<Longrightarrow> connected_component_set s x = s"
   130   by (simp add: connected_iff_eq_connected_component_set)
   131 
   132 lemma connected_iff_connected_component:
   133   "connected s \<longleftrightarrow> (\<forall>x \<in> s. \<forall>y \<in> s. connected_component s x y)"
   134   using connected_component_in by (auto simp: connected_iff_eq_connected_component_set)
   135 
   136 lemma connected_component_maximal:
   137   "x \<in> t \<Longrightarrow> connected t \<Longrightarrow> t \<subseteq> s \<Longrightarrow> t \<subseteq> (connected_component_set s x)"
   138   using connected_component_eq_self connected_component_of_subset by blast
   139 
   140 lemma connected_component_mono:
   141   "s \<subseteq> t \<Longrightarrow> connected_component_set s x \<subseteq> connected_component_set t x"
   142   by (simp add: Collect_mono connected_component_of_subset)
   143 
   144 lemma connected_component_eq_empty [simp]: "connected_component_set s x = {} \<longleftrightarrow> x \<notin> s"
   145   using connected_component_refl by (fastforce simp: connected_component_in)
   146 
   147 lemma connected_component_set_empty [simp]: "connected_component_set {} x = {}"
   148   using connected_component_eq_empty by blast
   149 
   150 lemma connected_component_eq:
   151   "y \<in> connected_component_set s x \<Longrightarrow> (connected_component_set s y = connected_component_set s x)"
   152   by (metis (no_types, lifting)
   153       Collect_cong connected_component_sym connected_component_trans mem_Collect_eq)
   154 
   155 lemma closed_connected_component:
   156   assumes s: "closed s"
   157   shows "closed (connected_component_set s x)"
   158 proof (cases "x \<in> s")
   159   case False
   160   then show ?thesis
   161     by (metis connected_component_eq_empty closed_empty)
   162 next
   163   case True
   164   show ?thesis
   165     unfolding closure_eq [symmetric]
   166   proof
   167     show "closure (connected_component_set s x) \<subseteq> connected_component_set s x"
   168       apply (rule connected_component_maximal)
   169         apply (simp add: closure_def True)
   170        apply (simp add: connected_imp_connected_closure)
   171       apply (simp add: s closure_minimal connected_component_subset)
   172       done
   173   next
   174     show "connected_component_set s x \<subseteq> closure (connected_component_set s x)"
   175       by (simp add: closure_subset)
   176   qed
   177 qed
   178 
   179 lemma connected_component_disjoint:
   180   "connected_component_set s a \<inter> connected_component_set s b = {} \<longleftrightarrow>
   181     a \<notin> connected_component_set s b"
   182   apply (auto simp: connected_component_eq)
   183   using connected_component_eq connected_component_sym
   184   apply blast
   185   done
   186 
   187 lemma connected_component_nonoverlap:
   188   "connected_component_set s a \<inter> connected_component_set s b = {} \<longleftrightarrow>
   189     a \<notin> s \<or> b \<notin> s \<or> connected_component_set s a \<noteq> connected_component_set s b"
   190   apply (auto simp: connected_component_in)
   191   using connected_component_refl_eq
   192     apply blast
   193    apply (metis connected_component_eq mem_Collect_eq)
   194   apply (metis connected_component_eq mem_Collect_eq)
   195   done
   196 
   197 lemma connected_component_overlap:
   198   "connected_component_set s a \<inter> connected_component_set s b \<noteq> {} \<longleftrightarrow>
   199     a \<in> s \<and> b \<in> s \<and> connected_component_set s a = connected_component_set s b"
   200   by (auto simp: connected_component_nonoverlap)
   201 
   202 lemma connected_component_sym_eq: "connected_component s x y \<longleftrightarrow> connected_component s y x"
   203   using connected_component_sym by blast
   204 
   205 lemma connected_component_eq_eq:
   206   "connected_component_set s x = connected_component_set s y \<longleftrightarrow>
   207     x \<notin> s \<and> y \<notin> s \<or> x \<in> s \<and> y \<in> s \<and> connected_component s x y"
   208   apply (cases "y \<in> s", simp)
   209    apply (metis connected_component_eq connected_component_eq_empty connected_component_refl_eq mem_Collect_eq)
   210   apply (cases "x \<in> s", simp)
   211    apply (metis connected_component_eq_empty)
   212   using connected_component_eq_empty
   213   apply blast
   214   done
   215 
   216 lemma connected_iff_connected_component_eq:
   217   "connected s \<longleftrightarrow> (\<forall>x \<in> s. \<forall>y \<in> s. connected_component_set s x = connected_component_set s y)"
   218   by (simp add: connected_component_eq_eq connected_iff_connected_component)
   219 
   220 lemma connected_component_idemp:
   221   "connected_component_set (connected_component_set s x) x = connected_component_set s x"
   222   apply (rule subset_antisym)
   223    apply (simp add: connected_component_subset)
   224   apply (metis connected_component_eq_empty connected_component_maximal
   225       connected_component_refl_eq connected_connected_component mem_Collect_eq set_eq_subset)
   226   done
   227 
   228 lemma connected_component_unique:
   229   "\<lbrakk>x \<in> c; c \<subseteq> s; connected c;
   230     \<And>c'. x \<in> c' \<and> c' \<subseteq> s \<and> connected c'
   231               \<Longrightarrow> c' \<subseteq> c\<rbrakk>
   232         \<Longrightarrow> connected_component_set s x = c"
   233 apply (rule subset_antisym)
   234 apply (meson connected_component_maximal connected_component_subset connected_connected_component contra_subsetD)
   235 by (simp add: connected_component_maximal)
   236 
   237 lemma joinable_connected_component_eq:
   238   "\<lbrakk>connected t; t \<subseteq> s;
   239     connected_component_set s x \<inter> t \<noteq> {};
   240     connected_component_set s y \<inter> t \<noteq> {}\<rbrakk>
   241     \<Longrightarrow> connected_component_set s x = connected_component_set s y"
   242 apply (simp add: ex_in_conv [symmetric])
   243 apply (rule connected_component_eq)
   244 by (metis (no_types, hide_lams) connected_component_eq_eq connected_component_in connected_component_maximal subsetD mem_Collect_eq)
   245 
   246 
   247 lemma Union_connected_component: "\<Union>(connected_component_set s ` s) = s"
   248   apply (rule subset_antisym)
   249   apply (simp add: SUP_least connected_component_subset)
   250   using connected_component_refl_eq
   251   by force
   252 
   253 
   254 lemma complement_connected_component_unions:
   255     "s - connected_component_set s x =
   256      \<Union>(connected_component_set s ` s - {connected_component_set s x})"
   257   apply (subst Union_connected_component [symmetric], auto)
   258   apply (metis connected_component_eq_eq connected_component_in)
   259   by (metis connected_component_eq mem_Collect_eq)
   260 
   261 lemma connected_component_intermediate_subset:
   262         "\<lbrakk>connected_component_set u a \<subseteq> t; t \<subseteq> u\<rbrakk>
   263         \<Longrightarrow> connected_component_set t a = connected_component_set u a"
   264   apply (case_tac "a \<in> u")
   265   apply (simp add: connected_component_maximal connected_component_mono subset_antisym)
   266   using connected_component_eq_empty by blast
   267 
   268 
   269 subsection \<open>The set of connected components of a set\<close>
   270 
   271 definition%important components:: "'a::topological_space set \<Rightarrow> 'a set set"
   272   where "components s \<equiv> connected_component_set s ` s"
   273 
   274 lemma components_iff: "s \<in> components u \<longleftrightarrow> (\<exists>x. x \<in> u \<and> s = connected_component_set u x)"
   275   by (auto simp: components_def)
   276 
   277 lemma componentsI: "x \<in> u \<Longrightarrow> connected_component_set u x \<in> components u"
   278   by (auto simp: components_def)
   279 
   280 lemma componentsE:
   281   assumes "s \<in> components u"
   282   obtains x where "x \<in> u" "s = connected_component_set u x"
   283   using assms by (auto simp: components_def)
   284 
   285 lemma Union_components [simp]: "\<Union>(components u) = u"
   286   apply (rule subset_antisym)
   287   using Union_connected_component components_def apply fastforce
   288   apply (metis Union_connected_component components_def set_eq_subset)
   289   done
   290 
   291 lemma pairwise_disjoint_components: "pairwise (\<lambda>X Y. X \<inter> Y = {}) (components u)"
   292   apply (simp add: pairwise_def)
   293   apply (auto simp: components_iff)
   294   apply (metis connected_component_eq_eq connected_component_in)+
   295   done
   296 
   297 lemma in_components_nonempty: "c \<in> components s \<Longrightarrow> c \<noteq> {}"
   298     by (metis components_iff connected_component_eq_empty)
   299 
   300 lemma in_components_subset: "c \<in> components s \<Longrightarrow> c \<subseteq> s"
   301   using Union_components by blast
   302 
   303 lemma in_components_connected: "c \<in> components s \<Longrightarrow> connected c"
   304   by (metis components_iff connected_connected_component)
   305 
   306 lemma in_components_maximal:
   307   "c \<in> components s \<longleftrightarrow>
   308     c \<noteq> {} \<and> c \<subseteq> s \<and> connected c \<and> (\<forall>d. d \<noteq> {} \<and> c \<subseteq> d \<and> d \<subseteq> s \<and> connected d \<longrightarrow> d = c)"
   309   apply (rule iffI)
   310    apply (simp add: in_components_nonempty in_components_connected)
   311    apply (metis (full_types) components_iff connected_component_eq_self connected_component_intermediate_subset connected_component_refl in_components_subset mem_Collect_eq rev_subsetD)
   312   apply (metis bot.extremum_uniqueI components_iff connected_component_eq_empty connected_component_maximal connected_component_subset connected_connected_component subset_emptyI)
   313   done
   314 
   315 lemma joinable_components_eq:
   316   "connected t \<and> t \<subseteq> s \<and> c1 \<in> components s \<and> c2 \<in> components s \<and> c1 \<inter> t \<noteq> {} \<and> c2 \<inter> t \<noteq> {} \<Longrightarrow> c1 = c2"
   317   by (metis (full_types) components_iff joinable_connected_component_eq)
   318 
   319 lemma closed_components: "\<lbrakk>closed s; c \<in> components s\<rbrakk> \<Longrightarrow> closed c"
   320   by (metis closed_connected_component components_iff)
   321 
   322 lemma components_nonoverlap:
   323     "\<lbrakk>c \<in> components s; c' \<in> components s\<rbrakk> \<Longrightarrow> (c \<inter> c' = {}) \<longleftrightarrow> (c \<noteq> c')"
   324   apply (auto simp: in_components_nonempty components_iff)
   325     using connected_component_refl apply blast
   326    apply (metis connected_component_eq_eq connected_component_in)
   327   by (metis connected_component_eq mem_Collect_eq)
   328 
   329 lemma components_eq: "\<lbrakk>c \<in> components s; c' \<in> components s\<rbrakk> \<Longrightarrow> (c = c' \<longleftrightarrow> c \<inter> c' \<noteq> {})"
   330   by (metis components_nonoverlap)
   331 
   332 lemma components_eq_empty [simp]: "components s = {} \<longleftrightarrow> s = {}"
   333   by (simp add: components_def)
   334 
   335 lemma components_empty [simp]: "components {} = {}"
   336   by simp
   337 
   338 lemma connected_eq_connected_components_eq: "connected s \<longleftrightarrow> (\<forall>c \<in> components s. \<forall>c' \<in> components s. c = c')"
   339   by (metis (no_types, hide_lams) components_iff connected_component_eq_eq connected_iff_connected_component)
   340 
   341 lemma components_eq_sing_iff: "components s = {s} \<longleftrightarrow> connected s \<and> s \<noteq> {}"
   342   apply (rule iffI)
   343   using in_components_connected apply fastforce
   344   apply safe
   345   using Union_components apply fastforce
   346    apply (metis components_iff connected_component_eq_self)
   347   using in_components_maximal
   348   apply auto
   349   done
   350 
   351 lemma components_eq_sing_exists: "(\<exists>a. components s = {a}) \<longleftrightarrow> connected s \<and> s \<noteq> {}"
   352   apply (rule iffI)
   353   using connected_eq_connected_components_eq apply fastforce
   354   apply (metis components_eq_sing_iff)
   355   done
   356 
   357 lemma connected_eq_components_subset_sing: "connected s \<longleftrightarrow> components s \<subseteq> {s}"
   358   by (metis Union_components components_empty components_eq_sing_iff connected_empty insert_subset order_refl subset_singletonD)
   359 
   360 lemma connected_eq_components_subset_sing_exists: "connected s \<longleftrightarrow> (\<exists>a. components s \<subseteq> {a})"
   361   by (metis components_eq_sing_exists connected_eq_components_subset_sing empty_iff subset_iff subset_singletonD)
   362 
   363 lemma in_components_self: "s \<in> components s \<longleftrightarrow> connected s \<and> s \<noteq> {}"
   364   by (metis components_empty components_eq_sing_iff empty_iff in_components_connected insertI1)
   365 
   366 lemma components_maximal: "\<lbrakk>c \<in> components s; connected t; t \<subseteq> s; c \<inter> t \<noteq> {}\<rbrakk> \<Longrightarrow> t \<subseteq> c"
   367   apply (simp add: components_def ex_in_conv [symmetric], clarify)
   368   by (meson connected_component_def connected_component_trans)
   369 
   370 lemma exists_component_superset: "\<lbrakk>t \<subseteq> s; s \<noteq> {}; connected t\<rbrakk> \<Longrightarrow> \<exists>c. c \<in> components s \<and> t \<subseteq> c"
   371   apply (cases "t = {}", force)
   372   apply (metis components_def ex_in_conv connected_component_maximal contra_subsetD image_eqI)
   373   done
   374 
   375 lemma components_intermediate_subset: "\<lbrakk>s \<in> components u; s \<subseteq> t; t \<subseteq> u\<rbrakk> \<Longrightarrow> s \<in> components t"
   376   apply (auto simp: components_iff)
   377   apply (metis connected_component_eq_empty connected_component_intermediate_subset)
   378   done
   379 
   380 lemma in_components_unions_complement: "c \<in> components s \<Longrightarrow> s - c = \<Union>(components s - {c})"
   381   by (metis complement_connected_component_unions components_def components_iff)
   382 
   383 lemma connected_intermediate_closure:
   384   assumes cs: "connected s" and st: "s \<subseteq> t" and ts: "t \<subseteq> closure s"
   385   shows "connected t"
   386 proof (rule connectedI)
   387   fix A B
   388   assume A: "open A" and B: "open B" and Alap: "A \<inter> t \<noteq> {}" and Blap: "B \<inter> t \<noteq> {}"
   389     and disj: "A \<inter> B \<inter> t = {}" and cover: "t \<subseteq> A \<union> B"
   390   have disjs: "A \<inter> B \<inter> s = {}"
   391     using disj st by auto
   392   have "A \<inter> closure s \<noteq> {}"
   393     using Alap Int_absorb1 ts by blast
   394   then have Alaps: "A \<inter> s \<noteq> {}"
   395     by (simp add: A open_Int_closure_eq_empty)
   396   have "B \<inter> closure s \<noteq> {}"
   397     using Blap Int_absorb1 ts by blast
   398   then have Blaps: "B \<inter> s \<noteq> {}"
   399     by (simp add: B open_Int_closure_eq_empty)
   400   then show False
   401     using cs [unfolded connected_def] A B disjs Alaps Blaps cover st
   402     by blast
   403 qed
   404 
   405 lemma closedin_connected_component: "closedin (top_of_set s) (connected_component_set s x)"
   406 proof (cases "connected_component_set s x = {}")
   407   case True
   408   then show ?thesis
   409     by (metis closedin_empty)
   410 next
   411   case False
   412   then obtain y where y: "connected_component s x y"
   413     by blast
   414   have *: "connected_component_set s x \<subseteq> s \<inter> closure (connected_component_set s x)"
   415     by (auto simp: closure_def connected_component_in)
   416   have "connected_component s x y \<Longrightarrow> s \<inter> closure (connected_component_set s x) \<subseteq> connected_component_set s x"
   417     apply (rule connected_component_maximal, simp)
   418     using closure_subset connected_component_in apply fastforce
   419     using * connected_intermediate_closure apply blast+
   420     done
   421   with y * show ?thesis
   422     by (auto simp: closedin_closed)
   423 qed
   424 
   425 lemma closedin_component:
   426    "C \<in> components s \<Longrightarrow> closedin (top_of_set s) C"
   427   using closedin_connected_component componentsE by blast
   428 
   429 
   430 subsection%unimportant \<open>Proving a function is constant on a connected set
   431   by proving that a level set is open\<close>
   432 
   433 lemma continuous_levelset_openin_cases:
   434   fixes f :: "_ \<Rightarrow> 'b::t1_space"
   435   shows "connected s \<Longrightarrow> continuous_on s f \<Longrightarrow>
   436         openin (top_of_set s) {x \<in> s. f x = a}
   437         \<Longrightarrow> (\<forall>x \<in> s. f x \<noteq> a) \<or> (\<forall>x \<in> s. f x = a)"
   438   unfolding connected_clopen
   439   using continuous_closedin_preimage_constant by auto
   440 
   441 lemma continuous_levelset_openin:
   442   fixes f :: "_ \<Rightarrow> 'b::t1_space"
   443   shows "connected s \<Longrightarrow> continuous_on s f \<Longrightarrow>
   444         openin (top_of_set s) {x \<in> s. f x = a} \<Longrightarrow>
   445         (\<exists>x \<in> s. f x = a)  \<Longrightarrow> (\<forall>x \<in> s. f x = a)"
   446   using continuous_levelset_openin_cases[of s f ]
   447   by meson
   448 
   449 lemma continuous_levelset_open:
   450   fixes f :: "_ \<Rightarrow> 'b::t1_space"
   451   assumes "connected s"
   452     and "continuous_on s f"
   453     and "open {x \<in> s. f x = a}"
   454     and "\<exists>x \<in> s.  f x = a"
   455   shows "\<forall>x \<in> s. f x = a"
   456   using continuous_levelset_openin[OF assms(1,2), of a, unfolded openin_open]
   457   using assms (3,4)
   458   by fast
   459 
   460 
   461 subsection%unimportant \<open>Preservation of Connectedness\<close>
   462 
   463 lemma homeomorphic_connectedness:
   464   assumes "s homeomorphic t"
   465   shows "connected s \<longleftrightarrow> connected t"
   466 using assms unfolding homeomorphic_def homeomorphism_def by (metis connected_continuous_image)
   467 
   468 lemma connected_monotone_quotient_preimage:
   469   assumes "connected T"
   470       and contf: "continuous_on S f" and fim: "f ` S = T"
   471       and opT: "\<And>U. U \<subseteq> T
   472                  \<Longrightarrow> openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow>
   473                      openin (top_of_set T) U"
   474       and connT: "\<And>y. y \<in> T \<Longrightarrow> connected (S \<inter> f -` {y})"
   475     shows "connected S"
   476 proof (rule connectedI)
   477   fix U V
   478   assume "open U" and "open V" and "U \<inter> S \<noteq> {}" and "V \<inter> S \<noteq> {}"
   479     and "U \<inter> V \<inter> S = {}" and "S \<subseteq> U \<union> V"
   480   moreover
   481   have disjoint: "f ` (S \<inter> U) \<inter> f ` (S \<inter> V) = {}"
   482   proof -
   483     have False if "y \<in> f ` (S \<inter> U) \<inter> f ` (S \<inter> V)" for y
   484     proof -
   485       have "y \<in> T"
   486         using fim that by blast
   487       show ?thesis
   488         using connectedD [OF connT [OF \<open>y \<in> T\<close>] \<open>open U\<close> \<open>open V\<close>]
   489               \<open>S \<subseteq> U \<union> V\<close> \<open>U \<inter> V \<inter> S = {}\<close> that by fastforce
   490     qed
   491     then show ?thesis by blast
   492   qed
   493   ultimately have UU: "(S \<inter> f -` f ` (S \<inter> U)) = S \<inter> U" and VV: "(S \<inter> f -` f ` (S \<inter> V)) = S \<inter> V"
   494     by auto
   495   have opeU: "openin (top_of_set T) (f ` (S \<inter> U))"
   496     by (metis UU \<open>open U\<close> fim image_Int_subset le_inf_iff opT openin_open_Int)
   497   have opeV: "openin (top_of_set T) (f ` (S \<inter> V))"
   498     by (metis opT fim VV \<open>open V\<close> openin_open_Int image_Int_subset inf.bounded_iff)
   499   have "T \<subseteq> f ` (S \<inter> U) \<union> f ` (S \<inter> V)"
   500     using \<open>S \<subseteq> U \<union> V\<close> fim by auto
   501   then show False
   502     using \<open>connected T\<close> disjoint opeU opeV \<open>U \<inter> S \<noteq> {}\<close> \<open>V \<inter> S \<noteq> {}\<close>
   503     by (auto simp: connected_openin)
   504 qed
   505 
   506 lemma connected_open_monotone_preimage:
   507   assumes contf: "continuous_on S f" and fim: "f ` S = T"
   508     and ST: "\<And>C. openin (top_of_set S) C \<Longrightarrow> openin (top_of_set T) (f ` C)"
   509     and connT: "\<And>y. y \<in> T \<Longrightarrow> connected (S \<inter> f -` {y})"
   510     and "connected C" "C \<subseteq> T"
   511   shows "connected (S \<inter> f -` C)"
   512 proof -
   513   have contf': "continuous_on (S \<inter> f -` C) f"
   514     by (meson contf continuous_on_subset inf_le1)
   515   have eqC: "f ` (S \<inter> f -` C) = C"
   516     using \<open>C \<subseteq> T\<close> fim by blast
   517   show ?thesis
   518   proof (rule connected_monotone_quotient_preimage [OF \<open>connected C\<close> contf' eqC])
   519     show "connected (S \<inter> f -` C \<inter> f -` {y})" if "y \<in> C" for y
   520     proof -
   521       have "S \<inter> f -` C \<inter> f -` {y} = S \<inter> f -` {y}"
   522         using that by blast
   523       moreover have "connected (S \<inter> f -` {y})"
   524         using \<open>C \<subseteq> T\<close> connT that by blast
   525       ultimately show ?thesis
   526         by metis
   527     qed
   528     have "\<And>U. openin (top_of_set (S \<inter> f -` C)) U
   529                \<Longrightarrow> openin (top_of_set C) (f ` U)"
   530       using open_map_restrict [OF _ ST \<open>C \<subseteq> T\<close>] by metis
   531     then show "\<And>D. D \<subseteq> C
   532           \<Longrightarrow> openin (top_of_set (S \<inter> f -` C)) (S \<inter> f -` C \<inter> f -` D) =
   533               openin (top_of_set C) D"
   534       using open_map_imp_quotient_map [of "(S \<inter> f -` C)" f] contf' by (simp add: eqC)
   535   qed
   536 qed
   537 
   538 
   539 lemma connected_closed_monotone_preimage:
   540   assumes contf: "continuous_on S f" and fim: "f ` S = T"
   541     and ST: "\<And>C. closedin (top_of_set S) C \<Longrightarrow> closedin (top_of_set T) (f ` C)"
   542     and connT: "\<And>y. y \<in> T \<Longrightarrow> connected (S \<inter> f -` {y})"
   543     and "connected C" "C \<subseteq> T"
   544   shows "connected (S \<inter> f -` C)"
   545 proof -
   546   have contf': "continuous_on (S \<inter> f -` C) f"
   547     by (meson contf continuous_on_subset inf_le1)
   548   have eqC: "f ` (S \<inter> f -` C) = C"
   549     using \<open>C \<subseteq> T\<close> fim by blast
   550   show ?thesis
   551   proof (rule connected_monotone_quotient_preimage [OF \<open>connected C\<close> contf' eqC])
   552     show "connected (S \<inter> f -` C \<inter> f -` {y})" if "y \<in> C" for y
   553     proof -
   554       have "S \<inter> f -` C \<inter> f -` {y} = S \<inter> f -` {y}"
   555         using that by blast
   556       moreover have "connected (S \<inter> f -` {y})"
   557         using \<open>C \<subseteq> T\<close> connT that by blast
   558       ultimately show ?thesis
   559         by metis
   560     qed
   561     have "\<And>U. closedin (top_of_set (S \<inter> f -` C)) U
   562                \<Longrightarrow> closedin (top_of_set C) (f ` U)"
   563       using closed_map_restrict [OF _ ST \<open>C \<subseteq> T\<close>] by metis
   564     then show "\<And>D. D \<subseteq> C
   565           \<Longrightarrow> openin (top_of_set (S \<inter> f -` C)) (S \<inter> f -` C \<inter> f -` D) =
   566               openin (top_of_set C) D"
   567       using closed_map_imp_quotient_map [of "(S \<inter> f -` C)" f] contf' by (simp add: eqC)
   568   qed
   569 qed
   570 
   571 
   572 
   573 subsection\<open>A couple of lemmas about components (see Newman IV, 3.3 and 3.4)\<close>
   574 
   575 
   576 lemma connected_Un_clopen_in_complement:
   577   fixes S U :: "'a::metric_space set"
   578   assumes "connected S" "connected U" "S \<subseteq> U" 
   579       and opeT: "openin (top_of_set (U - S)) T" 
   580       and cloT: "closedin (top_of_set (U - S)) T"
   581     shows "connected (S \<union> T)"
   582 proof -
   583   have *: "\<lbrakk>\<And>x y. P x y \<longleftrightarrow> P y x; \<And>x y. P x y \<Longrightarrow> S \<subseteq> x \<or> S \<subseteq> y;
   584             \<And>x y. \<lbrakk>P x y; S \<subseteq> x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> \<not>(\<exists>x y. (P x y))" for P
   585     by metis
   586   show ?thesis
   587     unfolding connected_closedin_eq
   588   proof (rule *)
   589     fix H1 H2
   590     assume H: "closedin (top_of_set (S \<union> T)) H1 \<and> 
   591                closedin (top_of_set (S \<union> T)) H2 \<and>
   592                H1 \<union> H2 = S \<union> T \<and> H1 \<inter> H2 = {} \<and> H1 \<noteq> {} \<and> H2 \<noteq> {}"
   593     then have clo: "closedin (top_of_set S) (S \<inter> H1)"
   594                    "closedin (top_of_set S) (S \<inter> H2)"
   595       by (metis Un_upper1 closedin_closed_subset inf_commute)+
   596     have Seq: "S \<inter> (H1 \<union> H2) = S"
   597       by (simp add: H)
   598     have "S \<inter> ((S \<union> T) \<inter> H1) \<union> S \<inter> ((S \<union> T) \<inter> H2) = S"
   599       using Seq by auto
   600     moreover have "H1 \<inter> (S \<inter> ((S \<union> T) \<inter> H2)) = {}"
   601       using H by blast
   602     ultimately have "S \<inter> H1 = {} \<or> S \<inter> H2 = {}"
   603       by (metis (no_types) H Int_assoc \<open>S \<inter> (H1 \<union> H2) = S\<close> \<open>connected S\<close>
   604           clo Seq connected_closedin inf_bot_right inf_le1)
   605     then show "S \<subseteq> H1 \<or> S \<subseteq> H2"
   606       using H \<open>connected S\<close> unfolding connected_closedin by blast
   607   next
   608     fix H1 H2
   609     assume H: "closedin (top_of_set (S \<union> T)) H1 \<and>
   610                closedin (top_of_set (S \<union> T)) H2 \<and>
   611                H1 \<union> H2 = S \<union> T \<and> H1 \<inter> H2 = {} \<and> H1 \<noteq> {} \<and> H2 \<noteq> {}" 
   612        and "S \<subseteq> H1"
   613     then have H2T: "H2 \<subseteq> T"
   614       by auto
   615     have "T \<subseteq> U"
   616       using Diff_iff opeT openin_imp_subset by auto
   617     with \<open>S \<subseteq> U\<close> have Ueq: "U = (U - S) \<union> (S \<union> T)" 
   618       by auto
   619     have "openin (top_of_set ((U - S) \<union> (S \<union> T))) H2"
   620     proof (rule openin_subtopology_Un)
   621       show "openin (top_of_set (S \<union> T)) H2"
   622         using \<open>H2 \<subseteq> T\<close> apply (auto simp: openin_closedin_eq)
   623         by (metis Diff_Diff_Int Diff_disjoint Diff_partition Diff_subset H Int_absorb1 Un_Diff)
   624       then show "openin (top_of_set (U - S)) H2"
   625         by (meson H2T Un_upper2 opeT openin_subset_trans openin_trans)
   626     qed
   627     moreover have "closedin (top_of_set ((U - S) \<union> (S \<union> T))) H2"
   628     proof (rule closedin_subtopology_Un)
   629       show "closedin (top_of_set (U - S)) H2"
   630         using H H2T cloT closedin_subset_trans 
   631         by (blast intro: closedin_subtopology_Un closedin_trans)
   632     qed (simp add: H)
   633     ultimately
   634     have H2: "H2 = {} \<or> H2 = U"
   635       using Ueq \<open>connected U\<close> unfolding connected_clopen by metis   
   636     then have "H2 \<subseteq> S"
   637       by (metis Diff_partition H Un_Diff_cancel Un_subset_iff \<open>H2 \<subseteq> T\<close> assms(3) inf.orderE opeT openin_imp_subset)
   638     moreover have "T \<subseteq> H2 - S"
   639       by (metis (no_types) H2 H opeT openin_closedin_eq topspace_euclidean_subtopology)
   640     ultimately show False
   641       using H \<open>S \<subseteq> H1\<close> by blast
   642   qed blast
   643 qed
   644 
   645 
   646 proposition component_diff_connected:
   647   fixes S :: "'a::metric_space set"
   648   assumes "connected S" "connected U" "S \<subseteq> U" and C: "C \<in> components (U - S)"
   649   shows "connected(U - C)"
   650   using \<open>connected S\<close> unfolding connected_closedin_eq not_ex de_Morgan_conj
   651 proof clarify
   652   fix H3 H4 
   653   assume clo3: "closedin (top_of_set (U - C)) H3" 
   654     and clo4: "closedin (top_of_set (U - C)) H4" 
   655     and "H3 \<union> H4 = U - C" and "H3 \<inter> H4 = {}" and "H3 \<noteq> {}" and "H4 \<noteq> {}"
   656     and * [rule_format]:
   657     "\<forall>H1 H2. \<not> closedin (top_of_set S) H1 \<or>
   658                       \<not> closedin (top_of_set S) H2 \<or>
   659                       H1 \<union> H2 \<noteq> S \<or> H1 \<inter> H2 \<noteq> {} \<or> \<not> H1 \<noteq> {} \<or> \<not> H2 \<noteq> {}"
   660   then have "H3 \<subseteq> U-C" and ope3: "openin (top_of_set (U - C)) (U - C - H3)"
   661     and "H4 \<subseteq> U-C" and ope4: "openin (top_of_set (U - C)) (U - C - H4)"
   662     by (auto simp: closedin_def)
   663   have "C \<noteq> {}" "C \<subseteq> U-S" "connected C"
   664     using C in_components_nonempty in_components_subset in_components_maximal by blast+
   665   have cCH3: "connected (C \<union> H3)"
   666   proof (rule connected_Un_clopen_in_complement [OF \<open>connected C\<close> \<open>connected U\<close> _ _ clo3])
   667     show "openin (top_of_set (U - C)) H3"
   668       apply (simp add: openin_closedin_eq \<open>H3 \<subseteq> U - C\<close>)
   669       apply (simp add: closedin_subtopology)
   670       by (metis Diff_cancel Diff_triv Un_Diff clo4 \<open>H3 \<inter> H4 = {}\<close> \<open>H3 \<union> H4 = U - C\<close> closedin_closed inf_commute sup_bot.left_neutral)
   671   qed (use clo3 \<open>C \<subseteq> U - S\<close> in auto)
   672   have cCH4: "connected (C \<union> H4)"
   673   proof (rule connected_Un_clopen_in_complement [OF \<open>connected C\<close> \<open>connected U\<close> _ _ clo4])
   674     show "openin (top_of_set (U - C)) H4"
   675       apply (simp add: openin_closedin_eq \<open>H4 \<subseteq> U - C\<close>)
   676       apply (simp add: closedin_subtopology)
   677       by (metis Diff_cancel Int_commute Un_Diff Un_Diff_Int \<open>H3 \<inter> H4 = {}\<close> \<open>H3 \<union> H4 = U - C\<close> clo3 closedin_closed)
   678   qed (use clo4 \<open>C \<subseteq> U - S\<close> in auto)
   679   have "closedin (top_of_set S) (S \<inter> H3)" "closedin (top_of_set S) (S \<inter> H4)"
   680     using clo3 clo4 \<open>S \<subseteq> U\<close> \<open>C \<subseteq> U - S\<close> by (auto simp: closedin_closed)
   681   moreover have "S \<inter> H3 \<noteq> {}"      
   682     using components_maximal [OF C cCH3] \<open>C \<noteq> {}\<close> \<open>C \<subseteq> U - S\<close> \<open>H3 \<noteq> {}\<close> \<open>H3 \<subseteq> U - C\<close> by auto
   683   moreover have "S \<inter> H4 \<noteq> {}"
   684     using components_maximal [OF C cCH4] \<open>C \<noteq> {}\<close> \<open>C \<subseteq> U - S\<close> \<open>H4 \<noteq> {}\<close> \<open>H4 \<subseteq> U - C\<close> by auto
   685   ultimately show False
   686     using * [of "S \<inter> H3" "S \<inter> H4"] \<open>H3 \<inter> H4 = {}\<close> \<open>C \<subseteq> U - S\<close> \<open>H3 \<union> H4 = U - C\<close> \<open>S \<subseteq> U\<close> 
   687     by auto
   688 qed
   689 
   690 
   691 subsection%unimportant\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
   692 
   693 text\<open>Still missing: versions for a set that is smaller than R, or countable.\<close>
   694 
   695 lemma continuous_disconnected_range_constant:
   696   assumes S: "connected S"
   697       and conf: "continuous_on S f"
   698       and fim: "f ` S \<subseteq> t"
   699       and cct: "\<And>y. y \<in> t \<Longrightarrow> connected_component_set t y = {y}"
   700     shows "f constant_on S"
   701 proof (cases "S = {}")
   702   case True then show ?thesis
   703     by (simp add: constant_on_def)
   704 next
   705   case False
   706   { fix x assume "x \<in> S"
   707     then have "f ` S \<subseteq> {f x}"
   708     by (metis connected_continuous_image conf connected_component_maximal fim image_subset_iff rev_image_eqI S cct)
   709   }
   710   with False show ?thesis
   711     unfolding constant_on_def by blast
   712 qed
   713 
   714 
   715 text\<open>This proof requires the existence of two separate values of the range type.\<close>
   716 lemma finite_range_constant_imp_connected:
   717   assumes "\<And>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
   718               \<lbrakk>continuous_on S f; finite(f ` S)\<rbrakk> \<Longrightarrow> f constant_on S"
   719     shows "connected S"
   720 proof -
   721   { fix t u
   722     assume clt: "closedin (top_of_set S) t"
   723        and clu: "closedin (top_of_set S) u"
   724        and tue: "t \<inter> u = {}" and tus: "t \<union> u = S"
   725     have conif: "continuous_on S (\<lambda>x. if x \<in> t then 0 else 1)"
   726       apply (subst tus [symmetric])
   727       apply (rule continuous_on_cases_local)
   728       using clt clu tue
   729       apply (auto simp: tus continuous_on_const)
   730       done
   731     have fi: "finite ((\<lambda>x. if x \<in> t then 0 else 1) ` S)"
   732       by (rule finite_subset [of _ "{0,1}"]) auto
   733     have "t = {} \<or> u = {}"
   734       using assms [OF conif fi] tus [symmetric]
   735       by (auto simp: Ball_def constant_on_def) (metis IntI empty_iff one_neq_zero tue)
   736   }
   737   then show ?thesis
   738     by (simp add: connected_closedin_eq)
   739 qed
   740 
   741 end