Quelle Abstract_Metric_Spaces.thy Sprache: Isabelle

section \<open>Abstract Metric Spaces\<close>

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 \<open>Link with the type class version\<close>
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> Open and closed balls \<close>

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 Metric topology \<close>

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\<open>Bounded sets\<close>

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\
 \<Longrightarrow> \<exists>y. y \<in> M \<and> (\<exists>B \<ge> d y a. \<forall>x\<in>S. d y x \<le> 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 \<open>S \<subseteq> M\<close> obtain a where "a \<in> S" "a \<in> M"
 by blast
 with \<open>S \<subseteq> M\<close> gt_ex have "S \<subseteq> \<Union>(range (mball a))"
 by force
 then obtain \<F> where "finite \<F>" "\<F> \<subseteq> range (mball a)" "S \<subseteq> \<Union>\<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\<open>Subspace of a metric space\<close>

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

sublocale Submetric \<subseteq> 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 \<open>S = T \<inter> A\<close> inf.bounded_iff subsetI)
 then show "openin sub.mtopology S"
 using \<open>S = T \<inter> A\<close> 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 \<open>Abstract type of metric spaces\<close>

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 \<open>Allows reference to the current metric space within the locale as a value\<close>
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\<open> Subspace of a metric space\<close>

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\<open>The discrete metric\<close>

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 \<subseteq> 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\<open>Metrizable spaces\<close>

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 \ where "\ \<equiv> mball x ` {r \<in> \<rat>. 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: \_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 \_def using \<open>x \<in> M\<close> r by fastforce
 qed
 qed (auto simp: \_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 \<equiv> 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 \<open>openin X (g ` S)\<close> m.openin_mtopology using \<open>y \<in> S\<close> 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 \<open>0 < r\<close> 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 \<open>0 < r\<close> 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
 \<Longrightarrow> 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 \<open>X = M.mtopology\<close> 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 \<open>S \<subseteq> M\<close> 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 \<section> 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 * \<open>x \<in> M\<close> 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 \<open>S \<subseteq> M\<close> 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 \<open>S \<subseteq> M\<close> 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 \<open>a \<notin> C\<close> 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 \<open>0 < r\<close> a by force
 show "C \ topspace mtopology - mcball a (r/2)"
 using C \<open>0 < r\<close> 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\<open>Limits at a point in a topological space\<close>

lemma (in Metric_space) eventually_atin_metric:
 "eventually P (atin mtopology a) \
 (a \<in> M \<longrightarrow> (\<exists>\<delta>>0. \<forall>x. x \<in> M \<and> 0 < d x a \<and> d x a < \<delta> \<longrightarrow> 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 \<delta> where "\<delta>>0" and \<delta>: "\<forall>x. x \<in> M \<and> 0 < d x a \<and> d x a < \<delta> \<longrightarrow> 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 \<open>0 < \<delta>\<close> centre_in_mball_iff openin_mball openin_mtopology)
 qed
qed auto

subsection \<open>Normal spaces and metric spaces\<close>

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 \<delta> where d0: "\<And>x. x \<in> M - S \<Longrightarrow> \<delta> x > 0 \<and> mball x (\<delta> x) \<subseteq> 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 \<epsilon> where e: "\<And>x. x \<in> M - T \<Longrightarrow> \<epsilon> x > 0 \<and> mball x (\<epsilon> x) \<subseteq> M - T"
 by metis
 assume "disjnt S T"
 have "S \ M" "T \ M"
 using \<open>closedin mtopology S\<close> \<open>closedin mtopology T\<close> closedin_metric by blast+
 have \<delta>: "\<And>x. x \<in> T \<Longrightarrow> \<delta> x > 0 \<and> mball x (\<delta> x) \<subseteq> M - S"
 by (meson DiffI \<open>T \<subseteq> M\<close> \<open>disjnt S T\<close> d0 disjnt_iff subsetD)
 have \<epsilon>: "\<And>x. x \<in> S \<Longrightarrow> \<epsilon> x > 0 \<and> mball x (\<epsilon> x) \<subseteq> M - T"
 by (meson Diff_iff \<open>S \<subseteq> M\<close> \<open>disjnt S T\<close> 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 \<epsilon> \<open>S \<subseteq> M\<close> by force
 show "T \ (\x\T. mball x (\ x / 2))"
 using \<delta> \<open>T \<subseteq> M\<close> by force
 show "disjnt (\x\S. mball x (\ x / 2)) (\x\T. mball x (\ x / 2))"
 using \<epsilon> \<delta>
 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\<open>Topological limitin in metric spaces\<close>

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 \<epsilon>::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 \<in> M \<and> (\<forall>\<epsilon>>0. \<exists>N. \<forall>n\<ge>N. f n \<in> M \<and> d (f n) l < \<epsilon>)"
 by (auto simp: limitin_metric eventually_sequentially)

lemma (in Submetric) limitin_submetric_iff:
 "limitin sub.mtopology f l F \
 l \<in> A \<and> eventually (\<lambda>x. f x \<in> A) F \<and> 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 \<subseteq> M \<and> (\<forall>\<sigma> l. range \<sigma> \<subseteq> S \<and> limitin mtopology \<sigma> l sequentially \<longrightarrow> l \<in> 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 \<sigma> where \<sigma>: "\<And>n. \<sigma> n \<in> M \<and> \<sigma> n \<in> S \<and> d x (\<sigma> 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 \<sigma> 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 \<sigma> have "limitin mtopology \<sigma> x sequentially"
 using \<open>x \<in> M - S\<close> commute limit_metric_sequentially by auto
 then show ?thesis
 by (metis R DiffD2 \<sigma> image_subset_iff \<open>x \<in> M - S\<close>)
 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 \<in> topspace X \<and>
 (x \<in> M
 \<longrightarrow> (\<forall>V. openin X V \<and> y \<in> V
 \<longrightarrow> (\<exists>\<delta>>0. \<forall>x'. x' \<in> M \<and> 0 < d x' x \<and> d x' x < \<delta> \<longrightarrow> f x' \<in> 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\<open>Cauchy sequences and complete metric spaces\<close>

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 \
 (\<forall>\<sigma>. (\<forall>\<^sub>F n in sequentially. \<sigma> n \<in> M) \<and>
 (\<forall>\<epsilon>>0. \<exists>N. \<forall>n n'. N \<le> n \<longrightarrow> N \<le> n' \<longrightarrow> d (\<sigma> n) (\<sigma> n') < \<epsilon>) \<longrightarrow>
 (\<exists>x. limitin mtopology \<sigma> x sequentially))" (is "?lhs=?rhs")
proof
 assume L: ?lhs
 show ?rhs
 proof clarify
 fix \<sigma>
 assume "\\<^sub>F n in sequentially. \ n \ M"
 and \<sigma>: "\<forall>\<epsilon>>0. \<exists>N. \<forall>n n'. N \<le> n \<longrightarrow> N \<le> n' \<longrightarrow> d (\<sigma> n) (\<sigma> n') < \<epsilon>"
 then obtain N where "\n. n\N \ \ n \ M"
 by (auto simp: eventually_sequentially)
 with \<sigma> have "MCauchy (\<sigma> \<circ> (+)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 \<epsilon>::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 \<epsilon> 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 \<epsilon> :: real
 assume "\ > 0"
 obtain N where "\n n'. N \ n \ N \ n' \ d ((\ \ (+)k) n) ((\ \ (+)k) n') < \"
 using cau \<open>\<epsilon> > 0\<close> 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 \<epsilon> :: 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 \<open>\<epsilon> > 0\<close> 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 \<open>strict_mono r\<close> le_trans max.cobounded1 strict_mono_imp_increasing that)
 then show "d (\ n) a < \"
 using N1[of n "r n"] N2[of n] \<open>\<sigma> n \<in> M\<close> \<open>a \<in> M\<close> 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 \<and> MCauchy y \<and> (\<lambda>n. d (x n) (y n)) \<longlonglongrightarrow> 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 \<epsilon> :: 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 \<epsilon> :: 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 \<open>\<epsilon> > 0\<close>)
 obtain Ny where Ny: "\n n'. \n\Ny; n'\Ny\ \ d (y n) (y n') < \/2"
 by (meson half_gt_zero MCauchy_def R \<open>\<epsilon> > 0\<close>)
 obtain Nxy where Nxy: "\n. n\Nxy \ d (x n) (y n) < \/2"
 using R \<open>\<epsilon> > 0\<close> 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)) < \<epsilon>/2"
 and dynn': "d (y (n div 2)) (y (n' div 2)) < \<epsilon>/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 \<open>\<epsilon> > 0\<close> 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) \<open>\<epsilon> > 0\<close> dxyn dxnn' triangle commute inM field_sum_of_halves)
 next
 case False
 with \<open>\<epsilon> > 0\<close> 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 \<sigma> \<subseteq> M \<and> limitin mtopology \<sigma> 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 \
 (\<forall>C::nat \<Rightarrow>'a set. (\<forall>n. closedin mtopology (C n)) \<and>
 (\<forall>n. C n \<noteq> {}) \<and> decseq C \<and> (\<forall>\<epsilon>>0. \<exists>n a. C n \<subseteq> mcball a \<epsilon>)
 \<longrightarrow> \<Inter> (range C) \<noteq> {})" (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 \<sigma> where \<sigma>: "\<And>n. \<sigma> n \<in> C n"
 by (meson ne empty_iff set_eq_iff)
 have "MCauchy \"
 unfolding MCauchy_def
 proof (intro conjI strip)
 show "range \ \ M"
 using \<sigma> clo metric_closedin_iff_sequentially_closed by auto
 fix \<epsilon> :: 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 \<sigma> that by (fastforce simp: decseq_def)+
 then have "d (\ m) (\ n) \ \/3 + \/3"
 using triangle \<sigma> commute dec decseq_def subsetD that N
 by (smt (verit, ccfv_threshold) in_mcball)
 also have "... < \"
 using \<open>\<epsilon> > 0\<close> 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 \<sigma> 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 \<sigma>
 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 \<open>MCauchy \<sigma>\<close> 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 \<open>0 < \<epsilon>\<close> \<open>MCauchy \<sigma>\<close>)
 then have "\ ` {N..} \ mcball (\ N) \"
 using MCauchy_def \<open>MCauchy \<sigma>\<close> 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 \<open>\<forall>n. closedin mtopology (C n)\<close> closedin_subset x by fastforce
 fix \<epsilon>::real
 assume "\ > 0"
 obtain N where N: "\m n. N \ m \ N \ n \ d (\ m) (\ n) < \/2"
 by (meson MCauchy_def \<open>0 < \<epsilon>\<close> \<open>MCauchy \<sigma>\<close> half_gt_zero)
 with * [of "\/2" N]
 have "\n\N. \ n \ M \ d (\ n) l < \"
 by (smt (verit) \<open>range \<sigma> \<subseteq> M\<close> 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 \
 (\<forall>C. (\<forall>n. closedin mtopology (C n)) \<and>
 (\<forall>n. C n \<noteq> {}) \<and> decseq C \<and> (\<forall>e>0. \<exists>n a. C n \<subseteq> mcball a e)
 \<longrightarrow> (\<exists>l. l \<in> M \<and> \<Inter> (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' \<in> \<Inter> (range C)" and "l' \<noteq> 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 \<open>l \<in> M\<close> l' \<open>l' \<noteq> l\<close> 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 \<open>l \<in> M\<close> \<open>l' \<in> M\<close> 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 \<open>l \<in> M\<close> 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 \
 (\<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> \<Inter> \<C> \<noteq> {})"
 (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 \<open>0 < \<epsilon>\<close> 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

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

quality100%

¤ Dauer der Verarbeitung: 0.37 Sekunden (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.