Theory Set_Based_Metric_Space

(*  Title:   Set_Based_Metric_Space.thy
    Author:  Michikazu Hirata, Tokyo Institute of Technology
*)

section  ‹Set-Based Metric Spaces›
theory Set_Based_Metric_Space
  imports Lemmas_StandardBorel
begin

subsection ‹Set-Based Metric Spaces ›
locale metric_set =
  fixes S :: "'a set"
    and dist :: "'a  'a  real"
  assumes dist_geq0: "x y. dist x y  0"
      and dist_notin: "x y. x  S  dist x y = 0"
      and dist_0: "x y. x  S  y  S  (x = y) = (dist x y = 0)"
      and dist_sym: "x y. dist x y = dist y x"
      and dist_tr: "x y z. x  S  y  S  z  S  dist x z  dist x y + dist y z"

lemma metric_class_metric_set[simp]: "metric_set UNIV dist"
  by standard (auto simp: dist_commute dist_triangle)

context metric_set
begin

abbreviation "dist_typeclass  Real_Vector_Spaces.dist"

lemma dist_notin':
  assumes "y  S"
  shows "dist x y = 0"
  by(auto simp: dist_sym[of x y] intro!: dist_notin assms)

lemma dist_ge0:
  assumes "x  S" "y  S"
  shows "x  y  dist x y > 0"
  using dist_0[OF assms] dist_geq0[of x y] by auto

lemma dist_0'[simp]: "dist x x = 0"
  by(cases "x  S") (use dist_notin dist_0 in auto)

lemma dist_tr_abs:
  assumes "x  S" "y  S" "z  S"
  shows "¦dist x y - dist y z¦  dist x z"
  using dist_tr[OF assms(1,3,2),simplified dist_sym[of z]] dist_tr[OF assms(2,1,3),simplified dist_sym[of _ x]]
  by auto

text ‹ Ball ›
definition open_ball :: "'a  real  'a set" where
"open_ball a r  if a  S then {x  S. dist a x < r} else {}"

lemma open_ball_subset_ofS: "open_ball a ε  S"
  by(auto simp: open_ball_def)

lemma open_ballD:
  assumes "x  open_ball a ε"
  shows "dist a x < ε"
proof -
  have [simp]:"a  S"
    apply(rule ccontr) using assms by(simp add: open_ball_def)
  show ?thesis
    using assms by(simp add: open_ball_def)
qed

lemma open_ballD':
  assumes "x  open_ball a ε"
  shows "x  S" "a  S" "ε > 0"
proof -
  have 1:"a  S"
    apply(rule ccontr)
    using assms by(auto simp: open_ball_def)
  have 2:"x  S"
    apply(rule ccontr)
    using assms 1 by(auto simp: open_ball_def)
  have 3: "dist a x < ε"
    using assms by(simp add: 1 2 open_ball_def)
  show "ε > 0"
    apply(rule ccontr)
    using 3 dist_geq0[of a x] by auto
  show "x  S" "a  S"
    by fact+
qed

lemma open_ball_inverse:
 "x  open_ball y ε  y  open_ball x ε"
proof -
  have 0:"x y. x  open_ball y ε  y  open_ball x ε"
  proof -
    fix x y
    assume 1:"x  open_ball y ε"
    show "y  open_ball x ε"
      using open_ballD'[OF 1] dist_sym[of y x] 1 by(simp add: open_ball_def)
  qed
  show ?thesis
    using 0[of x y] 0[of y x] by auto
qed

lemma open_ball_ina[simp]:
  assumes "a  S" and "ε > 0"
  shows "a  open_ball a ε"
  using assms dist_0[of a a] by(simp add: open_ball_def)

lemma open_ball_nin_le:
  assumes "a  S" "ε > 0" "b  S" "b  open_ball a ε"
  shows "ε  dist a b"
  using assms by(simp add: open_ball_def)

lemma open_ball_le:
  assumes "r  l"
  shows "open_ball a r  open_ball a l"
  using assms by(auto simp: open_ball_def)

lemma open_ball_le_0:
  assumes "ε  0"
  shows "open_ball a ε = {}"
  using assms dist_geq0[of a]
  by(auto simp: open_ball_def) (meson linorder_not_less order_trans)

lemma open_ball_nin:
  assumes "a  S"
  shows "open_ball a ε = {}"
  by(simp add: open_ball_def assms)

definition closed_ball :: "'a  real  'a set" where
"closed_ball a r  if a  S then {x  S. dist a x  r} else {}"

lemma closed_ball_subset_ofS:
 "closed_ball a ε  S"
  by(auto simp: closed_ball_def)

lemma closed_ballD:
  assumes "x  closed_ball a ε"
  shows "dist a x  ε"
proof -
  have [simp]:"a  S"
    apply(rule ccontr) using assms by(simp add: closed_ball_def)
  show ?thesis
    using assms by(simp add: closed_ball_def)
qed

lemma closed_ballD':
  assumes "x  closed_ball a ε"
  shows "x  S" "a  S" "ε  0"
proof -
  have 1:"a  S"
    apply(rule ccontr)
    using assms by(auto simp: closed_ball_def)
  have 2:"x  S"
    apply(rule ccontr)
    using assms 1 by(auto simp: closed_ball_def)
  have 3: "dist a x  ε"
    using assms by(simp add: 1 2 closed_ball_def)
  show "ε  0"
    apply(rule ccontr)
    using 3 dist_geq0[of a x] by auto
  show "x  S" "a  S"
    by fact+
qed

lemma closed_ball_ina[simp]:
  assumes "a  S" and "ε  0"
  shows "a  closed_ball a ε"
  using assms dist_0[of a a] by(simp add: closed_ball_def)

lemma closed_ball_le:
  assumes "r  l"
  shows "closed_ball a r  closed_ball a l"
  using closed_ballD'[of _ a r] closed_ballD[of _ a r] assms
  by(fastforce simp: closed_ball_def[of _ l])

lemma closed_ball_le_0:
  assumes "ε < 0"
  shows "closed_ball a ε = {}"
  using assms dist_geq0[of a]
  by(auto simp: closed_ball_def) (meson linorder_not_less order_trans)

lemma closed_ball_0:
  assumes "a  S"
  shows "closed_ball a 0 = {a}"
  using assms dist_0[OF assms assms] dist_0[OF assms] dist_geq0[of a] order_antisym_conv
  by(auto simp: closed_ball_def)

lemma closed_ball_nin:
  assumes "a  S"
  shows "closed_ball a ε = {}"
  by(simp add: closed_ball_def assms)

lemma open_ball_closed_ball:
 "open_ball a ε  closed_ball a ε"
  using open_ballD'[of _ a ε] open_ballD[of _ a ε]
  by(fastforce simp: closed_ball_def)

lemma closed_ball_open_ball:
  assumes "e < f"
  shows "closed_ball a e  open_ball a f"
  using closed_ballD'[of _ a e] closed_ballD[of _ a e] assms
  by(fastforce simp: open_ball_def)

lemma closed_ball_open_ball_un1:
  assumes "e > 0"
  shows "open_ball a e  {xS. dist a x = e} = closed_ball a e"
  using assms dist_notin by(auto simp: open_ball_def closed_ball_def)

lemma closed_ball_open_ball_un2:
  assumes "a  S"
  shows "open_ball a e  {xS. dist a x = e} = closed_ball a e"
  using assms by(auto simp: open_ball_def closed_ball_def)

definition mtopology :: "'a topology" where
"mtopology = topology (λU. U  S  (xU. ε>0. open_ball x ε  U))"

lemma mtopology_istopology:
 "istopology (λU. U  S  (xU. ε>0. open_ball x ε  U))"
  unfolding istopology_def
proof safe
  fix U1 U2 x
  assume h1: "U1  S" "yU1. ε>0. open_ball y ε  U1"
     and h2: "U2  S" "yU2. ε>0. open_ball y ε  U2"
     and hx: "x  U1" "x  U2"
  obtain ε1 ε2 where
   "ε1 > 0" "ε2 > 0""open_ball x ε1  U1" "open_ball x ε2  U2"
    using h1 h2 hx by blast
  thus "ε>0. open_ball x ε  U1  U2"
    using open_ball_le[of "min ε1 ε2" ε1 x] open_ball_le[of "min ε1 ε2" ε2 x]
    by(auto intro!: exI[where x="min ε1 ε2"])
next
  fix 𝒦 U x
  assume h:"K𝒦. K  S  (xK. ε>0. open_ball x ε  K)"
           "U  𝒦" "x  U"
  then obtain ε where 
   "ε > 0" "open_ball x ε  U"
    by blast
  thus "ε>0. open_ball x ε   𝒦"
    using h(2) by(auto intro!: exI[where x=ε])
qed auto

lemma mtopology_openin_iff:
 "openin mtopology U  U  S  (xU. ε>0. open_ball x ε  U)"
  by (simp add: mtopology_def mtopology_istopology)

lemma mtopology_topspace: "topspace mtopology = S"
  unfolding topspace_def mtopology_def topology_inverse'[OF mtopology_istopology]
proof -
  have "xS. ε>0. open_ball x ε  S"
    by(auto intro!: exI[where x=1] simp: open_ball_def)
  thus " {U. U  S  (xU. ε>0. open_ball x ε  U)} = S"
    by auto
qed

lemma openin_S[simp]: "openin mtopology S"
  by (metis openin_topspace mtopology_topspace)

lemma mtopology_open_ball_in':
  assumes "x  open_ball a ε"
  shows "ε'>0. open_ball x ε'  open_ball a ε"
proof -
  show "ε'>0. open_ball x ε'  open_ball a ε"
  proof(intro exI[where x="ε - dist a x"] conjI)
    show "0 < ε - dist a x"
      using open_ballD'[OF assms] open_ballD[OF assms] by auto
  next
    show "open_ball x (ε - dist a x)  open_ball a ε"
    proof
      fix y
      assume hy:"y  open_ball x (ε - dist a x)"
      show "y  open_ball a ε"        
        using open_ballD[OF hy] open_ballD[OF assms] open_ballD'(2)[OF assms] dist_tr[OF open_ballD'(2)[OF assms] open_ballD'(1)[OF assms] open_ballD'(1)[OF hy]]
        by(auto simp: open_ball_def assms(1) open_ballD'[OF hy])
    qed
  qed
qed

lemma mtopology_open_ball_in:
  assumes "a  S" and "ε > 0"
  shows "openin mtopology (open_ball a ε)"
  using mtopology_open_ball_in' topology_inverse'[OF mtopology_istopology] open_ball_subset_ofS mtopology_def
  by auto

lemma openin_open_ball: "openin mtopology (open_ball a ε)"
proof -
  consider "a  S  ε > 0" | "a  S" | "ε  0" by fastforce
  thus ?thesis
    by cases (simp_all add: mtopology_open_ball_in open_ball_le_0 open_ball_nin)
qed

lemma closedin_closed_ball: "closedin mtopology (closed_ball a ε)"
  unfolding closedin_def mtopology_topspace mtopology_openin_iff
proof safe
  fix x
  assume h:"x  S" "x  closed_ball a ε"
  consider "a  S" | "ε < 0" | "a  S" "ε  0"  by fastforce
  thus "ε'>0. open_ball x ε'  S - closed_ball a ε"
  proof cases
    case 3
    then have "dist a x > ε"
      using h by(auto simp: closed_ball_def)
    show ?thesis
    proof(intro exI[where x="dist a x - ε"] conjI)
      show "open_ball x (dist a x - ε)  S - closed_ball a ε"
      proof safe
        fix z
        assume h':"z  open_ball x (dist a x - ε)" "z  closed_ball a ε"
        have "dist a x  dist a z + dist z x"
          by(auto intro!: dist_tr 3 open_ballD'[OF h'(1)])
        also have "...  ε + dist z x"
          using closed_ballD[OF h'(2)] by simp
        also have "... < dist a x"
          using open_ballD[OF h'(1),simplified dist_sym[of x]] by auto
        finally show False ..
      qed(use open_ball_subset_ofS dist a x > ε in auto)
    qed(use open_ball_subset_ofS dist a x > ε in auto)
  qed(auto simp: closed_ball_nin closed_ball_le_0 open_ball_subset_ofS intro!: exI[where x=1])
qed(use closed_ball_subset_ofS in auto)

lemma mtopology_def2:
 "mtopology = topology_generated_by {open_ball a ε | a ε. a  S  ε > 0}"
  (is "?lhs = ?rhs")
proof -
  have "U. openin ?lhs U = openin ?rhs U"
  proof
    fix U
    assume h:"openin mtopology U"
    then have "x U. ε > 0. open_ball x ε  U"
      using topology_inverse'[OF mtopology_istopology]
      by(simp add: mtopology_def)
    then obtain ε where he:
      "x. x  U  ε x > 0  open_ball x (ε x)  U"
      using bchoice[of U "λx ε.  ε > 0   open_ball x ε  U"]
      by blast
    have "U = {open_ball x (ε x)|x. x U}"
    proof
      show " {open_ball x (ε x) |x. x  U}  U"
        using he by auto
    next
      show "U   {open_ball x (ε x) |x. x  U}"
      proof
        fix a
        assume ha:"a  U"
        then have "a  open_ball a (ε a)"
          using he[of a] open_ball_ina[of a "ε a"] openin_subset[OF h,simplified]
          by(auto simp: mtopology_topspace)
        thus "a   {open_ball x (ε x) |x. x  U}"
          using ha by auto
      qed
    qed
    also have "generate_topology_on {open_ball a ε |a ε. a  S  0 < ε} ..."
      apply(rule generate_topology_on.UN)
      apply(rule generate_topology_on.Basis)
      using he openin_subset[OF h,simplified]
      by(fastforce simp: mtopology_topspace)
    finally show "openin (topology_generated_by {open_ball a ε |a ε. a  S  0 < ε}) U"
      by (simp add: openin_topology_generated_by_iff)
  next
    fix U
    assume "openin (topology_generated_by {open_ball a ε |a ε. a  S  0 < ε}) U"
    then have "generate_topology_on {open_ball a ε |a ε. a  S  0 < ε} U"
      by (simp add: openin_topology_generated_by_iff)
    thus "openin mtopology U"
      apply induction
      using mtopology_open_ball_in
      by auto
  qed
  thus ?thesis
    by(simp add: topology_eq)
qed

abbreviation mtopology_subbasis :: "'a set set  bool" where
"mtopology_subbasis 𝒪  subbase_of mtopology  𝒪"

lemma mtopology_subbasis1:
 "mtopology_subbasis {open_ball a ε | a ε. a  S  ε > 0}"
  by(simp add: mtopology_def2 subbase_of_def)

abbreviation mtopology_basis :: "'a set set  bool" where
"mtopology_basis 𝒪  base_of mtopology 𝒪"

lemma mtopology_basis_ball:
 "mtopology_basis {open_ball a ε | a ε. a  S  ε > 0}"
  unfolding base_of_def
proof -
  show "U. openin mtopology U = (𝒰. U =  𝒰  𝒰  {open_ball a ε |a ε. a  S  0 < ε})"
  proof safe
    fix U
    assume "openin mtopology U"
    then have "U  S" "x. xU  ε>0. open_ball x ε  U"
      by(auto simp: mtopology_openin_iff)
    then obtain ε where he:
      "x. x  U  ε x > 0" "x. x  U  open_ball x (ε x)  U"
      by metis
    hence "( { open_ball x (ε x) | x. x  U}) = U"
      using U  S open_ball_ina[of _ "ε _"] by fastforce
    thus "𝒰. U =  𝒰  𝒰  {open_ball a ε |a ε. a  S  0 < ε}"
      using he(1) U  S by(fastforce intro!: exI[where x="{ open_ball x (ε x) | x. x  U}"])
  qed(use mtopology_open_ball_in in blast)
qed

abbreviation sequence :: "(nat  'a) set" where
"sequence  UNIV  S"

lemma sequence_comp:
 "xn  sequence  (λn. (xn (a n)))  sequence"
 "xn  sequence  xn  an  sequence"
  by auto

definition converge_to_inS :: "[nat  'a, 'a]  bool" where
"converge_to_inS f s  f  sequence  s  S  (λn. dist (f n) s)  0"

lemma converge_to_inS_const:
  assumes "x  S"
  shows "converge_to_inS (λn. x) x"
  using assms dist_0[of x x] by(simp add: converge_to_inS_def)

lemma converge_to_inS_subseq:
  assumes "strict_mono a" "converge_to_inS f s"
  shows "converge_to_inS (f  a) s"
proof -
  have "((λn. dist (f n) s)  a)  0"
    using assms by(auto intro!: LIMSEQ_subseq_LIMSEQ simp: converge_to_inS_def)
  thus ?thesis
    using assms by(auto simp: converge_to_inS_def comp_def)
qed

lemma converge_to_inS_ignore_initial:
  assumes "converge_to_inS xn x"
  shows "converge_to_inS (λn. xn (n + k)) x"
  using LIMSEQ_ignore_initial_segment[of "λn. dist (xn n) x" 0 k] assms
  by(auto simp: converge_to_inS_def)

lemma converge_to_inS_offset:
  assumes "converge_to_inS (λn. xn (n + k)) x" "xn  sequence"
  shows "converge_to_inS xn x"
  using LIMSEQ_offset[of "λn. dist (xn n) x" k] assms
  by(auto simp: converge_to_inS_def)

lemma converge_to_inS_def2:
 "converge_to_inS f s  (f  sequence  s  S  (ε>0. N. nN. dist (f n) s < ε))"
proof
  assume h:"converge_to_inS f s "
  show "f  sequence  s  S  (ε>0. N. nN. dist (f n) s < ε)"
  proof safe
    fix ε :: real
    assume he:"0 < ε"
    have hs:"S. open S  0  S  (N. nN. dist (f n) s  S)"
      using h lim_explicit[of "λn. dist (f n) s" 0]
      by(simp add: converge_to_inS_def)
    then obtain N where
     "nN. dist (f n) s  {-1<..<ε}"
      using hs[of "{-1<..<ε}"] he by fastforce
    thus "N. nN. dist (f n) s < ε"
      by(auto intro!: exI[where x=N])
  qed(use h[simplified converge_to_inS_def] in auto)
next
  assume h:"f  sequence  s  S  (ε>0. N. nN. dist (f n) s < ε)"
  have "S. open S  0  S  (N. nN. dist (f n) s  S)"
  proof safe
    fix S :: "real set"
    assume hs:"open S" "0  S"
    then obtain ε where he:
      "ε > 0" "ball 0 ε  S"
      using open_contains_ball[of S] by fastforce
    then obtain N where
     "nN. dist (f n) s < ε"
      using h by auto
    thus "N. nN. dist (f n) s  S"
      using he dist_geq0 by(auto intro!: exI[where x=N])
  qed
  thus "converge_to_inS f s "
    using lim_explicit[of "λn. dist (f n) s" 0] h
    by(simp add: converge_to_inS_def)
qed

lemma converge_to_inS_def2':
 "converge_to_inS f s  (f  sequence  s  S  (ε>0. N. nN. (f n)  open_ball s ε))"
  unfolding converge_to_inS_def2 open_ball_def dist_sym[of s]
  by fastforce

lemma converge_to_inS_unique:
  assumes "converge_to_inS f x" "converge_to_inS f y"
  shows "x = y"
proof -
  have inS:"n. f n  S" "x  S" "y  S"
    using assms by(auto simp: converge_to_inS_def)
  have "¦dist x y¦ < ε" if "ε > 0" for ε
  proof -
    have "0 < ε / 2" using that by simp
    then obtain N1 N2 where hn:
     "n. n  N1  dist (f n) x < ε / 2" "n. n  N2  dist (f n) y < ε / 2"
      using assms converge_to_inS_def2 by blast
    have "dist x y  dist (f (max N1 N2)) x + dist (f (max N1 N2)) y"
      unfolding dist_sym[of "f (max N1 N2)" x] by(rule dist_tr[OF inS(2) inS(1)[of "max N1 N2"] inS(3)])
    also have "... < ε / 2 + ε / 2"
      by(rule add_strict_mono) (use hn[of "max N1 N2"] in auto)
    finally show ?thesis
      using dist_geq0[of x y] by simp
  qed
  hence "dist x y = 0"
    using zero_less_abs_iff by blast
  thus ?thesis
    using dist_0[OF inS(2,3)] by simp
qed

lemma mtopology_closedin_iff: "closedin mtopology M  M  S  (f(UNIV  M). s. converge_to_inS f s  s  M)"
proof
  assume "closedin mtopology M"
  then have h:"xS - M. ε>0. open_ball x ε  S - M"
    by (simp add: closedin_def mtopology_openin_iff mtopology_topspace)
  show "M  S  (fUNIV  M. s. converge_to_inS f s  s  M)"
  proof safe
    fix f :: "nat  'a" and s
    assume hf:"f  UNIV  M" "converge_to_inS f s"
    show "s  M"
    proof(rule ccontr)
      assume "s  M"
      then have "s  S - M"
        using hf(2) by(auto simp: converge_to_inS_def)
      then obtain ε where "ε > 0" "open_ball s ε  S - M"
        using h by auto
      then obtain N where "n. n  N  f n  open_ball s ε"
        using hf(2) by(auto simp: converge_to_inS_def2') metis
      from open_ball s ε  S - M this[of N] hf(1)
      show False by auto
    qed
  qed(rule subsetD[OF closedin_subset[OF closedin mtopology M,simplified mtopology_topspace]])
next
  assume h:"M  S  (fUNIV  M. s. converge_to_inS f s  s  M)"
  show "closedin mtopology M"
    unfolding closedin_def mtopology_openin_iff mtopology_topspace
  proof safe
    fix x
    assume "x  S" "x  M"
    show "ε>0. open_ball x ε  S - M"
    proof(rule ccontr)
      assume "¬ (ε>0. open_ball x ε  S - M)"
      then have "ε>0. open_ball x ε  M  {}"
        by (metis Diff_mono Diff_triv open_ball_subset_ofS subset_refl)
      hence "n. a. a  open_ball x (1 / real (Suc n))  M"
        by (meson of_nat_0_less_iff subsetI subset_empty zero_less_Suc zero_less_divide_1_iff)
      then obtain f where hf:"n. f n  open_ball x (1 / (Suc n))  M" by metis
      hence "f  UNIV  M" by auto
      moreover have "converge_to_inS f x"
        unfolding converge_to_inS_def2'
      proof safe
        show "f x  S" for x
          using h hf by auto
      next
        fix ε
        assume "(0::real) < ε"
        then obtain N where "1 / real (Suc N) < ε"
          using nat_approx_posE by blast
        show "N. nN. f n  open_ball x ε"
        proof(rule exI[where x=N])
          show "nN. f n  open_ball x ε"
          proof safe
            fix n
            assume "N  n"
            then have "1 / real (Suc n)  1 / real (Suc N)"
              by (simp add: frac_le)
            also have "...  ε"
              using 1 / real (Suc N) < ε by simp
            finally show "f n  open_ball x ε"
              using open_ball_le[of "1 / real (Suc n)" ε x] hf by auto
          qed
        qed
      qed fact
      ultimately show False
        using h x  M by blast
    qed
  qed(use h in auto)
qed

lemma mtopology_closedin_iff2: "closedin mtopology M  M  S  (x. x  M  (ε>0. open_ball x ε  M  {}))"
proof
  assume h:"closedin mtopology M"
  have 1: "M  S"
    using h by(auto simp add: mtopology_closedin_iff)
  show "M  S  (x. (x  M) = (ε>0. open_ball x ε  M  {}))"
  proof safe
    fix ε x
    assume "x  M" "(0 :: real) < ε" "open_ball x ε  M = {}"
    thus False
      using open_ball_ina[of x ε] 1 by blast
  next
    fix x
    assume "ε>0. open_ball x ε  M  {}"
    hence "f. f  open_ball x (1 / real (Suc n))  M" for n
      by (meson all_not_in_conv divide_pos_pos of_nat_0_less_iff zero_less_Suc zero_less_one)
    then obtain f where hf:"n. f n  open_ball x (1 / real (Suc n))  M"
      by metis
    hence "x  S" "f  UNIV  M"
      using open_ballD'(2)[of "f 0" x] by auto
    have "converge_to_inS f x"
      unfolding converge_to_inS_def2'
    proof safe
      show "x. f x  S"
        using 1 f  UNIV  M by auto
    next
      fix ε
      assume "(0 :: real) < ε"
      then obtain N where hN: "1 / real (Suc N) < ε"
        using nat_approx_posE by blast
      show "N. nN. f n  open_ball x ε"
      proof(rule exI[where x="N"])
        show "nN. f n  open_ball x ε"
        proof safe
          fix n
          assume "N  n"
          then have "1 / real (Suc n)  1 / real (Suc N)"
            using inverse_of_nat_le by blast
          thus "f n  open_ball x ε "
            using hf[of n] open_ball_le[of "1 / real (Suc n)" "ε" x] hN
            by auto
        qed
      qed
    qed fact
    with f  UNIV  M show "x  M"
      using h[simplified mtopology_closedin_iff] by simp
  qed(use 1 in auto)
next
  assume"M  S  (x. (x  M)  (ε>0. open_ball x ε  M  {}))"
  hence h:"M  S" "x. (x  M)  (ε>0. open_ball x ε  M  {})"
    by simp_all
  show "closedin mtopology M"
    unfolding mtopology_closedin_iff
  proof safe
    fix f s
    assume h':"f  UNIV  M" "converge_to_inS f s"
    hence "s  S" by(simp add: converge_to_inS_def)
    have "open_ball s ε  M  {}" if "ε > 0" for ε
    proof -
      obtain N where hN:"n. n  N  dist (f n) s < ε"
        using h'(2) ε > 0 by(auto simp: converge_to_inS_def2) metis
      have "f N  open_ball s ε  M"
        using f  UNIV  M s  S hN[of N] that open_ball_def[of s ε] h(1) dist_sym[of s]
        by auto
      thus "open_ball s ε  M  {}" by auto
    qed
    with h(2)[of s] show "s  M" by simp
  qed(use h(1) in auto)
qed

lemma mtopology_openin_iff2:
 "openin mtopology A  A  S  (f x. converge_to_inS f x  x  A  (N. nN. f n  A))"
proof
  show "openin mtopology A  A  S  (f x. converge_to_inS f x  x  A  (N. nN. f n  A))"
    unfolding mtopology_openin_iff
  proof safe
    fix f x
    assume "xA. ε>0. open_ball x ε  A" "converge_to_inS f x" "x  A"
    then obtain ε where "ε > 0" "open_ball x ε  A"
      by auto
    then obtain N where "n. n  N  dist (f n) x < ε"
      using converge_to_inS f x by(fastforce simp: converge_to_inS_def2)
    hence "n. n  N  f n  open_ball x ε"
      using converge_to_inS f x by(auto simp: dist_sym[of _ x] open_ball_def converge_to_inS_def)
    with open_ball x ε  A show "N. nN. f n  A"
      by(auto intro!: exI[where x=N])
  qed
next
  assume "A  S  (f x. converge_to_inS f x  x  A  (N. nN. f n  A))"
  hence h:"A  S" "f x. converge_to_inS f x  x  A  N. nN. f n  A"
    by auto
  have "closedin mtopology (S - A)"
    unfolding mtopology_closedin_iff
  proof safe
    fix f s
    assume hf:"f  UNIV  S - A"
              "converge_to_inS f s"
    have False if "s  A"
    proof -
      from h(2)[OF hf(2) that]
      obtain N where "n. n  N  f n  A" by auto
      from hf (1) this[of N] show False by auto
    qed
    thus "s  S" "s  A  False"
      using hf(2) by (auto simp: converge_to_inS_def)
  qed
  thus "openin mtopology A"
    using h(1) mtopology_topspace by(simp add: openin_closedin_eq)
qed

lemma closure_of_mtopology: "mtopology closure_of A = {a. ε>0. open_ball a ε  A  {}}"
proof safe
  fix x ε
  assume "x  mtopology closure_of A" "(0 :: real) < ε" "open_ball x ε  A = {}"
  then show False
    using mtopology_closedin_iff2[of "mtopology closure_of A",simplified]
    by (simp add: mtopology_open_ball_in' mtopology_openin_iff open_ball_subset_ofS openin_Int_closure_of_eq_empty)
next
  fix x
  assume "ε>0. open_ball x ε  A  {}"
  then have "ε>0. open_ball x ε  mtopology closure_of A  {}"
    by (simp add: mtopology_open_ball_in' mtopology_openin_iff open_ball_subset_ofS openin_Int_closure_of_eq_empty)
  thus "x  mtopology closure_of A"
    using mtopology_closedin_iff2[of "mtopology closure_of A",simplified]
    by auto
qed

lemma closure_of_mtopology':
 "mtopology closure_of A = {a. anUNIV  A. converge_to_inS an a}"
proof safe
  fix a
  assume "a  mtopology closure_of A"
  then have "ε>0. open_ball a ε  A  {}"
    by(simp add: closure_of_mtopology)
  hence "n. an. an  open_ball a (1/real (Suc n))  A"
    by (meson all_not_in_conv divide_pos_pos of_nat_0_less_iff zero_less_Suc zero_less_one)
  then obtain an where han:"n. an n  open_ball a (1/real (Suc n))  A" by metis
  hence "an  UNIV  A" by auto
  show "anUNIV  A. converge_to_inS an a"
  proof(safe intro!: bexI[where x=an] an  UNIV  A)
    show "converge_to_inS an a"
      unfolding converge_to_inS_def2'
    proof safe
      show "an n  S" "a  S" for n
        using open_ballD'(2)[of "an 0" a] open_ballD'(1)[of "an n"] han by auto
    next
      fix ε
      assume "(0 :: real) < ε"
      then obtain N where "1 / real (Suc N)  ε"
        by (meson less_eq_real_def nat_approx_posE)
      show "N. nN. an n  open_ball a ε"
      proof(safe intro!: exI[where x=N])
        fix n
        assume "N  n"
        then have "1 / real (Suc n)  1 / real (Suc N)"
          by (simp add: frac_le)
        from open_ball_le[OF order_trans[OF this 1 / real (Suc N)  ε]]
        show "an n  open_ball a ε"
          using han by auto
      qed
    qed
  qed
next
  fix a an
  assume h:"an  UNIV  A" "converge_to_inS an a"
  have "ε>0. open_ball a ε  A  {}"
  proof safe
    fix ε
    assume "(0 :: real) < ε" "open_ball a ε  A = {}"
    then obtain N where "an N  open_ball a ε"
      using h(2) converge_to_inS_def2' by blast
    with open_ball a ε  A = {} h(1) show False by auto
  qed
  thus "a  mtopology closure_of A"
    by(simp add: closure_of_mtopology)
qed

lemma closure_of_mtopology_an:
  assumes "a  mtopology closure_of A"
  obtains an where "anUNIV  A" "converge_to_inS an a"
  using assms by(auto simp: closure_of_mtopology')

lemma closure_of_open_ball: "mtopology closure_of open_ball a ε  closed_ball a ε"
  by(rule closure_of_minimal_eq[THEN iffD2]) (auto simp: open_ball_subset_ofS mtopology_topspace closedin_closed_ball open_ball_closed_ball)

lemma interior_of_closed_ball: "open_ball a e  mtopology interior_of closed_ball a e"
  by(auto simp: interior_of_maximal_eq openin_open_ball open_ball_closed_ball)

lemma derived_set_of_mtopology:
 "mtopology derived_set_of A = {a. anUNIV  A. (n. an n  a)  converge_to_inS an a}"
proof safe
  fix a
  assume "a  mtopology derived_set_of A"
  then have h:"a  S" "v. a  v  openin mtopology v  y. y  a  y  v  y  A"
    by(auto simp: in_derived_set_of mtopology_topspace)
  hence "a  open_ball a (1 / real (Suc n))" for n
    by(auto intro!: open_ball_ina)
  from h(2)[OF this openin_open_ball[of a]]
  obtain an where an:"n. an n  a" "n. an n  open_ball a (1 / real (Suc n))" "n. an n  A"
    by metis
  show "anUNIV  A. (n. an n  a)  converge_to_inS an a"
  proof(safe intro!: bexI[where x=an] an(1))
    show "converge_to_inS an a"
      unfolding converge_to_inS_def2'
    proof safe
      show "x. an x  S"
        using an(2) open_ball_subset_ofS by auto
    next
      fix ε
      assume "(0 :: real) < ε"
      then obtain N where hN:"1 / real (Suc N) < ε"
        using nat_approx_posE by blast
      show "N. nN. an n  open_ball a ε"
      proof(safe intro!: exI[where x=N])
        fix n
        assume "N  n"
        then have "1 / real (Suc n)  1 / real (Suc N)"
          by (simp add: frac_le)
        from order.strict_trans1[OF this hN] open_ball_le[of _ ε a] an(2)[of n]
        show "an n  open_ball a ε" by(auto simp: less_le)
      qed
    qed(use h in auto)
  qed(use an in auto)
next
  fix a an
  assume h:"an  UNIV  A" "n. an n  a" "converge_to_inS an a"
  have "y. y  a  y  v  y  A" if "a  v" "openin mtopology v" for v
  proof -
    obtain ε where he:"ε > 0" "a  open_ball a ε" "open_ball a ε  v"
      by (meson a  v openin mtopology v converge_to_inS_def2 h(3) mtopology_openin_iff open_ball_ina)
    then obtain N where hn:"n. n  N  an n  open_ball a ε"
      using h(3) by(fastforce simp: converge_to_inS_def2')
    show " y. y  a  y  v  y  A"
      using h(1,2) he hn by(auto intro!: exI[where x="an N"])
  qed
  thus "a  mtopology derived_set_of A"
    using h(3) by(auto simp: in_derived_set_of converge_to_inS_def mtopology_topspace)
qed

lemma isolated_points_of_mtopology:
 "mtopology isolated_points_of A = {aSA. anUNIV  A. converge_to_inS an a  (no. nno. an n = a)}"
proof safe
  fix a an
  assume h:"a  mtopology isolated_points_of A" "converge_to_inS an a" "an  UNIV  A"
  then have ha:"a  topspace mtopology" "a  A" "U. a  U  openin mtopology U  U  (A - {a}) = {}"
    by(simp_all add: in_isolated_points_of)
  then obtain U where u:"a  U" "openin mtopology U" "U  (A - {a}) = {}"
    by auto
  then obtain ε where e: "ε > 0" "open_ball a ε  U"
    by(auto simp: mtopology_openin_iff)
  then obtain N where "n. n  N  an n  open_ball a ε"
    using h(2) by(fastforce simp: converge_to_inS_def2')
  thus "no. nno. an n = a"
    using h(3) e(2) u(3) by(auto intro!: exI[where x=N])
qed (auto simp: derived_set_of_mtopology isolated_points_of_def mtopology_topspace)

lemma perfect_set_open_ball_infinite:
  assumes "perfect_set mtopology A"
  shows "closedin mtopology A  (aA. ε>0. infinite (open_ball a ε))"
proof safe
  fix a ε
  assume h: "a  A" "0 < ε" "finite (open_ball a ε)"
  then have "a  S"
    using open_ball_ina[OF _ 0 < ε,of a] perfect_setD(2)[OF assms]
    by(auto simp: mtopology_topspace)
  have "e > 0. open_ball a e = {a}"
  proof -
    consider "open_ball a ε = {a}" | "{a}  open_ball a ε"
      using open_ball_ina[OF a  S h(2)] by blast
    thus ?thesis
    proof cases
      case 1
      with h(2) show ?thesis by auto
    next
      case 2
      then have nen:"{dist a b |b. b  open_ball a ε  a  b}  {}"
        by auto
      have fin: "finite {dist a b |b. b  open_ball a ε  a  b}"
        using h(3) by auto
      define e where "e  Min {dist a b |b. b  open_ball a ε  a  b}"
      have "e > 0"
        using dist_0[OF a  S open_ballD'(1)[of _ a ε]] dist_geq0[of a]
        by(auto simp: e_def Min_gr_iff[OF fin nen] order_neq_le_trans)
      have bd:"b. b  open_ball a ε  a  b  e  dist a b"
        by(auto simp: e_def Min_le_iff[OF fin nen])
      have "e  ε"
        using nen open_ballD[of _ a ε]
        by(fastforce simp add: e_def Min_le_iff[OF fin nen])
      show ?thesis
      proof(safe intro!: exI[where x=e])
        fix x
        assume x:"x  open_ball a e"
        then show "x = a"
          using open_ball_le[OF e  ε,of a] open_ballD[OF x] bd[of x]
          by auto
      qed (simp_all add: open_ball_ina[OF a  S e > 0] 0 < e)
    qed
  qed
  then obtain e where e:"e > 0" "open_ball a e = {a}" by auto
  show False
    using perfect_setD(3)[OF assms h(1) open_ball_ina[OF a  S e > 0]]
    by(auto simp: openin_open_ball) (use e(2) in auto)
qed(use perfect_setD[OF assms] in simp)

lemma nbh_subset:
  assumes A: "A  S" and e: "e > 0"
  shows "A  (aA. open_ball a e)"
  using A open_ball_ina[OF _ e] by auto

lemma nbh_decseq:
  assumes "decseq an"
  shows "decseq (λn. aA. open_ball a (an n))"
proof(safe intro!: decseq_SucI)
  fix n a b
  assume "a  A" "b  open_ball a (an (Suc n))"
  with open_ball_le[OF decseq_SucD[OF assms]] show "b  (cA. open_ball c (an n))"
    by(auto intro!: bexI[where x=a] simp: frac_le)
qed

lemma nbh_Int:
  assumes A: "A  {}" "A  S"
      and an:"n. an n > 0" "decseq an" "an  0"
  shows "(n. aA. open_ball a (an n)) = mtopology closure_of A"
proof safe
  fix x
  assume "x  (n. aA. open_ball a (an n))"
  then have h:"n. aA. x  open_ball a (an n)"
    by auto
  hence x:"x  S"
    using open_ball_subset_ofS by auto
  show "x  mtopology closure_of A"
    unfolding closure_of_mtopology
  proof safe
    fix e :: real
    assume h':"e > 0" "open_ball x e  A = {}"
    then obtain n where n:"an n < e"
      using an(1,3) by(auto simp: LIMSEQ_def abs_of_pos) (metis dual_order.refl)
    from h obtain a where "a  A" "x  open_ball a (an n)"
      by auto
    with h'(2) open_ball_le[of "an n" e x] n
    show False
      by(auto simp: open_ball_inverse[of x])
  qed
next
  fix x n
  assume "x  mtopology closure_of A"
  with an(1) have "open_ball x (an n)  A  {}"
    by(auto simp: closure_of_mtopology)
  thus "x  (aA. open_ball a (an n))"
    by(auto simp: open_ball_inverse[of x])
qed

lemma nbh_add: "(b(aA. open_ball a e). open_ball b f)  (aA. open_ball a (e + f))"
proof safe
  fix a x b
  assume h:"a  A" "b  open_ball a e" "x  open_ball b f"
  show "x  (aA. open_ball a (e + f))"
  proof(rule UN_I[OF h(1)])
    have "dist a x  dist a b + dist b x"
      by(auto intro!: dist_tr open_ballD'(2)[OF h(2)] open_ballD'[OF h(3)])
    also have "... < e + f"
      using  open_ballD[OF h(2)] open_ballD[OF h(3)] by auto
    finally show "x  open_ball a (e + f)"
      using open_ballD'[OF h(2)] open_ballD'[OF h(3)]
      by(auto simp: open_ball_def)
  qed
qed

definition convergent_inS :: "(nat  'a)  bool" where
"convergent_inS f  s. converge_to_inS f s"

lemma convergent_inS_const:
  assumes "x  S"
  shows "convergent_inS (λn. x)"
  using converge_to_inS_const[OF assms] by(auto simp: convergent_inS_def)

lemma convergent_inS_ignore_initial:
  assumes "convergent_inS xn"
  shows "convergent_inS (λn. xn (n + k))"
  using converge_to_inS_ignore_initial[of xn] assms
  by(auto simp: convergent_inS_def)

lemma convergent_inS_offset:
  assumes "convergent_inS (λn. xn (n + k))" "xn  sequence"
  shows "convergent_inS xn"
  using converge_to_inS_offset[of xn k] assms
  by(auto simp: convergent_inS_def)

definition the_limit_of :: "(nat  'a)  'a" where
"the_limit_of xn  THE x. converge_to_inS xn x"

lemma the_limit_if_converge:
  assumes "convergent_inS xn"
  shows "converge_to_inS xn (the_limit_of xn)"
  unfolding the_limit_of_def
  by(rule theI') (auto simp: assms[simplified convergent_inS_def] converge_to_inS_unique)

lemma the_limit_of_eq:
  assumes "converge_to_inS xn x"
  shows "the_limit_of xn = x"
  using assms converge_to_inS_unique the_limit_of_def by auto

lemma the_limit_of_inS:
  assumes "convergent_inS xn"
  shows "the_limit_of xn  S"
  using the_limit_if_converge[OF assms] by(simp add:converge_to_inS_def)

lemma the_limit_of_const:
  assumes "x  S"
  shows "the_limit_of (λn. x) = x"
  by(rule the_limit_of_eq[OF converge_to_inS_const[OF assms]])

lemma convergent_inS_dest1:
  assumes "convergent_inS f"
  shows "f n  S"
  using assms by(auto simp: convergent_inS_def converge_to_inS_def2)

definition Cauchy_inS:: "(nat  'a)  bool" where
"Cauchy_inS f  f  sequence  (ε>0. N. nN. mN. dist (f n) (f m) < ε)"

lemma Cauchy_inS_def2:
 "Cauchy_inS f  f  sequence  (ε>0. N. nN. f n  open_ball (f N) ε)"
  unfolding Cauchy_inS_def
proof safe
  fix ε :: real
  assume h:"f  sequence" " ε>0. N. nN. mN. dist (f n) (f m) < ε" "0 < ε"
  then obtain N where hn:
     "n m. n  N   mN  dist (f n) (f m) < ε"
    by fastforce
  show "N. nN. f n  open_ball (f N) ε"
  proof(safe intro!: exI[where x=N])
    fix n
    assume "N  n"
    then show "f n  open_ball (f N) ε"
      using h(1) hn[of N n] by(auto simp: open_ball_def)
  qed
next
  fix ε :: real
  assume h:"f  sequence" "ε>0. N. nN. f n  open_ball (f N) ε" "0 < ε"
  then obtain N where hn:
   "n. n  N  f n  open_ball (f N) (ε/2)"
    using linordered_field_class.half_gt_zero[OF h(3)] by blast
  show "N. nN. mN. dist (f n) (f m) < ε"
  proof(safe intro!: exI[where x=N])
    fix n m
    assume "N  n" "N  m"
    from order.strict_trans1[OF dist_tr [of "f n" "f N" "f m"] strict_ordered_ab_semigroup_add_class.add_strict_mono[OF open_ballD[OF hn[OF this(1)],simplified dist_sym[of _ "f n"]] open_ballD[OF hn[OF this(2)]],simplified]]
    show "dist (f n) (f m) < ε"
      using h(1) by auto
  qed
qed

lemma Cauchy_inS_def2':
 "Cauchy_inS f  f  sequence  (ε>0. xS. N. nN. f n  open_ball x ε)"
  unfolding Cauchy_inS_def2
proof safe
  fix ε :: real
  assume h:"f  sequence" "ε>0. N. nN. f n  open_ball (f N) ε" "0 < ε"
  then obtain N where "nN. f n  open_ball (f N) ε" by auto
  thus "xS. N. nN. f n  open_ball x ε"
    using h(1) by(auto intro!: exI[where x=N] bexI[where x="f N"])
next
  fix ε :: real
  assume h:"f  sequence" "ε>0. xS. N. nN. f n  open_ball x ε" "0 < ε"
  then obtain x N where hxn:
   "x  S" "n. n  N  f n  open_ball x (ε/2)"
    using linordered_field_class.half_gt_zero[OF h(3)] by blast
  show "N. nN. f n  open_ball (f N) ε"
  proof(safe intro!: exI[where x=N])
    fix n
    assume "N  n"
    from order.strict_trans1[OF dist_tr strict_ordered_ab_semigroup_add_class.add_strict_mono[OF open_ballD[OF hxn(2)[OF order.refl],simplified dist_sym[of x]] open_ballD[OF hxn(2)[OF this]],simplified]]
    show "f n  open_ball (f N) ε"
      using hxn(1) h(1) by(auto simp: open_ball_def)
  qed
qed

lemma Cauchy_inS_def2'':
 "Cauchy_inS f  f  sequence  (ε>0. xS. N. nN. dist x (f n) < ε)"
  unfolding Cauchy_inS_def2'
proof safe
  fix ε :: real
  assume h:"f  sequence" "ε>0. xS. N. nN. f n  open_ball x ε" "0 < ε"
  then obtain x N where
   "x  S" "n. n  N  f n  open_ball x ε"
    by blast
  then show "xS. N. nN. dist x (f n) < ε"
    by(auto intro!: bexI[where x=x] exI[where x=N] simp: open_ballD[of _ x ε])
next
  fix ε :: real
  assume h:"f  sequence" "ε>0. xS. N. nN. dist x (f n) < ε" "0 < ε"
  then obtain x N where 
   "x  S" "n. n  N  dist x (f n) < ε" by blast
  then show "xS. N. nN. f n  open_ball x ε"
    using h(1) by(auto intro!: bexI[where x=x] exI[where x=N] simp: open_ball_def)
qed

lemma Cauchy_inS_dest1:
  assumes "Cauchy_inS f"
  shows "f n  S"
  using assms by(auto simp: Cauchy_inS_def)

lemma Cauchy_if_convergent_inS:
  assumes "convergent_inS f"
  shows "Cauchy_inS f"
  unfolding Cauchy_inS_def
proof safe
  fix ε :: real
  assume h:"0 < ε"
  obtain s where hs:
   "s  S" "ε>0. N. nN. dist (f n) s < ε"
    using assms by(auto simp: convergent_inS_def converge_to_inS_def2)
  then obtain N where hn:
    "n. nN  dist (f n) s < ε/2"
    using half_gt_zero[OF h] by blast
  show "N. nN. mN. dist (f n) (f m) < ε"
  proof(safe intro!: exI[where x=N])
    fix n m
    assume hnm:"N  n" "N  m"
    have "dist (f n) (f m)  dist (f n) s + dist s (f m)"
      using convergent_inS_dest1[OF assms] hs
      by(auto intro!: dist_tr)
    also have "... = dist (f n) s + dist (f m) s"
      by(simp add: dist_sym[of s])
    also have "... < ε"
      using hn[OF hnm(1)] hn[OF hnm(2)] by auto
    finally show "dist (f n) (f m) < ε" .
  qed
next
  show "x. f x  S"
    using assms[simplified convergent_inS_def converge_to_inS_def]
    by auto
qed

corollary Cauchy_inS_const: "a  S  Cauchy_inS (λn. a)"
  by(auto intro!: Cauchy_if_convergent_inS convergent_inS_const)

lemma converge_if_Cauchy_and_subconverge:
  assumes "strict_mono a" "converge_to_inS (f  a) s" "Cauchy_inS f"
  shows "converge_to_inS f s"
  unfolding  converge_to_inS_def2
proof safe
  fix ε
  assume "(0 :: real) < ε"
  then have 1:"0 < ε/2" by auto
  then obtain N where hn:"n. n  N  dist (f (a n)) s < ε/2"
    using assms(2) by(simp only: comp_def converge_to_inS_def2) metis
  obtain N' where hn':"n m. n  N'  m  N'  dist (f n) (f m) < ε/2"
    using assms(3) 1 by(simp only: Cauchy_inS_def) metis
  show "N. nN. dist (f n) s < ε"
  proof(safe intro!: exI[where x="max N N'"])
    fix n
    assume "max N N'  n"
    then have "N  n" "N'  n" by auto
    show "dist (f n) s < ε"
      using add_strict_mono[OF hn'[OF N'  n order_trans[OF N'  n seq_suble[OF assms(1),of n]]] hn[OF N  n]]  assms(2)
      by(auto simp: converge_to_inS_def intro!: order.strict_trans1[OF dist_tr[OF Cauchy_inS_dest1[OF assms(3),of n] Cauchy_inS_dest1[OF assms(3),of "a n"],of s],of ε])
  qed
qed(auto simp: Cauchy_inS_dest1[OF assms(3)] assms(2)[simplified converge_to_inS_def])

lemma subCauchy_Cahcuy:
  assumes "Cauchy_inS xn" "strict_mono a"
  shows "Cauchy_inS (xn  a)"
  unfolding Cauchy_inS_def
proof safe
  show "x. (xn  a) x  S"
    using assms(1) by(simp add: Cauchy_inS_dest1)
next
  fix ε
  assume "(0 :: real) < ε"
  then obtain N where "n m. n  N  m  N  dist (xn n) (xn m) < ε"
    using assms(1) by(auto simp: Cauchy_inS_def) metis
  thus "N. nN. mN. dist ((xn  a) n) ((xn  a) m) < ε"
    by(auto intro!: exI[where x=N] dest: order_trans[OF seq_suble[OF assms(2)] strict_mono_leD[OF assms(2)]])
qed

corollary Cauchy_inS_ignore_initial:
  assumes "Cauchy_inS xn"
  shows "Cauchy_inS (λn. xn (n + k))"
  using subCauchy_Cahcuy[OF assms,of "λn. n + k"]
  by(auto simp: comp_def strict_monoI)

(* TODO: offset *)

lemma Cauchy_inS_dist_Cauchy:
  assumes "Cauchy_inS xn" "Cauchy_inS yn"
  shows "Cauchy (λn. dist (xn n) (yn n))"
  unfolding metric_space_class.Cauchy_altdef2 dist_real_def
proof safe
  have h:"n. xn n  S" "n. yn n  S"
    using assms by(auto simp: Cauchy_inS_dest1)
  fix e :: real
  assume e:"0 < e"
  with assms obtain N1 N2 where N: "n m. n  N1  m  N1  dist (xn n) (xn m) < e / 2" "n m. n  N2  m  N2  dist (yn n) (yn m) < e / 2"
    by (metis Cauchy_inS_def zero_less_divide_iff zero_less_numeral)
  define N where "N  max N1 N2"
  then have N': "N  N1" "N  N2" by auto
  show "N. nN. ¦dist (xn n) (yn n) - dist (xn N) (yn N)¦ < e"
  proof(safe intro!: exI[where x=N])
    fix n
    assume n:"N  n"
    have "dist (xn n) (yn n)  dist (xn n) (xn N) + dist (xn N) (yn N) + dist (yn N) (yn n)"
         "dist (xn N) (yn N)  dist (xn N) (xn n) + dist (xn n) (yn n) + dist (yn n) (yn N)"
      using dist_tr[OF h(1)[of n] h(1)[of N] h(2)[of n]] dist_tr[OF h(1)[of N] h(2)[of N] h(2)[of n]]
            dist_tr[OF h(1)[of N] h(2)[of n] h(2)[of N]] dist_tr[OF h(1)[of N] h(1)[of n] h(2)[of n]] by auto
    thus "¦dist (xn n) (yn n) - dist (xn N) (yn N)¦ < e"
      using N(1)[OF N'(1) order.trans[OF N'(1) n]] N(2)[OF N'(2) order.trans[OF N'(2) n]] N(1)[OF order.trans[OF N'(1) n] N'(1)] N(2)[OF order.trans[OF N'(2) n] N'(2)]
      by auto
  qed
qed

corollary Cauchy_inS_dist_convergent:
  assumes "Cauchy_inS xn" "Cauchy_inS yn"
  shows "convergent (λn. dist (xn n) (yn n))"
  using Cauchy_inS_dist_Cauchy[OF assms] Cauchy_convergent_iff by blast

text 🌐‹https://people.bath.ac.uk/mw2319/ma30252/sec-dense.html.›
abbreviation "dense_set  dense_of mtopology"

lemma dense_set_def:
 "dense_set U  U  S  (xS. ε>0. open_ball x ε  U  {})"
proof
  assume h:" U  S (xS. ε>0. open_ball x ε  U  {})"
  show "dense_of mtopology U"
  proof(rule dense_ofI)
    fix V
    assume h':"openin mtopology V" "V  {}"
    then obtain x where 1:"x  V" by auto
    then obtain ε where 2:"ε>0" "open_ball x ε  V"
      using h' mtopology_openin_iff[of V] by blast
    have "open_ball x ε  U  {}"
      using h 1 2 openin_subset[OF h'(1), simplified mtopology_topspace]
      by auto
    thus "U  V  {}" using 2 by auto
  next
    show "U  topspace mtopology"
      using h mtopology_topspace by auto
  qed 
next
  assume h:"dense_of mtopology U"
  have "xS. ε>0. open_ball x ε  U  {}"
  proof safe
    fix x ε
    assume "x  S" "(0 :: real) < ε" "open_ball x ε  U = {}"
    then have "open_ball x ε  {}" "openin mtopology (open_ball x ε)"
      using open_ball_ina[of x ε] mtopology_open_ball_in[of x ε]
      by blast+
    thus False
      using h open_ball x ε  U = {} by(auto simp: dense_of_def)
  qed
  thus "U  S  (xS. ε>0. open_ball x ε  U  {})"
    using h mtopology_topspace by(auto simp: dense_of_def)
qed

corollary dense_set_balls_cover:
  assumes "dense_set U" and "e > 0"
  shows "(uU. open_ball u e) = S"
  using assms open_ball_subset_ofS by(auto simp: dense_set_def) (meson Int_emptyI open_ball_inverse)

lemma dense_set_empty_iff: "dense_set {}  S = {}"
  by(auto simp: dense_set_def ) (use zero_less_one in blast)

lemma dense_set_S: "dense_set S"
  using open_ball_ina dense_set_def by blast

lemma dense_set_def2:
 "dense_set U  U  S  (xS. ε>0.yU. dist x y < ε)"
proof
  assume h: "dense_set U"
  show "U  S  (xS. ε>0. yU. dist x y < ε)"
  proof safe
    fix x ε
    assume hxe: "x  S" "(0 :: real) < ε"
    then obtain z where
      "z  open_ball x ε  U"
      using h by(fastforce simp: dense_set_def)
    thus "yU. dist x y < ε"
      by(auto intro!: bexI[where x=z] simp: open_ball_def hxe)
  qed(use h[simplified dense_set_def] in auto)
next
  assume h:"U  S  (xS. ε>0. yU. dist x y < ε)"
  show "dense_set U"
    unfolding dense_set_def
  proof safe
    fix x ε
    assume hxe: "x  S" "(0 :: real) < ε" "open_ball x ε  U = {}"
    then obtain y where
      "y  U" "y  S" "dist x y < ε"
      using h by blast
    hence "y  open_ball x ε  U"
      by(auto simp: open_ball_def hxe)
    thus False
      using hxe(3) by auto
  qed(use h in auto)
qed

lemma dense_set_def2':
 "dense_set U  U  S  (xS. fUNIV  U. converge_to_inS f x)"
  unfolding dense_set_def
proof
  show "U  S  (xS. ε>0. open_ball x ε  U  {})  U  S  (xS. fUNIV  U. converge_to_inS f x)"
  proof safe
    fix x
    assume h: "U  S" "xS. ε>0. open_ball x ε  U  {}" "x  S"
    then have "n::nat. open_ball x (1 / (real n + 1))  U  {}"
      by auto
    hence "n. k. k  open_ball x (1 / (real n + 1))  U" by auto
    hence "a. n. a n  open_ball x (1 / (real n + 1))  U" by(rule choice)
    then obtain a where hf: "n :: nat. a n  open_ball x (1 / (real n + 1))  U"
      by auto
    show "fUNIV  U. converge_to_inS f x"
      unfolding converge_to_inS_def2'
    proof(safe intro!: bexI[where x=a])
      fix ε :: real
      assume he:"0 < ε"
      then obtain N where hn: "1 / ε < real N"
        using reals_Archimedean2 by blast
      have hn': "0 < real N"
        by(rule ccontr) (use hn he in fastforce)
      hence "1 / real N < ε"
        using he hn by (metis divide_less_eq mult.commute)
      hence hn'':"1 / (real N + 1) < ε"
        using hn' by(auto intro!: order.strict_trans[OF linordered_field_class.divide_strict_left_mono[of "real N" "real N + 1" 1]])
      show "N. nN. a n  open_ball x ε"
      proof(safe intro!: exI[where x="N"])
        fix n
        assume "N  n"
        then have 1:"1 / (real n + 1)  1 / (real N + 1)"
          using hn' by(auto intro!: linordered_field_class.divide_left_mono)
        show "a n  open_ball x ε"
          using open_ball_le[OF 1,of x] open_ball_le[OF order.strict_implies_order[OF hn''],of x] hf[of n]
          by auto
      qed
    next
      show "x. a x  S" "x  S" "x. a x  U"
        using h(1,3) hf by auto
    qed
  qed
next
  assume h:"U  S  (xS. fUNIV  U. converge_to_inS f x)"
  have "xS. ε>0. open_ball x ε  U  {}"
  proof safe
    fix x ε
    assume hxe:"x  S" "(0 :: real) < ε" "open_ball x ε  U = {}"
    then obtain f N where
     "fUNIV  U" "nN :: nat. f n  open_ball x ε"
      using h[simplified converge_to_inS_def2'] by blast
    hence "f N  open_ball x ε  U"
      by auto
    thus False using hxe by auto
  qed
  thus "U  S  (xS. ε>0. open_ball x ε  U  {})"
    using h by auto
qed

lemma dense_set_infinite:
  assumes "infinite S" "dense_set U"
  shows "infinite U"
proof
  assume finu:"finite U"
  with assms(1) obtain x where x:"x  S" "x  U"
    by (meson finite_subset subset_iff)
  define e where "e  Min {dist x y |y. y  U}"
  have nen: "{dist x y |y. y  U}  {}"
    using dense_set_empty_iff assms by auto
  have fin: "finite {dist x y |y. y  U}"
    using finu by auto
  have epos: "0 < e"
    unfolding Min_gr_iff[OF fin nen] e_def
  proof safe
    fix y
    assume "y  U"
    then have "y  S" "x  y"
      using assms(2) x(2) by(auto simp: dense_set_def)
    thus "0 < dist x y"
      using dist_0[OF x(1),of y] dist_geq0[of x y] by auto
  qed
  then obtain y where y:"yU" "dist x y < e"
    using assms(2) x(1) by(fastforce simp: dense_set_def2)
  thus False
    using Min_le[OF fin,of "dist x y"] by(auto simp: e_def)
qed

lemma mtopology_Hausdorff: "Hausdorff_space mtopology"
  unfolding Hausdorff_space_def
proof safe
  fix x y
  assume "x  topspace mtopology" "y  topspace mtopology" "x  y"
  then have [simp]:"x  S" "y  S"
    using mtopology_topspace by auto
  with x  y have 1:"dist x y > 0"
    using dist_0[of x y] dist_geq0[of x y] by auto
  show "U V. openin mtopology U  openin mtopology V  x  U  y  V  disjnt U V"
  proof(rule exI[where x="open_ball x (dist x y/2)"])
    show "V. openin mtopology (open_ball x (dist x y / 2))  openin mtopology V  x  open_ball x (dist x y / 2)  y  V  disjnt (open_ball x (dist x y / 2)) V"
    proof(safe intro!: exI[where x="open_ball y (dist x y/2)"])
      show "disjnt (open_ball x (dist x y / 2)) (open_ball y (dist x y / 2))"
        unfolding disjnt_iff
      proof safe
        fix z
        assume h:"z  open_ball x (dist x y / 2)" "z  open_ball y (dist x y / 2)"
        show False
          using dist_tr[OF x  S open_ballD'(1)[OF h(1)] y  S] open_ballD[OF h(1)] open_ballD[OF h(2)]
          by (simp add: dist_sym)
      qed
    qed(auto intro!: mtopology_open_ball_in 1 open_ball_ina)
  qed
qed

text ‹ Diameter›
definition diam :: "'a set  ennreal" where
"diam A   {ennreal (dist x y) | x y. x  A  S  y  A  S}"

lemma diam_empty[simp]:
 "diam {} = 0"
  by(simp add: diam_def bot_ennreal)

lemma diam_def2:
  assumes "A  S"
  shows "diam A =  {ennreal (dist x y) | x y. x  A  y  A}"
  using assms by(auto simp: diam_def) (meson subset_eq)

lemma diam_subset:
  assumes "A  B"
  shows "diam A  diam B"
  unfolding diam_def using assms by(auto intro!: Sup_subset_mono)

lemma diam_cball_leq: "diam (closed_ball a ε)  ennreal (2 * ε)"
  unfolding Sup_le_iff diam_def
proof safe
  fix x y
  assume h:"x  closed_ball a ε" "y  closed_ball a ε" "x  S" "y  S"
  have "dist x y  2 * ε"
    using dist_tr[OF h(3) closed_ballD'(2)[OF h(1)] h(4)] closed_ballD[OF h(1),simplified dist_sym[of a x]] closed_ballD[OF h(2)]
    by auto
  thus "ennreal (dist x y)  ennreal (2 * ε)"
    using dist_geq0[of x y] ennreal_leI[of _ "2*ε"] by simp
qed

lemma diam_ball_leq:
 "diam (open_ball a ε)  ennreal (2 * ε)"
  using diam_subset[OF open_ball_closed_ball[of a ε]] diam_cball_leq[of a ε]
  by auto

lemma diam_is_sup:
  assumes "x  A  S" "y  A  S"
  shows "dist x y  diam A"
  using assms by(auto simp: diam_def intro!:Sup_upper)

lemma diam_is_sup':
  assumes "x  A  S" "y  A  S" "diam A  ennreal r" "r  0"
  shows "dist x y  r"
  using order.trans[OF diam_is_sup[OF assms(1,2)] assms(3)] assms(4) by simp

lemma diam_le:
  assumes "x y. x  A  y  A  dist x y  r"
  shows "diam A  r"
  using assms by(auto simp: diam_def Sup_le_iff ennreal_leI)

lemma diam_eq_closure: "diam (mtopology closure_of A) = diam A"
proof(rule antisym)
  show "diam A  diam (mtopology closure_of A)"
    by(auto intro!: Sup_subset_mono simp: diam_def) (metis in_closure_of mtopology_topspace)
next
  have "{ennreal (dist x y) |x y. x  A  S  y  A  S} = ennreal ` {dist x y |x y. x  A  S  y  A  S}"
    by auto
  also have "diam (mtopology closure_of A)   ..."
    unfolding le_Sup_iff_less
  proof safe
    fix r
    assume "r < diam (mtopology closure_of A)"
    then obtain x y where xy:"x  mtopology closure_of A" "x  S" "y  mtopology closure_of A" "y  S" "r < ennreal (dist x y)"
      by(auto simp: diam_def less_Sup_iff)
    hence "r < "
      using dual_order.strict_trans ennreal_less_top by blast
    define e where "e  (dist x y - enn2real r)/2"
    have "e > 0"
      using xy(5) r <  by(simp add: e_def)
    then obtain x' y' where xy':"x'  open_ball x e" "x' A" "y'  open_ball y e" "y' A"
      using xy by(fastforce simp: closure_of_mtopology)
    show "i{dist x y |x y. x  A  S  y  A  S}. r  ennreal i"
    proof(safe intro!: bexI[where x="dist x' y'"])
      have "dist x y  dist x x' + dist x' y' + dist y y'"
        using dist_tr[OF xy(2) open_ballD'(1)[OF xy'(1)] xy(4)] dist_tr[OF open_ballD'(1)[OF xy'(1)] open_ballD'(1)[OF xy'(3)] xy(4)]
        by(simp add: dist_sym)
      also have "... < dist x y - enn2real r + dist x' y'"
        using open_ballD[OF xy'(1)] open_ballD[OF xy'(3)]
        by(simp add: e_def)
      finally have "enn2real r < dist x' y'" by simp
      thus "r  ennreal (dist x' y')"
        by (simp add: r < )
    qed(use open_ballD'(1)[OF xy'(1)] open_ballD'(1)[OF xy'(3)] xy'(2,4) in auto)
  qed
  finally show "diam (mtopology closure_of A)  diam A"
    by(simp add: diam_def)
qed

definition bounded_set :: "'a set  bool" where
"bounded_set A  diam A < "

lemma bounded_set_def2': "bounded_set A  (e. xAS. yAS. dist x y < e)"
proof
  assume "bounded_set A"
  consider "A  S = {}" | "A  S  {}" by auto
  then show " e. xA  S. yA  S. dist x y < e"
  proof cases
    case h:2
    then have 1:"{dist x y |x y. x  A  S  y  A  S}  {}" by auto
    have eq:"{ennreal (dist x y) | x y. x  A  S  y  A  S} = ennreal ` {dist x y | x y. x  A  S  y  A  S}"
      by auto
    hence 2:"diam A =  (ennreal ` {dist x y | x y. x  A  S  y  A  S})"
      by(simp add: diam_def)
    obtain x y where hxy:
     "x  A  S" "y  A  S" "diam A < ennreal (dist x y) + ennreal 1"
      using SUP_approx_ennreal[OF _ 1 2,of 1] bounded_set A
      by(fastforce simp: bounded_set_def)
    hence "diam A < ennreal (dist x y + 1)"
      using dist_geq0 by simp
    from SUP_lessD[OF this[simplified 2]]
    have "w z. w  A  S  z  A  S  ennreal (dist w z) < ennreal (dist x y + 1)"
      by blast
    thus "e. xA  S. yA  S. dist x y < e"
      by(auto intro!: exI[where x="dist x y + 1"] simp: ennreal_less_iff[OF dist_geq0])
  qed simp
next
  assume "e. xAS. yAS. dist x y < e"
  then obtain e where he: "x y. x  A  S  y  A  S  dist x y < e"
    by auto
  hence "z. z  {ennreal (dist x y) | x y. x  A  S  y  A  S}  z < ennreal e"
    using ennreal_less_iff[OF dist_geq0] by auto
  hence " {ennreal (dist x y) | x y. x  A  S  y  A  S}  ennreal e"
    by (meson Sup_least order_less_le)
  thus "bounded_set A"
    by(simp add: bounded_set_def diam_def order_le_less_trans[OF _  ennreal_less_top])
qed

lemma bounded_set_def2:
  assumes "A  S"
  shows "bounded_set A  (e. xA. yA. dist x y < e)"
  using assms by(fastforce simp: bounded_set_def2')

lemma bounded_set_def3':
  assumes "S  {}"
  shows "bounded_set A  (e. xS. yAS. dist x y < e)"
  unfolding bounded_set_def2'
proof
  assume h:"e. xA  S. yA  S. dist x y < e"
  obtain s where [simp]:"s  S" using assms by auto
  consider "A  S = {}" | "A  S  {}" by auto
  then show "e. xS. yA  S. dist x y < e"
  proof cases
    case 1
    then show ?thesis
      by(auto intro!: exI[where x=0] exI[where x=s])
  next
    case 2
    then obtain sa where [simp]:"sa  A" "sa  S" by auto
    obtain e where "xA  S. yA  S. dist x y < e"
      using h by auto
    then show ?thesis
      by(auto intro!: exI[where x=e] bexI[where x=sa])
  qed
next
  assume "e. xS. yA  S. dist x y < e"
  then obtain e a where
   [simp]:"a  S" and hea:"y. y  A  y  S  dist a y < e" by auto
  show "e. xA  S. yA  S. dist x y < e"
  proof(safe intro!: exI[where x="2*e"])
    fix x y
    assume [simp]:"x  A" "x  S" "y  A" "y  S"
    show "dist x y < 2 * e"
      using dist_tr[of x a y] hea[of x] hea[of y]
      by(simp add: dist_sym[of x a])
  qed
qed

lemma bounded_set_def4':
 "bounded_set A  (x e. A  S  open_ball x e)"
proof
  assume h:"bounded_set A"
  consider "A  S = {}" | "A  S  {}" by auto
  then show "x e. A  S  open_ball x e"
  proof cases
    case 1
    then show ?thesis by auto
  next
    case 2
    then have "e. xS. yAS. dist x y < e"
      using bounded_set_def3' h by blast
    then obtain e x where
     [simp]: "x  S" and hex: "y. y  A  y  S  dist x y < e"
      by auto
    thus ?thesis
      by(auto intro!: exI[where x=x] exI[where x=e] simp:open_ball_def)
  qed
next
  assume "x e. A  S  open_ball x e"
  then obtain a e where hxe:"A  S  open_ball a e" by auto
  show "bounded_set A"
    unfolding bounded_set_def2'
  proof(safe intro!: exI[where x="2*e"])
    fix x y
    assume [simp]:"x  A" "x  S" "y  A" "y  S"
    then have "x  open_ball a e" "y  open_ball a e"
      using hxe by auto
    hence "dist a x < e" "dist a y < e" "a  S"
      by(auto dest: open_ballD open_ballD')
    thus "dist x y < 2 * e"
      using dist_tr[of x a y] by(simp add: dist_sym[of x a])
  qed
qed

lemma bounded_set_def4:
  assumes "A  S"
  shows "bounded_set A  (x e. A  open_ball x e)"
  using bounded_set_def4'[of A] assms by blast


text ‹ Distance between a point and a set. ›
definition dist_set :: "'a set  'a  real" where
"dist_set A  (λx. if A = {} then 0 else Inf {dist x y |y. y  A})"

lemma dist_set_geq0:
 "dist_set A x  0"
proof -
  have "{dist x y |y. y  A} = dist x ` A" by auto
  thus ?thesis
    using dist_geq0[of x] by(auto simp: dist_set_def intro!: cINF_greatest[of _ _ "dist x"])
qed

lemma dist_set_bdd_below[simp]:
 "bdd_below {dist x y |y. y  A}"
  by(auto simp: bdd_below_def dist_geq0 intro!: exI[where x=0])

lemma dist_set_singleton[simp]:
  "dist_set {y} x = dist x y"
  by(auto simp: dist_set_def)

lemma dist_set_singleton'[simp]:
  "dist_set {y} = (λx. dist x y)"
  by auto

lemma dist_set_empty[simp]:
 "dist_set {} x = 0"
  by(simp add: dist_set_def)

lemma dist_set_nsubset0[simp]:
  assumes "¬ (A  S)"
  shows "dist_set A x = 0"
proof -
  obtain a where "a  A" "a  S"
    using assms by auto
  hence "A  {}" "0  {dist x y |y. y  A}"
    using dist_notin'[of a x] by auto
  thus ?thesis
    using A  {} dist_set_geq0[of A x] cInf_lower[OF 0  {dist x y |y. y  A}]
    by(auto simp: dist_set_def)
qed

lemma dist_set_notin[simp]:
  assumes "x  S"
  shows "dist_set A x = 0"
proof -
  have "A  {}  {dist x y |y. y  A} = {0}"
    using dist_notin[OF x  S] by auto
  thus ?thesis
    by(simp add: dist_set_def)
qed

lemma dist_set_inA:
  assumes "x  A"
  shows "dist_set A x = 0"
proof(cases "A  S")
  case h:True
  hence "A  {}" "0  {dist x y |y. y  A}"
    using dist_0[of x x] assms by force+
  thus ?thesis
    using cInf_lower[OF 0  {dist x y |y. y  A}] dist_set_geq0[of A x]
    by(auto simp: dist_set_def)
qed (simp add: dist_geq0)

lemma dist_set_nzeroD:
  assumes "dist_set A x  0"
  shows "A  S" "x  A"
  by(rule ccontr, use assms dist_set_inA in auto)

lemma dist_set_antimono:
  assumes "A  B" "A  {}"
  shows "dist_set B x  dist_set A x"
proof(cases "B = {}")
  case h:False
  with assms have "{dist x y |y. y  B}  {}" "{dist x y |y. y  A}  {dist x y |y. y  B}"
    by auto
  thus ?thesis
    by(simp add: dist_set_def cInf_superset_mono assms(2))
qed(use assms in simp)

lemma dist_set_bounded:
  assumes "y. y  A  dist x y < K" "K > 0"
  shows "dist_set A x < K"
proof(cases "A = {}")
  case True
  then show ?thesis
    by(simp add: assms)
next
  case 1:False
  then have 2:"{dist x y |y. y  A}  {}" by auto
  show ?thesis
    using assms by (auto simp add: dist_set_def cInf_lessD[OF 2]  cInf_less_iff[OF 2])
qed

lemma dist_set_tr:
  assumes "x  S" "y  S"
  shows "dist_set A x  dist x y + dist_set A y"
proof(cases "A  S")
  case h:True
  consider "A = {}" | "A  {}" by auto
  then show ?thesis
  proof cases
    case 1
    then show ?thesis
      by(simp add: dist_set_def dist_geq0)
  next
    case 2
    have "dist_set A x  Inf {dist x y + dist y a |a. aA}"
    proof -
      have " {dist x y |y. y  A}   {dist x y + dist y a |a. a  A}"
      proof(rule cInf_mono)
        fix b
        assume "b  {dist x y + dist y a |a. a  A}"
        then obtain a where "a  A" "b = dist x y + dist y a"
          by auto
        thus "a{dist x y |y. y  A}. a  b"
          using h assms by(auto intro!: exI[where x="dist x a"] dist_tr)
      qed(simp_all add: 2)
      thus ?thesis
        by(simp add: dist_set_def 2)
    qed
    also have "... = dist x y + Inf {dist y a |a. aA}"
    proof -
      have "ereal (Inf {dist x y + dist y a |a. aA}) = ereal (dist x y + Inf {dist y a |a. aA})"
           (is "?lhs = ?rhs")
      proof -
        have "?lhs = Inf (ereal ` {(dist x y + dist y a) |a. aA})"
          using dist_geq0 by(auto intro!: ereal_Inf' bdd_belowI[where m=0] simp: 2)
        also have "... = Inf {ereal (dist x y + dist y a) |a. aA}"
        proof -
          have "ereal ` {(dist x y + dist y a) |a. aA} = {ereal (dist x y + dist y a) |a. aA}"
            by auto
          thus ?thesis by simp
        qed
        also have "... = (aA. ereal (dist x y) + ereal (dist y a))"
          by (simp add: Setcompr_eq_image)
        also have "... = ereal (dist x y) + (aA. ereal (dist y a))"
          by(rule INF_ereal_add_right) (use 2 dist_geq0 in auto)
        also have "... = ereal (dist x y) + ( (ereal ` {dist y a | a. a  A}))"
          by (simp add: Setcompr_eq_image image_image)
        also have "... = ereal (dist x y) + ereal (Inf {dist y a |a. aA})"
        proof -
          have "ereal (Inf {dist y a |a. aA}) = ( (ereal ` {dist y a | a. a  A}))"
            using dist_geq0 by(auto intro!: ereal_Inf' simp: 2)
          thus ?thesis by simp
        qed
        also have "... = ?rhs" by simp
        finally show ?thesis .
      qed
      thus ?thesis by simp
    qed
    also have "... = dist x y + dist_set A y"
      by(simp add: 2 dist_set_def)
    finally show ?thesis .
  qed
qed (simp add: dist_geq0)

lemma dist_set_abs_le:
  assumes "x  S" "y  S"
  shows "¦dist_set A x - dist_set A y¦  dist x y"
  using dist_set_tr[OF assms,of A] dist_set_tr[OF assms(2,1),of A,simplified dist_sym[of y x]]
  by auto

lemma dist_set_inA_le:
  assumes "y  A"
  shows "dist_set A x  dist x y"
proof -
  consider "x  S  y  S" | "x  S  y  S" by auto
  thus ?thesis
  proof cases
    case 1
    have "y  S  ¬ (A  S)"
      using assms by auto
    with 1 dist_geq0 show ?thesis
      by auto
  next
    case 2
    with dist_set_tr[of x y A] dist_set_inA[OF assms]
    show ?thesis by simp
  qed
qed

lemma dist_set_ball_open:
 "openin mtopology {xS. dist_set A x < ε}"
  unfolding mtopology_openin_iff
proof safe
  fix x
  assume h:"x  S" "dist_set A x < ε"
  show "ε'>0. open_ball x ε'  {x  S. dist_set A x < ε}"
  proof(safe intro!: exI[where x="ε - dist_set A x"])
    fix y
    assume h':"y  open_ball x (ε - dist_set A x)"
    have "dist_set A y  dist x y + dist_set A x"
      by(rule dist_set_tr[OF open_ballD'(1)[OF h'] h(1),simplified dist_sym[of y x]])
    also have "... < ε"
      using open_ballD[OF h'] by auto
    finally show "dist_set A y < ε" .
  qed(use h open_ballD'(1) in auto)
qed

lemma dist_set_ball_empty:
  assumes "A  {}" "A  S" "e > 0" "x  S" "open_ball x e  A = {}"
  shows "dist_set A x  e"
  using assms by(auto simp: dist_set_def assms(1) le_cInf_iff intro!: open_ball_nin_le[OF assms(4,3)])

lemma dist_set_closed_ge0:
  assumes "closedin mtopology A" "A  {}" "x  S" "x  A"
  shows "dist_set A x > 0"
proof -
  have a:"A  S" "openin mtopology (S - A)"
    using closedin_subset[OF assms(1)] assms(1)
    by(auto simp: closedin_def mtopology_topspace)
  with assms(3,4) obtain e where e: "e > 0" "open_ball x e  S - A"
    by(auto simp: mtopology_openin_iff) (meson Diff_iff)
  thus ?thesis
    by(auto intro!: order.strict_trans2[OF e(1) dist_set_ball_empty[OF assms(2) a(1) e(1) assms(3)]])
qed

lemma g_delta_of_closed:
  assumes "closedin mtopology M"
  shows "g_delta_of mtopology M"
proof(cases "M = {}")
  case True
  then show ?thesis by simp
next
  case M_ne:False
  have "M  S"
    using assms mtopology_topspace by (simp add: closedin_def)
  define U where "U  (λn. {xS. dist_set M x < 1 / real n})"
  define 𝒰 where "𝒰  {U n| n. n > 0}"
  have mun:"M  U n" if "n > 0" for n
    using dist_set_inA[of _ M] that M  S by(auto simp: U_def)
  show ?thesis
  proof(rule g_delta_ofI[of "𝒰"])
    show "𝒰  {}"
      by(auto simp: 𝒰_def)
  next
    have "𝒰 = U ` {0<..}" by(auto simp: 𝒰_def)
    thus "countable 𝒰" by simp
  next
    fix b
    assume "b  𝒰"
    then show "openin mtopology b"
      using dist_set_ball_open by(auto simp: 𝒰_def U_def)
  next
    show "M =  𝒰"
    proof(standard;standard)
      fix x
      assume "x  M"
      with mun
      show "x   𝒰"
        by(auto simp: 𝒰_def)
    next
      fix x
      assume "x   𝒰"
      then have "Inf {dist x m|m. mM} < 1 / real n" if "n > 0" for n
        using that by(auto simp: 𝒰_def U_def M_ne dist_set_def)
      hence 1:"Inf {dist x m|m. mM} < 1 / real (Suc n)" for n
        by blast
      have "mM. dist x m < 1 / real (Suc n)" for n
        using 1[of n] cInf_less_iff[of "{dist x m |m. m  M}" "1 / real (Suc n)"] M_ne
        by auto
      then obtain m where hm: "n. m n  M" "n. dist x (m n) < 1 / real (Suc n)"
        by metis
      hence "m  UNIV  M" by auto
      have "converge_to_inS m x"
        unfolding converge_to_inS_def2
      proof safe
        show "x. m x  S" "x  S"
          using x   𝒰 m  UNIV  M M  S
          by(auto simp: 𝒰_def U_def)
      next
        fix ε
        assume "(0 :: real) < ε"
        then obtain N where hN: "1 / real (Suc N) < ε"
          using nat_approx_posE by blast
        show "N. nN. dist (m n) x < ε"
        proof(safe intro!: exI[where x=N])
          fix n
          assume "N  n"
          then have "1 / real (Suc n)  1 / real (Suc N)"
            by (simp add: frac_le)
          from  order.strict_trans1[OF this hN] hm(2)[of n]
          show "dist (m n) x < ε"
            by(simp add: dist_sym[of x])
        qed
      qed
      thus "x  M"
        using assms[simplified mtopology_closedin_iff] m  UNIV  M
        by simp
    qed
  qed
qed

text ‹ Oscillation›
definition osc_on :: "['b set, 'b topology, 'b  'a, 'b]  ennreal" where
"osc_on A X f  (λy.  {diam (f ` (A  U)) |U. y  U  openin X U})"

abbreviation "osc X  osc_on (topspace X) X"

lemma osc_def: "osc X f = (λy.  {diam (f ` U) |U. y  U  openin X U})"
  by(standard,auto simp: osc_on_def) (metis (no_types, opaque_lifting) inf.absorb2 openin_subset)

lemma osc_on_less_iff:
 "osc_on A X f x < t  (v. x  v  openin X v  diam (f ` (A  v)) < t)"
  by(auto simp add: osc_on_def Inf_less_iff)

lemma osc_less_iff:
 "osc X f x < t  (v. x  v  openin X v  diam (f ` v) < t)"
  by(auto simp add: osc_def Inf_less_iff)

definition sequentially_compact :: bool where
"sequentially_compact  (xnsequence. a. strict_mono a  convergent_inS (xn  a))"

definition eps_net_on :: "'a set  real  'a set  bool" where
"eps_net_on B ε A  ε > 0  finite A  A  S  B  (aA. open_ball a ε)"

abbreviation "eps_net  eps_net_on S"

lemma eps_net_def: "eps_net ε A  ε > 0  finite A  A  S  S =  ((λa. open_ball a ε) ` A)"
  using open_ball_subset_ofS by(auto simp: eps_net_on_def)

lemma eps_net_onD:
  assumes "eps_net_on B e A"
  shows "e > 0" "finite A" "A  S" "B  (aA. open_ball a e)" "B  S"
  using assms open_ball_subset_ofS by(auto simp: eps_net_on_def) blast

lemma eps_netD:
  assumes "eps_net ε A"
  shows "ε > 0" "finite A" "A  S" "S =  ((λa. open_ball a ε) ` A)"
  using assms by(auto simp: eps_net_def)

lemma eps_net_le:
  assumes "eps_net e A" "e  e'"
  shows "eps_net e' A"
  using assms open_ball_le[OF assms(2)] open_ballD'(1)
  by(auto simp: eps_net_def) blast

definition totally_bounded_on :: "'a set  bool" where
"totally_bounded_on B  (e>0. A. eps_net_on B e A)"

abbreviation "totally_boundedS  totally_bounded_on S"

lemma totally_boundedS_def: "totally_boundedS  (e>0. A. eps_net e A)"
  by(auto simp: totally_bounded_on_def)

lemma totally_bounded_onD_sub:
  assumes "totally_bounded_on B"
  shows "B  S"
  by (meson assms eps_net_onD(5) gt_ex totally_bounded_on_def)

lemma totally_bounded_onD:
  assumes "totally_bounded_on B" "e > 0"
  obtains A where "finite A" "A  S" "B  (aA. open_ball a e)"
  by (metis assms that eps_net_on_def totally_bounded_on_def)

lemma totally_boundedSD:
  assumes totally_boundedS "e > 0"
  obtains A where "finite A" "A  S" "S = (aA. open_ball a e)"
  by (metis assms that eps_net_def totally_boundedS_def)

lemma totally_bounded_on_iff:
"totally_bounded_on B  B  S  (xn(UNIV :: nat set)  B. a. strict_mono a  Cauchy_inS (xn  a))"
proof safe
  fix xn :: "nat  'a"
  assume h:"totally_bounded_on B" "xn  UNIV  B"
  then have h': "B  S"
    by (auto dest: totally_bounded_onD_sub)
  have 1: "b::nat  nat. strict_mono b  (n m. dist (yn (b n)) (yn (b m)) < e)" if "yn  UNIV  B" "e > 0" for e yn
  proof -
    obtain A where A: "finite A" "A  S" "B  (aA. open_ball a (e/2))"
      using totally_bounded_onD[OF h(1) half_gt_zero[OF e > 0]] by metis
    have "¬ (aA. finite {n. yn n  open_ball a (e/2)})"
    proof
      assume "aA. finite {n. yn n  open_ball a (e/2)}"
      then have "finite (aA. {n. yn n  open_ball a (e/2)})"
        using A by auto
      moreover have "UNIV = (aA. {n. yn n  open_ball a (e/2)})"
        using that(1) A(3) by auto
      ultimately show False by simp
    qed
    then obtain a where a:"a  A" "infinite {n. yn n  open_ball a (e/2)}"
      by auto
    then obtain b where b:"strict_mono b" "n::nat. yn (b n)  open_ball a (e/2)"
      using obtain_subsequence[of "λ_ ynn. ynn  open_ball a (e/2)" yn] by auto
    show ?thesis
      using a A by(auto intro!: exI[where x=b] b order.strict_trans1[OF dist_tr[OF open_ballD'(1)[OF b(2)] _ open_ballD'(1)[OF b(2)],of a] add_strict_mono[OF open_ballD[OF b(2),simplified dist_sym[of a]] open_ballD[OF b(2)]],simplified])
  qed

  define anm where "anm  rec_nat (xn  (SOME b::nat  nat. strict_mono b  (n m. dist (xn (b n)) (xn (b m)) < 1))) (λn an. an  (SOME b. strict_mono b  (l k. dist (an (b l)) (an (b k)) < 1 / Suc (Suc n))))"
  have anm_Suc:"anm (Suc n) = anm n  (SOME b. strict_mono b  (l k. dist (anm n (b l)) (anm n (b k)) < 1 / Suc (Suc n)))" for n
    by(simp add: anm_def)
  have anm1:"anm n  UNIV  B  (l k. dist (anm n l) (anm n k) < 1 / Suc n)" for n
  proof(induction n)
    case 0
    obtain b ::"nat  nat" where b:"strict_mono b" "l k. dist (xn (b l)) (xn (b k)) < 1"
      using 1[OF h(2),of 1] by auto
    show ?case
      by(simp add: anm_def,rule someI2[where a=b]) (use b h(2) in auto)
  next
    case ih:(Suc n')
    obtain b ::"nat  nat" where b:"strict_mono b" "l k. dist (anm n' (b l)) (anm n' (b k)) < 1 / real (Suc (Suc n'))"
      using 1[of "anm n'" "1 / Suc (Suc n')"] ih by auto 
    show ?case
      by(simp only: anm_Suc,rule someI2[where a=b]) (use ih b in auto)
  qed

  define bnm :: "nat  nat  nat" where "bnm  rec_nat (SOME b. strict_mono b  anm 0 = xn  b) (λn bn. SOME b. strict_mono b  anm (Suc n) = anm n  b)"
  have bnm_Suc:"bnm (Suc n) = (SOME b. strict_mono b  anm (Suc n) = anm n  b)" for n
    by(simp add: bnm_def)
  have bnm0:"strict_mono (bnm 0)  anm 0 = xn  (bnm 0)"
  proof -
    have b0:"b::nat  nat. strict_mono b  anm 0 = xn  b"
    proof -
      obtain b ::"nat  nat" where b:"strict_mono b" "l k. dist (xn (b l)) (xn (b k)) < 1"
        using 1[OF h(2),of 1] by auto
      show ?thesis
        by(simp add: anm_def,rule someI2[where a=b],auto simp: b)
    qed
    thus ?thesis
      unfolding bnm_def by(simp,rule someI_ex)
  qed
  have bnm_S: "strict_mono (bnm (Suc n))  anm (Suc n) = anm n  (bnm (Suc n))" for n
  proof -
    have bn:"b::nat  nat. strict_mono b  anm (Suc m) = anm m  b" for m
    proof -
      obtain b ::"nat  nat" where b:"strict_mono b" "l k. dist (anm m (b l)) (anm m (b k)) < 1 / real (Suc (Suc m))"
        using 1[of "anm m" "1 / Suc (Suc m)"] anm1 by auto
      show ?thesis
        by(simp only: anm_Suc,rule someI2[where a=b]) (auto simp: b[simplified])
    qed
    thus ?thesis
      by(simp add: bnm_Suc, rule someI_ex)
  qed
  define bnm_r where "bnm_r  rec_nat (bnm 0) (λn bn. bn  (bnm (Suc n)))"
  have bnm_r_Suc: "bnm_r (Suc n) = bnm_r n  (bnm (Suc n))" for n
    by(simp add: bnm_r_def)
  have anm_bnm_r:"anm n = xn  (bnm_r n)" for n
    by(induction n,simp add: bnm0 bnm_r_def) (auto simp: bnm_S bnm_r_Suc)
  have bnm_r_sm:"strict_mono (bnm_r n)" for n
    by(induction n, simp add: bnm0 bnm_r_def) (insert bnm_S, auto simp: bnm_r_Suc strict_mono_def)
  have bnm_r_Suc_le:"bnm_r n l  bnm_r (Suc n) l" for l n
    using bnm_S bnm_r_sm by(auto simp: bnm_r_Suc strict_mono_imp_increasing strict_mono_leD)
  have sm:"strict_mono (λn. bnm_r n n)"
    by(auto simp add: strict_mono_Suc_iff) (meson lessI order_le_less_trans strict_monoD bnm_r_sm bnm_r_Suc_le)
  have bnm_r_de:"l. bnm_r (n + k) = bnm_r n  l" for n k
    by(induction k) (auto simp: bnm_r_Suc)
  show "a::nat  nat. strict_mono a  Cauchy_inS (xn  a)"
    unfolding Cauchy_inS_def
  proof(safe intro!: exI[where x="λn. bnm_r n n"] sm)
    fix e :: real
    assume "e > 0"
    then obtain N where N:"1 / Suc N < e"
      using nat_approx_posE by blast
    show "N. nN. mN. dist ((xn  (λn. bnm_r n n)) n) ((xn  (λn. bnm_r n n)) m) < e"
    proof(safe intro!: exI[where x=N])
      fix n m
      assume "N  n" "N  m"
      then have "n = N + (n - N)" "m = N + (m - N)" by auto
      then obtain l1 l2 where l:"bnm_r n = bnm_r N  l1" "bnm_r m = bnm_r N  l2"
        by (metis bnm_r_de)  
      have "dist (xn (bnm_r n n)) (xn (bnm_r m m)) = dist (anm N (l1 n)) (anm N (l2 m))"
        by(simp add: l anm_bnm_r)
      also have "... < 1 / Suc N"
        using anm1 by auto
      finally show "dist ((xn  (λn. bnm_r n n)) n) ((xn  (λn. bnm_r n n)) m) < e"
        using N by simp
    qed
  qed(use h h' in auto)
next
  assume h:"xn(UNIV :: nat set)  B. a. strict_mono a  Cauchy_inS (xn  a)" "B  S"
  show "totally_bounded_on B"
  proof(rule ccontr)
    assume "¬ totally_bounded_on B"
    then obtain e where e:"e > 0" "A. ¬ eps_net_on B e A"
      by(auto simp: totally_bounded_on_def)
    have A:"¬ B  (aA. open_ball a e)" if "finite A" for A
    proof -
      have [simp]:"(aA. open_ball a e) = (aA S. open_ball a e)"
        using Collect_cong IntD1 IntI Sup_set_def UN_iff open_ballD'(2) by auto
      have "finite (A  S)" using that by auto
      thus ?thesis
        using e by(auto simp: eps_net_on_def)
    qed
    obtain a0 where a0:"a0  B"
      using A by fastforce
    define xnl where "xnl  rec_nat [a0] (λn ln. (SOME x. x  B  x  (aset ln. open_ball a e)) # ln)"
    have xnl_Suc:"xnl (Suc n) = (SOME x. x  B  x  (aset (xnl n). open_ball a e)) # xnl n" for n
      by(simp add: xnl_def)
    define xn where "xn = (λn. (xnl n) ! 0)"
    have xn:"xn (Suc n)  B  xn (Suc n)  (aset (xnl n). open_ball a e)" for n
    proof -
      have "y. y  B  (xset (xnl n). y  open_ball x e)"
        using A[OF finite_set] by fastforce
      thus ?thesis
        by(simp add: xn_def xnl_Suc,rule someI_ex)
    qed
    have xn0:"xn 0  B"
      by(auto simp: xnl_def xn_def a0)
    with xn have xns:"xn  UNIV  B"
      by auto (metis old.nat.exhaust)
    have xnll:"length (xnl n) = Suc n" for n
      by(induction n) (simp add: xnl_def, auto simp: xnl_Suc)
    have xnin:"xn m  set (xnl (m + k))" for m k
      by(induction k) (auto simp: xn_def xnl_Suc xnll intro!: nth_mem)
    obtain a where a:"strict_mono a" "Cauchy_inS (xn  a)"
      using h xns by auto
    then obtain N where "n m. n  N  m  N  dist (xn (a n)) (xn (a m)) < e"
      using e Cauchy_inS_def by fastforce
    hence e1:"dist (xn (a N)) (xn (a (Suc N))) < e"
      by auto
    have "xn (a (Suc N))  (aset (xnl (a (Suc N) - 1)). open_ball a e)"
      by (metis a(1) diff_Suc_1 le_0_eq not0_implies_Suc strict_mono_less_eq xn zero_le)
    moreover have "xn (a N)  set (xnl (a (Suc N) - 1))"
      using a(1)[simplified strict_mono_Suc_iff] xnin[of "a N" "a (Suc N) - a N - 1"]
      by (simp add: Suc_leI)
    ultimately have "xn (a (Suc N))  open_ball (xn (a N)) e"
      by auto
    from open_ball_nin_le[OF _ e(1) _ this] xns e1 h(2)
    show False by auto
  qed
qed(auto dest: totally_bounded_onD_sub)

corollary totally_boundedS_iff: "totally_boundedS  (xnsequence. a. strict_mono a  Cauchy_inS (xn  a))"
  by(auto simp: totally_bounded_on_iff)

text ‹ Metric embedding›
definition embed_dist_on :: "['b set, 'b  'a, 'b, 'b]  real" where
"embed_dist_on B f a b  (if a  B  b  B then dist (f a) (f b) else 0)"

context
  fixes f B
  assumes f: "f  B  S" "inj_on f B"
begin

abbreviation "ed  embed_dist_on B f"

lemma embed_dist_dist: "metric_set B (embed_dist_on B f)"
proof
  fix x y
  assume "x  B" "y  B"
  then show "x = y  embed_dist_on B f x y = 0"
    using inj_onD[OF f(2)] dist_0[of "f x" "f y"] f(1)
    by(auto simp: embed_dist_on_def)
next
  fix x y
  show "embed_dist_on B f x y = embed_dist_on B f y x"
    by(simp add: embed_dist_on_def dist_sym[of "f x" "f y"])
next
  fix x y z
  assume "x  B" "y  B" "z  B"
  then show "embed_dist_on B f x z  embed_dist_on B f x y + embed_dist_on B f y z"
    using dist_tr[of "f x" "f y" "f z"] f(1) by(auto simp: embed_dist_on_def)
qed(simp_all add: embed_dist_on_def  dist_geq0)

interpretation ed : metric_set B ed
  by(rule embed_dist_dist)

lemma embed_dist_open_ball: 
  assumes "a  B"
  shows"f ` (ed.open_ball a e) = open_ball (f a) e  f ` B"
  using assms f by(auto simp: ed.open_ball_def open_ball_def embed_dist_on_def)

lemma embed_dist_closed_ball:
  assumes "a  B"
  shows"f ` (ed.closed_ball a e) = closed_ball (f a) e  f ` B"
  using assms f by(auto simp: ed.closed_ball_def closed_ball_def embed_dist_on_def)

lemma embed_dist_topology_homeomorphic_maps:
  assumes g1:"x. x  B  g (f x) = x"
  shows "homeomorphic_maps ed.mtopology (subtopology mtopology (f ` B)) f g"
proof -
  have g2: "x. x  f ` B  f (g x) = x" "g  (f ` B)  B"
    by(auto simp: g1)
  show ?thesis
    unfolding homeomorphic_maps_def mtopology_topspace ed.mtopology_topspace
  proof safe
    show "continuous_map ed.mtopology (subtopology mtopology (f ` B)) f"
      unfolding mtopology_def2 subtopology_generated_by
    proof(rule continuous_on_generated_topo)
      show "U. U  {f ` B  U |U. U  {open_ball a ε |a ε. a  S  0 < ε}}  openin ed.mtopology (f -` U  topspace ed.mtopology)"
        unfolding ed.mtopology_topspace
      proof safe
        fix a and e :: real
        assume h:"a  S" "0 < e"
        have 1:"(f -` (f ` B  open_ball a e)  B) = f -` open_ball a e  B" by blast
        show "openin ed.mtopology (f -` (f ` B  open_ball a e)  B)"
          unfolding 1 ed.mtopology_openin_iff
        proof safe
          fix x
          assume h':"x  B" "f x  open_ball a e"
          then obtain e' where e':"e' > 0" "open_ball (f x) e'  open_ball a e"
            using mtopology_open_ball_in' by blast
          show "ε>0. ed.open_ball x ε  f -` open_ball a e  B"
          proof(safe intro!: exI[where x=e'])
            fix y
            assume "y  ed.open_ball x e'"
            with e'(2) show "y  f -` open_ball a e"
              using embed_dist_open_ball[OF h'(1),of e'] by blast
          qed(use e' ed.open_ball_subset_ofS in auto)
        qed
      qed
    next
      show "f ` topspace ed.mtopology   {f ` B  U |U. U  {open_ball a ε |a ε. a  S  0 < ε}} "
        by(auto simp: ed.mtopology_topspace) (metis (mono_tags, opaque_lifting) IntE IntI closed_ball_def ed.closed_ball_ina ed.dist_set_geq0 ed.dist_set_inA embed_dist_closed_ball ennreal_le_epsilon ennreal_zero_less_top image_eqI le_zero_eq not_gr_zero open_ballD'(2) open_ball_ina open_ball_le_0)
    qed
  next
    show "continuous_map (subtopology mtopology (f ` B)) ed.mtopology g"
      unfolding ed.mtopology_def2
    proof(rule continuous_on_generated_topo)
      show "U. U  {ed.open_ball a ε |a ε. a  B  0 < ε}  openin (subtopology mtopology (f ` B)) (g -` U  topspace (subtopology mtopology (f ` B)))"
      proof safe
        fix a and e :: real
        assume h: "a  B" "0 < e"
        then have 1: "g -` ed.open_ball a e  (S  f ` B) = open_ball (f a) e  f ` B"
          using f(1) g1 g2 by(auto simp: ed.open_ball_def open_ball_def embed_dist_on_def)
        show "openin (subtopology mtopology (f ` B)) (g -` ed.open_ball a e  (topspace (subtopology mtopology (f ` B))))"
          by(auto simp: 1 openin_subtopology openin_open_ball mtopology_topspace intro!: exI[where x="open_ball (f a) e"])
      qed
      show "g ` topspace (subtopology mtopology (f ` B))   {ed.open_ball a ε |a ε. a  B  0 < ε}"
        by(auto simp: mtopology_topspace) (metis ed.mtopology_openin_iff ed.open_ball_ina ed.openin_S g1)
    qed
  qed(use g1 g2 in auto)
qed

lemma embed_dist_topology_homeomorphic_map:
 "homeomorphic_map ed.mtopology (subtopology mtopology (f ` B)) f"
proof -
  define g where "g  (λy. THE x. x  B  f x = y)"
  have g1: "g (f b) = b" if "b  B" for b
    unfolding g_def by(rule theI2[of _ b]) (insert that f(2), auto simp: inj_on_def)
  thus ?thesis
    using embed_dist_topology_homeomorphic_maps homeomorphic_map_maps by blast
qed

corollary embed_dist_topology_homeomorphic:
 "ed.mtopology homeomorphic_space (subtopology mtopology (f ` B))"
  using embed_dist_topology_homeomorphic_map
  by(rule homeomorphic_map_imp_homeomorphic_space)

corollary embed_dist_topology_homeomorphic_map':
  assumes "f ` B = S"
  shows "homeomorphic_map ed.mtopology mtopology f"
  using embed_dist_topology_homeomorphic_map[simplified assms]
  by(simp add:subtopology_topspace[of mtopology, simplified mtopology_topspace])

corollary embed_dist_topology_homeomorphic':
  assumes "f ` B = S"
  shows "ed.mtopology homeomorphic_space mtopology"
  using embed_dist_topology_homeomorphic_map'[OF assms]
  by(rule homeomorphic_map_imp_homeomorphic_space)

lemma embed_dist_converge_to_inS_iff:
 "ed.converge_to_inS xn x  xn  ed.sequence  x  B  converge_to_inS (λn. f (xn n)) (f x)"
proof safe
  assume h:"ed.converge_to_inS xn x"
  then show h':"x  B" "n. xn n  B"
    by(auto simp: ed.converge_to_inS_def)
  thus "converge_to_inS (λn. f (xn n)) (f x)"
    using h f by(auto simp: converge_to_inS_def2 ed.converge_to_inS_def2 embed_dist_on_def)
next
  assume h:"xn  ed.sequence" "x  B" "converge_to_inS (λn. f (xn n)) (f x)"
  show "ed.converge_to_inS xn x"
    using h f by(fastforce simp: ed.converge_to_inS_def2 h embed_dist_on_def converge_to_inS_def2)
qed

lemma embed_dist_convergent_inS_iff:
  assumes "closedin mtopology (f ` B)"
  shows "ed.convergent_inS xn  xn  ed.sequence  convergent_inS (λn. f (xn n))"
proof -
  {
    fix s
    assume h:"xn  ed.sequence" "converge_to_inS (λn. f (xn n)) s"
    with f have "(λn. f (xn n))  UNIV  f ` B" by auto
    hence "s  f ` B"
      using assms h(2) by(auto simp: mtopology_closedin_iff)
    hence "b  B. s = f b" by auto
  }
  thus ?thesis
    using embed_dist_converge_to_inS_iff[of xn] f(1)
    by(fastforce simp: ed.convergent_inS_def convergent_inS_def)
qed

lemma embed_dist_Cauchy_inS_iff:
 "ed.Cauchy_inS xn  xn  ed.sequence  Cauchy_inS (λn. f (xn n))"
  using f(1) by(auto simp: ed.Cauchy_inS_def Cauchy_inS_def embed_dist_on_def; meson PiE UNIV_I)

end

end

text ‹ Relations to elementary topology. ›
lemma ball_def_set: "ball a ε = metric_set.open_ball UNIV dist a ε"
  using metric_set.open_ball_def metric_class_metric_set
  by fastforce

lemma converge_to_def_set:
  fixes xn :: "nat  ('a::metric_space)"
  shows "xn  x  metric_set.converge_to_inS UNIV dist xn x"
proof -
  interpret m: metric_set UNIV dist
    by simp
  show ?thesis
    by(simp add: lim_sequentially m.converge_to_inS_def)
qed

lemma the_limit_of_limit:
  fixes xn :: "nat  ('a::metric_space)"
  shows "metric_set.the_limit_of UNIV dist xn = lim xn"
  by(simp add: metric_set.the_limit_of_def lim_def converge_to_def_set)

lemma convergent_def_set:
  fixes f :: "nat  ('a::metric_space)"
  shows "convergent f  metric_set.convergent_inS UNIV dist f"
proof -
  interpret m: metric_set UNIV dist
    by(rule metric_class_metric_set)
  show "convergent f  m.convergent_inS f"
    using converge_to_def_set[of f]
    by(auto simp: convergent_def m.convergent_inS_def)
qed

lemma Cahuchy_def_set: "Cauchy f  metric_set.Cauchy_inS UNIV dist f"
proof -
  interpret m: metric_set UNIV dist
    by(rule metric_class_metric_set)
  show "Cauchy f = m.Cauchy_inS f"
    by(simp add: Cauchy_def m.Cauchy_inS_def dist_real_def)
qed

lemma open_openin_set: "open U  openin (metric_set.mtopology UNIV dist) U"
 (is "?LHS  ?RHS")
proof -
  interpret m: metric_set UNIV dist
    by(rule metric_class_metric_set)
  have "?LHS  (xU. e>0. ball x e  U)"
    by(simp add: open_contains_ball)
  also have "...  (xU. e>0. m.open_ball x e  U)"
    by(simp add: ball_def_set)
  also have "...  ?RHS"
    by(simp add: m.mtopology_openin_iff[of U])
  finally show ?thesis .
qed

lemma topological_basis_set: "topological_basis 𝒪  metric_set.mtopology_basis UNIV dist 𝒪"
  (is "?LHS = ?RHS")
proof -
  interpret m: metric_set UNIV dist
    by(rule metric_class_metric_set)
  have "?LHS  (b𝒪. open b)  (x. open x  (B'𝒪.  B' = x))"
    by(simp add: topological_basis_def)
  also have "...  (b𝒪. openin m.mtopology b)  (x. openin m.mtopology x  (B'𝒪.  B' = x))"
    by(simp add: open_openin_set)
  also have "...  ?RHS"
    by(simp add: base_of_def2')
  finally show ?thesis .
qed

lemma euclidean_mtopology: "metric_set.mtopology UNIV dist = euclidean"
  using open_openin open_openin_set topology_eq by blast

text ‹ Distances generate the same topological space.›
lemma metric_generates_same_topology:
  assumes "metric_set S d" "metric_set S d'"
          "x U. U  S  (yU. ε>0. metric_set.open_ball S d y ε  U)  x  U  ε>0. metric_set.open_ball S d' x ε  U"
      and "x U. U  S  (yU. ε>0. metric_set.open_ball S d' y ε  U)  x  U  ε>0. metric_set.open_ball S d x ε  U"
    shows "metric_set.mtopology S d = metric_set.mtopology S d'"
proof -
  interpret m1: metric_set S d by fact
  interpret m2: metric_set S d' by fact
  have "(λU. U  S  (xU. ε>0. m1.open_ball x ε  U)) = (λU. U  S  (xU. ε>0. m2.open_ball x ε  U))"
    by standard (use assms(3,4) in auto)
  thus ?thesis
    using topology.topology_inject m1.mtopology_istopology m2.mtopology_istopology
    by(simp add: m2.mtopology_def m1.mtopology_def)
qed

lemma metric_generates_same_topology_inverse:
  assumes "metric_set S d" "metric_set S d'"
      and "metric_set.mtopology S d = metric_set.mtopology S d'"
    shows "U  S  (yU. ε>0. metric_set.open_ball S d y ε  U)  x  U  ε>0. metric_set.open_ball S d' x ε  U"
      and "U  S  (yU. ε>0. metric_set.open_ball S d' y ε  U)  x  U  ε>0. metric_set.open_ball S d x ε  U"
proof -
  interpret m1: metric_set S d by fact
  interpret m2: metric_set S d' by fact
  have "(λU. U  S  (xU. ε>0. m1.open_ball x ε  U)) = (λU. U  S  (xU. ε>0. m2.open_ball x ε  U))"
    using topology.topology_inject[of "λU. U  S  (xU. ε>0. m1.open_ball x ε  U)" "λU. U  S  (xU. ε>0. m2.open_ball x ε  U)"] m1.mtopology_istopology m2.mtopology_istopology assms(3)
    by(auto simp: m2.mtopology_def m1.mtopology_def)
  thus "U  S  yU. ε>0. m1.open_ball y ε  U  x  U  ε>0. m2.open_ball x ε  U"
       "U  S  yU. ε>0. m2.open_ball y ε  U  x  U  ε>0. m1.open_ball x ε  U"
    by(auto dest: fun_cong[where x=U])
qed

lemma metric_generates_same_topology_converges':
  assumes "metric_set S d" "metric_set S d'"
          "metric_set.mtopology S d = metric_set.mtopology S d'"
      and "metric_set.converge_to_inS S d f x"
    shows "metric_set.converge_to_inS S d' f x"
proof -
  interpret m1: metric_set S d by fact
  interpret m2: metric_set S d' by fact
  show ?thesis
    unfolding m2.converge_to_inS_def2'
  proof safe
    fix ε :: real
    assume h:"0 < ε"
    obtain ε' where he:
    "ε'>0" "m1.open_ball x ε'  m2.open_ball x ε"
      using m2.mtopology_open_ball_in'[of _ x]  assms(4)[simplified m1.converge_to_inS_def2'] metric_generates_same_topology_inverse(2)[OF assms(1-3) m2.open_ball_subset_ofS, of x ε,OF _ m2.open_ball_ina[OF _ h,of x]]
      by auto
    then obtain N where hn:
    "nN. f n  m1.open_ball x ε'"
      using assms(4)[simplified m1.converge_to_inS_def2'] by auto
    show "N. nN. f n  m2.open_ball x ε"
      using hn he(2) by(auto intro!: exI[where x=N])
  next
    show "x. f x  S" "x  S"
      using assms(4)[simplified m1.converge_to_inS_def2'] by auto
  qed
qed

lemma metric_generates_same_topology_converges:
  assumes "metric_set S d" "metric_set S d'"
      and "metric_set.mtopology S d = metric_set.mtopology S d'"
    shows "metric_set.converge_to_inS S d f x  metric_set.converge_to_inS S d' f x"
  using metric_generates_same_topology_converges'[OF assms(2,1) assms(3)[symmetric]] metric_generates_same_topology_converges'[OF assms(1-3)]
  by auto

lemma metric_generates_same_topology_convergent:
  assumes "metric_set S d" "metric_set S d'"
      and "metric_set.mtopology S d = metric_set.mtopology S d'"
    shows "metric_set.convergent_inS S d f  metric_set.convergent_inS S d' f"
  using metric_generates_same_topology_converges[OF assms,of f]
  by (simp add: assms(1) assms(2) metric_set.convergent_inS_def)

subsubsection ‹ Sub-Metric Spaces›
definition submetric :: "['a set, 'a  'a  real]  'a  'a  real" where
"submetric S' d  (λx y. if x  S'  y  S' then d x y else 0)"

lemma(in metric_set) submetric_metric_set:
  assumes "S'  S"
  shows "metric_set S' (submetric S' dist)"
proof
  show "x y. 0  submetric S' dist x y"
       "x y. x  S'  submetric S' dist x y = 0"
       "x y. x  S'  y  S'  (x = y) = (submetric S' dist x y = 0)"
       "x y. submetric S' dist x y = submetric S' dist y x" 
    using assms dist_geq0 dist_tr dist_0 dist_sym
    by(fastforce simp: submetric_def)+
next
  show "x y z. x  S'  y  S'  z  S'  submetric S' dist x z  submetric S' dist x y + submetric S' dist y z"
    by (metis assms dist_tr submetric_def subset_iff)
qed

lemma(in metric_set) submetric_open_ball:
  assumes "S'  S" and "a  S'"
  shows "open_ball a ε  S' = metric_set.open_ball S' (submetric S' dist) a ε"
proof -
  interpret m: metric_set S' "submetric S' dist"
    by(rule submetric_metric_set[OF assms(1)])
  show ?thesis
    using assms by(auto simp: open_ball_def m.open_ball_def,simp_all add: submetric_def)
qed

lemma(in metric_set) submetric_open_ball_subset:
  assumes "S'  S"
  shows "metric_set.open_ball S' (submetric S' dist) a ε  open_ball a ε"
proof -
  interpret m: metric_set S' "submetric S' dist"
    by(rule submetric_metric_set[OF assms(1)])
  show ?thesis
    by (metis assms empty_subsetI inf_commute inf_sup_ord(2) m.open_ball_nin submetric_open_ball)
qed

lemma(in metric_set) submetric_subtopology:
  assumes "S'  S"
  shows "subtopology mtopology S' = metric_set.mtopology S' (submetric S' dist)"
proof -
  interpret m: metric_set S' "submetric S' dist"
    by(rule submetric_metric_set[OF assms(1)])
  show ?thesis
    unfolding topology_eq
  proof safe
    fix U
    assume "openin (subtopology mtopology S') U"
    then obtain T where ht: "openin mtopology T" "U = T  S'"
      by(auto simp: openin_subtopology)
    have "U  S'"
      by (simp add: ht(2))
    show "openin m.mtopology U"
      unfolding m.mtopology_openin_iff
    proof safe
      fix x
      assume "x  U"
      then obtain ε where he: "ε > 0" "open_ball x ε  T"
        using ht by(auto simp: mtopology_openin_iff)
      thus "ε>0. m.open_ball x ε  U"
        using ht(2) x  U submetric_open_ball[OF assms(1),of x ε]
        by(auto intro!: exI[where x=ε])
    qed(use U  S' in auto)
  next
    fix U
    assume "openin m.mtopology U"
    then have "xU. ε>0. m.open_ball x ε  U"
      by(simp add: m.mtopology_openin_iff)
    then obtain ε where he:
     "x. x  U  ε x > 0" "x. x  U  m.open_ball x (ε x)  U"
      by metis
    have "U  S'"
      using openin m.mtopology U m.mtopology_openin_iff by auto

    show "openin (subtopology mtopology S') U"
      unfolding openin_subtopology
    proof(intro exI[where x=" { open_ball x (ε x) | x. xU}"] conjI)
      show "openin mtopology ( { open_ball x (ε x) | x. xU})"
        by(rule openin_Union) (use he(1) open_ball_def mtopology_open_ball_in in fastforce)
    next
      have *:"U = ( { m.open_ball x (ε x) | x. xU})"
        using he m.open_ball_ina U  S' by fastforce
      also have "... = ( { open_ball x (ε x)   S' | x. xU})"
        using submetric_open_ball[OF assms(1)] U  S' by auto
      also have "... = ( { open_ball x (ε x) | x. xU})  S'"
        by auto
      finally show "U =  {open_ball x (ε x) |x. x  U}  S' " .
    qed
  qed
qed

lemma(in metric_set) converge_to_insub_converge_to_inS:
  assumes "S'  S" and "metric_set.converge_to_inS S' (submetric S' dist) f x"
  shows "converge_to_inS f x"
proof -
  interpret m: metric_set S' "submetric S' dist"
    by(rule submetric_metric_set[OF assms(1)])
  have *:"f  m.sequence" "x  S'"
    using assms(2) by(auto simp: m.converge_to_inS_def)
  show ?thesis
    unfolding converge_to_inS_def2 using * assms[simplified  m.converge_to_inS_def2]
    by(auto simp: submetric_def funcset_mem)
qed

lemma(in metric_set) convergent_insub_convergent_inS:
  assumes "S'  S" and "metric_set.convergent_inS S' (submetric S' dist) f"
  shows "convergent_inS f"
  by (meson assms(1) assms(2) converge_to_insub_converge_to_inS convergent_inS_def in_mono metric_set.convergent_inS_def submetric_metric_set)

lemma(in metric_set) Cauchy_insub_Cauchy:
  assumes "S'  S" and "metric_set.Cauchy_inS S' (submetric S' dist) f"
  shows "Cauchy_inS f"
proof -
  interpret m: metric_set S' "submetric S' dist"
    by(rule submetric_metric_set[OF assms(1)])
  have *:"f  m.sequence"
    using assms(2) by(auto simp: m.Cauchy_inS_def)
  show ?thesis
    unfolding Cauchy_inS_def using * assms[simplified m.Cauchy_inS_def]
    by(auto simp: submetric_def funcset_mem[OF *])
qed

lemma(in metric_set) Cauchy_insub_Cauchy_inverse:
  assumes "S'  S" "f  UNIV  S'" "Cauchy_inS f"
  shows "metric_set.Cauchy_inS S' (submetric S' dist) f"
proof -
  interpret m: metric_set S' "submetric S' dist"
    by(rule submetric_metric_set[OF assms(1)])
  show ?thesis
    using assms by(auto simp: m.Cauchy_inS_def Cauchy_inS_def,simp add: submetric_def) metis
qed

lemma(in metric_set) convergent_insubmetric:
  assumes "S'  S" "f  UNIV  S'" "x  S'" "converge_to_inS f x"
  shows "metric_set.converge_to_inS S' (submetric S' dist) f x"
proof -
  interpret m: metric_set S' "submetric S' dist"
    by(rule submetric_metric_set[OF assms(1)])
  show ?thesis
    unfolding m.converge_to_inS_def using assms
    by(auto simp: converge_to_inS_def funcset_mem[OF assms(2)] submetric_def)
qed

lemma(in metric_set) the_limit_of_submetric_eq:
  assumes "S'  S" "metric_set.convergent_inS S' (submetric S' dist) f"
  shows "metric_set.the_limit_of S' (submetric S' dist) f = the_limit_of f"
  by (meson assms(1) assms(2) converge_to_insub_converge_to_inS convergent_insub_convergent_inS metric_set.converge_to_inS_unique metric_set.the_limit_if_converge metric_set_axioms submetric_metric_set)

lemma submetric_of_euclidean:
 "metric_set A (submetric A dist)" "metric_set.mtopology A (submetric A dist) = top_of_set A"
  using metric_set.submetric_metric_set[OF metric_class_metric_set,of A] metric_set.submetric_subtopology[OF metric_class_metric_set,of A]
  by(auto simp: euclidean_mtopology)

lemma(in metric_set)
  assumes "B  S"
  shows totally_bounded_on_submetric: "totally_bounded_on B  metric_set.totally_boundedS B (submetric B dist)"
proof -
  interpret m: metric_set B "submetric B dist"
    by(rule submetric_metric_set[OF assms(1)])
  show ?thesis
    unfolding totally_bounded_on_def m.totally_boundedS_def
  proof safe
    fix e :: real
    assume h:"e>0. A. eps_net_on B e A" "e > 0"
    then obtain A where A:"eps_net_on B (e / 2) A"
      by fastforce
    define A' where "A'  A  {z.  open_ball z (e / 2)  B  {}}"
    have A': "eps_net_on B (e / 2) A'"
      unfolding eps_net_on_def
    proof safe
      fix x
      assume x:"x  B"
      then obtain a where a:"a  A" "x  open_ball a (e / 2)"
        using A by(auto dest: eps_net_onD)
      with x have "a  A'"
        by(auto simp: A'_def)
      with a show "x  (aA'. open_ball a (e / 2))" by auto
    qed(use h eps_net_on_def A'_def A in auto)
    define b where "b  (λa. SOME b. b  B  b  open_ball a (e / 2))"
    have b:"b a  B" "b a  open_ball a (e / 2)" if a: "a  A'" for a
    proof -
      have "b a  B  b a  open_ball a (e / 2)"
        unfolding b_def by(rule someI_ex) (insert that, auto simp: A'_def)
      thus "b a  B" "b a  open_ball a (e / 2)" by auto
    qed
    show "A. m.eps_net e A"
      unfolding m.eps_net_on_def
    proof(safe intro!: exI[where x="b ` A'"])
      fix x
      assume "x  B"
      then obtain a where a: "a  A'" "x  open_ball a (e / 2)"
        using A' by(auto simp: eps_net_on_def)
      show "x  (ab ` A'. m.open_ball a e)"
      proof
        show "b a  b ` A'"
          using a by auto
      next
        have [simp]: "b a  S" "x  S" "b a  B" "x  B" "a  S"
          using b(1)[OF a(1)] assms x  B a  A' by (auto simp: eps_net_on_def)
        note order.strict_trans1[OF dist_tr add_strict_mono[OF open_ballD[OF a(2),simplified dist_sym[of a]] open_ballD[OF b(2)[OF a(1)]]],simplified]
        hence "submetric B dist x (b a) < e"
          by(auto simp: submetric_def)
        thus "x  m.open_ball (b a) e"
          by(auto simp: m.open_ball_def m.dist_sym)
      qed
    qed(insert h(2) A' b, auto simp: eps_net_on_def)
  next
    fix e :: real
    assume "e>0. A. m.eps_net e A" "e > 0"
    then obtain A where A: "m.eps_net e A" by auto
    thus "A. eps_net_on B e A"
      using assms submetric_open_ball_subset[OF assms] by(auto intro!: exI[where x=A] simp: eps_net_on_def m.eps_net_def) blast
  qed
qed
    
text ‹ Continuous functions ›
context
  fixes S :: "'a set" and d
    and S':: "'b set" and d'
  assumes "metric_set S d" "metric_set S' d'"
begin

interpretation m1: metric_set S d by fact
interpretation m2: metric_set S' d' by fact

lemma metric_set_continuous_map_eq:
  shows "continuous_map m1.mtopology m2.mtopology f
          f  S  S'  (xS. ε>0. δ>0. yS. d x y < δ  d' (f x) (f y) < ε)"
proof safe
  show "x. continuous_map m1.mtopology m2.mtopology f  x  S  f x  S'"
    using m1.mtopology_topspace m2.mtopology_topspace by(auto dest: continuous_map_image_subset_topspace)
next
  fix x ε
  assume "continuous_map m1.mtopology m2.mtopology f"
           "x  S" "(0 :: real) < ε"
  then have "openin m1.mtopology {z  S. f z  m2.open_ball (f x) ε}" "f x  S'"
    using openin_continuous_map_preimage[OF continuous_map m1.mtopology m2.mtopology f]  m2.mtopology_open_ball_in[of "f x",OF _ 0 < ε] continuous_map_image_subset_topspace[OF continuous_map m1.mtopology m2.mtopology f] m1.mtopology_topspace m2.mtopology_topspace
    by auto
  moreover have "x  {z  S. f z  m2.open_ball (f x) ε}"
    using x  S 0 < ε continuous_map_image_subset_topspace[OF continuous_map m1.mtopology m2.mtopology f] m1.mtopology_topspace  m2.mtopology_topspace m2.dist_0[of "f x" "f x"]
    by(auto simp: m2.open_ball_def)
  ultimately obtain δ where
   "δ>0" "m1.open_ball x δ  {z  S. f z  m2.open_ball (f x) ε}"
    by (auto simp: m1.mtopology_openin_iff)
  thus "δ>0. yS. d x y < δ  d' (f x) (f y) < ε"
    using  x  S f x  S' by(auto intro!: exI[where x=δ] simp: m1.open_ball_def m2.open_ball_def)
next
  assume  "f  S  S'"
    and h:"xS. ε>0. δ>0. yS. d x y < δ  d' (f x) (f y) < ε"
  show "continuous_map m1.mtopology m2.mtopology f"
    unfolding continuous_map
  proof safe
    show "x. x  topspace m1.mtopology  f x  topspace m2.mtopology"
      using f  S  S' m1.mtopology_topspace m2.mtopology_topspace by auto
  next
    fix U
    assume "openin m2.mtopology U"
    show "openin m1.mtopology {x  topspace m1.mtopology. f x  U}"
      unfolding m1.mtopology_openin_iff
    proof safe
      show "x. x  topspace m1.mtopology  f x  U  x  S"
        using f  S  S' m1.mtopology_topspace m2.mtopology_topspace by auto
    next
      fix x
      assume "x  topspace m1.mtopology" "f x  U"
      then obtain ε where he:
       "ε > 0" "m2.open_ball (f x) ε  U"
        using openin m2.mtopology U by(auto simp: m2.mtopology_openin_iff)
      then obtain δ where hd:
       "δ > 0" "y. y  S  d x y < δ  d' (f x) (f y) < ε"
        using x  topspace m1.mtopology m1.mtopology_topspace h by metis
      thus "ε>0. m1.open_ball x ε  {x  topspace m1.mtopology. f x  U}"
        using m1.open_ballD m1.open_ballD' m1.mtopology_topspace he(2) f  S  S'
        by(auto intro!: exI[where x=δ] simp: m2.open_ball_def) fastforce
    qed
  qed
qed

lemma metric_set_continuous_map_eq':
  shows "continuous_map m1.mtopology m2.mtopology f
          f  S  S'  (x z. m1.converge_to_inS x z  m2.converge_to_inS (λn. f (x n)) (f z))"
proof
  show "continuous_map m1.mtopology m2.mtopology f  f  S  S'  (x z. m1.converge_to_inS x z  m2.converge_to_inS (λn. f (x n)) (f z))"
    unfolding metric_set_continuous_map_eq
  proof safe
    fix x z
    assume h:"f  S  S'" "xS. ε>0. δ>0. yS. d x y < δ  d' (f x) (f y) < ε" "m1.converge_to_inS x z"
    hence h':"x  m1.sequence" "z  S" "ε. ε > 0  N. nN. d (x n) z < ε"
      by(auto simp: m1.converge_to_inS_def2)
    show "m2.converge_to_inS (λn. f (x n)) (f z)"
      unfolding m2.converge_to_inS_def2
    proof safe
      show "f (x n)  S'" "f z  S'" for n
        using h'(1,2) h(1) by auto
    next
      fix ε
      assume he:"(0 :: real) < ε"
      then obtain δ where hd:"δ > 0" "y. y  S  d z y < δ  d' (f z) (f y) < ε"
        using h(2) h'(2) by metis
      obtain N where hn: "n. n  N  d z (x n) < δ"
        using h'(3)[OF hd(1),simplified m1.dist_sym[of _ z]] by auto
      show "N. nN. d' (f (x n)) (f z) < ε"
      proof(safe intro!: exI[where x=N])
        fix n
        assume "n  N"
        then have "x n  S" "d z (x n) < δ"
          using hn[OF n  N] h'(1) by auto
        thus "d' (f (x n)) (f z) < ε"
          by(auto intro!: hd(2) simp: m2.dist_sym[of _ "f z"])
      qed
    qed
  qed
next
  assume "f  S  S'  (x z. m1.converge_to_inS x z  m2.converge_to_inS (λn. f (x n)) (f z))"
  hence h:"f  S  S'" "x z. m1.converge_to_inS x z  m2.converge_to_inS (λn. f (x n)) (f z)" by auto
  show "continuous_map m1.mtopology m2.mtopology f"
    unfolding continuous_map_closedin
  proof safe
    show "x  topspace m1.mtopology  f x  topspace m2.mtopology" for x
      using m1.mtopology_topspace m2.mtopology_topspace h(1) by auto
  next
    fix C
    assume hcl:"closedin m2.mtopology C"
    show "closedin m1.mtopology {x  topspace m1.mtopology. f x  C}"
      unfolding m1.mtopology_closedin_iff
    proof safe
      fix y s
      assume hg:"y  UNIV  {x  topspace m1.mtopology. f x  C}" " m1.converge_to_inS y s"
      hence "(λn. f (y n))  UNIV  C"
        by auto
      thus "f s  C" "s  topspace m1.mtopology"
        using h(2)[OF hg(2)] hcl[simplified m2.mtopology_closedin_iff] hg(2)[simplified m1.converge_to_inS_def] m1.mtopology_topspace
        by auto
    qed(simp add: m1.mtopology_topspace)
  qed
qed

lemma continuous_map_limit_of:
  assumes "continuous_map m1.mtopology m2.mtopology f" "m1.convergent_inS xn"
  shows "m2.the_limit_of (λn. f (xn n)) = f (m1.the_limit_of xn)"
  using assms  m1.the_limit_if_converge m2.the_limit_of_eq
  by(simp add: metric_set_continuous_map_eq')

text ‹ Uniform continuous functions. ›
definition uniform_continuous_map :: "('a  'b)  bool" where
"uniform_continuous_map f  f  S  S'  (ε>0. δ>0. xS. yS. d x y < δ  d' (f x) (f y) < ε)"

lemma uniform_continuous_map_const:
  assumes "y  S'"
  shows "uniform_continuous_map (λx. y)"
  using assms by(auto simp: uniform_continuous_map_def)

lemma continuous_if_uniform_continuous:
  assumes "uniform_continuous_map f"
  shows "continuous_map m1.mtopology m2.mtopology f"
  unfolding metric_set_continuous_map_eq
proof safe
  show "x  S  f x  S'" for x
    using assms by(auto simp: uniform_continuous_map_def)
next
  fix x ε
  assume [simp]:"x  S" and "(0 :: real) < ε"
  then obtain δ where "δ > 0" "x y. x  S  y  S  d x y < δ  d' (f x) (f y) < ε"
    using assms by(auto simp: uniform_continuous_map_def)
  thus "δ>0. yS. d x y < δ  d' (f x) (f y) < ε"
    by(auto intro!: exI[where x=δ])
qed

definition converges_uniformly :: "[nat  'a  'b, 'a  'b]  bool" where
"converges_uniformly fn f  (n. fn n  S  S')  (f  S  S')  (e>0. N. nN. xS. d' (fn n x) (f x) < e)"

lemma converges_uniformly_continuous:
  assumes "n. continuous_map m1.mtopology m2.mtopology (fn n)"
      and "converges_uniformly fn f"
    shows "continuous_map m1.mtopology m2.mtopology f"
  unfolding metric_set_continuous_map_eq
proof safe
  fix x e
  assume h:"x  S" "e > (0 :: real)"
  then obtain N where N: "z n. n  N  z  S  d' (fn n z) (f z) < e / 3"
    using assms(2) by(simp only: converges_uniformly_def) (meson zero_less_divide_iff zero_less_numeral)
  have f: "n x. x  S  fn n x  S'" "x. x  S  f x  S'"
    using assms(2) by(auto simp: converges_uniformly_def)
  from assms(1)[of N] h obtain δ where h': "δ > 0" "y. y  S  d x y < δ  d' (fn N x) (fn N y) < e / 3"
    by (metis metric_set_continuous_map_eq zero_less_divide_iff zero_less_numeral)
  show "δ>0. yS. d x y < δ  d' (f x) (f y) < e"
  proof(safe intro!: exI[where x=δ])
    fix y
    assume y:"y  S" "d x y < δ"
    have "d' (f x) (f y)  d' (f x) (fn N x) + d' (fn N x) (fn N y) + d' (fn N y) (f y)"
      using m2.dist_tr[of "f x" "fn N x" "f y"] m2.dist_tr[of "fn N x" "fn N y" "f y"] f[OF y(1)] f[OF h(1)]
      by auto
    also have "... < e"
      using N[OF order_refl h(1),simplified m2.dist_sym] N[OF order_refl y(1)] h'(2)[OF y]
      by auto
    finally show "d' (f x) (f y) < e" .
  qed(use h' in auto)
qed(use assms(2) converges_uniformly_def in auto)

text ‹ Lemma related @{term osc_on}.›
lemma osc_on_inA_0:
  assumes "x  A  S" "continuous_map (subtopology m1.mtopology (A  S)) m2.mtopology f"
  shows "m2.osc_on A m1.mtopology f x = 0"
proof -
  interpret subm1: metric_set "A  S" "submetric (A  S) d"
    by(auto intro!: m1.submetric_metric_set)
  have cont: "continuous_map subm1.mtopology m2.mtopology f"
    using assms(2) by (simp add: m1.submetric_subtopology)
  have "m2.osc_on A m1.mtopology f x < ennreal ε" if e:"ε > 0" for ε
    unfolding m2.osc_on_less_iff
  proof -
    obtain ε' where "ε' > 0" "2*ε' < ε"
      using e field_lbound_gt_zero[of "ε/2" "ε/2"] by auto
    then obtain δ where hd:"δ>0" "y. y  A  yS  d x y < δ  d' (f x) (f y) < ε'"
      using assms(1) cont[simplified Set_Based_Metric_Space.metric_set_continuous_map_eq[OF subm1.metric_set_axioms m2.metric_set_axioms]]
      by(fastforce simp: submetric_def)
    show "v. x  v  openin m1.mtopology v  m2.diam (f ` (A  v)) < ennreal ε"
    proof(safe intro!: exI[where x="m1.open_ball x δ"] m1.open_ball_ina m1.mtopology_open_ball_in)
      have "m2.diam (f ` (A  m1.open_ball x δ))  ennreal (2*ε')"
        unfolding m2.diam_def Sup_le_iff
      proof safe
        fix a1 a2
        assume h:"a1  A" "a1  m1.open_ball x δ" "f a1  S'"
                 "a2  A" "a2  m1.open_ball x δ" "f a2  S'"
        have "f x  S'"
          using cont assms(1) by(auto simp: Set_Based_Metric_Space.metric_set_continuous_map_eq[OF subm1.metric_set_axioms m2.metric_set_axioms])
        have "d' (f a1) (f a2) < 2*ε'"
          using hd(2)[OF a1  A m1.open_ballD'(1)[OF h(2)] m1.open_ballD[OF h(2)]] hd(2)[OF a2  A m1.open_ballD'(1)[OF h(5)] m1.open_ballD[OF h(5)]] m2.dist_tr[OF f a1  S' f x  S' f a2  S',simplified m2.dist_sym[of "f a1" "f x"]]
          by auto
        thus "ennreal (d' (f a1) (f a2))  ennreal (2*ε')"
          by (simp add: ennreal_leI)
      qed
      also have "... < ennreal ε"
        using 2*ε' < ε ennreal_lessI e by presburger 
      finally show "m2.diam (f ` (A  m1.open_ball x δ)) < ennreal ε" .
    qed(use hd(1) IntD2[OF assms(1)] in auto)
  qed
  hence "m2.osc_on A m1.mtopology f x < ε" if "ε > 0" for ε
    by (metis ennreal_enn2real ennreal_le_epsilon ennreal_less_zero_iff linorder_not_le order_le_less_trans that)
  thus ?thesis
    by fastforce
qed

end

context metric_set
begin

interpretation rnv: metric_set "UNIV :: ('b :: real_normed_vector) set" dist_typeclass
  by simp

lemma dist_set_uniform_continuous:
 "uniform_continuous_map S dist UNIV dist_typeclass (dist_set A)"
  unfolding uniform_continuous_map_def[OF metric_set_axioms rnv.metric_set_axioms] dist_real_def
proof safe
  fix ε :: real
  assume "0 < ε"
  then show "δ>0. xS. yS. dist x y < δ  ¦dist_set A x - dist_set A y¦ < ε"
    using order.strict_trans1[OF dist_set_abs_le] by(auto intro!: exI[where x=ε])
qed simp

lemma dist_set_continuous: "continuous_map mtopology euclideanreal (dist_set A)"
  unfolding euclidean_mtopology[symmetric]
  by(auto intro!: continuous_if_uniform_continuous simp: dist_set_uniform_continuous metric_set_axioms)


lemma uniform_continuous_map_add:
 fixes f :: "'a  'b::real_normed_vector"
 assumes "uniform_continuous_map S dist UNIV dist_typeclass f" "uniform_continuous_map S dist UNIV dist_typeclass g"
 shows "uniform_continuous_map S dist UNIV dist_typeclass (λx. f x + g x)"
  unfolding uniform_continuous_map_def[OF metric_set_axioms rnv.metric_set_axioms]
proof safe
  fix e :: real
  assume "e > 0"
  from half_gt_zero[OF this] assms obtain d1 d2 where d: "d1 > 0" "d2 > 0"
   "x y. x  S  y  S  dist x y < d1  dist_typeclass (f x) (f y) < e / 2"    "x y. x  S  y  S  dist x y < d2  dist_typeclass (g x) (g y) < e / 2"
    by(simp only: uniform_continuous_map_def[OF metric_set_axioms rnv.metric_set_axioms]) metis
  show "δ>0. xS. yS. dist x y < δ  dist_typeclass (f x + g x) (f y + g y) < e"
    using d by(fastforce intro!: exI[where x="min d1 d2"] order.strict_trans1[OF dist_triangle_add])
qed simp

lemma uniform_continuous_map_real_devide:
 fixes f :: "'a  real"
 assumes "uniform_continuous_map S dist UNIV dist_typeclass f" "uniform_continuous_map S dist UNIV dist_typeclass g"
     and "x. x  S  g x  0" "x. x  S  ¦g x¦  a" "a > 0" "x. x  S  ¦g x¦ < Kg"
     and "x. x  S  ¦f x¦ < Kf"
   shows "uniform_continuous_map S dist UNIV dist_typeclass (λx. f x / g x)"
  unfolding uniform_continuous_map_def[OF metric_set_axioms rnv.metric_set_axioms]
proof safe
  fix e :: real
  assume e[arith]:"e > 0"
  consider "S = {}" | "S  {}" by auto
  then show "δ>0. xS. yS. dist x y < δ  dist_typeclass (f x / g x) (f y / g y) < e"
  proof cases
    case 1
    then show ?thesis by (auto intro!: exI[where x=1])
  next
    case S:2
    then have Kfg_pos[arith]: "Kg > 0" "Kf  0"
      using assms(4-7) by auto fastforce+
    define e' where "e'  a^2 / (Kf + Kg)  * e"
    have e':"e' > 0"
      using assms(5) by(auto simp: e'_def)
    with assms obtain d1 d2 where d: "d1 > 0" "d2 > 0"
    "x y. x  S  y  S  dist x y < d1  ¦f x - f y¦ < e'"    "x y. x  S  y  S  dist x y < d2  ¦g x - g y¦ < e'"
      by(auto simp: uniform_continuous_map_def[OF metric_set_axioms rnv.metric_set_axioms] dist_real_def) metis
    show ?thesis
      unfolding dist_real_def
    proof(safe intro!: exI[where x="min d1 d2"])
      fix x y
      assume x:"x  S" and y:"y  S" and "dist x y < min d1 d2"
      then have dist[arith]: "dist x y < d1" "dist x y < d2" by auto
      note [arith] = assms(3,4,6,7)[OF x] assms(3,4,6,7)[OF y]
      have "¦f x / g x - f y / g y¦ = ¦(f x * g y - f y * g x) / (g x * g y)¦"
        by(simp add: diff_frac_eq)
      also have "... = ¦(f x * g y - f x * g x + (f x * g x  - f y * g x)) / (g x * g y)¦"
        by simp
      also have "... = ¦(f x - f y) * g x - f x * (g x - g y)¦ / (¦g x¦ * ¦g y¦)"
        by(simp add: left_diff_distrib right_diff_distrib abs_mult)
      also have "...  (¦f x - f y¦ * ¦g x¦ + ¦f x¦ * ¦g x - g y¦) / (¦g x¦ * ¦g y¦)"
        by(rule divide_right_mono) (use abs_triangle_ineq4 abs_mult in metis,auto)
      also have "... < (e' * Kg + Kf * e') / (¦g x¦ * ¦g y¦)"
        by(rule divide_strict_right_mono[OF add_less_le_mono]) (auto intro!: mult_mono' mult_strict_mono, use  d(3,4)[OF x y] in auto)
      also have "...  (e' * Kg + Kf * e') / a^2"
        by(auto intro!: divide_left_mono simp: power2_eq_square) (insert assms(5) e', auto simp: a  ¦g x¦ mult_mono')
      also have "... = (Kf + Kg) / a^2 * e'"
        by (simp add: distrib_left mult.commute)
      also have "... = e"
        using assms(5) by(auto simp: e'_def)
      finally show " ¦f x / g x - f y / g y¦ < e" .
    qed(use d in auto)
  qed
qed simp

lemma the_limit_of_dist_converge:
  assumes "converge_to_inS xn x"
  shows "(λn. dist (xn n) y)  dist (the_limit_of xn) y"
proof -
  have "continuous_map mtopology euclideanreal (λz. dist z y)"
    using dist_set_continuous[of "{y}"] by simp
  hence "(λn. dist (xn n) y)  dist x y"
    using assms
    by(auto simp: metric_set_continuous_map_eq'[OF metric_set_axioms rnv.metric_set_axioms,simplified euclidean_mtopology] converge_to_def_set)
  thus ?thesis
    by(simp add: the_limit_of_eq[OF assms])
qed

lemma the_limit_of_dist_converge':
  assumes "converge_to_inS xn x" "ε > 0"
  shows "N. nN. ¦ dist (xn n) y - dist (the_limit_of xn) y ¦ < ε"
  using the_limit_of_dist_converge[OF assms(1)] assms(2) by(simp add: LIMSEQ_iff)

lemma the_limit_of_dist:
  assumes "converge_to_inS xn x"
  shows "lim (λn. dist (xn n) y) = dist (the_limit_of xn) y"
  using the_limit_of_dist_converge[OF assms] limI by blast

text ‹ Upper-semicontinuous functions.›
lemma upper_semicontinuous_map_def2:
  fixes f :: "'a  ('b :: {complete_linorder,linorder_topology})"
  shows "upper_semicontinuous_map mtopology f  (x y. converge_to_inS x y  limsup (λn. f (x n))  f y)"
proof
  show "upper_semicontinuous_map mtopology f  x y. converge_to_inS x y  limsup (λn. f (x n))  f y"
    unfolding upper_semicontinuous_map_def
  proof safe
    fix x y
    assume h:"a. openin mtopology {x  topspace mtopology. f x < a}" "converge_to_inS x y"
    show "limsup (λn. f (x n))  f y"
      unfolding Limsup_le_iff eventually_sequentially
    proof safe
      fix c
      assume "f y < c"
      show "N. nN. f (x n) < c"
      proof(rule ccontr)
        assume "N. nN. f (x n) < c"
        then have hc:"N. nN. f (x n)  c"
          using linorder_not_less by blast
        define a :: "nat  nat" where "a  rec_nat (SOME n. f (x n)  c) (λn an. SOME m. m > an  f (x m)  c)"
        have "strict_mono a"
        proof(rule strict_monoI_Suc)
          fix n
          have [simp]:"a (Suc n) = (SOME m. m > a n  f (x m)  c)"
            by(auto simp: a_def)
          show "a n < a (Suc n)"
            by simp (metis (mono_tags, lifting) Suc_le_lessD hc someI)
        qed
        have *:"f (x (a n))  c" for n
        proof(cases n)
          case 0
          then show ?thesis
            using hc[of 0] by(auto simp: a_def intro!: someI_ex)
        next
          case (Suc n')
          then show ?thesis
            by(simp add: a_def) (metis (mono_tags, lifting) Suc_le_lessD hc someI_ex)
        qed
        obtain N where "n. n  N  x (a n)  {x  S. f x < c}"
          using converge_to_inS_subseq[OF strict_mono a h(2)] mtopology_openin_iff2[of "{x  S. f x < c}"] h(2)[simplified converge_to_inS_def] mtopology_topspace f y < c h
          by fastforce
        from *[of N] this[of N] show False by auto
      qed
    qed
  qed
next
  assume h:"x y. converge_to_inS x y  limsup (λn. f (x n))  f y"
  show "upper_semicontinuous_map mtopology f"
    unfolding upper_semicontinuous_map_def mtopology_openin_iff2 mtopology_topspace
  proof safe
    fix a y s
    assume "converge_to_inS y s" "s  S" "f s < a"
    then have "limsup (λn. f (y n))  f s"
      using h by auto
    with f s < a obtain N where "n. nN  f (y n) < a"
      by(auto simp: Limsup_le_iff eventually_sequentially)
    thus "N. nN. y n  {x  S. f x < a}"
      using converge_to_inS y s by(auto intro!: exI[where x=N] simp: converge_to_inS_def)
  qed
qed

lemma upper_semicontinuous_map_def2real:
  fixes f :: "'a  real"
  shows "upper_semicontinuous_map mtopology f  (x y. converge_to_inS x y  limsup (λn. f (x n))  f y)"
  unfolding upper_semicontinuous_map_real_iff upper_semicontinuous_map_def2
  by auto

lemma osc_upper_semicontinuous_map:
 "upper_semicontinuous_map X (osc X f)"
proof -
  have "{x  topspace X. osc X f x < a} =  {V. openin X V  diam (f ` V) < a}" for a
   using openin_subset by(auto simp add: osc_less_iff)
  thus ?thesis
    by(auto simp: upper_semicontinuous_map_def)
qed

end

text ‹ Open maps.›
lemma metric_set_opem_map_from_dist:
  assumes "metric_set S d" "metric_set S' d'" "f  S  S'"
      and "x ε. x  S  ε > 0  δ>0. yS. d' (f x) (f y) < δ  d x y < ε"
    shows "open_map (metric_set.mtopology S d) (subtopology (metric_set.mtopology S' d') (f ` S)) f"
proof -
  interpret m1: metric_set S d by fact
  interpret m2: metric_set S' d' by fact
  interpret m2': metric_set "f ` S" "submetric (f ` S) d'"
    using assms(3) by(auto intro!: m2.submetric_metric_set)
  show ?thesis
  proof(rule open_map_with_base[OF m1.mtopology_basis_ball])
    fix A
    assume "A  {m1.open_ball a ε |a ε. a  S  0 < ε}"
    then obtain a ε where hae:
     "a  S" "0 < ε" "A = m1.open_ball a ε" by auto
    show "openin (subtopology m2.mtopology (f ` S)) (f ` A)"
      unfolding m2.submetric_subtopology[OF funcset_image[OF assms(3)]]  m2'.mtopology_openin_iff
    proof
      show "f ` A  f ` S"
        using m1.open_ball_subset_ofS[of a ε] by(auto simp: hae(3))
    next
      show "xf ` A. ε>0. m2'.open_ball x ε  f ` A"
      proof safe
        fix x
        assume "x  A"
        hence "x  S"
          using m1.open_ball_subset_ofS[of a ε] by(auto simp: hae(3))
        moreover have "0 < ε - d a x"
          using x  A m1.open_ballD[of x a ε] by(auto simp: hae(3))
        ultimately obtain δ where hd:"δ > 0" "y. yS  d' (f x) (f y) < δ  d x y <  ε - d a x"
          using assms(4) by metis
        show "ε>0. m2'.open_ball (f x) ε  f ` A"
        proof(safe intro!: exI[where x=δ])
          fix z
          assume "z  m2'.open_ball (f x) δ"
          note hz = m2'.open_ballD'[OF this]
          then obtain y where "y  S" "z = f y" by auto
          hence "d' (f x) (f y) < δ"
            using m2'.open_ballD[OF z  m2'.open_ball (f x) δ] x  A m1.open_ball_subset_ofS[of a ε]
            by(auto simp: submetric_def  hae(3))
          hence "d x y <  ε - d a x"
            by(auto intro!: hd(2)[OF y  S])
          hence "d a y < ε"
            using m1.dist_tr[OF a  S x  S y  S] by auto
          thus "z  f ` A"
            by (simp add: y  S z = f y hae(1) hae(3) m1.open_ball_def)
        qed(use hd in auto)
      qed
    qed
  qed
qed

subsubsection ‹ Complete Metric Spaces›
locale complete_metric_set = metric_set +
  assumes convergence: "f. Cauchy_inS f  convergent_inS f"

lemma complete_space_complete_metric_set:
 "complete_metric_set (UNIV :: 'a :: complete_space set) dist"
proof -
  interpret m: metric_set UNIV dist
    by(rule metric_class_metric_set)
  show ?thesis
    by standard (simp add: Cahuchy_def_set[symmetric] convergent_def_set[symmetric] Cauchy_convergent_iff)
qed

lemma(in complete_metric_set) submetric_complete_iff:
  assumes "M  S"
  shows "complete_metric_set M (submetric M dist)  closedin mtopology M"
proof
  assume "complete_metric_set M (submetric M dist)"
  then interpret m: complete_metric_set M "submetric M dist" .
  show "closedin mtopology M"
  proof(rule ccontr)
    assume "¬ closedin mtopology M"
    then have "fm.sequence. s. converge_to_inS f s  s  M"
      using assms mtopology_closedin_iff by auto
    then obtain f s where hfs:"f  m.sequence" "converge_to_inS f s" "s  M"
      by auto
    hence "convergent_inS f"
      by(auto simp: convergent_inS_def converge_to_inS_def)
    have "m.Cauchy_inS f"
      using Cauchy_if_convergent_inS[OF convergent_inS f] hfs(1)
      by(auto simp: m.Cauchy_inS_def Cauchy_inS_def) (fastforce simp: submetric_def)
    then obtain s' where "s'  M" "m.converge_to_inS f s'"
      using m.convergence by(auto simp: m.convergent_inS_def m.converge_to_inS_def)
    from converge_to_insub_converge_to_inS[OF assms this(2)] hfs(2)
    have "s' = s"
      by(rule converge_to_inS_unique)
    thus False
      using s'  M s  M by simp
  qed
next
  interpret m: metric_set M "submetric M dist"
    by(rule submetric_metric_set[OF assms])
  assume cls:"closedin mtopology M"
  show "complete_metric_set M (submetric M dist)"
  proof
    fix f
    assume "m.Cauchy_inS f"
    then have "f  m.sequence" by(simp add: m.Cauchy_inS_def)
    have "Cauchy_inS f"
      by(rule Cauchy_insub_Cauchy[OF assms m.Cauchy_inS f])
    then obtain x where hx:"x  S" "converge_to_inS f x"
      using convergence by(auto simp: convergent_inS_def converge_to_inS_def)
    hence "x  M"
      using cls[simplified mtopology_closedin_iff] f  m.sequence assms
      by auto
    hence "m.converge_to_inS f x"
      using convergent_insubmetric[OF assms f  m.sequence] hx by auto
    thus "m.convergent_inS f"
      using x  M by(auto simp: m.convergent_inS_def)
  qed
qed

lemma(in complete_metric_set) embed_dist_complete:
  assumes "f  B  S" "inj_on f B" "closedin mtopology (f ` B)"
  shows "complete_metric_set B (embed_dist_on B f)"
proof -
  interpret m: metric_set B "embed_dist_on B f"
    by(rule embed_dist_dist[OF assms(1,2)])
  show ?thesis
  proof
    fix xn
    assume "m.Cauchy_inS xn"
    hence h:"xn  m.sequence" "Cauchy_inS (λn. f (xn n))"
      by(auto simp add: embed_dist_Cauchy_inS_iff[OF assms(1,2)])
    with convergence obtain x where x: "converge_to_inS (λn. f (xn n)) x"
      by(auto simp: convergent_inS_def)
    have x': "x  f ` B"
    proof -
      have "(λn. f (xn n))  UNIV  f ` B"
        using assms(1) h(1) by auto
      thus ?thesis
        using assms(3) x by(auto simp: mtopology_closedin_iff) 
    qed
    then obtain b where b: "b  B" "f b = x" by auto
    show "m.convergent_inS xn"
      by(auto simp: m.convergent_inS_def embed_dist_converge_to_inS_iff[OF assms(1,2)] b x h intro!: exI[where x=b])
  qed
qed

lemma(in metric_set) Cantor_intersection_theorem:
 "complete_metric_set S dist  (Fn. (n. Fn n  {})  (n. closedin mtopology (Fn n))  decseq Fn  (ε > 0. N. nN. diam (Fn n) < ε)  (xS.  (range Fn) = {x}))"
proof safe
  fix Fn
  assume "complete_metric_set S dist"
  interpret complete_metric_set S dist by fact
  assume h: "n. Fn n  {}" " n. closedin mtopology (Fn n)" "decseq Fn" "ε > 0. N. nN. diam (Fn n) < ε"
  then obtain xn where xn1: "n. xn n  Fn n"
    by (meson all_not_in_conv)
  hence xn2: "xn  sequence"
    using closedin_subset[of mtopology] h(2) by(auto simp: mtopology_topspace)
  have "Cauchy_inS xn"
    unfolding Cauchy_inS_def
  proof safe
    fix ε :: real
    assume "0 < ε"
    then obtain N where N:"n. nN  diam (Fn n) < ennreal ε"
      using h(4) ennreal_less_zero_iff by blast
    show "N. nN. mN. dist (xn n) (xn m) < ε"
    proof(safe intro!: exI[where x=N])
      fix n m
      assume "n  N" "m  N"
      define nm where "nm = min m n"
      have "nm  N" "nm  n" "nm  m"
        using n  N m  N by(auto simp: nm_def)
      hence "xn n  Fn nm" "xn m  Fn nm"
        using decseqD[OF h(3)] xn1[of n] xn1[of m] by auto
      hence "ennreal (dist (xn n) (xn m))  diam (Fn nm)"
        using xn2 by(auto intro!: diam_is_sup  mtopology_topspace)
      also have "... < ennreal ε"
        by(rule N[OF nm  N])
      finally show "dist (xn n) (xn m) < ε"
        by (simp add: dist_geq0 ennreal_less_iff)
    qed
  qed(use xn2 in auto)
  then obtain x where x:"x  S" "converge_to_inS xn x"
    using convergence[of xn] by(auto simp: convergent_inS_def converge_to_inS_def)
  show "xS.  (range Fn) = {x}"
  proof(safe intro!: bexI[where x=x])
    fix n
    show "x  Fn n"
    proof(rule ccontr)
      assume "x  Fn n"
      moreover have "openin mtopology (S - Fn n)"
        using h(2) by (simp add: openin_diff)
      ultimately obtain ε where e: "ε > 0" "open_ball x ε  S - Fn n"
        using x(1) by(auto simp: mtopology_openin_iff)
      then have "N. nN. xn n  open_ball x ε"
        using mtopology_openin_iff2[of "open_ball x ε"] open_ball_ina[OF x(1) e(1)] x(2)
        by(auto simp: openin_open_ball)
      then obtain N where N:"m. m  N  xn m  open_ball x ε"
        by auto
      hence "xn m  S - Fn m" if "m  N" "m  n" for m
        using e(2) decseqD[OF h(3) that(2)] using that(1) by blast
      from xn1[of "max N n"] this[of "max N n"]
      show False by auto
    qed
  next
    fix y
    assume "y   (range Fn)"
    then have hy:"n. y  Fn n" by auto
    have "y  S"
        using closedin_subset[of mtopology] h(2) hy mtopology_topspace by auto
    have "converge_to_inS xn y"
      unfolding converge_to_inS_def2
    proof safe
      fix ε :: real
      assume "0 < ε"
      then obtain N where N:"n. n  N  diam (Fn n) < ennreal ε"
        using ennreal_less_zero_iff h(4) by presburger
      show "N. nN. dist (xn n) y < ε"
      proof(safe intro!: exI[where x=N])
        fix n
        assume "n  N"
        then have "ennreal (dist (xn n) y) < ennreal ε"
          using y  S hy xn1[of n] xn2
          by(auto intro!: order.strict_trans1[OF diam_is_sup[of "xn n" "Fn n" y] N[of n]])
        thus "dist (xn n) y < ε"
          by (simp add: dist_geq0 ennreal_less_iff)
      qed
    qed(use xn2 y  S in auto)
    with converge_to_inS_unique[OF x(2)]
    show "y = x" by simp
  qed(use x in auto)
next
  assume h:"Fn. (n. Fn n  {})  (n. closedin mtopology (Fn n))  decseq Fn  (ε>0. N. nN. diam (Fn n) < ε)  (xS.  (range Fn) = {x})"
  show "complete_metric_set S dist"
  proof
    fix xn
    assume cauchy:"Cauchy_inS xn"
    hence xn: "xn  sequence"
      by (simp add: Cauchy_inS_dest1)
    define Fn where "Fn  (λn. mtopology closure_of {xn m|m. m  n})"
    have Fn0': "{xn m|m. m  n}  Fn n" for n
      using xn by(auto intro!: closure_of_subset simp: Fn_def mtopology_topspace)
    have Fn0: "n. Fn n  S"
      using xn by(auto simp: Fn_def in_closure_of metric_set.mtopology_topspace metric_set_axioms)
    have Fn1: "Fn n  {}" for n
      using xn closure_of_eq_empty[of "{xn m|m. m  n}" mtopology,simplified mtopology_topspace]
      by(auto simp: Fn_def)
    have Fn2:"n. closedin mtopology (Fn n)"
      by(simp add: Fn_def)
    have Fn3: "decseq Fn"
      by standard (auto simp: Fn_def intro!: closure_of_mono)
    have Fn4:"ε>0. N. nN. diam (Fn n) < ε"
    proof safe
      fix ε :: ennreal
      assume "0 < ε"
      define e where "e  min 1 ε"
      have he: "e  ε" "enn2real e > 0" "ennreal (enn2real e) = e"
        using 0 < ε by(auto simp: e_def enn2real_positive_iff min_less_iff_disj)
      then obtain e' where e':"e' > 0" "e' < enn2real e"
        using field_lbound_gt_zero by auto
      then obtain N where N:"n m. n  N  m  N  dist (xn n) (xn m)  e'"
        using cauchy by(fastforce simp: Cauchy_inS_def)
      show "N. nN. diam (Fn n) < ε"
      proof(safe intro!: exI[where x=N])
        fix n
        assume "N  n"
        then have "diam (Fn n)  ennreal e'"
          by(auto intro!: diam_le N simp: Fn_def diam_eq_closure)
        also have "... < e"
          using e'(2) ennreal_lessI he(2) he(3) by fastforce
        finally show "diam (Fn n) < ε"
          using he(1) by auto
      qed
    qed
    obtain x where x:"xS" " (range Fn) = {x}"
      using h Fn1 Fn2 Fn3 Fn4 by metis
    show "convergent_inS xn"
      unfolding convergent_inS_def converge_to_inS_def2
    proof(safe intro!: exI[where x=x])
      fix ε :: real
      assume he:"0 < ε"
      then have "0 < ennreal ε" by simp
      then obtain N where N: "n. n  N  diam (Fn n) < ennreal ε"
        using Fn4 by metis
      show "N. nN. dist (xn n) x < ε"
      proof(safe intro!: exI[where x=N])
        fix n
        assume "N  n"
        then have "xn n  Fn N" "x  Fn N"
          using x(2) Fn0'[of N] by auto
        hence "ennreal (dist (xn n) x)  diam (Fn N)"
          using Fn0 by(auto intro!: diam_is_sup)
        also have "... <  ennreal ε"
          by(auto intro!: N)
        finally show "dist (xn n) x < ε"
          by (simp add: dist_geq0 ennreal_less_iff)
      qed
    qed(use xn x in auto)
  qed
qed

lemma(in complete_metric_set) closed_decseq_Inter':
  assumes "n. Fn n  {}" "n. closedin mtopology (Fn n)" "decseq Fn"
      and "ε. ε > 0  N. nN. diam (Fn n) < ε"
    shows "xS.  (range Fn) = {x}"
  using assms Cantor_intersection_theorem by(simp add: complete_metric_set_axioms)

lemma(in complete_metric_set) closed_decseq_Inter:
  assumes "n. Fn n  {}" "n. closedin mtopology (Fn n)" "decseq Fn"
      and "ε. ε > 0  N. nN. diam (Fn n) < ennreal ε"
    shows "xS.  (range Fn) = {x}"
proof -
  have "N. nN. diam (Fn n) < ε" if "ε > 0" for ε
  proof -
    consider "ε < " | "ε = "
      using top.not_eq_extremum by fastforce
    then show ?thesis
    proof cases
      case 1
      with that have 2:"ennreal (enn2real ε) = ε"
        by simp
      have "0 < enn2real ε"
        using 1 that by(simp add: enn2real_positive_iff)
      from assms(4)[OF this] show ?thesis
        by(simp add: 2)
    next
      case 2
      then show ?thesis
        by (metis assms(4) ennreal_less_top gt_ex infinity_ennreal_def order_less_imp_not_less top.not_eq_extremum)
    qed
  qed
  thus ?thesis
    using closed_decseq_Inter'[OF assms(1-3)] by simp
qed

subsubsection ‹ Separable Metric Spaces ›
locale separable_metric_set = metric_set +
  assumes separable: "U. countable U  dense_set U"

lemma(in metric_set) separable_if_countable:
  assumes "countable S"
  shows "separable_metric_set S dist"
  apply standard
  using assms by(auto intro!: exI[where x=S] simp: dense_set_S)

lemma(in metric_set) separable_iff_topological_separable:
 "separable_metric_set S dist  separable mtopology"
  by(simp add: separable_metric_set_def separable_metric_set_axioms_def separable_def metric_set_axioms)

lemma(in separable_metric_set) topological_separable_if_separable:
  "separable mtopology"
  using separable_iff_topological_separable
  by (simp add: separable_metric_set_axioms)

lemma separable_metric_setI:
  assumes "metric_set S d" "separable (metric_set.mtopology S d)"
  shows "separable_metric_set S d"
  by (simp add: assms(1) assms(2) metric_set.separable_iff_topological_separable)

text ‹ For a metric space $X$, $X$ is separable iff $X$ is second countable.›
lemma(in metric_set) generated_by_countable_balls:
  assumes "countable U" and "dense_set U"
  shows "mtopology = topology_generated_by {open_ball y (1 / real n) | y n. y  U}"
proof -
  have hu: "U  S" "x ε. x  S  ε > 0  open_ball x ε  U  {}"
    using assms by(auto simp: dense_set_def)
  show ?thesis
    unfolding mtopology_def2
  proof(rule topology_generated_by_eq)
    fix K
    assume "K  {open_ball y (1 / real n) |y n. y  U}"
    then obtain y n where hyn:
     "y  U" "y  S" "K = open_ball y (1 / real n)"
      using hu(1) by auto
    consider "n = 0" | "n > 0" by auto
    then show "openin (topology_generated_by {open_ball a ε |a ε. a  S  0 < ε}) K"
    proof cases
      case 1
      then have "K = {}"
        using hyn dist_geq0[of y] not_less by(auto simp: open_ball_def)
      thus ?thesis
        by auto
    next
      case 2
      then have "1 / real n > 0" by auto
      thus ?thesis
        using hyn mtopology_open_ball_in[simplified mtopology_def2] by auto
    qed
  next
    have h0:"x ε. x  S  ε > 0  yU. n. x  open_ball y (1 / real n)  open_ball y (1 / real n)  open_ball x ε"
    proof -
      fix x ε
      assume h: "x  S" "(0 :: real) < ε"
      then obtain N where hn: "1 / ε < real N"
        using reals_Archimedean2 by blast
      have hn0: "0 < real N"
        by(rule ccontr) (use hn h in fastforce)
      hence hn':"1 / real N < ε"
        using h hn by (metis divide_less_eq mult.commute)
      have "open_ball x (1 / (2 * real N))  U  {}"
        using dense_set_def[of U] assms(2) h(1) hn0 by fastforce
      then obtain y where hy:
        "yU" "y  S" "y  open_ball x (1 / (real (2 * N)))"
        using hu by auto
      show "yU. n. x  open_ball y (1 / real n)  open_ball y (1 / real n)  open_ball x ε"
      proof(intro bexI[where x=y] exI[where x="2 * N"] conjI)
        show "x  open_ball y (1 / real (2 * N))"
          using hy(3) by(simp add: open_ball_inverse[of x y])
      next
        show "open_ball y (1 / real (2 * N))  open_ball x ε"
        proof
          fix y'
          assume hy':"y'  open_ball y (1 / real (2 * N))"
          have "dist x y' < ε" (is "?lhs < ?rhs")
          proof -
            have "?lhs  dist x y + dist y y'"
              using hy(2) open_ballD'(1)[OF hy'] h(1) by(auto intro!: dist_tr)
            also have "... < 1 / real (2 * N) + 1 / real (2 * N)"
              apply(rule strict_ordered_ab_semigroup_add_class.add_strict_mono)
              using hy(3) hy(2) open_ballD'(1)[OF hy'] h(1) hy' by(simp_all add: open_ball_def dist_sym[of x y])
            finally show ?thesis
              using hn' by auto
          qed
          thus "y'  open_ball x ε"
            using open_ballD'(1)[OF hy'] h(1) by(simp add: open_ball_def)
        qed
      qed fact
    qed
    fix K
    assume hk: "K  {open_ball a ε |a ε. a  S  0 < ε}"
    then obtain x εx where hxe:
       "x  S" "0 < εx" "K = open_ball x εx" by auto
    have gh:"K = ({open_ball y (1 / real n) | y n. y  U  open_ball y (1 / real n)  K})"
    proof
      show "K  ( {open_ball y (1 / real n) |y n. y  U  open_ball y (1 / real n)  K})"
      proof
        fix k
        assume hkink:"k  K"
        then have hkinS:"k  S"
          using open_ballD'(1)[of k] by(simp add: hxe)
        obtain εk where hek:
          "εk > 0" "open_ball k εk  K"
          using mtopology_open_ball_in'[of k x] hkink
          by(auto simp: hxe)
        obtain y n where hyey:
          "y  U" "k  open_ball y (1 / real n)" "open_ball y (1 / real n)  open_ball k εk"
          using h0[OF hkinS hek(1)] by auto
        show "k    {open_ball y (1 / real n) |y n. y  U  open_ball y (1 / real n)  K}"
          using hek(2) hyey by blast
      qed
    qed auto
    show "openin (topology_generated_by {open_ball y (1 / real n) |y n. y  U}) K"
      unfolding openin_topology_generated_by_iff
      apply(rule generate_topology_on.UN[of "{open_ball y (1 / real n) |y n. y  U  open_ball y (1 / real n)  K}", simplified gh[symmetric]])
      apply(rule generate_topology_on.Basis) by auto
  qed
qed

lemma(in separable_metric_set) second_countable':
 "𝒪. countable 𝒪  mtopology_basis 𝒪"
proof -
  obtain U where hu:
   "countable U" "dense_set U"
    using separable by auto
  show ?thesis
  proof(rule countable_base_from_countable_subbase[where 𝒪="{open_ball y (1 / real n) | y n. y  U}",simplified second_countable_def])
    have "{open_ball y (1 / real n) |y n. y  U} = (λ(y,n). open_ball y (1 / real n)) ` (U × UNIV)"
      by auto
    also have "countable ..."
      using hu by auto
    finally show "countable {open_ball y (1 / real n) |y n. y  U}" .
  qed (simp add: generated_by_countable_balls[OF hu] subbase_of_def)
qed

lemma(in separable_metric_set) second_countable: "second_countable mtopology"
  by(simp add: second_countable_def second_countable')

lemma(in metric_set) separable_if_second_countable:
  assumes "countable 𝒪" and "mtopology_basis 𝒪"
  shows "separable_metric_set S dist"
proof
  have 1:"mtopology = topology_generated_by {U  𝒪. U  {}}"
    by(simp add: topology_generated_by_without_empty[symmetric] base_is_subbase[OF assms(2),simplified subbase_of_def])
  have "U  {U 𝒪. U  {} }. x. x  U"
    by auto
  then have "x. U  { U  𝒪. U  {} }. x U  U"
    by(rule bchoice)
  then obtain x where hx:
    "U  { U  𝒪. U  {} }. x U  U"
    by auto
  show "U. countable U  dense_set U"
  proof(intro exI[where x="{ x U | U.  U  𝒪  U  {}}"] conjI)
    have "{x U |U. U  𝒪  U  {}} = (λU. x U) ` { U  𝒪. U  {} }"
      by auto
    also have "countable ..."
      using assms(1) by auto
    finally show "countable {x U |U. U  𝒪  U  {}}" .
  next
    show "dense_set {x U |U. U  𝒪  U  {}}"
      unfolding dense_set_def
    proof
      have "U. U  𝒪  U  topspace mtopology"
        using assms(2)[simplified base_of_def2']
        by(auto intro!: openin_subset)
      then show "{x U |U. U  𝒪  U  {}}  S"
        using hx by(auto simp add: mtopology_topspace)
    next
      show "xaS. ε>0. open_ball xa ε  {x U |U. U  𝒪  U  {}}  {}"
      proof safe
        fix s ε
        assume h:"s  S" "(0::real) < ε" "open_ball s ε  {x U |U. U  𝒪  U  {}} = {}"
        then have "openin mtopology (open_ball s ε)"
          by(auto intro!: mtopology_open_ball_in)
        moreover have "open_ball s ε  {}"
          using h open_ball_ina by blast
        ultimately obtain U' where
          "U'𝒪" "U'  {}" "U'  open_ball s ε"
          using assms(2)[simplified base_of_def] by fastforce
        then have "x U'  open_ball s ε  {x U |U. U  𝒪  U  {}}"
          using hx by blast
        with h show False
          by auto
      qed
    qed
  qed
qed

lemma metric_generates_same_topology_separable_if:
  assumes "metric_set S d" "metric_set S d'"
      and "metric_set.mtopology S d = metric_set.mtopology S d'"
      and "separable_metric_set S d"
    shows "separable_metric_set S d'"
proof -
  interpret m1: separable_metric_set S d by fact
  interpret m2: metric_set S d' by fact
  obtain 𝒪 where "countable 𝒪" "m1.mtopology_basis 𝒪"
    using m1.second_countable' by auto
  thus ?thesis
    by(auto intro!: m2.separable_if_second_countable simp: assms(3)[symmetric])
qed

lemma metric_generates_same_topology_separable:
  assumes "metric_set S d" "metric_set S d'"
      and "metric_set.mtopology S d = metric_set.mtopology S d'"
    shows "separable_metric_set S d  separable_metric_set S d'"
  using metric_generates_same_topology_separable_if[OF assms] metric_generates_same_topology_separable_if[OF assms(2,1) assms(3)[symmetric]]
  by auto

lemma(in metric_set) separable_if_totally_bounded:
  assumes totally_boundedS
  shows "separable_metric_set S dist"
  unfolding separable_iff_topological_separable
proof -
  have "A. finite A  A  S  S =  ((λa. open_ball a (1 / real (Suc n))) ` A)" for n
    using totally_boundedSD[OF assms,of "1 / Suc n"] by fastforce 
  then obtain A where A:"n. finite (A n)" "n. A n  S" "n. S =   ((λa. open_ball a (1 / real (Suc n))) ` (A n))"
    by metis
  define K where "K   (range A)"
  have 1: "countable K"
    using A(1) by(auto intro!: countable_UN[of _ id,simplified] simp: K_def countable_finite)
  show "separable mtopology"
    unfolding dense_set_def2 separable_def
  proof(safe intro!: exI[where x=K] 1)
    fix x and ε :: real
    assume h: "x  S" "0 < ε"
    then obtain n where n:"1 / real (Suc n)  ε"
      by (meson nat_approx_posE order.strict_iff_not)
    then obtain y where y: "y  A n" "x  open_ball y (1 / real (Suc n))"
      using h(1) A(3)[of n] by auto
    then show "yK. dist x y < ε"
      using open_ballD[OF y(2)] n by(auto intro!: bexI[where x=y] simp: dist_sym[of y x] K_def)
  qed(use K_def A(2) in auto)
qed

lemma second_countable_metric_class_separable_set:
 "separable_metric_set (UNIV :: 'a ::{metric_space,second_countable_topology} set) dist"
proof -
  interpret m: metric_set UNIV dist
    by(rule metric_class_metric_set)
  obtain B :: "'a set set" where "countable B  topological_basis B"
    using second_countable_topology_class.ex_countable_basis by auto
  then show ?thesis
    by(auto intro!: m.separable_if_second_countable[where 𝒪=B] simp: topological_basis_set)
qed

lemma second_countable_euclidean[simp]:
 "second_countable (euclidean :: 'a :: {metric_space,second_countable_topology} topology)"
  by (metis euclidean_mtopology second_countable_metric_class_separable_set separable_metric_set.second_countable)

lemma separable_euclidean[simp]:
 "separable (euclidean :: 'a :: {metric_space,second_countable_topology} topology)"
  by(auto intro!: separable_if_second_countable)

lemma(in separable_metric_set) submetric_separable:
  assumes "S'  S"
  shows "separable_metric_set S' (submetric S' dist)"
proof -
  interpret m: metric_set S' "submetric S' dist"
    by(rule submetric_metric_set[OF assms])
  obtain 𝒪 where ho:"countable 𝒪" "mtopology_basis 𝒪"
    using second_countable' by auto
  show ?thesis
  proof(rule m.separable_if_second_countable[where 𝒪="{S'  U | U. U𝒪}"])
    show "countable {S'  U |U. U  𝒪}"
      using countable_image[where f="(∩) S'",OF ho(1)]
      by (simp add: Setcompr_eq_image)
  next
    show "m.mtopology_basis {S'  U |U. U  𝒪}"
      by(auto simp: submetric_subtopology[OF assms,symmetric] intro!: subtopology_base_of ho(2))
  qed
qed

lemma(in separable_metric_set) Lindelof_diam:
  assumes "0 < e"
  shows "U. countable U   U = S  (uU. diam u < ennreal e)"
proof -
  have "(u. u  {open_ball x (e / 3) |x. x  S}  openin mtopology u)"
    by(auto simp: openin_open_ball)
  moreover have " {open_ball x (e / 3) |x. x  S} = S"
    using open_ball_ina open_ball_subset_ofS assms by auto
  ultimately have "U'. countable U'  U'  {open_ball x (e / 3) |x. x  S}   U' = S"
    by(rule Lindelof_of[OF second_countable,simplified mtopology_topspace]) auto
  then obtain U' where U': "countable U'" "U'  {open_ball x (e / 3) |x. x  S}" " U' = S"
    by auto
  show ?thesis
  proof(safe intro!: exI[where x=U'])
    fix u
    assume "u  U'"
    then obtain x where u:"u = open_ball x (e / 3)"
      using U' by auto
    have "diam u  ennreal (2 * (e / 3))"
      by(simp only: u diam_ball_leq)
    also have "... < ennreal e"
      by(auto intro!: ennreal_lessI assms)
    finally show "diam u < ennreal e" .
  qed(use U' in auto)
qed

subsubsection ‹ Polish Metric Spaces ›
locale polish_metric_set = complete_metric_set + separable_metric_set

lemma polish_class_polish_set[simp]:
 "polish_metric_set (UNIV :: 'a :: polish_space set) dist"
  using second_countable_metric_class_separable_set complete_space_complete_metric_set
  by(simp add: polish_metric_set_def)

lemma(in polish_metric_set) submetric_polish:
  assumes "M  S" and "closedin mtopology M"
  shows "polish_metric_set M (submetric M dist)"
  using submetric_separable[OF assms(1)] submetric_complete_iff[OF assms(1)]
  by(simp add: polish_metric_set_def assms(2))

lemma polish_metric_setI:
  assumes "complete_metric_set S d" "separable (metric_set.mtopology S d)"
  shows "polish_metric_set S d"
  using assms by(auto intro!: separable_metric_setI simp: polish_metric_set_def complete_metric_set_def)

subsubsection ‹ Compact Metric Spaces›
locale compact_metric_set = metric_set +
  assumes mtopology_compact:"compact_space mtopology"
begin

context
  fixes S' :: "'b set" and dist'
  assumes S'_dist: "metric_set S' dist'"
begin

interpretation m': metric_set S' dist' by fact

lemma continuous_map_is_uniform:
  assumes "continuous_map mtopology m'.mtopology f"
  shows "uniform_continuous_map S dist S' dist' f"
  unfolding uniform_continuous_map_def[OF metric_set_axioms m'.metric_set_axioms]
proof safe
  show goal1:"x. x  S  f x  S'"
    using assms by(auto simp: continuous_map_def mtopology_topspace m'.mtopology_topspace)
  fix e :: real
  assume e:"0 < e"
  { fix x
    assume x:"x  S"
    then have "δ>0. yS. dist x y < δ  dist' (f x) (f y) < e / 2"
      using assms(1)[simplified metric_set_continuous_map_eq[OF metric_set_axioms m'.metric_set_axioms]] half_gt_zero[OF e]
      by metis
  }
  then obtain δ where delta:"x. x  S  δ x > 0" "x y. x  S  y  S  dist x y < δ x  dist' (f x) (f y) < e / 2"
    by metis
  show "δ>0. xS. yS. dist x y < δ  dist' (f x) (f y) < e"
  proof(cases "S = {}")
    case True
    then show ?thesis
      by (auto intro!: exI[where x=1])
  next
    case nem:False
    have ". finite     {open_ball x (δ x / 2)|x. x  S}  S   "
      using open_ball_ina[OF _ half_gt_zero[OF delta(1)]] mtopology_compact
      by(auto intro!: compactinD simp: compact_space_def mtopology_topspace openin_open_ball)
    then obtain F where F: "finite F" "F  {open_ball x (δ x / 2)|x. x  S}" "S   F"
      by auto
    have F_nem:"F  {}"
      using nem F by auto
    have "a  F  (xS. a = open_ball x (δ x / 2))" for a
      using F(2) by auto
    then obtain xa where xa:"a. a  F  xa a  S" "a. a  F  a = open_ball (xa a) (δ (xa a) / 2)"
      by metis
    define δ' where "δ'  (MIN aF. δ (xa a) / 2)"
    have fin:"finite ((λa. δ (xa a)/ 2) ` F)"
      using F by auto
    have nemd: "((λa. δ (xa a)/ 2) ` F)  {}"
      using F_nem by auto
    have d_pos: "δ' > 0"
      by(auto simp: δ'_def linorder_class.Min_gr_iff[OF fin nemd] intro!: delta(1) xa)
    show ?thesis
    proof(safe intro!: exI[where x=δ'])
      fix x y
      assume h:"x  S" "y  S" "dist x y < δ'"
      then obtain a where a:"x  a" "a  F"
        using F(3) by auto
      have "dist (xa a) y  dist (xa a) x + dist x y"
        by(auto intro!: dist_tr xa a simp: h)
      also have "... < δ' + δ (xa a) / 2"
        using h xa(2)[OF a(2)] a(1) open_ballD[of x "xa a"] by fastforce
      also have "...  δ (xa a) / 2 + δ (xa a) / 2"
      proof -
        have "δ'  δ (xa a) / 2"
          by(simp only: δ'_def,rule Min.coboundedI[OF fin]) (use a in auto)
        thus ?thesis by simp
      qed
      finally have 2:"dist (xa a) y < δ (xa a)" by simp
      have "dist' (f x) (f y)  dist' (f x) (f (xa a)) + dist' (f (xa a)) (f y)"
        by(auto intro!: m'.dist_tr goal1 h xa a)
      also have "... < e"
      proof -
        have [simp]:"dist (xa a) x < δ (xa a)"
          using a(1) xa[OF a(2)] delta(1) open_ballD by fastforce
        have "dist' (f x) (f (xa a)) < e / 2"
          by(simp only: m'.dist_sym[where x="f x"],rule delta(2)) (auto intro!: xa a h)
        moreover have "dist' (f (xa a)) (f y) < e / 2"
          by(rule delta(2)[OF _ _ 2]) (auto intro!: h xa a)
        ultimately show ?thesis by simp
      qed
      finally show "dist' (f x) (f y) < e" .
    qed(rule d_pos)
  qed
qed

end


lemma totally_bounded: totally_boundedS
  unfolding totally_boundedS_def
proof safe
  fix ε :: real
  assume "0 < ε"
  define 𝒰 where "𝒰  (λa. open_ball a ε) ` S"
  have 1: "U. U  𝒰  openin mtopology U"
    by(auto simp: 𝒰_def openin_open_ball)
  have 2:" 𝒰 = S"
    using open_ball_ina[OF _ 0 < ε] open_ball_subset_ofS
    by(auto simp: 𝒰_def)
  obtain  where "  𝒰" "finite " "  = S"
    using 1 2 compact_space[of mtopology,simplified mtopology_compact mtopology_topspace] by metis 
  then obtain A where "A  S" "finite A" " ((λa. open_ball a ε) ` A) = S"
    by(simp add: 𝒰_def) (metis finite_subset_image)
  thus "A. eps_net ε A"
    by(auto intro!: exI[where x=A] simp: eps_net_def 0 < ε)
qed

lemma sequentially_compact: sequentially_compact
  unfolding sequentially_compact_def
proof safe
  fix xn
  assume "xn  sequence"
  then have xn:"n. xn n  S" by auto
  have "¬ (xS. e>0. finite {n. xn n  open_ball x e})"
  proof
    assume contr:"xS. e>0. finite {n. xn n  open_ball x e}"
    then obtain e where e: "x. x  S  e x > 0" "x. x  S  finite {n. xn n  open_ball x (e x)}"
      by metis
    define U where "U  {open_ball x (e x)|x. x  S}"
    have "u. u  U  openin mtopology u" "topspace mtopology  U"
      by(auto simp: U_def openin_open_ball mtopology_topspace open_ball_ina[OF _ e(1)])
    then obtain F where F: "finite F" "F  U" "S   F"
      using mtopology_compact compactinD by (metis compact_space_def mtopology_topspace)
    then have "finite (fF. {n. xn n  f})"
      using e(2) by(auto simp: U_def)
    moreover have "UNIV = (fF. {n. xn n  f})"
      using F(3) xn by auto
    ultimately show False by simp
  qed
  then obtain x where x:"x  S" "e. e > 0  infinite {n. xn n  open_ball x e}"
    by metis
  have inf:"infinite {n. n > m  xn n  open_ball x e}" if "e > 0" for e m
  proof
    assume "finite {n. m < n  xn n  open_ball x e}"
    then have "finite ({..m}  {n. m < n  xn n  open_ball x e})"
      by auto
    moreover have "{n. xn n  open_ball x e}  {..m}  {n. m < n  xn n  open_ball x e}"
      by auto
    ultimately show False
      using x(2)[OF that] finite_subset by blast
  qed
  define a where "a  rec_nat (SOME n. xn n  open_ball x 1) (λn an. SOME m. m > an  xn m  open_ball x (1 / Suc n))"
  have an: "xn (a n)  open_ball x (1 / n)" if "n > 0" for n
  proof(cases n)
    case 0
    with that show ?thesis by simp
  next
    case (Suc n)
    have [simp]:"a (Suc n) = (SOME m. m > a n  xn m  open_ball x (1 / Suc n))"
      by(auto simp: a_def)
    obtain m where m:"a n < m" "xn m  open_ball x (1 / (Suc n))"
      using inf[of "1 / (real (Suc n))" "a n"] not_finite_existsD by auto
    have "a (Suc n) > a n  xn (a (Suc n))  open_ball x (1 / (Suc n))"
      by(simp,rule someI2[of _ m]) (use m in auto)
    then show ?thesis
      by(simp only: Suc)
  qed
  have as:"strict_mono a"
    unfolding strict_mono_Suc_iff
  proof safe
    fix n
    have [simp]:"a (Suc n) = (SOME m. m > a n  xn m  open_ball x (1 / Suc n))"
      by(auto simp: a_def)
    obtain m where m:"a n < m" "xn m  open_ball x (1 / (Suc n))"
      using inf[of "1 / (real (Suc n))" "a n"] not_finite_existsD by auto
    have "a (Suc n) > a n  xn (a (Suc n))  open_ball x (1 / (Suc n))"
      by(simp,rule someI2[of _ m]) (use m in auto)
    thus "a n < a (Suc n)" by simp
  qed
  show "a. strict_mono a  convergent_inS (xn  a)"
    unfolding convergent_inS_def converge_to_inS_def2'
  proof(safe intro!: exI[where x=a] exI[where x=x])
    fix e :: real
    assume "0 < e"
    then obtain N ::nat where N: "N > 0" "1 / N < e"
      by (meson nat_approx_posE zero_less_Suc)
    show "N. nN. (xn  a) n  open_ball x e"
    proof(safe intro!: exI[where x=N])
      fix n
      assume n:"n  N"
      show "(xn  a) n  open_ball x e"
        using order.trans[OF open_ball_le[of "1 / n"] open_ball_le[of "1 / N" e]] N n an[of n] inverse_of_nat_le
        by auto
    qed
  qed(auto simp: simp: as  x xn)
qed

lemma polish: "polish_metric_set S dist"
  using separable_if_totally_bounded[OF totally_bounded]
  by(simp add: polish_metric_set_def complete_metric_set_def complete_metric_set_axioms_def separable_metric_set_def)
    (meson Cauchy_inS_def converge_if_Cauchy_and_subconverge convergent_inS_def sequentially_compact sequentially_compact_def)

sublocale polish_metric_set
  by(rule polish)

end

lemma(in metric_set) ex_lebesgue_number:
  assumes "S  {}" sequentially_compact "u. u  U  openin mtopology u" "S   U"
  shows "d>0. aS. diam a < ennreal d  (uU. a  u)"
proof(rule ccontr)
  assume "¬ (d>0. aS. diam a < ennreal d  (uU. a  u))"
  then have "n. aS. diam a < ennreal (1 / Suc n)  (xU. ¬ a  x)" by auto
  then obtain An where an: "n. An n  S" "n. diam (An n) < ennreal (1 / Suc n)" "n u. u  U  ¬ (An n)  u"
    by metis
  have "An n  {}" for n
  proof
    assume "An n = {}"
    then have "U = {}  (uU. u = {})"
      using an(3)[of _ n] by auto
    thus False
      using assms(1,4) by blast
  qed
  then obtain xn where xn:"n. xn n  An n"
    by (meson ex_in_conv)
  then have xn':"n. xn n  S" using an by auto
  then obtain a x where ax:"strict_mono a" "converge_to_inS (xn  a) x"
    using assms(2) by(fastforce simp: sequentially_compact_def convergent_inS_def)
  then have x: "x  S" by(auto simp: converge_to_inS_def)
  then obtain u where u:"x  u" "u  U"
    using assms(4) by auto
  obtain e where e:"e > 0" "open_ball x e  u"
    using assms(3)[OF u(2)] u(1) mtopology_openin_iff by fastforce
  obtain n ::nat where n: "1 / Suc n < e / 2"
    using e(1) half_gt_zero nat_approx_posE by blast
  obtain n' where n':"n. n  n'  xn (a n)  open_ball x (e / 2)"
    using e(1) ax(2) by(auto simp: converge_to_inS_def2') (meson half_gt_zero)
  define n0 where "n0  max (a (Suc n)) (a n')"
  have n0:"1 / Suc n0 < e / 2" "xn n0  open_ball x (e / 2)"
  proof -
    have "Suc n0  Suc n"
      using seq_suble[OF ax(1),of "Suc n"]  by (simp add: n0_def)
    hence "1 / Suc n0  1 / Suc n"
      using inverse_of_nat_le by blast
    thus "1 / Suc n0 < e / 2"
      using n by auto
    show "xn n0  open_ball x (e / 2)"
      by (cases "a (Suc n)  a n'") (auto intro!: n' simp: n0_def ax(1) strict_mono_less_eq)
  qed
  have "An n0  open_ball x e"
    unfolding open_ball_def
  proof safe
    fix y
    assume y:"y  An n0"
    have "dist x y  dist x (xn n0) + dist (xn n0) y"
      using y xn' an by(auto intro!: dist_tr simp: x)
    also have "... < e / 2 + dist (xn n0) y"
      using open_ballD[OF n0(2)] by auto
    also have "...  e / 2 + 1 / Suc n0"
      using xn[of n0] xn' y an by(auto intro!: diam_is_sup'[OF _ _ order.strict_implies_order[OF an(2)[of n0]],simplified])
    also have "... < e"
      using n0(1) by auto
    finally show "y  (if x  S then {xa  S. dist x xa < e} else {})"
      using an(1) x y by auto
  qed
  hence "An n0  u"
    using e by auto
  with an(3)[OF u(2)] show False by auto
qed

lemma(in metric_set) sequentially_compact_iff1:
  "sequentially_compact  totally_boundedS  complete_metric_set S dist"
proof safe
  assume h:sequentially_compact
  then show totally_boundedS
    using Cauchy_if_convergent_inS by(fastforce simp: totally_boundedS_iff sequentially_compact_def)
  show "complete_metric_set S dist"
  proof
    fix xn
    assume 1:"Cauchy_inS xn"
    with h obtain a x where 2:"strict_mono a" "converge_to_inS (xn  a) x"
      by(fastforce dest: Cauchy_inS_dest1 simp: sequentially_compact_def convergent_inS_def)
    thus "convergent_inS xn"
      by(auto simp: convergent_inS_def converge_if_Cauchy_and_subconverge[OF 2 1] intro!: exI[where x=x])
  qed
next
  assume h:"totally_boundedS" "complete_metric_set S dist"
  show sequentially_compact
    unfolding sequentially_compact_def
  proof safe
    fix xn
    assume "xn  sequence"
    then obtain a where a:"strict_mono a" "Cauchy_inS (xn  a)"
      using h by(auto simp: totally_boundedS_iff) 
    thus "a. strict_mono a  convergent_inS (xn  a)"
      using h by(auto intro!: exI[where x=a] simp: complete_metric_set_def complete_metric_set_axioms_def)
  qed
qed

lemma(in metric_set) sequentially_compact_compact:
  assumes sequentially_compact
  shows "compact_metric_set S dist"
proof
  show "compact_space mtopology"
  proof(cases "S = {}")
    case True
    have [simp]:"topspace mtopology = {}"
      by(simp add: mtopology_topspace,fact)
    show ?thesis
      by(auto simp: compact_space intro!: exI[where x="{}"])
  next
    case 1:False
    {
      fix U
      assume h:"u. u  U  openin mtopology u" "S   U"
      obtain d where d:"d > 0" "a. a  S  diam a < ennreal d  uU. a  u"
        using ex_lebesgue_number[OF 1 assms h] by metis
      obtain B where B:"finite B" "B  S" "S = (aB. open_ball a (d / 3))"
        using totally_boundedSD[of "d / 3"] d(1) assms
        by(auto simp: sequentially_compact_iff1)
      have "uU. open_ball b (d / 3)  u" if "b  B" for b
        using open_ballD' d(1) by(auto intro!: d(2) order.strict_trans1[OF diam_ball_leq[of b "d / 3"]] simp: ennreal_less_iff)
      then obtain u where u:"b. b  B  u b  U" "b. b  B  open_ball b (d / 3)  u b"
        by metis
      have "F. finite F  F  U  S  ( F)"
        using B u by(fastforce intro!: exI[where x="u ` B"])
    }
    thus ?thesis
      by (simp add: compact_space_alt mtopology_topspace)
  qed
qed

corollary(in metric_set) compact_iff_sequentially_compact:
"compact_space mtopology  sequentially_compact"
  using compact_metric_set.sequentially_compact sequentially_compact_compact compact_metric_set_axioms_def compact_metric_set_def metric_set_axioms
  by blast

corollary(in metric_set) compact_iff2:
"compact_space mtopology  totally_boundedS  complete_metric_set S dist"
  by(simp add: compact_iff_sequentially_compact sequentially_compact_iff1)

corollary(in complete_metric_set) compactin_closed_iff:
  assumes "closedin mtopology C"
  shows "compactin mtopology C  totally_bounded_on C"
proof -
  from assms have C:"C  S"
    using mtopology_closedin_iff by blast
  then interpret C: complete_metric_set C "submetric C dist"
    by(auto simp: submetric_complete_iff assms)
  show ?thesis
    by(simp add: compactin_subspace submetric_subtopology[OF C] totally_bounded_on_submetric[OF C] mtopology_topspace C  C.compact_iff2 C.complete_metric_set_axioms)
qed

subsubsection ‹ Completion ›
context metric_set
begin

abbreviation "Cauchys  Collect Cauchy_inS"

definition Cauchy_r :: "((nat  'a) × (nat  'a)) set" where
"Cauchy_r  {(xn,yn)|xn yn. Cauchy_inS xn  Cauchy_inS yn  (λn. dist (xn n) (yn n))  0}"

lemma Cauchy_r_equiv[simp]: "equiv Cauchys Cauchy_r"
proof(rule equivI)
  show "refl_on Cauchys Cauchy_r"
    by(auto simp: refl_on_def Cauchy_r_def)
next
  show "sym Cauchy_r"
    using dist_sym by(auto simp: sym_def Cauchy_r_def)
next
  show "trans Cauchy_r"
  proof(rule transI)
    show "x y z. (x, y)  Cauchy_r  (y, z)  Cauchy_r  (x, z)  Cauchy_r"
      unfolding Cauchy_r_def
    proof safe
      fix xn yn zn
      assume h:"Cauchy_inS xn" "Cauchy_inS yn" "Cauchy_inS zn"
               "(λn. dist (xn n) (yn n))  0" "(λn. dist (yn n) (zn n))  0"
      then show "xn' yn'. (xn, zn) = (xn', yn')  Cauchy_inS xn'  Cauchy_inS yn'  (λn. dist (xn' n) (yn' n))  0"
        by(auto intro!: tendsto_0_le[OF tendsto_add_zero[OF h(4,5)],of _ 1] dist_tr eventuallyI simp: dist_geq0 Cauchy_inS_dest1)
    qed
  qed
qed

abbreviation S_completion :: "(nat  'a) set set" ("S*") where
"S_completion  Cauchys // Cauchy_r"

lemma S_c_represent:
  assumes "X  S*"
  obtains xn where "xn  X" "Cauchy_inS xn"
  using equiv_Eps_in[OF _ assms] equiv_Eps_preserves[OF _ assms] by auto

lemma Cauchy_inS_ignore_initial_eq:
  assumes "Cauchy_inS xn"
  shows "(xn, (λn. xn (n + k)))  Cauchy_r"
  by(auto simp: Cauchy_r_def Cauchy_inS_ignore_initial[OF assms] assms,insert assms)
    (auto simp: LIMSEQ_def dist_real_def dist_geq0 Cauchy_inS_def,metis add.commute trans_le_add2)

corollary Cauchy_inS_r: "a  S  (λn. a, λn. a)  Cauchy_r"
  by(auto intro!: Cauchy_inS_ignore_initial_eq Cauchy_inS_const)

abbreviation dist_completion' :: "[nat  'a, nat  'a]  real" where
"dist_completion' xn yn  lim (λn. dist (xn n) (yn n))"

lemma dist_of_completion_congruent2: "dist_completion' respects2 Cauchy_r"
proof(safe intro!: congruent2_commuteI[OF Cauchy_r_equiv])
  fix xn yn zn
  assume h:"(xn,yn)  Cauchy_r" "Cauchy_inS zn"
  then have h':"Cauchy_inS xn" "Cauchy_inS yn" "(λn. dist (xn n) (yn n))  0"
    by(auto simp: Cauchy_r_def)
  have 1:"(λn. dist (zn n) (xn n))  lim (λn. dist (zn n) (xn n))"
    using Cauchy_inS_dist_convergent[OF h(2) h'(1)] by(simp add: convergent_LIMSEQ_iff)
  have 2:"(λn. dist (zn n) (yn n))  lim (λn. dist (zn n) (xn n))"
    using h(2) h'(1,2) dist_tr_abs[of "zn _" "xn _" "yn _",simplified abs_diff_le_iff]
    by(auto intro!: real_tendsto_sandwich[OF _ _ tendsto_diff[OF 1 h'(3),simplified] tendsto_add[OF 1 h'(3),simplified]] eventuallyI dist_tr dest: Cauchy_inS_dest1) (simp add: Cauchy_inS_dest1 add.commute diff_le_eq)
  show "dist_completion' zn xn = dist_completion' zn yn"
    using 1 2 by(auto dest: limI)
qed(auto simp: dist_sym)

definition dist_completion :: "[(nat  'a) set, (nat  'a) set]  real" ("dist*") where
"dist* X Y  (if X  S*  Y  S* then dist_completion' (SOME xn. xn  X) (SOME yn. yn  Y) else 0)"

lemma dist_c_def:
  assumes "xn  X" "yn  Y" "X  S*" "Y  S*"
  shows "dist* X Y = dist_completion' xn yn"
  by(auto simp: assms dist_completion_def,rule someI2[of "λx. x  X",OF assms(1)],rule someI2[of "λx. x  Y",OF assms(2)])
    (auto simp: congruent2D[OF dist_of_completion_congruent2 quotient_eq_iff[OF _ assms(3,3,1),simplified] quotient_eq_iff[OF _ assms(4,4,2),simplified]])


lemma completion_metric_set: "metric_set S* dist*"
proof
  fix X Y
  consider "X  S*" "Y  S*" | "X  S*" | "Y  S*" by blast
  then show "0  dist* X Y"
  proof cases
    case 1
    then obtain xn yn where h: "xn  X" "yn  Y" "Cauchy_inS xn" "Cauchy_inS yn"
      by (meson S_c_represent)
    with 1 show ?thesis
      by(auto simp: dist_c_def intro!: Lim_bounded2[OF Cauchy_inS_dist_convergent[OF h(3,4),simplified convergent_LIMSEQ_iff]] dist_geq0)
  qed(auto simp: dist_completion_def)
next
  fix X Y
  show "dist* X Y = dist* Y X"
    by(auto simp: dist_completion_def dist_sym)
next
  fix X Y
  assume h:"X  S*" "Y  S*"
  then obtain xn yn where h': "xn  X" "yn  Y" "Cauchy_inS xn" "Cauchy_inS yn"
    by (meson S_c_represent)
  show "X = Y  dist* X Y = 0"
  proof
    assume "X = Y"
    then show "dist* X Y = 0"
      using h' h by(auto simp: dist_c_def)
  next
    assume "dist* X Y = 0"
    then have "(xn, yn)  Cauchy_r"
      using h h' convergent_LIMSEQ_iff[THEN iffD1,OF Cauchy_inS_dist_convergent[OF h'(3,4)]]
      by(auto simp: dist_c_def Cauchy_r_def)
    thus "X = Y"
      by(simp add: quotient_eq_iff[OF _ h h'(1,2)])
  qed
next
  fix X Y Z
  assume h:"X  S*" "Y  S*" "Z  S*"
  then obtain xn yn zn where h': "xn  X" "yn  Y" "zn  Z" "Cauchy_inS xn" "Cauchy_inS yn" "Cauchy_inS zn"
    by (meson S_c_represent)
  have "dist* X Z = dist_completion' xn zn"
    using h h' by(simp add: dist_c_def)
  also have "...  lim (λn. dist (xn n) (yn n) + dist (yn n) (zn n))"
    using h' by(auto intro!: lim_mono[OF _  convergent_LIMSEQ_iff[THEN iffD1,OF Cauchy_inS_dist_convergent[OF h'(4,6)]] convergent_LIMSEQ_iff[THEN iffD1,OF convergent_add[OF Cauchy_inS_dist_convergent[OF h'(4,5)] Cauchy_inS_dist_convergent[OF h'(5,6)]]]] dist_tr dest: Cauchy_inS_dest1)
  also have "... = dist_completion' xn yn + dist_completion' yn zn"
    using tendsto_add[OF convergent_LIMSEQ_iff[THEN iffD1,OF Cauchy_inS_dist_convergent[OF h'(4,5)]] convergent_LIMSEQ_iff[THEN iffD1,OF Cauchy_inS_dist_convergent[OF h'(5,6)]]]
    by(simp add: limI)
  also have "... = dist* X Y + dist* Y Z"
    using h h' by(simp add: dist_c_def)
  finally show "dist* X Z  dist* X Y + dist* Y Z" .
qed(simp add: dist_completion_def)

interpretation c:metric_set "S*" "dist*"
  by(rule completion_metric_set)

definition into_S_c :: "'a  (nat  'a) set" where
"into_S_c a  Cauchy_r `` {(λn. a)}"

lemma into_S_c_in:
  assumes "a  S"
  shows "(λn. a)  into_S_c a"
  using Cauchy_inS_const[OF assms] Cauchy_inS_r[OF assms]
  by(auto simp: into_S_c_def)

lemma into_S_c_into:
  assumes "a  S"
  shows "into_S_c a  S*"
  by(auto simp: into_S_c_def intro!: quotientI Cauchy_if_convergent_inS convergent_inS_const assms)

lemma into_S_inj: "inj_on into_S_c S"
proof
  fix x y
  assume "x  S" "y  S" "into_S_c x = into_S_c y"
  with eq_equiv_class_iff[THEN iffD1,OF Cauchy_r_equiv _ _ this(3)[simplified into_S_c_def]]
  have "(λn. x, λn. y)  Cauchy_r"
    by(auto simp: Cauchy_if_convergent_inS convergent_inS_const)
  thus "x = y"
    using dist_0[OF x  S y  S]
    by(auto simp: Cauchy_r_def LIMSEQ_const_iff)
qed

lemma dist_into_S_c:
  assumes "x  S" "y  S"
  shows "dist* (into_S_c x) (into_S_c y) = dist x y"
  using into_S_c_in[OF assms(1)] into_S_c_in[OF assms(2)] into_S_c_into[OF assms(1)] into_S_c_into[OF assms(2)]
  by(simp add: dist_c_def)

lemma S_c_isometry:
 "c.ed into_S_c S = dist"
  by standard+ (auto simp: c.embed_dist_on_def dist_into_S_c dist_notin dist_notin')

corollary mtopology_embedding_S_c_map:
 "homeomorphic_map mtopology (subtopology c.mtopology (into_S_c ` S)) into_S_c"
  using into_S_c_into by(auto intro!: c.embed_dist_topology_homeomorphic_map[OF _ into_S_inj,simplified S_c_isometry])

corollary mtopology_embedding_S_c:
 "mtopology homeomorphic_space subtopology c.mtopology (into_S_c ` S)"
  using mtopology_embedding_S_c_map homeomorphic_space by blast

lemma into_S_c_image_dense: "c.dense_set (into_S_c ` S)"
  unfolding c.dense_set_def2'
proof safe
  fix X
  assume X:"X  S*"
  from S_c_represent[OF this] obtain xn where xn:"xn  X" "Cauchy_inS xn"
    by auto
  show "fUNIV  into_S_c ` S. c.converge_to_inS f X"
  proof(safe intro!: bexI[where x="λn. into_S_c (xn n)"])
    show "c.converge_to_inS (λn. into_S_c (xn n)) X"
      unfolding c.converge_to_inS_def2
    proof safe
      fix e :: real
      assume e:"e > 0"
      then obtain N where N:"n m. n  N  m  N  dist (xn n) (xn m) < e / 2"
        using xn(2) by (meson Cauchy_inS_def half_gt_zero)
      show "N. nN. dist* (into_S_c (xn n)) X < e"
      proof(safe intro!: exI[where x=N])
        fix n
        assume n:"N  n"
        have "dist* (into_S_c (xn n)) X = dist_completion' (λna. xn n) xn"
          by(rule dist_c_def[OF into_S_c_in[OF Cauchy_inS_dest1[OF xn(2),of n]] xn(1) into_S_c_into[OF Cauchy_inS_dest1[OF xn(2),of n]] X])
        also have "...  e / 2"
          by(rule Lim_bounded[OF Cauchy_inS_dist_convergent[OF Cauchy_inS_const[OF  Cauchy_inS_dest1[OF xn(2),of n]] xn(2),simplified convergent_LIMSEQ_iff],of N "e/2"],auto dest: N[OF n])
        also have "... < e"
          using e by auto
        finally show "dist* (into_S_c (xn n)) X < e" .
      qed
    qed(auto simp: Cauchy_inS_dest1[OF xn(2)] into_S_c_into X)
  qed(auto simp: Cauchy_inS_dest1[OF xn(2)] into_S_c_into)
qed (use into_S_c_into in auto)

lemma completion_complete:"complete_metric_set S* dist*"
proof
  fix Xn
  assume h:"c.Cauchy_inS Xn"
  have "n. xnS. dist* (Xn n) (into_S_c xn) < 1 / (Suc n)"
    using into_S_c_image_dense c.Cauchy_inS_dest1[OF h]
    by(auto simp: c.dense_set_def2)
  then obtain xn where xn: "n. xn n  S" "n.  dist* (Xn n) (into_S_c (xn n)) < 1 / (Suc n)"
    by metis
  have xnC:"Cauchy_inS xn"
    unfolding Cauchy_inS_def
  proof safe
    fix e :: real
    assume e:"0 < e"
    then obtain N1 where N1: "1 / Suc N1 < e / 3"
      by (meson nat_approx_posE zero_less_divide_iff zero_less_numeral)
    obtain N2 where N2: "n m. n  N2  m  N2  dist* (Xn n) (Xn m) < e / 3"
      using e h by(simp only: c.Cauchy_inS_def) (meson zero_less_divide_iff zero_less_numeral)
    show "N. nN. mN. dist (xn n) (xn m) < e"
    proof(safe intro!: exI[where x="max N1 N2"])
      fix n m
      assume "max N1 N2  n" "max N1 N2  m"
      hence n: "N1  n" "N2  n"
        and m: "N1  m" "N2  m" by auto
      have "dist (xn n) (xn m) = c.ed into_S_c S (xn n) (xn m)"
        by(simp add: S_c_isometry)
      also have "... = dist* (into_S_c (xn n)) (into_S_c (xn m))"
        using xn by(simp add: c.embed_dist_on_def)
      also have "...  dist* (into_S_c (xn n)) (Xn n) + dist* (Xn n) (Xn m) + dist* (Xn m) (into_S_c (xn m))"
        using c.dist_tr[OF into_S_c_into[OF xn(1)[of n]] c.Cauchy_inS_dest1[OF h,of m] into_S_c_into[OF xn(1)[of m]]] c.dist_tr[OF into_S_c_into[OF xn(1)[of n]] c.Cauchy_inS_dest1[OF h,of n] c.Cauchy_inS_dest1[OF h,of m]]
        by simp
      also have "... < 1 / Suc n + e / 3 + 1 / Suc m"
        using N2[OF n(2) m(2)] xn(2)[of m] xn(2)[of n,simplified c.dist_sym[of "Xn n"]] by auto
      also have "... < e"
      proof -
        have "1 / Suc n  1 / Suc N1" "1 / Suc m  1 / Suc N1"
          using n m inverse_of_nat_le by blast+
        thus ?thesis
          using N1 by linarith
      qed
      finally show "dist (xn n) (xn m) < e" .
    qed
  qed(simp add: xn)
  show "c.convergent_inS Xn"
    unfolding c.convergent_inS_def c.converge_to_inS_def2
  proof(safe intro!:  exI[where x="Cauchy_r `` {xn}"] quotientI xnC)
    fix e :: real
    assume e:"0 < e"
    then obtain N1 where N1: "1 / Suc N1 < e / 2"
      by (meson nat_approx_posE zero_less_divide_iff zero_less_numeral)
    hence 1:"dist* (Xn n) (into_S_c (xn n)) < e / 2" if "n  N1" for n
    proof -
      have "1 / Suc n  1 / Suc N1"
        using that inverse_of_nat_le by blast
      thus ?thesis
        using xn(2)[of n] N1 by linarith
    qed
    then obtain N2 where N2:"n m. n  N2  m  N2  dist (xn n) (xn m) < e / 3"
      using xnC e by (meson Cauchy_inS_def zero_less_divide_iff zero_less_numeral) 
    have 2:"dist* (into_S_c (xn n)) (Cauchy_r `` {xn}) < e / 2" if "n  N2" for n
    proof -
      have "dist* (into_S_c (xn n)) (Cauchy_r `` {xn}) = dist_completion' (λm. xn n) xn"
        using dist_c_def[OF into_S_c_in[OF Cauchy_inS_dest1[OF xnC,of n]] equiv_class_self[OF Cauchy_r_equiv,of xn] into_S_c_into[OF Cauchy_inS_dest1[OF xnC,of n]]] xnC
        by (simp add: quotientI)
      also have "...  e / 3"
        by(rule Lim_bounded[OF Cauchy_inS_dist_convergent[OF Cauchy_inS_const[OF  Cauchy_inS_dest1[OF xnC,of n]] xnC,simplified convergent_LIMSEQ_iff],of N2 "e/3"], auto dest: N2[OF that])
      also have "... < e / 2" using e by simp
      finally show "dist* (into_S_c (xn n)) (Cauchy_r `` {xn}) < e / 2" .
    qed
    show "N. nN. dist* (Xn n) (Cauchy_r `` {xn}) < e"
    proof(safe intro!: exI[where x="max N1 N2"])
      fix n
      assume "max N1 N2  n"
      then have n:"n  N1" "n  N2" by auto
      show "dist* (Xn n) (Cauchy_r `` {xn}) < e"
        using c.dist_tr[OF c.Cauchy_inS_dest1[OF h,of n] into_S_c_into[OF Cauchy_inS_dest1[OF xnC],of n] quotientI[of xn]] xnC 1[OF n(1)] 2[OF n(2)]
        by auto
    qed
  qed(use c.Cauchy_inS_dest1[OF h] in auto)
qed

lemma dense_set_c_dense:
  assumes "dense_set U"
  shows "c.dense_set (into_S_c ` U)"
  unfolding c.dense_set_def2
proof safe
  fix X and e :: real
  assume h:"X  S*" "0 < e"
  then obtain xn where xn:"xn  X" "Cauchy_inS xn"
    by(auto dest: S_c_represent)
  obtain y where y:"y  S" "dist* X (into_S_c y) < e / 2"
    using h into_S_c_image_dense half_gt_zero[OF h(2)] by(simp only: c.dense_set_def2) blast
  obtain z where z:"z  U" "dist y z < e / 2"
    using half_gt_zero[OF h(2)] y(1) assms by(simp only: dense_set_def2) blast
  show "yinto_S_c ` U. dist* X y < e"
  proof(rule bexI[OF _ imageI[OF z(1)]])
    have "dist* X (into_S_c z)  dist* X (into_S_c y) + dist* (into_S_c y) (into_S_c z)"
      using z(1) assms by(auto intro!: c.dist_tr h into_S_c_into y simp: dense_set_def)
    also have "... =  dist* X (into_S_c y) + dist y z"
      using z(1) assms y(1) dist_into_S_c[of y z] by(auto simp: dense_set_def)
    also have "... < e"
      using y(2) z(2) by simp
    finally show "dist* X (into_S_c z) < e" .
  qed
qed(insert assms, auto simp: dense_set_def intro!: into_S_c_into)

end

lemma(in separable_metric_set) completion_polish: "polish_metric_set S* dist*"
proof -
  interpret c:complete_metric_set "S*" "dist*"
    by(rule completion_complete)
  show ?thesis
  proof
    obtain U where U: "countable U" "dense_set U"
      using separable by blast
    show "U. countable U  c.dense_set U"
      using U by(auto intro!: exI[where x="into_S_c ` U"] dense_set_c_dense)
  qed
qed

subsection  ‹Discrete Distance›
definition discrete_dist :: "'a set  'a  'a  real" where
"discrete_dist S  (λa b. if a  S  b  S  a  b then 1 else 0)"

lemma
  assumes "a  S" and "b  S"
  shows discrete_dist_iff_1: "discrete_dist S a b = 1  a  b"
    and discrete_dist_iff_0: "discrete_dist S a b = 0  a = b"
  using assms by(auto simp: discrete_dist_def)

lemma discrete_dist_metric:
 "metric_set S (discrete_dist S)"
  by(auto simp: discrete_dist_def metric_set_def)

lemma
 shows discrete_dist_ball_ge1: "x  S  1 < ε  metric_set.open_ball S (discrete_dist S) x ε = S"
 and discrete_dist_ball_leq1: "x  S  0 < ε  ε  1  metric_set.open_ball S (discrete_dist S) x ε = {x}"
   apply(auto simp: metric_set.open_ball_def[OF discrete_dist_metric],simp_all add: discrete_dist_def)
  using less_le_not_le by fastforce
  

lemma discrete_dist_complete_metric:
 "complete_metric_set S (discrete_dist S)"
proof -
  interpret m: metric_set S "discrete_dist S"
    by(rule discrete_dist_metric)
  show ?thesis
  proof
    fix f
    assume h:"m.Cauchy_inS f"
    then have "ε. ε>0  xS. N. nN. f n  m.open_ball x ε"
      by(auto simp: m.Cauchy_inS_def2')
    from this[of 1] obtain x N where hxn:
     "x  S" "nN. f n  m.open_ball x 1"
      by auto
    hence "n. n  N  f n = x"
      using discrete_dist_ball_leq1[of x S 1] by auto
    thus "m.convergent_inS f"
      unfolding m.convergent_inS_def using h hxn(1)
      by(auto intro!: bexI[where x=x] exI[where x=N] simp:m.converge_to_inS_def2' m.Cauchy_inS_def)
  qed
qed

lemma discrete_dist_dense_set:
 "metric_set.dense_set S (discrete_dist S) U  S = U"
proof -
  interpret m: metric_set S "discrete_dist S"
    by(rule discrete_dist_metric)
  show ?thesis
  proof
    assume h:"m.dense_set U"
    show "S = U"
    proof safe
      fix x
      assume hx:"x  S"
      then have "ε. ε>0  m.open_ball x ε  U  {}"
        using h by(simp add: m.dense_set_def)
      hence "m.open_ball x 1  U  {}" by auto
      thus "x  U"
        using discrete_dist_ball_leq1[OF hx,of 1]
        by auto
    next
      show "x. x  U  x  S"
        using h by(auto simp: m.dense_set_def)
    qed
  next
    show "S = U  m.dense_set U "
      using m.dense_set_S by auto
  qed
qed

lemma discrete_dist_separable_iff:
 "separable_metric_set S (discrete_dist S)  countable S"
proof -
  interpret m: metric_set S "discrete_dist S"
    by(rule discrete_dist_metric)
  show ?thesis
  proof
    assume "separable_metric_set S (discrete_dist S)"
    then obtain U where "countable U" "m.dense_set U"
      by(auto simp: separable_metric_set_def separable_metric_set_axioms_def)
    thus "countable S"
      using discrete_dist_dense_set[of S] by auto
  next
    assume "countable S"
    then show "separable_metric_set S (discrete_dist S)"
      by(auto simp: separable_metric_set_def separable_metric_set_axioms_def intro!:exI[where x=S] m.dense_set_S discrete_dist_metric)
  qed
qed

lemma discrete_dist_polish_iff: "polish_metric_set S (discrete_dist S)  countable S"
  using discrete_dist_separable_iff[of S] discrete_dist_complete_metric[of S]
  by(auto simp: polish_metric_set_def)


lemma discrete_dist_topology_x:
  assumes "x  S"
  shows "openin (metric_set.mtopology S (discrete_dist S)) {x}"
proof -
  interpret m: metric_set S "discrete_dist S"
    by(rule discrete_dist_metric)
  show ?thesis
    by(auto simp: m.mtopology_open_ball_in[OF assms,of 1, simplified discrete_dist_ball_leq1[OF assms]])
qed

lemma discrete_dist_topology:
 "openin (metric_set.mtopology S (discrete_dist S)) U  U  S"
proof -
  interpret m: metric_set S "discrete_dist S"
    by(rule discrete_dist_metric)
  show ?thesis
  proof
    show "openin m.mtopology U  U  S"
      using m.mtopology_topspace
      by(auto simp: topspace_def)
  next
    assume "U  S"
    then have "x. x  U  openin m.mtopology {x}"
      by(auto simp: discrete_dist_topology_x)
    hence "openin m.mtopology ({{x} | x. x  U})"
      by auto
    moreover have "{{x} | x. x  U} = U" by blast
    ultimately show "openin m.mtopology U"
      by simp
  qed
qed

lemma discrete_dist_topology':
 "metric_set.mtopology S (discrete_dist S) = discrete_topology S"
  by (simp add: discrete_dist_topology topology_eq)

text ‹ Empty space. ›
lemma empty_metric_compact: "compact_metric_set {} (λx y. 0)"
proof -
  interpret metric_set "{}" "λx y. 0"
    by(auto simp: metric_set_def)
  show ?thesis
    by standard (use Hausdorff_space_finite_topspace[OF mtopology_Hausdorff,simplified mtopology_topspace] in blast)
qed

corollary
  shows empty_metric_polish: "polish_metric_set {} (λx y. 0)"
    and empty_metric_complete: "complete_metric_set {} (λx y. 0)"
    and empty_metric_separable: "separable_metric_set {} (λx y. 0)"
    and empty_metric: "metric_set {} (λx y. 0)"
proof -
  interpret compact_metric_set "{}" "λx y. 0"
    by(rule empty_metric_compact)
  show "polish_metric_set {} (λx y. 0)" "complete_metric_set {} (λx y. 0)"
       "separable_metric_set {} (λx y. 0)" "metric_set {} (λx y. 0)"
    using polish_metric_set_axioms complete_metric_set_axioms separable_metric_set_axioms metric_set_axioms
    by blast+
qed

lemma empty_metric_unique:
  assumes "metric_set {} d"
  shows "d = (λx y. 0)"
  apply standard+
  using assms by(auto simp: metric_set_def)

lemma empty_metric_mtopology:
 "metric_set.mtopology {} (λx y. 0) = discrete_topology {}"
proof -
  have 1:"(λU. U = {}  (xU. ε>0. metric_set.open_ball {} (λx y. 0) x ε  U)) = (λU. U = {})"
    by standard auto
  thus ?thesis
    using metric_set.mtopology_def[of "{}" "λx y. 0"]
    by(simp add:  metric_set_def discrete_topology_def 1)
qed

text ‹ Singleton space ›
lemma singleton_metric_compact:
 "compact_metric_set {a} (λx y. 0)"
proof -
  interpret metric_set "{a}" "λx y. 0"
    by(auto simp: metric_set_def)
  show ?thesis
    by standard (use Hausdorff_space_finite_topspace[OF mtopology_Hausdorff,simplified mtopology_topspace] in blast)
qed

corollary
  shows singleton_metric_polish: "polish_metric_set {a} (λx y. 0)"
    and singleton_metric_complete: "complete_metric_set {a} (λx y. 0)"
    and singleton_metric_separable: "separable_metric_set {a} (λx y. 0)"
    and singleton_metric: "metric_set {a} (λx y. 0)"
proof -
  interpret compact_metric_set "{a}" "λx y. 0"
    by(rule singleton_metric_compact)
  show "polish_metric_set {a} (λx y. 0)" "complete_metric_set {a} (λx y. 0)"
       "separable_metric_set {a} (λx y. 0)" "metric_set {a} (λx y. 0)"
    using polish_metric_set_axioms complete_metric_set_axioms separable_metric_set_axioms metric_set_axioms
    by blast+
qed

lemma singleton_metric_unique:
  assumes "metric_set {a} d"
  shows "d = (λx y. 0)"
  by standard+ (insert assms,auto simp: metric_set_def, metis)

lemma singleton_metric_mtopology:
 "metric_set.mtopology {a} (λx y. 0) = discrete_topology {a}"
proof -
  have "(λU. U  {a}  (xU. ε>0. metric_set.open_ball {a} (λx y. 0) x ε  U)) = (λU. U  {a})"
  proof
    fix U
    have "(U  {a}  (xU. ε>0. metric_set.open_ball {a} (λx y. 0) x ε  U))" if "U  {a}"
    proof safe
      fix x
      assume "x  U"
      then have "x = a" using that by auto
      thus "ε>0. metric_set.open_ball {a} (λx y. 0) x ε  U"
        by(auto intro!: exI[where x=1]) (metis x  U complete_metric_set_def empty_iff metric_set.open_ballD'(1) polish_metric_set_def singleton_metric_polish subset_singletonD that)
    qed(use that in auto)
    thus "(U  {a}  (xU. ε>0. metric_set.open_ball {a} (λx y. 0) x ε  U)) = (U  {a})"
      by auto
  qed
  thus ?thesis
    using metric_set.mtopology_def[of "{a}" "λx y. 0"]
    by(simp add:  metric_set_def discrete_topology_def )
qed

subsection  ‹Binary Product Metric Spaces›
text ‹ We define the $L^{1}$-distance. $L^{1}$-distance and $L^{2}$ distance (Euclid distance)
       generate the same topological space.›

definition binary_distance :: "['a set, 'a  'a  real, 'b set, 'b  'b  real]  'a × 'b  'a × 'b  real" where
"binary_distance S d S' d'  (λ(x,x') (y,y'). if (x,x')  S × S'  (y,y')  S × S' then d x y + d' x' y' else 0)"


context
  fixes S S' d d'
  assumes "metric_set S d" "metric_set S' d'"
begin

interpretation m1: metric_set S d by fact
interpretation m2: metric_set S' d' by fact

lemma binary_metric_set:
 "metric_set (S × S') (binary_distance S d S' d')"
proof
  fix x y z
  assume "x  S × S'" "y  S × S'" "z  S × S'"
  then show "binary_distance S d S' d' x z  binary_distance S d S' d' x y + binary_distance S d S' d' y z"
    using m1.dist_tr[of "fst x" "fst y" "fst z"] m2.dist_tr[of "snd x" "snd y" "snd z"]
    by(fastforce simp: binary_distance_def split_beta')
next
  show "x y. 0  binary_distance S d S' d' x y"
       "x y. x  S × S'  binary_distance S d S' d' x y = 0"
    using m1.dist_geq0 m2.dist_geq0 m1.dist_notin m2.dist_notin by(auto simp: binary_distance_def split_beta')
next
  fix x y
  assume "x  S × S'" "y  S × S'"
  then show "(x = y) = (binary_distance S d S' d' x y = 0)"
    using m1.dist_0[of "fst x" "fst y"] m2.dist_0[of "snd x" "snd y"] m1.dist_geq0[of "fst x" "fst y"] m2.dist_geq0[of "snd x" "snd y"]
    by(auto simp: binary_distance_def split_beta)
next
  show "x y. binary_distance S d S' d' x y = binary_distance S d S' d' y x"
    using m1.dist_sym m2.dist_sym by(auto simp: binary_distance_def split_beta')
qed

interpretation m: metric_set "S × S'" "binary_distance S d S' d'"
  by (rule binary_metric_set)

lemma binary_distance_geq:
  assumes "x  S" "y  S" "x'  S'" "y'  S'"
  shows "d x y  binary_distance S d S' d' (x,x') (y,y')"
        "d' x' y'  binary_distance S d S' d' (x,x') (y,y')"
  using m1.dist_geq0 m2.dist_geq0 assms by(auto simp: binary_distance_def)


lemma binary_distance_ball:
  assumes "(x,x')  m.open_ball (a,a') ε"
    shows "x  m1.open_ball a ε"
      and "x'  m2.open_ball a' ε"
proof -
  have 1:"x  S" "x'  S'" "ε > 0" "a  S" "a'  S'"
    using m.open_ballD'[OF assms(1)] by auto
  thus "x  metric_set.open_ball S d a ε"
   and "x'  metric_set.open_ball S' d' a' ε"
    using m.open_ballD[OF assms(1)] binary_distance_geq[OF 1(4,1,5,2)] 1
    by(auto simp: m1.open_ball_def m2.open_ball_def)
qed

lemma binary_distance_ball':
  assumes "z  m.open_ball a ε"
    shows "fst z  m1.open_ball (fst a) ε"
      and "snd z  m2.open_ball (snd a) ε"
  using binary_distance_ball[of "fst z" "snd z" "fst a" "snd a" ε] assms by auto

lemma binary_distance_ball1':
  assumes "a  S" "ε > 0" "a' S'" "ε' > 0"
    shows "ε''>0. m.open_ball (a,a') ε''  m1.open_ball a ε × m2.open_ball a' ε'"
proof(rule exI[where x="min ε ε'"])
  show "0 < min ε ε'  m.open_ball (a, a') (min ε ε')  m1.open_ball a ε × m2.open_ball a' ε'"
  proof 
    show "0 < min ε ε'"
      using assms by auto
  next
    show "m.open_ball (a, a') (min ε ε')  m1.open_ball a ε × m2.open_ball a' ε'"
    proof safe
      fix x x'
      assume h:"(x,x')  m.open_ball (a, a') (min ε ε')"
      then have hx:"x  S" "x'  S'"
        using m.open_ballD'(1)[of "(x,x')" "(a, a')" "min ε ε'"] by auto
      hence "d a x + d' a' x' < min ε ε'"
        using h assms by(auto simp: m.open_ball_def,auto simp: binary_distance_def)
      thus "x  m1.open_ball a ε" "x'  m2.open_ball a' ε'"
        using m1.dist_geq0[of a x] m2.dist_geq0[of a' x'] assms hx
        by(auto simp: m1.open_ball_def m2.open_ball_def)
    qed
  qed
qed

lemma binary_distance_ball1:
  assumes "b  m1.open_ball a ε" "b'  m2.open_ball a' ε'"
    shows "ε''>0. m.open_ball (b,b') ε''  m1.open_ball a ε × m2.open_ball a' ε'"
proof -
  obtain εa εa' where he:
    "εa > 0" "εa' > 0" "m1.open_ball b εa  m1.open_ball a ε" "m2.open_ball b' εa'  m2.open_ball a' ε'"
    using m1.mtopology_open_ball_in'[OF assms(1)] m2.mtopology_open_ball_in'[OF assms(2)] by auto
  thus ?thesis
    using binary_distance_ball1'[OF m1.open_ballD'(1)[OF assms(1)] he(1) m2.open_ballD'(1)[OF assms(2)] he(2)]
    by blast
qed


lemma binary_distance_ball2':
  assumes "a  S" "ε'' > 0" "a' S'"
  shows "ε>0. ε'>0. m1.open_ball a ε × m2.open_ball a' ε'  m.open_ball (a,a') ε''"
proof(safe intro!: exI[where x="ε''/2"])
  fix x x'
  assume "x  m1.open_ball a (ε'' / 2)" "x'  m2.open_ball a' (ε'' / 2)"
  then have "x  S" "x'  S'" "d a x < ε'' / 2" "d' a' x' < ε'' / 2"
    using assms by(auto simp: m1.open_ball_def m2.open_ball_def)
  thus "(x,x')  m.open_ball (a, a') ε''"
    using assms by(auto simp: m.open_ball_def,auto simp: binary_distance_def)
qed (use assms in auto)

lemma binary_distance_ball2:
  assumes "(b,b')  m.open_ball (a,a') ε''"
    shows "ε>0. ε'>0. m1.open_ball b ε × m2.open_ball b' ε'  m.open_ball (a,a') ε''"
proof -
  obtain ε''' where "ε''' > 0" "m.open_ball (b,b') ε'''  m.open_ball (a,a') ε''"
    using m.mtopology_open_ball_in'[OF assms(1)] by blast
  thus ?thesis
    using binary_distance_ball2'[of b ε''' b'] m.open_ballD'[OF assms(1),simplified]
    by blast
qed

lemma binary_distance_mtopology:
  "m.mtopology = prod_topology m1.mtopology m2.mtopology"
proof -
  have "m.mtopology = topology_generated_by { m1.open_ball a ε × m2.open_ball a' ε' | a a' ε ε'. a  S  a'  S'  ε > 0  ε' > 0}"
    unfolding m.mtopology_def2
  proof(rule topology_generated_by_eq)
    fix U
    assume "U  {m1.open_ball a ε × m2.open_ball a' ε' |a a' ε ε'. a  S  a'  S'  0 < ε  0 < ε'}"
    then obtain a ε a' ε' where hae:
    "U = m1.open_ball a ε × m2.open_ball a' ε'" "a  S" "a'  S'" "0 < ε" "0 < ε'"
      by auto
    show "openin (topology_generated_by {m.open_ball a ε |a ε. a  S × S'  0 < ε}) U"
      unfolding m.mtopology_def2[symmetric] m.mtopology_openin_iff hae(1)
      using binary_distance_ball1[of _ a ε _ a' ε'] m1.open_ball_subset_ofS m2.open_ball_subset_ofS
      by fastforce
  next
    fix U
    assume "U  {m.open_ball a ε |a ε. a  S × S'  0 < ε}"
    then obtain a a' ε where hae:
    "U = m.open_ball (a,a') ε" "a  S" "a'  S'" "0 < ε"
      by auto
    show "openin (topology_generated_by {m1.open_ball a ε × m2.open_ball a' ε' |a a' ε ε'. a  S  a'  S'  0 < ε  0 < ε'}) U"
      unfolding openin_subopen[of _ " m.open_ball (a,a') ε"] hae(1)
    proof
      fix x
      assume h:"x  m.open_ball (a, a') ε"
      with binary_distance_ball2[of "fst x" "snd x" a a' ε]
      obtain ε' ε'' where he:
        "ε' > 0" "ε'' > 0" "m1.open_ball (fst x) ε' × m2.open_ball (snd x) ε''  m.open_ball (a, a') ε"
        by auto
      show "T. openin (topology_generated_by {m1.open_ball a ε × m2.open_ball a' ε' |a a' ε ε'. a  S  a'  S'  0 < ε  0 < ε'}) T  x  T  T  m.open_ball (a, a') ε"
        unfolding openin_topology_generated_by_iff
        using he m1.open_ball_ina[of "fst x",OF _ he(1)] m.open_ballD'(1,2)[OF h] m2.open_ball_ina[of "snd x",OF _ he(2)]
        by(fastforce intro!: generate_topology_on.Basis exI[where x="m1.open_ball (fst x) ε' × m2.open_ball (snd x) ε''"] exI[where x="fst x"] exI[where x="snd x"])
    qed
  qed
  also have "... = prod_topology m1.mtopology m2.mtopology"
  proof -
    have "{m1.open_ball a ε × m2.open_ball a' ε' |a a' ε ε'. a  S  a'  S'  0 < ε  0 < ε'} = {U × V |U V. U  {m1.open_ball a ε |a ε. a  S  0 < ε}  V  {m2.open_ball a ε |a ε. a  S'  0 < ε}}"
      by blast
    thus ?thesis
      unfolding m1.mtopology_def2 m2.mtopology_def2
      by(simp only: prod_topology_generated_by[symmetric])
  qed
  finally show ?thesis .
qed

lemma binary_distance_converge_to_inS_iff:
 "m.converge_to_inS zn (x,y)  m1.converge_to_inS (λn. fst (zn n)) x  m2.converge_to_inS (λn. snd (zn n)) y"
proof safe
  assume "m.converge_to_inS zn (x, y)"
  then have h:"zn  UNIV  S × S'" "x  S" "y  S'" "e. e>0  N. nN. zn n  m.open_ball (x, y) e"
    by(auto simp: m.converge_to_inS_def2')
  show "m1.converge_to_inS (λn. fst (zn n)) x"
       "m2.converge_to_inS (λn. snd (zn n)) y"
    unfolding m1.converge_to_inS_def2' m2.converge_to_inS_def2'
  proof safe
    fix e :: real
    assume "e > 0"
    then obtain N where "n. n  N  zn n  m.open_ball (x, y) e"
      using h(4) by auto
    thus "N. nN. fst (zn n)  m1.open_ball x e"
         "N. nN. snd (zn n)  m2.open_ball y e"
      using binary_distance_ball'[of "zn _" "(x,y)"]
      by(auto intro!: exI[where x=N])
  qed(insert h(1-3),simp_all add: Pi_iff mem_Times_iff)
next
  assume h:"m1.converge_to_inS (λn. fst (zn n)) x" "m2.converge_to_inS (λn. snd (zn n)) y"
  show "m.converge_to_inS zn (x, y)"
    unfolding m.converge_to_inS_def2'
  proof safe
    show goal1:"x  S" "y  S'" "zn n  S × S'" for n
      using h by(auto simp: m1.converge_to_inS_def m2.converge_to_inS_def Pi_iff mem_Times_iff)
    fix e :: real
    assume "e > 0"
    from binary_distance_ball2'[OF goal1(1) this goal1(2)]
    obtain e1 e2 where e12:"e1 > 0" "e2 > 0" "m1.open_ball x e1 × m2.open_ball y e2  m.open_ball (x, y) e " by auto
    then obtain N1 N2 where N12: "n. n  N1  fst (zn n)  m1.open_ball x e1" "n. n  N2  snd (zn n)  m2.open_ball y e2"
      using h by(auto simp: m1.converge_to_inS_def2' m2.converge_to_inS_def2') metis
    with e12 have "n. n  max N1 N2  zn n  m1.open_ball x e1 × m2.open_ball y e2"
      by (simp add: mem_Times_iff)
    with e12(3) show "N. nN. zn n  m.open_ball (x, y) e"
      by(auto intro!: exI[where x="max N1 N2"])
  qed
qed

lemma binary_distance_converge_to_inS_iff':
 "m.converge_to_inS zn z  m1.converge_to_inS (λn. fst (zn n)) (fst z)  m2.converge_to_inS (λn. snd (zn n)) (snd z)"
  using binary_distance_converge_to_inS_iff[of _ "fst z" "snd z"] by simp

corollary binary_distance_convergent_inS_iff:
 "m.convergent_inS zn  m1.convergent_inS (λn. fst (zn n))  m2.convergent_inS (λn. snd (zn n))"
  by(auto simp: m.convergent_inS_def m1.convergent_inS_def m2.convergent_inS_def binary_distance_converge_to_inS_iff)

lemma binary_distance_Cauchy_inS_iff:
 "m.Cauchy_inS zn  m1.Cauchy_inS (λn. fst (zn n))  m2.Cauchy_inS (λn. snd (zn n))"
proof safe
  assume h:"m.Cauchy_inS zn"
  show "m1.Cauchy_inS (λn. fst (zn n))" "m2.Cauchy_inS (λn. snd (zn n))"
    unfolding m1.Cauchy_inS_def2' m2.Cauchy_inS_def2'
  proof safe
    fix e :: real
    assume "e > 0"
    then obtain x y N where "x  S" "y  S'" "n. n  N  zn n  m.open_ball (x,y) e"
      using h by(auto simp: m.Cauchy_inS_def2') metis
    thus "xS. N. nN. fst (zn n)  m1.open_ball x e"
         "yS'. N. nN. snd (zn n)  m2.open_ball y e"
      using binary_distance_ball'[of "zn _" "(x,y)"]
      by(auto intro!: exI[where x=x] exI[where x=y] exI[where x=N]) blast
  qed(insert h, simp_all add: m.Cauchy_inS_def Pi_iff mem_Times_iff)
next
  assume h: "m1.Cauchy_inS (λn. fst (zn n))" "m2.Cauchy_inS (λn. snd (zn n))"
  show "m.Cauchy_inS zn"
    unfolding m.Cauchy_inS_def
  proof safe
    show 1:"zn n  S × S'" for n
      using h(1,2) m1.Cauchy_inS_dest1 m2.Cauchy_inS_dest1 mem_Times_iff by blast
    fix e :: real
    assume "e > 0"
    then obtain N1 N2 where N:"n m. n  N1  m  N1  d (fst (zn n)) (fst (zn m)) < e / 2" "n m. n  N2  m  N2  d' (snd (zn n)) (snd (zn m)) < e / 2"
      by (metis h(1) h(2) less_divide_eq_numeral1(1) m1.Cauchy_inS_def m2.Cauchy_inS_def mult_zero_left)
    show "N. nN. mN. binary_distance S d S' d' (zn n) (zn m) < e"
    proof(safe intro!: exI[where x="max N1 N2"])
      fix n m
      assume "max N1 N2  n" "max N1 N2  m"
      then have le:"N1  n" "N1  m" "N2  n" "N2  m" by auto
      show "binary_distance S d S' d' (zn n) (zn m) < e"
        using N(1)[OF le(1,2)] N(2)[OF le(3,4)] e > 0
        by(auto simp: binary_distance_def split_beta')
    qed
  qed
qed

end

lemma binary_distance_separable:
  assumes "separable_metric_set S d" "separable_metric_set S' d'"
  shows "separable_metric_set (S × S') (binary_distance S d S' d')"
proof -
  interpret m1:separable_metric_set S d by fact
  interpret m2:separable_metric_set S' d' by fact
  interpret m : metric_set "S × S'" "binary_distance S d S' d'"
    by(auto intro!: binary_metric_set m1.metric_set_axioms m2.metric_set_axioms)
  show ?thesis
    using m.separable_iff_topological_separable separable_prod[OF m1.topological_separable_if_separable m2.topological_separable_if_separable] binary_distance_mtopology[OF m1.metric_set_axioms m2.metric_set_axioms]
    by auto
qed

lemma binary_distance_complete:
  assumes "complete_metric_set S d" "complete_metric_set S' d'"
  shows "complete_metric_set (S × S') (binary_distance S d S' d')"
proof -
  interpret m1:complete_metric_set S d by fact
  interpret m2:complete_metric_set S' d' by fact
  interpret m : metric_set "S × S'" "binary_distance S d S' d'"
    by(auto intro!: binary_metric_set m1.metric_set_axioms m2.metric_set_axioms)
  show ?thesis
    by standard (simp add: binary_distance_Cauchy_inS_iff[OF m1.metric_set_axioms m2.metric_set_axioms] binary_distance_convergent_inS_iff[OF m1.metric_set_axioms m2.metric_set_axioms] m1.convergence m2.convergence)
qed

lemma binary_distance_polish:
  assumes "polish_metric_set S d" and "polish_metric_set S' d'"
  shows "polish_metric_set (S×S') (binary_distance S d S' d')"
  using assms by(simp add: polish_metric_set_def binary_distance_separable binary_distance_complete)

subsection  ‹Sum Metric Spaces›

locale sum_metric =
  fixes I :: "'i set"
    and Si :: "'i  'a set"
    and di :: "'i  'a  'a  real"
  assumes disj_fam: "disjoint_family_on Si I"
      and d_nonneg: "i x y. 0  di i x y"
      and d_bounded: "i x y. di i x y < 1"
      and sd_metric: "i. i  I  metric_set (Si i) (di i)"
begin

abbreviation "S  iI. Si i"

lemma Si_inj_on:
  assumes "i  I" "j  I" "a  Si i" "a  Si j"
  shows "i = j"
  using disj_fam assms by(auto simp: disjoint_family_on_def)

definition sum_dist :: "['a, 'a]  real" where
"sum_dist x y  (if x  S  y  S then (if iI. x  Si i  y  Si i then di (THE i. i  I  x  Si i  y  Si i) x y else 1) else 0)"

lemma sum_dist_simps:
  shows "i. i  I; x  Si i; y  Si i  sum_dist x y = di i x y"
    and "i j. i  I; j  I; i  j; x  Si i; y  Si j  sum_dist x y = 1"
    and "i. i  I; y  S; x  Si i; y  Si i  sum_dist x y = 1"
    and "i. i  I; x  S; y  Si i; x  Si i  sum_dist x y = 1"
    and "x  S  sum_dist x y = 0"
proof -
  { fix i
    assume h:"i  I" "x  Si i" "y  Si i"
    then have "sum_dist x y = di (THE i. i  I  x  Si i  y  Si i) x y"
      by(auto simp: sum_dist_def)
    also have "... = di i x y"
    proof -
      have "(THE i. i  I  x  Si i  y  Si i) = i"
        using disj_fam h by(auto intro!: the1_equality simp: disjoint_family_on_def)
      thus ?thesis by simp
    qed
    finally show "sum_dist x y = di i x y" . }
  show "i j. i  I; j  I; i  j; x  Si i; y  Si j  sum_dist x y = 1"
       "i. i  I; y  S; x  Si i; y  Si i  sum_dist x y = 1" "i. i  I; x  S; y  Si i; x  Si i  sum_dist x y = 1"
       "x  S  sum_dist x y = 0"
    using disj_fam by(auto simp: sum_dist_def disjoint_family_on_def dest:Si_inj_on)
qed

lemma sum_dist_if_less1:
  assumes "i  I" "x  Si i" "y  S" "sum_dist x y < 1"
  shows "y  Si i"
  using assms sum_dist_simps(3) by fastforce

lemma inS_cases:
  assumes "x  S" "y  S"
      and "i. i  I; x  Si i; y  Si i  P x y"
      and "i j. i  I; j  I; i  j; x  Si i; y  Si j; x  y  P x y"
    shows "P x y" using assms by auto

sublocale metric_set S sum_dist
proof
  fix x y
  assume "x  S" "y  S"
  then show "x = y  sum_dist x y = 0"
    by(rule inS_cases, insert sd_metric) (auto simp: sum_dist_simps metric_set_def)
next
  { fix i x y
    assume h: "i  I" "x  Si i" "y  Si i"
    then have "sum_dist x y = di i x y"
              "sum_dist y x = di i x y"
      using sd_metric by(auto simp: sum_dist_simps metric_set_def) }
  thus "x y. sum_dist x y = sum_dist y x"
    by (metis (no_types, lifting) sum_dist_def)
next
  show 1:"x y. 0  sum_dist x y"
    using d_nonneg by(simp add: sum_dist_def)
  fix x y z
  assume h: "x  S" "y  S" "z  S"
  show "sum_dist x z  sum_dist x y + sum_dist y z" (is "?lhs  ?rhs")
  proof(rule inS_cases[OF h(1,3)])
    fix i
    assume h':"i  I" "x  Si i" "z  Si i"
    consider "y  Si i" | "y  Si i" by auto
    thus "?lhs  ?rhs"
    proof cases
      case 1
      with h' sd_metric [OF h'(1)]show ?thesis
        by(simp add: sum_dist_simps metric_set_def)
    next
      case 2
      with h' h(2) d_bounded[of i x z] 1[of y z]
      show ?thesis
        by(auto simp: sum_dist_simps)
    qed
  next
    fix i j
    assume h': "i  I" "j  I" "i  j" "x  Si i" "z  Si j"
    consider "y  Si i" | "y  Si j"
      using h' h(2) disj_fam by(auto simp: disjoint_family_on_def)
    thus "?lhs  ?rhs"
      by (cases, insert 1[of x y] 1[of y z] h' h(2)) (auto simp: sum_dist_simps)
  qed
qed(simp add: sum_dist_simps)

lemma sum_dist_le1: "sum_dist x y  1"
  using d_bounded[of _ x y] by(auto simp: sum_dist_def less_eq_real_def)


lemma sum_dist_ball_eq_ball:
  assumes "i  I" "e  1" "x  Si i"
  shows "metric_set.open_ball (Si i) (di i) x e = open_ball x e"
proof -
  interpret m: metric_set "Si i" "di i"
    by(simp add: assms sd_metric)
  show ?thesis
    using assms sum_dist_simps(1)[OF assms(1) assms(3)] sum_dist_if_less1[OF assms(1,3)]
    by(auto simp: m.open_ball_def open_ball_def) fastforce+
qed

lemma ball_le_sum_dist_ball:
  assumes "i  I"
  shows "metric_set.open_ball (Si i) (di i) x e  open_ball x e"
proof -
  interpret m: metric_set "Si i" "di i"
    by(simp add: assms sd_metric)
  show ?thesis
  proof safe
    fix y
    assume y: "y  m.open_ball x e"
    show "y  open_ball x e"
      using m.open_ballD[OF y] m.open_ballD'[OF y] assms
      by(auto simp: open_ball_def sum_dist_simps)
  qed
qed

lemma openin_sum_mtopology_iff:
 "openin mtopology U  U  S  (iI. openin (metric_set.mtopology (Si i) (di i)) (U  Si i))"
proof safe
  fix i
  assume h:"openin mtopology U" "i  I"
  then interpret m: metric_set "Si i" "di i"
    using sd_metric by simp
  show "openin m.mtopology (U  Si i)"
    unfolding m.mtopology_openin_iff
  proof safe
    fix x
    assume x:"x  U" "x  Si i"
    with h obtain e where e: "e > 0" "open_ball x e  U"
      by(auto simp: mtopology_openin_iff)
    show "ε>0. m.open_ball x ε  U  Si i"
    proof(safe intro!: exI[where x=e])
      fix y
      assume "y  m.open_ball x e"
      from m.open_ballD[OF this] x(2)  m.open_ballD'(1)[OF this] h(2)
      have "y  open_ball x e"
        by(auto simp: open_ball_def sum_dist_simps)
      with e show "y  U" by auto
    qed(use e m.open_ball_subset_ofS in auto)
  qed
next
  show "x. openin mtopology U  x  U  x  S"
    by(auto simp: mtopology_openin_iff)
next
  assume h: "U  S" "iI. openin (metric_set.mtopology (Si i) (di i)) (U  Si i)"
  show "openin mtopology U"
    unfolding mtopology_openin_iff
  proof safe
    fix x
    assume x: "x  U"
    then obtain i where i: "i  I" "x  Si i"
      using h(1) by auto
    then interpret m: metric_set "Si i" "di i"
      using sd_metric by simp
    obtain e where e: "e > 0" "m.open_ball x e  U  Si i"
      using i h(2) by (meson IntI m.mtopology_openin_iff x)
    show "ε>0. open_ball x ε  U"
    proof(safe intro!: exI[where x="min e 1"])
      fix y
      assume y:"y  open_ball x (min e 1)"
      then show "y  U"
        using sum_dist_ball_eq_ball[OF i(1) _ i(2),of "min e 1"] e m.open_ball_le[of "min e 1" e x]
        by auto 
    qed(simp add: e)
  qed(use h(1) in auto)
qed

corollary openin_sum_mtopology_Si:
  assumes "i  I"
  shows "openin mtopology (Si i)"
  unfolding openin_sum_mtopology_iff
proof safe
  fix j
  assume j:"j  I"
  then interpret m: metric_set "Si j" "di j"
    by(simp add: sd_metric)
  show "openin m.mtopology (Si i  Si j)"
    by (cases "i = j", insert assms disj_fam j) (auto simp: disjoint_family_on_def)
qed(use assms in auto)

lemma converge_to_inSi_converge_to_inS:
  assumes "i  I" "metric_set.converge_to_inS (Si i) (di i) xn x"
  shows "converge_to_inS xn x"
proof -
  interpret m: metric_set "Si i" "di i"
    by(simp add: assms sd_metric)
  {
    fix e :: real
    assume "e > 0"
    then obtain N where "n. n  N  xn n  m.open_ball x e"
      using assms(2) by(auto simp: m.converge_to_inS_def2') metis
    hence "N. nN. xn n  open_ball x e"
      using ball_le_sum_dist_ball[OF assms(1),of x e]
      by(auto intro!: exI[where x=N]) }
  thus ?thesis
    using assms by(auto simp: m.converge_to_inS_def2' converge_to_inS_def2')
qed

corollary convergent_inSi_convergent_inS:
  assumes "i  I" "metric_set.convergent_inS (Si i) (di i) xn"
  shows "convergent_inS xn"
  using converge_to_inSi_converge_to_inS[OF assms(1)] assms(1) assms(2) convergent_inS_def metric_set.the_limit_if_converge sd_metric
  by blast

lemma converge_to_inS_converge_to_inSi_off_set:
  assumes "converge_to_inS xn x"
  shows "n. jI. metric_set.converge_to_inS (Si j) (di j) (λi. xn (i + n)) x"
proof -
  obtain i where i: "i  I" "x  Si i"
    using assms by(auto simp: converge_to_inS_def)
  then interpret m: metric_set "Si i" "di i"
    by(simp add: sd_metric)
  obtain N where N: "n. n  N  sum_dist (xn n) x < 1"
    using assms by(fastforce simp: converge_to_inS_def2)
  hence N': "n  N  xn n  Si i" for n
    using assms by(auto intro!: sum_dist_if_less1[OF i,of "xn n"] simp: dist_sym[of _ x] converge_to_inS_def)
  show ?thesis
  proof(safe intro!: exI[where x=N] bexI[OF _ i(1)])
    show "m.converge_to_inS (λi. xn (i + N)) x"
      unfolding m.converge_to_inS_def2
    proof(safe intro!: N' i(2))
      fix e :: real
      assume "0 < e"
      then obtain M where M: "n. n  M  sum_dist (xn n) x < e"
        using assms by(fastforce simp: converge_to_inS_def2)
      hence "n  max N M  di i (xn n) x < e" for n
        using sum_dist_simps(1)[OF i(1) N'[of n] i(2),symmetric] by auto        
      thus "M. nM. di i (xn (n + N)) x < e"
        by(auto intro!: exI[where x=M])
    qed simp
  qed
qed

corollary convergent_inS_convergent_inSi_off_set:
  assumes "convergent_inS xn"
  shows "n. jI. metric_set.convergent_inS (Si j) (di j) (λi. xn (i + n))"
  using converge_to_inS_converge_to_inSi_off_set
  by (meson assms metric_set.convergent_inS_def metric_set_axioms sd_metric)


lemma Cauchy_inSi_Cauchy_inS:
  assumes "i  I" "metric_set.Cauchy_inS (Si i) (di i)xn"
  shows "Cauchy_inS xn"
proof -
  interpret m: metric_set "Si i" "di i"
    by(simp add: assms sd_metric)
  have [simp]:"sum_dist (xn n) (xn m) = di i (xn n) (xn m)" for n m
    using assms sum_dist_simps(1)[OF assms(1)]
    by(auto simp: m.Cauchy_inS_def Cauchy_inS_def)
  show ?thesis
    using assms by(auto simp: m.Cauchy_inS_def Cauchy_inS_def)
qed

lemma Cauchy_inS_Cauchy_inSi:
  assumes "Cauchy_inS xn"
  shows "n. jI. metric_set.Cauchy_inS (Si j) (di j) (λi. xn (i + n))"
proof -
  obtain x i N where xiN: "i  I" "x  Si i" "n. n  N  xn n  open_ball x 1"
    using assms by(auto simp: Cauchy_inS_def2') (metis UNION_empty_conv(2) d_bounded d_nonneg dist_0 empty_subsetI less_eq_real_def open_ball_le_0 subsetI subset_antisym sum_dist_le1) 
  then interpret m: metric_set "Si i" "di i"
    by(simp add: sd_metric)
  have xn: "n  N  xn n  Si i" for n
    using xiN(3)[of n] by(auto simp: sum_dist_ball_eq_ball[OF xiN(1) order_refl xiN(2),symmetric] dest: m.open_ballD')
  show ?thesis
  proof(safe intro!: exI[where x=N] bexI[OF _ xiN(1)])
    show "m.Cauchy_inS (λi. xn (i + N))"
      unfolding m.Cauchy_inS_def
    proof safe
      fix e :: real
      assume "0 < e"
      then obtain M where M: "n m. n  M  m  M  sum_dist (xn n) (xn m) < e"
        using assms by(auto simp: Cauchy_inS_def) metis
      have [simp]: "n  N  m  N  di i (xn n) (xn m) = sum_dist (xn n) (xn m)" for n m
        using xn sum_dist_simps(1)[OF xiN(1) xn[of n] xn[of m]] by simp
      show "N'. nN'. mN'. di i (xn (n + N)) (xn (m + N)) < e"
        using M by(auto intro!: exI[where x="max N M"])
    qed(use xn in auto)
  qed
qed

end

lemma sum_metricI:
  fixes Si
  assumes "disjoint_family_on Si I"
      and "i x y. i  I  0  di i x y"
      and "i x y. di i x y < 1"
      and "i. i  I  metric_set (Si i) (di i)"
    shows "sum_metric I Si di"
  using assms by(auto simp: sum_metric_def) (meson metric_set.dist_geq0)

locale sum_separable_metric = sum_metric +
  assumes I: "countable I"
      and sd_separable_metric: "i. i  I  separable_metric_set (Si i) (di i)"
begin

sublocale separable_metric_set S sum_dist
proof
  obtain Ui where Ui: "i. i  I  countable (Ui i)" "i. i  I  metric_set.dense_set (Si i) (di i) (Ui i)" 
    using sd_separable_metric by(auto simp: separable_metric_set_def separable_metric_set_axioms_def) metis
  define U where "U  iI. Ui i"
  show "U. countable U  dense_set U"
  proof(safe intro!: exI[where x=U])
    show "countable U"
      using Ui(1) I by(auto simp: U_def)
  next
    show "dense_set U"
      unfolding dense_set_def U_def
    proof safe
      fix i x
      assume "i  I" "x  Ui i"
      then show "x  S"
        using sd_separable_metric Ui by(auto intro!: bexI[where x=i] simp: separable_metric_set_def metric_set.dense_set_def)
    next
      fix i x e
      assume h:"i  I" "x  Si i" "(0 :: real) < e" "open_ball x e   (Ui ` I) = {}"
      then interpret sd: separable_metric_set "Si i" "di i"
        by(simp add: sd_separable_metric)
      have "sd.open_ball x e  Ui i  {}"
        using Ui(2)[OF h(1)] h(1-3) by(auto simp: U_def sd.dense_set_def)
      hence "sd.open_ball x e   (Ui ` I)  {}"
        using h(1) by blast
      thus False
        using ball_le_sum_dist_ball[OF i  I,of x e] h(4) by blast
    qed
  qed
qed

end

locale sum_complete_metric = sum_metric +
  assumes sd_complete_metric: "i. i  I  complete_metric_set (Si i) (di i)"
begin

sublocale complete_metric_set S sum_dist
proof
  fix xn
  assume 1:"Cauchy_inS xn"
  from Cauchy_inS_Cauchy_inSi[OF this] obtain n j where h: "j  I"  "metric_set.Cauchy_inS (Si j) (di j) (λi. xn (i + n))"
    by auto
  then have "metric_set.convergent_inS (Si j) (di j) (λi. xn (i + n))"
    by (simp add: complete_metric_set.convergence sd_complete_metric)
  from convergent_inS_offset[OF convergent_inSi_convergent_inS[OF h(1) this]] 1
  show "convergent_inS xn"
    by(simp add: Cauchy_inS_def)
qed

end

locale sum_polish_metric = sum_complete_metric + sum_separable_metric
begin

sublocale polish_metric_set S sum_dist
  by (simp add: complete_metric_set_axioms polish_metric_set_def separable_metric_set_axioms)

end

lemma sum_polish_metricI:
  fixes Si
  assumes "countable I"
      and "disjoint_family_on Si I"
      and "i x y. i  I  0  di i x y"
      and "i x y. di i x y < 1"
      and "i. i  I  polish_metric_set (Si i) (di i)"
    shows "sum_polish_metric I Si di"
  using assms by(auto simp: sum_polish_metric_def sum_complete_metric_def sum_separable_metric_def sum_complete_metric_axioms_def sum_separable_metric_axioms_def polish_metric_set_def complete_metric_set_def sum_metricI)

end