Quelle  Abstract_Metric_Spaces.thy   Sprache: Isabelle

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\\. mopen K) \ mopen (\\)"
    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 \; \X. X \ \ \ mbounded X\ \ mbounded (\\)"
  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\\. openin mtopology U; S \ \\\ \ \\. finite \ \ \ \ \ \ S \ \\"
    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 \" "\ \ range (mball a)" "S \ \\"
      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 "\ \ mball x ` {r \ \. 0 < r}"
  show "\\. countable \ \ (\V\\. openin mtopology V) \ (\U. openin mtopology U \ x \ U \ (\V\\. x \ V \ V \ U))"
  proof (intro exI conjI ballI)
    show "countable \"
      by (simp add: B_def countable_rat)
    show "\U. openin mtopology U \ x \ U \ (\V\\. 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\\. 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 "\\<^sub>F x in F. f x \ mball l \"
      using L openin_mball by (fastforce simp: limitin_def)
    then show "\\<^sub>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 "\\<^sub>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 "\\<^sub>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 "\\<^sub>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 "\\<^sub>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 "\\<^sub>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\\. closedin mtopology C"
      and cover: "\e>0. \C a. C \ \ \ C \ mcball a e"
      and fip: "\\. finite \ \ \ \ \ \ \ \ \ {}"
    then have "\n. \C. C \ \ \ (\a. C \ mcball a (inverse (Suc n)))"
      by simp
    then obtain C where C: "\n. C n \ \" 
          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 \ \\" 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)
--> --------------------

--> maximum size reached

--> --------------------