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