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 ‹Elementary Metric Spaces›

theory Elementary_Metric_Spaces
  imports
    Abstract_Topology_2
    Metric_Arith
begin

section ‹Open and closed balls›

definition🍋‹tag important› ball :: "'a::metric_space \ real \ 'a set"
  where "ball x \ = {y. dist x y < \}"

definition🍋‹tag important› cball :: "'a::metric_space \ real \ 'a set"
  where "cball x \ = {y. dist x y \ \}"

definition🍋‹tag important› sphere :: "'a::metric_space \ real \ '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 ε where "\>0" "ball x \ \ 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 _ δ]) (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 _ δ]) (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 ‹As above, but scaled by a complex number›
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 ε :: real
    assume ε: "\ > 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 ε 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 ‹Limit Points›

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 ‹Perfect Metric Spaces›

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 ε]
  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 ‹Finite and discrete›

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 ε where "\ = max e0 (2 * dist a x)"
  have "\>0" unfolding ε_def using ‹e0>0› by auto
  moreover have "insert x S \ ball a \"
    using e0 ‹ε>0› unfolding ε_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 δ where "\ > 0" and δ: "\x\S. x \ a \ \ \ 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 ε: "0 < \"
    and δ: "\x \ S. \y \ S. dist y x < \ \ 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 ε half_gt_zero)
    then have mp: "min (\/2) (dist x y) > 0"
      by (simp add: dist_commute)
    from δ 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 ε: "0 < \"
    and δ: "\x y. x \ S \ y \ S \ dist y x < \ \ y = x"
  shows "\ x islimpt S"
  by (metis closed_limpt δ discrete_imp_closed ε islimpt_approachable)
  

section ‹Interior›

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 ‹Frontier›

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 ‹Limits›

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 ‹Show that they yield usual definitions in the various cases.›

proposition Lim_within_le: "(f \ l)(at a within S) \
    (∀ε>0. ∃δ>0. ∀x∈S. 0 < dist x a ∧ dist x a ≤ δ ⟶ dist (f x) l < ε)"
  by (auto simp: tendsto_iff eventually_at_le)

proposition Lim_within: "(f \ l) (at a within S) \
    (∀ε >0. ∃δ>0. ∀x ∈ S. 0 < dist x a ∧ dist x a  < δ ⟶ dist (f x) l < ε)"
  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) \
    (∀ε >0. ∃δ>0. ∀x. 0 < dist x a ∧ dist x a < δ  ⟶ dist (f x) l < ε)"
  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)\
         ==> (f ---> l) (at a within T)"
  by (simp add: eventually_at Lim_within) (smt (verit, best))

text ‹Another limit point characterization.›

lemma limpt_sequential_inj:
  fixes x :: "'a::metric_space"
  shows "x islimpt S \
         (∃f. (∀n::nat. f n ∈ S - {x}) ∧ inj f ∧ (f ---> 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 ‹Continuity›

text‹Derive the epsilon-delta forms, which we often use as "definitions"›

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‹Versions in terms of open balls.›

lemma continuous_within_ball:
  "continuous (at x within S) f \
    (∀ε > 0. ∃δ > 0. f ` (ball x δ ∩ S) ⊆ ball (f x) ε)"
  (is "?lhs = ?rhs")
proof
  assume ?lhs
  {
    fix ε :: real
    assume "\ > 0"
    then obtain δ where "\>0" and δ: "\y\S. 0 < dist y x \ dist y x < \ \ dist (f y) (f x) < \"
      using ‹?lhs›[unfolded continuous_within Lim_within] by auto
    have "y \ ball (f x) \" if "y \ f ` (ball x \ \ S)" for y
        using that δ ‹ε > 0› by (auto simp: dist_commute)
    then have "\\>0. f ` (ball x \ \ S) \ ball (f x) \"
      using ‹δ > 0› 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‹Define setwise continuity in terms of limits within the set.›

lemma continuous_on_iff:
  "continuous_on s f \
    (∀x∈s. ∀ε>0. ∃δ>0. ∀x'\s. dist x' x < δ ⟶ dist (f x') (f x) < \)"
  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 δ where "\>0"  "\x'. \x'\ S; dist x' x \ \\ \ dist (f x') (f x) < \"
  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‹Some simple consequential lemmas.›

lemma continuous_onE:
    assumes "continuous_on s f" "x\s" "\>0"
    obtains δ where "\>0"  "\x'. \x' \ s; dist x' x \ \\ \ dist (f x') (f x) < \"
  using assms
  unfolding continuous_on_iff by (metis dense order_le_less_trans)

text‹The usual transformation theorems.›

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 ‹Closure and Limit Characterization›

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 ε :: 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 ε :: 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 ε :: real
      assume "\ > 0"
      then obtain y where "y \ S - {x}" and "dist y x < \"
        using ‹?lhs› 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 ε :: real
      assume "\ > 0"
      then obtain y where "y \ S \ ball x \ - {x}"
        using ‹?rhs› 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 ‹Boundedness›

  (* FIXME: This has to be unified with BSEQ!! *)
definition🍋‹tag important› (in metric_space) bounded :: "'a set \ 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 ε::real and y where "S \ cball y \" "0 \ \"
    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 ‹Compactness›

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 ‹finite D› have "bounded (\x\D. ball x 1)"
    by (simp add: bounded_UN)
  then show "bounded U" using ‹U ⊆ (∪x∈D. ball x 1)›
    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 ‹compact S› by (intro compact_Times)
  moreover have "S \ S \ {}"
    using ‹S ≠ {}› 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 ‹
  If ‹A› is a compact subset of an open set ‹B› in a metric space, then there exists an ‹ε > 0›
  such that the Minkowski sum of ‹A› with an open ball of radius ‹ε› is also a subset of ‹B›.
›
lemma compact_subset_open_imp_ball_epsilon_subset:
  assumes "compact A" "open B" "A \ B"
  obtains ε where "\ > 0"  "(\x\A. ball x \) \ B"
proof -
  have "\x\A. \\. \ > 0 \ ball x \ \ B"
    using assms unfolding open_contains_ball by blast
  then obtain ε where ε: "\x. x \ A \ \ x > 0" "\x. x \ A \ ball x (\ x) \ B"
    by metis
  define C where "C = \ ` A"
  obtain X where X: "X \ A" "finite X" "A \ (\c\X. ball c (\ c / 2))"
    using ‹compact A›
  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 ε by auto
  qed auto

  define e' where "e' = Min (insert 1 ((λx. ε x / 2) ` X))"
  have "e' > 0"
    unfolding e'_def using \ X by (subst Min_gr_iff) auto
  have e': "e' ≤ ε x / 2" if "x ∈ 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 ε) auto
      finally show "y \ B" .
    qed
  qed
qed

lemma compact_subset_open_imp_cball_epsilon_subset:
  assumes "compact A" "open B" "A \ B"
  obtains ε where "\ > 0"  "(\x\A. cball x \) \ B"
proof -
  obtain ε where "\ > 0" and ε: "(\x\A. ball x \) \ 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 ‹0 < ε› that show ?thesis
    by (metis ε half_gt_zero_iff order_trans)
qed

subsubsection‹Totally bounded›

proposition seq_compact_imp_totally_bounded:
  assumes "seq_compact S"
  shows "\\>0. \k. finite k \ k \ S \ S \ (\x\k. ball x \)"
proof -
  { fix ε::real assume "\ > 0" assume *: "\k. finite k \ k \ S \ \ S \ (\x\k. ball x \)"
    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 ‹ε > 0› 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‹Heine-Borel theorem›

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 ‹seq_compact S› 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 ε where "0 < \" "ball x \ \ T"
      by auto
    then have "0 < \/2" "ball x (\/2) \ T"
      by auto
    from Rats_dense_in_real[OF ‹0 < ε/2›] obtain r where "r \ \" "0 < r" "r < \/2"
      by auto
    from f[rule_format, of r] ‹0 < r› ‹x ∈ S› obtain k where "k \ f r" "x \ ball k r"
      by auto
    from ‹r ∈ ℚ› ‹0 < r› ‹k ∈ f r› have "ball k r \ 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 ‹r < ε/2› ‹x ∈ ball k r› have "dist x y < \"
        by (intro dist_triangle_half_r [of k _ ε]) (auto simp: dist_commute)
      with ‹ball x ε ⊆ T› show "y \ 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: 🍋 ‹this is the definition of compactness in HOL Light›
  "compact (S :: 'a::metric_space set) \
   (∀f. (∀n. f n ∈ S) ⟶ (∃l∈S. ∃r::nat==>nat. strict_mono r ∧ (f ∘ r) <---- l))"
  unfolding compact_eq_seq_compact_metric seq_compact_def by auto

subsubsection ‹Complete the chain of compactness variants›

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 ‹Banach fixed point theorem›
  
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 δ where "\ = 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: δ_def)
  next
    case (Suc m)
    with ‹0 ≤ c› have "c * dist (z m) (z (Suc m)) \ c ^ Suc m * \"
      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 ‹ε > 0› show ?thesis by simp
  next
    case False
    with zero_le_dist[of "z 0" "z 1"] have "\ > 0"
      by (metis δ_def less_le)
    with c ‹ε > 0› have "0 < \ * (1 - c) / \"
      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 ‹n≥N›, of c] c by simp
      have "1 - c ^ (m - n) > 0"
        using power_strict_mono[of c 1 "m - n"] c ‹m > n› by simp
      with ‹δ > 0› c have **: "\ * (1 - c ^ (m - n)) / (1 - c) > 0"
        by simp
      from cf_z2[of n "m - n"] ‹m > n›
      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 ‹1 - c ^ (m - n) > 0› ‹ε > 0› have "\ \ \"
        using mult_right_le_one_le[of ε "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 ‹0 < ε› 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 ‹complete S› complete_def z_in_s by blast

  define ε where "\ = dist (f x) x"
  have "\ = 0"
  proof (rule ccontr)
    assume "\ \ 0"
    then have "\ > 0"
      unfolding ε_def using zero_le_dist[of "f x" x]
      by (metis dist_eq_0_iff dist_nz ε_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: ‹x ∈ S› lipschitz z_in_s)
    also have "\ < \/2"
      using N' and c using * by auto
    finally show False
      unfolding fzn
      by (metis N ε_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: ε_def)
  moreover have "y = x" if "f y = y" "y \ S" for y
  proof -
    from ‹x ∈ S› ‹f x = x› that have "dist x y \ 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 ‹x∈S› by blast
qed


section ‹Edelstein fixed point theorem›

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 ‹a ∈ S› dist gs image_subset_iff le order.strict_iff_not)
  moreover have "\x. x \ S \ g x = x \ x = a"
    using ‹a ∈ S› calculation dist by fastforce
  ultimately show "\!x\S. g x = x"
    using ‹a ∈ S› by blast
qed

section ‹The diameter of a set›

definition🍋‹tag important› diameter :: "'a::metric_space set \ 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 δ where z: "\x. x \ S \ dist z x \ \"
    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 ‹x ∈ S› show ?thesis
    by (auto simp: diameter_def)
qed

lemma diameter_lower_bounded:
  fixes S :: "'a :: metric_space set"
  assumes S: "bounded S"
    and δ: "0 < \" "\ < diameter S"
  shows "\x\S. \y\S. \ < dist x y"
proof (rule ccontr)
  assume contr: "\ ?thesis"
  moreover have "S \ {}"
    using δ by (auto simp: diameter_def)
  ultimately have "diameter S \ \"
    by (auto simp: not_less diameter_def intro!: cSUP_least)
  with ‹δ < diameter S› 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 ‹bounded T› diameter_bounded_bound by (force simp: bdd_above_def)
  with False ‹S ⊆ T› 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 δ where "\ = diameter(closure S) - diameter(S)"
    have "\ > 0"
      using that by (simp add: δ_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: δ_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 ‹0 < δ› 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 δ_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 δ where "0 < \" "\T. \T \ S; diameter T < \\ \ \B \ \. T \ B"
proof (cases "S = {}")
  case True
  then show ?thesis
    by (metis ‹C ≠ {}› 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 ‹S ⊆ ∪C› 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 \" "S \ \\" and T: "\ \ (\x. ball x (r x)) ` S"
    by (rule compactE [OF ‹compact S›]) 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 ‹S ⊆ ∪T› by auto
  define δ where "\ = Inf (r ` S0)"
  have "\ > 0"
    using ‹finite S0› ‹S0 ⊆ S› ‹S0 ≠ {}› r by (auto simp: δ_def finite_less_Inf_iff)
  show ?thesis
  proof
    show "0 < \"
      by (simp add: ‹0 < δ›)
    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 ‹T ⊆ S› by auto
      then obtain x where "x \ S0" and x: "y \ ball x (r x)"
        using ‹S ⊆ ∪T› S0 that by blast
      have "ball y \ \ ball y (r x)"
        by (metis δ_def ‹S0 ≠ {}› ‹finite S0› ‹x ∈ S0› 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 ‹S0 ⊆ S› ‹x ∈ S0› dual_order.trans subsetCE)
      have "bounded T"
        using ‹compact S› bounded_subset compact_imp_bounded ‹T ⊆ S› by blast
      then have "T \ ball y \"
        using ‹y ∈ T› dia diameter_bounded_bound by fastforce
      then show ?thesis
        by (meson ‹C ∈ C› ‹ball y δ ⊆ C› subset_eq)
    qed (use ‹C ≠ {}› in auto)
  qed
qed


section ‹Metric spaces with the Heine-Borel property›

text ‹
  A metric space (or topological vector space) is said to have the
  Heine-Borel property if every closed and bounded subset is compact.
›

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

--> maximum size reached

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