--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Abstract_Metric_Spaces.thy Tue May 23 12:31:23 2023 +0100
@@ -0,0 +1,2634 @@
+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 \<Rightarrow> 'a \<Rightarrow> real"
+ assumes nonneg [simp]: "\<And>x y. 0 \<le> d x y"
+ assumes commute: "\<And>x y. d x y = d y x"
+ assumes zero [simp]: "\<And>x y. \<lbrakk>x \<in> M; y \<in> M\<rbrakk> \<Longrightarrow> d x y = 0 \<longleftrightarrow> x=y"
+ assumes triangle: "\<And>x y z. \<lbrakk>x \<in> M; y \<in> M; z \<in> M\<rbrakk> \<Longrightarrow> d x z \<le> 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' \<subseteq> M \<Longrightarrow> Metric_space M' d"
+ by (simp add: commute in_mono Metric_space.intro triangle)
+
+lemma abs_mdist [simp] : "\<bar>d x y\<bar> = d x y"
+ by simp
+
+lemma mdist_pos_less: "\<lbrakk>x \<noteq> y; x \<in> M; y \<in> M\<rbrakk> \<Longrightarrow> 0 < d x y"
+ by (metis less_eq_real_def nonneg zero)
+
+lemma mdist_zero [simp]: "x \<in> M \<Longrightarrow> d x x = 0"
+ by simp
+
+lemma mdist_pos_eq [simp]: "\<lbrakk>x \<in> M; y \<in> M\<rbrakk> \<Longrightarrow> 0 < d x y \<longleftrightarrow> x \<noteq> y"
+ using mdist_pos_less zero by fastforce
+
+lemma triangle': "\<lbrakk>x \<in> M; y \<in> M; z \<in> M\<rbrakk> \<Longrightarrow> d x z \<le> d x y + d z y"
+ by (simp add: commute triangle)
+
+lemma triangle'': "\<lbrakk>x \<in> M; y \<in> M; z \<in> M\<rbrakk> \<Longrightarrow> d x z \<le> d y x + d y z"
+ by (simp add: commute triangle)
+
+lemma mdist_reverse_triangle: "\<lbrakk>x \<in> M; y \<in> M; z \<in> M\<rbrakk> \<Longrightarrow> \<bar>d x y - d y z\<bar> \<le> d x z"
+ by (smt (verit) commute triangle)
+
+text\<open> Open and closed balls \<close>
+
+definition mball where "mball x r \<equiv> {y. x \<in> M \<and> y \<in> M \<and> d x y < r}"
+definition mcball where "mcball x r \<equiv> {y. x \<in> M \<and> y \<in> M \<and> d x y \<le> r}"
+
+lemma in_mball [simp]: "y \<in> mball x r \<longleftrightarrow> x \<in> M \<and> y \<in> M \<and> d x y < r"
+ by (simp add: local.Metric_space_axioms Metric_space.mball_def)
+
+lemma centre_in_mball_iff [iff]: "x \<in> mball x r \<longleftrightarrow> x \<in> M \<and> 0 < r"
+ using in_mball mdist_zero by force
+
+lemma mball_subset_mspace: "mball x r \<subseteq> M"
+ by auto
+
+lemma mball_eq_empty: "mball x r = {} \<longleftrightarrow> (x \<notin> M) \<or> r \<le> 0"
+ by (smt (verit, best) Collect_empty_eq centre_in_mball_iff mball_def nonneg)
+
+lemma mball_subset: "\<lbrakk>d x y + a \<le> b; y \<in> M\<rbrakk> \<Longrightarrow> mball x a \<subseteq> mball y b"
+ by (smt (verit) commute in_mball subsetI triangle)
+
+lemma disjoint_mball: "r + r' \<le> d x x' \<Longrightarrow> disjnt (mball x r) (mball x' r')"
+ by (smt (verit) commute disjnt_iff in_mball triangle)
+
+lemma mball_subset_concentric: "r \<le> s \<Longrightarrow> mball x r \<subseteq> mball x s"
+ by auto
+
+lemma in_mcball [simp]: "y \<in> mcball x r \<longleftrightarrow> x \<in> M \<and> y \<in> M \<and> d x y \<le> r"
+ by (simp add: local.Metric_space_axioms Metric_space.mcball_def)
+
+lemma centre_in_mcball_iff [iff]: "x \<in> mcball x r \<longleftrightarrow> x \<in> M \<and> 0 \<le> r"
+ using mdist_zero by force
+
+lemma mcball_eq_empty: "mcball x r = {} \<longleftrightarrow> (x \<notin> M) \<or> 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 \<subseteq> M"
+ by auto
+
+lemma mball_subset_mcball: "mball x r \<subseteq> mcball x r"
+ by auto
+
+lemma mcball_subset: "\<lbrakk>d x y + a \<le> b; y \<in> M\<rbrakk> \<Longrightarrow> mcball x a \<subseteq> mcball y b"
+ by (smt (verit) in_mcball mdist_reverse_triangle subsetI)
+
+lemma mcball_subset_concentric: "r \<le> s \<Longrightarrow> mcball x r \<subseteq> mcball x s"
+ by force
+
+lemma mcball_subset_mball: "\<lbrakk>d x y + a < b; y \<in> M\<rbrakk> \<Longrightarrow> mcball x a \<subseteq> mball y b"
+ by (smt (verit) commute in_mball in_mcball subsetI triangle)
+
+lemma mcball_subset_mball_concentric: "a < b \<Longrightarrow> mcball x a \<subseteq> mball x b"
+ by force
+
+end
+
+
+
+subsection \<open>Metric topology \<close>
+
+context Metric_space
+begin
+
+definition mopen where
+ "mopen U \<equiv> U \<subseteq> M \<and> (\<forall>x. x \<in> U \<longrightarrow> (\<exists>r>0. mball x r \<subseteq> U))"
+
+definition mtopology :: "'a topology" where
+ "mtopology \<equiv> topology mopen"
+
+lemma is_topology_metric_topology [iff]: "istopology mopen"
+proof -
+ have "\<And>S T. \<lbrakk>mopen S; mopen T\<rbrakk> \<Longrightarrow> mopen (S \<inter> T)"
+ by (smt (verit, del_insts) Int_iff in_mball mopen_def subset_eq)
+ moreover have "\<And>\<K>. (\<forall>K\<in>\<K>. mopen K) \<longrightarrow> mopen (\<Union>\<K>)"
+ using mopen_def by fastforce
+ ultimately show ?thesis
+ by (simp add: istopology_def)
+qed
+
+lemma openin_mtopology: "openin mtopology U \<longleftrightarrow> U \<subseteq> M \<and> (\<forall>x. x \<in> U \<longrightarrow> (\<exists>r>0. mball x r \<subseteq> 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 "\<And>y. \<lbrakk>x \<in> M; d x y < r\<rbrakk> \<Longrightarrow> \<exists>s>0. mball y s \<subseteq> 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 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 \<sigma> x F = tendsto \<sigma> x F"
+ by (simp add: Met_TC.mtopology_def)
+
+lemma mtopology_is_euclideanreal [simp]: "Met_TC.mtopology = euclideanreal"
+ by (simp add: Met_TC.mtopology_def)
+
+(*
+lemma metric_injective_image:
+ "\<And>f m s.
+ f ` s \<subseteq> M \<and>
+ (\<forall>x y. x \<in> s \<and> y \<in> s \<and> f x = f y \<Longrightarrow> x = y)
+ \<Longrightarrow> (mspace(metric(s,\<lambda>(x,y). d (f x) (f y))) = s) \<and>
+ (d(metric(s,\<lambda>(x,y). d (f x) (f y))) =
+ \<lambda>(x,y). d (f x) (f y))"
+oops
+ REWRITE_TAC[\<subseteq>; FORALL_IN_IMAGE; INJECTIVE_ON_ALT] THEN
+ REPEAT GEN_TAC THEN STRIP_TAC THEN
+ REWRITE_TAC[mspace; d; GSYM PAIR_EQ] THEN
+ REWRITE_TAC[GSYM(CONJUNCT2 metric_tybij); is_metric_space] THEN
+ REWRITE_TAC[GSYM mspace; GSYM d] THEN
+ ASM_SIMP_TAC[MDIST_POS_LE; MDIST_TRIANGLE; MDIST_0] THEN
+ ASM_MESON_TAC[MDIST_SYM]);;
+*)
+
+lemma mtopology_base:
+ "mtopology = topology(arbitrary union_of (\<lambda>U. \<exists>x \<in> M. \<exists>r>0. U = mball x r))"
+proof -
+ have "\<And>S. \<exists>x r. x \<in> M \<and> 0 < r \<and> S = mball x r \<Longrightarrow> openin mtopology S"
+ using openin_mball by blast
+ moreover have "\<And>U x. \<lbrakk>openin mtopology U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>B. (\<exists>x r. x \<in> M \<and> 0 < r \<and> B = mball x r) \<and> x \<in> B \<and> B \<subseteq> 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 \<longleftrightarrow> C \<subseteq> M \<and> (\<forall>x. x \<in> M - C \<longrightarrow> (\<exists>r>0. disjnt C (mball x r)))" (is "?lhs = ?rhs")
+proof
+ show "?lhs \<Longrightarrow> ?rhs"
+ unfolding closedin_def openin_mtopology
+ by (metis Diff_disjoint disjnt_def disjnt_subset2 topspace_mtopology)
+ show "?rhs \<Longrightarrow> ?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 "\<exists>ra>0. disjnt (mcball x r) (mball y ra)" if "x \<notin> 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 \<in> 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: "(\<exists>r>0. mball x r \<subseteq> U) = (\<exists>r>0. mcball x r \<subseteq> U)"
+ by (meson dense mball_subset_mcball mcball_subset_mball_concentric order_trans)
+
+lemma openin_mtopology_mcball:
+ "openin mtopology U \<longleftrightarrow> U \<subseteq> M \<and> (\<forall>x. x \<in> U \<longrightarrow> (\<exists>r. 0 < r \<and> mcball x r \<subseteq> U))"
+ using mball_iff_mcball openin_mtopology by presburger
+
+lemma metric_derived_set_of:
+ "mtopology derived_set_of S = {x \<in> M. \<forall>r>0. \<exists>y\<in>S. y\<noteq>x \<and> y \<in> mball x r}" (is "?lhs=?rhs")
+proof
+ show "?lhs \<subseteq> ?rhs"
+ unfolding openin_mtopology derived_set_of_def
+ by clarsimp (metis in_mball openin_mball openin_mtopology zero)
+ show "?rhs \<subseteq> ?lhs"
+ unfolding openin_mtopology derived_set_of_def
+ by clarify (metis subsetD topspace_mtopology)
+qed
+
+lemma metric_closure_of:
+ "mtopology closure_of S = {x \<in> M. \<forall>r>0. \<exists>y \<in> S. y \<in> mball x r}"
+proof -
+ have "\<And>x r. \<lbrakk>0 < r; x \<in> mtopology closure_of S\<rbrakk> \<Longrightarrow> \<exists>y\<in>S. y \<in> mball x r"
+ by (metis centre_in_mball_iff in_closure_of openin_mball topspace_mtopology)
+ moreover have "\<And>x T. \<lbrakk>x \<in> M; \<forall>r>0. \<exists>y\<in>S. y \<in> mball x r\<rbrakk> \<Longrightarrow> x \<in> 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 \<in> M. \<forall>r>0. \<exists>y \<in> S. y \<in> mcball x r}"
+proof -
+ have "\<And>x r. \<lbrakk>\<forall>r>0. x \<in> M \<and> (\<exists>y\<in>S. y \<in> mcball x r); 0 < r\<rbrakk> \<Longrightarrow> \<exists>y\<in>S. y \<in> M \<and> 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 \<in> M. \<exists>\<epsilon>>0. mball x \<epsilon> \<subseteq> S}" (is "?lhs=?rhs")
+proof
+ show "?lhs \<subseteq> ?rhs"
+ using interior_of_maximal_eq openin_mtopology by fastforce
+ show "?rhs \<subseteq> ?lhs"
+ using interior_of_def openin_mball by fastforce
+qed
+
+lemma metric_interior_of_alt:
+ "mtopology interior_of S = {x \<in> M. \<exists>\<epsilon>>0. mcball x \<epsilon> \<subseteq> S}"
+ by (fastforce simp: mball_iff_mcball metric_interior_of)
+
+lemma in_interior_of_mball:
+ "x \<in> mtopology interior_of S \<longleftrightarrow> x \<in> M \<and> (\<exists>\<epsilon>>0. mball x \<epsilon> \<subseteq> S)"
+ using metric_interior_of by force
+
+lemma in_interior_of_mcball:
+ "x \<in> mtopology interior_of S \<longleftrightarrow> x \<in> M \<and> (\<exists>\<epsilon>>0. mcball x \<epsilon> \<subseteq> 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 \<in> topspace mtopology" and y: "y \<in> topspace mtopology" and "x \<noteq> 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 "\<exists>U V. openin mtopology U \<and> openin mtopology V \<and> x \<in> U \<and> y \<in> V \<and> 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 \<longleftrightarrow> (\<exists>x B. S \<subseteq> mcball x B)"
+
+lemma mbounded_pos: "mbounded S \<longleftrightarrow> (\<exists>x B. 0 < B \<and> S \<subseteq> mcball x B)"
+proof -
+ have "\<exists>x' r'. 0 < r' \<and> S \<subseteq> mcball x' r'" if "S \<subseteq> 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 \<longleftrightarrow> S \<subseteq> M \<and> (\<exists>B. \<forall>x \<in> S. \<forall>y \<in> S. d x y \<le> B)"
+proof -
+ have "\<And>x B. S \<subseteq> mcball x B \<Longrightarrow> \<forall>x\<in>S. \<forall>y\<in>S. d x y \<le> 2 * B"
+ by (smt (verit, best) commute in_mcball subsetD triangle)
+ then show ?thesis
+ apply (auto simp: mbounded_def subset_iff)
+ apply blast+
+ done
+qed
+
+
+lemma mbounded_alt_pos:
+ "mbounded S \<longleftrightarrow> S \<subseteq> M \<and> (\<exists>B>0. \<forall>x \<in> S. \<forall>y \<in> S. d x y \<le> B)"
+ by (smt (verit, del_insts) gt_ex mbounded_alt)
+
+lemma mbounded_subset: "\<lbrakk>mbounded T; S \<subseteq> T\<rbrakk> \<Longrightarrow> mbounded S"
+ by (meson mbounded_def order_trans)
+
+lemma mbounded_subset_mspace: "mbounded S \<Longrightarrow> S \<subseteq> M"
+ by (simp add: mbounded_alt)
+
+lemma mbounded:
+ "mbounded S \<longleftrightarrow> S = {} \<or> (\<forall>x \<in> S. x \<in> M) \<and> (\<exists>y B. y \<in> M \<and> (\<forall>x \<in> S. d y x \<le> 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) \<longleftrightarrow> a \<in> M \<and> mbounded S"
+proof -
+ have "\<And>y B. \<lbrakk>y \<in> M; \<forall>x\<in>S. d y x \<le> B\<rbrakk>
+ \<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 \<Longrightarrow> mbounded (S \<inter> T)"
+ by (meson inf_le1 mbounded_subset)
+
+lemma mbounded_Un: "mbounded (S \<union> T) \<longleftrightarrow> mbounded S \<and> mbounded T" (is "?lhs=?rhs")
+proof
+ assume R: ?rhs
+ show ?lhs
+ proof (cases "S={} \<or> T={}")
+ case True then show ?thesis
+ using R by auto
+ next
+ case False
+ obtain x y B C where "S \<subseteq> mcball x B" "T \<subseteq> mcball y C" "B > 0" "C > 0" "x \<in> M" "y \<in> M"
+ using R mbounded_pos
+ by (metis False mcball_eq_empty subset_empty)
+ then have "S \<union> T \<subseteq> 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 \<Longrightarrow> ?rhs"
+ using mbounded_def by auto
+qed
+
+lemma mbounded_Union:
+ "\<lbrakk>finite \<F>; \<And>X. X \<in> \<F> \<Longrightarrow> mbounded X\<rbrakk> \<Longrightarrow> mbounded (\<Union>\<F>)"
+ by (induction \<F> rule: finite_induct) (auto simp: mbounded_Un)
+
+lemma mbounded_closure_of:
+ "mbounded S \<Longrightarrow> mbounded (mtopology closure_of S)"
+ by (meson closedin_mcball closure_of_minimal mbounded_def)
+
+lemma mbounded_closure_of_eq:
+ "S \<subseteq> M \<Longrightarrow> (mbounded (mtopology closure_of S) \<longleftrightarrow> mbounded S)"
+ by (metis closure_of_subset mbounded_closure_of mbounded_subset topspace_mtopology)
+
+
+lemma maxdist_thm:
+ assumes "mbounded S"
+ and "x \<in> S"
+ and "y \<in> S"
+ shows "d x y = (SUP z\<in>S. \<bar>d x z - d z y\<bar>)"
+proof -
+ have "\<bar>d x z - d z y\<bar> \<le> d x y" if "z \<in> S" for z
+ by (metis all_not_in_conv assms mbounded mdist_reverse_triangle that)
+ moreover have "d x y \<le> r"
+ if "\<And>z. z \<in> S \<Longrightarrow> \<bar>d x z - d z y\<bar> \<le> 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: "\<lbrakk>S \<subseteq> M; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> (x = y) = (\<forall>z\<in>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 \<subseteq> M"
+ and com: "\<And>\<U>. \<lbrakk>\<forall>U\<in>\<U>. openin mtopology U; S \<subseteq> \<Union>\<U>\<rbrakk> \<Longrightarrow> \<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> S \<subseteq> \<Union>\<F>"
+ 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
+ moreover have "\<forall>U \<in> range (mball a). openin mtopology U"
+ by (simp add: openin_mball)
+ ultimately obtain \<F> where "finite \<F>" "\<F> \<subseteq> range (mball a)" "S \<subseteq> \<Union>\<F>"
+ by (meson com)
+ then show ?thesis
+ using mbounded_Union mbounded_subset by fastforce
+ qed auto
+qed
+
+end
+
+
+subsection\<open>Subspace of a metric space\<close>
+
+locale submetric = Metric_space +
+ fixes A
+ assumes subset: "A \<subseteq> 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 \<in> A then A \<inter> mball a r else {})"
+and mcball_submetric_eq: "sub.mcball a r = (if a \<in> A then A \<inter> 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 "\<exists>T. openin (subtopology mtopology A) T \<and> x \<in> T \<and> T \<subseteq> S" if "x \<in> 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 \<inter> A"
+ by (meson openin_subtopology)
+ then have "mopen T"
+ by (simp add: mopen_def openin_mtopology)
+ then have "sub.mopen (T \<inter> 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 \<longleftrightarrow> mbounded T \<and> T \<subseteq> A"
+ by (meson mbounded_alt sub.mbounded_alt subset subset_trans)
+
+end
+
+lemma (in Metric_space) submetric_empty [iff]: "submetric M d {}"
+ by (simp add: Metric_space_axioms submetric.intro submetric_axioms_def)
+
+
+subsection\<open>The discrete metric\<close>
+
+locale discrete_metric =
+ fixes M :: "'a set"
+
+definition (in discrete_metric) dd :: "'a \<Rightarrow> 'a \<Rightarrow> real"
+ where "dd \<equiv> \<lambda>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 \<in> M" shows "disc.mopen {x}"
+proof -
+ have "disc.mball x (1/2) \<subseteq> {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 "\<And>x. x \<in> M \<Longrightarrow> 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 \<le> max (dd x y) (dd y z)"
+ by (simp add: dd_def)
+
+
+lemma (in discrete_metric) dd_le1: "dd x y \<le> 1"
+ by (simp add: dd_def)
+
+lemma (in discrete_metric) mbounded_discrete_metric: "disc.mbounded S \<longleftrightarrow> S \<subseteq> M"
+ by (meson dd_le1 disc.mbounded_alt)
+
+
+
+subsection\<open>Metrizable spaces\<close>
+
+definition metrizable_space where
+ "metrizable_space X \<equiv> \<exists>M d. Metric_space M d \<and> 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 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:
+ "metrizable_space(discrete_topology U)"
+ by (metis discrete_metric.mtopology_discrete_metric metric_M_dd metrizable_space_def)
+
+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 \<inter> 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: "(\<forall>x \<in> M. g(f x) = x) \<and> (\<forall>y \<in> 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 \<in> topspace Y" "y \<in> 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) \<le> d (g x) (g y) + d (g y) (g z)"
+ if "x \<in> topspace Y" and "y \<in> topspace Y" and "z \<in> 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 \<subseteq> topspace Y" and "openin X (g ` S)"
+ unfolding m'.openin_mtopology
+ proof (intro conjI that strip)
+ fix y
+ assume "y \<in> S"
+ then obtain r where "r>0" and r: "m.mball (g y) r \<subseteq> 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 \<subseteq> m.mball (g y) r"
+ using X d'_def hmg homeomorphic_imp_surjective_map by fastforce
+ with S fg have "m'.mball y r \<subseteq> S"
+ by (smt (verit, del_insts) image_iff m'.in_mball r subset_iff)
+ then show "\<exists>r>0. m'.mball y r \<subseteq> S"
+ using \<open>0 < r\<close> by blast
+ qed
+ moreover have "openin X (g ` S)" if ope': "openin m'.mtopology S"
+ proof -
+ have "\<exists>r>0. m.mball (g y) r \<subseteq> g ` S" if "y \<in> S" for y
+ proof -
+ have y: "y \<in> topspace Y"
+ using m'.openin_mtopology ope' that by blast
+ obtain r where "r > 0" and r: "m'.mball y r \<subseteq> S"
+ using ope' by (meson \<open>y \<in> S\<close> m'.openin_mtopology)
+ moreover have "\<And>x. \<lbrakk>x \<in> M; d (g y) x < r\<rbrakk> \<Longrightarrow> \<exists>u. u \<in> topspace Y \<and> d' y u < r \<and> x = g u"
+ using fg X d'_def hmf homeomorphic_imp_surjective_map by fastforce
+ ultimately have "m.mball (g y) r \<subseteq> 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 \<subseteq> topspace Y \<and> 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 \<longleftrightarrow> 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 \<and> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<subseteq> 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 "\<exists>y\<in>S. d x y < inverse (1 + real n)" if "x \<in> S" for x n
+ using \<open>S \<subseteq> M\<close> M.mdist_zero [of x] that by force
+ moreover
+ have "x \<in> S" if "x \<in> M" and \<section>: "\<And>n. \<exists>y\<in>S. d x y < inverse(Suc n)" for x
+ proof -
+ have *: "\<exists>y\<in>S. d x y < \<epsilon>" if "\<epsilon> > 0" for \<epsilon>
+ 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)
+ then show ?thesis
+ apply (simp add: M.closedin_metric)
+ by (metis * \<open>x \<in> M\<close> M.in_mball disjnt_insert1 insert_absorb subsetD)
+ qed
+ ultimately have Seq: "S = \<Inter>(range (\<lambda>n. {x\<in>M. \<exists>y\<in>S. d x y < inverse(Suc n)}))"
+ using \<open>S \<subseteq> M\<close> by force
+ have "openin M.mtopology {xa \<in> M. \<exists>y\<in>S. d xa y < inverse (1 + real n)}" for n
+ proof (clarsimp simp: M.openin_mtopology)
+ fix x y
+ assume "x \<in> M" "y \<in> S" and dxy: "d x y < inverse (1 + real n)"
+ then have "\<And>z. \<lbrakk>z \<in> M; d x z < inverse (1 + real n) - d x y\<rbrakk> \<Longrightarrow> \<exists>y\<in>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 "\<exists>r>0. M.mball x r \<subseteq> {z \<in> M. \<exists>y\<in>S. d z y < inverse (1 + real n)}"
+ by (rule_tac x="inverse(Suc n) - d x y" in exI) auto
+ qed
+ then show ?thesis
+ apply (subst Seq)
+ apply (force simp: Xeq intro: gdelta_in_Inter open_imp_gdelta_in)
+ done
+ qed
+qed
+
+lemma open_imp_fsigma_in:
+ "\<lbrakk>metrizable_space X; openin X S\<rbrakk> \<Longrightarrow> fsigma_in X S"
+ by (meson closed_imp_gdelta_in fsigma_in_gdelta_in openin_closedin openin_subset)
+
+(*NEEDS first_countable
+lemma first_countable_mtopology:
+ "first_countable mtopology"
+oops
+ GEN_TAC THEN REWRITE_TAC[first_countable; TOPSPACE_MTOPOLOGY] THEN
+ X_GEN_TAC `x::A` THEN DISCH_TAC THEN
+ EXISTS_TAC `{ mball m (x::A,r) | rational r \<and> 0 < r}` THEN
+ REWRITE_TAC[FORALL_IN_GSPEC; OPEN_IN_MBALL; EXISTS_IN_GSPEC] THEN
+ ONCE_REWRITE_TAC[SET_RULE
+ `{f x | S x \<and> Q x} = f ` {x \<in> S. Q x}`] THEN
+ SIMP_TAC[COUNTABLE_IMAGE; COUNTABLE_RATIONAL; COUNTABLE_RESTRICT] THEN
+ REWRITE_TAC[OPEN_IN_MTOPOLOGY] THEN
+ X_GEN_TAC `U::A=>bool` THEN STRIP_TAC THEN
+ FIRST_X_ASSUM(MP_TAC \<circ> SPEC `x::A`) THEN
+ ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
+ X_GEN_TAC `r::real` THEN STRIP_TAC THEN FIRST_ASSUM
+ (MP_TAC \<circ> SPEC `r::real` \<circ> MATCH_MP RATIONAL_APPROXIMATION_BELOW) THEN
+ MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `q::real` THEN
+ REWRITE_TAC[REAL_SUB_REFL] THEN STRIP_TAC THEN
+ ASM_SIMP_TAC[CENTRE_IN_MBALL] THEN
+ TRANS_TAC SUBSET_TRANS `mball m (x::A,r)` THEN
+ ASM_SIMP_TAC[MBALL_SUBSET_CONCENTRIC; REAL_LT_IMP_LE]);;
+
+lemma metrizable_imp_first_countable:
+ "metrizable_space X \<Longrightarrow> first_countable X"
+oops
+ REWRITE_TAC[FORALL_METRIZABLE_SPACE; FIRST_COUNTABLE_MTOPOLOGY]);;
+*)
+
+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 metrizable_space_euclidean:
+ "metrizable_space (euclidean :: 'a::metric_space topology)"
+ unfolding metrizable_space_def
+ by (metis Met_TC.Metric_space_axioms Met_TC.mtopology_def mopen_eq_open)
+
+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 \<in> topspace mtopology" and "a \<notin> C"
+ have "openin mtopology (topspace mtopology - C)"
+ by (simp add: C openin_diff)
+ then obtain r where "r>0" and r: "mball a r \<subseteq> topspace mtopology - C"
+ unfolding openin_mtopology using \<open>a \<notin> C\<close> a by auto
+ show "\<exists>U V. openin mtopology U \<and> openin mtopology V \<and> a \<in> U \<and> C \<subseteq> V \<and> disjnt U V"
+ proof (intro exI conjI)
+ show "a \<in> mball a (r/2)"
+ using \<open>0 < r\<close> a by force
+ show "C \<subseteq> 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 \<Longrightarrow> 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) \<longleftrightarrow>
+ (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 \<in> M")
+ case True
+ show ?thesis
+ proof
+ assume L: ?lhs
+ with True obtain U where "openin mtopology U" "a \<in> U" and U: "\<forall>x\<in>U - {a}. P x"
+ by (auto simp: eventually_atin)
+ then obtain r where "r>0" and "mball a r \<subseteq> 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 "\<forall>x \<in> mball a \<delta> - {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 "\<And>x. x \<in> M - S \<Longrightarrow> (\<exists>r>0. mball x r \<subseteq> 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 "\<And>x. x \<in> M - T \<Longrightarrow> (\<exists>r>0. mball x r \<subseteq> 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 \<subseteq> M" "T \<subseteq> 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 "\<exists>U V. openin mtopology U \<and> openin mtopology V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V"
+ proof (intro exI conjI)
+ show "openin mtopology (\<Union>x\<in>S. mball x (\<epsilon> x / 2))" "openin mtopology (\<Union>x\<in>T. mball x (\<delta> x / 2))"
+ by force+
+ show "S \<subseteq> (\<Union>x\<in>S. mball x (\<epsilon> x / 2))"
+ using \<epsilon> \<open>S \<subseteq> M\<close> by force
+ show "T \<subseteq> (\<Union>x\<in>T. mball x (\<delta> x / 2))"
+ using \<delta> \<open>T \<subseteq> M\<close> by force
+ show "disjnt (\<Union>x\<in>S. mball x (\<epsilon> x / 2)) (\<Union>x\<in>T. mball x (\<delta> 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 \<Longrightarrow> 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 \<Longrightarrow> l \<in> M"
+ using limitin_topspace by fastforce
+
+lemma (in Metric_space) limitin_metric_unique:
+ "\<lbrakk>limitin mtopology f l1 F; limitin mtopology f l2 F; F \<noteq> bot\<rbrakk> \<Longrightarrow> l1 = l2"
+ by (meson Hausdorff_space_mtopology limitin_Hausdorff_unique)
+
+lemma (in Metric_space) limitin_metric:
+ "limitin mtopology f l F \<longleftrightarrow> l \<in> M \<and> (\<forall>\<epsilon>>0. eventually (\<lambda>x. f x \<in> M \<and> d (f x) l < \<epsilon>) F)"
+ (is "?lhs=?rhs")
+proof
+ assume L: ?lhs
+ show ?rhs
+ unfolding limitin_def
+ proof (intro conjI strip)
+ show "l \<in> M"
+ using L limitin_mspace by blast
+ fix \<epsilon>::real
+ assume "\<epsilon>>0"
+ then have "\<forall>\<^sub>F x in F. f x \<in> mball l \<epsilon>"
+ using L openin_mball by (fastforce simp: limitin_def)
+ then show "\<forall>\<^sub>F x in F. f x \<in> M \<and> d (f x) l < \<epsilon>"
+ 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 \<longleftrightarrow>
+ 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 \<longleftrightarrow>
+ 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 \<longleftrightarrow>
+ 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 \<subseteq> M"
+ using R by blast
+ fix x
+ assume "x \<in> M - S"
+ have False if "\<forall>r>0. \<exists>y. y \<in> M \<and> y \<in> S \<and> d x y < r"
+ proof -
+ have "\<forall>n. \<exists>y. y \<in> M \<and> y \<in> S \<and> 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 \<sigma> \<subseteq> M"
+ by blast
+ have "\<exists>N. \<forall>n\<ge>N. d x (\<sigma> n) < \<epsilon>" if "\<epsilon>>0" for \<epsilon>
+ proof -
+ have "real (Suc (nat \<lceil>inverse \<epsilon>\<rceil>)) \<ge> inverse \<epsilon>"
+ by linarith
+ then have "\<forall>n \<ge> nat \<lceil>inverse \<epsilon>\<rceil>. d x (\<sigma> n) < \<epsilon>"
+ 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 "\<exists>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) \<longleftrightarrow>
+ 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 \<longleftrightarrow> l \<in> M \<and> eventually (\<lambda>x. f x \<in> M) F \<and> ((\<lambda>x. d (f x) l) \<longlongrightarrow> 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 \<Rightarrow> 'a) \<Rightarrow> bool"
+ where "MCauchy \<sigma> \<equiv> range \<sigma> \<subseteq> M \<and> (\<forall>\<epsilon>>0. \<exists>N. \<forall>n n'. N \<le> n \<longrightarrow> N \<le> n' \<longrightarrow> d (\<sigma> n) (\<sigma> n') < \<epsilon>)"
+
+definition mcomplete
+ where "mcomplete \<equiv> (\<forall>\<sigma>. MCauchy \<sigma> \<longrightarrow> (\<exists>x. limitin mtopology \<sigma> 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 \<sigma> \<Longrightarrow> MCauchy (\<sigma> \<circ> (+)n)"
+ unfolding MCauchy_def image_subset_iff comp_apply
+ by (metis UNIV_I add.commute trans_le_add1)
+
+lemma mcomplete:
+ "mcomplete \<longleftrightarrow>
+ (\<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 "\<forall>\<^sub>F n in sequentially. \<sigma> n \<in> 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 "\<And>n. n\<ge>N \<Longrightarrow> \<sigma> n \<in> 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 (\<sigma> \<circ> (+)N) x sequentially"
+ using L MCauchy_imp_MCauchy_suffix mcomplete_def by blast
+ then have "limitin mtopology \<sigma> x sequentially"
+ unfolding o_def by (auto simp: add.commute limitin_sequentially_offset_rev)
+ then show "\<exists>x. limitin mtopology \<sigma> x sequentially" ..
+ qed
+qed (simp add: mcomplete_def MCauchy_def image_subset_iff)
+
+lemma mcomplete_empty_mspace: "M = {} \<Longrightarrow> mcomplete"
+ using MCauchy_def mcomplete_def by blast
+
+lemma MCauchy_const [simp]: "MCauchy (\<lambda>n. a) \<longleftrightarrow> a \<in> M"
+ using MCauchy_def mdist_zero by auto
+
+lemma convergent_imp_MCauchy:
+ assumes "range \<sigma> \<subseteq> M" and lim: "limitin mtopology \<sigma> l sequentially"
+ shows "MCauchy \<sigma>"
+ unfolding MCauchy_def image_subset_iff
+proof (intro conjI strip)
+ fix \<epsilon>::real
+ assume "\<epsilon> > 0"
+ then have "\<forall>\<^sub>F n in sequentially. \<sigma> n \<in> M \<and> d (\<sigma> n) l < \<epsilon>/2"
+ using half_gt_zero lim limitin_metric by blast
+ then obtain N where "\<And>n. n\<ge>N \<Longrightarrow> \<sigma> n \<in> M \<and> d (\<sigma> n) l < \<epsilon>/2"
+ by (force simp: eventually_sequentially)
+ then show "\<exists>N. \<forall>n n'. N \<le> n \<longrightarrow> N \<le> n' \<longrightarrow> d (\<sigma> n) (\<sigma> n') < \<epsilon>"
+ by (smt (verit) Metric_space.limitin_mspace Metric_space.mdist_reverse_triangle Metric_space_axioms field_sum_of_halves lim)
+qed (use assms in blast)
+
+
+lemma mcomplete_alt:
+ "mcomplete \<longleftrightarrow> (\<forall>\<sigma>. MCauchy \<sigma> \<longleftrightarrow> range \<sigma> \<subseteq> M \<and> (\<exists>x. limitin mtopology \<sigma> x sequentially))"
+ using MCauchy_def convergent_imp_MCauchy mcomplete_def by blast
+
+lemma MCauchy_subsequence:
+ assumes "strict_mono r" "MCauchy \<sigma>"
+ shows "MCauchy (\<sigma> \<circ> r)"
+proof -
+ have "d (\<sigma> (r n)) (\<sigma> (r n')) < \<epsilon>"
+ if "N \<le> n" "N \<le> n'" "strict_mono r" "\<forall>n n'. N \<le> n \<longrightarrow> N \<le> n' \<longrightarrow> d (\<sigma> n) (\<sigma> n') < \<epsilon>"
+ for \<epsilon> N n n'
+ using that by (meson le_trans strict_mono_imp_increasing)
+ moreover have "range (\<lambda>x. \<sigma> (r x)) \<subseteq> 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 (\<sigma> \<circ> (+)k)" and \<sigma>: "\<And>n. n < k \<Longrightarrow> \<sigma> n \<in> M"
+ shows "MCauchy \<sigma>"
+ unfolding MCauchy_def image_subset_iff
+proof (intro conjI strip)
+ fix n
+ show "\<sigma> n \<in> 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 "\<epsilon> > 0"
+ obtain N where "\<forall>n n'. N \<le> n \<longrightarrow> N \<le> n' \<longrightarrow> d ((\<sigma> \<circ> (+)k) n) ((\<sigma> \<circ> (+)k) n') < \<epsilon>"
+ using cau \<open>\<epsilon> > 0\<close> by (fastforce simp: MCauchy_def)
+ then show "\<exists>N. \<forall>n n'. N \<le> n \<longrightarrow> N \<le> n' \<longrightarrow> d (\<sigma> n) (\<sigma> n') < \<epsilon>"
+ unfolding o_def
+ apply (rule_tac x="k+N" in exI)
+ by (smt (verit, del_insts) add.assoc le_add1 less_eqE)
+qed
+
+lemma MCauchy_convergent_subsequence:
+ assumes cau: "MCauchy \<sigma>" and "strict_mono r"
+ and lim: "limitin mtopology (\<sigma> \<circ> r) a sequentially"
+ shows "limitin mtopology \<sigma> a sequentially"
+ unfolding limitin_metric
+proof (intro conjI strip)
+ show "a \<in> M"
+ by (meson assms limitin_mspace)
+ fix \<epsilon> :: real
+ assume "\<epsilon> > 0"
+ then obtain N1 where N1: "\<And>n n'. \<lbrakk>n\<ge>N1; n'\<ge>N1\<rbrakk> \<Longrightarrow> d (\<sigma> n) (\<sigma> n') < \<epsilon>/2"
+ using cau unfolding MCauchy_def by (meson half_gt_zero)
+ obtain N2 where N2: "\<And>n. n \<ge> N2 \<Longrightarrow> (\<sigma> \<circ> r) n \<in> M \<and> d ((\<sigma> \<circ> r) n) a < \<epsilon>/2"
+ by (metis (no_types, lifting) lim \<open>\<epsilon> > 0\<close> half_gt_zero limit_metric_sequentially)
+ have "\<sigma> n \<in> M \<and> d (\<sigma> n) a < \<epsilon>" if "n \<ge> max N1 N2" for n
+ proof (intro conjI)
+ show "\<sigma> n \<in> M"
+ using MCauchy_def cau by blast
+ have "N1 \<le> r n"
+ by (meson \<open>strict_mono r\<close> le_trans max.cobounded1 strict_mono_imp_increasing that)
+ then show "d (\<sigma> n) a < \<epsilon>"
+ 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 "\<forall>\<^sub>F n in sequentially. \<sigma> n \<in> M \<and> d (\<sigma> n) a < \<epsilon>"
+ using eventually_sequentially by blast
+qed
+
+lemma MCauchy_interleaving_gen:
+ "MCauchy (\<lambda>n. if even n then x(n div 2) else y(n div 2)) \<longleftrightarrow>
+ (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 (\<lambda>n::nat. 2 * n)" and odds: "strict_mono (\<lambda>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 "(\<lambda>n. d (x n) (y n)) \<longlonglongrightarrow> 0"
+ unfolding LIMSEQ_iff
+ proof (intro strip)
+ fix \<epsilon> :: real
+ assume "\<epsilon> > 0"
+ then obtain N where N:
+ "\<And>n n'. \<lbrakk>n\<ge>N; n'\<ge>N\<rbrakk> \<Longrightarrow> 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)) < \<epsilon>"
+ using L MCauchy_def by fastforce
+ have "d (x n) (y n) < \<epsilon>" if "n\<ge>N" for n
+ using N [of "2*n" "Suc(2*n)"] that by auto
+ then show "\<exists>N. \<forall>n\<ge>N. norm (d (x n) (y n) - 0) < \<epsilon>"
+ by auto
+ qed
+ qed
+next
+ assume R: ?rhs
+ show ?lhs
+ unfolding MCauchy_def
+ proof (intro conjI strip)
+ show "range (\<lambda>n. if even n then x (n div 2) else y (n div 2)) \<subseteq> M"
+ using R by (auto simp: MCauchy_def)
+ fix \<epsilon> :: real
+ assume "\<epsilon> > 0"
+ obtain Nx where Nx: "\<And>n n'. \<lbrakk>n\<ge>Nx; n'\<ge>Nx\<rbrakk> \<Longrightarrow> d (x n) (x n') < \<epsilon>/2"
+ by (meson half_gt_zero MCauchy_def R \<open>\<epsilon> > 0\<close>)
+ obtain Ny where Ny: "\<And>n n'. \<lbrakk>n\<ge>Ny; n'\<ge>Ny\<rbrakk> \<Longrightarrow> d (y n) (y n') < \<epsilon>/2"
+ by (meson half_gt_zero MCauchy_def R \<open>\<epsilon> > 0\<close>)
+ obtain Nxy where Nxy: "\<And>n. n\<ge>Nxy \<Longrightarrow> d (x n) (y n) < \<epsilon>/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 \<equiv> 2 * Max{Nx,Ny,Nxy}"
+ show "\<exists>N. \<forall>n n'. N \<le> n \<longrightarrow> N \<le> n' \<longrightarrow> 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)) < \<epsilon>"
+ proof (intro exI strip)
+ fix n n'
+ assume "N \<le> n" and "N \<le> n'"
+ then have "n div 2 \<ge> Nx" "n div 2 \<ge> Ny" "n div 2 \<ge> Nxy" "n' div 2 \<ge> Nx" "n' div 2 \<ge> Ny"
+ by (auto simp: N_def)
+ then have dxyn: "d (x (n div 2)) (y (n div 2)) < \<epsilon>/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) \<in> M" "x (n' div 2) \<in> M""y (n div 2) \<in> M" "y (n' div 2) \<in> M"
+ using Metric_space.MCauchy_def Metric_space_axioms 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)) < \<epsilon>"
+ 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 (\<lambda>n. if even n then \<sigma>(n div 2) else a) \<longleftrightarrow>
+ range \<sigma> \<subseteq> M \<and> limitin mtopology \<sigma> a sequentially" (is "?lhs=?rhs")
+proof -
+ have "?lhs \<longleftrightarrow> (MCauchy \<sigma> \<and> a \<in> M \<and> (\<lambda>n. d (\<sigma> n) a) \<longlonglongrightarrow> 0)"
+ by (simp add: MCauchy_interleaving_gen [where y = "\<lambda>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 \<longleftrightarrow>
+ (\<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 \<Rightarrow> 'a set"
+ assume clo: "\<forall>n. closedin mtopology (C n)"
+ and ne: "\<forall>n. C n \<noteq> ({}::'a set)"
+ and dec: "decseq C"
+ and cover [rule_format]: "\<forall>\<epsilon>>0. \<exists>n a. C n \<subseteq> mcball a \<epsilon>"
+ obtain \<sigma> where \<sigma>: "\<And>n. \<sigma> n \<in> C n"
+ by (meson ne empty_iff set_eq_iff)
+ have "MCauchy \<sigma>"
+ unfolding MCauchy_def
+ proof (intro conjI strip)
+ show "range \<sigma> \<subseteq> M"
+ using \<sigma> clo metric_closedin_iff_sequentially_closed by auto
+ fix \<epsilon> :: real
+ assume "\<epsilon> > 0"
+ then obtain N a where N: "C N \<subseteq> mcball a (\<epsilon>/3)"
+ using cover by fastforce
+ have "d (\<sigma> m) (\<sigma> n) < \<epsilon>" if "N \<le> m" "N \<le> n" for m n
+ proof -
+ have "d a (\<sigma> m) \<le> \<epsilon>/3" "d a (\<sigma> n) \<le> \<epsilon>/3"
+ using dec N \<sigma> that by (fastforce simp: decseq_def)+
+ then have "d (\<sigma> m) (\<sigma> n) \<le> \<epsilon>/3 + \<epsilon>/3"
+ using triangle \<sigma> commute dec decseq_def subsetD that N
+ by (smt (verit, ccfv_threshold) in_mcball)
+ also have "... < \<epsilon>"
+ using \<open>\<epsilon> > 0\<close> by auto
+ finally show ?thesis .
+ qed
+ then show "\<exists>N. \<forall>m n. N \<le> m \<longrightarrow> N \<le> n \<longrightarrow> d (\<sigma> m) (\<sigma> n) < \<epsilon>"
+ by blast
+ qed
+ then obtain x where x: "limitin mtopology \<sigma> x sequentially"
+ using L mcomplete_def by blast
+ have "x \<in> C n" for n
+ proof (rule limitin_closedin [OF x])
+ show "closedin mtopology (C n)"
+ by (simp add: clo)
+ show "\<forall>\<^sub>F x in sequentially. \<sigma> x \<in> C n"
+ by (metis \<sigma> dec decseq_def eventually_sequentiallyI subsetD)
+ qed auto
+ then show "\<Inter> (range C) \<noteq> {}"
+ by blast
+qed
+next
+ assume R: ?rhs
+ show ?lhs
+ unfolding mcomplete_def
+ proof (intro strip)
+ fix \<sigma>
+ assume "MCauchy \<sigma>"
+ then have "range \<sigma> \<subseteq> M"
+ using MCauchy_def by blast
+ define C where "C \<equiv> \<lambda>n. mtopology closure_of (\<sigma> ` {n..})"
+ have "\<forall>n. closedin mtopology (C n)"
+ by (auto simp: C_def)
+ moreover
+ have ne: "\<And>n. C n \<noteq> {}"
+ 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 \<le> n"
+ then have "{n..} \<subseteq> {m..}"
+ by auto
+ then show "C n \<subseteq> C m"
+ unfolding C_def by (meson closure_of_mono image_mono)
+ qed
+ moreover
+ have C: "\<exists>N u. C N \<subseteq> mcball u \<epsilon>" if "\<epsilon>>0" for \<epsilon>
+ proof -
+ obtain N where "\<And>m n. N \<le> m \<and> N \<le> n \<Longrightarrow> d (\<sigma> m) (\<sigma> n) < \<epsilon>"
+ by (meson MCauchy_def \<open>0 < \<epsilon>\<close> \<open>MCauchy \<sigma>\<close>)
+ then have "\<sigma> ` {N..} \<subseteq> mcball (\<sigma> N) \<epsilon>"
+ using MCauchy_def \<open>MCauchy \<sigma>\<close> by (force simp: less_eq_real_def)
+ then have "C N \<subseteq> mcball (\<sigma> N) \<epsilon>"
+ by (simp add: C_def closure_of_minimal)
+ then show ?thesis
+ by blast
+ qed
+ ultimately obtain l where x: "l \<in> \<Inter> (range C)"
+ by (metis R ex_in_conv)
+ then have *: "\<And>\<epsilon> N. 0 < \<epsilon> \<Longrightarrow> \<exists>n'. N \<le> n' \<and> l \<in> M \<and> \<sigma> n' \<in> M \<and> d l (\<sigma> n') < \<epsilon>"
+ by (force simp: C_def metric_closure_of)
+ then have "l \<in> M"
+ using gt_ex by blast
+ show "\<exists>l. limitin mtopology \<sigma> l sequentially"
+ unfolding limitin_metric
+ proof (intro conjI strip exI)
+ show "l \<in> M"
+ using \<open>\<forall>n. closedin mtopology (C n)\<close> closedin_subset x by fastforce
+ fix \<epsilon>::real
+ assume "\<epsilon> > 0"
+ obtain N where N: "\<And>m n. N \<le> m \<and> N \<le> n \<Longrightarrow> d (\<sigma> m) (\<sigma> n) < \<epsilon>/2"
+ by (meson MCauchy_def \<open>0 < \<epsilon>\<close> \<open>MCauchy \<sigma>\<close> half_gt_zero)
+ with * [of "\<epsilon>/2" N]
+ have "\<forall>n\<ge>N. \<sigma> n \<in> M \<and> d (\<sigma> n) l < \<epsilon>"
+ by (smt (verit) \<open>range \<sigma> \<subseteq> M\<close> commute field_sum_of_halves range_subsetD triangle)
+ then show "\<forall>\<^sub>F n in sequentially. \<sigma> n \<in> M \<and> d (\<sigma> n) l < \<epsilon>"
+ using eventually_sequentially by blast
+ qed
+ qed
+qed
+
+
+lemma mcomplete_nest_sing:
+ "mcomplete \<longleftrightarrow>
+ (\<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: "\<forall>n. closedin mtopology (C n)"
+ and cover: "\<forall>\<epsilon>>0. \<exists>n a. C n \<subseteq> mcball a \<epsilon>"
+ and no_sing: "\<And>y. y \<in> M \<Longrightarrow> \<Inter> (range C) \<noteq> {y}"
+ and l: "\<forall>n. l \<in> C n"
+ for C :: "nat \<Rightarrow> 'a set" and l
+ proof -
+ have inM: "\<And>x. x \<in> \<Inter> (range C) \<Longrightarrow> x \<in> M"
+ using closedin_metric clo by fastforce
+ then have "l \<in> M"
+ by (simp add: l)
+ have False if l': "l' \<in> \<Inter> (range C)" and "l' \<noteq> l" for l'
+ proof -
+ have "l' \<in> M"
+ using inM l' by blast
+ obtain n a where na: "C n \<subseteq> 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 \<le> (d l l' / 3)" "d a l' \<le> (d l l' / 3)" "a \<in> M"
+ using l l' na in_mcball by auto
+ then have "d l l' \<le> (d l l' / 3) + (d l l' / 3)"
+ using \<open>l \<in> M\<close> \<open>l' \<in> M\<close> mdist_reverse_triangle by fastforce
+ then show False
+ using nonneg [of l l'] \<open>l' \<noteq> l\<close> \<open>l \<in> M\<close> \<open>l' \<in> M\<close> 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 \<longleftrightarrow>
+ (\<forall>\<C>. (\<forall>C \<in> \<C>. closedin mtopology C) \<and>
+ (\<forall>e>0. \<exists>C a. C \<in> \<C> \<and> C \<subseteq> mcball a e) \<and> (\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<C> \<longrightarrow> \<Inter> \<F> \<noteq> {})
+ \<longrightarrow> \<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: "\<forall>C\<in>\<C>. closedin mtopology C"
+ and cover: "\<forall>e>0. \<exists>C a. C \<in> \<C> \<and> C \<subseteq> mcball a e"
+ and fip: "\<forall>\<F>. finite \<F> \<longrightarrow> \<F> \<subseteq> \<C> \<longrightarrow> \<Inter> \<F> \<noteq> {}"
+ then have "\<forall>n. \<exists>C. C \<in> \<C> \<and> (\<exists>a. C \<subseteq> mcball a (inverse (Suc n)))"
+ by simp
+ then obtain C where C: "\<And>n. C n \<in> \<C>"
+ and coverC: "\<And>n. \<exists>a. C n \<subseteq> mcball a (inverse (Suc n))"
+ by metis
+ define D where "D \<equiv> \<lambda>n. \<Inter> (C ` {..n})"
+ have cloD: "closedin mtopology (D n)" for n
+ unfolding D_def using clo C by blast
+ have neD: "D n \<noteq> {}" 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: "\<exists>n a. D n \<subseteq> mcball a \<epsilon>" if " \<epsilon> >0" for \<epsilon>
+ proof -
+ obtain n where "inverse (Suc n) < \<epsilon>"
+ using \<open>0 < \<epsilon>\<close> reals_Archimedean by blast
+ then obtain a where "C n \<subseteq> mcball a \<epsilon>"
+ by (meson coverC less_eq_real_def mcball_subset_concentric order_trans)
+ then show ?thesis
+ unfolding D_def by blast
+ qed
+ have *: "a \<in> \<Inter>\<C>" if a: "\<Inter> (range D) = {a}" and "a \<in> M" for a
+ proof -
+ have aC: "a \<in> C n" for n
+ using that by (auto simp: D_def)
+ have eqa: "\<And>u. (\<forall>n. u \<in> C n) \<Longrightarrow> a = u"
+ using that by (auto simp: D_def)
+ have "a \<in> T" if "T \<in> \<C>" for T
+ proof -
+ have cloT: "closedin mtopology (T \<inter> D n)" for n
+ using clo cloD that by blast
+ have "\<Inter> (insert T (C ` {..n})) \<noteq> {}" for n
+ using that C by (intro fip [rule_format]) auto
+ then have neT: "T \<inter> D n \<noteq> {}" for n
+ by (simp add: D_def)
+ have decT: "decseq (\<lambda>n. T \<inter> D n)"
+ by (force simp: D_def decseq_def)
+ have coverT: "\<exists>n a. T \<inter> D n \<subseteq> mcball a \<epsilon>" if " \<epsilon> >0" for \<epsilon>
+ by (meson coverD le_infI2 that)
+ show ?thesis
+ using L [unfolded mcomplete_nest_sing, rule_format, of "\<lambda>n. T \<inter> D n"] a
+ by (force simp: cloT neT decT coverT)
+ qed
+ then show ?thesis by auto
+ qed
+ show "\<Inter> \<C> \<noteq> {}"
+ by (metis L cloD neD decD coverD * empty_iff mcomplete_nest_sing)
+ qed
+next
+ assume R [rule_format]: ?rhs
+ show ?lhs
+ unfolding mcomplete_nest imp_conjL
+ proof (intro strip)
+ fix C :: "nat \<Rightarrow> 'a set"
+ assume clo: "\<forall>n. closedin mtopology (C n)"
+ and ne: "\<forall>n. C n \<noteq> {}"
+ and dec: "decseq C"
+ and cover: "\<forall>\<epsilon>>0. \<exists>n a. C n \<subseteq> mcball a \<epsilon>"
+ have "\<Inter>(C ` N) \<noteq> {}" if "finite N" for N
+ proof -
+ obtain k where "N \<subseteq> {..k}"
+ using \<open>finite N\<close> finite_nat_iff_bounded_le by auto
+ with dec have "C k \<subseteq> \<Inter>(C ` N)" by (auto simp: decseq_def)
+ then show ?thesis
+ using ne by force
+ qed
+ with clo cover R [of "range C"] show "\<Inter> (range C) \<noteq> {}"
+ by (metis (no_types, opaque_lifting) finite_subset_image image_iff UNIV_I)
+ qed
+qed
+
+
+lemma mcomplete_fip_sing:
+ "mcomplete \<longleftrightarrow>
+ (\<forall>\<C>. (\<forall>C\<in>\<C>. closedin mtopology C) \<and>
+ (\<forall>e>0. \<exists>c a. c \<in> \<C> \<and> c \<subseteq> mcball a e) \<and>
+ (\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<C> \<longrightarrow> \<Inter> \<F> \<noteq> {}) \<longrightarrow>
+ (\<exists>l. l \<in> M \<and> \<Inter> \<C> = {l}))"
+ (is "?lhs = ?rhs")
+proof
+ have *: "l \<in> M" "\<Inter> \<C> = {l}"
+ if clo: "Ball \<C> (closedin mtopology)"
+ and cover: "\<forall>e>0. \<exists>C a. C \<in> \<C> \<and> C \<subseteq> mcball a e"
+ and fin: "\<forall>\<F>. finite \<F> \<longrightarrow> \<F> \<subseteq> \<C> \<longrightarrow> \<Inter> \<F> \<noteq> {}"
+ and l: "l \<in> \<Inter> \<C>"
+ for \<C> :: "'a set set" and l
+ proof -
+ show "l \<in> M"
+ by (meson Inf_lower2 clo cover gt_ex metric_closedin_iff_sequentially_closed subsetD that(4))
+ show "\<Inter> \<C> = {l}"
+ proof (cases "\<C> = {}")
+ case True
+ then show ?thesis
+ using cover mbounded_pos by auto
+ next
+ case False
+ have CM: "\<And>a. a \<in> \<Inter>\<C> \<Longrightarrow> a \<in> M"
+ using False clo closedin_subset by fastforce
+ have "l' \<notin> \<Inter> \<C>" if "l' \<noteq> l" for l'
+ proof
+ assume l': "l' \<in> \<Inter> \<C>"
+ with CM have "l' \<in> M" by blast
+ with that \<open>l \<in> M\<close> have gt0: "0 < d l l'"
+ by simp
+ then obtain C a where "C \<in> \<C>" and C: "C \<subseteq> mcball a (d l l' / 3)"
+ using cover [rule_format, of "d l l' / 3"] by auto
+ then have "d a l \<le> (d l l' / 3)" "d a l' \<le> (d l l' / 3)" "a \<in> M"
+ using l l' in_mcball by auto
+ then have "d l l' \<le> (d l l' / 3) + (d l l' / 3)"
+ using \<open>l \<in> M\<close> \<open>l' \<in> M\<close> mdist_reverse_triangle by fastforce
+ with gt0 show False by auto
+ qed
+ then show ?thesis
+ using l by fastforce
+ qed
+ qed
+ assume L: ?lhs
+ with * show ?rhs
+ unfolding mcomplete_fip imp_conjL ex_in_conv [symmetric]
+ by (elim all_forward imp_forward2 asm_rl) (blast intro: elim: )
+next
+ assume ?rhs then show ?lhs
+ unfolding mcomplete_fip by (force elim!: all_forward)
+qed
+
+end
+
+lemma MCauchy_iff_Cauchy [iff]: "Met_TC.MCauchy = Cauchy"
+ by (force simp: Cauchy_def Met_TC.MCauchy_def)
+
+lemma mcomplete_iff_complete [iff]:
+ "Met_TC.mcomplete (Pure.type ::'a::metric_space itself) \<longleftrightarrow> complete (UNIV::'a set)"
+ by (auto simp: Met_TC.mcomplete_def complete_def)
+
+lemma euclidean_metric: "Met_TC.mcomplete (Pure.type ::'a::euclidean_space itself)"
+ using complete_UNIV mcomplete_iff_complete by blast
+
+context submetric
+begin
+
+lemma MCauchy_submetric:
+ "sub.MCauchy \<sigma> \<longleftrightarrow> range \<sigma> \<subseteq> A \<and> MCauchy \<sigma>"
+ using MCauchy_def sub.MCauchy_def subset by force
+
+lemma closedin_mcomplete_imp_mcomplete:
+ assumes clo: "closedin mtopology A" and "mcomplete"
+ shows "sub.mcomplete"
+ unfolding sub.mcomplete_def
+proof (intro strip)
+ fix \<sigma>
+ assume "sub.MCauchy \<sigma>"
+ then have \<sigma>: "MCauchy \<sigma>" "range \<sigma> \<subseteq> A"
+ using MCauchy_submetric by blast+
+ then obtain x where x: "limitin mtopology \<sigma> x sequentially"
+ using \<open>mcomplete\<close> unfolding mcomplete_def by blast
+ then have "x \<in> A"
+ using \<sigma> clo metric_closedin_iff_sequentially_closed by force
+ with \<sigma> x show "\<exists>x. limitin sub.mtopology \<sigma> x sequentially"
+ using limitin_submetric_iff range_subsetD by fastforce
+qed
+
+
+lemma sequentially_closedin_mcomplete_imp_mcomplete:
+ assumes "mcomplete" and "\<And>\<sigma> l. range \<sigma> \<subseteq> A \<and> limitin mtopology \<sigma> l sequentially \<Longrightarrow> l \<in> A"
+ shows "sub.mcomplete"
+ using assms closedin_mcomplete_imp_mcomplete metric_closedin_iff_sequentially_closed subset by blast
+
+end
+
+
+context Metric_space
+begin
+
+lemma mcomplete_Un:
+ assumes A: "submetric M d A" "Metric_space.mcomplete A d"
+ and B: "submetric M d B" "Metric_space.mcomplete B d"
+ shows "submetric M d (A \<union> B)" "Metric_space.mcomplete (A \<union> B) d"
+proof -
+ show "submetric M d (A \<union> B)"
+ by (meson assms le_sup_iff submetric_axioms_def submetric_def)
+ then interpret MAB: Metric_space "A \<union> B" d
+ by (meson submetric.subset subspace)
+ interpret MA: Metric_space A d
+ by (meson A submetric.subset subspace)
+ interpret MB: Metric_space B d
+ by (meson B submetric.subset subspace)
+ show "Metric_space.mcomplete (A \<union> B) d"
+ unfolding MAB.mcomplete_def
+ proof (intro strip)
+ fix \<sigma>
+ assume "MAB.MCauchy \<sigma>"
+ then have "range \<sigma> \<subseteq> A \<union> B"
+ using MAB.MCauchy_def by blast
+ then have "UNIV \<subseteq> \<sigma> -` A \<union> \<sigma> -` B"
+ by blast
+ then consider "infinite (\<sigma> -` A)" | "infinite (\<sigma> -` B)"
+ using finite_subset by auto
+ then show "\<exists>x. limitin MAB.mtopology \<sigma> x sequentially"
+ proof cases
+ case 1
+ then obtain r where "strict_mono r" and r: "\<And>n::nat. r n \<in> \<sigma> -` A"
+ using infinite_enumerate by blast
+ then have "MA.MCauchy (\<sigma> \<circ> r)"
+ using MA.MCauchy_def MAB.MCauchy_def MAB.MCauchy_subsequence \<open>MAB.MCauchy \<sigma>\<close> by auto
+ with A obtain x where "limitin MA.mtopology (\<sigma> \<circ> r) x sequentially"
+ using MA.mcomplete_def by blast
+ then have "limitin MAB.mtopology (\<sigma> \<circ> r) x sequentially"
+ by (metis MA.limit_metric_sequentially MAB.limit_metric_sequentially UnCI)
+ then show ?thesis
+ using MAB.MCauchy_convergent_subsequence \<open>MAB.MCauchy \<sigma>\<close> \<open>strict_mono r\<close> by blast
+ next
+ case 2
+ then obtain r where "strict_mono r" and r: "\<And>n::nat. r n \<in> \<sigma> -` B"
+ using infinite_enumerate by blast
+ then have "MB.MCauchy (\<sigma> \<circ> r)"
+ using MB.MCauchy_def MAB.MCauchy_def MAB.MCauchy_subsequence \<open>MAB.MCauchy \<sigma>\<close> by auto
+ with B obtain x where "limitin MB.mtopology (\<sigma> \<circ> r) x sequentially"
+ using MB.mcomplete_def by blast
+ then have "limitin MAB.mtopology (\<sigma> \<circ> r) x sequentially"
+ by (metis MB.limit_metric_sequentially MAB.limit_metric_sequentially UnCI)
+ then show ?thesis
+ using MAB.MCauchy_convergent_subsequence \<open>MAB.MCauchy \<sigma>\<close> \<open>strict_mono r\<close> by blast
+ qed
+ qed
+qed
+
+lemma mcomplete_Union:
+ assumes "finite \<S>"
+ and "\<And>A. A \<in> \<S> \<Longrightarrow> submetric M d A" "\<And>A. A \<in> \<S> \<Longrightarrow> Metric_space.mcomplete A d"
+ shows "submetric M d (\<Union>\<S>)" "Metric_space.mcomplete (\<Union>\<S>) d"
+ using assms
+ by (induction rule: finite_induct) (auto simp: mcomplete_Un)
+
+lemma mcomplete_Inter:
+ assumes "finite \<S>" "\<S> \<noteq> {}"
+ and sub: "\<And>A. A \<in> \<S> \<Longrightarrow> submetric M d A"
+ and comp: "\<And>A. A \<in> \<S> \<Longrightarrow> Metric_space.mcomplete A d"
+ shows "submetric M d (\<Inter>\<S>)" "Metric_space.mcomplete (\<Inter>\<S>) d"
+proof -
+ show "submetric M d (\<Inter>\<S>)"
+ using assms unfolding submetric_def submetric_axioms_def
+ by (metis Inter_lower equals0I inf.orderE le_inf_iff)
+ then interpret MS: submetric M d "\<Inter>\<S>"
+ by (meson submetric.subset subspace)
+ show "Metric_space.mcomplete (\<Inter>\<S>) d"
+ unfolding MS.sub.mcomplete_def
+ proof (intro strip)
+ fix \<sigma>
+ assume "MS.sub.MCauchy \<sigma>"
+ then have "range \<sigma> \<subseteq> \<Inter>\<S>"
+ using MS.MCauchy_submetric by blast
+ obtain A where "A \<in> \<S>" and A: "Metric_space.mcomplete A d"
+ using assms by blast
+ then have "range \<sigma> \<subseteq> A"
+ using \<open>range \<sigma> \<subseteq> \<Inter>\<S>\<close> by blast
+ interpret SA: submetric M d A
+ by (meson \<open>A \<in> \<S>\<close> sub submetric.subset subspace)
+ have "MCauchy \<sigma>"
+ using MS.MCauchy_submetric \<open>MS.sub.MCauchy \<sigma>\<close> by blast
+ then obtain x where x: "limitin SA.sub.mtopology \<sigma> x sequentially"
+ by (metis A SA.sub.MCauchy_def SA.sub.mcomplete_alt MCauchy_def \<open>range \<sigma> \<subseteq> A\<close>)
+ show "\<exists>x. limitin MS.sub.mtopology \<sigma> x sequentially"
+ apply (rule_tac x="x" in exI)
+ unfolding MS.limitin_submetric_iff
+ proof (intro conjI)
+ show "x \<in> \<Inter> \<S>"
+ proof clarsimp
+ fix U
+ assume "U \<in> \<S>"
+ interpret SU: submetric M d U
+ by (meson \<open>U \<in> \<S>\<close> sub submetric.subset subspace)
+ have "range \<sigma> \<subseteq> U"
+ using \<open>U \<in> \<S>\<close> \<open>range \<sigma> \<subseteq> \<Inter> \<S>\<close> by blast
+ moreover have "Metric_space.mcomplete U d"
+ by (simp add: \<open>U \<in> \<S>\<close> comp)
+ ultimately obtain x' where x': "limitin SU.sub.mtopology \<sigma> x' sequentially"
+ using MCauchy_def SU.sub.MCauchy_def SU.sub.mcomplete_alt \<open>MCauchy \<sigma>\<close> by meson
+ have "x' = x"
+ proof (intro limitin_metric_unique)
+ show "limitin mtopology \<sigma> x' sequentially"
+ by (meson SU.submetric_axioms submetric.limitin_submetric_iff x')
+ show "limitin mtopology \<sigma> x sequentially"
+ by (meson SA.submetric_axioms submetric.limitin_submetric_iff x)
+ qed auto
+ then show "x \<in> U"
+ using SU.sub.limitin_mspace x' by blast
+ qed
+ show "\<forall>\<^sub>F n in sequentially. \<sigma> n \<in> \<Inter>\<S>"
+ by (meson \<open>range \<sigma> \<subseteq> \<Inter> \<S>\<close> always_eventually range_subsetD)
+ show "limitin mtopology \<sigma> x sequentially"
+ by (meson SA.submetric_axioms submetric.limitin_submetric_iff x)
+ qed
+ qed
+qed
+
+
+lemma mcomplete_Int:
+ assumes A: "submetric M d A" "Metric_space.mcomplete A d"
+ and B: "submetric M d B" "Metric_space.mcomplete B d"
+ shows "submetric M d (A \<inter> B)" "Metric_space.mcomplete (A \<inter> B) d"
+ using mcomplete_Inter [of "{A,B}"] assms by force+
+
+subsection\<open>Totally bounded subsets of metric spaces\<close>
+
+definition mtotally_bounded
+ where "mtotally_bounded S \<equiv> \<forall>\<epsilon>>0. \<exists>K. finite K \<and> K \<subseteq> S \<and> S \<subseteq> (\<Union>x\<in>K. mball x \<epsilon>)"
+
+lemma mtotally_bounded_empty [iff]: "mtotally_bounded {}"
+by (simp add: mtotally_bounded_def)
+
+lemma finite_imp_mtotally_bounded:
+ "\<lbrakk>finite S; S \<subseteq> M\<rbrakk> \<Longrightarrow> mtotally_bounded S"
+ by (auto simp: mtotally_bounded_def)
+
+lemma mtotally_bounded_imp_subset: "mtotally_bounded S \<Longrightarrow> S \<subseteq> M"
+ by (force simp: mtotally_bounded_def intro!: zero_less_one)
+
+lemma mtotally_bounded_sing [simp]:
+ "mtotally_bounded {x} \<longleftrightarrow> x \<in> M"
+ by (meson empty_subsetI finite.simps finite_imp_mtotally_bounded insert_subset mtotally_bounded_imp_subset)
+
+lemma mtotally_bounded_Un:
+ assumes "mtotally_bounded S" "mtotally_bounded T"
+ shows "mtotally_bounded (S \<union> T)"
+proof -
+ have "\<exists>K. finite K \<and> K \<subseteq> S \<union> T \<and> S \<union> T \<subseteq> (\<Union>x\<in>K. mball x e)"
+ if "e>0" and K: "finite K \<and> K \<subseteq> S \<and> S \<subseteq> (\<Union>x\<in>K. mball x e)"
+ and L: "finite L \<and> L \<subseteq> T \<and> T \<subseteq> (\<Union>x\<in>L. mball x e)" for K L e
+ using that by (rule_tac x="K \<union> L" in exI) auto
+ with assms show ?thesis
+ unfolding mtotally_bounded_def by presburger
+qed
+
+lemma mtotally_bounded_Union:
+ assumes "finite f" "\<And>S. S \<in> f \<Longrightarrow> mtotally_bounded S"
+ shows "mtotally_bounded (\<Union>f)"
+ using assms by (induction f) (auto simp: mtotally_bounded_Un)
+
+lemma mtotally_bounded_imp_mbounded:
+ assumes "mtotally_bounded S"
+ shows "mbounded S"
+proof -
+ obtain K where "finite K \<and> K \<subseteq> S \<and> S \<subseteq> (\<Union>x\<in>K. mball x 1)"
+ using assms by (force simp: mtotally_bounded_def)
+ then show ?thesis
+ by (smt (verit) finite_imageI image_iff mbounded_Union mbounded_mball mbounded_subset)
+qed
+
+
+lemma mtotally_bounded_sequentially:
+ "mtotally_bounded S \<longleftrightarrow>
+ S \<subseteq> M \<and> (\<forall>\<sigma>::nat \<Rightarrow> 'a. range \<sigma> \<subseteq> S \<longrightarrow> (\<exists>r. strict_mono r \<and> MCauchy (\<sigma> \<circ> r)))"
+ (is "_ \<longleftrightarrow> _ \<and> ?rhs")
+proof (cases "S \<subseteq> M")
+ case True
+ show ?thesis
+ proof -
+ { fix \<sigma> :: "nat \<Rightarrow> 'a"
+ assume L: "mtotally_bounded S" and \<sigma>: "range \<sigma> \<subseteq> S"
+ have "\<exists>j > i. d (\<sigma> i) (\<sigma> j) < 3*\<epsilon>/2 \<and> infinite (\<sigma> -` mball (\<sigma> j) (\<epsilon>/2))"
+ if inf: "infinite (\<sigma> -` mball (\<sigma> i) \<epsilon>)" and "\<epsilon> > 0" for i \<epsilon>
+ proof -
+ obtain K where "finite K" "K \<subseteq> S" and K: "S \<subseteq> (\<Union>x\<in>K. mball x (\<epsilon>/4))"
+ by (metis L mtotally_bounded_def \<open>\<epsilon> > 0\<close> zero_less_divide_iff zero_less_numeral)
+ then have K_imp_ex: "\<And>y. y \<in> S \<Longrightarrow> \<exists>x\<in>K. d x y < \<epsilon>/4"
+ by fastforce
+ have False if "\<forall>x\<in>K. d x (\<sigma> i) < \<epsilon> + \<epsilon>/4 \<longrightarrow> finite (\<sigma> -` mball x (\<epsilon>/4))"
+ proof -
+ have "\<exists>w. w \<in> K \<and> d w (\<sigma> i) < 5 * \<epsilon>/4 \<and> d w (\<sigma> j) < \<epsilon>/4"
+ if "d (\<sigma> i) (\<sigma> j) < \<epsilon>" for j
+ proof -
+ obtain w where w: "d w (\<sigma> j) < \<epsilon>/4" "w \<in> K"
+ using K_imp_ex \<sigma> by blast
+ then have "d w (\<sigma> i) < \<epsilon> + \<epsilon>/4"
+ by (smt (verit, ccfv_SIG) True \<open>K \<subseteq> S\<close> \<sigma> rangeI subset_eq that triangle')
+ with w show ?thesis
+ using in_mball by auto
+ qed
+ then have "(\<sigma> -` mball (\<sigma> i) \<epsilon>) \<subseteq> (\<Union>x\<in>K. if d x (\<sigma> i) < \<epsilon> + \<epsilon>/4 then \<sigma> -` mball x (\<epsilon>/4) else {})"
+ using True \<open>K \<subseteq> S\<close> by force
+ then show False
+ using finite_subset inf \<open>finite K\<close> that by fastforce
+ qed
+ then obtain x where "x \<in> K" and dxi: "d x (\<sigma> i) < \<epsilon> + \<epsilon>/4" and infx: "infinite (\<sigma> -` mball x (\<epsilon>/4))"
+ by blast
+ then obtain j where "j \<in> (\<sigma> -` mball x (\<epsilon>/4)) - {..i}"
+ using bounded_nat_set_is_finite by (meson Diff_infinite_finite finite_atMost)
+ then have "j > i" and dxj: "d x (\<sigma> j) < \<epsilon>/4"
+ by auto
+ have "(\<sigma> -` mball x (\<epsilon>/4)) \<subseteq> (\<sigma> -` mball y (\<epsilon>/2))" if "d x y < \<epsilon>/4" "y \<in> M" for y
+ using that by (simp add: mball_subset Metric_space_axioms vimage_mono)
+ then have infj: "infinite (\<sigma> -` mball (\<sigma> j) (\<epsilon>/2))"
+ by (meson True \<open>d x (\<sigma> j) < \<epsilon>/4\<close> \<sigma> in_mono infx rangeI finite_subset)
+ have "\<sigma> i \<in> M" "\<sigma> j \<in> M" "x \<in> M"
+ using True \<open>K \<subseteq> S\<close> \<open>x \<in> K\<close> \<sigma> by force+
+ then have "d (\<sigma> i) (\<sigma> j) \<le> d x (\<sigma> i) + d x (\<sigma> j)"
+ using triangle'' by blast
+ also have "\<dots> < 3*\<epsilon>/2"
+ using dxi dxj by auto
+ finally have "d (\<sigma> i) (\<sigma> j) < 3*\<epsilon>/2" .
+ with \<open>i < j\<close> infj show ?thesis by blast
+ qed
+ then obtain nxt where nxt: "\<And>i \<epsilon>. \<lbrakk>\<epsilon> > 0; infinite (\<sigma> -` mball (\<sigma> i) \<epsilon>)\<rbrakk> \<Longrightarrow>
+ nxt i \<epsilon> > i \<and> d (\<sigma> i) (\<sigma> (nxt i \<epsilon>)) < 3*\<epsilon>/2 \<and> infinite (\<sigma> -` mball (\<sigma> (nxt i \<epsilon>)) (\<epsilon>/2))"
+ by metis
+ have "mbounded S"
+ using L by (simp add: mtotally_bounded_imp_mbounded)
+ then obtain B where B: "\<forall>y \<in> S. d (\<sigma> 0) y \<le> B" and "B > 0"
+ by (meson \<sigma> mbounded_alt_pos range_subsetD)
+ define eps where "eps \<equiv> \<lambda>n. (B+1) / 2^n"
+ have [simp]: "eps (Suc n) = eps n / 2" "eps n > 0" for n
+ using \<open>B > 0\<close> by (auto simp: eps_def)
+ have "UNIV \<subseteq> \<sigma> -` mball (\<sigma> 0) (B+1)"
+ using B True \<sigma> unfolding image_iff subset_iff
+ by (smt (verit, best) UNIV_I in_mball vimageI)
+ then have inf0: "infinite (\<sigma> -` mball (\<sigma> 0) (eps 0))"
+ using finite_subset by (auto simp: eps_def)
+ define r where "r \<equiv> rec_nat 0 (\<lambda>n rec. nxt rec (eps n))"
+ have [simp]: "r 0 = 0" "r (Suc n) = nxt (r n) (eps n)" for n
+ by (auto simp: r_def)
+ have \<sigma>rM[simp]: "\<sigma> (r n) \<in> M" for n
+ using True \<sigma> by blast
+ have inf: "infinite (\<sigma> -` mball (\<sigma> (r n)) (eps n))" for n
+ proof (induction n)
+ case 0 then show ?case
+ by (simp add: inf0)
+ next
+ case (Suc n) then show ?case
+ using nxt [of "eps n" "r n"] by simp
+ qed
+ then have "r (Suc n) > r n" for n
+ by (simp add: nxt)
+ then have "strict_mono r"
+ by (simp add: strict_mono_Suc_iff)
+ have d_less: "d (\<sigma> (r n)) (\<sigma> (r (Suc n))) < 3 * eps n / 2" for n
+ using nxt [OF _ inf] by simp
+ have eps_plus: "eps (k + n) = eps n * (1/2)^k" for k n
+ by (simp add: eps_def power_add field_simps)
+ have *: "d (\<sigma> (r n)) (\<sigma> (r (k + n))) < 3 * eps n" for n k
+ proof -
+ have "d (\<sigma> (r n)) (\<sigma> (r (k+n))) \<le> 3/2 * eps n * (\<Sum>i<k. (1/2)^i)"
+ proof (induction k)
+ case 0 then show ?case
+ by simp
+ next
+ case (Suc k)
+ have "d (\<sigma> (r n)) (\<sigma> (r (Suc k + n))) \<le> d (\<sigma> (r n)) (\<sigma> (r (k + n))) + d (\<sigma> (r (k + n))) (\<sigma> (r (Suc (k + n))))"
+ by (metis \<sigma>rM add.commute add_Suc_right triangle)
+ with d_less[of "k+n"] Suc show ?case
+ by (simp add: algebra_simps eps_plus)
+ qed
+ also have "\<dots> < 3/2 * eps n * 2"
+ using geometric_sum [of "1/2::real" k] by simp
+ finally show ?thesis by simp
+ qed
+ have "\<exists>N. \<forall>n\<ge>N. \<forall>n'\<ge>N. d (\<sigma> (r n)) (\<sigma> (r n')) < \<epsilon>" if "\<epsilon> > 0" for \<epsilon>
+ proof -
+ define N where "N \<equiv> nat \<lceil>(log 2 (6*(B+1) / \<epsilon>))\<rceil>"
+ have \<section>: "b \<le> 2 ^ nat \<lceil>log 2 b\<rceil>" for b
+ by (smt (verit) less_log_of_power real_nat_ceiling_ge)
+ have N: "6 * eps N \<le> \<epsilon>"
+ using \<section> [of "(6*(B+1) / \<epsilon>)"] that by (auto simp: N_def eps_def field_simps)
+ have "d (\<sigma> (r N)) (\<sigma> (r n)) < 3 * eps N" if "n \<ge> N" for n
+ by (metis * add.commute nat_le_iff_add that)
+ then have "\<forall>n\<ge>N. \<forall>n'\<ge>N. d (\<sigma> (r n)) (\<sigma> (r n')) < 3 * eps N + 3 * eps N"
+ by (smt (verit, best) \<sigma>rM triangle'')
+ with N show ?thesis
+ by fastforce
+ qed
+ then have "MCauchy (\<sigma> \<circ> r)"
+ unfolding MCauchy_def using True \<sigma> by auto
+ then have "\<exists>r. strict_mono r \<and> MCauchy (\<sigma> \<circ> r)"
+ using \<open>strict_mono r\<close> by blast
+ }
+ moreover
+ { assume R: ?rhs
+ have "mtotally_bounded S"
+ unfolding mtotally_bounded_def
+ proof (intro strip)
+ fix \<epsilon> :: real
+ assume "\<epsilon> > 0"
+ have False if \<section>: "\<And>K. \<lbrakk>finite K; K \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>s\<in>S. s \<notin> (\<Union>x\<in>K. mball x \<epsilon>)"
+ proof -
+ obtain f where f: "\<And>K. \<lbrakk>finite K; K \<subseteq> S\<rbrakk> \<Longrightarrow> f K \<in> S \<and> f K \<notin> (\<Union>x\<in>K. mball x \<epsilon>)"
+ using \<section> by metis
+ define \<sigma> where "\<sigma> \<equiv> wfrec less_than (\<lambda>seq n. f (seq ` {..<n}))"
+ have \<sigma>_eq: "\<sigma> n = f (\<sigma> ` {..<n})" for n
+ by (simp add: cut_apply def_wfrec [OF \<sigma>_def])
+ have [simp]: "\<sigma> n \<in> S" for n
+ using wf_less_than
+ proof (induction n rule: wf_induct_rule)
+ case (less n) with f show ?case
+ by (auto simp: \<sigma>_eq [of n])
+ qed
+ then have "range \<sigma> \<subseteq> S" by blast
+ have \<sigma>: "p < n \<Longrightarrow> \<epsilon> \<le> d (\<sigma> p) (\<sigma> n)" for n p
+ using f[of "\<sigma> ` {..<n}"] True by (fastforce simp: \<sigma>_eq [of n] Ball_def)
+ then obtain r where "strict_mono r" "MCauchy (\<sigma> \<circ> r)"
+ by (meson R \<open>range \<sigma> \<subseteq> S\<close>)
+ with \<open>0 < \<epsilon>\<close> obtain N
+ where N: "\<And>n n'. \<lbrakk>n\<ge>N; n'\<ge>N\<rbrakk> \<Longrightarrow> d (\<sigma> (r n)) (\<sigma> (r n')) < \<epsilon>"
+ by (force simp: MCauchy_def)
+ show ?thesis
+ using N [of N "Suc (r N)"] \<open>strict_mono r\<close>
+ by (smt (verit) Suc_le_eq \<sigma> le_SucI order_refl strict_mono_imp_increasing)
+ qed
+ then show "\<exists>K. finite K \<and> K \<subseteq> S \<and> S \<subseteq> (\<Union>x\<in>K. mball x \<epsilon>)"
+ by blast
+ qed
+ }
+ ultimately show ?thesis
+ using True by blast
+ qed
+qed (use mtotally_bounded_imp_subset in auto)
+
+
+lemma mtotally_bounded_subset:
+ "\<lbrakk>mtotally_bounded S; T \<subseteq> S\<rbrakk> \<Longrightarrow> mtotally_bounded T"
+ by (meson mtotally_bounded_sequentially order_trans)
+
+lemma mtotally_bounded_submetric:
+ assumes "mtotally_bounded S" "S \<subseteq> T" "T \<subseteq> M"
+ shows "Metric_space.mtotally_bounded T d S"
+proof -
+ interpret submetric M d T
+ by (simp add: Metric_space_axioms assms submetric.intro submetric_axioms.intro)
+ show ?thesis
+ using assms
+ unfolding sub.mtotally_bounded_def mtotally_bounded_def
+ by (force simp: subset_iff elim!: all_forward ex_forward)
+qed
+
+lemma mtotally_bounded_absolute:
+ "mtotally_bounded S \<longleftrightarrow> S \<subseteq> M \<and> Metric_space.mtotally_bounded S d S "
+proof -
+ have "mtotally_bounded S" if "S \<subseteq> M" "Metric_space.mtotally_bounded S d S"
+ proof -
+ interpret submetric M d S
+ by (simp add: Metric_space_axioms submetric_axioms.intro submetric_def \<open>S \<subseteq> M\<close>)
+ show ?thesis
+ using that
+ by (metis MCauchy_submetric Metric_space.mtotally_bounded_sequentially Metric_space_axioms subspace)
+ qed
+ moreover have "mtotally_bounded S \<Longrightarrow> Metric_space.mtotally_bounded S d S"
+ by (simp add: mtotally_bounded_imp_subset mtotally_bounded_submetric)
+ ultimately show ?thesis
+ using mtotally_bounded_imp_subset by blast
+qed
+
+lemma mtotally_bounded_closure_of:
+ assumes "mtotally_bounded S"
+ shows "mtotally_bounded (mtopology closure_of S)"
+proof -
+ have "S \<subseteq> M"
+ by (simp add: assms mtotally_bounded_imp_subset)
+ have "mtotally_bounded(mtopology closure_of S)"
+ unfolding mtotally_bounded_def
+ proof (intro strip)
+ fix \<epsilon>::real
+ assume "\<epsilon> > 0"
+ then obtain K where "finite K" "K \<subseteq> S" and K: "S \<subseteq> (\<Union>x\<in>K. mball x (\<epsilon>/2))"
+ by (metis assms mtotally_bounded_def half_gt_zero)
+ have "mtopology closure_of S \<subseteq> (\<Union>x\<in>K. mball x \<epsilon>)"
+ unfolding metric_closure_of
+ proof clarsimp
+ fix x
+ assume "x \<in> M" and x: "\<forall>r>0. \<exists>y\<in>S. y \<in> M \<and> d x y < r"
+ then obtain y where "y \<in> S" and y: "d x y < \<epsilon>/2"
+ using \<open>0 < \<epsilon>\<close> half_gt_zero by blast
+ then obtain x' where "x' \<in> K" "y \<in> mball x' (\<epsilon>/2)"
+ using K by auto
+ then have "d x' x < \<epsilon>/2 + \<epsilon>/2"
+ using triangle y \<open>x \<in> M\<close> commute by fastforce
+ then show "\<exists>x'\<in>K. x' \<in> M \<and> d x' x < \<epsilon>"
+ using \<open>K \<subseteq> S\<close> \<open>S \<subseteq> M\<close> \<open>x' \<in> K\<close> by force
+ qed
+ then show "\<exists>K. finite K \<and> K \<subseteq> mtopology closure_of S \<and> mtopology closure_of S \<subseteq> (\<Union>x\<in>K. mball x \<epsilon>)"
+ using closure_of_subset_Int \<open>K \<subseteq> S\<close> \<open>finite K\<close> K by fastforce
+ qed
+ then show ?thesis
+ by (simp add: assms inf.absorb2 mtotally_bounded_imp_subset)
+qed
+
+lemma mtotally_bounded_closure_of_eq:
+ "S \<subseteq> M \<Longrightarrow> mtotally_bounded (mtopology closure_of S) \<longleftrightarrow> mtotally_bounded S"
+ by (metis closure_of_subset mtotally_bounded_closure_of mtotally_bounded_subset topspace_mtopology)
+
+lemma mtotally_bounded_cauchy_sequence:
+ assumes "MCauchy \<sigma>"
+ shows "mtotally_bounded (range \<sigma>)"
+ unfolding MCauchy_def mtotally_bounded_def
+proof (intro strip)
+ fix \<epsilon>::real
+ assume "\<epsilon> > 0"
+ then obtain N where "\<And>n. N \<le> n \<Longrightarrow> d (\<sigma> N) (\<sigma> n) < \<epsilon>"
+ using assms by (force simp: MCauchy_def)
+ then have "\<And>m. \<exists>n\<le>N. \<sigma> n \<in> M \<and> \<sigma> m \<in> M \<and> d (\<sigma> n) (\<sigma> m) < \<epsilon>"
+ by (metis MCauchy_def assms mdist_zero nle_le range_subsetD)
+ then
+ show "\<exists>K. finite K \<and> K \<subseteq> range \<sigma> \<and> range \<sigma> \<subseteq> (\<Union>x\<in>K. mball x \<epsilon>)"
+ by (rule_tac x="\<sigma> ` {0..N}" in exI) force
+qed
+
+lemma MCauchy_imp_mbounded:
+ "MCauchy \<sigma> \<Longrightarrow> mbounded (range \<sigma>)"
+ by (simp add: mtotally_bounded_cauchy_sequence mtotally_bounded_imp_mbounded)
+
+subsection\<open>Compactness in metric spaces\<close>
+
+lemma Bolzano_Weierstrass_property:
+ assumes "S \<subseteq> U" "S \<subseteq> M"
+ shows
+ "(\<forall>\<sigma>::nat\<Rightarrow>'a. range \<sigma> \<subseteq> S
+ \<longrightarrow> (\<exists>l r. l \<in> U \<and> strict_mono r \<and> limitin mtopology (\<sigma> \<circ> r) l sequentially)) \<longleftrightarrow>
+ (\<forall>T. T \<subseteq> S \<and> infinite T \<longrightarrow> U \<inter> mtopology derived_set_of T \<noteq> {})" (is "?lhs=?rhs")
+proof
+ assume L: ?lhs
+ show ?rhs
+ proof clarify
+ fix T
+ assume "T \<subseteq> S" and "infinite T"
+ and T: "U \<inter> mtopology derived_set_of T = {}"
+ then obtain \<sigma> :: "nat\<Rightarrow>'a" where "inj \<sigma>" "range \<sigma> \<subseteq> T"
+ by (meson infinite_countable_subset)
+ with L obtain l r where "l \<in> U" "strict_mono r"
+ and lr: "limitin mtopology (\<sigma> \<circ> r) l sequentially"
+ by (meson \<open>T \<subseteq> S\<close> subset_trans)
+ then obtain \<epsilon> where "\<epsilon> > 0" and \<epsilon>: "\<And>y. y \<in> T \<Longrightarrow> y = l \<or> \<not> d l y < \<epsilon>"
+ using T \<open>T \<subseteq> S\<close> \<open>S \<subseteq> M\<close>
+ by (force simp: metric_derived_set_of limitin_metric disjoint_iff)
+ with lr have "\<forall>\<^sub>F n in sequentially. \<sigma> (r n) \<in> M \<and> d (\<sigma> (r n)) l < \<epsilon>"
+ by (auto simp: limitin_metric)
+ then obtain N where N: "d (\<sigma> (r N)) l < \<epsilon>" "d (\<sigma> (r (Suc N))) l < \<epsilon>"
+ using less_le_not_le by (auto simp: eventually_sequentially)
+ moreover have "\<sigma> (r N) \<noteq> l \<or> \<sigma> (r (Suc N)) \<noteq> l"
+ by (meson \<open>inj \<sigma>\<close> \<open>strict_mono r\<close> injD n_not_Suc_n strict_mono_eq)
+ ultimately
+ show False
+ using \<epsilon> \<open>range \<sigma> \<subseteq> T\<close> commute by fastforce
+ qed
+next
+ assume R: ?rhs
+ show ?lhs
+ proof (intro strip)
+ fix \<sigma> :: "nat \<Rightarrow> 'a"
+ assume "range \<sigma> \<subseteq> S"
+ show "\<exists>l r. l \<in> U \<and> strict_mono r \<and> limitin mtopology (\<sigma> \<circ> r) l sequentially"
+ proof (cases "finite (range \<sigma>)")
+ case True
+ then obtain m where "infinite (\<sigma> -` {\<sigma> m})"
+ by (metis image_iff inf_img_fin_dom nat_not_finite)
+ then obtain r where [iff]: "strict_mono r" and r: "\<And>n::nat. r n \<in> \<sigma> -` {\<sigma> m}"
+ using infinite_enumerate by blast
+ have [iff]: "\<sigma> m \<in> U" "\<sigma> m \<in> M"
+ using \<open>range \<sigma> \<subseteq> S\<close> assms by blast+
+ show ?thesis
+ proof (intro conjI exI)
+ show "limitin mtopology (\<sigma> \<circ> r) (\<sigma> m) sequentially"
+ using r by (simp add: limitin_metric)
+ qed auto
+ next
+ case False
+ then obtain l where "l \<in> U" and l: "l \<in> mtopology derived_set_of (range \<sigma>)"
+ by (meson R \<open>range \<sigma> \<subseteq> S\<close> disjoint_iff)
+ then obtain g where g: "\<And>\<epsilon>. \<epsilon>>0 \<Longrightarrow> \<sigma> (g \<epsilon>) \<noteq> l \<and> d l (\<sigma> (g \<epsilon>)) < \<epsilon>"
+ by (simp add: metric_derived_set_of) metis
+ have "range \<sigma> \<subseteq> M"
+ using \<open>range \<sigma> \<subseteq> S\<close> assms by auto
+ have "l \<in> M"
+ using l metric_derived_set_of by auto
+ define E where \<comment>\<open>a construction to ensure monotonicity\<close>
+ "E \<equiv> \<lambda>rec n. insert (inverse (Suc n)) ((\<lambda>i. d l (\<sigma> i)) ` (\<Union>k<n. {0..rec k})) - {0}"
+ define r where "r \<equiv> wfrec less_than (\<lambda>rec n. g (Min (E rec n)))"
+ have "(\<Union>k<n. {0..cut r less_than n k}) = (\<Union>k<n. {0..r k})" for n
+ by (auto simp: cut_apply)
+ then have r_eq: "r n = g (Min (E r n))" for n
+ by (metis E_def def_wfrec [OF r_def] wf_less_than)
+ have dl_pos[simp]: "d l (\<sigma> (r n)) > 0" for n
+ using wf_less_than
+ proof (induction n rule: wf_induct_rule)
+ case (less n)
+ then have *: "Min (E r n) > 0"
+ using \<open>l \<in> M\<close> \<open>range \<sigma> \<subseteq> M\<close> by (auto simp: E_def image_subset_iff)
+ show ?case
+ using g [OF *] r_eq [of n]
+ by (metis \<open>l \<in> M\<close> \<open>range \<sigma> \<subseteq> M\<close> mdist_pos_less range_subsetD)
+ qed
+ then have non_l: "\<sigma> (r n) \<noteq> l" for n
+ using \<open>range \<sigma> \<subseteq> M\<close> mdist_pos_eq by blast
+ have Min_pos: "Min (E r n) > 0" for n
+ using dl_pos \<open>l \<in> M\<close> \<open>range \<sigma> \<subseteq> M\<close> by (auto simp: E_def image_subset_iff)
+ have d_small: "d (\<sigma>(r n)) l < inverse(Suc n)" for n
+ proof -
+ have "d (\<sigma>(r n)) l < Min (E r n)"
+ by (simp add: \<open>0 < Min (E r n)\<close> commute g r_eq)
+ also have "... \<le> inverse(Suc n)"
+ by (simp add: E_def)
+ finally show ?thesis .
+ qed
+ have d_lt_d: "d l (\<sigma> (r n)) < d l (\<sigma> i)" if \<section>: "p < n" "i \<le> r p" "\<sigma> i \<noteq> l" for i p n
+ proof -
+ have 1: "d l (\<sigma> i) \<in> E r n"
+ using \<section> \<open>l \<in> M\<close> \<open>range \<sigma> \<subseteq> M\<close>
+ by (force simp: E_def image_subset_iff image_iff)
+ have "d l (\<sigma> (g (Min (E r n)))) < Min (E r n)"
+ by (rule conjunct2 [OF g [OF Min_pos]])
+ also have "Min (E r n) \<le> d l (\<sigma> i)"
+ using 1 unfolding E_def by (force intro!: Min.coboundedI)
+ finally show ?thesis
+ by (simp add: r_eq)
+ qed
+ have r: "r p < r n" if "p < n" for p n
+ using d_lt_d [OF that] non_l by (meson linorder_not_le order_less_irrefl)
+ show ?thesis
+ proof (intro exI conjI)
+ show "strict_mono r"
+ by (simp add: r strict_monoI)
+ show "limitin mtopology (\<sigma> \<circ> r) l sequentially"
+ unfolding limitin_metric
+ proof (intro conjI strip \<open>l \<in> M\<close>)
+ fix \<epsilon> :: real
+ assume "\<epsilon> > 0"
+ then have "\<forall>\<^sub>F n in sequentially. inverse(Suc n) < \<epsilon>"
+ using Archimedean_eventually_inverse by auto
+ then show "\<forall>\<^sub>F n in sequentially. (\<sigma> \<circ> r) n \<in> M \<and> d ((\<sigma> \<circ> r) n) l < \<epsilon>"
+ by (smt (verit) \<open>range \<sigma> \<subseteq> M\<close> commute comp_apply d_small eventually_mono range_subsetD)
+ qed
+ qed (use \<open>l \<in> U\<close> in auto)
+ qed
+ qed
+qed
+
+subsubsection \<open>More on Bolzano Weierstrass\<close>
+
+lemma Bolzano_Weierstrass_A:
+ assumes "compactin mtopology S" "T \<subseteq> S" "infinite T"
+ shows "S \<inter> mtopology derived_set_of T \<noteq> {}"
+ by (simp add: assms compactin_imp_Bolzano_Weierstrass)
+
+lemma Bolzano_Weierstrass_B:
+ fixes \<sigma> :: "nat \<Rightarrow> 'a"
+ assumes "S \<subseteq> M" "range \<sigma> \<subseteq> S"
+ and "\<And>T. \<lbrakk>T \<subseteq> S \<and> infinite T\<rbrakk> \<Longrightarrow> S \<inter> mtopology derived_set_of T \<noteq> {}"
+ shows "\<exists>l r. l \<in> S \<and> strict_mono r \<and> limitin mtopology (\<sigma> \<circ> r) l sequentially"
+ using Bolzano_Weierstrass_property assms by blast
+
+lemma Bolzano_Weierstrass_C:
+ assumes "S \<subseteq> M"
+ assumes "\<And>\<sigma>:: nat \<Rightarrow> 'a. range \<sigma> \<subseteq> S \<Longrightarrow>
+ (\<exists>l r. l \<in> S \<and> strict_mono r \<and> limitin mtopology (\<sigma> \<circ> r) l sequentially)"
+ shows "mtotally_bounded S"
+ unfolding mtotally_bounded_sequentially
+ by (metis convergent_imp_MCauchy assms image_comp image_mono subset_UNIV subset_trans)
+
+lemma Bolzano_Weierstrass_D:
+ assumes "S \<subseteq> M" "S \<subseteq> \<Union>\<C>" and opeU: "\<And>U. U \<in> \<C> \<Longrightarrow> openin mtopology U"
+ assumes \<section>: "(\<forall>\<sigma>::nat\<Rightarrow>'a. range \<sigma> \<subseteq> S
+ \<longrightarrow> (\<exists>l r. l \<in> S \<and> strict_mono r \<and> limitin mtopology (\<sigma> \<circ> r) l sequentially))"
+ shows "\<exists>\<epsilon>>0. \<forall>x \<in> S. \<exists>U \<in> \<C>. mball x \<epsilon> \<subseteq> U"
+proof (rule ccontr)
+ assume "\<not> (\<exists>\<epsilon>>0. \<forall>x \<in> S. \<exists>U \<in> \<C>. mball x \<epsilon> \<subseteq> U)"
+ then have "\<forall>n. \<exists>x\<in>S. \<forall>U\<in>\<C>. \<not> mball x (inverse (Suc n)) \<subseteq> U"
+ by simp
+ then obtain \<sigma> where "\<And>n. \<sigma> n \<in> S"
+ and \<sigma>: "\<And>n U. U \<in> \<C> \<Longrightarrow> \<not> mball (\<sigma> n) (inverse (Suc n)) \<subseteq> U"
+ by metis
+ then obtain l r where "l \<in> S" "strict_mono r"
+ and lr: "limitin mtopology (\<sigma> \<circ> r) l sequentially"
+ by (meson \<section> image_subsetI)
+ with \<open>S \<subseteq> \<Union>\<C>\<close> obtain B where "l \<in> B" "B \<in> \<C>"
+ by auto
+ then obtain \<epsilon> where "\<epsilon> > 0" and \<epsilon>: "\<And>z. \<lbrakk>z \<in> M; d z l < \<epsilon>\<rbrakk> \<Longrightarrow> z \<in> B"
+ by (metis opeU [OF \<open>B \<in> \<C>\<close>] commute in_mball openin_mtopology subset_iff)
+ then have "\<forall>\<^sub>F n in sequentially. \<sigma> (r n) \<in> M \<and> d (\<sigma> (r n)) l < \<epsilon>/2"
+ using lr half_gt_zero unfolding limitin_metric o_def by blast
+ moreover have "\<forall>\<^sub>F n in sequentially. inverse (real (Suc n)) < \<epsilon>/2"
+ using Archimedean_eventually_inverse \<open>0 < \<epsilon>\<close> half_gt_zero by blast
+ ultimately obtain n where n: "d (\<sigma> (r n)) l < \<epsilon>/2" "inverse (real (Suc n)) < \<epsilon>/2"
+ by (smt (verit, del_insts) eventually_sequentially le_add1 le_add2)
+ have "x \<in> B" if "d (\<sigma> (r n)) x < inverse (Suc(r n))" "x \<in> M" for x
+ proof -
+ have rle: "inverse (real (Suc (r n))) \<le> inverse (real (Suc n))"
+ using \<open>strict_mono r\<close> strict_mono_imp_increasing by auto
+ have "d x l \<le> d (\<sigma> (r n)) x + d (\<sigma> (r n)) l"
+ using that by (metis triangle \<open>\<And>n. \<sigma> n \<in> S\<close> \<open>l \<in> S\<close> \<open>S \<subseteq> M\<close> commute subsetD)
+ also have "... < \<epsilon>"
+ using that n rle by linarith
+ finally show ?thesis
+ by (simp add: \<epsilon> that)
+ qed
+ then show False
+ using \<sigma> [of B "r n"] by (simp add: \<open>B \<in> \<C>\<close> subset_iff)
+qed
+
+
+lemma Bolzano_Weierstrass_E:
+ assumes "mtotally_bounded S" "S \<subseteq> M"
+ and S: "\<And>\<C>. \<lbrakk>\<And>U. U \<in> \<C> \<Longrightarrow> openin mtopology U; S \<subseteq> \<Union>\<C>\<rbrakk> \<Longrightarrow> \<exists>\<epsilon>>0. \<forall>x \<in> S. \<exists>U \<in> \<C>. mball x \<epsilon> \<subseteq> U"
+ shows "compactin mtopology S"
+proof (clarsimp simp: compactin_def assms)
+ fix \<U> :: "'a set set"
+ assume \<U>: "\<forall>x\<in>\<U>. openin mtopology x" and "S \<subseteq> \<Union>\<U>"
+ then obtain \<epsilon> where "\<epsilon>>0" and \<epsilon>: "\<And>x. x \<in> S \<Longrightarrow> \<exists>U \<in> \<U>. mball x \<epsilon> \<subseteq> U"
+ by (metis S)
+ then obtain f where f: "\<And>x. x \<in> S \<Longrightarrow> f x \<in> \<U> \<and> mball x \<epsilon> \<subseteq> f x"
+ by metis
+ then obtain K where "finite K" "K \<subseteq> S" and K: "S \<subseteq> (\<Union>x\<in>K. mball x \<epsilon>)"
+ by (metis \<open>0 < \<epsilon>\<close> \<open>mtotally_bounded S\<close> mtotally_bounded_def)
+ show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> S \<subseteq> \<Union>\<F>"
+ proof (intro conjI exI)
+ show "finite (f ` K)"
+ by (simp add: \<open>finite K\<close>)
+ show "f ` K \<subseteq> \<U>"
+ using \<open>K \<subseteq> S\<close> f by blast
+ show "S \<subseteq> \<Union>(f ` K)"
+ using K \<open>K \<subseteq> S\<close> by (force dest: f)
+ qed
+qed
+
+
+lemma compactin_eq_Bolzano_Weierstrass:
+ "compactin mtopology S \<longleftrightarrow>
+ S \<subseteq> M \<and> (\<forall>T. T \<subseteq> S \<and> infinite T \<longrightarrow> S \<inter> mtopology derived_set_of T \<noteq> {})"
+ using Bolzano_Weierstrass_C Bolzano_Weierstrass_D Bolzano_Weierstrass_E
+ by (smt (verit, del_insts) Bolzano_Weierstrass_property compactin_imp_Bolzano_Weierstrass compactin_subspace subset_refl topspace_mtopology)
+
+lemma compactin_sequentially:
+ shows "compactin mtopology S \<longleftrightarrow>
+ S \<subseteq> M \<and>
+ ((\<forall>\<sigma>::nat\<Rightarrow>'a. range \<sigma> \<subseteq> S
+ \<longrightarrow> (\<exists>l r. l \<in> S \<and> strict_mono r \<and> limitin mtopology (\<sigma> \<circ> r) l sequentially)))"
+ by (metis Bolzano_Weierstrass_property compactin_eq_Bolzano_Weierstrass subset_refl)
+
+lemma compactin_imp_mtotally_bounded:
+ "compactin mtopology S \<Longrightarrow> mtotally_bounded S"
+ by (simp add: Bolzano_Weierstrass_C compactin_sequentially)
+
+lemma lebesgue_number:
+ "\<lbrakk>compactin mtopology S; S \<subseteq> \<Union>\<C>; \<And>U. U \<in> \<C> \<Longrightarrow> openin mtopology U\<rbrakk>
+ \<Longrightarrow> \<exists>\<epsilon>>0. \<forall>x \<in> S. \<exists>U \<in> \<C>. mball x \<epsilon> \<subseteq> U"
+ by (simp add: Bolzano_Weierstrass_D compactin_sequentially)
+
+lemma compact_space_sequentially:
+ "compact_space mtopology \<longleftrightarrow>
+ (\<forall>\<sigma>::nat\<Rightarrow>'a. range \<sigma> \<subseteq> M
+ \<longrightarrow> (\<exists>l r. l \<in> M \<and> strict_mono r \<and> limitin mtopology (\<sigma> \<circ> r) l sequentially))"
+ by (simp add: compact_space_def compactin_sequentially)
+
+lemma compact_space_eq_Bolzano_Weierstrass:
+ "compact_space mtopology \<longleftrightarrow>
+ (\<forall>S. S \<subseteq> M \<and> infinite S \<longrightarrow> mtopology derived_set_of S \<noteq> {})"
+ using Int_absorb1 [OF derived_set_of_subset_topspace [of mtopology]]
+ by (force simp: compact_space_def compactin_eq_Bolzano_Weierstrass)
+
+lemma compact_space_nest:
+ "compact_space mtopology \<longleftrightarrow>
+ (\<forall>C. (\<forall>n::nat. closedin mtopology (C n)) \<and> (\<forall>n. C n \<noteq> {}) \<and> decseq C \<longrightarrow> \<Inter>(range C) \<noteq> {})"
+ (is "?lhs=?rhs")
+proof
+ assume L: ?lhs
+ show ?rhs
+ proof clarify
+ fix C :: "nat \<Rightarrow> 'a set"
+ assume "\<forall>n. closedin mtopology (C n)"
+ and "\<forall>n. C n \<noteq> {}"
+ and "decseq C"
+ and "\<Inter> (range C) = {}"
+ then obtain K where K: "finite K" "\<Inter>(C ` K) = {}"
+ by (metis L compact_space_imp_nest)
+ then obtain k where "K \<subseteq> {..k}"
+ using finite_nat_iff_bounded_le by auto
+ then have "C k \<subseteq> \<Inter>(C ` K)"
+ using \<open>decseq C\<close> by (auto simp:decseq_def)
+ then show False
+ by (simp add: K \<open>\<forall>n. C n \<noteq> {}\<close>)
+ qed
+next
+ assume R [rule_format]: ?rhs
+ show ?lhs
+ unfolding compact_space_sequentially
+ proof (intro strip)
+ fix \<sigma> :: "nat \<Rightarrow> 'a"
+ assume \<sigma>: "range \<sigma> \<subseteq> M"
+ have "mtopology closure_of \<sigma> ` {n..} \<noteq> {}" for n
+ using \<open>range \<sigma> \<subseteq> M\<close> by (auto simp: closure_of_eq_empty image_subset_iff)
+ moreover have "decseq (\<lambda>n. mtopology closure_of \<sigma> ` {n..})"
+ using closure_of_mono image_mono by (smt (verit) atLeast_subset_iff decseq_def)
+ ultimately obtain l where l: "\<And>n. l \<in> mtopology closure_of \<sigma> ` {n..}"
+ using R [of "\<lambda>n. mtopology closure_of (\<sigma> ` {n..})"] by auto
+ then have "l \<in> M" and "\<And>n. \<forall>r>0. \<exists>k\<ge>n. \<sigma> k \<in> M \<and> d l (\<sigma> k) < r"
+ using metric_closure_of by fastforce+
+ then obtain f where f: "\<And>n r. r>0 \<Longrightarrow> f n r \<ge> n \<and> \<sigma> (f n r) \<in> M \<and> d l (\<sigma> (f n r)) < r"
+ by metis
+ define r where "r = rec_nat (f 0 1) (\<lambda>n rec. (f (Suc rec) (inverse (Suc (Suc n)))))"
+ have r: "d l (\<sigma>(r n)) < inverse(Suc n)" for n
+ by (induction n) (auto simp: rec_nat_0_imp [OF r_def] rec_nat_Suc_imp [OF r_def] f)
+ have "r n < r(Suc n)" for n
+ by (simp add: Suc_le_lessD f r_def)
+ then have "strict_mono r"
+ by (simp add: strict_mono_Suc_iff)
+ moreover have "limitin mtopology (\<sigma> \<circ> r) l sequentially"
+ proof (clarsimp simp: limitin_metric \<open>l \<in> M\<close>)
+ fix \<epsilon> :: real
+ assume "\<epsilon> > 0"
+ then have "(\<forall>\<^sub>F n in sequentially. inverse (real (Suc n)) < \<epsilon>)"
+ using Archimedean_eventually_inverse by blast
+ then show "\<forall>\<^sub>F n in sequentially. \<sigma> (r n) \<in> M \<and> d (\<sigma> (r n)) l < \<epsilon>"
+ by eventually_elim (metis commute \<open>range \<sigma> \<subseteq> M\<close> order_less_trans r range_subsetD)
+ qed
+ ultimately show "\<exists>l r. l \<in> M \<and> strict_mono r \<and> limitin mtopology (\<sigma> \<circ> r) l sequentially"
+ using \<open>l \<in> M\<close> by blast
+ qed
+qed
+
+
+lemma (in discrete_metric) mcomplete_discrete_metric: "disc.mcomplete"
+proof (clarsimp simp: disc.mcomplete_def)
+ fix \<sigma> :: "nat \<Rightarrow> 'a"
+ assume "disc.MCauchy \<sigma>"
+ then obtain N where "\<And>n. N \<le> n \<Longrightarrow> \<sigma> N = \<sigma> n"
+ unfolding disc.MCauchy_def by (metis dd_def dual_order.refl order_less_irrefl zero_less_one)
+ moreover have "range \<sigma> \<subseteq> M"
+ using \<open>disc.MCauchy \<sigma>\<close> disc.MCauchy_def by blast
+ ultimately have "limitin disc.mtopology \<sigma> (\<sigma> N) sequentially"
+ by (metis disc.limit_metric_sequentially disc.zero range_subsetD)
+ then show "\<exists>x. limitin disc.mtopology \<sigma> x sequentially" ..
+qed
+
+lemma compact_space_imp_mcomplete: "compact_space mtopology \<Longrightarrow> mcomplete"
+ by (simp add: compact_space_nest mcomplete_nest)
+
+lemma (in submetric) compactin_imp_mcomplete:
+ "compactin mtopology A \<Longrightarrow> sub.mcomplete"
+ by (simp add: compactin_subspace mtopology_submetric sub.compact_space_imp_mcomplete)
+
+lemma (in submetric) mcomplete_imp_closedin:
+ assumes "sub.mcomplete"
+ shows "closedin mtopology A"
+proof -
+ have "l \<in> A"
+ if "range \<sigma> \<subseteq> A" and l: "limitin mtopology \<sigma> l sequentially"
+ for \<sigma> :: "nat \<Rightarrow> 'a" and l
+ proof -
+ have "sub.MCauchy \<sigma>"
+ using convergent_imp_MCauchy subset that by (force simp: MCauchy_submetric)
+ then have "limitin sub.mtopology \<sigma> l sequentially"
+ using assms unfolding sub.mcomplete_def
+ using l limitin_metric_unique limitin_submetric_iff trivial_limit_sequentially by blast
+ then show ?thesis
+ using limitin_submetric_iff by blast
+ qed
+ then show ?thesis
+ using metric_closedin_iff_sequentially_closed subset by auto
+qed
+
+lemma (in submetric) closedin_eq_mcomplete:
+ "mcomplete \<Longrightarrow> (closedin mtopology A \<longleftrightarrow> sub.mcomplete)"
+ using closedin_mcomplete_imp_mcomplete mcomplete_imp_closedin by blast
+
+lemma compact_space_eq_mcomplete_mtotally_bounded:
+ "compact_space mtopology \<longleftrightarrow> mcomplete \<and> mtotally_bounded M"
+ by (meson Bolzano_Weierstrass_C compact_space_imp_mcomplete compact_space_sequentially limitin_mspace
+ mcomplete_alt mtotally_bounded_sequentially subset_refl)
+
+
+lemma compact_closure_of_imp_mtotally_bounded:
+ "\<lbrakk>compactin mtopology (mtopology closure_of S); S \<subseteq> M\<rbrakk>
+ \<Longrightarrow> mtotally_bounded S"
+ using compactin_imp_mtotally_bounded mtotally_bounded_closure_of_eq by blast
+
+lemma mtotally_bounded_eq_compact_closure_of:
+ assumes "mcomplete"
+ shows "mtotally_bounded S \<longleftrightarrow> S \<subseteq> M \<and> compactin mtopology (mtopology closure_of S)"
+ (is "?lhs=?rhs")
+proof
+ assume L: ?lhs
+ show ?rhs
+ unfolding compactin_subspace
+ proof (intro conjI)
+ show "S \<subseteq> M"
+ using L by (simp add: mtotally_bounded_imp_subset)
+ show "mtopology closure_of S \<subseteq> topspace mtopology"
+ by (simp add: \<open>S \<subseteq> M\<close> closure_of_minimal)
+ then have MSM: "mtopology closure_of S \<subseteq> M"
+ by auto
+ interpret S: submetric M d "mtopology closure_of S"
+ proof qed (use MSM in auto)
+ have "S.sub.mtotally_bounded (mtopology closure_of S)"
+ using L mtotally_bounded_absolute mtotally_bounded_closure_of by blast
+ then
+ show "compact_space (subtopology mtopology (mtopology closure_of S))"
+ using S.closedin_mcomplete_imp_mcomplete S.mtopology_submetric S.sub.compact_space_eq_mcomplete_mtotally_bounded assms by force
+ qed
+qed (auto simp: compact_closure_of_imp_mtotally_bounded)
+
+
+
+lemma compact_closure_of_eq_Bolzano_Weierstrass:
+ "compactin mtopology (mtopology closure_of S) \<longleftrightarrow>
+ (\<forall>T. infinite T \<and> T \<subseteq> S \<and> T \<subseteq> M \<longrightarrow> mtopology derived_set_of T \<noteq> {})" (is "?lhs=?rhs")
+proof
+ assume L: ?lhs
+ show ?rhs
+ proof (intro strip)
+ fix T
+ assume T: "infinite T \<and> T \<subseteq> S \<and> T \<subseteq> M"
+ show "mtopology derived_set_of T \<noteq> {}"
+ proof (intro compact_closure_of_imp_Bolzano_Weierstrass)
+ show "compactin mtopology (mtopology closure_of S)"
+ by (simp add: L)
+ qed (use T in auto)
+ qed
+next
+ have "compactin mtopology (mtopology closure_of S)"
+ if \<section>: "\<And>T. \<lbrakk>infinite T; T \<subseteq> S\<rbrakk> \<Longrightarrow> mtopology derived_set_of T \<noteq> {}" and "S \<subseteq> M" for S
+ unfolding compactin_sequentially
+ proof (intro conjI strip)
+ show MSM: "mtopology closure_of S \<subseteq> M"
+ using closure_of_subset_topspace by fastforce
+ fix \<sigma> :: "nat \<Rightarrow> 'a"
+ assume \<sigma>: "range \<sigma> \<subseteq> mtopology closure_of S"
+ then have "\<exists>y \<in> S. d (\<sigma> n) y < inverse(Suc n)" for n
+ by (simp add: metric_closure_of image_subset_iff) (metis inverse_Suc of_nat_Suc)
+ then obtain \<tau> where \<tau>: "\<And>n. \<tau> n \<in> S \<and> d (\<sigma> n) (\<tau> n) < inverse(Suc n)"
+ by metis
+ then have "range \<tau> \<subseteq> S"
+ by blast
+ moreover
+ have *: "\<forall>T. T \<subseteq> S \<and> infinite T \<longrightarrow> mtopology closure_of S \<inter> mtopology derived_set_of T \<noteq> {}"
+ using "\<section>"(1) derived_set_of_mono derived_set_of_subset_closure_of by fastforce
+ moreover have "S \<subseteq> mtopology closure_of S"
+ by (simp add: \<open>S \<subseteq> M\<close> closure_of_subset)
+ ultimately obtain l r where lr:
+ "l \<in> mtopology closure_of S" "strict_mono r" "limitin mtopology (\<tau> \<circ> r) l sequentially"
+ using Bolzano_Weierstrass_property \<open>S \<subseteq> M\<close> by metis
+ then have "l \<in> M"
+ using limitin_mspace by blast
+ have dr_less: "d ((\<sigma> \<circ> r) n) ((\<tau> \<circ> r) n) < inverse(Suc n)" for n
+ proof -
+ have "d ((\<sigma> \<circ> r) n) ((\<tau> \<circ> r) n) < inverse(Suc (r n))"
+ using \<tau> by auto
+ also have "... \<le> inverse(Suc n)"
+ using lr strict_mono_imp_increasing by auto
+ finally show ?thesis .
+ qed
+ have "limitin mtopology (\<sigma> \<circ> r) l sequentially"
+ unfolding limitin_metric
+ proof (intro conjI strip)
+ show "l \<in> M"
+ using limitin_mspace lr by blast
+ fix \<epsilon> :: real
+ assume "\<epsilon> > 0"
+ then have "\<forall>\<^sub>F n in sequentially. (\<tau> \<circ> r) n \<in> M \<and> d ((\<tau> \<circ> r) n) l < \<epsilon>/2"
+ using lr half_gt_zero limitin_metric by blast
+ moreover have "\<forall>\<^sub>F n in sequentially. inverse (real (Suc n)) < \<epsilon>/2"
+ using Archimedean_eventually_inverse \<open>0 < \<epsilon>\<close> half_gt_zero by blast
+ then have "\<forall>\<^sub>F n in sequentially. d ((\<sigma> \<circ> r) n) ((\<tau> \<circ> r) n) < \<epsilon>/2"
+ by eventually_elim (smt (verit, del_insts) dr_less)
+ ultimately have "\<forall>\<^sub>F n in sequentially. d ((\<sigma> \<circ> r) n) l < \<epsilon>/2 + \<epsilon>/2"
+ by eventually_elim (smt (verit) triangle \<open>l \<in> M\<close> MSM \<sigma> comp_apply order_trans range_subsetD)
+ then show "\<forall>\<^sub>F n in sequentially. (\<sigma> \<circ> r) n \<in> M \<and> d ((\<sigma> \<circ> r) n) l < \<epsilon>"
+ apply eventually_elim
+ using \<open>mtopology closure_of S \<subseteq> M\<close> \<sigma> by auto
+ qed
+ with lr show "\<exists>l r. l \<in> mtopology closure_of S \<and> strict_mono r \<and> limitin mtopology (\<sigma> \<circ> r) l sequentially"
+ by blast
+ qed
+ then show "?rhs \<Longrightarrow> ?lhs"
+ by (metis Int_subset_iff closure_of_restrict inf_le1 topspace_mtopology)
+qed
+
+end
+
+lemma (in discrete_metric) mtotally_bounded_discrete_metric:
+ "disc.mtotally_bounded S \<longleftrightarrow> finite S \<and> S \<subseteq> M" (is "?lhs=?rhs")
+proof
+ assume L: ?lhs
+ show ?rhs
+ proof
+ show "finite S"
+ by (metis (no_types) L closure_of_subset_Int compactin_discrete_topology disc.mtotally_bounded_eq_compact_closure_of
+ disc.topspace_mtopology discrete_metric.mcomplete_discrete_metric inf.absorb_iff2 mtopology_discrete_metric finite_subset)
+ show "S \<subseteq> M"
+ by (simp add: L disc.mtotally_bounded_imp_subset)
+ qed
+qed (simp add: disc.finite_imp_mtotally_bounded)
+
+
+context Metric_space
+begin
+
+lemma derived_set_of_infinite_openin_metric:
+ "mtopology derived_set_of S =
+ {x \<in> M. \<forall>U. x \<in> U \<and> openin mtopology U \<longrightarrow> infinite(S \<inter> U)}"
+ by (simp add: derived_set_of_infinite_openin Hausdorff_space_mtopology)
+
+lemma derived_set_of_infinite_1:
+ assumes "infinite (S \<inter> mball x \<epsilon>)"
+ shows "infinite (S \<inter> mcball x \<epsilon>)"
+ by (meson Int_mono assms finite_subset mball_subset_mcball subset_refl)
+
+lemma derived_set_of_infinite_2:
+ assumes "openin mtopology U" "\<And>\<epsilon>. 0 < \<epsilon> \<Longrightarrow> infinite (S \<inter> mcball x \<epsilon>)" and "x \<in> U"
+ shows "infinite (S \<inter> U)"
+ by (metis assms openin_mtopology_mcball finite_Int inf.absorb_iff2 inf_assoc)
+
+lemma derived_set_of_infinite_mball:
+ "mtopology derived_set_of S = {x \<in> M. \<forall>e>0. infinite(S \<inter> mball x e)}"
+ unfolding derived_set_of_infinite_openin_metric
+ by (meson centre_in_mball_iff openin_mball derived_set_of_infinite_1 derived_set_of_infinite_2)
+
+lemma derived_set_of_infinite_mcball:
+ "mtopology derived_set_of S = {x \<in> M. \<forall>e>0. infinite(S \<inter> mcball x e)}"
+ unfolding derived_set_of_infinite_openin_metric
+ by (meson centre_in_mball_iff openin_mball derived_set_of_infinite_1 derived_set_of_infinite_2)
+
+end
+
+subsection\<open>Continuous functions on metric spaces\<close>
+
+context Metric_space
+begin
+
+lemma continuous_map_to_metric:
+ "continuous_map X mtopology f \<longleftrightarrow>
+ (\<forall>x \<in> topspace X. \<forall>\<epsilon>>0. \<exists>U. openin X U \<and> x \<in> U \<and> (\<forall>y\<in>U. f y \<in> mball (f x) \<epsilon>))"
+ (is "?lhs=?rhs")
+proof
+ show "?lhs \<Longrightarrow> ?rhs"
+ unfolding continuous_map_eq_topcontinuous_at topcontinuous_at_def
+ by (metis centre_in_mball_iff openin_mball topspace_mtopology)
+next
+ assume R: ?rhs
+ then have "\<forall>x\<in>topspace X. f x \<in> M"
+ by (meson gt_ex in_mball)
+ moreover
+ have "\<And>x V. \<lbrakk>x \<in> topspace X; openin mtopology V; f x \<in> V\<rbrakk> \<Longrightarrow> \<exists>U. openin X U \<and> x \<in> U \<and> (\<forall>y\<in>U. f y \<in> V)"
+ unfolding openin_mtopology by (metis Int_iff R inf.orderE)
+ ultimately
+ show ?lhs
+ by (simp add: continuous_map_eq_topcontinuous_at topcontinuous_at_def)
+qed
+
+lemma continuous_map_from_metric:
+ "continuous_map mtopology X f \<longleftrightarrow>
+ f ` M \<subseteq> topspace X \<and>
+ (\<forall>a \<in> M. \<forall>U. openin X U \<and> f a \<in> U \<longrightarrow> (\<exists>r>0. \<forall>x. x \<in> M \<and> d a x < r \<longrightarrow> f x \<in> U))"
+proof (cases "f ` M \<subseteq> topspace X")
+ case True
+ then show ?thesis
+ by (fastforce simp: continuous_map openin_mtopology subset_eq)
+next
+ case False
+ then show ?thesis
+ by (simp add: continuous_map_eq_image_closure_subset_gen)
+qed
+
+text \<open>An abstract formulation, since the limits do not have to be sequential\<close>
+lemma continuous_map_uniform_limit:
+ assumes contf: "\<forall>\<^sub>F \<xi> in F. continuous_map X mtopology (f \<xi>)"
+ and dfg: "\<And>\<epsilon>. 0 < \<epsilon> \<Longrightarrow> \<forall>\<^sub>F \<xi> in F. \<forall>x \<in> topspace X. g x \<in> M \<and> d (f \<xi> x) (g x) < \<epsilon>"
+ and nontriv: "\<not> trivial_limit F"
+ shows "continuous_map X mtopology g"
+ unfolding continuous_map_to_metric
+proof (intro strip)
+ fix x and \<epsilon>::real
+ assume "x \<in> topspace X" and "\<epsilon> > 0"
+ then obtain \<xi> where k: "continuous_map X mtopology (f \<xi>)"
+ and gM: "\<forall>x \<in> topspace X. g x \<in> M"
+ and third: "\<forall>x \<in> topspace X. d (f \<xi> x) (g x) < \<epsilon>/3"
+ using eventually_conj [OF contf] contf dfg [of "\<epsilon>/3"] eventually_happens' [OF nontriv]
+ by (smt (verit, ccfv_SIG) zero_less_divide_iff)
+ then obtain U where U: "openin X U" "x \<in> U" and Uthird: "\<forall>y\<in>U. d (f \<xi> y) (f \<xi> x) < \<epsilon>/3"
+ unfolding continuous_map_to_metric
+ by (metis \<open>0 < \<epsilon>\<close> \<open>x \<in> topspace X\<close> commute divide_pos_pos in_mball zero_less_numeral)
+ have f_inM: "f \<xi> y \<in> M" if "y\<in>U" for y
+ using U k openin_subset that by (fastforce simp: continuous_map_def)
+ have "d (g y) (g x) < \<epsilon>" if "y\<in>U" for y
+ proof -
+ have "g y \<in> M"
+ using U gM openin_subset that by blast
+ have "d (g y) (g x) \<le> d (g y) (f \<xi> x) + d (f \<xi> x) (g x)"
+ by (simp add: U \<open>g y \<in> M\<close> \<open>x \<in> topspace X\<close> f_inM gM triangle)
+ also have "\<dots> \<le> d (g y) (f \<xi> y) + d (f \<xi> y) (f \<xi> x) + d (f \<xi> x) (g x)"
+ by (simp add: U \<open>g y \<in> M\<close> commute f_inM that triangle')
+ also have "\<dots> < \<epsilon>/3 + \<epsilon>/3 + \<epsilon>/3"
+ by (smt (verit) U(1) Uthird \<open>x \<in> topspace X\<close> commute openin_subset subsetD that third)
+ finally show ?thesis by simp
+ qed
+ with U gM show "\<exists>U. openin X U \<and> x \<in> U \<and> (\<forall>y\<in>U. g y \<in> mball (g x) \<epsilon>)"
+ by (metis commute in_mball in_mono openin_subset)
+qed
+
+
+lemma continuous_map_uniform_limit_alt:
+ assumes contf: "\<forall>\<^sub>F \<xi> in F. continuous_map X mtopology (f \<xi>)"
+ and gim: "g ` (topspace X) \<subseteq> M"
+ and dfg: "\<And>\<epsilon>. 0 < \<epsilon> \<Longrightarrow> \<forall>\<^sub>F \<xi> in F. \<forall>x \<in> topspace X. d (f \<xi> x) (g x) < \<epsilon>"
+ and nontriv: "\<not> trivial_limit F"
+ shows "continuous_map X mtopology g"
+proof (rule continuous_map_uniform_limit [OF contf])
+ fix \<epsilon> :: real
+ assume "\<epsilon> > 0"
+ with gim dfg show "\<forall>\<^sub>F \<xi> in F. \<forall>x\<in>topspace X. g x \<in> M \<and> d (f \<xi> x) (g x) < \<epsilon>"
+ by (simp add: image_subset_iff)
+qed (use nontriv in auto)
+
+
+lemma continuous_map_uniformly_Cauchy_limit:
+ assumes "mcomplete"
+ assumes contf: "\<forall>\<^sub>F n in sequentially. continuous_map X mtopology (f n)"
+ and Cauchy': "\<And>\<epsilon>. \<epsilon> > 0 \<Longrightarrow> \<exists>N. \<forall>m n x. N \<le> m \<longrightarrow> N \<le> n \<longrightarrow> x \<in> topspace X \<longrightarrow> d (f m x) (f n x) < \<epsilon>"
+ obtains g where
+ "continuous_map X mtopology g"
+ "\<And>\<epsilon>. 0 < \<epsilon> \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>topspace X. d (f n x) (g x) < \<epsilon>"
+proof -
+ have "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>l. limitin mtopology (\<lambda>n. f n x) l sequentially"
+ using \<open>mcomplete\<close> [unfolded mcomplete, rule_format] assms
+ by (smt (verit) contf continuous_map_def eventually_mono topspace_mtopology)
+ then obtain g where g: "\<And>x. x \<in> topspace X \<Longrightarrow> limitin mtopology (\<lambda>n. f n x) (g x) sequentially"
+ by metis
+ show thesis
+ proof
+ show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>topspace X. d (f n x) (g x) < \<epsilon>"
+ if "\<epsilon> > 0" for \<epsilon> :: real
+ proof -
+ obtain N where N: "\<And>m n x. \<lbrakk>N \<le> m; N \<le> n; x \<in> topspace X\<rbrakk> \<Longrightarrow> d (f m x) (f n x) < \<epsilon>/2"
+ by (meson Cauchy' \<open>0 < \<epsilon>\<close> half_gt_zero)
+ obtain P where P: "\<And>n x. \<lbrakk>n \<ge> P; x \<in> topspace X\<rbrakk> \<Longrightarrow> f n x \<in> M"
+ using contf by (auto simp: eventually_sequentially continuous_map_def)
+ show ?thesis
+ proof (intro eventually_sequentiallyI strip)
+ fix n x
+ assume "max N P \<le> n" and x: "x \<in> topspace X"
+ obtain L where "g x \<in> M" and L: "\<forall>n\<ge>L. f n x \<in> M \<and> d (f n x) (g x) < \<epsilon>/2"
+ using g [OF x] \<open>\<epsilon> > 0\<close> unfolding limitin_metric
+ by (metis (no_types, lifting) eventually_sequentially half_gt_zero)
+ define n' where "n' \<equiv> Max{L,N,P}"
+ have L': "\<forall>m \<ge> n'. f m x \<in> M \<and> d (f m x) (g x) < \<epsilon>/2"
+ using L by (simp add: n'_def)
+ moreover
+ have "d (f n x) (f n' x) < \<epsilon>/2"
+ using N [of n n' x] \<open>max N P \<le> n\<close> n'_def x by fastforce
+ ultimately have "d (f n x) (g x) < \<epsilon>/2 + \<epsilon>/2"
+ by (smt (verit, ccfv_SIG) P \<open>g x \<in> M\<close> \<open>max N P \<le> n\<close> le_refl max.bounded_iff mdist_zero triangle' x)
+ then show "d (f n x) (g x) < \<epsilon>" by simp
+ qed
+ qed
+ then show "continuous_map X mtopology g"
+ by (smt (verit, del_insts) eventually_mono g limitin_mspace trivial_limit_sequentially continuous_map_uniform_limit [OF contf])
+ qed
+qed
+
+lemma metric_continuous_map:
+ assumes "Metric_space M' d'"
+ shows
+ "continuous_map mtopology (Metric_space.mtopology M' d') f \<longleftrightarrow>
+ f ` M \<subseteq> M' \<and> (\<forall>a \<in> M. \<forall>\<epsilon>>0. \<exists>\<delta>>0. (\<forall>x. x \<in> M \<and> d a x < \<delta> \<longrightarrow> d' (f a) (f x) < \<epsilon>))"
+ (is "?lhs = ?rhs")
+proof -
+ interpret M': Metric_space M' d'
+ by (simp add: assms)
+ show ?thesis
+ proof
+ assume L: ?lhs
+ show ?rhs
+ proof (intro conjI strip)
+ show "f ` M \<subseteq> M'"
+ using L by (auto simp: continuous_map_def)
+ fix a and \<epsilon> :: real
+ assume "a \<in> M" and "\<epsilon> > 0"
+ then have "openin mtopology {x \<in> M. f x \<in> M'.mball (f a) \<epsilon>}" "f a \<in> M'"
+ using L unfolding continuous_map_def by fastforce+
+ then obtain \<delta> where "\<delta> > 0" "mball a \<delta> \<subseteq> {x \<in> M. f x \<in> M' \<and> d' (f a) (f x) < \<epsilon>}"
+ using \<open>0 < \<epsilon>\<close> \<open>a \<in> M\<close> openin_mtopology by auto
+ then show "\<exists>\<delta>>0. \<forall>x. x \<in> M \<and> d a x < \<delta> \<longrightarrow> d' (f a) (f x) < \<epsilon>"
+ using \<open>a \<in> M\<close> in_mball by blast
+ qed
+ next
+ assume R: ?rhs
+ show ?lhs
+ unfolding continuous_map_def
+ proof (intro conjI strip)
+ fix U
+ assume "openin M'.mtopology U"
+ then show "openin mtopology {x \<in> topspace mtopology. f x \<in> U}"
+ apply (simp add: continuous_map_def openin_mtopology M'.openin_mtopology subset_iff)
+ by (metis R image_subset_iff)
+ qed (use R in auto)
+ qed
+qed
+
+end (*Metric_space*)
+
+end
+
--- a/src/HOL/Analysis/Abstract_Topological_Spaces.thy Mon May 22 12:01:05 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy Tue May 23 12:31:23 2023 +0100
@@ -1276,6 +1276,10 @@
using Hausdorff_space_closedin_diagonal embedding_imp_closed_map_eq by blast
qed
+lemma proper_map_diag_eq [simp]:
+ "proper_map X (prod_topology X X) (\<lambda>x. (x,x)) \<longleftrightarrow> Hausdorff_space X"
+ by (simp add: closed_map_diag_eq inj_on_convol_ident injective_imp_proper_eq_closed_map)
+
lemma closedin_continuous_maps_eq:
assumes "Hausdorff_space Y" and f: "continuous_map X Y f" and g: "continuous_map X Y g"
shows "closedin X {x \<in> topspace X. f x = g x}"
@@ -1606,6 +1610,340 @@
"\<lbrakk>Hausdorff_space X; kc_space Y\<rbrakk> \<Longrightarrow> kc_space (prod_topology X Y)"
using kc_space_prod_topology_left homeomorphic_kc_space homeomorphic_space_prod_topology_swap by blast
+subsection \<open>Technical results about proper maps, perfect maps, etc\<close>
+
+lemma compact_imp_proper_map_gen:
+ assumes Y: "\<And>S. \<lbrakk>S \<subseteq> topspace Y; \<And>K. compactin Y K \<Longrightarrow> compactin Y (S \<inter> K)\<rbrakk>
+ \<Longrightarrow> closedin Y S"
+ and fim: "f ` (topspace X) \<subseteq> topspace Y"
+ and f: "continuous_map X Y f \<or> kc_space X"
+ and YX: "\<And>K. compactin Y K \<Longrightarrow> compactin X {x \<in> topspace X. f x \<in> K}"
+ shows "proper_map X Y f"
+ unfolding proper_map_alt closed_map_def
+proof (intro conjI strip)
+ fix C
+ assume C: "closedin X C"
+ show "closedin Y (f ` C)"
+ proof (intro Y)
+ show "f ` C \<subseteq> topspace Y"
+ using C closedin_subset fim by blast
+ fix K
+ assume K: "compactin Y K"
+ define A where "A \<equiv> {x \<in> topspace X. f x \<in> K}"
+ have eq: "f ` C \<inter> K = f ` ({x \<in> topspace X. f x \<in> K} \<inter> C)"
+ using C closedin_subset by auto
+ show "compactin Y (f ` C \<inter> K)"
+ unfolding eq
+ proof (rule image_compactin)
+ show "compactin (subtopology X A) ({x \<in> topspace X. f x \<in> K} \<inter> C)"
+ proof (rule closedin_compact_space)
+ show "compact_space (subtopology X A)"
+ by (simp add: A_def K YX compact_space_subtopology)
+ show "closedin (subtopology X A) ({x \<in> topspace X. f x \<in> K} \<inter> C)"
+ using A_def C closedin_subtopology by blast
+ qed
+ have "continuous_map (subtopology X A) (subtopology Y K) f" if "kc_space X"
+ unfolding continuous_map_closedin
+ proof (intro conjI strip)
+ show "f x \<in> topspace (subtopology Y K)"
+ if "x \<in> topspace (subtopology X A)" for x
+ using that A_def K compactin_subset_topspace by auto
+ next
+ fix C
+ assume C: "closedin (subtopology Y K) C"
+ show "closedin (subtopology X A) {x \<in> topspace (subtopology X A). f x \<in> C}"
+ proof (rule compactin_imp_closedin_gen)
+ show "kc_space (subtopology X A)"
+ by (simp add: kc_space_subtopology that)
+ have [simp]: "{x \<in> topspace X. f x \<in> K \<and> f x \<in> C} = {x \<in> topspace X. f x \<in> C}"
+ using C closedin_imp_subset by auto
+ have "compactin (subtopology Y K) C"
+ by (simp add: C K closedin_compact_space compact_space_subtopology)
+ then have "compactin X {x \<in> topspace X. x \<in> A \<and> f x \<in> C}"
+ by (auto simp: A_def compactin_subtopology dest: YX)
+ then show "compactin (subtopology X A) {x \<in> topspace (subtopology X A). f x \<in> C}"
+ by (auto simp add: compactin_subtopology)
+ qed
+ qed
+ with f show "continuous_map (subtopology X A) Y f"
+ using continuous_map_from_subtopology continuous_map_in_subtopology by blast
+ qed
+ qed
+qed (simp add: YX)
+
+lemma tube_lemma_left:
+ assumes W: "openin (prod_topology X Y) W" and C: "compactin X C"
+ and y: "y \<in> topspace Y" and subW: "C \<times> {y} \<subseteq> W"
+ shows "\<exists>U V. openin X U \<and> openin Y V \<and> C \<subseteq> U \<and> y \<in> V \<and> U \<times> V \<subseteq> W"
+proof (cases "C = {}")
+ case True
+ with y show ?thesis by auto
+next
+ case False
+ have "\<exists>U V. openin X U \<and> openin Y V \<and> x \<in> U \<and> y \<in> V \<and> U \<times> V \<subseteq> W"
+ if "x \<in> C" for x
+ using W openin_prod_topology_alt subW subsetD that by fastforce
+ then obtain U V where UV: "\<And>x. x \<in> C \<Longrightarrow> openin X (U x) \<and> openin Y (V x) \<and> x \<in> U x \<and> y \<in> V x \<and> U x \<times> V x \<subseteq> W"
+ by metis
+ then obtain D where D: "finite D" "D \<subseteq> C" "C \<subseteq> \<Union> (U ` D)"
+ using compactinD [OF C, of "U`C"]
+ by (smt (verit) UN_I finite_subset_image imageE subsetI)
+ show ?thesis
+ proof (intro exI conjI)
+ show "openin X (\<Union> (U ` D))" "openin Y (\<Inter> (V ` D))"
+ using D False UV by blast+
+ show "y \<in> \<Inter> (V ` D)" "C \<subseteq> \<Union> (U ` D)" "\<Union>(U ` D) \<times> \<Inter>(V ` D) \<subseteq> W"
+ using D UV by force+
+ qed
+qed
+
+lemma Wallace_theorem_prod_topology:
+ assumes "compactin X K" "compactin Y L"
+ and W: "openin (prod_topology X Y) W" and subW: "K \<times> L \<subseteq> W"
+ obtains U V where "openin X U" "openin Y V" "K \<subseteq> U" "L \<subseteq> V" "U \<times> V \<subseteq> W"
+proof -
+ have "\<And>y. y \<in> L \<Longrightarrow> \<exists>U V. openin X U \<and> openin Y V \<and> K \<subseteq> U \<and> y \<in> V \<and> U \<times> V \<subseteq> W"
+ proof (intro tube_lemma_left assms)
+ fix y assume "y \<in> L"
+ show "y \<in> topspace Y"
+ using assms \<open>y \<in> L\<close> compactin_subset_topspace by blast
+ show "K \<times> {y} \<subseteq> W"
+ using \<open>y \<in> L\<close> subW by force
+ qed
+ then obtain U V where UV:
+ "\<And>y. y \<in> L \<Longrightarrow> openin X (U y) \<and> openin Y (V y) \<and> K \<subseteq> U y \<and> y \<in> V y \<and> U y \<times> V y \<subseteq> W"
+ by metis
+ then obtain M where "finite M" "M \<subseteq> L" and M: "L \<subseteq> \<Union> (V ` M)"
+ using \<open>compactin Y L\<close> unfolding compactin_def
+ by (smt (verit) UN_iff finite_subset_image imageE subset_iff)
+ show thesis
+ proof (cases "M={}")
+ case True
+ with M have "L={}"
+ by blast
+ then show ?thesis
+ using \<open>compactin X K\<close> compactin_subset_topspace that by fastforce
+ next
+ case False
+ show ?thesis
+ proof
+ show "openin X (\<Inter>(U`M))"
+ using False UV \<open>M \<subseteq> L\<close> \<open>finite M\<close> by blast
+ show "openin Y (\<Union>(V`M))"
+ using UV \<open>M \<subseteq> L\<close> by blast
+ show "K \<subseteq> \<Inter>(U`M)"
+ by (meson INF_greatest UV \<open>M \<subseteq> L\<close> subsetD)
+ show "L \<subseteq> \<Union>(V`M)"
+ by (simp add: M)
+ show "\<Inter>(U`M) \<times> \<Union>(V`M) \<subseteq> W"
+ using UV \<open>M \<subseteq> L\<close> by fastforce
+ qed
+ qed
+qed
+
+lemma proper_map_prod:
+ "proper_map (prod_topology X Y) (prod_topology X' Y') (\<lambda>(x,y). (f x, g y)) \<longleftrightarrow>
+ topspace(prod_topology X Y) = {} \<or> proper_map X X' f \<and> proper_map Y Y' g"
+ (is "?lhs \<longleftrightarrow> _ \<or> ?rhs")
+proof (cases "topspace(prod_topology X Y) = {}")
+ case True
+ then show ?thesis
+ by (simp add: proper_map_on_empty)
+next
+ case False
+ then have ne: "topspace X \<noteq> {}" "topspace Y \<noteq> {}"
+ by auto
+ define h where "h \<equiv> \<lambda>(x,y). (f x, g y)"
+ have "proper_map X X' f" "proper_map Y Y' g" if ?lhs
+ proof -
+ have cm: "closed_map X X' f" "closed_map Y Y' g"
+ using that False closed_map_prod proper_imp_closed_map by blast+
+ show "proper_map X X' f"
+ proof (clarsimp simp add: proper_map_def cm)
+ fix y
+ assume y: "y \<in> topspace X'"
+ obtain z where z: "z \<in> topspace Y"
+ using ne by blast
+ then have eq: "{x \<in> topspace X. f x = y} =
+ fst ` {u \<in> topspace X \<times> topspace Y. h u = (y,g z)}"
+ by (force simp: h_def)
+ show "compactin X {x \<in> topspace X. f x = y}"
+ unfolding eq
+ proof (intro image_compactin)
+ have "g z \<in> topspace Y'"
+ by (meson closed_map_def closedin_subset closedin_topspace cm image_subset_iff z)
+ with y show "compactin (prod_topology X Y) {u \<in> topspace X \<times> topspace Y. (h u) = (y, g z)}"
+ using that by (simp add: h_def proper_map_def)
+ show "continuous_map (prod_topology X Y) X fst"
+ by (simp add: continuous_map_fst)
+ qed
+ qed
+ show "proper_map Y Y' g"
+ proof (clarsimp simp add: proper_map_def cm)
+ fix y
+ assume y: "y \<in> topspace Y'"
+ obtain z where z: "z \<in> topspace X"
+ using ne by blast
+ then have eq: "{x \<in> topspace Y. g x = y} =
+ snd ` {u \<in> topspace X \<times> topspace Y. h u = (f z,y)}"
+ by (force simp: h_def)
+ show "compactin Y {x \<in> topspace Y. g x = y}"
+ unfolding eq
+ proof (intro image_compactin)
+ have "f z \<in> topspace X'"
+ by (meson closed_map_def closedin_subset closedin_topspace cm image_subset_iff z)
+ with y show "compactin (prod_topology X Y) {u \<in> topspace X \<times> topspace Y. (h u) = (f z, y)}"
+ using that by (simp add: proper_map_def h_def)
+ show "continuous_map (prod_topology X Y) Y snd"
+ by (simp add: continuous_map_snd)
+ qed
+ qed
+ qed
+ moreover
+ { assume R: ?rhs
+ then have fgim: "f ` topspace X \<subseteq> topspace X'" "g ` topspace Y \<subseteq> topspace Y'"
+ and cm: "closed_map X X' f" "closed_map Y Y' g"
+ by (auto simp: proper_map_def closed_map_imp_subset_topspace)
+ have "closed_map (prod_topology X Y) (prod_topology X' Y') h"
+ unfolding closed_map_fibre_neighbourhood imp_conjL
+ proof (intro conjI strip)
+ show "h ` topspace (prod_topology X Y) \<subseteq> topspace (prod_topology X' Y')"
+ unfolding h_def using fgim by auto
+ fix W w
+ assume W: "openin (prod_topology X Y) W"
+ and w: "w \<in> topspace (prod_topology X' Y')"
+ and subW: "{x \<in> topspace (prod_topology X Y). h x = w} \<subseteq> W"
+ then obtain x' y' where weq: "w = (x',y')" "x' \<in> topspace X'" "y' \<in> topspace Y'"
+ by auto
+ have eq: "{u \<in> topspace X \<times> topspace Y. h u = (x',y')} = {x \<in> topspace X. f x = x'} \<times> {y \<in> topspace Y. g y = y'}"
+ by (auto simp: h_def)
+ obtain U V where "openin X U" "openin Y V" "U \<times> V \<subseteq> W"
+ and U: "{x \<in> topspace X. f x = x'} \<subseteq> U"
+ and V: "{x \<in> topspace Y. g x = y'} \<subseteq> V"
+ proof (rule Wallace_theorem_prod_topology)
+ show "compactin X {x \<in> topspace X. f x = x'}" "compactin Y {x \<in> topspace Y. g x = y'}"
+ using R weq unfolding proper_map_def closed_map_fibre_neighbourhood by fastforce+
+ show "{x \<in> topspace X. f x = x'} \<times> {x \<in> topspace Y. g x = y'} \<subseteq> W"
+ using weq subW by (auto simp: h_def)
+ qed (use W in auto)
+ obtain U' where "openin X' U'" "x' \<in> U'" and U': "{x \<in> topspace X. f x \<in> U'} \<subseteq> U"
+ using cm U \<open>openin X U\<close> weq unfolding closed_map_fibre_neighbourhood by meson
+ obtain V' where "openin Y' V'" "y' \<in> V'" and V': "{x \<in> topspace Y. g x \<in> V'} \<subseteq> V"
+ using cm V \<open>openin Y V\<close> weq unfolding closed_map_fibre_neighbourhood by meson
+ show "\<exists>V. openin (prod_topology X' Y') V \<and> w \<in> V \<and> {x \<in> topspace (prod_topology X Y). h x \<in> V} \<subseteq> W"
+ proof (intro conjI exI)
+ show "openin (prod_topology X' Y') (U' \<times> V')"
+ by (simp add: \<open>openin X' U'\<close> \<open>openin Y' V'\<close> openin_prod_Times_iff)
+ show "w \<in> U' \<times> V'"
+ using \<open>x' \<in> U'\<close> \<open>y' \<in> V'\<close> weq by blast
+ show "{x \<in> topspace (prod_topology X Y). h x \<in> U' \<times> V'} \<subseteq> W"
+ using \<open>U \<times> V \<subseteq> W\<close> U' V' h_def by auto
+ qed
+ qed
+ moreover
+ have "compactin (prod_topology X Y) {u \<in> topspace X \<times> topspace Y. h u = (w, z)}"
+ if "w \<in> topspace X'" and "z \<in> topspace Y'" for w z
+ proof -
+ have eq: "{u \<in> topspace X \<times> topspace Y. h u = (w,z)} =
+ {u \<in> topspace X. f u = w} \<times> {y. y \<in> topspace Y \<and> g y = z}"
+ by (auto simp: h_def)
+ show ?thesis
+ using R that by (simp add: eq compactin_Times proper_map_def)
+ qed
+ ultimately have ?lhs
+ by (auto simp: h_def proper_map_def)
+ }
+ ultimately show ?thesis using False by metis
+qed
+
+lemma proper_map_paired:
+ assumes "Hausdorff_space X \<and> proper_map X Y f \<and> proper_map X Z g \<or>
+ Hausdorff_space Y \<and> continuous_map X Y f \<and> proper_map X Z g \<or>
+ Hausdorff_space Z \<and> proper_map X Y f \<and> continuous_map X Z g"
+ shows "proper_map X (prod_topology Y Z) (\<lambda>x. (f x,g x))"
+ using assms
+proof (elim disjE conjE)
+ assume \<section>: "Hausdorff_space X" "proper_map X Y f" "proper_map X Z g"
+ have eq: "(\<lambda>x. (f x, g x)) = (\<lambda>(x, y). (f x, g y)) \<circ> (\<lambda>x. (x, x))"
+ by auto
+ show "proper_map X (prod_topology Y Z) (\<lambda>x. (f x, g x))"
+ unfolding eq
+ proof (rule proper_map_compose)
+ show "proper_map X (prod_topology X X) (\<lambda>x. (x,x))"
+ by (simp add: \<section>)
+ show "proper_map (prod_topology X X) (prod_topology Y Z) (\<lambda>(x,y). (f x, g y))"
+ by (simp add: \<section> proper_map_prod)
+ qed
+next
+ assume \<section>: "Hausdorff_space Y" "continuous_map X Y f" "proper_map X Z g"
+ have eq: "(\<lambda>x. (f x, g x)) = (\<lambda>(x,y). (x,g y)) \<circ> (\<lambda>x. (f x,x))"
+ by auto
+ show "proper_map X (prod_topology Y Z) (\<lambda>x. (f x, g x))"
+ unfolding eq
+ proof (rule proper_map_compose)
+ show "proper_map X (prod_topology Y X) (\<lambda>x. (f x,x))"
+ by (simp add: \<section> proper_map_paired_continuous_map_left)
+ show "proper_map (prod_topology Y X) (prod_topology Y Z) (\<lambda>(x,y). (x,g y))"
+ by (simp add: \<section> proper_map_prod proper_map_id [unfolded id_def])
+ qed
+next
+ assume \<section>: "Hausdorff_space Z" "proper_map X Y f" "continuous_map X Z g"
+ have eq: "(\<lambda>x. (f x, g x)) = (\<lambda>(x,y). (f x,y)) \<circ> (\<lambda>x. (x,g x))"
+ by auto
+ show "proper_map X (prod_topology Y Z) (\<lambda>x. (f x, g x))"
+ unfolding eq
+ proof (rule proper_map_compose)
+ show "proper_map X (prod_topology X Z) (\<lambda>x. (x, g x))"
+ using \<section> proper_map_paired_continuous_map_right by auto
+ show "proper_map (prod_topology X Z) (prod_topology Y Z) (\<lambda>(x,y). (f x,y))"
+ by (simp add: \<section> proper_map_prod proper_map_id [unfolded id_def])
+ qed
+qed
+
+lemma proper_map_pairwise:
+ assumes
+ "Hausdorff_space X \<and> proper_map X Y (fst \<circ> f) \<and> proper_map X Z (snd \<circ> f) \<or>
+ Hausdorff_space Y \<and> continuous_map X Y (fst \<circ> f) \<and> proper_map X Z (snd \<circ> f) \<or>
+ Hausdorff_space Z \<and> proper_map X Y (fst \<circ> f) \<and> continuous_map X Z (snd \<circ> f)"
+ shows "proper_map X (prod_topology Y Z) f"
+ using proper_map_paired [OF assms] by (simp add: o_def)
+
+lemma proper_map_from_composition_right:
+ assumes "Hausdorff_space Y" "proper_map X Z (g \<circ> f)" and "continuous_map X Y f"
+ and contg: "continuous_map Y Z g"
+ shows "proper_map X Y f"
+proof -
+ define YZ where "YZ \<equiv> subtopology (prod_topology Y Z) ((\<lambda>x. (x, g x)) ` topspace Y)"
+ have "proper_map X Y (fst \<circ> (\<lambda>x. (f x, (g \<circ> f) x)))"
+ proof (rule proper_map_compose)
+ have [simp]: "x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y" for x
+ by (meson assms(3) continuous_map_def)
+ show "proper_map X YZ (\<lambda>x. (f x, (g \<circ> f) x))"
+ unfolding YZ_def
+ using assms
+ by (force intro!: proper_map_into_subtopology proper_map_paired simp: o_def image_iff)+
+ show "proper_map YZ Y fst"
+ using contg
+ by (simp flip: homeomorphic_maps_graph add: YZ_def homeomorphic_maps_map homeomorphic_imp_proper_map)
+ qed
+ moreover have "fst \<circ> (\<lambda>x. (f x, (g \<circ> f) x)) = f"
+ by auto
+ ultimately show ?thesis
+ by auto
+qed
+
+lemma perfect_map_from_composition_right:
+ "\<lbrakk>Hausdorff_space Y; perfect_map X Z (g \<circ> f);
+ continuous_map X Y f; continuous_map Y Z g; f ` topspace X = topspace Y\<rbrakk>
+ \<Longrightarrow> perfect_map X Y f"
+ by (meson perfect_map_def proper_map_from_composition_right)
+
+lemma perfect_map_from_composition_right_inj:
+ "\<lbrakk>perfect_map X Z (g \<circ> f); f ` topspace X = topspace Y;
+ continuous_map X Y f; continuous_map Y Z g; inj_on g (topspace Y)\<rbrakk>
+ \<Longrightarrow> perfect_map X Y f"
+ by (meson continuous_map_image_subset_topspace perfect_map_def proper_map_from_composition_right_inj)
+
subsection \<open>Regular spaces\<close>
@@ -2022,6 +2360,10 @@
by auto
qed
+lemma continuous_imp_proper_map:
+ "\<lbrakk>compact_space X; kc_space Y; continuous_map X Y f\<rbrakk> \<Longrightarrow> proper_map X Y f"
+ by (simp add: continuous_closed_imp_proper_map continuous_imp_closed_map_gen kc_imp_t1_space)
+
lemma tube_lemma_right:
assumes W: "openin (prod_topology X Y) W" and C: "compactin Y C"
@@ -2060,8 +2402,7 @@
have **: "\<And>U y. \<lbrakk>openin (prod_topology X Y) U; y \<in> topspace X;
{x \<in> topspace X \<times> topspace Y. fst x = y} \<subseteq> U\<rbrakk>
\<Longrightarrow> \<exists>V. openin X V \<and> y \<in> V \<and> V \<times> topspace Y \<subseteq> U"
- using tube_lemma_right[of X Y _ "topspace Y"] assms compact_space_def
- by force
+ using tube_lemma_right[of X Y _ "topspace Y"] assms by (fastforce simp: compact_space_def)
show ?thesis
unfolding closed_map_fibre_neighbourhood
by (force simp: * openin_subset cong: conj_cong intro: **)
@@ -2492,17 +2833,19 @@
qed
lemma locally_compact_space_open_subset:
- assumes reg: "regular_space X" and loc: "locally_compact_space X" and "openin X S"
+ assumes X: "Hausdorff_space X \<or> regular_space X" and loc: "locally_compact_space X" and "openin X S"
shows "locally_compact_space (subtopology X S)"
proof (clarsimp simp: locally_compact_space_def)
fix x assume x: "x \<in> topspace X" "x \<in> S"
then obtain U K where UK: "openin X U" "compactin X K" "x \<in> U" "U \<subseteq> K"
by (meson loc locally_compact_space_def)
- have "openin X (U \<inter> S)"
+ moreover have reg: "regular_space X"
+ using X loc locally_compact_Hausdorff_imp_regular_space by blast
+ moreover have "openin X (U \<inter> S)"
by (simp add: UK \<open>openin X S\<close> openin_Int)
- with UK reg x obtain V C
+ ultimately obtain V C
where VC: "openin X V" "closedin X C" "x \<in> V" "V \<subseteq> C" "C \<subseteq> U" "C \<subseteq> S"
- by (metis IntI le_inf_iff neighbourhood_base_of neighbourhood_base_of_closedin)
+ by (metis \<open>x \<in> S\<close> IntI le_inf_iff neighbourhood_base_of neighbourhood_base_of_closedin)
show "\<exists>U. openin (subtopology X S) U \<and>
(\<exists>K. compactin (subtopology X S) K \<and> x \<in> U \<and> U \<subseteq> K)"
proof (intro conjI exI)
@@ -2575,19 +2918,17 @@
then have "C \<subseteq> topspace X"
by (simp add: closedin_subset)
have "locally_compact_space (subtopology (subtopology X C) (topspace (subtopology X C) \<inter> U))"
- proof (rule locally_compact_space_open_subset)
- show "regular_space (subtopology X C)"
- by (simp add: \<open>Hausdorff_space X\<close> loc locally_compact_Hausdorff_imp_regular_space regular_space_subtopology)
- show "locally_compact_space (subtopology X C)"
- by (simp add: \<open>closedin X C\<close> loc locally_compact_space_closed_subset)
- show "openin (subtopology X C) (topspace (subtopology X C) \<inter> U)"
- by (simp add: \<open>openin X U\<close> Int_left_commute inf_commute openin_Int openin_subtopology_Int2)
-qed
- then show ?rhs
- by (metis Seq \<open>C \<subseteq> topspace X\<close> inf.coboundedI1 subtopology_subtopology subtopology_topspace)
+ proof (rule locally_compact_space_open_subset)
+ show "locally_compact_space (subtopology X C)"
+ by (simp add: \<open>closedin X C\<close> loc locally_compact_space_closed_subset)
+ show "openin (subtopology X C) (topspace (subtopology X C) \<inter> U)"
+ by (simp add: \<open>openin X U\<close> Int_left_commute inf_commute openin_Int openin_subtopology_Int2)
+ qed (simp add: Hausdorff_space_subtopology \<open>Hausdorff_space X\<close>)
+ then show ?rhs
+ by (metis Seq \<open>C \<subseteq> topspace X\<close> inf.coboundedI1 subtopology_subtopology subtopology_topspace)
next
assume ?rhs then show ?lhs
- using assms locally_compact_subspace_closed_Int_openin by blast
+ using assms locally_compact_subspace_closed_Int_openin by blast
qed
lemma dense_locally_compact_openin_Hausdorff_space:
@@ -3505,7 +3846,7 @@
lemma quasi_component_of:
"quasi_component_of X x y \<longleftrightarrow>
x \<in> topspace X \<and> y \<in> topspace X \<and> (\<forall>T. x \<in> T \<and> closedin X T \<and> openin X T \<longrightarrow> y \<in> T)"
- unfolding quasi_component_of_def by blast
+ unfolding quasi_component_of_def by (metis Diff_iff closedin_def openin_closedin_eq)
lemma quasi_component_of_alt:
"quasi_component_of X x y \<longleftrightarrow>
@@ -4433,5 +4774,536 @@
\<Longrightarrow> X frontier_of C \<inter> X frontier_of S \<noteq> {}"
by (simp add: boundary_bumping_theorem_gen closedin_compact_space compact_imp_locally_compact_space)
+subsection \<open>Compactly generated spaces (k-spaces)\<close>
+
+text \<open>These don't have to be Hausdorff\<close>
+
+definition k_space where
+ "k_space X \<equiv>
+ \<forall>S. S \<subseteq> topspace X \<longrightarrow>
+ (closedin X S \<longleftrightarrow> (\<forall>K. compactin X K \<longrightarrow> closedin (subtopology X K) (K \<inter> S)))"
+
+lemma k_space:
+ "k_space X \<longleftrightarrow>
+ (\<forall>S. S \<subseteq> topspace X \<and>
+ (\<forall>K. compactin X K \<longrightarrow> closedin (subtopology X K) (K \<inter> S)) \<longrightarrow> closedin X S)"
+ by (metis closedin_subtopology inf_commute k_space_def)
+
+lemma k_space_open:
+ "k_space X \<longleftrightarrow>
+ (\<forall>S. S \<subseteq> topspace X \<and>
+ (\<forall>K. compactin X K \<longrightarrow> openin (subtopology X K) (K \<inter> S)) \<longrightarrow> openin X S)"
+proof -
+ have "openin X S"
+ if "k_space X" "S \<subseteq> topspace X"
+ and "\<forall>K. compactin X K \<longrightarrow> openin (subtopology X K) (K \<inter> S)" for S
+ using that unfolding k_space openin_closedin_eq
+ by (metis Diff_Int_distrib2 Diff_subset inf_commute topspace_subtopology)
+ moreover have "k_space X"
+ if "\<forall>S. S \<subseteq> topspace X \<and> (\<forall>K. compactin X K \<longrightarrow> openin (subtopology X K) (K \<inter> S)) \<longrightarrow> openin X S"
+ unfolding k_space openin_closedin_eq
+ by (simp add: Diff_Int_distrib closedin_def inf_commute that)
+ ultimately show ?thesis
+ by blast
+qed
+
+lemma k_space_alt:
+ "k_space X \<longleftrightarrow>
+ (\<forall>S. S \<subseteq> topspace X
+ \<longrightarrow> (openin X S \<longleftrightarrow> (\<forall>K. compactin X K \<longrightarrow> openin (subtopology X K) (K \<inter> S))))"
+ by (meson k_space_open openin_subtopology_Int2)
+
+lemma k_space_quotient_map_image:
+ assumes q: "quotient_map X Y q" and X: "k_space X"
+ shows "k_space Y"
+ unfolding k_space
+proof clarify
+ fix S
+ assume "S \<subseteq> topspace Y" and S: "\<forall>K. compactin Y K \<longrightarrow> closedin (subtopology Y K) (K \<inter> S)"
+ then have iff: "closedin X {x \<in> topspace X. q x \<in> S} \<longleftrightarrow> closedin Y S"
+ using q quotient_map_closedin by fastforce
+ have "closedin (subtopology X K) (K \<inter> {x \<in> topspace X. q x \<in> S})" if "compactin X K" for K
+ proof -
+ have "{x \<in> topspace X. q x \<in> q ` K} \<inter> K = K"
+ using compactin_subset_topspace that by blast
+ then have *: "subtopology X K = subtopology (subtopology X {x \<in> topspace X. q x \<in> q ` K}) K"
+ by (simp add: subtopology_subtopology)
+ have **: "K \<inter> {x \<in> topspace X. q x \<in> S} =
+ K \<inter> {x \<in> topspace (subtopology X {x \<in> topspace X. q x \<in> q ` K}). q x \<in> q ` K \<inter> S}"
+ by auto
+ have "K \<subseteq> topspace X"
+ by (simp add: compactin_subset_topspace that)
+ show ?thesis
+ unfolding * **
+ proof (intro closedin_continuous_map_preimage closedin_subtopology_Int_closed)
+ show "continuous_map (subtopology X {x \<in> topspace X. q x \<in> q ` K}) (subtopology Y (q ` K)) q"
+ by (auto simp add: continuous_map_in_subtopology continuous_map_from_subtopology q quotient_imp_continuous_map)
+ show "closedin (subtopology Y (q ` K)) (q ` K \<inter> S)"
+ by (meson S image_compactin q quotient_imp_continuous_map that)
+ qed
+ qed
+ then have "closedin X {x \<in> topspace X. q x \<in> S}"
+ by (metis (no_types, lifting) X k_space mem_Collect_eq subsetI)
+ with iff show "closedin Y S" by simp
+qed
+
+lemma k_space_retraction_map_image:
+ "\<lbrakk>retraction_map X Y r; k_space X\<rbrakk> \<Longrightarrow> k_space Y"
+ using k_space_quotient_map_image retraction_imp_quotient_map by blast
+
+lemma homeomorphic_k_space:
+ "X homeomorphic_space Y \<Longrightarrow> k_space X \<longleftrightarrow> k_space Y"
+ by (meson homeomorphic_map_def homeomorphic_space homeomorphic_space_sym k_space_quotient_map_image)
+
+lemma k_space_perfect_map_image:
+ "\<lbrakk>k_space X; perfect_map X Y f\<rbrakk> \<Longrightarrow> k_space Y"
+ using k_space_quotient_map_image perfect_imp_quotient_map by blast
+
+lemma locally_compact_imp_k_space:
+ assumes "locally_compact_space X"
+ shows "k_space X"
+ unfolding k_space
+proof clarify
+ fix S
+ assume "S \<subseteq> topspace X" and S: "\<forall>K. compactin X K \<longrightarrow> closedin (subtopology X K) (K \<inter> S)"
+ have False if non: "\<not> (X closure_of S \<subseteq> S)"
+ proof -
+ obtain x where "x \<in> X closure_of S" "x \<notin> S"
+ using non by blast
+ then have "x \<in> topspace X"
+ by (simp add: in_closure_of)
+ then obtain K U where "openin X U" "compactin X K" "x \<in> U" "U \<subseteq> K"
+ by (meson assms locally_compact_space_def)
+ then show False
+ using \<open>x \<in> X closure_of S\<close> openin_Int_closure_of_eq [OF \<open>openin X U\<close>]
+ by (smt (verit, ccfv_threshold) Int_iff S \<open>x \<notin> S\<close> closedin_Int_closure_of inf.orderE inf_assoc)
+ qed
+ then show "closedin X S"
+ using S \<open>S \<subseteq> topspace X\<close> closure_of_subset_eq by blast
+qed
+
+lemma compact_imp_k_space:
+ "compact_space X \<Longrightarrow> k_space X"
+ by (simp add: compact_imp_locally_compact_space locally_compact_imp_k_space)
+
+lemma k_space_discrete_topology: "k_space(discrete_topology U)"
+ by (simp add: k_space_open)
+
+lemma k_space_closed_subtopology:
+ assumes "k_space X" "closedin X C"
+ shows "k_space (subtopology X C)"
+unfolding k_space compactin_subtopology
+proof clarsimp
+ fix S
+ assume Ssub: "S \<subseteq> topspace X" "S \<subseteq> C"
+ and S: "\<forall>K. compactin X K \<and> K \<subseteq> C \<longrightarrow> closedin (subtopology (subtopology X C) K) (K \<inter> S)"
+ have "closedin (subtopology X K) (K \<inter> S)" if "compactin X K" for K
+ proof -
+ have "closedin (subtopology (subtopology X C) (K \<inter> C)) ((K \<inter> C) \<inter> S)"
+ by (simp add: S \<open>closedin X C\<close> compact_Int_closedin that)
+ then show ?thesis
+ using \<open>closedin X C\<close> Ssub by (auto simp add: closedin_subtopology)
+ qed
+ then show "closedin (subtopology X C) S"
+ by (metis Ssub \<open>k_space X\<close> closedin_subset_topspace k_space_def)
+qed
+
+lemma k_space_subtopology:
+ assumes 1: "\<And>T. \<lbrakk>T \<subseteq> topspace X; T \<subseteq> S;
+ \<And>K. compactin X K \<Longrightarrow> closedin (subtopology X (K \<inter> S)) (K \<inter> T)\<rbrakk> \<Longrightarrow> closedin (subtopology X S) T"
+ assumes 2: "\<And>K. compactin X K \<Longrightarrow> k_space(subtopology X (K \<inter> S))"
+ shows "k_space (subtopology X S)"
+ unfolding k_space
+proof (intro conjI strip)
+ fix U
+ assume \<section>: "U \<subseteq> topspace (subtopology X S) \<and> (\<forall>K. compactin (subtopology X S) K \<longrightarrow> closedin (subtopology (subtopology X S) K) (K \<inter> U))"
+ have "closedin (subtopology X (K \<inter> S)) (K \<inter> U)" if "compactin X K" for K
+ proof -
+ have "K \<inter> U \<subseteq> topspace (subtopology X (K \<inter> S))"
+ using "\<section>" by auto
+ moreover
+ have "\<And>K'. compactin (subtopology X (K \<inter> S)) K' \<Longrightarrow> closedin (subtopology (subtopology X (K \<inter> S)) K') (K' \<inter> K \<inter> U)"
+ by (metis "\<section>" compactin_subtopology inf.orderE inf_commute subtopology_subtopology)
+ ultimately show ?thesis
+ by (metis (no_types, opaque_lifting) "2" inf.assoc k_space_def that)
+ qed
+ then show "closedin (subtopology X S) U"
+ using "1" \<section> by auto
+qed
+
+lemma k_space_subtopology_open:
+ assumes 1: "\<And>T. \<lbrakk>T \<subseteq> topspace X; T \<subseteq> S;
+ \<And>K. compactin X K \<Longrightarrow> openin (subtopology X (K \<inter> S)) (K \<inter> T)\<rbrakk> \<Longrightarrow> openin (subtopology X S) T"
+ assumes 2: "\<And>K. compactin X K \<Longrightarrow> k_space(subtopology X (K \<inter> S))"
+ shows "k_space (subtopology X S)"
+ unfolding k_space_open
+proof (intro conjI strip)
+ fix U
+ assume \<section>: "U \<subseteq> topspace (subtopology X S) \<and> (\<forall>K. compactin (subtopology X S) K \<longrightarrow> openin (subtopology (subtopology X S) K) (K \<inter> U))"
+ have "openin (subtopology X (K \<inter> S)) (K \<inter> U)" if "compactin X K" for K
+ proof -
+ have "K \<inter> U \<subseteq> topspace (subtopology X (K \<inter> S))"
+ using "\<section>" by auto
+ moreover
+ have "\<And>K'. compactin (subtopology X (K \<inter> S)) K' \<Longrightarrow> openin (subtopology (subtopology X (K \<inter> S)) K') (K' \<inter> K \<inter> U)"
+ by (metis "\<section>" compactin_subtopology inf.orderE inf_commute subtopology_subtopology)
+ ultimately show ?thesis
+ by (metis (no_types, opaque_lifting) "2" inf.assoc k_space_open that)
+ qed
+ then show "openin (subtopology X S) U"
+ using "1" \<section> by auto
+qed
+
+
+lemma k_space_open_subtopology_aux:
+ assumes "kc_space X" "compact_space X" "openin X V"
+ shows "k_space (subtopology X V)"
+proof (clarsimp simp: k_space subtopology_subtopology compactin_subtopology Int_absorb1)
+ fix S
+ assume "S \<subseteq> topspace X"
+ and "S \<subseteq> V"
+ and S: "\<forall>K. compactin X K \<and> K \<subseteq> V \<longrightarrow> closedin (subtopology X K) (K \<inter> S)"
+ then have "V \<subseteq> topspace X"
+ using assms openin_subset by blast
+ have "S = V \<inter> ((topspace X - V) \<union> S)"
+ using \<open>S \<subseteq> V\<close> by auto
+ moreover have "closedin (subtopology X V) (V \<inter> ((topspace X - V) \<union> S))"
+ proof (intro closedin_subtopology_Int_closed compactin_imp_closedin_gen \<open>kc_space X\<close>)
+ show "compactin X (topspace X - V \<union> S)"
+ unfolding compactin_def
+ proof (intro conjI strip)
+ show "topspace X - V \<union> S \<subseteq> topspace X"
+ by (simp add: \<open>S \<subseteq> topspace X\<close>)
+ fix \<U>
+ assume \<U>: "Ball \<U> (openin X) \<and> topspace X - V \<union> S \<subseteq> \<Union>\<U>"
+ moreover
+ have "compactin X (topspace X - V)"
+ using assms closedin_compact_space by blast
+ ultimately obtain \<G> where "finite \<G>" "\<G> \<subseteq> \<U>" and \<G>: "topspace X - V \<subseteq> \<Union>\<G>"
+ unfolding compactin_def using \<open>V \<subseteq> topspace X\<close> by (metis le_sup_iff)
+ then have "topspace X - \<Union>\<G> \<subseteq> V"
+ by blast
+ then have "closedin (subtopology X (topspace X - \<Union>\<G>)) ((topspace X - \<Union>\<G>) \<inter> S)"
+ by (meson S \<U> \<open>\<G> \<subseteq> \<U>\<close> \<open>compact_space X\<close> closedin_compact_space openin_Union openin_closedin_eq subset_iff)
+ then have "compactin X ((topspace X - \<Union>\<G>) \<inter> S)"
+ by (meson \<U> \<open>\<G> \<subseteq> \<U>\<close>\<open>compact_space X\<close> closedin_compact_space closedin_trans_full openin_Union openin_closedin_eq subset_iff)
+ then obtain \<H> where "finite \<H>" "\<H> \<subseteq> \<U>" "(topspace X - \<Union>\<G>) \<inter> S \<subseteq> \<Union>\<H>"
+ unfolding compactin_def by (smt (verit, best) \<U> inf_le2 subset_trans sup.boundedE)
+ with \<G> have "topspace X - V \<union> S \<subseteq> \<Union>(\<G> \<union> \<H>)"
+ using \<open>S \<subseteq> topspace X\<close> by auto
+ then show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> topspace X - V \<union> S \<subseteq> \<Union>\<F>"
+ by (metis \<open>\<G> \<subseteq> \<U>\<close> \<open>\<H> \<subseteq> \<U>\<close> \<open>finite \<G>\<close> \<open>finite \<H>\<close> finite_Un le_sup_iff)
+ qed
+ qed
+ ultimately show "closedin (subtopology X V) S"
+ by metis
+qed
+
+
+lemma k_space_open_subtopology:
+ assumes X: "kc_space X \<or> Hausdorff_space X \<or> regular_space X" and "k_space X" "openin X S"
+ shows "k_space(subtopology X S)"
+proof (rule k_space_subtopology_open)
+ fix T
+ assume "T \<subseteq> topspace X"
+ and "T \<subseteq> S"
+ and T: "\<And>K. compactin X K \<Longrightarrow> openin (subtopology X (K \<inter> S)) (K \<inter> T)"
+ have "openin (subtopology X K) (K \<inter> T)" if "compactin X K" for K
+ by (smt (verit, ccfv_threshold) T assms(3) inf_assoc inf_commute openin_Int openin_subtopology that)
+ then show "openin (subtopology X S) T"
+ by (metis \<open>T \<subseteq> S\<close> \<open>T \<subseteq> topspace X\<close> assms(2) k_space_alt subset_openin_subtopology)
+next
+ fix K
+ assume "compactin X K"
+ then have KS: "openin (subtopology X K) (K \<inter> S)"
+ by (simp add: \<open>openin X S\<close> openin_subtopology_Int2)
+ have XK: "compact_space (subtopology X K)"
+ by (simp add: \<open>compactin X K\<close> compact_space_subtopology)
+ show "k_space (subtopology X (K \<inter> S))"
+ using X
+ proof (rule disjE)
+ assume "kc_space X"
+ then show "k_space (subtopology X (K \<inter> S))"
+ using k_space_open_subtopology_aux [of "subtopology X K" "K \<inter> S"]
+ by (simp add: KS XK kc_space_subtopology subtopology_subtopology)
+ next
+ assume "Hausdorff_space X \<or> regular_space X"
+ then have "locally_compact_space (subtopology (subtopology X K) (K \<inter> S))"
+ using locally_compact_space_open_subset Hausdorff_space_subtopology KS XK
+ compact_imp_locally_compact_space regular_space_subtopology by blast
+ then show "k_space (subtopology X (K \<inter> S))"
+ by (simp add: locally_compact_imp_k_space subtopology_subtopology)
+ qed
+qed
+
+lemma k_kc_space_subtopology:
+ "\<lbrakk>k_space X; kc_space X; openin X S \<or> closedin X S\<rbrakk> \<Longrightarrow> k_space(subtopology X S) \<and> kc_space(subtopology X S)"
+ by (metis k_space_closed_subtopology k_space_open_subtopology kc_space_subtopology)
+
+
+lemma k_space_as_quotient_explicit:
+ "k_space X \<longleftrightarrow> quotient_map (sum_topology (subtopology X) {K. compactin X K}) X snd"
+proof -
+ have [simp]: "{x \<in> topspace X. x \<in> K \<and> x \<in> U} = K \<inter> U" if "U \<subseteq> topspace X" for K U
+ using that by blast
+ show "?thesis"
+ apply (simp add: quotient_map_def openin_sum_topology snd_image_Sigma k_space_alt)
+ by (smt (verit, del_insts) Union_iff compactin_sing inf.orderE mem_Collect_eq singletonI subsetI)
+qed
+
+lemma k_space_as_quotient:
+ fixes X :: "'a topology"
+ shows "k_space X \<longleftrightarrow> (\<exists>q. \<exists>Y:: ('a set * 'a) topology. locally_compact_space Y \<and> quotient_map Y X q)"
+ (is "?lhs=?rhs")
+proof
+ show "k_space X" if ?rhs
+ using that k_space_quotient_map_image locally_compact_imp_k_space by blast
+next
+ assume "k_space X"
+ show ?rhs
+ proof (intro exI conjI)
+ show "locally_compact_space (sum_topology (subtopology X) {K. compactin X K})"
+ by (simp add: compact_imp_locally_compact_space compact_space_subtopology locally_compact_space_sum_topology)
+ show "quotient_map (sum_topology (subtopology X) {K. compactin X K}) X snd"
+ using \<open>k_space X\<close> k_space_as_quotient_explicit by blast
+ qed
+qed
+
+lemma k_space_prod_topology_left:
+ assumes X: "locally_compact_space X" "Hausdorff_space X \<or> regular_space X" and "k_space Y"
+ shows "k_space (prod_topology X Y)"
+proof -
+ obtain q and Z :: "('b set * 'b) topology" where "locally_compact_space Z" and q: "quotient_map Z Y q"
+ using \<open>k_space Y\<close> k_space_as_quotient by blast
+ then show ?thesis
+ using quotient_map_prod_right [OF X q] X k_space_quotient_map_image locally_compact_imp_k_space
+ locally_compact_space_prod_topology by blast
+qed
+
+text \<open>Essentially the same proof\<close>
+lemma k_space_prod_topology_right:
+ assumes "k_space X" and Y: "locally_compact_space Y" "Hausdorff_space Y \<or> regular_space Y"
+ shows "k_space (prod_topology X Y)"
+proof -
+ obtain q and Z :: "('a set * 'a) topology" where "locally_compact_space Z" and q: "quotient_map Z X q"
+ using \<open>k_space X\<close> k_space_as_quotient by blast
+ then show ?thesis
+ using quotient_map_prod_left [OF Y q] using Y k_space_quotient_map_image locally_compact_imp_k_space
+ locally_compact_space_prod_topology by blast
+qed
+
+
+lemma continuous_map_from_k_space:
+ assumes "k_space X" and f: "\<And>K. compactin X K \<Longrightarrow> continuous_map(subtopology X K) Y f"
+ shows "continuous_map X Y f"
+proof -
+ have "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y"
+ by (metis compactin_absolute compactin_sing f image_compactin image_empty image_insert)
+ moreover have "closedin X {x \<in> topspace X. f x \<in> C}" if "closedin Y C" for C
+ proof -
+ have "{x \<in> topspace X. f x \<in> C} \<subseteq> topspace X"
+ by fastforce
+ moreover
+ have eq: "K \<inter> {x \<in> topspace X. f x \<in> C} = {x. x \<in> topspace(subtopology X K) \<and> f x \<in> (f ` K \<inter> C)}" for K
+ by auto
+ have "closedin (subtopology X K) (K \<inter> {x \<in> topspace X. f x \<in> C})" if "compactin X K" for K
+ unfolding eq
+ proof (rule closedin_continuous_map_preimage)
+ show "continuous_map (subtopology X K) (subtopology Y (f`K)) f"
+ by (simp add: continuous_map_in_subtopology f image_mono that)
+ show "closedin (subtopology Y (f`K)) (f ` K \<inter> C)"
+ using \<open>closedin Y C\<close> closedin_subtopology by blast
+ qed
+ ultimately show ?thesis
+ using \<open>k_space X\<close> k_space by blast
+ qed
+ ultimately show ?thesis
+ by (simp add: continuous_map_closedin)
+qed
+
+lemma closed_map_into_k_space:
+ assumes "k_space Y" and fim: "f ` (topspace X) \<subseteq> topspace Y"
+ and f: "\<And>K. compactin Y K
+ \<Longrightarrow> closed_map(subtopology X {x \<in> topspace X. f x \<in> K}) (subtopology Y K) f"
+ shows "closed_map X Y f"
+ unfolding closed_map_def
+proof (intro strip)
+ fix C
+ assume "closedin X C"
+ have "closedin (subtopology Y K) (K \<inter> f ` C)"
+ if "compactin Y K" for K
+ proof -
+ have eq: "K \<inter> f ` C = f ` ({x \<in> topspace X. f x \<in> K} \<inter> C)"
+ using \<open>closedin X C\<close> closedin_subset by auto
+ show ?thesis
+ unfolding eq
+ by (metis (no_types, lifting) \<open>closedin X C\<close> closed_map_def closedin_subtopology f inf_commute that)
+ qed
+ then show "closedin Y (f ` C)"
+ using \<open>k_space Y\<close> unfolding k_space
+ by (meson \<open>closedin X C\<close> closedin_subset dual_order.trans fim image_mono)
+qed
+
+
+text \<open>Essentially the same proof\<close>
+lemma open_map_into_k_space:
+ assumes "k_space Y" and fim: "f ` (topspace X) \<subseteq> topspace Y"
+ and f: "\<And>K. compactin Y K
+ \<Longrightarrow> open_map (subtopology X {x \<in> topspace X. f x \<in> K}) (subtopology Y K) f"
+ shows "open_map X Y f"
+ unfolding open_map_def
+proof (intro strip)
+ fix C
+ assume "openin X C"
+ have "openin (subtopology Y K) (K \<inter> f ` C)"
+ if "compactin Y K" for K
+ proof -
+ have eq: "K \<inter> f ` C = f ` ({x \<in> topspace X. f x \<in> K} \<inter> C)"
+ using \<open>openin X C\<close> openin_subset by auto
+ show ?thesis
+ unfolding eq
+ by (metis (no_types, lifting) \<open>openin X C\<close> open_map_def openin_subtopology f inf_commute that)
+ qed
+ then show "openin Y (f ` C)"
+ using \<open>k_space Y\<close> unfolding k_space_open
+ by (meson \<open>openin X C\<close> openin_subset dual_order.trans fim image_mono)
+qed
+
+lemma quotient_map_into_k_space:
+ fixes f :: "'a \<Rightarrow> 'b"
+ assumes "k_space Y" and cmf: "continuous_map X Y f"
+ and fim: "f ` (topspace X) = topspace Y"
+ and f: "\<And>k. compactin Y k
+ \<Longrightarrow> quotient_map (subtopology X {x \<in> topspace X. f x \<in> k})
+ (subtopology Y k) f"
+ shows "quotient_map X Y f"
+proof -
+ have "closedin Y C"
+ if "C \<subseteq> topspace Y" and K: "closedin X {x \<in> topspace X. f x \<in> C}" for C
+ proof -
+ have "closedin (subtopology Y K) (K \<inter> C)" if "compactin Y K" for K
+ proof -
+ define Kf where "Kf \<equiv> {x \<in> topspace X. f x \<in> K}"
+ have *: "K \<inter> C \<subseteq> topspace Y \<and> K \<inter> C \<subseteq> K"
+ using \<open>C \<subseteq> topspace Y\<close> by blast
+ then have eq: "closedin (subtopology X Kf) (Kf \<inter> {x \<in> topspace X. f x \<in> C}) =
+ closedin (subtopology Y K) (K \<inter> C)"
+ using f [OF that] * unfolding quotient_map_closedin Kf_def
+ by (smt (verit, ccfv_SIG) Collect_cong Int_def compactin_subset_topspace mem_Collect_eq that topspace_subtopology topspace_subtopology_subset)
+ have dd: "{x \<in> topspace X \<inter> Kf. f x \<in> K \<inter> C} = Kf \<inter> {x \<in> topspace X. f x \<in> C}"
+ by (auto simp add: Kf_def)
+ have "closedin (subtopology X Kf) {x \<in> topspace X. x \<in> Kf \<and> f x \<in> K \<and> f x \<in> C}"
+ using K closedin_subtopology by (fastforce simp add: Kf_def)
+ with K closedin_subtopology_Int_closed eq show ?thesis
+ by blast
+ qed
+ then show ?thesis
+ using \<open>k_space Y\<close> that unfolding k_space by blast
+ qed
+ moreover have "closedin X {x \<in> topspace X. f x \<in> K}"
+ if "K \<subseteq> topspace Y" "closedin Y K" for K
+ using that cmf continuous_map_closedin by fastforce
+ ultimately show ?thesis
+ unfolding quotient_map_closedin using fim by blast
+qed
+
+lemma quotient_map_into_k_space_eq:
+ assumes "k_space Y" "kc_space Y"
+ shows "quotient_map X Y f \<longleftrightarrow>
+ continuous_map X Y f \<and> f ` (topspace X) = topspace Y \<and>
+ (\<forall>K. compactin Y K
+ \<longrightarrow> quotient_map (subtopology X {x \<in> topspace X. f x \<in> K}) (subtopology Y K) f)"
+ using assms
+ by (auto simp: kc_space_def intro: quotient_map_into_k_space quotient_map_restriction
+ dest: quotient_imp_continuous_map quotient_imp_surjective_map)
+
+lemma open_map_into_k_space_eq:
+ assumes "k_space Y"
+ shows "open_map X Y f \<longleftrightarrow>
+ f ` (topspace X) \<subseteq> topspace Y \<and>
+ (\<forall>k. compactin Y k
+ \<longrightarrow> open_map (subtopology X {x \<in> topspace X. f x \<in> k}) (subtopology Y k) f)"
+ (is "?lhs=?rhs")
+proof
+ show "?lhs \<Longrightarrow> ?rhs"
+ by (simp add: open_map_imp_subset_topspace open_map_restriction)
+ show "?rhs \<Longrightarrow> ?lhs"
+ by (simp add: assms open_map_into_k_space)
+qed
+
+lemma closed_map_into_k_space_eq:
+ assumes "k_space Y"
+ shows "closed_map X Y f \<longleftrightarrow>
+ f ` (topspace X) \<subseteq> topspace Y \<and>
+ (\<forall>k. compactin Y k
+ \<longrightarrow> closed_map (subtopology X {x \<in> topspace X. f x \<in> k}) (subtopology Y k) f)"
+ (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+ show "?lhs \<Longrightarrow> ?rhs"
+ by (simp add: closed_map_imp_subset_topspace closed_map_restriction)
+ show "?rhs \<Longrightarrow> ?lhs"
+ by (simp add: assms closed_map_into_k_space)
+qed
+
+lemma proper_map_into_k_space:
+ assumes "k_space Y" and fim: "f ` (topspace X) \<subseteq> topspace Y"
+ and f: "\<And>K. compactin Y K
+ \<Longrightarrow> proper_map (subtopology X {x \<in> topspace X. f x \<in> K})
+ (subtopology Y K) f"
+ shows "proper_map X Y f"
+proof -
+ have "closed_map X Y f"
+ by (meson assms closed_map_into_k_space fim proper_map_def)
+ with f topspace_subtopology_subset show ?thesis
+ apply (simp add: proper_map_alt)
+ by (smt (verit, best) Collect_cong compactin_absolute)
+qed
+
+lemma proper_map_into_k_space_eq:
+ assumes "k_space Y"
+ shows "proper_map X Y f \<longleftrightarrow>
+ f ` (topspace X) \<subseteq> topspace Y \<and>
+ (\<forall>K. compactin Y K
+ \<longrightarrow> proper_map (subtopology X {x \<in> topspace X. f x \<in> K}) (subtopology Y K) f)"
+ (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+ show "?lhs \<Longrightarrow> ?rhs"
+ by (simp add: proper_map_imp_subset_topspace proper_map_restriction)
+ show "?rhs \<Longrightarrow> ?lhs"
+ by (simp add: assms proper_map_into_k_space)
+qed
+
+lemma compact_imp_proper_map:
+ assumes "k_space Y" "kc_space Y" and fim: "f ` (topspace X) \<subseteq> topspace Y"
+ and f: "continuous_map X Y f \<or> kc_space X"
+ and comp: "\<And>K. compactin Y K \<Longrightarrow> compactin X {x \<in> topspace X. f x \<in> K}"
+ shows "proper_map X Y f"
+proof (rule compact_imp_proper_map_gen)
+ fix S
+ assume "S \<subseteq> topspace Y"
+ and "\<And>K. compactin Y K \<Longrightarrow> compactin Y (S \<inter> K)"
+ with assms show "closedin Y S"
+ by (simp add: closedin_subset_topspace inf_commute k_space kc_space_def)
+qed (use assms in auto)
+
+lemma proper_eq_compact_map:
+ assumes "k_space Y" "kc_space Y"
+ and f: "continuous_map X Y f \<or> kc_space X"
+ shows "proper_map X Y f \<longleftrightarrow>
+ f ` (topspace X) \<subseteq> topspace Y \<and>
+ (\<forall>K. compactin Y K \<longrightarrow> compactin X {x \<in> topspace X. f x \<in> K})"
+ (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+ show "?lhs \<Longrightarrow> ?rhs"
+ by (simp add: proper_map_alt proper_map_imp_subset_topspace)
+qed (use assms compact_imp_proper_map in auto)
+
+lemma compact_imp_perfect_map:
+ assumes "k_space Y" "kc_space Y" and "f ` (topspace X) = topspace Y"
+ and "continuous_map X Y f"
+ and "\<And>K. compactin Y K \<Longrightarrow> compactin X {x \<in> topspace X. f x \<in> K}"
+ shows "perfect_map X Y f"
+ by (simp add: assms compact_imp_proper_map perfect_map_def)
+
end
--- a/src/HOL/Analysis/Abstract_Topology.thy Mon May 22 12:01:05 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy Tue May 23 12:31:23 2023 +0100
@@ -269,6 +269,10 @@
unfolding subtopology_def topology_inverse'[OF istopology_subtopology]
by auto
+lemma subset_openin_subtopology:
+ "\<lbrakk>openin X S; S \<subseteq> T\<rbrakk> \<Longrightarrow> openin (subtopology X T) S"
+ by (metis inf.orderE openin_subtopology)
+
lemma openin_subtopology_Int:
"openin X S \<Longrightarrow> openin (subtopology X T) (S \<inter> T)"
using openin_subtopology by auto
@@ -296,6 +300,10 @@
unfolding closedin_def topspace_subtopology
by (auto simp: openin_subtopology)
+lemma closedin_subtopology_Int_closed:
+ "closedin X T \<Longrightarrow> closedin (subtopology X S) (S \<inter> T)"
+ using closedin_subtopology inf_commute by blast
+
lemma closedin_subset_topspace:
"\<lbrakk>closedin X S; S \<subseteq> T\<rbrakk> \<Longrightarrow> closedin (subtopology X T) S"
using closedin_subtopology by fastforce
@@ -4808,6 +4816,18 @@
"proper_map X Y f \<Longrightarrow> f ` (topspace X) \<subseteq> topspace Y"
by (simp add: closed_map_imp_subset_topspace proper_map_def)
+lemma proper_map_restriction:
+ assumes "proper_map X Y f" "{x \<in> topspace X. f x \<in> V} = U"
+ shows "proper_map (subtopology X U) (subtopology Y V) f"
+proof -
+ have [simp]: "{x \<in> topspace X. f x \<in> V \<and> f x = y} = {x \<in> topspace X. f x = y}"
+ if "y \<in> V" for y
+ using that by auto
+ show ?thesis
+ using assms unfolding proper_map_def using closed_map_restriction
+ by (force simp: compactin_subtopology)
+qed
+
lemma closed_injective_imp_proper_map:
assumes f: "closed_map X Y f" and inj: "inj_on f (topspace X)"
shows "proper_map X Y f"
@@ -4976,6 +4996,45 @@
"S \<subseteq> topspace X \<Longrightarrow> proper_map (subtopology X S) X id \<longleftrightarrow> closedin X S \<and> (\<forall>k. compactin X k \<longrightarrow> compactin X (S \<inter> k))"
by (metis closed_Int_compactin closed_map_inclusion_eq inf.absorb_iff2 inj_on_id injective_imp_proper_eq_closed_map)
+lemma proper_map_into_subtopology:
+ "\<lbrakk>proper_map X Y f; f ` topspace X \<subseteq> C\<rbrakk> \<Longrightarrow> proper_map X (subtopology Y C) f"
+ by (simp add: closed_map_into_subtopology compactin_subtopology proper_map_alt)
+
+lemma proper_map_from_composition_left:
+ assumes gf: "proper_map X Z (g \<circ> f)" and contf: "continuous_map X Y f" and fim: "f ` topspace X = topspace Y"
+ shows "proper_map Y Z g"
+ unfolding proper_map_def
+proof (intro strip conjI)
+ show "closed_map Y Z g"
+ by (meson closed_map_from_composition_left gf contf fim proper_imp_closed_map)
+ fix z assume "z \<in> topspace Z"
+ have eq: "{y \<in> topspace Y. g y = z} = f ` {x \<in> topspace X. (g \<circ> f) x = z}"
+ using fim by force
+ show "compactin Y {x \<in> topspace Y. g x = z}"
+ unfolding eq
+ proof (rule image_compactin [OF _ contf])
+ show "compactin X {x \<in> topspace X. (g \<circ> f) x = z}"
+ using \<open>z \<in> topspace Z\<close> gf proper_map_def by fastforce
+ qed
+qed
+
+lemma proper_map_from_composition_right_inj:
+ assumes gf: "proper_map X Z (g \<circ> f)" and fim: "f ` topspace X \<subseteq> topspace Y"
+ and contf: "continuous_map Y Z g" and inj: "inj_on g (topspace Y)"
+ shows "proper_map X Y f"
+ unfolding proper_map_def
+proof (intro strip conjI)
+ show "closed_map X Y f"
+ by (meson closed_map_from_composition_right assms proper_imp_closed_map)
+ fix y
+ assume "y \<in> topspace Y"
+ with fim inj have eq: "{x \<in> topspace X. f x = y} = {x \<in> topspace X. (g \<circ> f) x = g y}"
+ by (auto simp: image_subset_iff inj_onD)
+ show "compactin X {x \<in> topspace X. f x = y}"
+ unfolding eq
+ by (smt (verit) Collect_cong \<open>y \<in> topspace Y\<close> contf continuous_map_closedin gf proper_map_def)
+qed
+
subsection\<open>Perfect maps (proper, continuous and surjective)\<close>
@@ -5021,4 +5080,11 @@
"perfect_map X Y f \<Longrightarrow> f ` (topspace X) = topspace Y"
by (simp add: perfect_map_def)
+lemma perfect_map_from_composition_left:
+ assumes "perfect_map X Z (g \<circ> f)" and "continuous_map X Y f"
+ and "continuous_map Y Z g" and "f ` topspace X = topspace Y"
+ shows "perfect_map Y Z g"
+ using assms unfolding perfect_map_def
+ by (metis image_comp proper_map_from_composition_left)
+
end
--- a/src/HOL/Analysis/Analysis.thy Mon May 22 12:01:05 2023 +0200
+++ b/src/HOL/Analysis/Analysis.thy Tue May 23 12:31:23 2023 +0100
@@ -7,6 +7,7 @@
FSigma
Sum_Topology
Abstract_Topological_Spaces
+ Abstract_Metric_Spaces
Connected
Abstract_Limits
Isolated
--- a/src/HOL/Analysis/Measure_Space.thy Mon May 22 12:01:05 2023 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy Tue May 23 12:31:23 2023 +0100
@@ -2288,12 +2288,8 @@
subsection\<^marker>\<open>tag unimportant\<close> \<open>Counting space\<close>
lemma strict_monoI_Suc:
- assumes ord [simp]: "(\<And>n. f n < f (Suc n))" shows "strict_mono f"
- unfolding strict_mono_def
-proof safe
- fix n m :: nat assume "n < m" then show "f n < f m"
- by (induct m) (auto simp: less_Suc_eq intro: less_trans ord)
-qed
+ assumes "(\<And>n. f n < f (Suc n))" shows "strict_mono f"
+ by (simp add: assms strict_mono_Suc_iff)
lemma emeasure_count_space:
assumes "X \<subseteq> A" shows "emeasure (count_space A) X = (if finite X then of_nat (card X) else \<infinity>)"
--- a/src/HOL/Analysis/Product_Topology.thy Mon May 22 12:01:05 2023 +0200
+++ b/src/HOL/Analysis/Product_Topology.thy Tue May 23 12:31:23 2023 +0100
@@ -139,6 +139,47 @@
qed
qed
+text \<open>Missing the opposite direction. Does it hold? A converse is proved for proper maps, a stronger condition\<close>
+lemma closed_map_prod:
+ assumes "closed_map (prod_topology X Y) (prod_topology X' Y') (\<lambda>(x,y). (f x, g y))"
+ shows "topspace(prod_topology X Y) = {} \<or> closed_map X X' f \<and> closed_map Y Y' g"
+proof (cases "topspace(prod_topology X Y) = {}")
+ case False
+ then have ne: "topspace X \<noteq> {}" "topspace Y \<noteq> {}"
+ by auto
+ have "closed_map X X' f"
+ unfolding closed_map_def
+ proof (intro strip)
+ fix C
+ assume "closedin X C"
+ show "closedin X' (f ` C)"
+ proof (cases "C={}")
+ case False
+ with assms have "closedin (prod_topology X' Y') ((\<lambda>(x,y). (f x, g y)) ` (C \<times> topspace Y))"
+ by (simp add: \<open>closedin X C\<close> closed_map_def closedin_prod_Times_iff)
+ with False ne show ?thesis
+ by (simp add: image_paired_Times closedin_Times closedin_prod_Times_iff)
+ qed auto
+ qed
+ moreover
+ have "closed_map Y Y' g"
+ unfolding closed_map_def
+ proof (intro strip)
+ fix C
+ assume "closedin Y C"
+ show "closedin Y' (g ` C)"
+ proof (cases "C={}")
+ case False
+ with assms have "closedin (prod_topology X' Y') ((\<lambda>(x,y). (f x, g y)) ` (topspace X \<times> C))"
+ by (simp add: \<open>closedin Y C\<close> closed_map_def closedin_prod_Times_iff)
+ with False ne show ?thesis
+ by (simp add: image_paired_Times closedin_Times closedin_prod_Times_iff)
+ qed auto
+ qed
+ ultimately show ?thesis
+ by (auto simp: False)
+qed auto
+
subsection \<open>Continuity\<close>
lemma continuous_map_pairwise:
--- a/src/HOL/Analysis/T1_Spaces.thy Mon May 22 12:01:05 2023 +0200
+++ b/src/HOL/Analysis/T1_Spaces.thy Tue May 23 12:31:23 2023 +0100
@@ -49,6 +49,12 @@
apply (simp add: closedin_contains_derived_set t1_space_derived_set_of_singleton)
using t1_space_alt by auto
+lemma continuous_closed_imp_proper_map:
+ "\<lbrakk>compact_space X; t1_space Y; continuous_map X Y f; closed_map X Y f\<rbrakk> \<Longrightarrow> proper_map X Y f"
+ unfolding proper_map_def
+ by (smt (verit) closedin_compact_space closedin_continuous_map_preimage
+ Collect_cong singleton_iff t1_space_closedin_singleton)
+
lemma t1_space_euclidean: "t1_space (euclidean :: 'a::metric_space topology)"
by (simp add: t1_space_closedin_singleton)
--- a/src/HOL/Nat.thy Mon May 22 12:01:05 2023 +0200
+++ b/src/HOL/Nat.thy Tue May 23 12:31:23 2023 +0100
@@ -2029,6 +2029,17 @@
lemma antimono_iff_le_Suc: "antimono f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)"
unfolding antimono_def by (auto intro: lift_Suc_antimono_le [of f])
+lemma strict_mono_Suc_iff: "strict_mono f \<longleftrightarrow> (\<forall>n. f n < f (Suc n))"
+proof (intro iffI strict_monoI)
+ assume *: "\<forall>n. f n < f (Suc n)"
+ fix m n :: nat assume "m < n"
+ thus "f m < f n"
+ by (induction rule: less_Suc_induct) (use * in auto)
+qed (auto simp: strict_mono_def)
+
+lemma strict_mono_add: "strict_mono (\<lambda>n::'a::linordered_semidom. n + k)"
+ by (auto simp: strict_mono_def)
+
lemma mono_nat_linear_lb:
fixes f :: "nat \<Rightarrow> nat"
assumes "\<And>m n. m < n \<Longrightarrow> f m < f n"
--- a/src/HOL/Topological_Spaces.thy Mon May 22 12:01:05 2023 +0200
+++ b/src/HOL/Topological_Spaces.thy Tue May 23 12:31:23 2023 +0100
@@ -1319,17 +1319,6 @@
subsubsection \<open>Subsequence (alternative definition, (e.g. Hoskins)\<close>
-lemma strict_mono_Suc_iff: "strict_mono f \<longleftrightarrow> (\<forall>n. f n < f (Suc n))"
-proof (intro iffI strict_monoI)
- assume *: "\<forall>n. f n < f (Suc n)"
- fix m n :: nat assume "m < n"
- thus "f m < f n"
- by (induction rule: less_Suc_induct) (use * in auto)
-qed (auto simp: strict_mono_def)
-
-lemma strict_mono_add: "strict_mono (\<lambda>n::'a::linordered_semidom. n + k)"
- by (auto simp: strict_mono_def)
-
text \<open>For any sequence, there is a monotonic subsequence.\<close>
lemma seq_monosub:
fixes s :: "nat \<Rightarrow> 'a::linorder"