SSL Elementary_Metric_Spaces.thy

(*  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 *🪙R x) ` cball c r = cball (a *🪙R c :: 'a :: real_normed_vector) (∣a∣ * r)"
proof -
  have *: "(λx. a *🪙R x) ` cball c r ⊆ cball (a *🪙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 *🪙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 "*" by blast
  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)"
    using "*" by blast
  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 *: "(λx. a *🪙R x) ` ball c r ⊆ ball (a *🪙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 *🪙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 *) 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 *) auto
  ultimately show ?thesis by blast
qed

lemma sphere_scale:
  assumes "a ≠ 0"
  shows   "(λx. a *🪙R x) ` sphere c r = sphere (a *🪙R c :: 'a :: real_normed_vector) (∣a∣ * r)"
proof -
  have *: "(λx. a *🪙R x) ` sphere c r ⊆ sphere (a *🪙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 *🪙R c) (∣a∣ * r) = (λx. a *🪙R x) ` (λx. inverse a *🪙R x) ` sphere (a *🪙R c) (∣a∣ * r)"
    unfolding image_image using assms by simp
  also have "… ⊆ (λx. a *🪙R x) ` sphere (inverse a *🪙R (a *🪙R c)) (∣inverse a∣ * (∣a∣ * r))"
    using "*" by blast
  also have "… = (λx. a *🪙R x) ` sphere c r"
    using assms by (simp add: algebra_simps)
  finally have "sphere (a *🪙R c) (∣a∣ * r) ⊆ (λx. a *🪙R x) ` sphere c r" .
  moreover have "(λx. a *🪙R x) ` sphere c r ⊆ sphere (a *🪙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 "∀🪙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🪙2 + b🪙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› i
  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 🚫› ‹x ∈ S› obtain k where "k ∈ f r" "x ∈ ball k r"
      by auto
    from ‹r ∈ ℚ› ‹0 🚫› ‹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 ‹δ 🚫 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" "C ≠ {}" "S ⊆ ∪C" and ope: "∧B. B ∈ C ==> open B"
  obtains δ where "0 < δ" "∧T. [T ⊆ S; diameter T < δ] ==> ∃B ∈ C. 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 ∈ 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 ∈ C. ball x (2*r x) ⊆ C)"
    by metis
  then have "S ⊆ (∪x ∈ S. ball x (r x))"
    by auto
  then obtain T where "finite T" "S ⊆ ∪T" and T: "T ⊆ (λx. ball x (r x)) ` S"
    by (rule compactE [OF ‹compact S›]) auto
  then obtain S0 where "S0 ⊆ S" "finite S0" and S0: "T = (λ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 ∈ C. 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 ∈ 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 +
  assumes bounded_imp_convergent_subsequence:
    "bounded (range f) ==> ∃l r. strict_mono (r::nat==>nat) ∧ ((f ∘ r) ---> l) sequentially"

proposition bounded_closed_imp_seq_compact:
  fixes S::"'a::heine_borel set"
  assumes "bounded S"
    and "closed S"
  shows "seq_compact S"
  unfolding seq_compact_def
proof (intro strip)
  fix f :: "nat ==> 'a"
  assume f: "∀n. f n ∈ S"
  with ‹bounded S› have "bounded (range f)"
    by (auto intro: bounded_subset)
  obtain l r where r: "strict_mono (r :: nat ==> nat)" and l: "((f ∘ r) ---> l) sequentially"
    using bounded_imp_convergent_subsequence [OF ‹bounded (range f)›] by auto
  from f have fr: "∀n. (f ∘ r) n ∈ S"
    by simp
  show "∃l∈S. ∃r. strict_mono r ∧ (f ∘ r) <---- l"
    using assms(2) closed_sequentially fr l r by blast
qed

lemma compact_eq_bounded_closed:
  fixes S :: "'a::heine_borel set"
  shows "compact S ⟷ bounded S ∧ closed S"
  using bounded_closed_imp_seq_compact compact_eq_seq_compact_metric compact_imp_bounded compact_imp_closed 
  by auto

lemma bounded_infinite_imp_islimpt:
  fixes S :: "'a::heine_borel set"
  assumes "T ⊆ S" "bounded S" "infinite T"
  obtains x where "x islimpt S" 
  by (meson assms closed_limpt compact_eq_Bolzano_Weierstrass compact_eq_bounded_closed islimpt_subset) 

lemma compact_Inter:
  fixes F :: "'a :: heine_borel set set"
  assumes com: "∧S. S ∈ F ==> compact S" and "F ≠ {}"
  shows "compact(∩ F)"
  using assms
  by (meson Inf_lower all_not_in_conv bounded_subset closed_Inter compact_eq_bounded_closed)

lemma compact_closure [simp]:
  fixes S :: "'a::heine_borel set"
  shows "compact(closure S) ⟷ bounded S"
by (meson bounded_closure bounded_subset closed_closure closure_subset compact_eq_bounded_closed)

instance🍋‹tag important› real :: heine_borel
proof
  fix f :: "nat ==> real"
  assume f: "bounded (range f)"
  obtain r :: "nat ==> nat" where r: "strict_mono r" "monoseq (f ∘ r)"
    unfolding comp_def by (metis seq_monosub)
  then have "Bseq (f ∘ r)"
    unfolding Bseq_eq_bounded by (metis f BseqI' bounded_iff comp_apply rangeI)
  with r show "∃l r. strict_mono r ∧ (f ∘ r) <---- l"
    using Bseq_monoseq_convergent[of "f ∘ r"] by (auto simp: convergent_def)
qed

lemma compact_lemma_general:
  fixes f :: "nat ==> 'a"
  fixes proj::"'a ==> 'b ==> 'c::heine_borel" (infixl ‹proj› 60)
  fixes unproj:: "('b ==> 'c) ==> 'a"
  assumes finite_basis: "finite basis"
  assumes bounded_proj: "∧k. k ∈ basis ==> bounded ((λx. x proj k) ` range f)"
  assumes proj_unproj: "∧ε k. k ∈ basis ==> (unproj ε) proj k = ε k"
  assumes unproj_proj: "∧x. unproj (λk. x proj k) = x"
  shows "∀δ⊆basis. ∃l::'a. ∃ r::nat==>nat.
    strict_mono r ∧ (∀ε>0. eventually (λn. ∀i∈δ. dist (f (r n) proj i) (l proj i) < ε) sequentially)"
proof safe
  fix δ :: "'b set"
  assume δ: "δ ⊆ basis"
  with finite_basis have "finite δ"
    by (blast intro: finite_subset)
  from this δ show "∃l::'a. ∃r::nat==>nat. strict_mono r ∧
    (∀ε>0. eventually (λn. ∀i∈δ. dist (f (r n) proj i) (l proj i) < ε) sequentially)"
  proof (induct δ)
    case empty
    then show ?case
      unfolding strict_mono_def by auto
  next
    case (insert k δ)
    have k[intro]: "k ∈ basis"
      using insert by auto
    have s': "bounded ((λx. x proj k) ` range f)"
      using k
      by (rule bounded_proj)
    obtain l1::"'a" and r1 where r1: "strict_mono r1"
      and lr1: "∀ε > 0. ∀🪙F n in sequentially. ∀i∈δ. dist (f (r1 n) proj i) (l1 proj i) < ε"
      using insert by auto
    have f': "∀n. f (r1 n) proj k ∈ (λx. x proj k) ` range f"
      by simp
    have "bounded (range (λi. f (r1 i) proj k))"
      by (metis (lifting) bounded_subset f' image_subsetI s')
    then obtain l2 r2 where r2: "strict_mono r2" and lr2: "(λi. f (r1 (r2 i)) proj k) <---- l2"
      using bounded_imp_convergent_subsequence[of "λi. f (r1 i) proj k"]
      by (auto simp: o_def)
    define r where "r = r1 ∘ r2"
    have r: "strict_mono r"
      using r1 and r2 unfolding r_def o_def strict_mono_def by auto
    moreover
    define l where "l = unproj (λi. if i = k then l2 else l1 proj i)"
    { fix ε::real
      assume "ε > 0"
      from lr1 ‹ε > 0› have N1: "∀🪙F n in sequentially. ∀i∈δ. dist (f (r1 n) proj i) (l1 proj i) < ε"
        by blast
      from lr2 ‹ε > 0› have N2: "∀🪙F n in sequentially. dist (f (r1 (r2 n)) proj k) l2 < ε"
        by (rule tendstoD)
      from r2 N1 have N1': "∀🪙F n in sequentially. ∀i∈δ. dist (f (r1 (r2 n)) proj i) (l1 proj i) < ε"
        by (rule eventually_subseq)
      have "∀🪙F n in sequentially. ∀i∈insert k δ. dist (f (r n) proj i) (l proj i) < ε"
        using N1' N2
        by eventually_elim (use insert.prems in ‹auto simp: l_def r_def o_def proj_unproj›)
    }
    ultimately show ?case by auto
  qed
qed

lemma bounded_fst: "bounded s ==> bounded (fst ` s)"
  unfolding bounded_def
  by (metis (erased, opaque_lifting) dist_fst_le image_iff order_trans)

lemma bounded_snd: "bounded s ==> bounded (snd ` s)"
  unfolding bounded_def
  by (metis (no_types, opaque_lifting) dist_snd_le image_iff order.trans)

instance🍋‹tag important› prod :: (heine_borel, heine_borel) heine_borel
proof
  fix f :: "nat ==> 'a × 'b"
  assume f: "bounded (range f)"
  then have "bounded (fst ` range f)"
    by (rule bounded_fst)
  then have s1: "bounded (range (fst ∘ f))"
    by (simp add: image_comp)
  obtain l1 r1 where r1: "strict_mono r1" and l1: "(λn. fst (f (r1 n))) <---- l1"
    using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast
  from f have s2: "bounded (range (snd ∘ f ∘ r1))"
    by (auto simp: image_comp intro: bounded_snd bounded_subset)
  obtain l2 r2 where r2: "strict_mono r2" and l2: "(λn. snd (f (r1 (r2 n)))) <---- l2"
    using bounded_imp_convergent_subsequence [OF s2]
    unfolding o_def by fast
  have l1': "((λn. fst (f (r1 (r2 n)))) ---> l1) sequentially"
    using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def .
  have l: "((f ∘ (r1 ∘ r2)) ---> (l1, l2)) sequentially"
    using tendsto_Pair [OF l1' l2] unfolding o_def by simp
  have r: "strict_mono (r1 ∘ r2)"
    using r1 r2 unfolding strict_mono_def by simp
  show "∃l r. strict_mono r ∧ ((f ∘ r) ---> l) sequentially"
    using l r by fast
qed


section ‹Completeness›

proposition (in metric_space) completeI:
  assumes "∧f. ∀n. f n ∈ s ==> Cauchy f ==> ∃l∈s. f <---- l"
  shows "complete s"
  using assms unfolding complete_def by fast

proposition (in metric_space) completeE:
  assumes "complete s" and "∀n. f n ∈ s" and "Cauchy f"
  obtains l where "l ∈ s" and "f <---- l"
  using assms unfolding complete_def by fast

(* TODO: generalize to uniform spaces *)
lemma compact_imp_complete:
  fixes S :: "'a::metric_space set"
  assumes "compact S"
  shows "complete S"
  unfolding complete_def
proof clarify
  fix f
  assume as: "(∀n::nat. f n ∈ S)" "Cauchy f"
  from as(1) obtain l r where lr: "l∈S" "strict_mono r" "(f ∘ r) <---- l"
    using assms unfolding compact_def by blast

  note lr' = seq_suble [OF lr(2)]
  {
    fix ε :: real
    assume "ε > 0"
    from as(2) obtain N where N:"∀m n. N ≤ m ∧ N ≤ n ⟶ dist (f m) (f n) < ε/2"
      unfolding Cauchy_def using ‹ε > 0› by (meson half_gt_zero)
    then obtain M where M:"∀n≥M. dist ((f ∘ r) n) l < ε/2"
      by (metis dist_self lim_sequentially lr(3))
    {
      fix n :: nat
      assume n: "n ≥ max N M"
      have "dist ((f ∘ r) n) l < ε/2"
        using n M by auto
      moreover have "r n ≥ N"
        using lr'[of n] n by auto
      then have "dist (f n) ((f ∘ r) n) < ε/2"
        using N and n by auto
      ultimately have "dist (f n) l < ε" using n M
        by metric
    }
    then have "∃N. ∀n≥N. dist (f n) l < ε" by blast
  }
  then show "∃l∈S. (f ---> l) sequentially" using ‹l∈S›
    unfolding lim_sequentially by auto
qed

proposition compact_eq_totally_bounded:
  "compact S ⟷ complete S ∧ (∀ε>0. ∃k. finite k ∧ S ⊆ (∪x∈k. ball x ε))"
    (is "_ ⟷ ?rhs")
proof
  assume assms: "?rhs"
  then obtain k where k: "∧ε. 0 < ε ==> finite (k ε)" "∧ε. 0 < ε ==> S ⊆ (∪x∈k ε. ball x ε)"
    by metis

  show "compact S"
  proof cases
    assume "S = {}"
    then show "compact S" by (simp add: compact_def)
  next
    assume "S ≠ {}"
    show ?thesis
      unfolding compact_def
    proof safe
      fix f :: "nat ==> 'a"
      assume f: "∀n. f n ∈ S"

      define ε where "ε n = 1 / (2 * Suc n)" for n
      then have [simp]: "∧n. 0 < ε n" by auto
      define B where "B n U = (SOME b. infinite {n. f n ∈ b} ∧ (∃x. b ⊆ ball x (ε n) ∩ U))" for n U
      {
        fix n U
        assume "infinite {n. f n ∈ U}"
        then have "∃b∈k (ε n). infinite {i∈{n. f n ∈ U}. f i ∈ ball b (ε n)}"
          using k f by (intro pigeonhole_infinite_rel) (auto simp: subset_eq)
        then obtain a where
          "a ∈ k (ε n)"
          "infinite {i ∈ {n. f n ∈ U}. f i ∈ ball a (ε n)}" ..
        then have "∃b. infinite {i. f i ∈ b} ∧ (∃x. b ⊆ ball x (ε n) ∩ U)"
          by (intro exI[of _ "ball a (ε n) ∩ U"] exI[of _ a]) (auto simp: ac_simps)
        from someI_ex[OF this]
        have "infinite {i. f i ∈ B n U}" "∃x. B n U ⊆ ball x (ε n) ∩ U"
          unfolding B_def by auto
      }
      note B = this

      define F where "F = rec_nat (B 0 UNIV) B"
      {
        fix n
        have "infinite {i. f i ∈ F n}"
          by (induct n) (auto simp: F_def B)
      }
      then have F: "∧n. ∃x. F (Suc n) ⊆ ball x (ε n) ∩ F n"
        using B by (simp add: F_def)
      then have F_dec: "∧m n. m ≤ n ==> F n ⊆ F m"
        using decseq_SucI[of F] by (auto simp: decseq_def)
      have "∃x>i. f x ∈ F k" for k i
      proof -
        have "infinite ({n. f n ∈ F k} - {.. i})"
          using ‹infinite {n. f n ∈ F k}› by auto
        from infinite_imp_nonempty[OF this]
        show "∃x>i. f x ∈ F k"
          by (simp add: set_eq_iff not_le conj_commute)
      qed
      then obtain sel where sel: "∧k i. i < sel k i" "∧k i. f (sel k i) ∈ F k"
        by meson

      define t where "t = rec_nat (sel 0 0) (λn i. sel (Suc n) i)"
      have "strict_mono t"
        unfolding strict_mono_Suc_iff by (simp add: t_def sel)
      moreover have "∀i. (f ∘ t) i ∈ S"
        using f by auto
      moreover
      have t: "(f ∘ t) n ∈ F n" for n
        by (cases n) (simp_all add: t_def sel)

      have "Cauchy (f ∘ t)"
      proof (safe intro!: metric_CauchyI exI elim!: nat_approx_posE)
        fix r :: real and N n m
        assume "1 / Suc N < r" "Suc N ≤ n" "Suc N ≤ m"
        then have "(f ∘ t) n ∈ F (Suc N)" "(f ∘ t) m ∈ F (Suc N)" "2 * ε N < r"
          using F_dec t by (auto simp: ε_def field_simps)
        with F[of N] obtain x where "dist x ((f ∘ t) n) < ε N" "dist x ((f ∘ t) m) < ε N"
          by (auto simp: subset_eq)
        with ‹2 * ε N 🚫› show "dist ((f ∘ t) m) ((f ∘ t) n) < r"
          by metric
      qed

      ultimately show "∃l∈S. ∃r. strict_mono r ∧ (f ∘ r) <---- l"
        using assms unfolding complete_def by blast
    qed
  qed
next
  show "compact S ==> ?rhs"
    by (metis compact_imp_complete compact_imp_seq_compact seq_compact_imp_totally_bounded)
qed 

lemma cauchy_imp_bounded:
  assumes "Cauchy S"
  shows "bounded (range S)"
proof -
  from assms obtain N :: nat where "∀m n. N ≤ m ∧ N ≤ n ⟶ dist (S m) (S n) < 1"
    by (meson Cauchy_def zero_less_one)
  then have N:"∀n. N ≤ n ⟶ dist (S N) (S n) < 1" by auto
  moreover
  have "bounded (S ` {0..N})"
    using finite_imp_bounded[of "S ` {1..N}"] by auto
  then obtain a where a:"∀x∈S ` {0..N}. dist (S N) x ≤ a"
    unfolding bounded_any_center [where a="S N"] by auto
  ultimately have "∀y∈range S. dist (S N) y ≤ max a 1"
    by (force simp: le_max_iff_disj less_le_not_le)
  then show ?thesis
    unfolding bounded_any_center [where a="S N"] by blast
qed

instance heine_borel < complete_space
proof
  fix f :: "nat ==> 'a" assume "Cauchy f"
  then show "convergent f"
    unfolding convergent_def
    using Cauchy_converges_subseq cauchy_imp_bounded bounded_imp_convergent_subsequence by blast
qed

lemma complete_UNIV: "complete (UNIV :: ('a::complete_space) set)"
  by (meson Cauchy_convergent UNIV_I completeI convergent_def)

lemma complete_imp_closed:
  fixes S :: "'a::metric_space set"
  shows "complete S ==> closed S"
  by (metis LIMSEQ_imp_Cauchy LIMSEQ_unique closed_sequential_limits completeE)

lemma complete_Int_closed:
  fixes S :: "'a::metric_space set"
  assumes "complete S" and "closed t"
  shows "complete (S ∩ t)"
  by (metis Int_iff assms closed_sequentially completeE completeI)

lemma complete_closed_subset:
  fixes S :: "'a::metric_space set"
  assumes "closed S" and "S ⊆ t" and "complete t"
  shows "complete S"
  by (metis assms complete_Int_closed inf.absorb_iff2)

lemma complete_eq_closed:
  fixes S :: "('a::complete_space) set"
  shows "complete S ⟷ closed S"
  using complete_UNIV complete_closed_subset complete_imp_closed by auto

lemma convergent_eq_Cauchy:
  fixes S :: "nat ==> 'a::complete_space"
  shows "(∃l. (S ---> l) sequentially) ⟷ Cauchy S"
  unfolding Cauchy_convergent_iff convergent_def ..

lemma convergent_imp_bounded:
  fixes S :: "nat ==> 'a::metric_space"
  shows "(S ---> l) sequentially ==> bounded (range S)"
  by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy)

lemma frontier_subset_compact:
  fixes S :: "'a::heine_borel set"
  shows "compact S ==> frontier S ⊆ S"
  using frontier_subset_closed compact_eq_bounded_closed
  by blast

lemma banach_fix_type:
  fixes f::"'a::complete_space==>'a"
  assumes c:"0 ≤ c" "c < 1"
      and lipschitz:"∀x. ∀y. dist (f x) (f y) ≤ c * dist x y"
  shows "∃!x. (f x = x)"
  using assms Banach_fix[OF complete_UNIV UNIV_not_empty c subset_UNIV, of f]
  by auto

section ‹Cauchy continuity›

definition Cauchy_continuous_on where
  "Cauchy_continuous_on ≡ λS f. ∀σ. Cauchy σ ⟶ range σ ⊆ S ⟶ Cauchy (f ∘ σ)"

lemma continuous_closed_imp_Cauchy_continuous:
  fixes S :: "('a::complete_space) set"
  shows "[continuous_on S f; closed S] ==> Cauchy_continuous_on S f"
  unfolding Cauchy_continuous_on_def
  by (metis LIMSEQ_imp_Cauchy completeE complete_eq_closed continuous_on_sequentially range_subsetD)

lemma uniformly_continuous_imp_Cauchy_continuous:
  fixes f :: "'a::metric_space ==> 'b::metric_space"
  shows "uniformly_continuous_on S f ==> Cauchy_continuous_on S f"
  by (metis (no_types, lifting) ext Cauchy_continuous_on_def UNIV_I image_subset_iff
      o_apply uniformly_continuous_on_Cauchy)

lemma Cauchy_continuous_on_imp_continuous:
  fixes f :: "'a::metric_space ==> 'b::metric_space"
  assumes "Cauchy_continuous_on S f"
  shows "continuous_on S f"
proof -
  have False if x: "∀n. ∃x'∈S. dist x' x < inverse(Suc n) ∧ ¬ dist (f x') (f x) < ε" "ε>0" "x ∈ S" for x and ε::real
  proof -
    obtain ρ where ρ: "∀n. ρ n ∈ S" and dx: "∀n. dist (ρ n) x < inverse(Suc n)" and dfx: "∀n. ¬ dist (f (ρ n)) (f x) < ε"
      using x by metis
    define σ where "σ ≡ λn. if even n then ρ n else x"
    with ρ ‹x ∈ S› have "range σ ⊆ S"
      by auto
    have "σ <---- x"
      unfolding tendsto_iff
    proof (intro strip)
      fix ε :: real
      assume "ε>0"
      then obtain N where "inverse (Suc N) < ε"
        using reals_Archimedean by blast
      then have "∀n. N ≤ n ⟶ dist (ρ n) x < ε"
        by (metis dx inverse_positive_iff_positive le_imp_inverse_le nless_le not_less_eq_eq
            of_nat_mono order_le_less_trans zero_le_dist)
      with ‹ε>0› show "∀🪙F n in sequentially. dist (σ n) x < ε"
        by (auto simp: eventually_sequentially σ_def)
    qed
    then have "Cauchy σ"
      by (intro LIMSEQ_imp_Cauchy)
    then have Cf: "Cauchy (f ∘ σ)"
      by (meson Cauchy_continuous_on_def ‹range σ ⊆ S› assms)
    have "(f ∘ σ) <---- f x"
      unfolding tendsto_iff 
    proof (intro strip)
      fix ε :: real
      assume "ε>0"
      then obtain N where N: "∀m≥N. ∀n≥N. dist ((f ∘ σ) m) ((f ∘ σ) n) < ε"
        using Cf unfolding Cauchy_def by presburger
      moreover have "(f ∘ σ) (Suc(N+N)) = f x"
        by (simp add: σ_def)
      ultimately have "∀n≥N. dist ((f ∘ σ) n) (f x) < ε"
        by (metis add_Suc le_add2)
      then show "∀🪙F n in sequentially. dist ((f ∘ σ) n) (f x) < ε"
        using eventually_sequentially by blast
    qed
    moreover have "∧n. ¬ dist (f (σ (2*n))) (f x) < ε"
      using dfx by (simp add: σ_def)
    ultimately show False
      using ‹ε>0› by (fastforce simp: mult_2 nat_le_iff_add tendsto_iff eventually_sequentially)
  qed
  then show ?thesis
    unfolding continuous_on_iff by (meson inverse_Suc)
qed


section🍋‹tag unimportant›\<open> Finite intersection property›

text‹Also developed in HOL's toplogical spaces theory, but the Heine-Borel type class isn't available there.›

lemma closed_imp_fip:
  fixes S :: "'a::heine_borel set"
  assumes "closed S"
      and T: "T ∈ F" "bounded T"
      and clof: "∧T. T ∈ F ==> closed T"
      and 🍋: "∧F'. [finite F'; F' ⊆ F] ==> S ∩ ∩F' ≠ {}"
    shows "S ∩ ∩F ≠ {}"
proof -
  have "(S ∩ T) ∩ ∩F ≠ {}"
  proof (rule compact_imp_fip)
    show "compact (S ∩ T)"
      using ‹closed S› clof compact_eq_bounded_closed T by blast
  next
    fix F'
    assume "finite F'" and "F' ⊆ F"
    then show "S ∩ T ∩ ∩ F' ≠ {}"
      by (metis Inf_insert Int_assoc ‹T ∈ F› finite_insert insert_subset 🍋)
  qed (simp add: clof)
  then show ?thesis by blast
qed

lemma closed_imp_fip_compact:
  fixes S :: "'a::heine_borel set"
  shows
   "[closed S; ∧T. T ∈ F ==> compact T;
     ∧F'. [finite F'; F' ⊆ F] ==> S ∩ ∩F' ≠ {}] ==> S ∩ ∩F ≠ {}"
  by (metis closed_imp_fip compact_eq_bounded_closed equals0I finite.emptyI order.refl)

lemma closed_fip_Heine_Borel:
  fixes F :: "'a::heine_borel set set"
  assumes "T ∈ F" "bounded T"
      and "∧T. T ∈ F ==> closed T"
      and "∧F'. [finite F'; F' ⊆ F] ==> ∩F' ≠ {}"
    shows "∩F ≠ {}"
  using closed_imp_fip [OF closed_UNIV] assms by auto

lemma compact_fip_Heine_Borel:
  fixes F :: "'a::heine_borel set set"
  assumes clof: "∧T. T ∈ F ==> compact T"
      and none: "∧F'. [finite F'; F' ⊆ F] ==> ∩F' ≠ {}"
    shows "∩F ≠ {}"
  by (metis InterI clof closed_fip_Heine_Borel compact_eq_bounded_closed equals0D none)

lemma compact_sequence_with_limit:
  fixes f :: "nat ==> 'a::heine_borel"
  shows "f <---- l ==> compact (insert l (range f))"
  by (simp add: closed_limpt compact_eq_bounded_closed convergent_imp_bounded islimpt_insert sequence_unique_limpt)


section ‹Properties of Balls and Spheres›

lemma compact_cball[simp]:
  fixes x :: "'a::heine_borel"
  shows "compact (cball x ε)"
  using compact_eq_bounded_closed bounded_cball closed_cball by blast

lemma compact_frontier_bounded[intro]:
  fixes S :: "'a::heine_borel set"
  shows "bounded S ==> compact (frontier S)"
  unfolding frontier_def
  using compact_eq_bounded_closed by blast

lemma compact_frontier[intro]:
  fixes S :: "'a::heine_borel set"
  shows "compact S ==> compact (frontier S)"
  using compact_eq_bounded_closed compact_frontier_bounded by blast

lemma no_limpt_imp_countable:
  assumes "∧z. ¬z islimpt (X :: 'a :: {real_normed_vector, heine_borel} set)"
  shows   "countable X"
proof -
  have "countable (∪n. cball 0 (real n) ∩ X)"
  proof (intro countable_UN[OF _ countable_finite])
    fix n :: nat
    show "finite (cball 0 (real n) ∩ X)"
      using assms by (intro finite_not_islimpt_in_compact) auto
  qed auto
  also have "(∪n. cball 0 (real n)) = (UNIV :: 'a set)"
    by (force simp: real_arch_simple)
  hence "(∪n. cball 0 (real n) ∩ X) = X"
    by blast
  finally show "countable X" .
qed


section ‹Distance from a Set›

lemma distance_attains_sup:
  assumes "compact S" "S ≠ {}"
  shows "∃x∈S. ∀y∈S. dist a y ≤ dist a x"
proof (rule continuous_attains_sup [OF assms])
  show "continuous_on S (dist a)"
    unfolding continuous_on
    using Lim_at_imp_Lim_at_within continuous_at_dist isCont_def by blast
qed

text ‹For \emph{minimal} distance, we only need closure, not compactness.›

lemma distance_attains_inf:
  fixes a :: "'a::heine_borel"
  assumes "closed S" and "S ≠ {}"
  obtains x where "x∈S" "∧y. y ∈ S ==> dist a x ≤ dist a y"
proof -
  from assms obtain b where "b ∈ S" by auto
  let ?B = "S ∩ cball a (dist b a)"
  have "?B ≠ {}" using ‹b ∈ S›
    by (auto simp: dist_commute)
  moreover have "continuous_on ?B (dist a)"
    by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)
  moreover have "compact ?B"
    by (intro closed_Int_compact ‹closed S› compact_cball)
  ultimately obtain x where "x ∈ ?B" "∀y∈?B. dist a x ≤ dist a y"
    by (metis continuous_attains_inf)
  with that show ?thesis by fastforce
qed


section ‹Infimum Distance›

definition🍋‹tag important› "infdist x A = (if A = {} then 0 else INF a∈A. dist x a)"

lemma bdd_below_image_dist[intro, simp]: "bdd_below (dist x ` A)"
  by (auto intro!: zero_le_dist)

lemma infdist_notempty: "A ≠ {} ==> infdist x A = (INF a∈A. dist x a)"
  by (simp add: infdist_def)

lemma infdist_nonneg: "0 ≤ infdist x A"
  by (auto simp: infdist_def intro: cINF_greatest)

lemma infdist_le: "a ∈ A ==> infdist x A ≤ dist x a"
  by (auto intro: cINF_lower simp add: infdist_def)

lemma infdist_le2: "a ∈ A ==> dist x a ≤ δ ==> infdist x A ≤ δ"
  by (auto intro!: cINF_lower2 simp add: infdist_def)

lemma infdist_zero[simp]: "a ∈ A ==> infdist a A = 0"
  by (auto intro!: antisym infdist_nonneg infdist_le2)

lemma infdist_Un_min:
  assumes "A ≠ {}" "B ≠ {}"
  shows "infdist x (A ∪ B) = min (infdist x A) (infdist x B)"
using assms by (simp add: infdist_def cINF_union inf_real_def)

lemma infdist_triangle: "infdist x A ≤ infdist y A + dist x y"
proof (cases "A = {}")
  case True
  then show ?thesis by (simp add: infdist_def)
next
  case False
  then obtain a where "a ∈ A" by auto
  have "infdist x A ≤ Inf {dist x y + dist y a |a. a ∈ A}"
  proof (rule cInf_greatest)
    from ‹A ≠ {}› show "{dist x y + dist y a |a. a ∈ A} ≠ {}"
      by simp
    fix δ
    assume "δ ∈ {dist x y + dist y a |a. a ∈ A}"
    then obtain a where δ: "δ = dist x y + dist y a" "a ∈ A"
      by auto
    show "infdist x A ≤ δ"
      using infdist_notempty[OF ‹A ≠ {}›]
      by (metis δ dist_commute dist_triangle3 infdist_le2)
  qed
  also have "… = dist x y + infdist y A"
  proof (rule cInf_eq, safe)
    fix a
    assume "a ∈ A"
    then show "dist x y + infdist y A ≤ dist x y + dist y a"
      by (auto intro: infdist_le)
  next
    fix i
    assume inf: "∧δ. δ ∈ {dist x y + dist y a |a. a ∈ A} ==> i ≤ δ"
    then have "i - dist x y ≤ infdist y A"
      unfolding infdist_notempty[OF ‹A ≠ {}›] using ‹a ∈ A›
      by (intro cINF_greatest) (auto simp: field_simps)
    then show "i ≤ dist x y + infdist y A"
      by simp
  qed
  finally show ?thesis by simp
qed

lemma infdist_triangle_abs: "∣infdist x A - infdist y A∣ ≤ dist x y"
  by (metis abs_diff_le_iff diff_le_eq dist_commute infdist_triangle)

lemma in_closure_iff_infdist_zero:
  assumes "A ≠ {}"
  shows "x ∈ closure A ⟷ infdist x A = 0"
proof
  assume "x ∈ closure A"
  show "infdist x A = 0"
  proof (rule ccontr)
    assume "infdist x A ≠ 0"
    with infdist_nonneg[of x A] have "infdist x A > 0"
      by auto
    then have "ball x (infdist x A) ∩ closure A = {}"
      by (meson ‹x ∈ closure A› closure_approachableD infdist_le linorder_not_le)
    then have "x ∉ closure A"
      by (metis ‹0 🚫 x A› centre_in_ball disjoint_iff_not_equal)
    then show False using ‹x ∈ closure A› by simp
  qed
next
  assume x: "infdist x A = 0"
  then obtain a where "a ∈ A"
    by atomize_elim (metis all_not_in_conv assms)
  have False if "ε > 0" "¬ (∃y∈A. dist y x < ε)" for ε
  proof -
    have "infdist x A ≥ ε" using ‹a ∈ A›
      unfolding infdist_def using that
      by (force simp: dist_commute intro: cINF_greatest)
    with x ‹ε > 0› show False by auto
  qed
  then show "x ∈ closure A"
    using closure_approachable by blast
qed

lemma in_closed_iff_infdist_zero:
  assumes "closed A" "A ≠ {}"
  shows "x ∈ A ⟷ infdist x A = 0"
  by (metis assms closure_closed in_closure_iff_infdist_zero)

lemma infdist_pos_not_in_closed:
  assumes "closed S" "S ≠ {}" "x ∉ S"
  shows "infdist x S > 0"
  by (meson assms dual_order.order_iff_strict in_closed_iff_infdist_zero infdist_nonneg)

lemma
  infdist_attains_inf:
  fixes X::"'a::heine_borel set"
  assumes "closed X"
  assumes "X ≠ {}"
  obtains x where "x ∈ X" "infdist y X = dist y x"
proof -
  have "bdd_below (dist y ` X)"
    by auto
  from distance_attains_inf[OF assms, of y]
  obtain x where "x ∈ X" "∧z. z ∈ X ==> dist y x ≤ dist y z" by auto
  then have "infdist y X = dist y x"
    by (metis antisym assms(2) cINF_greatest infdist_def infdist_le)
  with ‹x ∈ X› show ?thesis ..
qed


text ‹Every metric space is a T4 space:›

instance metric_space ⊆ t4_space
proof
  fix S T::"'a set" assume H: "closed S" "closed T" "S ∩ T = {}"
  consider "S = {}" | "T = {}" | "S ≠ {} ∧ T ≠ {}" by auto
  then show "∃U V. open U ∧ open V ∧ S ⊆ U ∧ T ⊆ V ∧ U ∩ V = {}"
  proof (cases)
    case 1 then show ?thesis by blast
  next
    case 2 then show ?thesis by blast
  next
    case 3
    define U where "U = (∪x∈S. ball x ((infdist x T)/2))"
    have A: "open U" unfolding U_def by auto
    have "infdist x T > 0" if "x ∈ S" for x
      using H that 3 by (auto intro!: infdist_pos_not_in_closed)
    then have B: "S ⊆ U" unfolding U_def by auto
    define V where "V = (∪x∈T. ball x ((infdist x S)/2))"
    have C: "open V" unfolding V_def by auto
    have "infdist x S > 0" if "x ∈ T" for x
      using H that 3 by (auto intro!: infdist_pos_not_in_closed)
    then have D: "T ⊆ V" unfolding V_def by auto

    have "(ball x ((infdist x T)/2)) ∩ (ball y ((infdist y S)/2)) = {}" if "x ∈ S" "y ∈ T" for x y
    proof auto
      fix z assume H: "dist x z * 2 < infdist x T" "dist y z * 2 < infdist y S"
      have "2 * dist x y ≤ 2 * dist x z + 2 * dist y z"
        by metric
      also have "… < infdist x T + infdist y S"
        using H by auto
      finally have "dist x y < infdist x T ∨ dist x y < infdist y S"
        by auto
      then show False
        using infdist_le[OF ‹x ∈ S›, of y] infdist_le[OF ‹y ∈ T›, of x] by (auto simp: dist_commute)
    qed
    then have E: "U ∩ V = {}"
      unfolding U_def V_def by auto
    show ?thesis
      using A B C D E by blast
  qed
qed

lemma tendsto_infdist [tendsto_intros]:
  assumes f: "(f ---> l) F"
  shows "((λx. infdist (f x) A) ---> infdist l A) F"
proof (rule tendstoI)
  fix ε ::real
  assume "ε > 0"
  from tendstoD[OF f this]
  show "eventually (λx. dist (infdist (f x) A) (infdist l A) < ε) F"
  proof (eventually_elim)
    fix x
    from infdist_triangle[of l A "f x"] infdist_triangle[of "f x" A l]
    have "dist (infdist (f x) A) (infdist l A) ≤ dist (f x) l"
      by (simp add: dist_commute dist_real_def)
    also assume "dist (f x) l < ε"
    finally show "dist (infdist (f x) A) (infdist l A) < ε" .
  qed
qed

lemma continuous_infdist[continuous_intros]:
  assumes "continuous F f"
  shows "continuous F (λx. infdist (f x) A)"
  using assms unfolding continuous_def by (rule tendsto_infdist)

lemma continuous_on_infdist [continuous_intros]:
  assumes "continuous_on S f"
  shows "continuous_on S (λx. infdist (f x) A)"
using assms unfolding continuous_on by (auto intro: tendsto_infdist)

lemma compact_infdist_le:
  fixes A::"'a::heine_borel set"
  assumes "A ≠ {}"
  assumes "compact A"
  assumes "ε > 0"
  shows "compact {x. infdist x A ≤ ε}"
proof -
  from continuous_closed_vimage[of "{0..ε}" "λx. infdist x A"]
    continuous_infdist[OF continuous_ident, of _ UNIV A]
  have "closed {x. infdist x A ≤ ε}" by (auto simp: vimage_def infdist_nonneg)
  moreover
  from assms obtain x0 b where b: "∧x. x ∈ A ==> dist x0 x ≤ b" "closed A"
    by (auto simp: compact_eq_bounded_closed bounded_def)
  {
    fix y
    assume "infdist y A ≤ ε"
    moreover
    from infdist_attains_inf[OF ‹closed A› ‹A ≠ {}›, of y]
    obtain z where "z ∈ A" "infdist y A = dist y z" by blast
    ultimately
    have "dist x0 y ≤ b + ε" using b by metric
  } then
  have "bounded {x. infdist x A ≤ ε}"
    by (auto simp: bounded_any_center[where a=x0] intro!: exI[where x="b + ε"])
  ultimately show "compact {x. infdist x A ≤ ε}"
    by (simp add: compact_eq_bounded_closed)
qed


section ‹Separation between Points and Sets›

proposition separate_point_closed:
  fixes S :: "'a::heine_borel set"
  assumes "closed S" and "a ∉ S"
  shows "∃δ>0. ∀x∈S. δ ≤ dist a x"
  by (metis assms distance_attains_inf empty_iff gt_ex zero_less_dist_iff)

proposition separate_compact_closed:
  fixes S T :: "'a::heine_borel set"
  assumes "compact S"
    and T: "closed T" "S ∩ T = {}"
  shows "∃δ>0. ∀x∈S. ∀y∈T. δ ≤ dist x y"
proof cases
  assume "S ≠ {} ∧ T ≠ {}"
  then have "S ≠ {}" "T ≠ {}" by auto
  let ?inf = "λx. infdist x T"
  have "continuous_on S ?inf"
    by (auto intro!: continuous_at_imp_continuous_on continuous_infdist continuous_ident)
  then obtain x where x: "x ∈ S" "∀y∈S. ?inf x ≤ ?inf y"
    using continuous_attains_inf[OF ‹compact S› ‹S ≠ {}›] by auto
  then have "0 < ?inf x"
    using T ‹T ≠ {}› in_closed_iff_infdist_zero by (auto simp: less_le infdist_nonneg)
  moreover have "∀x'∈S. ∀y∈T. ?inf x ≤ dist x' y"
    using x by (auto intro: order_trans infdist_le)
  ultimately show ?thesis by auto
qed (auto intro!: exI[of _ 1])

proposition separate_closed_compact:
  fixes S T :: "'a::heine_borel set"
  assumes S: "closed S"
    and T: "compact T"
    and dis: "S ∩ T = {}"
  shows "∃δ>0. ∀x∈S. ∀y∈T. δ ≤ dist x y"
  by (metis separate_compact_closed[OF T S] dis dist_commute inf_commute)

proposition compact_in_open_separated:
  fixes A::"'a::heine_borel set"
  assumes A: "A ≠ {}" "compact A"
  assumes "open B"
  assumes "A ⊆ B"
  obtains ε where "ε > 0" "{x. infdist x A ≤ ε} ⊆ B"
proof atomize_elim
  have "closed (- B)" "compact A" "- B ∩ A = {}"
    using assms by (auto simp: open_Diff compact_eq_bounded_closed)
  from separate_closed_compact[OF this]
  obtain d'::real where d': "d'>0" "∧x y. x ∉ B ==> y ∈ A ==> d' ≤ dist x y"
    by auto
  define δ where "δ = d' / 2"
  hence "δ>0" "δ < d'" using d' by auto
  with d' have δ: "∧x y. x ∉ B ==> y ∈ A ==> δ < dist x y"
    by force
  show "∃ε>0. {x. infdist x A ≤ ε} ⊆ B"
  proof (rule ccontr)
    assume "∄ε. 0 < ε ∧ {x. infdist x A ≤ ε} ⊆ B"
    with ‹δ > 0› obtain x where x: "infdist x A ≤ δ" "x ∉ B"
      by auto
    then show False
      by (metis A compact_eq_bounded_closed infdist_attains_inf x δ linorder_not_less)
  qed
qed


section ‹Uniform Continuity›

lemma uniformly_continuous_onE:
  assumes "uniformly_continuous_on s f" "0 < ε"
  obtains δ where "δ>0" "∧x x'. [x∈s; x'∈s; dist x' x < δ] ==> dist (f x') (f x) < ε"
  using assms
  by (auto simp: uniformly_continuous_on_def)

lemma uniformly_continuous_on_sequentially:
  "uniformly_continuous_on s f ⟷ (∀x y. (∀n. x n ∈ s) ∧ (∀n. y n ∈ s) ∧
    (λn. dist (x n) (y n)) <---- 0 ⟶ (λn. dist (f(x n)) (f(y n))) <---- 0)" (is "?lhs = ?rhs")
proof
  assume ?lhs
  {
    fix x y
    assume x: "∀n. x n ∈ s"
      and y: "∀n. y n ∈ s"
      and xy: "((λn. dist (x n) (y n)) ---> 0) sequentially"
    {
      fix ε :: real
      assume "ε > 0"
      then obtain δ where "δ > 0" and δ: "∀x∈s. ∀x'∈s. dist x' x < δ ⟶ dist (f x') (f x) < ε"
        by (metis ‹?lhs› uniformly_continuous_onE)
      obtain N where N: "∀n≥N. dist (x n) (y n) < δ"
        using xy[unfolded lim_sequentially dist_norm] and ‹δ>0› by auto
      then have "∃N. ∀n≥N. dist (f (x n)) (f (y n)) < ε"
        using δ x y by blast
    }
    then have "((λn. dist (f(x n)) (f(y n))) ---> 0) sequentially"
      unfolding lim_sequentially and dist_real_def by auto
  }
  then show ?rhs by auto
next
  assume ?rhs
  {
    assume "¬ ?lhs"
    then obtain ε where "ε > 0" "∀δ>0. ∃x∈s. ∃x'∈s. dist x' x < δ ∧ ¬ dist (f x') (f x) < ε"
      unfolding uniformly_continuous_on_def by auto
    then obtain fa where fa:
      "∀x. 0 < x ⟶ fst (fa x) ∈ s ∧ snd (fa x) ∈ s ∧ dist (fst (fa x)) (snd (fa x)) < x ∧ ¬ dist (f (fst (fa x))) (f (snd (fa x))) < ε"
      using choice[of "λδ x. δ>0 ⟶ fst x ∈ s ∧ snd x ∈ s ∧ dist (snd x) (fst x) < δ ∧ ¬ dist (f (snd x)) (f (fst x)) < ε"]
      by (auto simp: Bex_def dist_commute)
    define x where "x n = fst (fa (inverse (real n + 1)))" for n
    define y where "y n = snd (fa (inverse (real n + 1)))" for n
    have xyn: "∀n. x n ∈ s ∧ y n ∈ s"
      and xy0: "∀n. dist (x n) (y n) < inverse (real n + 1)"
      and fxy:"∀n. ¬ dist (f (x n)) (f (y n)) < ε"
      unfolding x_def and y_def using fa
      by auto
    {
      fix ε :: real
      assume "ε > 0"
      then obtain N :: nat where "N ≠ 0" and N: "0 < inverse (real N) ∧ inverse (real N) < ε"
        unfolding real_arch_inverse[of ε] by auto
      with xy0 have "∃N. ∀n≥N. dist (x n) (y n) < ε"
        by (metis order.strict_trans inverse_positive_iff_positive less_imp_inverse_less
            nat_le_real_less)
    }
    then have "∀ε>0. ∃N. ∀n≥N. dist (f (x n)) (f (y n)) < ε"
      using ‹?rhs› xyn by (auto simp: lim_sequentially dist_real_def)
    then have False using fxy and ‹ε>0› by auto
  }
  then show ?lhs
    unfolding uniformly_continuous_on_def by blast
qed


section ‹Continuity on a Compact Domain Implies Uniform Continuity›

text‹From the proof of the Heine-Borel theorem: Lemma 2 in section 3.7, page 69 of
 J. C. Burkill and H. Burkill. A Second Course in Mathematical Analysis (CUP, 2002)›

lemma Heine_Borel_lemma:
  assumes "compact S" and Ssub: "S ⊆ ∪G" and opn: "∧G. G ∈ G ==> open G"
  obtains ε where "0 < ε" "∧x. x ∈ S ==> ∃G ∈ G. ball x ε ⊆ G"
proof -
  have False if neg: "∧ε. 0 < ε ==> ∃x ∈ S. ∀G ∈ G. ¬ ball x ε ⊆ G"
  proof -
    have "∃x ∈ S. ∀G ∈ G. ¬ ball x (1 / Suc n) ⊆ G" for n
      using neg by simp
    then obtain f where "∧n. f n ∈ S" and fG: "∧G n. G ∈ G ==> ¬ ball (f n) (1 / Suc n) ⊆ G"
      by metis
    then obtain l r where "l ∈ S" "strict_mono r" and to_l: "(f ∘ r) <---- l"
      using ‹compact S› compact_def that by metis
    then obtain G where "l ∈ G" "G ∈ G"
      using Ssub by auto
    then obtain ε where "0 < ε" and ε: "∧z. dist z l < ε ==> z ∈ G"
      using opn open_dist by blast
    obtain N1 where N1: "∧n. n ≥ N1 ==> dist (f (r n)) l < ε/2"
      by (metis ‹0 🚫ε› half_gt_zero lim_sequentially o_apply to_l)
    obtain N2 where N2: "of_nat N2 > 2/ε"
      using reals_Archimedean2 by blast
    obtain x where "x ∈ ball (f (r (max N1 N2))) (1 / real (Suc (r (max N1 N2))))" and "x ∉ G"
      using fG [OF ‹G ∈ G›, of "r (max N1 N2)"] by blast
    then have "dist (f (r (max N1 N2))) x < 1 / real (Suc (r (max N1 N2)))"
      by simp
    also have "… ≤ 1 / real (Suc (max N1 N2))"
      by (meson Suc_le_mono ‹strict_mono r› inverse_of_nat_le nat.discI seq_suble)
    also have "… ≤ 1 / real (Suc N2)"
      by (simp add: field_simps)
    also have "… < ε/2"
      using N2 ‹0 🚫ε› by (simp add: field_simps)
    finally have "dist (f (r (max N1 N2))) x < ε/2" .
    moreover have "dist (f (r (max N1 N2))) l < ε/2"
      using N1 max.cobounded1 by blast
    ultimately have "dist x l < ε"
      by metric
    then show ?thesis
      using ε ‹x ∉ G› by blast
  qed
  then show ?thesis
    by (meson that)
qed

lemma compact_uniformly_equicontinuous:
  assumes "compact S"
      and cont: "∧x ε. [x ∈ S; 0 < ε]
                        ==> ∃δ. 0 < δ ∧
                                (∀f ∈ F. ∀x' ∈ S. dist x' x < δ ⟶ dist (f x') (f x) < ε)"
      and "0 < ε"
  obtains δ where "0 < δ"
                  "∧f x x'. [f ∈ F; x ∈ S; x' ∈ S; dist x' x < δ] ==> dist (f x') (f x) < ε"
proof -
  obtain δ where d_pos: "∧x ε. [x ∈ S; 0 < ε] ==> 0 < δ x ε"
     and d_dist : "∧x x' ε f. [dist x' x < δ x ε; x ∈ S; x' ∈ S; 0 < ε; f ∈ F] ==> dist (f x') (f x) < ε"
    using cont by metis
  let ?G = "((λx. ball x (δ x (ε/2))) ` S)"
  have Ssub: "S ⊆ ∪ ?G"
    using ‹0 🚫ε› d_pos by auto
  then obtain k where "0 < k" and k: "∧x. x ∈ S ==> ∃G ∈ ?G. ball x k ⊆ G"
    by (rule Heine_Borel_lemma [OF ‹compact S›]) auto
  moreover have "dist (f v) (f u) < ε" if "f ∈ F" "u ∈ S" "v ∈ S" "dist v u < k" for f u v
  proof -
    obtain G where "G ∈ ?G" "u ∈ G" "v ∈ G"
      using k that
      by (metis ‹dist v u 🚫› ‹u ∈ S› ‹0 🚫› centre_in_ball subsetD dist_commute mem_ball)
    then obtain w where w: "dist w u < δ w (ε/2)" "dist w v < δ w (ε/2)" "w ∈ S"
      by auto
    with that d_dist have "dist (f w) (f v) < ε/2"
      by (metis ‹0 🚫ε› dist_commute half_gt_zero)
    moreover
    have "dist (f w) (f u) < ε/2"
      using that d_dist w by (metis ‹0 🚫ε› dist_commute divide_pos_pos zero_less_numeral)
    ultimately show ?thesis
      using dist_triangle_half_r by blast
  qed
  ultimately show ?thesis using that by blast
qed

corollary compact_uniformly_continuous:
  fixes f :: "'a :: metric_space ==> 'b :: metric_space"
  assumes f: "continuous_on S f" and S: "compact S"
  shows "uniformly_continuous_on S f"
  using f
    unfolding continuous_on_iff uniformly_continuous_on_def
    by (force intro: compact_uniformly_equicontinuous [OF S, of "{f}"])


section🍋‹tag unimportant›\<open> Theorems relating continuity and uniform continuity to closures›

lemma continuous_on_closure:
   "continuous_on (closure S) f ⟷
    (∀x ε. x ∈ closure S ∧ 0 < ε
           ⟶ (∃δ. 0 < δ ∧ (∀y. y ∈ S ∧ dist y x < δ ⟶ dist (f y) (f x) < ε)))"
   (is "?lhs = ?rhs")
proof
  assume ?lhs then show ?rhs
    unfolding continuous_on_iff  by (metis Un_iff closure_def)
next
  assume R [rule_format]: ?rhs
  show ?lhs
  proof
    fix x and ε::real
    assume "0 < ε" and x: "x ∈ closure S"
    obtain δ::real where "δ > 0"
                   and δ: "∧y. [y ∈ S; dist y x < δ] ==> dist (f y) (f x) < ε/2"
      using R [of x "ε/2"] ‹0 🚫ε› x by auto
    have "dist (f y) (f x) ≤ ε" if y: "y ∈ closure S" and dyx: "dist y x < δ/2" for y
    proof -
      obtain δ'::real where "δ' > 0"
                      and δ': "∧z. [z ∈ S; dist z y < δ'] ==> dist (f z) (f y) < ε/2"
        using R [of y "ε/2"] ‹0 🚫ε› y by auto
      obtain z where "z ∈ S" and z: "dist z y < min δ' δ / 2"
        using closure_approachable y
        by (metis ‹0 🚫δ'› ‹0 🚫δ› divide_pos_pos min_less_iff_conj zero_less_numeral)
      have "dist (f z) (f y) < ε/2"
        using δ' [OF ‹z ∈ S›] z ‹0 🚫δ'› by metric
      moreover have "dist (f z) (f x) < ε/2"
        using δ[OF ‹z ∈ S›] z dyx by metric
      ultimately show ?thesis
        by metric
    qed
    then show "∃δ>0. ∀x'∈closure S. dist x' x < δ ⟶ dist (f x') (f x) ≤ ε"
      by (rule_tac x="δ/2" in exI) (simp add: ‹δ > 0›)
  qed
qed

lemma continuous_on_closure_sequentially:
  fixes f :: "'a::metric_space ==> 'b :: metric_space"
  shows
   "continuous_on (closure S) f ⟷
    (∀x a. a ∈ closure S ∧ (∀n. x n ∈ S) ∧ x <---- a ⟶ (f ∘ x) <---- f a)"
   (is "?lhs = ?rhs")
proof -
  have "continuous_on (closure S) f ⟷
        (∀x ∈ closure S. continuous (at x within S) f)"
    by (force simp: continuous_on_closure continuous_within_eps_delta)
  also have "… = ?rhs"
    by (force simp: continuous_within_sequentially)
  finally show ?thesis .
qed

lemma uniformly_continuous_on_closure:
  fixes f :: "'a::metric_space ==> 'b::metric_space"
  assumes ucont: "uniformly_continuous_on S f"
      and cont: "continuous_on (closure S) f"
    shows "uniformly_continuous_on (closure S) f"
unfolding uniformly_continuous_on_def
proof (intro allI impI)
  fix ε::real
  assume "0 < ε"
  then obtain δ::real
    where "δ>0"
      and δ: "∧x x'. [x∈S; x'∈S; dist x' x < δ] ==> dist (f x') (f x) < ε/3"
    using ucont [unfolded uniformly_continuous_on_def, rule_format, of "ε/3"] by auto
  show "∃δ>0. ∀x∈closure S. ∀x'∈closure S. dist x' x < δ ⟶ dist (f x') (f x) < ε"
  proof (rule exI [where x="δ/3"], clarsimp simp: ‹δ > 0›)
    fix x y
    assume x: "x ∈ closure S" and y: "y ∈ closure S" and dyx: "dist y x * 3 < δ"
    obtain d1::real where "d1 > 0"
           and d1: "∧w. [w ∈ closure S; dist w x < d1] ==> dist (f w) (f x) < ε/3"
      using cont [unfolded continuous_on_iff, rule_format, of "x" "ε/3"] ‹0 🚫ε› x by auto
     obtain x' where "x' ∈ S" and x': "dist x' x < min d1 (δ / 3)"
        using closure_approachable [of x S]
        by (metis ‹0 🚫› ‹0 🚫δ› divide_pos_pos min_less_iff_conj x zero_less_numeral)
    obtain d2::real where "d2 > 0"
           and d2: "∀w ∈ closure S. dist w y < d2 ⟶ dist (f w) (f y) < ε/3"
      using cont [unfolded continuous_on_iff, rule_format, of "y" "ε/3"] ‹0 🚫ε› y by auto
    obtain y' where "y' ∈ S" and y': "dist y' y < min d2 (δ / 3)"
      using closure_approachable [of y S]
      by (metis ‹0 🚫› ‹0 🚫δ› divide_pos_pos min_less_iff_conj y zero_less_numeral)
    have "dist x' x < δ/3" using x' by auto
    then have "dist x' y' < δ"
      using dyx y' by metric
    then have "dist (f x') (f y') < ε/3"
      by (rule δ [OF ‹y' ∈ S› ‹x' ∈ S›])
    moreover have "dist (f x') (f x) < ε/3" using ‹x' ∈ S› closure_subset x' d1
      by (simp add: closure_def)
    moreover have "dist (f y') (f y) < ε/3" using ‹y' ∈ S› closure_subset y' d2
      by (simp add: closure_def)
    ultimately show "dist (f y) (f x) < ε" by metric
  qed
qed

lemma uniformly_continuous_on_extension_at_closure:
  fixes f::"'a::metric_space ==> 'b::complete_space"
  assumes uc: "uniformly_continuous_on X f"
  assumes "x ∈ closure X"
  obtains l where "(f ---> l) (at x within X)"
proof -
  from assms obtain xs where xs: "xs <---- x" "∧n. xs n ∈ X"
    by (auto simp: closure_sequential)

  from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF xs]
  obtain l where l: "(λn. f (xs n)) <---- l"
    by atomize_elim (simp only: convergent_eq_Cauchy)

  have "(f ---> l) (at x within X)"
  proof (clarify intro!: Lim_within_LIMSEQ)
    fix xs'
    assume "∀n. xs' n ≠ x ∧ xs' n ∈ X"
      and xs': "xs' <---- x"
    then have "xs' n ≠ x" "xs' n ∈ X" for n by auto

    from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF ‹xs' <---- x› ‹xs' _ ∈ X›]
    obtain l' where l': "(λn. f (xs' n)) <---- l'"
      by atomize_elim (simp only: convergent_eq_Cauchy)

    show "(λn. f (xs' n)) <---- l"
    proof (rule tendstoI)
      fix ε::real assume "ε > 0"
      define e' where "e' ≡ ε/2"
      have "e' > 0" using ‹ε > 0› by (simp add: e'_def)

      have "∀🪙F n in sequentially. dist (f (xs n)) l < e'"
        by (simp add: ‹0 🚫'› l tendstoD)
      moreover
      obtain δ where δ: "δ > 0" "∧x x'. x ∈ X ==> x' ∈ X ==> dist x x' < δ ==> dist (f x) (f x') < e'"
        by (metis ‹0 🚫'› uc uniformly_continuous_on_def)
      have "∀🪙F n in sequentially. dist (xs n) (xs' n) < δ"
        by (auto intro!: ‹0 🚫δ› order_tendstoD tendsto_eq_intros xs xs')
      ultimately
      show "∀🪙F n in sequentially. dist (f (xs' n)) l < ε"
      proof eventually_elim
        case (elim n)
        have "dist (f (xs' n)) l ≤ dist (f (xs n)) (f (xs' n)) + dist (f (xs n)) l"
          by metric
        also have "dist (f (xs n)) (f (xs' n)) < e'"
          by (auto intro!: δ xs ‹xs' _ ∈ _› elim)
        also note ‹dist (f (xs n)) l 🚫'›
        also have "e' + e' = ε" by (simp add: e'_def)
        finally show ?case by simp
      qed
    qed
  qed
  thus ?thesis ..
qed

lemma uniformly_continuous_on_extension_on_closure:
  fixes f::"'a::metric_space ==> 'b::complete_space"
  assumes uc: "uniformly_continuous_on X f"
  obtains g where "uniformly_continuous_on (closure X) g" "∧x. x ∈ X ==> f x = g x"
    "∧Y h x. X ⊆ Y ==> Y ⊆ closure X ==> continuous_on Y h ==> (∧x. x ∈ X ==> f x = h x) ==> x ∈ Y ==> h x = g x"
proof -
  from uc have cont_f: "continuous_on X f"
    by (simp add: uniformly_continuous_imp_continuous)
  obtain y where y: "(f ---> y x) (at x within X)" if "x ∈ closure X" for x
    using uniformly_continuous_on_extension_at_closure[OF assms] by meson
  let ?g = "λx. if x ∈ X then f x else y x"

  have "uniformly_continuous_on (closure X) ?g"
    unfolding uniformly_continuous_on_def
  proof safe
    fix ε::real assume "ε > 0"
    define e' where "e' ≡ ε / 3"
    have "e' > 0" using ‹ε > 0› by (simp add: e'_def)
    obtain δ where "δ > 0" and δ: "∧x x'. x ∈ X ==> x' ∈ X ==> dist x' x < δ ==> dist (f x') (f x) < e'"
      using ‹0 🚫'› uc uniformly_continuous_onE by blast
    define d' where "d' = δ / 3"
    have "d' > 0" using ‹δ > 0› by (simp add: d'_def)
    show "∃δ>0. ∀x∈closure X. ∀x'∈closure X. dist x' x < δ ⟶ dist (?g x') (?g x) < ε"
    proof (safe intro!: exI[where x=d'] ‹d' > 0›)
      fix x x' assume x: "x ∈ closure X" and x': "x' ∈ closure X" and dist: "dist x' x < d'"
      then obtain xs xs' where xs: "xs <---- x" "∧n. xs n ∈ X"
        and xs': "xs' <---- x'" "∧n. xs' n ∈ X"
        by (auto simp: closure_sequential)
      have "∀🪙F n in sequentially. dist (xs' n) x' < d'"
        and "∀🪙F n in sequentially. dist (xs n) x < d'"
        by (auto intro!: ‹0 🚫'› order_tendstoD tendsto_eq_intros xs xs')
      moreover
      have "(λx. f (xs x)) <---- y x" 
        if "x ∈ closure X" "x ∉ X" "xs <---- x" "∧n. xs n ∈ X" for xs x
        using that not_eventuallyD
        by (force intro!: filterlim_compose[OF y[OF ‹x ∈ closure X›]] simp: filterlim_at)
      then have "(λx. f (xs' x)) <---- ?g x'" "(λx. f (xs x)) <---- ?g x"
        using x x'
        by (auto intro!: continuous_on_tendsto_compose[OF cont_f] simp: xs' xs)
      then have "∀🪙F n in sequentially. dist (f (xs' n)) (?g x') < e'"
        "∀🪙F n in sequentially. dist (f (xs n)) (?g x) < e'"
        by (auto intro!: ‹0 🚫'› order_tendstoD tendsto_eq_intros)
      ultimately
      have "∀🪙F n in sequentially. dist (?g x') (?g x) < ε"
      proof eventually_elim
        case (elim n)
        have "dist (?g x') (?g x) ≤
          dist (f (xs' n)) (?g x') + dist (f (xs' n)) (f (xs n)) + dist (f (xs n)) (?g x)"
          by (metis add.commute add_le_cancel_left dist_commute dist_triangle dist_triangle_le)
        also
        from ‹dist (xs' n) x' 🚫'› ‹dist x' x 🚫'› ‹dist (xs n) x 🚫'›
        have "dist (xs' n) (xs n) < δ" unfolding d'_def by metric
        with ‹xs _ ∈ X› ‹xs' _ ∈ X› have "dist (f (xs' n)) (f (xs n)) < e'"
          by (rule δ)
        also note ‹dist (f (xs' n)) (?g x') 🚫'›
        also note ‹dist (f (xs n)) (?g x) 🚫'›
        finally show ?case by (simp add: e'_def)
      qed
      then show "dist (?g x') (?g x) < ε" by simp
    qed
  qed
  moreover have "f x = ?g x" if "x ∈ X" for x
    using that by simp
  moreover
  {
    fix Y h x
    assume Y: "x ∈ Y" "X ⊆ Y" "Y ⊆ closure X" and cont_h: "continuous_on Y h"
      and extension: "(∧x. x ∈ X ==> f x = h x)"
    {
      assume "x ∉ X"
      have "x ∈ closure X" using Y by auto
      then obtain xs where xs: "xs <---- x" "∧n. xs n ∈ X"
        by (auto simp: closure_sequential)
      from continuous_on_tendsto_compose[OF cont_h xs(1)] xs(2) Y
      have hx: "(λx. f (xs x)) <---- h x"
        by (auto simp: subsetD extension)
      then have "(λx. f (xs x)) <---- y x"
        using ‹x ∉ X› not_eventuallyD xs(2)
        by (force intro!: filterlim_compose[OF y[OF ‹x ∈ closure X›]] simp: filterlim_at xs)
      with hx have "h x = y x" by (rule LIMSEQ_unique)
    } 
    then have "h x = ?g x"
      using extension by auto
  }
  ultimately show ?thesis ..
qed

lemma bounded_uniformly_continuous_image:
  fixes f :: "'a :: heine_borel ==> 'b :: heine_borel"
  assumes "uniformly_continuous_on S f" "bounded S"
  shows "bounded(f ` S)"
proof -
  obtain g where "uniformly_continuous_on (closure S) g" and g: "∧x. x ∈ S ==> f x = g x"
    using uniformly_continuous_on_extension_on_closure assms by metis
  then have "compact (g ` closure S)"
    using ‹bounded S› compact_closure compact_continuous_image
      uniformly_continuous_imp_continuous by blast
  then show ?thesis
    using g bounded_closure_image compact_eq_bounded_closed
    by auto
qed


section ‹With Abstract Topology (TODO: move and remove dependency?)›

lemma openin_contains_ball:
    "openin (top_of_set T) S ⟷
     S ⊆ T ∧ (∀x ∈ S. ∃ε. 0 < ε ∧ ball x ε ∩ T ⊆ S)"
    (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (metis IntD2 Int_commute Int_lower1 Int_mono inf.idem openE openin_open)
next
  assume R: ?rhs
  then have "∀x∈S. ∃R. openin (top_of_set T) R ∧ x ∈ R ∧ R ⊆ S"
    by (metis open_ball Int_iff centre_in_ball inf_sup_aci(1) openin_open_Int subsetD)
  with R show ?lhs
    using openin_subopen by auto
qed

lemma openin_contains_cball:
   "openin (top_of_set T) S ⟷
        S ⊆ T ∧ (∀x ∈ S. ∃ε. 0 < ε ∧ cball x ε ∩ T ⊆ S)"
  by (fastforce simp: openin_contains_ball intro: exI [where x="_/2"])



section ‹Closed Nest›

text ‹Bounded closed nest property (proof does not use Heine-Borel)›

lemma bounded_closed_nest:
  fixes S :: "nat ==> ('a::heine_borel) set"
  assumes "∧n. closed (S n)"
      and "∧n. S n ≠ {}"
      and "∧m n. m ≤ n ==> S n ⊆ S m"
      and "bounded (S 0)"
  obtains a where "∧n. a ∈ S n"
proof -
  from assms(2) obtain x where x: "∀n. x n ∈ S n"
    by (meson ex_in_conv) 
  from assms(4,1) have "seq_compact (S 0)"
    by (simp add: bounded_closed_imp_seq_compact)
  then obtain l r where lr: "l ∈ S 0" "strict_mono r" "(x ∘ r) <---- l"
    using x and assms(3) unfolding seq_compact_def by blast
  have "∀n. l ∈ S n"
  proof
    fix n :: nat
    have "closed (S n)"
      using assms(1) by simp
    moreover have "∀i. (x ∘ r) i ∈ S i"
      using x and assms(3) and lr(2) [THEN seq_suble] by auto
    then have "∀i. (x ∘ r) (i + n) ∈ S n"
      using assms(3) by (fast intro!: le_add2)
    ultimately show "l ∈ S n"
      by (metis LIMSEQ_ignore_initial_segment closed_sequential_limits lr(3))
  qed
  then show ?thesis 
    using that by blast
qed

text ‹Decreasing case does not even need compactness, just completeness.›

lemma decreasing_closed_nest:
  fixes S :: "nat ==> ('a::complete_space) set"
  assumes "∧n. closed (S n)"
          "∧n. S n ≠ {}"
          "∧m n. m ≤ n ==> S n ⊆ S m"
          "∧ε. ε>0 ==> ∃n. ∀x∈S n. ∀y∈S n. dist x y < ε"
  obtains a where "∧n. a ∈ S n"
proof -
  obtain t where t: "∀n. t n ∈ S n"
    by (meson assms(2) equals0I)
  have "Cauchy t"
  proof (intro metric_CauchyI)
    fix ε :: real
    assume "ε > 0"
    then obtain N where N: "∀x∈S N. ∀y∈S N. dist x y < ε"
      using assms(4) by blast
    {
      fix m n :: nat
      assume "N ≤ m ∧ N ≤ n"
      then have "t m ∈ S N" "t n ∈ S N"
        using assms(3) t unfolding  subset_eq t by blast+
      then have "dist (t m) (t n) < ε"
        using N by auto
    }
    then show "∃M. ∀m≥M. ∀n≥M. dist (t m) (t n) < ε"
      by auto
  qed
  then obtain l where l:"(t ---> l) sequentially"
    using complete_UNIV unfolding complete_def by auto
  show thesis
  proof
    fix n :: nat
    { fix ε :: real
      assume "ε > 0"
      then obtain N :: nat where N: "∀n≥N. dist (t n) l < ε"
        using l[unfolded lim_sequentially] by auto
      have "t (max n N) ∈ S n"
        by (meson assms(3) subsetD max.cobounded1 t)
      then have "∃y∈S n. dist y l < ε"
        using N max.cobounded2 by blast
    }
    then show "l ∈ S n"
      using closed_approachable[of "S n" l] assms(1) by auto
  qed
qed

text ‹Strengthen it to the intersection actually being a singleton.›

lemma decreasing_closed_nest_sing:
  fixes S :: "nat ==> 'a::complete_space set"
  assumes "∧n. closed(S n)"
          "∧n. S n ≠ {}"
          "∧m n. m ≤ n ==> S n ⊆ S m"
   and 🍋: "∧ε. ε>0 ==> ∃n. ∀x ∈ (S n). ∀ y∈(S n). dist x y < ε"
  shows "∃a. ∩(range S) = {a}"
proof -
  obtain a where a: "∀n. a ∈ S n"
    using decreasing_closed_nest[of S] using assms by auto
  then have "dist a b = 0" if "b ∈ ∩(range S)" for b
    by (meson that InterE 🍋 linorder_neq_iff linorder_not_less range_eqI zero_le_dist)
  with a have "∩(range S) = {a}"
    unfolding image_def by auto
  then show ?thesis ..
qed

section🍋‹tag unimportant› ‹Making a continuous function avoid some value in a neighbourhood›

lemma continuous_within_avoid:
  fixes f :: "'a::metric_space ==> 'b::t1_space"
  assumes "continuous (at x within S) f"
    and "f x ≠ a"
  shows "∃ε>0. ∀y ∈ S. dist x y < ε ⟶ f y ≠ a"
proof -
  obtain U where "open U" and "f x ∈ U" and "a ∉ U"
    using t1_space [OF ‹f x ≠ a›] by fast
  have "∀🪙F y in at x within S. f y ∈ U"
    using ‹open U› and ‹f x ∈ U›
    using assms(1) continuous_within tendsto_def by blast
  with ‹f x ≠ a› ‹a ∉ U› show ?thesis
    by (metis (no_types, lifting) dist_commute eventually_at)
qed

lemma continuous_at_avoid:
  fixes f :: "'a::metric_space ==> 'b::t1_space"
  assumes "continuous (at x) f"
    and "f x ≠ a"
  shows "∃ε>0. ∀y. dist x y < ε ⟶ f y ≠ a"
  using assms continuous_within_avoid[of x UNIV f a] by simp

lemma continuous_on_avoid:
  fixes f :: "'a::metric_space ==> 'b::t1_space"
  assumes "continuous_on S f"
    and "x ∈ S"
    and "f x ≠ a"
  shows "∃ε>0. ∀y ∈ S. dist x y < ε ⟶ f y ≠ a"
  using continuous_within_avoid[of x S f a] assms
  by (meson continuous_on_eq_continuous_within)

lemma continuous_on_open_avoid:
  fixes f :: "'a::metric_space ==> 'b::t1_space"
  assumes "continuous_on S f"
    and "open S"
    and "x ∈ S"
    and "f x ≠ a"
  shows "∃ε>0. ∀y. dist x y < ε ⟶ f y ≠ a"
  using continuous_at_avoid[of x f a]  assms
  by (meson continuous_on_eq_continuous_at)

section ‹Consequences for Real Numbers›

lemma closed_contains_Inf:
  fixes S :: "real set"
  shows "S ≠ {} ==> bdd_below S ==> closed S ==> Inf S ∈ S"
  by (metis closure_contains_Inf closure_closed)

lemma closed_subset_contains_Inf:
  fixes A C :: "real set"
  shows "closed C ==> A ⊆ C ==> A ≠ {} ==> bdd_below A ==> Inf A ∈ C"
  by (metis closure_contains_Inf closure_minimal subset_eq)

lemma closed_contains_Sup:
  fixes S :: "real set"
  shows "S ≠ {} ==> bdd_above S ==> closed S ==> Sup S ∈ S"
  by (metis closure_closed closure_contains_Sup)

lemma closed_subset_contains_Sup:
  fixes A C :: "real set"
  shows "closed C ==> A ⊆ C ==> A ≠ {} ==> bdd_above A ==> Sup A ∈ C"
  by (metis closure_contains_Sup closure_minimal subset_eq)

lemma atLeastAtMost_subset_contains_Inf:
  fixes A :: "real set" and a b :: real
  shows "A ≠ {} ==> a ≤ b ==> A ⊆ {a..b} ==> Inf A ∈ {a..b}"
  by (meson bdd_below_Icc bdd_below_mono closed_real_atLeastAtMost
      closed_subset_contains_Inf)

lemma bounded_real: "bounded (S::real set) ⟷ (∃a. ∀x∈S. ∣x∣ ≤ a)"
  by (simp add: bounded_iff)

lemma bounded_imp_bdd_above: "bounded S ==> bdd_above (S :: real set)"
  by (meson abs_le_D1 bdd_above.unfold bounded_real)

lemma bounded_imp_bdd_below: "bounded S ==> bdd_below (S :: real set)"
  by (metis add.commute abs_le_D1 bdd_below.unfold bounded_def diff_le_eq dist_real_def)

lemma bounded_norm_le_SUP_norm:
  "bounded (range f) ==> norm (f x) ≤ (SUP x. norm (f x))"
  by (auto intro!: cSUP_upper bounded_imp_bdd_above simp: bounded_norm_comp)

lemma bounded_has_Sup:
  fixes S :: "real set"
  assumes "bounded S"
    and "S ≠ {}"
  shows "∀x∈S. x ≤ Sup S"
    and "∀b. (∀x∈S. x ≤ b) ⟶ Sup S ≤ b"
proof
  show "∀b. (∀x∈S. x ≤ b) ⟶ Sup S ≤ b"
    using assms by (metis cSup_least)
qed (metis cSup_upper assms(1) bounded_imp_bdd_above)

lemma Sup_insert:
  fixes S :: "real set"
  shows "bounded S ==> Sup (insert x S) = (if S = {} then x else max x (Sup S))"
  by (auto simp: bounded_imp_bdd_above sup_max cSup_insert_If)

lemma bounded_has_Inf:
  fixes S :: "real set"
  assumes "bounded S"
    and "S ≠ {}"
  shows "∀x∈S. x ≥ Inf S"
    and "∀b. (∀x∈S. x ≥ b) ⟶ Inf S ≥ b"
proof
  show "∀b. (∀x∈S. x ≥ b) ⟶ Inf S ≥ b"
    using assms by (metis cInf_greatest)
qed (metis cInf_lower assms(1) bounded_imp_bdd_below)

lemma Inf_insert:
  fixes S :: "real set"
  shows "bounded S ==> Inf (insert x S) = (if S = {} then x else min x (Inf S))"
  by (auto simp: bounded_imp_bdd_below inf_min cInf_insert_If)

lemma open_real:
  fixes S :: "real set"
  shows "open S ⟷ (∀x ∈ S. ∃ε>0. ∀x'. ∣x' - x∣ < ε --> x' ∈ S)"
  unfolding open_dist dist_norm by simp

lemma islimpt_approachable_real:
  fixes S :: "real set"
  shows "x islimpt S ⟷ (∀ε>0. ∃x'∈ S. x' ≠ x ∧ ∣x' - x∣ < ε)"
  unfolding islimpt_approachable dist_norm by simp

lemma closed_real:
  fixes S :: "real set"
  shows "closed S ⟷ (∀x. (∀ε>0. ∃x' ∈ S. x' ≠ x ∧ ∣x' - x∣ < ε) ⟶ x ∈ S)"
  unfolding closed_limpt islimpt_approachable dist_norm by simp

lemma continuous_at_real_range:
  fixes f :: "'a::real_normed_vector ==> real"
  shows "continuous (at x) f ⟷ (∀ε>0. ∃δ>0. ∀x'. norm(x' - x) < δ ⟶ ∣f x' - f x∣ < ε)"
  by (simp add: continuous_at_eps_delta dist_norm)

lemma continuous_on_real_range:
  fixes f :: "'a::real_normed_vector ==> real"
  shows "continuous_on S f ⟷
         (∀x ∈ S. ∀ε>0. ∃δ>0. (∀x' ∈ S. norm(x' - x) < δ ⟶ ∣f x' - f x∣ < ε))"
  unfolding continuous_on_iff dist_norm by simp

lemma continuous_on_closed_Collect_le:
  fixes f g :: "'a::topological_space ==> real"
  assumes f: "continuous_on S f" and g: "continuous_on S g" and S: "closed S"
  shows "closed {x ∈ S. f x ≤ g x}"
proof -
  have "closed ((λx. g x - f x) -` {0..} ∩ S)"
    using closed_real_atLeast continuous_on_diff [OF g f]
    by (simp add: continuous_on_closed_vimage [OF S])
  also have "((λx. g x - f x) -` {0..} ∩ S) = {x∈S. f x ≤ g x}"
    by auto
  finally show ?thesis .
qed

lemma continuous_le_on_closure:
  fixes a::real
  assumes f: "continuous_on (closure S) f"
      and x: "x ∈ closure(S)"
      and xlo: "∧x. x ∈ S ==> f(x) ≤ a"
    shows "f(x) ≤ a"
  using image_closure_subset [OF f, where T=" {x. x ≤ a}" ] assms
    continuous_on_closed_Collect_le[of "UNIV" "λx. x" "λx. a"]
  by auto

lemma continuous_ge_on_closure:
  fixes a::real
  assumes f: "continuous_on (closure S) f"
      and x: "x ∈ closure S"
      and xlo: "∧x. x ∈ S ==> f(x) ≥ a"
    shows "f(x) ≥ a"
  using image_closure_subset [OF f, where T=" {x. a ≤ x}"] assms
    continuous_on_closed_Collect_le[of "UNIV" "λx. a" "λx. x"]
  by auto


section‹The infimum of the distance between two sets›

definition🍋‹tag important› setdist :: "'a::metric_space set ==> 'a set ==> real" where
  "setdist S T ≡
       (if S = {} ∨ T = {} then 0
        else Inf {dist x y| x y. x ∈ S ∧ y ∈ T})"

lemma setdist_empty1 [simp]: "setdist {} T = 0"
  by (simp add: setdist_def)

lemma setdist_empty2 [simp]: "setdist T {} = 0"
  by (simp add: setdist_def)

lemma setdist_pos_le [simp]: "0 ≤ setdist S T"
  by (auto simp: setdist_def ex_in_conv [symmetric] intro: cInf_greatest)

lemma le_setdistI:
  assumes "S ≠ {}" "T ≠ {}" "∧x y. [x ∈ S; y ∈ T] ==> δ ≤ dist x y"
    shows "δ ≤ setdist S T"
  using assms
  by (auto simp: setdist_def Set.ex_in_conv [symmetric] intro: cInf_greatest)

lemma setdist_le_dist: "[x ∈ S; y ∈ T] ==> setdist S T ≤ dist x y"
  unfolding setdist_def
  by (auto intro!: bdd_belowI [where m=0] cInf_lower)

lemma le_setdist_iff:
  "δ ≤ setdist S T ⟷ (∀x ∈ S. ∀y ∈ T. δ ≤ dist x y) ∧ (S = {} ∨ T = {} ⟶ δ ≤ 0)"
  (is "?lhs = ?rhs")
proof
  show "?rhs ==> ?lhs"
    by (meson le_setdistI order_trans setdist_pos_le)
qed (use setdist_le_dist in fastforce)

lemma setdist_ltE:
  assumes "setdist S T < b" "S ≠ {}" "T ≠ {}"
  obtains x y where "x ∈ S" "y ∈ T" "dist x y < b"
  using assms
  by (auto simp: not_le [symmetric] le_setdist_iff)

lemma setdist_refl: "setdist S S = 0"
proof (rule antisym)
  show "setdist S S ≤ 0"
    by (metis dist_self equals0I order_refl setdist_empty1 setdist_le_dist)
qed simp

lemma setdist_sym: "setdist S T = setdist T S"
  by (force simp: setdist_def dist_commute intro!: arg_cong [where f=Inf])

lemma setdist_triangle: "setdist S T ≤ setdist S {a} + setdist {a} T"
proof (cases "S = {} ∨ T = {}")
  case True then show ?thesis
    using setdist_pos_le by fastforce
next
  case False
  then have "setdist S T - dist x a ≤ setdist {a} T" if "x ∈ S" for x
    unfolding le_setdist_iff
    by (metis diff_le_eq dist_commute dist_triangle3 order.trans empty_not_insert
        setdist_le_dist singleton_iff that)
  then have "setdist S T - setdist {a} T ≤ setdist S {a}"
    using False by (fastforce intro: le_setdistI)
  then show ?thesis
    by (simp add: algebra_simps)
qed

lemma setdist_singletons [simp]: "setdist {x} {y} = dist x y"
  by (simp add: setdist_def)

lemma setdist_Lipschitz: "∣setdist {x} S - setdist {y} S∣ ≤ dist x y"
  unfolding setdist_singletons [symmetric]
  by (metis abs_diff_le_iff diff_le_eq setdist_triangle setdist_sym)

lemma continuous_at_setdist [continuous_intros]: "continuous (at x) (λy. (setdist {y} S))"
  by (force simp: continuous_at_eps_delta dist_real_def intro: le_less_trans [OF setdist_Lipschitz])

lemma continuous_on_setdist [continuous_intros]: "continuous_on T (λy. (setdist {y} S))"
  by (metis continuous_at_setdist continuous_at_imp_continuous_on)

lemma uniformly_continuous_on_setdist: "uniformly_continuous_on T (λy. (setdist {y} S))"
  by (force simp: uniformly_continuous_on_def dist_real_def intro: le_less_trans [OF setdist_Lipschitz])

lemma setdist_subset_right: "[T ≠ {}; T ⊆ u] ==> setdist S u ≤ setdist S T"
  by (smt (verit, best) in_mono le_setdist_iff)

lemma setdist_subset_left: "[S ≠ {}; S ⊆ T] ==> setdist T u ≤ setdist S u"
  by (metis setdist_subset_right setdist_sym)

lemma setdist_closure_1 [simp]: "setdist (closure S) T = setdist S T"
proof (cases "S = {} ∨ T = {}")
  case True then show ?thesis by force
next
  case False
  { fix y
    assume "y ∈ T"
    have "continuous_on (closure S) (λa. dist a y)"
      by (auto simp: continuous_intros dist_norm)
    then have *: "∧x. x ∈ closure S ==> setdist S T ≤ dist x y"
      by (fast intro: setdist_le_dist ‹y ∈ T› continuous_ge_on_closure)
  } then
  show ?thesis
    by (metis False antisym closure_eq_empty closure_subset le_setdist_iff setdist_subset_left)
qed

lemma setdist_closure_2 [simp]: "setdist T (closure S) = setdist T S"
  by (metis setdist_closure_1 setdist_sym)

lemma setdist_eq_0I: "[x ∈ S; x ∈ T] ==> setdist S T = 0"
  by (metis antisym dist_self setdist_le_dist setdist_pos_le)

lemma setdist_unique:
  "[a ∈ S; b ∈ T; ∧x y. x ∈ S ∧ y ∈ T ==> dist a b ≤ dist x y]
   ==> setdist S T = dist a b"
  by (force simp: setdist_le_dist le_setdist_iff intro: antisym)

lemma setdist_le_sing: "x ∈ S ==> setdist S T ≤ setdist {x} T"
  using setdist_subset_left by auto

lemma infdist_eq_setdist: "infdist x A = setdist {x} A"
  by (simp add: infdist_def setdist_def Setcompr_eq_image)

lemma setdist_eq_infdist: "setdist A B = (if A = {} then 0 else INF a∈A. infdist a B)"
proof -
  have "Inf {dist x y |x y. x ∈ A ∧ y ∈ B} = (INF x∈A. Inf (dist x ` B))"
    if "b ∈ B" "a ∈ A" for a b
  proof (rule order_antisym)
    have "Inf {dist x y |x y. x ∈ A ∧ y ∈ B} ≤ Inf (dist x ` B)"
      if "b ∈ B" "a ∈ A" "x ∈ A" for x 
    proof -
      have "∧b'. b' ∈ B ==> Inf {dist x y |x y. x ∈ A ∧ y ∈ B} ≤ dist x b'"
        by (metis (mono_tags, lifting) ex_in_conv setdist_def setdist_le_dist ‹x ∈ A›)
      then show ?thesis
        by (metis (lifting) cINF_greatest emptyE ‹b ∈ B›)
    qed
    then show "Inf {dist x y |x y. x ∈ A ∧ y ∈ B} ≤ (INF x∈A. Inf (dist x ` B))"
      by (metis (mono_tags, lifting) cINF_greatest emptyE that)
  next
    have *: "∧x y. [b ∈ B; a ∈ A; x ∈ A; y ∈ B] ==> ∃a∈A. Inf (dist a ` B) ≤ dist x y"
      by (meson bdd_below_image_dist cINF_lower)
    show "(INF x∈A. Inf (dist x ` B)) ≤ Inf {dist x y |x y. x ∈ A ∧ y ∈ B}"
    proof (rule conditionally_complete_lattice_class.cInf_mono)
      show "bdd_below ((λx. Inf (dist x ` B)) ` A)"
        by (metis (no_types, lifting) bdd_belowI2 ex_in_conv infdist_def infdist_nonneg that(1))
    qed (use that in ‹auto simp: *›)
  qed
  then show ?thesis
    by (auto simp: setdist_def infdist_def)
qed

lemma infdist_mono:
  assumes "A ⊆ B" "A ≠ {}"
  shows "infdist x B ≤ infdist x A"
  by (simp add: assms infdist_eq_setdist setdist_subset_right)

lemma infdist_singleton [simp]: "infdist x {y} = dist x y"
  by (simp add: infdist_eq_setdist)

proposition setdist_attains_inf:
  assumes "compact B" "B ≠ {}"
  obtains y where "y ∈ B" "setdist A B = infdist y A"
proof (cases "A = {}")
  case True
  then show thesis
    by (metis assms diameter_compact_attained infdist_def setdist_def that)
next
  case False
  obtain y where "y ∈ B" and min: "∧y'. y' ∈ B ==> infdist y A ≤ infdist y' A"
    by (metis continuous_attains_inf [OF assms continuous_on_infdist] continuous_on_id)
  show thesis
  proof
    have "setdist A B = (INF y∈B. infdist y A)"
      by (metis ‹B ≠ {}› setdist_eq_infdist setdist_sym)
    also have "… = infdist y A"
    proof (rule order_antisym)
      show "(INF y∈B. infdist y A) ≤ infdist y A"
        by (meson ‹y ∈ B› bdd_belowI2 cInf_lower image_eqI infdist_nonneg)
    next
      show "infdist y A ≤ (INF y∈B. infdist y A)"
        by (simp add: ‹B ≠ {}› cINF_greatest min)
    qed
    finally show "setdist A B = infdist y A" .
  qed (fact ‹y ∈ B›)
qed


section ‹Diameter Lemma›

text ‹taken from the AFP entry Martingales, by Ata Keskin, TU München›

lemma diameter_comp_strict_mono:
  fixes s :: "nat ==> 'a :: metric_space"
  assumes "strict_mono r" and bnd: "bounded {s i |i. r n ≤ i}"
  shows "diameter {s (r i) | i. n ≤ i} ≤ diameter {s i | i. r n ≤ i}"
proof (rule diameter_subset)
  show "{s (r i) | i. n ≤ i} ⊆ {s i | i. r n ≤ i}" 
    using ‹strict_mono r› monotoneD strict_mono_mono by fastforce
qed (intro bnd)

lemma diameter_bounded_bound':
  fixes S :: "'a :: metric_space set"
  assumes S: "bdd_above (case_prod dist ` (S×S))" and "x ∈ S" "y ∈ S"
  shows "dist x y ≤ diameter S"
proof -
  have "(x,y) ∈ S×S" using assms by auto
  then have "dist x y ≤ (SUP (x,y)∈S×S. dist x y)"
    by (metis S cSUP_upper case_prod_conv)
  with ‹x ∈ S› show ?thesis by (auto simp: diameter_def)
qed

lemma bounded_imp_dist_bounded:
  assumes "bounded (range s)"
  shows "bounded ((λ(i, j). dist (s i) (s j)) ` ({n..} × {n..}))"
  unfolding image_iff case_prod_unfold
  by (intro bounded_dist_comp; meson assms bounded_dist_comp bounded_dist_comp bounded_subset image_subset_iff rangeI)

text ‹A sequence is Cauchy, if and only if it is bounded and its diameter tends to zero.
  The diameter is well-defined only if the sequence is bounded.›
lemma cauchy_iff_diameter_tends_to_zero_and_bounded:
  fixes s :: "nat ==> 'a :: metric_space"
  shows "Cauchy s ⟷ ((λn. diameter {s i | i. i ≥ n}) <---- 0 ∧ bounded (range s))"
         (is "_ = ?rhs")
proof -
  have "{s i |i. N ≤ i} ≠ {}" for N by blast
  hence diameter_SUP: "diameter {s i |i. N ≤ i} = (SUP (i, j) ∈ {N..} × {N..}. dist (s i) (s j))" for N 
    unfolding diameter_def by (auto intro!: arg_cong[of _ _ Sup])
  show ?thesis 
  proof (intro iffI)
    assume "Cauchy s"
    have "∃N. ∀n≥N. norm (diameter {s i |i. n ≤ i}) < ε" if e_pos: "ε > 0" for ε
    proof -
      obtain N where dist_less: "dist (s n) (s m) < (1/2) * ε" 
        if "n ≥ N" "m ≥ N" for n m 
        using ‹Cauchy s› e_pos
        by (meson half_gt_zero less_numeral_extra(1) metric_CauchyD mult_pos_pos)
      have "diameter {s i |i. r ≤ i} < ε" 
        if "r ≥ N" for r
      proof -
        have "dist (s n) (s m) < (1/2) * ε" if "n ≥ r" "m ≥ r" for n m 
          using ‹r ≥ N› dist_less that by simp
        hence "(SUP (i, j) ∈ {r..} × {r..}. dist (s i) (s j)) ≤ (1/2) * ε" 
          by (intro cSup_least) fastforce+
        also have "… < ε" using e_pos by simp
        finally show ?thesis 
          using diameter_SUP by presburger
      qed
      moreover have "diameter {s i |i. r ≤ i} ≥ 0" for r 
        unfolding diameter_SUP 
        using bounded_imp_dist_bounded[OF cauchy_imp_bounded, THEN bounded_imp_bdd_above] ‹Cauchy s›
        by (force intro: cSup_upper2)
      ultimately show ?thesis 
        by auto
    qed                 
    thus "(λn. diameter {s i |i. n ≤ i}) <---- 0 ∧ bounded (range s)" 
      using cauchy_imp_bounded[OF ‹Cauchy s›] by (simp add: LIMSEQ_iff)
  next
    assume R: ?rhs
    have "∃N. ∀n≥N. ∀m≥N. dist (s n) (s m) < ε" if e_pos: "ε > 0" for ε
    proof -
      obtain N where diam_less: "diameter {s i |i. r ≤ i} < ε" if "r ≥ N" for r 
        using LIMSEQ_D R e_pos by fastforce
      have "dist (s n) (s m) < ε" 
        if "n ≥ N" "m ≥ N" for n m
        using cSUP_lessD[OF bounded_imp_dist_bounded[THEN bounded_imp_bdd_above],
            OF _ diam_less[unfolded diameter_SUP]] 
        using R that by auto
      thus ?thesis by blast
    qed
    then show "Cauchy s" 
      by (simp add: Cauchy_def)
  qed            
qed
  
end