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. ∀n≥N. 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. ∀n≥N. 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. ∀n≥N. xn n ∈ mball x r"
    by(auto intro!: exI[where x=N] simp:commute)
  with r show "∃N. ∀n≥N. xn n ∈ U"
    by blast
next
  fix x
  assume h:"U ⊆ M" "∀xn x. limitin mtopology xn x sequentially ∧ x ∈ U ⟶ (∃N. ∀n≥N. 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. ∃xn∈mball 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. ∀n≥N. 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 = {x∈M∩A. ∀xn. range xn ⊆ A ∧ limitin mtopology xn x sequentially ⟶ (∃no. ∀n≥no. 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. ∀n≥no. 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. ∀n≥N. ¦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 ∧ (∀x∈M. ∀ε>0. mball x ε ∩ U ≠ {})"
proof safe
  assume h:" U ⊆ M" "(∀x∈M. ∀ε>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 "(⋃u∈U. 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 ∧ (∀x∈M. ∀ε>0.∃y∈U. d x y < ε)"
proof safe
  fix x e
  assume h: "mdense U" and hxe: "x ∈ M" "(0 :: real) < e"
  then have "x ∈ (⋃u∈U. mball u e)"
    by(simp add: mdense_balls_cover)
  thus "∃y∈U. d x y < e"
    by (fastforce simp: commute)
qed(fastforce simp: mdense_def)+

lemma mdense_def3:
 "mdense U ⟷ U ⊆ M ∧ (∀x∈M. ∃xn. range xn ⊆ U ∧ limitin mtopology xn x sequentially)"
  unfolding mdense_def
proof safe
  fix x
  assume h: "U ⊆ M" "∀x∈M. ∀ε>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. ∀n≥N. 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" " ∀x∈M. ∃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. a∈A}"
    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 "... = (⨅a∈A. 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. ∀x∈mspace m. ∀y∈mspace 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. ∀y∈mspace m. ∀x∈mspace 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. ∀x∈mspace m. ∀y∈mspace 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. ∀n≥no. ¦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 ∈ (⋃a∈U. m.mball a (e / 2))" | "x ∉ (⋃a∈U. 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. ∀y∈mspace 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 ⟹ ∃y∈U. ∃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:
        "y∈U" "y ∈ M" "y ∈ mball x (1 / (real (2 * N)))"
        using hu by auto
      show "∃y∈U. ∃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 ∧ (∀u∈U. 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 ∧ (∀x∈mspace 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 ∧ (∀x∈mspace m. ∀ε>0. ∃y∈U. 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 ∧ (∀x∈mspace 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 ⊆ (⋃x∈K. mball x ε))"
  unfolding mtotally_bounded_def
proof safe
  fix e :: real
  assume h:"e > 0" "∀e>0. ∃K. finite K ∧ K ⊆ S ∧ S ⊆ (⋃x∈K. mball x e)"
  then show "∃K. finite K ∧ K ⊆ M ∧ S ⊆ (⋃x∈K. 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 ⊆ (⋃x∈K. mball x ε)"
  then obtain K where K: "finite K" "K ⊆ M" "S ⊆ (⋃x∈K. mball x (e / 2))"
    by (meson half_gt_zero)
  define K' where "K' ≡ {x∈K. mball x (e / 2) ∩ S ≠ {}}"
  have K'1:"finite K'" "K' ⊆ M"
    using K by(auto simp: K'_def)
  have K'2: "S ⊆ (⋃x∈K'. 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 ∈ (⋃x∈K'. mball x (e / 2))"
      by auto
  qed
  have "∀k∈K'. ∃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 "(⋃x∈K'. mball x (e / 2)) ⊆ (⋃x∈xk ` K'. mball x e)"
    by blast
  with K'2 have "S ⊆ (⋃x∈xk ` K'. mball x e)"
    by blast
  thus "∃K. finite K ∧ K ⊆ S ∧ S ⊆ (⋃x∈K. 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 "∃y∈K. 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 ⊆ (⋃a∈B. 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 ⊆ (⋃a∈Xm m. dx.mball a (1 / Suc m))"
        by metis
      hence Xm_eq: "⋀m. topspace X = (⋃a∈Xm 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 ∧ (∀u∈U. 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). ∀x∈topspace X. ∀y∈topspace 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: "∃g∈Dmn m n. ∀y∈Xm 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 "∃g∈Dmn m n. ∀y∈Xm 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. x∈topspace X ⟹ y∈topspace 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:"g∈Dmn m n" "⋀y. y∈Xm 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. ∃g∈Dmn m n. mdist (cfunspace X Self) f g < e"
        proof(rule exI[where x=n])
          show "∃m. ∃g∈Dmn 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 "∃y∈⋃n 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. ∀n≥N. fst (zn n) ∈ M1 ∧ d1 (fst (zn n)) (fst z) < e"
         "∃N. ∀n≥N. 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. ∀n≥N. 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 ≡ ⋃i∈I. 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 ∃i∈I. 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 ∧ (∀i∈I. 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" "∀i∈I. 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. ∀n≥N. 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 "∃i∈I. 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. ∀n≥N. 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. ∃i∈I. 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 ≡ ⋃i∈I. 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