Theory Elementary_Metric_Spaces

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

section ‹Elementary Metric Spaces›

theory Elementary_Metric_Spaces
  imports
    Abstract_Topology_2
    Metric_Arith
begin

subsection ‹Open and closed balls›

definitiontag important› ball :: "'a::metric_space  real  'a set"
  where "ball x e = {y. dist x y < e}"

definitiontag important› cball :: "'a::metric_space  real  'a set"
  where "cball x e = {y. dist x y  e}"

definitiontag important› sphere :: "'a::metric_space  real  'a set"
  where "sphere x e = {y. dist x y = e}"

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

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

lemma mem_sphere [simp]: "y  sphere x e  dist x y = e"
  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 e  0 < e"
  by simp

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

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

lemma mem_ball_imp_mem_cball: "x  ball y e  x  cball y e"
  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]: "d  e  ball x d  ball x e"
  by auto

lemma subset_cball[intro]: "d  e  cball x d  cball x e"
  by auto

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

lemma mem_cball_leI: "x  cball y e  e  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 e)"
proof -
  have "open (dist x -` {..<e})"
    by (intro open_vimage open_lessThan continuous_intros)
  also have "dist x -` {..<e} = ball x e"
    by auto
  finally show ?thesis .
qed

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

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

lemma openE[elim?]:
  assumes "open S" "xS"
  obtains e where "e>0" "ball x e  S"
  using assms unfolding open_contains_ball by auto

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

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

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

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

lemma open_contains_cball: "open S  (xS. e>0.  cball x e  S)"
proof -
  {
    fix x and e::real
    assume "xS" "e>0" "ball x e  S"
    then have "d>0. cball x d  S"
      unfolding subset_eq by (rule_tac x="e/2" in exI, auto)
  }
  moreover
  {
    fix x and e::real
    assume "xS" "e>0" "cball x e  S"
    then have "d>0. ball x d  S"
      using mem_ball_imp_mem_cball by blast
  }
  ultimately show ?thesis
    unfolding open_contains_ball by auto
qed

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

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

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

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

lemma at_within_ball: "e > 0  dist x y < e  at y within ball x e = 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 e) = ball x e"
  by (simp add: interior_open)

lemma cball_eq_empty [simp]: "cball x e = {}  e < 0"
  by (smt (verit, best) Diff_empty ball_eq_empty cball_diff_sphere centre_in_ball centre_in_cball sphere_empty)

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

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

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

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

lemma cball_divide_subset: "d  1  cball x (e/d)  cball x e"
  by (smt (verit, best) cball_empty div_by_1 frac_le subset_cball zero_le_divide_iff)

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

lemma cball_scale:
  assumes "a  0"
  shows   "(λx. a *R x) ` cball c r = cball (a *R c :: 'a :: real_normed_vector) (¦a¦ * r)"
proof -
  have 1: "(λx. a *R x) ` cball c r  cball (a *R c) (¦a¦ * r)" if "a  0" for a r and c :: 'a
  proof safe
    fix x
    assume x: "x  cball c r"
    have "dist (a *R c) (a *R x) = norm (a *R c - a *R x)"
      by (auto simp: dist_norm)
    also have "a *R c - a *R x = a *R (c - x)"
      by (simp add: algebra_simps)
    finally show "a *R x  cball (a *R c) (¦a¦ * r)"
      using that x by (auto simp: dist_norm)
  qed

  have "cball (a *R c) (¦a¦ * r) = (λx. a *R x) ` (λx. inverse a *R x) ` cball (a *R c) (¦a¦ * r)"
    unfolding image_image using assms by simp
  also have "  (λx. a *R x) ` cball (inverse a *R (a *R c)) (¦inverse a¦ * (¦a¦ * r))"
    using assms by (intro image_mono 1) auto
  also have " = (λx. a *R x) ` cball c r"
    using assms by (simp add: algebra_simps)
  finally have "cball (a *R c) (¦a¦ * r)  (λx. a *R x) ` cball c r" .
  moreover from assms have "(λx. a *R x) ` cball c r  cball (a *R c) (¦a¦ * r)"
    by (intro 1) auto
  ultimately show ?thesis by blast
qed

lemma ball_scale:
  assumes "a  0"
  shows   "(λx. a *R x) ` ball c r = ball (a *R c :: 'a :: real_normed_vector) (¦a¦ * r)"
proof -
  have 1: "(λx. a *R x) ` ball c r  ball (a *R c) (¦a¦ * r)" if "a  0" for a r and c :: 'a
  proof safe
    fix x
    assume x: "x  ball c r"
    have "dist (a *R c) (a *R x) = norm (a *R c - a *R x)"
      by (auto simp: dist_norm)
    also have "a *R c - a *R x = a *R (c - x)"
      by (simp add: algebra_simps)
    finally show "a *R x  ball (a *R c) (¦a¦ * r)"
      using that x by (auto simp: dist_norm)
  qed

  have "ball (a *R c) (¦a¦ * r) = (λx. a *R x) ` (λx. inverse a *R x) ` ball (a *R c) (¦a¦ * r)"
    unfolding image_image using assms by simp
  also have "  (λx. a *R x) ` ball (inverse a *R (a *R c)) (¦inverse a¦ * (¦a¦ * r))"
    using assms by (intro image_mono 1) auto
  also have " = (λx. a *R x) ` ball c r"
    using assms by (simp add: algebra_simps)
  finally have "ball (a *R c) (¦a¦ * r)  (λx. a *R x) ` ball c r" .
  moreover from assms have "(λx. a *R x) ` ball c r  ball (a *R c) (¦a¦ * r)"
    by (intro 1) auto
  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 "zs. 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 e :: real
    assume e: "e > 0"
    then obtain n where n: "Suc n > 1 / e"
      by (meson le_nat_floor lessI not_le)
    have "dist (f k) x < e" 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 " < e"
        using n e by (simp add: field_simps)
      finally show ?thesis .
    qed
    thus "F k in sequentially. dist (f k) x < e"
      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

subsection ‹Limit Points›

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

lemma islimpt_approachable_le: "x islimpt S  (e>0. x' S. x'  x  dist x' x  e)"
  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  (e>0. infinite(S  ball x e))"
  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  (e>0. infinite(S  cball x e))"
  unfolding islimpt_eq_infinite_ball
  by (metis open_ball ball_subset_cball centre_in_ball finite_Int inf.absorb_iff2 inf_assoc open_contains_cball_eq)


subsection ‹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 cball_eq_sing:
  fixes x :: "'a::{metric_space,perfect_space}"
  shows "cball x e = {x}  e = 0"
  by (smt (verit, best) open_ball ball_eq_empty ball_subset_cball cball_empty cball_trivial 
      not_open_singleton subset_singleton_iff)


subsection ‹Finite and discrete›

lemma finite_ball_include:
  fixes a :: "'a::metric_space"
  assumes "finite S" 
  shows "e>0. S  ball a e"
  using assms
proof induction
  case (insert x S)
  then obtain e0 where "e0>0" and e0:"S  ball a e0" by auto
  define e where "e = max e0 (2 * dist a x)"
  have "e>0" unfolding e_def using e0>0 by auto
  moreover have "insert x S  ball a e"
    using e0 e>0 unfolding e_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 "d>0. xS. x  a  d  dist a x"
  using assms
proof induction
  case (insert x S)
  then obtain d where "d > 0" and d: "xS. x  a  d  dist a x"
    by blast
  show ?case
    by (smt (verit, del_insts) dist_pos_lt insert.IH insert_iff)
qed (auto intro: zero_less_one)

lemma discrete_imp_closed:
  fixes S :: "'a::metric_space set"
  assumes e: "0 < e"
    and d: "x  S. y  S. dist y x < e  y = x"
  shows "closed S"
proof -
  have False if C: "e. e>0  x'S. x'  x  dist x' x < e" for x
  proof -
    from e have e2: "e/2 > 0" by arith
    from C[OF e2] obtain y where y: "y  S" "y  x" "dist y x < e/2"
      by blast
    from e2 y(2) have mp: "min (e/2) (dist x y) > 0"
      by simp
    from d 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 e: "0 < e"
    and d: "x y. x  S  y  S  dist y x < e  y = x"
  shows "¬ x islimpt S"
proof
  assume "x islimpt S"
  hence "x islimpt S - {x}"
    by (meson islimpt_punctured)
  moreover from assms have "closed (S - {x})"
    by (intro discrete_imp_closed) auto
  ultimately show False
    unfolding closed_limpt by blast
qed
  

subsection ‹Interior›

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

lemma mem_interior_cball: "x  interior S  (e>0. cball x e  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)


subsection ‹Frontier›

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


subsection ‹Limits›

proposition Lim: "(f  l) net  trivial_limit net  (e>0. eventually (λx. dist (f x) l < e) 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) 
    (e>0. d>0. xS. 0 < dist x a  dist x a  d  dist (f x) l < e)"
  by (auto simp: tendsto_iff eventually_at_le)

proposition Lim_within: "(f  l) (at a within S) 
    (e >0. d>0. x  S. 0 < dist x a  dist x a  < d  dist (f x) l < e)"
  by (auto simp: tendsto_iff eventually_at)

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

proposition Lim_at: "(f  l) (at a) 
    (e >0. d>0. x. 0 < dist x a  dist x a < d   dist (f x) l < e)"
  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 "e>0. x'S. x'  x  dist x' x < e"
    by (force simp: islimpt_approachable)
  then obtain y where y: "e. e>0  y e  S  y e  x  dist (y e) x < e"
    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 show ?case
      by (smt (verit, best) fSuc dist_pos_lt inverse_positive_iff_positive y zero_less_power)
  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
      proof cases
        assume "m < n"
        have "dist (f(Suc n)) x = dist (y (min (inverse(2 ^ (Suc n))) (dist (f n) x))) x"
          by (simp add: fSuc)
        also have " < dist (f n) x"
          by (metis dist_pos_lt f min.strict_order_iff min_less_iff_conj y)
        also have " < dist (f m) x"
          using Suc.IH m < n by blast
        finally show ?thesis .
      next
        assume "m = n" then show ?case
          by (smt (verit, best) dist_pos_lt f fSuc y)
      qed
    qed
    then show "inj f"
      by (metis less_irrefl linorder_injI)
    have "e n. 0 < e; nat 1 / e  n  dist (f n) x < e"
      apply (rule less_trans [OF f [THEN conjunct2, THEN conjunct2]])
      by (simp add: divide_simps order_le_less_trans)
    then show "f  x"
      using lim_sequentially by blast
  qed
next
  assume ?rhs
  then show ?lhs
    by (fastforce simp add: islimpt_approachable lim_sequentially)
qed

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


subsection ‹Continuity›

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

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

corollary continuous_at_eps_delta:
  "continuous (at x) f  (e > 0. d > 0. x'. dist x' x < d  dist (f x') (f x) < e)"
  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  (e>0. d>0. f (a + d) - f a < e)"
  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)  (e > 0. delta > 0. f a - f (a - delta) < e)"
  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 
    (e > 0. d > 0. f ` (ball x d  S)  ball (f x) e)"
  (is "?lhs = ?rhs")
proof
  assume ?lhs
  {
    fix e :: real
    assume "e > 0"
    then obtain d where "d>0" and d: "yS. 0 < dist y x  dist y x < d  dist (f y) (f x) < e"
      using ?lhs[unfolded continuous_within Lim_within] by auto
    { fix y
      assume "y  f ` (ball x d  S)" then have "y  ball (f x) e"
        using d e > 0 by (auto simp: dist_commute)
    }
    then have "d>0. f ` (ball x d  S)  ball (f x) e"
      using d > 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

lemma continuous_at_ball:
  "continuous (at x) f  (e>0. d>0. f ` (ball x d)  ball (f x) e)"
  apply (simp add: continuous_at Lim_at subset_eq Ball_def Bex_def image_iff)
  by (smt (verit, ccfv_threshold) dist_commute dist_self)


text‹Define setwise continuity in terms of limits within the set.›

lemma continuous_on_iff:
  "continuous_on s f 
    (xs. e>0. d>0. x's. dist x' x < d  dist (f x') (f x) < e)"
  unfolding continuous_on_def Lim_within
  by (metis dist_pos_lt dist_self)

lemma continuous_within_E:
  assumes "continuous (at x within S) f" "e>0"
  obtains d where "d>0"  "x'. x' S; dist x' x  d  dist (f x') (f x) < e"
  using assms unfolding continuous_within_eps_delta
  by (metis dense order_le_less_trans)

lemma continuous_onI [intro?]:
  assumes "x e. e > 0; x  S  d>0. x'S. dist x' x < d  dist (f x') (f x)  e"
  shows "continuous_on S f"
apply (simp add: continuous_on_iff, clarify)
apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)
done

text‹Some simple consequential lemmas.›

lemma continuous_onE:
    assumes "continuous_on s f" "xs" "e>0"
    obtains d where "d>0"  "x'. x'  s; dist x' x  d  dist (f x') (f x) < e"
  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 < d"
    and "x  s"
    and "x'. x'  s; dist x' x < d  f x' = g x'"
  shows "continuous (at x within s) g"
  using assms
  unfolding continuous_within by (force intro: Lim_transform_within)


subsection ‹Closure and Limit Characterization›

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

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

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

lemma closed_approachable:
  fixes S :: "'a::metric_space set"
  shows "closed S  (e>0. yS. dist y x < e)  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 *: "xS. Inf S  x"
    using cInf_lower[of _ S] assms by metis
  { fix e :: real
    assume "e > 0"
    then have "Inf S < Inf S + e" by simp
    with assms obtain x where "x  S" "x < Inf S + e"
      using cInf_lessD by blast
    with * have "xS. dist x (Inf S) < e"
      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 *: "xS. x  Sup S"
    using cSup_upper[of _ S] assms by metis
  {
    fix e :: real
    assume "e > 0"
    then have "Sup S - e < Sup S" by simp
    with assms obtain x where "x  S" "Sup S - e < x"
      using less_cSupE by blast
    with * have "xS. dist x (Sup S) < e"
      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)  (e>0. S  ball x e - {x}  {})"
  (is "?lhs  ?rhs")
proof
  show ?rhs if ?lhs
  proof -
    { fix e :: real
      assume "e > 0"
      then obtain y where "y  S - {x}" and "dist y x < e"
        using ?lhs not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"]
        by auto
      then have "y  S  ball x e - {x}"
        unfolding ball_def by (simp add: dist_commute)
      then have "S  ball x e - {x}  {}" by blast
    }
    then show ?thesis by auto
  qed
  show ?lhs if ?rhs
  proof -
    { fix e :: real
      assume "e > 0"
      then obtain y where "y  S  ball x e - {x}"
        using ?rhs by blast
      then have "y  S - {x}" and "dist y x < e"
        unfolding ball_def by (simp_all add: dist_commute)
      then have "y  S - {x}. dist y x < e"
        by auto
    }
    then show ?thesis
      using not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"]
      by auto
  qed
qed


subsection ‹Boundedness›

  (* FIXME: This has to be unified with BSEQ!! *)
definitiontag important› (in metric_space) bounded :: "'a set  bool"
  where "bounded S  (x e. yS. dist x y  e)"

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

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

lemma bounded_iff: "bounded S  (a. xS. 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: "yS. 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 e)"
  unfolding bounded_def  using mem_cball by blast

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

lemma bounded_Un[simp]: "bounded (S  T)  bounded S  bounded T"
  by (auto simp: bounded_def) (metis Un_iff bounded_any_center le_max_iff_disj)

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

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

lemma bounded_insert [simp]: "bounded (insert x S)  bounded S"
proof -
  have "y{x}. dist x y  0"
    by simp
  then have "bounded {x}"
    unfolding bounded_def by fast
  then show ?thesis
    by (metis insert_is_Un bounded_Un)
qed

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 e::real and y where "S  cball y e" "0  e"
    using assms by (auto simp: bounded_subset_cball)
  then show ?thesis
    by (intro exI[where x="dist x y + e + 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 "zs. dist x z  a" "zt. dist y z  b"
    using assms [unfolded bounded_def] by auto
  then have "zs × t. dist (x, y) z  sqrt (a2 + b2)"
    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


subsection ‹Compactness›

lemma compact_imp_bounded:
  assumes "compact U"
  shows "bounded U"
proof -
  have "compact U" "xU. open (ball x 1)" "U  (xU. ball x 1)"
    using assms by auto
  then obtain D where D: "D  U" "finite D" "U  (xD. ball x 1)"
    by (metis compactE_image)
  from finite D have "bounded (xD. ball x 1)"
    by (simp add: bounded_UN)
  then show "bounded U" using U  (xD. 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 "xA. norm (f x)  B"
    by (auto dest!: compact_imp_bounded simp: bounded_iff)
  hence "max B 0  0" and "xA. 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 "xS. yS. uS. vS. 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 e where "e > 0"  "(xA. ball x e)  B"
proof -
  have "xA. e. e > 0  ball x e  B"
    using assms unfolding open_contains_ball by blast
  then obtain e where e: "x. x  A  e x > 0" "x. x  A  ball x (e x)  B"
    by metis
  define C where "C = e ` A"
  obtain X where X: "X  A" "finite X" "A  (cX. ball c (e c / 2))"
    using assms(1)
  proof (rule compactE_image)
    show "open (ball x (e x / 2))" if "x  A" for x
      by simp
    show "A  (cA. ball c (e c / 2))"
      using e by auto
  qed auto

  define e' where "e' = Min (insert 1 ((λx. e x / 2) ` X))"
  have "e' > 0"
    unfolding e'_def using e X by (subst Min_gr_iff) auto
  have e': "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 "(xA. 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 (e 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 < e z / 2"
        using xy z by auto
      also have "dist x y < e'"
        using xy by auto
      also have "  e z / 2"
        using z by (intro e') auto
      finally have "y  ball z (e z)"
        by (simp add: dist_commute)
      also have "  B"
        using z X by (intro e) auto
      finally show "y  B" .
    qed
  qed
qed

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

subsubsection‹Totally bounded›

proposition seq_compact_imp_totally_bounded:
  assumes "seq_compact S"
  shows "e>0. k. finite k  k  S  S  (xk. ball x e)"
proof -
  { fix e::real assume "e > 0" assume *: "k. finite k  k  S  ¬ S  (xk. ball x e)"
    let ?Q = "λx n r. r  S  (m < (n::nat). ¬ (dist (x m) r < e))"
    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  (xx ` {0..<n}. ball x e)"
        using *[of "x ` {0 ..< n}"] by (auto simp: subset_eq)
      then obtain z where z:"zS" "z  (xx ` {0..<n}. ball x e)"
        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) < e)"
      by blast
    then obtain l r where "l  S" and r:"strict_mono  r" and "((x  r)  l) sequentially"
      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) < e"
      unfolding Cauchy_def using e > 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 -
  from seq_compact_imp_totally_bounded[OF seq_compact S]
  obtain f where f: "e>0. finite (f e)  f e  S  S  (xf e. ball x e)"
    unfolding choice_iff' ..
  define K where "K = (λ(x, r). ball x r) ` ((e    {0 <..}. f e) × )"
  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 (auto intro: countable_finite countable_subset countable_rat
               intro!: countable_image countable_SIGMA countable_UN)
    show "bK. 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 e where "0 < e" "ball x e  T"
      by auto
    then have "0 < e/2" "ball x (e/2)  T"
      by auto
    from Rats_dense_in_real[OF 0 < e/2] obtain r where "r  " "0 < r" "r < e/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 "bK. x  b  b  S  T"
    proof (rule bexI[rotated], safe)
      fix y
      assume "y  ball k r"
      with r < e/2 x  ball k r have "dist x y < e"
        by (intro dist_triangle_half_r [of k _ e]) (auto simp: dist_commute)
      with ball x e  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)  (lS. r::natnat. 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


subsection ‹Banach fixed point theorem›
  
theorem banach_fix:― ‹TODO: rename to Banach_fix›
  assumes s: "complete s" "s  {}"
    and c: "0  c" "c < 1"
    and f: "f ` s  s"
    and lipschitz: "xs. ys. dist (f x) (f y)  c * dist x y"
  shows "∃!xs. f x = x"
proof -
  from c have "1 - c > 0" by simp

  from s(2) 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 d where "d = 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) * d" for n :: nat
  proof (induct n)
    case 0
    then show ?case
      by (simp add: d_def)
  next
    case (Suc m)
    with 0  c have "c * dist (z m) (z (Suc m))  c ^ Suc m * d"
      using mult_left_mono[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by simp
    then show ?case
      using lipschitz[THEN bspec[where x="z m"], OF z_in_s, THEN bspec[where x="z (Suc m)"], OF z_in_s]
      by (simp add: fzn mult_le_cancel_left)
  qed

  have cf_z2: "(1 - c) * dist (z m) (z (m + n))  (c ^ m) * d * (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) * d)"
      by simp
    also from Suc have "  c ^ m * d * (1 - c ^ k) + (1 - c) * c ^ (m + k) * d"
      by (simp add: field_simps)
    also have " = (c ^ m) * (d * (1 - c ^ k) + (1 - c) * c ^ k * d)"
      by (simp add: power_add field_simps)
    also from c have "  (c ^ m) * d * (1 - c ^ Suc k)"
      by (simp add: field_simps)
    finally show ?case by simp
  qed

  have "N. m n. N  m  N  n  dist (z m) (z n) < e" if "e > 0" for e
  proof (cases "d = 0")
    case True
    from 1 - c > 0 have "(1 - c) * x  0  x  0" for x
      by (simp add: mult_le_0_iff)
    with c cf_z2[of 0] True have "z n = z0" for n
      by (simp add: z_def)
    with e > 0 show ?thesis by simp
  next
    case False
    with zero_le_dist[of "z 0" "z 1"] have "d > 0"
      by (metis d_def less_le)
    with 1 - c > 0 e > 0 have "0 < e * (1 - c) / d"
      by simp
    with c obtain N where N: "c ^ N < e * (1 - c) / d"
      using real_arch_pow_inv[of "e * (1 - c) / d" c] by auto
    have *: "dist (z m) (z n) < e" if "m > n" and as: "m  N" "n  N" for m n :: nat
    proof -
      from c n  N have *: "c ^ n  c ^ N"
        using power_decreasing[OF nN, of c] by simp
      from c m > n have "1 - c ^ (m - n) > 0"
        using power_strict_mono[of c 1 "m - n"] by simp
      with d > 0 0 < 1 - c have **: "d * (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 * d * (1 - c ^ (m - n)) / (1 - c)"
        by (simp add: pos_le_divide_eq[OF 1 - c > 0] mult.commute dist_commute)
      also have "  c ^ N * d * (1 - c ^ (m - n)) / (1 - c)"
        using mult_right_mono[OF * order_less_imp_le[OF **]]
        by (simp add: mult.assoc)
      also have " < (e * (1 - c) / d) * d * (1 - c ^ (m - n)) / (1 - c)"
        using mult_strict_right_mono[OF N **] by (auto simp: mult.assoc)
      also from c d > 0 1 - c > 0 have " = e * (1 - c ^ (m - n))"
        by simp
      also from c 1 - c ^ (m - n) > 0 e > 0 have "  e"
        using mult_right_le_one_le[of e "1 - c ^ (m - n)"] by auto
      finally show ?thesis by simp
    qed
    have "dist (z n) (z m) < e" if "N  m" "N  n" for m n :: nat
    proof (cases "n = m")
      case True
      with e > 0 show ?thesis by simp
    next
      case False
      with *[of n m] *[of m n] and that show ?thesis
        by (auto simp: dist_commute nat_neq_iff)
    qed
    then show ?thesis by auto
  qed
  then have "Cauchy z"
    by (metis metric_CauchyI)
  then obtain x where "xs" and x:"(z  x) sequentially"
    using s(1)[unfolded compact_def complete_def, THEN spec[where x=z]] and z_in_s by auto

  define e where "e = dist (f x) x"
  have "e = 0"
  proof (rule ccontr)
    assume "e  0"
    then have "e > 0"
      unfolding e_def using zero_le_dist[of "f x" x]
      by (metis dist_eq_0_iff dist_nz e_def)
    then obtain N where N:"nN. dist (z n) x < e/2"
      using x[unfolded lim_sequentially, THEN spec[where x="e/2"]] by auto
    then have N':"dist (z N) x < e/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"
      using lipschitz[THEN bspec[where x="z N"], THEN bspec[where x=x]]
      using z_in_s[of N] xs
      using c
      by auto
    also have " < e/2"
      using N' and c using * by auto
    finally show False
      unfolding fzn
      using N[THEN spec[where x="Suc N"]] and dist_triangle_half_r[of "z (Suc N)" "f x" e x]
      unfolding e_def
      by auto
  qed
  then have "f x = x" by (auto simp: e_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[THEN bspec[where x=x], THEN bspec[where x=y]] by simp
    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 xs by blast
qed


subsection ‹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: "xS. yS. x  y  dist (g x) (g y) < dist x y"
  shows "∃!xS. 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 e. x  S  y  S  0 < e  dist y x < e  dist (g y) (g x) < e"
    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"
  proof (rule ccontr)
    assume "g a  a"
    with a  S gs have "dist (g (g a)) (g a) < dist (g a) a"
      by (intro dist[rule_format]) auto
    moreover have "dist (g a) a  dist (g (g a)) (g a)"
      using a  S gs by (intro le) auto
    ultimately show False by auto
  qed
  moreover have "x. x  S  g x = x  x = a"
    using dist[THEN bspec[where x=a]] g a = a and aS by auto
  ultimately show "∃!xS. g x = x"
    using a  S by blast
qed

subsection ‹The diameter of a set›

definitiontag 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  d"
    and no: "x y. x  S; y  S  norm(x - y)  d"
  shows "diameter S  d"
  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 d where z: "x. x  S  dist z x  d"
    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 * d"
      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 d: "0 < d" "d < diameter S"
  shows "xS. yS. d < dist x y"
proof (rule ccontr)
  assume contr: "¬ ?thesis"
  moreover have "S  {}"
    using d by (auto simp: diameter_def)
  ultimately have "diameter S  d"
    by (auto simp: not_less diameter_def intro!: cSUP_least)
  with d < diameter S show False by auto
qed

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

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

lemma diameter_compact_attained:
  assumes "compact S"
    and "S  {}"
  shows "xS. yS. dist x y = diameter S"
proof -
  have b: "bounded S" using assms(1)
    by (rule compact_imp_bounded)
  then obtain x y where xys: "xS" "yS"
    and xy: "uS. vS. 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 all_not_in_conv assms diameter_bounded_bound diameter_empty dist_self 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
    apply (simp add: diameter_def)
    apply (rule cSUP_subset_mono, auto)
    done
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 d where "d = diameter(closure S) - diameter(S)"
    have "d > 0"
      using that by (simp add: d_def)
    then have dle: "diameter(closure(S)) - d / 2 < diameter(closure(S))"
      by simp
    have dd: "diameter (closure S) - d / 2 = (diameter(closure(S)) + diameter(S)) / 2"
      by (simp add: d_def field_split_simps)
     have bocl: "bounded (closure S)"
      using assms by blast
    moreover have "0  diameter S"
      using assms diameter_ge_0 by blast
    ultimately obtain x y where "x  closure S" "y  closure S" and xy: "diameter(closure(S)) - d / 2 < dist x y"
      by (smt (verit) dle d_less_d d_def