Theory Standard_Borel_Spaces.Set_Based_Metric_Space

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

subsection  ‹Lemmas for Abstract Metric Spaces›
theory Set_Based_Metric_Space
  imports Lemmas_StandardBorel
begin

text ‹ We prove additional lemmas related to set-based metric spaces. ›

subsubsection ‹ Basic Lemmas ›
lemma
  assumes "Metric_space M d" "x y. x  M  y  M  d x y = d' x y"
      and "x y. d' x y = d' y x" "x y. d' x y  0"
    shows Metric_space_eq: "Metric_space M d'"
      and Metric_space_eq_mtopology: "Metric_space.mtopology M d = Metric_space.mtopology M d'"
      and Metric_space_eq_mcomplete: "Metric_space.mcomplete M d  Metric_space.mcomplete M d'"
proof -
  interpret m1: Metric_space M d by fact
  show "Metric_space M d'"
    using assms by(auto simp: Metric_space_def)
  then interpret m2:Metric_space M d' .
  have [simp]: "m1.mball x e = m2.mball x e" for x e
    using assms by(auto simp: m1.mball_def m2.mball_def)
  show 1:"m1.mtopology = m2.mtopology"
    by(auto simp: topology_eq m1.openin_mtopology m2.openin_mtopology)
  show "m1.mcomplete = m2.mcomplete"
    by(auto simp: 1 m1.mcomplete_def m2.mcomplete_def m1.MCauchy_def m2.MCauchy_def assms(2) in_mono)
qed

context Metric_space
begin

lemma mtopology_base_in_balls: "base_in mtopology {mball a ε | a ε. a  M  ε > 0}"
proof -
  have 1:"x. x  {mball a ε | a ε. a  M  ε > 0}  openin mtopology x"
    by auto
  show ?thesis
    unfolding base_in_def2[of "{mball a ε | a ε. a  M  ε > 0}",OF 1,simplified]
    by (metis centre_in_mball_iff in_mono openin_mtopology)
qed

lemma closedin_metric2: "closedin mtopology C  C  M  (x. x  C  (ε>0. mball x ε  C  {}))"
proof
  assume h:"closedin mtopology C"
  have 1: "C  M"
    using Metric_space.closedin_metric Metric_space_axioms h by blast
  show "C  M  (x. x  C  (ε>0. mball x ε  C  {}))"
  proof safe
    fix ε x
    assume "x  C" "(0 :: real) < ε" "mball x ε  C = {}"
    with 1 show False
      by blast
  next
    fix x
    assume "ε>0. mball x ε  C  {}"
    hence "xn. xn  mball x (1 / real (Suc n))  C" for n
      by (meson all_not_in_conv divide_pos_pos of_nat_0_less_iff zero_less_Suc zero_less_one)
    then obtain xn where xn:"n. xn n  mball x (1 / real (Suc n))  C"
      by metis
    hence xxn:"x  M" "range xn  C"
      using xn by auto
    have "limitin mtopology xn x sequentially"
      unfolding limitin_metric eventually_sequentially
    proof safe
      fix ε
      assume "(0 :: real) < ε"
      then obtain N where hN: "1 / real (Suc N) < ε"
        using nat_approx_posE by blast
      show "N. nN. xn n  M  d (xn n) x < ε"
      proof(safe intro!: exI[where x="N"])
        fix n
        assume n[arith]: "N  n"
        then have "1 / real (Suc n) < ε"
          by (metis Suc_le_mono hN inverse_of_nat_le nat.distinct(1) order_le_less_trans)
        with xn[of n] show "d (xn n) x < ε"
          by (simp add: commute)
      qed(use xxn 1 in auto)
    qed fact
    with h 1 xxn show "x  C"
      by(auto simp: metric_closedin_iff_sequentially_closed)
  qed(use 1 in auto)
next
  assume"C  M  (x. (x  C)  (ε>0. mball x ε  C  {}))"
  hence h:"C  M" "x. (x  C)  (ε>0. mball x ε  C  {})"
    by simp_all
  show "closedin mtopology C"
    unfolding metric_closedin_iff_sequentially_closed
  proof safe
    fix xn x
    assume h':"range xn  C" "limitin mtopology xn x sequentially"
    hence "x  M" by (simp add: limitin_mspace) 
    have "mball x ε  C  {}" if "ε > 0" for ε
    proof -
      obtain N where hN:"n. n  N  d (xn n) x < ε"
        using h'(2) ε > 0 limit_metric_sequentially by blast
      have "xn N  mball x ε  C"
        using h'(1) hN[of N] x  M commute h(1) by fastforce
      thus "mball x ε  C  {}" by auto
    qed
    with h(2)[of x] show "x  C" by simp
  qed(use h(1) in auto)
qed

lemma openin_mtopology2:
 "openin mtopology U  U  M  (xn x. limitin mtopology xn x sequentially  x  U  (N. nN. xn n  U))"
  unfolding openin_mtopology
proof safe
  fix xn x
  assume h: "x. x  U  (r>0. mball x r  U)" "limitin mtopology xn x sequentially" "x  U" "U  M"
  then obtain r where r: "r > 0" "mball x r  U"
    by auto
  with h(2) obtain N where N: "n. n  N  xn n  M" "n. n  N  d (xn n) x < r"
    by (metis limit_metric_sequentially)
  with h have "N. nN. xn n  mball x r"
    by(auto intro!: exI[where x=N] simp:commute)
  with r show "N. nN. xn n  U"
    by blast
next
  fix x
  assume h:"U  M" "xn x. limitin mtopology xn x sequentially  x  U  (N. nN. xn n  U)" "x  U"
  show "r>0. mball x r  U"
  proof(rule ccontr)
    assume "¬ (r>0. mball x r  U)"
    then have "n. xnmball x (1 / Suc n). xn  U"
      by (meson of_nat_0_less_iff subsetI zero_less_Suc zero_less_divide_1_iff)
    then obtain xn where xn: "n. xn n  mball x (1 / Suc n)" "n. xn n   U"
      by metis
    have "limitin mtopology xn x sequentially"
      unfolding limit_metric_sequentially
    proof safe
      fix e :: real
      assume e:"0 < e"
      then obtain N where N: "1 / real (Suc N) < e"
        using nat_approx_posE by blast
      show "N. nN. xn n  M  d (xn n) x < e"
      proof(safe intro!: exI[where x=N])
        fix n
        assume n: "n  N"
        then have "1 / Suc n < e"
          by (metis N Suc_le_mono inverse_of_nat_le nat.distinct(1) order_le_less_trans)
        thus "d (xn n) x < e"
          using xn(1)[of n] by(auto simp: commute)
      qed(use xn in auto)
    qed(use h in auto)
    with h(2,3) xn(2) show False
      by auto
  qed
qed

lemma closure_of_mball: "mtopology closure_of mball a e  mcball a e"
  by (simp add: closure_of_minimal mball_subset_mcball)

lemma interior_of_mcball: "mball a e  mtopology interior_of mcball a e"
  by (simp add: interior_of_maximal_eq mball_subset_mcball)

lemma isolated_points_of_mtopology:
 "mtopology isolated_points_of A = {xMA. xn. range xn  A  limitin mtopology xn x sequentially  (no. nno. xn n = x)}"
proof safe
  fix x xn
  assume h:"x  mtopology isolated_points_of A" "limitin mtopology xn x sequentially" "range xn  A"
  then have ha:"x  topspace mtopology" "x  A" "U. x  U  openin mtopology U  U  (A - {x}) = {}"
    by(simp_all add: in_isolated_points_of)
  then obtain U where u:"x  U" "openin mtopology U" "U  (A - {x}) = {}"
    by auto
  then obtain e where e: "e > 0" "mball x e  U"
    by (meson openin_mtopology)
  then obtain N where "n. n  N  xn n  mball x e"
    using h(2) commute limit_metric_sequentially by fastforce
  thus "no. nno. xn n = x"
    using h(3) e(2) u(3) by(fastforce intro!: exI[where x=N])
qed (auto simp: derived_set_of_sequentially isolated_points_of_def, blast)

lemma perfect_set_mball_infinite:
  assumes "perfect_set mtopology A" "a  A" "e > 0"
  shows "infinite (mball a e)"
proof safe
  assume h: "finite (mball a e)"
  have "a  M"
    using assms perfect_setD(2)[OF assms(1)] by auto
  have "e > 0. mball a e = {a}"
  proof -
    consider "mball a e = {a}" | "{a}  mball a e"
      using a  M assms(3) by blast
    thus ?thesis
    proof cases
      case 1
      with assms show ?thesis by auto
    next
      case 2
      then have nen:"{d a b |b. b  mball a e  a  b}  {}"
        by auto
      have fin: "finite {d a b |b. b  mball a e  a  b}"
        using h by (auto simp del: in_mball)
      define e' where "e'  Min {d a b |b. b  mball a e  a  b}"
      have "e' > 0"
        using mdist_pos_eq[OF a  M] by(simp add: e'_def Min_gr_iff[OF fin nen] del: in_mball) auto
      have bd:"b. b  mball a e  a  b  e'  d a b"
        by(auto simp: e'_def Min_le_iff[OF fin nen] simp del: in_mball)
      have "e'  e"
        unfolding e'_def Min_le_iff[OF fin nen]
        using nen by auto
      show ?thesis
      proof(safe intro!: exI[where x=e'])
        fix x
        assume x:"x  mball a e'"
        then show "x = a"
          using e'  e bd by fastforce
      qed (use a  M e' > 0 in auto)
    qed
  qed
  then obtain e' where e':"e' > 0" "mball a e' = {a}" by auto
  show False
    using perfect_setD(3)[OF assms(1,2) centre_in_mball_iff[of a e',THEN iffD2]] a  M e' > 0 e'(2) by blast
qed

lemma MCauchy_dist_Cauchy:
  assumes "MCauchy xn" "MCauchy yn"
  shows "Cauchy (λn. d (xn n) (yn n))"
  unfolding metric_space_class.Cauchy_altdef2 dist_real_def
proof safe
  have h:"n. xn n  M" "n. yn n  M"
    using assms by(auto simp: MCauchy_def)
  fix e :: real
  assume e:"0 < e"
  with assms obtain N1 N2 where N: "n m. n  N1  m  N1  d (xn n) (xn m) < e / 2" "n m. n  N2  m  N2  d (yn n) (yn m) < e / 2"
    by (metis MCauchy_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. ¦d (xn n) (yn n) - d (xn N) (yn N)¦ < e"
  proof(safe intro!: exI[where x=N])
    fix n
    assume n:"N  n"
    have "d (xn n) (yn n)  d (xn n) (xn N) + d (xn N) (yn N) + d (yn N) (yn n)"
         "d (xn N) (yn N)  d (xn N) (xn n) + d (xn n) (yn n) + d (yn n) (yn N)"
      using triangle[OF h(1)[of n] h(1)[of N] h(2)[of n]] triangle[OF h(1)[of N] h(2)[of N] h(2)[of n]]
            triangle[OF h(1)[of N] h(2)[of n] h(2)[of N]] triangle[OF h(1)[of N] h(1)[of n] h(2)[of n]] by auto
    thus "¦d (xn n) (yn n) - d (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

subsubsection ‹ Dense in Metric Spaces›
abbreviation "mdense  dense_in mtopology"

text 🌐‹https://people.bath.ac.uk/mw2319/ma30252/sec-dense.html›
lemma mdense_def:
 "mdense U  U  M  (xM. ε>0. mball x ε  U  {})"
proof safe
  assume h:" U  M" "(xM. ε>0. mball x ε  U  {})"
  show "dense_in mtopology U"
  proof(rule dense_inI)
    fix V
    assume h':"openin mtopology V" "V  {}"
    then obtain x where 1:"x  V" by auto
    then obtain ε where 2:"ε>0" "mball x ε  V"
      by (meson h'(1) openin_mtopology)
    have "mball x ε  U  {}"
      using h 1 2 openin_subset[OF h'(1)]
      by (auto simp del: in_mball)
    thus "U  V  {}" using 2 by auto
  qed(use h in auto)
next
  fix x ε
  assume h:"x  M" "(0 :: real) < ε" "mball x ε  U = {}" "mdense U"
  then have "mball x ε  {}" "openin mtopology (mball x ε)"
    by auto
  with h(4) have "mball x ε  U  {}"
    by(auto simp: dense_in_def)
  with h(3) show False
    by simp
qed(auto simp: dense_in_def)

corollary mdense_balls_cover:
  assumes "mdense U" and "e > 0"
  shows "(uU. mball u e) = M"
  using assms[simplified mdense_def] commute by fastforce

lemma mdense_empty_iff: "mdense {}  M = {}"
  by(auto simp: mdense_def) (use zero_less_one in blast)

lemma mdense_M: "mdense M"
  by(auto simp: mdense_def)

lemma mdense_def2:
 "mdense U  U  M  (xM. ε>0.yU. d x y < ε)"
proof safe
  fix x e
  assume h: "mdense U" and hxe: "x  M" "(0 :: real) < e"
  then have "x  (uU. mball u e)"
    by(simp add: mdense_balls_cover)
  thus "yU. d x y < e"
    by (fastforce simp: commute)
qed(fastforce simp: mdense_def)+

lemma mdense_def3:
 "mdense U  U  M  (xM. xn. range xn  U  limitin mtopology xn x sequentially)"
  unfolding mdense_def
proof safe
  fix x
  assume h: "U  M" "xM. ε>0. mball x ε  U  {}" "x  M"
  then have "n. mball x (1 / (real n + 1))  U  {}"
    by auto
  hence "n. k. k  mball x (1 / (real n + 1))  U" by (auto simp del: in_mball)
  hence "a. n. a n  mball x (1 / (real n + 1))  U" by(rule choice)
  then obtain xn where xn: "n. xn n  mball x (1 / (real n + 1))  U"
    by auto
  show "xn. range xn  U  limitin mtopology xn x sequentially"
    unfolding limitin_metric eventually_sequentially
  proof(safe intro!: exI[where x=xn])
    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. xn n  M  d (xn n) 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 "d (xn n) x < ε"
        using xn[of n] order.strict_trans1[OF 1 hn''] by (auto simp: commute)
    qed(use xn in auto)
  qed(use xn h in auto)
next
  fix x and e :: real
  assume h: "U  M" " xM. xn. range xn  U  limitin mtopology xn x sequentially" "x  M" "0 < e" "mball x e  U = {}"
  then obtain xn where xn:"range xn  U" "limitin mtopology xn x sequentially"
    by auto
  with h(4) obtain N where N: "n. n  N  d (xn n) x < e"
    by (meson limit_metric_sequentially)
  have "xn N  mball x e  U"
    using N[of N] xn(1) h(1,3) by (auto simp: commute)
  with h(5) show False by simp
qed

text ‹ Diameter›
definition mdiameter :: "'a set  ennreal" where
"mdiameter A   {ennreal (d x y) | x y. x  A  M  y  A  M}"

lemma mdiameter_empty[simp]:
 "mdiameter {} = 0"
  by(simp add: mdiameter_def bot_ennreal)

lemma mdiameter_def2:
  assumes "A  M"
  shows "mdiameter A =  {ennreal (d x y) | x y. x  A  y  A}"
  using assms by(auto simp: mdiameter_def) (meson subset_eq)

lemma mdiameter_subset:
  assumes "A  B"
  shows "mdiameter A  mdiameter B"
  unfolding mdiameter_def using assms by(auto intro!: Sup_subset_mono)

lemma mdiameter_cball_leq: "mdiameter (mcball a ε)  ennreal (2 * ε)"
  unfolding Sup_le_iff mdiameter_def
proof safe
  fix x y
  assume h:"x  mcball a ε" "y  mcball a ε" "x  M" "y  M"
  have "d x y  2 * ε"
    using h(1) h(2) triangle'' by fastforce
  thus "ennreal (d x y)  ennreal (2 * ε)"
    using ennreal_leI by blast
qed

lemma mdiameter_ball_leq:
 "mdiameter (mball a ε)  ennreal (2 * ε)"
  using mdiameter_subset[OF mball_subset_mcball[of a ε]] mdiameter_cball_leq[of a ε]
  by auto

lemma mdiameter_is_sup:
  assumes "x  A  M" "y  A  M"
  shows "d x y  mdiameter A"
  using assms by(auto simp: mdiameter_def intro!: Sup_upper)

lemma mdiameter_is_sup':
  assumes "x  A  M" "y  A  M" "mdiameter A  ennreal r" "r  0"
  shows "d x y  r"
  using order.trans[OF mdiameter_is_sup[OF assms(1,2)] assms(3)] assms(4) by simp

lemma mdiameter_le:
  assumes "x y. x  A  y  A  d x y  r"
  shows "mdiameter A  r"
  using assms by(auto simp: mdiameter_def Sup_le_iff ennreal_leI)

lemma mdiameter_eq_closure: "mdiameter (mtopology closure_of A) = mdiameter A"
proof(rule antisym)
  show "mdiameter A  mdiameter (mtopology closure_of A)"
    by(fastforce intro!: Sup_subset_mono simp: mdiameter_def metric_closure_of)
next
  have "{ennreal (d x y) |x y. x  A  M  y  A  M} = ennreal ` {d x y |x y. x  A  M  y  A  M}"
    by auto
  also have "mdiameter (mtopology closure_of A)   ..."
    unfolding le_Sup_iff_less
  proof safe
    fix r
    assume "r < mdiameter (mtopology closure_of A)"
    then obtain x y where xy:"x  mtopology closure_of A" "x  M" "y  mtopology closure_of A" "y  M" "r < ennreal (d x y)"
      by(auto simp: mdiameter_def less_Sup_iff)
    hence "r < "
      using dual_order.strict_trans ennreal_less_top by blast
    define e where "e  (d x y - enn2real r)/2"
    have "e > 0"
      using xy(5) r <  by(simp add: e_def)
    then obtain x' y' where xy':"x'  mball x e" "x' A" "y'  mball y e" "y' A"
      using xy by(fastforce simp: metric_closure_of)
    show "i{d x y |x y. x  A  M  y  A  M}. r  ennreal i"
    proof(safe intro!: bexI[where x="d x' y'"])
      have "d x y  d x x' + d x' y' + d y y'"
        using triangle[OF xy(2) _ xy(4),of x'] xy' triangle[of x' y' y]
        by(fastforce simp add: commute)
      also have "... < d x y - enn2real r + d x' y'"
        using xy'(1) xy'(3) by(simp add: e_def)
      finally have "enn2real r < d x' y'" by simp
      thus "r  ennreal (d x' y')"
        by (simp add: r < )
    qed(use xy'(1) xy'(3) xy'(2,4) in auto)
  qed
  finally show "mdiameter (mtopology closure_of A)  mdiameter A"
    by(simp add: mdiameter_def)
qed

lemma mbounded_finite_mdiameter: "mbounded A  A  M  mdiameter A < "
proof safe
  assume "mbounded A"
  then obtain x B where "A  mcball x B"
    by(auto simp: mbounded_def)
  then have "mdiameter A  mdiameter (mcball x B)"
    by(rule mdiameter_subset)
  also have "...  ennreal (2 * B)"
    by(rule mdiameter_cball_leq)
  also have "... < "
    by auto
  finally show "mdiameter A < " .
next
  assume h:"mdiameter A < " "A  M"
  consider "A = {}" | "A  {}" by auto
  then show "mbounded A"
  proof cases
    case h2:2
    then have 1:"{d x y |x y. x  A  y  A}  {}" by auto
    have eq:"{ennreal (d x y) | x y. x  A  y  A} = ennreal ` {d x y | x y. x  A  y  A}"
      by auto
    hence 2:"mdiameter A =  (ennreal ` {d x y | x y. x  A  y  A})"
      using h by(auto simp add: mdiameter_def2)
    obtain x y where hxy:
     "x  A" "y  A" "mdiameter A < ennreal (d x y + 1)"
      using SUP_approx_ennreal[OF _ 1 2,of 1] h by(fastforce simp: diameter_def)
    show ?thesis
      unfolding mbounded_alt
    proof(safe intro!: exI[where x="d x y + 1"])
      fix w z
      assume "w  A" "z  A "
      with SUP_lessD[OF hxy(3)[simplified 2]]
      have "ennreal (d w z) < ennreal (d x y + 1)"
        by blast
      thus "d w z  d x y + 1"
        by (metis canonically_ordered_monoid_add_class.lessE ennreal_le_iff2 ennreal_neg le_iff_add not_less_zero)
    qed (use h in auto)
  qed(auto simp: mbounded_def)
qed(auto simp: mbounded_def)

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

lemma d_set_nonneg[simp]:
 "d_set A x  0"
proof -
  have "{d x y |y. y  A} = d x ` A" by auto
  thus ?thesis
    by(auto simp: d_set_def intro!: cINF_greatest[of _ _ "d x"])
qed

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

lemma d_set_singleton[simp]:
  "x  M  y  M  d_set {y} x = d x y"
  by(auto simp: d_set_def)

lemma d_set_empty[simp]:
 "d_set {} x = 0"
  by(simp add: d_set_def)

lemma d_set_notin:
  "x  M  d_set A x = 0"
  by(auto simp: d_set_def)

lemma d_set_inA:
  assumes "x  A"
  shows "d_set A x = 0"
proof -
  {
    assume "x  M" "A  M"
    then have "0  {d x y |y. y  A}"
      using assms by(auto intro: exI[where x=x])
    moreover have "A  {}"
      using assms by auto
    ultimately have "Inf {d x y |y. y  A} = 0"
      using cInf_lower[OF 0  {d x y |y. y  A}] d_set_nonneg[of A x] A  M x  M
      by(auto simp: d_set_def)
  }
  thus ?thesis
    using assms by(auto simp: d_set_def)
qed

lemma d_set_nzeroD:
  assumes "d_set A x  0"
  shows "A  M" "x  A" "A  {}"
   by(rule ccontr, use assms d_set_inA d_set_def in auto)

lemma d_set_antimono:
  assumes "A  B" "A  {}" "B  M"
  shows "d_set B x  d_set A x"
proof(cases "B = {}")
  case h:False
  with assms have "{d x y |y. y  B}  {}" "{d x y |y. y  A}  {d x y |y. y  B}" "A  M"
    by auto
  with assms(3) show ?thesis
    by(simp add: d_set_def cInf_superset_mono assms(2))
qed(use assms in simp)

lemma d_set_bounded:
  assumes "y. y  A  d x y < K" "K > 0"
  shows "d_set A x < K"
proof -
  consider "A = {}" | "¬ A  M" | "x  M" | "A  {}" "A  M" "x  M"
    by blast
  then show ?thesis
  proof cases
    case 4
    then have 2:"{d x y |y. y  A}  {}" by auto
    show ?thesis
      using assms by (auto simp add: d_set_def cInf_lessD[OF 2]  cInf_less_iff[OF 2])
  qed(auto simp: d_set_def assms)
qed

lemma d_set_tr:
  assumes "x  M" "y  M"
  shows "d_set A x  d x y + d_set A y"
proof -
  consider "A = {}" | "¬ A  M" | "A  {}" "A  M"
    by blast
  then show ?thesis
  proof cases
    case 3
    have "d_set A x  Inf {d x y + d y a |a. aA}"
    proof -
      have " {d x y |y. y  A}   {d x y + d y a |a. a  A}"
        by(rule cInf_mono) (use 3 assms triangle in fastforce)+
      thus ?thesis
        by(simp add: d_set_def assms 3)
    qed
    also have "... = (aA. d x y + d y a)"
      by (simp add: Setcompr_eq_image)
    also have "... = d x y +  (d y ` A)"
      using 3 by(auto intro!: Inf_add_eq bdd_belowI[where m=0])
    also have "... = d x y + d_set A y"
      using assms 3 by(auto simp: d_set_def Setcompr_eq_image)
    finally show ?thesis .
  qed(auto simp: d_set_def)
qed

lemma d_set_abs_le:
  assumes "x  M" "y  M"
  shows "¦d_set A x - d_set A y¦  d x y"
  using d_set_tr[OF assms,of A] d_set_tr[OF assms(2,1),of A,simplified commute[of y x]]
  by auto

lemma d_set_inA_le:
  assumes "y  A"
  shows "d_set A x  d x y"
proof -
  consider "A  {}" "A  M" "x  M" | "¬ A  M" | "x  M"
    using assms by blast
  then show ?thesis
  proof cases
    case 1
    with assms have "y  M" by auto
    from d_set_tr[OF 1(3) this,of A] show ?thesis
      by(simp add: d_set_inA[OF assms])
  qed(auto simp: d_set_def)
qed

lemma d_set_ball_empty:
  assumes "A  {}" "A  M" "e > 0" "x  M" "mball x e  A = {}"
  shows "d_set A x  e"
  using assms by(fastforce simp: d_set_def assms(1) le_cInf_iff)

lemma d_set_closed_pos:
  assumes "closedin mtopology A" "A  {}" "x  M" "x  A"
  shows "d_set A x > 0"
proof -
  have a:"A  M" "openin mtopology (M - A)"
    using closedin_subset[OF assms(1)] assms(1) by auto
  with assms(3,4) obtain e where e: "e > 0" "mball x e  M - A"
    using openin_mtopology by auto
  thus ?thesis
    by(auto intro!: order.strict_trans2[OF e(1) d_set_ball_empty[OF assms(2) a(1) e(1) assms(3)]])
qed

lemma gdelta_in_closed:
  assumes "closedin mtopology M"
  shows "gdelta_in mtopology M"
  by(auto intro!: closed_imp_gdelta_in metrizable_space_mtopology)

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

abbreviation "osc X  osc_on (topspace X) X"

lemma osc_def: "osc X f = (λy.  {mdiameter (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  mdiameter (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  mdiameter (f ` v) < t)"
  by(auto simp add: osc_def Inf_less_iff)

end

definition mdist_set :: "'a metric  'a set  'a  real" where
"mdist_set m  Metric_space.d_set (mspace m) (mdist m)"

lemma(in Metric_space) mdist_set_Self: "mdist_set Self = d_set"
  by(simp add: mdist_set_def)

lemma mdist_set_nonneg[simp]: "mdist_set m A x  0"
  by(auto simp: mdist_set_def Metric_space.d_set_nonneg)

lemma mdist_set_singleton[simp]:
  "x  mspace m  y  mspace m  mdist_set m {y} x = mdist m x y"
  by(auto simp: mdist_set_def Metric_space.d_set_singleton)

lemma mdist_set_empty[simp]: "mdist_set m {} x = 0"
  by(auto simp: mdist_set_def Metric_space.d_set_empty)

lemma mdist_set_inA:
  assumes "x  A"
  shows "mdist_set m A x = 0"
  by(auto simp: assms mdist_set_def Metric_space.d_set_inA)

lemma mdist_set_nzeroD:
  assumes "mdist_set m A x  0"
  shows "A  mspace m" "x  A" "A  {}"
  using assms Metric_space.d_set_nzeroD[of "mspace m" "mdist m"]
  by(auto simp: mdist_set_def)

lemma mdist_set_antimono:
  assumes "A  B" "A  {}" "B  mspace m"
  shows "mdist_set m B x  mdist_set m A x"
  by(auto simp: assms mdist_set_def Metric_space.d_set_antimono)

lemma mdist_set_bounded:
  assumes "y. y  A  mdist m x y < K" "K > 0"
  shows "mdist_set m A x < K"
  by(auto simp: assms mdist_set_def Metric_space.d_set_bounded)

lemma mdist_set_tr:
  assumes "x  mspace m" "y  mspace m"
  shows "mdist_set m A x  mdist m x y + mdist_set m A y"
  by(auto simp: assms mdist_set_def Metric_space.d_set_tr)

lemma mdist_set_abs_le:
  assumes "x  mspace m" "y  mspace m"
  shows "¦mdist_set m A x - mdist_set m A y¦  mdist m x y"
  by(auto simp: assms mdist_set_def Metric_space.d_set_abs_le)

lemma mdist_set_inA_le:
  assumes "y  A"
  shows "mdist_set m A x  mdist m x y"
  by(auto simp: assms mdist_set_def Metric_space.d_set_inA_le)

lemma mdist_set_ball_empty:
  assumes "A  {}" "A  mspace m" "e > 0" "x  mspace m" "mball_of m x e  A = {}"
  shows "mdist_set m A x  e"
  by (metis Metric_space.d_set_ball_empty Metric_space_mspace_mdist assms mball_of_def mdist_set_def)

lemma mdist_set_closed_pos:
  assumes "closedin (mtopology_of m) A" "A  {}" "x  mspace m" "x  A"
  shows "mdist_set m A x > 0"
  by (metis Metric_space.d_set_closed_pos Metric_space_mspace_mdist assms mdist_set_def mtopology_of_def)

lemma mdist_set_uniformly_continuous: "uniformly_continuous_map m euclidean_metric (mdist_set m A)"
  unfolding uniformly_continuous_map_def
proof safe
  fix e :: real
  assume "0 < e"
  then show "δ>0. xmspace m. ymspace m. mdist m y x < δ  mdist euclidean_metric (mdist_set m A y) (mdist_set m A x) < e"
    using order.strict_trans1[OF mdist_set_abs_le] by(auto intro!: exI[where x=e] simp: dist_real_def)
qed simp

lemma uniformly_continuous_map_add:
  fixes f :: "'a  'b::real_normed_vector"
  assumes "uniformly_continuous_map m euclidean_metric f" "uniformly_continuous_map m euclidean_metric g"
  shows "uniformly_continuous_map m euclidean_metric (λx. f x + g x)"
  unfolding uniformly_continuous_map_def
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  mspace m  y  mspace m  mdist m x y < d1  dist (f x) (f y) < e / 2"    "x y. x  mspace m  y  mspace m  mdist m x y < d2  dist (g x) (g y) < e / 2"
    by(simp only: uniformly_continuous_map_def mdist_euclidean_metric) metis
  show "δ>0. ymspace m. xmspace m. mdist m x y < δ  mdist euclidean_metric (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 uniformly_continuous_map_real_divide:
  fixes f :: "'a  real"
  assumes "uniformly_continuous_map m euclidean_metric f" "uniformly_continuous_map m euclidean_metric g"
      and "x. x  mspace m  g x  0" "x. x  mspace m  ¦g x¦  a" "a > 0" "x. x  mspace m  ¦g x¦ < Kg"
      and "x. x  mspace m  ¦f x¦ < Kf"
    shows "uniformly_continuous_map m euclidean_metric (λx. f x / g x)"
  unfolding uniformly_continuous_map_def
proof safe
  fix e :: real
  assume e[arith]:"e > 0"
  consider "mspace m  {}" | "mspace m = {}" by auto
  then show "δ>0. xmspace m. ymspace m. mdist m y x < δ  mdist euclidean_metric (f y / g y) (f x / g x) < e"
  proof cases
    case m:1
    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  mspace m  y  mspace m  mdist m x y < d1  ¦f x - f y¦ < e'"    "x y. x  mspace m  y  mspace m  mdist m x y < d2  ¦g x - g y¦ < e'"
      by(simp only: uniformly_continuous_map_def mdist_euclidean_metric dist_real_def) metis
    show ?thesis
      unfolding mdist_euclidean_metric dist_real_def
    proof(safe intro!: exI[where x="min d1 d2"])
      fix x y
      assume x:"x  mspace m" and y:"y  mspace m" and "mdist m x y < min d1 d2"
      then have dist[arith]: "mdist m x y < d1" "mdist m 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 (auto intro!: exI[where x=1])
qed simp

lemma
  assumes "e > 0"
  shows uniformly_continuous_map_from_capped_metric:"uniformly_continuous_map (capped_metric e m1) m2 f  uniformly_continuous_map m1 m2 f" (is ?g1)
    and uniformly_continuous_map_to_capped_metric:"uniformly_continuous_map m1 (capped_metric e m2) f  uniformly_continuous_map m1 m2 f" (is ?g2)
proof -
  have [simp]:"(λn. min e (X n))  0  X  0" for X
  proof
    assume h:"(λn. min e (X n))  0"
    show "X  0"
      unfolding LIMSEQ_def dist_real_def
    proof safe
      fix r :: real
      assume "0 < r"
      then have "min (e / 2) r > 0"
        using assms by auto
      from LIMSEQ_D[OF h this] obtain N where N:"n. n  N  ¦min e (X n)¦ < min (e / 2) r"
        by auto
      have "min e (X n) = X n" if h:"n  N " for n
      proof(rule ccontr)
        assume "min e (X n)  X n"
        then have "min e (X n) = e"
          by auto
        with N[OF h] show False
          by auto
      qed
      with N show "no. nno. ¦X n - 0¦ < r"
        by(auto intro!: exI[where x=N])
    qed
  qed(auto intro!: tendsto_eq_intros(4)[of "λx. e" e sequentially X _ ] simp: assms)
  show ?g1 ?g2
    using assms by(auto simp: uniformly_continuous_map_sequentially capped_metric_mdist)
qed

lemma Urysohn_lemma_uniform:
  assumes "closedin (mtopology_of m) T" "closedin (mtopology_of m) U" "T  U = {}" "x y. x  T  y  U  mdist m x y  e" "e > 0"
  obtains f :: "'a  real"
  where "uniformly_continuous_map m euclidean_metric f"
        "x. f x  0" "x. f x  1" "x. x  T  f x = 1" "x. x  U  f x = 0"
proof -
  consider "T = {}" | "U = {}" | "T  {}" "U  {}" by auto
  then show ?thesis
  proof cases
    case 1
    define f where "f  (λx::'a. 0::real)"
    with 1 have "uniformly_continuous_map m euclidean_metric f" "x. f x  0" "x. f x  1" "x. x  T  f x = 1" "x. x  U  f x = 0"
      by auto
    then show ?thesis
      using that by auto
  next
    case 2
    define f where "f  (λx::'a. 1::real)"
    with 2 have "uniformly_continuous_map m euclidean_metric f" "x. f x  0" "x. f x  1" "x. x  T  f x = 1" "x. x  U  f x = 0"
      by auto
    then show ?thesis
      using that by auto
  next
    case TU:3
    then have STU:"mspace m  {}" "T  mspace m" "U  mspace m"
      using assms(1,2) closedin_topspace_empty closedin_subset by fastforce+
    interpret m: Metric_space "mspace m" "mdist (capped_metric e m)"
      by (metis Metric_space_mspace_mdist capped_metric_mspace)
    have e:"x  T  y  U  mdist (capped_metric e m) x y  e" for x y
      by (simp add: assms(4) capped_metric_mdist)
    define f where "f  (λx. mdist_set (capped_metric e m) U x / (mdist_set (capped_metric e m) U x + mdist_set (capped_metric e m) T x))"
    have "uniformly_continuous_map m euclidean_metric f"
      unfolding uniformly_continuous_map_from_capped_metric[OF assms(5),of m,symmetric] f_def
    proof(rule uniformly_continuous_map_real_divide[where Kf="e + 1" and Kg="2 * e + 1" and a="e / 2"])
      show "uniformly_continuous_map (capped_metric e m) euclidean_metric (mdist_set (capped_metric e m) U)"
           "uniformly_continuous_map (capped_metric e m) euclidean_metric (λx. mdist_set (capped_metric e m) U x + mdist_set (capped_metric e m) T x)"
        by(auto intro!: mdist_set_uniformly_continuous uniformly_continuous_map_add)
    next
      fix x
      assume x:"x  mspace (capped_metric e m)"
      then consider "x  T" | "x  U"
        using TU assms by auto
      thus "mdist_set (capped_metric e m) U x + mdist_set (capped_metric e m) T x  0"
      proof cases
        case 1
        with TU x assms have "mdist_set (capped_metric e m) T x > 0"
          by(auto intro!: mdist_set_closed_pos simp: mtopology_capped_metric)
        thus?thesis
          by (metis add_less_same_cancel2 linorder_not_less mdist_set_nonneg)
      next
        case 2
        with TU x assms have "mdist_set (capped_metric e m) U x > 0"
          by(auto intro!: mdist_set_closed_pos simp: mtopology_capped_metric)
        thus?thesis
          by (metis add_less_same_cancel1 linorder_not_less mdist_set_nonneg)
      qed
    next
      fix x
      assume x:"x  mspace (capped_metric e m)"
      consider "x  (aU. m.mball a (e / 2))" | "x  (aU. m.mball a (e / 2))" by auto
      then show "e / 2  ¦mdist_set (capped_metric e m) U x + mdist_set (capped_metric e m) T x¦"
      proof cases
        case 1
        have "m.mball x (e / 2)  T = {}"
        proof(rule ccontr)
          assume "m.mball x (e / 2)  T  {}"
          then obtain y where y: "y  m.mball x (e / 2)" "y  T"
            by blast
          then obtain u where u:"u  U" "x  m.mball u (e / 2)"
            using 1 by auto
          have "mdist (capped_metric e m) y u  mdist (capped_metric e m) y x + mdist (capped_metric e m) x u"
            using STU u y x by(auto intro!: m.triangle)
          also have "... < e / 2 + e / 2"
            using y u by(auto simp: m.commute)
          also have "... = e" using assms(5) by linarith
          finally show False
            using e[OF y(2) u(1)] by simp
        qed
        from m.d_set_ball_empty[OF _ _ _ _ this] TU STU x assms(1,5)
        have "e / 2  m.d_set T x"
          using STU(2) x by auto
        also have "...  ¦mdist_set (capped_metric e m) U x + mdist_set (capped_metric e m) T x¦"
          by (simp add: mdist_set_def)
        finally show ?thesis .
      next
        case 2
        then have "m.mball x (e / 2)  U = {}"
          using x by (auto simp: m.commute)
        hence "e / 2  m.d_set U x"
          by (metis STU(3) TU(2) assms(5) capped_metric_mspace half_gt_zero m.d_set_ball_empty x)
        also have "...  ¦mdist_set (capped_metric e m) U x + mdist_set (capped_metric e m) T x¦"
          by (simp add: mdist_set_def)
        finally show ?thesis .
      qed
    next
      fix x
      assume "x  mspace (capped_metric e m)"
      have "¦mdist_set (capped_metric e m) U x + mdist_set (capped_metric e m) T x¦ = mdist_set (capped_metric e m) U x + mdist_set (capped_metric e m) T x"
        using mdist_set_nonneg by auto
      also have "... < (e + 1 / 2) + (e + 1 / 2)"
        apply(intro add_strict_mono mdist_set_bounded)
        using assms(5) add_strict_increasing[of "1 / 2",OF _ mdist_capped[OF assms(5),of m x]] by (auto simp add: add.commute)
      also have "... = 2 * e + 1"
        by auto
      finally show "¦mdist_set (capped_metric e m) U x + mdist_set (capped_metric e m) T x¦ < 2 * e + 1" .
      show " ¦mdist_set (capped_metric e m) U x¦ < e + 1"
        using assms(5) add_strict_increasing[of 1,OF _ mdist_capped[OF assms(5),of m x]] by (auto simp add: add.commute intro!: mdist_set_bounded)
    qed(use assms in auto)
    moreover have "x. f x {0..1}"
    proof -
      fix x
      have "f x  mdist_set (capped_metric e m) U x / mdist_set (capped_metric e m) U x"
      proof -
        consider "mdist_set (capped_metric e m) U x = 0" | "mdist_set (capped_metric e m) U x > 0"
          using antisym_conv1 by fastforce
        thus ?thesis
        proof cases
          case 2
          show ?thesis
            unfolding f_def by(rule divide_left_mono[OF _ _ mult_pos_pos]) (auto simp: 2 add_strict_increasing)
        qed (simp add: f_def)
      qed
      also have "...  1" by simp
      finally show "f x  {0..1}"
        by (auto simp: f_def)
    qed      
    moreover have "f x = 1" if x:"x  T" for x
    proof -
      { assume h:"mdist_set (capped_metric e m) U x = 0"
        then have "x  U" using assms STU x by blast
        hence False
          by (metis STU(2) TU(2) assms(2) capped_metric_mspace h mdist_set_closed_pos mtopology_capped_metric order_less_irrefl subset_eq x)
      }
      thus ?thesis
        by (metis add.right_neutral divide_self_if f_def mdist_set_nzeroD(2) x)
    qed
    moreover have "x. x  U  f x = 0"
      by (simp add: f_def m.d_set_inA mdist_set_def)
    ultimately show ?thesis
      using that by auto
  qed
qed

text ‹ Open maps ›
lemma Metric_space_open_map_from_dist:
  assumes "f  mspace m1  mspace m2"
      and "x ε. x  mspace m1  ε > 0  δ>0. ymspace m1. mdist m2 (f x) (f y) < δ  mdist m1 x y < ε"
    shows "open_map (mtopology_of m1) (subtopology (mtopology_of m2) (f ` mspace m1)) f"
proof -
  interpret m1: Metric_space "mspace m1" "mdist m1" by simp
  interpret m2: Metric_space "mspace m2" "mdist m2" by simp
  interpret m2': Submetric "mspace m2" "mdist m2" "f ` mspace m1"
    using assms(1) by(auto simp: Submetric_def Submetric_axioms_def)
  have "open_map m1.mtopology m2'.sub.mtopology f"
  proof(safe intro!: open_map_with_base[OF m1.mtopology_base_in_balls])
    fix a and e :: real
    assume h:"a  mspace m1" "0 < e"
    show "openin m2'.sub.mtopology (f ` m1.mball a e)"
      unfolding m2'.sub.openin_mtopology
    proof safe
      fix x
      assume x:"x  m1.mball a e"
      then have xs:"x  mspace m1"
        by auto
      have "0 < e - mdist m1 a x"
        using x by auto
      from assms(2)[OF xs this] obtain d where d:"d > 0" "y. y  mspace m1  mdist m2 (f x) (f y) < d  mdist m1 x y < e - mdist m1 a x"
        by auto
      show "r>0. m2'.sub.mball (f x) r  f ` m1.mball a e"
      proof(safe intro!: exI[where x=d])
        fix z
        assume z:"z  m2'.sub.mball (f x) d"
        then obtain y where y:"z = f y" "y  mspace m1"
          by auto
        hence "mdist m2 (f x) (f y) < d"
          using z by simp
        hence "mdist m1 x y < e - mdist m1 a x"
          using d y by auto
        hence "mdist m1 a y < e"
          using h(1) x y m1.triangle[of a x y] by auto
        with h(1) show "z  f ` m1.mball a e"
          by(auto simp: y)
      qed fact
    qed auto
  qed
  thus "open_map (mtopology_of m1) (subtopology (mtopology_of m2) (f ` mspace m1)) f"
    by (simp add: mtopology_of_def m2'.mtopology_submetric)
qed

subsubsection ‹ Separability in Metric Spaces ›

context Metric_space
begin

text ‹ For a metric space $M$, $M$ is separable iff $M$ is second countable.›
lemma generated_by_countable_balls:
  assumes "countable U" and "mdense U"
  shows "mtopology = topology_generated_by {mball y (1 / real n) | y n. y  U}"
proof -
  have hu: "U  M" "x ε. x  M  ε > 0  mball x ε  U  {}"
    using assms by(auto simp: mdense_def)
  show ?thesis
    unfolding base_is_subbase[OF mtopology_base_in_balls,simplified subbase_in_def]
  proof(rule topology_generated_by_eq)
    fix K
    assume "K  {mball y (1 / real n) |y n. y  U}"
    then show "openin (topology_generated_by {mball a ε |a ε. a  M  0 < ε}) K"
      by(auto simp: base_is_subbase[OF mtopology_base_in_balls,simplified subbase_in_def,symmetric])
  next
    have h0:"x ε. x  M  ε > 0  yU. n. x  mball y (1 / real n)  mball y (1 / real n)  mball x ε"
    proof -
      fix x ε
      assume h: "x  M" "(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 "mball x (1 / (2 * real N))  U  {}"
        using mdense_def[of U] assms(2) h(1) hn0 by fastforce
      then obtain y where hy:
        "yU" "y  M" "y  mball x (1 / (real (2 * N)))"
        using hu by auto
      show "yU. n. x  mball y (1 / real n)  mball y (1 / real n)  mball x ε"
      proof(intro bexI[where x=y] exI[where x="2 * N"] conjI)
        show "x  mball y (1 / real (2 * N))"
          using hy(3) by (auto simp: commute)
      next
        show "mball y (1 / real (2 * N))  mball x ε"
        proof
          fix y'
          assume hy':"y'  mball y (1 / real (2 * N))"
          have "d x y' < ε" (is "?lhs < ?rhs")
          proof -
            have "?lhs  d x y + d y y'"
              using hy(2)  hy' h(1) triangle by auto
            also have "... < 1 / real (2 * N) + 1 / real (2 * N)"
              by(rule strict_ordered_ab_semigroup_add_class.add_strict_mono) (use hy(3) hy(2) hy' h(1) hy' in auto)
            finally show ?thesis
              using hn' by auto
          qed
          thus "y'  mball x ε"
            using hy' h(1) by auto
        qed
      qed fact
    qed
    fix K
    assume hk: "K  {mball a ε |a ε. a  M  0 < ε}"
    then obtain x εx where hxe:
       "x  M" "0 < εx" "K = mball x εx" by auto
    have gh:"K = ({mball y (1 / real n) | y n. y  U  mball y (1 / real n)  K})"
    proof
      show "K  ( {mball y (1 / real n) |y n. y  U  mball y (1 / real n)  K})"
      proof
        fix k
        assume hkink:"k  K"
        then have hkinS:"k  M"
          by(simp add: hxe)
        obtain εk where hek: "εk > 0" "mball k εk  K"
          by (metis Metric_space.openin_mtopology Metric_space_axioms hxe(3) hkink openin_mball)
        obtain y n where hyey:
          "y  U" "k  mball y (1 / real n)" "mball y (1 / real n)  mball k εk"
          using h0[OF hkinS hek(1)] by auto
        show "k    {mball y (1 / real n) |y n. y  U  mball y (1 / real n)  K}"
          using hek(2) hyey by blast
      qed
    qed auto
    show "openin (topology_generated_by {mball y (1 / real n) |y n. y  U}) K"
      unfolding openin_topology_generated_by_iff
      apply(rule generate_topology_on.UN[of "{mball y (1 / real n) |y n. y  U  mball y (1 / real n)  K}", simplified gh[symmetric]])
      apply(rule generate_topology_on.Basis) by auto
  qed
qed

lemma separable_space_imp_second_countable:
  assumes "separable_space mtopology"
  shows "second_countable mtopology"
proof -
  obtain U where hu:
   "countable U" "mdense U"
    using assms separable_space_def2 by blast
  show ?thesis
  proof(rule countable_base_from_countable_subbase[where 𝒪="{mball y (1 / real n) | y n. y  U}"])
    have "{mball y (1 / real n) |y n. y  U} = (λ(y,n). mball y (1 / real n)) ` (U × UNIV)"
      by auto
    also have "countable ..."
      using hu by auto
    finally show "countable {mball y (1 / real n) |y n. y  U}" .
  qed(use subbase_in_def generated_by_countable_balls[of U] hu in auto)
qed

corollary separable_space_iff_second_countable:
  "separable_space mtopology  second_countable mtopology"
  using second_countable_imp_separable_space separable_space_imp_second_countable by auto

lemma Lindelof_mdiameter:
  assumes "separable_space mtopology" "0 < e"
  shows "U. countable U   U = M  (uU. mdiameter u < ennreal e)"
proof -
  have "(u. u  {mball x (e / 3) |x. x  M}  openin mtopology u)"
    by auto
  moreover have " {mball x (e / 3) |x. x  M} = M"
    using assms by auto
  ultimately have "U'. countable U'  U'  {mball x (e / 3) |x. x  M}   U' = M"
    using second_countable_imp_Lindelof_space[OF assms(1)[simplified separable_space_iff_second_countable]]
    by(auto simp: Lindelof_space_def)
  then obtain U' where U': "countable U'" "U'  {mball x (e / 3) |x. x  M}" " U' = M"
    by auto
  show ?thesis
  proof(safe intro!: exI[where x=U'])
    fix u
    assume "u  U'"
    then obtain x where u:"u = mball x (e / 3)"
      using U' by auto
    have "mdiameter u  ennreal (2 * (e / 3))"
      by(simp only: u mdiameter_ball_leq)
    also have "... < ennreal e"
      by(auto intro!: ennreal_lessI assms)
    finally show "mdiameter u < ennreal e" .
  qed(use U' in auto)
qed

end

lemma metrizable_space_separable_iff_second_countable:
  assumes "metrizable_space X"
  shows "separable_space X  second_countable X"
proof -
  obtain d where "Metric_space (topspace X) d" "Metric_space.mtopology (topspace X) d = X"
    by (metis assms(1) Metric_space.topspace_mtopology metrizable_space_def)
  thus ?thesis
    using Metric_space.separable_space_iff_second_countable by fastforce
qed

abbreviation "mdense_of m U  dense_in (mtopology_of m) U"

lemma mdense_of_def: "mdense_of m U  (U  mspace m  (xmspace m. ε>0. mball_of m x ε  U  {}))"
  using Metric_space.mdense_def[of "mspace m" "mdist m"] by (simp add: mball_of_def mtopology_of_def)

lemma mdense_of_def2: "mdense_of m U  (U  mspace m  (xmspace m. ε>0. yU. mdist m x y < ε))"
  using Metric_space.mdense_def2[of "mspace m" "mdist m"] by (simp add: mtopology_of_def)

lemma mdense_of_def3: "mdense_of m U  (U  mspace m  (xmspace m. xn. range xn  U  limitin (mtopology_of m) xn x sequentially))"
  using Metric_space.mdense_def3[of "mspace m" "mdist m"] by (simp add: mtopology_of_def)

subsubsection ‹ Compact Metric Spaces›

context Metric_space
begin

lemma mtotally_bounded_eq_compact_closedin:
  assumes "mcomplete" "closedin mtopology S"
  shows "mtotally_bounded S  S  M  compactin mtopology S"
  by (metis assms closure_of_eq mtotally_bounded_eq_compact_closure_of)

lemma mtotally_bounded_def2: "mtotally_bounded S  (ε>0. K. finite K  K  M  S  (xK. mball x ε))"
  unfolding mtotally_bounded_def
proof safe
  fix e :: real
  assume h:"e > 0" "e>0. K. finite K  K  S  S  (xK. mball x e)"
  then show "K. finite K  K  M  S  (xK. mball x e)"
    by (metis Metric_space.mbounded_subset Metric_space.mtotally_bounded_imp_mbounded Metric_space_axioms mbounded_subset_mspace mtotally_bounded_def)
next
  fix e :: real
  assume "e > 0" "ε>0. K. finite K  K  M  S  (xK. mball x ε)"
  then obtain K where K: "finite K" "K  M" "S  (xK. mball x (e / 2))"
    by (meson half_gt_zero)
  define K' where "K'  {xK. mball x (e / 2)  S  {}}"
  have K'1:"finite K'" "K'  M"
    using K by(auto simp: K'_def)
  have K'2: "S  (xK'. mball x (e / 2))"
  proof
    fix x
    assume x:"x  S"
    then obtain k where k:"k  K" "x  mball k (e / 2)"
      using K by auto
    with x have "k  K'"
      by(auto simp: K'_def)
    with k show "x  (xK'. mball x (e / 2))"
      by auto
  qed
  have "kK'. y. y  mball k (e / 2)  S"
    by(auto simp: K'_def)
  then obtain xk where xk: "k. k  K'  xk k  mball k (e / 2)" "k. k  K'  xk k  S"
    by (metis IntD2 inf_commute)
  hence "k. k  K'  mball k (e / 2)  mball (xk k) e"
    using triangle commute by fastforce
  hence "(xK'. mball x (e / 2))  (xxk ` K'. mball x e)"
    by blast
  with K'2 have "S  (xxk ` K'. mball x e)"
    by blast
  thus "K. finite K  K  S  S  (xK. mball x e)"
    by(intro exI[where x="xk ` K'"]) (use xk(2) K'1(1) in blast)
qed

lemma compact_space_imp_separable:
  assumes "compact_space mtopology"
  shows "separable_space mtopology"
proof -
  have "A. finite A  A  M  M   ((λa. mball a (1 / real (Suc n))) ` A)" for n
    using assms by(auto simp: compact_space_eq_mcomplete_mtotally_bounded mtotally_bounded_def)
  then obtain A where A: "n. finite (A n)" "n. A n  M" "n. M    ((λa. mball 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_space mtopology"
    unfolding mdense_def2 separable_space_def2
  proof(safe intro!: exI[where x=K] 1)
    fix x and ε :: real
    assume h: "x  M" "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  mball y (1 / real (Suc n))"
      using h(1) A(3)[of n] by auto
    thus "yK. d x y < ε"
      using n by(auto intro!: bexI[where x=y] simp: commute K_def)
  qed(use K_def A(2) in auto)
qed

lemma separable_space_cfunspace:
  assumes "separable_space mtopology" mcomplete
      and "metrizable_space X" "compact_space X"
    shows "separable_space (mtopology_of (cfunspace X Self))"
proof -
  consider "topspace X = {}" | "topspace X  {}" "M = {}" | "topspace X  {}" "M  {}" by auto
  thus ?thesis
  proof cases
    case 1
    then show ?thesis
      by(auto intro!: countable_space_separable_space)
  next
    case 2
    then have [simp]:"mtopology = trivial_topology"
      using topspace_mtopology by auto
    have 1:"topspace (mtopology_of (cfunspace X Self)) = {}"
      apply simp
      using 2(1) by(auto simp: mtopology_of_def)
    show ?thesis
      by(rule countable_space_separable_space, simp only: 1) simp
  next
    case XS_nem:3
    have cm: "mcomplete_of (cfunspace X Self)"
      by (simp add: assms(2) mcomplete_cfunspace)
    show ?thesis
    proof -
      obtain dx where dx: "Metric_space (topspace X) dx" "Metric_space.mtopology (topspace X) dx = X"
        by (metis Metric_space.topspace_mtopology assms(3) metrizable_space_def)
      interpret dx: Metric_space "topspace X" dx
        by fact
      have dx_c: dx.mcomplete
        using assms by(auto intro!: dx.compact_space_imp_mcomplete simp: dx(2))
      have "B. finite B  B  topspace X  topspace X  (aB. dx.mball a (1 / Suc m))" for m
        using dx.compactin_imp_mtotally_bounded[of "topspace X"] assms(4)
        by(fastforce simp: dx(2) compact_space_def dx.mtotally_bounded_def2)
      then obtain Xm where Xm: "m. finite (Xm m)" "m. (Xm m)  topspace X" "m. topspace X  (aXm m. dx.mball a (1 / Suc m))"
        by metis
      hence Xm_eq: "m. topspace X = (aXm m. dx.mball a (1 / Suc m))"
        by fastforce
      have Xm_nem:"m. (Xm m)  {}"
        using XS_nem Xm_eq by blast
      define xmk where "xmk  (λm. from_nat_into (Xm m))"
      define km where "km  (λm. card (Xm m))"
      have km_pos:"km m > 0" for m
        by(simp add: km_def card_gt_0_iff Xm Xm_nem)
      have xmk_bij: "bij_betw (xmk m) {..<km m} (Xm m)" for m
        using bij_betw_from_nat_into_finite[OF Xm(1)] by(simp add: km_def xmk_def)
      have xmk_into: "xmk m i  Xm m" for m i
        by (simp add: Xm_nem from_nat_into xmk_def)
      have "U. countable U   U = M  (uU. mdiameter u < 1 / (Suc l))" for l
        by(rule Lindelof_mdiameter[OF assms(1)]) auto
      then obtain U where U: "l. countable (U l)" "l. ( (U l)) = M" "l u. u  U l  mdiameter u < 1 / Suc l"
        by metis
      have Ul_nem: "U l  {}" for l
        using XS_nem U(2) by auto
      define uli where "uli  (λl. from_nat_into (U l))"
      have uli_into:"uli l i  U l" for l i
        by (simp add: Ul_nem from_nat_into uli_def)
      hence uli_diam: "mdiameter (uli l i) < 1 / Suc l" for l i
        using U(3) by auto
      have uli_un:"M = (i. uli l i)" for l
        by(auto simp: range_from_nat_into[OF Ul_nem[of l] U(1)] uli_def U)
      define Cmn where "Cmn  (λm n. {f  mspace (cfunspace X Self). xtopspace X. ytopspace X. dx x y < 1 / (Suc m)  d (f x) (f y) < 1 / Suc n})"
      define fmnls where "fmnls  (λm n l s. SOME f. f  Cmn m n  (j<km m. f (xmk m j)  uli l (s j)))"
      define Dmnl where "Dmnl  (λm n l. {fmnls m n l s |s. s  {..<km m} E UNIV  (f  Cmn m n. (j<km m. f (xmk m j)  uli l (s j))) })"
      have in_Dmnl: "fmnls m n l s  Dmnl m n l" if "s{..<km m} E UNIV" "f Cmn m n" "j<km m. f (xmk m j)  uli l (s j)"for m n l s f
        using Dmnl_def that by blast
      define Dmn where "Dmn  (λm n. l. Dmnl m n l)"
      have Dmn_subset: "Dmn m n  Cmn m n" for m n
      proof -
        have "Dmnl m n l  Cmn m n" for l
          by(auto simp: Dmnl_def fmnls_def someI[of "λf. f  Cmn m n  (j<km m. f (xmk m j)  uli l (_ j))"])
        thus ?thesis by(auto simp: Dmn_def)
      qed
      have c_Dmn: "countable (Dmn m n)" for m n
      proof -
        have "countable (Dmnl m n l)" for l
        proof -
          have 1:"Dmnl m n l  (λs. fmnls m n l s) ` ({..<km m} E UNIV)"
            by(auto simp: Dmnl_def)
          have "countable ..."
            by(auto intro!: countable_PiE)
          with 1 show ?thesis
            using countable_subset by blast
        qed
        thus ?thesis
          by(auto simp: Dmn_def)
      qed
      have claim: "gDmn m n. yXm m. d (f y) (g y) < e" if f:"f  Cmn m n" and e:"e > 0" for f m n e
      proof -
        obtain l where l:"1 / Suc l < e"
          using e nat_approx_posE by blast
        define s where "s  (λi{..<km m}. SOME j. f (xmk m i)  uli l j)"
        have s1:"s{..<km m} E UNIV" by(simp add: s_def)
        have s2:"i<km m. f (xmk m i)  uli l (s i)"
        proof -
          fix i
          have "f (xmk m i)  uli l (SOME j. f (xmk m i)  uli l j)" for i
          proof(rule someI_ex)
            have "xmk m i  topspace X"
              using Xm(2) xmk_into by auto
            hence "f (xmk m i)  M"
              using f by(auto simp: Cmn_def continuous_map_def)
            thus "x. f (xmk m i)  uli l x"
              using uli_un by auto
          qed
          thus ?thesis
            by (auto simp: s_def)
        qed
        have fmnls:"fmnls m n l s  Cmn m n  (j<km m. fmnls m n l s (xmk m j)  uli l (s j))"
          by(simp add: fmnls_def,rule someI[where x=f],auto simp: s2 f)
        show "gDmn m n. yXm m. d (f y) (g y) < e"
        proof(safe intro!: bexI[where x="fmnls m n l s"])
          fix y
          assume y:"y  Xm m"
          then obtain i where i:"i < km m" "xmk m i = y"
            by (meson xmk_bij[of m] bij_betw_iff_bijections lessThan_iff)
          have "f y  uli l (s i)" "fmnls m n l s y  uli l (s i)"
            using i(1) s2 fmnls by(auto simp: i(2)[symmetric])
          moreover have "f y  M" "fmnls m n l s y  M"
            using f fmnls y Xm(2)[of m] by(auto simp: Cmn_def continuous_map_def)
          ultimately have "ennreal (d (f y) (fmnls m n l s y))  mdiameter (uli l (s i))"
            by(auto intro!: mdiameter_is_sup)
          also have "... < ennreal (1 / Suc l)"
            by(rule uli_diam)
          also have "... < ennreal e"
            using l e by(auto intro!: ennreal_lessI)
          finally show "d (f y) (fmnls m n l s y) < e"
            by(simp add: ennreal_less_iff[OF nonneg])
        qed(use in_Dmnl[OF s1 f s2] Dmn_def in auto)
      qed
      show "separable_space (mtopology_of (cfunspace X Self))"
        unfolding separable_space_def2 mdense_of_def2
      proof(safe intro!: exI[where x="n. (m. Dmn m n)"])
        fix f and e :: real
        assume h:"f   mspace (cfunspace X Self)" "0 < e"
        then obtain n where n:"1 / Suc n < e / 4"
          by (metis zero_less_divide_iff zero_less_numeral nat_approx_posE)
        have "m. l m. f  Cmn l n"
        proof -
          have "uniformly_continuous_map dx.Self Self f"
            using continuous_eq_uniformly_continuous_map[of dx.Self Self f] h assms(4) by(auto simp: mtopology_of_def dx)
          then obtain δ where δ:"δ > 0" "x y. xtopspace X  ytopspace X  dx x y < δ  d (f x) (f y) < 1 / (Suc n)"
            by(simp only: uniformly_continuous_map_def) (metis  dx.mdist_Self dx.mspace_Self mdist_Self of_nat_0_less_iff zero_less_Suc zero_less_divide_1_iff)
          then obtain m where m:"1 / Suc m < δ"
            using nat_approx_posE by blast
          have l: "l  m  1 / Suc l  1 / Suc m" for l
            by (simp add: frac_le)
          show ?thesis
            using δ(2)[OF _ _ order.strict_trans[OF _ order.strict_trans1[OF l m]]] h by(auto simp: Cmn_def)
        qed
        then obtain m where m:"f  Cmn m n" by auto
        obtain g where g:"gDmn m n" "y. yXm m  d (f y) (g y) < e / 4"
          by (metis claim[OF m] h(2) zero_less_divide_iff zero_less_numeral)
        have "n m. gDmn m n. mdist (cfunspace X Self) f g < e"
        proof(rule exI[where x=n])
          show "m. gDmn m n. mdist (cfunspace X Self) f g < e"
          proof(intro exI[where x=m] bexI[OF _ g(1)])
            have g_cm:"g  mspace (cfunspace X Self)"
              using g(1) Dmn_subset[of m n] by(auto simp: Cmn_def)
            have "mdist (cfunspace X Self) f g  3 * e / 4"
            proof(rule mdist_cfunspace_le)
              fix x
              assume x:"x  topspace X"
              obtain y where y:"y  Xm m" "x  dx.mball y (1 / real (Suc m))"
                using Xm(3) x by fastforce
              hence ytop:"y  topspace X"
                by auto
              have "mdist Self (f x) (g x)  d (f x) (f y) + d (f y) (g x)"
                using x g_cm h(1) ytop by(auto intro!: triangle simp: continuous_map_def)
              also have "...  d (f x) (f y) + d (f y) (g y) + d (g y) (g x)"
                using x g_cm h(1) ytop by(auto intro!: triangle simp: continuous_map_def)
              also have "...  e / 4 + e / 4 + e / 4"
              proof -
                have dxy: "dx x y < 1 / Suc m" "dx y x < 1 / Suc m"
                  using y(2) by(auto simp: dx.commute)
                hence "d (f x) (f y) < 1 / (Suc n)" "d (g y) (g x) < 1 / (Suc n)"
                  using m x ytop g Dmn_subset[of m n] by(auto simp: Cmn_def)
                hence "d (f x) (f y) < e / 4" "d (g y) (g x) < e / 4"
                  using n by auto
                thus ?thesis
                  using g(2)[OF y(1)] by auto
              qed
              finally show "mdist Self (f x) (g x)  3 * e / 4"
                by simp
            qed(use h in auto)
            also have "... < e"
              using h by auto
            finally show "mdist (cfunspace X Self) f g < e" .
          qed
        qed
        thus "yn m. Dmn m n. mdist (cfunspace X Self) f y  < e"
          by auto
      qed(insert Dmn_subset c_Dmn,unfold Cmn_def, blast)+
    qed
  qed
qed

end

context Submetric
begin

lemma separable_sub:
  assumes "separable_space mtopology"
  shows "separable_space sub.mtopology"
  using assms unfolding separable_space_iff_second_countable sub.separable_space_iff_second_countable
  by(auto simp: second_countable_subtopology mtopology_submetric)

end

subsubsection  ‹Discrete Distance›
lemma(in discrete_metric) separable_space_iff: "separable_space disc.mtopology  countable M"
  by(simp add: mtopology_discrete_metric separable_space_discrete_topology)

subsubsection  ‹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 "prod_dist_L1  λd1 d2 (x,y) (x',y'). d1 x x' + d2 y y'"

context Metric_space12
begin

lemma prod_L1_metric: "Metric_space (M1 × M2) (prod_dist_L1 d1 d2)"
proof
  fix x y z
  assume "x  M1 × M2" "y  M1 × M2" "z  M1 × M2"
  then show "prod_dist_L1 d1 d2 x z  prod_dist_L1 d1 d2 x y + prod_dist_L1 d1 d2 y z"
    by(auto simp: prod_dist_L1_def) (metis M1.commute M1.triangle'' M2.commute M2.triangle'' ab_semigroup_add_class.add_ac(1) add.left_commute add_mono)
qed(auto simp: prod_dist_L1_def add_nonneg_eq_0_iff M1.commute M2.commute)

sublocale Prod_metric_L1: Metric_space "M1 × M2" "prod_dist_L1 d1 d2"
  by(simp add: prod_L1_metric)

lemma prod_dist_L1_geq:
  shows "d1 x y  prod_dist_L1 d1 d2 (x,x') (y,y')"
        "d2 x' y'  prod_dist_L1 d1 d2 (x,x') (y,y')"
  by(auto simp: prod_dist_L1_def)

lemma prod_dist_L1_ball:
  assumes "(x,x')  Prod_metric_L1.mball (a,a') ε"
    shows "x  M1.mball a ε"
      and "x'  M2.mball a' ε"
  using assms prod_dist_L1_geq order.strict_trans1 by simp_all blast+

lemma prod_dist_L1_ball':
  assumes "z  Prod_metric_L1.mball a ε"
    shows "fst z  M1.mball (fst a) ε"
      and "snd z  M2.mball (snd a) ε"
  using prod_dist_L1_ball[of "fst z" "snd z" "fst a" "snd a" ε] assms by auto

lemma prod_dist_L1_ball1': "Prod_metric_L1.mball (a1,a2) (min e1 e2)  M1.mball a1 e1 × M2.mball a2 e2"
  using prod_dist_L1_geq order.strict_trans1 by auto blast+

lemma prod_dist_L1_ball1:
  assumes "b1  M1.mball a1 e1" "b2  M2.mball a2 e2"
  shows "e12>0. Prod_metric_L1.mball (b1,b2) e12  M1.mball a1 e1 × M2.mball a2 e2"
proof -
  obtain ea1 ea2 where ea: "ea1 > 0" "ea2 > 0" "M1.mball b1 ea1  M1.mball a1 e1" "M2.mball b2 ea2  M2.mball a2 e2"
    using assms by (meson M1.openin_mball M1.openin_mtopology M2.openin_mball M2.openin_mtopology)
  thus ?thesis
    using prod_dist_L1_ball1'[of b1 b2 ea1 ea2] by(auto intro!: exI[where x="min ea1 ea2"])
qed

lemma prod_dist_L1_ball2':
  "M1.mball a1 e1 × M2.mball a2 e2  Prod_metric_L1.mball (a1,a2) (e1 + e2)"
  by auto (auto simp: prod_dist_L1_def)

lemma prod_dist_L1_ball2:
  assumes "(b1,b2)  Prod_metric_L1.mball (a1,a2) e12"
    shows "e1>0. e2>0. M1.mball b1 e1 × M2.mball b2 e2  Prod_metric_L1.mball (a1,a2) e12"
proof -
  obtain e12' where "e12' > 0" "Prod_metric_L1.mball (b1,b2) e12'  Prod_metric_L1.mball (a1,a2) e12"
    by (metis assms Prod_metric_L1.openin_mball Prod_metric_L1.openin_mtopology)
  thus ?thesis
    using prod_dist_L1_ball2'[of b1 "e12' / 2" b2 "e12' / 2"] by(auto intro!: exI[where x="e12' / 2"])
qed

lemma prod_dist_L1_mtopology:
  "Prod_metric_L1.mtopology = prod_topology M1.mtopology M2.mtopology"
proof -
  have "Prod_metric_L1.mtopology = topology_generated_by { M1.mball a1 e1 × M2.mball a2 e2 | a1 a2 e1 e2. a1  M1  a2  M2  e1 > 0  e2 > 0}"
    unfolding base_is_subbase[OF Prod_metric_L1.mtopology_base_in_balls,simplified subbase_in_def]
  proof(rule topology_generated_by_eq)
    fix U
    assume "U  {M1.mball a1 e1 × M2.mball a2 e2 | a1 a2 e1 e2. a1  M1  a2  M2  0 < e1  0 < e2}"
    then obtain a1 e1 a2 e2 where hae:
    "U = M1.mball a1 e1 × M2.mball a2 e2" "a1  M1" "a2  M2" "0 < e1" "0 < e2"
      by auto
    show "openin (topology_generated_by {Prod_metric_L1.mball a ε |a ε. a  M1 × M2  0 < ε}) U"
      unfolding base_is_subbase[OF Prod_metric_L1.mtopology_base_in_balls,simplified subbase_in_def,symmetric] Prod_metric_L1.openin_mtopology hae(1)
      using prod_dist_L1_ball1[of _ a1 e1 _ a2 e2] by fastforce
  next
    fix U
    assume "U  {Prod_metric_L1.mball a ε |a ε. a  M1 × M2  0 < ε}"
    then obtain a1 a2 ε where hae:
    "U = Prod_metric_L1.mball (a1,a2) ε" "a1  M1" "a2  M2" "0 < ε"
      by auto
    show "openin (topology_generated_by {M1.mball a1 e1 × M2.mball a2 e2 | a1 a2 e1 e2. a1  M1  a2  M2  0 < e1  0 < e2}) U"
      unfolding openin_subopen[of _ "Prod_metric_L1.mball (a1,a2) ε"] hae(1)
    proof safe
      fix b1 b2
      assume h:"(b1, b2)  Prod_metric_L1.mball (a1, a2) ε"
      from prod_dist_L1_ball2[OF this] obtain e1 e2 where "e1 > 0" "e2 > 0" "M1.mball b1 e1 × M2.mball b2 e2  Prod_metric_L1.mball (a1, a2) ε"
        by metis
      with h show "T. openin (topology_generated_by {M1.mball a1 e1 × M2.mball a2 e2 | a1 a2 e1 e2. a1  M1  a2  M2  0 < e1  0 < e2}) T  (b1, b2)  T  T  Prod_metric_L1.mball (a1, a2) ε"
        unfolding openin_topology_generated_by_iff
        by(auto intro!: generate_topology_on.Basis exI[where x="M1.mball b1 e1 × M2.mball b2 e2"])
    qed
  qed
  also have "... = prod_topology M1.mtopology M2.mtopology"
  proof -
    have "{M1.mball a ε × M2.mball a' ε' |a a' ε ε'. a  M1  a'  M2  0 < ε  0 < ε'} = {U × V |U V. U  {M1.mball a ε |a ε. a  M1  0 < ε}  V  {M2.mball a ε |a ε. a  M2  0 < ε}}"
      by blast
    thus ?thesis
      unfolding base_is_subbase[OF M1.mtopology_base_in_balls,simplified subbase_in_def] base_is_subbase[OF M2.mtopology_base_in_balls,simplified subbase_in_def]
      by(simp only: prod_topology_generated_by[symmetric])
  qed
  finally show ?thesis .
qed

lemma prod_dist_L1_limitin_iff: "limitin Prod_metric_L1.mtopology zn z sequentially  limitin M1.mtopology (λn. fst (zn n)) (fst z) sequentially  limitin M2.mtopology (λn. snd (zn n)) (snd z) sequentially"
proof safe
  assume h:"limitin Prod_metric_L1.mtopology zn z sequentially"
  show "limitin M1.mtopology (λn. fst (zn n)) (fst z) sequentially"
       "limitin M2.mtopology (λn. snd (zn n)) (snd z) sequentially"
    unfolding M1.limit_metric_sequentially M2.limit_metric_sequentially
  proof safe
    fix e :: real
    assume e: "0 < e"
    with h obtain N where N:"n. n  N  zn n  M1 × M2" "n. n  N  prod_dist_L1 d1 d2 (zn n) z < e"
      by(simp only: Prod_metric_L1.limit_metric_sequentially) metis
    show "N. nN. fst (zn n)  M1  d1 (fst (zn n)) (fst z) < e"
         "N. nN. snd (zn n)  M2  d2 (snd (zn n)) (snd z) < e"
    proof(safe intro!: exI[where x=N])
      fix n
      assume "N  n"
      from N[OF this]
      show "d1 (fst (zn n)) (fst z) < e" " d2 (snd (zn n)) (snd z) < e"
        using order.strict_trans1[OF prod_dist_L1_geq(1)[of "fst (zn n)" "fst z" "snd (zn n)" "snd z"]] order.strict_trans1[OF prod_dist_L1_geq(2)[of "snd (zn n)" "snd z" "fst (zn n)" "fst z"]]
        by auto
    qed(use N(1)[simplified mem_Times_iff] in auto)
  qed(use h Prod_metric_L1.limit_metric_sequentially in auto)
next
  assume h:"limitin M1.mtopology (λn. fst (zn n)) (fst z) sequentially"
           "limitin M2.mtopology (λn. snd (zn n)) (snd z) sequentially"
  show "limitin Prod_metric_L1.mtopology zn z sequentially"
    unfolding Prod_metric_L1.limit_metric_sequentially
  proof safe
    fix e :: real
    assume e: "0 < e"
    with h obtain N1 N2 where N: "n. n  N1  fst (zn n)  M1" "n. n  N1  d1 (fst (zn n)) (fst z) < e / 2"
      "n. n  N2  snd (zn n)  M2" "n. n  N2  d2 (snd (zn n)) (snd z) < e / 2"
      unfolding M1.limit_metric_sequentially M2.limit_metric_sequentially
      using half_gt_zero by metis
    thus "N. nN. zn n  M1 × M2  prod_dist_L1 d1 d2 (zn n) z < e"
      by(fastforce intro!: exI[where x="max N1 N2"] simp: prod_dist_L1_def split_beta' mem_Times_iff)
  qed(auto simp: mem_Times_iff h[simplified M1.limit_metric_sequentially M2.limit_metric_sequentially])
qed

lemma prod_dist_L1_MCauchy_iff: "Prod_metric_L1.MCauchy zn  M1.MCauchy (λn. fst (zn n))  M2.MCauchy (λn. snd (zn n))"
proof safe
  assume h:"Prod_metric_L1.MCauchy zn"
  show "M1.MCauchy (λn. fst (zn n))" "M2.MCauchy (λn. snd (zn n))"
    unfolding M1.MCauchy_def M2.MCauchy_def
  proof safe
    fix e :: real
    assume "0 < e"
    with h obtain N where N:"n m. N  n  N  m  prod_dist_L1 d1 d2 (zn n) (zn m) < e"
      by(fastforce simp: Prod_metric_L1.MCauchy_def)
    show "N. n n'. N  n  N  n'  d1 (fst (zn n)) (fst (zn n')) < e" " N. n n'. N  n  N  n'  d2 (snd (zn n)) (snd (zn n')) < e"
    proof(safe intro!: exI[where x=N])
      fix n m
      assume "n  N" "m  N"
      from N[OF this]
      show "d1 (fst (zn n)) (fst (zn m)) < e" "d2 (snd (zn n)) (snd (zn m)) < e"
        using order.strict_trans1[OF prod_dist_L1_geq(1)[of "fst (zn n)" "fst (zn m)" "snd (zn n)" "snd (zn m)"]] order.strict_trans1[OF prod_dist_L1_geq(2)[of "snd (zn n)" "snd (zn m)" "fst (zn n)" "fst (zn m)"]]
        by auto
    qed
  next
    have "n. zn n  M1 × M2"
      using h by(auto simp: Prod_metric_L1.MCauchy_def)
    thus "fst (zn n)  M1" "snd (zn n)  M2" for n
      by (auto simp: mem_Times_iff)
  qed
next
  assume h:"M1.MCauchy (λn. fst (zn n))" "M2.MCauchy (λn. snd (zn n))"
  show "Prod_metric_L1.MCauchy zn"
    unfolding Prod_metric_L1.MCauchy_def
  proof safe
    fix e :: real
    assume "0 < e"
    with h obtain N1 N2 where "n m. n  N1  m  N1  d1 (fst (zn n)) (fst (zn m)) < e / 2"
         "n m. n  N2  m  N2  d2 (snd (zn n)) (snd (zn m)) < e / 2"
      unfolding M1.MCauchy_def M2.MCauchy_def using half_gt_zero by metis
    thus "N. n n'. N  n  N  n'  prod_dist_L1 d1 d2 (zn n) (zn n') < e"
      by(fastforce intro!: exI[where x="max N1 N2"] simp: prod_dist_L1_def split_beta')
  next
    fix x y n
    assume 1:"(x,y) = zn n"
    have "fst (zn n)  M1" "snd (zn n)  M2"
      using h[simplified M1.MCauchy_def M2.MCauchy_def] by auto
    thus "x  M1" "y  M2"
      by(simp_all add: 1[symmetric])
  qed
qed

end

subsubsection  ‹Sum Metric Spaces›
locale Sum_metric =
  fixes I :: "'i set"
    and Mi :: "'i  'a set"
    and di :: "'i  'a  'a  real"
  assumes Mi_disj: "disjoint_family_on Mi I"
      and d_nonneg: "i x y. 0  di i x y"
      and d_bounded: "i x y. di i x y < 1"
      and Md_metric: "i. i  I  Metric_space (Mi i) (di i)"
begin

abbreviation "M  iI. Mi i"

lemma Mi_inj_on:
  assumes "i  I" "j  I" "a  Mi i" "a  Mi j"
  shows "i = j"
  using Mi_disj assms by(auto simp: disjoint_family_on_def)

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

lemma sum_dist_simps:
  shows "i. i  I; x  Mi i; y  Mi i  sum_dist x y = di i x y"
    and "i j. i  I; j  I; i  j; x  Mi i; y  Mi j  sum_dist x y = 1"
    and "i. i  I; y  M; x  Mi i; y  Mi i  sum_dist x y = 1"
    and "i. i  I; x  M; y  Mi i; x  Mi i  sum_dist x y = 1"
    and "x  M  sum_dist x y = 0" "y  M  sum_dist x y = 0"
proof -
  { fix i
    assume h:"i  I" "x  Mi i" "y  Mi i"
    then have "sum_dist x y = di (THE i. i  I  x  Mi i  y  Mi i) x y"
      by(auto simp: sum_dist_def)
    also have "... = di i x y"
    proof -
      have "(THE i. i  I  x  Mi i  y  Mi i) = i"
        using Mi_disj 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  Mi i; y  Mi j  sum_dist x y = 1"
       "i. i  I; y  M; x  Mi i; y  Mi i  sum_dist x y = 1" "i. i  I; x  M; y  Mi i; x  Mi i  sum_dist x y = 1"
       "x  M  sum_dist x y = 0" "y  M  sum_dist x y = 0"
    using Mi_disj by(auto simp: sum_dist_def disjoint_family_on_def dest: Mi_inj_on)
qed

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

lemma inM_cases:
  assumes "x  M" "y  M"
      and "i. i  I; x  Mi i; y  Mi i  P x y"
      and "i j. i  I; j  I; i  j; x  Mi i; y  Mi j; x  y  P x y"
    shows "P x y" using assms by auto

sublocale Sum_metric: Metric_space M sum_dist
proof
  fix x y
  assume "x  M" "y  M"
  then show "sum_dist x y = 0  x = y"
    by(rule inM_cases, insert Md_metric) (auto simp: sum_dist_simps Metric_space_def)
next
  { fix i x y
    assume h: "i  I" "x  Mi i" "y  Mi i"
    then have "sum_dist x y = di i x y"
              "sum_dist y x = di i x y"
      using Md_metric by(auto simp: sum_dist_simps Metric_space_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  M" "y  M" "z  M"
  show "sum_dist x z  sum_dist x y + sum_dist y z" (is "?lhs  ?rhs")
  proof(rule inM_cases[OF h(1,3)])
    fix i
    assume h':"i  I" "x  Mi i" "z  Mi i"
    consider "y  Mi i" | "y  Mi i" by auto
    thus "?lhs  ?rhs"
    proof cases
      case 1
      with h' Md_metric [OF h'(1)] show ?thesis
        by(simp add: sum_dist_simps Metric_space_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  Mi i" "z  Mi j"
    consider "y  Mi i" | "y  Mi j"
      using h' h(2) Mi_disj 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

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  Mi i"
  shows "Metric_space.mball (Mi i) (di i) x e = Sum_metric.mball x e"
proof -
  interpret m: Metric_space "Mi i" "di i"
    by(simp add: assms Md_metric)
  show ?thesis
    using assms sum_dist_simps(1)[OF assms(1) assms(3)] sum_dist_if_less1[OF assms(1,3)]
    by(fastforce simp: Sum_metric.mball_def)
qed

lemma ball_le_sum_dist_ball:
  assumes "i  I"
  shows "Metric_space.mball (Mi i) (di i) x e  Sum_metric.mball x e"
proof -
  interpret m: Metric_space "Mi i" "di i"
    by(simp add: assms Md_metric)
  show ?thesis
    using assms by(auto simp: sum_dist_simps)
qed

lemma openin_mtopology_iff:
 "openin Sum_metric.mtopology U  U  M  (iI. openin (Metric_space.mtopology (Mi i) (di i)) (U  Mi i))"
proof safe
  fix i
  assume h:"openin Sum_metric.mtopology U" "i  I"
  then interpret m: Metric_space "Mi i" "di i"
    using Md_metric by simp
  show "openin m.mtopology (U  Mi i)"
    unfolding m.openin_mtopology
  proof safe
    fix x
    assume x:"x  U" "x  Mi i"
    with h obtain e where e: "e > 0" "Sum_metric.mball x e  U"
      by(auto simp: Sum_metric.openin_mtopology)
    show "ε>0. m.mball x ε  U  Mi i"
    proof(safe intro!: exI[where x=e])
      fix y
      assume "y  m.mball x e"
      with h(2) have "y  Sum_metric.mball x e"
        by(auto simp:sum_dist_simps)
      with e show "y  U" by blast
    qed(use e in auto)
  qed
next
  show "x. openin Sum_metric.mtopology U  x  U  x  M"
    by(auto simp: Sum_metric.openin_mtopology)
next
  assume h: "U  M" "iI. openin (Metric_space.mtopology (Mi i) (di i)) (U  Mi i)"
  show "openin Sum_metric.mtopology U"
    unfolding Sum_metric.openin_mtopology
  proof safe
    fix x
    assume x: "x  U"
    then obtain i where i: "i  I" "x  Mi i"
      using h(1) by auto
    then interpret m: Metric_space "Mi i" "di i"
      using Md_metric by simp
    obtain e where e: "e > 0" "m.mball x e  U  Mi i"
      using i h(2) by (meson IntI m.openin_mtopology x)
    show "ε>0. Sum_metric.mball x ε  U"
    proof(safe intro!: exI[where x="min e 1"])
      fix y
      assume y:"y  Sum_metric.mball x (min e 1)"
      then show "y  U"
        using sum_dist_ball_eq_ball[OF i(1) _ i(2),of "min e 1"] e by fastforce
    qed(simp add: e)
  qed(use h(1) in auto)
qed

corollary openin_mtopology_Mi:
  assumes "i  I"
  shows "openin Sum_metric.mtopology (Mi i)"
  unfolding openin_mtopology_iff
proof safe
  fix j
  assume j:"j  I"
  then interpret m: Metric_space "Mi j" "di j"
    by(simp add: Md_metric)
  show "openin m.mtopology (Mi i  Mi j)"
    by (cases "i = j", insert assms Mi_disj j) (auto simp: disjoint_family_on_def)
qed(use assms in auto)

corollary subtopology_mtopology_Mi:
  assumes "i  I"
  shows "subtopology Sum_metric.mtopology (Mi i) = Metric_space.mtopology (Mi i) (di i)"
proof -
  interpret Mi: Metric_space "Mi i" "di i"
    by (simp add: Md_metric assms)
  show ?thesis
    unfolding topology_eq openin_subtopology
  proof safe
    fix T
    assume "openin Sum_metric.mtopology T"
    thus "openin Mi.mtopology (T  Mi i)"
      using assms by(auto simp: openin_mtopology_iff)
  next
    fix S
    assume h:"openin Mi.mtopology S"
    show "T. openin Sum_metric.mtopology T  S = T  Mi i"
    proof(safe intro!: exI[where x=S])
      show "openin Sum_metric.mtopology S"
        unfolding openin_mtopology_iff
      proof safe
        fix j
        assume j:"j  I"
        then interpret Mj: Metric_space "Mi j" "di j"
          using Md_metric by auto
        have "i  j  S  Mi j = {}"
          using openin_subset[OF h] Mi_disj j assms
          by(auto simp: disjoint_family_on_def)
        thus "openin Mj.mtopology (S  Mi j)"
          by(cases "i = j") (use openin_subset[OF h] h in auto)
      qed(use openin_subset[OF h] assms in auto)
    qed(use openin_subset[OF h] assms in auto)
  qed
qed

lemma limitin_Mi_limitin_M:
  assumes "i  I" "limitin (Metric_space.mtopology (Mi i) (di i)) xn x sequentially"
  shows "limitin Sum_metric.mtopology xn x sequentially"
proof -
  interpret m: Metric_space "Mi i" "di i"
    by(simp add: assms Md_metric)
  {
    fix e :: real
    assume "e > 0"
    then obtain N where "n. n  N  xn n  m.mball x e"
      using assms(2) m.commute m.limit_metric_sequentially by fastforce
    hence "N. nN. xn n  Sum_metric.mball x e"
      using ball_le_sum_dist_ball[OF assms(1),of x e]
      by(fastforce intro!: exI[where x=N]) }
  thus ?thesis
    by (metis Sum_metric.commute Sum_metric.in_mball Sum_metric.limit_metric_sequentially UN_I m.limitin_mspace assms)
qed

lemma limitin_M_limitin_Mi:
  assumes "limitin Sum_metric.mtopology xn x sequentially"
  shows "iI. limitin (Metric_space.mtopology (Mi i) (di i)) xn x sequentially"
proof -
  obtain i where i: "i  I" "x  Mi i"
    using assms by (meson Sum_metric.limitin_mspace UN_E)
  then interpret m: Metric_space "Mi i" "di i"
    by(simp add: Md_metric)
  obtain N where N: "n. n  N  sum_dist (xn n) x < 1" "n. n  N  (xn n)  M"
    using assms by (metis d_bounded i(2) m.mdist_zero Sum_metric.limit_metric_sequentially)
  hence xni: "n  N  xn n  Mi i" for n
    using assms by(auto intro!: sum_dist_if_less1[OF i,of "xn n"] simp: Sum_metric.commute)
  show ?thesis
  proof(safe intro!: bexI[where x=i] i)
    show "limitin m.mtopology xn x sequentially"
      unfolding m.limit_metric_sequentially
    proof safe
      fix e :: real
      assume e: "0 < e"
      then obtain N' where N': "n. n  N'  sum_dist (xn n) x < e"
        using assms by (meson Sum_metric.limit_metric_sequentially)
      hence "n  max N N'  di i (xn n) x < e" for n
        using sum_dist_simps(1)[OF i(1) xni[of n] i(2),symmetric] by auto        
      thus "N. nN. xn n  Mi i  di i (xn n) x < e"
        using xni by(auto intro!: exI[where x="max N N'"])
    qed fact
  qed
qed

lemma MCauchy_Mi_MCauchy_M:
  assumes "i  I" "Metric_space.MCauchy (Mi i) (di i) xn"
  shows "Sum_metric.MCauchy xn"
proof -
  interpret m: Metric_space "Mi i" "di i"
    by(simp add: assms Md_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),of "xn n" "xn m"]
    by(auto simp: m.MCauchy_def)
  show ?thesis
    using assms by(auto simp: m.MCauchy_def Sum_metric.MCauchy_def)
qed

lemma MCauchy_M_MCauchy_Mi:
  assumes "Sum_metric.MCauchy xn"
  shows "m. iI. Metric_space.MCauchy (Mi i) (di i) (λn. xn (n + m))"
proof -
  obtain N where N: "n m. n  N  m  N  sum_dist (xn n) (xn m) < 1"
    using assms by(fastforce simp: Sum_metric.MCauchy_def)
  obtain i where i: "i  I" "xn N  Mi i"
    by (metis assms Sum_metric.MCauchy_def UNIV_I UN_E image_eqI subsetD)
  then have xn:"n. n  N  xn n  Mi i"
    by (metis N Sum_metric.MCauchy_def assms dual_order.refl range_subsetD sum_dist_if_less1)
  interpret m: Metric_space "Mi i" "di i"
    using i Md_metric by auto
  show ?thesis
  proof(safe intro!: exI[where x=N] bexI[where x=i])
    show "m.MCauchy (λn. xn (n + N))"
      unfolding m.MCauchy_def
    proof safe
      show 1: "n. xn (n + N)  Mi i"
        by(auto intro!: xn)
      fix e :: real
      assume "0 < e"
      then obtain N' where N': "n m. n  N'  m  N'  sum_dist (xn n) (xn m) < e"
        using Sum_metric.MCauchy_def assms by blast
      thus "N'. n n'. N'  n  N'  n'  di i (xn (n + N)) (xn (n' + N)) < e"
        by(auto intro!: exI[where x="N'"] simp: sum_dist_simps(1)[OF i(1) xn xn,symmetric])
    qed
  qed fact
qed

lemma separable_Mi_separable_M:
  assumes "countable I" "i. i  I  separable_space (Metric_space.mtopology (Mi i) (di i))"
  shows "separable_space Sum_metric.mtopology"
proof -
  obtain Ui where Ui: "i. i  I  countable (Ui i)" "i. i  I  dense_in (Metric_space.mtopology (Mi i) (di i)) (Ui i)"
    using assms by(simp only: separable_space_def2) metis
  define U where "U  iI. Ui i"
  show "separable_space Sum_metric.mtopology"
    unfolding separable_space_def2
  proof(safe intro!: exI[where x=U])
    show "countable U"
      using Ui(1) assms by(auto simp: U_def)
  next
    show "Sum_metric.mdense U"
      unfolding Sum_metric.mdense_def U_def
    proof safe
      fix i x
      assume "i  I" "x  Ui i"
      then show "x  M"
        using Ui(2) by(auto intro!: bexI[where x=i] simp: Md_metric Metric_space.mdense_def2)
    next
      fix i x e
      assume h:"i  I" "x  Mi i" "(0 :: real) < e" "Sum_metric.mball x e   (Ui ` I) = {}"
      then interpret m: Metric_space "Mi i" "di i"
        by(simp add: Md_metric)
      have "m.mball x e  Ui i  {}"
        using Ui(2)[OF h(1)] h by(auto simp: m.mdense_def)
      hence "m.mball 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

lemma separable_M_separable_Mi:
  assumes "separable_space Sum_metric.mtopology" "i. i  I"
  shows "separable_space (Metric_space.mtopology (Mi i) (di i))"
  using subtopology_mtopology_Mi[OF assms(2)] separable_space_open_subset[OF assms(1) openin_mtopology_Mi[OF assms(2)]]
  by simp

lemma mcomplete_Mi_mcomplete_M:
  assumes "i. i  I  Metric_space.mcomplete (Mi i) (di i)"
  shows Sum_metric.mcomplete
  unfolding Sum_metric.mcomplete_def
proof safe
  fix xn
  assume "Sum_metric.MCauchy xn"
  from MCauchy_M_MCauchy_Mi[OF this] obtain m i where mi:
  "i  I" "Metric_space.MCauchy (Mi i) (di i) (λn. xn (n + m))"
    by metis
  then interpret m: Metric_space "Mi i" "di i"
    by(simp add: Md_metric)
  from assms[OF mi(1)] mi(2) obtain x where x: "limitin m.mtopology (λn. xn (n + m)) x sequentially"
    by(auto simp: m.mcomplete_def)
  from limitin_Mi_limitin_M[OF mi(1) limitin_sequentially_offset_rev[OF this]]
  show "x. limitin Sum_metric.mtopology xn x sequentially"
    by auto
qed

lemma mcomplete_M_mcomplete_Mi:
  assumes Sum_metric.mcomplete "i  I"
  shows "Metric_space.mcomplete (Mi i) (di i)"
proof -
  interpret Mi: Metric_space "Mi i" "di i"
    using assms(2) Md_metric by fastforce
  show ?thesis
    unfolding Mi.mcomplete_def
  proof safe
    fix xn
    assume xn:"Mi.MCauchy xn"
    from MCauchy_Mi_MCauchy_M[OF assms(2) this] assms(1) obtain x where "limitin Sum_metric.mtopology xn x sequentially"
      by(auto simp: Sum_metric.mcomplete_def)
    from limitin_M_limitin_Mi[OF this] obtain j where j:"j  I" "limitin (Metric_space.mtopology (Mi j) (di j)) xn x sequentially"
      by auto
    have "j = i"
    proof -
      obtain N where "n. n  N  xn n  Mi j"
        by (metis Md_metric Metric_space.limitin_metric_dist_null eventually_sequentially j)
      hence "xn N  Mi i  Mi j"
        using xn by(auto simp: Mi.MCauchy_def)
      with Mi_disj j(1) assms(2) show ?thesis
        by(fastforce simp: disjoint_family_on_def)
    qed
    thus "x. limitin Mi.mtopology xn x sequentially"
      using j(2) by(auto intro!: exI[where x=x])
  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_space (Si i) (di i)"
    shows "Sum_metric I Si di"
  using assms by (metis Metric_space.nonneg Sum_metric_def) 

(* TDODO?: Sum metric space for Abstract type *)

end