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