# HG changeset patch
# User paulson
# Date 1687786706 -3600
# Node ID b0ad3aba48f1fed35635054ccf96935998e1d4b4
# Parent  d6e6618db92965b7875c05251103e2a83425e871# Parent  264f2b69d09ce1637d6c188e79013ecd745b84f3
merged

diff -r d6e6618db929 -r b0ad3aba48f1 src/HOL/Analysis/Abstract_Metric_Spaces.thy
--- a/src/HOL/Analysis/Abstract_Metric_Spaces.thy	Mon Jun 26 13:22:50 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Metric_Spaces.thy	Mon Jun 26 14:38:26 2023 +0100
@@ -144,21 +144,6 @@
     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.
@@ -419,7 +404,26 @@
   qed auto
 qed
 
-end
+
+end (*Metric_space*)
+
+lemma mcball_eq_cball [simp]: "Met_TC.mcball = cball"
+  by force
+
+lemma mball_eq_ball [simp]: "Met_TC.mball = ball"
+  by force
+
+lemma mopen_eq_open [simp]: "Met_TC.mopen = open"
+  by (force simp: open_contains_ball Met_TC.mopen_def)
+
+lemma limitin_iff_tendsto [iff]: "limitin Met_TC.mtopology \<sigma> x F = tendsto \<sigma> x F"
+  by (simp add: Met_TC.mtopology_def)
+
+lemma mtopology_is_euclidean [simp]: "Met_TC.mtopology = euclidean"
+  by (simp add: Met_TC.mtopology_def)
+
+lemma mbounded_iff_bounded [iff]: "Met_TC.mbounded A \<longleftrightarrow> bounded A"
+  by (metis Met_TC.mbounded UNIV_I all_not_in_conv bounded_def)
 
 
 subsection\<open>Subspace of a metric space\<close>
@@ -472,7 +476,6 @@
 
 subsection \<open>Abstract type of metric spaces\<close>
 
-
 typedef 'a metric = "{(M::'a set,d). Metric_space M d}"
   morphisms "dest_metric" "metric"
 proof -
@@ -486,7 +489,7 @@
 
 definition mdist where "mdist m \<equiv> snd (dest_metric m)"
 
-lemma Metric_space_mspace_mdist: "Metric_space (mspace m) (mdist m)"
+lemma Metric_space_mspace_mdist [iff]: "Metric_space (mspace m) (mdist m)"
   by (metis Product_Type.Collect_case_prodD dest_metric mdist_def mspace_def)
 
 lemma mdist_nonneg [simp]: "\<And>x y. 0 \<le> mdist m x y"
@@ -524,12 +527,18 @@
 
 definition "mball_of \<equiv> \<lambda>m. Metric_space.mball (mspace m) (mdist m)"
 
+lemma in_mball_of [simp]: "y \<in> mball_of m x r \<longleftrightarrow> x \<in> mspace m \<and> y \<in> mspace m \<and> mdist m x y < r"
+  by (simp add: Metric_space.in_mball mball_of_def)
+
 lemma (in Metric_space) mball_of [simp]:
   "mball_of (metric (M,d)) = mball"
   by (simp add: mball_of_def)
 
 definition "mcball_of \<equiv> \<lambda>m. Metric_space.mcball (mspace m) (mdist m)"
 
+lemma in_mcball_of [simp]: "y \<in> mcball_of m x r \<longleftrightarrow> x \<in> mspace m \<and> y \<in> mspace m \<and> mdist m x y \<le> r"
+  by (simp add: Metric_space.in_mcball mcball_of_def)
+
 lemma (in Metric_space) mcball_of [simp]:
   "mcball_of (metric (M,d)) = mcball"
   by (simp add: mcball_of_def)
@@ -545,6 +554,15 @@
 lemma mtopology_of_euclidean [simp]: "mtopology_of euclidean_metric = euclidean"
   by (simp add: Met_TC.mtopology_def mtopology_of_def)
 
+text \<open>Allows reference to the current metric space within the locale as a value\<close>
+definition (in Metric_space) "Self \<equiv> metric (M,d)"
+
+lemma (in Metric_space) mspace_Self [simp]: "mspace Self = M"
+  by (simp add: Self_def)
+
+lemma (in Metric_space) mdist_Self [simp]: "mdist Self = d"
+  by (simp add: Self_def)
+
 text\<open> Subspace of a metric space\<close>
 
 definition submetric where
@@ -822,12 +840,6 @@
    "\<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)
 
-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
@@ -1551,6 +1563,23 @@
 
 end
 
+definition mcomplete_of :: "'a metric \<Rightarrow> bool"
+  where "mcomplete_of \<equiv> \<lambda>m. Metric_space.mcomplete (mspace m) (mdist m)"
+
+lemma (in Metric_space) mcomplete_of [simp]: "mcomplete_of (metric (M,d)) = mcomplete"
+  by (simp add: mcomplete_of_def)
+
+lemma mcomplete_trivial: "Metric_space.mcomplete {} (\<lambda>x y. 0)"
+  using Metric_space.intro Metric_space.mcomplete_empty_mspace by force
+
+lemma mcomplete_trivial_singleton: "Metric_space.mcomplete {\<lambda>x. a} (\<lambda>x y. 0)"
+proof -
+  interpret Metric_space "{\<lambda>x. a}" "\<lambda>x y. 0"
+    by unfold_locales auto
+  show ?thesis
+    unfolding mcomplete_def MCauchy_def image_subset_iff by (metis UNIV_I limit_metric_sequentially)
+qed
+
 lemma MCauchy_iff_Cauchy [iff]: "Met_TC.MCauchy = Cauchy"
   by (force simp: Cauchy_def Met_TC.MCauchy_def)
 
@@ -1558,9 +1587,6 @@
   "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 
 
@@ -1593,7 +1619,6 @@
 
 end
 
-
 context Metric_space
 begin
 
@@ -2745,9 +2770,9 @@
   unfolding completely_metrizable_space_def
   by (metis discrete_metric.mcomplete_discrete_metric discrete_metric.mtopology_discrete_metric metric_M_dd)
 
-lemma completely_metrizable_space_euclideanreal:
-    "completely_metrizable_space euclideanreal"
-  by (metis Met_TC.mtopology_is_euclideanreal Met_TC.completely_metrizable_space_mtopology euclidean_metric)
+lemma completely_metrizable_space_euclidean:
+    "completely_metrizable_space (euclidean:: 'a::complete_space topology)"
+  using Met_TC.completely_metrizable_space_mtopology complete_UNIV by auto
 
 lemma completely_metrizable_space_closedin:
   assumes X: "completely_metrizable_space X" and S: "closedin X S"
@@ -2772,6 +2797,9 @@
   qed
 qed
 
+lemma completely_metrizable_space_cbox: "completely_metrizable_space (top_of_set (cbox a b))"
+    using closed_closedin completely_metrizable_space_closedin completely_metrizable_space_euclidean by blast
+
 lemma homeomorphic_completely_metrizable_space_aux:
   assumes homXY: "X homeomorphic_space Y" and X: "completely_metrizable_space X"
   shows "completely_metrizable_space Y"
@@ -3364,6 +3392,14 @@
   finally show ?thesis by (simp add: True)
 qed (simp add: atin_within_def)
 
+lemma eventually_within_imp:
+   "eventually P (atin_within X a S) \<longleftrightarrow> eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) (atin X a)"
+  by (auto simp add: eventually_atin_within eventually_atin)
+
+lemma limit_within_subset:
+   "\<lbrakk>limitin X f l (atin_within Y a S); T \<subseteq> S\<rbrakk> \<Longrightarrow> limitin X f l (atin_within Y a T)"
+  by (smt (verit) eventually_atin_within limitin_def subset_eq)
+
 lemma atin_subtopology_within:
   assumes "a \<in> S"
   shows "atin (subtopology X S) a = atin_within X a S"
@@ -4504,7 +4540,7 @@
     using assms continuous_map_compose continuous_map_metric by blast
 qed
 
-lemma continuous_map_mdist:
+lemma continuous_map_mdist [continuous_intros]:
   assumes f: "continuous_map X (mtopology_of m) f" 
       and g: "continuous_map X (mtopology_of m) g"
   shows "continuous_map X euclidean (\<lambda>x. mdist m (f x) (g x))"
@@ -4560,6 +4596,542 @@
   assumes fim: "f ` M1 = M2" and d: "\<And>x y. \<lbrakk>x \<in> M1; y \<in> M1\<rbrakk> \<Longrightarrow> d2 (f x) (f y) = d1 x y"
   shows "homeomorphic_map M1.mtopology M2.mtopology f"
   by (metis M1.topspace_mtopology M2.subtopology_mspace d embedding_map_def fim isometry_imp_embedding_map subsetI)
+subsection\<open>"Capped" equivalent bounded metrics and general product metrics\<close>
+
+definition (in Metric_space) capped_dist where
+  "capped_dist \<equiv> \<lambda>\<delta> x y. if \<delta> > 0 then min \<delta> (d x y) else d x y"
+
+lemma (in Metric_space) capped_dist: "Metric_space M (capped_dist \<delta>)"
+proof
+  fix x y
+  assume "x \<in> M" "y \<in> M"
+  then show "(capped_dist \<delta> x y = 0) = (x = y)"
+    by (smt (verit, best) capped_dist_def zero)
+  fix z 
+  assume "z \<in> M"
+  show "capped_dist \<delta> x z \<le> capped_dist \<delta> x y + capped_dist \<delta> y z"
+    unfolding capped_dist_def using \<open>x \<in> M\<close> \<open>y \<in> M\<close> \<open>z \<in> M\<close> 
+    by (smt (verit, del_insts) Metric_space.mdist_pos_eq Metric_space_axioms mdist_reverse_triangle)
+qed (use capped_dist_def commute in auto)
+
+
+definition capped_metric where
+  "capped_metric \<delta> m \<equiv> metric(mspace m, Metric_space.capped_dist (mdist m) \<delta>)"
+
+lemma capped_metric:
+  "capped_metric \<delta> m = (if \<delta> \<le> 0 then m else metric(mspace m, \<lambda>x y. min \<delta> (mdist m x y)))"
+proof -
+  interpret Metric_space "mspace m" "mdist m"
+    by (simp add: Metric_space_mspace_mdist)
+  show ?thesis
+    by (auto simp: capped_metric_def capped_dist_def)
+qed
+
+lemma capped_metric_mspace [simp]:
+  "mspace (capped_metric \<delta> m) = mspace m"
+  apply (simp add: capped_metric not_le)
+  by (smt (verit, ccfv_threshold) Metric_space.mspace_metric Metric_space_def Metric_space_mspace_mdist)
+
+lemma capped_metric_mdist:
+  "mdist (capped_metric \<delta> m) = (\<lambda>x y. if \<delta> \<le> 0 then mdist m x y else min \<delta> (mdist m x y))"
+  apply (simp add: capped_metric not_le)
+  by (smt (verit, del_insts) Metric_space.mdist_metric Metric_space_def Metric_space_mspace_mdist)
+
+lemma mdist_capped_le: "mdist (capped_metric \<delta> m) x y \<le> mdist m x y"
+  by (simp add: capped_metric_mdist)
+
+lemma mdist_capped: "\<delta> > 0 \<Longrightarrow> mdist (capped_metric \<delta> m) x y \<le> \<delta>"
+  by (simp add: capped_metric_mdist)
+
+lemma mball_of_capped_metric [simp]: 
+  assumes "x \<in> mspace m" "r > \<delta>" "\<delta> > 0" 
+  shows "mball_of (capped_metric \<delta> m) x r = mspace m"
+proof -
+  interpret Metric_space "mspace m" "mdist m"
+    by (simp add: Metric_space_mspace_mdist)
+  have "Metric_space.mball (mspace m) (mdist (capped_metric \<delta> m)) x r \<subseteq> mspace m"
+    by (metis Metric_space.mball_subset_mspace Metric_space_mspace_mdist capped_metric_mspace)
+  moreover have "mspace m \<subseteq> Metric_space.mball (mspace m) (mdist (capped_metric \<delta> m)) x r"
+    by (smt (verit) Metric_space.in_mball Metric_space_mspace_mdist assms capped_metric_mspace mdist_capped subset_eq)
+  ultimately show ?thesis
+    by (simp add: mball_of_def)
+qed
+
+lemma Metric_space_capped_dist[simp]:
+  "Metric_space (mspace m) (Metric_space.capped_dist (mdist m) \<delta>)"
+  using Metric_space.capped_dist Metric_space_mspace_mdist by blast
+
+lemma mtopology_capped_metric:
+  "mtopology_of(capped_metric \<delta> m) = mtopology_of m"
+proof (cases "\<delta> > 0")
+  case True
+  interpret Metric_space "mspace m" "mdist m"
+    by (simp add: Metric_space_mspace_mdist)
+  interpret Cap: Metric_space "mspace m" "mdist (capped_metric \<delta> m)"
+    by (metis Metric_space_mspace_mdist capped_metric_mspace)
+  show ?thesis
+    unfolding topology_eq
+  proof
+    fix S
+    show "openin (mtopology_of (capped_metric \<delta> m)) S = openin (mtopology_of m) S"
+    proof (cases "S \<subseteq> mspace m")
+      case True
+      have "mball x r \<subseteq> Cap.mball x r" for x r
+        by (smt (verit, ccfv_SIG) Cap.in_mball in_mball mdist_capped_le subsetI)
+      moreover have "\<exists>r>0. Cap.mball x r \<subseteq> S" if "r>0" "x \<in> S" and r: "mball x r \<subseteq> S" for r x
+      proof (intro exI conjI)
+        show "min (\<delta>/2) r > 0"
+          using \<open>r>0\<close> \<open>\<delta>>0\<close> by force
+        show "Cap.mball x (min (\<delta>/2) r) \<subseteq> S"
+          using that
+          by clarsimp (smt (verit) capped_metric_mdist field_sum_of_halves in_mball subsetD)
+      qed
+      ultimately have "(\<exists>r>0. Cap.mball x r \<subseteq> S) = (\<exists>r>0. mball x r \<subseteq> S)" if "x \<in> S" for x
+        by (meson subset_trans that)
+      then show ?thesis
+        by (simp add: mtopology_of_def openin_mtopology Cap.openin_mtopology)
+    qed (simp add: openin_closedin_eq)
+  qed
+qed (simp add: capped_metric)
+
+text \<open>Might have been easier to prove this within the locale to start with (using Self)\<close>
+lemma (in Metric_space) mtopology_capped_metric:
+  "Metric_space.mtopology M (capped_dist \<delta>) = mtopology"
+  using mtopology_capped_metric [of \<delta> "metric(M,d)"]
+  by (simp add: Metric_space.mtopology_of capped_dist capped_metric_def)
+
+lemma (in Metric_space) MCauchy_capped_metric:
+  "Metric_space.MCauchy M (capped_dist \<delta>) \<sigma> \<longleftrightarrow> MCauchy \<sigma>"
+proof (cases "\<delta> > 0")
+  case True
+  interpret Cap: Metric_space "M" "capped_dist \<delta>"
+    by (simp add: capped_dist)
+  show ?thesis
+  proof
+    assume \<sigma>: "Cap.MCauchy \<sigma>"
+    show "MCauchy \<sigma>"
+      unfolding MCauchy_def
+    proof (intro conjI strip)
+      show "range \<sigma> \<subseteq> M"
+        using Cap.MCauchy_def \<sigma> by presburger
+      fix \<epsilon> :: real
+      assume "\<epsilon> > 0"
+      with True \<sigma>
+      obtain N where "\<forall>n n'. N \<le> n \<longrightarrow> N \<le> n' \<longrightarrow> capped_dist \<delta> (\<sigma> n) (\<sigma> n') < min \<delta> \<epsilon>"
+        unfolding Cap.MCauchy_def by (metis min_less_iff_conj)
+      with True show "\<exists>N. \<forall>n n'. N \<le> n \<longrightarrow> N \<le> n' \<longrightarrow> d (\<sigma> n) (\<sigma> n') < \<epsilon>"
+        by (force simp: capped_dist_def)
+    qed
+  next
+    assume "MCauchy \<sigma>"
+    then show "Cap.MCauchy \<sigma>"
+      unfolding MCauchy_def Cap.MCauchy_def by (force simp: capped_dist_def)
+  qed
+qed (simp add: capped_dist_def)
+
+
+lemma (in Metric_space) mcomplete_capped_metric:
+   "Metric_space.mcomplete M (capped_dist \<delta>) \<longleftrightarrow> mcomplete"
+  by (simp add: MCauchy_capped_metric Metric_space.mcomplete_def capped_dist mtopology_capped_metric mcomplete_def)
+
+lemma bounded_equivalent_metric:
+  assumes "\<delta> > 0"
+  obtains m' where "mspace m' = mspace m" "mtopology_of m' = mtopology_of m" "\<And>x y. mdist m' x y < \<delta>"
+proof
+  let ?m = "capped_metric (\<delta>/2) m"
+  fix x y
+  show "mdist ?m x y < \<delta>"
+    by (smt (verit, best) assms field_sum_of_halves mdist_capped)    
+qed (auto simp: mtopology_capped_metric)
+
+text \<open>A technical lemma needed below\<close>
+lemma Sup_metric_cartesian_product:
+  fixes I m
+  defines "S \<equiv> PiE I (mspace \<circ> m)"
+  defines "D \<equiv> \<lambda>x y. if x \<in> S \<and> y \<in> S then SUP i\<in>I. mdist (m i) (x i) (y i) else 0"
+  defines "m' \<equiv> metric(S,D)"
+  assumes "I \<noteq> {}"
+    and c: "\<And>i x y. \<lbrakk>i \<in> I; x \<in> mspace(m i); y \<in> mspace(m i)\<rbrakk> \<Longrightarrow> mdist (m i) x y \<le> c"
+  shows "Metric_space S D" 
+    and "\<forall>x \<in> S. \<forall>y \<in> S. \<forall>b. D x y \<le> b \<longleftrightarrow> (\<forall>i \<in> I. mdist (m i) (x i) (y i) \<le> b)"  (is "?the2")
+proof -
+  have bdd: "bdd_above ((\<lambda>i. mdist (m i) (x i) (y i)) ` I)"
+    if "x \<in> S" "y \<in> S" for x y 
+    using c that by (force simp: S_def bdd_above_def)
+  have D_iff: "D x y \<le> b \<longleftrightarrow> (\<forall>i \<in> I. mdist (m i) (x i) (y i) \<le> b)"
+    if "x \<in> S" "y \<in> S" for x y b
+    using that \<open>I \<noteq> {}\<close> by (simp add: D_def PiE_iff cSup_le_iff bdd)
+  show "Metric_space S D"
+  proof
+    fix x y
+    show D0: "0 \<le> D x y"
+      using bdd  
+      apply (simp add: D_def)
+      by (meson \<open>I \<noteq> {}\<close> cSUP_upper dual_order.trans ex_in_conv mdist_nonneg)
+    show "D x y = D y x"
+      by (simp add: D_def mdist_commute)
+    assume "x \<in> S" and "y \<in> S"
+    then
+    have "D x y = 0 \<longleftrightarrow> (\<forall>i\<in>I. mdist (m i) (x i) (y i) = 0)"
+      using D0 D_iff [of x y 0] nle_le by fastforce
+    also have "... \<longleftrightarrow> x = y"
+      using \<open>x \<in> S\<close> \<open>y \<in> S\<close> by (fastforce simp: S_def PiE_iff extensional_def)
+    finally show "(D x y = 0) \<longleftrightarrow> (x = y)" .
+    fix z
+    assume "z \<in> S"
+    have "mdist (m i) (x i) (z i) \<le> D x y + D y z" if "i \<in> I" for i
+    proof -
+      have "mdist (m i) (x i) (z i) \<le> mdist (m i) (x i) (y i) + mdist (m i) (y i) (z i)"
+        by (metis PiE_E S_def \<open>x \<in> S\<close> \<open>y \<in> S\<close> \<open>z \<in> S\<close> comp_apply mdist_triangle that)
+      also have "... \<le> D x y + D y z"
+        using \<open>x \<in> S\<close> \<open>y \<in> S\<close> \<open>z \<in> S\<close> by (meson D_iff add_mono order_refl that)
+      finally show ?thesis .
+    qed
+    then show "D x z \<le> D x y + D y z"
+      by (simp add: D_iff \<open>x \<in> S\<close> \<open>z \<in> S\<close>)
+  qed
+  then interpret Metric_space S D .
+  show ?the2
+  proof (intro strip)
+    show "(D x y \<le> b) = (\<forall>i\<in>I. mdist (m i) (x i) (y i) \<le> b)"
+      if "x \<in> S" and "y \<in> S" for x y b
+      using that by (simp add: D_iff m'_def)
+  qed
+qed
+
+lemma metrizable_topology_A:
+  assumes "metrizable_space (product_topology X I)"
+  shows "topspace (product_topology X I) = {} \<or> (\<forall>i \<in> I. metrizable_space (X i))"
+    by (meson assms metrizable_space_retraction_map_image retraction_map_product_projection)
+
+lemma metrizable_topology_C:
+  assumes "completely_metrizable_space (product_topology X I)"
+  shows "topspace (product_topology X I) = {} \<or> (\<forall>i \<in> I. completely_metrizable_space (X i))"
+    by (meson assms completely_metrizable_space_retraction_map_image retraction_map_product_projection)
+
+lemma metrizable_topology_B:
+  fixes a X I
+  defines "L \<equiv> {i \<in> I. \<nexists>a. topspace (X i) \<subseteq> {a}}"
+  assumes "topspace (product_topology X I) \<noteq> {}"
+    and met: "metrizable_space (product_topology X I)"
+    and "\<And>i. i \<in> I \<Longrightarrow> metrizable_space (X i)"
+  shows  "countable L"
+proof -
+  have "\<And>i. \<exists>p q. i \<in> L \<longrightarrow> p \<in> topspace(X i) \<and> q \<in> topspace(X i) \<and> p \<noteq> q"
+    unfolding L_def by blast
+  then obtain \<phi> \<psi> where \<phi>: "\<And>i. i \<in> L \<Longrightarrow> \<phi> i \<in> topspace(X i) \<and> \<psi> i \<in> topspace(X i) \<and> \<phi> i \<noteq> \<psi> i"
+    by metis
+  obtain z where z: "z \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+    using assms(2) by fastforce
+  define p where "p \<equiv> \<lambda>i. if i \<in> L then \<phi> i else z i"
+  define q where "q \<equiv> \<lambda>i j. if j = i then \<psi> i else p j"
+  have p: "p \<in> topspace(product_topology X I)"
+    using z \<phi> by (auto simp: p_def L_def)
+  then have q: "\<And>i. i \<in> L \<Longrightarrow> q i \<in> topspace (product_topology X I)" 
+    by (auto simp: L_def q_def \<phi>)
+  have fin: "finite {i \<in> L. q i \<notin> U}" if U: "openin (product_topology X I) U" "p \<in> U" for U
+  proof -
+    obtain V where V: "finite {i \<in> I. V i \<noteq> topspace (X i)}" "(\<forall>i\<in>I. openin (X i) (V i))" "p \<in> Pi\<^sub>E I V" "Pi\<^sub>E I V \<subseteq> U"
+      using U by (force simp: openin_product_topology_alt)
+    moreover 
+    have "V x \<noteq> topspace (X x)" if "x \<in> L" and "q x \<notin> U" for x
+      using that V q
+      by (smt (verit, del_insts) PiE_iff q_def subset_eq topspace_product_topology)
+    then have "{i \<in> L. q i \<notin> U} \<subseteq> {i \<in> I. V i \<noteq> topspace (X i)}"
+      by (force simp: L_def)
+    ultimately show ?thesis
+      by (meson finite_subset)
+  qed
+  obtain M d where "Metric_space M d" and XI: "product_topology X I = Metric_space.mtopology M d"
+    using met metrizable_space_def by blast
+  then interpret Metric_space M d
+    by blast
+  define C where "C \<equiv> \<Union>n::nat. {i \<in> L. q i \<notin> mball p (inverse (Suc n))}"
+  have "finite {i \<in> L. q i \<notin> mball p (inverse (real (Suc n)))}" for n
+    using XI p  by (intro fin; force)
+  then have "countable C"
+    unfolding C_def
+    by (meson countableI_type countable_UN countable_finite)
+  moreover have "L \<subseteq> C"
+  proof (clarsimp simp: C_def)
+    fix i
+    assume "i \<in> L" and "q i \<in> M" and "p \<in> M"
+    then show "\<exists>n. \<not> d p (q i) < inverse (1 + real n)"
+      using reals_Archimedean [of "d p (q i)"]
+      by (metis \<phi> mdist_pos_eq not_less_iff_gr_or_eq of_nat_Suc p_def q_def)
+  qed
+  ultimately show ?thesis
+    using countable_subset by blast
+qed
+
+lemma metrizable_topology_DD:
+  assumes "topspace (product_topology X I) \<noteq> {}"
+    and co: "countable {i \<in> I. \<nexists>a. topspace (X i) \<subseteq> {a}}"
+    and m: "\<And>i. i \<in> I \<Longrightarrow> X i = mtopology_of (m i)"
+  obtains M d where "Metric_space M d" "product_topology X I = Metric_space.mtopology M d"
+                    "(\<And>i. i \<in> I \<Longrightarrow> mcomplete_of (m i)) \<Longrightarrow> Metric_space.mcomplete M d"
+proof (cases "I = {}")
+  case True
+  then show ?thesis
+    by (metis discrete_metric.mcomplete_discrete_metric discrete_metric.mtopology_discrete_metric metric_M_dd product_topology_empty_discrete that)
+next
+  case False
+  obtain nk and C:: "nat set" where nk: "{i \<in> I. \<nexists>a. topspace (X i) \<subseteq> {a}} = nk ` C" and "inj_on nk C"
+    using co by (force simp: countable_as_injective_image_subset)
+  then obtain kn where kn: "\<And>w. w \<in> C \<Longrightarrow> kn (nk w) = w"
+    by (metis inv_into_f_f)
+  define cm where "cm \<equiv> \<lambda>i. capped_metric (inverse(Suc(kn i))) (m i)"
+  have mspace_cm: "mspace (cm i) = mspace (m i)" for i
+    by (simp add: cm_def)
+  have c1: "\<And>i x y. mdist (cm i) x y \<le> 1"
+    by (simp add: cm_def capped_metric_mdist min_le_iff_disj divide_simps)
+  then have bdd: "bdd_above ((\<lambda>i. mdist (cm i) (x i) (y i)) ` I)" for x y
+    by (meson bdd_above.I2)
+  define M where "M \<equiv> Pi\<^sub>E I (mspace \<circ> cm)"
+  define d where "d \<equiv> \<lambda>x y. if x \<in> M \<and> y \<in> M then SUP i\<in>I. mdist (cm i) (x i) (y i) else 0"
+
+  have d_le1: "d x y \<le> 1" for x y
+    using \<open>I \<noteq> {}\<close> c1 by (simp add: d_def bdd cSup_le_iff)
+  with \<open>I \<noteq> {}\<close> Sup_metric_cartesian_product [of I cm]
+  have "Metric_space M d" 
+    and *: "\<forall>x\<in>M. \<forall>y\<in>M. \<forall>b. (d x y \<le> b) \<longleftrightarrow> (\<forall>i\<in>I. mdist (cm i) (x i) (y i) \<le> b)"
+    by (auto simp: False bdd M_def d_def cSUP_le_iff intro: c1) 
+  then interpret Metric_space M d 
+    by metis
+  have le_d: "mdist (cm i) (x i) (y i) \<le> d x y" if "i \<in> I" "x \<in> M" "y \<in> M" for i x y
+    using "*" that by blast
+  have product_m: "PiE I (\<lambda>i. mspace (m i)) = topspace(product_topology X I)"
+    using m by force
+
+  define m' where "m' = metric (M,d)"
+  define J where "J \<equiv> \<lambda>U. {i \<in> I. U i \<noteq> topspace (X i)}"
+  have 1: "\<exists>U. finite (J U) \<and> (\<forall>i\<in>I. openin (X i) (U i)) \<and> x \<in> Pi\<^sub>E I U \<and> Pi\<^sub>E I U \<subseteq> mball z r"
+    if "x \<in> M" "z \<in> M" and r: "0 < r" "d z x < r" for x z r
+  proof -
+    have x: "\<And>i. i \<in> I \<Longrightarrow> x i \<in> topspace(X i)"
+      using M_def m mspace_cm that(1) by auto
+    have z: "\<And>i. i \<in> I \<Longrightarrow> z i \<in> topspace(X i)"
+      using M_def m mspace_cm that(2) by auto
+    obtain R where "0 < R" "d z x < R" "R < r"
+      using r dense by (smt (verit, ccfv_threshold))
+    define U where "U \<equiv> \<lambda>i. if R \<le> inverse(Suc(kn i)) then mball_of (m i) (z i) R else topspace(X i)"
+    show ?thesis
+    proof (intro exI conjI)
+      obtain n where n: "real n * R > 1"
+        using \<open>0 < R\<close> ex_less_of_nat_mult by blast
+      have "finite (nk ` (C \<inter> {..n}))"
+        by force
+      moreover 
+      have "\<exists>m. m \<in> C \<and> m \<le> n \<and> i = nk m"
+        if R: "R \<le> inverse (1 + real (kn i))" and "i \<in> I" 
+          and neq: "mball_of (m i) (z i) R \<noteq> topspace (X i)" for i 
+      proof -
+        interpret MI: Metric_space "mspace (m i)" "mdist (m i)"
+          by auto
+        have "MI.mball (z i) R \<noteq> topspace (X i)"
+          by (metis mball_of_def neq)
+        then have "\<nexists>a. topspace (X i) \<subseteq> {a}"
+          using \<open>0 < R\<close> m subset_antisym \<open>i \<in> I\<close> z by fastforce
+        then have "i \<in> nk ` C"
+          using nk \<open>i \<in> I\<close> by auto
+        then show ?thesis
+          by (smt (verit, ccfv_SIG) R \<open>0 < R\<close> image_iff kn lift_Suc_mono_less_iff mult_mono n not_le_imp_less of_nat_0_le_iff of_nat_Suc right_inverse)
+      qed
+      then have "J U \<subseteq> nk ` (C \<inter> {..n})"
+        by (auto simp: image_iff Bex_def J_def U_def split: if_split_asm)
+      ultimately show "finite (J U)"
+        using finite_subset by blast
+      show "\<forall>i\<in>I. openin (X i) (U i)"
+        by (simp add: Metric_space.openin_mball U_def mball_of_def mtopology_of_def m)
+      have xin: "x \<in> Pi\<^sub>E I (topspace \<circ> X)"
+        using M_def \<open>x \<in> M\<close> x by auto
+      moreover 
+      have "\<And>i. \<lbrakk>i \<in> I; R \<le> inverse (1 + real (kn i))\<rbrakk> \<Longrightarrow> mdist (m i) (z i) (x i) < R"
+        by (smt (verit, ccfv_SIG) \<open>d z x < R\<close> capped_metric_mdist cm_def le_d of_nat_Suc that)
+      ultimately show "x \<in> Pi\<^sub>E I U"
+        using m z by (auto simp: U_def PiE_iff)
+      show "Pi\<^sub>E I U \<subseteq> mball z r"
+      proof
+        fix y
+        assume y: "y \<in> Pi\<^sub>E I U"
+        then have "y \<in> M"
+          by (force simp: PiE_iff M_def U_def m mspace_cm split: if_split_asm)
+        moreover 
+        have "\<forall>i\<in>I. mdist (cm i) (z i) (y i) \<le> R"
+          by (smt (verit) PiE_mem U_def cm_def in_mball_of inverse_Suc mdist_capped mdist_capped_le y)
+        then have "d z y \<le> R"
+          by (simp add: \<open>y \<in> M\<close> \<open>z \<in> M\<close> *)
+        ultimately show "y \<in> mball z r"
+          using \<open>R < r\<close> \<open>z \<in> M\<close> by force
+      qed
+    qed
+  qed
+  have 2: "\<exists>r>0. mball x r \<subseteq> S"
+    if "finite (J U)" and x: "x \<in> Pi\<^sub>E I U" and S: "Pi\<^sub>E I U \<subseteq> S"
+      and U: "\<And>i. i\<in>I \<Longrightarrow> openin (X i) (U i)" 
+      and "x \<in> S" for U S x
+  proof -
+    { fix i
+      assume "i \<in> J U"
+      then have "i \<in> I"
+        by (auto simp: J_def)
+      then have "openin (mtopology_of (m i)) (U i)"
+        using U m by force
+      then have "openin (mtopology_of (cm i)) (U i)"
+        by (simp add: Abstract_Metric_Spaces.mtopology_capped_metric cm_def)
+      then have "\<exists>r>0. mball_of (cm i) (x i) r \<subseteq> U i"
+        using x
+        by (simp add: Metric_space.openin_mtopology PiE_mem \<open>i \<in> I\<close> mball_of_def mtopology_of_def) 
+    }
+    then obtain rf where rf: "\<And>j. j \<in> J U \<Longrightarrow> rf j >0 \<and> mball_of (cm j) (x j) (rf j) \<subseteq> U j"
+      by metis
+    define r where "r \<equiv> Min (insert 1 (rf ` J U))"
+    show ?thesis
+    proof (intro exI conjI)
+      show "r > 0"
+        by (simp add: \<open>finite (J U)\<close> r_def rf)
+      have r [simp]: "\<And>j. j \<in> J U \<Longrightarrow> r \<le> rf j" "r \<le> 1"
+        by (auto simp: r_def that(1))
+      have *: "mball_of (cm i) (x i) r \<subseteq> U i" if "i \<in> I" for i
+      proof (cases "i \<in> J U")
+        case True
+        with r show ?thesis
+          by (smt (verit) Metric_space.in_mball Metric_space_mspace_mdist mball_of_def rf subset_eq)
+      next
+        case False
+        then show ?thesis
+          by (simp add: J_def cm_def m subset_eq that)
+      qed
+      show "mball x r \<subseteq> S"
+        by (smt (verit) x * in_mball_of M_def Metric_space.in_mball Metric_space_axioms PiE_iff le_d o_apply subset_eq S)
+    qed
+  qed
+  have 3: "x \<in> M"
+    if \<section>: "\<And>x. x\<in>S \<Longrightarrow> \<exists>U. finite (J U) \<and> (\<forall>i\<in>I. openin (X i) (U i)) \<and> x \<in> Pi\<^sub>E I U \<and> Pi\<^sub>E I U \<subseteq> S"
+      and "x \<in> S" for S x
+    using \<section> [OF \<open>x \<in> S\<close>] m openin_subset by (fastforce simp: M_def PiE_iff cm_def)
+  show thesis
+  proof
+    show "Metric_space M d"
+      using Metric_space_axioms by blast
+    show eq: "product_topology X I = Metric_space.mtopology M d"
+      unfolding topology_eq openin_mtopology openin_product_topology_alt  
+      using J_def 1 2 3 subset_iff zero by (smt (verit, ccfv_threshold))
+    show "mcomplete" if "\<And>i. i \<in> I \<Longrightarrow> mcomplete_of (m i)" 
+      unfolding mcomplete_def
+    proof (intro strip)
+      fix \<sigma>
+      assume \<sigma>: "MCauchy \<sigma>"
+      have "\<exists>y. i \<in> I \<longrightarrow> limitin (X i) (\<lambda>n. \<sigma> n i) y sequentially" for i
+      proof (cases "i \<in> I")
+        case True
+        interpret MI: Metric_space "mspace (m i)" "mdist (m i)"
+          by auto
+        have "\<And>\<sigma>. MI.MCauchy \<sigma> \<longrightarrow> (\<exists>x. limitin MI.mtopology \<sigma> x sequentially)"
+          by (meson MI.mcomplete_def True mcomplete_of_def that)
+        moreover have "MI.MCauchy (\<lambda>n. \<sigma> n i)"
+          unfolding MI.MCauchy_def
+        proof (intro conjI strip)
+          show "range (\<lambda>n. \<sigma> n i) \<subseteq> mspace (m i)"
+            by (smt (verit, ccfv_threshold) MCauchy_def PiE_iff True \<sigma> eq image_subset_iff m topspace_mtopology topspace_mtopology_of topspace_product_topology)
+          fix \<epsilon>::real
+          define r where "r \<equiv> min \<epsilon> (inverse(Suc (kn i)))"
+          assume "\<epsilon> > 0"
+          then have "r > 0"
+            by (simp add: r_def)
+          then obtain N where N: "\<And>n n'. N \<le> n \<and> N \<le> n' \<Longrightarrow> d (\<sigma> n) (\<sigma> n') < r"
+            using \<sigma> unfolding MCauchy_def by meson
+          show "\<exists>N. \<forall>n n'. N \<le> n \<longrightarrow> N \<le> n' \<longrightarrow> mdist (m i) (\<sigma> n i) (\<sigma> n' i) < \<epsilon>"
+          proof (intro strip exI)
+            fix n n'
+            assume "N \<le> n" and "N \<le> n'"
+            then have "mdist (cm i) (\<sigma> n i) (\<sigma> n' i) < r"
+              using *
+              by (smt (verit) Metric_space.MCauchy_def Metric_space_axioms N True \<sigma> rangeI subsetD)
+            then
+            show "mdist (m i) (\<sigma> n i) (\<sigma> n' i) < \<epsilon>"
+              unfolding cm_def r_def
+              by (smt (verit, ccfv_SIG) capped_metric_mdist)
+          qed
+        qed
+        ultimately show ?thesis
+          by (simp add: m mtopology_of_def)
+      qed auto
+      then obtain y where "\<And>i. i \<in> I \<Longrightarrow> limitin (X i) (\<lambda>n. \<sigma> n i) (y i) sequentially"
+        by metis
+      with \<sigma> show "\<exists>x. limitin mtopology \<sigma> x sequentially"
+        apply (rule_tac x="\<lambda>i\<in>I. y i" in exI)
+        apply (simp add: MCauchy_def limitin_componentwise flip: eq)
+        by (metis eq eventually_at_top_linorder range_subsetD topspace_mtopology topspace_product_topology)
+    qed
+  qed
+qed
+
+
+lemma metrizable_topology_D:
+  assumes "topspace (product_topology X I) \<noteq> {}"
+    and co: "countable {i \<in> I. \<nexists>a. topspace (X i) \<subseteq> {a}}"
+    and met: "\<And>i. i \<in> I \<Longrightarrow> metrizable_space (X i)"
+  shows "metrizable_space (product_topology X I)"
+proof -
+  have "\<And>i. i \<in> I \<Longrightarrow> \<exists>m. X i = mtopology_of m"
+    by (metis Metric_space.mtopology_of met metrizable_space_def)
+  then obtain m where m: "\<And>i. i \<in> I \<Longrightarrow> X i = mtopology_of (m i)"
+    by metis 
+  then show ?thesis
+    using metrizable_topology_DD [of X I m] assms by (force simp: metrizable_space_def)
+qed
+
+lemma metrizable_topology_E:
+  assumes "topspace (product_topology X I) \<noteq> {}"
+    and "countable {i \<in> I. \<nexists>a. topspace (X i) \<subseteq> {a}}"
+    and met: "\<And>i. i \<in> I \<Longrightarrow> completely_metrizable_space (X i)"
+  shows "completely_metrizable_space (product_topology X I)"
+proof -
+  have "\<And>i. i \<in> I \<Longrightarrow> \<exists>m. mcomplete_of m \<and> X i = mtopology_of m"
+    using met Metric_space.mtopology_of Metric_space.mcomplete_of unfolding completely_metrizable_space_def
+    by metis 
+  then obtain m where "\<And>i. i \<in> I \<Longrightarrow> mcomplete_of (m i) \<and> X i = mtopology_of (m i)"
+    by metis 
+  then show ?thesis
+    using  metrizable_topology_DD [of X I m] assms unfolding metrizable_space_def
+    by (metis (full_types) completely_metrizable_space_def)
+qed
+
+
+lemma metrizable_space_product_topology:
+  "metrizable_space (product_topology X I) \<longleftrightarrow>
+        topspace (product_topology X I) = {} \<or>
+        countable {i \<in> I. \<not> (\<exists>a. topspace(X i) \<subseteq> {a})} \<and>
+        (\<forall>i \<in> I. metrizable_space (X i))"
+  by (metis (mono_tags, lifting) empty_metrizable_space metrizable_topology_A metrizable_topology_B metrizable_topology_D)
+
+lemma completely_metrizable_space_product_topology:
+  "completely_metrizable_space (product_topology X I) \<longleftrightarrow>
+        topspace (product_topology X I) = {} \<or>
+        countable {i \<in> I. \<not> (\<exists>a. topspace(X i) \<subseteq> {a})} \<and>
+        (\<forall>i \<in> I. completely_metrizable_space (X i))"
+  by (metis (mono_tags, lifting) completely_metrizable_imp_metrizable_space empty_completely_metrizable_space metrizable_topology_B metrizable_topology_C metrizable_topology_E)
+
+
+lemma completely_metrizable_Euclidean_space:
+  "completely_metrizable_space(Euclidean_space n)"
+  unfolding Euclidean_space_def
+proof (rule completely_metrizable_space_closedin)
+  show "completely_metrizable_space (powertop_real (UNIV::nat set))"
+    by (simp add: completely_metrizable_space_product_topology completely_metrizable_space_euclidean)
+  show "closedin (powertop_real UNIV) {x. \<forall>i\<ge>n. x i = 0}"
+    using closedin_Euclidean_space topspace_Euclidean_space by auto
+qed
+
+lemma metrizable_Euclidean_space:
+   "metrizable_space(Euclidean_space n)"
+  by (simp add: completely_metrizable_Euclidean_space completely_metrizable_imp_metrizable_space)
+
+lemma locally_connected_Euclidean_space:
+   "locally_connected_space(Euclidean_space n)"
+  by (simp add: locally_path_connected_Euclidean_space locally_path_connected_imp_locally_connected_space)
+
 
 end
 
diff -r d6e6618db929 -r b0ad3aba48f1 src/HOL/Analysis/Abstract_Topological_Spaces.thy
--- a/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Mon Jun 26 13:22:50 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Mon Jun 26 14:38:26 2023 +0100
@@ -3,7 +3,7 @@
 section \<open>Various Forms of Topological Spaces\<close>
 
 theory Abstract_Topological_Spaces
-  imports Lindelof_Spaces Locally Sum_Topology FSigma
+  imports Lindelof_Spaces Locally Abstract_Euclidean_Space Sum_Topology FSigma
 begin
 
 
@@ -1122,7 +1122,7 @@
 
 
 lemma open_map_Kolmogorov_quotient_gen:
-   "open_map (subtopology X S) (subtopology X (image (Kolmogorov_quotient X) S)) (Kolmogorov_quotient X)"
+   "open_map (subtopology X S) (subtopology X (Kolmogorov_quotient X ` S)) (Kolmogorov_quotient X)"
 proof (clarsimp simp: open_map_def openin_subtopology_alt image_iff)
   fix U
   assume "openin X U"
@@ -1233,11 +1233,10 @@
 
 lemma Kolmogorov_quotient_lift_exists:
   assumes "S \<subseteq> topspace X" "t0_space Y" and f: "continuous_map (subtopology X S) Y f"
-  obtains g where "continuous_map (subtopology X (image (Kolmogorov_quotient X) S)) Y g"
+  obtains g where "continuous_map (subtopology X (Kolmogorov_quotient X ` S)) Y g"
               "\<And>x. x \<in> S \<Longrightarrow> g(Kolmogorov_quotient X x) = f x"
 proof -
-  have "\<And>x y. \<lbrakk>x \<in> S; y \<in> S; Kolmogorov_quotient X x = Kolmogorov_quotient X y\<rbrakk>
-            \<Longrightarrow> f x = f y"
+  have "\<And>x y. \<lbrakk>x \<in> S; y \<in> S; Kolmogorov_quotient X x = Kolmogorov_quotient X y\<rbrakk> \<Longrightarrow> f x = f y"
     using assms
     apply (simp add: Kolmogorov_quotient_eq t0_space_def continuous_map_def Int_absorb1 openin_subtopology)
     by (smt (verit, del_insts) Int_iff mem_Collect_eq)
@@ -1253,8 +1252,7 @@
 subsection\<open>Closed diagonals and graphs\<close>
 
 lemma Hausdorff_space_closedin_diagonal:
-  "Hausdorff_space X \<longleftrightarrow>
-        closedin (prod_topology X X) ((\<lambda>x. (x,x)) ` topspace X)"
+  "Hausdorff_space X \<longleftrightarrow> closedin (prod_topology X X) ((\<lambda>x. (x,x)) ` topspace X)"
 proof -
   have \<section>: "((\<lambda>x. (x, x)) ` topspace X) \<subseteq> topspace X \<times> topspace X"
     by auto
@@ -1296,6 +1294,26 @@
   qed
 qed
 
+lemma forall_in_closure_of:
+  assumes "x \<in> X closure_of S" "\<And>x. x \<in> S \<Longrightarrow> P x"
+    and "closedin X {x \<in> topspace X. P x}"
+  shows "P x"
+  by (smt (verit, ccfv_threshold) Diff_iff assms closedin_def in_closure_of mem_Collect_eq)
+
+lemma forall_in_closure_of_eq:
+  assumes x: "x \<in> X closure_of S"
+    and Y: "Hausdorff_space Y" 
+    and f: "continuous_map X Y f" and g: "continuous_map X Y g"
+    and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
+  shows "f x = g x"
+proof -
+  have "closedin X {x \<in> topspace X. f x = g x}"
+    using Y closedin_continuous_maps_eq f g by blast
+  then show ?thesis
+    using forall_in_closure_of [OF x fg]
+    by fastforce
+qed
+    
 lemma retract_of_space_imp_closedin:
   assumes "Hausdorff_space X" and S: "S retract_of_space X"
   shows "closedin X S"
@@ -3067,6 +3085,23 @@
   qed
 qed
 
+lemma locally_compact_space_euclidean:
+  "locally_compact_space (euclidean::'a::heine_borel topology)" 
+  unfolding locally_compact_space_def
+proof (intro strip)
+  fix x::'a
+  assume "x \<in> topspace euclidean"
+  have "ball x 1 \<subseteq> cball x 1"
+    by auto
+  then show "\<exists>U K. openin euclidean U \<and> compactin euclidean K \<and> x \<in> U \<and> U \<subseteq> K"
+    by (metis Elementary_Metric_Spaces.open_ball centre_in_ball compact_cball compactin_euclidean_iff open_openin zero_less_one)
+qed
+
+lemma locally_compact_Euclidean_space:
+  "locally_compact_space(Euclidean_space n)"
+  using homeomorphic_locally_compact_space [OF homeomorphic_Euclidean_space_product_topology] 
+  using locally_compact_space_product_topology locally_compact_space_euclidean by fastforce
+
 proposition quotient_map_prod_right:
   assumes loc: "locally_compact_space Z" 
     and reg: "Hausdorff_space Z \<or> regular_space Z" 
diff -r d6e6618db929 -r b0ad3aba48f1 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Mon Jun 26 13:22:50 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Mon Jun 26 14:38:26 2023 +0100
@@ -3033,7 +3033,7 @@
 definition homeomorphic_space (infixr "homeomorphic'_space" 50)
   where "X homeomorphic_space Y \<equiv> \<exists>f g. homeomorphic_maps X Y f g"
 
-lemma homeomorphic_space_refl: "X homeomorphic_space X"
+lemma homeomorphic_space_refl [iff]: "X homeomorphic_space X"
   by (meson homeomorphic_maps_id homeomorphic_space_def)
 
 lemma homeomorphic_space_sym:
diff -r d6e6618db929 -r b0ad3aba48f1 src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Mon Jun 26 13:22:50 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Mon Jun 26 14:38:26 2023 +0100
@@ -1644,6 +1644,11 @@
   shows "(x / (1 + \<bar>x\<bar>) = y) \<longleftrightarrow> (\<bar>y\<bar> < 1 \<and> y / (1 - \<bar>y\<bar>) = x)"
   using real_grow_shrink by (fastforce simp add: distrib_left)
 
+lemma real_shrink_eq:
+  fixes x y::real
+  shows "(x / (1 + \<bar>x\<bar>) = y / (1 + \<bar>y\<bar>)) \<longleftrightarrow> x = y"
+  by (metis real_shrink_Galois)
+
 lemma real_shrink_lt:
   fixes x::real
   shows "x / (1 + \<bar>x\<bar>) < y / (1 + \<bar>y\<bar>) \<longleftrightarrow> x < y"
diff -r d6e6618db929 -r b0ad3aba48f1 src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Mon Jun 26 13:22:50 2023 +0200
+++ b/src/HOL/Analysis/Function_Topology.thy	Mon Jun 26 14:38:26 2023 +0100
@@ -194,6 +194,10 @@
     unfolding product_topology_def using PiE_def by (auto)
 qed
 
+lemma topspace_product_topology_alt:
+  "topspace (product_topology X I) = {x \<in> extensional I. \<forall>i \<in> I. x i \<in> topspace(X i)}"
+  by (fastforce simp: PiE_iff)
+
 lemma product_topology_basis:
   assumes "\<And>i. openin (T i) (X i)" "finite {i. X i \<noteq> topspace (T i)}"
   shows "openin (product_topology T I) (\<Pi>\<^sub>E i\<in>I. X i)"
@@ -1577,4 +1581,76 @@
   then show ?thesis by metis
 qed
 
+subsection \<open>Limits\<close>
+
+text \<open>The original HOL Light proof was a mess, yuk\<close>
+lemma limitin_componentwise:
+   "limitin (product_topology X I) f l F \<longleftrightarrow>
+        l \<in> extensional I \<and>
+        eventually (\<lambda>a. f a \<in> topspace(product_topology X I)) F \<and>
+        (\<forall>i \<in> I. limitin (X i) (\<lambda>c. f c i) (l i) F)"
+    (is "?L \<longleftrightarrow> _ \<and> ?R1 \<and> ?R2")
+proof (cases "l \<in> extensional I")
+  case l: True
+  show ?thesis
+  proof (cases "\<forall>i\<in>I. l i \<in> topspace (X i)")
+    case True
+    have ?R1 if ?L
+      by (metis limitin_subtopology subtopology_topspace that)
+    moreover
+    have ?R2 if ?L
+      unfolding limitin_def
+    proof (intro conjI strip)
+      fix i U
+      assume "i \<in> I" and U: "openin (X i) U \<and> l i \<in> U"
+      then have "openin (product_topology X I) ({y. y i \<in> U} \<inter> topspace (product_topology X I))"
+        unfolding openin_product_topology arbitrary_union_of_relative_to [symmetric]
+        apply (simp add: relative_to_def topspace_product_topology_alt)
+        by (smt (verit, del_insts) Collect_cong arbitrary_union_of_inc finite_intersection_of_inc inf_commute)
+      moreover have "l \<in> {y. y i \<in> U} \<inter> topspace (product_topology X I)"
+        using U True l by (auto simp: extensional_def)
+      ultimately have "eventually (\<lambda>x. f x \<in> {y. y i \<in> U} \<inter> topspace (product_topology X I)) F"
+        by (metis limitin_def that)
+      then show "\<forall>\<^sub>F x in F. f x i \<in> U"
+        by (simp add: eventually_conj_iff)
+    qed (use True in auto)
+    moreover
+    have ?L if R1: ?R1 and R2: ?R2
+      unfolding limitin_def openin_product_topology all_union_of imp_conjL arbitrary_def
+    proof (intro conjI strip)
+      show l: "l \<in> topspace (product_topology X I)"
+        by (simp add: PiE_iff True l)
+      fix \<V>
+      assume "\<V> \<subseteq> Collect (finite intersection_of (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U)
+                   relative_to topspace (product_topology X I))"
+        and "l \<in> \<Union> \<V>"
+      then obtain \<W> where "finite \<W>" and \<W>X: "\<forall>X\<in>\<W>. l \<in> X"
+               and \<W>: "\<And>C. C \<in> \<W> \<Longrightarrow> C \<in> {{x. x i \<in> U} |i U. i \<in> I \<and> openin (X i) U}" 
+               and \<W>\<V>: "topspace (product_topology X I) \<inter> \<Inter> \<W> \<in> \<V>"
+        by (fastforce simp: intersection_of_def relative_to_def subset_eq)
+      have "\<forall>\<^sub>F x in F. f x \<in> topspace (product_topology X I) \<inter> \<Inter>\<W>"
+      proof -
+        have "\<And>W. W \<in> {{x. x i \<in> U} | i U. i \<in> I \<and> openin (X i) U} \<Longrightarrow> W \<in> \<W> \<Longrightarrow> \<forall>\<^sub>F x in F. f x \<in> W"
+          using \<W>X R2 by (auto simp: limitin_def)
+        with \<W> have "\<forall>\<^sub>F x in F. \<forall>W\<in>\<W>. f x \<in> W"
+          by (simp add: \<open>finite \<W>\<close> eventually_ball_finite)
+        with R1 show ?thesis
+          by (simp add: eventually_conj_iff)
+      qed
+      then show "\<forall>\<^sub>F x in F. f x \<in> \<Union>\<V>"
+        by (smt (verit, ccfv_threshold) \<W>\<V> UnionI eventually_mono)
+    qed
+    ultimately show ?thesis
+      using l by blast
+  next
+    case False
+    then show ?thesis
+      by (metis PiE_iff limitin_def topspace_product_topology)
+   qed
+next
+  case False
+  then show ?thesis
+    by (simp add: limitin_def PiE_iff)
+qed
+
 end
diff -r d6e6618db929 -r b0ad3aba48f1 src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Mon Jun 26 13:22:50 2023 +0200
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Mon Jun 26 14:38:26 2023 +0100
@@ -157,27 +157,27 @@
   shows "((\<lambda>i. inf (X i) (Y i)) \<longlongrightarrow> inf x y) net"
    unfolding inf_min eucl_inf by (intro assms tendsto_intros)
 
-lemma tendsto_Inf:
+lemma tendsto_Inf[tendsto_intros]:
   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::ordered_euclidean_space"
   assumes "finite K" "\<And>i. i \<in> K \<Longrightarrow> ((\<lambda>x. f x i) \<longlongrightarrow> l i) F"
   shows "((\<lambda>x. Inf (f x ` K)) \<longlongrightarrow> Inf (l ` K)) F"
   using assms
   by (induction K rule: finite_induct) (auto simp: cInf_insert_If tendsto_inf)
 
-lemma tendsto_Sup:
+lemma tendsto_Sup[tendsto_intros]:
   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::ordered_euclidean_space"
   assumes "finite K" "\<And>i. i \<in> K \<Longrightarrow> ((\<lambda>x. f x i) \<longlongrightarrow> l i) F"
   shows "((\<lambda>x. Sup (f x ` K)) \<longlongrightarrow> Sup (l ` K)) F"
   using assms
   by (induction K rule: finite_induct) (auto simp: cSup_insert_If tendsto_sup)
 
-lemma continuous_map_Inf:
+lemma continuous_map_Inf [continuous_intros]:
   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::ordered_euclidean_space"
   assumes "finite K" "\<And>i. i \<in> K \<Longrightarrow> continuous_map X euclidean (\<lambda>x. f x i)"
   shows "continuous_map X euclidean (\<lambda>x. INF i\<in>K. f x i)"
   using assms by (simp add: continuous_map_atin tendsto_Inf)
 
-lemma continuous_map_Sup:
+lemma continuous_map_Sup [continuous_intros]:
   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::ordered_euclidean_space"
   assumes "finite K" "\<And>i. i \<in> K \<Longrightarrow> continuous_map X euclidean (\<lambda>x. f x i)"
   shows "continuous_map X euclidean (\<lambda>x. SUP i\<in>K. f x i)"
diff -r d6e6618db929 -r b0ad3aba48f1 src/HOL/Analysis/Urysohn.thy
--- a/src/HOL/Analysis/Urysohn.thy	Mon Jun 26 13:22:50 2023 +0200
+++ b/src/HOL/Analysis/Urysohn.thy	Mon Jun 26 14:38:26 2023 +0100
@@ -161,7 +161,7 @@
     qed
   qed
   then have contf: "continuous_map X (top_of_set {0..1}) f"
-    by (force simp add: Met_TC.continuous_map_to_metric dist_real_def continuous_map_in_subtopology fim simp flip: Met_TC.mtopology_is_euclideanreal)
+    by (force simp add: Met_TC.continuous_map_to_metric dist_real_def continuous_map_in_subtopology fim simp flip: mtopology_is_euclidean)
   define g where "g \<equiv> \<lambda>x. a + (b - a) * f x"
   show thesis
   proof
@@ -1976,8 +1976,8 @@
         regular_space (subtopology ?Y (topspace ?Y - {None})) \<and> locally_compact_space (subtopology ?Y (topspace ?Y - {None}))"
     by (rule regular_space_one_point_compactification) (auto simp: compactin_subtopology closedin_subtopology closedin_Alexandroff_I)
   also have "... \<longleftrightarrow> regular_space X \<and> locally_compact_space X"
-    using embedding_map_Some embedding_map_imp_homeomorphic_space homeomorphic_locally_compact_space homeomorphic_regular_space 
-      by fastforce
+    by (metis embedding_map_Some embedding_map_imp_homeomorphic_space homeomorphic_locally_compact_space 
+        homeomorphic_regular_space topspace_Alexandroff_compactification_delete)
   finally show ?thesis .
 qed
 
diff -r d6e6618db929 -r b0ad3aba48f1 src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Mon Jun 26 13:22:50 2023 +0200
+++ b/src/HOL/Library/Countable_Set.thy	Mon Jun 26 14:38:26 2023 +0100
@@ -14,6 +14,9 @@
 definition countable :: "'a set \<Rightarrow> bool" where
   "countable S \<longleftrightarrow> (\<exists>f::'a \<Rightarrow> nat. inj_on f S)"
 
+lemma countable_as_injective_image_subset: "countable S \<longleftrightarrow> (\<exists>f. \<exists>K::nat set. S = f ` K \<and> inj_on f K)"
+  by (metis countable_def inj_on_the_inv_into the_inv_into_onto)
+   
 lemma countableE:
   assumes S: "countable S" obtains f :: "'a \<Rightarrow> nat" where "inj_on f S"
   using S by (auto simp: countable_def)
diff -r d6e6618db929 -r b0ad3aba48f1 src/HOL/Library/Equipollence.thy
--- a/src/HOL/Library/Equipollence.thy	Mon Jun 26 13:22:50 2023 +0200
+++ b/src/HOL/Library/Equipollence.thy	Mon Jun 26 14:38:26 2023 +0100
@@ -1,7 +1,7 @@
 section \<open>Equipollence and Other Relations Connected with Cardinality\<close>
 
 theory "Equipollence"
-  imports FuncSet 
+  imports FuncSet Countable_Set
 begin
 
 subsection\<open>Eqpoll\<close>
@@ -47,11 +47,7 @@
   by (meson card_of_ordLeq eqpoll_iff_card_of_ordIso lepoll_def lepoll_trans ordIso_iff_ordLeq)
 
 lemma lepoll_trans2 [trans]: "\<lbrakk>A \<lesssim> B; B \<approx> C\<rbrakk> \<Longrightarrow> A \<lesssim> C"
-  apply (clarsimp simp: eqpoll_def lepoll_def bij_betw_def)
-  apply (rename_tac f g)
-  apply (rule_tac x="g \<circ> f" in exI)
-  apply (auto simp: image_subset_iff inj_on_def)
-  done
+  by (metis bij_betw_def eqpoll_def lepoll_def lepoll_trans order_refl)
 
 lemma eqpoll_sym: "A \<approx> B \<Longrightarrow> B \<approx> A"
   unfolding eqpoll_def
@@ -87,9 +83,7 @@
   by (auto simp: lepoll_iff)
 
 lemma infinite_le_lepoll: "infinite A \<longleftrightarrow> (UNIV::nat set) \<lesssim> A"
-apply (auto simp: lepoll_def)
-  apply (simp add: infinite_countable_subset)
-  using infinite_iff_countable_subset by blast
+  by (simp add: infinite_iff_countable_subset lepoll_def)
 
 lemma lepoll_Pow_self: "A \<lesssim> Pow A"
   unfolding lepoll_def inj_def
@@ -121,12 +115,7 @@
   by (blast intro: lepoll_antisym singleton_lepoll)
 
 lemma subset_singleton_iff_lepoll: "(\<exists>x. S \<subseteq> {x}) \<longleftrightarrow> S \<lesssim> {()}"
-proof safe
-  show "S \<lesssim> {()}" if "S \<subseteq> {x}" for x
-    using subset_imp_lepoll [OF that] by (simp add: singleton_eqpoll lepoll_trans2)
-  show "\<exists>x. S \<subseteq> {x}" if "S \<lesssim> {()}"
-  by (metis (no_types, opaque_lifting) image_empty image_insert lepoll_iff that)
-qed
+  using lepoll_iff by fastforce
 
 lemma infinite_insert_lepoll:
   assumes "infinite A" shows "insert a A \<lesssim> A"
@@ -158,6 +147,12 @@
     using \<open>infinite A\<close> infinite_le_lepoll lepoll_trans by auto
 qed
 
+lemma countable_lepoll: "\<lbrakk>countable A; B \<lesssim> A\<rbrakk> \<Longrightarrow> countable B"
+  by (meson countable_image countable_subset lepoll_iff)
+
+lemma countable_eqpoll: "\<lbrakk>countable A; B \<approx> A\<rbrakk> \<Longrightarrow> countable B"
+  using countable_lepoll eqpoll_imp_lepoll by blast
+
 subsection\<open>The strict relation\<close>
 
 lemma lesspoll_not_refl [iff]: "~ (i \<prec> i)"
@@ -192,6 +187,9 @@
   assumes "infinite A" "finite B" shows "B \<prec> A"
   by (meson assms eqpoll_finite_iff finite_lepoll_infinite lesspoll_def)
 
+lemma countable_lesspoll: "\<lbrakk>countable A; B \<prec> A\<rbrakk> \<Longrightarrow> countable B"
+  using countable_lepoll lesspoll_def by blast
+
 subsection\<open>Mapping by an injection\<close>
 
 lemma inj_on_image_eqpoll_self: "inj_on f A \<Longrightarrow> f ` A \<approx> A"