src/HOL/Analysis/Connected.thy
author nipkow
Thu Dec 07 15:48:50 2017 +0100 (10 months ago)
changeset 67155 9e5b05d54f9d
parent 66953 826a5fd4d36c
child 67237 1fe0ec14a90a
permissions -rw-r--r--
canonical name
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
lp15@66827
     5
section \<open>Connected Components, Homeomorphisms, Baire property, etc.\<close>
lp15@66827
     6
lp15@66827
     7
theory Connected
lp15@66827
     8
imports Topology_Euclidean_Space
lp15@66827
     9
begin
lp15@66827
    10
lp15@66827
    11
subsection \<open>More properties of closed balls, spheres, etc.\<close>
lp15@66827
    12
lp15@66827
    13
lemma mem_interior_cball: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S)"
lp15@66827
    14
  apply (simp add: interior_def, safe)
lp15@66827
    15
  apply (force simp: open_contains_cball)
lp15@66827
    16
  apply (rule_tac x="ball x e" in exI)
lp15@66827
    17
  apply (simp add: subset_trans [OF ball_subset_cball])
lp15@66827
    18
  done
lp15@66827
    19
lp15@66827
    20
lemma islimpt_ball:
lp15@66827
    21
  fixes x y :: "'a::{real_normed_vector,perfect_space}"
lp15@66827
    22
  shows "y islimpt ball x e \<longleftrightarrow> 0 < e \<and> y \<in> cball x e"
lp15@66827
    23
  (is "?lhs \<longleftrightarrow> ?rhs")
lp15@66827
    24
proof
lp15@66827
    25
  show ?rhs if ?lhs
lp15@66827
    26
  proof
lp15@66827
    27
    {
lp15@66827
    28
      assume "e \<le> 0"
lp15@66827
    29
      then have *: "ball x e = {}"
lp15@66827
    30
        using ball_eq_empty[of x e] by auto
lp15@66827
    31
      have False using \<open>?lhs\<close>
lp15@66827
    32
        unfolding * using islimpt_EMPTY[of y] by auto
lp15@66827
    33
    }
lp15@66827
    34
    then show "e > 0" by (metis not_less)
lp15@66827
    35
    show "y \<in> cball x e"
lp15@66827
    36
      using closed_cball[of x e] islimpt_subset[of y "ball x e" "cball x e"]
lp15@66827
    37
        ball_subset_cball[of x e] \<open>?lhs\<close>
lp15@66827
    38
      unfolding closed_limpt by auto
lp15@66827
    39
  qed
lp15@66827
    40
  show ?lhs if ?rhs
lp15@66827
    41
  proof -
lp15@66827
    42
    from that have "e > 0" by auto
lp15@66827
    43
    {
lp15@66827
    44
      fix d :: real
lp15@66827
    45
      assume "d > 0"
lp15@66827
    46
      have "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
lp15@66827
    47
      proof (cases "d \<le> dist x y")
lp15@66827
    48
        case True
lp15@66827
    49
        then show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
lp15@66827
    50
        proof (cases "x = y")
lp15@66827
    51
          case True
lp15@66827
    52
          then have False
lp15@66827
    53
            using \<open>d \<le> dist x y\<close> \<open>d>0\<close> by auto
lp15@66827
    54
          then show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
lp15@66827
    55
            by auto
lp15@66827
    56
        next
lp15@66827
    57
          case False
lp15@66827
    58
          have "dist x (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) =
lp15@66827
    59
            norm (x - y + (d / (2 * norm (y - x))) *\<^sub>R (y - x))"
lp15@66827
    60
            unfolding mem_cball mem_ball dist_norm diff_diff_eq2 diff_add_eq[symmetric]
lp15@66827
    61
            by auto
lp15@66827
    62
          also have "\<dots> = \<bar>- 1 + d / (2 * norm (x - y))\<bar> * norm (x - y)"
lp15@66827
    63
            using scaleR_left_distrib[of "- 1" "d / (2 * norm (y - x))", symmetric, of "y - x"]
lp15@66827
    64
            unfolding scaleR_minus_left scaleR_one
lp15@66827
    65
            by (auto simp: norm_minus_commute)
lp15@66827
    66
          also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
lp15@66827
    67
            unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
lp15@66827
    68
            unfolding distrib_right using \<open>x\<noteq>y\<close>  by auto
lp15@66827
    69
          also have "\<dots> \<le> e - d/2" using \<open>d \<le> dist x y\<close> and \<open>d>0\<close> and \<open>?rhs\<close>
lp15@66827
    70
            by (auto simp: dist_norm)
lp15@66827
    71
          finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \<in> ball x e" using \<open>d>0\<close>
lp15@66827
    72
            by auto
lp15@66827
    73
          moreover
lp15@66827
    74
          have "(d / (2*dist y x)) *\<^sub>R (y - x) \<noteq> 0"
lp15@66827
    75
            using \<open>x\<noteq>y\<close>[unfolded dist_nz] \<open>d>0\<close> unfolding scaleR_eq_0_iff
lp15@66827
    76
            by (auto simp: dist_commute)
lp15@66827
    77
          moreover
lp15@66827
    78
          have "dist (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) y < d"
lp15@66827
    79
            unfolding dist_norm
lp15@66827
    80
            apply simp
lp15@66827
    81
            unfolding norm_minus_cancel
lp15@66827
    82
            using \<open>d > 0\<close> \<open>x\<noteq>y\<close>[unfolded dist_nz] dist_commute[of x y]
lp15@66827
    83
            unfolding dist_norm
lp15@66827
    84
            apply auto
lp15@66827
    85
            done
lp15@66827
    86
          ultimately show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
lp15@66827
    87
            apply (rule_tac x = "y - (d / (2*dist y x)) *\<^sub>R (y - x)" in bexI)
lp15@66827
    88
            apply auto
lp15@66827
    89
            done
lp15@66827
    90
        qed
lp15@66827
    91
      next
lp15@66827
    92
        case False
lp15@66827
    93
        then have "d > dist x y" by auto
lp15@66827
    94
        show "\<exists>x' \<in> ball x e. x' \<noteq> y \<and> dist x' y < d"
lp15@66827
    95
        proof (cases "x = y")
lp15@66827
    96
          case True
lp15@66827
    97
          obtain z where **: "z \<noteq> y" "dist z y < min e d"
lp15@66827
    98
            using perfect_choose_dist[of "min e d" y]
lp15@66827
    99
            using \<open>d > 0\<close> \<open>e>0\<close> by auto
lp15@66827
   100
          show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
lp15@66827
   101
            unfolding \<open>x = y\<close>
lp15@66827
   102
            using \<open>z \<noteq> y\<close> **
lp15@66827
   103
            apply (rule_tac x=z in bexI)
lp15@66827
   104
            apply (auto simp: dist_commute)
lp15@66827
   105
            done
lp15@66827
   106
        next
lp15@66827
   107
          case False
lp15@66827
   108
          then show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
lp15@66827
   109
            using \<open>d>0\<close> \<open>d > dist x y\<close> \<open>?rhs\<close>
lp15@66827
   110
            apply (rule_tac x=x in bexI, auto)
lp15@66827
   111
            done
lp15@66827
   112
        qed
lp15@66827
   113
      qed
lp15@66827
   114
    }
lp15@66827
   115
    then show ?thesis
lp15@66827
   116
      unfolding mem_cball islimpt_approachable mem_ball by auto
lp15@66827
   117
  qed
lp15@66827
   118
qed
lp15@66827
   119
lp15@66827
   120
lemma closure_ball_lemma:
lp15@66827
   121
  fixes x y :: "'a::real_normed_vector"
lp15@66827
   122
  assumes "x \<noteq> y"
lp15@66827
   123
  shows "y islimpt ball x (dist x y)"
lp15@66827
   124
proof (rule islimptI)
lp15@66827
   125
  fix T
lp15@66827
   126
  assume "y \<in> T" "open T"
lp15@66827
   127
  then obtain r where "0 < r" "\<forall>z. dist z y < r \<longrightarrow> z \<in> T"
lp15@66827
   128
    unfolding open_dist by fast
lp15@66827
   129
  (* choose point between x and y, within distance r of y. *)
lp15@66827
   130
  define k where "k = min 1 (r / (2 * dist x y))"
lp15@66827
   131
  define z where "z = y + scaleR k (x - y)"
lp15@66827
   132
  have z_def2: "z = x + scaleR (1 - k) (y - x)"
lp15@66827
   133
    unfolding z_def by (simp add: algebra_simps)
lp15@66827
   134
  have "dist z y < r"
lp15@66827
   135
    unfolding z_def k_def using \<open>0 < r\<close>
lp15@66827
   136
    by (simp add: dist_norm min_def)
lp15@66827
   137
  then have "z \<in> T"
lp15@66827
   138
    using \<open>\<forall>z. dist z y < r \<longrightarrow> z \<in> T\<close> by simp
lp15@66827
   139
  have "dist x z < dist x y"
lp15@66827
   140
    unfolding z_def2 dist_norm
lp15@66827
   141
    apply (simp add: norm_minus_commute)
lp15@66827
   142
    apply (simp only: dist_norm [symmetric])
lp15@66827
   143
    apply (subgoal_tac "\<bar>1 - k\<bar> * dist x y < 1 * dist x y", simp)
lp15@66827
   144
    apply (rule mult_strict_right_mono)
lp15@66827
   145
    apply (simp add: k_def \<open>0 < r\<close> \<open>x \<noteq> y\<close>)
lp15@66827
   146
    apply (simp add: \<open>x \<noteq> y\<close>)
lp15@66827
   147
    done
lp15@66827
   148
  then have "z \<in> ball x (dist x y)"
lp15@66827
   149
    by simp
lp15@66827
   150
  have "z \<noteq> y"
lp15@66827
   151
    unfolding z_def k_def using \<open>x \<noteq> y\<close> \<open>0 < r\<close>
lp15@66827
   152
    by (simp add: min_def)
lp15@66827
   153
  show "\<exists>z\<in>ball x (dist x y). z \<in> T \<and> z \<noteq> y"
lp15@66827
   154
    using \<open>z \<in> ball x (dist x y)\<close> \<open>z \<in> T\<close> \<open>z \<noteq> y\<close>
lp15@66827
   155
    by fast
lp15@66827
   156
qed
lp15@66827
   157
lp15@66827
   158
lemma closure_ball [simp]:
lp15@66827
   159
  fixes x :: "'a::real_normed_vector"
lp15@66827
   160
  shows "0 < e \<Longrightarrow> closure (ball x e) = cball x e"
lp15@66827
   161
  apply (rule equalityI)
lp15@66827
   162
  apply (rule closure_minimal)
lp15@66827
   163
  apply (rule ball_subset_cball)
lp15@66827
   164
  apply (rule closed_cball)
lp15@66827
   165
  apply (rule subsetI, rename_tac y)
lp15@66827
   166
  apply (simp add: le_less [where 'a=real])
lp15@66827
   167
  apply (erule disjE)
lp15@66827
   168
  apply (rule subsetD [OF closure_subset], simp)
lp15@66827
   169
  apply (simp add: closure_def, clarify)
lp15@66827
   170
  apply (rule closure_ball_lemma)
haftmann@66953
   171
  apply simp
lp15@66827
   172
  done
lp15@66827
   173
lp15@66827
   174
(* In a trivial vector space, this fails for e = 0. *)
lp15@66827
   175
lemma interior_cball [simp]:
lp15@66827
   176
  fixes x :: "'a::{real_normed_vector, perfect_space}"
lp15@66827
   177
  shows "interior (cball x e) = ball x e"
lp15@66827
   178
proof (cases "e \<ge> 0")
lp15@66827
   179
  case False note cs = this
lp15@66827
   180
  from cs have null: "ball x e = {}"
lp15@66827
   181
    using ball_empty[of e x] by auto
lp15@66827
   182
  moreover
lp15@66827
   183
  {
lp15@66827
   184
    fix y
lp15@66827
   185
    assume "y \<in> cball x e"
lp15@66827
   186
    then have False
lp15@66827
   187
      by (metis ball_eq_empty null cs dist_eq_0_iff dist_le_zero_iff empty_subsetI mem_cball subset_antisym subset_ball)
lp15@66827
   188
  }
lp15@66827
   189
  then have "cball x e = {}" by auto
lp15@66827
   190
  then have "interior (cball x e) = {}"
lp15@66827
   191
    using interior_empty by auto
lp15@66827
   192
  ultimately show ?thesis by blast
lp15@66827
   193
next
lp15@66827
   194
  case True note cs = this
lp15@66827
   195
  have "ball x e \<subseteq> cball x e"
lp15@66827
   196
    using ball_subset_cball by auto
lp15@66827
   197
  moreover
lp15@66827
   198
  {
lp15@66827
   199
    fix S y
lp15@66827
   200
    assume as: "S \<subseteq> cball x e" "open S" "y\<in>S"
lp15@66827
   201
    then obtain d where "d>0" and d: "\<forall>x'. dist x' y < d \<longrightarrow> x' \<in> S"
lp15@66827
   202
      unfolding open_dist by blast
lp15@66827
   203
    then obtain xa where xa_y: "xa \<noteq> y" and xa: "dist xa y < d"
lp15@66827
   204
      using perfect_choose_dist [of d] by auto
lp15@66827
   205
    have "xa \<in> S"
lp15@66827
   206
      using d[THEN spec[where x = xa]]
lp15@66827
   207
      using xa by (auto simp: dist_commute)
lp15@66827
   208
    then have xa_cball: "xa \<in> cball x e"
lp15@66827
   209
      using as(1) by auto
lp15@66827
   210
    then have "y \<in> ball x e"
lp15@66827
   211
    proof (cases "x = y")
lp15@66827
   212
      case True
lp15@66827
   213
      then have "e > 0" using cs order.order_iff_strict xa_cball xa_y by fastforce
lp15@66827
   214
      then show "y \<in> ball x e"
lp15@66827
   215
        using \<open>x = y \<close> by simp
lp15@66827
   216
    next
lp15@66827
   217
      case False
lp15@66827
   218
      have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) y < d"
lp15@66827
   219
        unfolding dist_norm
lp15@66827
   220
        using \<open>d>0\<close> norm_ge_zero[of "y - x"] \<open>x \<noteq> y\<close> by auto
lp15@66827
   221
      then have *: "y + (d / 2 / dist y x) *\<^sub>R (y - x) \<in> cball x e"
lp15@66827
   222
        using d as(1)[unfolded subset_eq] by blast
lp15@66827
   223
      have "y - x \<noteq> 0" using \<open>x \<noteq> y\<close> by auto
lp15@66827
   224
      hence **:"d / (2 * norm (y - x)) > 0"
lp15@66827
   225
        unfolding zero_less_norm_iff[symmetric] using \<open>d>0\<close> by auto
lp15@66827
   226
      have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) x =
lp15@66827
   227
        norm (y + (d / (2 * norm (y - x))) *\<^sub>R y - (d / (2 * norm (y - x))) *\<^sub>R x - x)"
lp15@66827
   228
        by (auto simp: dist_norm algebra_simps)
lp15@66827
   229
      also have "\<dots> = norm ((1 + d / (2 * norm (y - x))) *\<^sub>R (y - x))"
lp15@66827
   230
        by (auto simp: algebra_simps)
lp15@66827
   231
      also have "\<dots> = \<bar>1 + d / (2 * norm (y - x))\<bar> * norm (y - x)"
lp15@66827
   232
        using ** by auto
lp15@66827
   233
      also have "\<dots> = (dist y x) + d/2"
lp15@66827
   234
        using ** by (auto simp: distrib_right dist_norm)
lp15@66827
   235
      finally have "e \<ge> dist x y +d/2"
lp15@66827
   236
        using *[unfolded mem_cball] by (auto simp: dist_commute)
lp15@66827
   237
      then show "y \<in> ball x e"
lp15@66827
   238
        unfolding mem_ball using \<open>d>0\<close> by auto
lp15@66827
   239
    qed
lp15@66827
   240
  }
lp15@66827
   241
  then have "\<forall>S \<subseteq> cball x e. open S \<longrightarrow> S \<subseteq> ball x e"
lp15@66827
   242
    by auto
lp15@66827
   243
  ultimately show ?thesis
lp15@66827
   244
    using interior_unique[of "ball x e" "cball x e"]
lp15@66827
   245
    using open_ball[of x e]
lp15@66827
   246
    by auto
lp15@66827
   247
qed
lp15@66827
   248
lp15@66827
   249
lemma interior_ball [simp]: "interior (ball x e) = ball x e"
lp15@66827
   250
  by (simp add: interior_open)
lp15@66827
   251
lp15@66827
   252
lemma frontier_ball [simp]:
lp15@66827
   253
  fixes a :: "'a::real_normed_vector"
lp15@66827
   254
  shows "0 < e \<Longrightarrow> frontier (ball a e) = sphere a e"
lp15@66827
   255
  by (force simp: frontier_def)
lp15@66827
   256
lp15@66827
   257
lemma frontier_cball [simp]:
lp15@66827
   258
  fixes a :: "'a::{real_normed_vector, perfect_space}"
lp15@66827
   259
  shows "frontier (cball a e) = sphere a e"
lp15@66827
   260
  by (force simp: frontier_def)
lp15@66827
   261
lp15@66827
   262
lemma cball_eq_empty [simp]: "cball x e = {} \<longleftrightarrow> e < 0"
lp15@66827
   263
  apply (simp add: set_eq_iff not_le)
lp15@66827
   264
  apply (metis zero_le_dist dist_self order_less_le_trans)
lp15@66827
   265
  done
lp15@66827
   266
lp15@66827
   267
lemma cball_empty [simp]: "e < 0 \<Longrightarrow> cball x e = {}"
lp15@66827
   268
  by simp
lp15@66827
   269
lp15@66827
   270
lemma cball_eq_sing:
lp15@66827
   271
  fixes x :: "'a::{metric_space,perfect_space}"
lp15@66827
   272
  shows "cball x e = {x} \<longleftrightarrow> e = 0"
lp15@66827
   273
proof (rule linorder_cases)
lp15@66827
   274
  assume e: "0 < e"
lp15@66827
   275
  obtain a where "a \<noteq> x" "dist a x < e"
lp15@66827
   276
    using perfect_choose_dist [OF e] by auto
lp15@66827
   277
  then have "a \<noteq> x" "dist x a \<le> e"
lp15@66827
   278
    by (auto simp: dist_commute)
lp15@66827
   279
  with e show ?thesis by (auto simp: set_eq_iff)
lp15@66827
   280
qed auto
lp15@66827
   281
lp15@66827
   282
lemma cball_sing:
lp15@66827
   283
  fixes x :: "'a::metric_space"
lp15@66827
   284
  shows "e = 0 \<Longrightarrow> cball x e = {x}"
lp15@66827
   285
  by (auto simp: set_eq_iff)
lp15@66827
   286
lp15@66827
   287
lemma ball_divide_subset: "d \<ge> 1 \<Longrightarrow> ball x (e/d) \<subseteq> ball x e"
lp15@66827
   288
  apply (cases "e \<le> 0")
lp15@66827
   289
  apply (simp add: ball_empty divide_simps)
lp15@66827
   290
  apply (rule subset_ball)
lp15@66827
   291
  apply (simp add: divide_simps)
lp15@66827
   292
  done
lp15@66827
   293
lp15@66827
   294
lemma ball_divide_subset_numeral: "ball x (e / numeral w) \<subseteq> ball x e"
lp15@66827
   295
  using ball_divide_subset one_le_numeral by blast
lp15@66827
   296
lp15@66827
   297
lemma cball_divide_subset: "d \<ge> 1 \<Longrightarrow> cball x (e/d) \<subseteq> cball x e"
lp15@66827
   298
  apply (cases "e < 0")
lp15@66827
   299
  apply (simp add: divide_simps)
lp15@66827
   300
  apply (rule subset_cball)
lp15@66827
   301
  apply (metis div_by_1 frac_le not_le order_refl zero_less_one)
lp15@66827
   302
  done
lp15@66827
   303
lp15@66827
   304
lemma cball_divide_subset_numeral: "cball x (e / numeral w) \<subseteq> cball x e"
lp15@66827
   305
  using cball_divide_subset one_le_numeral by blast
lp15@66827
   306
lp15@66827
   307
lemma compact_cball[simp]:
lp15@66827
   308
  fixes x :: "'a::heine_borel"
lp15@66827
   309
  shows "compact (cball x e)"
lp15@66827
   310
  using compact_eq_bounded_closed bounded_cball closed_cball
lp15@66827
   311
  by blast
lp15@66827
   312
lp15@66827
   313
lemma compact_frontier_bounded[intro]:
lp15@66827
   314
  fixes S :: "'a::heine_borel set"
lp15@66827
   315
  shows "bounded S \<Longrightarrow> compact (frontier S)"
lp15@66827
   316
  unfolding frontier_def
lp15@66827
   317
  using compact_eq_bounded_closed
lp15@66827
   318
  by blast
lp15@66827
   319
lp15@66827
   320
lemma compact_frontier[intro]:
lp15@66827
   321
  fixes S :: "'a::heine_borel set"
lp15@66827
   322
  shows "compact S \<Longrightarrow> compact (frontier S)"
lp15@66827
   323
  using compact_eq_bounded_closed compact_frontier_bounded
lp15@66827
   324
  by blast
lp15@66827
   325
lp15@66827
   326
corollary compact_sphere [simp]:
lp15@66827
   327
  fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"
lp15@66827
   328
  shows "compact (sphere a r)"
lp15@66827
   329
using compact_frontier [of "cball a r"] by simp
lp15@66827
   330
lp15@66827
   331
corollary bounded_sphere [simp]:
lp15@66827
   332
  fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"
lp15@66827
   333
  shows "bounded (sphere a r)"
lp15@66827
   334
by (simp add: compact_imp_bounded)
lp15@66827
   335
lp15@66827
   336
corollary closed_sphere  [simp]:
lp15@66827
   337
  fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"
lp15@66827
   338
  shows "closed (sphere a r)"
lp15@66827
   339
by (simp add: compact_imp_closed)
lp15@66827
   340
lp15@66827
   341
subsection \<open>Connectedness\<close>
lp15@66827
   342
lp15@66827
   343
lemma connected_local:
lp15@66827
   344
 "connected S \<longleftrightarrow>
lp15@66827
   345
  \<not> (\<exists>e1 e2.
lp15@66827
   346
      openin (subtopology euclidean S) e1 \<and>
lp15@66827
   347
      openin (subtopology euclidean S) e2 \<and>
lp15@66827
   348
      S \<subseteq> e1 \<union> e2 \<and>
lp15@66827
   349
      e1 \<inter> e2 = {} \<and>
lp15@66827
   350
      e1 \<noteq> {} \<and>
lp15@66827
   351
      e2 \<noteq> {})"
lp15@66827
   352
  unfolding connected_def openin_open
lp15@66827
   353
  by safe blast+
lp15@66827
   354
lp15@66827
   355
lemma exists_diff:
lp15@66827
   356
  fixes P :: "'a set \<Rightarrow> bool"
lp15@66827
   357
  shows "(\<exists>S. P (- S)) \<longleftrightarrow> (\<exists>S. P S)"
lp15@66827
   358
    (is "?lhs \<longleftrightarrow> ?rhs")
lp15@66827
   359
proof -
lp15@66827
   360
  have ?rhs if ?lhs
lp15@66827
   361
    using that by blast
lp15@66827
   362
  moreover have "P (- (- S))" if "P S" for S
lp15@66827
   363
  proof -
lp15@66827
   364
    have "S = - (- S)" by simp
lp15@66827
   365
    with that show ?thesis by metis
lp15@66827
   366
  qed
lp15@66827
   367
  ultimately show ?thesis by metis
lp15@66827
   368
qed
lp15@66827
   369
lp15@66827
   370
lemma connected_clopen: "connected S \<longleftrightarrow>
lp15@66827
   371
  (\<forall>T. openin (subtopology euclidean S) T \<and>
lp15@66827
   372
     closedin (subtopology euclidean S) T \<longrightarrow> T = {} \<or> T = S)" (is "?lhs \<longleftrightarrow> ?rhs")
lp15@66827
   373
proof -
lp15@66827
   374
  have "\<not> connected S \<longleftrightarrow>
lp15@66827
   375
    (\<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
   376
    unfolding connected_def openin_open closedin_closed
lp15@66827
   377
    by (metis double_complement)
lp15@66827
   378
  then have th0: "connected S \<longleftrightarrow>
lp15@66827
   379
    \<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
   380
    (is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)")
lp15@66827
   381
    by (simp add: closed_def) metis
lp15@66827
   382
  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
   383
    (is "_ \<longleftrightarrow> \<not> (\<exists>t' t. ?Q t' t)")
lp15@66827
   384
    unfolding connected_def openin_open closedin_closed by auto
lp15@66827
   385
  have "(\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)" for e2
lp15@66827
   386
  proof -
lp15@66827
   387
    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
   388
      by auto
lp15@66827
   389
    then show ?thesis
lp15@66827
   390
      by metis
lp15@66827
   391
  qed
lp15@66827
   392
  then have "\<forall>e2. (\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)"
lp15@66827
   393
    by blast
lp15@66827
   394
  then show ?thesis
lp15@66827
   395
    by (simp add: th0 th1)
lp15@66827
   396
qed
lp15@66827
   397
lp15@66827
   398
lemma connected_linear_image:
lp15@66827
   399
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
lp15@66827
   400
  assumes "linear f" and "connected s"
lp15@66827
   401
  shows "connected (f ` s)"
lp15@66827
   402
using connected_continuous_image assms linear_continuous_on linear_conv_bounded_linear by blast
lp15@66827
   403
lp15@66827
   404
subsection \<open>Connected components, considered as a connectedness relation or a set\<close>
lp15@66827
   405
lp15@66827
   406
definition "connected_component s x y \<equiv> \<exists>t. connected t \<and> t \<subseteq> s \<and> x \<in> t \<and> y \<in> t"
lp15@66827
   407
lp15@66827
   408
abbreviation "connected_component_set s x \<equiv> Collect (connected_component s x)"
lp15@66827
   409
lp15@66827
   410
lemma connected_componentI:
lp15@66827
   411
  "connected t \<Longrightarrow> t \<subseteq> s \<Longrightarrow> x \<in> t \<Longrightarrow> y \<in> t \<Longrightarrow> connected_component s x y"
lp15@66827
   412
  by (auto simp: connected_component_def)
lp15@66827
   413
lp15@66827
   414
lemma connected_component_in: "connected_component s x y \<Longrightarrow> x \<in> s \<and> y \<in> s"
lp15@66827
   415
  by (auto simp: connected_component_def)
lp15@66827
   416
lp15@66827
   417
lemma connected_component_refl: "x \<in> s \<Longrightarrow> connected_component s x x"
lp15@66827
   418
  by (auto simp: connected_component_def) (use connected_sing in blast)
lp15@66827
   419
lp15@66827
   420
lemma connected_component_refl_eq [simp]: "connected_component s x x \<longleftrightarrow> x \<in> s"
lp15@66827
   421
  by (auto simp: connected_component_refl) (auto simp: connected_component_def)
lp15@66827
   422
lp15@66827
   423
lemma connected_component_sym: "connected_component s x y \<Longrightarrow> connected_component s y x"
lp15@66827
   424
  by (auto simp: connected_component_def)
lp15@66827
   425
lp15@66827
   426
lemma connected_component_trans:
lp15@66827
   427
  "connected_component s x y \<Longrightarrow> connected_component s y z \<Longrightarrow> connected_component s x z"
lp15@66827
   428
  unfolding connected_component_def
lp15@66827
   429
  by (metis Int_iff Un_iff Un_subset_iff equals0D connected_Un)
lp15@66827
   430
lp15@66827
   431
lemma connected_component_of_subset:
lp15@66827
   432
  "connected_component s x y \<Longrightarrow> s \<subseteq> t \<Longrightarrow> connected_component t x y"
lp15@66827
   433
  by (auto simp: connected_component_def)
lp15@66827
   434
lp15@66827
   435
lemma connected_component_Union: "connected_component_set s x = \<Union>{t. connected t \<and> x \<in> t \<and> t \<subseteq> s}"
lp15@66827
   436
  by (auto simp: connected_component_def)
lp15@66827
   437
lp15@66827
   438
lemma connected_connected_component [iff]: "connected (connected_component_set s x)"
lp15@66827
   439
  by (auto simp: connected_component_Union intro: connected_Union)
lp15@66827
   440
lp15@66827
   441
lemma connected_iff_eq_connected_component_set:
lp15@66827
   442
  "connected s \<longleftrightarrow> (\<forall>x \<in> s. connected_component_set s x = s)"
lp15@66827
   443
proof (cases "s = {}")
lp15@66827
   444
  case True
lp15@66827
   445
  then show ?thesis by simp
lp15@66827
   446
next
lp15@66827
   447
  case False
lp15@66827
   448
  then obtain x where "x \<in> s" by auto
lp15@66827
   449
  show ?thesis
lp15@66827
   450
  proof
lp15@66827
   451
    assume "connected s"
lp15@66827
   452
    then show "\<forall>x \<in> s. connected_component_set s x = s"
lp15@66827
   453
      by (force simp: connected_component_def)
lp15@66827
   454
  next
lp15@66827
   455
    assume "\<forall>x \<in> s. connected_component_set s x = s"
lp15@66827
   456
    then show "connected s"
lp15@66827
   457
      by (metis \<open>x \<in> s\<close> connected_connected_component)
lp15@66827
   458
  qed
lp15@66827
   459
qed
lp15@66827
   460
lp15@66827
   461
lemma connected_component_subset: "connected_component_set s x \<subseteq> s"
lp15@66827
   462
  using connected_component_in by blast
lp15@66827
   463
lp15@66827
   464
lemma connected_component_eq_self: "connected s \<Longrightarrow> x \<in> s \<Longrightarrow> connected_component_set s x = s"
lp15@66827
   465
  by (simp add: connected_iff_eq_connected_component_set)
lp15@66827
   466
lp15@66827
   467
lemma connected_iff_connected_component:
lp15@66827
   468
  "connected s \<longleftrightarrow> (\<forall>x \<in> s. \<forall>y \<in> s. connected_component s x y)"
lp15@66827
   469
  using connected_component_in by (auto simp: connected_iff_eq_connected_component_set)
lp15@66827
   470
lp15@66827
   471
lemma connected_component_maximal:
lp15@66827
   472
  "x \<in> t \<Longrightarrow> connected t \<Longrightarrow> t \<subseteq> s \<Longrightarrow> t \<subseteq> (connected_component_set s x)"
lp15@66827
   473
  using connected_component_eq_self connected_component_of_subset by blast
lp15@66827
   474
lp15@66827
   475
lemma connected_component_mono:
lp15@66827
   476
  "s \<subseteq> t \<Longrightarrow> connected_component_set s x \<subseteq> connected_component_set t x"
lp15@66827
   477
  by (simp add: Collect_mono connected_component_of_subset)
lp15@66827
   478
lp15@66827
   479
lemma connected_component_eq_empty [simp]: "connected_component_set s x = {} \<longleftrightarrow> x \<notin> s"
lp15@66827
   480
  using connected_component_refl by (fastforce simp: connected_component_in)
lp15@66827
   481
lp15@66827
   482
lemma connected_component_set_empty [simp]: "connected_component_set {} x = {}"
lp15@66827
   483
  using connected_component_eq_empty by blast
lp15@66827
   484
lp15@66827
   485
lemma connected_component_eq:
lp15@66827
   486
  "y \<in> connected_component_set s x \<Longrightarrow> (connected_component_set s y = connected_component_set s x)"
lp15@66827
   487
  by (metis (no_types, lifting)
lp15@66827
   488
      Collect_cong connected_component_sym connected_component_trans mem_Collect_eq)
lp15@66827
   489
lp15@66827
   490
lemma closed_connected_component:
lp15@66827
   491
  assumes s: "closed s"
lp15@66827
   492
  shows "closed (connected_component_set s x)"
lp15@66827
   493
proof (cases "x \<in> s")
lp15@66827
   494
  case False
lp15@66827
   495
  then show ?thesis
lp15@66827
   496
    by (metis connected_component_eq_empty closed_empty)
lp15@66827
   497
next
lp15@66827
   498
  case True
lp15@66827
   499
  show ?thesis
lp15@66827
   500
    unfolding closure_eq [symmetric]
lp15@66827
   501
  proof
lp15@66827
   502
    show "closure (connected_component_set s x) \<subseteq> connected_component_set s x"
lp15@66827
   503
      apply (rule connected_component_maximal)
lp15@66827
   504
        apply (simp add: closure_def True)
lp15@66827
   505
       apply (simp add: connected_imp_connected_closure)
lp15@66827
   506
      apply (simp add: s closure_minimal connected_component_subset)
lp15@66827
   507
      done
lp15@66827
   508
  next
lp15@66827
   509
    show "connected_component_set s x \<subseteq> closure (connected_component_set s x)"
lp15@66827
   510
      by (simp add: closure_subset)
lp15@66827
   511
  qed
lp15@66827
   512
qed
lp15@66827
   513
lp15@66827
   514
lemma connected_component_disjoint:
lp15@66827
   515
  "connected_component_set s a \<inter> connected_component_set s b = {} \<longleftrightarrow>
lp15@66827
   516
    a \<notin> connected_component_set s b"
lp15@66827
   517
  apply (auto simp: connected_component_eq)
lp15@66827
   518
  using connected_component_eq connected_component_sym
lp15@66827
   519
  apply blast
lp15@66827
   520
  done
lp15@66827
   521
lp15@66827
   522
lemma connected_component_nonoverlap:
lp15@66827
   523
  "connected_component_set s a \<inter> connected_component_set s b = {} \<longleftrightarrow>
lp15@66827
   524
    a \<notin> s \<or> b \<notin> s \<or> connected_component_set s a \<noteq> connected_component_set s b"
lp15@66827
   525
  apply (auto simp: connected_component_in)
lp15@66827
   526
  using connected_component_refl_eq
lp15@66827
   527
    apply blast
lp15@66827
   528
   apply (metis connected_component_eq mem_Collect_eq)
lp15@66827
   529
  apply (metis connected_component_eq mem_Collect_eq)
lp15@66827
   530
  done
lp15@66827
   531
lp15@66827
   532
lemma connected_component_overlap:
lp15@66827
   533
  "connected_component_set s a \<inter> connected_component_set s b \<noteq> {} \<longleftrightarrow>
lp15@66827
   534
    a \<in> s \<and> b \<in> s \<and> connected_component_set s a = connected_component_set s b"
lp15@66827
   535
  by (auto simp: connected_component_nonoverlap)
lp15@66827
   536
lp15@66827
   537
lemma connected_component_sym_eq: "connected_component s x y \<longleftrightarrow> connected_component s y x"
lp15@66827
   538
  using connected_component_sym by blast
lp15@66827
   539
lp15@66827
   540
lemma connected_component_eq_eq:
lp15@66827
   541
  "connected_component_set s x = connected_component_set s y \<longleftrightarrow>
lp15@66827
   542
    x \<notin> s \<and> y \<notin> s \<or> x \<in> s \<and> y \<in> s \<and> connected_component s x y"
lp15@66827
   543
  apply (cases "y \<in> s", simp)
lp15@66827
   544
   apply (metis connected_component_eq connected_component_eq_empty connected_component_refl_eq mem_Collect_eq)
lp15@66827
   545
  apply (cases "x \<in> s", simp)
lp15@66827
   546
   apply (metis connected_component_eq_empty)
lp15@66827
   547
  using connected_component_eq_empty
lp15@66827
   548
  apply blast
lp15@66827
   549
  done
lp15@66827
   550
lp15@66827
   551
lemma connected_iff_connected_component_eq:
lp15@66827
   552
  "connected s \<longleftrightarrow> (\<forall>x \<in> s. \<forall>y \<in> s. connected_component_set s x = connected_component_set s y)"
lp15@66827
   553
  by (simp add: connected_component_eq_eq connected_iff_connected_component)
lp15@66827
   554
lp15@66827
   555
lemma connected_component_idemp:
lp15@66827
   556
  "connected_component_set (connected_component_set s x) x = connected_component_set s x"
lp15@66827
   557
  apply (rule subset_antisym)
lp15@66827
   558
   apply (simp add: connected_component_subset)
lp15@66827
   559
  apply (metis connected_component_eq_empty connected_component_maximal
lp15@66827
   560
      connected_component_refl_eq connected_connected_component mem_Collect_eq set_eq_subset)
lp15@66827
   561
  done
lp15@66827
   562
lp15@66827
   563
lemma connected_component_unique:
lp15@66827
   564
  "\<lbrakk>x \<in> c; c \<subseteq> s; connected c;
lp15@66827
   565
    \<And>c'. x \<in> c' \<and> c' \<subseteq> s \<and> connected c'
lp15@66827
   566
              \<Longrightarrow> c' \<subseteq> c\<rbrakk>
lp15@66827
   567
        \<Longrightarrow> connected_component_set s x = c"
lp15@66827
   568
apply (rule subset_antisym)
lp15@66827
   569
apply (meson connected_component_maximal connected_component_subset connected_connected_component contra_subsetD)
lp15@66827
   570
by (simp add: connected_component_maximal)
lp15@66827
   571
lp15@66827
   572
lemma joinable_connected_component_eq:
lp15@66827
   573
  "\<lbrakk>connected t; t \<subseteq> s;
lp15@66827
   574
    connected_component_set s x \<inter> t \<noteq> {};
lp15@66827
   575
    connected_component_set s y \<inter> t \<noteq> {}\<rbrakk>
lp15@66827
   576
    \<Longrightarrow> connected_component_set s x = connected_component_set s y"
lp15@66827
   577
apply (simp add: ex_in_conv [symmetric])
lp15@66827
   578
apply (rule connected_component_eq)
lp15@66827
   579
by (metis (no_types, hide_lams) connected_component_eq_eq connected_component_in connected_component_maximal subsetD mem_Collect_eq)
lp15@66827
   580
lp15@66827
   581
lp15@66827
   582
lemma Union_connected_component: "\<Union>(connected_component_set s ` s) = s"
lp15@66827
   583
  apply (rule subset_antisym)
lp15@66827
   584
  apply (simp add: SUP_least connected_component_subset)
lp15@66827
   585
  using connected_component_refl_eq
lp15@66827
   586
  by force
lp15@66827
   587
lp15@66827
   588
lp15@66827
   589
lemma complement_connected_component_unions:
lp15@66827
   590
    "s - connected_component_set s x =
lp15@66827
   591
     \<Union>(connected_component_set s ` s - {connected_component_set s x})"
lp15@66827
   592
  apply (subst Union_connected_component [symmetric], auto)
lp15@66827
   593
  apply (metis connected_component_eq_eq connected_component_in)
lp15@66827
   594
  by (metis connected_component_eq mem_Collect_eq)
lp15@66827
   595
lp15@66827
   596
lemma connected_component_intermediate_subset:
lp15@66827
   597
        "\<lbrakk>connected_component_set u a \<subseteq> t; t \<subseteq> u\<rbrakk>
lp15@66827
   598
        \<Longrightarrow> connected_component_set t a = connected_component_set u a"
lp15@66827
   599
  apply (case_tac "a \<in> u")
lp15@66827
   600
  apply (simp add: connected_component_maximal connected_component_mono subset_antisym)
lp15@66827
   601
  using connected_component_eq_empty by blast
lp15@66827
   602
lp15@66827
   603
proposition connected_Times:
lp15@66827
   604
  assumes S: "connected S" and T: "connected T"
lp15@66827
   605
  shows "connected (S \<times> T)"
lp15@66827
   606
proof (clarsimp simp add: connected_iff_connected_component)
lp15@66827
   607
  fix x y x' y'
lp15@66827
   608
  assume xy: "x \<in> S" "y \<in> T" "x' \<in> S" "y' \<in> T"
lp15@66827
   609
  with xy obtain U V where U: "connected U" "U \<subseteq> S" "x \<in> U" "x' \<in> U"
lp15@66827
   610
                       and V: "connected V" "V \<subseteq> T" "y \<in> V" "y' \<in> V"
lp15@66827
   611
    using S T \<open>x \<in> S\<close> \<open>x' \<in> S\<close> by blast+
lp15@66827
   612
  show "connected_component (S \<times> T) (x, y) (x', y')"
lp15@66827
   613
    unfolding connected_component_def
lp15@66827
   614
  proof (intro exI conjI)
lp15@66827
   615
    show "connected ((\<lambda>x. (x, y)) ` U \<union> Pair x' ` V)"
lp15@66827
   616
    proof (rule connected_Un)
lp15@66827
   617
      have "continuous_on U (\<lambda>x. (x, y))"
lp15@66827
   618
        by (intro continuous_intros)
lp15@66827
   619
      then show "connected ((\<lambda>x. (x, y)) ` U)"
lp15@66827
   620
        by (rule connected_continuous_image) (rule \<open>connected U\<close>)
lp15@66827
   621
      have "continuous_on V (Pair x')"
lp15@66827
   622
        by (intro continuous_intros)
lp15@66827
   623
      then show "connected (Pair x' ` V)"
lp15@66827
   624
        by (rule connected_continuous_image) (rule \<open>connected V\<close>)
lp15@66827
   625
    qed (use U V in auto)
lp15@66827
   626
  qed (use U V in auto)
lp15@66827
   627
qed
lp15@66827
   628
lp15@66827
   629
corollary connected_Times_eq [simp]:
lp15@66827
   630
   "connected (S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> connected S \<and> connected T"  (is "?lhs = ?rhs")
lp15@66827
   631
proof
lp15@66827
   632
  assume L: ?lhs
lp15@66827
   633
  show ?rhs
lp15@66827
   634
  proof (cases "S = {} \<or> T = {}")
lp15@66827
   635
    case True
lp15@66827
   636
    then show ?thesis by auto
lp15@66827
   637
  next
lp15@66827
   638
    case False
lp15@66827
   639
    have "connected (fst ` (S \<times> T))" "connected (snd ` (S \<times> T))"
lp15@66827
   640
      using continuous_on_fst continuous_on_snd continuous_on_id
lp15@66827
   641
      by (blast intro: connected_continuous_image [OF _ L])+
lp15@66827
   642
    with False show ?thesis
lp15@66827
   643
      by auto
lp15@66827
   644
  qed
lp15@66827
   645
next
lp15@66827
   646
  assume ?rhs
lp15@66827
   647
  then show ?lhs
lp15@66827
   648
    by (auto simp: connected_Times)
lp15@66827
   649
qed
lp15@66827
   650
lp15@66827
   651
lp15@66827
   652
subsection \<open>The set of connected components of a set\<close>
lp15@66827
   653
lp15@66827
   654
definition components:: "'a::topological_space set \<Rightarrow> 'a set set"
lp15@66827
   655
  where "components s \<equiv> connected_component_set s ` s"
lp15@66827
   656
lp15@66827
   657
lemma components_iff: "s \<in> components u \<longleftrightarrow> (\<exists>x. x \<in> u \<and> s = connected_component_set u x)"
lp15@66827
   658
  by (auto simp: components_def)
lp15@66827
   659
lp15@66827
   660
lemma componentsI: "x \<in> u \<Longrightarrow> connected_component_set u x \<in> components u"
lp15@66827
   661
  by (auto simp: components_def)
lp15@66827
   662
lp15@66827
   663
lemma componentsE:
lp15@66827
   664
  assumes "s \<in> components u"
lp15@66827
   665
  obtains x where "x \<in> u" "s = connected_component_set u x"
lp15@66827
   666
  using assms by (auto simp: components_def)
lp15@66827
   667
lp15@66827
   668
lemma Union_components [simp]: "\<Union>(components u) = u"
lp15@66827
   669
  apply (rule subset_antisym)
lp15@66827
   670
  using Union_connected_component components_def apply fastforce
lp15@66827
   671
  apply (metis Union_connected_component components_def set_eq_subset)
lp15@66827
   672
  done
lp15@66827
   673
lp15@66827
   674
lemma pairwise_disjoint_components: "pairwise (\<lambda>X Y. X \<inter> Y = {}) (components u)"
lp15@66827
   675
  apply (simp add: pairwise_def)
lp15@66827
   676
  apply (auto simp: components_iff)
lp15@66827
   677
  apply (metis connected_component_eq_eq connected_component_in)+
lp15@66827
   678
  done
lp15@66827
   679
lp15@66827
   680
lemma in_components_nonempty: "c \<in> components s \<Longrightarrow> c \<noteq> {}"
lp15@66827
   681
    by (metis components_iff connected_component_eq_empty)
lp15@66827
   682
lp15@66827
   683
lemma in_components_subset: "c \<in> components s \<Longrightarrow> c \<subseteq> s"
lp15@66827
   684
  using Union_components by blast
lp15@66827
   685
lp15@66827
   686
lemma in_components_connected: "c \<in> components s \<Longrightarrow> connected c"
lp15@66827
   687
  by (metis components_iff connected_connected_component)
lp15@66827
   688
lp15@66827
   689
lemma in_components_maximal:
lp15@66827
   690
  "c \<in> components s \<longleftrightarrow>
lp15@66827
   691
    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
   692
  apply (rule iffI)
lp15@66827
   693
   apply (simp add: in_components_nonempty in_components_connected)
lp15@66827
   694
   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
   695
  apply (metis bot.extremum_uniqueI components_iff connected_component_eq_empty connected_component_maximal connected_component_subset connected_connected_component subset_emptyI)
lp15@66827
   696
  done
lp15@66827
   697
lp15@66827
   698
lemma joinable_components_eq:
lp15@66827
   699
  "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
   700
  by (metis (full_types) components_iff joinable_connected_component_eq)
lp15@66827
   701
lp15@66827
   702
lemma closed_components: "\<lbrakk>closed s; c \<in> components s\<rbrakk> \<Longrightarrow> closed c"
lp15@66827
   703
  by (metis closed_connected_component components_iff)
lp15@66827
   704
lp15@66827
   705
lemma compact_components:
lp15@66827
   706
  fixes s :: "'a::heine_borel set"
lp15@66827
   707
  shows "\<lbrakk>compact s; c \<in> components s\<rbrakk> \<Longrightarrow> compact c"
lp15@66827
   708
by (meson bounded_subset closed_components in_components_subset compact_eq_bounded_closed)
lp15@66827
   709
lp15@66827
   710
lemma components_nonoverlap:
lp15@66827
   711
    "\<lbrakk>c \<in> components s; c' \<in> components s\<rbrakk> \<Longrightarrow> (c \<inter> c' = {}) \<longleftrightarrow> (c \<noteq> c')"
lp15@66827
   712
  apply (auto simp: in_components_nonempty components_iff)
lp15@66827
   713
    using connected_component_refl apply blast
lp15@66827
   714
   apply (metis connected_component_eq_eq connected_component_in)
lp15@66827
   715
  by (metis connected_component_eq mem_Collect_eq)
lp15@66827
   716
lp15@66827
   717
lemma components_eq: "\<lbrakk>c \<in> components s; c' \<in> components s\<rbrakk> \<Longrightarrow> (c = c' \<longleftrightarrow> c \<inter> c' \<noteq> {})"
lp15@66827
   718
  by (metis components_nonoverlap)
lp15@66827
   719
lp15@66827
   720
lemma components_eq_empty [simp]: "components s = {} \<longleftrightarrow> s = {}"
lp15@66827
   721
  by (simp add: components_def)
lp15@66827
   722
lp15@66827
   723
lemma components_empty [simp]: "components {} = {}"
lp15@66827
   724
  by simp
lp15@66827
   725
lp15@66827
   726
lemma connected_eq_connected_components_eq: "connected s \<longleftrightarrow> (\<forall>c \<in> components s. \<forall>c' \<in> components s. c = c')"
lp15@66827
   727
  by (metis (no_types, hide_lams) components_iff connected_component_eq_eq connected_iff_connected_component)
lp15@66827
   728
lp15@66827
   729
lemma components_eq_sing_iff: "components s = {s} \<longleftrightarrow> connected s \<and> s \<noteq> {}"
lp15@66827
   730
  apply (rule iffI)
lp15@66827
   731
  using in_components_connected apply fastforce
lp15@66827
   732
  apply safe
lp15@66827
   733
  using Union_components apply fastforce
lp15@66827
   734
   apply (metis components_iff connected_component_eq_self)
lp15@66827
   735
  using in_components_maximal
lp15@66827
   736
  apply auto
lp15@66827
   737
  done
lp15@66827
   738
lp15@66827
   739
lemma components_eq_sing_exists: "(\<exists>a. components s = {a}) \<longleftrightarrow> connected s \<and> s \<noteq> {}"
lp15@66827
   740
  apply (rule iffI)
lp15@66827
   741
  using connected_eq_connected_components_eq apply fastforce
lp15@66827
   742
  apply (metis components_eq_sing_iff)
lp15@66827
   743
  done
lp15@66827
   744
lp15@66827
   745
lemma connected_eq_components_subset_sing: "connected s \<longleftrightarrow> components s \<subseteq> {s}"
lp15@66827
   746
  by (metis Union_components components_empty components_eq_sing_iff connected_empty insert_subset order_refl subset_singletonD)
lp15@66827
   747
lp15@66827
   748
lemma connected_eq_components_subset_sing_exists: "connected s \<longleftrightarrow> (\<exists>a. components s \<subseteq> {a})"
lp15@66827
   749
  by (metis components_eq_sing_exists connected_eq_components_subset_sing empty_iff subset_iff subset_singletonD)
lp15@66827
   750
lp15@66827
   751
lemma in_components_self: "s \<in> components s \<longleftrightarrow> connected s \<and> s \<noteq> {}"
lp15@66827
   752
  by (metis components_empty components_eq_sing_iff empty_iff in_components_connected insertI1)
lp15@66827
   753
lp15@66827
   754
lemma components_maximal: "\<lbrakk>c \<in> components s; connected t; t \<subseteq> s; c \<inter> t \<noteq> {}\<rbrakk> \<Longrightarrow> t \<subseteq> c"
lp15@66827
   755
  apply (simp add: components_def ex_in_conv [symmetric], clarify)
lp15@66827
   756
  by (meson connected_component_def connected_component_trans)
lp15@66827
   757
lp15@66827
   758
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
   759
  apply (cases "t = {}", force)
lp15@66827
   760
  apply (metis components_def ex_in_conv connected_component_maximal contra_subsetD image_eqI)
lp15@66827
   761
  done
lp15@66827
   762
lp15@66827
   763
lemma components_intermediate_subset: "\<lbrakk>s \<in> components u; s \<subseteq> t; t \<subseteq> u\<rbrakk> \<Longrightarrow> s \<in> components t"
lp15@66827
   764
  apply (auto simp: components_iff)
lp15@66827
   765
  apply (metis connected_component_eq_empty connected_component_intermediate_subset)
lp15@66827
   766
  done
lp15@66827
   767
lp15@66827
   768
lemma in_components_unions_complement: "c \<in> components s \<Longrightarrow> s - c = \<Union>(components s - {c})"
lp15@66827
   769
  by (metis complement_connected_component_unions components_def components_iff)
lp15@66827
   770
lp15@66827
   771
lemma connected_intermediate_closure:
lp15@66827
   772
  assumes cs: "connected s" and st: "s \<subseteq> t" and ts: "t \<subseteq> closure s"
lp15@66827
   773
  shows "connected t"
lp15@66827
   774
proof (rule connectedI)
lp15@66827
   775
  fix A B
lp15@66827
   776
  assume A: "open A" and B: "open B" and Alap: "A \<inter> t \<noteq> {}" and Blap: "B \<inter> t \<noteq> {}"
lp15@66827
   777
    and disj: "A \<inter> B \<inter> t = {}" and cover: "t \<subseteq> A \<union> B"
lp15@66827
   778
  have disjs: "A \<inter> B \<inter> s = {}"
lp15@66827
   779
    using disj st by auto
lp15@66827
   780
  have "A \<inter> closure s \<noteq> {}"
lp15@66827
   781
    using Alap Int_absorb1 ts by blast
lp15@66827
   782
  then have Alaps: "A \<inter> s \<noteq> {}"
lp15@66827
   783
    by (simp add: A open_Int_closure_eq_empty)
lp15@66827
   784
  have "B \<inter> closure s \<noteq> {}"
lp15@66827
   785
    using Blap Int_absorb1 ts by blast
lp15@66827
   786
  then have Blaps: "B \<inter> s \<noteq> {}"
lp15@66827
   787
    by (simp add: B open_Int_closure_eq_empty)
lp15@66827
   788
  then show False
lp15@66827
   789
    using cs [unfolded connected_def] A B disjs Alaps Blaps cover st
lp15@66827
   790
    by blast
lp15@66827
   791
qed
lp15@66827
   792
lp15@66827
   793
lemma closedin_connected_component: "closedin (subtopology euclidean s) (connected_component_set s x)"
lp15@66827
   794
proof (cases "connected_component_set s x = {}")
lp15@66827
   795
  case True
lp15@66827
   796
  then show ?thesis
lp15@66827
   797
    by (metis closedin_empty)
lp15@66827
   798
next
lp15@66827
   799
  case False
lp15@66827
   800
  then obtain y where y: "connected_component s x y"
lp15@66827
   801
    by blast
lp15@66827
   802
  have *: "connected_component_set s x \<subseteq> s \<inter> closure (connected_component_set s x)"
lp15@66827
   803
    by (auto simp: closure_def connected_component_in)
lp15@66827
   804
  have "connected_component s x y \<Longrightarrow> s \<inter> closure (connected_component_set s x) \<subseteq> connected_component_set s x"
lp15@66827
   805
    apply (rule connected_component_maximal, simp)
lp15@66827
   806
    using closure_subset connected_component_in apply fastforce
lp15@66827
   807
    using * connected_intermediate_closure apply blast+
lp15@66827
   808
    done
lp15@66827
   809
  with y * show ?thesis
lp15@66827
   810
    by (auto simp: closedin_closed)
lp15@66827
   811
qed
lp15@66827
   812
lp15@66939
   813
lemma closedin_component:
lp15@66939
   814
   "C \<in> components s \<Longrightarrow> closedin (subtopology euclidean s) C"
lp15@66939
   815
  using closedin_connected_component componentsE by blast
lp15@66939
   816
lp15@66827
   817
lp15@66827
   818
subsection \<open>Intersecting chains of compact sets and the Baire property\<close>
lp15@66827
   819
lp15@66827
   820
proposition bounded_closed_chain:
lp15@66827
   821
  fixes \<F> :: "'a::heine_borel set set"
lp15@66827
   822
  assumes "B \<in> \<F>" "bounded B" and \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> closed S" and "{} \<notin> \<F>"
lp15@66827
   823
      and chain: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
lp15@66827
   824
    shows "\<Inter>\<F> \<noteq> {}"
lp15@66827
   825
proof -
lp15@66827
   826
  have "B \<inter> \<Inter>\<F> \<noteq> {}"
lp15@66827
   827
  proof (rule compact_imp_fip)
lp15@66827
   828
    show "compact B" "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
lp15@66827
   829
      by (simp_all add: assms compact_eq_bounded_closed)
lp15@66827
   830
    show "\<lbrakk>finite \<G>; \<G> \<subseteq> \<F>\<rbrakk> \<Longrightarrow> B \<inter> \<Inter>\<G> \<noteq> {}" for \<G>
lp15@66827
   831
    proof (induction \<G> rule: finite_induct)
lp15@66827
   832
      case empty
lp15@66827
   833
      with assms show ?case by force
lp15@66827
   834
    next
lp15@66827
   835
      case (insert U \<G>)
lp15@66827
   836
      then have "U \<in> \<F>" and ne: "B \<inter> \<Inter>\<G> \<noteq> {}" by auto
lp15@66827
   837
      then consider "B \<subseteq> U" | "U \<subseteq> B"
lp15@66827
   838
          using \<open>B \<in> \<F>\<close> chain by blast
lp15@66827
   839
        then show ?case
lp15@66827
   840
        proof cases
lp15@66827
   841
          case 1
lp15@66827
   842
          then show ?thesis
lp15@66827
   843
            using Int_left_commute ne by auto
lp15@66827
   844
        next
lp15@66827
   845
          case 2
lp15@66827
   846
          have "U \<noteq> {}"
lp15@66827
   847
            using \<open>U \<in> \<F>\<close> \<open>{} \<notin> \<F>\<close> by blast
lp15@66827
   848
          moreover
lp15@66827
   849
          have False if "\<And>x. x \<in> U \<Longrightarrow> \<exists>Y\<in>\<G>. x \<notin> Y"
lp15@66827
   850
          proof -
lp15@66827
   851
            have "\<And>x. x \<in> U \<Longrightarrow> \<exists>Y\<in>\<G>. Y \<subseteq> U"
lp15@66827
   852
              by (metis chain contra_subsetD insert.prems insert_subset that)
lp15@66827
   853
            then obtain Y where "Y \<in> \<G>" "Y \<subseteq> U"
lp15@66827
   854
              by (metis all_not_in_conv \<open>U \<noteq> {}\<close>)
lp15@66827
   855
            moreover obtain x where "x \<in> \<Inter>\<G>"
lp15@66827
   856
              by (metis Int_emptyI ne)
lp15@66827
   857
            ultimately show ?thesis
lp15@66827
   858
              by (metis Inf_lower subset_eq that)
lp15@66827
   859
          qed
lp15@66827
   860
          with 2 show ?thesis
lp15@66827
   861
            by blast
lp15@66827
   862
        qed
lp15@66827
   863
      qed
lp15@66827
   864
  qed
lp15@66827
   865
  then show ?thesis by blast
lp15@66827
   866
qed
lp15@66827
   867
lp15@66827
   868
corollary compact_chain:
lp15@66827
   869
  fixes \<F> :: "'a::heine_borel set set"
lp15@66827
   870
  assumes "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" "{} \<notin> \<F>"
lp15@66827
   871
          "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
lp15@66827
   872
    shows "\<Inter> \<F> \<noteq> {}"
lp15@66827
   873
proof (cases "\<F> = {}")
lp15@66827
   874
  case True
lp15@66827
   875
  then show ?thesis by auto
lp15@66827
   876
next
lp15@66827
   877
  case False
lp15@66827
   878
  show ?thesis
lp15@66827
   879
    by (metis False all_not_in_conv assms compact_imp_bounded compact_imp_closed bounded_closed_chain)
lp15@66827
   880
qed
lp15@66827
   881
lp15@66827
   882
lemma compact_nest:
lp15@66827
   883
  fixes F :: "'a::linorder \<Rightarrow> 'b::heine_borel set"
lp15@66827
   884
  assumes F: "\<And>n. compact(F n)" "\<And>n. F n \<noteq> {}" and mono: "\<And>m n. m \<le> n \<Longrightarrow> F n \<subseteq> F m"
lp15@66827
   885
  shows "\<Inter>range F \<noteq> {}"
lp15@66827
   886
proof -
lp15@66827
   887
  have *: "\<And>S T. S \<in> range F \<and> T \<in> range F \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
lp15@66827
   888
    by (metis mono image_iff le_cases)
lp15@66827
   889
  show ?thesis
lp15@66827
   890
    apply (rule compact_chain [OF _ _ *])
lp15@66827
   891
    using F apply (blast intro: dest: *)+
lp15@66827
   892
    done
lp15@66827
   893
qed
lp15@66827
   894
lp15@66827
   895
text\<open>The Baire property of dense sets\<close>
lp15@66827
   896
theorem Baire:
lp15@66827
   897
  fixes S::"'a::{real_normed_vector,heine_borel} set"
lp15@66827
   898
  assumes "closed S" "countable \<G>"
lp15@66827
   899
      and ope: "\<And>T. T \<in> \<G> \<Longrightarrow> openin (subtopology euclidean S) T \<and> S \<subseteq> closure T"
lp15@66827
   900
 shows "S \<subseteq> closure(\<Inter>\<G>)"
lp15@66827
   901
proof (cases "\<G> = {}")
lp15@66827
   902
  case True
lp15@66827
   903
  then show ?thesis
lp15@66827
   904
    using closure_subset by auto
lp15@66827
   905
next
lp15@66827
   906
  let ?g = "from_nat_into \<G>"
lp15@66827
   907
  case False
lp15@66827
   908
  then have gin: "?g n \<in> \<G>" for n
lp15@66827
   909
    by (simp add: from_nat_into)
lp15@66827
   910
  show ?thesis
lp15@66827
   911
  proof (clarsimp simp: closure_approachable)
lp15@66827
   912
    fix x and e::real
lp15@66827
   913
    assume "x \<in> S" "0 < e"
lp15@66827
   914
    obtain TF where opeF: "\<And>n. openin (subtopology euclidean S) (TF n)"
lp15@66827
   915
               and ne: "\<And>n. TF n \<noteq> {}"
lp15@66827
   916
               and subg: "\<And>n. S \<inter> closure(TF n) \<subseteq> ?g n"
lp15@66827
   917
               and subball: "\<And>n. closure(TF n) \<subseteq> ball x e"
lp15@66827
   918
               and decr: "\<And>n. TF(Suc n) \<subseteq> TF n"
lp15@66827
   919
    proof -
lp15@66827
   920
      have *: "\<exists>Y. (openin (subtopology euclidean S) Y \<and> Y \<noteq> {} \<and>
lp15@66827
   921
                   S \<inter> closure Y \<subseteq> ?g n \<and> closure Y \<subseteq> ball x e) \<and> Y \<subseteq> U"
lp15@66827
   922
        if opeU: "openin (subtopology euclidean S) U" and "U \<noteq> {}" and cloU: "closure U \<subseteq> ball x e" for U n
lp15@66827
   923
      proof -
lp15@66827
   924
        obtain T where T: "open T" "U = T \<inter> S"
lp15@66827
   925
          using \<open>openin (subtopology euclidean S) U\<close> by (auto simp: openin_subtopology)
lp15@66827
   926
        with \<open>U \<noteq> {}\<close> have "T \<inter> closure (?g n) \<noteq> {}"
lp15@66827
   927
          using gin ope by fastforce
lp15@66827
   928
        then have "T \<inter> ?g n \<noteq> {}"
lp15@66827
   929
          using \<open>open T\<close> open_Int_closure_eq_empty by blast
lp15@66827
   930
        then obtain y where "y \<in> U" "y \<in> ?g n"
lp15@66827
   931
          using T ope [of "?g n", OF gin] by (blast dest:  openin_imp_subset)
lp15@66827
   932
        moreover have "openin (subtopology euclidean S) (U \<inter> ?g n)"
lp15@66827
   933
          using gin ope opeU by blast
lp15@66827
   934
        ultimately obtain d where U: "U \<inter> ?g n \<subseteq> S" and "d > 0" and d: "ball y d \<inter> S \<subseteq> U \<inter> ?g n"
lp15@66827
   935
          by (force simp: openin_contains_ball)
lp15@66827
   936
        show ?thesis
lp15@66827
   937
        proof (intro exI conjI)
lp15@66827
   938
          show "openin (subtopology euclidean S) (S \<inter> ball y (d/2))"
lp15@66827
   939
            by (simp add: openin_open_Int)
lp15@66827
   940
          show "S \<inter> ball y (d/2) \<noteq> {}"
lp15@66827
   941
            using \<open>0 < d\<close> \<open>y \<in> U\<close> opeU openin_imp_subset by fastforce
lp15@66827
   942
          have "S \<inter> closure (S \<inter> ball y (d/2)) \<subseteq> S \<inter> closure (ball y (d/2))"
lp15@66827
   943
            using closure_mono by blast
lp15@66827
   944
          also have "... \<subseteq> ?g n"
lp15@66827
   945
            using \<open>d > 0\<close> d by force
lp15@66827
   946
          finally show "S \<inter> closure (S \<inter> ball y (d/2)) \<subseteq> ?g n" .
lp15@66827
   947
          have "closure (S \<inter> ball y (d/2)) \<subseteq> S \<inter> ball y d"
lp15@66827
   948
          proof -
lp15@66827
   949
            have "closure (ball y (d/2)) \<subseteq> ball y d"
lp15@66827
   950
              using \<open>d > 0\<close> by auto
lp15@66827
   951
            then have "closure (S \<inter> ball y (d/2)) \<subseteq> ball y d"
lp15@66827
   952
              by (meson closure_mono inf.cobounded2 subset_trans)
lp15@66827
   953
            then show ?thesis
lp15@66827
   954
              by (simp add: \<open>closed S\<close> closure_minimal)
lp15@66827
   955
          qed
lp15@66827
   956
          also have "...  \<subseteq> ball x e"
lp15@66827
   957
            using cloU closure_subset d by blast
lp15@66827
   958
          finally show "closure (S \<inter> ball y (d/2)) \<subseteq> ball x e" .
lp15@66827
   959
          show "S \<inter> ball y (d/2) \<subseteq> U"
lp15@66827
   960
            using ball_divide_subset_numeral d by blast
lp15@66827
   961
        qed
lp15@66827
   962
      qed
lp15@66827
   963
      let ?\<Phi> = "\<lambda>n X. openin (subtopology euclidean S) X \<and> X \<noteq> {} \<and>
lp15@66827
   964
                      S \<inter> closure X \<subseteq> ?g n \<and> closure X \<subseteq> ball x e"
lp15@66827
   965
      have "closure (S \<inter> ball x (e / 2)) \<subseteq> closure(ball x (e/2))"
lp15@66827
   966
        by (simp add: closure_mono)
lp15@66827
   967
      also have "...  \<subseteq> ball x e"
lp15@66827
   968
        using \<open>e > 0\<close> by auto
lp15@66827
   969
      finally have "closure (S \<inter> ball x (e / 2)) \<subseteq> ball x e" .
lp15@66827
   970
      moreover have"openin (subtopology euclidean S) (S \<inter> ball x (e / 2))" "S \<inter> ball x (e / 2) \<noteq> {}"
lp15@66827
   971
        using \<open>0 < e\<close> \<open>x \<in> S\<close> by auto
lp15@66827
   972
      ultimately obtain Y where Y: "?\<Phi> 0 Y \<and> Y \<subseteq> S \<inter> ball x (e / 2)"
lp15@66827
   973
            using * [of "S \<inter> ball x (e/2)" 0] by metis
lp15@66827
   974
      show thesis
lp15@66827
   975
      proof (rule exE [OF dependent_nat_choice [of ?\<Phi> "\<lambda>n X Y. Y \<subseteq> X"]])
lp15@66827
   976
        show "\<exists>x. ?\<Phi> 0 x"
lp15@66827
   977
          using Y by auto
lp15@66827
   978
        show "\<exists>Y. ?\<Phi> (Suc n) Y \<and> Y \<subseteq> X" if "?\<Phi> n X" for X n
lp15@66827
   979
          using that by (blast intro: *)
lp15@66827
   980
      qed (use that in metis)
lp15@66827
   981
    qed
lp15@66827
   982
    have "(\<Inter>n. S \<inter> closure (TF n)) \<noteq> {}"
lp15@66827
   983
    proof (rule compact_nest)
lp15@66827
   984
      show "\<And>n. compact (S \<inter> closure (TF n))"
lp15@66827
   985
        by (metis closed_closure subball bounded_subset_ballI compact_eq_bounded_closed closed_Int_compact [OF \<open>closed S\<close>])
lp15@66827
   986
      show "\<And>n. S \<inter> closure (TF n) \<noteq> {}"
lp15@66827
   987
        by (metis Int_absorb1 opeF \<open>closed S\<close> closure_eq_empty closure_minimal ne openin_imp_subset)
lp15@66827
   988
      show "\<And>m n. m \<le> n \<Longrightarrow> S \<inter> closure (TF n) \<subseteq> S \<inter> closure (TF m)"
lp15@66827
   989
        by (meson closure_mono decr dual_order.refl inf_mono lift_Suc_antimono_le)
lp15@66827
   990
    qed
lp15@66827
   991
    moreover have "(\<Inter>n. S \<inter> closure (TF n)) \<subseteq> {y \<in> \<Inter>\<G>. dist y x < e}"
lp15@66827
   992
    proof (clarsimp, intro conjI)
lp15@66827
   993
      fix y
lp15@66827
   994
      assume "y \<in> S" and y: "\<forall>n. y \<in> closure (TF n)"
lp15@66827
   995
      then show "\<forall>T\<in>\<G>. y \<in> T"
lp15@66827
   996
        by (metis Int_iff from_nat_into_surj [OF \<open>countable \<G>\<close>] set_mp subg)
lp15@66827
   997
      show "dist y x < e"
lp15@66827
   998
        by (metis y dist_commute mem_ball subball subsetCE)
lp15@66827
   999
    qed
lp15@66827
  1000
    ultimately show "\<exists>y \<in> \<Inter>\<G>. dist y x < e"
lp15@66827
  1001
      by auto
lp15@66827
  1002
  qed
lp15@66827
  1003
qed
lp15@66827
  1004
lp15@66827
  1005
subsection\<open>Some theorems on sups and infs using the notion "bounded".\<close>
lp15@66827
  1006
lp15@66827
  1007
lemma bounded_real: "bounded (S::real set) \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. \<bar>x\<bar> \<le> a)"
lp15@66827
  1008
  by (simp add: bounded_iff)
lp15@66827
  1009
lp15@66827
  1010
lemma bounded_imp_bdd_above: "bounded S \<Longrightarrow> bdd_above (S :: real set)"
lp15@66827
  1011
  by (auto simp: bounded_def bdd_above_def dist_real_def)
lp15@66827
  1012
     (metis abs_le_D1 abs_minus_commute diff_le_eq)
lp15@66827
  1013
lp15@66827
  1014
lemma bounded_imp_bdd_below: "bounded S \<Longrightarrow> bdd_below (S :: real set)"
lp15@66827
  1015
  by (auto simp: bounded_def bdd_below_def dist_real_def)
lp15@66827
  1016
     (metis abs_le_D1 add.commute diff_le_eq)
lp15@66827
  1017
lp15@66827
  1018
lemma bounded_inner_imp_bdd_above:
lp15@66827
  1019
  assumes "bounded s"
lp15@66827
  1020
    shows "bdd_above ((\<lambda>x. x \<bullet> a) ` s)"
lp15@66827
  1021
by (simp add: assms bounded_imp_bdd_above bounded_linear_image bounded_linear_inner_left)
lp15@66827
  1022
lp15@66827
  1023
lemma bounded_inner_imp_bdd_below:
lp15@66827
  1024
  assumes "bounded s"
lp15@66827
  1025
    shows "bdd_below ((\<lambda>x. x \<bullet> a) ` s)"
lp15@66827
  1026
by (simp add: assms bounded_imp_bdd_below bounded_linear_image bounded_linear_inner_left)
lp15@66827
  1027
lp15@66827
  1028
lemma bounded_has_Sup:
lp15@66827
  1029
  fixes S :: "real set"
lp15@66827
  1030
  assumes "bounded S"
lp15@66827
  1031
    and "S \<noteq> {}"
lp15@66827
  1032
  shows "\<forall>x\<in>S. x \<le> Sup S"
lp15@66827
  1033
    and "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> b"
lp15@66827
  1034
proof
lp15@66827
  1035
  show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> b"
lp15@66827
  1036
    using assms by (metis cSup_least)
lp15@66827
  1037
qed (metis cSup_upper assms(1) bounded_imp_bdd_above)
lp15@66827
  1038
lp15@66827
  1039
lemma Sup_insert:
lp15@66827
  1040
  fixes S :: "real set"
lp15@66827
  1041
  shows "bounded S \<Longrightarrow> Sup (insert x S) = (if S = {} then x else max x (Sup S))"
lp15@66827
  1042
  by (auto simp: bounded_imp_bdd_above sup_max cSup_insert_If)
lp15@66827
  1043
lp15@66827
  1044
lemma Sup_insert_finite:
lp15@66827
  1045
  fixes S :: "'a::conditionally_complete_linorder set"
lp15@66827
  1046
  shows "finite S \<Longrightarrow> Sup (insert x S) = (if S = {} then x else max x (Sup S))"
lp15@66827
  1047
by (simp add: cSup_insert sup_max)
lp15@66827
  1048
lp15@66827
  1049
lemma bounded_has_Inf:
lp15@66827
  1050
  fixes S :: "real set"
lp15@66827
  1051
  assumes "bounded S"
lp15@66827
  1052
    and "S \<noteq> {}"
lp15@66827
  1053
  shows "\<forall>x\<in>S. x \<ge> Inf S"
lp15@66827
  1054
    and "\<forall>b. (\<forall>x\<in>S. x \<ge> b) \<longrightarrow> Inf S \<ge> b"
lp15@66827
  1055
proof
lp15@66827
  1056
  show "\<forall>b. (\<forall>x\<in>S. x \<ge> b) \<longrightarrow> Inf S \<ge> b"
lp15@66827
  1057
    using assms by (metis cInf_greatest)
lp15@66827
  1058
qed (metis cInf_lower assms(1) bounded_imp_bdd_below)
lp15@66827
  1059
lp15@66827
  1060
lemma Inf_insert:
lp15@66827
  1061
  fixes S :: "real set"
lp15@66827
  1062
  shows "bounded S \<Longrightarrow> Inf (insert x S) = (if S = {} then x else min x (Inf S))"
lp15@66827
  1063
  by (auto simp: bounded_imp_bdd_below inf_min cInf_insert_If)
lp15@66827
  1064
lp15@66827
  1065
lemma Inf_insert_finite:
lp15@66827
  1066
  fixes S :: "'a::conditionally_complete_linorder set"
lp15@66827
  1067
  shows "finite S \<Longrightarrow> Inf (insert x S) = (if S = {} then x else min x (Inf S))"
lp15@66827
  1068
by (simp add: cInf_eq_Min)
lp15@66827
  1069
lp15@66827
  1070
lemma finite_imp_less_Inf:
lp15@66827
  1071
  fixes a :: "'a::conditionally_complete_linorder"
lp15@66827
  1072
  shows "\<lbrakk>finite X; x \<in> X; \<And>x. x\<in>X \<Longrightarrow> a < x\<rbrakk> \<Longrightarrow> a < Inf X"
lp15@66827
  1073
  by (induction X rule: finite_induct) (simp_all add: cInf_eq_Min Inf_insert_finite)
lp15@66827
  1074
lp15@66827
  1075
lemma finite_less_Inf_iff:
lp15@66827
  1076
  fixes a :: "'a :: conditionally_complete_linorder"
lp15@66827
  1077
  shows "\<lbrakk>finite X; X \<noteq> {}\<rbrakk> \<Longrightarrow> a < Inf X \<longleftrightarrow> (\<forall>x \<in> X. a < x)"
lp15@66827
  1078
  by (auto simp: cInf_eq_Min)
lp15@66827
  1079
lp15@66827
  1080
lemma finite_imp_Sup_less:
lp15@66827
  1081
  fixes a :: "'a::conditionally_complete_linorder"
lp15@66827
  1082
  shows "\<lbrakk>finite X; x \<in> X; \<And>x. x\<in>X \<Longrightarrow> a > x\<rbrakk> \<Longrightarrow> a > Sup X"
lp15@66827
  1083
  by (induction X rule: finite_induct) (simp_all add: cSup_eq_Max Sup_insert_finite)
lp15@66827
  1084
lp15@66827
  1085
lemma finite_Sup_less_iff:
lp15@66827
  1086
  fixes a :: "'a :: conditionally_complete_linorder"
lp15@66827
  1087
  shows "\<lbrakk>finite X; X \<noteq> {}\<rbrakk> \<Longrightarrow> a > Sup X \<longleftrightarrow> (\<forall>x \<in> X. a > x)"
lp15@66827
  1088
  by (auto simp: cSup_eq_Max)
lp15@66827
  1089
lp15@66827
  1090
proposition is_interval_compact:
lp15@66827
  1091
   "is_interval S \<and> compact S \<longleftrightarrow> (\<exists>a b. S = cbox a b)"   (is "?lhs = ?rhs")
lp15@66827
  1092
proof (cases "S = {}")
lp15@66827
  1093
  case True
lp15@66827
  1094
  with empty_as_interval show ?thesis by auto
lp15@66827
  1095
next
lp15@66827
  1096
  case False
lp15@66827
  1097
  show ?thesis
lp15@66827
  1098
  proof
lp15@66827
  1099
    assume L: ?lhs
lp15@66827
  1100
    then have "is_interval S" "compact S" by auto
lp15@66827
  1101
    define a where "a \<equiv> \<Sum>i\<in>Basis. (INF x:S. x \<bullet> i) *\<^sub>R i"
lp15@66827
  1102
    define b where "b \<equiv> \<Sum>i\<in>Basis. (SUP x:S. x \<bullet> i) *\<^sub>R i"
lp15@66827
  1103
    have 1: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> (INF x:S. x \<bullet> i) \<le> x \<bullet> i"
lp15@66827
  1104
      by (simp add: cInf_lower bounded_inner_imp_bdd_below compact_imp_bounded L)
lp15@66827
  1105
    have 2: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> x \<bullet> i \<le> (SUP x:S. x \<bullet> i)"
lp15@66827
  1106
      by (simp add: cSup_upper bounded_inner_imp_bdd_above compact_imp_bounded L)
lp15@66827
  1107
    have 3: "x \<in> S" if inf: "\<And>i. i \<in> Basis \<Longrightarrow> (INF x:S. x \<bullet> i) \<le> x \<bullet> i"
lp15@66827
  1108
                   and sup: "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<le> (SUP x:S. x \<bullet> i)" for x
lp15@66827
  1109
    proof (rule mem_box_componentwiseI [OF \<open>is_interval S\<close>])
lp15@66827
  1110
      fix i::'a
lp15@66827
  1111
      assume i: "i \<in> Basis"
lp15@66827
  1112
      have cont: "continuous_on S (\<lambda>x. x \<bullet> i)"
lp15@66827
  1113
        by (intro continuous_intros)
lp15@66827
  1114
      obtain a where "a \<in> S" and a: "\<And>y. y\<in>S \<Longrightarrow> a \<bullet> i \<le> y \<bullet> i"
lp15@66827
  1115
        using continuous_attains_inf [OF \<open>compact S\<close> False cont] by blast
lp15@66827
  1116
      obtain b where "b \<in> S" and b: "\<And>y. y\<in>S \<Longrightarrow> y \<bullet> i \<le> b \<bullet> i"
lp15@66827
  1117
        using continuous_attains_sup [OF \<open>compact S\<close> False cont] by blast
lp15@66827
  1118
      have "a \<bullet> i \<le> (INF x:S. x \<bullet> i)"
lp15@66827
  1119
        by (simp add: False a cINF_greatest)
lp15@66827
  1120
      also have "\<dots> \<le> x \<bullet> i"
lp15@66827
  1121
        by (simp add: i inf)
lp15@66827
  1122
      finally have ai: "a \<bullet> i \<le> x \<bullet> i" .
lp15@66827
  1123
      have "x \<bullet> i \<le> (SUP x:S. x \<bullet> i)"
lp15@66827
  1124
        by (simp add: i sup)
lp15@66827
  1125
      also have "(SUP x:S. x \<bullet> i) \<le> b \<bullet> i"
lp15@66827
  1126
        by (simp add: False b cSUP_least)
lp15@66827
  1127
      finally have bi: "x \<bullet> i \<le> b \<bullet> i" .
lp15@66827
  1128
      show "x \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` S"
lp15@66827
  1129
        apply (rule_tac x="\<Sum>j\<in>Basis. (if j = i then x \<bullet> i else a \<bullet> j) *\<^sub>R j" in image_eqI)
lp15@66827
  1130
        apply (simp add: i)
lp15@66827
  1131
        apply (rule mem_is_intervalI [OF \<open>is_interval S\<close> \<open>a \<in> S\<close> \<open>b \<in> S\<close>])
lp15@66827
  1132
        using i ai bi apply force
lp15@66827
  1133
        done
lp15@66827
  1134
    qed
lp15@66827
  1135
    have "S = cbox a b"
lp15@66827
  1136
      by (auto simp: a_def b_def mem_box intro: 1 2 3)
lp15@66827
  1137
    then show ?rhs
lp15@66827
  1138
      by blast
lp15@66827
  1139
  next
lp15@66827
  1140
    assume R: ?rhs
lp15@66827
  1141
    then show ?lhs
lp15@66827
  1142
      using compact_cbox is_interval_cbox by blast
lp15@66827
  1143
  qed
lp15@66827
  1144
qed
lp15@66827
  1145
lp15@66827
  1146
subsection\<open>Relations among convergence and absolute convergence for power series.\<close>
lp15@66827
  1147
lp15@66827
  1148
lemma summable_imp_bounded:
lp15@66827
  1149
  fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
lp15@66827
  1150
  shows "summable f \<Longrightarrow> bounded (range f)"
lp15@66827
  1151
by (frule summable_LIMSEQ_zero) (simp add: convergent_imp_bounded)
lp15@66827
  1152
lp15@66827
  1153
lemma summable_imp_sums_bounded:
lp15@66827
  1154
   "summable f \<Longrightarrow> bounded (range (\<lambda>n. sum f {..<n}))"
lp15@66827
  1155
by (auto simp: summable_def sums_def dest: convergent_imp_bounded)
lp15@66827
  1156
lp15@66827
  1157
lemma power_series_conv_imp_absconv_weak:
lp15@66827
  1158
  fixes a:: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}" and w :: 'a
lp15@66827
  1159
  assumes sum: "summable (\<lambda>n. a n * z ^ n)" and no: "norm w < norm z"
lp15@66827
  1160
    shows "summable (\<lambda>n. of_real(norm(a n)) * w ^ n)"
lp15@66827
  1161
proof -
lp15@66827
  1162
  obtain M where M: "\<And>x. norm (a x * z ^ x) \<le> M"
lp15@66827
  1163
    using summable_imp_bounded [OF sum] by (force simp: bounded_iff)
lp15@66827
  1164
  then have *: "summable (\<lambda>n. norm (a n) * norm w ^ n)"
lp15@66827
  1165
    by (rule_tac M=M in Abel_lemma) (auto simp: norm_mult norm_power intro: no)
lp15@66827
  1166
  show ?thesis
lp15@66827
  1167
    apply (rule series_comparison_complex [of "(\<lambda>n. of_real(norm(a n) * norm w ^ n))"])
lp15@66827
  1168
    apply (simp only: summable_complex_of_real *)
lp15@66827
  1169
    apply (auto simp: norm_mult norm_power)
lp15@66827
  1170
    done
lp15@66827
  1171
qed
lp15@66827
  1172
lp15@66827
  1173
subsection \<open>Bounded closed nest property (proof does not use Heine-Borel)\<close>
lp15@66827
  1174
lp15@66827
  1175
lemma bounded_closed_nest:
lp15@66827
  1176
  fixes s :: "nat \<Rightarrow> ('a::heine_borel) set"
lp15@66827
  1177
  assumes "\<forall>n. closed (s n)"
lp15@66827
  1178
    and "\<forall>n. s n \<noteq> {}"
lp15@66827
  1179
    and "\<forall>m n. m \<le> n \<longrightarrow> s n \<subseteq> s m"
lp15@66827
  1180
    and "bounded (s 0)"
lp15@66827
  1181
  shows "\<exists>a. \<forall>n. a \<in> s n"
lp15@66827
  1182
proof -
lp15@66827
  1183
  from assms(2) obtain x where x: "\<forall>n. x n \<in> s n"
lp15@66827
  1184
    using choice[of "\<lambda>n x. x \<in> s n"] by auto
lp15@66827
  1185
  from assms(4,1) have "seq_compact (s 0)"
lp15@66827
  1186
    by (simp add: bounded_closed_imp_seq_compact)
lp15@66827
  1187
  then obtain l r where lr: "l \<in> s 0" "strict_mono r" "(x \<circ> r) \<longlonglongrightarrow> l"
lp15@66827
  1188
    using x and assms(3) unfolding seq_compact_def by blast
lp15@66827
  1189
  have "\<forall>n. l \<in> s n"
lp15@66827
  1190
  proof
lp15@66827
  1191
    fix n :: nat
lp15@66827
  1192
    have "closed (s n)"
lp15@66827
  1193
      using assms(1) by simp
lp15@66827
  1194
    moreover have "\<forall>i. (x \<circ> r) i \<in> s i"
lp15@66827
  1195
      using x and assms(3) and lr(2) [THEN seq_suble] by auto
lp15@66827
  1196
    then have "\<forall>i. (x \<circ> r) (i + n) \<in> s n"
lp15@66827
  1197
      using assms(3) by (fast intro!: le_add2)
lp15@66827
  1198
    moreover have "(\<lambda>i. (x \<circ> r) (i + n)) \<longlonglongrightarrow> l"
lp15@66827
  1199
      using lr(3) by (rule LIMSEQ_ignore_initial_segment)
lp15@66827
  1200
    ultimately show "l \<in> s n"
lp15@66827
  1201
      by (rule closed_sequentially)
lp15@66827
  1202
  qed
lp15@66827
  1203
  then show ?thesis ..
lp15@66827
  1204
qed
lp15@66827
  1205
lp15@66827
  1206
text \<open>Decreasing case does not even need compactness, just completeness.\<close>
lp15@66827
  1207
lp15@66827
  1208
lemma decreasing_closed_nest:
lp15@66827
  1209
  fixes s :: "nat \<Rightarrow> ('a::complete_space) set"
lp15@66827
  1210
  assumes
lp15@66827
  1211
    "\<forall>n. closed (s n)"
lp15@66827
  1212
    "\<forall>n. s n \<noteq> {}"
lp15@66827
  1213
    "\<forall>m n. m \<le> n \<longrightarrow> s n \<subseteq> s m"
lp15@66827
  1214
    "\<forall>e>0. \<exists>n. \<forall>x\<in>s n. \<forall>y\<in>s n. dist x y < e"
lp15@66827
  1215
  shows "\<exists>a. \<forall>n. a \<in> s n"
lp15@66827
  1216
proof -
lp15@66827
  1217
  have "\<forall>n. \<exists>x. x \<in> s n"
lp15@66827
  1218
    using assms(2) by auto
lp15@66827
  1219
  then have "\<exists>t. \<forall>n. t n \<in> s n"
lp15@66827
  1220
    using choice[of "\<lambda>n x. x \<in> s n"] by auto
lp15@66827
  1221
  then obtain t where t: "\<forall>n. t n \<in> s n" by auto
lp15@66827
  1222
  {
lp15@66827
  1223
    fix e :: real
lp15@66827
  1224
    assume "e > 0"
lp15@66827
  1225
    then obtain N where N:"\<forall>x\<in>s N. \<forall>y\<in>s N. dist x y < e"
lp15@66827
  1226
      using assms(4) by auto
lp15@66827
  1227
    {
lp15@66827
  1228
      fix m n :: nat
lp15@66827
  1229
      assume "N \<le> m \<and> N \<le> n"
lp15@66827
  1230
      then have "t m \<in> s N" "t n \<in> s N"
lp15@66827
  1231
        using assms(3) t unfolding  subset_eq t by blast+
lp15@66827
  1232
      then have "dist (t m) (t n) < e"
lp15@66827
  1233
        using N by auto
lp15@66827
  1234
    }
lp15@66827
  1235
    then have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (t m) (t n) < e"
lp15@66827
  1236
      by auto
lp15@66827
  1237
  }
lp15@66827
  1238
  then have "Cauchy t"
lp15@66827
  1239
    unfolding cauchy_def by auto
lp15@66827
  1240
  then obtain l where l:"(t \<longlongrightarrow> l) sequentially"
lp15@66827
  1241
    using complete_UNIV unfolding complete_def by auto
lp15@66827
  1242
  {
lp15@66827
  1243
    fix n :: nat
lp15@66827
  1244
    {
lp15@66827
  1245
      fix e :: real
lp15@66827
  1246
      assume "e > 0"
lp15@66827
  1247
      then obtain N :: nat where N: "\<forall>n\<ge>N. dist (t n) l < e"
lp15@66827
  1248
        using l[unfolded lim_sequentially] by auto
lp15@66827
  1249
      have "t (max n N) \<in> s n"
lp15@66835
  1250
        by (meson assms(3) contra_subsetD max.cobounded1 t)
lp15@66827
  1251
      then have "\<exists>y\<in>s n. dist y l < e"
lp15@66835
  1252
        using N max.cobounded2 by blast
lp15@66827
  1253
    }
lp15@66827
  1254
    then have "l \<in> s n"
lp15@66827
  1255
      using closed_approachable[of "s n" l] assms(1) by auto
lp15@66827
  1256
  }
lp15@66827
  1257
  then show ?thesis by auto
lp15@66827
  1258
qed
lp15@66827
  1259
lp15@66827
  1260
text \<open>Strengthen it to the intersection actually being a singleton.\<close>
lp15@66827
  1261
lp15@66827
  1262
lemma decreasing_closed_nest_sing:
lp15@66827
  1263
  fixes s :: "nat \<Rightarrow> 'a::complete_space set"
lp15@66827
  1264
  assumes
lp15@66827
  1265
    "\<forall>n. closed(s n)"
lp15@66827
  1266
    "\<forall>n. s n \<noteq> {}"
lp15@66827
  1267
    "\<forall>m n. m \<le> n \<longrightarrow> s n \<subseteq> s m"
lp15@66827
  1268
    "\<forall>e>0. \<exists>n. \<forall>x \<in> (s n). \<forall> y\<in>(s n). dist x y < e"
lp15@66827
  1269
  shows "\<exists>a. \<Inter>(range s) = {a}"
lp15@66827
  1270
proof -
lp15@66827
  1271
  obtain a where a: "\<forall>n. a \<in> s n"
lp15@66827
  1272
    using decreasing_closed_nest[of s] using assms by auto
lp15@66827
  1273
  {
lp15@66827
  1274
    fix b
lp15@66827
  1275
    assume b: "b \<in> \<Inter>(range s)"
lp15@66827
  1276
    {
lp15@66827
  1277
      fix e :: real
lp15@66827
  1278
      assume "e > 0"
lp15@66827
  1279
      then have "dist a b < e"
lp15@66827
  1280
        using assms(4) and b and a by blast
lp15@66827
  1281
    }
lp15@66827
  1282
    then have "dist a b = 0"
lp15@66827
  1283
      by (metis dist_eq_0_iff dist_nz less_le)
lp15@66827
  1284
  }
lp15@66827
  1285
  with a have "\<Inter>(range s) = {a}"
lp15@66827
  1286
    unfolding image_def by auto
lp15@66827
  1287
  then show ?thesis ..
lp15@66827
  1288
qed
lp15@66827
  1289
lp15@66827
  1290
lp15@66827
  1291
subsection \<open>Infimum Distance\<close>
lp15@66827
  1292
lp15@66827
  1293
definition "infdist x A = (if A = {} then 0 else INF a:A. dist x a)"
lp15@66827
  1294
lp15@66827
  1295
lemma bdd_below_infdist[intro, simp]: "bdd_below (dist x`A)"
lp15@66827
  1296
  by (auto intro!: zero_le_dist)
lp15@66827
  1297
lp15@66827
  1298
lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = (INF a:A. dist x a)"
lp15@66827
  1299
  by (simp add: infdist_def)
lp15@66827
  1300
lp15@66827
  1301
lemma infdist_nonneg: "0 \<le> infdist x A"
lp15@66827
  1302
  by (auto simp: infdist_def intro: cINF_greatest)
lp15@66827
  1303
lp15@66827
  1304
lemma infdist_le: "a \<in> A \<Longrightarrow> infdist x A \<le> dist x a"
lp15@66827
  1305
  by (auto intro: cINF_lower simp add: infdist_def)
lp15@66827
  1306
lp15@66827
  1307
lemma infdist_le2: "a \<in> A \<Longrightarrow> dist x a \<le> d \<Longrightarrow> infdist x A \<le> d"
lp15@66827
  1308
  by (auto intro!: cINF_lower2 simp add: infdist_def)
lp15@66827
  1309
lp15@66827
  1310
lemma infdist_zero[simp]: "a \<in> A \<Longrightarrow> infdist a A = 0"
lp15@66827
  1311
  by (auto intro!: antisym infdist_nonneg infdist_le2)
lp15@66827
  1312
lp15@66827
  1313
lemma infdist_triangle: "infdist x A \<le> infdist y A + dist x y"
lp15@66827
  1314
proof (cases "A = {}")
lp15@66827
  1315
  case True
lp15@66827
  1316
  then show ?thesis by (simp add: infdist_def)
lp15@66827
  1317
next
lp15@66827
  1318
  case False
lp15@66827
  1319
  then obtain a where "a \<in> A" by auto
lp15@66827
  1320
  have "infdist x A \<le> Inf {dist x y + dist y a |a. a \<in> A}"
lp15@66827
  1321
  proof (rule cInf_greatest)
lp15@66827
  1322
    from \<open>A \<noteq> {}\<close> show "{dist x y + dist y a |a. a \<in> A} \<noteq> {}"
lp15@66827
  1323
      by simp
lp15@66827
  1324
    fix d
lp15@66827
  1325
    assume "d \<in> {dist x y + dist y a |a. a \<in> A}"
lp15@66827
  1326
    then obtain a where d: "d = dist x y + dist y a" "a \<in> A"
lp15@66827
  1327
      by auto
lp15@66827
  1328
    show "infdist x A \<le> d"
lp15@66827
  1329
      unfolding infdist_notempty[OF \<open>A \<noteq> {}\<close>]
lp15@66827
  1330
    proof (rule cINF_lower2)
lp15@66827
  1331
      show "a \<in> A" by fact
lp15@66827
  1332
      show "dist x a \<le> d"
lp15@66827
  1333
        unfolding d by (rule dist_triangle)
lp15@66827
  1334
    qed simp
lp15@66827
  1335
  qed
lp15@66827
  1336
  also have "\<dots> = dist x y + infdist y A"
lp15@66827
  1337
  proof (rule cInf_eq, safe)
lp15@66827
  1338
    fix a
lp15@66827
  1339
    assume "a \<in> A"
lp15@66827
  1340
    then show "dist x y + infdist y A \<le> dist x y + dist y a"
lp15@66827
  1341
      by (auto intro: infdist_le)
lp15@66827
  1342
  next
lp15@66827
  1343
    fix i
lp15@66827
  1344
    assume inf: "\<And>d. d \<in> {dist x y + dist y a |a. a \<in> A} \<Longrightarrow> i \<le> d"
lp15@66827
  1345
    then have "i - dist x y \<le> infdist y A"
lp15@66827
  1346
      unfolding infdist_notempty[OF \<open>A \<noteq> {}\<close>] using \<open>a \<in> A\<close>
lp15@66827
  1347
      by (intro cINF_greatest) (auto simp: field_simps)
lp15@66827
  1348
    then show "i \<le> dist x y + infdist y A"
lp15@66827
  1349
      by simp
lp15@66827
  1350
  qed
lp15@66827
  1351
  finally show ?thesis by simp
lp15@66827
  1352
qed
lp15@66827
  1353
lp15@66827
  1354
lemma in_closure_iff_infdist_zero:
lp15@66827
  1355
  assumes "A \<noteq> {}"
lp15@66827
  1356
  shows "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
lp15@66827
  1357
proof
lp15@66827
  1358
  assume "x \<in> closure A"
lp15@66827
  1359
  show "infdist x A = 0"
lp15@66827
  1360
  proof (rule ccontr)
lp15@66827
  1361
    assume "infdist x A \<noteq> 0"
lp15@66827
  1362
    with infdist_nonneg[of x A] have "infdist x A > 0"
lp15@66827
  1363
      by auto
lp15@66827
  1364
    then have "ball x (infdist x A) \<inter> closure A = {}"
lp15@66827
  1365
      apply auto
lp15@66827
  1366
      apply (metis \<open>x \<in> closure A\<close> closure_approachable dist_commute infdist_le not_less)
lp15@66827
  1367
      done
lp15@66827
  1368
    then have "x \<notin> closure A"
lp15@66827
  1369
      by (metis \<open>0 < infdist x A\<close> centre_in_ball disjoint_iff_not_equal)
lp15@66827
  1370
    then show False using \<open>x \<in> closure A\<close> by simp
lp15@66827
  1371
  qed
lp15@66827
  1372
next
lp15@66827
  1373
  assume x: "infdist x A = 0"
lp15@66827
  1374
  then obtain a where "a \<in> A"
lp15@66827
  1375
    by atomize_elim (metis all_not_in_conv assms)
lp15@66827
  1376
  show "x \<in> closure A"
lp15@66827
  1377
    unfolding closure_approachable
lp15@66827
  1378
    apply safe
lp15@66827
  1379
  proof (rule ccontr)
lp15@66827
  1380
    fix e :: real
lp15@66827
  1381
    assume "e > 0"
lp15@66827
  1382
    assume "\<not> (\<exists>y\<in>A. dist y x < e)"
lp15@66827
  1383
    then have "infdist x A \<ge> e" using \<open>a \<in> A\<close>
lp15@66827
  1384
      unfolding infdist_def
lp15@66827
  1385
      by (force simp: dist_commute intro: cINF_greatest)
lp15@66827
  1386
    with x \<open>e > 0\<close> show False by auto
lp15@66827
  1387
  qed
lp15@66827
  1388
qed
lp15@66827
  1389
lp15@66827
  1390
lemma in_closed_iff_infdist_zero:
lp15@66827
  1391
  assumes "closed A" "A \<noteq> {}"
lp15@66827
  1392
  shows "x \<in> A \<longleftrightarrow> infdist x A = 0"
lp15@66827
  1393
proof -
lp15@66827
  1394
  have "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
lp15@66827
  1395
    by (rule in_closure_iff_infdist_zero) fact
lp15@66827
  1396
  with assms show ?thesis by simp
lp15@66827
  1397
qed
lp15@66827
  1398
lp15@66827
  1399
lemma tendsto_infdist [tendsto_intros]:
lp15@66827
  1400
  assumes f: "(f \<longlongrightarrow> l) F"
lp15@66827
  1401
  shows "((\<lambda>x. infdist (f x) A) \<longlongrightarrow> infdist l A) F"
lp15@66827
  1402
proof (rule tendstoI)
lp15@66827
  1403
  fix e ::real
lp15@66827
  1404
  assume "e > 0"
lp15@66827
  1405
  from tendstoD[OF f this]
lp15@66827
  1406
  show "eventually (\<lambda>x. dist (infdist (f x) A) (infdist l A) < e) F"
lp15@66827
  1407
  proof (eventually_elim)
lp15@66827
  1408
    fix x
lp15@66827
  1409
    from infdist_triangle[of l A "f x"] infdist_triangle[of "f x" A l]
lp15@66827
  1410
    have "dist (infdist (f x) A) (infdist l A) \<le> dist (f x) l"
lp15@66827
  1411
      by (simp add: dist_commute dist_real_def)
lp15@66827
  1412
    also assume "dist (f x) l < e"
lp15@66827
  1413
    finally show "dist (infdist (f x) A) (infdist l A) < e" .
lp15@66827
  1414
  qed
lp15@66827
  1415
qed
lp15@66827
  1416
lp15@66827
  1417
lemma continuous_infdist[continuous_intros]:
lp15@66827
  1418
  assumes "continuous F f"
lp15@66827
  1419
  shows "continuous F (\<lambda>x. infdist (f x) A)"
lp15@66827
  1420
  using assms unfolding continuous_def by (rule tendsto_infdist)
lp15@66827
  1421
lp15@66827
  1422
subsection \<open>Equality of continuous functions on closure and related results.\<close>
lp15@66827
  1423
lp15@66827
  1424
lemma continuous_closedin_preimage_constant:
lp15@66827
  1425
  fixes f :: "_ \<Rightarrow> 'b::t1_space"
lp15@66884
  1426
  shows "continuous_on S f \<Longrightarrow> closedin (subtopology euclidean S) {x \<in> S. f x = a}"
lp15@66884
  1427
  using continuous_closedin_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)
lp15@66827
  1428
lp15@66827
  1429
lemma continuous_closed_preimage_constant:
lp15@66827
  1430
  fixes f :: "_ \<Rightarrow> 'b::t1_space"
lp15@66884
  1431
  shows "continuous_on S f \<Longrightarrow> closed S \<Longrightarrow> closed {x \<in> S. f x = a}"
lp15@66884
  1432
  using continuous_closed_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)
lp15@66827
  1433
lp15@66827
  1434
lemma continuous_constant_on_closure:
lp15@66827
  1435
  fixes f :: "_ \<Rightarrow> 'b::t1_space"
lp15@66827
  1436
  assumes "continuous_on (closure S) f"
lp15@66827
  1437
      and "\<And>x. x \<in> S \<Longrightarrow> f x = a"
lp15@66827
  1438
      and "x \<in> closure S"
lp15@66827
  1439
  shows "f x = a"
lp15@66827
  1440
    using continuous_closed_preimage_constant[of "closure S" f a]
lp15@66827
  1441
      assms closure_minimal[of S "{x \<in> closure S. f x = a}"] closure_subset
lp15@66827
  1442
    unfolding subset_eq
lp15@66827
  1443
    by auto
lp15@66827
  1444
lp15@66827
  1445
lemma image_closure_subset:
lp15@66884
  1446
  assumes contf: "continuous_on (closure S) f"
lp15@66884
  1447
    and "closed T"
lp15@66884
  1448
    and "(f ` S) \<subseteq> T"
lp15@66884
  1449
  shows "f ` (closure S) \<subseteq> T"
lp15@66827
  1450
proof -
lp15@66884
  1451
  have "S \<subseteq> {x \<in> closure S. f x \<in> T}"
lp15@66827
  1452
    using assms(3) closure_subset by auto
lp15@66884
  1453
  moreover have "closed (closure S \<inter> f -` T)"
lp15@66884
  1454
    using continuous_closed_preimage[OF contf] \<open>closed T\<close> by auto
lp15@66884
  1455
  ultimately have "closure S = (closure S \<inter> f -` T)"
lp15@66884
  1456
    using closure_minimal[of S "(closure S \<inter> f -` T)"] by auto
lp15@66827
  1457
  then show ?thesis by auto
lp15@66827
  1458
qed
lp15@66827
  1459
lp15@66827
  1460
lemma continuous_on_closure_norm_le:
lp15@66827
  1461
  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
lp15@66827
  1462
  assumes "continuous_on (closure s) f"
lp15@66827
  1463
    and "\<forall>y \<in> s. norm(f y) \<le> b"
lp15@66827
  1464
    and "x \<in> (closure s)"
lp15@66827
  1465
  shows "norm (f x) \<le> b"
lp15@66827
  1466
proof -
lp15@66827
  1467
  have *: "f ` s \<subseteq> cball 0 b"
lp15@66827
  1468
    using assms(2)[unfolded mem_cball_0[symmetric]] by auto
lp15@66827
  1469
  show ?thesis
lp15@66835
  1470
    by (meson "*" assms(1) assms(3) closed_cball image_closure_subset image_subset_iff mem_cball_0)
lp15@66827
  1471
qed
lp15@66827
  1472
lp15@66827
  1473
lemma isCont_indicator:
lp15@66827
  1474
  fixes x :: "'a::t2_space"
lp15@66827
  1475
  shows "isCont (indicator A :: 'a \<Rightarrow> real) x = (x \<notin> frontier A)"
lp15@66827
  1476
proof auto
lp15@66827
  1477
  fix x
lp15@66827
  1478
  assume cts_at: "isCont (indicator A :: 'a \<Rightarrow> real) x" and fr: "x \<in> frontier A"
lp15@66827
  1479
  with continuous_at_open have 1: "\<forall>V::real set. open V \<and> indicator A x \<in> V \<longrightarrow>
lp15@66827
  1480
    (\<exists>U::'a set. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> V))" by auto
lp15@66827
  1481
  show False
lp15@66827
  1482
  proof (cases "x \<in> A")
lp15@66827
  1483
    assume x: "x \<in> A"
lp15@66827
  1484
    hence "indicator A x \<in> ({0<..<2} :: real set)" by simp
lp15@66827
  1485
    hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({0<..<2} :: real set))"
lp15@66827
  1486
      using 1 open_greaterThanLessThan by blast
lp15@66827
  1487
    then guess U .. note U = this
lp15@66827
  1488
    hence "\<forall>y\<in>U. indicator A y > (0::real)"
lp15@66827
  1489
      unfolding greaterThanLessThan_def by auto
lp15@66827
  1490
    hence "U \<subseteq> A" using indicator_eq_0_iff by force
lp15@66827
  1491
    hence "x \<in> interior A" using U interiorI by auto
lp15@66827
  1492
    thus ?thesis using fr unfolding frontier_def by simp
lp15@66827
  1493
  next
lp15@66827
  1494
    assume x: "x \<notin> A"
lp15@66827
  1495
    hence "indicator A x \<in> ({-1<..<1} :: real set)" by simp
lp15@66827
  1496
    hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({-1<..<1} :: real set))"
lp15@66827
  1497
      using 1 open_greaterThanLessThan by blast
lp15@66827
  1498
    then guess U .. note U = this
lp15@66827
  1499
    hence "\<forall>y\<in>U. indicator A y < (1::real)"
lp15@66827
  1500
      unfolding greaterThanLessThan_def by auto
lp15@66827
  1501
    hence "U \<subseteq> -A" by auto
lp15@66827
  1502
    hence "x \<in> interior (-A)" using U interiorI by auto
lp15@66827
  1503
    thus ?thesis using fr interior_complement unfolding frontier_def by auto
lp15@66827
  1504
  qed
lp15@66827
  1505
next
lp15@66827
  1506
  assume nfr: "x \<notin> frontier A"
lp15@66827
  1507
  hence "x \<in> interior A \<or> x \<in> interior (-A)"
lp15@66827
  1508
    by (auto simp: frontier_def closure_interior)
lp15@66827
  1509
  thus "isCont ((indicator A)::'a \<Rightarrow> real) x"
lp15@66827
  1510
  proof
lp15@66827
  1511
    assume int: "x \<in> interior A"
lp15@66827
  1512
    then obtain U where U: "open U" "x \<in> U" "U \<subseteq> A" unfolding interior_def by auto
lp15@66827
  1513
    hence "\<forall>y\<in>U. indicator A y = (1::real)" unfolding indicator_def by auto
lp15@66827
  1514
    hence "continuous_on U (indicator A)" by (simp add: continuous_on_const indicator_eq_1_iff)
lp15@66827
  1515
    thus ?thesis using U continuous_on_eq_continuous_at by auto
lp15@66827
  1516
  next
lp15@66827
  1517
    assume ext: "x \<in> interior (-A)"
lp15@66827
  1518
    then obtain U where U: "open U" "x \<in> U" "U \<subseteq> -A" unfolding interior_def by auto
lp15@66827
  1519
    then have "continuous_on U (indicator A)"
lp15@66827
  1520
      using continuous_on_topological by (auto simp: subset_iff)
lp15@66827
  1521
    thus ?thesis using U continuous_on_eq_continuous_at by auto
lp15@66827
  1522
  qed
lp15@66827
  1523
qed
lp15@66827
  1524
lp15@66827
  1525
subsection \<open>A function constant on a set\<close>
lp15@66827
  1526
lp15@66827
  1527
definition constant_on  (infixl "(constant'_on)" 50)
lp15@66827
  1528
  where "f constant_on A \<equiv> \<exists>y. \<forall>x\<in>A. f x = y"
lp15@66827
  1529
lp15@66827
  1530
lemma constant_on_subset: "\<lbrakk>f constant_on A; B \<subseteq> A\<rbrakk> \<Longrightarrow> f constant_on B"
lp15@66827
  1531
  unfolding constant_on_def by blast
lp15@66827
  1532
lp15@66827
  1533
lemma injective_not_constant:
lp15@66827
  1534
  fixes S :: "'a::{perfect_space} set"
lp15@66827
  1535
  shows "\<lbrakk>open S; inj_on f S; f constant_on S\<rbrakk> \<Longrightarrow> S = {}"
lp15@66827
  1536
unfolding constant_on_def
lp15@66827
  1537
by (metis equals0I inj_on_contraD islimpt_UNIV islimpt_def)
lp15@66827
  1538
lp15@66827
  1539
lemma constant_on_closureI:
lp15@66827
  1540
  fixes f :: "_ \<Rightarrow> 'b::t1_space"
lp15@66827
  1541
  assumes cof: "f constant_on S" and contf: "continuous_on (closure S) f"
lp15@66827
  1542
    shows "f constant_on (closure S)"
lp15@66827
  1543
using continuous_constant_on_closure [OF contf] cof unfolding constant_on_def
lp15@66827
  1544
by metis
lp15@66827
  1545
lp15@66827
  1546
subsection\<open>Relating linear images to open/closed/interior/closure\<close>
lp15@66827
  1547
lp15@66827
  1548
proposition open_surjective_linear_image:
lp15@66827
  1549
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
lp15@66827
  1550
  assumes "open A" "linear f" "surj f"
lp15@66827
  1551
    shows "open(f ` A)"
lp15@66827
  1552
unfolding open_dist
lp15@66827
  1553
proof clarify
lp15@66827
  1554
  fix x
lp15@66827
  1555
  assume "x \<in> A"
lp15@66827
  1556
  have "bounded (inv f ` Basis)"
lp15@66827
  1557
    by (simp add: finite_imp_bounded)
lp15@66827
  1558
  with bounded_pos obtain B where "B > 0" and B: "\<And>x. x \<in> inv f ` Basis \<Longrightarrow> norm x \<le> B"
lp15@66827
  1559
    by metis
lp15@66827
  1560
  obtain e where "e > 0" and e: "\<And>z. dist z x < e \<Longrightarrow> z \<in> A"
lp15@66827
  1561
    by (metis open_dist \<open>x \<in> A\<close> \<open>open A\<close>)
lp15@66827
  1562
  define \<delta> where "\<delta> \<equiv> e / B / DIM('b)"
lp15@66827
  1563
  show "\<exists>e>0. \<forall>y. dist y (f x) < e \<longrightarrow> y \<in> f ` A"
lp15@66827
  1564
  proof (intro exI conjI)
lp15@66827
  1565
    show "\<delta> > 0"
lp15@66827
  1566
      using \<open>e > 0\<close> \<open>B > 0\<close>  by (simp add: \<delta>_def divide_simps)
lp15@66827
  1567
    have "y \<in> f ` A" if "dist y (f x) * (B * real DIM('b)) < e" for y
lp15@66827
  1568
    proof -
lp15@66827
  1569
      define u where "u \<equiv> y - f x"
lp15@66827
  1570
      show ?thesis
lp15@66827
  1571
      proof (rule image_eqI)
lp15@66827
  1572
        show "y = f (x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i))"
lp15@66827
  1573
          apply (simp add: linear_add linear_sum linear.scaleR \<open>linear f\<close> surj_f_inv_f \<open>surj f\<close>)
lp15@66827
  1574
          apply (simp add: euclidean_representation u_def)
lp15@66827
  1575
          done
lp15@66827
  1576
        have "dist (x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i)) x \<le> (\<Sum>i\<in>Basis. norm ((u \<bullet> i) *\<^sub>R inv f i))"
lp15@66827
  1577
          by (simp add: dist_norm sum_norm_le)
lp15@66827
  1578
        also have "... = (\<Sum>i\<in>Basis. \<bar>u \<bullet> i\<bar> * norm (inv f i))"
lp15@66827
  1579
          by simp
lp15@66827
  1580
        also have "... \<le> (\<Sum>i\<in>Basis. \<bar>u \<bullet> i\<bar>) * B"
lp15@66827
  1581
          by (simp add: B sum_distrib_right sum_mono mult_left_mono)
lp15@66827
  1582
        also have "... \<le> DIM('b) * dist y (f x) * B"
lp15@66827
  1583
          apply (rule mult_right_mono [OF sum_bounded_above])
lp15@66827
  1584
          using \<open>0 < B\<close> by (auto simp: Basis_le_norm dist_norm u_def)
lp15@66827
  1585
        also have "... < e"
lp15@66827
  1586
          by (metis mult.commute mult.left_commute that)
lp15@66827
  1587
        finally show "x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i) \<in> A"
lp15@66827
  1588
          by (rule e)
lp15@66827
  1589
      qed
lp15@66827
  1590
    qed
lp15@66827
  1591
    then show "\<forall>y. dist y (f x) < \<delta> \<longrightarrow> y \<in> f ` A"
lp15@66827
  1592
      using \<open>e > 0\<close> \<open>B > 0\<close>
lp15@66827
  1593
      by (auto simp: \<delta>_def divide_simps mult_less_0_iff)
lp15@66827
  1594
  qed
lp15@66827
  1595
qed
lp15@66827
  1596
lp15@66827
  1597
corollary open_bijective_linear_image_eq:
lp15@66827
  1598
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
lp15@66827
  1599
  assumes "linear f" "bij f"
lp15@66827
  1600
    shows "open(f ` A) \<longleftrightarrow> open A"
lp15@66827
  1601
proof
lp15@66827
  1602
  assume "open(f ` A)"
lp15@66827
  1603
  then have "open(f -` (f ` A))"
lp15@66827
  1604
    using assms by (force simp: linear_continuous_at linear_conv_bounded_linear continuous_open_vimage)
lp15@66827
  1605
  then show "open A"
lp15@66827
  1606
    by (simp add: assms bij_is_inj inj_vimage_image_eq)
lp15@66827
  1607
next
lp15@66827
  1608
  assume "open A"
lp15@66827
  1609
  then show "open(f ` A)"
lp15@66827
  1610
    by (simp add: assms bij_is_surj open_surjective_linear_image)
lp15@66827
  1611
qed
lp15@66827
  1612
lp15@66827
  1613
corollary interior_bijective_linear_image:
lp15@66827
  1614
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
lp15@66827
  1615
  assumes "linear f" "bij f"
lp15@66827
  1616
  shows "interior (f ` S) = f ` interior S"  (is "?lhs = ?rhs")
lp15@66827
  1617
proof safe
lp15@66827
  1618
  fix x
lp15@66827
  1619
  assume x: "x \<in> ?lhs"
lp15@66827
  1620
  then obtain T where "open T" and "x \<in> T" and "T \<subseteq> f ` S"
lp15@66827
  1621
    by (metis interiorE)
lp15@66827
  1622
  then show "x \<in> ?rhs"
lp15@66827
  1623
    by (metis (no_types, hide_lams) assms subsetD interior_maximal open_bijective_linear_image_eq subset_image_iff)
lp15@66827
  1624
next
lp15@66827
  1625
  fix x
lp15@66827
  1626
  assume x: "x \<in> interior S"
lp15@66827
  1627
  then show "f x \<in> interior (f ` S)"
lp15@66827
  1628
    by (meson assms imageI image_mono interiorI interior_subset open_bijective_linear_image_eq open_interior)
lp15@66827
  1629
qed
lp15@66827
  1630
lp15@66827
  1631
lemma interior_injective_linear_image:
lp15@66827
  1632
  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
lp15@66827
  1633
  assumes "linear f" "inj f"
lp15@66827
  1634
   shows "interior(f ` S) = f ` (interior S)"
lp15@66827
  1635
  by (simp add: linear_injective_imp_surjective assms bijI interior_bijective_linear_image)
lp15@66827
  1636
lp15@66827
  1637
lemma interior_surjective_linear_image:
lp15@66827
  1638
  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
lp15@66827
  1639
  assumes "linear f" "surj f"
lp15@66827
  1640
   shows "interior(f ` S) = f ` (interior S)"
lp15@66827
  1641
  by (simp add: assms interior_injective_linear_image linear_surjective_imp_injective)
lp15@66827
  1642
lp15@66827
  1643
lemma interior_negations:
lp15@66827
  1644
  fixes S :: "'a::euclidean_space set"
lp15@66827
  1645
  shows "interior(uminus ` S) = image uminus (interior S)"
lp15@66827
  1646
  by (simp add: bij_uminus interior_bijective_linear_image linear_uminus)
lp15@66827
  1647
lp15@66827
  1648
text \<open>Preservation of compactness and connectedness under continuous function.\<close>
lp15@66827
  1649
lp15@66827
  1650
lemma compact_eq_openin_cover:
lp15@66827
  1651
  "compact S \<longleftrightarrow>
lp15@66827
  1652
    (\<forall>C. (\<forall>c\<in>C. openin (subtopology euclidean S) c) \<and> S \<subseteq> \<Union>C \<longrightarrow>
lp15@66827
  1653
      (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
lp15@66827
  1654
proof safe
lp15@66827
  1655
  fix C
lp15@66827
  1656
  assume "compact S" and "\<forall>c\<in>C. openin (subtopology euclidean S) c" and "S \<subseteq> \<Union>C"
lp15@66827
  1657
  then have "\<forall>c\<in>{T. open T \<and> S \<inter> T \<in> C}. open c" and "S \<subseteq> \<Union>{T. open T \<and> S \<inter> T \<in> C}"
lp15@66827
  1658
    unfolding openin_open by force+
lp15@66827
  1659
  with \<open>compact S\<close> obtain D where "D \<subseteq> {T. open T \<and> S \<inter> T \<in> C}" and "finite D" and "S \<subseteq> \<Union>D"
lp15@66827
  1660
    by (meson compactE)
lp15@66827
  1661
  then have "image (\<lambda>T. S \<inter> T) D \<subseteq> C \<and> finite (image (\<lambda>T. S \<inter> T) D) \<and> S \<subseteq> \<Union>(image (\<lambda>T. S \<inter> T) D)"
lp15@66827
  1662
    by auto
lp15@66827
  1663
  then show "\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D" ..
lp15@66827
  1664
next
lp15@66827
  1665
  assume 1: "\<forall>C. (\<forall>c\<in>C. openin (subtopology euclidean S) c) \<and> S \<subseteq> \<Union>C \<longrightarrow>
lp15@66827
  1666
        (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D)"
lp15@66827
  1667
  show "compact S"
lp15@66827
  1668
  proof (rule compactI)
lp15@66827
  1669
    fix C
lp15@66827
  1670
    let ?C = "image (\<lambda>T. S \<inter> T) C"
lp15@66827
  1671
    assume "\<forall>t\<in>C. open t" and "S \<subseteq> \<Union>C"
lp15@66827
  1672
    then have "(\<forall>c\<in>?C. openin (subtopology euclidean S) c) \<and> S \<subseteq> \<Union>?C"
lp15@66827
  1673
      unfolding openin_open by auto
lp15@66827
  1674
    with 1 obtain D where "D \<subseteq> ?C" and "finite D" and "S \<subseteq> \<Union>D"
lp15@66827
  1675
      by metis
lp15@66827
  1676
    let ?D = "inv_into C (\<lambda>T. S \<inter> T) ` D"
lp15@66827
  1677
    have "?D \<subseteq> C \<and> finite ?D \<and> S \<subseteq> \<Union>?D"
lp15@66827
  1678
    proof (intro conjI)
lp15@66827
  1679
      from \<open>D \<subseteq> ?C\<close> show "?D \<subseteq> C"
lp15@66827
  1680
        by (fast intro: inv_into_into)
lp15@66827
  1681
      from \<open>finite D\<close> show "finite ?D"
lp15@66827
  1682
        by (rule finite_imageI)
lp15@66827
  1683
      from \<open>S \<subseteq> \<Union>D\<close> show "S \<subseteq> \<Union>?D"
lp15@66827
  1684
        apply (rule subset_trans, clarsimp)
lp15@66827
  1685
        apply (frule subsetD [OF \<open>D \<subseteq> ?C\<close>, THEN f_inv_into_f])
lp15@66827
  1686
        apply (erule rev_bexI, fast)
lp15@66827
  1687
        done
lp15@66827
  1688
    qed
lp15@66827
  1689
    then show "\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D" ..
lp15@66827
  1690
  qed
lp15@66827
  1691
qed
lp15@66827
  1692
lp15@66827
  1693
subsection\<open> Theorems relating continuity and uniform continuity to closures\<close>
lp15@66827
  1694
lp15@66827
  1695
lemma continuous_on_closure:
lp15@66827
  1696
   "continuous_on (closure S) f \<longleftrightarrow>
lp15@66827
  1697
    (\<forall>x e. x \<in> closure S \<and> 0 < e
lp15@66827
  1698
           \<longrightarrow> (\<exists>d. 0 < d \<and> (\<forall>y. y \<in> S \<and> dist y x < d \<longrightarrow> dist (f y) (f x) < e)))"
lp15@66827
  1699
   (is "?lhs = ?rhs")
lp15@66827
  1700
proof
lp15@66827
  1701
  assume ?lhs then show ?rhs
lp15@66827
  1702
    unfolding continuous_on_iff  by (metis Un_iff closure_def)
lp15@66827
  1703
next
lp15@66827
  1704
  assume R [rule_format]: ?rhs
lp15@66827
  1705
  show ?lhs
lp15@66827
  1706
  proof
lp15@66827
  1707
    fix x and e::real
lp15@66827
  1708
    assume "0 < e" and x: "x \<in> closure S"
lp15@66827
  1709
    obtain \<delta>::real where "\<delta> > 0"
lp15@66827
  1710
                   and \<delta>: "\<And>y. \<lbrakk>y \<in> S; dist y x < \<delta>\<rbrakk> \<Longrightarrow> dist (f y) (f x) < e/2"
lp15@66827
  1711
      using R [of x "e/2"] \<open>0 < e\<close> x by auto
lp15@66827
  1712
    have "dist (f y) (f x) \<le> e" if y: "y \<in> closure S" and dyx: "dist y x < \<delta>/2" for y
lp15@66827
  1713
    proof -
lp15@66827
  1714
      obtain \<delta>'::real where "\<delta>' > 0"
lp15@66827
  1715
                      and \<delta>': "\<And>z. \<lbrakk>z \<in> S; dist z y < \<delta>'\<rbrakk> \<Longrightarrow> dist (f z) (f y) < e/2"
lp15@66827
  1716
        using R [of y "e/2"] \<open>0 < e\<close> y by auto
lp15@66827
  1717
      obtain z where "z \<in> S" and z: "dist z y < min \<delta>' \<delta> / 2"
lp15@66827
  1718
        using closure_approachable y
lp15@66827
  1719
        by (metis \<open>0 < \<delta>'\<close> \<open>0 < \<delta>\<close> divide_pos_pos min_less_iff_conj zero_less_numeral)
lp15@66827
  1720
      have "dist (f z) (f y) < e/2"
lp15@66827
  1721
        apply (rule \<delta>' [OF \<open>z \<in> S\<close>])
lp15@66827
  1722
        using z \<open>0 < \<delta>'\<close> by linarith
lp15@66827
  1723
      moreover have "dist (f z) (f x) < e/2"
lp15@66827
  1724
        apply (rule \<delta> [OF \<open>z \<in> S\<close>])
lp15@66827
  1725
        using z \<open>0 < \<delta>\<close>  dist_commute[of y z] dist_triangle_half_r [of y] dyx by auto
lp15@66827
  1726
      ultimately show ?thesis
lp15@66827
  1727
        by (metis dist_commute dist_triangle_half_l less_imp_le)
lp15@66827
  1728
    qed
lp15@66827
  1729
    then show "\<exists>d>0. \<forall>x'\<in>closure S. dist x' x < d \<longrightarrow> dist (f x') (f x) \<le> e"
lp15@66827
  1730
      by (rule_tac x="\<delta>/2" in exI) (simp add: \<open>\<delta> > 0\<close>)
lp15@66827
  1731
  qed
lp15@66827
  1732
qed
lp15@66827
  1733
lp15@66827
  1734
lemma continuous_on_closure_sequentially:
lp15@66827
  1735
  fixes f :: "'a::metric_space \<Rightarrow> 'b :: metric_space"
lp15@66827
  1736
  shows
lp15@66827
  1737
   "continuous_on (closure S) f \<longleftrightarrow>
lp15@66827
  1738
    (\<forall>x a. a \<in> closure S \<and> (\<forall>n. x n \<in> S) \<and> x \<longlonglongrightarrow> a \<longrightarrow> (f \<circ> x) \<longlonglongrightarrow> f a)"
lp15@66827
  1739
   (is "?lhs = ?rhs")
lp15@66827
  1740
proof -
lp15@66827
  1741
  have "continuous_on (closure S) f \<longleftrightarrow>
lp15@66827
  1742
           (\<forall>x \<in> closure S. continuous (at x within S) f)"
lp15@66827
  1743
    by (force simp: continuous_on_closure continuous_within_eps_delta)
lp15@66827
  1744
  also have "... = ?rhs"
lp15@66827
  1745
    by (force simp: continuous_within_sequentially)
lp15@66827
  1746
  finally show ?thesis .
lp15@66827
  1747
qed
lp15@66827
  1748
lp15@66827
  1749
lemma uniformly_continuous_on_closure:
lp15@66827
  1750
  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
lp15@66827
  1751
  assumes ucont: "uniformly_continuous_on S f"
lp15@66827
  1752
      and cont: "continuous_on (closure S) f"
lp15@66827
  1753
    shows "uniformly_continuous_on (closure S) f"
lp15@66827
  1754
unfolding uniformly_continuous_on_def
lp15@66827
  1755
proof (intro allI impI)
lp15@66827
  1756
  fix e::real
lp15@66827
  1757
  assume "0 < e"
lp15@66827
  1758
  then obtain d::real
lp15@66827
  1759
    where "d>0"
lp15@66827
  1760
      and d: "\<And>x x'. \<lbrakk>x\<in>S; x'\<in>S; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e/3"
lp15@66827
  1761
    using ucont [unfolded uniformly_continuous_on_def, rule_format, of "e/3"] by auto
lp15@66827
  1762
  show "\<exists>d>0. \<forall>x\<in>closure S. \<forall>x'\<in>closure S. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
lp15@66827
  1763
  proof (rule exI [where x="d/3"], clarsimp simp: \<open>d > 0\<close>)
lp15@66827
  1764
    fix x y
lp15@66827
  1765
    assume x: "x \<in> closure S" and y: "y \<in> closure S" and dyx: "dist y x * 3 < d"
lp15@66827
  1766
    obtain d1::real where "d1 > 0"
lp15@66827
  1767
           and d1: "\<And>w. \<lbrakk>w \<in> closure S; dist w x < d1\<rbrakk> \<Longrightarrow> dist (f w) (f x) < e/3"
lp15@66827
  1768
      using cont [unfolded continuous_on_iff, rule_format, of "x" "e/3"] \<open>0 < e\<close> x by auto
lp15@66827
  1769
     obtain x' where "x' \<in> S" and x': "dist x' x < min d1 (d / 3)"
lp15@66827
  1770
        using closure_approachable [of x S]
lp15@66827
  1771
        by (metis \<open>0 < d1\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj x zero_less_numeral)
lp15@66827
  1772
    obtain d2::real where "d2 > 0"
lp15@66827
  1773
           and d2: "\<forall>w \<in> closure S. dist w y < d2 \<longrightarrow> dist (f w) (f y) < e/3"
lp15@66827
  1774
      using cont [unfolded continuous_on_iff, rule_format, of "y" "e/3"] \<open>0 < e\<close> y by auto
lp15@66827
  1775
     obtain y' where "y' \<in> S" and y': "dist y' y < min d2 (d / 3)"
lp15@66827
  1776
        using closure_approachable [of y S]
lp15@66827
  1777
        by (metis \<open>0 < d2\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj y zero_less_numeral)
lp15@66827
  1778
     have "dist x' x < d/3" using x' by auto
lp15@66827
  1779
     moreover have "dist x y < d/3"
lp15@66827
  1780
       by (metis dist_commute dyx less_divide_eq_numeral1(1))
lp15@66827
  1781
     moreover have "dist y y' < d/3"
lp15@66827
  1782
       by (metis (no_types) dist_commute min_less_iff_conj y')
lp15@66827
  1783
     ultimately have "dist x' y' < d/3 + d/3 + d/3"
lp15@66827
  1784
       by (meson dist_commute_lessI dist_triangle_lt add_strict_mono)
lp15@66827
  1785
     then have "dist x' y' < d" by simp
lp15@66827
  1786
     then have "dist (f x') (f y') < e/3"
lp15@66827
  1787
       by (rule d [OF \<open>y' \<in> S\<close> \<open>x' \<in> S\<close>])
lp15@66827
  1788
     moreover have "dist (f x') (f x) < e/3" using \<open>x' \<in> S\<close> closure_subset x' d1
lp15@66827
  1789
       by (simp add: closure_def)
lp15@66827
  1790
     moreover have "dist (f y') (f y) < e/3" using \<open>y' \<in> S\<close> closure_subset y' d2
lp15@66827
  1791
       by (simp add: closure_def)
lp15@66827
  1792
     ultimately have "dist (f y) (f x) < e/3 + e/3 + e/3"
lp15@66827
  1793
       by (meson dist_commute_lessI dist_triangle_lt add_strict_mono)
lp15@66827
  1794
    then show "dist (f y) (f x) < e" by simp
lp15@66827
  1795
  qed
lp15@66827
  1796
qed
lp15@66827
  1797
lp15@66827
  1798
lemma uniformly_continuous_on_extension_at_closure:
lp15@66827
  1799
  fixes f::"'a::metric_space \<Rightarrow> 'b::complete_space"
lp15@66827
  1800
  assumes uc: "uniformly_continuous_on X f"
lp15@66827
  1801
  assumes "x \<in> closure X"
lp15@66827
  1802
  obtains l where "(f \<longlongrightarrow> l) (at x within X)"
lp15@66827
  1803
proof -
lp15@66827
  1804
  from assms obtain xs where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X"
lp15@66827
  1805
    by (auto simp: closure_sequential)
lp15@66827
  1806
lp15@66827
  1807
  from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF xs]
lp15@66827
  1808
  obtain l where l: "(\<lambda>n. f (xs n)) \<longlonglongrightarrow> l"
lp15@66827
  1809
    by atomize_elim (simp only: convergent_eq_Cauchy)
lp15@66827
  1810
lp15@66827
  1811
  have "(f \<longlongrightarrow> l) (at x within X)"
lp15@66827
  1812
  proof (safe intro!: Lim_within_LIMSEQ)
lp15@66827
  1813
    fix xs'
lp15@66827
  1814
    assume "\<forall>n. xs' n \<noteq> x \<and> xs' n \<in> X"
lp15@66827
  1815
      and xs': "xs' \<longlonglongrightarrow> x"
lp15@66827
  1816
    then have "xs' n \<noteq> x" "xs' n \<in> X" for n by auto
lp15@66827
  1817
lp15@66827
  1818
    from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF \<open>xs' \<longlonglongrightarrow> x\<close> \<open>xs' _ \<in> X\<close>]
lp15@66827
  1819
    obtain l' where l': "(\<lambda>n. f (xs' n)) \<longlonglongrightarrow> l'"
lp15@66827
  1820
      by atomize_elim (simp only: convergent_eq_Cauchy)
lp15@66827
  1821
lp15@66827
  1822
    show "(\<lambda>n. f (xs' n)) \<longlonglongrightarrow> l"
lp15@66827
  1823
    proof (rule tendstoI)
lp15@66827
  1824
      fix e::real assume "e > 0"
lp15@66827
  1825
      define e' where "e' \<equiv> e / 2"
lp15@66827
  1826
      have "e' > 0" using \<open>e > 0\<close> by (simp add: e'_def)
lp15@66827
  1827
lp15@66827
  1828
      have "\<forall>\<^sub>F n in sequentially. dist (f (xs n)) l < e'"
lp15@66827
  1829
        by (simp add: \<open>0 < e'\<close> l tendstoD)
lp15@66827
  1830
      moreover
lp15@66827
  1831
      from uc[unfolded uniformly_continuous_on_def, rule_format, OF \<open>e' > 0\<close>]
lp15@66827
  1832
      obtain d where d: "d > 0" "\<And>x x'. x \<in> X \<Longrightarrow> x' \<in> X \<Longrightarrow> dist x x' < d \<Longrightarrow> dist (f x) (f x') < e'"
lp15@66827
  1833
        by auto
lp15@66827
  1834
      have "\<forall>\<^sub>F n in sequentially. dist (xs n) (xs' n) < d"
lp15@66827
  1835
        by (auto intro!: \<open>0 < d\<close> order_tendstoD tendsto_eq_intros xs xs')
lp15@66827
  1836
      ultimately
lp15@66827
  1837
      show "\<forall>\<^sub>F n in sequentially. dist (f (xs' n)) l < e"
lp15@66827
  1838
      proof eventually_elim
lp15@66827
  1839
        case (elim n)
lp15@66827
  1840
        have "dist (f (xs' n)) l \<le> dist (f (xs n)) (f (xs' n)) + dist (f (xs n)) l"
lp15@66827
  1841
          by (metis dist_triangle dist_commute)
lp15@66827
  1842
        also have "dist (f (xs n)) (f (xs' n)) < e'"
lp15@66827
  1843
          by (auto intro!: d xs \<open>xs' _ \<in> _\<close> elim)
lp15@66827
  1844
        also note \<open>dist (f (xs n)) l < e'\<close>
lp15@66827
  1845
        also have "e' + e' = e" by (simp add: e'_def)
lp15@66827
  1846
        finally show ?case by simp
lp15@66827
  1847
      qed
lp15@66827
  1848
    qed
lp15@66827
  1849
  qed
lp15@66827
  1850
  thus ?thesis ..
lp15@66827
  1851
qed
lp15@66827
  1852
lp15@66827
  1853
lemma uniformly_continuous_on_extension_on_closure:
lp15@66827
  1854
  fixes f::"'a::metric_space \<Rightarrow> 'b::complete_space"
lp15@66827
  1855
  assumes uc: "uniformly_continuous_on X f"
lp15@66827
  1856
  obtains g where "uniformly_continuous_on (closure X) g" "\<And>x. x \<in> X \<Longrightarrow> f x = g x"
lp15@66827
  1857
    "\<And>Y h x. X \<subseteq> Y \<Longrightarrow> Y \<subseteq> closure X \<Longrightarrow> continuous_on Y h \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> f x = h x) \<Longrightarrow> x \<in> Y \<Longrightarrow> h x = g x"
lp15@66827
  1858
proof -
lp15@66827
  1859
  from uc have cont_f: "continuous_on X f"
lp15@66827
  1860
    by (simp add: uniformly_continuous_imp_continuous)
lp15@66827
  1861
  obtain y where y: "(f \<longlongrightarrow> y x) (at x within X)" if "x \<in> closure X" for x
lp15@66827
  1862
    apply atomize_elim
lp15@66827
  1863
    apply (rule choice)
lp15@66827
  1864
    using uniformly_continuous_on_extension_at_closure[OF assms]
lp15@66827
  1865
    by metis
lp15@66827
  1866
  let ?g = "\<lambda>x. if x \<in> X then f x else y x"
lp15@66827
  1867
lp15@66827
  1868
  have "uniformly_continuous_on (closure X) ?g"
lp15@66827
  1869
    unfolding uniformly_continuous_on_def
lp15@66827
  1870
  proof safe
lp15@66827
  1871
    fix e::real assume "e > 0"
lp15@66827
  1872
    define e' where "e' \<equiv> e / 3"
lp15@66827
  1873
    have "e' > 0" using \<open>e > 0\<close> by (simp add: e'_def)
lp15@66827
  1874
    from uc[unfolded uniformly_continuous_on_def, rule_format, OF \<open>0 < e'\<close>]
lp15@66827
  1875
    obtain d where "d > 0" and d: "\<And>x x'. x \<in> X \<Longrightarrow> x' \<in> X \<Longrightarrow> dist x' x < d \<Longrightarrow> dist (f x') (f x) < e'"
lp15@66827
  1876
      by auto
lp15@66827
  1877
    define d' where "d' = d / 3"
lp15@66827
  1878
    have "d' > 0" using \<open>d > 0\<close> by (simp add: d'_def)
lp15@66827
  1879
    show "\<exists>d>0. \<forall>x\<in>closure X. \<forall>x'\<in>closure X. dist x' x < d \<longrightarrow> dist (?g x') (?g x) < e"
lp15@66827
  1880
    proof (safe intro!: exI[where x=d'] \<open>d' > 0\<close>)
lp15@66827
  1881
      fix x x' assume x: "x \<in> closure X" and x': "x' \<in> closure X" and dist: "dist x' x < d'"
lp15@66827
  1882
      then obtain xs xs' where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X"
lp15@66827
  1883
        and xs': "xs' \<longlonglongrightarrow> x'" "\<And>n. xs' n \<in> X"
lp15@66827
  1884
        by (auto simp: closure_sequential)
lp15@66827
  1885
      have "\<forall>\<^sub>F n in sequentially. dist (xs' n) x' < d'"
lp15@66827
  1886
        and "\<forall>\<^sub>F n in sequentially. dist (xs n) x < d'"
lp15@66827
  1887
        by (auto intro!: \<open>0 < d'\<close> order_tendstoD tendsto_eq_intros xs xs')
lp15@66827
  1888
      moreover
lp15@66827
  1889
      have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> y x" if "x \<in> closure X" "x \<notin> X" "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X" for xs x
lp15@66827
  1890
        using that not_eventuallyD
lp15@66827
  1891
        by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at)
lp15@66827
  1892
      then have "(\<lambda>x. f (xs' x)) \<longlonglongrightarrow> ?g x'" "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> ?g x"
lp15@66827
  1893
        using x x'
lp15@66827
  1894
        by (auto intro!: continuous_on_tendsto_compose[OF cont_f] simp: xs' xs)
lp15@66827
  1895
      then have "\<forall>\<^sub>F n in sequentially. dist (f (xs' n)) (?g x') < e'"
lp15@66827
  1896
        "\<forall>\<^sub>F n in sequentially. dist (f (xs n)) (?g x) < e'"
lp15@66827
  1897
        by (auto intro!: \<open>0 < e'\<close> order_tendstoD tendsto_eq_intros)
lp15@66827
  1898
      ultimately
lp15@66827
  1899
      have "\<forall>\<^sub>F n in sequentially. dist (?g x') (?g x) < e"
lp15@66827
  1900
      proof eventually_elim
lp15@66827
  1901
        case (elim n)
lp15@66827
  1902
        have "dist (?g x') (?g x) \<le>
lp15@66827
  1903
          dist (f (xs' n)) (?g x') + dist (f (xs' n)) (f (xs n)) + dist (f (xs n)) (?g x)"
lp15@66827
  1904
          by (metis add.commute add_le_cancel_left dist_commute dist_triangle dist_triangle_le)
lp15@66827
  1905
        also
lp15@66827
  1906
        {
lp15@66827
  1907
          have "dist (xs' n) (xs n) \<le> dist (xs' n) x' + dist x' x + dist (xs n) x"
lp15@66827
  1908
            by (metis add.commute add_le_cancel_left  dist_triangle dist_triangle_le)
lp15@66827
  1909
          also note \<open>dist (xs' n) x' < d'\<close>
lp15@66827
  1910
          also note \<open>dist x' x < d'\<close>
lp15@66827
  1911
          also note \<open>dist (xs n) x < d'\<close>
lp15@66827
  1912
          finally have "dist (xs' n) (xs n) < d" by (simp add: d'_def)
lp15@66827
  1913
        }
lp15@66827
  1914
        with \<open>xs _ \<in> X\<close> \<open>xs' _ \<in> X\<close> have "dist (f (xs' n)) (f (xs n)) < e'"
lp15@66827
  1915
          by (rule d)
lp15@66827
  1916
        also note \<open>dist (f (xs' n)) (?g x') < e'\<close>
lp15@66827
  1917
        also note \<open>dist (f (xs n)) (?g x) < e'\<close>
lp15@66827
  1918
        finally show ?case by (simp add: e'_def)
lp15@66827
  1919
      qed
lp15@66827
  1920
      then show "dist (?g x') (?g x) < e" by simp
lp15@66827
  1921
    qed
lp15@66827
  1922
  qed
lp15@66827
  1923
  moreover have "f x = ?g x" if "x \<in> X" for x using that by simp
lp15@66827
  1924
  moreover
lp15@66827
  1925
  {
lp15@66827
  1926
    fix Y h x
lp15@66827
  1927
    assume Y: "x \<in> Y" "X \<subseteq> Y" "Y \<subseteq> closure X" and cont_h: "continuous_on Y h"
lp15@66827
  1928
      and extension: "(\<And>x. x \<in> X \<Longrightarrow> f x = h x)"
lp15@66827
  1929
    {
lp15@66827
  1930
      assume "x \<notin> X"
lp15@66827
  1931
      have "x \<in> closure X" using Y by auto
lp15@66827
  1932
      then obtain xs where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X"
lp15@66827
  1933
        by (auto simp: closure_sequential)
lp15@66827
  1934
      from continuous_on_tendsto_compose[OF cont_h xs(1)] xs(2) Y
lp15@66827
  1935
      have hx: "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> h x"
lp15@66827
  1936
        by (auto simp: set_mp extension)
lp15@66827
  1937
      then have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> y x"
lp15@66827
  1938
        using \<open>x \<notin> X\<close> not_eventuallyD xs(2)
lp15@66827
  1939
        by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at xs)
lp15@66827
  1940
      with hx have "h x = y x" by (rule LIMSEQ_unique)
lp15@66827
  1941
    } then
lp15@66827
  1942
    have "h x = ?g x"
lp15@66827
  1943
      using extension by auto
lp15@66827
  1944
  }
lp15@66827
  1945
  ultimately show ?thesis ..
lp15@66827
  1946
qed
lp15@66827
  1947
lp15@66827
  1948
lemma bounded_uniformly_continuous_image:
lp15@66827
  1949
  fixes f :: "'a :: heine_borel \<Rightarrow> 'b :: heine_borel"
lp15@66827
  1950
  assumes "uniformly_continuous_on S f" "bounded S"
lp15@66884
  1951
  shows "bounded(f ` S)"
lp15@66827
  1952
  by (metis (no_types, lifting) assms bounded_closure_image compact_closure compact_continuous_image compact_eq_bounded_closed image_cong uniformly_continuous_imp_continuous uniformly_continuous_on_extension_on_closure)
lp15@66827
  1953
lp15@66827
  1954
subsection \<open>Making a continuous function avoid some value in a neighbourhood.\<close>
lp15@66827
  1955
lp15@66827
  1956
lemma continuous_within_avoid:
lp15@66827
  1957
  fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
lp15@66827
  1958
  assumes "continuous (at x within s) f"
lp15@66827
  1959
    and "f x \<noteq> a"
lp15@66827
  1960
  shows "\<exists>e>0. \<forall>y \<in> s. dist x y < e --> f y \<noteq> a"
lp15@66827
  1961
proof -
lp15@66827
  1962
  obtain U where "open U" and "f x \<in> U" and "a \<notin> U"
lp15@66827
  1963
    using t1_space [OF \<open>f x \<noteq> a\<close>] by fast
lp15@66827
  1964
  have "(f \<longlongrightarrow> f x) (at x within s)"
lp15@66827
  1965
    using assms(1) by (simp add: continuous_within)
lp15@66827
  1966
  then have "eventually (\<lambda>y. f y \<in> U) (at x within s)"
lp15@66827
  1967
    using \<open>open U\<close> and \<open>f x \<in> U\<close>
lp15@66827
  1968
    unfolding tendsto_def by fast
lp15@66827
  1969
  then have "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
lp15@66827
  1970
    using \<open>a \<notin> U\<close> by (fast elim: eventually_mono)
lp15@66827
  1971
  then show ?thesis
haftmann@66953
  1972
    using \<open>f x \<noteq> a\<close> by (auto simp: dist_commute eventually_at)
lp15@66827
  1973
qed
lp15@66827
  1974
lp15@66827
  1975
lemma continuous_at_avoid:
lp15@66827
  1976
  fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
lp15@66827
  1977
  assumes "continuous (at x) f"
lp15@66827
  1978
    and "f x \<noteq> a"
lp15@66827
  1979
  shows "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> f y \<noteq> a"
lp15@66827
  1980
  using assms continuous_within_avoid[of x UNIV f a] by simp
lp15@66827
  1981
lp15@66827
  1982
lemma continuous_on_avoid:
lp15@66827
  1983
  fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
lp15@66827
  1984
  assumes "continuous_on s f"
lp15@66827
  1985
    and "x \<in> s"
lp15@66827
  1986
    and "f x \<noteq> a"
lp15@66827
  1987
  shows "\<exists>e>0. \<forall>y \<in> s. dist x y < e \<longrightarrow> f y \<noteq> a"
lp15@66827
  1988
  using assms(1)[unfolded continuous_on_eq_continuous_within, THEN bspec[where x=x],
lp15@66827
  1989
    OF assms(2)] continuous_within_avoid[of x s f a]
lp15@66827
  1990
  using assms(3)
lp15@66827
  1991
  by auto
lp15@66827
  1992
lp15@66827
  1993
lemma continuous_on_open_avoid:
lp15@66827
  1994
  fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
lp15@66827
  1995
  assumes "continuous_on s f"
lp15@66827
  1996
    and "open s"
lp15@66827
  1997
    and "x \<in> s"
lp15@66827
  1998
    and "f x \<noteq> a"
lp15@66827
  1999
  shows "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> f y \<noteq> a"
lp15@66827
  2000
  using assms(1)[unfolded continuous_on_eq_continuous_at[OF assms(2)], THEN bspec[where x=x], OF assms(3)]
lp15@66827
  2001
  using continuous_at_avoid[of x f a] assms(4)
lp15@66827
  2002
  by auto
lp15@66827
  2003
lp15@66827
  2004
subsection\<open>Quotient maps\<close>
lp15@66827
  2005
lp15@66827
  2006
lemma quotient_map_imp_continuous_open:
lp15@66884
  2007
  assumes T: "f ` S \<subseteq> T"
lp15@66884
  2008
      and ope: "\<And>U. U \<subseteq> T
lp15@66884
  2009
              \<Longrightarrow> (openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
lp15@66884
  2010
                   openin (subtopology euclidean T) U)"
lp15@66884
  2011
    shows "continuous_on S f"
lp15@66827
  2012
proof -
lp15@66884
  2013
  have [simp]: "S \<inter> f -` f ` S = S" by auto
lp15@66827
  2014
  show ?thesis
lp15@66884
  2015
    using ope [OF T]
lp15@66827
  2016
    apply (simp add: continuous_on_open)
lp15@66884
  2017
    by (meson ope openin_imp_subset openin_trans)
lp15@66827
  2018
qed
lp15@66827
  2019
lp15@66827
  2020
lemma quotient_map_imp_continuous_closed:
lp15@66884
  2021
  assumes T: "f ` S \<subseteq> T"
lp15@66884
  2022
      and ope: "\<And>U. U \<subseteq> T
lp15@66884
  2023
                  \<Longrightarrow> (closedin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
lp15@66884
  2024
                       closedin (subtopology euclidean T) U)"
lp15@66884
  2025
    shows "continuous_on S f"
lp15@66827
  2026
proof -
lp15@66884
  2027
  have [simp]: "S \<inter> f -` f ` S = S" by auto
lp15@66827
  2028
  show ?thesis
lp15@66884
  2029
    using ope [OF T]
lp15@66827
  2030
    apply (simp add: continuous_on_closed)
lp15@66884
  2031
    by (metis (no_types, lifting) ope closedin_imp_subset closedin_trans)
lp15@66827
  2032
qed
lp15@66827
  2033
lp15@66827
  2034
lemma open_map_imp_quotient_map:
lp15@66884
  2035
  assumes contf: "continuous_on S f"
lp15@66884
  2036
      and T: "T \<subseteq> f ` S"
lp15@66884
  2037
      and ope: "\<And>T. openin (subtopology euclidean S) T
lp15@66884
  2038
                   \<Longrightarrow> openin (subtopology euclidean (f ` S)) (f ` T)"
lp15@66884
  2039
    shows "openin (subtopology euclidean S) (S \<inter> f -` T) =
lp15@66884
  2040
           openin (subtopology euclidean (f ` S)) T"
lp15@66827
  2041
proof -
lp15@66884
  2042
  have "T = f ` (S \<inter> f -` T)"
lp15@66884
  2043
    using T by blast
lp15@66827
  2044
  then show ?thesis
lp15@66884
  2045
    using "ope" contf continuous_on_open by metis
lp15@66827
  2046
qed
lp15@66827
  2047
lp15@66827
  2048
lemma closed_map_imp_quotient_map:
lp15@66884
  2049
  assumes contf: "continuous_on S f"
lp15@66884
  2050
      and T: "T \<subseteq> f ` S"
lp15@66884
  2051
      and ope: "\<And>T. closedin (subtopology euclidean S) T
lp15@66884
  2052
              \<Longrightarrow> closedin (subtopology euclidean (f ` S)) (f ` T)"
lp15@66884
  2053
    shows "openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow>
lp15@66884
  2054
           openin (subtopology euclidean (f ` S)) T"
lp15@66827
  2055
          (is "?lhs = ?rhs")
lp15@66827
  2056
proof
lp15@66827
  2057
  assume ?lhs
lp15@66884
  2058
  then have *: "closedin (subtopology euclidean S) (S - (S \<inter> f -` T))"
lp15@66827
  2059
    using closedin_diff by fastforce
lp15@66884
  2060
  have [simp]: "(f ` S - f ` (S - (S \<inter> f -` T))) = T"
lp15@66884
  2061
    using T by blast
lp15@66827
  2062
  show ?rhs
lp15@66827
  2063
    using ope [OF *, unfolded closedin_def] by auto
lp15@66827
  2064
next
lp15@66827
  2065
  assume ?rhs
lp15@66827
  2066
  with contf show ?lhs
lp15@66827
  2067
    by (auto simp: continuous_on_open)
lp15@66827
  2068
qed
lp15@66827
  2069
lp15@66827
  2070
lemma continuous_right_inverse_imp_quotient_map:
lp15@66884
  2071
  assumes contf: "continuous_on S f" and imf: "f ` S \<subseteq> T"
lp15@66884
  2072
      and contg: "continuous_on T g" and img: "g ` T \<subseteq> S"
lp15@66884
  2073
      and fg [simp]: "\<And>y. y \<in> T \<Longrightarrow> f(g y) = y"
lp15@66884
  2074
      and U: "U \<subseteq> T"
lp15@66884
  2075
    shows "openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
lp15@66884
  2076
           openin (subtopology euclidean T) U"
lp15@66827
  2077
          (is "?lhs = ?rhs")
lp15@66827
  2078
proof -
lp15@66884
  2079
  have f: "\<And>Z. openin (subtopology euclidean (f ` S)) Z \<Longrightarrow>
lp15@66884
  2080
                openin (subtopology euclidean S) (S \<inter> f -` Z)"
lp15@66884
  2081
  and  g: "\<And>Z. openin (subtopology euclidean (g ` T)) Z \<Longrightarrow>
lp15@66884
  2082
                openin (subtopology euclidean T) (T \<inter> g -` Z)"
lp15@66827
  2083
    using contf contg by (auto simp: continuous_on_open)
lp15@66827
  2084
  show ?thesis
lp15@66827
  2085
  proof
lp15@66884
  2086
    have "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = {x \<in> T. f (g x) \<in> U}"
lp15@66827
  2087
      using imf img by blast
lp15@66884
  2088
    also have "... = U"
lp15@66884
  2089
      using U by auto
lp15@66884
  2090
    finally have eq: "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = U" .
lp15@66827
  2091
    assume ?lhs
lp15@66884
  2092
    then have *: "openin (subtopology euclidean (g ` T)) (g ` T \<inter> (S \<inter> f -` U))"
lp15@66827
  2093
      by (meson img openin_Int openin_subtopology_Int_subset openin_subtopology_self)
lp15@66827
  2094
    show ?rhs
lp15@66884
  2095
      using g [OF *] eq by auto
lp15@66827
  2096
  next
lp15@66827
  2097
    assume rhs: ?rhs
lp15@66827
  2098
    show ?lhs
lp15@66884
  2099
      by (metis f fg image_eqI image_subset_iff imf img openin_subopen openin_subtopology_self openin_trans rhs)
lp15@66827
  2100
  qed
lp15@66827
  2101
qed
lp15@66827
  2102
lp15@66827
  2103
lemma continuous_left_inverse_imp_quotient_map:
lp15@66884
  2104
  assumes "continuous_on S f"