Quelle Elementary_Metric_Spaces.thy Sprache: Isabelle

(*  Author:     L C Paulson, University of Cambridge
    Author:     Amine Chaieb, University of Cambridge
    Author:     Robert Himmelmann, TU Muenchen
    Author:     Brian Huffman, Portland State University
    Author:     Ata Keskin, TU Muenchen
*)

chapter \<open>Elementary Metric Spaces\<close>

theory Elementary_Metric_Spaces
  imports
    Abstract_Topology_2
    Metric_Arith
begin

section \<open>Open and closed balls\<close>

definition\<^marker>\<open>tag important\<close> ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
  where "ball x \ = {y. dist x y < \}"

definition\<^marker>\<open>tag important\<close> cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
  where "cball x \ = {y. dist x y \ \}"

definition\<^marker>\<open>tag important\<close> sphere :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
  where "sphere x \ = {y. dist x y = \}"

lemma mem_ball [simp, metric_unfold]: "y \ ball x \ \ dist x y < \"
  by (simp add: ball_def)

lemma mem_cball [simp, metric_unfold]: "y \ cball x \ \ dist x y \ \"
  by (simp add: cball_def)

lemma mem_sphere [simp]: "y \ sphere x \ \ dist x y = \"
  by (simp add: sphere_def)

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

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

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

lemma disjoint_ballI: "dist x y \ r+s \ ball x r \ ball y s = {}"
  using dist_triangle_less_add not_le by fastforce

lemma disjoint_cballI: "dist x y > r + s \ cball x r \ cball y s = {}"
  by (metis add_mono disjoint_iff_not_equal dist_triangle2 dual_order.trans leD mem_cball)

lemma sphere_empty [simp]: "r < 0 \ sphere a r = {}"
  for a :: "'a::metric_space"
  by auto

lemma centre_in_ball [simp]: "x \ ball x \ \ 0 < \"
  by simp

lemma centre_in_cball [simp]: "x \ cball x \ \ 0 \ \"
  by simp

lemma ball_subset_cball [simp, intro]: "ball x \ \ cball x \"
  by (simp add: subset_eq)

lemma mem_ball_imp_mem_cball: "x \ ball y \ \ x \ cball y \"
  by auto

lemma sphere_cball [simp,intro]: "sphere z r \ cball z r"
  by force

lemma cball_diff_sphere: "cball a r - sphere a r = ball a r"
  by auto

lemma subset_ball[intro]: "\ \ \ \ ball x \ \ ball x \"
  by auto

lemma subset_cball[intro]: "\ \ \ \ cball x \ \ cball x \"
  by auto

lemma mem_ball_leI: "x \ ball y \ \ \ \ f \ x \ ball y f"
  by auto

lemma mem_cball_leI: "x \ cball y \ \ \ \ f \ x \ cball y f"
  by auto

lemma cball_trans: "y \ cball z b \ x \ cball y a \ x \ cball z (b + a)"
  by metric

lemma ball_max_Un: "ball a (max r s) = ball a r \ ball a s"
  by auto

lemma ball_min_Int: "ball a (min r s) = ball a r \ ball a s"
  by auto

lemma cball_max_Un: "cball a (max r s) = cball a r \ cball a s"
  by auto

lemma cball_min_Int: "cball a (min r s) = cball a r \ cball a s"
  by auto

lemma cball_diff_eq_sphere: "cball a r - ball a r = sphere a r"
  by auto

lemma open_ball [intro, simp]: "open (ball x \)"
proof -
  have "open (dist x -` {..<\})"
    by (intro open_vimage open_lessThan continuous_intros)
  also have "dist x -` {..<\} = ball x \"
    by auto
  finally show ?thesis .
qed

lemma open_contains_ball: "open S \ (\x\S. \\>0. ball x \ \ S)"
  by (simp add: open_dist subset_eq Ball_def dist_commute)

lemma openI [intro?]: "(\x. x\S \ \\>0. ball x \ \ S) \ open S"
  by (auto simp: open_contains_ball)

lemma openE[elim?]:
  assumes "open S" "x\S"
  obtains \<epsilon> where "\<epsilon>>0" "ball x \<epsilon> \<subseteq> S"
  using assms unfolding open_contains_ball by auto

lemma open_contains_ball_eq: "open S \ x\S \ (\\>0. ball x \ \ S)"
  by (metis open_contains_ball subset_eq centre_in_ball)

lemma ball_eq_empty[simp]: "ball x \ = {} \ \ \ 0"
  unfolding mem_ball set_eq_iff
  by (simp add: not_less) metric

lemma ball_empty: "\ \ 0 \ ball x \ = {}"
  by simp

lemma closed_cball [iff]: "closed (cball x \)"
proof -
  have "closed (dist x -` {..\})"
    by (intro closed_vimage closed_atMost continuous_intros)
  also have "dist x -` {..\} = cball x \"
    by auto
  finally show ?thesis .
qed

lemma cball_subset_ball:
  assumes "\>0"
  shows "\\>0. cball x \ \ ball x \"
  using assms unfolding subset_eq by (intro exI [where x="\/2"], auto)

lemma open_contains_cball: "open S \ (\x\S. \\>0. cball x \ \ S)"
  by (meson ball_subset_cball cball_subset_ball open_contains_ball subset_trans)

lemma open_contains_cball_eq: "open S \ (\x. x \ S \ (\\>0. cball x \ \ S))"
  by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball)

lemma eventually_nhds_ball: "\ > 0 \ eventually (\x. x \ ball z \) (nhds z)"
  by (rule eventually_nhds_in_open) simp_all

lemma eventually_at_ball: "\ > 0 \ eventually (\t. t \ ball z \ \ t \ A) (at z within A)"
  unfolding eventually_at by (intro exI[of _ \<delta>]) (simp_all add: dist_commute)

lemma eventually_at_ball': "\ > 0 \ eventually (\t. t \ ball z \ \ t \ z \ t \ A) (at z within A)"
  unfolding eventually_at by (intro exI[of _ \<delta>]) (simp_all add: dist_commute)

lemma at_within_ball: "\ > 0 \ dist x y < \ \ at y within ball x \ = at y"
  by (subst at_within_open) auto

lemma atLeastAtMost_eq_cball:
  fixes a b::real
  shows "{a .. b} = cball ((a + b)/2) ((b - a)/2)"
  by (auto simp: dist_real_def field_simps)

lemma cball_eq_atLeastAtMost:
  fixes a b::real
  shows "cball a b = {a - b .. a + b}"
  by (auto simp: dist_real_def)

lemma greaterThanLessThan_eq_ball:
  fixes a b::real
  shows "{a <..< b} = ball ((a + b)/2) ((b - a)/2)"
  by (auto simp: dist_real_def field_simps)

lemma ball_eq_greaterThanLessThan:
  fixes a b::real
  shows "ball a b = {a - b <..< a + b}"
  by (auto simp: dist_real_def)

lemma interior_ball [simp]: "interior (ball x \) = ball x \"
  by (simp add: interior_open)

lemma cball_eq_empty [simp]: "cball x \ = {} \ \ < 0"
  by (metis centre_in_cball order.trans ex_in_conv linorder_not_le mem_cball
      zero_le_dist)

lemma cball_empty [simp]: "\ < 0 \ cball x \ = {}"
  by simp

lemma cball_sing:
  fixes x :: "'a::metric_space"
  shows "\ = 0 \ cball x \ = {x}"
  by simp

lemma ball_divide_subset: "\ \ 1 \ ball x (\/\) \ ball x \"
  by (metis ball_eq_empty div_by_1 frac_le linear subset_ball zero_less_one)

lemma ball_divide_subset_numeral: "ball x (\ / numeral w) \ ball x \"
  using ball_divide_subset one_le_numeral by blast

lemma cball_divide_subset:
  assumes "\ \ 1"
  shows "cball x (\/\) \ cball x \"
proof (cases "\\0")
  case True
  then show ?thesis
    by (metis assms div_by_1 divide_mono order_le_less subset_cball zero_less_one)
next
  case False
  then have "(\/\) < 0"
    using assms divide_less_0_iff by fastforce
  then show ?thesis by auto
qed

lemma cball_divide_subset_numeral: "cball x (\ / numeral w) \ cball x \"
  using cball_divide_subset one_le_numeral by blast

lemma cball_scale:
  assumes "a \ 0"
  shows   "(\x. a *\<^sub>R x) ` cball c r = cball (a *\<^sub>R c :: 'a :: real_normed_vector) (\a\ * r)"
proof -
  have *: "(\x. a *\<^sub>R x) ` cball c r \ cball (a *\<^sub>R c) (\a\ * r)" for a r and c :: 'a
    by (auto simp: dist_norm simp flip: scaleR_right_diff_distrib intro!: mult_left_mono)
  have "cball (a *\<^sub>R c) (\a\ * r) = (\x. a *\<^sub>R x) ` (\x. inverse a *\<^sub>R x) ` cball (a *\<^sub>R c) (\a\ * r)"
    unfolding image_image using assms by simp
  also have "\ \ (\x. a *\<^sub>R x) ` cball (inverse a *\<^sub>R (a *\<^sub>R c)) (\inverse a\ * (\a\ * r))"
    using "*" by blast
  also have "\ = (\x. a *\<^sub>R x) ` cball c r"
    using assms by (simp add: algebra_simps)
  finally have "cball (a *\<^sub>R c) (\a\ * r) \ (\x. a *\<^sub>R x) ` cball c r" .
  moreover from assms have "(\x. a *\<^sub>R x) ` cball c r \ cball (a *\<^sub>R c) (\a\ * r)"
    using "*" by blast
  ultimately show ?thesis by blast
qed

lemma ball_scale:
  assumes "a \ 0"
  shows   "(\x. a *\<^sub>R x) ` ball c r = ball (a *\<^sub>R c :: 'a :: real_normed_vector) (\a\ * r)"
proof -
  have *: "(\x. a *\<^sub>R x) ` ball c r \ ball (a *\<^sub>R c) (\a\ * r)" if "a \ 0" for a r and c :: 'a
    using that by (auto simp: dist_norm simp flip: scaleR_right_diff_distrib)
  have "ball (a *\<^sub>R c) (\a\ * r) = (\x. a *\<^sub>R x) ` (\x. inverse a *\<^sub>R x) ` ball (a *\<^sub>R c) (\a\ * r)"
    unfolding image_image using assms by simp
  also have "\ \ (\x. a *\<^sub>R x) ` ball (inverse a *\<^sub>R (a *\<^sub>R c)) (\inverse a\ * (\a\ * r))"
    using assms by (intro image_mono *) auto
  also have "\ = (\x. a *\<^sub>R x) ` ball c r"
    using assms by (simp add: algebra_simps)
  finally have "ball (a *\<^sub>R c) (\a\ * r) \ (\x. a *\<^sub>R x) ` ball c r" .
  moreover from assms have "(\x. a *\<^sub>R x) ` ball c r \ ball (a *\<^sub>R c) (\a\ * r)"
    by (intro *) auto
  ultimately show ?thesis by blast
qed

lemma sphere_scale:
  assumes "a \ 0"
  shows   "(\x. a *\<^sub>R x) ` sphere c r = sphere (a *\<^sub>R c :: 'a :: real_normed_vector) (\a\ * r)"
proof -
  have *: "(\x. a *\<^sub>R x) ` sphere c r \ sphere (a *\<^sub>R c) (\a\ * r)" for a r and c :: 'a
    by (metis (no_types, opaque_lifting) scaleR_right_diff_distrib dist_norm image_subsetI mem_sphere norm_scaleR)
  have "sphere (a *\<^sub>R c) (\a\ * r) = (\x. a *\<^sub>R x) ` (\x. inverse a *\<^sub>R x) ` sphere (a *\<^sub>R c) (\a\ * r)"
    unfolding image_image using assms by simp
  also have "\ \ (\x. a *\<^sub>R x) ` sphere (inverse a *\<^sub>R (a *\<^sub>R c)) (\inverse a\ * (\a\ * r))"
    using "*" by blast
  also have "\ = (\x. a *\<^sub>R x) ` sphere c r"
    using assms by (simp add: algebra_simps)
  finally have "sphere (a *\<^sub>R c) (\a\ * r) \ (\x. a *\<^sub>R x) ` sphere c r" .
  moreover have "(\x. a *\<^sub>R x) ` sphere c r \ sphere (a *\<^sub>R c) (\a\ * r)"
    using "*" by blast
  ultimately show ?thesis by blast
qed

text \<open>As above, but scaled by a complex number\<close>
lemma sphere_cscale:
  assumes "a \ 0"
  shows   "(\x. a * x) ` sphere c r = sphere (a * c :: complex) (cmod a * r)"
proof -
  have *: "(\x. a * x) ` sphere c r \ sphere (a * c) (cmod a * r)" for a r c
    using dist_mult_left by fastforce
  have "sphere (a * c) (cmod a * r) = (\x. a * x) ` (\x. inverse a * x) ` sphere (a * c) (cmod a * r)"
    by (simp add: image_image inverse_eq_divide)
  also have "\ \ (\x. a * x) ` sphere (inverse a * (a * c)) (cmod (inverse a) * (cmod a * r))"
    using "*" by blast
  also have "\ = (\x. a * x) ` sphere c r"
    using assms by (simp add: field_simps flip: norm_mult)
  finally have "sphere (a * c) (cmod a * r) \ (\x. a * x) ` sphere c r" .
  moreover have "(\x. a * x) ` sphere c r \ sphere (a * c) (cmod a * r)"
    using "*" by blast
  ultimately show ?thesis by blast
qed

lemma frequently_atE:
  fixes x :: "'a :: metric_space"
  assumes "frequently P (at x within s)"
  shows   "\f. filterlim f (at x within s) sequentially \ (\n. P (f n))"
proof -
  have "\y. y \ s \ (ball x (1 / real (Suc n)) - {x}) \ P y" for n
  proof -
    have "\z\s. z \ x \ dist z x < (1 / real (Suc n)) \ P z"
      by (metis assms divide_pos_pos frequently_at of_nat_0_less_iff zero_less_Suc zero_less_one)
    then show ?thesis
      by (auto simp: dist_commute conj_commute)
  qed
  then obtain f where f: "\n. f n \ s \ (ball x (1 / real (Suc n)) - {x}) \ P (f n)"
    by metis
  have "filterlim f (nhds x) sequentially"
    unfolding tendsto_iff
  proof clarify
    fix \<epsilon> :: real
    assume \<epsilon>: "\<epsilon> > 0"
    then obtain n where n: "Suc n > 1 / \"
      by (meson le_nat_floor lessI not_le)
    have "dist (f k) x < \" if "k \ n" for k
    proof -
      have "dist (f k) x < 1 / real (Suc k)"
        using f[of k] by (auto simp: dist_commute)
      also have "\ \ 1 / real (Suc n)"
        using that by (intro divide_left_mono) auto
      also have "\ < \"
        using n \<epsilon> by (simp add: field_simps)
      finally show ?thesis .
    qed
    thus "\\<^sub>F k in sequentially. dist (f k) x < \"
      unfolding eventually_at_top_linorder by blast
  qed
  moreover have "f n \ x" for n
    using f[of n] by auto
  ultimately have "filterlim f (at x within s) sequentially"
    using f by (auto simp: filterlim_at)
  with f show ?thesis
    by blast
qed

section \<open>Limit Points\<close>

lemma islimpt_approachable:
  fixes x :: "'a::metric_space"
  shows "x islimpt S \ (\\>0. \x'\S. x' \ x \ dist x' x < \)"
  unfolding islimpt_iff_eventually eventually_at by fast

lemma islimpt_approachable_le: "x islimpt S \ (\\>0. \x'\ S. x' \ x \ dist x' x \ \)"
  for x :: "'a::metric_space"
  unfolding islimpt_approachable
  using approachable_lt_le2 [where f="\y. dist y x" and P="\y. y \ S \ y = x" and Q="\x. True"]
  by auto

lemma limpt_of_limpts: "x islimpt {y. y islimpt S} \ x islimpt S"
  for x :: "'a::metric_space"
  by (metis islimpt_def islimpt_eq_acc_point mem_Collect_eq)

lemma closed_limpts:  "closed {x::'a::metric_space. x islimpt S}"
  using closed_limpt limpt_of_limpts by blast

lemma limpt_of_closure: "x islimpt closure S \ x islimpt S"
  for x :: "'a::metric_space"
  by (auto simp: closure_def islimpt_Un dest: limpt_of_limpts)

lemma islimpt_eq_infinite_ball: "x islimpt S \ (\\>0. infinite(S \ ball x \))"
  unfolding islimpt_eq_acc_point
  by (metis open_ball Int_commute Int_mono finite_subset open_contains_ball_eq subset_eq)

lemma islimpt_eq_infinite_cball: "x islimpt S \ (\\>0. infinite(S \ cball x \))"
  unfolding islimpt_eq_infinite_ball
  by (metis ball_subset_cball cball_subset_ball finite_Int inf.absorb_iff2 inf_assoc)

section \<open>Perfect Metric Spaces\<close>

lemma perfect_choose_dist: "0 < r \ \a. a \ x \ dist a x < r"
  for x :: "'a::{perfect_space,metric_space}"
  using islimpt_UNIV [of x] by (simp add: islimpt_approachable)

lemma pointed_ball_nonempty:
  assumes "r > 0"
  shows   "ball x r - {x :: 'a :: {perfect_space, metric_space}} \ {}"
  using perfect_choose_dist[of r x] assms by (auto simp: ball_def dist_commute)

lemma cball_eq_sing:
  fixes x :: "'a::{metric_space,perfect_space}"
  shows "cball x \ = {x} \ \ = 0"
  using cball_eq_empty [of x \<epsilon>]
  by (metis open_ball ball_subset_cball cball_trivial
      centre_in_ball not_less_iff_gr_or_eq not_open_singleton subset_singleton_iff)

section \<open>Finite and discrete\<close>

lemma finite_ball_include:
  fixes a :: "'a::metric_space"
  assumes "finite S"
  shows "\\>0. S \ ball a \"
  using assms
proof induction
  case (insert x S)
  then obtain e0 where "e0>0" and e0:"S \ ball a e0" by auto
  define \<epsilon> where "\<epsilon> = max e0 (2 * dist a x)"
  have "\>0" unfolding \_def using \e0>0\ by auto
  moreover have "insert x S \ ball a \"
    using e0 \<open>\<epsilon>>0\<close> unfolding \<epsilon>_def by auto
  ultimately show ?case by auto
qed (auto intro: zero_less_one)

lemma finite_set_avoid:
  fixes a :: "'a::metric_space"
  assumes "finite S"
  shows "\\>0. \x\S. x \ a \ \ \ dist a x"
  using assms
proof induction
  case (insert x S)
  then obtain \<delta> where "\<delta> > 0" and \<delta>: "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> \<delta> \<le> dist a x"
    by blast
  then show ?case
    by (metis dist_nz dual_order.strict_implies_order insertE leI order.strict_trans2)
qed (auto intro: zero_less_one)

lemma discrete_imp_closed:
  fixes S :: "'a::metric_space set"
  assumes \<epsilon>: "0 < \<epsilon>"
    and \<delta>: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < \<epsilon> \<longrightarrow> y = x"
  shows "closed S"
proof -
  have False if C: "\\. \>0 \ \x'\S. x' \ x \ dist x' x < \" for x
  proof -
    obtain y where y: "y \ S" "y \ x" "dist y x < \/2"
      by (meson C \<epsilon> half_gt_zero)
    then have mp: "min (\/2) (dist x y) > 0"
      by (simp add: dist_commute)
    from \<delta> y C[OF mp] show ?thesis
      by metric
  qed
  then show ?thesis
    by (metis islimpt_approachable closed_limpt [where 'a='a])
qed

lemma discrete_imp_not_islimpt:
  assumes \<epsilon>: "0 < \<epsilon>"
    and \<delta>: "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> dist y x < \<epsilon> \<Longrightarrow> y = x"
  shows "\ x islimpt S"
  by (metis closed_limpt \<delta> discrete_imp_closed \<epsilon> islimpt_approachable)


section \<open>Interior\<close>

lemma mem_interior: "x \ interior S \ (\\>0. ball x \ \ S)"
  using open_contains_ball_eq [where S="interior S"]
  by (simp add: open_subset_interior)

lemma mem_interior_cball: "x \ interior S \ (\\>0. cball x \ \ S)"
  by (meson ball_subset_cball interior_subset mem_interior open_contains_cball open_interior
      subset_trans)

lemma ball_iff_cball: "(\r>0. ball x r \ U) \ (\r>0. cball x r \ U)"
  by (meson mem_interior mem_interior_cball)

section \<open>Frontier\<close>

lemma frontier_straddle:
  fixes a :: "'a::metric_space"
  shows "a \ frontier S \ (\\>0. (\x\S. dist a x < \) \ (\x. x \ S \ dist a x < \))"
  unfolding frontier_def closure_interior
  by (auto simp: mem_interior subset_eq ball_def)

section \<open>Limits\<close>

proposition Lim: "(f \ l) net \ trivial_limit net \ (\\>0. eventually (\x. dist (f x) l < \) net)"
  by (auto simp: tendsto_iff trivial_limit_eq)

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

proposition Lim_within_le: "(f \ l)(at a within S) \
    (\<forall>\<epsilon>>0. \<exists>\<delta>>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> \<delta> \<longrightarrow> dist (f x) l < \<epsilon>)"
  by (auto simp: tendsto_iff eventually_at_le)

proposition Lim_within: "(f \ l) (at a within S) \
    (\<forall>\<epsilon> >0. \<exists>\<delta>>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a  < \<delta> \<longrightarrow> dist (f x) l < \<epsilon>)"
  by (auto simp: tendsto_iff eventually_at)

corollary Lim_withinI [intro?]:
  assumes "\\. \ > 0 \ \\>0. \x \ S. 0 < dist x a \ dist x a < \ \ dist (f x) l \ \"
  shows "(f \ l) (at a within S)"
  unfolding Lim_within by (smt (verit, best) assms)

proposition Lim_at: "(f \ l) (at a) \
    (\<forall>\<epsilon> >0. \<exists>\<delta>>0. \<forall>x. 0 < dist x a \<and> dist x a < \<delta>  \<longrightarrow> dist (f x) l < \<epsilon>)"
  by (auto simp: tendsto_iff eventually_at)

lemma Lim_transform_within_set:
  fixes a :: "'a::metric_space" and l :: "'b::metric_space"
  shows "\(f \ l) (at a within S); eventually (\x. x \ S \ x \ T) (at a)\
         \<Longrightarrow> (f \<longlongrightarrow> l) (at a within T)"
  by (simp add: eventually_at Lim_within) (smt (verit, best))

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

lemma limpt_sequential_inj:
  fixes x :: "'a::metric_space"
  shows "x islimpt S \
         (\<exists>f. (\<forall>n::nat. f n \<in> S - {x}) \<and> inj f \<and> (f \<longlongrightarrow> x) sequentially)"
         (is "?lhs = ?rhs")
proof
  assume ?lhs
  then have "\\>0. \x'\S. x' \ x \ dist x' x < \"
    by (force simp: islimpt_approachable)
  then obtain y where y: "\\. \>0 \ y \ \ S \ y \ \ x \ dist (y \) x < \"
    by metis
  define f where "f \ rec_nat (y 1) (\n fn. y (min (inverse(2 ^ (Suc n))) (dist fn x)))"
  have [simp]: "f 0 = y 1"
            and fSuc: "f(Suc n) = y (min (inverse(2 ^ (Suc n))) (dist (f n) x))" for n
    by (simp_all add: f_def)
  have f: "f n \ S \ (f n \ x) \ dist (f n) x < inverse(2 ^ n)" for n
  proof (induction n)
    case 0 show ?case
      by (simp add: y)
  next
    case (Suc n)
    then have "dist (f (Suc n)) x < inverse (2 ^ Suc n)"
      unfolding fSuc
      by (metis dist_nz min_less_iff_conj positive_imp_inverse_positive y zero_less_numeral
          zero_less_power)
      with Suc show ?case
        by (auto simp: y fSuc)
  qed
  show ?rhs
  proof (intro exI conjI allI)
    show "\n. f n \ S - {x}"
      using f by blast
    have "dist (f n) x < dist (f m) x" if "m < n" for m n
    using that
    proof (induction n)
      case 0 then show ?case by simp
    next
      case (Suc n)
      then consider "m < n" | "m = n" using less_Suc_eq by blast
      then show ?case
        unfolding fSuc
        by (smt (verit, ccfv_threshold) Suc.IH dist_nz f y)
    qed
    then show "inj f"
      by (metis less_irrefl linorder_injI)
    have "\\ n. \0 < \; nat \1 / \::real\ \ n\ \ inverse (2 ^ n) < \"
      by (simp add: divide_simps order_le_less_trans)
    then show "f \ x"
      by (meson order.strict_trans f lim_sequentially)
  qed
next
  assume ?rhs
  then show ?lhs
    by (fastforce simp: islimpt_approachable lim_sequentially)
qed

lemma Lim_dist_ubound:
  assumes "\(trivial_limit net)"
    and "(f \ l) net"
    and "eventually (\x. dist a (f x) \ \) net"
  shows "dist a l \ \"
  using assms by (fast intro: tendsto_le tendsto_intros)

section \<open>Continuity\<close>

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

proposition continuous_within_eps_delta:
  "continuous (at x within s) f \ (\\>0. \\>0. \x'\ s. dist x' x < \ --> dist (f x') (f x) < \)"
  unfolding continuous_within and Lim_within  by fastforce

corollary continuous_at_eps_delta:
  "continuous (at x) f \ (\\ > 0. \\ > 0. \x'. dist x' x < \ \ dist (f x') (f x) < \)"
  using continuous_within_eps_delta [of x UNIV f] by simp

lemma continuous_at_right_real_increasing:
  fixes f :: "real \ real"
  assumes nondecF: "\x y. x \ y \ f x \ f y"
  shows "continuous (at_right a) f \ (\\>0. \\>0. f (a + \) - f a < \)"
  apply (simp add: greaterThan_def dist_real_def continuous_within Lim_within_le)
  apply (intro all_cong ex_cong)
  by (smt (verit, best) nondecF)

lemma continuous_at_left_real_increasing:
  assumes nondecF: "\ x y. x \ y \ f x \ ((f y) :: real)"
  shows "(continuous (at_left (a :: real)) f) \ (\\ > 0. \\ > 0. f a - f (a - \) < \)"
  apply (simp add: lessThan_def dist_real_def continuous_within Lim_within_le)
  apply (intro all_cong ex_cong)
  by (smt (verit) nondecF)

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

lemma continuous_within_ball:
  "continuous (at x within S) f \
    (\<forall>\<epsilon> > 0. \<exists>\<delta> > 0. f ` (ball x \<delta> \<inter> S) \<subseteq> ball (f x) \<epsilon>)"
  (is "?lhs = ?rhs")
proof
  assume ?lhs
  {
    fix \<epsilon> :: real
    assume "\ > 0"
    then obtain \<delta> where "\<delta>>0" and \<delta>: "\<forall>y\<in>S. 0 < dist y x \<and> dist y x < \<delta> \<longrightarrow> dist (f y) (f x) < \<epsilon>"
      using \<open>?lhs\<close>[unfolded continuous_within Lim_within] by auto
    have "y \ ball (f x) \" if "y \ f ` (ball x \ \ S)" for y
        using that \<delta> \<open>\<epsilon> > 0\<close> by (auto simp: dist_commute)
    then have "\\>0. f ` (ball x \ \ S) \ ball (f x) \"
      using \<open>\<delta> > 0\<close> by blast
  }
  then show ?rhs by auto
next
  assume ?rhs
  then show ?lhs
    apply (simp add: continuous_within Lim_within ball_def subset_eq)
    by (metis (mono_tags, lifting) Int_iff dist_commute mem_Collect_eq)
qed

corollary continuous_at_ball:
  "continuous (at x) f \ (\\>0. \\>0. f ` (ball x \) \ ball (f x) \)"
  by (simp add: continuous_within_ball)

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

lemma continuous_on_iff:
  "continuous_on s f \
    (\<forall>x\<in>s. \<forall>\<epsilon>>0. \<exists>\<delta>>0. \<forall>x'\<in>s. dist x' x < \<delta> \<longrightarrow> dist (f x') (f x) < \<epsilon>)"
  unfolding continuous_on_def Lim_within
  by (metis dist_pos_lt dist_self)

lemma continuous_within_E:
  assumes "continuous (at x within S) f" "\>0"
  obtains \<delta> where "\<delta>>0"  "\<And>x'. \<lbrakk>x'\<in> S; dist x' x \<le> \<delta>\<rbrakk> \<Longrightarrow> dist (f x') (f x) < \<epsilon>"
  using assms unfolding continuous_within_eps_delta
  by (metis dense order_le_less_trans)

lemma continuous_onI [intro?]:
  assumes "\x \. \\ > 0; x \ S\ \ \\>0. \x'\S. dist x' x < \ \ dist (f x') (f x) \ \"
  shows "continuous_on S f"
  using assms [OF half_gt_zero] by (force simp add: continuous_on_iff)

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

lemma continuous_onE:
    assumes "continuous_on s f" "x\s" "\>0"
    obtains \<delta> where "\<delta>>0"  "\<And>x'. \<lbrakk>x' \<in> s; dist x' x \<le> \<delta>\<rbrakk> \<Longrightarrow> dist (f x') (f x) < \<epsilon>"
  using assms
  unfolding continuous_on_iff by (metis dense order_le_less_trans)

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

lemma continuous_transform_within:
  fixes f g :: "'a::metric_space \ 'b::topological_space"
  assumes "continuous (at x within s) f"
    and "0 < \"
    and "x \ s"
    and "\x'. \x' \ s; dist x' x < \\ \ f x' = g x'"
  shows "continuous (at x within s) g"
  using assms
  unfolding continuous_within by (force intro: Lim_transform_within)

section \<open>Closure and Limit Characterization\<close>

lemma closure_approachable:
  fixes S :: "'a::metric_space set"
  shows "x \ closure S \ (\\>0. \y\S. dist y x < \)"
  using dist_self by (force simp: closure_def islimpt_approachable)

lemma closure_approachable_le:
  fixes S :: "'a::metric_space set"
  shows "x \ closure S \ (\\>0. \y\S. dist y x \ \)"
  unfolding closure_approachable
  using dense by force

lemma closure_approachableD:
  assumes "x \ closure S" "\>0"
  shows "\y\S. dist x y < \"
  using assms unfolding closure_approachable by (auto simp: dist_commute)

lemma closed_approachable:
  fixes S :: "'a::metric_space set"
  shows "closed S \ (\\>0. \y\S. dist y x < \) \ x \ S"
  by (metis closure_closed closure_approachable)

lemma closure_contains_Inf:
  fixes S :: "real set"
  assumes "S \ {}" "bdd_below S"
  shows "Inf S \ closure S"
proof -
  have *: "\x\S. Inf S \ x"
    using cInf_lower[of _ S] assms by metis
  { fix \<epsilon> :: real
    assume "\ > 0"
    then have "Inf S < Inf S + \" by simp
    with assms obtain x where "x \ S" "x < Inf S + \"
      using cInf_lessD by blast
    with * have "\x\S. dist x (Inf S) < \"
      using dist_real_def by force
  }
  then show ?thesis unfolding closure_approachable by auto
qed

lemma closure_contains_Sup:
  fixes S :: "real set"
  assumes "S \ {}" "bdd_above S"
  shows "Sup S \ closure S"
proof -
  have *: "\x\S. x \ Sup S"
    using cSup_upper[of _ S] assms by metis
  {
    fix \<epsilon> :: real
    assume "\ > 0"
    then have "Sup S - \ < Sup S" by simp
    with assms obtain x where "x \ S" "Sup S - \ < x"
      using less_cSupE by blast
    with * have "\x\S. dist x (Sup S) < \"
      using dist_real_def by force
  }
  then show ?thesis unfolding closure_approachable by auto
qed

lemma not_trivial_limit_within_ball:
  "\ trivial_limit (at x within S) \ (\\>0. S \ ball x \ - {x} \ {})"
  (is "?lhs \ ?rhs")
proof
  show ?rhs if ?lhs
  proof -
    { fix \<epsilon> :: real
      assume "\ > 0"
      then obtain y where "y \ S - {x}" and "dist y x < \"
        using \<open>?lhs\<close> not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"]
        by auto
      then have "y \ S \ ball x \ - {x}"
        unfolding ball_def by (simp add: dist_commute)
      then have "S \ ball x \ - {x} \ {}" by blast
    }
    then show ?thesis by auto
  qed
  show ?lhs if ?rhs
  proof -
    { fix \<epsilon> :: real
      assume "\ > 0"
      then obtain y where "y \ S \ ball x \ - {x}"
        using \<open>?rhs\<close> by blast
      then have "y \ S - {x}" and "dist y x < \"
        unfolding ball_def by (simp_all add: dist_commute)
      then have "\y \ S - {x}. dist y x < \"
        by auto
    }
    then show ?thesis
      using not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"]
      by auto
  qed
qed

section \<open>Boundedness\<close>

  (* FIXME: This has to be unified with BSEQ!! *)
definition\<^marker>\<open>tag important\<close> (in metric_space) bounded :: "'a set \<Rightarrow> bool"
  where "bounded S \ (\x \. \y\S. dist x y \ \)"

lemma bounded_subset_cball: "bounded S \ (\\ x. S \ cball x \ \ 0 \ \)"
  unfolding bounded_def subset_eq  by auto (meson order_trans zero_le_dist)

lemma bounded_any_center: "bounded S \ (\\. \y\S. dist a y \ \)"
  unfolding bounded_def
  by auto (metis add.commute add_le_cancel_right dist_commute dist_triangle_le)

lemma bounded_iff: "bounded S \ (\a. \x\S. norm x \ a)"
  unfolding bounded_any_center [where a=0]
  by (simp add: dist_norm)

lemma bdd_above_norm: "bdd_above (norm ` X) \ bounded X"
  by (simp add: bounded_iff bdd_above_def)

lemma bounded_norm_comp: "bounded ((\x. norm (f x)) ` S) = bounded (f ` S)"
  by (simp add: bounded_iff)

lemma boundedI:
  assumes "\x. x \ S \ norm x \ B"
  shows "bounded S"
  using assms bounded_iff by blast

lemma bounded_empty [simp]: "bounded {}"
  by (simp add: bounded_def)

lemma bounded_subset: "bounded T \ S \ T \ bounded S"
  by (metis bounded_def subset_eq)

lemma bounded_interior[intro]: "bounded S \ bounded(interior S)"
  by (metis bounded_subset interior_subset)

lemma bounded_closure[intro]:
  assumes "bounded S"
  shows "bounded (closure S)"
proof -
  from assms obtain x and a where a: "\y\S. dist x y \ a"
    unfolding bounded_def by auto
  { fix y
    assume "y \ closure S"
    then obtain f where f: "\n. f n \ S" "(f \ y) sequentially"
      unfolding closure_sequential by auto
    have "\n. f n \ S \ dist x (f n) \ a" using a by simp
    then have "eventually (\n. dist x (f n) \ a) sequentially"
      by (simp add: f(1))
    then have "dist x y \ a"
      using Lim_dist_ubound f(2) trivial_limit_sequentially by blast
  }
  then show ?thesis
    unfolding bounded_def by auto
qed

lemma bounded_closure_image: "bounded (f ` closure S) \ bounded (f ` S)"
  by (simp add: bounded_subset closure_subset image_mono)

lemma bounded_cball[simp,intro]: "bounded (cball x \)"
  unfolding bounded_def  using mem_cball by blast

lemma bounded_ball[simp,intro]: "bounded (ball x \)"
  by (metis ball_subset_cball bounded_cball bounded_subset)

lemma bounded_Un[simp]: "bounded (S \ T) \ bounded S \ bounded T"
  unfolding bounded_def
  by (metis Un_iff bounded_any_center order.trans linorder_linear)

lemma bounded_Union[intro]: "finite F \ \S\F. bounded S \ bounded (\F)"
  by (induct rule: finite_induct[of F]) auto

lemma bounded_UN [intro]: "finite A \ \x\A. bounded (B x) \ bounded (\x\A. B x)"
  by auto

lemma bounded_insert [simp]: "bounded (insert x S) \ bounded S"
  by (metis bounded_Un bounded_cball cball_trivial insert_is_Un)

lemma bounded_subset_ballI: "S \ ball x r \ bounded S"
  by (meson bounded_ball bounded_subset)

lemma bounded_subset_ballD:
  assumes "bounded S" shows "\r. 0 < r \ S \ ball x r"
proof -
  obtain \<epsilon>::real and y where "S \<subseteq> cball y \<epsilon>" "0 \<le> \<epsilon>"
    using assms by (auto simp: bounded_subset_cball)
  then show ?thesis
    by (intro exI[where x="dist x y + \ + 1"]) metric
qed

lemma finite_imp_bounded [intro]: "finite S \ bounded S"
  by (induct set: finite) simp_all

lemma bounded_Int[intro]: "bounded S \ bounded T \ bounded (S \ T)"
  by (metis Int_lower1 Int_lower2 bounded_subset)

lemma bounded_diff[intro]: "bounded S \ bounded (S - T)"
  by (metis Diff_subset bounded_subset)

lemma bounded_dist_comp:
  assumes "bounded (f ` S)" "bounded (g ` S)"
  shows "bounded ((\x. dist (f x) (g x)) ` S)"
proof -
  from assms obtain M1 M2 where *: "dist (f x) undefined \ M1" "dist undefined (g x) \ M2" if "x \ S" for x
    by (auto simp: bounded_any_center[of _ undefined] dist_commute)
  have "dist (f x) (g x) \ M1 + M2" if "x \ S" for x
    using *[OF that]
    by metric
  then show ?thesis
    by (auto intro!: boundedI)
qed

lemma bounded_Times:
  assumes "bounded S" "bounded T"
  shows "bounded (S \ T)"
proof -
  obtain x y a b where "\z\S. dist x z \ a" "\z\T. dist y z \ b"
    using assms [unfolded bounded_def] by auto
  then have "\z\S \ T. dist (x, y) z \ sqrt (a\<^sup>2 + b\<^sup>2)"
    by (auto simp: dist_Pair_Pair real_sqrt_le_mono add_mono power_mono)
  then show ?thesis unfolding bounded_any_center [where a="(x, y)"] by auto
qed

section \<open>Compactness\<close>

lemma compact_imp_bounded:
  assumes "compact U"
  shows "bounded U"
proof -
  have "compact U" "\x\U. open (ball x 1)" "U \ (\x\U. ball x 1)"
    using assms by auto
  then obtain D where D: "D \ U" "finite D" "U \ (\x\D. ball x 1)"
    by (metis compactE_image)
  from \<open>finite D\<close> have "bounded (\<Union>x\<in>D. ball x 1)"
    by (simp add: bounded_UN)
  then show "bounded U" using \<open>U \<subseteq> (\<Union>x\<in>D. ball x 1)\<close>
    by (rule bounded_subset)
qed

lemma continuous_on_compact_bound:
  assumes "compact A" "continuous_on A f"
  obtains B where "B \ 0" "\x. x \ A \ norm (f x) \ B"
proof -
  have "compact (f ` A)" by (metis assms compact_continuous_image)
  then obtain B where "\x\A. norm (f x) \ B"
    by (auto dest!: compact_imp_bounded simp: bounded_iff)
  hence "max B 0 \ 0" and "\x\A. norm (f x) \ max B 0" by auto
  thus ?thesis using that by blast
qed

lemma closure_Int_ball_not_empty:
  assumes "S \ closure T" "x \ S" "r > 0"
  shows "T \ ball x r \ {}"
  using assms centre_in_ball closure_iff_nhds_not_empty by blast

lemma compact_sup_maxdistance:
  fixes S :: "'a::metric_space set"
  assumes "compact S"
    and "S \ {}"
  shows "\x\S. \y\S. \u\S. \v\S. dist u v \ dist x y"
proof -
  have "compact (S \ S)"
    using \<open>compact S\<close> by (intro compact_Times)
  moreover have "S \ S \ {}"
    using \<open>S \<noteq> {}\<close> by auto
  moreover have "continuous_on (S \ S) (\x. dist (fst x) (snd x))"
    by (intro continuous_at_imp_continuous_on ballI continuous_intros)
  ultimately show ?thesis
    using continuous_attains_sup[of "S \ S" "\x. dist (fst x) (snd x)"] by auto
qed

text \<open>
  If \<open>A\<close> is a compact subset of an open set \<open>B\<close> in a metric space, then there exists an \<open>\<epsilon> > 0\<close>
  such that the Minkowski sum of \<open>A\<close> with an open ball of radius \<open>\<epsilon>\<close> is also a subset of \<open>B\<close>.
\<close>
lemma compact_subset_open_imp_ball_epsilon_subset:
  assumes "compact A" "open B" "A \ B"
  obtains \<epsilon> where "\<epsilon> > 0"  "(\<Union>x\<in>A. ball x \<epsilon>) \<subseteq> B"
proof -
  have "\x\A. \\. \ > 0 \ ball x \ \ B"
    using assms unfolding open_contains_ball by blast
  then obtain \<epsilon> where \<epsilon>: "\<And>x. x \<in> A \<Longrightarrow> \<epsilon> x > 0" "\<And>x. x \<in> A \<Longrightarrow> ball x (\<epsilon> x) \<subseteq> B"
    by metis
  define C where "C = \ ` A"
  obtain X where X: "X \ A" "finite X" "A \ (\c\X. ball c (\ c / 2))"
    using \<open>compact A\<close>
  proof (rule compactE_image)
    show "open (ball x (\ x / 2))" if "x \ A" for x
      by simp
    show "A \ (\c\A. ball c (\ c / 2))"
      using \<epsilon> by auto
  qed auto

  define e' where "e' = Min (insert 1 ((\<lambda>x. \<epsilon> x / 2) ` X))"
  have "e' > 0"
    unfolding e'_def using \ X by (subst Min_gr_iff) auto
  have e': "e' \<le> \<epsilon> x / 2" if "x \<in> X" for x
    using that X unfolding e'_def by (intro Min.coboundedI) auto

  show ?thesis
  proof
    show "e' > 0"
      by fact
  next
    show "(\x\A. ball x e') \ B"
    proof clarify
      fix x y assume xy: "x \ A" "y \ ball x e'"
      from xy(1) X obtain z where z: "z \ X" "x \ ball z (\ z / 2)"
        by auto
      have "dist y z \ dist x y + dist z x"
        by (metis dist_commute dist_triangle)
      also have "dist z x < \ z / 2"
        using xy z by auto
      also have "dist x y < e'"
        using xy by auto
      also have "\ \ \ z / 2"
        using z by (intro e') auto
      finally have "y \ ball z (\ z)"
        by (simp add: dist_commute)
      also have "\ \ B"
        using z X by (intro \<epsilon>) auto
      finally show "y \ B" .
    qed
  qed
qed

lemma compact_subset_open_imp_cball_epsilon_subset:
  assumes "compact A" "open B" "A \ B"
  obtains \<epsilon> where "\<epsilon> > 0"  "(\<Union>x\<in>A. cball x \<epsilon>) \<subseteq> B"
proof -
  obtain \<epsilon> where "\<epsilon> > 0" and \<epsilon>: "(\<Union>x\<in>A. ball x \<epsilon>) \<subseteq> B"
    using compact_subset_open_imp_ball_epsilon_subset [OF assms] by blast
  then have "(\x\A. cball x (\ / 2)) \ (\x\A. ball x \)"
    by auto
  with \<open>0 < \<epsilon>\<close> that show ?thesis
    by (metis \<epsilon> half_gt_zero_iff order_trans)
qed

subsubsection\<open>Totally bounded\<close>

proposition seq_compact_imp_totally_bounded:
  assumes "seq_compact S"
  shows "\\>0. \k. finite k \ k \ S \ S \ (\x\k. ball x \)"
proof -
  { fix \<epsilon>::real assume "\<epsilon> > 0" assume *: "\<And>k. finite k \<Longrightarrow> k \<subseteq> S \<Longrightarrow> \<not> S \<subseteq> (\<Union>x\<in>k. ball x \<epsilon>)"
    let ?Q = "\x n r. r \ S \ (\m < (n::nat). \ (dist (x m) r < \))"
    have "\x. \n::nat. ?Q x n (x n)"
    proof (rule dependent_wellorder_choice)
      fix n x assume "\y. y < n \ ?Q x y (x y)"
      then have "\ S \ (\x\x ` {0..)"
        using *[of "x ` {0 ..< n}"] by (auto simp: subset_eq)
      then obtain z where z:"z\S" "z \ (\x\x ` {0..)"
        unfolding subset_eq by auto
      show "\r. ?Q x n r"
        using z by auto
    qed simp
    then obtain x where "\n::nat. x n \ S" and x:"\n m. m < n \ \ (dist (x m) (x n) < \)"
      by blast
    then obtain l r where "l \ S" and r:"strict_mono r" and "(x \ r) \ l"
      using assms by (metis seq_compact_def)
    then have "Cauchy (x \ r)"
      using LIMSEQ_imp_Cauchy by auto
    then obtain N::nat where "\m n. N \ m \ N \ n \ dist ((x \ r) m) ((x \ r) n) < \"
      unfolding Cauchy_def using \<open>\<epsilon> > 0\<close> by blast
    then have False
      using x[of "r N" "r (N+1)"] r by (auto simp: strict_mono_def) }
  then show ?thesis
    by metis
qed

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

proposition seq_compact_imp_Heine_Borel:
  fixes S :: "'a :: metric_space set"
  assumes "seq_compact S"
  shows "compact S"
proof -
  obtain f where f: "\\>0. finite (f \) \ f \ \ S \ S \ (\x\f \. ball x \)"
    by (metis assms seq_compact_imp_totally_bounded)
  define K where "K = (\(x, r). ball x r) ` ((\\ \ \ \ {0 <..}. f \) \ \)"
  have "countably_compact S"
    using \<open>seq_compact S\<close> by (rule seq_compact_imp_countably_compact)
  then show "compact S"
  proof (rule countably_compact_imp_compact)
    show "countable K"
      unfolding K_def using f
      by (meson countable_Int1 countable_SIGMA countable_UN countable_finite
          countable_image countable_rat greaterThan_iff inf_le2 subset_iff)
    show "\b\K. open b" by (auto simp: K_def)
  next
    fix T x
    assume T: "open T" "x \ T" and x: "x \ S"
    from openE[OF T] obtain \<epsilon> where "0 < \<epsilon>" "ball x \<epsilon> \<subseteq> T"
      by auto
    then have "0 < \/2" "ball x (\/2) \ T"
      by auto
    from Rats_dense_in_real[OF \<open>0 < \<epsilon>/2\<close>] obtain r where "r \<in> \<rat>" "0 < r" "r < \<epsilon>/2"
      by auto
    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"
      by auto
    from \<open>r \<in> \<rat>\<close> \<open>0 < r\<close> \<open>k \<in> f r\<close> have "ball k r \<in> K"
      by (auto simp: K_def)
    then show "\b\K. x \ b \ b \ S \ T"
    proof (rule rev_bexI, intro conjI subsetI)
      fix y
      assume "y \ ball k r \ S"
      with \<open>r < \<epsilon>/2\<close> \<open>x \<in> ball k r\<close> have "dist x y < \<epsilon>"
        by (intro dist_triangle_half_r [of k _ \<epsilon>]) (auto simp: dist_commute)
      with \<open>ball x \<epsilon> \<subseteq> T\<close> show "y \<in> T"
        by auto
    next
      show "x \ ball k r" by fact
    qed
  qed
qed

proposition compact_eq_seq_compact_metric:
  "compact (S :: 'a::metric_space set) \ seq_compact S"
  using compact_imp_seq_compact seq_compact_imp_Heine_Borel by blast

proposition compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close>
  "compact (S :: 'a::metric_space set) \
   (\<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))"
  unfolding compact_eq_seq_compact_metric seq_compact_def by auto

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

proposition compact_eq_Bolzano_Weierstrass:
  fixes S :: "'a::metric_space set"
  shows "compact S \ (\T. infinite T \ T \ S \ (\x \ S. x islimpt T))"
  by (meson Bolzano_Weierstrass_imp_seq_compact Heine_Borel_imp_Bolzano_Weierstrass seq_compact_imp_Heine_Borel)

proposition Bolzano_Weierstrass_imp_bounded:
  "(\T. \infinite T; T \ S\ \ (\x \ S. x islimpt T)) \ bounded S"
  using compact_imp_bounded unfolding compact_eq_Bolzano_Weierstrass by metis

section \<open>Banach fixed point theorem\<close>

theorem Banach_fix:
  assumes S: "complete S" "S \ {}"
    and c: "0 \ c" "c < 1"
    and f: "f ` S \ S"
    and lipschitz: "\x y. \x\S; y\S\ \ dist (f x) (f y) \ c * dist x y"
  shows "\!x\S. f x = x"
proof -
  from S obtain z0 where z0: "z0 \ S" by blast
  define z where "z n = (f ^^ n) z0" for n
  with f z0 have z_in_s: "z n \ S" for n :: nat
    by (induct n) auto
  define \<delta> where "\<delta> = dist (z 0) (z 1)"

  have fzn: "f (z n) = z (Suc n)" for n
    by (simp add: z_def)
  have cf_z: "dist (z n) (z (Suc n)) \ (c ^ n) * \" for n :: nat
  proof (induct n)
    case 0
    then show ?case
      by (simp add: \<delta>_def)
  next
    case (Suc m)
    with \<open>0 \<le> c\<close> have "c * dist (z m) (z (Suc m)) \<le> c ^ Suc m * \<delta>"
      using mult_left_mono[of "dist (z m) (z (Suc m))" "c ^ m * \" c] by simp
    then show ?case
      by (metis fzn lipschitz order_trans z_in_s)
  qed

  have cf_z2: "(1 - c) * dist (z m) (z (m + n)) \ (c ^ m) * \ * (1 - c ^ n)" for n m :: nat
  proof (induct n)
    case 0
    show ?case by simp
  next
    case (Suc k)
    from c have "(1 - c) * dist (z m) (z (m + Suc k)) \
        (1 - c) * (dist (z m) (z (m + k)) + dist (z (m + k)) (z (Suc (m + k))))"
      by (simp add: dist_triangle)
    also from c cf_z[of "m + k"] have "\ \ (1 - c) * (dist (z m) (z (m + k)) + c ^ (m + k) * \)"
      by simp
    also from Suc have "\ \ c ^ m * \ * (1 - c ^ k) + (1 - c) * c ^ (m + k) * \"
      by (simp add: field_simps)
    also have "\ = (c ^ m) * (\ * (1 - c ^ k) + (1 - c) * c ^ k * \)"
      by (simp add: power_add field_simps)
    also from c have "\ \ (c ^ m) * \ * (1 - c ^ Suc k)"
      by (simp add: field_simps)
    finally show ?case .
  qed

  have "\N. \m n. N \ m \ N \ n \ dist (z m) (z n) < \" if "\ > 0" for \
  proof (cases "\ = 0")
    case True
    have "(1 - c) * x \ 0 \ x \ 0" for x
      using c mult_le_0_iff nle_le by fastforce
    with c cf_z2[of 0] True have "z n = z0" for n
      by (simp add: z_def)
    with \<open>\<epsilon> > 0\<close> show ?thesis by simp
  next
    case False
    with zero_le_dist[of "z 0" "z 1"] have "\ > 0"
      by (metis \<delta>_def less_le)
    with c \<open>\<epsilon> > 0\<close> have "0 < \<epsilon> * (1 - c) / \<delta>"
      by simp
    with c obtain N where N: "c ^ N < \ * (1 - c) / \"
      using real_arch_pow_inv[of "\ * (1 - c) / \" c] by auto
    have *: "dist (z m) (z n) < \" if "m > n" and as: "m \ N" "n \ N" for m n :: nat
    proof -
      have *: "c ^ n \ c ^ N"
        using power_decreasing[OF \<open>n\<ge>N\<close>, of c] c by simp
      have "1 - c ^ (m - n) > 0"
        using power_strict_mono[of c 1 "m - n"] c \<open>m > n\<close> by simp
      with \<open>\<delta> > 0\<close> c have **: "\<delta> * (1 - c ^ (m - n)) / (1 - c) > 0"
        by simp
      from cf_z2[of n "m - n"] \<open>m > n\<close>
      have "dist (z m) (z n) \ c ^ n * \ * (1 - c ^ (m - n)) / (1 - c)"
        by (simp add: pos_le_divide_eq c mult.commute dist_commute)
      also have "\ \ c ^ N * \ * (1 - c ^ (m - n)) / (1 - c)"
        using mult_right_mono[OF * order_less_imp_le[OF **]]
        by (simp add: mult.assoc)
      also have "\ < (\ * (1 - c) / \) * \ * (1 - c ^ (m - n)) / (1 - c)"
        using mult_strict_right_mono[OF N **] by (auto simp: mult.assoc)
      also from c \<open>1 - c ^ (m - n) > 0\<close> \<open>\<epsilon> > 0\<close> have "\<dots> \<le> \<epsilon>"
        using mult_right_le_one_le[of \<epsilon> "1 - c ^ (m - n)"] by auto
      finally show ?thesis .
    qed
    have "dist (z n) (z m) < \" if "N \ m" "N \ n" for m n :: nat
      using *[of n m] *[of m n]
      using \<open>0 < \<epsilon>\<close> dist_commute_lessI that by fastforce
    then show ?thesis by auto
  qed
  then have "Cauchy z"
    by (metis metric_CauchyI)
  then obtain x where "x\S" and x:"(z \ x) sequentially"
    using \<open>complete S\<close> complete_def z_in_s by blast

  define \<epsilon> where "\<epsilon> = dist (f x) x"
  have "\ = 0"
  proof (rule ccontr)
    assume "\ \ 0"
    then have "\ > 0"
      unfolding \<epsilon>_def using zero_le_dist[of "f x" x]
      by (metis dist_eq_0_iff dist_nz \<epsilon>_def)
    then obtain N where N:"\n\N. dist (z n) x < \/2"
      using x[unfolded lim_sequentially, THEN spec[where x="\/2"]] by auto
    then have N':"dist (z N) x < \/2" by auto
    have *: "c * dist (z N) x \ dist (z N) x"
      unfolding mult_le_cancel_right2
      using zero_le_dist[of "z N" x] and c
      by (metis dist_eq_0_iff dist_nz order_less_asym less_le)
    have "dist (f (z N)) (f x) \ c * dist (z N) x"
      by (simp add: \<open>x \<in> S\<close> lipschitz z_in_s)
    also have "\ < \/2"
      using N' and c using * by auto
    finally show False
      unfolding fzn
      by (metis N \<epsilon>_def dist_commute dist_triangle_half_l le_eq_less_or_eq lessI
          order_less_irrefl)
  qed
  then have "f x = x" by (auto simp: \<epsilon>_def)
  moreover have "y = x" if "f y = y" "y \ S" for y
  proof -
    from \<open>x \<in> S\<close> \<open>f x = x\<close> that have "dist x y \<le> c * dist x y"
      using lipschitz by fastforce
    with c and zero_le_dist[of x y] have "dist x y = 0"
      by (simp add: mult_le_cancel_right1)
    then show ?thesis by simp
  qed
  ultimately show ?thesis
    using \<open>x\<in>S\<close> by blast
qed

section \<open>Edelstein fixed point theorem\<close>

theorem Edelstein_fix:
  fixes S :: "'a::metric_space set"
  assumes S: "compact S" "S \ {}"
    and gs: "(g ` S) \ S"
    and dist: "\x y. \x\S; y\S\ \ x \ y \ dist (g x) (g y) < dist x y"
  shows "\!x\S. g x = x"
proof -
  let ?D = "(\x. (x, x)) ` S"
  have D: "compact ?D" "?D \ {}"
    by (rule compact_continuous_image)
       (auto intro!: S continuous_Pair continuous_ident simp: continuous_on_eq_continuous_within)

  have "\x y \. x \ S \ y \ S \ 0 < \ \ dist y x < \ \ dist (g y) (g x) < \"
    using dist by fastforce
  then have "continuous_on S g"
    by (auto simp: continuous_on_iff)
  then have cont: "continuous_on ?D (\x. dist ((g \ fst) x) (snd x))"
    unfolding continuous_on_eq_continuous_within
    by (intro continuous_dist ballI continuous_within_compose)
       (auto intro!: continuous_fst continuous_snd continuous_ident simp: image_image)

  obtain a where "a \ S" and le: "\x. x \ S \ dist (g a) a \ dist (g x) x"
    using continuous_attains_inf[OF D cont] by auto

  have "g a = a"
    by (metis \<open>a \<in> S\<close> dist gs image_subset_iff le order.strict_iff_not)
  moreover have "\x. x \ S \ g x = x \ x = a"
    using \<open>a \<in> S\<close> calculation dist by fastforce
  ultimately show "\!x\S. g x = x"
    using \<open>a \<in> S\<close> by blast
qed

section \<open>The diameter of a set\<close>

definition\<^marker>\<open>tag important\<close> diameter :: "'a::metric_space set \<Rightarrow> real" where
  "diameter S = (if S = {} then 0 else SUP (x,y)\S\S. dist x y)"

lemma diameter_empty [simp]: "diameter{} = 0"
  by (auto simp: diameter_def)

lemma diameter_singleton [simp]: "diameter{x} = 0"
  by (auto simp: diameter_def)

lemma diameter_le:
  assumes "S \ {} \ 0 \ \"
    and no: "\x y. \x \ S; y \ S\ \ norm(x - y) \ \"
  shows "diameter S \ \"
  using assms
  by (auto simp: dist_norm diameter_def intro: cSUP_least)

lemma diameter_bounded_bound:
  fixes S :: "'a :: metric_space set"
  assumes S: "bounded S" "x \ S" "y \ S"
  shows "dist x y \ diameter S"
proof -
  from S obtain z \<delta> where z: "\<And>x. x \<in> S \<Longrightarrow> dist z x \<le> \<delta>"
    unfolding bounded_def by auto
  have "bdd_above (case_prod dist ` (S\S))"
  proof (intro bdd_aboveI, safe)
    fix a b
    assume "a \ S" "b \ S"
    with z[of a] z[of b] dist_triangle[of a b z]
    show "dist a b \ 2 * \"
      by (simp add: dist_commute)
  qed
  moreover have "(x,y) \ S\S" using S by auto
  ultimately have "dist x y \ (SUP (x,y)\S\S. dist x y)"
    by (rule cSUP_upper2) simp
  with \<open>x \<in> S\<close> show ?thesis
    by (auto simp: diameter_def)
qed

lemma diameter_lower_bounded:
  fixes S :: "'a :: metric_space set"
  assumes S: "bounded S"
    and \<delta>: "0 < \<delta>" "\<delta> < diameter S"
  shows "\x\S. \y\S. \ < dist x y"
proof (rule ccontr)
  assume contr: "\ ?thesis"
  moreover have "S \ {}"
    using \<delta> by (auto simp: diameter_def)
  ultimately have "diameter S \ \"
    by (auto simp: not_less diameter_def intro!: cSUP_least)
  with \<open>\<delta> < diameter S\<close> show False by auto
qed

lemma diameter_bounded:
  assumes "bounded S"
  shows "\x\S. \y\S. dist x y \ diameter S"
    and "\\>0. \ < diameter S \ (\x\S. \y\S. dist x y > \)"
  using diameter_bounded_bound[of S] diameter_lower_bounded[of S] assms
  by auto

lemma bounded_two_points: "bounded S \ (\\. \x\S. \y\S. dist x y \ \)"
  by (meson bounded_def diameter_bounded(1))

lemma diameter_compact_attained:
  assumes "compact S"
    and "S \ {}"
  shows "\x\S. \y\S. dist x y = diameter S"
proof -
  have b: "bounded S" using assms(1)
    by (rule compact_imp_bounded)
  then obtain x y where xys: "x\S" "y\S"
    and xy: "\u\S. \v\S. dist u v \ dist x y"
    using compact_sup_maxdistance[OF assms] by auto
  then have "diameter S \ dist x y"
    unfolding diameter_def by (force intro!: cSUP_least)
  then show ?thesis
    by (metis b diameter_bounded_bound order_antisym xys)
qed

lemma diameter_ge_0:
  assumes "bounded S"  shows "0 \ diameter S"
  by (metis assms diameter_bounded(1) diameter_empty dist_self equals0I order.refl)

lemma diameter_subset:
  assumes "S \ T" "bounded T"
  shows "diameter S \ diameter T"
proof (cases "S = {} \ T = {}")
  case True
  with assms show ?thesis
    by (force simp: diameter_ge_0)
next
  case False
  then have "bdd_above ((\x. case x of (x, xa) \ dist x xa) ` (T \ T))"
    using \<open>bounded T\<close> diameter_bounded_bound by (force simp: bdd_above_def)
  with False \<open>S \<subseteq> T\<close> show ?thesis
    by (simp add: diameter_def cSUP_subset_mono times_subset_iff)
qed

lemma diameter_closure:
  assumes "bounded S"
  shows "diameter(closure S) = diameter S"
proof (rule order_antisym)
  have False if d_less_d: "diameter S < diameter (closure S)"
  proof -
    define \<delta> where "\<delta> = diameter(closure S) - diameter(S)"
    have "\ > 0"
      using that by (simp add: \<delta>_def)
    then have dle: "diameter(closure(S)) - \ / 2 < diameter(closure(S))"
      by simp
    have dd: "diameter (closure S) - \ / 2 = (diameter(closure(S)) + diameter(S)) / 2"
      by (simp add: \<delta>_def field_split_simps)
     have bocl: "bounded (closure S)"
      using assms by blast
    moreover
    have "diameter S \ 0"
      using diameter_bounded_bound [OF assms]
      by (metis closure_closed discrete_imp_closed dist_le_zero_iff not_less_iff_gr_or_eq
          that)
    then have "0 < diameter S"
      using assms diameter_ge_0 by fastforce
    ultimately obtain x y where "x \ closure S" "y \ closure S" and xy: "diameter(closure(S)) - \ / 2 < dist x y"
      using diameter_lower_bounded [OF bocl, of "diameter S"]
      by (metis d_less_d diameter_bounded(2) dist_not_less_zero dist_self dle
          not_less_iff_gr_or_eq)
    then obtain x' y' where x'y': "x' \ S" "dist x' x < \/4" "y' \ S" "dist y' y < \/4"
      by (metis \<open>0 < \<delta>\<close> zero_less_divide_iff zero_less_numeral closure_approachable)
    then have "dist x' y' \ diameter S"
      using assms diameter_bounded_bound by blast
    with x'y' have "dist x y \ \ / 4 + diameter S + \ / 4"
      by (meson add_mono dist_triangle dist_triangle3 less_eq_real_def order_trans)
    then show ?thesis
      using xy \<delta>_def by linarith
  qed
  then show "diameter (closure S) \ diameter S"
    by fastforce
  next
    show "diameter S \ diameter (closure S)"
      by (simp add: assms bounded_closure closure_subset diameter_subset)
qed

proposition Lebesgue_number_lemma:
  assumes "compact S" "\ \ {}" "S \ \\" and ope: "\B. B \ \ \ open B"
  obtains \<delta> where "0 < \<delta>" "\<And>T. \<lbrakk>T \<subseteq> S; diameter T < \<delta>\<rbrakk> \<Longrightarrow> \<exists>B \<in> \<C>. T \<subseteq> B"
proof (cases "S = {}")
  case True
  then show ?thesis
    by (metis \<open>\<C> \<noteq> {}\<close> zero_less_one empty_subsetI equals0I subset_trans that)
next
  case False
  have "\r C. r > 0 \ ball x (2*r) \ C \ C \ \" if "x \ S" for x
    by (metis \<open>S \<subseteq> \<Union>\<C>\<close> field_sum_of_halves half_gt_zero mult.commute mult_2_right
        UnionE ope open_contains_ball subset_eq that)
  then obtain r where r: "\x. x \ S \ r x > 0 \ (\C \ \. ball x (2*r x) \ C)"
    by metis
  then have "S \ (\x \ S. ball x (r x))"
    by auto
  then obtain \<T> where "finite \<T>" "S \<subseteq> \<Union>\<T>" and \<T>: "\<T> \<subseteq> (\<lambda>x. ball x (r x)) ` S"
    by (rule compactE [OF \<open>compact S\<close>]) auto
  then obtain S0 where "S0 \ S" "finite S0" and S0: "\ = (\x. ball x (r x)) ` S0"
    by (meson finite_subset_image)
  then have "S0 \ {}"
    using False \<open>S \<subseteq> \<Union>\<T>\<close> by auto
  define \<delta> where "\<delta> = Inf (r ` S0)"
  have "\ > 0"
    using \<open>finite S0\<close> \<open>S0 \<subseteq> S\<close> \<open>S0 \<noteq> {}\<close> r by (auto simp: \<delta>_def finite_less_Inf_iff)
  show ?thesis
  proof
    show "0 < \"
      by (simp add: \<open>0 < \<delta>\<close>)
    show "\B \ \. T \ B" if "T \ S" and dia: "diameter T < \" for T
    proof (cases "T = {}")
      case False
      then obtain y where "y \ T" by blast
      then have "y \ S"
        using \<open>T \<subseteq> S\<close> by auto
      then obtain x where "x \ S0" and x: "y \ ball x (r x)"
        using \<open>S \<subseteq> \<Union>\<T>\<close> S0 that by blast
      have "ball y \ \ ball y (r x)"
        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)
      also have "\ \ ball x (2*r x)"
        using x by metric
      finally obtain C where "C \ \" "ball y \ \ C"
        by (meson r \<open>S0 \<subseteq> S\<close> \<open>x \<in> S0\<close> dual_order.trans subsetCE)
      have "bounded T"
        using \<open>compact S\<close> bounded_subset compact_imp_bounded \<open>T \<subseteq> S\<close> by blast
      then have "T \ ball y \"
        using \<open>y \<in> T\<close> dia diameter_bounded_bound by fastforce
      then show ?thesis
        by (meson \<open>C \<in> \<C>\<close> \<open>ball y \<delta> \<subseteq> C\<close> subset_eq)
    qed (use \<open>\<C> \<noteq> {}\<close> in auto)
  qed
qed

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

text \<open>
  A metric space (or topological vector space) is said to have the
  Heine-Borel property if every closed and bounded subset is compact.
\<close>

class heine_borel = metric_space +
--> --------------------

--> maximum size reached

--> --------------------

quality97%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.10Bemerkung: (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.