src/HOL/Analysis/Elementary_Metric_Spaces.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (3 weeks ago) changeset 69981 3dced198b9ec parent 69922 4a9167f377b0 child 70136 f03a01a18c6e permissions -rw-r--r--
more strict AFP properties;
     1 (*  Author:     L C Paulson, University of Cambridge

     2     Author:     Amine Chaieb, University of Cambridge

     3     Author:     Robert Himmelmann, TU Muenchen

     4     Author:     Brian Huffman, Portland State University

     5 *)

     6

     7 chapter \<open>Functional Analysis\<close>

     8

     9 theory Elementary_Metric_Spaces

    10   imports

    11     Abstract_Topology_2

    12 begin

    13

    14 section \<open>Elementary Metric Spaces\<close>

    15

    16 subsection \<open>Open and closed balls\<close>

    17

    18 definition%important ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"

    19   where "ball x e = {y. dist x y < e}"

    20

    21 definition%important cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"

    22   where "cball x e = {y. dist x y \<le> e}"

    23

    24 definition%important sphere :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"

    25   where "sphere x e = {y. dist x y = e}"

    26

    27 lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e"

    28   by (simp add: ball_def)

    29

    30 lemma mem_cball [simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e"

    31   by (simp add: cball_def)

    32

    33 lemma mem_sphere [simp]: "y \<in> sphere x e \<longleftrightarrow> dist x y = e"

    34   by (simp add: sphere_def)

    35

    36 lemma ball_trivial [simp]: "ball x 0 = {}"

    37   by (simp add: ball_def)

    38

    39 lemma cball_trivial [simp]: "cball x 0 = {x}"

    40   by (simp add: cball_def)

    41

    42 lemma sphere_trivial [simp]: "sphere x 0 = {x}"

    43   by (simp add: sphere_def)

    44

    45 lemma disjoint_ballI: "dist x y \<ge> r+s \<Longrightarrow> ball x r \<inter> ball y s = {}"

    46   using dist_triangle_less_add not_le by fastforce

    47

    48 lemma disjoint_cballI: "dist x y > r + s \<Longrightarrow> cball x r \<inter> cball y s = {}"

    49   by (metis add_mono disjoint_iff_not_equal dist_triangle2 dual_order.trans leD mem_cball)

    50

    51 lemma sphere_empty [simp]: "r < 0 \<Longrightarrow> sphere a r = {}"

    52   for a :: "'a::metric_space"

    53   by auto

    54

    55 lemma centre_in_ball [simp]: "x \<in> ball x e \<longleftrightarrow> 0 < e"

    56   by simp

    57

    58 lemma centre_in_cball [simp]: "x \<in> cball x e \<longleftrightarrow> 0 \<le> e"

    59   by simp

    60

    61 lemma ball_subset_cball [simp, intro]: "ball x e \<subseteq> cball x e"

    62   by (simp add: subset_eq)

    63

    64 lemma mem_ball_imp_mem_cball: "x \<in> ball y e \<Longrightarrow> x \<in> cball y e"

    65   by (auto simp: mem_ball mem_cball)

    66

    67 lemma sphere_cball [simp,intro]: "sphere z r \<subseteq> cball z r"

    68   by force

    69

    70 lemma cball_diff_sphere: "cball a r - sphere a r = ball a r"

    71   by auto

    72

    73 lemma subset_ball[intro]: "d \<le> e \<Longrightarrow> ball x d \<subseteq> ball x e"

    74   by (simp add: subset_eq)

    75

    76 lemma subset_cball[intro]: "d \<le> e \<Longrightarrow> cball x d \<subseteq> cball x e"

    77   by (simp add: subset_eq)

    78

    79 lemma mem_ball_leI: "x \<in> ball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> ball y f"

    80   by (auto simp: mem_ball mem_cball)

    81

    82 lemma mem_cball_leI: "x \<in> cball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> cball y f"

    83   by (auto simp: mem_ball mem_cball)

    84

    85 lemma cball_trans: "y \<in> cball z b \<Longrightarrow> x \<in> cball y a \<Longrightarrow> x \<in> cball z (b + a)"

    86   unfolding mem_cball

    87 proof -

    88   have "dist z x \<le> dist z y + dist y x"

    89     by (rule dist_triangle)

    90   also assume "dist z y \<le> b"

    91   also assume "dist y x \<le> a"

    92   finally show "dist z x \<le> b + a" by arith

    93 qed

    94

    95 lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s"

    96   by (simp add: set_eq_iff) arith

    97

    98 lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s"

    99   by (simp add: set_eq_iff)

   100

   101 lemma cball_max_Un: "cball a (max r s) = cball a r \<union> cball a s"

   102   by (simp add: set_eq_iff) arith

   103

   104 lemma cball_min_Int: "cball a (min r s) = cball a r \<inter> cball a s"

   105   by (simp add: set_eq_iff)

   106

   107 lemma cball_diff_eq_sphere: "cball a r - ball a r =  sphere a r"

   108   by (auto simp: cball_def ball_def dist_commute)

   109

   110 lemma open_ball [intro, simp]: "open (ball x e)"

   111 proof -

   112   have "open (dist x - {..<e})"

   113     by (intro open_vimage open_lessThan continuous_intros)

   114   also have "dist x - {..<e} = ball x e"

   115     by auto

   116   finally show ?thesis .

   117 qed

   118

   119 lemma open_contains_ball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. ball x e \<subseteq> S)"

   120   by (simp add: open_dist subset_eq mem_ball Ball_def dist_commute)

   121

   122 lemma openI [intro?]: "(\<And>x. x\<in>S \<Longrightarrow> \<exists>e>0. ball x e \<subseteq> S) \<Longrightarrow> open S"

   123   by (auto simp: open_contains_ball)

   124

   125 lemma openE[elim?]:

   126   assumes "open S" "x\<in>S"

   127   obtains e where "e>0" "ball x e \<subseteq> S"

   128   using assms unfolding open_contains_ball by auto

   129

   130 lemma open_contains_ball_eq: "open S \<Longrightarrow> x\<in>S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"

   131   by (metis open_contains_ball subset_eq centre_in_ball)

   132

   133 lemma ball_eq_empty[simp]: "ball x e = {} \<longleftrightarrow> e \<le> 0"

   134   unfolding mem_ball set_eq_iff

   135   apply (simp add: not_less)

   136   apply (metis zero_le_dist order_trans dist_self)

   137   done

   138

   139 lemma ball_empty: "e \<le> 0 \<Longrightarrow> ball x e = {}" by simp

   140

   141 lemma closed_cball [iff]: "closed (cball x e)"

   142 proof -

   143   have "closed (dist x - {..e})"

   144     by (intro closed_vimage closed_atMost continuous_intros)

   145   also have "dist x - {..e} = cball x e"

   146     by auto

   147   finally show ?thesis .

   148 qed

   149

   150 lemma open_contains_cball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0.  cball x e \<subseteq> S)"

   151 proof -

   152   {

   153     fix x and e::real

   154     assume "x\<in>S" "e>0" "ball x e \<subseteq> S"

   155     then have "\<exists>d>0. cball x d \<subseteq> S" unfolding subset_eq by (rule_tac x="e/2" in exI, auto)

   156   }

   157   moreover

   158   {

   159     fix x and e::real

   160     assume "x\<in>S" "e>0" "cball x e \<subseteq> S"

   161     then have "\<exists>d>0. ball x d \<subseteq> S"

   162       unfolding subset_eq

   163       apply (rule_tac x="e/2" in exI, auto)

   164       done

   165   }

   166   ultimately show ?thesis

   167     unfolding open_contains_ball by auto

   168 qed

   169

   170 lemma open_contains_cball_eq: "open S \<Longrightarrow> (\<forall>x. x \<in> S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S))"

   171   by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball)

   172

   173 lemma eventually_nhds_ball: "d > 0 \<Longrightarrow> eventually (\<lambda>x. x \<in> ball z d) (nhds z)"

   174   by (rule eventually_nhds_in_open) simp_all

   175

   176 lemma eventually_at_ball: "d > 0 \<Longrightarrow> eventually (\<lambda>t. t \<in> ball z d \<and> t \<in> A) (at z within A)"

   177   unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)

   178

   179 lemma eventually_at_ball': "d > 0 \<Longrightarrow> eventually (\<lambda>t. t \<in> ball z d \<and> t \<noteq> z \<and> t \<in> A) (at z within A)"

   180   unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)

   181

   182 lemma at_within_ball: "e > 0 \<Longrightarrow> dist x y < e \<Longrightarrow> at y within ball x e = at y"

   183   by (subst at_within_open) auto

   184

   185 lemma atLeastAtMost_eq_cball:

   186   fixes a b::real

   187   shows "{a .. b} = cball ((a + b)/2) ((b - a)/2)"

   188   by (auto simp: dist_real_def field_simps mem_cball)

   189

   190 lemma greaterThanLessThan_eq_ball:

   191   fixes a b::real

   192   shows "{a <..< b} = ball ((a + b)/2) ((b - a)/2)"

   193   by (auto simp: dist_real_def field_simps mem_ball)

   194

   195 lemma interior_ball [simp]: "interior (ball x e) = ball x e"

   196   by (simp add: interior_open)

   197

   198 lemma cball_eq_empty [simp]: "cball x e = {} \<longleftrightarrow> e < 0"

   199   apply (simp add: set_eq_iff not_le)

   200   apply (metis zero_le_dist dist_self order_less_le_trans)

   201   done

   202

   203 lemma cball_empty [simp]: "e < 0 \<Longrightarrow> cball x e = {}"

   204   by simp

   205

   206 lemma cball_sing:

   207   fixes x :: "'a::metric_space"

   208   shows "e = 0 \<Longrightarrow> cball x e = {x}"

   209   by (auto simp: set_eq_iff)

   210

   211 lemma ball_divide_subset: "d \<ge> 1 \<Longrightarrow> ball x (e/d) \<subseteq> ball x e"

   212   apply (cases "e \<le> 0")

   213   apply (simp add: ball_empty divide_simps)

   214   apply (rule subset_ball)

   215   apply (simp add: divide_simps)

   216   done

   217

   218 lemma ball_divide_subset_numeral: "ball x (e / numeral w) \<subseteq> ball x e"

   219   using ball_divide_subset one_le_numeral by blast

   220

   221 lemma cball_divide_subset: "d \<ge> 1 \<Longrightarrow> cball x (e/d) \<subseteq> cball x e"

   222   apply (cases "e < 0")

   223   apply (simp add: divide_simps)

   224   apply (rule subset_cball)

   225   apply (metis div_by_1 frac_le not_le order_refl zero_less_one)

   226   done

   227

   228 lemma cball_divide_subset_numeral: "cball x (e / numeral w) \<subseteq> cball x e"

   229   using cball_divide_subset one_le_numeral by blast

   230

   231

   232 subsection \<open>Limit Points\<close>

   233

   234 lemma islimpt_approachable:

   235   fixes x :: "'a::metric_space"

   236   shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e)"

   237   unfolding islimpt_iff_eventually eventually_at by fast

   238

   239 lemma islimpt_approachable_le: "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> S. x' \<noteq> x \<and> dist x' x \<le> e)"

   240   for x :: "'a::metric_space"

   241   unfolding islimpt_approachable

   242   using approachable_lt_le [where f="\<lambda>y. dist y x" and P="\<lambda>y. y \<notin> S \<or> y = x",

   243     THEN arg_cong [where f=Not]]

   244   by (simp add: Bex_def conj_commute conj_left_commute)

   245

   246 lemma limpt_of_limpts: "x islimpt {y. y islimpt S} \<Longrightarrow> x islimpt S"

   247   for x :: "'a::metric_space"

   248   apply (clarsimp simp add: islimpt_approachable)

   249   apply (drule_tac x="e/2" in spec)

   250   apply (auto simp: simp del: less_divide_eq_numeral1)

   251   apply (drule_tac x="dist x' x" in spec)

   252   apply (auto simp: zero_less_dist_iff simp del: less_divide_eq_numeral1)

   253   apply (erule rev_bexI)

   254   apply (metis dist_commute dist_triangle_half_r less_trans less_irrefl)

   255   done

   256

   257 lemma closed_limpts:  "closed {x::'a::metric_space. x islimpt S}"

   258   using closed_limpt limpt_of_limpts by blast

   259

   260 lemma limpt_of_closure: "x islimpt closure S \<longleftrightarrow> x islimpt S"

   261   for x :: "'a::metric_space"

   262   by (auto simp: closure_def islimpt_Un dest: limpt_of_limpts)

   263

   264 lemma islimpt_eq_infinite_ball: "x islimpt S \<longleftrightarrow> (\<forall>e>0. infinite(S \<inter> ball x e))"

   265   apply (simp add: islimpt_eq_acc_point, safe)

   266    apply (metis Int_commute open_ball centre_in_ball)

   267   by (metis open_contains_ball Int_mono finite_subset inf_commute subset_refl)

   268

   269 lemma islimpt_eq_infinite_cball: "x islimpt S \<longleftrightarrow> (\<forall>e>0. infinite(S \<inter> cball x e))"

   270   apply (simp add: islimpt_eq_infinite_ball, safe)

   271    apply (meson Int_mono ball_subset_cball finite_subset order_refl)

   272   by (metis open_ball centre_in_ball finite_Int inf.absorb_iff2 inf_assoc open_contains_cball_eq)

   273

   274

   275 subsection \<open>Perfect Metric Spaces\<close>

   276

   277 lemma perfect_choose_dist: "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r"

   278   for x :: "'a::{perfect_space,metric_space}"

   279   using islimpt_UNIV [of x] by (simp add: islimpt_approachable)

   280

   281 lemma cball_eq_sing:

   282   fixes x :: "'a::{metric_space,perfect_space}"

   283   shows "cball x e = {x} \<longleftrightarrow> e = 0"

   284 proof (rule linorder_cases)

   285   assume e: "0 < e"

   286   obtain a where "a \<noteq> x" "dist a x < e"

   287     using perfect_choose_dist [OF e] by auto

   288   then have "a \<noteq> x" "dist x a \<le> e"

   289     by (auto simp: dist_commute)

   290   with e show ?thesis by (auto simp: set_eq_iff)

   291 qed auto

   292

   293

   294 subsection \<open>?\<close>

   295

   296 lemma finite_ball_include:

   297   fixes a :: "'a::metric_space"

   298   assumes "finite S"

   299   shows "\<exists>e>0. S \<subseteq> ball a e"

   300   using assms

   301 proof induction

   302   case (insert x S)

   303   then obtain e0 where "e0>0" and e0:"S \<subseteq> ball a e0" by auto

   304   define e where "e = max e0 (2 * dist a x)"

   305   have "e>0" unfolding e_def using \<open>e0>0\<close> by auto

   306   moreover have "insert x S \<subseteq> ball a e"

   307     using e0 \<open>e>0\<close> unfolding e_def by auto

   308   ultimately show ?case by auto

   309 qed (auto intro: zero_less_one)

   310

   311 lemma finite_set_avoid:

   312   fixes a :: "'a::metric_space"

   313   assumes "finite S"

   314   shows "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d \<le> dist a x"

   315   using assms

   316 proof induction

   317   case (insert x S)

   318   then obtain d where "d > 0" and d: "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> d \<le> dist a x"

   319     by blast

   320   show ?case

   321   proof (cases "x = a")

   322     case True

   323     with \<open>d > 0 \<close>d show ?thesis by auto

   324   next

   325     case False

   326     let ?d = "min d (dist a x)"

   327     from False \<open>d > 0\<close> have dp: "?d > 0"

   328       by auto

   329     from d have d': "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> ?d \<le> dist a x"

   330       by auto

   331     with dp False show ?thesis

   332       by (metis insert_iff le_less min_less_iff_conj not_less)

   333   qed

   334 qed (auto intro: zero_less_one)

   335

   336 lemma discrete_imp_closed:

   337   fixes S :: "'a::metric_space set"

   338   assumes e: "0 < e"

   339     and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x"

   340   shows "closed S"

   341 proof -

   342   have False if C: "\<And>e. e>0 \<Longrightarrow> \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" for x

   343   proof -

   344     from e have e2: "e/2 > 0" by arith

   345     from C[rule_format, OF e2] obtain y where y: "y \<in> S" "y \<noteq> x" "dist y x < e/2"

   346       by blast

   347     let ?m = "min (e/2) (dist x y) "

   348     from e2 y(2) have mp: "?m > 0"

   349       by simp

   350     from C[OF mp] obtain z where z: "z \<in> S" "z \<noteq> x" "dist z x < ?m"

   351       by blast

   352     from z y have "dist z y < e"

   353       by (intro dist_triangle_lt [where z=x]) simp

   354     from d[rule_format, OF y(1) z(1) this] y z show ?thesis

   355       by (auto simp: dist_commute)

   356   qed

   357   then show ?thesis

   358     by (metis islimpt_approachable closed_limpt [where 'a='a])

   359 qed

   360

   361

   362 subsection \<open>Interior\<close>

   363

   364 lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"

   365   using open_contains_ball_eq [where S="interior S"]

   366   by (simp add: open_subset_interior)

   367

   368 lemma mem_interior_cball: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S)"

   369   by (meson ball_subset_cball interior_subset mem_interior open_contains_cball open_interior

   370       subset_trans)

   371

   372

   373 subsection \<open>Frontier\<close>

   374

   375 lemma frontier_straddle:

   376   fixes a :: "'a::metric_space"

   377   shows "a \<in> frontier S \<longleftrightarrow> (\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e))"

   378   unfolding frontier_def closure_interior

   379   by (auto simp: mem_interior subset_eq ball_def)

   380

   381

   382 subsection \<open>Limits\<close>

   383

   384 proposition Lim: "(f \<longlongrightarrow> l) net \<longleftrightarrow> trivial_limit net \<or> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"

   385   by (auto simp: tendsto_iff trivial_limit_eq)

   386

   387 text \<open>Show that they yield usual definitions in the various cases.\<close>

   388

   389 proposition Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow>

   390     (\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> d \<longrightarrow> dist (f x) l < e)"

   391   by (auto simp: tendsto_iff eventually_at_le)

   392

   393 proposition Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow>

   394     (\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a  < d \<longrightarrow> dist (f x) l < e)"

   395   by (auto simp: tendsto_iff eventually_at)

   396

   397 corollary Lim_withinI [intro?]:

   398   assumes "\<And>e. e > 0 \<Longrightarrow> \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l \<le> e"

   399   shows "(f \<longlongrightarrow> l) (at a within S)"

   400   apply (simp add: Lim_within, clarify)

   401   apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)

   402   done

   403

   404 proposition Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow>

   405     (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d  \<longrightarrow> dist (f x) l < e)"

   406   by (auto simp: tendsto_iff eventually_at)

   407

   408 lemma Lim_transform_within_set:

   409   fixes a :: "'a::metric_space" and l :: "'b::metric_space"

   410   shows "\<lbrakk>(f \<longlongrightarrow> l) (at a within S); eventually (\<lambda>x. x \<in> S \<longleftrightarrow> x \<in> T) (at a)\<rbrakk>

   411          \<Longrightarrow> (f \<longlongrightarrow> l) (at a within T)"

   412 apply (clarsimp simp: eventually_at Lim_within)

   413 apply (drule_tac x=e in spec, clarify)

   414 apply (rename_tac k)

   415 apply (rule_tac x="min d k" in exI, simp)

   416 done

   417

   418 text \<open>Another limit point characterization.\<close>

   419

   420 lemma limpt_sequential_inj:

   421   fixes x :: "'a::metric_space"

   422   shows "x islimpt S \<longleftrightarrow>

   423          (\<exists>f. (\<forall>n::nat. f n \<in> S - {x}) \<and> inj f \<and> (f \<longlongrightarrow> x) sequentially)"

   424          (is "?lhs = ?rhs")

   425 proof

   426   assume ?lhs

   427   then have "\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e"

   428     by (force simp: islimpt_approachable)

   429   then obtain y where y: "\<And>e. e>0 \<Longrightarrow> y e \<in> S \<and> y e \<noteq> x \<and> dist (y e) x < e"

   430     by metis

   431   define f where "f \<equiv> rec_nat (y 1) (\<lambda>n fn. y (min (inverse(2 ^ (Suc n))) (dist fn x)))"

   432   have [simp]: "f 0 = y 1"

   433                "f(Suc n) = y (min (inverse(2 ^ (Suc n))) (dist (f n) x))" for n

   434     by (simp_all add: f_def)

   435   have f: "f n \<in> S \<and> (f n \<noteq> x) \<and> dist (f n) x < inverse(2 ^ n)" for n

   436   proof (induction n)

   437     case 0 show ?case

   438       by (simp add: y)

   439   next

   440     case (Suc n) then show ?case

   441       apply (auto simp: y)

   442       by (metis half_gt_zero_iff inverse_positive_iff_positive less_divide_eq_numeral1(1) min_less_iff_conj y zero_less_dist_iff zero_less_numeral zero_less_power)

   443   qed

   444   show ?rhs

   445   proof (rule_tac x=f in exI, intro conjI allI)

   446     show "\<And>n. f n \<in> S - {x}"

   447       using f by blast

   448     have "dist (f n) x < dist (f m) x" if "m < n" for m n

   449     using that

   450     proof (induction n)

   451       case 0 then show ?case by simp

   452     next

   453       case (Suc n)

   454       then consider "m < n" | "m = n" using less_Suc_eq by blast

   455       then show ?case

   456       proof cases

   457         assume "m < n"

   458         have "dist (f(Suc n)) x = dist (y (min (inverse(2 ^ (Suc n))) (dist (f n) x))) x"

   459           by simp

   460         also have "\<dots> < dist (f n) x"

   461           by (metis dist_pos_lt f min.strict_order_iff min_less_iff_conj y)

   462         also have "\<dots> < dist (f m) x"

   463           using Suc.IH \<open>m < n\<close> by blast

   464         finally show ?thesis .

   465       next

   466         assume "m = n" then show ?case

   467           by simp (metis dist_pos_lt f half_gt_zero_iff inverse_positive_iff_positive min_less_iff_conj y zero_less_numeral zero_less_power)

   468       qed

   469     qed

   470     then show "inj f"

   471       by (metis less_irrefl linorder_injI)

   472     show "f \<longlonglongrightarrow> x"

   473       apply (rule tendstoI)

   474       apply (rule_tac c="nat (ceiling(1/e))" in eventually_sequentiallyI)

   475       apply (rule less_trans [OF f [THEN conjunct2, THEN conjunct2]])

   476       apply (simp add: field_simps)

   477       by (meson le_less_trans mult_less_cancel_left not_le of_nat_less_two_power)

   478   qed

   479 next

   480   assume ?rhs

   481   then show ?lhs

   482     by (fastforce simp add: islimpt_approachable lim_sequentially)

   483 qed

   484

   485 lemma Lim_dist_ubound:

   486   assumes "\<not>(trivial_limit net)"

   487     and "(f \<longlongrightarrow> l) net"

   488     and "eventually (\<lambda>x. dist a (f x) \<le> e) net"

   489   shows "dist a l \<le> e"

   490   using assms by (fast intro: tendsto_le tendsto_intros)

   491

   492

   493 subsection \<open>Continuity\<close>

   494

   495 text\<open>Derive the epsilon-delta forms, which we often use as "definitions"\<close>

   496

   497 proposition continuous_within_eps_delta:

   498   "continuous (at x within s) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'\<in> s.  dist x' x < d --> dist (f x') (f x) < e)"

   499   unfolding continuous_within and Lim_within  by fastforce

   500

   501 corollary continuous_at_eps_delta:

   502   "continuous (at x) f \<longleftrightarrow> (\<forall>e > 0. \<exists>d > 0. \<forall>x'. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"

   503   using continuous_within_eps_delta [of x UNIV f] by simp

   504

   505 lemma continuous_at_right_real_increasing:

   506   fixes f :: "real \<Rightarrow> real"

   507   assumes nondecF: "\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y"

   508   shows "continuous (at_right a) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. f (a + d) - f a < e)"

   509   apply (simp add: greaterThan_def dist_real_def continuous_within Lim_within_le)

   510   apply (intro all_cong ex_cong, safe)

   511   apply (erule_tac x="a + d" in allE, simp)

   512   apply (simp add: nondecF field_simps)

   513   apply (drule nondecF, simp)

   514   done

   515

   516 lemma continuous_at_left_real_increasing:

   517   assumes nondecF: "\<And> x y. x \<le> y \<Longrightarrow> f x \<le> ((f y) :: real)"

   518   shows "(continuous (at_left (a :: real)) f) = (\<forall>e > 0. \<exists>delta > 0. f a - f (a - delta) < e)"

   519   apply (simp add: lessThan_def dist_real_def continuous_within Lim_within_le)

   520   apply (intro all_cong ex_cong, safe)

   521   apply (erule_tac x="a - d" in allE, simp)

   522   apply (simp add: nondecF field_simps)

   523   apply (cut_tac x="a - d" and y=x in nondecF, simp_all)

   524   done

   525

   526 text\<open>Versions in terms of open balls.\<close>

   527

   528 lemma continuous_within_ball:

   529   "continuous (at x within s) f \<longleftrightarrow>

   530     (\<forall>e > 0. \<exists>d > 0. f  (ball x d \<inter> s) \<subseteq> ball (f x) e)"

   531   (is "?lhs = ?rhs")

   532 proof

   533   assume ?lhs

   534   {

   535     fix e :: real

   536     assume "e > 0"

   537     then obtain d where d: "d>0" "\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e"

   538       using \<open>?lhs\<close>[unfolded continuous_within Lim_within] by auto

   539     {

   540       fix y

   541       assume "y \<in> f  (ball x d \<inter> s)"

   542       then have "y \<in> ball (f x) e"

   543         using d(2)

   544         apply (auto simp: dist_commute)

   545         apply (erule_tac x=xa in ballE, auto)

   546         using \<open>e > 0\<close>

   547         apply auto

   548         done

   549     }

   550     then have "\<exists>d>0. f  (ball x d \<inter> s) \<subseteq> ball (f x) e"

   551       using \<open>d > 0\<close>

   552       unfolding subset_eq ball_def by (auto simp: dist_commute)

   553   }

   554   then show ?rhs by auto

   555 next

   556   assume ?rhs

   557   then show ?lhs

   558     unfolding continuous_within Lim_within ball_def subset_eq

   559     apply (auto simp: dist_commute)

   560     apply (erule_tac x=e in allE, auto)

   561     done

   562 qed

   563

   564 lemma continuous_at_ball:

   565   "continuous (at x) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. f  (ball x d) \<subseteq> ball (f x) e)" (is "?lhs = ?rhs")

   566 proof

   567   assume ?lhs

   568   then show ?rhs

   569     unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball

   570     apply auto

   571     apply (erule_tac x=e in allE, auto)

   572     apply (rule_tac x=d in exI, auto)

   573     apply (erule_tac x=xa in allE)

   574     apply (auto simp: dist_commute)

   575     done

   576 next

   577   assume ?rhs

   578   then show ?lhs

   579     unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball

   580     apply auto

   581     apply (erule_tac x=e in allE, auto)

   582     apply (rule_tac x=d in exI, auto)

   583     apply (erule_tac x="f xa" in allE)

   584     apply (auto simp: dist_commute)

   585     done

   586 qed

   587

   588 text\<open>Define setwise continuity in terms of limits within the set.\<close>

   589

   590 lemma continuous_on_iff:

   591   "continuous_on s f \<longleftrightarrow>

   592     (\<forall>x\<in>s. \<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"

   593   unfolding continuous_on_def Lim_within

   594   by (metis dist_pos_lt dist_self)

   595

   596 lemma continuous_within_E:

   597   assumes "continuous (at x within s) f" "e>0"

   598   obtains d where "d>0"  "\<And>x'. \<lbrakk>x'\<in> s; dist x' x \<le> d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"

   599   using assms apply (simp add: continuous_within_eps_delta)

   600   apply (drule spec [of _ e], clarify)

   601   apply (rule_tac d="d/2" in that, auto)

   602   done

   603

   604 lemma continuous_onI [intro?]:

   605   assumes "\<And>x e. \<lbrakk>e > 0; x \<in> s\<rbrakk> \<Longrightarrow> \<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) \<le> e"

   606   shows "continuous_on s f"

   607 apply (simp add: continuous_on_iff, clarify)

   608 apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)

   609 done

   610

   611 text\<open>Some simple consequential lemmas.\<close>

   612

   613 lemma continuous_onE:

   614     assumes "continuous_on s f" "x\<in>s" "e>0"

   615     obtains d where "d>0"  "\<And>x'. \<lbrakk>x' \<in> s; dist x' x \<le> d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"

   616   using assms

   617   apply (simp add: continuous_on_iff)

   618   apply (elim ballE allE)

   619   apply (auto intro: that [where d="d/2" for d])

   620   done

   621

   622 text\<open>The usual transformation theorems.\<close>

   623

   624 lemma continuous_transform_within:

   625   fixes f g :: "'a::metric_space \<Rightarrow> 'b::topological_space"

   626   assumes "continuous (at x within s) f"

   627     and "0 < d"

   628     and "x \<in> s"

   629     and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"

   630   shows "continuous (at x within s) g"

   631   using assms

   632   unfolding continuous_within

   633   by (force intro: Lim_transform_within)

   634

   635

   636 subsection \<open>Closure and Limit Characterization\<close>

   637

   638 lemma closure_approachable:

   639   fixes S :: "'a::metric_space set"

   640   shows "x \<in> closure S \<longleftrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x < e)"

   641   apply (auto simp: closure_def islimpt_approachable)

   642   apply (metis dist_self)

   643   done

   644

   645 lemma closure_approachable_le:

   646   fixes S :: "'a::metric_space set"

   647   shows "x \<in> closure S \<longleftrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x \<le> e)"

   648   unfolding closure_approachable

   649   using dense by force

   650

   651 lemma closure_approachableD:

   652   assumes "x \<in> closure S" "e>0"

   653   shows "\<exists>y\<in>S. dist x y < e"

   654   using assms unfolding closure_approachable by (auto simp: dist_commute)

   655

   656 lemma closed_approachable:

   657   fixes S :: "'a::metric_space set"

   658   shows "closed S \<Longrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x < e) \<longleftrightarrow> x \<in> S"

   659   by (metis closure_closed closure_approachable)

   660

   661 lemma closure_contains_Inf:

   662   fixes S :: "real set"

   663   assumes "S \<noteq> {}" "bdd_below S"

   664   shows "Inf S \<in> closure S"

   665 proof -

   666   have *: "\<forall>x\<in>S. Inf S \<le> x"

   667     using cInf_lower[of _ S] assms by metis

   668   {

   669     fix e :: real

   670     assume "e > 0"

   671     then have "Inf S < Inf S + e" by simp

   672     with assms obtain x where "x \<in> S" "x < Inf S + e"

   673       by (subst (asm) cInf_less_iff) auto

   674     with * have "\<exists>x\<in>S. dist x (Inf S) < e"

   675       by (intro bexI[of _ x]) (auto simp: dist_real_def)

   676   }

   677   then show ?thesis unfolding closure_approachable by auto

   678 qed

   679

   680 lemma not_trivial_limit_within_ball:

   681   "\<not> trivial_limit (at x within S) \<longleftrightarrow> (\<forall>e>0. S \<inter> ball x e - {x} \<noteq> {})"

   682   (is "?lhs \<longleftrightarrow> ?rhs")

   683 proof

   684   show ?rhs if ?lhs

   685   proof -

   686     {

   687       fix e :: real

   688       assume "e > 0"

   689       then obtain y where "y \<in> S - {x}" and "dist y x < e"

   690         using \<open>?lhs\<close> not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"]

   691         by auto

   692       then have "y \<in> S \<inter> ball x e - {x}"

   693         unfolding ball_def by (simp add: dist_commute)

   694       then have "S \<inter> ball x e - {x} \<noteq> {}" by blast

   695     }

   696     then show ?thesis by auto

   697   qed

   698   show ?lhs if ?rhs

   699   proof -

   700     {

   701       fix e :: real

   702       assume "e > 0"

   703       then obtain y where "y \<in> S \<inter> ball x e - {x}"

   704         using \<open>?rhs\<close> by blast

   705       then have "y \<in> S - {x}" and "dist y x < e"

   706         unfolding ball_def by (simp_all add: dist_commute)

   707       then have "\<exists>y \<in> S - {x}. dist y x < e"

   708         by auto

   709     }

   710     then show ?thesis

   711       using not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"]

   712       by auto

   713   qed

   714 qed

   715

   716

   717 subsection \<open>Boundedness\<close>

   718

   719   (* FIXME: This has to be unified with BSEQ!! *)

   720 definition%important (in metric_space) bounded :: "'a set \<Rightarrow> bool"

   721   where "bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)"

   722

   723 lemma bounded_subset_cball: "bounded S \<longleftrightarrow> (\<exists>e x. S \<subseteq> cball x e \<and> 0 \<le> e)"

   724   unfolding bounded_def subset_eq  by auto (meson order_trans zero_le_dist)

   725

   726 lemma bounded_any_center: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>y\<in>S. dist a y \<le> e)"

   727   unfolding bounded_def

   728   by auto (metis add.commute add_le_cancel_right dist_commute dist_triangle_le)

   729

   730 lemma bounded_iff: "bounded S \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. norm x \<le> a)"

   731   unfolding bounded_any_center [where a=0]

   732   by (simp add: dist_norm)

   733

   734 lemma bdd_above_norm: "bdd_above (norm  X) \<longleftrightarrow> bounded X"

   735   by (simp add: bounded_iff bdd_above_def)

   736

   737 lemma bounded_norm_comp: "bounded ((\<lambda>x. norm (f x))  S) = bounded (f  S)"

   738   by (simp add: bounded_iff)

   739

   740 lemma boundedI:

   741   assumes "\<And>x. x \<in> S \<Longrightarrow> norm x \<le> B"

   742   shows "bounded S"

   743   using assms bounded_iff by blast

   744

   745 lemma bounded_empty [simp]: "bounded {}"

   746   by (simp add: bounded_def)

   747

   748 lemma bounded_subset: "bounded T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> bounded S"

   749   by (metis bounded_def subset_eq)

   750

   751 lemma bounded_interior[intro]: "bounded S \<Longrightarrow> bounded(interior S)"

   752   by (metis bounded_subset interior_subset)

   753

   754 lemma bounded_closure[intro]:

   755   assumes "bounded S"

   756   shows "bounded (closure S)"

   757 proof -

   758   from assms obtain x and a where a: "\<forall>y\<in>S. dist x y \<le> a"

   759     unfolding bounded_def by auto

   760   {

   761     fix y

   762     assume "y \<in> closure S"

   763     then obtain f where f: "\<forall>n. f n \<in> S"  "(f \<longlongrightarrow> y) sequentially"

   764       unfolding closure_sequential by auto

   765     have "\<forall>n. f n \<in> S \<longrightarrow> dist x (f n) \<le> a" using a by simp

   766     then have "eventually (\<lambda>n. dist x (f n) \<le> a) sequentially"

   767       by (simp add: f(1))

   768     have "dist x y \<le> a"

   769       apply (rule Lim_dist_ubound [of sequentially f])

   770       apply (rule trivial_limit_sequentially)

   771       apply (rule f(2))

   772       apply fact

   773       done

   774   }

   775   then show ?thesis

   776     unfolding bounded_def by auto

   777 qed

   778

   779 lemma bounded_closure_image: "bounded (f  closure S) \<Longrightarrow> bounded (f  S)"

   780   by (simp add: bounded_subset closure_subset image_mono)

   781

   782 lemma bounded_cball[simp,intro]: "bounded (cball x e)"

   783   apply (simp add: bounded_def)

   784   apply (rule_tac x=x in exI)

   785   apply (rule_tac x=e in exI, auto)

   786   done

   787

   788 lemma bounded_ball[simp,intro]: "bounded (ball x e)"

   789   by (metis ball_subset_cball bounded_cball bounded_subset)

   790

   791 lemma bounded_Un[simp]: "bounded (S \<union> T) \<longleftrightarrow> bounded S \<and> bounded T"

   792   by (auto simp: bounded_def) (metis Un_iff bounded_any_center le_max_iff_disj)

   793

   794 lemma bounded_Union[intro]: "finite F \<Longrightarrow> \<forall>S\<in>F. bounded S \<Longrightarrow> bounded (\<Union>F)"

   795   by (induct rule: finite_induct[of F]) auto

   796

   797 lemma bounded_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. bounded (B x) \<Longrightarrow> bounded (\<Union>x\<in>A. B x)"

   798   by (induct set: finite) auto

   799

   800 lemma bounded_insert [simp]: "bounded (insert x S) \<longleftrightarrow> bounded S"

   801 proof -

   802   have "\<forall>y\<in>{x}. dist x y \<le> 0"

   803     by simp

   804   then have "bounded {x}"

   805     unfolding bounded_def by fast

   806   then show ?thesis

   807     by (metis insert_is_Un bounded_Un)

   808 qed

   809

   810 lemma bounded_subset_ballI: "S \<subseteq> ball x r \<Longrightarrow> bounded S"

   811   by (meson bounded_ball bounded_subset)

   812

   813 lemma bounded_subset_ballD:

   814   assumes "bounded S" shows "\<exists>r. 0 < r \<and> S \<subseteq> ball x r"

   815 proof -

   816   obtain e::real and y where "S \<subseteq> cball y e"  "0 \<le> e"

   817     using assms by (auto simp: bounded_subset_cball)

   818   then show ?thesis

   819     apply (rule_tac x="dist x y + e + 1" in exI)

   820     apply (simp add: add.commute add_pos_nonneg)

   821     apply (erule subset_trans)

   822     apply (clarsimp simp add: cball_def)

   823     by (metis add_le_cancel_right add_strict_increasing dist_commute dist_triangle_le zero_less_one)

   824 qed

   825

   826 lemma finite_imp_bounded [intro]: "finite S \<Longrightarrow> bounded S"

   827   by (induct set: finite) simp_all

   828

   829 lemma bounded_Int[intro]: "bounded S \<or> bounded T \<Longrightarrow> bounded (S \<inter> T)"

   830   by (metis Int_lower1 Int_lower2 bounded_subset)

   831

   832 lemma bounded_diff[intro]: "bounded S \<Longrightarrow> bounded (S - T)"

   833   by (metis Diff_subset bounded_subset)

   834

   835 lemma bounded_dist_comp:

   836   assumes "bounded (f  S)" "bounded (g  S)"

   837   shows "bounded ((\<lambda>x. dist (f x) (g x))  S)"

   838 proof -

   839   from assms obtain M1 M2 where *: "dist (f x) undefined \<le> M1" "dist undefined (g x) \<le> M2" if "x \<in> S" for x

   840     by (auto simp: bounded_any_center[of _ undefined] dist_commute)

   841   have "dist (f x) (g x) \<le> M1 + M2" if "x \<in> S" for x

   842     using *[OF that]

   843     by (rule order_trans[OF dist_triangle add_mono])

   844   then show ?thesis

   845     by (auto intro!: boundedI)

   846 qed

   847

   848 lemma bounded_Times:

   849   assumes "bounded s" "bounded t"

   850   shows "bounded (s \<times> t)"

   851 proof -

   852   obtain x y a b where "\<forall>z\<in>s. dist x z \<le> a" "\<forall>z\<in>t. dist y z \<le> b"

   853     using assms [unfolded bounded_def] by auto

   854   then have "\<forall>z\<in>s \<times> t. dist (x, y) z \<le> sqrt (a\<^sup>2 + b\<^sup>2)"

   855     by (auto simp: dist_Pair_Pair real_sqrt_le_mono add_mono power_mono)

   856   then show ?thesis unfolding bounded_any_center [where a="(x, y)"] by auto

   857 qed

   858

   859

   860 subsection \<open>Compactness\<close>

   861

   862 lemma compact_imp_bounded:

   863   assumes "compact U"

   864   shows "bounded U"

   865 proof -

   866   have "compact U" "\<forall>x\<in>U. open (ball x 1)" "U \<subseteq> (\<Union>x\<in>U. ball x 1)"

   867     using assms by auto

   868   then obtain D where D: "D \<subseteq> U" "finite D" "U \<subseteq> (\<Union>x\<in>D. ball x 1)"

   869     by (metis compactE_image)

   870   from \<open>finite D\<close> have "bounded (\<Union>x\<in>D. ball x 1)"

   871     by (simp add: bounded_UN)

   872   then show "bounded U" using \<open>U \<subseteq> (\<Union>x\<in>D. ball x 1)\<close>

   873     by (rule bounded_subset)

   874 qed

   875

   876 lemma closure_Int_ball_not_empty:

   877   assumes "S \<subseteq> closure T" "x \<in> S" "r > 0"

   878   shows "T \<inter> ball x r \<noteq> {}"

   879   using assms centre_in_ball closure_iff_nhds_not_empty by blast

   880

   881 lemma compact_sup_maxdistance:

   882   fixes s :: "'a::metric_space set"

   883   assumes "compact s"

   884     and "s \<noteq> {}"

   885   shows "\<exists>x\<in>s. \<exists>y\<in>s. \<forall>u\<in>s. \<forall>v\<in>s. dist u v \<le> dist x y"

   886 proof -

   887   have "compact (s \<times> s)"

   888     using \<open>compact s\<close> by (intro compact_Times)

   889   moreover have "s \<times> s \<noteq> {}"

   890     using \<open>s \<noteq> {}\<close> by auto

   891   moreover have "continuous_on (s \<times> s) (\<lambda>x. dist (fst x) (snd x))"

   892     by (intro continuous_at_imp_continuous_on ballI continuous_intros)

   893   ultimately show ?thesis

   894     using continuous_attains_sup[of "s \<times> s" "\<lambda>x. dist (fst x) (snd x)"] by auto

   895 qed

   896

   897

   898 subsubsection\<open>Totally bounded\<close>

   899

   900 lemma cauchy_def: "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N \<longrightarrow> dist (s m) (s n) < e)"

   901   unfolding Cauchy_def by metis

   902

   903 proposition seq_compact_imp_totally_bounded:

   904   assumes "seq_compact s"

   905   shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>k. ball x e)"

   906 proof -

   907   { fix e::real assume "e > 0" assume *: "\<And>k. finite k \<Longrightarrow> k \<subseteq> s \<Longrightarrow> \<not> s \<subseteq> (\<Union>x\<in>k. ball x e)"

   908     let ?Q = "\<lambda>x n r. r \<in> s \<and> (\<forall>m < (n::nat). \<not> (dist (x m) r < e))"

   909     have "\<exists>x. \<forall>n::nat. ?Q x n (x n)"

   910     proof (rule dependent_wellorder_choice)

   911       fix n x assume "\<And>y. y < n \<Longrightarrow> ?Q x y (x y)"

   912       then have "\<not> s \<subseteq> (\<Union>x\<in>x  {0..<n}. ball x e)"

   913         using *[of "x  {0 ..< n}"] by (auto simp: subset_eq)

   914       then obtain z where z:"z\<in>s" "z \<notin> (\<Union>x\<in>x  {0..<n}. ball x e)"

   915         unfolding subset_eq by auto

   916       show "\<exists>r. ?Q x n r"

   917         using z by auto

   918     qed simp

   919     then obtain x where "\<forall>n::nat. x n \<in> s" and x:"\<And>n m. m < n \<Longrightarrow> \<not> (dist (x m) (x n) < e)"

   920       by blast

   921     then obtain l r where "l \<in> s" and r:"strict_mono  r" and "((x \<circ> r) \<longlongrightarrow> l) sequentially"

   922       using assms by (metis seq_compact_def)

   923     from this(3) have "Cauchy (x \<circ> r)"

   924       using LIMSEQ_imp_Cauchy by auto

   925     then obtain N::nat where "\<And>m n. N \<le> m \<Longrightarrow> N \<le> n \<Longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e"

   926       unfolding cauchy_def using \<open>e > 0\<close> by blast

   927     then have False

   928       using x[of "r N" "r (N+1)"] r by (auto simp: strict_mono_def) }

   929   then show ?thesis

   930     by metis

   931 qed

   932

   933 subsubsection\<open>Heine-Borel theorem\<close>

   934

   935 proposition seq_compact_imp_Heine_Borel:

   936   fixes s :: "'a :: metric_space set"

   937   assumes "seq_compact s"

   938   shows "compact s"

   939 proof -

   940   from seq_compact_imp_totally_bounded[OF \<open>seq_compact s\<close>]

   941   obtain f where f: "\<forall>e>0. finite (f e) \<and> f e \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>f e. ball x e)"

   942     unfolding choice_iff' ..

   943   define K where "K = (\<lambda>(x, r). ball x r)  ((\<Union>e \<in> \<rat> \<inter> {0 <..}. f e) \<times> \<rat>)"

   944   have "countably_compact s"

   945     using \<open>seq_compact s\<close> by (rule seq_compact_imp_countably_compact)

   946   then show "compact s"

   947   proof (rule countably_compact_imp_compact)

   948     show "countable K"

   949       unfolding K_def using f

   950       by (auto intro: countable_finite countable_subset countable_rat

   951                intro!: countable_image countable_SIGMA countable_UN)

   952     show "\<forall>b\<in>K. open b" by (auto simp: K_def)

   953   next

   954     fix T x

   955     assume T: "open T" "x \<in> T" and x: "x \<in> s"

   956     from openE[OF T] obtain e where "0 < e" "ball x e \<subseteq> T"

   957       by auto

   958     then have "0 < e / 2" "ball x (e / 2) \<subseteq> T"

   959       by auto

   960     from Rats_dense_in_real[OF \<open>0 < e / 2\<close>] obtain r where "r \<in> \<rat>" "0 < r" "r < e / 2"

   961       by auto

   962     from f[rule_format, of r] \<open>0 < r\<close> \<open>x \<in> s\<close> obtain k where "k \<in> f r" "x \<in> ball k r"

   963       by auto

   964     from \<open>r \<in> \<rat>\<close> \<open>0 < r\<close> \<open>k \<in> f r\<close> have "ball k r \<in> K"

   965       by (auto simp: K_def)

   966     then show "\<exists>b\<in>K. x \<in> b \<and> b \<inter> s \<subseteq> T"

   967     proof (rule bexI[rotated], safe)

   968       fix y

   969       assume "y \<in> ball k r"

   970       with \<open>r < e / 2\<close> \<open>x \<in> ball k r\<close> have "dist x y < e"

   971         by (intro dist_triangle_half_r [of k _ e]) (auto simp: dist_commute)

   972       with \<open>ball x e \<subseteq> T\<close> show "y \<in> T"

   973         by auto

   974     next

   975       show "x \<in> ball k r" by fact

   976     qed

   977   qed

   978 qed

   979

   980 proposition compact_eq_seq_compact_metric:

   981   "compact (s :: 'a::metric_space set) \<longleftrightarrow> seq_compact s"

   982   using compact_imp_seq_compact seq_compact_imp_Heine_Borel by blast

   983

   984 proposition compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close>

   985   "compact (S :: 'a::metric_space set) \<longleftrightarrow>

   986    (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l))"

   987   unfolding compact_eq_seq_compact_metric seq_compact_def by auto

   988

   989 subsubsection \<open>Complete the chain of compactness variants\<close>

   990

   991 proposition compact_eq_Bolzano_Weierstrass:

   992   fixes s :: "'a::metric_space set"

   993   shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))"

   994   (is "?lhs = ?rhs")

   995 proof

   996   assume ?lhs

   997   then show ?rhs

   998     using Heine_Borel_imp_Bolzano_Weierstrass[of s] by auto

   999 next

  1000   assume ?rhs

  1001   then show ?lhs

  1002     unfolding compact_eq_seq_compact_metric by (rule Bolzano_Weierstrass_imp_seq_compact)

  1003 qed

  1004

  1005 proposition Bolzano_Weierstrass_imp_bounded:

  1006   "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> bounded s"

  1007   using compact_imp_bounded unfolding compact_eq_Bolzano_Weierstrass .

  1008

  1009

  1010 subsection \<open>Banach fixed point theorem\<close>

  1011

  1012 theorem banach_fix:\<comment> \<open>TODO: rename to \<open>Banach_fix\<close>\<close>

  1013   assumes s: "complete s" "s \<noteq> {}"

  1014     and c: "0 \<le> c" "c < 1"

  1015     and f: "f  s \<subseteq> s"

  1016     and lipschitz: "\<forall>x\<in>s. \<forall>y\<in>s. dist (f x) (f y) \<le> c * dist x y"

  1017   shows "\<exists>!x\<in>s. f x = x"

  1018 proof -

  1019   from c have "1 - c > 0" by simp

  1020

  1021   from s(2) obtain z0 where z0: "z0 \<in> s" by blast

  1022   define z where "z n = (f ^^ n) z0" for n

  1023   with f z0 have z_in_s: "z n \<in> s" for n :: nat

  1024     by (induct n) auto

  1025   define d where "d = dist (z 0) (z 1)"

  1026

  1027   have fzn: "f (z n) = z (Suc n)" for n

  1028     by (simp add: z_def)

  1029   have cf_z: "dist (z n) (z (Suc n)) \<le> (c ^ n) * d" for n :: nat

  1030   proof (induct n)

  1031     case 0

  1032     then show ?case

  1033       by (simp add: d_def)

  1034   next

  1035     case (Suc m)

  1036     with \<open>0 \<le> c\<close> have "c * dist (z m) (z (Suc m)) \<le> c ^ Suc m * d"

  1037       using mult_left_mono[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by simp

  1038     then show ?case

  1039       using lipschitz[THEN bspec[where x="z m"], OF z_in_s, THEN bspec[where x="z (Suc m)"], OF z_in_s]

  1040       by (simp add: fzn mult_le_cancel_left)

  1041   qed

  1042

  1043   have cf_z2: "(1 - c) * dist (z m) (z (m + n)) \<le> (c ^ m) * d * (1 - c ^ n)" for n m :: nat

  1044   proof (induct n)

  1045     case 0

  1046     show ?case by simp

  1047   next

  1048     case (Suc k)

  1049     from c have "(1 - c) * dist (z m) (z (m + Suc k)) \<le>

  1050         (1 - c) * (dist (z m) (z (m + k)) + dist (z (m + k)) (z (Suc (m + k))))"

  1051       by (simp add: dist_triangle)

  1052     also from c cf_z[of "m + k"] have "\<dots> \<le> (1 - c) * (dist (z m) (z (m + k)) + c ^ (m + k) * d)"

  1053       by simp

  1054     also from Suc have "\<dots> \<le> c ^ m * d * (1 - c ^ k) + (1 - c) * c ^ (m + k) * d"

  1055       by (simp add: field_simps)

  1056     also have "\<dots> = (c ^ m) * (d * (1 - c ^ k) + (1 - c) * c ^ k * d)"

  1057       by (simp add: power_add field_simps)

  1058     also from c have "\<dots> \<le> (c ^ m) * d * (1 - c ^ Suc k)"

  1059       by (simp add: field_simps)

  1060     finally show ?case by simp

  1061   qed

  1062

  1063   have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (z m) (z n) < e" if "e > 0" for e

  1064   proof (cases "d = 0")

  1065     case True

  1066     from \<open>1 - c > 0\<close> have "(1 - c) * x \<le> 0 \<longleftrightarrow> x \<le> 0" for x

  1067       by (metis mult_zero_left mult.commute real_mult_le_cancel_iff1)

  1068     with c cf_z2[of 0] True have "z n = z0" for n

  1069       by (simp add: z_def)

  1070     with \<open>e > 0\<close> show ?thesis by simp

  1071   next

  1072     case False

  1073     with zero_le_dist[of "z 0" "z 1"] have "d > 0"

  1074       by (metis d_def less_le)

  1075     with \<open>1 - c > 0\<close> \<open>e > 0\<close> have "0 < e * (1 - c) / d"

  1076       by simp

  1077     with c obtain N where N: "c ^ N < e * (1 - c) / d"

  1078       using real_arch_pow_inv[of "e * (1 - c) / d" c] by auto

  1079     have *: "dist (z m) (z n) < e" if "m > n" and as: "m \<ge> N" "n \<ge> N" for m n :: nat

  1080     proof -

  1081       from c \<open>n \<ge> N\<close> have *: "c ^ n \<le> c ^ N"

  1082         using power_decreasing[OF \<open>n\<ge>N\<close>, of c] by simp

  1083       from c \<open>m > n\<close> have "1 - c ^ (m - n) > 0"

  1084         using power_strict_mono[of c 1 "m - n"] by simp

  1085       with \<open>d > 0\<close> \<open>0 < 1 - c\<close> have **: "d * (1 - c ^ (m - n)) / (1 - c) > 0"

  1086         by simp

  1087       from cf_z2[of n "m - n"] \<open>m > n\<close>

  1088       have "dist (z m) (z n) \<le> c ^ n * d * (1 - c ^ (m - n)) / (1 - c)"

  1089         by (simp add: pos_le_divide_eq[OF \<open>1 - c > 0\<close>] mult.commute dist_commute)

  1090       also have "\<dots> \<le> c ^ N * d * (1 - c ^ (m - n)) / (1 - c)"

  1091         using mult_right_mono[OF * order_less_imp_le[OF **]]

  1092         by (simp add: mult.assoc)

  1093       also have "\<dots> < (e * (1 - c) / d) * d * (1 - c ^ (m - n)) / (1 - c)"

  1094         using mult_strict_right_mono[OF N **] by (auto simp: mult.assoc)

  1095       also from c \<open>d > 0\<close> \<open>1 - c > 0\<close> have "\<dots> = e * (1 - c ^ (m - n))"

  1096         by simp

  1097       also from c \<open>1 - c ^ (m - n) > 0\<close> \<open>e > 0\<close> have "\<dots> \<le> e"

  1098         using mult_right_le_one_le[of e "1 - c ^ (m - n)"] by auto

  1099       finally show ?thesis by simp

  1100     qed

  1101     have "dist (z n) (z m) < e" if "N \<le> m" "N \<le> n" for m n :: nat

  1102     proof (cases "n = m")

  1103       case True

  1104       with \<open>e > 0\<close> show ?thesis by simp

  1105     next

  1106       case False

  1107       with *[of n m] *[of m n] and that show ?thesis

  1108         by (auto simp: dist_commute nat_neq_iff)

  1109     qed

  1110     then show ?thesis by auto

  1111   qed

  1112   then have "Cauchy z"

  1113     by (simp add: cauchy_def)

  1114   then obtain x where "x\<in>s" and x:"(z \<longlongrightarrow> x) sequentially"

  1115     using s(1)[unfolded compact_def complete_def, THEN spec[where x=z]] and z_in_s by auto

  1116

  1117   define e where "e = dist (f x) x"

  1118   have "e = 0"

  1119   proof (rule ccontr)

  1120     assume "e \<noteq> 0"

  1121     then have "e > 0"

  1122       unfolding e_def using zero_le_dist[of "f x" x]

  1123       by (metis dist_eq_0_iff dist_nz e_def)

  1124     then obtain N where N:"\<forall>n\<ge>N. dist (z n) x < e / 2"

  1125       using x[unfolded lim_sequentially, THEN spec[where x="e/2"]] by auto

  1126     then have N':"dist (z N) x < e / 2" by auto

  1127     have *: "c * dist (z N) x \<le> dist (z N) x"

  1128       unfolding mult_le_cancel_right2

  1129       using zero_le_dist[of "z N" x] and c

  1130       by (metis dist_eq_0_iff dist_nz order_less_asym less_le)

  1131     have "dist (f (z N)) (f x) \<le> c * dist (z N) x"

  1132       using lipschitz[THEN bspec[where x="z N"], THEN bspec[where x=x]]

  1133       using z_in_s[of N] \<open>x\<in>s\<close>

  1134       using c

  1135       by auto

  1136     also have "\<dots> < e / 2"

  1137       using N' and c using * by auto

  1138     finally show False

  1139       unfolding fzn

  1140       using N[THEN spec[where x="Suc N"]] and dist_triangle_half_r[of "z (Suc N)" "f x" e x]

  1141       unfolding e_def

  1142       by auto

  1143   qed

  1144   then have "f x = x" by (auto simp: e_def)

  1145   moreover have "y = x" if "f y = y" "y \<in> s" for y

  1146   proof -

  1147     from \<open>x \<in> s\<close> \<open>f x = x\<close> that have "dist x y \<le> c * dist x y"

  1148       using lipschitz[THEN bspec[where x=x], THEN bspec[where x=y]] by simp

  1149     with c and zero_le_dist[of x y] have "dist x y = 0"

  1150       by (simp add: mult_le_cancel_right1)

  1151     then show ?thesis by simp

  1152   qed

  1153   ultimately show ?thesis

  1154     using \<open>x\<in>s\<close> by blast

  1155 qed

  1156

  1157

  1158 subsection \<open>Edelstein fixed point theorem\<close>

  1159

  1160 theorem edelstein_fix:\<comment> \<open>TODO: rename to \<open>Edelstein_fix\<close>\<close>

  1161   fixes s :: "'a::metric_space set"

  1162   assumes s: "compact s" "s \<noteq> {}"

  1163     and gs: "(g  s) \<subseteq> s"

  1164     and dist: "\<forall>x\<in>s. \<forall>y\<in>s. x \<noteq> y \<longrightarrow> dist (g x) (g y) < dist x y"

  1165   shows "\<exists>!x\<in>s. g x = x"

  1166 proof -

  1167   let ?D = "(\<lambda>x. (x, x))  s"

  1168   have D: "compact ?D" "?D \<noteq> {}"

  1169     by (rule compact_continuous_image)

  1170        (auto intro!: s continuous_Pair continuous_ident simp: continuous_on_eq_continuous_within)

  1171

  1172   have "\<And>x y e. x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> 0 < e \<Longrightarrow> dist y x < e \<Longrightarrow> dist (g y) (g x) < e"

  1173     using dist by fastforce

  1174   then have "continuous_on s g"

  1175     by (auto simp: continuous_on_iff)

  1176   then have cont: "continuous_on ?D (\<lambda>x. dist ((g \<circ> fst) x) (snd x))"

  1177     unfolding continuous_on_eq_continuous_within

  1178     by (intro continuous_dist ballI continuous_within_compose)

  1179        (auto intro!: continuous_fst continuous_snd continuous_ident simp: image_image)

  1180

  1181   obtain a where "a \<in> s" and le: "\<And>x. x \<in> s \<Longrightarrow> dist (g a) a \<le> dist (g x) x"

  1182     using continuous_attains_inf[OF D cont] by auto

  1183

  1184   have "g a = a"

  1185   proof (rule ccontr)

  1186     assume "g a \<noteq> a"

  1187     with \<open>a \<in> s\<close> gs have "dist (g (g a)) (g a) < dist (g a) a"

  1188       by (intro dist[rule_format]) auto

  1189     moreover have "dist (g a) a \<le> dist (g (g a)) (g a)"

  1190       using \<open>a \<in> s\<close> gs by (intro le) auto

  1191     ultimately show False by auto

  1192   qed

  1193   moreover have "\<And>x. x \<in> s \<Longrightarrow> g x = x \<Longrightarrow> x = a"

  1194     using dist[THEN bspec[where x=a]] \<open>g a = a\<close> and \<open>a\<in>s\<close> by auto

  1195   ultimately show "\<exists>!x\<in>s. g x = x"

  1196     using \<open>a \<in> s\<close> by blast

  1197 qed

  1198

  1199 subsection \<open>The diameter of a set\<close>

  1200

  1201 definition%important diameter :: "'a::metric_space set \<Rightarrow> real" where

  1202   "diameter S = (if S = {} then 0 else SUP (x,y)\<in>S\<times>S. dist x y)"

  1203

  1204 lemma diameter_empty [simp]: "diameter{} = 0"

  1205   by (auto simp: diameter_def)

  1206

  1207 lemma diameter_singleton [simp]: "diameter{x} = 0"

  1208   by (auto simp: diameter_def)

  1209

  1210 lemma diameter_le:

  1211   assumes "S \<noteq> {} \<or> 0 \<le> d"

  1212       and no: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> norm(x - y) \<le> d"

  1213     shows "diameter S \<le> d"

  1214 using assms

  1215   by (auto simp: dist_norm diameter_def intro: cSUP_least)

  1216

  1217 lemma diameter_bounded_bound:

  1218   fixes s :: "'a :: metric_space set"

  1219   assumes s: "bounded s" "x \<in> s" "y \<in> s"

  1220   shows "dist x y \<le> diameter s"

  1221 proof -

  1222   from s obtain z d where z: "\<And>x. x \<in> s \<Longrightarrow> dist z x \<le> d"

  1223     unfolding bounded_def by auto

  1224   have "bdd_above (case_prod dist  (s\<times>s))"

  1225   proof (intro bdd_aboveI, safe)

  1226     fix a b

  1227     assume "a \<in> s" "b \<in> s"

  1228     with z[of a] z[of b] dist_triangle[of a b z]

  1229     show "dist a b \<le> 2 * d"

  1230       by (simp add: dist_commute)

  1231   qed

  1232   moreover have "(x,y) \<in> s\<times>s" using s by auto

  1233   ultimately have "dist x y \<le> (SUP (x,y)\<in>s\<times>s. dist x y)"

  1234     by (rule cSUP_upper2) simp

  1235   with \<open>x \<in> s\<close> show ?thesis

  1236     by (auto simp: diameter_def)

  1237 qed

  1238

  1239 lemma diameter_lower_bounded:

  1240   fixes s :: "'a :: metric_space set"

  1241   assumes s: "bounded s"

  1242     and d: "0 < d" "d < diameter s"

  1243   shows "\<exists>x\<in>s. \<exists>y\<in>s. d < dist x y"

  1244 proof (rule ccontr)

  1245   assume contr: "\<not> ?thesis"

  1246   moreover have "s \<noteq> {}"

  1247     using d by (auto simp: diameter_def)

  1248   ultimately have "diameter s \<le> d"

  1249     by (auto simp: not_less diameter_def intro!: cSUP_least)

  1250   with \<open>d < diameter s\<close> show False by auto

  1251 qed

  1252

  1253 lemma diameter_bounded:

  1254   assumes "bounded s"

  1255   shows "\<forall>x\<in>s. \<forall>y\<in>s. dist x y \<le> diameter s"

  1256     and "\<forall>d>0. d < diameter s \<longrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. dist x y > d)"

  1257   using diameter_bounded_bound[of s] diameter_lower_bounded[of s] assms

  1258   by auto

  1259

  1260 lemma bounded_two_points:

  1261   "bounded S \<longleftrightarrow> (\<exists>e. \<forall>x\<in>S. \<forall>y\<in>S. dist x y \<le> e)"

  1262   apply (rule iffI)

  1263   subgoal using diameter_bounded(1) by auto

  1264   subgoal using bounded_any_center[of S] by meson

  1265   done

  1266

  1267 lemma diameter_compact_attained:

  1268   assumes "compact s"

  1269     and "s \<noteq> {}"

  1270   shows "\<exists>x\<in>s. \<exists>y\<in>s. dist x y = diameter s"

  1271 proof -

  1272   have b: "bounded s" using assms(1)

  1273     by (rule compact_imp_bounded)

  1274   then obtain x y where xys: "x\<in>s" "y\<in>s"

  1275     and xy: "\<forall>u\<in>s. \<forall>v\<in>s. dist u v \<le> dist x y"

  1276     using compact_sup_maxdistance[OF assms] by auto

  1277   then have "diameter s \<le> dist x y"

  1278     unfolding diameter_def

  1279     apply clarsimp

  1280     apply (rule cSUP_least, fast+)

  1281     done

  1282   then show ?thesis

  1283     by (metis b diameter_bounded_bound order_antisym xys)

  1284 qed

  1285

  1286 lemma diameter_ge_0:

  1287   assumes "bounded S"  shows "0 \<le> diameter S"

  1288   by (metis all_not_in_conv assms diameter_bounded_bound diameter_empty dist_self order_refl)

  1289

  1290 lemma diameter_subset:

  1291   assumes "S \<subseteq> T" "bounded T"

  1292   shows "diameter S \<le> diameter T"

  1293 proof (cases "S = {} \<or> T = {}")

  1294   case True

  1295   with assms show ?thesis

  1296     by (force simp: diameter_ge_0)

  1297 next

  1298   case False

  1299   then have "bdd_above ((\<lambda>x. case x of (x, xa) \<Rightarrow> dist x xa)  (T \<times> T))"

  1300     using \<open>bounded T\<close> diameter_bounded_bound by (force simp: bdd_above_def)

  1301   with False \<open>S \<subseteq> T\<close> show ?thesis

  1302     apply (simp add: diameter_def)

  1303     apply (rule cSUP_subset_mono, auto)

  1304     done

  1305 qed

  1306

  1307 lemma diameter_closure:

  1308   assumes "bounded S"

  1309   shows "diameter(closure S) = diameter S"

  1310 proof (rule order_antisym)

  1311   have "False" if "diameter S < diameter (closure S)"

  1312   proof -

  1313     define d where "d = diameter(closure S) - diameter(S)"

  1314     have "d > 0"

  1315       using that by (simp add: d_def)

  1316     then have "diameter(closure(S)) - d / 2 < diameter(closure(S))"

  1317       by simp

  1318     have dd: "diameter (closure S) - d / 2 = (diameter(closure(S)) + diameter(S)) / 2"

  1319       by (simp add: d_def divide_simps)

  1320      have bocl: "bounded (closure S)"

  1321       using assms by blast

  1322     moreover have "0 \<le> diameter S"

  1323       using assms diameter_ge_0 by blast

  1324     ultimately obtain x y where "x \<in> closure S" "y \<in> closure S" and xy: "diameter(closure(S)) - d / 2 < dist x y"

  1325       using diameter_bounded(2) [OF bocl, rule_format, of "diameter(closure(S)) - d / 2"] \<open>d > 0\<close> d_def by auto

  1326     then obtain x' y' where x'y': "x' \<in> S" "dist x' x < d/4" "y' \<in> S" "dist y' y < d/4"

  1327       using closure_approachable

  1328       by (metis \<open>0 < d\<close> zero_less_divide_iff zero_less_numeral)

  1329     then have "dist x' y' \<le> diameter S"

  1330       using assms diameter_bounded_bound by blast

  1331     with x'y' have "dist x y \<le> d / 4 + diameter S + d / 4"

  1332       by (meson add_mono_thms_linordered_semiring(1) dist_triangle dist_triangle3 less_eq_real_def order_trans)

  1333     then show ?thesis

  1334       using xy d_def by linarith

  1335   qed

  1336   then show "diameter (closure S) \<le> diameter S"

  1337     by fastforce

  1338   next

  1339     show "diameter S \<le> diameter (closure S)"

  1340       by (simp add: assms bounded_closure closure_subset diameter_subset)

  1341 qed

  1342

  1343 proposition Lebesgue_number_lemma:

  1344   assumes "compact S" "\<C> \<noteq> {}" "S \<subseteq> \<Union>\<C>" and ope: "\<And>B. B \<in> \<C> \<Longrightarrow> open B"

  1345   obtains \<delta> where "0 < \<delta>" "\<And>T. \<lbrakk>T \<subseteq> S; diameter T < \<delta>\<rbrakk> \<Longrightarrow> \<exists>B \<in> \<C>. T \<subseteq> B"

  1346 proof (cases "S = {}")

  1347   case True

  1348   then show ?thesis

  1349     by (metis \<open>\<C> \<noteq> {}\<close> zero_less_one empty_subsetI equals0I subset_trans that)

  1350 next

  1351   case False

  1352   { fix x assume "x \<in> S"

  1353     then obtain C where C: "x \<in> C" "C \<in> \<C>"

  1354       using \<open>S \<subseteq> \<Union>\<C>\<close> by blast

  1355     then obtain r where r: "r>0" "ball x (2*r) \<subseteq> C"

  1356       by (metis mult.commute mult_2_right not_le ope openE field_sum_of_halves zero_le_numeral zero_less_mult_iff)

  1357     then have "\<exists>r C. r > 0 \<and> ball x (2*r) \<subseteq> C \<and> C \<in> \<C>"

  1358       using C by blast

  1359   }

  1360   then obtain r where r: "\<And>x. x \<in> S \<Longrightarrow> r x > 0 \<and> (\<exists>C \<in> \<C>. ball x (2*r x) \<subseteq> C)"

  1361     by metis

  1362   then have "S \<subseteq> (\<Union>x \<in> S. ball x (r x))"

  1363     by auto

  1364   then obtain \<T> where "finite \<T>" "S \<subseteq> \<Union>\<T>" and \<T>: "\<T> \<subseteq> (\<lambda>x. ball x (r x))  S"

  1365     by (rule compactE [OF \<open>compact S\<close>]) auto

  1366   then obtain S0 where "S0 \<subseteq> S" "finite S0" and S0: "\<T> = (\<lambda>x. ball x (r x))  S0"

  1367     by (meson finite_subset_image)

  1368   then have "S0 \<noteq> {}"

  1369     using False \<open>S \<subseteq> \<Union>\<T>\<close> by auto

  1370   define \<delta> where "\<delta> = Inf (r  S0)"

  1371   have "\<delta> > 0"

  1372     using \<open>finite S0\<close> \<open>S0 \<subseteq> S\<close> \<open>S0 \<noteq> {}\<close> r by (auto simp: \<delta>_def finite_less_Inf_iff)

  1373   show ?thesis

  1374   proof

  1375     show "0 < \<delta>"

  1376       by (simp add: \<open>0 < \<delta>\<close>)

  1377     show "\<exists>B \<in> \<C>. T \<subseteq> B" if "T \<subseteq> S" and dia: "diameter T < \<delta>" for T

  1378     proof (cases "T = {}")

  1379       case True

  1380       then show ?thesis

  1381         using \<open>\<C> \<noteq> {}\<close> by blast

  1382     next

  1383       case False

  1384       then obtain y where "y \<in> T" by blast

  1385       then have "y \<in> S"

  1386         using \<open>T \<subseteq> S\<close> by auto

  1387       then obtain x where "x \<in> S0" and x: "y \<in> ball x (r x)"

  1388         using \<open>S \<subseteq> \<Union>\<T>\<close> S0 that by blast

  1389       have "ball y \<delta> \<subseteq> ball y (r x)"

  1390         by (metis \<delta>_def \<open>S0 \<noteq> {}\<close> \<open>finite S0\<close> \<open>x \<in> S0\<close> empty_is_image finite_imageI finite_less_Inf_iff imageI less_irrefl not_le subset_ball)

  1391       also have "... \<subseteq> ball x (2*r x)"

  1392         by clarsimp (metis dist_commute dist_triangle_less_add mem_ball mult_2 x)

  1393       finally obtain C where "C \<in> \<C>" "ball y \<delta> \<subseteq> C"

  1394         by (meson r \<open>S0 \<subseteq> S\<close> \<open>x \<in> S0\<close> dual_order.trans subsetCE)

  1395       have "bounded T"

  1396         using \<open>compact S\<close> bounded_subset compact_imp_bounded \<open>T \<subseteq> S\<close> by blast

  1397       then have "T \<subseteq> ball y \<delta>"

  1398         using \<open>y \<in> T\<close> dia diameter_bounded_bound by fastforce

  1399       then show ?thesis

  1400         apply (rule_tac x=C in bexI)

  1401         using \<open>ball y \<delta> \<subseteq> C\<close> \<open>C \<in> \<C>\<close> by auto

  1402     qed

  1403   qed

  1404 qed

  1405

  1406

  1407 subsection \<open>Metric spaces with the Heine-Borel property\<close>

  1408

  1409 text \<open>

  1410   A metric space (or topological vector space) is said to have the

  1411   Heine-Borel property if every closed and bounded subset is compact.

  1412 \<close>

  1413

  1414 class heine_borel = metric_space +

  1415   assumes bounded_imp_convergent_subsequence:

  1416     "bounded (range f) \<Longrightarrow> \<exists>l r. strict_mono (r::nat\<Rightarrow>nat) \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"

  1417

  1418 proposition bounded_closed_imp_seq_compact:

  1419   fixes s::"'a::heine_borel set"

  1420   assumes "bounded s"

  1421     and "closed s"

  1422   shows "seq_compact s"

  1423 proof (unfold seq_compact_def, clarify)

  1424   fix f :: "nat \<Rightarrow> 'a"

  1425   assume f: "\<forall>n. f n \<in> s"

  1426   with \<open>bounded s\<close> have "bounded (range f)"

  1427     by (auto intro: bounded_subset)

  1428   obtain l r where r: "strict_mono (r :: nat \<Rightarrow> nat)" and l: "((f \<circ> r) \<longlongrightarrow> l) sequentially"

  1429     using bounded_imp_convergent_subsequence [OF \<open>bounded (range f)\<close>] by auto

  1430   from f have fr: "\<forall>n. (f \<circ> r) n \<in> s"

  1431     by simp

  1432   have "l \<in> s" using \<open>closed s\<close> fr l

  1433     by (rule closed_sequentially)

  1434   show "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"

  1435     using \<open>l \<in> s\<close> r l by blast

  1436 qed

  1437

  1438 lemma compact_eq_bounded_closed:

  1439   fixes s :: "'a::heine_borel set"

  1440   shows "compact s \<longleftrightarrow> bounded s \<and> closed s"

  1441   (is "?lhs = ?rhs")

  1442 proof

  1443   assume ?lhs

  1444   then show ?rhs

  1445     using compact_imp_closed compact_imp_bounded

  1446     by blast

  1447 next

  1448   assume ?rhs

  1449   then show ?lhs

  1450     using bounded_closed_imp_seq_compact[of s]

  1451     unfolding compact_eq_seq_compact_metric

  1452     by auto

  1453 qed

  1454

  1455 lemma compact_Inter:

  1456   fixes \<F> :: "'a :: heine_borel set set"

  1457   assumes com: "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" and "\<F> \<noteq> {}"

  1458   shows "compact(\<Inter> \<F>)"

  1459   using assms

  1460   by (meson Inf_lower all_not_in_conv bounded_subset closed_Inter compact_eq_bounded_closed)

  1461

  1462 lemma compact_closure [simp]:

  1463   fixes S :: "'a::heine_borel set"

  1464   shows "compact(closure S) \<longleftrightarrow> bounded S"

  1465 by (meson bounded_closure bounded_subset closed_closure closure_subset compact_eq_bounded_closed)

  1466

  1467 instance%important real :: heine_borel

  1468 proof%unimportant

  1469   fix f :: "nat \<Rightarrow> real"

  1470   assume f: "bounded (range f)"

  1471   obtain r :: "nat \<Rightarrow> nat" where r: "strict_mono r" "monoseq (f \<circ> r)"

  1472     unfolding comp_def by (metis seq_monosub)

  1473   then have "Bseq (f \<circ> r)"

  1474     unfolding Bseq_eq_bounded using f

  1475     by (metis BseqI' bounded_iff comp_apply rangeI)

  1476   with r show "\<exists>l r. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"

  1477     using Bseq_monoseq_convergent[of "f \<circ> r"] by (auto simp: convergent_def)

  1478 qed

  1479

  1480 lemma compact_lemma_general:

  1481   fixes f :: "nat \<Rightarrow> 'a"

  1482   fixes proj::"'a \<Rightarrow> 'b \<Rightarrow> 'c::heine_borel" (infixl "proj" 60)

  1483   fixes unproj:: "('b \<Rightarrow> 'c) \<Rightarrow> 'a"

  1484   assumes finite_basis: "finite basis"

  1485   assumes bounded_proj: "\<And>k. k \<in> basis \<Longrightarrow> bounded ((\<lambda>x. x proj k)  range f)"

  1486   assumes proj_unproj: "\<And>e k. k \<in> basis \<Longrightarrow> (unproj e) proj k = e k"

  1487   assumes unproj_proj: "\<And>x. unproj (\<lambda>k. x proj k) = x"

  1488   shows "\<forall>d\<subseteq>basis. \<exists>l::'a. \<exists> r::nat\<Rightarrow>nat.

  1489     strict_mono r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) proj i) (l proj i) < e) sequentially)"

  1490 proof safe

  1491   fix d :: "'b set"

  1492   assume d: "d \<subseteq> basis"

  1493   with finite_basis have "finite d"

  1494     by (blast intro: finite_subset)

  1495   from this d show "\<exists>l::'a. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and>

  1496     (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) proj i) (l proj i) < e) sequentially)"

  1497   proof (induct d)

  1498     case empty

  1499     then show ?case

  1500       unfolding strict_mono_def by auto

  1501   next

  1502     case (insert k d)

  1503     have k[intro]: "k \<in> basis"

  1504       using insert by auto

  1505     have s': "bounded ((\<lambda>x. x proj k)  range f)"

  1506       using k

  1507       by (rule bounded_proj)

  1508     obtain l1::"'a" and r1 where r1: "strict_mono r1"

  1509       and lr1: "\<forall>e > 0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially"

  1510       using insert(3) using insert(4) by auto

  1511     have f': "\<forall>n. f (r1 n) proj k \<in> (\<lambda>x. x proj k)  range f"

  1512       by simp

  1513     have "bounded (range (\<lambda>i. f (r1 i) proj k))"

  1514       by (metis (lifting) bounded_subset f' image_subsetI s')

  1515     then obtain l2 r2 where r2:"strict_mono r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) proj k) \<longlongrightarrow> l2) sequentially"

  1516       using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) proj k"]

  1517       by (auto simp: o_def)

  1518     define r where "r = r1 \<circ> r2"

  1519     have r:"strict_mono r"

  1520       using r1 and r2 unfolding r_def o_def strict_mono_def by auto

  1521     moreover

  1522     define l where "l = unproj (\<lambda>i. if i = k then l2 else l1 proj i)"

  1523     {

  1524       fix e::real

  1525       assume "e > 0"

  1526       from lr1 \<open>e > 0\<close> have N1: "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially"

  1527         by blast

  1528       from lr2 \<open>e > 0\<close> have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) proj k) l2 < e) sequentially"

  1529         by (rule tendstoD)

  1530       from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) proj i) (l1 proj i) < e) sequentially"

  1531         by (rule eventually_subseq)

  1532       have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) proj i) (l proj i) < e) sequentially"

  1533         using N1' N2

  1534         by eventually_elim (insert insert.prems, auto simp: l_def r_def o_def proj_unproj)

  1535     }

  1536     ultimately show ?case by auto

  1537   qed

  1538 qed

  1539

  1540 lemma bounded_fst: "bounded s \<Longrightarrow> bounded (fst  s)"

  1541   unfolding bounded_def

  1542   by (metis (erased, hide_lams) dist_fst_le image_iff order_trans)

  1543

  1544 lemma bounded_snd: "bounded s \<Longrightarrow> bounded (snd  s)"

  1545   unfolding bounded_def

  1546   by (metis (no_types, hide_lams) dist_snd_le image_iff order.trans)

  1547

  1548 instance%important prod :: (heine_borel, heine_borel) heine_borel

  1549 proof%unimportant

  1550   fix f :: "nat \<Rightarrow> 'a \<times> 'b"

  1551   assume f: "bounded (range f)"

  1552   then have "bounded (fst  range f)"

  1553     by (rule bounded_fst)

  1554   then have s1: "bounded (range (fst \<circ> f))"

  1555     by (simp add: image_comp)

  1556   obtain l1 r1 where r1: "strict_mono r1" and l1: "(\<lambda>n. fst (f (r1 n))) \<longlonglongrightarrow> l1"

  1557     using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast

  1558   from f have s2: "bounded (range (snd \<circ> f \<circ> r1))"

  1559     by (auto simp: image_comp intro: bounded_snd bounded_subset)

  1560   obtain l2 r2 where r2: "strict_mono r2" and l2: "((\<lambda>n. snd (f (r1 (r2 n)))) \<longlongrightarrow> l2) sequentially"

  1561     using bounded_imp_convergent_subsequence [OF s2]

  1562     unfolding o_def by fast

  1563   have l1': "((\<lambda>n. fst (f (r1 (r2 n)))) \<longlongrightarrow> l1) sequentially"

  1564     using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def .

  1565   have l: "((f \<circ> (r1 \<circ> r2)) \<longlongrightarrow> (l1, l2)) sequentially"

  1566     using tendsto_Pair [OF l1' l2] unfolding o_def by simp

  1567   have r: "strict_mono (r1 \<circ> r2)"

  1568     using r1 r2 unfolding strict_mono_def by simp

  1569   show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"

  1570     using l r by fast

  1571 qed

  1572

  1573

  1574 subsection \<open>Completeness\<close>

  1575

  1576 proposition (in metric_space) completeI:

  1577   assumes "\<And>f. \<forall>n. f n \<in> s \<Longrightarrow> Cauchy f \<Longrightarrow> \<exists>l\<in>s. f \<longlonglongrightarrow> l"

  1578   shows "complete s"

  1579   using assms unfolding complete_def by fast

  1580

  1581 proposition (in metric_space) completeE:

  1582   assumes "complete s" and "\<forall>n. f n \<in> s" and "Cauchy f"

  1583   obtains l where "l \<in> s" and "f \<longlonglongrightarrow> l"

  1584   using assms unfolding complete_def by fast

  1585

  1586 (* TODO: generalize to uniform spaces *)

  1587 lemma compact_imp_complete:

  1588   fixes s :: "'a::metric_space set"

  1589   assumes "compact s"

  1590   shows "complete s"

  1591 proof -

  1592   {

  1593     fix f

  1594     assume as: "(\<forall>n::nat. f n \<in> s)" "Cauchy f"

  1595     from as(1) obtain l r where lr: "l\<in>s" "strict_mono r" "(f \<circ> r) \<longlonglongrightarrow> l"

  1596       using assms unfolding compact_def by blast

  1597

  1598     note lr' = seq_suble [OF lr(2)]

  1599     {

  1600       fix e :: real

  1601       assume "e > 0"

  1602       from as(2) obtain N where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (f m) (f n) < e/2"

  1603         unfolding cauchy_def

  1604         using \<open>e > 0\<close>

  1605         apply (erule_tac x="e/2" in allE, auto)

  1606         done

  1607       from lr(3)[unfolded lim_sequentially, THEN spec[where x="e/2"]]

  1608       obtain M where M:"\<forall>n\<ge>M. dist ((f \<circ> r) n) l < e/2"

  1609         using \<open>e > 0\<close> by auto

  1610       {

  1611         fix n :: nat

  1612         assume n: "n \<ge> max N M"

  1613         have "dist ((f \<circ> r) n) l < e/2"

  1614           using n M by auto

  1615         moreover have "r n \<ge> N"

  1616           using lr'[of n] n by auto

  1617         then have "dist (f n) ((f \<circ> r) n) < e / 2"

  1618           using N and n by auto

  1619         ultimately have "dist (f n) l < e"

  1620           using dist_triangle_half_r[of "f (r n)" "f n" e l]

  1621           by (auto simp: dist_commute)

  1622       }

  1623       then have "\<exists>N. \<forall>n\<ge>N. dist (f n) l < e" by blast

  1624     }

  1625     then have "\<exists>l\<in>s. (f \<longlongrightarrow> l) sequentially" using \<open>l\<in>s\<close>

  1626       unfolding lim_sequentially by auto

  1627   }

  1628   then show ?thesis unfolding complete_def by auto

  1629 qed

  1630

  1631 proposition compact_eq_totally_bounded:

  1632   "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>x\<in>k. ball x e))"

  1633     (is "_ \<longleftrightarrow> ?rhs")

  1634 proof

  1635   assume assms: "?rhs"

  1636   then obtain k where k: "\<And>e. 0 < e \<Longrightarrow> finite (k e)" "\<And>e. 0 < e \<Longrightarrow> s \<subseteq> (\<Union>x\<in>k e. ball x e)"

  1637     by (auto simp: choice_iff')

  1638

  1639   show "compact s"

  1640   proof cases

  1641     assume "s = {}"

  1642     then show "compact s" by (simp add: compact_def)

  1643   next

  1644     assume "s \<noteq> {}"

  1645     show ?thesis

  1646       unfolding compact_def

  1647     proof safe

  1648       fix f :: "nat \<Rightarrow> 'a"

  1649       assume f: "\<forall>n. f n \<in> s"

  1650

  1651       define e where "e n = 1 / (2 * Suc n)" for n

  1652       then have [simp]: "\<And>n. 0 < e n" by auto

  1653       define B where "B n U = (SOME b. infinite {n. f n \<in> b} \<and> (\<exists>x. b \<subseteq> ball x (e n) \<inter> U))" for n U

  1654       {

  1655         fix n U

  1656         assume "infinite {n. f n \<in> U}"

  1657         then have "\<exists>b\<in>k (e n). infinite {i\<in>{n. f n \<in> U}. f i \<in> ball b (e n)}"

  1658           using k f by (intro pigeonhole_infinite_rel) (auto simp: subset_eq)

  1659         then obtain a where

  1660           "a \<in> k (e n)"

  1661           "infinite {i \<in> {n. f n \<in> U}. f i \<in> ball a (e n)}" ..

  1662         then have "\<exists>b. infinite {i. f i \<in> b} \<and> (\<exists>x. b \<subseteq> ball x (e n) \<inter> U)"

  1663           by (intro exI[of _ "ball a (e n) \<inter> U"] exI[of _ a]) (auto simp: ac_simps)

  1664         from someI_ex[OF this]

  1665         have "infinite {i. f i \<in> B n U}" "\<exists>x. B n U \<subseteq> ball x (e n) \<inter> U"

  1666           unfolding B_def by auto

  1667       }

  1668       note B = this

  1669

  1670       define F where "F = rec_nat (B 0 UNIV) B"

  1671       {

  1672         fix n

  1673         have "infinite {i. f i \<in> F n}"

  1674           by (induct n) (auto simp: F_def B)

  1675       }

  1676       then have F: "\<And>n. \<exists>x. F (Suc n) \<subseteq> ball x (e n) \<inter> F n"

  1677         using B by (simp add: F_def)

  1678       then have F_dec: "\<And>m n. m \<le> n \<Longrightarrow> F n \<subseteq> F m"

  1679         using decseq_SucI[of F] by (auto simp: decseq_def)

  1680

  1681       obtain sel where sel: "\<And>k i. i < sel k i" "\<And>k i. f (sel k i) \<in> F k"

  1682       proof (atomize_elim, unfold all_conj_distrib[symmetric], intro choice allI)

  1683         fix k i

  1684         have "infinite ({n. f n \<in> F k} - {.. i})"

  1685           using \<open>infinite {n. f n \<in> F k}\<close> by auto

  1686         from infinite_imp_nonempty[OF this]

  1687         show "\<exists>x>i. f x \<in> F k"

  1688           by (simp add: set_eq_iff not_le conj_commute)

  1689       qed

  1690

  1691       define t where "t = rec_nat (sel 0 0) (\<lambda>n i. sel (Suc n) i)"

  1692       have "strict_mono t"

  1693         unfolding strict_mono_Suc_iff by (simp add: t_def sel)

  1694       moreover have "\<forall>i. (f \<circ> t) i \<in> s"

  1695         using f by auto

  1696       moreover

  1697       {

  1698         fix n

  1699         have "(f \<circ> t) n \<in> F n"

  1700           by (cases n) (simp_all add: t_def sel)

  1701       }

  1702       note t = this

  1703

  1704       have "Cauchy (f \<circ> t)"

  1705       proof (safe intro!: metric_CauchyI exI elim!: nat_approx_posE)

  1706         fix r :: real and N n m

  1707         assume "1 / Suc N < r" "Suc N \<le> n" "Suc N \<le> m"

  1708         then have "(f \<circ> t) n \<in> F (Suc N)" "(f \<circ> t) m \<in> F (Suc N)" "2 * e N < r"

  1709           using F_dec t by (auto simp: e_def field_simps of_nat_Suc)

  1710         with F[of N] obtain x where "dist x ((f \<circ> t) n) < e N" "dist x ((f \<circ> t) m) < e N"

  1711           by (auto simp: subset_eq)

  1712         with dist_triangle[of "(f \<circ> t) m" "(f \<circ> t) n" x] \<open>2 * e N < r\<close>

  1713         show "dist ((f \<circ> t) m) ((f \<circ> t) n) < r"

  1714           by (simp add: dist_commute)

  1715       qed

  1716

  1717       ultimately show "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"

  1718         using assms unfolding complete_def by blast

  1719     qed

  1720   qed

  1721 qed (metis compact_imp_complete compact_imp_seq_compact seq_compact_imp_totally_bounded)

  1722

  1723 lemma cauchy_imp_bounded:

  1724   assumes "Cauchy s"

  1725   shows "bounded (range s)"

  1726 proof -

  1727   from assms obtain N :: nat where "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < 1"

  1728     unfolding cauchy_def by force

  1729   then have N:"\<forall>n. N \<le> n \<longrightarrow> dist (s N) (s n) < 1" by auto

  1730   moreover

  1731   have "bounded (s  {0..N})"

  1732     using finite_imp_bounded[of "s  {1..N}"] by auto

  1733   then obtain a where a:"\<forall>x\<in>s  {0..N}. dist (s N) x \<le> a"

  1734     unfolding bounded_any_center [where a="s N"] by auto

  1735   ultimately show "?thesis"

  1736     unfolding bounded_any_center [where a="s N"]

  1737     apply (rule_tac x="max a 1" in exI, auto)

  1738     apply (erule_tac x=y in allE)

  1739     apply (erule_tac x=y in ballE, auto)

  1740     done

  1741 qed

  1742

  1743 instance heine_borel < complete_space

  1744 proof

  1745   fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"

  1746   then have "bounded (range f)"

  1747     by (rule cauchy_imp_bounded)

  1748   then have "compact (closure (range f))"

  1749     unfolding compact_eq_bounded_closed by auto

  1750   then have "complete (closure (range f))"

  1751     by (rule compact_imp_complete)

  1752   moreover have "\<forall>n. f n \<in> closure (range f)"

  1753     using closure_subset [of "range f"] by auto

  1754   ultimately have "\<exists>l\<in>closure (range f). (f \<longlongrightarrow> l) sequentially"

  1755     using \<open>Cauchy f\<close> unfolding complete_def by auto

  1756   then show "convergent f"

  1757     unfolding convergent_def by auto

  1758 qed

  1759

  1760 lemma complete_UNIV: "complete (UNIV :: ('a::complete_space) set)"

  1761 proof (rule completeI)

  1762   fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"

  1763   then have "convergent f" by (rule Cauchy_convergent)

  1764   then show "\<exists>l\<in>UNIV. f \<longlonglongrightarrow> l" unfolding convergent_def by simp

  1765 qed

  1766

  1767 lemma complete_imp_closed:

  1768   fixes S :: "'a::metric_space set"

  1769   assumes "complete S"

  1770   shows "closed S"

  1771 proof (unfold closed_sequential_limits, clarify)

  1772   fix f x assume "\<forall>n. f n \<in> S" and "f \<longlonglongrightarrow> x"

  1773   from \<open>f \<longlonglongrightarrow> x\<close> have "Cauchy f"

  1774     by (rule LIMSEQ_imp_Cauchy)

  1775   with \<open>complete S\<close> and \<open>\<forall>n. f n \<in> S\<close> obtain l where "l \<in> S" and "f \<longlonglongrightarrow> l"

  1776     by (rule completeE)

  1777   from \<open>f \<longlonglongrightarrow> x\<close> and \<open>f \<longlonglongrightarrow> l\<close> have "x = l"

  1778     by (rule LIMSEQ_unique)

  1779   with \<open>l \<in> S\<close> show "x \<in> S"

  1780     by simp

  1781 qed

  1782

  1783 lemma complete_Int_closed:

  1784   fixes S :: "'a::metric_space set"

  1785   assumes "complete S" and "closed t"

  1786   shows "complete (S \<inter> t)"

  1787 proof (rule completeI)

  1788   fix f assume "\<forall>n. f n \<in> S \<inter> t" and "Cauchy f"

  1789   then have "\<forall>n. f n \<in> S" and "\<forall>n. f n \<in> t"

  1790     by simp_all

  1791   from \<open>complete S\<close> obtain l where "l \<in> S" and "f \<longlonglongrightarrow> l"

  1792     using \<open>\<forall>n. f n \<in> S\<close> and \<open>Cauchy f\<close> by (rule completeE)

  1793   from \<open>closed t\<close> and \<open>\<forall>n. f n \<in> t\<close> and \<open>f \<longlonglongrightarrow> l\<close> have "l \<in> t"

  1794     by (rule closed_sequentially)

  1795   with \<open>l \<in> S\<close> and \<open>f \<longlonglongrightarrow> l\<close> show "\<exists>l\<in>S \<inter> t. f \<longlonglongrightarrow> l"

  1796     by fast

  1797 qed

  1798

  1799 lemma complete_closed_subset:

  1800   fixes S :: "'a::metric_space set"

  1801   assumes "closed S" and "S \<subseteq> t" and "complete t"

  1802   shows "complete S"

  1803   using assms complete_Int_closed [of t S] by (simp add: Int_absorb1)

  1804

  1805 lemma complete_eq_closed:

  1806   fixes S :: "('a::complete_space) set"

  1807   shows "complete S \<longleftrightarrow> closed S"

  1808 proof

  1809   assume "closed S" then show "complete S"

  1810     using subset_UNIV complete_UNIV by (rule complete_closed_subset)

  1811 next

  1812   assume "complete S" then show "closed S"

  1813     by (rule complete_imp_closed)

  1814 qed

  1815

  1816 lemma convergent_eq_Cauchy:

  1817   fixes S :: "nat \<Rightarrow> 'a::complete_space"

  1818   shows "(\<exists>l. (S \<longlongrightarrow> l) sequentially) \<longleftrightarrow> Cauchy S"

  1819   unfolding Cauchy_convergent_iff convergent_def ..

  1820

  1821 lemma convergent_imp_bounded:

  1822   fixes S :: "nat \<Rightarrow> 'a::metric_space"

  1823   shows "(S \<longlongrightarrow> l) sequentially \<Longrightarrow> bounded (range S)"

  1824   by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy)

  1825

  1826 lemma frontier_subset_compact:

  1827   fixes S :: "'a::heine_borel set"

  1828   shows "compact S \<Longrightarrow> frontier S \<subseteq> S"

  1829   using frontier_subset_closed compact_eq_bounded_closed

  1830   by blast

  1831

  1832 lemma continuous_closed_imp_Cauchy_continuous:

  1833   fixes S :: "('a::complete_space) set"

  1834   shows "\<lbrakk>continuous_on S f; closed S; Cauchy \<sigma>; \<And>n. (\<sigma> n) \<in> S\<rbrakk> \<Longrightarrow> Cauchy(f \<circ> \<sigma>)"

  1835   apply (simp add: complete_eq_closed [symmetric] continuous_on_sequentially)

  1836   by (meson LIMSEQ_imp_Cauchy complete_def)

  1837

  1838 lemma banach_fix_type:

  1839   fixes f::"'a::complete_space\<Rightarrow>'a"

  1840   assumes c:"0 \<le> c" "c < 1"

  1841       and lipschitz:"\<forall>x. \<forall>y. dist (f x) (f y) \<le> c * dist x y"

  1842   shows "\<exists>!x. (f x = x)"

  1843   using assms banach_fix[OF complete_UNIV UNIV_not_empty assms(1,2) subset_UNIV, of f]

  1844   by auto

  1845

  1846

  1847 subsection%unimportant\<open> Finite intersection property\<close>

  1848

  1849 text\<open>Also developed in HOL's toplogical spaces theory, but the Heine-Borel type class isn't available there.\<close>

  1850

  1851 lemma closed_imp_fip:

  1852   fixes S :: "'a::heine_borel set"

  1853   assumes "closed S"

  1854       and T: "T \<in> \<F>" "bounded T"

  1855       and clof: "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"

  1856       and none: "\<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> S \<inter> \<Inter>\<F>' \<noteq> {}"

  1857     shows "S \<inter> \<Inter>\<F> \<noteq> {}"

  1858 proof -

  1859   have "compact (S \<inter> T)"

  1860     using \<open>closed S\<close> clof compact_eq_bounded_closed T by blast

  1861   then have "(S \<inter> T) \<inter> \<Inter>\<F> \<noteq> {}"

  1862     apply (rule compact_imp_fip)

  1863      apply (simp add: clof)

  1864     by (metis Int_assoc complete_lattice_class.Inf_insert finite_insert insert_subset none \<open>T \<in> \<F>\<close>)

  1865   then show ?thesis by blast

  1866 qed

  1867

  1868 lemma closed_imp_fip_compact:

  1869   fixes S :: "'a::heine_borel set"

  1870   shows

  1871    "\<lbrakk>closed S; \<And>T. T \<in> \<F> \<Longrightarrow> compact T;

  1872      \<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> S \<inter> \<Inter>\<F>' \<noteq> {}\<rbrakk>

  1873         \<Longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}"

  1874 by (metis Inf_greatest closed_imp_fip compact_eq_bounded_closed empty_subsetI finite.emptyI inf.orderE)

  1875

  1876 lemma closed_fip_Heine_Borel:

  1877   fixes \<F> :: "'a::heine_borel set set"

  1878   assumes "closed S" "T \<in> \<F>" "bounded T"

  1879       and "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"

  1880       and "\<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> \<Inter>\<F>' \<noteq> {}"

  1881     shows "\<Inter>\<F> \<noteq> {}"

  1882 proof -

  1883   have "UNIV \<inter> \<Inter>\<F> \<noteq> {}"

  1884     using assms closed_imp_fip [OF closed_UNIV] by auto

  1885   then show ?thesis by simp

  1886 qed

  1887

  1888 lemma compact_fip_Heine_Borel:

  1889   fixes \<F> :: "'a::heine_borel set set"

  1890   assumes clof: "\<And>T. T \<in> \<F> \<Longrightarrow> compact T"

  1891       and none: "\<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> \<Inter>\<F>' \<noteq> {}"

  1892     shows "\<Inter>\<F> \<noteq> {}"

  1893 by (metis InterI all_not_in_conv clof closed_fip_Heine_Borel compact_eq_bounded_closed none)

  1894

  1895 lemma compact_sequence_with_limit:

  1896   fixes f :: "nat \<Rightarrow> 'a::heine_borel"

  1897   shows "(f \<longlongrightarrow> l) sequentially \<Longrightarrow> compact (insert l (range f))"

  1898 apply (simp add: compact_eq_bounded_closed, auto)

  1899 apply (simp add: convergent_imp_bounded)

  1900 by (simp add: closed_limpt islimpt_insert sequence_unique_limpt)

  1901

  1902

  1903 subsection \<open>Properties of Balls and Spheres\<close>

  1904

  1905 lemma compact_cball[simp]:

  1906   fixes x :: "'a::heine_borel"

  1907   shows "compact (cball x e)"

  1908   using compact_eq_bounded_closed bounded_cball closed_cball

  1909   by blast

  1910

  1911 lemma compact_frontier_bounded[intro]:

  1912   fixes S :: "'a::heine_borel set"

  1913   shows "bounded S \<Longrightarrow> compact (frontier S)"

  1914   unfolding frontier_def

  1915   using compact_eq_bounded_closed

  1916   by blast

  1917

  1918 lemma compact_frontier[intro]:

  1919   fixes S :: "'a::heine_borel set"

  1920   shows "compact S \<Longrightarrow> compact (frontier S)"

  1921   using compact_eq_bounded_closed compact_frontier_bounded

  1922   by blast

  1923

  1924

  1925 subsection \<open>Distance from a Set\<close>

  1926

  1927 lemma distance_attains_sup:

  1928   assumes "compact s" "s \<noteq> {}"

  1929   shows "\<exists>x\<in>s. \<forall>y\<in>s. dist a y \<le> dist a x"

  1930 proof (rule continuous_attains_sup [OF assms])

  1931   {

  1932     fix x

  1933     assume "x\<in>s"

  1934     have "(dist a \<longlongrightarrow> dist a x) (at x within s)"

  1935       by (intro tendsto_dist tendsto_const tendsto_ident_at)

  1936   }

  1937   then show "continuous_on s (dist a)"

  1938     unfolding continuous_on ..

  1939 qed

  1940

  1941 text \<open>For \emph{minimal} distance, we only need closure, not compactness.\<close>

  1942

  1943 lemma distance_attains_inf:

  1944   fixes a :: "'a::heine_borel"

  1945   assumes "closed s" and "s \<noteq> {}"

  1946   obtains x where "x\<in>s" "\<And>y. y \<in> s \<Longrightarrow> dist a x \<le> dist a y"

  1947 proof -

  1948   from assms obtain b where "b \<in> s" by auto

  1949   let ?B = "s \<inter> cball a (dist b a)"

  1950   have "?B \<noteq> {}" using \<open>b \<in> s\<close>

  1951     by (auto simp: dist_commute)

  1952   moreover have "continuous_on ?B (dist a)"

  1953     by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)

  1954   moreover have "compact ?B"

  1955     by (intro closed_Int_compact \<open>closed s\<close> compact_cball)

  1956   ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y"

  1957     by (metis continuous_attains_inf)

  1958   with that show ?thesis by fastforce

  1959 qed

  1960

  1961

  1962 subsection \<open>Infimum Distance\<close>

  1963

  1964 definition%important "infdist x A = (if A = {} then 0 else INF a\<in>A. dist x a)"

  1965

  1966 lemma bdd_below_image_dist[intro, simp]: "bdd_below (dist x  A)"

  1967   by (auto intro!: zero_le_dist)

  1968

  1969 lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = (INF a\<in>A. dist x a)"

  1970   by (simp add: infdist_def)

  1971

  1972 lemma infdist_nonneg: "0 \<le> infdist x A"

  1973   by (auto simp: infdist_def intro: cINF_greatest)

  1974

  1975 lemma infdist_le: "a \<in> A \<Longrightarrow> infdist x A \<le> dist x a"

  1976   by (auto intro: cINF_lower simp add: infdist_def)

  1977

  1978 lemma infdist_le2: "a \<in> A \<Longrightarrow> dist x a \<le> d \<Longrightarrow> infdist x A \<le> d"

  1979   by (auto intro!: cINF_lower2 simp add: infdist_def)

  1980

  1981 lemma infdist_zero[simp]: "a \<in> A \<Longrightarrow> infdist a A = 0"

  1982   by (auto intro!: antisym infdist_nonneg infdist_le2)

  1983

  1984 lemma infdist_triangle: "infdist x A \<le> infdist y A + dist x y"

  1985 proof (cases "A = {}")

  1986   case True

  1987   then show ?thesis by (simp add: infdist_def)

  1988 next

  1989   case False

  1990   then obtain a where "a \<in> A" by auto

  1991   have "infdist x A \<le> Inf {dist x y + dist y a |a. a \<in> A}"

  1992   proof (rule cInf_greatest)

  1993     from \<open>A \<noteq> {}\<close> show "{dist x y + dist y a |a. a \<in> A} \<noteq> {}"

  1994       by simp

  1995     fix d

  1996     assume "d \<in> {dist x y + dist y a |a. a \<in> A}"

  1997     then obtain a where d: "d = dist x y + dist y a" "a \<in> A"

  1998       by auto

  1999     show "infdist x A \<le> d"

  2000       unfolding infdist_notempty[OF \<open>A \<noteq> {}\<close>]

  2001     proof (rule cINF_lower2)

  2002       show "a \<in> A" by fact

  2003       show "dist x a \<le> d"

  2004         unfolding d by (rule dist_triangle)

  2005     qed simp

  2006   qed

  2007   also have "\<dots> = dist x y + infdist y A"

  2008   proof (rule cInf_eq, safe)

  2009     fix a

  2010     assume "a \<in> A"

  2011     then show "dist x y + infdist y A \<le> dist x y + dist y a"

  2012       by (auto intro: infdist_le)

  2013   next

  2014     fix i

  2015     assume inf: "\<And>d. d \<in> {dist x y + dist y a |a. a \<in> A} \<Longrightarrow> i \<le> d"

  2016     then have "i - dist x y \<le> infdist y A"

  2017       unfolding infdist_notempty[OF \<open>A \<noteq> {}\<close>] using \<open>a \<in> A\<close>

  2018       by (intro cINF_greatest) (auto simp: field_simps)

  2019     then show "i \<le> dist x y + infdist y A"

  2020       by simp

  2021   qed

  2022   finally show ?thesis by simp

  2023 qed

  2024

  2025 lemma in_closure_iff_infdist_zero:

  2026   assumes "A \<noteq> {}"

  2027   shows "x \<in> closure A \<longleftrightarrow> infdist x A = 0"

  2028 proof

  2029   assume "x \<in> closure A"

  2030   show "infdist x A = 0"

  2031   proof (rule ccontr)

  2032     assume "infdist x A \<noteq> 0"

  2033     with infdist_nonneg[of x A] have "infdist x A > 0"

  2034       by auto

  2035     then have "ball x (infdist x A) \<inter> closure A = {}"

  2036       apply auto

  2037       apply (metis \<open>x \<in> closure A\<close> closure_approachable dist_commute infdist_le not_less)

  2038       done

  2039     then have "x \<notin> closure A"

  2040       by (metis \<open>0 < infdist x A\<close> centre_in_ball disjoint_iff_not_equal)

  2041     then show False using \<open>x \<in> closure A\<close> by simp

  2042   qed

  2043 next

  2044   assume x: "infdist x A = 0"

  2045   then obtain a where "a \<in> A"

  2046     by atomize_elim (metis all_not_in_conv assms)

  2047   show "x \<in> closure A"

  2048     unfolding closure_approachable

  2049     apply safe

  2050   proof (rule ccontr)

  2051     fix e :: real

  2052     assume "e > 0"

  2053     assume "\<not> (\<exists>y\<in>A. dist y x < e)"

  2054     then have "infdist x A \<ge> e" using \<open>a \<in> A\<close>

  2055       unfolding infdist_def

  2056       by (force simp: dist_commute intro: cINF_greatest)

  2057     with x \<open>e > 0\<close> show False by auto

  2058   qed

  2059 qed

  2060

  2061 lemma in_closed_iff_infdist_zero:

  2062   assumes "closed A" "A \<noteq> {}"

  2063   shows "x \<in> A \<longleftrightarrow> infdist x A = 0"

  2064 proof -

  2065   have "x \<in> closure A \<longleftrightarrow> infdist x A = 0"

  2066     by (rule in_closure_iff_infdist_zero) fact

  2067   with assms show ?thesis by simp

  2068 qed

  2069

  2070 lemma infdist_pos_not_in_closed:

  2071   assumes "closed S" "S \<noteq> {}" "x \<notin> S"

  2072   shows "infdist x S > 0"

  2073 using in_closed_iff_infdist_zero[OF assms(1) assms(2), of x] assms(3) infdist_nonneg le_less by fastforce

  2074

  2075 lemma

  2076   infdist_attains_inf:

  2077   fixes X::"'a::heine_borel set"

  2078   assumes "closed X"

  2079   assumes "X \<noteq> {}"

  2080   obtains x where "x \<in> X" "infdist y X = dist y x"

  2081 proof -

  2082   have "bdd_below (dist y  X)"

  2083     by auto

  2084   from distance_attains_inf[OF assms, of y]

  2085   obtain x where INF: "x \<in> X" "\<And>z. z \<in> X \<Longrightarrow> dist y x \<le> dist y z" by auto

  2086   have "infdist y X = dist y x"

  2087     by (auto simp: infdist_def assms

  2088       intro!: antisym cINF_lower[OF _ \<open>x \<in> X\<close>] cINF_greatest[OF assms(2) INF(2)])

  2089   with \<open>x \<in> X\<close> show ?thesis ..

  2090 qed

  2091

  2092

  2093 text \<open>Every metric space is a T4 space:\<close>

  2094

  2095 instance metric_space \<subseteq> t4_space

  2096 proof

  2097   fix S T::"'a set" assume H: "closed S" "closed T" "S \<inter> T = {}"

  2098   consider "S = {}" | "T = {}" | "S \<noteq> {} \<and> T \<noteq> {}" by auto

  2099   then show "\<exists>U V. open U \<and> open V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> U \<inter> V = {}"

  2100   proof (cases)

  2101     case 1

  2102     show ?thesis

  2103       apply (rule exI[of _ "{}"], rule exI[of _ UNIV]) using 1 by auto

  2104   next

  2105     case 2

  2106     show ?thesis

  2107       apply (rule exI[of _ UNIV], rule exI[of _ "{}"]) using 2 by auto

  2108   next

  2109     case 3

  2110     define U where "U = (\<Union>x\<in>S. ball x ((infdist x T)/2))"

  2111     have A: "open U" unfolding U_def by auto

  2112     have "infdist x T > 0" if "x \<in> S" for x

  2113       using H that 3 by (auto intro!: infdist_pos_not_in_closed)

  2114     then have B: "S \<subseteq> U" unfolding U_def by auto

  2115     define V where "V = (\<Union>x\<in>T. ball x ((infdist x S)/2))"

  2116     have C: "open V" unfolding V_def by auto

  2117     have "infdist x S > 0" if "x \<in> T" for x

  2118       using H that 3 by (auto intro!: infdist_pos_not_in_closed)

  2119     then have D: "T \<subseteq> V" unfolding V_def by auto

  2120

  2121     have "(ball x ((infdist x T)/2)) \<inter> (ball y ((infdist y S)/2)) = {}" if "x \<in> S" "y \<in> T" for x y

  2122     proof (auto)

  2123       fix z assume H: "dist x z * 2 < infdist x T" "dist y z * 2 < infdist y S"

  2124       have "2 * dist x y \<le> 2 * dist x z + 2 * dist y z"

  2125         using dist_triangle[of x y z] by (auto simp add: dist_commute)

  2126       also have "... < infdist x T + infdist y S"

  2127         using H by auto

  2128       finally have "dist x y < infdist x T \<or> dist x y < infdist y S"

  2129         by auto

  2130       then show False

  2131         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)

  2132     qed

  2133     then have E: "U \<inter> V = {}"

  2134       unfolding U_def V_def by auto

  2135     show ?thesis

  2136       apply (rule exI[of _ U], rule exI[of _ V]) using A B C D E by auto

  2137   qed

  2138 qed

  2139

  2140 lemma tendsto_infdist [tendsto_intros]:

  2141   assumes f: "(f \<longlongrightarrow> l) F"

  2142   shows "((\<lambda>x. infdist (f x) A) \<longlongrightarrow> infdist l A) F"

  2143 proof (rule tendstoI)

  2144   fix e ::real

  2145   assume "e > 0"

  2146   from tendstoD[OF f this]

  2147   show "eventually (\<lambda>x. dist (infdist (f x) A) (infdist l A) < e) F"

  2148   proof (eventually_elim)

  2149     fix x

  2150     from infdist_triangle[of l A "f x"] infdist_triangle[of "f x" A l]

  2151     have "dist (infdist (f x) A) (infdist l A) \<le> dist (f x) l"

  2152       by (simp add: dist_commute dist_real_def)

  2153     also assume "dist (f x) l < e"

  2154     finally show "dist (infdist (f x) A) (infdist l A) < e" .

  2155   qed

  2156 qed

  2157

  2158 lemma continuous_infdist[continuous_intros]:

  2159   assumes "continuous F f"

  2160   shows "continuous F (\<lambda>x. infdist (f x) A)"

  2161   using assms unfolding continuous_def by (rule tendsto_infdist)

  2162

  2163 lemma compact_infdist_le:

  2164   fixes A::"'a::heine_borel set"

  2165   assumes "A \<noteq> {}"

  2166   assumes "compact A"

  2167   assumes "e > 0"

  2168   shows "compact {x. infdist x A \<le> e}"

  2169 proof -

  2170   from continuous_closed_vimage[of "{0..e}" "\<lambda>x. infdist x A"]

  2171     continuous_infdist[OF continuous_ident, of _ UNIV A]

  2172   have "closed {x. infdist x A \<le> e}" by (auto simp: vimage_def infdist_nonneg)

  2173   moreover

  2174   from assms obtain x0 b where b: "\<And>x. x \<in> A \<Longrightarrow> dist x0 x \<le> b" "closed A"

  2175     by (auto simp: compact_eq_bounded_closed bounded_def)

  2176   {

  2177     fix y

  2178     assume le: "infdist y A \<le> e"

  2179     from infdist_attains_inf[OF \<open>closed A\<close> \<open>A \<noteq> {}\<close>, of y]

  2180     obtain z where z: "z \<in> A" "infdist y A = dist y z" by blast

  2181     have "dist x0 y \<le> dist y z + dist x0 z"

  2182       by (metis dist_commute dist_triangle)

  2183     also have "dist y z \<le> e" using le z by simp

  2184     also have "dist x0 z \<le> b" using b z by simp

  2185     finally have "dist x0 y \<le> b + e" by arith

  2186   } then

  2187   have "bounded {x. infdist x A \<le> e}"

  2188     by (auto simp: bounded_any_center[where a=x0] intro!: exI[where x="b + e"])

  2189   ultimately show "compact {x. infdist x A \<le> e}"

  2190     by (simp add: compact_eq_bounded_closed)

  2191 qed

  2192

  2193

  2194 subsection \<open>Separation between Points and Sets\<close>

  2195

  2196 proposition separate_point_closed:

  2197   fixes s :: "'a::heine_borel set"

  2198   assumes "closed s" and "a \<notin> s"

  2199   shows "\<exists>d>0. \<forall>x\<in>s. d \<le> dist a x"

  2200 proof (cases "s = {}")

  2201   case True

  2202   then show ?thesis by(auto intro!: exI[where x=1])

  2203 next

  2204   case False

  2205   from assms obtain x where "x\<in>s" "\<forall>y\<in>s. dist a x \<le> dist a y"

  2206     using \<open>s \<noteq> {}\<close> by (blast intro: distance_attains_inf [of s a])

  2207   with \<open>x\<in>s\<close> show ?thesis using dist_pos_lt[of a x] and\<open>a \<notin> s\<close>

  2208     by blast

  2209 qed

  2210

  2211 proposition separate_compact_closed:

  2212   fixes s t :: "'a::heine_borel set"

  2213   assumes "compact s"

  2214     and t: "closed t" "s \<inter> t = {}"

  2215   shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"

  2216 proof cases

  2217   assume "s \<noteq> {} \<and> t \<noteq> {}"

  2218   then have "s \<noteq> {}" "t \<noteq> {}" by auto

  2219   let ?inf = "\<lambda>x. infdist x t"

  2220   have "continuous_on s ?inf"

  2221     by (auto intro!: continuous_at_imp_continuous_on continuous_infdist continuous_ident)

  2222   then obtain x where x: "x \<in> s" "\<forall>y\<in>s. ?inf x \<le> ?inf y"

  2223     using continuous_attains_inf[OF \<open>compact s\<close> \<open>s \<noteq> {}\<close>] by auto

  2224   then have "0 < ?inf x"

  2225     using t \<open>t \<noteq> {}\<close> in_closed_iff_infdist_zero by (auto simp: less_le infdist_nonneg)

  2226   moreover have "\<forall>x'\<in>s. \<forall>y\<in>t. ?inf x \<le> dist x' y"

  2227     using x by (auto intro: order_trans infdist_le)

  2228   ultimately show ?thesis by auto

  2229 qed (auto intro!: exI[of _ 1])

  2230

  2231 proposition separate_closed_compact:

  2232   fixes s t :: "'a::heine_borel set"

  2233   assumes "closed s"

  2234     and "compact t"

  2235     and "s \<inter> t = {}"

  2236   shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"

  2237 proof -

  2238   have *: "t \<inter> s = {}"

  2239     using assms(3) by auto

  2240   show ?thesis

  2241     using separate_compact_closed[OF assms(2,1) *] by (force simp: dist_commute)

  2242 qed

  2243

  2244 proposition compact_in_open_separated:

  2245   fixes A::"'a::heine_borel set"

  2246   assumes "A \<noteq> {}"

  2247   assumes "compact A"

  2248   assumes "open B"

  2249   assumes "A \<subseteq> B"

  2250   obtains e where "e > 0" "{x. infdist x A \<le> e} \<subseteq> B"

  2251 proof atomize_elim

  2252   have "closed (- B)" "compact A" "- B \<inter> A = {}"

  2253     using assms by (auto simp: open_Diff compact_eq_bounded_closed)

  2254   from separate_closed_compact[OF this]

  2255   obtain d'::real where d': "d'>0" "\<And>x y. x \<notin> B \<Longrightarrow> y \<in> A \<Longrightarrow> d' \<le> dist x y"

  2256     by auto

  2257   define d where "d = d' / 2"

  2258   hence "d>0" "d < d'" using d' by auto

  2259   with d' have d: "\<And>x y. x \<notin> B \<Longrightarrow> y \<in> A \<Longrightarrow> d < dist x y"

  2260     by force

  2261   show "\<exists>e>0. {x. infdist x A \<le> e} \<subseteq> B"

  2262   proof (rule ccontr)

  2263     assume "\<nexists>e. 0 < e \<and> {x. infdist x A \<le> e} \<subseteq> B"

  2264     with \<open>d > 0\<close> obtain x where x: "infdist x A \<le> d" "x \<notin> B"

  2265       by auto

  2266     from assms have "closed A" "A \<noteq> {}" by (auto simp: compact_eq_bounded_closed)

  2267     from infdist_attains_inf[OF this]

  2268     obtain y where y: "y \<in> A" "infdist x A = dist x y"

  2269       by auto

  2270     have "dist x y \<le> d" using x y by simp

  2271     also have "\<dots> < dist x y" using y d x by auto

  2272     finally show False by simp

  2273   qed

  2274 qed

  2275

  2276

  2277 subsection \<open>Uniform Continuity\<close>

  2278

  2279 lemma uniformly_continuous_onE:

  2280   assumes "uniformly_continuous_on s f" "0 < e"

  2281   obtains d where "d>0" "\<And>x x'. \<lbrakk>x\<in>s; x'\<in>s; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"

  2282 using assms

  2283 by (auto simp: uniformly_continuous_on_def)

  2284

  2285 lemma uniformly_continuous_on_sequentially:

  2286   "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>

  2287     (\<lambda>n. dist (x n) (y n)) \<longlonglongrightarrow> 0 \<longrightarrow> (\<lambda>n. dist (f(x n)) (f(y n))) \<longlonglongrightarrow> 0)" (is "?lhs = ?rhs")

  2288 proof

  2289   assume ?lhs

  2290   {

  2291     fix x y

  2292     assume x: "\<forall>n. x n \<in> s"

  2293       and y: "\<forall>n. y n \<in> s"

  2294       and xy: "((\<lambda>n. dist (x n) (y n)) \<longlongrightarrow> 0) sequentially"

  2295     {

  2296       fix e :: real

  2297       assume "e > 0"

  2298       then obtain d where "d > 0" and d: "\<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"

  2299         using \<open>?lhs\<close>[unfolded uniformly_continuous_on_def, THEN spec[where x=e]] by auto

  2300       obtain N where N: "\<forall>n\<ge>N. dist (x n) (y n) < d"

  2301         using xy[unfolded lim_sequentially dist_norm] and \<open>d>0\<close> by auto

  2302       {

  2303         fix n

  2304         assume "n\<ge>N"

  2305         then have "dist (f (x n)) (f (y n)) < e"

  2306           using N[THEN spec[where x=n]]

  2307           using d[THEN bspec[where x="x n"], THEN bspec[where x="y n"]]

  2308           using x and y

  2309           by (simp add: dist_commute)

  2310       }

  2311       then have "\<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e"

  2312         by auto

  2313     }

  2314     then have "((\<lambda>n. dist (f(x n)) (f(y n))) \<longlongrightarrow> 0) sequentially"

  2315       unfolding lim_sequentially and dist_real_def by auto

  2316   }

  2317   then show ?rhs by auto

  2318 next

  2319   assume ?rhs

  2320   {

  2321     assume "\<not> ?lhs"

  2322     then obtain e where "e > 0" "\<forall>d>0. \<exists>x\<in>s. \<exists>x'\<in>s. dist x' x < d \<and> \<not> dist (f x') (f x) < e"

  2323       unfolding uniformly_continuous_on_def by auto

  2324     then obtain fa where fa:

  2325       "\<forall>x. 0 < x \<longrightarrow> fst (fa x) \<in> s \<and> snd (fa x) \<in> s \<and> dist (fst (fa x)) (snd (fa x)) < x \<and> \<not> dist (f (fst (fa x))) (f (snd (fa x))) < e"

  2326       using choice[of "\<lambda>d x. d>0 \<longrightarrow> fst x \<in> s \<and> snd x \<in> s \<and> dist (snd x) (fst x) < d \<and> \<not> dist (f (snd x)) (f (fst x)) < e"]

  2327       unfolding Bex_def

  2328       by (auto simp: dist_commute)

  2329     define x where "x n = fst (fa (inverse (real n + 1)))" for n

  2330     define y where "y n = snd (fa (inverse (real n + 1)))" for n

  2331     have xyn: "\<forall>n. x n \<in> s \<and> y n \<in> s"

  2332       and xy0: "\<forall>n. dist (x n) (y n) < inverse (real n + 1)"

  2333       and fxy:"\<forall>n. \<not> dist (f (x n)) (f (y n)) < e"

  2334       unfolding x_def and y_def using fa

  2335       by auto

  2336     {

  2337       fix e :: real

  2338       assume "e > 0"

  2339       then obtain N :: nat where "N \<noteq> 0" and N: "0 < inverse (real N) \<and> inverse (real N) < e"

  2340         unfolding real_arch_inverse[of e] by auto

  2341       {

  2342         fix n :: nat

  2343         assume "n \<ge> N"

  2344         then have "inverse (real n + 1) < inverse (real N)"

  2345           using of_nat_0_le_iff and \<open>N\<noteq>0\<close> by auto

  2346         also have "\<dots> < e" using N by auto

  2347         finally have "inverse (real n + 1) < e" by auto

  2348         then have "dist (x n) (y n) < e"

  2349           using xy0[THEN spec[where x=n]] by auto

  2350       }

  2351       then have "\<exists>N. \<forall>n\<ge>N. dist (x n) (y n) < e" by auto

  2352     }

  2353     then have "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e"

  2354       using \<open>?rhs\<close>[THEN spec[where x=x], THEN spec[where x=y]] and xyn

  2355       unfolding lim_sequentially dist_real_def by auto

  2356     then have False using fxy and \<open>e>0\<close> by auto

  2357   }

  2358   then show ?lhs

  2359     unfolding uniformly_continuous_on_def by blast

  2360 qed

  2361

  2362

  2363 subsection \<open>Continuity on a Compact Domain Implies Uniform Continuity\<close>

  2364

  2365 text\<open>From the proof of the Heine-Borel theorem: Lemma 2 in section 3.7, page 69 of

  2366 J. C. Burkill and H. Burkill. A Second Course in Mathematical Analysis (CUP, 2002)\<close>

  2367

  2368 lemma Heine_Borel_lemma:

  2369   assumes "compact S" and Ssub: "S \<subseteq> \<Union>\<G>" and opn: "\<And>G. G \<in> \<G> \<Longrightarrow> open G"

  2370   obtains e where "0 < e" "\<And>x. x \<in> S \<Longrightarrow> \<exists>G \<in> \<G>. ball x e \<subseteq> G"

  2371 proof -

  2372   have False if neg: "\<And>e. 0 < e \<Longrightarrow> \<exists>x \<in> S. \<forall>G \<in> \<G>. \<not> ball x e \<subseteq> G"

  2373   proof -

  2374     have "\<exists>x \<in> S. \<forall>G \<in> \<G>. \<not> ball x (1 / Suc n) \<subseteq> G" for n

  2375       using neg by simp

  2376     then obtain f where "\<And>n. f n \<in> S" and fG: "\<And>G n. G \<in> \<G> \<Longrightarrow> \<not> ball (f n) (1 / Suc n) \<subseteq> G"

  2377       by metis

  2378     then obtain l r where "l \<in> S" "strict_mono r" and to_l: "(f \<circ> r) \<longlonglongrightarrow> l"

  2379       using \<open>compact S\<close> compact_def that by metis

  2380     then obtain G where "l \<in> G" "G \<in> \<G>"

  2381       using Ssub by auto

  2382     then obtain e where "0 < e" and e: "\<And>z. dist z l < e \<Longrightarrow> z \<in> G"

  2383       using opn open_dist by blast

  2384     obtain N1 where N1: "\<And>n. n \<ge> N1 \<Longrightarrow> dist (f (r n)) l < e/2"

  2385       using to_l apply (simp add: lim_sequentially)

  2386       using \<open>0 < e\<close> half_gt_zero that by blast

  2387     obtain N2 where N2: "of_nat N2 > 2/e"

  2388       using reals_Archimedean2 by blast

  2389     obtain x where "x \<in> ball (f (r (max N1 N2))) (1 / real (Suc (r (max N1 N2))))" and "x \<notin> G"

  2390       using fG [OF \<open>G \<in> \<G>\<close>, of "r (max N1 N2)"] by blast

  2391     then have "dist (f (r (max N1 N2))) x < 1 / real (Suc (r (max N1 N2)))"

  2392       by simp

  2393     also have "... \<le> 1 / real (Suc (max N1 N2))"

  2394       apply (simp add: divide_simps del: max.bounded_iff)

  2395       using \<open>strict_mono r\<close> seq_suble by blast

  2396     also have "... \<le> 1 / real (Suc N2)"

  2397       by (simp add: field_simps)

  2398     also have "... < e/2"

  2399       using N2 \<open>0 < e\<close> by (simp add: field_simps)

  2400     finally have "dist (f (r (max N1 N2))) x < e / 2" .

  2401     moreover have "dist (f (r (max N1 N2))) l < e/2"

  2402       using N1 max.cobounded1 by blast

  2403     ultimately have "dist x l < e"

  2404       using dist_triangle_half_r by blast

  2405     then show ?thesis

  2406       using e \<open>x \<notin> G\<close> by blast

  2407   qed

  2408   then show ?thesis

  2409     by (meson that)

  2410 qed

  2411

  2412 lemma compact_uniformly_equicontinuous:

  2413   assumes "compact S"

  2414       and cont: "\<And>x e. \<lbrakk>x \<in> S; 0 < e\<rbrakk>

  2415                         \<Longrightarrow> \<exists>d. 0 < d \<and>

  2416                                 (\<forall>f \<in> \<F>. \<forall>x' \<in> S. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"

  2417       and "0 < e"

  2418   obtains d where "0 < d"

  2419                   "\<And>f x x'. \<lbrakk>f \<in> \<F>; x \<in> S; x' \<in> S; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"

  2420 proof -

  2421   obtain d where d_pos: "\<And>x e. \<lbrakk>x \<in> S; 0 < e\<rbrakk> \<Longrightarrow> 0 < d x e"

  2422      and d_dist : "\<And>x x' e f. \<lbrakk>dist x' x < d x e; x \<in> S; x' \<in> S; 0 < e; f \<in> \<F>\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"

  2423     using cont by metis

  2424   let ?\<G> = "((\<lambda>x. ball x (d x (e / 2)))  S)"

  2425   have Ssub: "S \<subseteq> \<Union> ?\<G>"

  2426     by clarsimp (metis d_pos \<open>0 < e\<close> dist_self half_gt_zero_iff)

  2427   then obtain k where "0 < k" and k: "\<And>x. x \<in> S \<Longrightarrow> \<exists>G \<in> ?\<G>. ball x k \<subseteq> G"

  2428     by (rule Heine_Borel_lemma [OF \<open>compact S\<close>]) auto

  2429   moreover have "dist (f v) (f u) < e" if "f \<in> \<F>" "u \<in> S" "v \<in> S" "dist v u < k" for f u v

  2430   proof -

  2431     obtain G where "G \<in> ?\<G>" "u \<in> G" "v \<in> G"

  2432       using k that

  2433       by (metis \<open>dist v u < k\<close> \<open>u \<in> S\<close> \<open>0 < k\<close> centre_in_ball subsetD dist_commute mem_ball)

  2434     then obtain w where w: "dist w u < d w (e / 2)" "dist w v < d w (e / 2)" "w \<in> S"

  2435       by auto

  2436     with that d_dist have "dist (f w) (f v) < e/2"

  2437       by (metis \<open>0 < e\<close> dist_commute half_gt_zero)

  2438     moreover

  2439     have "dist (f w) (f u) < e/2"

  2440       using that d_dist w by (metis \<open>0 < e\<close> dist_commute divide_pos_pos zero_less_numeral)

  2441     ultimately show ?thesis

  2442       using dist_triangle_half_r by blast

  2443   qed

  2444   ultimately show ?thesis using that by blast

  2445 qed

  2446

  2447 corollary compact_uniformly_continuous:

  2448   fixes f :: "'a :: metric_space \<Rightarrow> 'b :: metric_space"

  2449   assumes f: "continuous_on S f" and S: "compact S"

  2450   shows "uniformly_continuous_on S f"

  2451   using f

  2452     unfolding continuous_on_iff uniformly_continuous_on_def

  2453     by (force intro: compact_uniformly_equicontinuous [OF S, of "{f}"])

  2454

  2455

  2456 subsection%unimportant\<open> Theorems relating continuity and uniform continuity to closures\<close>

  2457

  2458 lemma continuous_on_closure:

  2459    "continuous_on (closure S) f \<longleftrightarrow>

  2460     (\<forall>x e. x \<in> closure S \<and> 0 < e

  2461            \<longrightarrow> (\<exists>d. 0 < d \<and> (\<forall>y. y \<in> S \<and> dist y x < d \<longrightarrow> dist (f y) (f x) < e)))"

  2462    (is "?lhs = ?rhs")

  2463 proof

  2464   assume ?lhs then show ?rhs

  2465     unfolding continuous_on_iff  by (metis Un_iff closure_def)

  2466 next

  2467   assume R [rule_format]: ?rhs

  2468   show ?lhs

  2469   proof

  2470     fix x and e::real

  2471     assume "0 < e" and x: "x \<in> closure S"

  2472     obtain \<delta>::real where "\<delta> > 0"

  2473                    and \<delta>: "\<And>y. \<lbrakk>y \<in> S; dist y x < \<delta>\<rbrakk> \<Longrightarrow> dist (f y) (f x) < e/2"

  2474       using R [of x "e/2"] \<open>0 < e\<close> x by auto

  2475     have "dist (f y) (f x) \<le> e" if y: "y \<in> closure S" and dyx: "dist y x < \<delta>/2" for y

  2476     proof -

  2477       obtain \<delta>'::real where "\<delta>' > 0"

  2478                       and \<delta>': "\<And>z. \<lbrakk>z \<in> S; dist z y < \<delta>'\<rbrakk> \<Longrightarrow> dist (f z) (f y) < e/2"

  2479         using R [of y "e/2"] \<open>0 < e\<close> y by auto

  2480       obtain z where "z \<in> S" and z: "dist z y < min \<delta>' \<delta> / 2"

  2481         using closure_approachable y

  2482         by (metis \<open>0 < \<delta>'\<close> \<open>0 < \<delta>\<close> divide_pos_pos min_less_iff_conj zero_less_numeral)

  2483       have "dist (f z) (f y) < e/2"

  2484         apply (rule \<delta>' [OF \<open>z \<in> S\<close>])

  2485         using z \<open>0 < \<delta>'\<close> by linarith

  2486       moreover have "dist (f z) (f x) < e/2"

  2487         apply (rule \<delta> [OF \<open>z \<in> S\<close>])

  2488         using z \<open>0 < \<delta>\<close>  dist_commute[of y z] dist_triangle_half_r [of y] dyx by auto

  2489       ultimately show ?thesis

  2490         by (metis dist_commute dist_triangle_half_l less_imp_le)

  2491     qed

  2492     then show "\<exists>d>0. \<forall>x'\<in>closure S. dist x' x < d \<longrightarrow> dist (f x') (f x) \<le> e"

  2493       by (rule_tac x="\<delta>/2" in exI) (simp add: \<open>\<delta> > 0\<close>)

  2494   qed

  2495 qed

  2496

  2497 lemma continuous_on_closure_sequentially:

  2498   fixes f :: "'a::metric_space \<Rightarrow> 'b :: metric_space"

  2499   shows

  2500    "continuous_on (closure S) f \<longleftrightarrow>

  2501     (\<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)"

  2502    (is "?lhs = ?rhs")

  2503 proof -

  2504   have "continuous_on (closure S) f \<longleftrightarrow>

  2505            (\<forall>x \<in> closure S. continuous (at x within S) f)"

  2506     by (force simp: continuous_on_closure continuous_within_eps_delta)

  2507   also have "... = ?rhs"

  2508     by (force simp: continuous_within_sequentially)

  2509   finally show ?thesis .

  2510 qed

  2511

  2512 lemma uniformly_continuous_on_closure:

  2513   fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"

  2514   assumes ucont: "uniformly_continuous_on S f"

  2515       and cont: "continuous_on (closure S) f"

  2516     shows "uniformly_continuous_on (closure S) f"

  2517 unfolding uniformly_continuous_on_def

  2518 proof (intro allI impI)

  2519   fix e::real

  2520   assume "0 < e"

  2521   then obtain d::real

  2522     where "d>0"

  2523       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"

  2524     using ucont [unfolded uniformly_continuous_on_def, rule_format, of "e/3"] by auto

  2525   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"

  2526   proof (rule exI [where x="d/3"], clarsimp simp: \<open>d > 0\<close>)

  2527     fix x y

  2528     assume x: "x \<in> closure S" and y: "y \<in> closure S" and dyx: "dist y x * 3 < d"

  2529     obtain d1::real where "d1 > 0"

  2530            and d1: "\<And>w. \<lbrakk>w \<in> closure S; dist w x < d1\<rbrakk> \<Longrightarrow> dist (f w) (f x) < e/3"

  2531       using cont [unfolded continuous_on_iff, rule_format, of "x" "e/3"] \<open>0 < e\<close> x by auto

  2532      obtain x' where "x' \<in> S" and x': "dist x' x < min d1 (d / 3)"

  2533         using closure_approachable [of x S]

  2534         by (metis \<open>0 < d1\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj x zero_less_numeral)

  2535     obtain d2::real where "d2 > 0"

  2536            and d2: "\<forall>w \<in> closure S. dist w y < d2 \<longrightarrow> dist (f w) (f y) < e/3"

  2537       using cont [unfolded continuous_on_iff, rule_format, of "y" "e/3"] \<open>0 < e\<close> y by auto

  2538      obtain y' where "y' \<in> S" and y': "dist y' y < min d2 (d / 3)"

  2539         using closure_approachable [of y S]

  2540         by (metis \<open>0 < d2\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj y zero_less_numeral)

  2541      have "dist x' x < d/3" using x' by auto

  2542      moreover have "dist x y < d/3"

  2543        by (metis dist_commute dyx less_divide_eq_numeral1(1))

  2544      moreover have "dist y y' < d/3"

  2545        by (metis (no_types) dist_commute min_less_iff_conj y')

  2546      ultimately have "dist x' y' < d/3 + d/3 + d/3"

  2547        by (meson dist_commute_lessI dist_triangle_lt add_strict_mono)

  2548      then have "dist x' y' < d" by simp

  2549      then have "dist (f x') (f y') < e/3"

  2550        by (rule d [OF \<open>y' \<in> S\<close> \<open>x' \<in> S\<close>])

  2551      moreover have "dist (f x') (f x) < e/3" using \<open>x' \<in> S\<close> closure_subset x' d1

  2552        by (simp add: closure_def)

  2553      moreover have "dist (f y') (f y) < e/3" using \<open>y' \<in> S\<close> closure_subset y' d2

  2554        by (simp add: closure_def)

  2555      ultimately have "dist (f y) (f x) < e/3 + e/3 + e/3"

  2556        by (meson dist_commute_lessI dist_triangle_lt add_strict_mono)

  2557     then show "dist (f y) (f x) < e" by simp

  2558   qed

  2559 qed

  2560

  2561 lemma uniformly_continuous_on_extension_at_closure:

  2562   fixes f::"'a::metric_space \<Rightarrow> 'b::complete_space"

  2563   assumes uc: "uniformly_continuous_on X f"

  2564   assumes "x \<in> closure X"

  2565   obtains l where "(f \<longlongrightarrow> l) (at x within X)"

  2566 proof -

  2567   from assms obtain xs where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X"

  2568     by (auto simp: closure_sequential)

  2569

  2570   from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF xs]

  2571   obtain l where l: "(\<lambda>n. f (xs n)) \<longlonglongrightarrow> l"

  2572     by atomize_elim (simp only: convergent_eq_Cauchy)

  2573

  2574   have "(f \<longlongrightarrow> l) (at x within X)"

  2575   proof (safe intro!: Lim_within_LIMSEQ)

  2576     fix xs'

  2577     assume "\<forall>n. xs' n \<noteq> x \<and> xs' n \<in> X"

  2578       and xs': "xs' \<longlonglongrightarrow> x"

  2579     then have "xs' n \<noteq> x" "xs' n \<in> X" for n by auto

  2580

  2581     from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF \<open>xs' \<longlonglongrightarrow> x\<close> \<open>xs' _ \<in> X\<close>]

  2582     obtain l' where l': "(\<lambda>n. f (xs' n)) \<longlonglongrightarrow> l'"

  2583       by atomize_elim (simp only: convergent_eq_Cauchy)

  2584

  2585     show "(\<lambda>n. f (xs' n)) \<longlonglongrightarrow> l"

  2586     proof (rule tendstoI)

  2587       fix e::real assume "e > 0"

  2588       define e' where "e' \<equiv> e / 2"

  2589       have "e' > 0" using \<open>e > 0\<close> by (simp add: e'_def)

  2590

  2591       have "\<forall>\<^sub>F n in sequentially. dist (f (xs n)) l < e'"

  2592         by (simp add: \<open>0 < e'\<close> l tendstoD)

  2593       moreover

  2594       from uc[unfolded uniformly_continuous_on_def, rule_format, OF \<open>e' > 0\<close>]

  2595       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'"

  2596         by auto

  2597       have "\<forall>\<^sub>F n in sequentially. dist (xs n) (xs' n) < d"

  2598         by (auto intro!: \<open>0 < d\<close> order_tendstoD tendsto_eq_intros xs xs')

  2599       ultimately

  2600       show "\<forall>\<^sub>F n in sequentially. dist (f (xs' n)) l < e"

  2601       proof eventually_elim

  2602         case (elim n)

  2603         have "dist (f (xs' n)) l \<le> dist (f (xs n)) (f (xs' n)) + dist (f (xs n)) l"

  2604           by (metis dist_triangle dist_commute)

  2605         also have "dist (f (xs n)) (f (xs' n)) < e'"

  2606           by (auto intro!: d xs \<open>xs' _ \<in> _\<close> elim)

  2607         also note \<open>dist (f (xs n)) l < e'\<close>

  2608         also have "e' + e' = e" by (simp add: e'_def)

  2609         finally show ?case by simp

  2610       qed

  2611     qed

  2612   qed

  2613   thus ?thesis ..

  2614 qed

  2615

  2616 lemma uniformly_continuous_on_extension_on_closure:

  2617   fixes f::"'a::metric_space \<Rightarrow> 'b::complete_space"

  2618   assumes uc: "uniformly_continuous_on X f"

  2619   obtains g where "uniformly_continuous_on (closure X) g" "\<And>x. x \<in> X \<Longrightarrow> f x = g x"

  2620     "\<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"

  2621 proof -

  2622   from uc have cont_f: "continuous_on X f"

  2623     by (simp add: uniformly_continuous_imp_continuous)

  2624   obtain y where y: "(f \<longlongrightarrow> y x) (at x within X)" if "x \<in> closure X" for x

  2625     apply atomize_elim

  2626     apply (rule choice)

  2627     using uniformly_continuous_on_extension_at_closure[OF assms]

  2628     by metis

  2629   let ?g = "\<lambda>x. if x \<in> X then f x else y x"

  2630

  2631   have "uniformly_continuous_on (closure X) ?g"

  2632     unfolding uniformly_continuous_on_def

  2633   proof safe

  2634     fix e::real assume "e > 0"

  2635     define e' where "e' \<equiv> e / 3"

  2636     have "e' > 0" using \<open>e > 0\<close> by (simp add: e'_def)

  2637     from uc[unfolded uniformly_continuous_on_def, rule_format, OF \<open>0 < e'\<close>]

  2638     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'"

  2639       by auto

  2640     define d' where "d' = d / 3"

  2641     have "d' > 0" using \<open>d > 0\<close> by (simp add: d'_def)

  2642     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"

  2643     proof (safe intro!: exI[where x=d'] \<open>d' > 0\<close>)

  2644       fix x x' assume x: "x \<in> closure X" and x': "x' \<in> closure X" and dist: "dist x' x < d'"

  2645       then obtain xs xs' where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X"

  2646         and xs': "xs' \<longlonglongrightarrow> x'" "\<And>n. xs' n \<in> X"

  2647         by (auto simp: closure_sequential)

  2648       have "\<forall>\<^sub>F n in sequentially. dist (xs' n) x' < d'"

  2649         and "\<forall>\<^sub>F n in sequentially. dist (xs n) x < d'"

  2650         by (auto intro!: \<open>0 < d'\<close> order_tendstoD tendsto_eq_intros xs xs')

  2651       moreover

  2652       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

  2653         using that not_eventuallyD

  2654         by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at)

  2655       then have "(\<lambda>x. f (xs' x)) \<longlonglongrightarrow> ?g x'" "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> ?g x"

  2656         using x x'

  2657         by (auto intro!: continuous_on_tendsto_compose[OF cont_f] simp: xs' xs)

  2658       then have "\<forall>\<^sub>F n in sequentially. dist (f (xs' n)) (?g x') < e'"

  2659         "\<forall>\<^sub>F n in sequentially. dist (f (xs n)) (?g x) < e'"

  2660         by (auto intro!: \<open>0 < e'\<close> order_tendstoD tendsto_eq_intros)

  2661       ultimately

  2662       have "\<forall>\<^sub>F n in sequentially. dist (?g x') (?g x) < e"

  2663       proof eventually_elim

  2664         case (elim n)

  2665         have "dist (?g x') (?g x) \<le>

  2666           dist (f (xs' n)) (?g x') + dist (f (xs' n)) (f (xs n)) + dist (f (xs n)) (?g x)"

  2667           by (metis add.commute add_le_cancel_left dist_commute dist_triangle dist_triangle_le)

  2668         also

  2669         {

  2670           have "dist (xs' n) (xs n) \<le> dist (xs' n) x' + dist x' x + dist (xs n) x"

  2671             by (metis add.commute add_le_cancel_left  dist_triangle dist_triangle_le)

  2672           also note \<open>dist (xs' n) x' < d'\<close>

  2673           also note \<open>dist x' x < d'\<close>

  2674           also note \<open>dist (xs n) x < d'\<close>

  2675           finally have "dist (xs' n) (xs n) < d" by (simp add: d'_def)

  2676         }

  2677         with \<open>xs _ \<in> X\<close> \<open>xs' _ \<in> X\<close> have "dist (f (xs' n)) (f (xs n)) < e'"

  2678           by (rule d)

  2679         also note \<open>dist (f (xs' n)) (?g x') < e'\<close>

  2680         also note \<open>dist (f (xs n)) (?g x) < e'\<close>

  2681         finally show ?case by (simp add: e'_def)

  2682       qed

  2683       then show "dist (?g x') (?g x) < e" by simp

  2684     qed

  2685   qed

  2686   moreover have "f x = ?g x" if "x \<in> X" for x using that by simp

  2687   moreover

  2688   {

  2689     fix Y h x

  2690     assume Y: "x \<in> Y" "X \<subseteq> Y" "Y \<subseteq> closure X" and cont_h: "continuous_on Y h"

  2691       and extension: "(\<And>x. x \<in> X \<Longrightarrow> f x = h x)"

  2692     {

  2693       assume "x \<notin> X"

  2694       have "x \<in> closure X" using Y by auto

  2695       then obtain xs where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X"

  2696         by (auto simp: closure_sequential)

  2697       from continuous_on_tendsto_compose[OF cont_h xs(1)] xs(2) Y

  2698       have hx: "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> h x"

  2699         by (auto simp: subsetD extension)

  2700       then have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> y x"

  2701         using \<open>x \<notin> X\<close> not_eventuallyD xs(2)

  2702         by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at xs)

  2703       with hx have "h x = y x" by (rule LIMSEQ_unique)

  2704     } then

  2705     have "h x = ?g x"

  2706       using extension by auto

  2707   }

  2708   ultimately show ?thesis ..

  2709 qed

  2710

  2711 lemma bounded_uniformly_continuous_image:

  2712   fixes f :: "'a :: heine_borel \<Rightarrow> 'b :: heine_borel"

  2713   assumes "uniformly_continuous_on S f" "bounded S"

  2714   shows "bounded(f  S)"

  2715   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)

  2716

  2717

  2718 subsection \<open>With Abstract Topology (TODO: move and remove dependency?)\<close>

  2719

  2720 lemma openin_contains_ball:

  2721     "openin (top_of_set t) s \<longleftrightarrow>

  2722      s \<subseteq> t \<and> (\<forall>x \<in> s. \<exists>e. 0 < e \<and> ball x e \<inter> t \<subseteq> s)"

  2723     (is "?lhs = ?rhs")

  2724 proof

  2725   assume ?lhs

  2726   then show ?rhs

  2727     apply (simp add: openin_open)

  2728     apply (metis Int_commute Int_mono inf.cobounded2 open_contains_ball order_refl subsetCE)

  2729     done

  2730 next

  2731   assume ?rhs

  2732   then show ?lhs

  2733     apply (simp add: openin_euclidean_subtopology_iff)

  2734     by (metis (no_types) Int_iff dist_commute inf.absorb_iff2 mem_ball)

  2735 qed

  2736

  2737 lemma openin_contains_cball:

  2738    "openin (top_of_set t) s \<longleftrightarrow>

  2739         s \<subseteq> t \<and>

  2740         (\<forall>x \<in> s. \<exists>e. 0 < e \<and> cball x e \<inter> t \<subseteq> s)"

  2741   apply (simp add: openin_contains_ball)

  2742   apply (rule iffI)

  2743    apply (auto dest!: bspec)

  2744    apply (rule_tac x="e/2" in exI, force+)

  2745   done

  2746

  2747

  2748 subsection \<open>Closed Nest\<close>

  2749

  2750 text \<open>Bounded closed nest property (proof does not use Heine-Borel)\<close>

  2751

  2752 lemma bounded_closed_nest:

  2753   fixes S :: "nat \<Rightarrow> ('a::heine_borel) set"

  2754   assumes "\<And>n. closed (S n)"

  2755       and "\<And>n. S n \<noteq> {}"

  2756       and "\<And>m n. m \<le> n \<Longrightarrow> S n \<subseteq> S m"

  2757       and "bounded (S 0)"

  2758   obtains a where "\<And>n. a \<in> S n"

  2759 proof -

  2760   from assms(2) obtain x where x: "\<forall>n. x n \<in> S n"

  2761     using choice[of "\<lambda>n x. x \<in> S n"] by auto

  2762   from assms(4,1) have "seq_compact (S 0)"

  2763     by (simp add: bounded_closed_imp_seq_compact)

  2764   then obtain l r where lr: "l \<in> S 0" "strict_mono r" "(x \<circ> r) \<longlonglongrightarrow> l"

  2765     using x and assms(3) unfolding seq_compact_def by blast

  2766   have "\<forall>n. l \<in> S n"

  2767   proof

  2768     fix n :: nat

  2769     have "closed (S n)"

  2770       using assms(1) by simp

  2771     moreover have "\<forall>i. (x \<circ> r) i \<in> S i"

  2772       using x and assms(3) and lr(2) [THEN seq_suble] by auto

  2773     then have "\<forall>i. (x \<circ> r) (i + n) \<in> S n"

  2774       using assms(3) by (fast intro!: le_add2)

  2775     moreover have "(\<lambda>i. (x \<circ> r) (i + n)) \<longlonglongrightarrow> l"

  2776       using lr(3) by (rule LIMSEQ_ignore_initial_segment)

  2777     ultimately show "l \<in> S n"

  2778       by (rule closed_sequentially)

  2779   qed

  2780   then show ?thesis

  2781     using that by blast

  2782 qed

  2783

  2784 text \<open>Decreasing case does not even need compactness, just completeness.\<close>

  2785

  2786 lemma decreasing_closed_nest:

  2787   fixes S :: "nat \<Rightarrow> ('a::complete_space) set"

  2788   assumes "\<And>n. closed (S n)"

  2789           "\<And>n. S n \<noteq> {}"

  2790           "\<And>m n. m \<le> n \<Longrightarrow> S n \<subseteq> S m"

  2791           "\<And>e. e>0 \<Longrightarrow> \<exists>n. \<forall>x\<in>S n. \<forall>y\<in>S n. dist x y < e"

  2792   obtains a where "\<And>n. a \<in> S n"

  2793 proof -

  2794   have "\<forall>n. \<exists>x. x \<in> S n"

  2795     using assms(2) by auto

  2796   then have "\<exists>t. \<forall>n. t n \<in> S n"

  2797     using choice[of "\<lambda>n x. x \<in> S n"] by auto

  2798   then obtain t where t: "\<forall>n. t n \<in> S n" by auto

  2799   {

  2800     fix e :: real

  2801     assume "e > 0"

  2802     then obtain N where N: "\<forall>x\<in>S N. \<forall>y\<in>S N. dist x y < e"

  2803       using assms(4) by blast

  2804     {

  2805       fix m n :: nat

  2806       assume "N \<le> m \<and> N \<le> n"

  2807       then have "t m \<in> S N" "t n \<in> S N"

  2808         using assms(3) t unfolding  subset_eq t by blast+

  2809       then have "dist (t m) (t n) < e"

  2810         using N by auto

  2811     }

  2812     then have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (t m) (t n) < e"

  2813       by auto

  2814   }

  2815   then have "Cauchy t"

  2816     unfolding cauchy_def by auto

  2817   then obtain l where l:"(t \<longlongrightarrow> l) sequentially"

  2818     using complete_UNIV unfolding complete_def by auto

  2819   { fix n :: nat

  2820     { fix e :: real

  2821       assume "e > 0"

  2822       then obtain N :: nat where N: "\<forall>n\<ge>N. dist (t n) l < e"

  2823         using l[unfolded lim_sequentially] by auto

  2824       have "t (max n N) \<in> S n"

  2825         by (meson assms(3) contra_subsetD max.cobounded1 t)

  2826       then have "\<exists>y\<in>S n. dist y l < e"

  2827         using N max.cobounded2 by blast

  2828     }

  2829     then have "l \<in> S n"

  2830       using closed_approachable[of "S n" l] assms(1) by auto

  2831   }

  2832   then show ?thesis

  2833     using that by blast

  2834 qed

  2835

  2836 text \<open>Strengthen it to the intersection actually being a singleton.\<close>

  2837

  2838 lemma decreasing_closed_nest_sing:

  2839   fixes S :: "nat \<Rightarrow> 'a::complete_space set"

  2840   assumes "\<And>n. closed(S n)"

  2841           "\<And>n. S n \<noteq> {}"

  2842           "\<And>m n. m \<le> n \<Longrightarrow> S n \<subseteq> S m"

  2843           "\<And>e. e>0 \<Longrightarrow> \<exists>n. \<forall>x \<in> (S n). \<forall> y\<in>(S n). dist x y < e"

  2844   shows "\<exists>a. \<Inter>(range S) = {a}"

  2845 proof -

  2846   obtain a where a: "\<forall>n. a \<in> S n"

  2847     using decreasing_closed_nest[of S] using assms by auto

  2848   { fix b

  2849     assume b: "b \<in> \<Inter>(range S)"

  2850     { fix e :: real

  2851       assume "e > 0"

  2852       then have "dist a b < e"

  2853         using assms(4) and b and a by blast

  2854     }

  2855     then have "dist a b = 0"

  2856       by (metis dist_eq_0_iff dist_nz less_le)

  2857   }

  2858   with a have "\<Inter>(range S) = {a}"

  2859     unfolding image_def by auto

  2860   then show ?thesis ..

  2861 qed

  2862

  2863 subsection%unimportant \<open>Making a continuous function avoid some value in a neighbourhood\<close>

  2864

  2865 lemma continuous_within_avoid:

  2866   fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"

  2867   assumes "continuous (at x within s) f"

  2868     and "f x \<noteq> a"

  2869   shows "\<exists>e>0. \<forall>y \<in> s. dist x y < e --> f y \<noteq> a"

  2870 proof -

  2871   obtain U where "open U" and "f x \<in> U" and "a \<notin> U"

  2872     using t1_space [OF \<open>f x \<noteq> a\<close>] by fast

  2873   have "(f \<longlongrightarrow> f x) (at x within s)"

  2874     using assms(1) by (simp add: continuous_within)

  2875   then have "eventually (\<lambda>y. f y \<in> U) (at x within s)"

  2876     using \<open>open U\<close> and \<open>f x \<in> U\<close>

  2877     unfolding tendsto_def by fast

  2878   then have "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"

  2879     using \<open>a \<notin> U\<close> by (fast elim: eventually_mono)

  2880   then show ?thesis

  2881     using \<open>f x \<noteq> a\<close> by (auto simp: dist_commute eventually_at)

  2882 qed

  2883

  2884 lemma continuous_at_avoid:

  2885   fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"

  2886   assumes "continuous (at x) f"

  2887     and "f x \<noteq> a"

  2888   shows "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> f y \<noteq> a"

  2889   using assms continuous_within_avoid[of x UNIV f a] by simp

  2890

  2891 lemma continuous_on_avoid:

  2892   fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"

  2893   assumes "continuous_on s f"

  2894     and "x \<in> s"

  2895     and "f x \<noteq> a"

  2896   shows "\<exists>e>0. \<forall>y \<in> s. dist x y < e \<longrightarrow> f y \<noteq> a"

  2897   using assms(1)[unfolded continuous_on_eq_continuous_within, THEN bspec[where x=x],

  2898     OF assms(2)] continuous_within_avoid[of x s f a]

  2899   using assms(3)

  2900   by auto

  2901

  2902 lemma continuous_on_open_avoid:

  2903   fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"

  2904   assumes "continuous_on s f"

  2905     and "open s"

  2906     and "x \<in> s"

  2907     and "f x \<noteq> a"

  2908   shows "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> f y \<noteq> a"

  2909   using assms(1)[unfolded continuous_on_eq_continuous_at[OF assms(2)], THEN bspec[where x=x], OF assms(3)]

  2910   using continuous_at_avoid[of x f a] assms(4)

  2911   by auto

  2912

  2913 subsection \<open>Consequences for Real Numbers\<close>

  2914

  2915 lemma closed_contains_Inf:

  2916   fixes S :: "real set"

  2917   shows "S \<noteq> {} \<Longrightarrow> bdd_below S \<Longrightarrow> closed S \<Longrightarrow> Inf S \<in> S"

  2918   by (metis closure_contains_Inf closure_closed)

  2919

  2920 lemma closed_subset_contains_Inf:

  2921   fixes A C :: "real set"

  2922   shows "closed C \<Longrightarrow> A \<subseteq> C \<Longrightarrow> A \<noteq> {} \<Longrightarrow> bdd_below A \<Longrightarrow> Inf A \<in> C"

  2923   by (metis closure_contains_Inf closure_minimal subset_eq)

  2924

  2925 lemma atLeastAtMost_subset_contains_Inf:

  2926   fixes A :: "real set" and a b :: real

  2927   shows "A \<noteq> {} \<Longrightarrow> a \<le> b \<Longrightarrow> A \<subseteq> {a..b} \<Longrightarrow> Inf A \<in> {a..b}"

  2928   by (rule closed_subset_contains_Inf)

  2929      (auto intro: closed_real_atLeastAtMost intro!: bdd_belowI[of A a])

  2930

  2931 lemma bounded_real: "bounded (S::real set) \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. \<bar>x\<bar> \<le> a)"

  2932   by (simp add: bounded_iff)

  2933

  2934 lemma bounded_imp_bdd_above: "bounded S \<Longrightarrow> bdd_above (S :: real set)"

  2935   by (auto simp: bounded_def bdd_above_def dist_real_def)

  2936      (metis abs_le_D1 abs_minus_commute diff_le_eq)

  2937

  2938 lemma bounded_imp_bdd_below: "bounded S \<Longrightarrow> bdd_below (S :: real set)"

  2939   by (auto simp: bounded_def bdd_below_def dist_real_def)

  2940      (metis abs_le_D1 add.commute diff_le_eq)

  2941

  2942 lemma bounded_has_Sup:

  2943   fixes S :: "real set"

  2944   assumes "bounded S"

  2945     and "S \<noteq> {}"

  2946   shows "\<forall>x\<in>S. x \<le> Sup S"

  2947     and "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> b"

  2948 proof

  2949   show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> b"

  2950     using assms by (metis cSup_least)

  2951 qed (metis cSup_upper assms(1) bounded_imp_bdd_above)

  2952

  2953 lemma Sup_insert:

  2954   fixes S :: "real set"

  2955   shows "bounded S \<Longrightarrow> Sup (insert x S) = (if S = {} then x else max x (Sup S))"

  2956   by (auto simp: bounded_imp_bdd_above sup_max cSup_insert_If)

  2957

  2958 lemma bounded_has_Inf:

  2959   fixes S :: "real set"

  2960   assumes "bounded S"

  2961     and "S \<noteq> {}"

  2962   shows "\<forall>x\<in>S. x \<ge> Inf S"

  2963     and "\<forall>b. (\<forall>x\<in>S. x \<ge> b) \<longrightarrow> Inf S \<ge> b"

  2964 proof

  2965   show "\<forall>b. (\<forall>x\<in>S. x \<ge> b) \<longrightarrow> Inf S \<ge> b"

  2966     using assms by (metis cInf_greatest)

  2967 qed (metis cInf_lower assms(1) bounded_imp_bdd_below)

  2968

  2969 lemma Inf_insert:

  2970   fixes S :: "real set"

  2971   shows "bounded S \<Longrightarrow> Inf (insert x S) = (if S = {} then x else min x (Inf S))"

  2972   by (auto simp: bounded_imp_bdd_below inf_min cInf_insert_If)

  2973

  2974 lemma open_real:

  2975   fixes s :: "real set"

  2976   shows "open s \<longleftrightarrow> (\<forall>x \<in> s. \<exists>e>0. \<forall>x'. \<bar>x' - x\<bar> < e --> x' \<in> s)"

  2977   unfolding open_dist dist_norm by simp

  2978

  2979 lemma islimpt_approachable_real:

  2980   fixes s :: "real set"

  2981   shows "x islimpt s \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> s. x' \<noteq> x \<and> \<bar>x' - x\<bar> < e)"

  2982   unfolding islimpt_approachable dist_norm by simp

  2983

  2984 lemma closed_real:

  2985   fixes s :: "real set"

  2986   shows "closed s \<longleftrightarrow> (\<forall>x. (\<forall>e>0.  \<exists>x' \<in> s. x' \<noteq> x \<and> \<bar>x' - x\<bar> < e) \<longrightarrow> x \<in> s)"

  2987   unfolding closed_limpt islimpt_approachable dist_norm by simp

  2988

  2989 lemma continuous_at_real_range:

  2990   fixes f :: "'a::real_normed_vector \<Rightarrow> real"

  2991   shows "continuous (at x) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'. norm(x' - x) < d --> \<bar>f x' - f x\<bar> < e)"

  2992   unfolding continuous_at

  2993   unfolding Lim_at

  2994   unfolding dist_norm

  2995   apply auto

  2996   apply (erule_tac x=e in allE, auto)

  2997   apply (rule_tac x=d in exI, auto)

  2998   apply (erule_tac x=x' in allE, auto)

  2999   apply (erule_tac x=e in allE, auto)

  3000   done

  3001

  3002 lemma continuous_on_real_range:

  3003   fixes f :: "'a::real_normed_vector \<Rightarrow> real"

  3004   shows "continuous_on s f \<longleftrightarrow>

  3005     (\<forall>x \<in> s. \<forall>e>0. \<exists>d>0. (\<forall>x' \<in> s. norm(x' - x) < d \<longrightarrow> \<bar>f x' - f x\<bar> < e))"

  3006   unfolding continuous_on_iff dist_norm by simp

  3007

  3008 lemma continuous_on_closed_Collect_le:

  3009   fixes f g :: "'a::topological_space \<Rightarrow> real"

  3010   assumes f: "continuous_on s f" and g: "continuous_on s g" and s: "closed s"

  3011   shows "closed {x \<in> s. f x \<le> g x}"

  3012 proof -

  3013   have "closed ((\<lambda>x. g x - f x) - {0..} \<inter> s)"

  3014     using closed_real_atLeast continuous_on_diff [OF g f]

  3015     by (simp add: continuous_on_closed_vimage [OF s])

  3016   also have "((\<lambda>x. g x - f x) - {0..} \<inter> s) = {x\<in>s. f x \<le> g x}"

  3017     by auto

  3018   finally show ?thesis .

  3019 qed

  3020

  3021 lemma continuous_le_on_closure:

  3022   fixes a::real

  3023   assumes f: "continuous_on (closure s) f"

  3024       and x: "x \<in> closure(s)"

  3025       and xlo: "\<And>x. x \<in> s ==> f(x) \<le> a"

  3026     shows "f(x) \<le> a"

  3027   using image_closure_subset [OF f, where T=" {x. x \<le> a}" ] assms

  3028     continuous_on_closed_Collect_le[of "UNIV" "\<lambda>x. x" "\<lambda>x. a"]

  3029   by auto

  3030

  3031 lemma continuous_ge_on_closure:

  3032   fixes a::real

  3033   assumes f: "continuous_on (closure s) f"

  3034       and x: "x \<in> closure(s)"

  3035       and xlo: "\<And>x. x \<in> s ==> f(x) \<ge> a"

  3036     shows "f(x) \<ge> a"

  3037   using image_closure_subset [OF f, where T=" {x. a \<le> x}"] assms

  3038     continuous_on_closed_Collect_le[of "UNIV" "\<lambda>x. a" "\<lambda>x. x"]

  3039   by auto

  3040

  3041

  3042 subsection\<open>The infimum of the distance between two sets\<close>

  3043

  3044 definition%important setdist :: "'a::metric_space set \<Rightarrow> 'a set \<Rightarrow> real" where

  3045   "setdist s t \<equiv>

  3046        (if s = {} \<or> t = {} then 0

  3047         else Inf {dist x y| x y. x \<in> s \<and> y \<in> t})"

  3048

  3049 lemma setdist_empty1 [simp]: "setdist {} t = 0"

  3050   by (simp add: setdist_def)

  3051

  3052 lemma setdist_empty2 [simp]: "setdist t {} = 0"

  3053   by (simp add: setdist_def)

  3054

  3055 lemma setdist_pos_le [simp]: "0 \<le> setdist s t"

  3056   by (auto simp: setdist_def ex_in_conv [symmetric] intro: cInf_greatest)

  3057

  3058 lemma le_setdistI:

  3059   assumes "s \<noteq> {}" "t \<noteq> {}" "\<And>x y. \<lbrakk>x \<in> s; y \<in> t\<rbrakk> \<Longrightarrow> d \<le> dist x y"

  3060     shows "d \<le> setdist s t"

  3061   using assms

  3062   by (auto simp: setdist_def Set.ex_in_conv [symmetric] intro: cInf_greatest)

  3063

  3064 lemma setdist_le_dist: "\<lbrakk>x \<in> s; y \<in> t\<rbrakk> \<Longrightarrow> setdist s t \<le> dist x y"

  3065   unfolding setdist_def

  3066   by (auto intro!: bdd_belowI [where m=0] cInf_lower)

  3067

  3068 lemma le_setdist_iff:

  3069         "d \<le> setdist s t \<longleftrightarrow>

  3070         (\<forall>x \<in> s. \<forall>y \<in> t. d \<le> dist x y) \<and> (s = {} \<or> t = {} \<longrightarrow> d \<le> 0)"

  3071   apply (cases "s = {} \<or> t = {}")

  3072   apply (force simp add: setdist_def)

  3073   apply (intro iffI conjI)

  3074   using setdist_le_dist apply fastforce

  3075   apply (auto simp: intro: le_setdistI)

  3076   done

  3077

  3078 lemma setdist_ltE:

  3079   assumes "setdist s t < b" "s \<noteq> {}" "t \<noteq> {}"

  3080     obtains x y where "x \<in> s" "y \<in> t" "dist x y < b"

  3081 using assms

  3082 by (auto simp: not_le [symmetric] le_setdist_iff)

  3083

  3084 lemma setdist_refl: "setdist s s = 0"

  3085   apply (cases "s = {}")

  3086   apply (force simp add: setdist_def)

  3087   apply (rule antisym [OF _ setdist_pos_le])

  3088   apply (metis all_not_in_conv dist_self setdist_le_dist)

  3089   done

  3090

  3091 lemma setdist_sym: "setdist s t = setdist t s"

  3092   by (force simp: setdist_def dist_commute intro!: arg_cong [where f=Inf])

  3093

  3094 lemma setdist_triangle: "setdist s t \<le> setdist s {a} + setdist {a} t"

  3095 proof (cases "s = {} \<or> t = {}")

  3096   case True then show ?thesis

  3097     using setdist_pos_le by fastforce

  3098 next

  3099   case False

  3100   have "\<And>x. x \<in> s \<Longrightarrow> setdist s t - dist x a \<le> setdist {a} t"

  3101     apply (rule le_setdistI, blast)

  3102     using False apply (fastforce intro: le_setdistI)

  3103     apply (simp add: algebra_simps)

  3104     apply (metis dist_commute dist_triangle3 order_trans [OF setdist_le_dist])

  3105     done

  3106   then have "setdist s t - setdist {a} t \<le> setdist s {a}"

  3107     using False by (fastforce intro: le_setdistI)

  3108   then show ?thesis

  3109     by (simp add: algebra_simps)

  3110 qed

  3111

  3112 lemma setdist_singletons [simp]: "setdist {x} {y} = dist x y"

  3113   by (simp add: setdist_def)

  3114

  3115 lemma setdist_Lipschitz: "\<bar>setdist {x} s - setdist {y} s\<bar> \<le> dist x y"

  3116   apply (subst setdist_singletons [symmetric])

  3117   by (metis abs_diff_le_iff diff_le_eq setdist_triangle setdist_sym)

  3118

  3119 lemma continuous_at_setdist [continuous_intros]: "continuous (at x) (\<lambda>y. (setdist {y} s))"

  3120   by (force simp: continuous_at_eps_delta dist_real_def intro: le_less_trans [OF setdist_Lipschitz])

  3121

  3122 lemma continuous_on_setdist [continuous_intros]: "continuous_on t (\<lambda>y. (setdist {y} s))"

  3123   by (metis continuous_at_setdist continuous_at_imp_continuous_on)

  3124

  3125 lemma uniformly_continuous_on_setdist: "uniformly_continuous_on t (\<lambda>y. (setdist {y} s))"

  3126   by (force simp: uniformly_continuous_on_def dist_real_def intro: le_less_trans [OF setdist_Lipschitz])

  3127

  3128 lemma setdist_subset_right: "\<lbrakk>t \<noteq> {}; t \<subseteq> u\<rbrakk> \<Longrightarrow> setdist s u \<le> setdist s t"

  3129   apply (cases "s = {} \<or> u = {}", force)

  3130   apply (auto simp: setdist_def intro!: bdd_belowI [where m=0] cInf_superset_mono)

  3131   done

  3132

  3133 lemma setdist_subset_left: "\<lbrakk>s \<noteq> {}; s \<subseteq> t\<rbrakk> \<Longrightarrow> setdist t u \<le> setdist s u"

  3134   by (metis setdist_subset_right setdist_sym)

  3135

  3136 lemma setdist_closure_1 [simp]: "setdist (closure s) t = setdist s t"

  3137 proof (cases "s = {} \<or> t = {}")

  3138   case True then show ?thesis by force

  3139 next

  3140   case False

  3141   { fix y

  3142     assume "y \<in> t"

  3143     have "continuous_on (closure s) (\<lambda>a. dist a y)"

  3144       by (auto simp: continuous_intros dist_norm)

  3145     then have *: "\<And>x. x \<in> closure s \<Longrightarrow> setdist s t \<le> dist x y"

  3146       apply (rule continuous_ge_on_closure)

  3147       apply assumption

  3148       apply (blast intro: setdist_le_dist \<open>y \<in> t\<close> )

  3149       done

  3150   } note * = this

  3151   show ?thesis

  3152     apply (rule antisym)

  3153      using False closure_subset apply (blast intro: setdist_subset_left)

  3154     using False *

  3155     apply (force simp add: closure_eq_empty intro!: le_setdistI)

  3156     done

  3157 qed

  3158

  3159 lemma setdist_closure_2 [simp]: "setdist t (closure s) = setdist t s"

  3160 by (metis setdist_closure_1 setdist_sym)

  3161

  3162 lemma setdist_eq_0I: "\<lbrakk>x \<in> S; x \<in> T\<rbrakk> \<Longrightarrow> setdist S T = 0"

  3163   by (metis antisym dist_self setdist_le_dist setdist_pos_le)

  3164

  3165 lemma setdist_unique:

  3166   "\<lbrakk>a \<in> S; b \<in> T; \<And>x y. x \<in> S \<and> y \<in> T ==> dist a b \<le> dist x y\<rbrakk>

  3167    \<Longrightarrow> setdist S T = dist a b"

  3168   by (force simp add: setdist_le_dist le_setdist_iff intro: antisym)

  3169

  3170 lemma setdist_le_sing: "x \<in> S ==> setdist S T \<le> setdist {x} T"

  3171   using setdist_subset_left by auto

  3172

  3173 lemma infdist_eq_setdist: "infdist x A = setdist {x} A"

  3174   by (simp add: infdist_def setdist_def Setcompr_eq_image)

  3175

  3176 lemma setdist_eq_infdist: "setdist A B = (if A = {} then 0 else INF a\<in>A. infdist a B)"

  3177 proof -

  3178   have "Inf {dist x y |x y. x \<in> A \<and> y \<in> B} = (INF x\<in>A. Inf (dist x  B))"

  3179     if "b \<in> B" "a \<in> A" for a b

  3180   proof (rule order_antisym)

  3181     have "Inf {dist x y |x y. x \<in> A \<and> y \<in> B} \<le> Inf (dist x  B)"

  3182       if  "b \<in> B" "a \<in> A" "x \<in> A" for x

  3183     proof -

  3184       have *: "\<And>b'. b' \<in> B \<Longrightarrow> Inf {dist x y |x y. x \<in> A \<and> y \<in> B} \<le> dist x b'"

  3185         by (metis (mono_tags, lifting) ex_in_conv setdist_def setdist_le_dist that(3))

  3186       show ?thesis

  3187         using that by (subst conditionally_complete_lattice_class.le_cInf_iff) (auto simp: *)+

  3188     qed

  3189     then show "Inf {dist x y |x y. x \<in> A \<and> y \<in> B} \<le> (INF x\<in>A. Inf (dist x  B))"

  3190       using that

  3191       by (subst conditionally_complete_lattice_class.le_cInf_iff) (auto simp: bdd_below_def)

  3192   next

  3193     have *: "\<And>x y. \<lbrakk>b \<in> B; a \<in> A; x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> \<exists>a\<in>A. Inf (dist a  B) \<le> dist x y"

  3194       by (meson bdd_below_image_dist cINF_lower)

  3195     show "(INF x\<in>A. Inf (dist x  B)) \<le> Inf {dist x y |x y. x \<in> A \<and> y \<in> B}"

  3196     proof (rule conditionally_complete_lattice_class.cInf_mono)

  3197       show "bdd_below ((\<lambda>x. Inf (dist x  B))  A)"

  3198         by (metis (no_types, lifting) bdd_belowI2 ex_in_conv infdist_def infdist_nonneg that(1))

  3199     qed (use that in \<open>auto simp: *\<close>)

  3200   qed

  3201   then show ?thesis

  3202     by (auto simp: setdist_def infdist_def)

  3203 qed

  3204

  3205 lemma continuous_on_infdist [continuous_intros]: "continuous_on B (\<lambda>y. infdist y A)"

  3206   by (simp add: continuous_on_setdist infdist_eq_setdist)

  3207

  3208 proposition setdist_attains_inf:

  3209   assumes "compact B" "B \<noteq> {}"

  3210   obtains y where "y \<in> B" "setdist A B = infdist y A"

  3211 proof (cases "A = {}")

  3212   case True

  3213   then show thesis

  3214     by (metis assms diameter_compact_attained infdist_def setdist_def that)

  3215 next

  3216   case False

  3217   obtain y where "y \<in> B" and min: "\<And>y'. y' \<in> B \<Longrightarrow> infdist y A \<le> infdist y' A"

  3218     using continuous_attains_inf [OF assms continuous_on_infdist] by blast

  3219   show thesis

  3220   proof

  3221     have "setdist A B = (INF y\<in>B. infdist y A)"

  3222       by (metis \<open>B \<noteq> {}\<close> setdist_eq_infdist setdist_sym)

  3223     also have "\<dots> = infdist y A"

  3224     proof (rule order_antisym)

  3225       show "(INF y\<in>B. infdist y A) \<le> infdist y A"

  3226       proof (rule cInf_lower)

  3227         show "infdist y A \<in> (\<lambda>y. infdist y A)  B"

  3228           using \<open>y \<in> B\<close> by blast

  3229         show "bdd_below ((\<lambda>y. infdist y A)  B)"

  3230           by (meson bdd_belowI2 infdist_nonneg)

  3231       qed

  3232     next

  3233       show "infdist y A \<le> (INF y\<in>B. infdist y A)"

  3234         by (simp add: \<open>B \<noteq> {}\<close> cINF_greatest min)

  3235     qed

  3236     finally show "setdist A B = infdist y A" .

  3237   qed (fact \<open>y \<in> B\<close>)

  3238 qed

  3239

  3240 end