section ‹Abstract Metric Spaces›

theory Abstract_Metric_Spaces
  imports Elementary_Metric_Spaces Abstract_Limits Abstract_Topological_Spaces
begin

(*Avoid a clash with the existing metric_space locale (from the type class)*)
locale Metric_space =
  fixes M :: "'a set" and d :: "'a → 'a → real"
  assumes nonneg [simp]: "∧x y. 0 ≤ d x y"
  assumes commute: "∧x y. d x y = d y x"
  assumes zero [simp]: "∧x y. [x ∈ M; y ∈ M] ==> d x y = 0 ⟷ x=y"
  assumes triangle: "∧x y z. [x ∈ M; y ∈ M; z ∈ M] ==> d x z ≤ d x y + d y z"

text ‹Link with the type class version›
interpretation Met_TC: Metric_space UNIV dist
  by (simp add: dist_commute dist_triangle Metric_space.intro)

context Metric_space
begin

lemma subspace: "M' ⊆ M ==> Metric_space M' d"
  by (simp add: commute in_mono Metric_space.intro triangle)

lemma abs_mdist [simp] : "∣d x y∣ = d x y"
  by simp

lemma mdist_pos_less: "[x ≠ y; x ∈ M; y ∈ M] ==> 0 < d x y"
  by (metis less_eq_real_def nonneg zero)

lemma mdist_zero [simp]: "x ∈ M ==> d x x = 0"
  by simp

lemma mdist_pos_eq [simp]: "[x ∈ M; y ∈ M] ==> 0 < d x y ⟷ x ≠ y"
  using mdist_pos_less zero by fastforce

lemma triangle': "[x ∈ M; y ∈ M; z ∈ M] ==> d x z ≤ d x y + d z y"
  by (simp add: commute triangle)

lemma triangle'': "[x ∈ M; y ∈ M; z ∈ M] ==> d x z ≤ d y x + d y z"
  by (simp add: commute triangle)

lemma mdist_reverse_triangle: "[x ∈ M; y ∈ M; z ∈ M] ==> ∣d x y - d y z∣ ≤ d x z"
  by (smt (verit) commute triangle)

text‹ Open and closed balls ›

definition mball where "mball x r ≡ {y. x ∈ M ∧ y ∈ M ∧ d x y < r}"
definition mcball where "mcball x r ≡ {y. x ∈ M ∧ y ∈ M ∧ d x y ≤ r}"

lemma in_mball [simp]: "y ∈ mball x r ⟷ x ∈ M ∧ y ∈ M ∧ d x y < r"
  by (simp add: mball_def)

lemma centre_in_mball_iff [iff]: "x ∈ mball x r ⟷ x ∈ M ∧ 0 < r"
  using in_mball mdist_zero by force

lemma mball_subset_mspace: "mball x r ⊆ M"
  by auto

lemma mball_eq_empty: "mball x r = {} ⟷ (x ∉ M) ∨ r ≤ 0"
  by (smt (verit, best) Collect_empty_eq centre_in_mball_iff mball_def nonneg)

lemma mball_subset: "[d x y + a ≤ b; y ∈ M] ==> mball x a ⊆ mball y b"
  by (smt (verit) commute in_mball subsetI triangle)

lemma disjoint_mball: "r + r' ≤ d x x' ==> disjnt (mball x r) (mball x' r')"
  by (smt (verit) commute disjnt_iff in_mball triangle)

lemma mball_subset_concentric: "r ≤ s ==> mball x r ⊆ mball x s"
  by auto

lemma in_mcball [simp]: "y ∈ mcball x r ⟷ x ∈ M ∧ y ∈ M ∧ d x y ≤ r"
  by (simp add: mcball_def)

lemma centre_in_mcball_iff [iff]: "x ∈ mcball x r ⟷ x ∈ M ∧ 0 ≤ r"
  using mdist_zero by force

lemma mcball_eq_empty: "mcball x r = {} ⟷ (x ∉ M) ∨ r < 0"
  by (smt (verit, best) Collect_empty_eq centre_in_mcball_iff empty_iff mcball_def nonneg)

lemma mcball_subset_mspace: "mcball x r ⊆ M"
  by auto

lemma mball_subset_mcball: "mball x r ⊆ mcball x r"
  by auto

lemma mcball_subset: "[d x y + a ≤ b; y ∈ M] ==> mcball x a ⊆ mcball y b"
  by (smt (verit) in_mcball mdist_reverse_triangle subsetI)

lemma mcball_subset_concentric: "r ≤ s ==> mcball x r ⊆ mcball x s"
  by force

lemma mcball_subset_mball: "[d x y + a < b; y ∈ M] ==> mcball x a ⊆ mball y b"
  by (smt (verit) commute in_mball in_mcball subsetI triangle)

lemma mcball_subset_mball_concentric: "a < b ==> mcball x a ⊆ mball x b"
  by force

end



subsection ‹Metric topology ›

context Metric_space
begin

definition mopen where 
  "mopen U ≡ U ⊆ M ∧ (∀x. x ∈ U ⟶ (∃r>0. mball x r ⊆ U))"

definition mtopology :: "'a topology" where 
  "mtopology ≡ topology mopen"

lemma is_topology_metric_topology [iff]: "istopology mopen"
proof -
  have "∧S T. [mopen S; mopen T] ==> mopen (S ∩ T)"
    by (smt (verit, del_insts) Int_iff in_mball mopen_def subset_eq)
  moreover have "∧K. (∀K∈K. mopen K) ⟶ mopen (∪K)"
    using mopen_def by fastforce
  ultimately show ?thesis
    by (simp add: istopology_def)
qed

lemma openin_mtopology: "openin mtopology U ⟷ U ⊆ M ∧ (∀x. x ∈ U ⟶ (∃r>0. mball x r ⊆ U))"
  by (simp add: mopen_def mtopology_def)

lemma topspace_mtopology [simp]: "topspace mtopology = M"
  by (meson order.refl mball_subset_mspace openin_mtopology openin_subset openin_topspace subset_antisym zero_less_one)

lemma subtopology_mspace [simp]: "subtopology mtopology M = mtopology"
  by (metis subtopology_topspace topspace_mtopology)

lemma open_in_mspace [iff]: "openin mtopology M"
  by (metis openin_topspace topspace_mtopology)

lemma closedin_mspace [iff]: "closedin mtopology M"
  by (metis closedin_topspace topspace_mtopology)

lemma openin_mball [iff]: "openin mtopology (mball x r)"
proof -
  have "∧y. [x ∈ M; d x y < r] ==> ∃s>0. mball y s ⊆ mball x r"
    by (metis add_diff_cancel_left' add_diff_eq commute less_add_same_cancel1 mball_subset order_refl)
  then show ?thesis
    by (auto simp: openin_mtopology)
qed

lemma mtopology_base:
   "mtopology = topology(arbitrary union_of (λU. ∃x ∈ M. ∃r>0. U = mball x r))"
proof -
  have "∧S. ∃x r. x ∈ M ∧ 0 < r ∧ S = mball x r ==> openin mtopology S"
    using openin_mball by blast
  moreover have "∧U x. [openin mtopology U; x ∈ U] ==> ∃B. (∃x r. x ∈ M ∧ 0 < r ∧ B = mball x r) ∧ x ∈ B ∧ B ⊆ U"
    by (metis centre_in_mball_iff in_mono openin_mtopology)
  ultimately show ?thesis
    by (smt (verit) topology_base_unique)
qed

lemma closedin_metric:
   "closedin mtopology C ⟷ C ⊆ M ∧ (∀x. x ∈ M - C ⟶ (∃r>0. disjnt C (mball x r)))"  (is "?lhs = ?rhs")
proof
  show "?lhs ==> ?rhs"
    unfolding closedin_def openin_mtopology
    by (metis Diff_disjoint disjnt_def disjnt_subset2 topspace_mtopology)
  show "?rhs ==> ?lhs"
    unfolding closedin_def openin_mtopology disjnt_def
    by (metis Diff_subset Diff_triv Int_Diff Int_commute inf.absorb_iff2 mball_subset_mspace topspace_mtopology)
qed

lemma closedin_mcball [iff]: "closedin mtopology (mcball x r)"
proof -
  have "∃ra>0. disjnt (mcball x r) (mball y ra)" if "x ∉ M" for y
    by (metis disjnt_empty1 gt_ex mcball_eq_empty that)
  moreover have "disjnt (mcball x r) (mball y (d x y - r))" if "y ∈ M" "d x y > r" for y
    using that disjnt_iff in_mball in_mcball mdist_reverse_triangle by force
  ultimately show ?thesis
    using closedin_metric mcball_subset_mspace by fastforce
qed

lemma mball_iff_mcball: "(∃r>0. mball x r ⊆ U) = (∃r>0. mcball x r ⊆ U)"
  by (meson dense mball_subset_mcball mcball_subset_mball_concentric order_trans)

lemma openin_mtopology_mcball:
  "openin mtopology U ⟷ U ⊆ M ∧ (∀x. x ∈ U ⟶ (∃r. 0 < r ∧ mcball x r ⊆ U))"
  by (simp add: mball_iff_mcball openin_mtopology)

lemma metric_derived_set_of:
  "mtopology derived_set_of S = {x ∈ M. ∀r>0. ∃y∈S. y≠x ∧ y ∈ mball x r}" (is "?lhs=?rhs")
proof
  show "?lhs ⊆ ?rhs"
    unfolding openin_mtopology derived_set_of_def
    by clarsimp (metis in_mball openin_mball openin_mtopology zero)
  show "?rhs ⊆ ?lhs"
    unfolding openin_mtopology derived_set_of_def 
    by clarify (metis subsetD topspace_mtopology)
qed

lemma metric_closure_of:
   "mtopology closure_of S = {x ∈ M. ∀r>0. ∃y ∈ S. y ∈ mball x r}"
proof -
  have "∧x r. [0 < r; x ∈ mtopology closure_of S] ==> ∃y∈S. y ∈ mball x r"
    by (metis centre_in_mball_iff in_closure_of openin_mball topspace_mtopology)
  moreover have "∧x T. [x ∈ M; ∀r>0. ∃y∈S. y ∈ mball x r] ==> x ∈ mtopology closure_of S"
    by (smt (verit) in_closure_of in_mball openin_mtopology subsetD topspace_mtopology)
  ultimately show ?thesis
    by (auto simp: in_closure_of)
qed

lemma metric_closure_of_alt:
  "mtopology closure_of S = {x ∈ M. ∀r>0. ∃y ∈ S. y ∈ mcball x r}"
proof -
  have "∧x r. [∀r>0. x ∈ M ∧ (∃y∈S. y ∈ mcball x r); 0 < r] ==> ∃y∈S. y ∈ M ∧ d x y < r"
    by (meson dense in_mcball le_less_trans)
  then show ?thesis
    by (fastforce simp: metric_closure_of in_closure_of)
qed

lemma metric_interior_of:
   "mtopology interior_of S = {x ∈ M. ∃ε>0. mball x ε ⊆ S}" (is "?lhs=?rhs")
proof
  show "?lhs ⊆ ?rhs"
    using interior_of_maximal_eq openin_mtopology by fastforce
  show "?rhs ⊆ ?lhs"
    using interior_of_def openin_mball by fastforce
qed

lemma metric_interior_of_alt:
   "mtopology interior_of S = {x ∈ M. ∃ε>0. mcball x ε ⊆ S}"
  by (fastforce simp: mball_iff_mcball metric_interior_of)

lemma in_interior_of_mball:
   "x ∈ mtopology interior_of S ⟷ x ∈ M ∧ (∃ε>0. mball x ε ⊆ S)"
  using metric_interior_of by force

lemma in_interior_of_mcball:
   "x ∈ mtopology interior_of S ⟷ x ∈ M ∧ (∃ε>0. mcball x ε ⊆ S)"
  using metric_interior_of_alt by force

lemma Hausdorff_space_mtopology: "Hausdorff_space mtopology"
  unfolding Hausdorff_space_def
proof clarify
  fix x y
  assume x: "x ∈ topspace mtopology" and y: "y ∈ topspace mtopology" and "x ≠ y"
  then have gt0: "d x y / 2 > 0"
    by auto
  have "disjnt (mball x (d x y / 2)) (mball y (d x y / 2))"
    by (simp add: disjoint_mball)
  then show "∃U V. openin mtopology U ∧ openin mtopology V ∧ x ∈ U ∧ y ∈ V ∧ disjnt U V"
    by (metis centre_in_mball_iff gt0 openin_mball topspace_mtopology x y)
qed

subsection‹Bounded sets›

definition mbounded where "mbounded S ⟷ (∃x B. S ⊆ mcball x B)"

lemma mbounded_pos: "mbounded S ⟷ (∃x B. 0 < B ∧ S ⊆ mcball x B)"
proof -
  have "∃x' r'. 0 < r' ∧ S ⊆ mcball x' r'" if "S ⊆ mcball x r" for x r
    by (metis gt_ex less_eq_real_def linorder_not_le mcball_subset_concentric order_trans that)
  then show ?thesis
    by (auto simp: mbounded_def)
qed

lemma mbounded_alt:
  "mbounded S ⟷ S ⊆ M ∧ (∃B. ∀x ∈ S. ∀y ∈ S. d x y ≤ B)"
proof -
  have "∧x B. S ⊆ mcball x B ==> ∀x∈S. ∀y∈S. d x y ≤ 2 * B"
    by (smt (verit, best) commute in_mcball subsetD triangle)
  then show ?thesis
    unfolding mbounded_def by (metis in_mcball in_mono subsetI)
qed


lemma mbounded_alt_pos:
  "mbounded S ⟷ S ⊆ M ∧ (∃B>0. ∀x ∈ S. ∀y ∈ S. d x y ≤ B)"
  by (smt (verit, del_insts) gt_ex mbounded_alt)

lemma mbounded_subset: "[mbounded T; S ⊆ T] ==> mbounded S"
  by (meson mbounded_def order_trans)

lemma mbounded_subset_mspace: "mbounded S ==> S ⊆ M"
  by (simp add: mbounded_alt)

lemma mbounded:
   "mbounded S ⟷ S = {} ∨ (∀x ∈ S. x ∈ M) ∧ (∃y B. y ∈ M ∧ (∀x ∈ S. d y x ≤ B))"
  by (meson all_not_in_conv in_mcball mbounded_def subset_iff)

lemma mbounded_empty [iff]: "mbounded {}"
  by (simp add: mbounded)

lemma mbounded_mcball: "mbounded (mcball x r)"
  using mbounded_def by auto

lemma mbounded_mball [iff]: "mbounded (mball x r)"
  by (meson mball_subset_mcball mbounded_def)

lemma mbounded_insert: "mbounded (insert a S) ⟷ a ∈ M ∧ mbounded S"
proof -
  have "∧y B. [y ∈ M; ∀x∈S. d y x ≤ B]
           ==> ∃y. y ∈ M ∧ (∃B ≥ d y a. ∀x∈S. d y x ≤ B)"
    by (metis order.trans nle_le)
  then show ?thesis
    by (auto simp: mbounded)
qed

lemma mbounded_Int: "mbounded S ==> mbounded (S ∩ T)"
  by (meson inf_le1 mbounded_subset)

lemma mbounded_Un: "mbounded (S ∪ T) ⟷ mbounded S ∧ mbounded T" (is "?lhs=?rhs")
proof
  assume R: ?rhs
  show ?lhs
  proof (cases "S={} ∨ T={}")
    case True then show ?thesis
      using R by auto
  next
    case False
    obtain x y B C where "S ⊆ mcball x B" "T ⊆ mcball y C" "B > 0" "C > 0" "x ∈ M" "y ∈ M"
      using R mbounded_pos
      by (metis False mcball_eq_empty subset_empty)
    then have "S ∪ T ⊆ mcball x (B + C + d x y)"
      by (smt (verit) commute dual_order.trans le_supI mcball_subset mdist_pos_eq)
    then show ?thesis
      using mbounded_def by blast
  qed
next
  show "?lhs ==> ?rhs"
    using mbounded_def by auto
qed

lemma mbounded_Union:
  "[finite F; ∧X. X ∈ F ==> mbounded X] ==> mbounded (∪F)"
  by (induction F rule: finite_induct) (auto simp: mbounded_Un)

lemma mbounded_closure_of:
   "mbounded S ==> mbounded (mtopology closure_of S)"
  by (meson closedin_mcball closure_of_minimal mbounded_def)

lemma mbounded_closure_of_eq:
   "S ⊆ M ==> (mbounded (mtopology closure_of S) ⟷ mbounded S)"
  by (metis closure_of_subset mbounded_closure_of mbounded_subset topspace_mtopology)


lemma maxdist_thm:
  assumes "mbounded S"
      and "x ∈ S"
      and "y ∈ S"
    shows  "d x y = (SUP z∈S. ∣d x z - d z y∣)"
proof -
  have "∣d x z - d z y∣ ≤ d x y" if "z ∈ S" for z
    by (metis all_not_in_conv assms mbounded mdist_reverse_triangle that) 
  moreover have "d x y ≤ r"
    if "∧z. z ∈ S ==> ∣d x z - d z y∣ ≤ r" for r :: real
    using that assms mbounded_subset_mspace mdist_zero by fastforce
  ultimately show ?thesis
    by (intro cSup_eq [symmetric]) auto
qed


lemma metric_eq_thm: "[S ⊆ M; x ∈ S; y ∈ S] ==> (x = y) = (∀z∈S. d x z = d y z)"
  by (metis commute  subset_iff zero)

lemma compactin_imp_mbounded:
  assumes "compactin mtopology S"
  shows "mbounded S"
proof -
  have "S ⊆ M"
    and com: "∧U. [∀U∈U. openin mtopology U; S ⊆ ∪U] ==> ∃F. finite F ∧ F ⊆ U ∧ S ⊆ ∪F"
    using assms by (auto simp: compactin_def mbounded_def)
  show ?thesis
  proof (cases "S = {}")
    case False
    with ‹S ⊆ M› obtain a where "a ∈ S" "a ∈ M"
      by blast
    with ‹S ⊆ M› gt_ex have "S ⊆ ∪(range (mball a))"
      by force
    then obtain F where "finite F" "F ⊆ range (mball a)" "S ⊆ ∪F"
      by (metis (no_types, opaque_lifting) com imageE openin_mball)
  then show ?thesis
      using mbounded_Union mbounded_subset by fastforce
  qed auto
qed


end (*Metric_space*)

lemma mcball_eq_cball [simp]: "Met_TC.mcball = cball"
  by force

lemma mball_eq_ball [simp]: "Met_TC.mball = ball"
  by force

lemma mopen_eq_open [simp]: "Met_TC.mopen = open"
  by (force simp: open_contains_ball Met_TC.mopen_def)

lemma limitin_iff_tendsto [iff]: "limitin Met_TC.mtopology σ x F = tendsto σ x F"
  by (simp add: Met_TC.mtopology_def)

lemma mtopology_is_euclidean [simp]: "Met_TC.mtopology = euclidean"
  by (simp add: Met_TC.mtopology_def)

lemma mbounded_iff_bounded [iff]: "Met_TC.mbounded A ⟷ bounded A"
  by (metis Met_TC.mbounded UNIV_I all_not_in_conv bounded_def)


subsection‹Subspace of a metric space›

locale Submetric = Metric_space + 
  fixes A
  assumes subset: "A ⊆ M"

sublocale Submetric ⊆ sub: Metric_space A d
  by (simp add: subset subspace)

context Submetric
begin 

lemma mball_submetric_eq: "sub.mball a r = (if a ∈ A then A ∩ mball a r else {})"
and mcball_submetric_eq: "sub.mcball a r = (if a ∈ A then A ∩ mcball a r else {})"
  using subset by force+

lemma mtopology_submetric: "sub.mtopology = subtopology mtopology A"
  unfolding topology_eq
proof (intro allI iffI)
  fix S
  assume "openin sub.mtopology S"
  then have "∃T. openin (subtopology mtopology A) T ∧ x ∈ T ∧ T ⊆ S" if "x ∈ S" for x
    by (metis mball_submetric_eq openin_mball openin_subtopology_Int2 sub.centre_in_mball_iff sub.openin_mtopology subsetD that)
  then show "openin (subtopology mtopology A) S"
    by (meson openin_subopen)
next
  fix S
  assume "openin (subtopology mtopology A) S"
  then obtain T where "openin mtopology T" "S = T ∩ A"
    by (meson openin_subtopology)
  then have "mopen T"
    by (simp add: mopen_def openin_mtopology)
  then have "sub.mopen (T ∩ A)"
    unfolding sub.mopen_def mopen_def
    by (metis inf.coboundedI2 mball_submetric_eq Int_iff ‹S = T ∩ A› inf.bounded_iff subsetI)
  then show "openin sub.mtopology S"
    using ‹S = T ∩ A› sub.mopen_def sub.openin_mtopology by force
qed

lemma mbounded_submetric: "sub.mbounded T ⟷ mbounded T ∧ T ⊆ A"
  by (meson mbounded_alt sub.mbounded_alt subset subset_trans)

end

lemma (in Metric_space) submetric_empty [iff]: "Submetric M d {}"
proof qed auto


subsection ‹Abstract type of metric spaces›

typedef 'a metric = "{(M::'a set,d). Metric_space M d}"
  morphisms "dest_metric" "metric"
proof -
  have "Metric_space {} (λx y. 0)"
    by (auto simp: Metric_space_def)
  then show ?thesis
    by blast
qed

definition mspace where "mspace m ≡ fst (dest_metric m)"

definition mdist where "mdist m ≡ snd (dest_metric m)"

lemma Metric_space_mspace_mdist [iff]: "Metric_space (mspace m) (mdist m)"
  by (metis Product_Type.Collect_case_prodD dest_metric mdist_def mspace_def)

lemma mdist_nonneg [simp]: "∧x y. 0 ≤ mdist m x y"
  by (metis Metric_space_def Metric_space_mspace_mdist)

lemma mdist_commute: "∧x y. mdist m x y = mdist m y x"
  by (metis Metric_space_def Metric_space_mspace_mdist)

lemma mdist_zero [simp]: "∧x y. [x ∈ mspace m; y ∈ mspace m] ==> mdist m x y = 0 ⟷ x=y"
  by (meson Metric_space.zero Metric_space_mspace_mdist)

lemma mdist_triangle: "∧x y z. [x ∈ mspace m; y ∈ mspace m; z ∈ mspace m] ==> mdist m x z ≤ mdist m x y + mdist m y z"
  by (meson Metric_space.triangle Metric_space_mspace_mdist)

lemma (in Metric_space) mspace_metric[simp]: 
  "mspace (metric (M,d)) = M"
  by (simp add: metric_inverse mspace_def subspace)

lemma (in Metric_space) mdist_metric[simp]: 
  "mdist (metric (M,d)) = d"
  by (simp add: mdist_def metric_inverse subspace)

lemma metric_collapse [simp]: "metric (mspace m, mdist m) = m"
  by (simp add: dest_metric_inverse mdist_def mspace_def)

definition mtopology_of :: "'a metric → 'a topology"
  where "mtopology_of ≡ λm. Metric_space.mtopology (mspace m) (mdist m)"

lemma topspace_mtopology_of [simp]: "topspace (mtopology_of m) = mspace m"
  by (simp add: Metric_space.topspace_mtopology Metric_space_mspace_mdist mtopology_of_def)

lemma (in Metric_space) mtopology_of [simp]:
  "mtopology_of (metric (M,d)) = mtopology"
  by (simp add: mtopology_of_def)

definition "mball_of ≡ λm. Metric_space.mball (mspace m) (mdist m)"

lemma in_mball_of [simp]: "y ∈ mball_of m x r ⟷ x ∈ mspace m ∧ y ∈ mspace m ∧ mdist m x y < r"
  by (simp add: Metric_space.in_mball mball_of_def)

lemma (in Metric_space) mball_of [simp]:
  "mball_of (metric (M,d)) = mball"
  by (simp add: mball_of_def)

definition "mcball_of ≡ λm. Metric_space.mcball (mspace m) (mdist m)"

lemma in_mcball_of [simp]: "y ∈ mcball_of m x r ⟷ x ∈ mspace m ∧ y ∈ mspace m ∧ mdist m x y ≤ r"
  by (simp add: Metric_space.in_mcball mcball_of_def)

lemma (in Metric_space) mcball_of [simp]:
  "mcball_of (metric (M,d)) = mcball"
  by (simp add: mcball_of_def)

definition "euclidean_metric ≡ metric (UNIV,dist)"

lemma mspace_euclidean_metric [simp]: "mspace euclidean_metric = UNIV"
  by (simp add: euclidean_metric_def)

lemma mdist_euclidean_metric [simp]: "mdist euclidean_metric = dist"
  by (simp add: euclidean_metric_def)

lemma mtopology_of_euclidean [simp]: "mtopology_of euclidean_metric = euclidean"
  by (simp add: Met_TC.mtopology_def mtopology_of_def)

text ‹Allows reference to the current metric space within the locale as a value›
definition (in Metric_space) "Self ≡ metric (M,d)"

lemma (in Metric_space) mspace_Self [simp]: "mspace Self = M"
  by (simp add: Self_def)

lemma (in Metric_space) mdist_Self [simp]: "mdist Self = d"
  by (simp add: Self_def)

text‹ Subspace of a metric space›

definition submetric where
  "submetric ≡ λm S. metric (S ∩ mspace m, mdist m)"

lemma mspace_submetric [simp]: "mspace (submetric m S) = S ∩ mspace m" 
  unfolding submetric_def
  by (meson Metric_space.subspace inf_le2 Metric_space_mspace_mdist Metric_space.mspace_metric)

lemma mdist_submetric [simp]: "mdist (submetric m S) = mdist m"
  unfolding submetric_def
  by (meson Metric_space.subspace inf_le2 Metric_space.mdist_metric Metric_space_mspace_mdist)

lemma submetric_UNIV [simp]: "submetric m UNIV = m"
  by (simp add: submetric_def dest_metric_inverse mdist_def mspace_def)

lemma submetric_submetric [simp]:
   "submetric (submetric m S) T = submetric m (S ∩ T)"
  by (metis submetric_def Int_assoc inf_commute mdist_submetric mspace_submetric)

lemma submetric_mspace [simp]:
   "submetric m (mspace m) = m"
  by (simp add: submetric_def dest_metric_inverse mdist_def mspace_def)

lemma submetric_restrict:
   "submetric m S = submetric m (mspace m ∩ S)"
  by (metis submetric_mspace submetric_submetric)

lemma mtopology_of_submetric: "mtopology_of (submetric m A) = subtopology (mtopology_of m) A"
proof -
  interpret Submetric "mspace m" "mdist m" "A ∩ mspace m"
    using Metric_space_mspace_mdist Submetric.intro Submetric_axioms.intro inf_le2 by blast
  have "sub.mtopology = subtopology (mtopology_of m) A"
    by (metis inf_commute mtopology_of_def mtopology_submetric subtopology_mspace subtopology_subtopology)
  then show ?thesis
    by (simp add: submetric_def)
qed


subsection‹The discrete metric›

locale discrete_metric =
  fixes M :: "'a set"

definition (in discrete_metric) dd :: "'a → 'a → real"
  where "dd ≡ λx y::'a. if x=y then 0 else 1"

lemma metric_M_dd: "Metric_space M discrete_metric.dd"
  by (simp add: discrete_metric.dd_def Metric_space.intro)

sublocale discrete_metric ⊆ disc: Metric_space M dd
  by (simp add: metric_M_dd)


lemma (in discrete_metric) mopen_singleton:
  assumes "x ∈ M" shows "disc.mopen {x}"
proof -
  have "disc.mball x (1/2) ⊆ {x}"
    by (smt (verit) dd_def disc.in_mball less_divide_eq_1_pos singleton_iff subsetI)
  with assms show ?thesis
    using disc.mopen_def half_gt_zero_iff zero_less_one by blast
qed

lemma (in discrete_metric) mtopology_discrete_metric:
   "disc.mtopology = discrete_topology M"
proof -
  have "∧x. x ∈ M ==> openin disc.mtopology {x}"
    by (simp add: disc.mtopology_def mopen_singleton)
  then show ?thesis
    by (metis disc.topspace_mtopology discrete_topology_unique)
qed

lemma (in discrete_metric) discrete_ultrametric:
   "dd x z ≤ max (dd x y) (dd y z)"
  by (simp add: dd_def)


lemma (in discrete_metric) dd_le1: "dd x y ≤ 1"
  by (simp add: dd_def)

lemma (in discrete_metric) mbounded_discrete_metric: "disc.mbounded S ⟷ S ⊆ M"
  by (meson dd_le1 disc.mbounded_alt)



subsection‹Metrizable spaces›

definition metrizable_space where
  "metrizable_space X ≡ ∃M d. Metric_space M d ∧ X = Metric_space.mtopology M d"

lemma (in Metric_space) metrizable_space_mtopology: "metrizable_space mtopology"
  using local.Metric_space_axioms metrizable_space_def by blast

lemma (in Metric_space) first_countable_mtopology: "first_countable mtopology"
proof (clarsimp simp add: first_countable_def)
  fix x
  assume "x ∈ M"
  define B where "B ≡ mball x ` {r ∈ ℚ. 0 < r}"
  show "∃B. countable B ∧ (∀V∈B. openin mtopology V) ∧ (∀U. openin mtopology U ∧ x ∈ U ⟶ (∃V∈B. x ∈ V ∧ V ⊆ U))"
  proof (intro exI conjI ballI)
    show "countable B"
      by (simp add: B_def countable_rat)
    show "∀U. openin mtopology U ∧ x ∈ U ⟶ (∃V∈B. x ∈ V ∧ V ⊆ U)"
    proof clarify
      fix U
      assume "openin mtopology U" and "x ∈ U"
      then obtain r where "r>0" and r: "mball x r ⊆ U"
        by (meson openin_mtopology)
      then obtain q where "q ∈ Rats" "0 < q" "q < r"
        using Rats_dense_in_real by blast
      then show "∃V∈B. x ∈ V ∧ V ⊆ U"
        unfolding B_def using ‹x ∈ M› r by fastforce
    qed
  qed (auto simp: B_def)
qed

lemma metrizable_imp_first_countable:
   "metrizable_space X ==> first_countable X"
  by (force simp: metrizable_space_def Metric_space.first_countable_mtopology)

lemma openin_mtopology_eq_open [simp]: "openin Met_TC.mtopology = open"
  by (simp add: Met_TC.mtopology_def)

lemma closedin_mtopology_eq_closed [simp]: "closedin Met_TC.mtopology = closed"
proof -
  have "(euclidean::'a topology) = Met_TC.mtopology"
    by (simp add: Met_TC.mtopology_def)
  then show ?thesis
    using closed_closedin by fastforce
qed

lemma compactin_mtopology_eq_compact [simp]: "compactin Met_TC.mtopology = compact"
  by (simp add: compactin_def compact_eq_Heine_Borel fun_eq_iff) meson

lemma metrizable_space_discrete_topology [simp]:
   "metrizable_space(discrete_topology U)"
  by (metis discrete_metric.mtopology_discrete_metric metric_M_dd metrizable_space_def)

lemma empty_metrizable_space: "metrizable_space trivial_topology"
  by simp

lemma metrizable_space_subtopology:
  assumes "metrizable_space X"
  shows "metrizable_space(subtopology X S)"
proof -
  obtain M d where "Metric_space M d" and X: "X = Metric_space.mtopology M d"
    using assms metrizable_space_def by blast
  then interpret Submetric M d "M ∩ S"
    by (simp add: Submetric.intro Submetric_axioms_def)
  show ?thesis
    unfolding metrizable_space_def
    by (metis X mtopology_submetric sub.Metric_space_axioms subtopology_restrict topspace_mtopology)
qed

lemma homeomorphic_metrizable_space_aux:
  assumes "X homeomorphic_space Y" "metrizable_space X"
  shows "metrizable_space Y"
proof -
  obtain M d where "Metric_space M d" and X: "X = Metric_space.mtopology M d"
    using assms by (auto simp: metrizable_space_def)
  then interpret m: Metric_space M d 
    by simp
  obtain f g where hmf: "homeomorphic_map X Y f" and hmg: "homeomorphic_map Y X g"
    and fg: "(∀x ∈ M. g(f x) = x) ∧ (∀y ∈ topspace Y. f(g y) = y)"
    using assms X homeomorphic_maps_map homeomorphic_space_def by fastforce
  define d' where "d' x y ≡ d (g x) (g y)" for x y
  interpret m': Metric_space "topspace Y" "d'"
    unfolding d'_def
  proof
    show "(d (g x) (g y) = 0) = (x = y)" if "x ∈ topspace Y" "y ∈ topspace Y" for x y
      by (metis fg X hmg homeomorphic_imp_surjective_map imageI m.topspace_mtopology m.zero that)
    show "d (g x) (g z) ≤ d (g x) (g y) + d (g y) (g z)"
      if "x ∈ topspace Y" and "y ∈ topspace Y" and "z ∈ topspace Y" for x y z
      by (metis X that hmg homeomorphic_eq_everything_map imageI m.topspace_mtopology m.triangle)
  qed (auto simp: m.nonneg m.commute)
  have "Y = Metric_space.mtopology (topspace Y) d'"
    unfolding topology_eq
  proof (intro allI)
    fix S
    have "openin m'.mtopology S" if S: "S ⊆ topspace Y" and "openin X (g ` S)"
      unfolding m'.openin_mtopology
    proof (intro conjI that strip)
      fix y
      assume "y ∈ S"
      then obtain r where "r>0" and r: "m.mball (g y) r ⊆ g ` S" 
        using X ‹openin X (g ` S)› m.openin_mtopology using ‹y ∈ S› by auto
      then have "g ` m'.mball y r ⊆ m.mball (g y) r"
        using X d'_def hmg homeomorphic_imp_surjective_map by fastforce
      with S fg have "m'.mball y r ⊆ S"
        by (smt (verit, del_insts) image_iff m'.in_mball r subset_iff)
      then show "∃r>0. m'.mball y r ⊆ S"
        using ‹0 < r› by blast 
    qed
    moreover have "openin X (g ` S)" if ope': "openin m'.mtopology S"
    proof -
      have "∃r>0. m.mball (g y) r ⊆ g ` S" if "y ∈ S" for y
      proof -
        have y: "y ∈ topspace Y"
          using m'.openin_mtopology ope' that by blast
        obtain r where "r > 0" and r: "m'.mball y r ⊆ S"
          using ope' by (meson ‹y ∈ S› m'.openin_mtopology)
        moreover have "∧x. [x ∈ M; d (g y) x < r] ==> ∃u. u ∈ topspace Y ∧ d' y u < r ∧ x = g u"
          using fg X d'_def hmf homeomorphic_imp_surjective_map by fastforce
        ultimately have "m.mball (g y) r ⊆ g ` m'.mball y r"
          using y by (force simp: m'.openin_mtopology)
        then show ?thesis
          using ‹0 < r› r by blast
      qed
      then show ?thesis
        using X hmg homeomorphic_imp_surjective_map m.openin_mtopology ope' openin_subset by fastforce
    qed
    ultimately have "(S ⊆ topspace Y ∧ openin X (g ` S)) = openin m'.mtopology S"
      using m'.topspace_mtopology openin_subset by blast
    then show "openin Y S = openin m'.mtopology S"
      by (simp add: m'.mopen_def homeomorphic_map_openness_eq [OF hmg])
  qed
  then show ?thesis
    using m'.metrizable_space_mtopology by force
qed

lemma homeomorphic_metrizable_space:
  assumes "X homeomorphic_space Y"
  shows "metrizable_space X ⟷ metrizable_space Y"
  using assms homeomorphic_metrizable_space_aux homeomorphic_space_sym by metis

lemma metrizable_space_retraction_map_image:
   "retraction_map X Y r ∧ metrizable_space X
        ==> metrizable_space Y"
  using hereditary_imp_retractive_property metrizable_space_subtopology homeomorphic_metrizable_space
  by blast


lemma metrizable_imp_Hausdorff_space:
   "metrizable_space X ==> Hausdorff_space X"
  by (metis Metric_space.Hausdorff_space_mtopology metrizable_space_def)

(**
lemma metrizable_imp_kc_space:
   "metrizable_space X \<Longrightarrow> kc_space X"
oops
  MESON_TAC[METRIZABLE_IMP_HAUSDORFF_SPACE; HAUSDORFF_IMP_KC_SPACE]);;

lemma kc_space_mtopology:
   "kc_space mtopology"
oops
  REWRITE_TAC[GSYM FORALL_METRIZABLE_SPACE; METRIZABLE_IMP_KC_SPACE]);;
**)

lemma metrizable_imp_t1_space:
   "metrizable_space X ==> t1_space X"
  by (simp add: Hausdorff_imp_t1_space metrizable_imp_Hausdorff_space)

lemma closed_imp_gdelta_in:
  assumes X: "metrizable_space X" and S: "closedin X S"
  shows "gdelta_in X S"
proof -
  obtain M d where "Metric_space M d" and Xeq: "X = Metric_space.mtopology M d"
    using X metrizable_space_def by blast
  then interpret M: Metric_space M d
    by blast
  have "S ⊆ M"
    using M.closedin_metric ‹X = M.mtopology› S by blast
  show ?thesis
  proof (cases "S = {}")
    case True
    then show ?thesis
      by simp
  next
    case False
    have "∃y∈S. d x y < inverse (1 + real n)" if "x ∈ S" for x n
      using ‹S ⊆ M› M.mdist_zero [of x] that by force
    moreover
    have "x ∈ S" if "x ∈ M" and §: "∧n. ∃y∈S. d x y < inverse(Suc n)" for x
    proof -
      have *: "∃y∈S. d x y < ε" if "ε > 0" for ε
        by (metis § that not0_implies_Suc order_less_le order_less_le_trans real_arch_inverse)
      have "closedin M.mtopology S"
        using S by (simp add: Xeq)
      with * ‹x ∈ M› show ?thesis
        by (force simp: M.closedin_metric disjnt_iff)
    qed
    ultimately have Seq: "S = ∩(range (λn. {x∈M. ∃y∈S. d x y < inverse(Suc n)}))"
      using ‹S ⊆ M› by force
    have "openin M.mtopology {xa ∈ M. ∃y∈S. d xa y < inverse (1 + real n)}" for n
    proof (clarsimp simp: M.openin_mtopology)
      fix x y
      assume "x ∈ M" "y ∈ S" and dxy: "d x y < inverse (1 + real n)"
      then have "∧z. [z ∈ M; d x z < inverse (1 + real n) - d x y] ==> ∃y∈S. d z y < inverse (1 + real n)"
        by (smt (verit) M.commute M.triangle ‹S ⊆ M› in_mono)
      with dxy show "∃r>0. M.mball x r ⊆ {z ∈ M. ∃y∈S. d z y < inverse (1 + real n)}"
        by (rule_tac x="inverse(Suc n) - d x y" in exI) auto
    qed
    then have "gdelta_in X (∩(range (λn. {x∈M. ∃y∈S. d x y < inverse(Suc n)})))"
      by (force simp: Xeq intro: gdelta_in_Inter open_imp_gdelta_in)
    with Seq show ?thesis
      by presburger
  qed
qed

lemma open_imp_fsigma_in:
   "[metrizable_space X; openin X S] ==> fsigma_in X S"
  by (meson closed_imp_gdelta_in fsigma_in_gdelta_in openin_closedin openin_subset)

lemma metrizable_space_euclidean:
  "metrizable_space (euclidean :: 'a::metric_space topology)"
  using Met_TC.metrizable_space_mtopology by auto

lemma (in Metric_space) regular_space_mtopology:
   "regular_space mtopology"
unfolding regular_space_def
proof clarify
  fix C a
  assume C: "closedin mtopology C" and a: "a ∈ topspace mtopology" and "a ∉ C"
  have "openin mtopology (topspace mtopology - C)"
    by (simp add: C openin_diff)
  then obtain r where "r>0" and r: "mball a r ⊆ topspace mtopology - C"
    unfolding openin_mtopology using ‹a ∉ C› a by auto
  show "∃U V. openin mtopology U ∧ openin mtopology V ∧ a ∈ U ∧ C ⊆ V ∧ disjnt U V"
  proof (intro exI conjI)
    show "a ∈ mball a (r/2)"
      using ‹0 < r› a by force
    show "C ⊆ topspace mtopology - mcball a (r/2)"
      using C ‹0 < r› r by (fastforce simp: closedin_metric)
  qed (auto simp: openin_mball closedin_mcball openin_diff disjnt_iff)
qed

lemma metrizable_imp_regular_space:
   "metrizable_space X ==> regular_space X"
  by (metis Metric_space.regular_space_mtopology metrizable_space_def)

lemma regular_space_euclidean:
 "regular_space (euclidean :: 'a::metric_space topology)"
  by (simp add: metrizable_imp_regular_space metrizable_space_euclidean)


subsection‹Limits at a point in a topological space›

lemma (in Metric_space) eventually_atin_metric:
   "eventually P (atin mtopology a) ⟷
        (a ∈ M ⟶ (∃δ>0. ∀x. x ∈ M ∧ 0 < d x a ∧ d x a < δ ⟶ P x))"  (is "?lhs=?rhs")
proof (cases "a ∈ M")
  case True
  show ?thesis
  proof
    assume L: ?lhs 
    with True obtain U where "openin mtopology U" "a ∈ U" and U: "∀x∈U - {a}. P x"
      by (auto simp: eventually_atin)
    then obtain r where "r>0" and "mball a r ⊆ U"
      by (meson openin_mtopology)
    with U show ?rhs
      by (smt (verit, ccfv_SIG) commute in_mball insert_Diff_single insert_iff subset_iff)
  next
    assume ?rhs 
    then obtain δ where "δ>0" and δ: "∀x. x ∈ M ∧ 0 < d x a ∧ d x a < δ ⟶ P x"
      using True by blast
    then have "∀x ∈ mball a δ - {a}. P x"
      by (simp add: commute)
    then show ?lhs
      unfolding eventually_atin openin_mtopology
      by (metis True ‹0 < \δ› centre_in_mball_iff openin_mball openin_mtopology) 
  qed
qed auto

subsection ‹Normal spaces and metric spaces›

lemma (in Metric_space) normal_space_mtopology:
   "normal_space mtopology"
  unfolding normal_space_def
proof clarify
  fix S T
  assume "closedin mtopology S"
  then have "∧x. x ∈ M - S ==> (∃r>0. mball x r ⊆ M - S)"
    by (simp add: closedin_def openin_mtopology)
  then obtain δ where d0: "∧x. x ∈ M - S ==> δ x > 0 ∧ mball x (δ x) ⊆ M - S"
    by metis
  assume "closedin mtopology T"
  then have "∧x. x ∈ M - T ==> (∃r>0. mball x r ⊆ M - T)"
    by (simp add: closedin_def openin_mtopology)
  then obtain ε where e: "∧x. x ∈ M - T ==> ε x > 0 ∧ mball x (ε x) ⊆ M - T"
    by metis
  assume "disjnt S T"
  have "S ⊆ M" "T ⊆ M"
    using ‹closedin mtopology S› ‹closedin mtopology T› closedin_metric by blast+
  have δ: "∧x. x ∈ T ==> δ x > 0 ∧ mball x (δ x) ⊆ M - S"
    by (meson DiffI ‹T ⊆ M› ‹disjnt S T› d0 disjnt_iff subsetD)
  have ε: "∧x. x ∈ S ==> ε x > 0 ∧ mball x (ε x) ⊆ M - T"
    by (meson Diff_iff ‹S ⊆ M› ‹disjnt S T› disjnt_iff e subsetD)
  show "∃U V. openin mtopology U ∧ openin mtopology V ∧ S ⊆ U ∧ T ⊆ V ∧ disjnt U V"
  proof (intro exI conjI)
    show "openin mtopology (∪x∈S. mball x (ε x / 2))" "openin mtopology (∪x∈T. mball x (δ x / 2))"
      by force+
    show "S ⊆ (∪x∈S. mball x (ε x / 2))"
      using ε ‹S ⊆ M› by force
    show "T ⊆ (∪x∈T. mball x (δ x / 2))"
      using δ ‹T ⊆ M› by force
    show "disjnt (∪x∈S. mball x (ε x / 2)) (∪x∈T. mball x (δ x / 2))"
      using ε δ 
      apply (clarsimp simp: disjnt_iff subset_iff)
      by (smt (verit, ccfv_SIG) field_sum_of_halves triangle')
  qed 
qed

lemma metrizable_imp_normal_space:
   "metrizable_space X ==> normal_space X"
  by (metis Metric_space.normal_space_mtopology metrizable_space_def)

subsection‹Topological limitin in metric spaces›


lemma (in Metric_space) limitin_mspace:
   "limitin mtopology f l F ==> l ∈ M"
  using limitin_topspace by fastforce

lemma (in Metric_space) limitin_metric_unique:
   "[limitin mtopology f l1 F; limitin mtopology f l2 F; F ≠ bot] ==> l1 = l2"
  by (meson Hausdorff_space_mtopology limitin_Hausdorff_unique)

lemma (in Metric_space) limitin_metric:
   "limitin mtopology f l F ⟷ l ∈ M ∧ (∀ε>0. eventually (λx. f x ∈ M ∧ d (f x) l < ε) F)"  
   (is "?lhs=?rhs")
proof
  assume L: ?lhs
  show ?rhs
    unfolding limitin_def
  proof (intro conjI strip)
    show "l ∈ M"
      using L limitin_mspace by blast
    fix ε::real
    assume "ε>0"
    then have "∀_F x in F. f x ∈ mball l ε"
      using L openin_mball by (fastforce simp: limitin_def)
    then show "∀_F x in F. f x ∈ M ∧ d (f x) l < ε"
      using commute eventually_mono by fastforce
  qed
next
  assume R: ?rhs 
  then show ?lhs
    by (force simp: limitin_def commute openin_mtopology subset_eq elim: eventually_mono)
qed

lemma (in Metric_space) limit_metric_sequentially:
   "limitin mtopology f l sequentially ⟷
     l ∈ M ∧ (∀ε>0. ∃N. ∀n≥N. f n ∈ M ∧ d (f n) l < ε)"
  by (auto simp: limitin_metric eventually_sequentially)

lemma (in Submetric) limitin_submetric_iff:
   "limitin sub.mtopology f l F ⟷
     l ∈ A ∧ eventually (λx. f x ∈ A) F ∧ limitin mtopology f l F" (is "?lhs=?rhs")
  by (simp add: limitin_subtopology mtopology_submetric)

lemma (in Metric_space) metric_closedin_iff_sequentially_closed:
   "closedin mtopology S ⟷
    S ⊆ M ∧ (∀σ l. range σ ⊆ S ∧ limitin mtopology σ l sequentially ⟶ l ∈ S)" (is "?lhs=?rhs")
proof
  assume ?lhs then show ?rhs
    by (force simp: closedin_metric limitin_closedin range_subsetD)
next
  assume R: ?rhs
  show ?lhs
    unfolding closedin_metric
  proof (intro conjI strip)
    show "S ⊆ M"
      using R by blast
    fix x
    assume "x ∈ M - S"
    have False if "∀r>0. ∃y. y ∈ M ∧ y ∈ S ∧ d x y < r"
    proof -
      have "∀n. ∃y. y ∈ M ∧ y ∈ S ∧ d x y < inverse(Suc n)"
        using that by auto
      then obtain σ where σ: "∧n. σ n ∈ M ∧ σ n ∈ S ∧ d x (σ n) < inverse(Suc n)"
        by metis
      then have "range σ ⊆ M"
        by blast
      have "∃N. ∀n≥N. d x (σ n) < ε" if "ε>0" for ε
      proof -
        have "real (Suc (nat ⌈inverse ε⌉)) ≥ inverse ε"
          by linarith
        then have "∀n ≥ nat ⌈inverse ε⌉. d x (σ n) < ε"
          by (metis σ inverse_inverse_eq inverse_le_imp_le nat_ceiling_le_eq nle_le not_less_eq_eq order.strict_trans2 that)
        then show ?thesis ..
      qed
      with σ have "limitin mtopology σ x sequentially"
        using ‹x ∈ M - S› commute limit_metric_sequentially by auto
      then show ?thesis
        by (metis R DiffD2 σ image_subset_iff ‹x ∈ M - S›)
    qed
    then show "∃r>0. disjnt S (mball x r)"
      by (meson disjnt_iff in_mball)
  qed
qed

lemma (in Metric_space) limit_atin_metric:
   "limitin X f y (atin mtopology x) ⟷
      y ∈ topspace X ∧
      (x ∈ M
       ⟶ (∀V. openin X V ∧ y ∈ V
               ⟶ (∃δ>0. ∀x'. x' ∈ M ∧ 0 < d x' x ∧ d x' x < δ ⟶ f x' ∈ V)))"
  by (force simp: limitin_def eventually_atin_metric)

lemma (in Metric_space) limitin_metric_dist_null:
   "limitin mtopology f l F ⟷ l ∈ M ∧ eventually (λx. f x ∈ M) F ∧ ((λx. d (f x) l) ---> 0) F"
  by (simp add: limitin_metric tendsto_iff eventually_conj_iff all_conj_distrib imp_conjR gt_ex)


subsection‹Cauchy sequences and complete metric spaces›

context Metric_space
begin

definition MCauchy :: "(nat → 'a) → bool"
  where "MCauchy σ ≡ range σ ⊆ M ∧ (∀ε>0. ∃N. ∀n n'. N ≤ n ⟶ N ≤ n' ⟶ d (σ n) (σ n') < ε)"

definition mcomplete
  where "mcomplete ≡ (∀σ. MCauchy σ ⟶ (∃x. limitin mtopology σ x sequentially))"

lemma mcomplete_empty [iff]: "Metric_space.mcomplete {} d"
  by (simp add: Metric_space.MCauchy_def Metric_space.mcomplete_def subspace)

lemma MCauchy_imp_MCauchy_suffix: "MCauchy σ ==> MCauchy (σ ∘ (+)n)"
  unfolding MCauchy_def image_subset_iff comp_apply
  by (metis UNIV_I add.commute trans_le_add1) 

lemma mcomplete:
   "mcomplete ⟷
    (∀σ. (∀_F n in sequentially. σ n ∈ M) ∧
     (∀ε>0. ∃N. ∀n n'. N ≤ n ⟶ N ≤ n' ⟶ d (σ n) (σ n') < ε) ⟶
     (∃x. limitin mtopology σ x sequentially))" (is "?lhs=?rhs")
proof
  assume L: ?lhs 
  show ?rhs
  proof clarify
    fix σ
    assume "∀_F n in sequentially. σ n ∈ M"
      and σ: "∀ε>0. ∃N. ∀n n'. N ≤ n ⟶ N ≤ n' ⟶ d (σ n) (σ n') < ε"
    then obtain N where "∧n. n≥N ==> σ n ∈ M"
      by (auto simp: eventually_sequentially)
    with σ have "MCauchy (σ ∘ (+)N)"
      unfolding MCauchy_def image_subset_iff comp_apply by (meson le_add1 trans_le_add2)
    then obtain x where "limitin mtopology (σ ∘ (+)N) x sequentially"
      using L MCauchy_imp_MCauchy_suffix mcomplete_def by blast
    then have "limitin mtopology σ x sequentially"
      unfolding o_def by (auto simp: add.commute limitin_sequentially_offset_rev)
    then show "∃x. limitin mtopology σ x sequentially" ..
  qed
qed (simp add: mcomplete_def MCauchy_def image_subset_iff)

lemma mcomplete_empty_mspace: "M = {} ==> mcomplete"
  using MCauchy_def mcomplete_def by blast

lemma MCauchy_const [simp]: "MCauchy (λn. a) ⟷ a ∈ M"
  using MCauchy_def mdist_zero by auto

lemma convergent_imp_MCauchy:
  assumes "range σ ⊆ M" and lim: "limitin mtopology σ l sequentially"
  shows "MCauchy σ"
  unfolding MCauchy_def image_subset_iff
proof (intro conjI strip)
  fix ε::real
  assume "ε > 0"
  then have "∀_F n in sequentially. σ n ∈ M ∧ d (σ n) l < ε/2"
    using half_gt_zero lim limitin_metric by blast
  then obtain N where "∧n. n≥N ==> σ n ∈ M ∧ d (σ n) l < ε/2"
    by (force simp: eventually_sequentially)
  then show "∃N. ∀n n'. N ≤ n ⟶ N ≤ n' ⟶ d (σ n) (σ n') < ε"
    by (smt (verit) limitin_mspace mdist_reverse_triangle field_sum_of_halves lim)
qed (use assms in blast)


lemma mcomplete_alt:
   "mcomplete ⟷ (∀σ. MCauchy σ ⟷ range σ ⊆ M ∧ (∃x. limitin mtopology σ x sequentially))"
  using MCauchy_def convergent_imp_MCauchy mcomplete_def by blast

lemma MCauchy_subsequence:
  assumes "strict_mono r" "MCauchy σ"
  shows "MCauchy (σ ∘ r)"
proof -
  have "d (σ (r n)) (σ (r n')) < ε"
    if "N ≤ n" "N ≤ n'" "strict_mono r" "∀n n'. N ≤ n ⟶ N ≤ n' ⟶ d (σ n) (σ n') < ε"
    for ε N n n'
    using that by (meson le_trans strict_mono_imp_increasing)
  moreover have "range (λx. σ (r x)) ⊆ M"
    using MCauchy_def assms by blast
  ultimately show ?thesis
    using assms by (simp add: MCauchy_def) metis
qed

lemma MCauchy_offset:
  assumes cau: "MCauchy (σ ∘ (+)k)" and σ: "∧n. n < k ==> σ n ∈ M" 
  shows "MCauchy σ"
  unfolding MCauchy_def image_subset_iff
proof (intro conjI strip)
  fix n
  show "σ n ∈ M"
    using assms
    unfolding MCauchy_def image_subset_iff
    by (metis UNIV_I comp_apply le_iff_add linorder_not_le)
next
  fix ε :: real
  assume "ε > 0"
  obtain N where "∀n n'. N ≤ n ⟶ N ≤ n' ⟶ d ((σ ∘ (+)k) n) ((σ ∘ (+)k) n') < ε"
    using cau ‹ε > 0› by (fastforce simp: MCauchy_def)
  then show "∃N. ∀n n'. N ≤ n ⟶ N ≤ n' ⟶ d (σ n) (σ n') < ε"
    unfolding o_def
    by (intro exI [where x="k+N"]) (smt (verit, del_insts) add.assoc le_add1 less_eqE)
qed

lemma MCauchy_convergent_subsequence:
  assumes cau: "MCauchy σ" and "strict_mono r" 
     and lim: "limitin mtopology (σ ∘ r) a sequentially"
  shows "limitin mtopology σ a sequentially"
  unfolding limitin_metric
proof (intro conjI strip)
  show "a ∈ M"
    by (meson assms limitin_mspace)
  fix ε :: real
  assume "ε > 0"
  then obtain N1 where N1: "∧n n'. [n≥N1; n'≥N1] ==> d (σ n) (σ n') < ε/2"
    using cau unfolding MCauchy_def by (meson half_gt_zero)
  obtain N2 where N2: "∧n. n ≥ N2 ==> (σ ∘ r) n ∈ M ∧ d ((σ ∘ r) n) a < ε/2"
    by (metis (no_types, lifting) lim ‹ε > 0› half_gt_zero limit_metric_sequentially)
  have "σ n ∈ M ∧ d (σ n) a < ε" if "n ≥ max N1 N2" for n
  proof (intro conjI)
    show "σ n ∈ M"
      using MCauchy_def cau by blast
    have "N1 ≤ r n"
      by (meson ‹strict_mono r› le_trans max.cobounded1 strict_mono_imp_increasing that)
    then show "d (σ n) a < ε"
      using N1[of n "r n"] N2[of n] ‹σ n ∈ M› ‹a ∈ M› triangle that by fastforce
  qed
  then show "∀_F n in sequentially. σ n ∈ M ∧ d (σ n) a < ε"
    using eventually_sequentially by blast
qed

lemma MCauchy_interleaving_gen:
  "MCauchy (λn. if even n then x(n div 2) else y(n div 2)) ⟷
    (MCauchy x ∧ MCauchy y ∧ (λn. d (x n) (y n)) <---- 0)" (is "?lhs=?rhs")
proof
  assume L: ?lhs
  have evens: "strict_mono (λn::nat. 2 * n)" and odds: "strict_mono (λn::nat. Suc (2 * n))"
    by (auto simp: strict_mono_def)
  show ?rhs
  proof (intro conjI)
    show "MCauchy x" "MCauchy y"
      using MCauchy_subsequence [OF evens L] MCauchy_subsequence [OF odds L] by (auto simp: o_def)
    show "(λn. d (x n) (y n)) <---- 0"
      unfolding LIMSEQ_iff
    proof (intro strip)
      fix ε :: real
      assume "ε > 0"
      then obtain N where N: 
        "∧n n'. [n≥N; n'≥N] ==> d (if even n then x (n div 2) else y (n div 2))
                                   (if even n' then x (n' div 2) else y (n' div 2)) < ε"
        using L MCauchy_def by fastforce
      have "d (x n) (y n) < ε" if "n≥N" for n
        using N [of "2*n" "Suc(2*n)"] that by auto
      then show "∃N. ∀n≥N. norm (d (x n) (y n) - 0) < ε"
        by auto
    qed
  qed
next
  assume R: ?rhs
  show ?lhs
    unfolding MCauchy_def
  proof (intro conjI strip)
    show "range (λn. if even n then x (n div 2) else y (n div 2)) ⊆ M"
      using R by (auto simp: MCauchy_def)
    fix ε :: real
    assume "ε > 0"
    obtain Nx where Nx: "∧n n'. [n≥Nx; n'≥Nx] ==> d (x n) (x n') < ε/2"
      by (meson half_gt_zero MCauchy_def R ‹ε > 0›)
    obtain Ny where Ny: "∧n n'. [n≥Ny; n'≥Ny] ==> d (y n) (y n') < ε/2"
      by (meson half_gt_zero MCauchy_def R ‹ε > 0›)
    obtain Nxy where Nxy: "∧n. n≥Nxy ==> d (x n) (y n) < ε/2"
      using R ‹ε > 0› half_gt_zero unfolding LIMSEQ_iff
      by (metis abs_mdist diff_zero real_norm_def)
    define N where "N ≡ 2 * Max{Nx,Ny,Nxy}"
    show "∃N. ∀n n'. N ≤ n ⟶ N ≤ n' ⟶ d (if even n then x (n div 2) else y (n div 2)) (if even n' then x (n' div 2) else y (n' div 2)) < ε"
    proof (intro exI strip)
      fix n n'
      assume "N ≤ n" and "N ≤ n'"
      then have "n div 2 ≥ Nx" "n div 2 ≥ Ny" "n div 2 ≥ Nxy" "n' div 2 ≥ Nx" "n' div 2 ≥ Ny" 
        by (auto simp: N_def)
      then have dxyn: "d (x (n div 2)) (y (n div 2)) < ε/2" 
            and dxnn': "d (x (n div 2)) (x (n' div 2)) < ε/2"
            and dynn': "d (y (n div 2)) (y (n' div 2)) < ε/2"
        using Nx Ny Nxy by blast+
      have inM: "x (n div 2) ∈ M" "x (n' div 2) ∈ M""y (n div 2) ∈ M" "y (n' div 2) ∈ M"
        using MCauchy_def R by blast+
      show "d (if even n then x (n div 2) else y (n div 2)) (if even n' then x (n' div 2) else y (n' div 2)) < ε"
      proof (cases "even n")
        case nt: True
        show ?thesis
        proof (cases "even n'")
          case True
          with ‹ε > 0› nt dxnn' show ?thesis by auto
        next
          case False
          with nt dxyn dynn' inM triangle show ?thesis
            by fastforce
        qed
      next
        case nf: False
        show ?thesis 
        proof (cases "even n'")
          case True
          then show ?thesis
            by (smt (verit) ‹ε > 0› dxyn dxnn' triangle commute inM field_sum_of_halves)
        next
          case False
          with ‹ε > 0› nf dynn' show ?thesis by auto
        qed
      qed
    qed
  qed
qed

lemma MCauchy_interleaving:
   "MCauchy (λn. if even n then σ(n div 2) else a) ⟷
    range σ ⊆ M ∧ limitin mtopology σ a sequentially"  (is "?lhs=?rhs")
proof -
  have "?lhs ⟷ (MCauchy σ ∧ a ∈ M ∧ (λn. d (σ n) a) <---- 0)"
    by (simp add: MCauchy_interleaving_gen [where y = "λn. a"])
  also have "... = ?rhs"
    by (metis MCauchy_def always_eventually convergent_imp_MCauchy limitin_metric_dist_null range_subsetD)
  finally show ?thesis .
qed

lemma mcomplete_nest:
   "mcomplete ⟷
      (∀C::nat →'a set. (∀n. closedin mtopology (C n)) ∧
          (∀n. C n ≠ {}) ∧ decseq C ∧ (∀ε>0. ∃n a. C n ⊆ mcball a ε)
          ⟶ ∩ (range C) ≠ {})" (is "?lhs=?rhs")
proof
  assume L: ?lhs 
  show ?rhs
    unfolding imp_conjL
  proof (intro strip)
    fix C :: "nat → 'a set"
    assume clo: "∀n. closedin mtopology (C n)"
      and ne: "∀n. C n ≠ ({}::'a set)"
      and dec: "decseq C"
      and cover [rule_format]: "∀ε>0. ∃n a. C n ⊆ mcball a ε"
    obtain σ where σ: "∧n. σ n ∈ C n"
      by (meson ne empty_iff set_eq_iff)
    have "MCauchy σ"
      unfolding MCauchy_def
    proof (intro conjI strip)
      show "range σ ⊆ M"
        using σ clo metric_closedin_iff_sequentially_closed by auto 
      fix ε :: real
      assume "ε > 0"
      then obtain N a where N: "C N ⊆ mcball a (ε/3)"
        using cover by fastforce
      have "d (σ m) (σ n) < ε" if "N ≤ m" "N ≤ n" for m n
      proof -
        have "d a (σ m) ≤ ε/3" "d a (σ n) ≤ ε/3"
          using dec N σ that by (fastforce simp: decseq_def)+
        then have "d (σ m) (σ n) ≤ ε/3 + ε/3"
          using triangle σ commute dec decseq_def subsetD that N
          by (smt (verit, ccfv_threshold) in_mcball)
        also have "... < ε"
          using ‹ε > 0› by auto
        finally show ?thesis .
      qed
      then show "∃N. ∀m n. N ≤ m ⟶ N ≤ n ⟶ d (σ m) (σ n) < ε"
        by blast
    qed
    then obtain x where x: "limitin mtopology σ x sequentially"
      using L mcomplete_def by blast
    have "x ∈ C n" for n
    proof (rule limitin_closedin [OF x])
      show "closedin mtopology (C n)"
        by (simp add: clo)
      show "∀_F x in sequentially. σ x ∈ C n"
        by (metis σ dec decseq_def eventually_sequentiallyI subsetD)
    qed auto
    then show "∩ (range C) ≠ {}"
      by blast
qed
next
  assume R: ?rhs  
  show ?lhs
    unfolding mcomplete_def
  proof (intro strip)
    fix σ
    assume "MCauchy σ"
    then have "range σ ⊆ M"
      using MCauchy_def by blast
    define C where "C ≡ λn. mtopology closure_of (σ ` {n..})"
    have "∀n. closedin mtopology (C n)" 
      by (auto simp: C_def)
    moreover
    have ne: "∧n. C n ≠ {}"
      using ‹MCauchy σ› by (auto simp: C_def MCauchy_def disjnt_iff closure_of_eq_empty_gen)
    moreover
    have dec: "decseq C"
      unfolding monotone_on_def
    proof (intro strip)
      fix m n::nat
      assume "m ≤ n"
      then have "{n..} ⊆ {m..}"
        by auto
      then show "C n ⊆ C m"
        unfolding C_def by (meson closure_of_mono image_mono)
    qed
    moreover
    have C: "∃N u. C N ⊆ mcball u ε" if "ε>0" for ε
    proof -
      obtain N where "∧m n. N ≤ m ∧ N ≤ n ==> d (σ m) (σ n) < ε"
        by (meson MCauchy_def ‹0 < \ε› ‹MCauchy σ›)
      then have "σ ` {N..} ⊆ mcball (σ N) ε"
        using MCauchy_def ‹MCauchy σ› by (force simp: less_eq_real_def)
      then have "C N ⊆ mcball (σ N) ε"
        by (simp add: C_def closure_of_minimal)
      then show ?thesis
        by blast
    qed
    ultimately obtain l where x: "l ∈ ∩ (range C)"
      by (metis R ex_in_conv)
    then have *: "∧ε N. 0 < ε ==> ∃n'. N ≤ n' ∧ l ∈ M ∧ σ n' ∈ M ∧ d l (σ n') < ε"
      by (force simp: C_def metric_closure_of)
    then have "l ∈ M"
      using gt_ex by blast
    show "∃l. limitin mtopology σ l sequentially"
      unfolding limitin_metric
    proof (intro conjI strip exI)
      show "l ∈ M"
        using ‹∀n. closedin mtopology (C n)› closedin_subset x by fastforce
      fix ε::real
      assume "ε > 0"
      obtain N where N: "∧m n. N ≤ m ∧ N ≤ n ==> d (σ m) (σ n) < ε/2"
        by (meson MCauchy_def ‹0 < \ε› ‹MCauchy σ› half_gt_zero)
      with * [of "ε/2" N]
      have "∀n≥N. σ n ∈ M ∧ d (σ n) l < ε"
        by (smt (verit) ‹range σ ⊆ M› commute field_sum_of_halves range_subsetD triangle)
      then show "∀_F n in sequentially. σ n ∈ M ∧ d (σ n) l < ε"
        using eventually_sequentially by blast
    qed
  qed
qed


lemma mcomplete_nest_sing:
   "mcomplete ⟷
    (∀C. (∀n. closedin mtopology (C n)) ∧
          (∀n. C n ≠ {}) ∧ decseq C ∧ (∀e>0. ∃n a. C n ⊆ mcball a e)
         ⟶ (∃l. l ∈ M ∧ ∩ (range C) = {l}))"
proof -
  have *: False
    if clo: "∀n. closedin mtopology (C n)"
      and cover: "∀ε>0. ∃n a. C n ⊆ mcball a ε"
      and no_sing: "∧y. y ∈ M ==> ∩ (range C) ≠ {y}"
      and l: "∀n. l ∈ C n"
    for C :: "nat → 'a set" and l
  proof -
    have inM: "∧x. x ∈ ∩ (range C) ==> x ∈ M"
      using closedin_metric clo by fastforce
    then have "l ∈ M"
      by (simp add: l)
    have False if l': "l' ∈ ∩ (range C)" and "l' ≠ l" for l'
    proof -
      have "l' ∈ M"
        using inM l' by blast
      obtain n a where na: "C n ⊆ mcball a (d l l' / 3)"
        using inM ‹l ∈ M› l' ‹l' ≠ l› cover by force
      then have "d a l ≤ (d l l' / 3)" "d a l' ≤ (d l l' / 3)" "a ∈ M"
        using l l' na in_mcball by auto
      then have "d l l' ≤ (d l l' / 3) + (d l l' / 3)"
        using ‹l ∈ M› ‹l' ∈ M› mdist_reverse_triangle by fastforce
      then show False
        using nonneg [of l l'] ‹l' ≠ l› ‹l ∈ M› ‹l' ∈ M› zero by force
    qed
    then show False
      by (metis l ‹l ∈ M› no_sing INT_I empty_iff insertI1 is_singletonE is_singletonI')
  qed
  show ?thesis
    unfolding mcomplete_nest imp_conjL 
    apply (intro all_cong1 imp_cong refl)
    using * 
    by (smt (verit) Inter_iff ex_in_conv range_constant range_eqI)
qed

lemma mcomplete_fip:
   "mcomplete ⟷
    (∀C. (∀C ∈ C. closedin mtopology C) ∧
         (∀e>0. ∃C a. C ∈ C ∧ C ⊆ mcball a e) ∧ (∀F. finite F ∧ F ⊆ C ⟶ ∩ F ≠ {})
        ⟶ ∩ C ≠ {})" 
   (is "?lhs = ?rhs")
proof
  assume L: ?lhs 
  show ?rhs
    unfolding mcomplete_nest_sing imp_conjL
  proof (intro strip)
    fix C :: "'a set set"
    assume clo: "∀C∈C. closedin mtopology C"
      and cover: "∀e>0. ∃C a. C ∈ C ∧ C ⊆ mcball a e"
      and fip: "∀F. finite F ⟶ F ⊆ C ⟶ ∩ F ≠ {}"
    then have "∀n. ∃C. C ∈ C ∧ (∃a. C ⊆ mcball a (inverse (Suc n)))"
      by simp
    then obtain C where C: "∧n. C n ∈ C" 
          and coverC: "∧n. ∃a. C n ⊆ mcball a (inverse (Suc n))"
      by metis
    define D where "D ≡ λn. ∩ (C ` {..n})"
    have cloD: "closedin mtopology (D n)" for n
      unfolding D_def using clo C by blast
    have neD: "D n ≠ {}" for n
      using fip C by (simp add: D_def image_subset_iff)
    have decD: "decseq D"
      by (force simp: D_def decseq_def)
    have coverD: "∃n a. D n ⊆ mcball a ε" if " ε >0" for ε
    proof -
      obtain n where "inverse (Suc n) < ε"
        using ‹0 < \ε› reals_Archimedean by blast
      then obtain a where "C n ⊆ mcball a ε"
        by (meson coverC less_eq_real_def mcball_subset_concentric order_trans)
      then show ?thesis
        unfolding D_def by blast
    qed
    have *: "a ∈ ∩C" if a: "∩ (range D) = {a}" and "a ∈ M" for a
    proof -
      have aC: "a ∈ C n" for n
        using that by (auto simp: D_def)
      have eqa: "∧u. (∀n. u ∈ C n) ==> a = u"
        using that by (auto simp: D_def)
      have "a ∈ T" if "T ∈ C" for T
      proof -
        have cloT: "closedin mtopology (T ∩ D n)" for n
          using clo cloD that by blast
        have "∩ (insert T (C ` {..n})) ≠ {}" for n
          using that C by (intro fip [rule_format]) auto
        then have neT: "T ∩ D n ≠ {}" for n
          by (simp add: D_def)
        have decT: "decseq (λn. T ∩ D n)"
          by (force simp: D_def decseq_def)
        have coverT: "∃n a. T ∩ D n ⊆ mcball a ε" if " ε >0" for ε
          by (meson coverD le_infI2 that)
        show ?thesis
          using L [unfolded mcomplete_nest_sing, rule_format, of "λn. T ∩ D n"] a
          by (force simp: cloT neT decT coverT)
      qed
      then show ?thesis by auto
    qed
    show "∩ C ≠ {}"
      by (metis L cloD neD decD coverD * empty_iff mcomplete_nest_sing)
  qed
next
  assume R [rule_format]: ?rhs
  show ?lhs
    unfolding mcomplete_nest imp_conjL
  proof (intro strip)
    fix C :: "nat → 'a set"
    assume clo: "∀n. closedin mtopology (C n)"
      and ne: "∀n. C n ≠ {}"
      and dec: "decseq C"
      and cover: "∀ε>0. ∃n a. C n ⊆ mcball a ε"
    have "\<Inter>(C ` N) \<noteq> {}" if "finite N" for N
    proof -
      obtain k where "N \<subseteq> {..k}"
        using \<open>finite N\<close> finite_nat_iff_bounded_le by auto
      with dec have "C k \<subseteq> \<Inter>(C ` N)" by (auto simp: decseq_def)
      then show ?thesis
        using ne by force
    qed
    with clo cover R [of "range C"] show "\<Inter> (range C) \<noteq> {}"
      by (metis (no_types, opaque_lifting) finite_subset_image image_iff UNIV_I)
  qed
qed


lemma mcomplete_fip_sing:
   "mcomplete \<longleftrightarrow>
    (\<forall>\<C>. (\<forall>C\<in>\<C>. closedin mtopology C) \<and>
     (\<forall>e>0. \<exists>c a. c \<in> \<C> \<and> c \<subseteq> mcball a e) \<and>
     (\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<C> \<longrightarrow> \<Inter> \<F> \<noteq> {}) \<longrightarrow>
     (\<exists>l. l \<in> M \<and> \<Inter> \<C> = {l}))"
   (is "?lhs = ?rhs")
proof
  have *: "l \<in> M" "\<Inter> \<C> = {l}"
    if clo: "Ball \<C> (closedin mtopology)"
      and cover: "\<forall>e>0. \<exists>C a. C \<in> \<C> \<and> C \<subseteq> mcball a e"
      and fin: "\<forall>\<F>. finite \<F> \<longrightarrow> \<F> \<subseteq> \<C> \<longrightarrow> \<Inter> \<F> \<noteq> {}"
      and l: "l \<in> \<Inter> \<C>"
    for \<C> :: "'a set set" and l
  proof -
    show "l \<in> M"
      by (meson Inf_lower2 clo cover gt_ex metric_closedin_iff_sequentially_closed subsetD that(4))
    show  "\<Inter> \<C> = {l}"
    proof (cases "\<C> = {}")
      case True
      then show ?thesis
        using cover mbounded_pos by auto
    next
      case False
      have CM: "\<And>a. a \<in> \<Inter>\<C> \<Longrightarrow> a \<in> M"
        using False clo closedin_subset by fastforce
      have "l' \<notin> \<Inter> \<C>" if "l' \<noteq> l" for l'
      proof 
        assume l': "l' \<in> \<Inter> \<C>"
        with CM have "l' \<in> M" by blast
        with that \<open>l \<in> M\<close> have gt0: "0 < d l l'"
          by simp
        then obtain C a where "C \<in> \<C>" and C: "C \<subseteq> mcball a (d l l' / 3)"
          using cover [rule_format, of "d l l' / 3"] by auto
        then have "d a l \<le> (d l l' / 3)" "d a l' \<le> (d l l' / 3)" "a \<in> M"
          using l l' in_mcball by auto
        then have "d l l' \<le> (d l l' / 3) + (d l l' / 3)"
          using \<open>l \<in> M\<close> \<open>l' \<in> M\<close> mdist_reverse_triangle by fastforce
        with gt0 show False by auto
      qed
      then show ?thesis
        using l by fastforce
    qed
  qed
  assume L: ?lhs
  with * show ?rhs
    unfolding mcomplete_fip imp_conjL ex_in_conv [symmetric]
    by (elim all_forward imp_forward2 asm_rl) (blast intro:  elim: )
next
  assume ?rhs then show ?lhs
    unfolding mcomplete_fip by (force elim!: all_forward)
qed

end

definition mcomplete_of :: "'a metric \<Rightarrow> bool"
  where "mcomplete_of \<equiv> \<lambda>m. Metric_space.mcomplete (mspace m) (mdist m)"

lemma (in Metric_space) mcomplete_of [simp]: "mcomplete_of (metric (M,d)) = mcomplete"
  by (simp add: mcomplete_of_def)

lemma mcomplete_trivial: "Metric_space.mcomplete {} (\<lambda>x y. 0)"
  using Metric_space.intro Metric_space.mcomplete_empty_mspace by force

lemma mcomplete_trivial_singleton: "Metric_space.mcomplete {\<lambda>x. a} (\<lambda>x y. 0)"
proof -
  interpret Metric_space "{\<lambda>x. a}" "\<lambda>x y. 0"
    by unfold_locales auto
  show ?thesis
    unfolding mcomplete_def MCauchy_def image_subset_iff by (metis UNIV_I limit_metric_sequentially)
qed

lemma MCauchy_iff_Cauchy [iff]: "Met_TC.MCauchy = Cauchy"
  by (force simp: Cauchy_def Met_TC.MCauchy_def)

lemma mcomplete_iff_complete [iff]:
  "Met_TC.mcomplete TYPE('a::metric_space) \<longleftrightarrow> complete (UNIV::'a set)"
  by (auto simp: Met_TC.mcomplete_def complete_def)

context Submetric
begin 

lemma MCauchy_submetric:
   "sub.MCauchy \<sigma> \<longleftrightarrow> range \<sigma> \<subseteq> A \<and> MCauchy \<sigma>"
  using MCauchy_def sub.MCauchy_def subset by force

lemma closedin_mcomplete_imp_mcomplete:
  assumes clo: "closedin mtopology A" and "mcomplete"
  shows "sub.mcomplete"
  unfolding sub.mcomplete_def
proof (intro strip)
  fix \<sigma>
  assume "sub.MCauchy \<sigma>"
  then have \<sigma>: "MCauchy \<sigma>" "range \<sigma> \<subseteq> A"
    using MCauchy_submetric by blast+
  then obtain x where x: "limitin mtopology \<sigma> x sequentially"
    using \<open>mcomplete\<close> unfolding mcomplete_def by blast
  then have "x \<in> A"
    using \<sigma> clo metric_closedin_iff_sequentially_closed by force
  with \<sigma> x show "\<exists>x. limitin sub.mtopology \<sigma> x sequentially"
    using limitin_submetric_iff range_subsetD by fastforce
qed


lemma sequentially_closedin_mcomplete_imp_mcomplete:
  assumes "mcomplete" and "\<And>\<sigma> l. range \<sigma> \<subseteq> A \<and> limitin mtopology \<sigma> l sequentially \<Longrightarrow> l \<in> A"
  shows "sub.mcomplete"
  using assms closedin_mcomplete_imp_mcomplete metric_closedin_iff_sequentially_closed subset by blast

end

context Metric_space
begin

lemma mcomplete_Un:
  assumes A: "Submetric M d A" "Metric_space.mcomplete A d" 
      and B: "Submetric M d B" "Metric_space.mcomplete B d"
  shows   "Submetric M d (A \<union> B)" "Metric_space.mcomplete (A \<union> B) d" 
proof -
  show "Submetric M d (A \<union> B)"
    by (meson assms le_sup_iff Submetric_axioms_def Submetric_def) 
  then interpret MAB: Metric_space "A \<union> B" d
    by (meson Submetric.subset subspace)
  interpret MA: Metric_space A d
    by (meson A Submetric.subset subspace)
  interpret MB: Metric_space B d
    by (meson B Submetric.subset subspace)
  show "Metric_space.mcomplete (A \<union> B) d"
    unfolding MAB.mcomplete_def
  proof (intro strip)
    fix \<sigma>
    assume "MAB.MCauchy \<sigma>"
    then have "range \<sigma> \<subseteq> A \<union> B"
      using MAB.MCauchy_def by blast
    then have "UNIV \<subseteq> \<sigma> -` A \<union> \<sigma> -` B"
      by blast
    then consider "infinite (\<sigma> -` A)" | "infinite (\<sigma> -` B)"
      using finite_subset by auto
    then show "\<exists>x. limitin MAB.mtopology \<sigma> x sequentially"
    proof cases
      case 1
      then obtain r where "strict_mono r" and r: "\<And>n::nat. r n \<in> \<sigma> -` A"
        using infinite_enumerate by blast 
      then have "MA.MCauchy (\<sigma> \<circ> r)"
        using MA.MCauchy_def MAB.MCauchy_def MAB.MCauchy_subsequence \<open>MAB.MCauchy \<sigma>\<close> by auto
      with A obtain x where "limitin MA.mtopology (\<sigma> \<circ> r) x sequentially"
        using MA.mcomplete_def by blast
      then have "limitin MAB.mtopology (\<sigma> \<circ> r) x sequentially"
        by (metis MA.limit_metric_sequentially MAB.limit_metric_sequentially UnCI)
      then show ?thesis
        using MAB.MCauchy_convergent_subsequence \<open>MAB.MCauchy \<sigma>\<close> \<open>strict_mono r\<close> by blast
    next
      case 2
      then obtain r where "strict_mono r" and r: "\<And>n::nat. r n \<in> \<sigma> -` B"
        using infinite_enumerate by blast 
      then have "MB.MCauchy (\<sigma> \<circ> r)"
        using MB.MCauchy_def MAB.MCauchy_def MAB.MCauchy_subsequence \<open>MAB.MCauchy \<sigma>\<close> by auto
      with B obtain x where "limitin MB.mtopology (\<sigma> \<circ> r) x sequentially"
        using MB.mcomplete_def by blast
      then have "limitin MAB.mtopology (\<sigma> \<circ> r) x sequentially"
        by (metis MB.limit_metric_sequentially MAB.limit_metric_sequentially UnCI)
      then show ?thesis
        using MAB.MCauchy_convergent_subsequence \<open>MAB.MCauchy \<sigma>\<close> \<open>strict_mono r\<close> by blast
    qed
  qed
qed

lemma mcomplete_Union:
  assumes "finite \<S>"
    and "\<And>A. A \<in> \<S> \<Longrightarrow> Submetric M d A" "\<And>A. A \<in> \<S> \<Longrightarrow> Metric_space.mcomplete A d"
  shows   "Submetric M d (\<Union>\<S>)" "Metric_space.mcomplete (\<Union>\<S>) d" 
  using assms
  by (induction rule: finite_induct) (auto simp: mcomplete_Un)

lemma mcomplete_Inter:
  assumes "finite \<S>" "\<S> \<noteq> {}"
    and sub: "\<And>A. A \<in> \<S> \<Longrightarrow> Submetric M d A" 
    and comp: "\<And>A. A \<in> \<S> \<Longrightarrow> Metric_space.mcomplete A d"
  shows "Submetric M d (\<Inter>\<S>)" "Metric_space.mcomplete (\<Inter>\<S>) d"
proof -
  show "Submetric M d (\<Inter>\<S>)"
    using assms unfolding Submetric_def Submetric_axioms_def
    by (metis Inter_lower equals0I inf.orderE le_inf_iff) 
  then interpret MS: Submetric M d "\<Inter>\<S>" 
    by (meson Submetric.subset subspace)
  show "Metric_space.mcomplete (\<Inter>\<S>) d"
    unfolding MS.sub.mcomplete_def
  proof (intro strip)
    fix \<sigma>
    assume "MS.sub.MCauchy \<sigma>"
    then have "range \<sigma> \<subseteq> \<Inter>\<S>"
      using MS.MCauchy_submetric by blast
    obtain A where "A \<in> \<S>" and A: "Metric_space.mcomplete A d"
      using assms by blast
    then have "range \<sigma> \<subseteq> A"
      using \<open>range \<sigma> \<subseteq> \<Inter>\<S>\<close> by blast
    interpret SA: Submetric M d A
      by (meson \<open>A \<in> \<S>\<close> sub Submetric.subset subspace)
    have "MCauchy \<sigma>"
      using MS.MCauchy_submetric \<open>MS.sub.MCauchy \<sigma>\<close> by blast
    then obtain x where x: "limitin SA.sub.mtopology \<sigma> x sequentially"
      by (metis A SA.sub.MCauchy_def SA.sub.mcomplete_alt MCauchy_def \<open>range \<sigma> \<subseteq> A\<close>)
    show "\<exists>x. limitin MS.sub.mtopology \<sigma> x sequentially"
      unfolding MS.limitin_submetric_iff
    proof (intro exI conjI)
      show "x \<in> \<Inter> \<S>"
      proof clarsimp
        fix U
        assume "U \<in> \<S>"
        interpret SU: Submetric M d U 
          by (meson \<open>U \<in> \<S>\<close> sub Submetric.subset subspace)
        have "range \<sigma> \<subseteq> U"
          using \<open>U \<in> \<S>\<close> \<open>range \<sigma> \<subseteq> \<Inter> \<S>\<close> by blast
        moreover have "Metric_space.mcomplete U d"
          by (simp add: \<open>U \<in> \<S>\<close> comp)
        ultimately obtain x' where x': "limitin SU.sub.mtopology \<sigma> x' sequentially"
          using MCauchy_def SU.sub.MCauchy_def SU.sub.mcomplete_alt \<open>MCauchy \<sigma>\<close> by meson 
        have "x' = x"
        proof (intro limitin_metric_unique)
          show "limitin mtopology \<sigma> x' sequentially"
            by (meson SU.Submetric_axioms Submetric.limitin_submetric_iff x')
          show "limitin mtopology \<sigma> x sequentially"
            by (meson SA.Submetric_axioms Submetric.limitin_submetric_iff x)
        qed auto
        then show "x \<in> U"
          using SU.sub.limitin_mspace x' by blast
      qed
      show "\<forall>\<^sub>F n in sequentially. \<sigma> n \<in> \<Inter>\<S>"
        by (meson \<open>range \<sigma> \<subseteq> \<Inter> \<S>\<close> always_eventually range_subsetD)
      show "limitin mtopology \<sigma> x sequentially"
        by (meson SA.Submetric_axioms Submetric.limitin_submetric_iff x)
    qed
  qed
qed


lemma mcomplete_Int:
  assumes A: "Submetric M d A" "Metric_space.mcomplete A d" 
      and B: "Submetric M d B" "Metric_space.mcomplete B d"
    shows   "Submetric M d (A \<inter> B)" "Metric_space.mcomplete (A \<inter> B) d"
  using mcomplete_Inter [of "{A,B}"] assms by force+

subsection\<open>Totally bounded subsets of metric spaces\<close>

definition mtotally_bounded 
  where "mtotally_bounded S \<equiv> \<forall>\<epsilon>>0. \<exists>K. finite K \<and> K \<subseteq> S \<and> S \<subseteq> (\<Union>x\<in>K. mball x \<epsilon>)"

lemma mtotally_bounded_empty [iff]: "mtotally_bounded {}"
by (simp add: mtotally_bounded_def)

lemma finite_imp_mtotally_bounded:
   "\<lbrakk>finite S; S \<subseteq> M\<rbrakk> \<Longrightarrow> mtotally_bounded S"
  by (auto simp: mtotally_bounded_def)

lemma mtotally_bounded_imp_subset: "mtotally_bounded S \<Longrightarrow> S \<subseteq> M"
  by (force simp: mtotally_bounded_def intro!: zero_less_one)

lemma mtotally_bounded_sing [simp]:
   "mtotally_bounded {x} \<longleftrightarrow> x \<in> M"
  by (meson empty_subsetI finite.simps finite_imp_mtotally_bounded insert_subset mtotally_bounded_imp_subset)

lemma mtotally_bounded_Un:
  assumes  "mtotally_bounded S" "mtotally_bounded T"
  shows "mtotally_bounded (S \<union> T)"
proof -
  have "\<exists>K. finite K \<and> K \<subseteq> S \<union> T \<and> S \<union> T \<subseteq> (\<Union>x\<in>K. mball x e)"
    if  "e>0" and K: "finite K \<and> K \<subseteq> S \<and> S \<subseteq> (\<Union>x\<in>K. mball x e)"
      and L: "finite L \<and> L \<subseteq> T \<and> T \<subseteq> (\<Union>x\<in>L. mball x e)" for K L e
    using that by (rule_tac x="K \<union> L" in exI) auto
  with assms show ?thesis
    unfolding mtotally_bounded_def by presburger
qed
 
lemma mtotally_bounded_Union:
  assumes "finite f" "\<And>S. S \<in> f \<Longrightarrow> mtotally_bounded S"
  shows "mtotally_bounded (\<Union>f)"
  using assms by (induction f) (auto simp: mtotally_bounded_Un)

lemma mtotally_bounded_imp_mbounded:
  assumes "mtotally_bounded S"
  shows "mbounded S"
proof -
  obtain K where "finite K \<and> K \<subseteq> S \<and> S \<subseteq> (\<Union>x\<in>K. mball x 1)" 
    using assms by (force simp: mtotally_bounded_def)
  then show ?thesis
    by (smt (verit) finite_imageI image_iff mbounded_Union mbounded_mball mbounded_subset)
qed


lemma mtotally_bounded_sequentially:
  "mtotally_bounded S \<longleftrightarrow>
    S \<subseteq> M \<and> (\<forall>\<sigma>::nat \<Rightarrow> 'a. range \<sigma> \<subseteq> S \<longrightarrow> (\<exists>r. strict_mono r \<and> MCauchy (\<sigma> \<circ> r)))"
  (is "_ \<longleftrightarrow> _ \<and> ?rhs")
proof (cases "S \<subseteq> M")
  case True
  show ?thesis
  proof -
    { fix \<sigma> :: "nat \<Rightarrow> 'a"                                                            
      assume L: "mtotally_bounded S" and \<sigma>: "range \<sigma> \<subseteq> S"
      have "\<exists>j > i. d (\<sigma> i) (\<sigma> j) < 3*\<epsilon>/2 \<and> infinite (\<sigma> -` mball (\<sigma> j) (\<epsilon>/2))"
        if inf: "infinite (\<sigma> -` mball (\<sigma> i) \<epsilon>)" and "\<epsilon> > 0" for i \<epsilon>
      proof -
        obtain K where "finite K" "K \<subseteq> S" and K: "S \<subseteq> (\<Union>x\<in>K. mball x (\<epsilon>/4))"
          by (metis L mtotally_bounded_def \<open>\<epsilon> > 0\<close> zero_less_divide_iff zero_less_numeral)
        then have K_imp_ex: "\<And>y. y \<in> S \<Longrightarrow> \<exists>x\<in>K. d x y < \<epsilon>/4"
          by fastforce
        have False if "\<forall>x\<in>K. d x (\<sigma> i) < \<epsilon> + \<epsilon>/4 \<longrightarrow> finite (\<sigma> -` mball x (\<epsilon>/4))"
        proof -
          have "\<exists>w. w \<in> K \<and> d w (\<sigma> i) < 5 * \<epsilon>/4 \<and> d w (\<sigma> j) < \<epsilon>/4"
            if "d (\<sigma> i) (\<sigma> j) < \<epsilon>" for j
          proof -
            obtain w where w: "d w (\<sigma> j) < \<epsilon>/4" "w \<in> K"
              using K_imp_ex \<sigma> by blast
            then have "d w (\<sigma> i) < \<epsilon> + \<epsilon>/4"
              by (smt (verit, ccfv_SIG) True \<open>K \<subseteq> S\<close> \<sigma> rangeI subset_eq that triangle')
            with w show ?thesis
              using in_mball by auto
          qed
          then have "(\<sigma> -` mball (\<sigma> i) \<epsilon>) \<subseteq> (\<Union>x\<in>K. if d x (\<sigma> i) < \<epsilon> + \<epsilon>/4 then \<sigma> -` mball x (\<epsilon>/4) else {})"
            using True \<open>K \<subseteq> S\<close> by force
          then show False
            using finite_subset inf \<open>finite K\<close> that by fastforce
        qed
        then obtain x where "x \<in> K" and dxi: "d x (\<sigma> i) < \<epsilon> + \<epsilon>/4" and infx: "infinite (\<sigma> -` mball x (\<epsilon>/4))"
          by blast
        then obtain j where "j \<in> (\<sigma> -` mball x (\<epsilon>/4)) - {..i}"
          using bounded_nat_set_is_finite by (meson Diff_infinite_finite finite_atMost)
        then have "j > i" and dxj: "d x (\<sigma> j) < \<epsilon>/4" 
          by auto
        have "(\<sigma> -` mball x (\<epsilon>/4)) \<subseteq> (\<sigma> -` mball y (\<epsilon>/2))" if "d x y < \<epsilon>/4" "y \<in> M" for y
          using that by (simp add: mball_subset vimage_mono)
        then have infj: "infinite (\<sigma> -` mball (\<sigma> j) (\<epsilon>/2))"
          by (meson True \<open>d x (\<sigma> j) < \<epsilon>/4\<close> \<sigma> in_mono infx rangeI finite_subset)
        have "\<sigma> i \<in> M" "\<sigma> j \<in> M" "x \<in> M"  
          using True \<open>K \<subseteq> S\<close> \<open>x \<in> K\<close> \<sigma> by force+
        then have "d (\<sigma> i) (\<sigma> j) \<le> d x (\<sigma> i) + d x (\<sigma> j)"
          using triangle'' by blast
        also have "\<dots> < 3*\<epsilon>/2"
          using dxi dxj by auto
        finally have "d (\<sigma> i) (\<sigma> j) < 3*\<epsilon>/2" .
        with \<open>i < j\<close> infj show ?thesis by blast
      qed
      then obtain nxt where nxt: "\<And>i \<epsilon>. \<lbrakk>\<epsilon> > 0; infinite (\<sigma> -` mball (\<sigma> i) \<epsilon>)\<rbrakk> \<Longrightarrow> 
                 nxt i \<epsilon> > i \<and> d (\<sigma> i) (\<sigma> (nxt i \<epsilon>)) < 3*\<epsilon>/2 \<and> infinite (\<sigma> -` mball (\<sigma> (nxt i \<epsilon>)) (\<epsilon>/2))"
        by metis
      have "mbounded S"
        using L by (simp add: mtotally_bounded_imp_mbounded)
      then obtain B where B: "\<forall>y \<in> S. d (\<sigma> 0) y \<le> B" and "B > 0"
        by (meson \<sigma> mbounded_alt_pos range_subsetD)
      define eps where "eps \<equiv> \<lambda>n. (B+1) / 2^n"
      have [simp]: "eps (Suc n) = eps n / 2" "eps n > 0" for n
        using \<open>B > 0\<close> by (auto simp: eps_def)
      have "UNIV \<subseteq> \<sigma> -` mball (\<sigma> 0) (B+1)"
        using B True \<sigma> unfolding image_iff subset_iff
        by (smt (verit, best) UNIV_I in_mball vimageI)
      then have inf0: "infinite (\<sigma> -` mball (\<sigma> 0) (eps 0))"
        using finite_subset by (auto simp: eps_def)
      define r where "r \<equiv> rec_nat 0 (\<lambda>n rec. nxt rec (eps n))"
      have [simp]: "r 0 = 0" "r (Suc n) = nxt (r n) (eps n)" for n
        by (auto simp: r_def)
      have \<sigma>rM[simp]: "\<sigma> (r n) \<in> M" for n
        using True \<sigma> by blast
      have inf: "infinite (\<sigma> -` mball (\<sigma> (r n)) (eps n))" for n
      proof (induction n)
        case 0 then show ?case  
          by (simp add: inf0)
      next
        case (Suc n) then show ?case
          using nxt [of "eps n" "r n"] by simp
      qed
      then have "r (Suc n) > r n" for n
        by (simp add: nxt)
      then have "strict_mono r"
        by (simp add: strict_mono_Suc_iff)
      have d_less: "d (\<sigma> (r n)) (\<sigma> (r (Suc n))) < 3 * eps n / 2" for n
        using nxt [OF _ inf] by simp
      have eps_plus: "eps (k + n) = eps n * (1/2)^k" for k n
        by (simp add: eps_def power_add field_simps)
      have *: "d (\<sigma> (r n)) (\<sigma> (r (k + n))) < 3 * eps n" for n k
      proof -
        have "d (\<sigma> (r n)) (\<sigma> (r (k+n))) \<le> 3/2 * eps n * (\<Sum>i<k. (1/2)^i)"
        proof (induction k)
          case 0 then show ?case 
            by simp
        next
          case (Suc k)
          have "d (\<sigma> (r n)) (\<sigma> (r (Suc k + n))) \<le> d (\<sigma> (r n)) (\<sigma> (r (k + n))) + d (\<sigma> (r (k + n))) (\<sigma> (r (Suc (k + n))))"
            by (metis \<sigma>rM add.commute add_Suc_right triangle)
          with d_less[of "k+n"] Suc show ?case
            by (simp add: algebra_simps eps_plus)
        qed
        also have "\<dots> < 3/2 * eps n * 2"
          using geometric_sum [of "1/2::real" k] by simp
        finally show ?thesis by simp
      qed
      have "\<exists>N. \<forall>n\<ge>N. \<forall>n'\<ge>N. d (\<sigma> (r n)) (\<sigma> (r n')) < \<epsilon>" if "\<epsilon> > 0" for \<epsilon>
      proof -
        define N where "N \<equiv> nat \<lceil>(log 2 (6*(B+1) / \<epsilon>))\<rceil>"
        have \<section>: "b \<le> 2 ^ nat \<lceil>log 2 b\<rceil>" for b
          by (smt (verit) less_log_of_power real_nat_ceiling_ge)
        have N: "6 * eps N \<le> \<epsilon>"
          using \<section> [of "(6*(B+1) / \<epsilon>)"] that by (auto simp: N_def eps_def field_simps)
        have "d (\<sigma> (r N)) (\<sigma> (r n)) < 3 * eps N" if "n \<ge> N" for n
          by (metis * add.commute nat_le_iff_add that)
        then have "\<forall>n\<ge>N. \<forall>n'\<ge>N. d (\<sigma> (r n)) (\<sigma> (r n')) < 3 * eps N + 3 * eps N"
          by (smt (verit, best) \<sigma>rM triangle'')
        with N show ?thesis
          by fastforce
      qed
      then have "MCauchy (\<sigma> \<circ> r)"
        unfolding MCauchy_def using True \<sigma> by auto
      then have "\<exists>r. strict_mono r \<and> MCauchy (\<sigma> \<circ> r)"
        using \<open>strict_mono r\<close> by blast      
    }
    moreover
    { assume R: ?rhs
      have "mtotally_bounded S"
        unfolding mtotally_bounded_def
      proof (intro strip)
        fix \<epsilon> :: real
        assume "\<epsilon> > 0"
        have False if \<section>: "\<And>K. \<lbrakk>finite K; K \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>s\<in>S. s \<notin> (\<Union>x\<in>K. mball x \<epsilon>)"
        proof -
          obtain f where f: "\<And>K. \<lbrakk>finite K; K \<subseteq> S\<rbrakk> \<Longrightarrow> f K \<in> S \<and> f K \<notin> (\<Union>x\<in>K. mball x \<epsilon>)"
            using \<section> by metis
          define \<sigma> where "\<sigma> \<equiv> wfrec less_than (\<lambda>seq n. f (seq ` {..<n}))"
          have \<sigma>_eq: "\<sigma> n = f (\<sigma> ` {..<n})" for n
            by (simp add: cut_apply def_wfrec [OF \<sigma>_def])
          have [simp]: "\<sigma> n \<in> S" for n
            using wf_less_than
          proof (induction n rule: wf_induct_rule)
            case (less n) with f show ?case
              by (auto simp: \<sigma>_eq [of n])
          qed
          then have "range \<sigma> \<subseteq> S" by blast
          have \<sigma>: "p < n \<Longrightarrow> \<epsilon> \<le> d (\<sigma> p) (\<sigma> n)" for n p
            using f[of "\<sigma> ` {..<n}"] True by (fastforce simp: \<sigma>_eq [of n] Ball_def)
          then obtain r where "strict_mono r" "MCauchy (\<sigma> \<circ> r)"
            by (meson R \<open>range \<sigma> \<subseteq> S\<close>)
          with \<open>0 < \<epsilon>\<close> obtain N 
            where N: "\<And>n n'. \<lbrakk>n\<ge>N; n'\<ge>N\<rbrakk> \<Longrightarrow> d (\<sigma> (r n)) (\<sigma> (r n')) < \<epsilon>"
            by (force simp: MCauchy_def)
          show ?thesis
            using N [of N "Suc (r N)"] \<open>strict_mono r\<close>
            by (smt (verit) Suc_le_eq \<sigma> le_SucI order_refl strict_mono_imp_increasing)
        qed
        then show "\<exists>K. finite K \<and> K \<subseteq> S \<and> S \<subseteq> (\<Union>x\<in>K. mball x \<epsilon>)"
          by blast
      qed
    }
    ultimately show ?thesis 
      using True by blast
  qed
qed (use mtotally_bounded_imp_subset in auto)


lemma mtotally_bounded_subset:
   "\<lbrakk>mtotally_bounded S; T \<subseteq> S\<rbrakk> \<Longrightarrow> mtotally_bounded T"
  by (meson mtotally_bounded_sequentially order_trans) 

lemma mtotally_bounded_submetric:
  assumes "mtotally_bounded S" "S \<subseteq> T" "T \<subseteq> M"
  shows "Metric_space.mtotally_bounded T d S"
proof -
  interpret Submetric M d T
    using \<open>T \<subseteq> M\<close> by unfold_locales
  show ?thesis
    using assms
    unfolding sub.mtotally_bounded_def mtotally_bounded_def
    by (force simp: subset_iff elim!: all_forward ex_forward)
qed

lemma mtotally_bounded_absolute:
   "mtotally_bounded S \<longleftrightarrow> S \<subseteq> M \<and> Metric_space.mtotally_bounded S d S "
proof -
  have "mtotally_bounded S" if "S \<subseteq> M" "Metric_space.mtotally_bounded S d S"
  proof -
    interpret Submetric M d S
      using \<open>S \<subseteq> M\<close> by unfold_locales
    show ?thesis
      using that
      by (meson MCauchy_submetric mtotally_bounded_sequentially sub.mtotally_bounded_sequentially)
  qed
  moreover have "mtotally_bounded S \<Longrightarrow> Metric_space.mtotally_bounded S d S"
    by (simp add: mtotally_bounded_imp_subset mtotally_bounded_submetric)
  ultimately show ?thesis
    using mtotally_bounded_imp_subset by blast
qed

lemma mtotally_bounded_closure_of:
  assumes "mtotally_bounded S"
  shows "mtotally_bounded (mtopology closure_of S)"
proof -
  have "S \<subseteq> M"
    by (simp add: assms mtotally_bounded_imp_subset)
  have "mtotally_bounded(mtopology closure_of S)"
    unfolding mtotally_bounded_def
  proof (intro strip)
    fix \<epsilon>::real
    assume "\<epsilon> > 0"
    then obtain K where "finite K" "K \<subseteq> S" and K: "S \<subseteq> (\<Union>x\<in>K. mball x (\<epsilon>/2))"
      by (metis assms mtotally_bounded_def half_gt_zero)
    have "mtopology closure_of S \<subseteq> (\<Union>x\<in>K. mball x \<epsilon>)"
      unfolding metric_closure_of
    proof clarsimp
      fix x
      assume "x \<in> M" and x: "\<forall>r>0. \<exists>y\<in>S. y \<in> M \<and> d x y < r"
      then obtain y where "y \<in> S" and y: "d x y < \<epsilon>/2"
        using \<open>0 < \<epsilon>\<close> half_gt_zero by blast
      then obtain x' where "x' \<in> K" "y \<in> mball x' (\<epsilon>/2)"
        using K by auto
      then have "d x' x < \<epsilon>/2 + \<epsilon>/2"
        using triangle y \<open>x \<in> M\<close> commute by fastforce
      then show "\<exists>x'\<in>K. x' \<in> M \<and> d x' x < \<epsilon>"
        using \<open>K \<subseteq> S\<close> \<open>S \<subseteq> M\<close> \<open>x' \<in> K\<close> by force
    qed
    then show "\<exists>K. finite K \<and> K \<subseteq> mtopology closure_of S \<and> mtopology closure_of S \<subseteq> (\<Union>x\<in>K. mball x \<epsilon>)"
      using closure_of_subset_Int  \<open>K \<subseteq> S\<close> \<open>finite K\<close> K by fastforce
  qed
  then show ?thesis
    by (simp add: assms inf.absorb2 mtotally_bounded_imp_subset)
qed

lemma mtotally_bounded_closure_of_eq:
   "S \<subseteq> M \<Longrightarrow> mtotally_bounded (mtopology closure_of S) \<longleftrightarrow> mtotally_bounded S"
  by (metis closure_of_subset mtotally_bounded_closure_of mtotally_bounded_subset topspace_mtopology)

lemma mtotally_bounded_cauchy_sequence:
  assumes "MCauchy \<sigma>"
  shows "mtotally_bounded (range \<sigma>)"
  unfolding MCauchy_def mtotally_bounded_def
proof (intro strip)
  fix \<epsilon>::real
  assume "\<epsilon> > 0"
  then obtain N where "\<And>n. N \<le> n \<Longrightarrow> d (\<sigma> N) (\<sigma> n) < \<epsilon>"
    using assms by (force simp: MCauchy_def)
  then have "\<And>m. \<exists>n\<le>N. \<sigma> n \<in> M \<and> \<sigma> m \<in> M \<and> d (\<sigma> n) (\<sigma> m) < \<epsilon>"
    by (metis MCauchy_def assms mdist_zero nle_le range_subsetD)
  then
  show "\<exists>K. finite K \<and> K \<subseteq> range \<sigma> \<and> range \<sigma> \<subseteq> (\<Union>x\<in>K. mball x \<epsilon>)"
    by (rule_tac x="\<sigma> ` {0..N}" in exI) force
qed

lemma MCauchy_imp_mbounded:
   "MCauchy \<sigma> \<Longrightarrow> mbounded (range \<sigma>)"
  by (simp add: mtotally_bounded_cauchy_sequence mtotally_bounded_imp_mbounded)

subsection\<open>Compactness in metric spaces\<close>

lemma Bolzano_Weierstrass_property:
  assumes "S \<subseteq> U" "S \<subseteq> M"
  shows
   "(\<forall>\<sigma>::nat\<Rightarrow>'a. range \<sigma> \<subseteq> S
         \<longrightarrow> (\<exists>l r. l \<in> U \<and> strict_mono r \<and> limitin mtopology (\<sigma> \<circ> r) l sequentially)) \<longleftrightarrow>
    (\<forall>T. T \<subseteq> S \<and> infinite T \<longrightarrow> U \<inter> mtopology derived_set_of T \<noteq> {})"  (is "?lhs=?rhs")
proof
  assume L: ?lhs 
  show ?rhs
  proof clarify
    fix T
    assume "T \<subseteq> S" and "infinite T"
      and T: "U \<inter> mtopology derived_set_of T = {}"
    then obtain \<sigma> :: "nat\<Rightarrow>'a" where "inj \<sigma>" "range \<sigma> \<subseteq> T"
      by (meson infinite_countable_subset)
    with L obtain l r where "l \<in> U" "strict_mono r" 
           and lr: "limitin mtopology (\<sigma> \<circ> r) l sequentially"
      by (meson \<open>T \<subseteq> S\<close> subset_trans)
    then obtain \<epsilon> where "\<epsilon> > 0" and \<epsilon>: "\<And>y. y \<in> T \<Longrightarrow> y = l \<or> \<not> d l y < \<epsilon>"
      using T \<open>T \<subseteq> S\<close> \<open>S \<subseteq> M\<close> 
      by (force simp: metric_derived_set_of limitin_metric disjoint_iff)
    with lr have "\<forall>\<^sub>F n in sequentially. \<sigma> (r n) \<in> M \<and> d (\<sigma> (r n)) l < \<epsilon>"
      by (auto simp: limitin_metric)
    then obtain N where N: "d (\<sigma> (r N)) l < \<epsilon>" "d (\<sigma> (r (Suc N))) l < \<epsilon>"
      using less_le_not_le by (auto simp: eventually_sequentially)
    moreover have "\<sigma> (r N) \<noteq> l \<or> \<sigma> (r (Suc N)) \<noteq> l"
      by (meson \<open>inj \<sigma>\<close> \<open>strict_mono r\<close> injD n_not_Suc_n strict_mono_eq)
    ultimately
    show False
       using \<epsilon> \<open>range \<sigma> \<subseteq> T\<close> commute by fastforce
  qed
next
  assume R: ?rhs 
  show ?lhs
  proof (intro strip)
    fix \<sigma> :: "nat \<Rightarrow> 'a"
    assume "range \<sigma> \<subseteq> S"
    show "\<exists>l r. l \<in> U \<and> strict_mono r \<and> limitin mtopology (\<sigma> \<circ> r) l sequentially"
    proof (cases "finite (range \<sigma>)")
      case True
      then obtain m where "infinite (\<sigma> -` {\<sigma> m})"
        by (metis image_iff inf_img_fin_dom nat_not_finite)
      then obtain r where [iff]: "strict_mono r" and r: "\<And>n::nat. r n \<in> \<sigma> -` {\<sigma> m}"
        using infinite_enumerate by blast 
      have [iff]: "\<sigma> m \<in> U" "\<sigma> m \<in> M"
        using \<open>range \<sigma> \<subseteq> S\<close> assms by blast+
      show ?thesis
      proof (intro conjI exI)
        show "limitin mtopology (\<sigma> \<circ> r) (\<sigma> m) sequentially"
          using r by (simp add: limitin_metric)
      qed auto
    next
      case False
      then obtain l where "l \<in> U" and l: "l \<in> mtopology derived_set_of (range \<sigma>)"
        by (meson R \<open>range \<sigma> \<subseteq> S\<close> disjoint_iff)
      then obtain g where g: "\<And>\<epsilon>. \<epsilon>>0 \<Longrightarrow> \<sigma> (g \<epsilon>) \<noteq> l \<and> d l (\<sigma> (g \<epsilon>)) < \<epsilon>"
        by (simp add: metric_derived_set_of) metis
      have "range \<sigma> \<subseteq> M"
        using \<open>range \<sigma> \<subseteq> S\<close> assms by auto
      have "l \<in> M"
        using l metric_derived_set_of by auto
      define E where  \<comment>\<open>a construction to ensure monotonicity\<close>
        "E \<equiv> \<lambda>rec n. insert (inverse (Suc n)) ((\<lambda>i. d l (\<sigma> i)) ` (\<Union>k<n. {0..rec k})) - {0}"
      define r where "r \<equiv> wfrec less_than (\<lambda>rec n. g (Min (E rec n)))"
      have "(\<Union>k<n. {0..cut r less_than n k}) = (\<Union>k<n. {0..r k})" for n
        by (auto simp: cut_apply)
      then have r_eq: "r n = g (Min (E r n))" for n
        by (metis E_def def_wfrec [OF r_def] wf_less_than)
      have dl_pos[simp]: "d l (\<sigma> (r n)) > 0" for n
        using wf_less_than
      proof (induction n rule: wf_induct_rule)
        case (less n) 
        then have *: "Min (E r n) > 0"
          using \<open>l \<in> M\<close> \<open>range \<sigma> \<subseteq> M\<close> by (auto simp: E_def image_subset_iff)
        show ?case
          using g [OF *] r_eq [of n]
          by (metis \<open>l \<in> M\<close> \<open>range \<sigma> \<subseteq> M\<close> mdist_pos_less range_subsetD)
      qed
      then have non_l: "\<sigma> (r n) \<noteq> l" for n
        using \<open>range \<sigma> \<subseteq> M\<close> mdist_pos_eq by blast
      have Min_pos: "Min (E r n) > 0" for n
        using dl_pos \<open>l \<in> M\<close> \<open>range \<sigma> \<subseteq> M\<close> by (auto simp: E_def image_subset_iff)
      have d_small: "d (\<sigma>(r n)) l < inverse(Suc n)" for n
      proof -
        have "d (\<sigma>(r n)) l < Min (E r n)"
          by (simp add: \<open>0 < Min (E r n)\<close> commute g r_eq) 
        also have "... \<le> inverse(Suc n)"
          by (simp add: E_def)
        finally show ?thesis .
      qed
      have d_lt_d: "d l (\<sigma> (r n)) < d l (\<sigma> i)" if \<section>: "p < n" "i \<le> r p" "\<sigma> i \<noteq> l" for i p n
      proof -
        have 1: "d l (\<sigma> i) \<in> E r n"
          using \<section> \<open>l \<in> M\<close> \<open>range \<sigma> \<subseteq> M\<close> 
          by (force simp: E_def image_subset_iff image_iff)
        have "d l (\<sigma> (g (Min (E r n)))) < Min (E r n)"
          by (rule conjunct2 [OF g [OF Min_pos]])
        also have "Min (E r n) \<le> d l (\<sigma> i)"
          using 1 unfolding E_def by (force intro!: Min.coboundedI)
        finally show ?thesis
          by (simp add: r_eq) 
      qed
      have r: "r p < r n" if "p < n" for p n
        using d_lt_d [OF that] non_l by (meson linorder_not_le order_less_irrefl) 
      show ?thesis
      proof (intro exI conjI)
        show "strict_mono r"
          by (simp add: r strict_monoI)
        show "limitin mtopology (\<sigma> \<circ> r) l sequentially"
          unfolding limitin_metric
        proof (intro conjI strip \<open>l \<in> M\<close>)
          fix \<epsilon> :: real
          assume "\<epsilon> > 0"
          then have "\<forall>\<^sub>F n in sequentially. inverse(Suc n) < \<epsilon>"
            using Archimedean_eventually_inverse by auto
          then show "\<forall>\<^sub>F n in sequentially. (\<sigma> \<circ> r) n \<in> M \<and> d ((\<sigma> \<circ> r) n) l < \<epsilon>"
            by (smt (verit) \<open>range \<sigma> \<subseteq> M\<close> commute comp_apply d_small eventually_mono range_subsetD)
        qed
      qed (use \<open>l \<in> U\<close> in auto)
    qed
  qed
qed

subsubsection \<open>More on Bolzano Weierstrass\<close>

lemma Bolzano_Weierstrass_A: 
  assumes "compactin mtopology S" "T \<subseteq> S" "infinite T"
  shows "S \<inter> mtopology derived_set_of T \<noteq> {}"
  by (simp add: assms compactin_imp_Bolzano_Weierstrass)

lemma Bolzano_Weierstrass_B:
  fixes \<sigma> :: "nat \<Rightarrow> 'a"
  assumes "S \<subseteq> M" "range \<sigma> \<subseteq> S"
    and "\<And>T. \<lbrakk>T \<subseteq> S \<and> infinite T\<rbrakk> \<Longrightarrow> S \<inter> mtopology derived_set_of T \<noteq> {}"
  shows "\<exists>l r. l \<in> S \<and> strict_mono r \<and> limitin mtopology (\<sigma> \<circ> r) l sequentially"
  using Bolzano_Weierstrass_property assms by blast

lemma Bolzano_Weierstrass_C:
  assumes "S \<subseteq> M"
  assumes "\<And>\<sigma>:: nat \<Rightarrow> 'a. range \<sigma> \<subseteq> S \<Longrightarrow>
                (\<exists>l r. l \<in> S \<and> strict_mono r \<and> limitin mtopology (\<sigma> \<circ> r) l sequentially)"
  shows "mtotally_bounded S"
  unfolding mtotally_bounded_sequentially
  by (metis convergent_imp_MCauchy assms image_comp image_mono subset_UNIV subset_trans)

lemma Bolzano_Weierstrass_D:
  assumes "S \<subseteq> M" "S \<subseteq> \<Union>\<C>" and opeU: "\<And>U. U \<in> \<C> \<Longrightarrow> openin mtopology U"
  assumes \<section>: "(\<forall>\<sigma>::nat\<Rightarrow>'a. range \<sigma> \<subseteq> S
         \<longrightarrow> (\<exists>l r. l \<in> S \<and> strict_mono r \<and> limitin mtopology (\<sigma> \<circ> r) l sequentially))"
  shows "\<exists>\<epsilon>>0. \<forall>x \<in> S. \<exists>U \<in> \<C>. mball x \<epsilon> \<subseteq> U"
proof (rule ccontr)
  assume "\<not> (\<exists>\<epsilon>>0. \<forall>x \<in> S. \<exists>U \<in> \<C>. mball x \<epsilon> \<subseteq> U)"
  then have "\<forall>n. \<exists>x\<in>S. \<forall>U\<in>\<C>. \<not> mball x (inverse (Suc n)) \<subseteq> U"
    by simp
  then obtain \<sigma> where "\<And>n. \<sigma> n \<in> S" 
       and \<sigma>: "\<And>n U. U \<in> \<C> \<Longrightarrow> \<not> mball (\<sigma> n) (inverse (Suc n)) \<subseteq> U"
    by metis
  then obtain l r where "l \<in> S" "strict_mono r" 
         and lr: "limitin mtopology (\<sigma> \<circ> r) l sequentially"
    by (meson \<section> image_subsetI)
  with \<open>S \<subseteq> \<Union>\<C>\<close> obtain B where "l \<in> B" "B \<in> \<C>"
    by auto
  then obtain \<epsilon> where "\<epsilon> > 0" and \<epsilon>: "\<And>z. \<lbrakk>z \<in> M; d z l < \<epsilon>\<rbrakk> \<Longrightarrow> z \<in> B"
    by (metis opeU [OF \<open>B \<in> \<C>\<close>] commute in_mball openin_mtopology subset_iff)
  then have "\<forall>\<^sub>F n in sequentially. \<sigma> (r n) \<in> M \<and> d (\<sigma> (r n)) l < \<epsilon>/2"
    using lr half_gt_zero unfolding limitin_metric o_def by blast
  moreover have "\<forall>\<^sub>F n in sequentially. inverse (real (Suc n)) < \<epsilon>/2"
    using Archimedean_eventually_inverse \<open>0 < \<epsilon>\<close> half_gt_zero by blast
  ultimately obtain n where n: "d (\<sigma> (r n)) l < \<epsilon>/2" "inverse (real (Suc n)) < \<epsilon>/2"
    by (smt (verit, del_insts) eventually_sequentially le_add1 le_add2)
  have "x \<in> B" if "d (\<sigma> (r n)) x < inverse (Suc(r n))" "x \<in> M" for x
  proof -
    have rle: "inverse (real (Suc (r n))) \<le> inverse (real (Suc n))"
      using \<open>strict_mono r\<close> strict_mono_imp_increasing by auto
    have "d x l \<le> d (\<sigma> (r n)) x + d (\<sigma> (r n)) l"
      using that by (metis triangle \<open>\<And>n. \<sigma> n \<in> S\<close> \<open>l \<in> S\<close> \<open>S \<subseteq> M\<close> commute subsetD)
    also have "... < \<epsilon>"
      using that n rle by linarith
    finally show ?thesis
      by (simp add: \<epsilon> that)
  qed
  then show False
    using \<sigma> [of B "r n"] by (simp add: \<open>B \<in> \<C>\<close> subset_iff)
qed


lemma Bolzano_Weierstrass_E:
  assumes "mtotally_bounded S" "S \<subseteq> M"
  and S: "\<And>\<C>. \<lbrakk>\<And>U. U \<in> \<C> \<Longrightarrow> openin mtopology U; S \<subseteq> \<Union>\<C>\<rbrakk> \<Longrightarrow> \<exists>\<epsilon>>0. \<forall>x \<in> S. \<exists>U \<in> \<C>. mball x \<epsilon> \<subseteq> U"
  shows "compactin mtopology S"
proof (clarsimp simp: compactin_def assms)
  fix \<U> :: "'a set set"
  assume \<U>: "\<forall>x\<in>\<U>. openin mtopology x" and "S \<subseteq> \<Union>\<U>"
  then obtain \<epsilon> where "\<epsilon>>0" and \<epsilon>: "\<And>x. x \<in> S \<Longrightarrow> \<exists>U \<in> \<U>. mball x \<epsilon> \<subseteq> U"
    by (metis S)
  then obtain f where f: "\<And>x. x \<in> S \<Longrightarrow> f x \<in> \<U> \<and> mball x \<epsilon> \<subseteq> f x"
    by metis
  then obtain K where "finite K" "K \<subseteq> S" and K: "S \<subseteq> (\<Union>x\<in>K. mball x \<epsilon>)"
    by (metis \<open>0 < \<epsilon>\<close> \<open>mtotally_bounded S\<close> mtotally_bounded_def)
  show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> S \<subseteq> \<Union>\<F>"
  proof (intro conjI exI)
    show "finite (f ` K)"
      by (simp add: \<open>finite K\<close>)
    show "f ` K \<subseteq> \<U>"
      using \<open>K \<subseteq> S\<close> f by blast
    show "S \<subseteq> \<Union>(f ` K)"
      using K \<open>K \<subseteq> S\<close> by (force dest: f)
  qed
qed


lemma compactin_eq_Bolzano_Weierstrass:
  "compactin mtopology S \<longleftrightarrow>
   S \<subseteq> M \<and> (\<forall>T. T \<subseteq> S \<and> infinite T \<longrightarrow> S \<inter> mtopology derived_set_of T \<noteq> {})"
  using Bolzano_Weierstrass_C Bolzano_Weierstrass_D Bolzano_Weierstrass_E
  by (smt (verit, del_insts) Bolzano_Weierstrass_property compactin_imp_Bolzano_Weierstrass compactin_subspace subset_refl topspace_mtopology)

lemma compactin_sequentially:
  shows "compactin mtopology S \<longleftrightarrow>
        S \<subseteq> M \<and>
        ((\<forall>\<sigma>::nat\<Rightarrow>'a. range \<sigma> \<subseteq> S
         \<longrightarrow> (\<exists>l r. l \<in> S \<and> strict_mono r \<and> limitin mtopology (\<sigma> \<circ> r) l sequentially)))"
  by (metis Bolzano_Weierstrass_property compactin_eq_Bolzano_Weierstrass subset_refl)

lemma compactin_imp_mtotally_bounded: 
  "compactin mtopology S \<Longrightarrow> mtotally_bounded S"
  by (simp add: Bolzano_Weierstrass_C compactin_sequentially)

lemma lebesgue_number:
    "\<lbrakk>compactin mtopology S; S \<subseteq> \<Union>\<C>; \<And>U. U \<in> \<C> \<Longrightarrow> openin mtopology U\<rbrakk>
    \<Longrightarrow> \<exists>\<epsilon>>0. \<forall>x \<in> S. \<exists>U \<in> \<C>. mball x \<epsilon> \<subseteq> U"
  by (simp add: Bolzano_Weierstrass_D compactin_sequentially)

lemma compact_space_sequentially:
   "compact_space mtopology \<longleftrightarrow>
    (\<forall>\<sigma>::nat\<Rightarrow>'a. range \<sigma> \<subseteq> M
         \<longrightarrow> (\<exists>l r. l \<in> M \<and> strict_mono r \<and> limitin mtopology (\<sigma> \<circ> r) l sequentially))"
  by (simp add: compact_space_def compactin_sequentially)

lemma compact_space_eq_Bolzano_Weierstrass:
   "compact_space mtopology \<longleftrightarrow>
    (\<forall>S. S \<subseteq> M \<and> infinite S \<longrightarrow> mtopology derived_set_of S \<noteq> {})"
  using Int_absorb1 [OF derived_set_of_subset_topspace [of mtopology]]
  by (force simp: compact_space_def compactin_eq_Bolzano_Weierstrass)

lemma compact_space_nest:
   "compact_space mtopology \<longleftrightarrow>
    (\<forall>C. (\<forall>n::nat. closedin mtopology (C n)) \<and> (\<forall>n. C n \<noteq> {}) \<and> decseq C \<longrightarrow> \<Inter>(range C) \<noteq> {})"
   (is "?lhs=?rhs")
proof
  assume L: ?lhs
  show ?rhs
  proof clarify
    fix C :: "nat \<Rightarrow> 'a set"
    assume "\<forall>n. closedin mtopology (C n)"
      and "\<forall>n. C n \<noteq> {}"
      and "decseq C"
      and "\<Inter> (range C) = {}"
    then obtain K where K: "finite K" "\<Inter>(C ` K) = {}"
      by (metis L compact_space_imp_nest)
    then obtain k where "K \<subseteq> {..k}"
      using finite_nat_iff_bounded_le by auto
    then have "C k \<subseteq> \<Inter>(C ` K)"
      using \<open>decseq C\<close> by (auto simp:decseq_def)
    then show False
      by (simp add: K \<open>\<forall>n. C n \<noteq> {}\<close>)
  qed
next
  assume R [rule_format]: ?rhs
  show ?lhs
    unfolding compact_space_sequentially
  proof (intro strip)
    fix \<sigma> :: "nat \<Rightarrow> 'a"
    assume \<sigma>: "range \<sigma> \<subseteq> M"
    have "mtopology closure_of \<sigma> ` {n..} \<noteq> {}" for n
      using \<open>range \<sigma> \<subseteq> M\<close> by (auto simp: closure_of_eq_empty image_subset_iff)
    moreover have "decseq (\<lambda>n. mtopology closure_of \<sigma> ` {n..})"
      using closure_of_mono image_mono by (smt (verit) atLeast_subset_iff decseq_def) 
    ultimately obtain l where l: "\<And>n. l \<in> mtopology closure_of \<sigma> ` {n..}"
      using R [of "\<lambda>n. mtopology closure_of (\<sigma> ` {n..})"] by auto
    then have "l \<in> M" and "\<And>n. \<forall>r>0. \<exists>k\<ge>n. \<sigma> k \<in> M \<and> d l (\<sigma> k) < r"
      using metric_closure_of by fastforce+
    then obtain f where f: "\<And>n r. r>0 \<Longrightarrow> f n r \<ge> n \<and> \<sigma> (f n r) \<in> M \<and> d l (\<sigma> (f n r)) < r"
      by metis
    define r where "r = rec_nat (f 0 1) (\<lambda>n rec. (f (Suc rec) (inverse (Suc (Suc n)))))"
    have r: "d l (\<sigma>(r n)) < inverse(Suc n)" for n
      by (induction n) (auto simp: rec_nat_0_imp [OF r_def] rec_nat_Suc_imp [OF r_def] f)
    have "r n < r(Suc n)" for n
      by (simp add: Suc_le_lessD f r_def)
    then have "strict_mono r"
      by (simp add: strict_mono_Suc_iff)
    moreover have "limitin mtopology (\<sigma> \<circ> r) l sequentially"
      proof (clarsimp simp: limitin_metric \<open>l \<in> M\<close>)
        fix \<epsilon> :: real
        assume "\<epsilon> > 0"
        then have "(\<forall>\<^sub>F n in sequentially. inverse (real (Suc n)) < \<epsilon>)"
          using Archimedean_eventually_inverse by blast
        then show "\<forall>\<^sub>F n in sequentially. \<sigma> (r n) \<in> M \<and> d (\<sigma> (r n)) l < \<epsilon>"
          by eventually_elim (metis commute \<open>range \<sigma> \<subseteq> M\<close>  order_less_trans r range_subsetD)
      qed
    ultimately show "\<exists>l r. l \<in> M \<and> strict_mono r \<and> limitin mtopology (\<sigma> \<circ> r) l sequentially"
      using \<open>l \<in> M\<close> by blast
  qed
qed


lemma (in discrete_metric) mcomplete_discrete_metric: "disc.mcomplete"
proof (clarsimp simp: disc.mcomplete_def)
  fix \<sigma> :: "nat \<Rightarrow> 'a"
  assume "disc.MCauchy \<sigma>"
  then obtain N where "\<And>n. N \<le> n \<Longrightarrow> \<sigma> N = \<sigma> n"
    unfolding disc.MCauchy_def by (metis dd_def dual_order.refl order_less_irrefl zero_less_one)
  moreover have "range \<sigma> \<subseteq> M"
    using \<open>disc.MCauchy \<sigma>\<close> disc.MCauchy_def by blast
  ultimately have "limitin disc.mtopology \<sigma> (\<sigma> N) sequentially"
    by (metis disc.limit_metric_sequentially disc.zero range_subsetD)
  then show "\<exists>x. limitin disc.mtopology \<sigma> x sequentially" ..
qed

lemma compact_space_imp_mcomplete: "compact_space mtopology \<Longrightarrow> mcomplete"
  by (simp add: compact_space_nest mcomplete_nest)

lemma (in Submetric) compactin_imp_mcomplete:
   "compactin mtopology A \<Longrightarrow> sub.mcomplete"
  by (simp add: compactin_subspace mtopology_submetric sub.compact_space_imp_mcomplete)

lemma (in Submetric) mcomplete_imp_closedin:
  assumes "sub.mcomplete"
  shows "closedin mtopology A"
proof -
  have "l \<in> A"
    if "range \<sigma> \<subseteq> A" and l: "limitin mtopology \<sigma> l sequentially"
    for \<sigma> :: "nat \<Rightarrow> 'a" and l
  proof -
    have "sub.MCauchy \<sigma>"
      using convergent_imp_MCauchy subset that by (force simp: MCauchy_submetric)
    then have "limitin sub.mtopology \<sigma> l sequentially"
      using assms unfolding sub.mcomplete_def
      using l limitin_metric_unique limitin_submetric_iff trivial_limit_sequentially by blast
    then show ?thesis
      using limitin_submetric_iff by blast
  qed
  then show ?thesis
    using metric_closedin_iff_sequentially_closed subset by auto
qed

lemma (in Submetric) closedin_eq_mcomplete:
   "mcomplete \<Longrightarrow> (closedin mtopology A \<longleftrightarrow> sub.mcomplete)"
  using closedin_mcomplete_imp_mcomplete mcomplete_imp_closedin by blast

lemma compact_space_eq_mcomplete_mtotally_bounded:
   "compact_space mtopology \<longleftrightarrow> mcomplete \<and> mtotally_bounded M"
  by (meson Bolzano_Weierstrass_C compact_space_imp_mcomplete compact_space_sequentially limitin_mspace 
            mcomplete_alt mtotally_bounded_sequentially subset_refl)


lemma compact_closure_of_imp_mtotally_bounded:
   "\<lbrakk>compactin mtopology (mtopology closure_of S); S \<subseteq> M\<rbrakk>
      \<Longrightarrow> mtotally_bounded S"
  using compactin_imp_mtotally_bounded mtotally_bounded_closure_of_eq by blast

lemma mtotally_bounded_eq_compact_closure_of:
  assumes "mcomplete"
  shows "mtotally_bounded S \<longleftrightarrow> S \<subseteq> M \<and> compactin mtopology (mtopology closure_of S)"
  (is "?lhs=?rhs")
proof
  assume L: ?lhs 
  show ?rhs
    unfolding compactin_subspace
  proof (intro conjI)
    show "S \<subseteq> M"
      using L by (simp add: mtotally_bounded_imp_subset)
    show "mtopology closure_of S \<subseteq> topspace mtopology"
      by (simp add: \<open>S \<subseteq> M\<close> closure_of_minimal)
    then have MSM: "mtopology closure_of S \<subseteq> M"
      by auto
    interpret S: Submetric M d "mtopology closure_of S"
    proof qed (use MSM in auto)
    have "S.sub.mtotally_bounded (mtopology closure_of S)"
      using L mtotally_bounded_absolute mtotally_bounded_closure_of by blast
    then
    show "compact_space (subtopology mtopology (mtopology closure_of S))"
      using S.closedin_mcomplete_imp_mcomplete S.mtopology_submetric S.sub.compact_space_eq_mcomplete_mtotally_bounded assms by force
  qed
qed (auto simp: compact_closure_of_imp_mtotally_bounded)



lemma compact_closure_of_eq_Bolzano_Weierstrass:
   "compactin mtopology (mtopology closure_of S) \<longleftrightarrow>
    (\<forall>T. infinite T \<and> T \<subseteq> S \<and> T \<subseteq> M \<longrightarrow> mtopology derived_set_of T \<noteq> {})"  (is "?lhs=?rhs")
proof
  assume L: ?lhs 
  show ?rhs
  proof (intro strip)
    fix T
    assume T: "infinite T \<and> T \<subseteq> S \<and> T \<subseteq> M"
    show "mtopology derived_set_of T \<noteq> {}"
    proof (intro compact_closure_of_imp_Bolzano_Weierstrass)
      show "compactin mtopology (mtopology closure_of S)"
        by (simp add: L)
    qed (use T in auto)
  qed
next
  have "compactin mtopology (mtopology closure_of S)"
    if \<section>: "\<And>T. \<lbrakk>infinite T; T \<subseteq> S\<rbrakk> \<Longrightarrow> mtopology derived_set_of T \<noteq> {}" and "S \<subseteq> M" for S
    unfolding compactin_sequentially
  proof (intro conjI strip)
    show MSM: "mtopology closure_of S \<subseteq> M"
      using closure_of_subset_topspace by fastforce
    fix \<sigma> :: "nat \<Rightarrow> 'a"
    assume \<sigma>: "range \<sigma> \<subseteq> mtopology closure_of S"
    then have "\<exists>y \<in> S. d (\<sigma> n) y < inverse(Suc n)" for n
      by (simp add: metric_closure_of image_subset_iff) (metis inverse_Suc of_nat_Suc)
    then obtain \<tau> where \<tau>: "\<And>n. \<tau> n \<in> S \<and> d (\<sigma> n) (\<tau> n) < inverse(Suc n)"
      by metis
    then have "range \<tau> \<subseteq> S"
      by blast
    moreover
    have *: "\<forall>T. T \<subseteq> S \<and> infinite T \<longrightarrow> mtopology closure_of S \<inter> mtopology derived_set_of T \<noteq> {}"
      using "\<section>"(1) derived_set_of_mono derived_set_of_subset_closure_of by fastforce
    moreover have "S \<subseteq> mtopology closure_of S"
      by (simp add: \<open>S \<subseteq> M\<close> closure_of_subset)
    ultimately obtain l r where lr:
      "l \<in> mtopology closure_of S" "strict_mono r" "limitin mtopology (\<tau> \<circ> r) l sequentially"
      using Bolzano_Weierstrass_property \<open>S \<subseteq> M\<close> by metis
    then have "l \<in> M"
      using limitin_mspace by blast
    have dr_less: "d ((\<sigma> \<circ> r) n) ((\<tau> \<circ> r) n) < inverse(Suc n)" for n
    proof -
      have "d ((\<sigma> \<circ> r) n) ((\<tau> \<circ> r) n) < inverse(Suc (r n))"
        using \<tau> by auto
      also have "... \<le> inverse(Suc n)"
        using lr strict_mono_imp_increasing by auto
      finally show ?thesis .
    qed
    have "limitin mtopology (\<sigma> \<circ> r) l sequentially"
      unfolding limitin_metric
    proof (intro conjI strip)
      show "l \<in> M"
        using limitin_mspace lr by blast
      fix \<epsilon> :: real
      assume "\<epsilon> > 0"
      then have "\<forall>\<^sub>F n in sequentially. (\<tau> \<circ> r) n \<in> M \<and> d ((\<tau> \<circ> r) n) l < \<epsilon>/2"
        using lr half_gt_zero limitin_metric by blast 
      moreover have "\<forall>\<^sub>F n in sequentially. inverse (real (Suc n)) < \<epsilon>/2"
        using Archimedean_eventually_inverse \<open>0 < \<epsilon>\<close> half_gt_zero by blast
      then have "\<forall>\<^sub>F n in sequentially. d ((\<sigma> \<circ> r) n) ((\<tau> \<circ> r) n) < \<epsilon>/2"
        by eventually_elim (smt (verit, del_insts) dr_less)
      ultimately have "\<forall>\<^sub>F n in sequentially. d ((\<sigma> \<circ> r) n) l < \<epsilon>/2 + \<epsilon>/2"
        by eventually_elim (smt (verit) triangle \<open>l \<in> M\<close> MSM \<sigma> comp_apply order_trans range_subsetD)      
      then show "\<forall>\<^sub>F n in sequentially. (\<sigma> \<circ> r) n \<in> M \<and> d ((\<sigma> \<circ> r) n) l < \<epsilon>"
        apply eventually_elim
        using \<open>mtopology closure_of S \<subseteq> M\<close> \<sigma> by auto
    qed
    with lr show "\<exists>l r. l \<in> mtopology closure_of S \<and> strict_mono r \<and> limitin mtopology (\<sigma> \<circ> r) l sequentially"
      by blast
  qed
  then show "?rhs \<Longrightarrow> ?lhs"
    by (metis Int_subset_iff closure_of_restrict inf_le1 topspace_mtopology)
qed

end

lemma (in discrete_metric) mtotally_bounded_discrete_metric:
   "disc.mtotally_bounded S \<longleftrightarrow> finite S \<and> S \<subseteq> M" (is "?lhs=?rhs")
proof
  assume L: ?lhs 
  show ?rhs
  proof
    show "finite S"
      by (metis (no_types) L closure_of_subset_Int compactin_discrete_topology disc.mtotally_bounded_eq_compact_closure_of
          disc.topspace_mtopology discrete_metric.mcomplete_discrete_metric inf.absorb_iff2 mtopology_discrete_metric finite_subset)
    show "S \<subseteq> M"
      by (simp add: L disc.mtotally_bounded_imp_subset)
  qed
qed (simp add: disc.finite_imp_mtotally_bounded)


context Metric_space
begin

lemma derived_set_of_infinite_openin_metric:
   "mtopology derived_set_of S =
    {x \<in> M. \<forall>U. x \<in> U \<and> openin mtopology U \<longrightarrow> infinite(S \<inter> U)}"
  by (simp add: derived_set_of_infinite_openin Hausdorff_space_mtopology)

lemma derived_set_of_infinite_1: 
  assumes "infinite (S \<inter> mball x \<epsilon>)" 
  shows "infinite (S \<inter> mcball x \<epsilon>)"
  by (meson Int_mono assms finite_subset mball_subset_mcball subset_refl)

lemma derived_set_of_infinite_2:
  assumes "openin mtopology U" "\<And>\<epsilon>. 0 < \<epsilon> \<Longrightarrow> infinite (S \<inter> mcball x \<epsilon>)" and "x \<in> U"
  shows "infinite (S \<inter> U)"
  by (metis assms openin_mtopology_mcball finite_Int inf.absorb_iff2 inf_assoc)

lemma derived_set_of_infinite_mball:
  "mtopology derived_set_of S = {x \<in> M. \<forall>e>0. infinite(S \<inter> mball x e)}"
  unfolding derived_set_of_infinite_openin_metric
  by (metis (no_types, opaque_lifting) centre_in_mball_iff openin_mball derived_set_of_infinite_1 derived_set_of_infinite_2)

lemma derived_set_of_infinite_mcball:
  "mtopology derived_set_of S = {x \<in> M. \<forall>e>0. infinite(S \<inter> mcball x e)}"
  unfolding derived_set_of_infinite_openin_metric
  by (metis (no_types, opaque_lifting) centre_in_mball_iff openin_mball derived_set_of_infinite_1 derived_set_of_infinite_2)

end

subsection\<open>Continuous functions on metric spaces\<close>

context Metric_space
begin

lemma continuous_map_to_metric:
   "continuous_map X mtopology f \<longleftrightarrow>
    (\<forall>x \<in> topspace X. \<forall>\<epsilon>>0. \<exists>U. openin X U \<and> x \<in> U \<and> (\<forall>y\<in>U. f y \<in> mball (f x) \<epsilon>))"
   (is "?lhs=?rhs")
proof
  show "?lhs \<Longrightarrow> ?rhs"
    unfolding continuous_map_eq_topcontinuous_at topcontinuous_at_def
    by (metis PiE centre_in_mball_iff openin_mball topspace_mtopology)
next
  assume R: ?rhs
  then have "\<forall>x\<in>topspace X. f x \<in> M"
    by (meson gt_ex in_mball)
  moreover 
  have "\<And>x V. \<lbrakk>x \<in> topspace X; openin mtopology V; f x \<in> V\<rbrakk> \<Longrightarrow> \<exists>U. openin X U \<and> x \<in> U \<and> (\<forall>y\<in>U. f y \<in> V)"
    unfolding openin_mtopology by (metis Int_iff R inf.orderE)
  ultimately
  show ?lhs
    by (simp add: continuous_map_eq_topcontinuous_at topcontinuous_at_def)
qed 

lemma continuous_map_from_metric:
   "continuous_map mtopology X f \<longleftrightarrow>
    f \<in> M \<rightarrow> topspace X \<and>
    (\<forall>a \<in> M. \<forall>U. openin X U \<and> f a \<in> U \<longrightarrow> (\<exists>r>0. \<forall>x. x \<in> M \<and> d a x < r \<longrightarrow> f x \<in> U))"
proof (cases "f ` M \<subseteq> topspace X")
  case True
  then show ?thesis
    by (fastforce simp: continuous_map openin_mtopology subset_eq)
next
  case False
  then show ?thesis
    by (simp add: continuous_map_def image_subset_iff_funcset)
qed

text \<open>An abstract formulation, since the limits do not have to be sequential\<close>
lemma continuous_map_uniform_limit:
  assumes contf: "\<forall>\<^sub>F \<xi> in F. continuous_map X mtopology (f \<xi>)"
    and dfg: "\<And>\<epsilon>. 0 < \<epsilon> \<Longrightarrow> \<forall>\<^sub>F \<xi> in F. \<forall>x \<in> topspace X. g x \<in> M \<and> d (f \<xi> x) (g x) < \<epsilon>"
    and nontriv: "\<not> trivial_limit F"
  shows "continuous_map X mtopology g"
  unfolding continuous_map_to_metric
proof (intro strip)
  fix x and \<epsilon>::real
  assume "x \<in> topspace X" and "\<epsilon> > 0"
  then obtain \<xi> where k: "continuous_map X mtopology (f \<xi>)" 
    and gM: "\<forall>x \<in> topspace X. g x \<in> M" 
    and third: "\<forall>x \<in> topspace X. d (f \<xi> x) (g x) < \<epsilon>/3"
    using eventually_conj [OF contf] contf dfg [of "\<epsilon>/3"] eventually_happens' [OF nontriv]
    by (smt (verit, ccfv_SIG) zero_less_divide_iff)
  then obtain U where U: "openin X U" "x \<in> U" and Uthird: "\<forall>y\<in>U. d (f \<xi> y) (f \<xi> x) < \<epsilon>/3"
    unfolding continuous_map_to_metric
    by (metis \<open>0 < \<epsilon>\<close> \<open>x \<in> topspace X\<close> commute divide_pos_pos in_mball zero_less_numeral)
  have f_inM: "f \<xi> y \<in> M" if "y\<in>U" for y
    using U k openin_subset that by (fastforce simp: continuous_map_def)
  have "d (g y) (g x) < \<epsilon>" if "y\<in>U" for y
  proof -
    have "g y \<in> M"
      using U gM openin_subset that by blast
    have "d (g y) (g x) \<le> d (g y) (f \<xi> x) + d (f \<xi> x) (g x)"
      by (simp add: U \<open>g y \<in> M\<close> \<open>x \<in> topspace X\<close> f_inM gM triangle)
    also have "\<dots> \<le> d (g y) (f \<xi> y) + d (f \<xi> y) (f \<xi> x) + d (f \<xi> x) (g x)"
      by (simp add: U \<open>g y \<in> M\<close> commute f_inM that triangle')
    also have "\<dots> < \<epsilon>/3 + \<epsilon>/3 + \<epsilon>/3"
      by (smt (verit) U(1) Uthird \<open>x \<in> topspace X\<close> commute openin_subset subsetD that third)
    finally show ?thesis by simp
  qed
  with U gM show "\<exists>U. openin X U \<and> x \<in> U \<and> (\<forall>y\<in>U. g y \<in> mball (g x) \<epsilon>)"
    by (metis commute in_mball in_mono openin_subset)
qed


lemma continuous_map_uniform_limit_alt:
  assumes contf: "\<forall>\<^sub>F \<xi> in F. continuous_map X mtopology (f \<xi>)"
    and gim: "g \<in> topspace X \<rightarrow> M"
    and dfg: "\<And>\<epsilon>. 0 < \<epsilon> \<Longrightarrow> \<forall>\<^sub>F \<xi> in F. \<forall>x \<in> topspace X. d (f \<xi> x) (g x) < \<epsilon>"
    and nontriv: "\<not> trivial_limit F"
  shows "continuous_map X mtopology g"
proof (rule continuous_map_uniform_limit [OF contf])
  fix \<epsilon> :: real
  assume "\<epsilon> > 0"
  with gim dfg show "\<forall>\<^sub>F \<xi> in F. \<forall>x\<in>topspace X. g x \<in> M \<and> d (f \<xi> x) (g x) < \<epsilon>"
    by (simp add: Pi_iff)
qed (use nontriv in auto)


lemma continuous_map_uniformly_Cauchy_limit:
  assumes "mcomplete"
  assumes contf: "\<forall>\<^sub>F n in sequentially. continuous_map X mtopology (f n)"
    and Cauchy': "\<And>\<epsilon>. \<epsilon> > 0 \<Longrightarrow> \<exists>N. \<forall>m n x. N \<le> m \<longrightarrow> N \<le> n \<longrightarrow> x \<in> topspace X \<longrightarrow> d (f m x) (f n x) < \<epsilon>"
  obtains g where
    "continuous_map X mtopology g"
    "\<And>\<epsilon>. 0 < \<epsilon> \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>topspace X. d (f n x) (g x) < \<epsilon>"
proof -
  have "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>l. limitin mtopology (\<lambda>n. f n x) l sequentially"
    using \<open>mcomplete\<close> [unfolded mcomplete, rule_format] assms
    unfolding continuous_map_def Pi_iff topspace_mtopology
    by (smt (verit, del_insts) eventually_mono)
  then obtain g where g: "\<And>x. x \<in> topspace X \<Longrightarrow> limitin mtopology (\<lambda>n. f n x) (g x) sequentially"
    by metis
  show thesis
  proof
    show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>topspace X. d (f n x) (g x) < \<epsilon>"
      if "\<epsilon> > 0" for \<epsilon> :: real
    proof -
      obtain N where N: "\<And>m n x. \<lbrakk>N \<le> m; N \<le> n; x \<in> topspace X\<rbrakk> \<Longrightarrow> d (f m x) (f n x) < \<epsilon>/2"
        by (meson Cauchy' \<open>0 < \<epsilon>\<close> half_gt_zero)
      obtain P where P: "\<And>n x. \<lbrakk>n \<ge> P; x \<in> topspace X\<rbrakk> \<Longrightarrow> f n x \<in> M"
        using contf by (auto simp: eventually_sequentially continuous_map_def)
      show ?thesis
      proof (intro eventually_sequentiallyI strip)
        fix n x
        assume "max N P \<le> n" and x: "x \<in> topspace X"
        obtain L where "g x \<in> M" and L: "\<forall>n\<ge>L. f n x \<in> M \<and> d (f n x) (g x) < \<epsilon>/2"
          using g [OF x] \<open>\<epsilon> > 0\<close> unfolding limitin_metric
          by (metis (no_types, lifting) eventually_sequentially half_gt_zero)
        define n' where "n' \<equiv> Max{L,N,P}"
        have L': "\<forall>m \<ge> n'. f m x \<in> M \<and> d (f m x) (g x) < \<epsilon>/2"
          using L by (simp add: n'_def)
        moreover
        have "d (f n x) (f n' x) < \<epsilon>/2"
          using N [of n n' x] \<open>max N P \<le> n\<close> n'_def x by fastforce
        ultimately have "d (f n x) (g x) < \<epsilon>/2 + \<epsilon>/2"
          by (smt (verit, ccfv_SIG) P \<open>g x \<in> M\<close> \<open>max N P \<le> n\<close> le_refl max.bounded_iff mdist_zero triangle' x)
        then show "d (f n x) (g x) < \<epsilon>" by simp
      qed
    qed
    then show "continuous_map X mtopology g"
      by (smt (verit, del_insts) eventually_mono g limitin_mspace trivial_limit_sequentially continuous_map_uniform_limit [OF contf])
  qed
qed

lemma metric_continuous_map:
  assumes "Metric_space M' d'"
  shows
   "continuous_map mtopology (Metric_space.mtopology M' d') f \<longleftrightarrow>
    f ` M \<subseteq> M' \<and> (\<forall>a \<in> M. \<forall>\<epsilon>>0. \<exists>\<delta>>0.  (\<forall>x. x \<in> M \<and> d a x < \<delta> \<longrightarrow> d' (f a) (f x) < \<epsilon>))"
   (is "?lhs = ?rhs")
proof -
  interpret M': Metric_space M' d'
    by (simp add: assms)
  show ?thesis
  proof
    assume L: ?lhs
    show ?rhs
    proof (intro conjI strip)
      show "f ` M \<subseteq> M'"
        using L by (auto simp: continuous_map_def)
      fix a and \<epsilon> :: real
      assume "a \<in> M" and "\<epsilon> > 0"
      then have "openin mtopology {x \<in> M. f x \<in> M'.mball (f a) \<epsilon>}" "f a \<in> M'"
        using L unfolding continuous_map_def by fastforce+
      then obtain \<delta> where "\<delta> > 0" "mball a \<delta> \<subseteq> {x \<in> M. f x \<in> M' \<and> d' (f a) (f x) < \<epsilon>}"
        using \<open>0 < \<epsilon>\<close> \<open>a \<in> M\<close> openin_mtopology by auto
      then show "\<exists>\<delta>>0. \<forall>x. x \<in> M \<and> d a x < \<delta> \<longrightarrow> d' (f a) (f x) < \<epsilon>"
        using \<open>a \<in> M\<close> in_mball by blast
    qed
  next
    assume R: ?rhs    
    show ?lhs
      unfolding continuous_map_def
    proof (intro conjI strip)
      fix U
      assume "openin M'.mtopology U"
      then show "openin mtopology {x \<in> topspace mtopology. f x \<in> U}"
        using R
        by (force simp: continuous_map_def openin_mtopology M'.openin_mtopology subset_iff)
    qed (use R in auto)
  qed
qed

end (*Metric_space*)


subsection \<open>Completely metrizable spaces\<close>

text \<open>These spaces are topologically complete\<close>

definition completely_metrizable_space where
 "completely_metrizable_space X \<equiv> 
     \<exists>M d. Metric_space M d \<and> Metric_space.mcomplete M d \<and> X = Metric_space.mtopology M d"

lemma empty_completely_metrizable_space: 
  "completely_metrizable_space trivial_topology"
  unfolding completely_metrizable_space_def subtopology_eq_discrete_topology_empty [symmetric]
  by (metis Metric_space.mcomplete_empty_mspace discrete_metric.mtopology_discrete_metric metric_M_dd)

lemma completely_metrizable_imp_metrizable_space:
   "completely_metrizable_space X \<Longrightarrow> metrizable_space X"
  using completely_metrizable_space_def metrizable_space_def by auto

lemma (in Metric_space) completely_metrizable_space_mtopology:
   "mcomplete \<Longrightarrow> completely_metrizable_space mtopology"
  using Metric_space_axioms completely_metrizable_space_def by blast

lemma completely_metrizable_space_discrete_topology:
   "completely_metrizable_space (discrete_topology U)"
  unfolding completely_metrizable_space_def
  by (metis discrete_metric.mcomplete_discrete_metric discrete_metric.mtopology_discrete_metric metric_M_dd)

lemma completely_metrizable_space_euclidean:
    "completely_metrizable_space (euclidean:: 'a::complete_space topology)"
  using Met_TC.completely_metrizable_space_mtopology complete_UNIV by auto

lemma completely_metrizable_space_closedin:
  assumes X: "completely_metrizable_space X" and S: "closedin X S"
  shows "completely_metrizable_space(subtopology X S)"
proof -
  obtain M d where "Metric_space M d" and comp: "Metric_space.mcomplete M d" 
                and Xeq: "X = Metric_space.mtopology M d"
    using assms completely_metrizable_space_def by blast
  then interpret Metric_space M d
    by blast
  show ?thesis
    unfolding completely_metrizable_space_def
  proof (intro conjI exI)
    show "Metric_space S d"
      using S Xeq closedin_subset subspace by force
    have sub: "Submetric_axioms M S"
      by (metis S Xeq closedin_metric Submetric_axioms_def)
    then show "Metric_space.mcomplete S d"
      using S Submetric.closedin_mcomplete_imp_mcomplete Submetric_def Xeq comp by blast
    show "subtopology X S = Metric_space.mtopology S d"
      by (metis Metric_space_axioms Xeq sub Submetric.intro Submetric.mtopology_submetric)
  qed
qed

lemma completely_metrizable_space_cbox: "completely_metrizable_space (top_of_set (cbox a b))"
    using closed_closedin completely_metrizable_space_closedin completely_metrizable_space_euclidean by blast


lemma homeomorphic_completely_metrizable_space_aux:
  assumes homXY: "X homeomorphic_space Y" and X: "completely_metrizable_space X"
  shows "completely_metrizable_space Y"
proof -
  obtain f g where hmf: "homeomorphic_map X Y f" and hmg: "homeomorphic_map Y X g"
    and fg: "\<And>x. x \<in> topspace X \<Longrightarrow> g(f x) = x" "\<And>y. y \<in> topspace Y \<Longrightarrow> f(g y) = y"
    and fim: "f \<in> topspace X \<rightarrow> topspace Y" and gim: "g \<in> topspace Y \<rightarrow> topspace X"
    using homXY
    using homeomorphic_space_unfold by blast
  obtain M d where Md: "Metric_space M d" "Metric_space.mcomplete M d" and Xeq: "X = Metric_space.mtopology M d"
    using X by (auto simp: completely_metrizable_space_def)
  then interpret MX: Metric_space M d by metis
  define D where "D \<equiv> \<lambda>x y. d (g x) (g y)"
  have "Metric_space (topspace Y) D"
  proof
    show "(D x y = 0) \<longleftrightarrow> (x = y)" if "x \<in> topspace Y" "y \<in> topspace Y" for x y
      unfolding D_def
      by (metis that MX.topspace_mtopology MX.zero Xeq fg gim Pi_iff)
    show "D x z \<le> D x y +D y z"
      if "x \<in> topspace Y" "y \<in> topspace Y" "z \<in> topspace Y" for x y z
      using that MX.triangle Xeq gim by (auto simp: D_def)
  qed (auto simp: D_def MX.commute)
  then interpret MY: Metric_space "topspace Y" "\<lambda>x y. D x y" by metis
  show ?thesis
    unfolding completely_metrizable_space_def
  proof (intro exI conjI)
    show "Metric_space (topspace Y) D"
      using MY.Metric_space_axioms by blast
    have gball: "g ` MY.mball y r = MX.mball (g y) r" if "y \<in> topspace Y" for y r
      using that MX.topspace_mtopology Xeq gim hmg homeomorphic_imp_surjective_map
      unfolding MX.mball_def MY.mball_def  by (fastforce simp: D_def)
    have "\<exists>r>0. MY.mball y r \<subseteq> S" if "openin Y S" and "y \<in> S" for S y
    proof -
      have "openin X (g`S)"
        using hmg homeomorphic_map_openness_eq that by auto
      then obtain r where "r>0" "MX.mball (g y) r \<subseteq> g`S"
        using MX.openin_mtopology Xeq \<open>y \<in> S\<close> by auto
      then show ?thesis
        by (smt (verit, ccfv_SIG) MY.in_mball gball fg image_iff in_mono openin_subset subsetI that(1))
    qed
    moreover have "openin Y S"
      if "S \<subseteq> topspace Y" and "\<And>y. y \<in> S \<Longrightarrow> \<exists>r>0. MY.mball y r \<subseteq> S" for S
    proof -
      have "\<And>x. x \<in> g`S \<Longrightarrow> \<exists>r>0. MX.mball x r \<subseteq> g`S"
        by (smt (verit) gball imageE image_mono subset_iff that)
      then have "openin X (g`S)"
        using MX.openin_mtopology Xeq gim that(1) by auto
      then show ?thesis
        using hmg homeomorphic_map_openness_eq that(1) by blast
    qed
    ultimately show Yeq: "Y = MY.mtopology"
      unfolding topology_eq MY.openin_mtopology by (metis openin_subset)

    show "MY.mcomplete"
      unfolding MY.mcomplete_def
    proof (intro strip)
      fix \<sigma>
      assume \<sigma>: "MY.MCauchy \<sigma>"
      have "MX.MCauchy (g \<circ> \<sigma>)"
        unfolding MX.MCauchy_def 
      proof (intro conjI strip)
        show "range (g \<circ> \<sigma>) \<subseteq> M"
          using MY.MCauchy_def Xeq \<sigma> gim by auto
        fix \<epsilon> :: real
        assume "\<epsilon> > 0"
        then obtain N where "\<forall>n n'. N \<le> n \<longrightarrow> N \<le> n' \<longrightarrow> D (\<sigma> n) (\<sigma> n') < \<epsilon>"
          using MY.MCauchy_def \<sigma> by presburger
        then show "\<exists>N. \<forall>n n'. N \<le> n \<longrightarrow> N \<le> n' \<longrightarrow> d ((g \<circ> \<sigma>) n) ((g \<circ> \<sigma>) n') < \<epsilon>"
          by (auto simp: o_def D_def)
      qed
      then obtain x where x: "limitin MX.mtopology (g \<circ> \<sigma>) x sequentially" "x \<in> topspace X"
        using MX.limitin_mspace MX.topspace_mtopology Md Xeq unfolding MX.mcomplete_def
        by blast
      with x have "limitin MY.mtopology (f \<circ> (g \<circ> \<sigma>)) (f x) sequentially"
        by (metis Xeq Yeq continuous_map_limit hmf homeomorphic_imp_continuous_map)
      moreover have "f \<circ> (g \<circ> \<sigma>) = \<sigma>"
        using \<open>MY.MCauchy \<sigma>\<close>  by (force simp: fg MY.MCauchy_def subset_iff)
      ultimately have "limitin MY.mtopology \<sigma> (f x) sequentially" by simp
      then show "\<exists>y. limitin MY.mtopology \<sigma> y sequentially"
        by blast 
    qed
  qed
qed

lemma homeomorphic_completely_metrizable_space:
   "X homeomorphic_space Y
        \<Longrightarrow> completely_metrizable_space X \<longleftrightarrow> completely_metrizable_space Y"
  by (meson homeomorphic_completely_metrizable_space_aux homeomorphic_space_sym)

lemma completely_metrizable_space_retraction_map_image:
  assumes r: "retraction_map X Y r" and X: "completely_metrizable_space X"
  shows "completely_metrizable_space Y"
proof -
  obtain s where s: "retraction_maps X Y r s"
    using r retraction_map_def by blast
  then have "subtopology X (s ` topspace Y) homeomorphic_space Y"
    using retraction_maps_section_image2 by blast
  then show ?thesis
    by (metis X retract_of_space_imp_closedin retraction_maps_section_image1 
        homeomorphic_completely_metrizable_space completely_metrizable_space_closedin 
        completely_metrizable_imp_metrizable_space metrizable_imp_Hausdorff_space s)
qed



subsection \<open>Product metric\<close>

text\<open>For the nicest fit with the main Euclidean theories, we choose the Euclidean product, 
though other definitions of the product work.\<close>


definition "prod_dist \<equiv> \<lambda>d1 d2 (x,y) (x',y'). sqrt(d1 x x' ^ 2 + d2 y y' ^ 2)"

locale Metric_space12 = M1: Metric_space M1 d1 + M2: Metric_space M2 d2 for M1 d1 M2 d2

lemma (in Metric_space12) prod_metric: "Metric_space (M1 \<times> M2) (prod_dist d1 d2)"
proof
  fix x y z
  assume xyz: "x \<in> M1 \<times> M2" "y \<in> M1 \<times> M2" "z \<in> M1 \<times> M2"
  have "sqrt ((d1 x1 z1)\<^sup>2 + (d2 x2 z2)\<^sup>2) \<le> sqrt ((d1 x1 y1)\<^sup>2 + (d2 x2 y2)\<^sup>2) + sqrt ((d1 y1 z1)\<^sup>2 + (d2 y2 z2)\<^sup>2)"
      (is "sqrt ?L \<le> ?R")
    if "x = (x1, x2)" "y = (y1, y2)" "z = (z1, z2)"
    for x1 x2 y1 y2 z1 z2
  proof -
    have tri: "d1 x1 z1 \<le> d1 x1 y1 + d1 y1 z1" "d2 x2 z2 \<le> d2 x2 y2 + d2 y2 z2"
      using that xyz M1.triangle [of x1 y1 z1] M2.triangle [of x2 y2 z2] by auto
    show ?thesis
    proof (rule real_le_lsqrt)
      have "?L \<le> (d1 x1 y1 + d1 y1 z1)\<^sup>2 + (d2 x2 y2 + d2 y2 z2)\<^sup>2"
        using tri by (smt (verit) M1.nonneg M2.nonneg power_mono)
      also have "... \<le> ?R\<^sup>2"
        by (metis real_sqrt_sum_squares_triangle_ineq sqrt_le_D)
      finally show "?L \<le> ?R\<^sup>2" .
    qed auto
  qed
  then show "prod_dist d1 d2 x z \<le> prod_dist d1 d2 x y + prod_dist d1 d2 y z"
    by (simp add: prod_dist_def case_prod_unfold)
qed (auto simp: M1.commute M2.commute case_prod_unfold prod_dist_def)

sublocale Metric_space12 \<subseteq> Prod_metric: Metric_space "M1\<times>M2" "prod_dist d1 d2" 
  by (simp add: prod_metric)

text \<open>For easy reference to theorems outside of the locale\<close>
lemma Metric_space12_mspace_mdist:
  "Metric_space12 (mspace m1) (mdist m1) (mspace m2) (mdist m2)"
  by (simp add: Metric_space12_def)

definition prod_metric where
 "prod_metric \<equiv> \<lambda>m1 m2. metric (mspace m1 \<times> mspace m2, prod_dist (mdist m1) (mdist m2))"

lemma submetric_prod_metric:
   "submetric (prod_metric m1 m2) (S \<times> T) = prod_metric (submetric m1 S) (submetric m2 T)"
  apply (simp add: prod_metric_def)
  by (simp add: submetric_def Metric_space.mspace_metric Metric_space.mdist_metric Metric_space12.prod_metric Metric_space12_def Times_Int_Times)

lemma mspace_prod_metric [simp]:"
  mspace (prod_metric m1 m2) = mspace m1 \<times> mspace m2"
  by (simp add: prod_metric_def Metric_space.mspace_metric Metric_space12.prod_metric Metric_space12_mspace_mdist)

lemma mdist_prod_metric [simp]: 
  "mdist (prod_metric m1 m2) = prod_dist (mdist m1) (mdist m2)"
  by (metis Metric_space.mdist_metric Metric_space12.prod_metric Metric_space12_mspace_mdist prod_metric_def)

lemma prod_dist_dist [simp]: "prod_dist dist dist = dist"
  by (simp add: prod_dist_def dist_prod_def fun_eq_iff)

lemma prod_metric_euclidean [simp]:
  "prod_metric euclidean_metric euclidean_metric = euclidean_metric"
  by (simp add: prod_metric_def euclidean_metric_def)

context Metric_space12
begin

lemma component_le_prod_metric:
   "d1 x1 x2 \<le> prod_dist d1 d2 (x1,y1) (x2,y2)" "d2 y1 y2 \<le> prod_dist d1 d2 (x1,y1) (x2,y2)"
  by (auto simp: prod_dist_def)

lemma prod_metric_le_components:
  "\<lbrakk>x1 \<in> M1; y1 \<in> M1; x2 \<in> M2; y2 \<in> M2\<rbrakk>
    \<Longrightarrow> prod_dist d1 d2 (x1,x2) (y1,y2) \<le> d1 x1 y1 + d2 x2 y2"
  by (auto simp: prod_dist_def sqrt_sum_squares_le_sum)

lemma mball_prod_metric_subset:
   "Prod_metric.mball (x,y) r \<subseteq> M1.mball x r \<times> M2.mball y r"
  by clarsimp (smt (verit, best) component_le_prod_metric)

lemma mcball_prod_metric_subset:
   "Prod_metric.mcball (x,y) r \<subseteq> M1.mcball x r \<times> M2.mcball y r"
  by clarsimp (smt (verit, best) component_le_prod_metric)

lemma mball_subset_prod_metric:
   "M1.mball x1 r1 \<times> M2.mball x2 r2 \<subseteq> Prod_metric.mball (x1,x2) (r1 + r2)"
  using prod_metric_le_components by force

lemma mcball_subset_prod_metric:
   "M1.mcball x1 r1 \<times> M2.mcball x2 r2 \<subseteq> Prod_metric.mcball (x1,x2) (r1 + r2)"
  using prod_metric_le_components by force

lemma mtopology_prod_metric:
  "Prod_metric.mtopology = prod_topology M1.mtopology M2.mtopology"
  unfolding prod_topology_def
proof (rule topology_base_unique [symmetric])
  fix U
  assume "U \<in> {S \<times> T |S T. openin M1.mtopology S \<and> openin M2.mtopology T}"
  then obtain S T where Ueq: "U = S \<times> T"
    and S: "openin M1.mtopology S" and T: "openin M2.mtopology T"
    by auto
  have "S \<subseteq> M1"
    using M1.openin_mtopology S by auto
  have "T \<subseteq> M2"
    using M2.openin_mtopology T by auto
  show "openin Prod_metric.mtopology U"
    unfolding Prod_metric.openin_mtopology
  proof (intro conjI strip)
    show "U \<subseteq> M1 \<times> M2"
      using Ueq by (simp add: Sigma_mono \<open>S \<subseteq> M1\<close> \<open>T \<subseteq> M2\<close>)
    fix z
    assume "z \<in> U"
    then obtain x1 x2 where "x1 \<in> S" "x2 \<in> T" and zeq: "z = (x1,x2)"
      using Ueq by blast
    obtain r1 where "r1>0" and r1: "M1.mball x1 r1 \<subseteq> S"
      by (meson M1.openin_mtopology \<open>openin M1.mtopology S\<close> \<open>x1 \<in> S\<close>)
    obtain r2 where "r2>0" and r2: "M2.mball x2 r2 \<subseteq> T"
      by (meson M2.openin_mtopology \<open>openin M2.mtopology T\<close> \<open>x2 \<in> T\<close>)
    have "Prod_metric.mball (x1,x2) (min r1 r2) \<subseteq> U"
    proof (rule order_trans [OF mball_prod_metric_subset])
      show "M1.mball x1 (min r1 r2) \<times> M2.mball x2 (min r1 r2) \<subseteq> U"
        using Ueq r1 r2 by force
    qed
    then show "\<exists>r>0. Prod_metric.mball z r \<subseteq> U"
      by (smt (verit, del_insts) zeq \<open>0 < r1\<close> \<open>0 < r2\<close>)
  qed
next
  fix U z
  assume "openin Prod_metric.mtopology U" and "z \<in> U"
  then have "U \<subseteq> M1 \<times> M2"
    by (simp add: Prod_metric.openin_mtopology)
  then obtain x y where "x \<in> M1" "y \<in> M2" and zeq: "z = (x,y)"
    using \<open>z \<in> U\<close> by blast
  obtain r where "r>0" and r: "Prod_metric.mball (x,y) r \<subseteq> U"
    by (metis Prod_metric.openin_mtopology \<open>openin Prod_metric.mtopology U\<close> \<open>z \<in> U\<close> zeq)
  define B1 where "B1 \<equiv> M1.mball x (r/2)"
  define B2 where "B2 \<equiv> M2.mball y (r/2)"
  have "openin M1.mtopology B1" "openin M2.mtopology B2"
    by (simp_all add: B1_def B2_def)
  moreover have "(x,y) \<in> B1 \<times> B2"
    using \<open>r > 0\<close> by (simp add: \<open>x \<in> M1\<close> \<open>y \<in> M2\<close> B1_def B2_def)
  moreover have "B1 \<times> B2 \<subseteq> U"
    using r prod_metric_le_components by (force simp: B1_def B2_def)
  ultimately show "\<exists>B. B \<in> {S \<times> T |S T. openin M1.mtopology S \<and> openin M2.mtopology T} \<and> z \<in> B \<and> B \<subseteq> U"
    by (auto simp: zeq)
qed

lemma MCauchy_prod_metric:
   "Prod_metric.MCauchy \<sigma> \<longleftrightarrow> M1.MCauchy (fst \<circ> \<sigma>) \<and> M2.MCauchy (snd \<circ> \<sigma>)"
   (is "?lhs \<longleftrightarrow> ?rhs")
proof safe
  assume L: ?lhs
  then have "range \<sigma> \<subseteq> M1 \<times> M2"
    using Prod_metric.MCauchy_def by blast
  then have 1: "range (fst \<circ> \<sigma>) \<subseteq> M1" and 2: "range (snd \<circ> \<sigma>) \<subseteq> M2"
    by auto
  have N1: "\<exists>N. \<forall>n\<ge>N. \<forall>n'\<ge>N. d1 (fst (\<sigma> n)) (fst (\<sigma> n')) < \<epsilon>" 
    and N2: "\<exists>N. \<forall>n\<ge>N. \<forall>n'\<ge>N. d2 (snd (\<sigma> n)) (snd (\<sigma> n')) < \<epsilon>" if "\<epsilon>>0" for \<epsilon> :: real
    using that L unfolding Prod_metric.MCauchy_def
    by (smt (verit, del_insts) add.commute add_less_imp_less_left add_right_mono 
        component_le_prod_metric prod.collapse)+
  show "M1.MCauchy (fst \<circ> \<sigma>)"
    using 1 N1 M1.MCauchy_def by auto
  have "\<exists>N. \<forall>n\<ge>N. \<forall>n'\<ge>N. d2 (snd (\<sigma> n)) (snd (\<sigma> n')) < \<epsilon>" if "\<epsilon>>0" for \<epsilon> :: real
    using that L unfolding Prod_metric.MCauchy_def
    by (smt (verit, del_insts) add.commute add_less_imp_less_left add_right_mono 
        component_le_prod_metric prod.collapse)
  show "M2.MCauchy (snd \<circ> \<sigma>)"
    using 2 N2 M2.MCauchy_def by auto
next
  assume M1: "M1.MCauchy (fst \<circ> \<sigma>)" and M2: "M2.MCauchy (snd \<circ> \<sigma>)"
  then have subM12: "range (fst \<circ> \<sigma>) \<subseteq> M1" "range (snd \<circ> \<sigma>) \<subseteq> M2"
    using M1.MCauchy_def M2.MCauchy_def by blast+
  show ?lhs
    unfolding Prod_metric.MCauchy_def
  proof (intro conjI strip)
    show "range \<sigma> \<subseteq> M1 \<times> M2"
      using subM12 by (smt (verit, best) SigmaI image_subset_iff o_apply prod.collapse) 
    fix \<epsilon> :: real
    assume "\<epsilon> > 0"
    obtain N1 where N1: "\<And>n n'. N1 \<le> n \<Longrightarrow> N1 \<le> n' \<Longrightarrow> d1 ((fst \<circ> \<sigma>) n) ((fst \<circ> \<sigma>) n') < \<epsilon>/2"
      by (meson M1.MCauchy_def \<open>0 < \<epsilon>\<close> M1 zero_less_divide_iff zero_less_numeral)
    obtain N2 where N2: "\<And>n n'. N2 \<le> n \<Longrightarrow> N2 \<le> n' \<Longrightarrow> d2 ((snd \<circ> \<sigma>) n) ((snd \<circ> \<sigma>) n') < \<epsilon>/2"
      by (meson M2.MCauchy_def \<open>0 < \<epsilon>\<close> M2 zero_less_divide_iff zero_less_numeral)
    have "prod_dist d1 d2 (\<sigma> n) (\<sigma> n') < \<epsilon>"
      if "N1 \<le> n" and "N2 \<le> n" and "N1 \<le> n'" and "N2 \<le> n'" for n n'
    proof -
      obtain a b a' b' where \<sigma>: "\<sigma> n = (a,b)" "\<sigma> n' = (a',b')"
        by fastforce+
      have "prod_dist d1 d2 (a,b) (a',b') \<le> d1 a a' + d2 b b'"
        by (metis \<open>range \<sigma> \<subseteq> M1 \<times> M2\<close> \<sigma> mem_Sigma_iff prod_metric_le_components range_subsetD)
      also have "\<dots> < \<epsilon>/2 + \<epsilon>/2"
        using N1 N2 \<sigma> that by fastforce
      finally show ?thesis
        by (simp add: \<sigma>)
    qed
    then show "\<exists>N. \<forall>n n'. N \<le> n \<longrightarrow> N \<le> n' \<longrightarrow> prod_dist d1 d2 (\<sigma> n) (\<sigma> n') < \<epsilon>"
      by (metis order.trans linorder_le_cases)
  qed
qed


lemma mcomplete_prod_metric:
  "Prod_metric.mcomplete \<longleftrightarrow> M1 = {} \<or> M2 = {} \<or> M1.mcomplete \<and> M2.mcomplete"
  (is "?lhs \<longleftrightarrow> ?rhs")
proof (cases "M1 = {} \<or> M2 = {}")
  case False
  then obtain x y where "x \<in> M1" "y \<in> M2"
    by blast
  have "M1.mcomplete \<and> M2.mcomplete \<Longrightarrow> Prod_metric.mcomplete"
    by (simp add: Prod_metric.mcomplete_def M1.mcomplete_def M2.mcomplete_def 
        mtopology_prod_metric MCauchy_prod_metric limitin_pairwise)
  moreover
  { assume L: "Prod_metric.mcomplete"
    have "M1.mcomplete"
      unfolding M1.mcomplete_def
    proof (intro strip)
      fix \<sigma>
      assume "M1.MCauchy \<sigma>"
      then have "Prod_metric.MCauchy (\<lambda>n. (\<sigma> n, y))"
        using \<open>y \<in> M2\<close> by (simp add: M1.MCauchy_def M2.MCauchy_def MCauchy_prod_metric)
      then obtain z where "limitin Prod_metric.mtopology (\<lambda>n. (\<sigma> n, y)) z sequentially"
        using L Prod_metric.mcomplete_def by blast
      then show "\<exists>x. limitin M1.mtopology \<sigma> x sequentially"
        by (auto simp: Prod_metric.mcomplete_def M1.mcomplete_def 
             mtopology_prod_metric limitin_pairwise o_def)
    qed
  }
  moreover
  { assume L: "Prod_metric.mcomplete"
    have "M2.mcomplete"
      unfolding M2.mcomplete_def
    proof (intro strip)
      fix \<sigma>
      assume "M2.MCauchy \<sigma>"
      then have "Prod_metric.MCauchy (\<lambda>n. (x, \<sigma> n))"
        using \<open>x \<in> M1\<close> by (simp add: M2.MCauchy_def M1.MCauchy_def MCauchy_prod_metric)
      then obtain z where "limitin Prod_metric.mtopology (\<lambda>n. (x, \<sigma> n)) z sequentially"
        using L Prod_metric.mcomplete_def by blast
      then show "\<exists>x. limitin M2.mtopology \<sigma> x sequentially"
        by (auto simp: Prod_metric.mcomplete_def M2.mcomplete_def 
             mtopology_prod_metric limitin_pairwise o_def)
    qed
  }
  ultimately show ?thesis
    using False by blast 
qed auto

lemma mbounded_prod_metric:
   "Prod_metric.mbounded U \<longleftrightarrow> M1.mbounded  (fst ` U) \<and> M2.mbounded (snd ` U)"
proof -
  have "(\<exists>B. U \<subseteq> Prod_metric.mcball (x,y) B) 
    \<longleftrightarrow> ((\<exists>B. (fst ` U) \<subseteq> M1.mcball x B) \<and> (\<exists>B. (snd ` U) \<subseteq> M2.mcball y B))" (is "?lhs \<longleftrightarrow> ?rhs")
    for x y
  proof safe
    fix B
    assume "U \<subseteq> Prod_metric.mcball (x, y) B"
    then have "(fst ` U) \<subseteq> M1.mcball x B" "(snd ` U) \<subseteq> M2.mcball y B"
      using mcball_prod_metric_subset by fastforce+
    then show "\<exists>B. (fst ` U) \<subseteq> M1.mcball x B" "\<exists>B. (snd ` U) \<subseteq> M2.mcball y B"
      by auto
  next
    fix B1 B2
    assume "(fst ` U) \<subseteq> M1.mcball x B1" "(snd ` U) \<subseteq> M2.mcball y B2"
    then have "fst ` U \<times> snd ` U \<subseteq>  M1.mcball x B1 \<times> M2.mcball y B2"
      by blast
    also have "\<dots> \<subseteq> Prod_metric.mcball (x, y) (B1+B2)"
      by (intro mcball_subset_prod_metric)
    finally show "\<exists>B. U \<subseteq> Prod_metric.mcball (x, y) B"
      by (metis subsetD subsetI subset_fst_snd)
  qed
  then show ?thesis
    by (simp add: M1.mbounded_def M2.mbounded_def Prod_metric.mbounded_def)
qed 

lemma mbounded_Times:
   "Prod_metric.mbounded (S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> M1.mbounded S \<and> M2.mbounded T"
  by (auto simp: mbounded_prod_metric)


lemma mtotally_bounded_Times:
   "Prod_metric.mtotally_bounded (S \<times> T) \<longleftrightarrow>
    S = {} \<or> T = {} \<or> M1.mtotally_bounded S \<and> M2.mtotally_bounded T"
    (is "?lhs \<longleftrightarrow> _")
proof (cases "S = {} \<or> T = {}")
  case False
  then obtain x y where "x \<in> S" "y \<in> T"
    by auto
  have "M1.mtotally_bounded S" if L: ?lhs
    unfolding M1.mtotally_bounded_sequentially
  proof (intro conjI strip)
    show "S \<subseteq> M1"
      using Prod_metric.mtotally_bounded_imp_subset \<open>y \<in> T\<close> that by blast
    fix \<sigma> :: "nat \<Rightarrow> 'a"
    assume "range \<sigma> \<subseteq> S"
    with L obtain r where "strict_mono r" "Prod_metric.MCauchy ((\<lambda>n. (\<sigma> n,y)) \<circ> r)"
      unfolding Prod_metric.mtotally_bounded_sequentially
      by (smt (verit) SigmaI \<open>y \<in> T\<close> image_subset_iff)
    then have "M1.MCauchy (fst \<circ> (\<lambda>n. (\<sigma> n,y)) \<circ> r)"
      by (simp add: MCauchy_prod_metric o_def)
    with \<open>strict_mono r\<close> show "\<exists>r. strict_mono r \<and> M1.MCauchy (\<sigma> \<circ> r)"
      by (auto simp: o_def)
  qed
  moreover
  have "M2.mtotally_bounded T" if L: ?lhs
    unfolding M2.mtotally_bounded_sequentially
  proof (intro conjI strip)
    show "T \<subseteq> M2"
      using Prod_metric.mtotally_bounded_imp_subset \<open>x \<in> S\<close> that by blast
    fix \<sigma> :: "nat \<Rightarrow> 'b"
    assume "range \<sigma> \<subseteq> T"
    with L obtain r where "strict_mono r" "Prod_metric.MCauchy ((\<lambda>n. (x,\<sigma> n)) \<circ> r)"
      unfolding Prod_metric.mtotally_bounded_sequentially
      by (smt (verit) SigmaI \<open>x \<in> S\<close> image_subset_iff)
    then have "M2.MCauchy (snd \<circ> (\<lambda>n. (x,\<sigma> n)) \<circ> r)"
      by (simp add: MCauchy_prod_metric o_def)
    with \<open>strict_mono r\<close> show "\<exists>r. strict_mono r \<and> M2.MCauchy (\<sigma> \<circ> r)"
      by (auto simp: o_def)
  qed
  moreover have ?lhs if 1: "M1.mtotally_bounded S" and 2: "M2.mtotally_bounded T"
    unfolding Prod_metric.mtotally_bounded_sequentially
  proof (intro conjI strip)
    show "S \<times> T \<subseteq> M1 \<times> M2"
      using that 
      by (auto simp: M1.mtotally_bounded_sequentially M2.mtotally_bounded_sequentially)
    fix \<sigma> :: "nat \<Rightarrow> 'a \<times> 'b"
    assume \<sigma>: "range \<sigma> \<subseteq> S \<times> T"
    with 1 obtain r1 where r1: "strict_mono r1" "M1.MCauchy (fst ∘ σ ∘ r1)"
      by (metis M1.mtotally_bounded_sequentially comp_apply image_subset_iff mem_Sigma_iff prod.collapse)
    from σ 2 obtain r2 where r2: "strict_mono r2" "M2.MCauchy (snd ∘ σ ∘ r1 ∘ r2)"
      apply (clarsimp simp: M2.mtotally_bounded_sequentially image_subset_iff)
      by (smt (verit, best) comp_apply mem_Sigma_iff prod.collapse)
    then have "M1.MCauchy (fst ∘ σ ∘ r1 ∘ r2)"
      by (simp add: M1.MCauchy_subsequence r1)
    with r2 have "Prod_metric.MCauchy (σ ∘ (r1 ∘ r2))"
      by (simp add: MCauchy_prod_metric o_def)
    then show "∃r. strict_mono r ∧ Prod_metric.MCauchy (σ ∘ r)"
      using r1 r2 strict_mono_o by blast
  qed
  ultimately show ?thesis
    using False by blast
qed auto

lemma mtotally_bounded_prod_metric:
   "Prod_metric.mtotally_bounded U ⟷
    M1.mtotally_bounded (fst ` U) ∧ M2.mtotally_bounded (snd ` U)" (is "?lhs ⟷ ?rhs")
proof
  assume L: ?lhs
  then have "U ⊆ M1 × M2"
    and *: "∧σ. range σ ⊆ U ==> ∃r::nat→nat. strict_mono r ∧ Prod_metric.MCauchy (σ∘r)"
    by (simp_all add: Prod_metric.mtotally_bounded_sequentially)
  show ?rhs
    unfolding M1.mtotally_bounded_sequentially M2.mtotally_bounded_sequentially
  proof (intro conjI strip)
    show "fst ` U ⊆ M1" "snd ` U ⊆ M2"
      using ‹U ⊆ M1 × M2› by auto
  next
    fix σ :: "nat → 'a"
    assume "range σ ⊆ fst ` U"
    then obtain ζ where ζ: "∧n. σ n = fst (ζ n) ∧ ζ n ∈ U"
      unfolding image_subset_iff image_iff by (meson UNIV_I)
    then obtain r where "strict_mono r ∧ Prod_metric.MCauchy (ζ∘r)"
      by (metis "*" image_subset_iff)
    with ζ show "∃r. strict_mono r ∧ M1.MCauchy (σ ∘ r)"
      by (auto simp: MCauchy_prod_metric o_def)
  next
    fix σ:: "nat → 'b"
    assume "range σ ⊆ snd ` U"
    then obtain ζ where ζ: "∧n. σ n = snd (ζ n) ∧ ζ n ∈ U"
      unfolding image_subset_iff image_iff by (meson UNIV_I)
    then obtain r where "strict_mono r ∧ Prod_metric.MCauchy (ζ∘r)"
      by (metis "*" image_subset_iff)
    with ζ show "∃r. strict_mono r ∧ M2.MCauchy (σ ∘ r)"
      by (auto simp: MCauchy_prod_metric o_def)
  qed
next
  assume ?rhs
  then have "Prod_metric.mtotally_bounded ((fst ` U) × (snd ` U))"
    by (simp add: mtotally_bounded_Times)
  then show ?lhs
    by (metis Prod_metric.mtotally_bounded_subset subset_fst_snd)
qed

end


lemma metrizable_space_prod_topology:
   "metrizable_space (prod_topology X Y) ⟷
    (prod_topology X Y) = trivial_topology ∨ metrizable_space X ∧ metrizable_space Y"
   (is "?lhs ⟷ ?rhs")
proof (cases "(prod_topology X Y) = trivial_topology")
  case False
  then obtain x y where "x ∈ topspace X" "y ∈ topspace Y"
    by fastforce
  show ?thesis
  proof
    show "?rhs ==> ?lhs"
      unfolding metrizable_space_def
      using Metric_space12.mtopology_prod_metric
      by (metis False Metric_space12.prod_metric Metric_space12_def)
  next
    assume L: ?lhs
    have "metrizable_space (subtopology (prod_topology X Y) (topspace X × {y}))"
      "metrizable_space (subtopology (prod_topology X Y) ({x} × topspace Y))"
      using L metrizable_space_subtopology by auto
    moreover
    have "(subtopology (prod_topology X Y) (topspace X × {y})) homeomorphic_space X"
      by (metis ‹y ∈ topspace Y› homeomorphic_space_prod_topology_sing1 homeomorphic_space_sym prod_topology_subtopology(2))
    moreover
    have "(subtopology (prod_topology X Y) ({x} × topspace Y)) homeomorphic_space Y"
      by (metis ‹x ∈ topspace X› homeomorphic_space_prod_topology_sing2 homeomorphic_space_sym prod_topology_subtopology(1))
    ultimately show ?rhs
      by (simp add: homeomorphic_metrizable_space)
  qed
qed auto


lemma completely_metrizable_space_prod_topology:
   "completely_metrizable_space (prod_topology X Y) ⟷
    (prod_topology X Y) = trivial_topology ∨
    completely_metrizable_space X ∧ completely_metrizable_space Y"
   (is "?lhs ⟷ ?rhs")
proof (cases "(prod_topology X Y) = trivial_topology")
  case False
  then obtain x y where "x ∈ topspace X" "y ∈ topspace Y"
    by fastforce
  show ?thesis
  proof
    show "?rhs ==> ?lhs"
      unfolding completely_metrizable_space_def
      by (metis False Metric_space12.mtopology_prod_metric Metric_space12.mcomplete_prod_metric
          Metric_space12.prod_metric Metric_space12_def)
  next
    assume L: ?lhs
    then have "Hausdorff_space (prod_topology X Y)"
      by (simp add: completely_metrizable_imp_metrizable_space metrizable_imp_Hausdorff_space)
    then have H: "Hausdorff_space X ∧ Hausdorff_space Y"
      using False Hausdorff_space_prod_topology by blast
    then have "closedin (prod_topology X Y) (topspace X × {y}) ∧ closedin (prod_topology X Y) ({x} × topspace Y)"
      using ‹x ∈ topspace X› ‹y ∈ topspace Y›
      by (auto simp: closedin_Hausdorff_sing_eq closedin_prod_Times_iff)
    with L have "completely_metrizable_space(subtopology (prod_topology X Y) (topspace X × {y}))
               ∧ completely_metrizable_space(subtopology (prod_topology X Y) ({x} × topspace Y))"
      by (simp add: completely_metrizable_space_closedin)
    moreover
    have "(subtopology (prod_topology X Y) (topspace X × {y})) homeomorphic_space X"
      by (metis ‹y ∈ topspace Y› homeomorphic_space_prod_topology_sing1 homeomorphic_space_sym prod_topology_subtopology(2))
    moreover
    have "(subtopology (prod_topology X Y) ({x} × topspace Y)) homeomorphic_space Y"
      by (metis ‹x ∈ topspace X› homeomorphic_space_prod_topology_sing2 homeomorphic_space_sym prod_topology_subtopology(1))
    ultimately show ?rhs
      by (simp add: homeomorphic_completely_metrizable_space)
  qed
next
  case True then show ?thesis
    using empty_completely_metrizable_space by auto
qed

    
subsection‹More sequential characterizations in a metric space›

context Metric_space
begin
  
definition decreasing_dist :: "(nat → 'a) → 'a → bool"
    where "decreasing_dist σ x ≡ (∀m n. m < n ⟶ d (σ n) x < d (σ m) x)"

lemma decreasing_dist_imp_inj: "decreasing_dist σ a ==> inj σ"
  by (metis decreasing_dist_def dual_order.irrefl linorder_inj_onI')

lemma eventually_atin_within_metric:
   "eventually P (atin_within mtopology a S) ⟷
    (a ∈ M ⟶ (∃δ>0. ∀x. x ∈ M ∧ x ∈ S ∧ 0 < d x a ∧ d x a < δ ⟶ P x))" (is "?lhs=?rhs")
proof
  assume ?lhs then show ?rhs
unfolding eventually_atin_within openin_mtopology subset_iff
  by (metis commute in_mball mdist_zero order_less_irrefl topspace_mtopology)
next
  assume R: ?rhs
  show ?lhs
  proof (cases "a ∈ M")
    case True
    then obtain δ where "δ > 0" and δ: "∧x. [x ∈ M; x ∈ S; 0 < d x a; d x a < δ] ==> P x"
      using R by blast
    then have "openin mtopology (mball a δ) ∧ (∀x ∈ mball a δ. x ∈ S ∧ x ≠ a ⟶ P x)"
      by (simp add: commute openin_mball)
    then show ?thesis
      by (metis True ‹0 < δ› centre_in_mball_iff eventually_atin_within)
  next
    case False
    with R show ?thesis
      by (simp add: eventually_atin_within)
  qed
qed


lemma eventually_atin_within_A:
  assumes
    "(∧σ. [range σ ⊆ (S ∩ M) - {a}; decreasing_dist σ a;
          inj σ; limitin mtopology σ a sequentially]
      ==> eventually (λn. P (σ n)) sequentially)"
  shows "eventually P (atin_within mtopology a S)"
proof -
  have False if SP: "∧δ. δ>0 ==> ∃x ∈ M-{a}. d x a < δ ∧ x ∈ S ∧ ¬ P x" and "a ∈ M"
  proof -
    define Φ where "Φ ≡ λn x. x ∈ M-{a} ∧ d x a < inverse (Suc n) ∧ x ∈ S ∧ ¬ P x"
    obtain σ where σ: "∧n. Φ n (σ n)" and dless: "∧n. d (σ(Suc n)) a < d (σ n) a"
    proof -
      obtain x0 where x0: "Φ 0 x0"
        using SP [OF zero_less_one] by (force simp: Φ_def)
      have "∃y. Φ (Suc n) y ∧ d y a < d x a" if "Φ n x" for n x
        using SP [of "min (inverse (Suc (Suc n))) (d x a)"] ‹a ∈ M› that
        by (auto simp: Φ_def)
      then obtain f where f: "∧n x. Φ n x ==> Φ (Suc n) (f n x) ∧ d (f n x) a < d x a"
        by metis
      show thesis
        proof
          show "Φ n (rec_nat x0 f n)" for n
            by (induction n) (auto simp: x0 dest: f)
          with f show "d (rec_nat x0 f (Suc n)) a < d (rec_nat x0 f n) a" for n
            by auto
        qed
    qed
    have 1: "range σ ⊆ (S ∩ M) - {a}"
      using σ by (auto simp: Φ_def)
    have "d (σ(Suc (m+n))) a < d (σ n) a" for m n
      by (induction m) (auto intro: order_less_trans dless)
    then have 2: "decreasing_dist σ a"
      unfolding decreasing_dist_def by (metis add.commute less_imp_Suc_add)
    have "∀_F xa in sequentially. d (σ xa) a < ε" if "ε > 0" for ε
    proof -
      obtain N where "inverse (Suc N) < ε"
        using ‹ε > 0› reals_Archimedean by blast
      with σ 2 show ?thesis
        unfolding decreasing_dist_def by (smt (verit, best) Φ_def eventually_at_top_dense)
    qed
    then have 4: "limitin mtopology σ a sequentially"
      using σ ‹a ∈ M› by (simp add: Φ_def limitin_metric)
    show False
      using 2 assms [OF 1 _ decreasing_dist_imp_inj 4] σ by (force simp: Φ_def)
  qed
  then show ?thesis
    by (fastforce simp: eventually_atin_within_metric)
qed


lemma eventually_atin_within_B:
  assumes ev: "eventually P (atin_within mtopology a S)"
    and ran: "range σ ⊆ (S ∩ M) - {a}"
    and lim: "limitin mtopology σ a sequentially"
  shows "eventually (λn. P (σ n)) sequentially"
proof -
  have "a ∈ M"
    using lim limitin_mspace by auto
  with ev obtain δ where "0 < δ"
    and δ: "∧σ. [σ ∈ M; σ ∈ S; 0 < d σ a; d σ a < δ] ==> P σ"
    by (auto simp: eventually_atin_within_metric)
  then have *: "∧n. σ n ∈ M ∧ d (σ n) a < δ ==> P (σ n)"
    using ‹a ∈ M› ran by auto
  have "∀_F n in sequentially. σ n ∈ M ∧ d (σ n) a < δ"
    using lim ‹0 < δ› by (auto simp: limitin_metric)
  then show ?thesis
    by (simp add: "*" eventually_mono)
qed

lemma eventually_atin_within_sequentially:
     "eventually P (atin_within mtopology a S) ⟷
        (∀σ. range σ ⊆ (S ∩ M) - {a} ∧
            limitin mtopology σ a sequentially
            ⟶ eventually (λn. P(σ n)) sequentially)"
  by (metis eventually_atin_within_A eventually_atin_within_B)

lemma eventually_atin_within_sequentially_inj:
     "eventually P (atin_within mtopology a S) ⟷
        (∀σ. range σ ⊆ (S ∩ M) - {a} ∧ inj σ ∧
            limitin mtopology σ a sequentially
            ⟶ eventually (λn. P(σ n)) sequentially)"
  by (metis eventually_atin_within_A eventually_atin_within_B)

lemma eventually_atin_within_sequentially_decreasing:
     "eventually P (atin_within mtopology a S) ⟷
        (∀σ. range σ ⊆ (S ∩ M) - {a} ∧ decreasing_dist σ a ∧
            limitin mtopology σ a sequentially
            ⟶ eventually (λn. P(σ n)) sequentially)"
  by (metis eventually_atin_within_A eventually_atin_within_B)


lemma eventually_atin_sequentially:
   "eventually P (atin mtopology a) ⟷
    (∀σ. range σ ⊆ M - {a} ∧ limitin mtopology σ a sequentially
         ⟶ eventually (λn. P(σ n)) sequentially)"
  using eventually_atin_within_sequentially [where S=UNIV] by simp

lemma eventually_atin_sequentially_inj:
   "eventually P (atin mtopology a) ⟷
    (∀σ. range σ ⊆ M - {a} ∧ inj σ ∧
        limitin mtopology σ a sequentially
        ⟶ eventually (λn. P(σ n)) sequentially)"
  using eventually_atin_within_sequentially_inj [where S=UNIV] by simp

lemma eventually_atin_sequentially_decreasing:
   "eventually P (atin mtopology a) ⟷
    (∀σ. range σ ⊆ M - {a} ∧ decreasing_dist σ a ∧
         limitin mtopology σ a sequentially
        ⟶ eventually (λn. P(σ n)) sequentially)"
  using eventually_atin_within_sequentially_decreasing [where S=UNIV] by simp

end

context Metric_space12
begin

lemma limit_atin_sequentially_within:
  "limitin M2.mtopology f l (atin_within M1.mtopology a S) \longleftrightarrow
     l ∈
     (∀σ ⊆ M1 - {a} ∧ueSPe)
          limitin M1.mtopology σ
          ⟶g( <c> \<igma)‹HOL-Analysis.Sigma_Algebra›.
    by (auto simp: M1.eventually_atin_within_sequentially limitin_def)

lemma limit_atin_sequentially_within_inj:
  "limitin M2.mtopology f l (atin_within M1.mtopology a S) ⟷
     l ∈ M2 ∧
     (∀σ. range σ ⊆ S ∩ M1 - {a} ∧ inj σ ∧
          limitin M1.mtopology σ a sequentially
          ⟶ limitin M2.mtopology (f ∘ σ) l sequentially)"
    by (auto simp: M1.eventually_atin_within_sequentially_inj limitin_def)

lemma limit_atin_sequentially_within_decreasing:
  "limitin M2.mtopology f l (atin_within M1.mtopology a S) ⟷
     l ∈ M2 ∧
     (∀σ. range σ ⊆ S ∩ M1 - {a} ∧ M1.decreasing_dist σ a ∧
          limitin M1.mtopology σ a sequentially
          ⟶ limitin M2.mtopology (f ∘ σ) l sequentially)"
    by (auto simp: M1.eventually_atin_within_sequentially_decreasing limitin_def)

lemma limit_atin_sequentially:
   "limitin M2.mtopology f l (atin M1.mtopology a) ⟷
        l ∈ M2 ∧
        (∀σ. range σ ⊆ M1 - {a} ∧
            limitin M1.mtopology σ a sequentially
            ⟶ limitin M2.mtopology (f ∘ σ) l sequentially)"
  using limit_atin_sequentially_within [where S=UNIV] by simp

lemma limit_atin_sequentially_inj:
   "limitin M2.mtopology f l (atin M1.mtopology a) ⟷
        l ∈ M2 ∧
        (∀σ. range σ ⊆ M1 - {a} ∧ inj σ ∧
            limitin M1.mtopology σ a sequentially
            ⟶ limitin M2.mtopology (f ∘ σ›definition subadditive where
  using limit_atin_sequentially_within_inj

lemma limit_atin_sequentially_decreasing:
java.lang.StringIndexOutOfBoundsException: Range [71, 70) out of bounds for length 71
     l ∈ M2 ∧
     (∀σ. range σ ⊆ M1 - {a} ∧ M1.decreasing_dist σ a ∧
          limitin M1.mtopology σ a sequentially
          ⟶ limitin M2.mtopology (f ∘ σ) l sequentially)"
  using limit_atin_sequentially_within_decreasing [where S=UNIV] by simp

end

text ‹An experiment: same result as within the locale, but using metric space variables›
lemma limit_atin_sequentially_within:
  "limitin (mtopology_of m2) f l (atin_within (mtopology_of m1) a S) ⟷
     l ∈ mspace m2 ∧
     (∀σ. range σ ⊆ S ∩ mspace m1 - {a} ∧
          limitin (mtopology_of m1) σ a sequentially
          ⟶ limitin (mtopology_of m2) (f ∘ σ) l sequentially)"
  using Metric_space12.limit_atin_sequentially_within [OF Metric_space12_mspace_mdist]
  by (metis mtopology_of_def)


context Metric_space
begin

lemma atin_within_imp_M:
   "atin_within mtopology x S ≠ bot ==> x ∈ M"
  by (metis derived_set_of_trivial_limit in_derived_set_of topspace_mtopology)

lemma atin_within_sequentially_sequence:
  assumes "atin_within mtopology x S ≠ bot"
  obtains σ where "range σ subseteq> S ∩ M - {x}"
          "decreasing_dist σ x" "inj σ" "limitin mtopology σ x sequentially"
  by (metis evenalyai_ihinA evetully_Fleass

lemma derived_set_of_sequentially:
  "mtpog eie_eo
   {x ∈:pstv <L> f {} = 0" by (auto simp: positive_def)
proof -
  have False
    if "range σ ⊆ countably_additive M f"
java.lang.StringIndexOutOfBoundsException: Range [37, 36) out of bounds for length 53
 an ai_ihnmolg o"
java.lang.StringIndexOutOfBoundsException: Range [18, 17) out of bounds for length 18
  proof -
    have "∀F n in sequentially. P (σn)" f
      using that by (metis eventually_atin_within_B eventually_bot)
    then show False
      by (meso vula_qtayvntual_on
  qed
  then show heis
    using derived_set_of_trivial_limit
    by (fastforce elim!: atin_within_sequentially_sequence intro: atin_within_imp
qed

java.lang.StringIndexOutOfBoundsException: Range [13, 5) out of bounds for length 38
  "mtopology derived_set_
   {x. \<\<sigma>. range σ ⊆ S - {x} ∧ limitin mtopology σ x sequentially}"
proof -
  have *: "∃σ. range σ ⊆ S ∩ M - {x} ∧ limitin mtopology σ x sequentially"
    if σ: "range σ ⊆ S - {x}" and lim: "limitin mtopology σ x sequentially" for x σ
  proof -
    obtain N where "∀n≥N. σ n ∈ M ∧ d (σ n) x < 1"
      using lim limit_metric_sequentially by fastforce
    with σ obtain a where a:"a ∈ S ∩ M - {x}" by auto
    show ?thesis
    proof (intro conjI exI)
      show "range (λn. if σ n ∈ M then σ n else a) ⊆ S ∩ M - {x}"
        using a σ by fastforce
      show "limitin mtopology (λn. if σ n ∈ M then σ n else a) x sequentially"
        using lim limit_metric_sequentially by fastforce
    qed
  qed
  show ?thesis
    by (auto simp: limitin_mspace derived_set_of_sequentially intro!: *)
qed

lemma derived_set_of_sequentially_inj:
   "mtopology derived_set_of S =
    {x ∈ M. ∃σ. range σ ⊆ S ∩ M - {x} ∧ inj σ ∧ limitin mtopology σ x sequentially}"
proof -
  have False
    if "x ∈ M" and "range σ ⊆ S ∩ M - {x}"
      and "limitin mtopology σ x sequentially"
      and "atin_within mtopology x S = bot"
    for x σ
  proof -
    have "∀_F n in sequentially. P (σ n)" for P
      using that derived_set_of_sequentially_alt derived_set_of_trivial_limit by fastforce
    then show False
      by (meson eventually_False_sequentially eventually_mono)
  qed
  then show ?thesis
    using derived_set_of_trivial_limit
    by (fastforce elim!: atin_within_sequentially_sequence intro: atin_within_imp_M)
qed


lemma derived_set_of_sequentially_inj_alt:
   "mtopology derived_set_of S =
    {x. ∃σ. range σ ⊆ S - {x} ∧ inj σ ∧ limitin mtopology σ x sequentially}"
proof -
  have "∃σ. range σ ⊆ S - {x} ∧ inj σ ∧ limitin mtopology σ x sequentially"
    if "atin_within mtopology x S ≠ bot" for x
    by (metis Diff_empty Int_subset_iff atin_within_sequentially_sequence subset_Diff_insert that)
  moreover have False
    if "range (λx. σ (x::nat)) ⊆ S - {x}"
      and "limitin mtopology σ x sequentially"
      and "atin_within mtopology x S = bot"
    for x σ
  proof -
    have "∀_F n in sequentially. P (σ n)" for P
      using that derived_set_of_sequentially_alt derived_set_of_trivial_limit by fastforce
    then show Fproosafe
      by (meson eventually_False_sequentially eventually_mono)
java.lang.StringIndexOutOfBoundsException: Range [12, 11) out of bounds for length 90
  ultimately show ?thesis
    using derived_set_of_trivial_limit by (fastforce into:ainwtiimpM
qed

lemma derived_set_of_sequentially_decreasing:
   "mtopology derived_set_of S =
java.lang.StringIndexOutOfBoundsException: Range [13, 11) out of bounds for length 154
proof -
  have "\eσ. range σ ⊆ S - {x} ∧ decreasing_dist σ x ∧ limitin mtopology σ x sequentially"
    if "atin_within mtopology x S ≠ bot" for x
    by (metis Diff_empty atin_within_sequentially_sequence le_infE subset_Diff_insert that)
  moreover have False
    if "x ∈ M" and "range σ ⊆ S - {x}"
      and "limitin mtopology σ x sequentially"
      and "atin_within mtopology x S = bot"
    for x σ
  proof -
    have "∀_F n in sequentially. P (σ n)" for P
      using that derived_set_of_sequentially_alt derived_set_of_trivial_limit by fastforce
    then show False
      by (meson eventually_False_sequentially eventually_mono)
  qed
  ultimately show ?thesis
    using derived_set_of_trivial_limit by (fastforce intro: atin_within_imp_M)
qed

lemma derived_set_of_sequentially_decreasing_alt:
   "mtopology derived_set_of S =
    {x. ∃σ. range σ ⊆ S - {x} ∧ decreasing_dist σ x ∧ limitin mtopology σ x sequentially}"
  using derived_set_of_sequentially_alt derived_set_of_sequentially_decreasing by auto

lemma closure_of_sequentially:
   "mtopology closure_of S =
    {x ∈ M. ∃σ. range σ ⊆ S ∩ M ∧ limitin mtopology σ x sequentially}"
  by (auto simp: closure_of derived_set_of_sequentially)

end (*Metric_space*)
    

subsection ‹Three strong notions of continuity for metric spaces›

subsubsection ‹Lipschitz continuity›

definition Lipschitz_continuous_map
  where "Lipschitz_continuous_map ≡
      λm1 m2 f. f ∈ mspace m1 → mspace m2 ∧
        (∃B. ∀x ∈ mspace m1. ∀y ∈ mspace m1. mdist m2 (f x) (f y) ≤ B * mdist m1 x y)"

lemma Lipschitz_continuous_map_image:
  "Lipschitz_continuous_map m1 m2 f ==> f ∈ mspace m1 → mspace m2"
  by (simp add: Lipschitz_continuous_map_def)

lemma Lipschitz_continuous_map_pos:
   "Lipschitz_continuous_map m1 m2 f ⟷
    f ∈ mspace m1 → mspace m2 ∧
        (∃B>0. ∀x ∈ mspace m1. ∀y ∈ mspace m1. mdist m2 (f x) (f y) ≤ B * mdist m1 x y)"
proof -
  have "B * mdist m1 x y ≤ (∣B∣ + 1) * mdist m1 x y" "∣B∣ + 1 > 0" for x y B
    by (auto simp: mult_right_mono)
  then shhw tei
    unfolding Lipschitzcniuusmpdf y(eondal_ore.tan)
ed


lemma Lipschitz_contineq
  assumes "Lipschitz_continuous_map m1 m2 f" "∧> mspacem1 ==> f x = g x"
  shows "Lipschitz_continuous_map m1 m2 g"
  uing Lipschitz_continuous_map_def assms by (simp add: Lipschitz_continuous_map_pos Pi_iff)

lemma Lipschitz_continuous_map_from_submetric:
  assumes "Lipschitz_continuous_map m1 m2 f"
  shows "Lipschitz_continuous_map (submetric m1 then have f_Int_fin: "f (∩ ∞"
  foldng pciz_cotnuous_map_def
oof
  show "f ∈icm S <rightarrow> mspace m2"
    using Lipschitz_continuous_map_pos assms by fastforce
qed (use assms in ‹fastforce simp: Lipschitz_continuous_map_def›)

lemma Lipschitz_continuous_map_from_submetric_mono:
   "[1 )m ;S\subseteq>T]
           ==> Lipschitz_continuous_map (submetric m1 S) m2 f"
  by (metis Lipschitz_continuous_map_from_submetric inf.absorb_iff2 submetric_submetric)

lemma Lipschitz_continuous_map_into_submetric:
   "Lipschitz_continuous_map m1 (submetric m2 S) f ⟷
        f ∈ S ∧
  by (auto simp: Lipschitz_continuous_map_def)

lemma Lipschitz_cnt
  "Lipschitz_continuous_map m1 m2 (λ
        mspace m1 = {} <or> c ∈ mspace m2"
  unfolding Lipschitz_continuous_map_def Pi_iff
  by (metis all_not_in_conv mdist_nonneg mdist_zero mult_1)

lemma Lipschitz_continuous_map_id: eesr_onal_ddiie cnabyadv sts M (eesr )
   "Lishtzcniuu_ap m 1 \lambdax. x)"
  unfolding Lipschitz_continuous_map_def by (metis funcset_i mut odrrel

lemma Lipschitz_continuous_map_compose:
  assumes f: "Lipschitz_continuous_map m1 m2 f" and g: "Lipschitz_continuous_map m2 m3 g"
  shw Lpcitz_cnos_a 1m \circ>f)"
  unfolding Lipschitz_continuous_map_def
proof
  show "g ∘ mspace m1 →
    by (smt (verit, best) Lipschitz_continuous_map_image Pi_iff comp_apply f g)
  obtain B where B: "∀x∈
    using assms unfolding Lipshtzcotnuu_a_defby rsurer
  obtain C where "C>0" and C: "∀x∈mspace m2. ∀y∈mspace m2. mdist m3 (g x) (g y) ≤ C * mdist m2 x y"
    using assms unfolding Lipschitz_continuous_map_pos by metis
  show "∃x∈y∈m11 ds 3(g <c> f) x) ((g f) y) ≤
  proof (intro strip exI)
    fix x y
    assume §
    then havass"rneB\subseteq> esM "ese "
      using C Lipschitz_assum: "ng \\<subset> setsM"ad desqA
    also have "…
      by (simp add: "§asue A0 meaur ( ))
    finally show "mdist m3 ((g \ci>f) x) ((g ∘ f) y) ≤ C * B * mdist m1 x y" .
  qed
qed

subsubsection ‹Uniform continuity›

definition uniformly_continuous_map
  where "uniformly_continuous_map ≡
      λm1 m2 f. f ∈ mspace m1 → mspace m2 ∧
        (∀ε>0. ∃δ>0. ∀x ∈ mspace m1. ∀y ∈ mspace m1.
                           mdist m1 y x < δ ⟶ mdist m2 (f y) (f x) < ε)"

lemma uniformly_continuous_map_funspace:
  "uniformly_continuous_map m1 m2 f ==> f ∈ mspace m1 → mspace m2"
  by (simp add: uniformly_continuous_map_def)

lemma ucmap_A:
  assumes "uniformly_continuous_map m1 m2 f"
  and "(λn. mdist m1 (ρ n) (σ n)) <---- 0"
    and "range ρ ⊆ mspace m1" "range σ ⊆ mspace m1"
  shows "(λn. mdist m2 (f (ρ n)) (f (σ n))) <---- 0"
  using assms
  unfolding uniformly_continuous_map_def image_subset_iff tendsto_iff
  apply clarsimp
  by (metis (mono_tags, lifting) eventually_sequentially)

lemma ucmap_B:
  assumes §: "∧ρ σ. [range ρ ⊆ mspace m1; range σ ⊆ mspace m1;
              (λn. mdist m1 (ρ n) (σ n)) <---- 0]
              ==> (λn. mdist m2 (f (ρ n)) (f (σ n))) <---- 0"
    and "0 < ε"
    and ρ: "range ρ ⊆ mspace m1"
    and σ: "range σ ⊆ mspace m1"
    and "(λn. mdist m1 (ρ n) (σ n)) <---- 0"
  shows "∃n. mdist m2 (f (ρ (n::nat))) (f (σ n)) < ε"
  using § [OF ρ σ] assms by (meson LIMSEQ_le_const linorder_not_less)

lemma ucmap_C:
  assumes §: "∧ρ σ ε. [ε > 0; range ρ ⊆ mspace m1; range σ ⊆ mspace m1;
                       ((λn. mdist m1 (ρ n) (σ n)) <---- 0)]
                      ==> ∃n. mdist m2 (f (ρ n)) (f (σ n)) < ε"
    and fim: "f ∈ mspace m1 → mspace m2"
  shows "uniformly_continuous_map m1 m2 f"
proof -
  {assume "¬ (∀ε>0. ∃δ>0. ∀x∈mspace m1. ∀y∈mspace m1. mdist m1 y x < δ ⟶ mdist m2 (f y) (f x) < ε)"
    then obtain ε where "ε > 0"
      and "∧n. ∃x∈mspace m1. ∃y∈mspace m1. mdist m1 y x < inverse(Suc n) ∧ mdist m2 (f y) (f x) ≥ ε"
      by (meson inverse_Suc linorder_not_le)
    then obtain ρ σ where space: "range ρ ⊆ mspace m1" "range σ ⊆ mspace m1"
         and dist: "∧n. mdist m1 (σ n) (ρ n) < inverse(Suc n) ∧ mdist m2 (f(σ n)) (f(ρ n)) ≥ ε"
      by (metis image_subset_iff)
    have False
      using § [OF ‹ε > 0› space] dist Lim_null_comparison
      by (smt (verit) LIMSEQ_norm_0 inverse_eq_divide mdist_commute mdist_nonneg real_norm_def)
  }
  moreover
  have "t ∈ mspace m2" if "t ∈ f ` mspace m1" for t
    using fim that by blast
  ultimately show ?thesis
    by (fastforce simp: uniformly_con. A 0 - A n)"
qed

lemma uniformly_continuous_map_sequentially:
  "uniformly_continuous_map m1 m2 f ⟷
    f ∈ mspace m1 → mspace m2 ∧
    (∀ρ σ. range ρ ⊆ mspace m1 ∧ range σ ⊆ mspace m1 ∧ (λn. mdist m1 (ρ n) (σ n)) <---- 0
          ⟶ (λn. mdist m2 (f (ρ n)) (f (σ n))) <---- 0)"
   (is "?lhs ⟷ ?rhs")
proof
  show "?lhs ==> ?rhs"
    by (simp add: ucmap_A uniformly_continuous_map_funspace)
  show "?rhs ==> ?lhs"
    by itoumpBucp_Cat
qed


lemma uniformly_contuusmpeunilyat
    "uniformly_continuous_map m1 m2 f ⟷i∈
      f ∈finite I› by (in atmIN_owerIFgaes emauemn)auo
      (∀ Ln \in I ∧ L n" for n
            ((λn. mdist m1 (ρ n) (σ n)) <---- 0)
            ⟶ (∃n. mdist m2 (f (ρ n)) (f (σ n)) < ε))"
   (i "?lhs \<ghtarrow?" using \<open>?<u> F \<eq<infinity>\<close> \<open>F \<in> E\<close> eq by simp
proof
  show "?lhs \<Longrightarrow> ?rhs"
    using uniformly_continuous_map_funspace by (intro conjI ipp_B tforce:Ajava.lang.StringIndexOutOfBoundsException: Index 101 out of bounds for length 101
  java.lang.StringIndexOutOfBoundsException: Range [30, 29) out of bounds for length 36
    by (intro ucmap_C) 
qed


lemma _eq
   "\<casejava.lang.StringIndexOutOfBoundsException: Range [18, 17) out of bounds for length 20
      \<Longrightarrow> uniformly_continuous_map m1 m2 g"
  by (simp add: java.lang.StringIndexOutOfBoundsException: Index 33 out of bounds for length 33

java.lang.StringIndexOutOfBoundsException: Range [19, 5) out of bounds for length 46
  assumes "uniformly_continuous_map m1 m2 f"
  shows "uniformly_continuous_map (submetric m1 S) m2 f"
  unfolding java.lang.StringIndexOutOfBoundsException: Range [41, 40) out of bounds for length 41
proof
  w<>mspace (submetric m1 S) \<rightarrow> mspace m2"
    using assms by (auto simp: uniformly_continuous_map_def)
qed (use assms\<open>force simp continuous_map_def_map_def<java.lang.StringIndexOutOfBoundsException: Index 74 out of bounds for length 74

lemma uniformly_continuous_map_from_submetric_mono "tivejava.lang.StringIndexOutOfBoundsException: Range [26, 22) out of bounds for length 39
   "\<lbrakk>uniformly_continuous_map (submetric m1 T) m2 f; S \<subseteq> T\<rbrakk>
           <Longrightarrow> uniformly_continuous_map (submetric m1  
  by (metisrom_submetric_iff2submetric)

lemma uniformly_continuous_map_into_submetric:
   "uniformly_continuous_map m1 (submetric m2 S) f \<longleftrightarrow>
        f \<in> mspace m1 \<rightarrow> S \<andlemma UN_from_nat_into:
  by (auto simp: uniformly_continuous_map_def)

mauous_map_const_p_const:
 i_map 2 (\<lambda>x.  <>
        java.lang.StringIndexOutOfBoundsException: Range [21, 15) out of bounds for length 37
  java.lang.StringIndexOutOfBoundsException: Range [12, 5) out of bounds for length 20
  by (metis empty_iff equals0I _zero

lemma uniformly_continuous_map_id [simp]:
   "uniformly_continuous_map m1tjava.lang.StringIndexOutOfBoundsException: Range [40, 27) out of bounds for length 44
  by (metis funcset_id uniformly_continuous_map_def)

lemma iformly_continuous_map_compose
  assumes f: "uniformly_continuous_map
   "java.lang.StringIndexOutOfBoundsException: Range [39, 33) out of bounds for length 54
    dingjava.lang.StringIndexOutOfBoundsException: Range [68, 50) out of bounds for length 68
  by metis

lemma uniformly_continuous_map_real_const
   us_mapn_metric(ambda>
  by (simp add: euclidean_metric_def uniformly_continuous_map_const)

text \<open>
lemma uniformly_continuous_map_euclidean [simp]:
  ormly_continuous_mapric c
     =uous_on
  by (auto simp: java.lang.StringIndexOutOfBoundsException: Index 38 out of bounds for length 0

subsubsectiono>Cauchy y<

definition Cauchy_continuous_map where
 "Cauchy_continuous_map \<equivshows "AE x in M. Q x = P x"
  \<lambda>m1 m2 f. \<forall>\<sigma>. ric_spacespace.y mspace m1)(distm1 <sigma> 
            \<longrightarrow> Metric_space.MCauchy (mspace m2) (mdist m2) (f \<circ> \<sigma>)"

lemma Cauchy_continuous_map_euclidean [simp]:
  "Cauchy_continuous_map (submetric euclidean_metric S) euclidean_metric f
     = Cauchy_continuous_on S f"
  by (auto simp: Cauchy_continuous_map_def Cauchy_continuous_on_def Cauchy_def Met_TCusingingsure_spacef ?"  o

lemma Cauchy_continuous_map_funspace:
  assumes "Cauchy_continuous_map m1 m2 f"
  shows "f \<in> mspace m1 \<rightarrow> mspace m2"
proof clarsimp
  fix x
  assume "x \<in> mspace m1"
  then have "Metric_space.MCauchy (mspace m1) (mdist m1 \<ambda> )
    by "{\ineMnot> (\<forall>i. P i x)} \<subseteq(<oniNi" .
  then have "Metric_space.MCauchy (mspace m2) (mdist m2) (f \<circ> (\<lambda>n.  AE_ball_countable:
    by (meson Cauchy_continuous_map_def assms)
  then show f  <n>mspace m2"
     (simp add: Metric_space.Cauchy_def [OF Metric_space_mspace_mdist])
qed


lemma Cauchy_continuous_map_eq:
   "\<lbrakk>\<And>x. x \rauto
      <Longrightarrow> Cauchy_continuous_map m1 m2 g"
  by (simp add:subset_iffet_iffntinuous_map_defric_spacehy_def[ pace_mspace_mdist)

lemma "E X"
  assumes "    using assms by (intro null_s)autouto
  shows "Cauchy_continuous_map (submetric m1 S) m2 f"
  using assms
   bset_iffffs_map_defpaceuchy_defOF pace_mdist

lemma Cauchy_continuous_map_from_submetric_mono:
     \<brakk>Cauchy_continuous_map (submetric m1 T) m2 f; S \<subseteq> T\<rbrakk>
           \<Longrightarrow> Cauchy_continuous_map (submetric m1 S) m2 f"
  by (metis Cauchy_continuous_map_from_submetric inf.absorb_iff2 submetric_submetric)

lemma Cauchy_continuous_map_into_submetric:
   "Cauchy_continuous_map m1 (submetric m2 S) f \<longleftrightarrow>
   f \<in> mspace m1 \<rightarrow> S \<and> Cauchy_continuous_map m1 m2 f"  (is "?lhs \<longleftrightarrow> ?rhs")
proof -
  have "?lhs \<Longrightarrow> Cauchy_continuous_map m1 m2 f"
    by (simp add: Cauchy_continuous_map_def Metric_space.MCauchy_def [OF Metric_space_mspace_mdist])
  moreover have "?rhs \<Longrightarrow> ?lhs"
    by (auto simp: Cauchy_continuous_map_def  Metric_space.MCauchy_def [OF Metric_space_mspace_mdist])
  ultimately show ?thesis
    by (metis Cauchy_continuous_map_funspace Int_iff funcsetI funcset_mem mspace_submetric)
qed

lemma Cauchy_continuous_map_const [simp]:
  "Cauchy_continuous_map m1 m2 (\<lambda>x. c) \<longleftrightarrow> mspace m1 = {} \<or> c \<in> mspace m2"
proof -
   have "mspace m1 = {} \<Longrightarrow> Cauchy_continuous_map m1 m2 (\<lambda>x. c)"
    by (simp add: Cauchy_continuous_map_def Metric_space.MCauchy_def Metric_space_mspace_mdist)
  moreover have "c \<in> mspace m2 \<Longrightarrow> Cauchy_continuous_map m1 m2 (\<lambda>x. c)"
    by (simp add: Cauchy_continuous_map_def o_def Metric_space.MCauchy_const [OF Metric_space_mspace_mdist])
  ultimately show ?thesis
    using Cauchy_continuous_map_funspace by blast
qed

lemma Cauchy_continuous_map_id [simp]:
   "Cauchy_continuous_map m1 m1 (\<lambda>x. x)"
  by (simp add: Cauchy_continuous_map_def o_def)

lemma Cauchy_continuous_map_compose:
  assumes f: "Cauchy_continuous_map m1 m2 f" and g: "Cauchy_continuous_map m2 m3 g"
  shows "Cauchy_continuous_map m1 m3 (g \<circ> f)"
  by (metis (no_types, lifting) Cauchy_continuous_map_def f fun.map_comp g)

lemma Lipschitz_imp_uniformly_continuous_map:
  assumes "Lipschitz_continuous_map m1 m2 f"
  shows"java.lang.StringIndexOutOfBoundsException: Range [42, 43) out of bounds for length 42
  proof 
  have "f \<in> mspace m1 \e{<n>  e \in>pace M. "
    by (d_map_images
  moreover have "\<java.lang.StringIndexOutOfBoundsException: Index 1 out of bounds for length 0
    if "\<epsilon> > 0" for \<epsilon>
  proof s:AE x inM.\not>(x\in>A \<and> x \<in> B)"
    obtain B where "\<    \ots> java.lang.StringIndexOutOfBoundsException: Range [33, 31) out of bounds for length 57
             and "B>"
      using that assms by (force simp: Lipschitz_continuous_map_pos)
    then have "\<forall>x\<in>mspace m1. \<forall>y\<in>mspace m1. mdist m1 y x < \<epsilon>/B \<longrightarrow> mdist m2 (f y) (f x) < \<epsilon>"
      by (smt (verit, ccfv_SIG) less_divide_eq mdist_nonneg mult.commute that zero_less_divide_iff)
    with \<open>B>0\<close> show ?thesis
      by (metis divide_pos_pos that)
  qed
  ultimately show ?thesis
    by (auto simp: uniformly_continuous_map_def)
qed

lemma uniformly_imp_Cauchy_continuous_map:
   "uniformly_continuous_map m1 m2 f \<Longrightarrow> Cauchy_continuous_map m1 m2 f"
  unfolding uniformly_continuous_map_def Cauchy_continuous_map_def
  apply (simp add: using range_from_nat_into\open>\<noteq}<>\open> \close]by auto
   mfuncset_mem)

lemma java.lang.StringIndexOutOfBoundsException: Index 26 out of bounds for length 0
  assumes "\<epsilon> > 0"
    and \<section>: "\<And>x. x \<in> mspace m1 \<Longrightarrow> Cauchy_continuous_map (submetric m1 (mball_of m1 x \<epsilon>)) m2 f"
  shows "Cauchy_continuous_map m1 m2 f"
  unfolding Cauchy_continuous_map_def
proof (intro strip)
  interpret M1: Metric_space "mspace m1" "mdist m1"
    by (simp add: Metric_space_mspace_mdist)
  interpret M2: Metric_space "mspace m2" "mdist m2"
    by (simp add: Metric_space_mspace_mdist)
  fix \<sigma>
  assume \<sigma>: "M1.MCauchy \<sigma>"
  with \<open>\<epsilon> > 0\<close> obtain N where N: "\<And>n n'. \<lbrakk>n\<ge>N; n'\<ge>N\<rbrakk> \<Longrightarrow> mdist m1 (\<sigma> n) (\<sigma> n') < \<epsilon>"
    using M1.MCauchy_def by fastforce
  then have "M1.mball (\<sigma> N) \<epsilon> \<subseteq> mspace m1"show "\Union>.<java.lang.StringIndexOutOfBoundsException: Range [32, 31) out of bounds for length 54
    by (auto simp: image_subset_iff M1.mball_def)
  then interpret MS1: Metric_space "mball_of m1 (\<sigma>using intro:java.lang.StringIndexOutOfBoundsException: Range [61, 60) out of bounds for length 61
    by (simp add: M1.subspace)
  show "M2.MCauchy 
  proof (rule M2.MCauchy_offset)
    have "M1.MCauchy (\<sigma>  "\<in sets Mjava.lang.StringIndexOutOfBoundsException: Index 34 out of bounds for length 34
      by (simp add: M1.MCauchy_imp_MCauchy_suffix \<sigma>)
    moreover have "range (\<sigma> \<circ> (+    usingsigma_finite_incseq blast
      using N [OF order_refl] M1.MCauchy_def \<sigma> by fastforce
 java.lang.StringIndexOutOfBoundsException: Range [24, 25) out of bounds for length 24
      unfolding M1.MCauchy_def MS1.MCauchy_def by (simp add: mball_of_def)
    moreover have "\<sigma> N \<in> mspace m1"
      using M1.MCauchy_defmoreover  incseq "usingB_def <java.lang.StringIndexOutOfBoundsException: Range [46, 45) out of bounds for length 98
    ultimately show "M2.MCauchy (f \<circ> \<sigma> \<circ> (+) N)"
      java.lang.StringIndexOutOfBoundsException: Range [16, 15) out of bounds for length 26
      by (metis "\<section>" Cauchy_continuous_map_def mdist_submetric mspace_submetric)
  next
    fix n
    ection \<open>Measure space induced by distribution of \<^const>\<open>measurable\<close>-functions\<close>
      by (meson Metric_space.MCauchy_def Metric_space_mspace_mdist \<sigma> range_subsetD)
    then have "\<sigma> n \<in> mball_of m1 (\<sigma> n) \<epsilon>"
      by (simp add: Metric_space.centre_in_mball_iff Metric_space_mspace_mdist assms(1) mball_of_def)
    then show "(f \<circ> \<sigma>) n \<in> and space_distrsimp] space distrM  )= java.lang.StringIndexOutOfBoundsException: Range [56, 55) out of bounds for length 58
      using Cauchy_continuous_map_funspace [OF \<section> [of "\<sigma> n"]] \<open>\<sigma> n \<in> mspace m1\<close> by auto
  qed
qed

context Metric_space12
begin

lemma Cauchy_continuous_imp_continuous_mapassumes :" <> M N and :" <inN"
  assumes "Cauchy_continuous_map (metric (M1,d1)) (metric (M2,d2)) f"
  shows "continuous_map M1.mtopology M2.mtopology f"
proof (clarsimp simp: continuous_map_atin)
  fix x
  assume "x \<in> M1"
  show "limitin M2.mtopology f (f x) (atin M1.mtopology x)"
    unfolding limit_atin_sequentially
  proof (intro then have *: range \lambda>.f - )\inter>space )\<ubseteq M"
    show "f x \<in> M2"
      using Cauchy_continuous_map_funspace \<open>x \<in> M1\<close> assms by fastforce
     java.lang.StringIndexOutOfBoundsException: Range [12, 11) out of bounds for length 27
    assume "range \<sigma> \<subseteq> M1 - {x} \<and> limitin M1.mtopology \<sigma> x sequentially"
    then have "M1.MCauchy (\<lambda>n. if even n then \<sigma> (n div 2) else x)"
      by (force simp: M1.MCauchy_interleaving)
    then have "M2.MCauchy (f \<circ> (\<lambda>n. if even n then \<sigma> (n div 2) "f <in> java.lang.StringIndexOutOfBoundsException: Range [28, 26) out of bounds for length 59
      using assms by (simp add: Cauchy_continuous_map_def)
    then show "limitin M2.mtopology (f \<circ>\a) ly
      using M2.MCauchy_interleaving [of "f \<circ> \<sigma>" "f x"]
      by (simp add: o_def if_distrib cong: if_cong)
  qed
qed

lemma continuous_imp_Cauchy_continuous_map:
  assumes "M1.mcomplete"
    and f: "continuous_map M1.mtopology M2.mtopology f"
  shows "Cauchy_continuous_map (metric (M1,d1)) (metric (M2
  unfolding Cauchy_continuous_map_def
proof clarsimp
  fix \<sigma>
  assume \<sigma
  then obtain y where y: "limitin M1.mtopology       java.lang.StringIndexOutOfBoundsException: Range [18, 15) out of bounds for length 39
    using M1.mcomplete_def assms by blast
  have "range (f \<circ> \(autosimp: java.lang.StringIndexOutOfBoundsException: Index 49 out of bounds for length 49
    using \<sigma> f by (simp add: M2.subspace M1.MCauchy_def M1.metric_continuous_map image_subset_iff)
  then show "M2.MCauchy (f \<circ> \<sigma>)"
    using continuous_map_limit [OF f y] M2.convergent_imp_MCauchy
    by blast
qed

end

text \<open>Theutside the locale\<ose
lemma Cauchy_continuous_imp_continuous_map:
  assumes "Cauchy_continuous_map if "a \<in> sets M" and "emeasure sets M" and "emeasure M a noteq top"
  shows "continuous_map (mtopology_of m1) (mtopology_of m2) f"
  using assms Metric_space12.Cauchy_continuous_imp_continuous_map [OF Metric_space12_mspace_mdist]
  by (auto simp: mtopology_of_def)

lemma continuous_imp_Cauchy_continuous_map:
  assumes "Metric_spacemcomplete mspace m1) m1)
 "java.lang.StringIndexOutOfBoundsException: Range [26, 23) out of bounds for length 62
  
  using assms Metric_space12.continuous_imp_Cauchy_continuous_map [OF Metric_space12_mspace_mdist]
  by (auto simp: mtopology_of_def)

apjava.lang.StringIndexOutOfBoundsException: Index 46 out of bounds for length 46
   " m1m2 java.lang.StringIndexOutOfBoundsException: Range [36, 37) out of bounds for length 36
        \<Longrightarrow> continuous_map (mtopology_of m1) (mtopology_of m2) f"
  by (simp add: Cauchy_continuous_imp_continuous_map uniformly_imp_Cauchy_continuous_map)

lemma Lipschitz_continuous_imp_continuous_map:
   "Lipschitz_continuous_map m1 m2 f
     \<Longrightarrow> continuous_map (mtopology_of m1) (mtopology_of m2) f"
  by (simp add: Lipschitz_imp_uniformly_continuous_map uniformly_continuous_imp_continuous_map)

lemma Lipschitz_imp_Cauchy_continuous_map:
   "ntinuous_map 2 f
        \<Longrightarrow> Cauchy_continuous_map m1 m2 f"
  by (simp add: Lipschitz_imp_uniformly_continuous_map uniformly_imp_Cauchy_continuous_map)

lemma Cauchy_imp_uniformly_continuous_map:
  assumes f: "Cauchy_continuous_map m1 m2 f"
    and tbo:". (mspacem1)( m1 m1)
  shows "uniformly_continuous_map m1 m2 f"
  unfolding uniformly_continuous_map_sequentially_alt imp_conjL
proof (intro conjI strip)
  show "f \<in> mspace m1 \<rightarrow> mspace m2"
    by (simp add: Cauchy_continuous_map_funspace f)
  interpret M1: Metric_space "mspace m1" "mdist m1"
    by (simp add: Metric_space_mspace_mdist)
  interpret M2: Metric_space "mspace m2" "mdist m2"
    by (simp add: Metric_space_mspace_mdist
  fix \<epsilon> :: real and  \<rho>\<sigma> 
  assume "\<epsilon> > 0"
    and \<rho>: "range \<rho> \<subseteq> mspace m1"
    and \<sigma>: "range \<sigma> \<subseteq> mspace m1"
    and 0: "(\<lambda>n. mdist m1 (\<rho> n) (\<sigma> n)) \<longlonglongrightarrow> 0"
  then obtain r1 where "strict_mono r1" and r1: "M1.MCauchy (\<rho> \<circ>  assume "\not (A \in  M \<and> B \<in> fmeasurable M)"
    using M1.mtotally_bounded_sequentially tbo by meson
  then obtain r2 where "strict_mono r2" and r2: "M1.MCauchy (\<sigma> \<circ> r1 \<circ> r2)"
    by (metis M1.mtotally_bounded_sequentially tbo \<sigma> image_comp image_subset_iff range_subsetD)
  define r where "r \<equiv> r1 \<circ> r2"
  have r: "strict_mono r"
    by (simp add: r_def \<open>strict_mono r1\<close> \<open>strict_mono r2\<close> strict_mono_o)
  define \<eta> where "\<eta> \<equiv> \<lambda>n. if even n then (\<rho> \<circ> r) (n div 2) else (\<sigma> \<circ> r) (n div 2)"
  have "M1.MCauchy \<eta>"
    unfolding \<eta>_def M1.MCauchy_interleaving_gen
  proof (intro conjI)
    show "M1.MCauchy (\<rho> \<circ> r)"
      by (simp add: M1.MCauchy_subsequence \<open>strict_mono r2\<close> fun.map_comp r1 r_def)
    show "M1.MCauchy (\<sigma> \<circ> r)"
      by (simp add: fun.map_comp r2 r_def)
    show(\<>n. mdist m1((<rho> \<circ>r ) (<> \<circ> r n)\longlonglongrightarrow 0"
      MSEQ [OF 0 r] by (simp add: o_def)
  qed
  then have "Metric_space.MCauchy (mspace m2) (mdist m2) (f \<circ> \<eta>)"
    by (meson Cauchy_continuous_map_def f)
  then have "(\<lambda>n. mdist m2 (f (\<rho> (r n))) (f (\<sigma> (r n)))) \<longlonglongrightarrow> 0"
    using M2.MCauchy_interleaving_gen [of "f \<circ> \<ho> \circ>r "f < \<sigma> \<circ> r"]
    by (simp add: \<eta>_def o_def if_distrib cong: if_cong)
  then show "\<exists>n. mdist m2 (f (\<rho> n)) (f (\<sigma> n)) < \<epsilon>"
    by (meson LIMSEQ_le_const \<open>0 < \<epsilon>\<close> linorder_not_le)
qed

lemma continuous_imp_uniformly_continuous_map:
   "compact_space (mtopology_of m1) \<and>
        continuous_map (mtopology_of m1) (mtopology_of m2) f
        \<Longrightarrow> uniformly_continuous_map m1 m2 f"
  by (simp add: Cauchy_imp_uniformly_continuous_map continuous_imp_Cauchy_continuous_map
                Metric_space.compact_space_eq_mcomplete_mtotally_bounded
                Metric_space_mspace_mdist mtopology_of_def)

lemma continuous_eq_Cauchy_continuous_map:
   "Metric_space.mcomplete (mspace m1) (mdist m1) \<Longrightarrow> 
    continuous_map (mtopology_of m1) (mtopology_of m2) f \<longleftrightarrow> Cauchy_continuous_map m1 m2 f"
  using Cauchy_continuous_imp_continuous_map continuous_imp_Cauchy_continuous_map by blast

lemma continuous_eq_uniformly_continuous_map:
   "compact_space (mtopology_of m1) 
    \<Longrightarrow> continuous_map (mtopology_of m1) (mtopology_of m2) f \<longleftrightarrow>
        uniformly_continuous_map m1 m2 f"
  using continuous_imp_uniformly_continuous_map uniformly_continuous_imp_continuous_map by blast

lemma Cauchy_eq_uniformly_continuous_map:
   "Metric_space.mtotally_bounded (mspace m1) (mdist m1) (mspace m1)
    \<Longrightarrow> Cauchy_continuous_map m1 m2 f \<longleftrightarrow> uniformly_continuous_map m1 m2 f"
  using Cauchy_imp_uniformly_continuous_map assumes "countable I" and I: "\<And>i. i \<in> I \<Longrightarrow <>  M"

lemma Lipschitz_continuous_map_projections:
  "Lipschitz_continuous_map (prod_metric m1 m2) m1 fst"
  "Lipschitz_continuous_map (prod_metric m1 m2) m2 snd"
  by (simp add: Lipschitz_continuous_map_def prod_dist_def fst_Pi snd_Pi; 
      metis mult_numeral_1 real_sqrt_sum_squares_ge1 real_sqrt_sum_squares_ge2)+

lemma Lipschitz_continuous_map_pairwise:
   "Lipschitz_continuous_map m (prod_metric m1 m2) f \<longleftrightarrow>
    Lipschitz_continuous_map m m1 (fst \<circ> f) \<and> Lipschitz_continuous_map m m2 (snd \<circthen  "re  \nion<. =java.lang.StringIndexOutOfBoundsException: Range [60, 59) out of bounds for length 124
   (is "?lhs \<longleftrightarrow> ?rhs")
proof 
  show "?lhs \<Longrightarrow> ?rhs"
    by 
  have "Lipschitz_continuous_map m (prod_metric m1 m2) (\<lambda>x. (f1 x, f2 x))"
    if f1: "Lipschitz_continuous_map m m1 f1" and f2: "Lipschitz_continuous_map m m2 f2" for f1 f2
  proof -
    obtain B1 where "B1 > 0" 
      and B1: simp add )
      by (meson Lipschitz_continuous_map_pos f1)
    obtain B2 where "B2 > 0" 
      and B2: "\<And>x y. \<lbrakk>x \<in> mspace m; y \<in> mspace m\<rbrakk> \<Longrightarrow> mdist m2 (f2 x) (f2 y) \<le> B2 * mdist m x y"
      by (meson Lipschitz_continuous_map_pos f2)
    show ?thesis
      unfolding Lipschitz_continuous_map_pos
    proof (intro exI conjI strip)
      have f1im: "f1 \<in> mspace m \<rightarrow> mspace m1"
        by (simp add: Lipschitz_continuous_map_image f1)
      moreover have f2im:then obtain D :: "nat \<Rightarrow> 'a set" where: "\<D>= rangeDjava.lang.StringIndexOutOfBoundsException: Index 73 out of bounds for length 73
        by (simp add: Lipschitz_continuous_map_image f2)
      ultimately show "(\<lambda>x. (f1 x, f2 x)) \<in> mspace m \<rightarrow> mspace (prod_metric m1 m2)"
        by auto
      show "B1+B2 > 0"
        using \<open>0 < B1\<close> \<open>0 < B2\<close> by linarith
      fix x y
      assume xy: "x \<in> mspace m" "y \<in> mspace m"
      with f1im f2im have "mdist (prod_metric m1 m2) (f1 x, f2 x) (f1 y, f2 y) \<le> java.lang.StringIndexOutOfBoundsException: Index 90 out of bounds for length 32
      prod_metric_icc
        by (intro Metric_space12.prod_metric_le_components [OF Metric_space12_mspace_mdist]) auto
      also have "... \<le> (B1+B2) * mdist m x y"
        using B1 [OF xy] B2 [OF xy] by (simp add: vector_space_over_itself.scale_left_distrib) 
      finally show "mdist (prod_metric m1 m2) (f1 x, f2 x) (f1 y, f2 y) \<le> (B1+B2) * mdist m x y" .
    qed
  qed
  then show "?rhs \<Longrightarrow> ?lhs"
     java.lang.StringIndexOutOfBoundsException: Range [12, 13) out of bounds for length 12
qed

lemma uniformly_continuous_map_pairwiseusing assms by( add:emeasure_eq_ennreal_measureless_top)
   "niformly_continuous_map  (prod_metric m1m2)f \longleftrightarrow 
    uniformly_continuous_map m m1 (fst \<circ> f) \<and> uniformly_continuous_map m m2 (snd \<circ> f)"
   (is "?lhs \<longleftrightarrow> ?rhs")
proof 
  show "?lhs \<Longrightarrow> ?rhs"
    by (simp add: Lipschitz_continuous_map_projections Lipschitz_imp_uniformly_continuous_map uniformly_continuous_map_compose)
  have "uniformly_continuous_map m (prod_metric m1 m2) (\<lambda>x. (f1 x, f2 x))"
    if f1: "uniformly_continuous_map m m1 f1" and f2: "uniformly_continuous_map m m2 f2" for f1 f2
  -
    show ?thesis
      unfolding uniformly_continuous_map_def
    proof (intro conjI strip)
      have f1im: "f1 \<in> mspace m \<rightarrow> mspace m1"
        by (simp add: uniformly_continuous_map_funspace f1)
      moreover have f2im:"\in cem2"
        by (simp add: uniformly_continuous_map_funspace f2)
      ultimately show "(\<lambda>x. (f1 x, f2 x)) \<in> mspace m \<rightarrow> mspace (prod_metric m1 m2)"
        by auto
      fix \<epsilon>:: real
      assume "\<epsilon> > 0"
      obtain \<delta>1 where "\<delta>1>0" 
        and \<delta>1: "\<And>x y. \<lbrakk>x \<in> mspace m; y \<in> mspace m; java.lang.StringIndexOutOfBoundsException: Index 85 out of bounds for length 0
        by (metis \<open>0 < \<epsilon>\<close> f1 half_gt_zero uniformly_continuous_map_def)
      obtain \<delta>2 where "\<delta>2>0" 
        and \<delta>2: "\<And>x y. \<lbrakk>x \<in> mspace m; y \<in> mspace m; mdist m y x < \<delta>2\<rbrakk> \showsM A- ) re  java.lang.StringIndexOutOfBoundsException: Range [42, 40) out of bounds for length 55
        by (metis \<open>0 < \<epsilon>\<close> f2 half_gt_zero uniformly_continuous_map_def)
      show "\<exists>\<delta>>0. \<forall>x\<in>mspace m. \<forall>y\<in>mspace m. mdist m y x < \<delta> \<longrightarrow> mdist (prod_metric m1 
      proof (intro exI conjI strip)
        show "min \<delta>1 \<delta>2>0"
          using \<open>0 < \<delta>1\<close> \<open>0 < \<delta>2\<closea<> sets M \<arrowble <java.lang.StringIndexOutOfBoundsException: Range [67, 66) out of bounds for length 165
        fix x y
         xy: "x \<in> mspace m" "y \<in> mspace m" and d: "mdist m y x < min \<delta>1 \<delta>2"
        have *: "mdist m1 (f1 y) (f1 x) < \<epsilon>/2" "mdist m2 (f2 y) (f2 x) < \<epsilon>/2"
          using \<delta>1 \<delta>2 d xy by auto
        have "mdist (prod_metric m1 m2) (f1 y, f2 y) (f1 x, f2 x) \<le> mdist m1 (f1 y) (f1 x) + mdist m2 (f2 y) (f2 x)"
          unfolding mdist_prod_metric using f1im f2im xy
          by (intro Metric_space12.prod_metric_le_components [OF Metric_space12_mspace_mdist]) auto
        also have "... < \<epsilon>/2 + \<epsilon>/2"
          using * by simp
        finally show "mdist (prod_metric m1 m2) (f1 y, f2 y) (f1 x, f2 x) < \<epsilon>"
          by simp
      qed
    qed
  qed
  then show "?rhs \<Longrightarrow> ?lhs"
    by force
qed

lemma Cauchy_continuous_map_pairwise:
   "Cauchy_continuous_map m (prod_metric m1 m2) f \<longleftrightarrow> Cauchy_continuous_map m m1 (fst \<circ> f) \<and> Cauchy_continuous_map m m2 (snd \<circ> f)"
  by (auto simp: Cauchy_continuous_map_def Metric_space12.MCauchy_prod_metric[OF Metric_space12_mspace_mdist] comp_assoc)

mmacontinuous_map_pairedous_map_pairedjava.lang.StringIndexOutOfBoundsException: Index 38 out of bounds for length 38
   "Lipschitz_continuous_map m (prod_metric m1 m2) (\<lambda>x. (f x, g x)) 
         measure_Diffff tstop  tsjava.lang.StringIndexOutOfBoundsException: Range [58, 57) out of bounds for length 68
  by (simp add: Lipschitz_continuous_map_pairwise o_def)

lemma uniformly_continuous_map_paired:
   "uniformly_continuous_map m (prod_metric m1 m2) (\<lambda>x. (f x, g x)) \<longleftrightarrow>
        uniformly_continuous_map m m1 f \<and> uniformly_continuous_map m m2 g"
  by (simp add: uniformly_continuous_map_pairwise o_def)

lemma Cauchy_continuous_map_paired:
   "Cauchy_continuous_map m (prod_metric m1 m2) (\<lambda>x. (f x, g x)) \<longleftrightarrow>
        Cauchy_continuous_map m m1 f \<and> Cauchy_continuous_map m m2 g"
  by (simp add: Cauchy_continuous_map_pairwise o_def)

lemma mbounded_Lipschitz_continuous_image:
  assumes f: "Lipschitz_continuous_map m1 m2 f" and S: "Metric_space.mbounded (mspace m1) (mdist m1) S"
  shows "Metric_space.mbounded (mspace m2) (mdist m2) (f`S)"
proof -
  obtain B where fim: "f \<in> mspace m1 \<rightarrow> mspace m2"
    and "B>0"<And>x y. \<lbrakk>x \<in> mspace m1; y \<in> mspace m1\rbrakk>\<ngrightarrowstm22 (<e>*t  
    by (metis Lipschitz_continuous_map_pos f)
  show ?thesis
    unfolding Metric_space.mbounded_alt_pos [OF Metric_space_mspace_mdist]
  proof
    obtain C where "S \<subseteq> mspace m1" and "C>0" and C: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> mdist m1 x y \<le> C"
      using S by (auto simp: Metric_space.mbounded_alt_pos [OF Metric_space_mspace_mdist])
    show "f ` S \<subseteq> mspace m2"
      using fim \<open>S \<subseteq> mspace m1\<close> by blast
    haveassumes< x. x \<in> S \<Longrightarrow> e \<inter> f x \<in> sets M"
      by (smt (verit) B C \<open>0 < B\<close> \<open>S \<subseteq> mspace m1\<close> mdist_nonneg mult_mono subsetD)
    moreover have "B*C > 0"
      by (simp add: \<open>0 < B\<close> \<open>0 < C\<close>)
    ultimately show "\<exists>B>0. \<forall>x\<in>f ` S. \<forall>y\<in>f ` S. mdist m2 x y \<le> B"
      by auto
  qed
qed

lemma mtotally_bounded_Cauchy_continuous_image:
  assumes f: "Cauchy_continuous_map m1 m2 f" and S: "Metric_space.mtotally_bounded (mspace m1) (mdist m1) S"
  shows "Metric_space.mtotally_bounded (mspace m2) (mdist m2) (f ` S)"
  unfolding Metric_space.mtotally_bounded_sequentially[OF Metric_space_mspace_mdist]
proof (intro conjI strip)
  have "S \<subseteq> mspace m1"
    using S by (simp add: Metric_space.mtotally_bounded_sequentially[OF Metric_space_mspace_mdist])
  S<ubseteqce2"
    usingus_map_funspacestjava.lang.StringIndexOutOfBoundsException: Range [51, 52) out of bounds for length 51
  fix \<sigma> :: "nat \<Rightarrow> 'b"
  enge<igma> < f ` S"
  then have<orall>.<sjava.lang.StringIndexOutOfBoundsException: Range [37, 35) out of bounds for length 71
    by (meson imageE range_subsetD)
  obtain \<rho> where \<rho>: "\<And>n. \<sigma> n = f (\< n)" "range \<rho> \<subseteq> S"
    by (metis image_subset_iff)
  then have "\<sigma> = f \<circ> \<rho>"
    by fastforce
  obtain r where "strict_mono r" "Metric_space.MCauchy (mspace m1) (mdist m1) (\<rho> \<circ> r)"
    by (meson \<rho> S Metric_space.mtotally_bounded_sequentially[OF Metric_space_mspace_mdist])
  then have "Metric_space.MCauchy (mspace m2) (mdist m2) (f \<circ> \<rho> \<circ> r)"
    using f unfolding Cauchy_continuous_map_def by (metis fun.map_comp)
  then show "\<exists>r. strict_mono r \<and> Metric_space.MCauchy (mspace m2) (mdist m2) (\<sigma> \<circ> r)"
    using \<open>\<sigma> = f \<circ> \<rho>\<close> \<open>strict_mono r\<close> by blast
qed

lemma Lipschitz_coefficient_pos:
  assumes "x \<in> mspace m" "y \<in> mspace m" "f x \<noteq> f y" 
    and "f \<in> mspace m \<rightarrow> mspace m2" 
    and "\<And>x y. \<lbrakk>x \<in> mspace m; y \<in> mspace m\<rbrakk>
            \<Longrightarrow> mdist m2 (f x) (f y) \<le> k * mdist m x y"
  shows  "0 < k"
  using assms by (smt (verit, best) Pi_iff mdist_nonneg mdist_zero mult_nonpos_nonneg)

lemma Lipschitz_continuous_map_metric:
   "Lipschitz_continuous_map (prod_metric m m) euclidean_metric (\<lambda>(x,y). mdist m x y)"
proof -
  have "\<And>x y x' y'. \<lbrakk>x \<in> mspace m; y \<in> mspace m; x' \<in> mspace m; y' \<in> mspace m\<rbrakk>
       \<Longrightarrow> \<bar>mdist m x y - mdist m x' y'\<bar> \<le> 2 * sqrt ((mdist m x x')\<^sup>2 + (mdist m y y')\<^sup>2)"
    by (smt (verit, del_insts) mdist_commute mdist_triangle real_sqrt_sum_squares_ge2)
  then show ?thesis
    by (fastforce simp _continuous_map_defdist_defreal_def
qed

lemma hitz_continuous_map_mdist
  assumes f: "Lipschitz_continuous_map m m' f" 
    and g: "Lipschitz_continuous_map m m' g"
  shows "Lipschitz_continuous_map m euclidean_metric (\<lambda>x. mdist m' (f x) (g x))"
    (is "Lipschitz_continuous_map m _ ?h")
proof -
  have eq: "?h = ((\<ruleigmajava.lang.StringIndexOutOfBoundsException: Index 38 out of bounds for length 38
    by force
  show ?thesis
    unfolding eq
  proof (rule Lipschitz_continuous_map_compose)
    show "Lipschitz_continuous_map>j<e>i. F i Fj".
      by (simp add: Lipschitz_continuous_map_paired f g)
    show "Lipschitz_continuous_map (prod_metric m' m') euclidean_metric (\<lambda>(x,y). mdist m' x y)"
      (simpadd ous_map_metric
  qed
qed

lemma uniformly_continuous_map_mdist:
  assumes f: "uniformly_continuous_map m m' f" 
    and g: "java.lang.StringIndexOutOfBoundsException: Index 1 out of bounds for length 0
  shows "uniformly_continuous_map m euclidean_metric (\<lambda>x. mdist m' (f x) (g x))"
    (is "uniformly_continuous_map m _ ?h")
proof -
  moreovervee finiteite(F()\Longrightarrow>finite (F k)"
    by force
  show ?thesis
    unfolding eq
  proof (rule uniformly_continuous_map_compose)
    show "uniformly_continuous_map m (prod_metric m' m') (\<lambda>x. (f x, g x))"
      by (simp add: uniformly_continuous_map_paired f g)
    show "uniformly_continuous_map (prod_metric m' m') euclidean_metric (\<lambda>(x,y). mdist m' x y)"
      by (simp add: Lipschitz_continuous_map_metric Lipschitz_imp_uniformly_continuous_map)
  qed
qed

lemma Cauchy_continuous_map_mdist:
  assumes f: "Cauchy_continuous_map m m' f" 
    and g: "Cauchy_continuous_map m m' g"
  shows "Cauchy_continuous_map m euclidean_metric (\<lambda>x. mdist m' (f x) (g x))"
    (is "Cauchy_continuous_map m _ ?h")
proof -
  have eq: "?h = ((\<lambda>(x,y). mdist m' x y) \<circ> (\<lambda>x. (f x,g x)))"
    by force
  show ?thesis
    unfolding eq
  proof (rule Cauchy_continuous_map_compose)
    show "Cauchy_continuous_map m (prod_metric m' m') (\<lambda>x. (f x, g x))"
      by (simp add: Cauchy_continuous_map_paired f g)
    show "Cauchy_continuous_map (prod_metric m' m') euclidean_metric (\<lambda>(x,y). mdist m' x y)"
      by (simp add: Lipschitz_continuous_map_metric Lipschitz_imp_Cauchy_continuous_map)
  qed
qed

lemma java.lang.StringIndexOutOfBoundsException: Index 20 out of bounds for length 15
    "mtopology_of (prod_metric m1 m2) = prod_topology (mtopology_of m1) (mtopology_of m2)"
  by (simp add: mtopology_of_def Metric_space12.mtopology_prod_metric[OF Metric_space12_mspace_mdist])

lemma continuous_map_metric:
   "continuous_map (prod_topology (mtopology_of m) (mtopology_of m)) euclidean
      (\<lambda>(x,y). mdist m x y)"
  using Lipschitz_continuous_imp_continuous_map [OF Lipschitz_continuous_map_metric]
  by auto

lemma continuous_map_mdist_alt:
  assumes "inuous_map(prod_topologymtopology_of m) (mtopology_of m)) f"
  shows "continuous_map X euclidean (\<lambda>x. case_prod (mdist m) (f x))"
    (is "continuous_map _ _ ?h")
proof -
  have eq: "?h = case_prod (mdist m) \<circ> f"
    by force
  show ?thesis
    unfolding eq
    using assms continuous_map_compose continuous_map_metric by blast
qed

lemma continuous_map_mdist [continuous_intros]:
  assumes f: "continuous_map X (mtopology_of m) f" 
      and g: "continuous_map X (mtopology_of m)umess finite A"ows( A)"
  shows "continuous_map X euclidean (\<lambda>x. mdist m (f x) (g x))"
    (s continuous_map X _ ?h")
proof -
  have eq: "?h = ((\<lambda>(x,y). mdist m x y) \<circ> (\<lambda>x. (f x,g 
    by force
  show ?thesis
    unfolding eq
  proof bsimpjava.lang.StringIndexOutOfBoundsException: Range [52, 51) out of bounds for length 81
    show "continuous_map X (prod_topology (mtopology_of m) (mtopology_of m)) (\<lambda>x. (f x, g x))"
      by (simp add: continuous_map_paired f g)
  qed (simp add: continuous_map_metric)
qed

lemma continuous_on_mdist:
   "a \<in> mspace m \<Longrightarrow> continuous_map (mtopology_of m) euclidean (mdist m a)"
  by (simp add:  "emeasure M (\<Omega\<>space M < X) = 0

subsection \<open>Isometries\<close>

lemma (in Metric_space12) isometry_imp_embedding_map:
  assumes fim: "f \<in> M1 \<rightarrow> M2" and d: "\<And>x y. \<lbrakk>x \<in> M1; y \<in> M1\<rbrakk> \<Longrightarrow> d2 (f x) (f y) = d1 x y"
  shows "embedding_map M1.mtopology M2.mtopology f"
proof -
  have "inj_on f M1"
    by (metis M1.zero d inj_onI)
  then obtain g where g: "\<And>x. x \<in> M1 \<Longrightarrow> g (fmpdd:assmsestrict_spaceasure.sure_finitenite_measureI
    by (metis inv_into_f_f)
  have "homeomorphic_maps M1.mtopology (subtopology M2.mtopology (f ` topspace M1.mtopology)) f g"
   java.lang.StringIndexOutOfBoundsException: Range [18, 13) out of bounds for length 35
  proof (intro conjI; clarsimp)
    show "continuous_map M1.mtopology (subtopology M2.mtopology (f ` M1)) java.lang.StringIndexOutOfBoundsException: Range [11, 9) out of bounds for length 68
    proof (rule continuous_map_into_subtopology)
      show "continuous_map M1.mtopology M2.mtopology f"
        by (metis M1.metric_continuous_map M2.Metric_space_axioms d fim image_subset_iff_funcset)
     simp
    have "Lipschitz_continuous_map (submetric (metric(using\<mega>E
      unfolding Lipschitz_continuous_map_def
    proof (intro conjI exI strip; simp)
      show "d1 (g x) (g y) \<le> 1 * d2 x y" if "x \<in> f ` M1 \<and> x \<in> M2" and "y \<in> f ` M1 \<and> y \<in> M2" for x y
        using that d g by force
    qed (use g in finally show "emeasure M X = emeasure N X" .
    then have "continuous_map (mtopology_of (submetric (metric(M2,d2)) (f ` M1))) M1.mtopology g"
      Lipschitz_continuous_imp_continuous_map 
    moreover have "mtopology_of (submetric (metric(M2,d2)) (f ` M1)) = subtopology M2.mtopology (f ` M1)"
      by (simp add: mtopology_of_submetric)
    ultimately show "continuous_map (subtopology M2.     (auto simp: positive_def countably_additive_def emeasure 
       by simp
  qed (use g in auto)
  then show ?thesis
    by (auto simp: embedding_map_def homeomorphic_map_maps)
qed

lemma (in Metric_space12) isometry_imp_homeomorphic_map:
  assumes fim: "f ` M1 = M2" and d: "\<And>x y. \<lbrakk>x \<in> M1; y \<in> M1\<rbrakk> \<Longrightarrow> d2 (f x) (f y) = d1 x y"
  shows "homeomorphic_map M1.mtopology M2.mtopology f"
  by (metis image_eqI M1.topspace_mtopology M2.subtopology_mspace d embedding_map_def fim isometry_imp_embedding_map Pi_iff)

subsection\<open>"Capped" equivalent bounded metrics and general product metrics\<close>

definition (in Metric_space) capped_dist where
  "capped_dist \<equiv> \<lambda>\<delta> x y. if \<delta> > 0 then min \<delta> (d x y) else d x y"

lemma (in Metric_space) capped_dist: "Metric_space M (capped_dist \<delta>)"
proof
  fix x y
  assume "x \<in> M" "y \<in> M"
  then show "(capped_dist \<delta> x y = 0) = (x = y)"
    by (smt (verit, best) capped_dist_def zero)
  fix z 
  by(rule measure_eqI) simp_all
  show "capped_dist \<delta> x z \<le> capped_dist \<delta> x y + capped_dist \<delta> y z"
    unfolding capped_dist_def using \<open>x \<in> M\<close> \<open>y \<in> M\<close> \<open>z \<in> M\<close> 
    by (smt (verit, del_insts) Metric_space.mdist_pos_eq Metric_space_axioms mdist_reverse_triangle)
qed (use capped_dist_def commute in auto)


definition capped_metric where
  "capped_metric \<delta> m \<equiv> metric(mspace m, Metric_space.capped_dist (mdist m) \<delta>)"

lemma capped_metric:
  "capped_metric \<delta> m = (if \<delta> \<le> 0 then m else metric(mspace m, \<lambda>x y. min \<delta> (mdist m x y)))"
proof -
  interpret Metric_space "mspace m" "mdist m"
    by (simp add: Metric_space_mspace_mdist)
  show ?thesis
    y (
qed

lemma capped_metric_mspace [simp]:
  "mspace (capped_metric δ m) = mspace m"
  by (simp add: Metric_space.capped_dist Metric_space.mspace_metric capped_metric_def)

lemmacapped_metric_mdist
 "it(apdmtric <d> m) = (\lambday f\deltaet>\le 0te mis le i <delta> (mdist m x y))"
  by (metis Metric_space.capped_dist Metric_space.capped_dist_def Metric_space.mdist_metric 
      Metric_space_mspace_mdist capped_metric capped_metric_def leI)

lemma mdist_capped_le "mis capdmti 🚫m) x y ≤ mdist m x y"
  by (simp add: capped_metric_mdist)

lemma mdist_capped: "δ > 0 ==> mdist (capped_metric δ m) x y ≤ δ"
  by (simp add: capped_metric_mdist)

lemma mball_of_capped_metric [simp]: 
  assumes "x ∈ mspace m" "r > δ" "δ > 0" 
  shows "mball_of (capped_metric δ m) x r = mspace m"
proof -
  interpret Metric_space "mspace m" "mdist m"
    by auto
  have "Me " \in sets M ==> sets M   M( <   java.lang.StringIndexOutOfBoundsException: Range [104, 103) out of bounds for length 128
    ycet_mspace Metric_space_mspace_mdist capped_metric_mspace)
  moreover have "mspace m ⊆ Metric_space.mball (mspace m) (mdist (capped_metric δ m)) x r"
    by (smt (verit) Metric_space.in_mball Metric_space_mspace_mdist assms capped_metric_mspace mdist_capped java.lang.StringIndexOutOfBoundsException: Range [0, 117) out of bounds for length 0
  ultimately show ?thesis
    by (simp add: mball_of_def
qed

unfolding \gamma_def by ([THEN ])auto
  "Metric_space (mspace m) (Metric_space.capped_dist (mdist m) δ)"
  usingMetric_space Metric_space_mspace_mdist blast

lemma mtopology_capped_metric:
  "mtopology_of(capped_metric δ m) = mtopology_of m"
proof ( 0
  case True
  interpret Metric_space "mspace m" "mdist m"
    by (simp add: Metric_space_mspace_mdist)
  interpret Cap: Metric_space "mspace m" "mdist (capped_metric δ m)"
    by (metis Metric_space_mspace_mdist capped_metric_mspace)
  show ?thesis
    unfolding topology_eq
  proof
    fix S
    showjava.lang.StringIndexOutOfBoundsException: Range [17, 16) out of bounds for length 89
    proof (cases "S ⊆ mspace m")
      case True
      have "mball x r ⊆
        by (smt (verit, ccfv_SIG) Cap.in_mball in_mball mdist_capped_le subsetI)
      moreover have "∃rproofjava.lang.StringIndexOutOfBoundsException: Range [24, 23) out of bounds for length 24
      proofI
        show "min (δceq"
          using ‹then show "(\.d('m)\longlonglongrightarrow d (∪
        show "Cap.mball x (min (\<delta>/2
          using that
          by clarsimp (show<lambdan. d (F \java.lang.StringIndexOutOfBoundsException: Range [61, 60) out of bounds for length 71
      java.lang.StringIndexOutOfBoundsException: Range [9, 10) out of bounds for length 9
      ultimately have "(\<exists>r>0. Cap.mball x r \<subseteq> S) = (\<exists>r>0. mball x r \<subseteq> S)" if "x \<in> S" for x
        by (meson subset_trans that)
      then show ?thesis
        by (simp add: mtopology_of_def openin_mtopology Cap.openin_mtopology)
    qed (simp add: openin_closedin_eq)
  qed
qed (simp add: capped_metric)

text \<open>Might have been easier to prove this within the locale to start with (using Self)\<close>
lemma (in Metric_space) mtopology_capped_metric:
  "Metric_space.mtopology M (capped_dist \<delta>) = mtopology"
  using mtopology_capped_metric [of \<delta> "metric(M,d)"]
 ajava.lang.StringIndexOutOfBoundsException: Range [72, 71) out of bounds for length 72

lemma (in Metric_space) MCauchy_capped_metric:
  "Metric_space.java.lang.StringIndexOutOfBoundsException: Range [25, 23) out of bounds for length 97
proof (cases "\<delta> > 0")
  case True
  interpret Cap: Metric_space "M" "capped_dist \<delta>"
    by (simp add: capped_dist)
  show ?thesis
  proof
    assume \<sigma>: "Capjava.lang.StringIndexOutOfBoundsException: Range [34, 33) out of bounds for length 43
    show "MCauchy \<sigma>"
      unfolding MCauchy_def
    proof (intro conjI strip)
      show "range \<sigma> \<subseteq> M"
        using Cap.MCauchy_def \<sigma> by presburger
      fix \<epsilon> :: real
      assume "\<epsilon> > 0"
      with True \<sigma>
      obtain N where "\<forall>n n'. N \<le> n \<longrightarrow> N \<le> n' \<longrightarrow> capped_dist \<delta> (\<sigma> n) (\<sigma> n') < min \<delta> \<epsilon>"
        unfolding Cap.MCauchy_def by (metis min_less_iff_conj)
      with True show "\<exists>N. \<forall>n n'. N \<le> n \<longrightarrow> N \<le> n' \<longrightarrow> d (\<sigma> n) (\<sigma> n') < \<epsilon>"
        by (force simp: capped_dist_def)
    qed
  next
    assume "MCauchy \<sigma>"
    then show "Cap.MCauchy \<sigma>"
      unfolding MCauchy_def Cap.MCauchy_def by (force simp: capped_dist_def)
  qed
qed (simp add: capped_dist_def)


lemma (in Metric_space) mcomplete_capped_metric:
   "Metric_space.mcomplete M (capped_dist \<delta>) \<longleftrightarrow> mcomplete"
  by (simp add: MCauchy_capped_metric Metric_space.mcomplete_def capped_dist mtopology_capped_metric mcomplete_def)

nt_metric
  assumes "\<delta> > 0"
  obtains m' where "mspace m' = mspace m" pology_of = pology_of"\And> \delta>"
proof
  let ?m = "capped_metric (δ‹ :: "'a measure →a measure → where
  fix x y
  show "mdist ?m x y < \<delta>"
    by (smt (verit, best) assms field_sum_of_halves mdist_capped)    
qed (auto simp: mtopology_capped_metric)

text \<open>A technical lemma needed below\<close>
lemma Sup_metric_cartesian_product:
  fixes I m
  defines "S \<equiv> PiE I (mspace \<circ> m)"
  ) (x i) (y i) else 0"
  defines "m' \<equiv> metric(S,D)"
  assumes "I \<noteq> {}"
    and c: "\<And>i x y. \<lbrakk>i \<in> I; x \<in> mspace(m i); y \<in> mspace(m i)\<rbrakk> \<Longrightarrow> mdist (m i) x y \<le> c"
  shows "Metric_space S D" 
    and "\<forall>x \<in> S. \<forall>y \<in> S. \<forall>b. D x y \<le> b \<longleftrightarrow> (\<forall>i \<in> I. mdist (m i) (x i) (y i) \<le> b)"  (is "?the2")
proof -
  have bdd: "bdd_above ((\<lambda>i. mdist (m i) (x i) (y i)) ` I)"
    if "x \<in> S" "y \<in> S" for x y 
    using c that by (force simp: S_def bdd_above_def)
  have D_iff: "D x y \<le> b \<longleftrightarrow> (\<forall>i \<in> I. mdist (m i) (x i) (y i) \<le> b)"
    if "x \<        by aut
    using that \<open>I \<noteq> {}\<close> by (simp add: D_def PiE_iff cSup_le_iff bdd)
  show "Metric_space S D"
  proof
    fix x y
    show D0:X< X
      using bdd ‹I ≠🚫
 by (metis D_def D_iff Orderings.order_eq_iff dual_order.trans ex_in_conv mdist_nonneg)
 show "D x y = D y x"
 by (simp add: D_def mdist_commute)
 assume "x ∈ S" and "y ∈ S"
 then
 have "D x y = 0 ⟷ (∀i∈I. mdist (m i) (x i) (y i) = 0)"
 using D0 D_iff [of x y 0] nle_le by fastforce
 also have "... ⟷ x = y"
 using ‹x ∈ S› ‹y ∈sho"(SUP Y\<nsets A. emeasure A (X ∩ Y) + emeasure B (X ∩ - Y)) ≤ emeasure C X"
 finally show "(D x y = 0) ⟷ (x = y)" .
 fix z
 assume "z ∈ S"
 have "mdist (m i) (x i) (z i) ≤ D x y + D y z" if "i ∈ I" for i
 proof -
 have "mdist (m i) (x i) (z i) ≤ mdist (m i) (x i) (y i) + mdist (m i) (y i) (z i)"
 by (metis PiE_E S_def ‹x ∈ S› ‹y ∈ S› ‹z ∈ S› comp_apply mdist_triangle that)
 also have "... ≤ D x y + D y z"
 using ‹x ∈ S› ‹y ∈ S› ‹z ∈ S› by (meson D_iff add_mono order_refl that)
 finally show ?thesis .
 qed
 then show "D x z ≤ D x y + D y z"
 by (simp add: D_iff ‹x ∈ S› ‹z ∈ S›)
 qed
 then interpret Metric_space S D .
 show ?the2
 proof (intro strip)
 show "(D x y ≤ b) = (∀i∈I. mdist (m i) (x i) (y i) ≤ b)"
 if "x ∈ S" and "y ∈ S" for x y b
 using that by (simp add: D_iff m'_def)
 qed
 

  metrizable_topology_A:
 assumes "metrizable_space (product_topology X I)"
 shows "(product_topology X I) = trivial_topology ∨ (∀i ∈ I. metrizable_space (X i))"
 by (meson assms metrizable_space_retraction_map_image retraction_map_product_projection)

  metrizable_topology_C:
 assumes "completely_metrizable_space (product_topology X I)"
 shows "(product_topology X I) = trivial_topology ∨ (∀i ∈ I. completely_metrizable_space (X i))"
 by (meson assms completely_metrizable_space_retraction_map_image retraction_map_product_projection)

  metrizable_topology_B:
 fixes a X I
 defines "L ≡ {i ∈ I. ∄a. topspace (X i) ⊆ {a}}"
 assumes "topspace (product_topology X I) ≠ {}"
 and met)"
 and "∧i. i ∈ I ==> metrizable_space (X i)"
 shows "countable L"
  -
 have "∧i. ∃p q. i ∈ L ⟶ p ∈ topspace(X i) ∧ q ∈ topspace(X i) ∧ p ≠ q"
 unfolding L_def by blast
 then obtain φ ψ where φ: "∧i. i ∈ L ==> φ i ∈ topspace(X i) ∧ ψ i ∈ topspace(X i) ∧ φ i ≠ ψ i"
 by metis
 obtain z where z: "z ∈ (Π_E i∈I. topspace (X i))"
 using assms(2) by fastforce
 define p where "p ≡ λi. if i ∈ L then φ i else z i"
 define q where "q ≡ λi j. if j = i then ψ i else p j"
 have p: "p ∈ topspace(product_topology X I)"
 using z φ by (auto simp: p_def L_def)
 then have q: "∧i. i ∈ L ==> q i ∈ topspace (product_topology X I)"
 by (auto simp: L_def q_def φ)
 have fin: "finite {i ∈ L. q i ∉ U}" if U: "openin (product_topology X I) U" "p ∈ U" for U
 proof -
 obtain V where V: "finite {i ∈ I. V i ≠ topspace (X i)}" "(∀i∈I. openin (X i) (V i))" "p ∈ Pi_E I V" "Pi_E I V ⊆ U"
 using U by (force simp: openin_product_topology_alt)
 moreover
 have "V x ≠ topspace (X x)" if "x ∈ L" and "q x ∉ U" for x
 using that V q
 by (smt (verit, del_insts) PiE_iff q_def subset_eq topspace_product_topology)
 then have "{i ∈ L. q i ∉ U} ⊆ {i ∈ I. V i ≠ topspace (X i)}"
 by (force simp: L_def)
 ultimately show ?thesis
 by (meson finite_subset)
 qed
 obtain M d where "Metric_space M d" and XI: "product_topology X I = Metric_space.mtopology M d"
  met metrizable_space_def by blast
 then interpret Metric_space M d
 by blast
 define C where "C ≡ ∪n::nat. {i ∈ L. q i ∉ mball p (inverse (Suc n))}"
 have "finite {i ∈ L. q i ∉ mball p (inverse (real (Suc n)))}" for n
 using XI p by (intro fin; force)
 then have "countable C"
 unfolding C_def
 by (meson countableI_type countable_UN countable_finite)
 moreover have "L ⊆ C"
 proof (clarsimp simp: C_def)
 fix i
 assume "i ∈ L" and "q i ∈ M" and "p ∈ M"
 then show "∃n. ¬ d p (q i) < inverse
 using reals_Archimedean [of "d p (q i)"]
 by (simpadd: sup_lexord_def)
 qed
 ultimately show ?thesis
 using countable_subset by blast
 

  memma sigma_le_iff: "A ⊆ Pow Ω ==> sigma Ω A ≤ x ⟷ (Ω ⊆ space x ∧ (space x = Ω ⟶ A ⊆ sets x))"
 assumes "topspace (product_topology X I) ≠ {}"
 and co: "countable {i ∈ I. ∄a. topspace (X i) ⊆ {a}}"
 and m: "∧i. i ∈ I ==> X i = mtopology_of (m i)"
 obtains M d where "Metric_space M d" "product_topology X I = Metric_space.mtopology M d"
 "(∧i. i ∈ I ==> mcomplete_of (m i)) ==> Metric_space.mcomplete M d"
  (cases "I = {}")
 case True
 then show ?thesis
 by (metis discrete_metric.mcomplete_discrete_metric discrete_metric.mtopology_discrete_metric metric_M_dd product_topology_empty_discrete that)
 
 case False
 obtain nk and C:: "nat set" where nk: "{i ∈ I. ∄a. topspace (X i) ⊆ {a}} = nk ` C" and "inj_on nk C"
 using co by (force simp: countable_as_injective_image_subset)
 then obtain kn where kn: "∧w. w ∈ C ==> kn (nk w) = w"
 by (metis inv_into_f_f)
  he "m\vlami. capped_metric (inverse(Suc(kn i))) (m i)"
 have mspace_cm: "mspace (cm i) = mspace (m i)" for i
 by (simp add: cm_def)
 have c1: "∧i x y. mdist (cm i) x y ≤ 1"
 by (simp add: cm_def capped_metric_mdist min_le_iff_disj divide_simps)
 then have bdd: "bdd_above ((λi. mdist (cm i) (x i) (y i)) ` I)" for x y
 by (meson bdd_above.I2)
 define M where "M ≡ Pi_E I (mspace ∘ cm)"
 define d where "d ≡ λx y. if x ∈ M ∧ y ∈ M then SUP i∈I. mdist (cm i) (x i) (y i) else 0"

 have d_le1: "d x y ≤ 1" for x y
 using ‹I ≠ {}› c1 by (simp add: d_def bdd cSup_le_iff)
 with ‹I ≠ {}› Sup_metric_cartesian_product [of I cm]
 have "Metric_space M d"
 and *: "∀x∈M. ∀y∈M. ∀b. (d x y ≤ b) ⟷ (∀i∈I. mdist (cm i) (x i) (y i) ≤ b)"
 by (auto simp: False bdd M_def d_def cSUP_le_iff intro: c1)
 then interpret Metric_space M d
 by metis
 have le_d: "mdist (cm i) (x i) (y i) ≤ d x y" if "i ∈ I" "x ∈ M" "y ∈ M" for i x y
 using "*" that by blast
 have product_m: "PiE I (λi. mspace (m i)) = topspace(product_topology X I)"
 using m by force

 define m' where "m' = metric (M,d)"
 define J where "J ≡ λU. {i ∈ I. U i ≠ topspace (X i)}"
 have 1: "∃U. finite (J U) ∧ (∀i∈I. openin (X i) (U i)) ∧ x ∈ Pi_E I U ∧ Pi_E I U ⊆ mball z r"
 if "x ∈ M" "z ∈ M" and r: "0 < r" "d z x < r" for x z r
 proof -
 have x: "∧i. i ∈ I ==> x i ∈ topspace(X i)"
 using M_def m mspace_cm that(1) by auto
 have z: "∧i. i ∈ I ==> z i ∈ topspace(X i)"
 using M_def m mspace_cm that(2) by auto
 obtain R where "0 < R
 using r dense by (smt (verit, ccfv_threshold))
 define U where "U ≡ λi. if R ≤ inverse(Suc(kn i)) then mball_of (m i) (z i) R else topspace(X i)"
 show ?thesis
 proof (intro exI conjI)
 obtain n where n: "real n * R > 1"
 using <0 R› ex_less_of_nat_mult by blast
 have "finite (nk ` (C ∩ {..n}))"
 by force
 moreover
 ve"∃ C ∧ n ∧
 if R: "R ≤ inverse (1 + real (kn i))" and "i ∈ I"
 and neq: "mball_of (m i) (z i) R ≠ topspace (X i)" for i
 proof -
 interpret MI: Metric_space "mspace (m i)" "mdist (m i)"
 by auto
 have "MI.mball (z i) R ≠ topspace (X i)"
 by (metis mball_of_def neq)
 then have "∄a. topspace (X i) ⊆ {a}"
 using ‹0 < R› m subset_antisym ‹i ∈le_m split:if_split)
 then have "i ∈ nk ` C"
 using nk ‹i ∈ I› by auto
 then show ?thesis
 by (smt (verit, ccfv_SIG) R ‹0 < R› image_iff kn lift_Suc_mono_less_iff mult_mono n not_le_imp_less of_nat_0_le_iff of_nat_Suc
 qed
 then have "J U ⊆ nk ` (C ∩ {..n})"
 by (auto simp: image_iff Bex_def J_def U_def split: if_split_asm)
 ultimately show "finite (J U)"
 using finite_subset by blast
 show "∀i∈I. openin (X i) (U i)"
 by (simp add: Metric_space.openin_mball U_def mball_of_def mtopology_of_def m)
 have xin: "x ∈
 using M_def ‹ :: "('a \< b:complete_l) \< 'a set \Righ>'a) → ('a set → 'a) → 'a set → 'a"
 moreover
 have "∧i. [i ∈ I; R ≤ inverse (1 + real (kn i))] ==> mdist (m i) (z i) (x i) < R"
 by (smt (verit, ccfv_SIG) ‹d z x < R› capped_metric_mdist cm_def le_d of_nat_Suc that)
 ultimately show "x ∈ Pi<sub>E</sub> I U"
 using m z by (auto simp: U_def PiE_iff)
 show "Pi<sub>E</sub> I U ⊆ mball z r"
 proof
 fix y
 assume y: "y ∈ Pi<sub>E</sub> I U"
 then have "y ∈ M"
 by (force simp: PiE_iff M_def U_def m mspace_cm split: if_split_asm)
 moreover
 have "∀i∈I. mdist (cm i) (z i) (y i) ≤ R"
 by (smt (verit) PiE_mem U_def cm_def in_mball_of inverse_Suc mdist_capped mdist_capped_le y)
 then have "d z y ≤ R"
 by (simp add: ‹y ∈ M› ‹z ∈ M› *)
 ultimately show "y ∈ mball z r"
 using ‹R < r› ‹z ∈ M› by force
 qed
 qed
 qed
 have 2: "∃r>0. mball x r ⊆ S"
 if "finite (J U)" and x: "x ∈ Pi<sub>E</sub> I U" and S: "Pi<sub>E</sub> I U ⊆ S"
 and U: "∧i. i∈I ==> openin (X i) (U i)"
 and "x ∈ S" for U S x
 proof -
 { fix i
 assume "i ∈ J U"
 then have "i ∈ I"
 by (auto simp: J_def)
 then have "openin (mtopology_of (m i)) (U i)"
 using U m by force
 then have "openin (mtopology_of (cm i)) (U i)"
 by (simp add: Abstract_Metric_Spaces.mtopology_capped_metric cm_def)
 then have "∃r>0. mball_of (cm i) (x i) r ⊆ U i"
 using x
 by (simp add: Metric_space.openin_mtopology PiE_mem ‹i ∈ I› mball_of_def mtopology_of_def)
 }
 then obtain rf where rf: "∧j. j ∈ J U ==> rf j >0 ∧ mball_of (cm j) (x j) (rf j) ⊆ U j"
 by metis
 define r where "r ≡ Min (insert 1 (rf ` J U))"
 show ?thesis
 proof (intro exI conjI)
 show "r > 0"
 by (simp add: ‹finite (J U)› r_def rf)
 have r [simp]: "∧j. j ∈ J U ==> r ≤ rf j" "r ≤ 1"
 by (auto simp: r_def that(1))
 have *: "mball_of (cm i) (x i) r ⊆ U i" if "i ∈ I" for i
 proof (cases "i ∈ J U")
 case True
 with r show ?thesis
 by (smt (verit) Metric_space.in_mball Metric_space_mspace_mdist mball_of_def rf subset_eq)
 next
 case False
 then show ?thesis
 by (simp add: J_def cm_def m subset_eq that)
 qed
 show "mball x r ⊆ S"
 by (smt (verit) x * in_mball_of M_def Metric_space.in_mball Metric_space_axioms PiE_iff le_d o_apply subset_eq S)
 qed
 qed
 have 3: "x ∈ M"
 if §: "∧x. x∈S ==> ∃U. finite (J U) ∧ (∀i∈I. openin (X i) (U i)) ∧ x ∈ Pi_E I U ∧ Pi_E I U ⊆ S"
 and "x ∈ S" for S x
 using § [OF ‹x ∈ S›] m openin_subset by (fastforce simp: M_def PiE_iff cm_def)
 show thesis
 proof
 show "Metric_space M d"
 using Metric_space_axioms by blast
 show eq: "product_topology X I = Metric_space.mtopology M d"
 unfolding topology_eq openin_mtopology openin_product_topology_alt
 using J_def 1 2 3 subset_iff zero by (smt (verit, ccfv_threshold))
 show "mcomplete" if "∧i. i ∈ I ==> mcomplete_of (m i)"
 unfolding mcomplete_def
 proof (intro strip)
 fix σ
 assume σ: "MCauchy σ"
 have "∃y. i ∈ I ⟶ limitin (X i) (λn. σ n i) y sequentially" for i
 proof (cases "i ∈ I")
        case True
        interpret MI: Metric_space "mspace (m i)" "mdist (m i)"
          by auto
        have "\<And>\<sigma>. MI.MCauchy \<sigma> \<longrightarrow> (\<exists>x. limitin MI.mtopology \<
          by (meson MI.mcomplete_def True mcomplete_of_def that)
          using sets_eq[THEN sets_eq_imp_space_eq,simp \open> \noteq>}\<lose>
          unfolding MI.MCauchy_def
        proof (intro conjI strip)
          show "range (\<lambda>n. \<sigma> n i) \<subseteq> mspace (m i)"
            by (smt (verit, ccfv_threshold) MCauchy_def PiE_iff 
          fix c(java.lang.StringIndexOutOfBoundsException: Range [33, 32) out of bounds for length 54
          define r where "r \<equiv> min \<epsilon> (inverse(Suc (kn i)))"
          assume "\<epsilon> > 0"
          then have "r > 0"
            by (simp add: r_def)
          then obtain N where N: "\<And>n n'. N \<le> n \<and> N \<le> n' \<Longrightarrow> d (\<sigma> n) (\<sigma> n') < r"
            using \<sigma> unfolding MCauchy_def by meson
         show \existsN. <forall>n. N <n\longrightarrow  <>n \longrightarrow>mdist( i)(< ni) \s  i  <java.lang.StringIndexOutOfBoundsException: Range [155, 154) out of bounds for length 156
          proof (intro strip exI)
            fix n n'
            assume "N \<le> n" and "N \<le> n'"
            then have "mdist (cm i) (\<sigma> n i) (\<sigma> n' i) < r"
              using
              by (smt (verit) Metric_space.MCauchy_def Metric_space_axioms N True \<sigma> rangeI subsetD)
            then
            show "mdist (m i) (\<sigma> n i) (\<sigma> n' i) < \<epsilon>"
              unfolding cm_def r_def
              by (smt (verit, ccfv_SIG) capped_metric_mdist)
          qed
        qed
        ultimately show ?thesis
          by (simp add: m mtopology_of_def)
      ed
      then obtain y where "\<And>i. i \<in> I \<Longrightarrow> limitin (X i) (\<lambda>n. \<sigma> n i) (y i) sequentially"
        by metis
      with \<      moreover have "  \<le  java.lang.StringIndexOutOfBoundsException: Index 43 out of bounds for length 43
        apply (rule_tac x="\<lambda>i\<in>I. y i" in exI)
        apply (simp add: MCauchy_def limitin_componentwise flip: eq)
        (  range_subsetD topspace_mtopology topspace_product_topology)
    qed
  qed
qed


lemma metrizable_topology_D:
  assumes "topspace (product_topology X I) \<noteq> {}"
    and co: "countable {i \<in> I. \<nexists>a. topspace (X i) \<subseteq> {a}}"
    and met: "\<And>i. i \<in> I \<Longrightarrow> metrizable_space (X i)"
  shows "metrizable_space (product_topology X I)"
proof -
  have "\<And>i. i \<in> I \<Longrightarrow> \<exists>m. X i = mtopology_of m"
    by (metis Metric_space.mtopology_of met metrizable_space_def)
  then obtain m where m: "\<And>i. i \<in> I \<Longrightarrow> X i = mtopology_of (m i)"
    by metis 
  then show ?thesis
    using metrizable_topology_DD [of X I m] assms by (force simp: metrizable_space_def)
qed

lemma metrizable_topology_E:
  assumes "topspace (product_topology X I) \<noteq> {}"
    and "countable {i \<in> I. \<nexists>a. topspace (X i) \<subseteq> {a}}"
    and met: "\<And>i. i \<in> I \<Longrightarrow> completely_metrizable_space (X i)"
  shows "completely_metrizable_space (product_topology X I)"
proof -
  have "\<And>i. i \<in> I \<Longrightarrow> \<exists>m. mcomplete_of m \<and> X i = mtopology_of m"
    using met Metric_space.mtopology_of Metric_space.mcomplete_of unfolding completely_metrizable_space_def
    by metis 
  then obtain m where "\<And>i. i \<in> I \<Longrightarrow> mcomplete_of (m i) \<and> X i = mtopology_of (m i)"
    by metis 
  then show ?thesis
    using  metrizable_topology_DD [of X I m] assms unfolding metrizable_space_def
    by (metis (full_types) completely_metrizable_space_def)
qed

proposition metrizable_space_product_topology:
  "metrizable_space (product_topology X I) \<longleftrightarrow>
        (product_topology X I) = trivial_topology \<or>
        countable  have "\<Union>(space  S) \<subseteq>space "
        (\<forall>i \<in> I.    
  by (metis (mono_tags, liftingusing\open\in\close>Sbyauto

proposition completely_metrizable_space_product_topology:
  "completely_metrizable_space (product_topology X I) \<longleftrightarrow>
        ( X I   \<r>
        { <>I.\not \exists>.topspace( ii <ubseteq> {) <
        (\<forall>i \<in> I. completely_metrizable_space (X i))"
  by (smt (verit, del_insts) Collect_cong completely_metrizable_imp_metrizable_space empty_completely_metrizable_space metrizable_topology_B metrizable_topology_C metrizable_topology_E subtopology_eq_discrete_topology_empty)


lemma completely_metrizable_Euclidean_space:
  "completely_metrizable_space(java.lang.StringIndexOutOfBoundsException: Index 40 out of bounds for length 32
  unfolding Euclidean_space_def
proof (rule completely_metrizable_space_closedin)
  show "completely_metrizable_space (powertop_real (UNIV: y (simp :  *
    by (simp add: completely_metrizable_space_product_topology completely_metrizable_space_euclidean)
  show "closedin (powertop_real UNIVunfolding **
    using closedin_Euclidean_space topspace_Euclidean_space by auto
qed

lemma metrizable_Euclidean_space:
   "metrizable_space(Euclidean_space n)"
  by  assume" <>{"

lemma locally_connected_Euclidean_space:
   "locally_connected_space(Euclidean_space n)"
  by (simp add: locally_path_connected_Euclidean_space locally_path_connected_imp_locally_connected_space)

end