merged
authorwenzelm
Wed, 05 Jul 2023 15:01:46 +0200
changeset 78255 3e11f510b3f6
parent 78250 400aecdfd71f (diff)
parent 78254 50a949d316d3 (current diff)
child 78256 71e1aa0d9421
merged
--- a/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Wed Jul 05 14:33:32 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Wed Jul 05 15:01:46 2023 +0200
@@ -1438,7 +1438,7 @@
     have "topspace Y = topspace X"
       by (auto simp: Y_def)
     have "openin X T \<longrightarrow> openin Y T" for T
-      by (simp add: Y_def arbitrary_union_of_inc finite_intersection_of_inc openin_subbase openin_subset relative_to_subset)
+      by (simp add: Y_def arbitrary_union_of_inc finite_intersection_of_inc openin_subbase openin_subset relative_to_subset_inc)
     have "compact_space Y"
     proof (rule Alexander_subbase_alt)
       show "\<exists>\<F>'. finite \<F>' \<and> \<F>' \<subseteq> \<C> \<and> topspace X \<subseteq> \<Union> \<F>'" 
@@ -1465,7 +1465,7 @@
     have "Y = X"
       using R \<open>\<And>S. openin X S \<longrightarrow> openin Y S\<close> \<open>compact_space Y\<close> \<open>topspace Y = topspace X\<close> by blast
     moreover have "openin Y (topspace X - S)"
-      by (simp add: Y_def arbitrary_union_of_inc finite_intersection_of_inc openin_subbase relative_to_subset)
+      by (simp add: Y_def arbitrary_union_of_inc finite_intersection_of_inc openin_subbase relative_to_subset_inc)
     ultimately show "closedin X S"
       unfolding closedin_def using S compactin_subset_topspace by blast
   qed
@@ -2580,7 +2580,6 @@
 qed
 
 
-
 subsection\<open>Locally compact spaces\<close>
 
 definition locally_compact_space 
@@ -3897,6 +3896,9 @@
     by (metis Diff_disjoint Diff_iff Un_Diff_cancel closedin_def disjnt_def inf_commute sup.orderE sup_commute)
 qed
 
+lemma quasi_components_lepoll_topspace: "quasi_components_of X \<lesssim> topspace X"
+  by (simp add: image_lepoll quasi_components_of_def)
+
 lemma quasi_component_of_separated:
    "quasi_component_of X x y \<longleftrightarrow>
      x \<in> topspace X \<and> y \<in> topspace X \<and>
--- a/src/HOL/Analysis/Abstract_Topology.thy	Wed Jul 05 14:33:32 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Wed Jul 05 15:01:46 2023 +0200
@@ -4490,7 +4490,7 @@
   next
     case (Basis s)
     then show ?case
-      by (simp add: Sup_upper arbitrary_union_of_inc finite'_intersection_of_inc relative_to_subset)
+      by (simp add: Sup_upper arbitrary_union_of_inc finite'_intersection_of_inc relative_to_subset_inc)
   qed auto
 next
   fix A
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Wed Jul 05 14:33:32 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Wed Jul 05 15:01:46 2023 +0200
@@ -8,9 +8,9 @@
 
 theory Abstract_Topology_2
   imports
-    Elementary_Topology
-    Abstract_Topology
+    Elementary_Topology Abstract_Topology
     "HOL-Library.Indicator_Function"
+    "HOL-Library.Equipollence"
 begin
 
 text \<open>Combination of Elementary and Abstract Topology\<close>
@@ -1695,4 +1695,30 @@
     by (metis continuous_on_subset continuous_shrink subset_UNIV)
 qed
 
+lemma card_eq_real_subset:
+  fixes a b::real
+  assumes "a < b" and S: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> x \<in> S"
+  shows "S \<approx> (UNIV::real set)"
+proof (rule lepoll_antisym)
+  show "S \<lesssim> (UNIV::real set)"
+    by (simp add: subset_imp_lepoll)
+  define f where "f \<equiv> \<lambda>x. (a+b) / 2 + (b-a) / 2 * (x / (1 + \<bar>x\<bar>))"
+  show "(UNIV::real set) \<lesssim> S"
+    unfolding lepoll_def
+  proof (intro exI conjI)
+    show "inj f"
+      unfolding inj_on_def f_def
+      by (smt (verit, ccfv_SIG) real_shrink_eq \<open>a<b\<close> divide_eq_0_iff mult_cancel_left times_divide_eq_right)
+    have pos: "(b-a) / 2 > 0"
+      using \<open>a<b\<close> by auto
+    have *: "a < (a + b) / 2 + (b - a) / 2 * x \<longleftrightarrow> (b - a) > (b - a) * -x"
+            "(a + b) / 2 + (b - a) / 2 * x < b \<longleftrightarrow> (b - a) * x < (b - a)" for x
+      by (auto simp: field_simps)
+    show "range f \<subseteq> S"
+      using shrink_range [of UNIV] \<open>a < b\<close>
+      unfolding subset_iff f_def greaterThanLessThan_iff image_iff
+      by (smt (verit, best) S * mult_less_cancel_left2 mult_minus_right)
+  qed
+qed
+
 end
\ No newline at end of file
--- a/src/HOL/Analysis/FSigma.thy	Wed Jul 05 14:33:32 2023 +0200
+++ b/src/HOL/Analysis/FSigma.thy	Wed Jul 05 15:01:46 2023 +0200
@@ -27,7 +27,7 @@
     by (simp add: countable_intersection_of_inc)
   then show ?thesis
     unfolding gdelta_in_def
-    by (metis countable_intersection_of_inter relative_to_def relative_to_imp_subset relative_to_subset)
+    by (metis countable_intersection_of_inter relative_to_def relative_to_imp_subset relative_to_subset_inc)
 qed
 
 lemma fsigma_in_subset: "fsigma_in X S \<Longrightarrow> S \<subseteq> topspace X"
--- a/src/HOL/Analysis/Locally.thy	Wed Jul 05 14:33:32 2023 +0200
+++ b/src/HOL/Analysis/Locally.thy	Wed Jul 05 15:01:46 2023 +0200
@@ -968,5 +968,191 @@
   qed
 qed
 
+subsection \<open>Dimension of a topological space\<close>
+
+text\<open>Basic definition of the small inductive dimension relation. Works in any topological space.\<close>
+
+inductive dimension_le :: "['a topology, int] \<Rightarrow> bool" (infix "dim'_le" 50) 
+  where "\<lbrakk>-1 \<le> n;
+        \<And>V a. \<lbrakk>openin X V; a \<in> V\<rbrakk> \<Longrightarrow> \<exists>U. a \<in> U \<and> U \<subseteq> V \<and> openin X U \<and> (subtopology X (X frontier_of U)) dim_le (n-1)\<rbrakk>
+              \<Longrightarrow> X dim_le (n::int)"
+
+lemma dimension_le_neighbourhood_base:
+   "X dim_le n \<longleftrightarrow>
+   -1 \<le> n \<and> neighbourhood_base_of (\<lambda>U. openin X U \<and> (subtopology X (X frontier_of U)) dim_le (n-1)) X"
+  by (smt (verit, best) dimension_le.simps open_neighbourhood_base_of)
+
+lemma dimension_le_bound: "X dim_le n \<Longrightarrow>-1 \<le> n"
+  using dimension_le.simps by blast
+  
+lemma dimension_le_mono [rule_format]:
+  assumes "X dim_le m"
+  shows "m \<le> n \<longrightarrow> X dim_le n"
+  using assms
+proof (induction arbitrary: n rule: dimension_le.induct)
+  case (1 m X)
+  show ?case
+  proof (intro strip dimension_le.intros)
+    show "-1 \<le> n" if "m \<le> n" for n :: int using that using "1.hyps" by fastforce    
+    show "\<exists>U. a \<in> U \<and> U \<subseteq> V \<and> openin X U \<and> subtopology X (X frontier_of U) dim_le n-1"
+      if "m \<le> n" and "openin X V" and "a \<in> V" for n V a
+      using that by (meson "1.IH" diff_right_mono)
+  qed
+qed
+
+lemma dimension_le_eq_empty:
+   "X dim_le -1 \<longleftrightarrow> topspace X = {}"
+proof
+  assume "X dim_le (-1)"
+  then show "topspace X = {}"
+    by (smt (verit, ccfv_threshold) Diff_empty Diff_eq_empty_iff dimension_le.cases openin_topspace subset_eq)
+next
+  assume "topspace X = {}"
+  then show "X dim_le (-1)"
+    using dimension_le.simps openin_subset by fastforce
+qed
+
+lemma dimension_le_0_neighbourhood_base_of_clopen:
+  "X dim_le 0 \<longleftrightarrow> neighbourhood_base_of (\<lambda>U. closedin X U \<and> openin X U) X"
+proof -
+  have "(subtopology X (X frontier_of U) dim_le -1) =
+        closedin X U" if "openin X U" for U
+    by (metis dimension_le_eq_empty frontier_of_eq_empty frontier_of_subset_topspace openin_subset that topspace_subtopology_subset)
+  then show ?thesis
+    by (smt (verit, del_insts) dimension_le.simps open_neighbourhood_base_of)
+qed
+
+lemma dimension_le_subtopology:
+  "X dim_le n \<Longrightarrow> subtopology X S dim_le n"
+proof (induction arbitrary: S rule: dimension_le.induct)
+  case (1 n X)
+  show ?case 
+  proof (intro dimension_le.intros)
+    show "- 1 \<le> n"
+      by (simp add: "1.hyps")
+    fix U' a
+    assume U': "openin (subtopology X S) U'" and "a \<in> U'"
+    then obtain U where U: "openin X U" "U' = U \<inter> S"
+      by (meson openin_subtopology)
+    then obtain V where "a \<in> V" "V \<subseteq> U" "openin X V" 
+      and subV: "subtopology X (X frontier_of V) dim_le n-1" 
+      and dimV: "\<And>T. subtopology X (X frontier_of V \<inter> T) dim_le n-1"
+      by (metis "1.IH" Int_iff \<open>a \<in> U'\<close> subtopology_subtopology)
+    show "\<exists>W. a \<in> W \<and> W \<subseteq> U' \<and> openin (subtopology X S) W \<and> subtopology (subtopology X S) (subtopology X S frontier_of W) dim_le n-1"
+    proof (intro exI conjI)
+      show "a \<in> S \<inter> V" "S \<inter> V \<subseteq> U'"
+        using \<open>U' = U \<inter> S\<close> \<open>a \<in> U'\<close> \<open>a \<in> V\<close> \<open>V \<subseteq> U\<close> by blast+
+      show "openin (subtopology X S) (S \<inter> V)"
+        by (simp add: \<open>openin X V\<close> openin_subtopology_Int2)
+      have "S \<inter> subtopology X S frontier_of V \<subseteq> X frontier_of V"
+        by (simp add: frontier_of_subtopology_subset)
+      then show "subtopology (subtopology X S) (subtopology X S frontier_of (S \<inter> V)) dim_le n-1"
+        by (metis dimV frontier_of_restrict inf.absorb_iff2 inf_left_idem subtopology_subtopology topspace_subtopology)
+    qed
+  qed
+qed
+
+lemma dimension_le_subtopologies:
+   "\<lbrakk>subtopology X T dim_le n; S \<subseteq> T\<rbrakk> \<Longrightarrow> (subtopology X S) dim_le n"
+  by (metis dimension_le_subtopology inf.absorb_iff2 subtopology_subtopology)
+
+lemma dimension_le_eq_subtopology:
+   "(subtopology X S) dim_le n \<longleftrightarrow>
+    -1 \<le> n \<and>
+    (\<forall>V a. openin X V \<and> a \<in> V \<and> a \<in> S
+           \<longrightarrow> (\<exists>U. a \<in> U \<and> U \<subseteq> V \<and> openin X U \<and>
+                    subtopology X (subtopology X S frontier_of (S \<inter> U)) dim_le (n-1)))"
+proof -
+  have *: "(\<exists>T. a \<in> T \<and> T \<inter> S \<subseteq> V \<inter> S \<and> openin X T \<and> subtopology X (S \<inter> (subtopology X S frontier_of (T \<inter> S))) dim_le n-1)
+       \<longleftrightarrow> (\<exists>U. a \<in> U \<and> U \<subseteq> V \<and> openin X U \<and> subtopology X (subtopology X S frontier_of (S \<inter> U)) dim_le n-1)"
+    if "a \<in> V" "a \<in> S" "openin X V" for a V
+  proof -
+    have "\<exists>U. a \<in> U \<and> U \<subseteq> V \<and> openin X U \<and> subtopology X (subtopology X S frontier_of (S \<inter> U)) dim_le n-1"
+      if "a \<in> T" and sub: "T \<inter> S \<subseteq> V \<inter> S" and "openin X T"
+        and dim: "subtopology X (S \<inter> subtopology X S frontier_of (T \<inter> S)) dim_le n-1"
+      for T 
+    proof (intro exI conjI)
+      show "openin X (T \<inter> V)"
+        using \<open>openin X V\<close> \<open>openin X T\<close> by blast
+      show "subtopology X (subtopology X S frontier_of (S \<inter> (T \<inter> V))) dim_le n-1"
+        by (metis dim frontier_of_subset_subtopology inf.boundedE inf_absorb2 inf_assoc inf_commute sub)
+    qed (use \<open>a \<in> V\<close> \<open>a \<in> T\<close> in auto)
+    moreover have "\<exists>T. a \<in> T \<and> T \<inter> S \<subseteq> V \<inter> S \<and> openin X T \<and> subtopology X (S \<inter> subtopology X S frontier_of (T \<inter> S)) dim_le n-1"
+      if "a \<in> U" and "U \<subseteq> V" and "openin X U"
+        and dim: "subtopology X (subtopology X S frontier_of (S \<inter> U)) dim_le n-1"
+      for U
+      by (metis that frontier_of_subset_subtopology inf_absorb2 inf_commute inf_le1 le_inf_iff)
+    ultimately show ?thesis
+      by safe
+  qed
+  show ?thesis
+    apply (simp add: dimension_le.simps [of _ n] subtopology_subtopology openin_subtopology flip: *)
+    by (safe; metis Int_iff inf_le2 le_inf_iff)
+qed
+
+
+lemma homeomorphic_space_dimension_le_aux:
+  assumes "X homeomorphic_space Y" "X dim_le of_nat n - 1"
+  shows "Y dim_le of_nat n - 1"
+  using assms
+proof (induction n arbitrary: X Y)
+  case 0
+  then show ?case
+    by (simp add: dimension_le_eq_empty homeomorphic_empty_space)
+next
+  case (Suc n)
+  then have X_dim_n: "X dim_le n"
+    by simp
+  show ?case 
+  proof (clarsimp simp add: dimension_le.simps [of Y n])
+    fix V b
+    assume "openin Y V" and "b \<in> V"
+    obtain f g where fg: "homeomorphic_maps X Y f g"
+      using \<open>X homeomorphic_space Y\<close> homeomorphic_space_def by blast
+    then have "openin X (g ` V)"
+      using \<open>openin Y V\<close> homeomorphic_map_openness_eq homeomorphic_maps_map by blast
+    then obtain U where "g b \<in> U" "openin X U" and gim: "U \<subseteq> g ` V" and sub: "subtopology X (X frontier_of U) dim_le int n - int 1"
+      using X_dim_n unfolding dimension_le.simps [of X n] by (metis \<open>b \<in> V\<close> imageI of_nat_eq_1_iff)
+    show "\<exists>U. b \<in> U \<and> U \<subseteq> V \<and> openin Y U \<and> subtopology Y (Y frontier_of U) dim_le int n - 1"
+    proof (intro conjI exI)
+      show "b \<in> f ` U"
+        by (metis (no_types, lifting) \<open>b \<in> V\<close> \<open>g b \<in> U\<close> \<open>openin Y V\<close> fg homeomorphic_maps_map image_iff openin_subset subsetD)
+      show "f ` U \<subseteq> V"
+        by (smt (verit, ccfv_threshold) \<open>openin Y V\<close> fg gim homeomorphic_maps_map image_iff openin_subset subset_iff)
+      show "openin Y (f ` U)"
+        using \<open>openin X U\<close> fg homeomorphic_map_openness_eq homeomorphic_maps_map by blast
+      show "subtopology Y (Y frontier_of f ` U) dim_le int n-1"
+      proof (rule Suc.IH)
+        have "homeomorphic_maps (subtopology X (X frontier_of U)) (subtopology Y (Y frontier_of f ` U)) f g"
+          using \<open>openin X U\<close> fg
+          by (metis frontier_of_subset_topspace homeomorphic_map_frontier_of homeomorphic_maps_map homeomorphic_maps_subtopologies openin_subset topspace_subtopology topspace_subtopology_subset)
+        then show "subtopology X (X frontier_of U) homeomorphic_space subtopology Y (Y frontier_of f ` U)"
+          using homeomorphic_space_def by blast
+        show "subtopology X (X frontier_of U) dim_le int n-1"
+          using sub by fastforce
+      qed
+    qed
+  qed
+qed
+
+lemma homeomorphic_space_dimension_le:
+  assumes "X homeomorphic_space Y"
+  shows "X dim_le n \<longleftrightarrow> Y dim_le n"
+proof (cases "n \<ge> -1")
+  case True
+  then show ?thesis
+    using homeomorphic_space_dimension_le_aux [of _ _ "nat(n+1)"] by (smt (verit) assms homeomorphic_space_sym nat_eq_iff)
+next
+  case False
+  then show ?thesis
+    by (metis dimension_le_bound)
+qed
+
+lemma dimension_le_retraction_map_image:
+   "\<lbrakk>retraction_map X Y r; X dim_le n\<rbrakk> \<Longrightarrow> Y dim_le n"
+  by (meson dimension_le_subtopology homeomorphic_space_dimension_le retraction_map_def retraction_maps_section_image2)
+
+lemma dimension_le_discrete_topology [simp]: "(discrete_topology U) dim_le 0"
+  using dimension_le.simps dimension_le_eq_empty by fastforce
 
 end
--- a/src/HOL/Analysis/Urysohn.thy	Wed Jul 05 14:33:32 2023 +0200
+++ b/src/HOL/Analysis/Urysohn.thy	Wed Jul 05 15:01:46 2023 +0200
@@ -1263,6 +1263,27 @@
 qed
 
 
+lemma zero_dimensional_imp_completely_regular_space:
+  assumes "X dim_le 0" 
+  shows "completely_regular_space X"
+proof (clarsimp simp: completely_regular_space_def)
+  fix C a
+  assume "closedin X C" and "a \<in> topspace X" and "a \<notin> C"
+  then obtain U where "closedin X U" "openin X U" "a \<in> U" and U: "U \<subseteq> topspace X - C"
+    using assms by (force simp add: closedin_def dimension_le_0_neighbourhood_base_of_clopen open_neighbourhood_base_of)
+  show "\<exists>f. continuous_map X (top_of_set {0::real..1}) f \<and> f a = 0 \<and> f ` C \<subseteq> {1}"
+  proof (intro exI conjI)
+    have "continuous_map X euclideanreal (\<lambda>x. if x \<in> U then 0 else 1)"
+      using \<open>closedin X U\<close> \<open>openin X U\<close> apply (clarsimp simp: continuous_map_def closedin_def)
+      by (smt (verit) Diff_iff mem_Collect_eq openin_subopen subset_eq)
+    then show "continuous_map X (top_of_set {0::real..1}) (\<lambda>x. if x \<in> U then 0 else 1)"
+      by (auto simp: continuous_map_in_subtopology)
+  qed (use U \<open>a \<in> U\<close> in auto)
+qed
+
+lemma zero_dimensional_imp_regular_space: "X dim_le 0 \<Longrightarrow> regular_space X"
+  by (simp add: completely_regular_imp_regular_space zero_dimensional_imp_completely_regular_space)
+
 lemma (in Metric_space) t1_space_mtopology:
    "t1_space mtopology"
   using Hausdorff_space_mtopology t1_or_Hausdorff_space by blast
@@ -4301,4 +4322,864 @@
   qed
 qed
 
+subsection\<open>Size bounds on connected or path-connected spaces\<close>
+
+lemma connected_space_imp_card_ge_alt:
+  assumes "connected_space X" "completely_regular_space X" "closedin X S" "S \<noteq> {}" "S \<noteq> topspace X"
+  shows "(UNIV::real set) \<lesssim> topspace X"
+proof -
+  have "S \<subseteq> topspace X"
+    using \<open>closedin X S\<close> closedin_subset by blast
+  then obtain a where "a \<in> topspace X" "a \<notin> S"
+    using \<open>S \<noteq> topspace X\<close> by blast
+  have "(UNIV::real set) \<lesssim> {0..1::real}"
+    using card_eq_real_subset 
+    by (meson atLeastAtMost_iff eqpoll_imp_lepoll eqpoll_sym less_eq_real_def zero_less_one)
+  also have "\<dots> \<lesssim> topspace X"
+  proof -
+    obtain f where contf: "continuous_map X euclidean f"
+      and fim: "f \<in> (topspace X) \<rightarrow> {0..1::real}"
+      and f0: "f a = 0" and f1: "f ` S \<subseteq> {1}"
+      using \<open>completely_regular_space X\<close>
+      unfolding completely_regular_space_def
+      by (metis Diff_iff \<open>a \<in> topspace X\<close> \<open>a \<notin> S\<close> \<open>closedin X S\<close> continuous_map_in_subtopology image_subset_iff_funcset)
+    have "\<exists>y\<in>topspace X. x = f y" if "0 \<le> x" and "x \<le> 1" for x
+    proof -
+      have "connectedin euclidean (f ` topspace X)"
+        using \<open>connected_space X\<close> connectedin_continuous_map_image connectedin_topspace contf by blast
+      moreover have "\<exists>y. 0 = f y \<and> y \<in> topspace X"
+        using \<open>a \<in> topspace X\<close> f0 by auto
+      moreover have "\<exists>y. 1 = f y \<and> y \<in> topspace X"
+        using \<open>S \<subseteq> topspace X\<close> \<open>S \<noteq> {}\<close> f1 by fastforce
+      ultimately show ?thesis
+        using that by (fastforce simp: is_interval_1 simp flip: is_interval_connected_1)
+    qed
+    then show ?thesis
+      unfolding lepoll_iff using atLeastAtMost_iff by blast
+  qed
+  finally show ?thesis .
+qed
+
+
+lemma connected_space_imp_card_ge_gen:
+  assumes "connected_space X" "normal_space X" "closedin X S" "closedin X T" "S \<noteq> {}" "T \<noteq> {}" "disjnt S T"
+  shows "(UNIV::real set) \<lesssim> topspace X"
+proof -
+  have "(UNIV::real set) \<lesssim> {0..1::real}"
+    by (metis atLeastAtMost_iff card_eq_real_subset eqpoll_imp_lepoll eqpoll_sym less_le_not_le zero_less_one)
+  also have "\<dots>\<lesssim> topspace X"
+  proof -
+    obtain f where contf: "continuous_map X euclidean f"
+       and fim: "f \<in> (topspace X) \<rightarrow> {0..1::real}"
+       and f0: "f ` S \<subseteq> {0}" and f1: "f ` T \<subseteq> {1}"
+      using assms by (metis continuous_map_in_subtopology normal_space_iff_Urysohn image_subset_iff_funcset)
+    have "\<exists>y\<in>topspace X. x = f y" if "0 \<le> x" and "x \<le> 1" for x
+    proof -
+      have "connectedin euclidean (f ` topspace X)"
+        using \<open>connected_space X\<close> connectedin_continuous_map_image connectedin_topspace contf by blast
+      moreover have "\<exists>y. 0 = f y \<and> y \<in> topspace X"
+        using \<open>closedin X S\<close> \<open>S \<noteq> {}\<close> closedin_subset f0 by fastforce
+      moreover have "\<exists>y. 1 = f y \<and> y \<in> topspace X"
+        using \<open>closedin X T\<close> \<open>T \<noteq> {}\<close> closedin_subset f1 by fastforce
+      ultimately show ?thesis
+        using that by (fastforce simp: is_interval_1 simp flip: is_interval_connected_1)
+    qed
+    then show ?thesis
+      unfolding lepoll_iff using atLeastAtMost_iff by blast
+  qed
+  finally show ?thesis .
+qed
+
+lemma connected_space_imp_card_ge:
+  assumes "connected_space X" "normal_space X" "t1_space X" and nosing: "\<not> (\<exists>a. topspace X \<subseteq> {a})"
+  shows "(UNIV::real set) \<lesssim> topspace X"
+proof -
+  obtain a b where "a \<in> topspace X" "b \<in> topspace X" "a \<noteq> b"
+    by (metis nosing singletonI subset_iff)
+  then have "{a} \<noteq> topspace X"
+    by force
+  with connected_space_imp_card_ge_alt assms show ?thesis
+    by (metis \<open>a \<in> topspace X\<close> closedin_t1_singleton insert_not_empty normal_imp_completely_regular_space_A)
+qed
+
+lemma connected_space_imp_infinite_gen:
+   "\<lbrakk>connected_space X; t1_space X; \<nexists>a. topspace X \<subseteq> {a}\<rbrakk> \<Longrightarrow> infinite(topspace X)"
+  by (metis connected_space_discrete_topology finite_t1_space_imp_discrete_topology)
+
+lemma connected_space_imp_infinite:
+   "\<lbrakk>connected_space X; Hausdorff_space X; \<nexists>a. topspace X \<subseteq> {a}\<rbrakk> \<Longrightarrow> infinite(topspace X)"
+  by (simp add: Hausdorff_imp_t1_space connected_space_imp_infinite_gen)
+
+lemma connected_space_imp_infinite_alt:
+  assumes "connected_space X" "regular_space X" "closedin X S" "S \<noteq> {}" "S \<noteq> topspace X"
+  shows "infinite(topspace X)"
+proof -
+  have "S \<subseteq> topspace X"
+    using \<open>closedin X S\<close> closedin_subset by blast
+  then obtain a where a: "a \<in> topspace X" "a \<notin> S"
+    using \<open>S \<noteq> topspace X\<close> by blast
+  have "\<exists>\<Phi>. \<forall>n. (disjnt (\<Phi> n) S \<and> a \<in> \<Phi> n \<and> openin X (\<Phi> n)) \<and> \<Phi>(Suc n) \<subset> \<Phi> n"
+  proof (rule dependent_nat_choice)
+    show "\<exists>T. disjnt T S \<and> a \<in> T \<and> openin X T"
+      by (metis Diff_iff a \<open>closedin X S\<close> closedin_def disjnt_iff)
+    fix V n
+    assume \<section>: "disjnt V S \<and> a \<in> V \<and> openin X V"
+    then obtain U C where U: "openin X U" "closedin X C" "a \<in> U" "U \<subseteq> C" "C \<subseteq> V"
+      using \<open>regular_space X\<close> by (metis neighbourhood_base_of neighbourhood_base_of_closedin)
+    with assms have "U \<subset> V"
+      by (metis "\<section>" \<open>S \<subseteq> topspace X\<close> connected_space_clopen_in disjnt_def empty_iff inf.absorb_iff2 inf.orderE psubsetI subset_trans)
+    with U show "\<exists>U. (disjnt U S \<and> a \<in> U \<and> openin X U) \<and> U \<subset> V"
+      using "\<section>" disjnt_subset1 by blast
+  qed
+  then obtain \<Phi> where \<Phi>: "\<And>n. disjnt (\<Phi> n) S \<and> a \<in> \<Phi> n \<and> openin X (\<Phi> n)"
+    and \<Phi>sub: "\<And>n. \<Phi> (Suc n) \<subset> \<Phi> n" by metis
+  then have "decseq \<Phi>"
+    by (simp add: decseq_SucI psubset_eq)
+  have "\<forall>n. \<exists>x. x \<in> \<Phi> n \<and> x \<notin> \<Phi>(Suc n)"
+    by (meson \<Phi>sub psubsetE subsetI)
+  then obtain f where fin: "\<And>n. f n \<in> \<Phi> n" and fout: "\<And>n. f n \<notin> \<Phi>(Suc n)"
+    by metis
+  have "range f \<subseteq> topspace X"
+    by (meson \<Phi> fin image_subset_iff openin_subset subset_iff)
+  moreover have "inj f"
+    by (metis Suc_le_eq \<open>decseq \<Phi>\<close> decseq_def fin fout linorder_injI subsetD)
+  ultimately show ?thesis
+    using infinite_iff_countable_subset by blast
+qed
+
+lemma path_connected_space_imp_card_ge:
+  assumes "path_connected_space X" "Hausdorff_space X" and nosing: "\<not> (\<exists>x. topspace X \<subseteq> {x})"
+  shows "(UNIV::real set) \<lesssim> topspace X"
+proof -
+  obtain a b where "a \<in> topspace X" "b \<in> topspace X" "a \<noteq> b"
+    by (metis nosing singletonI subset_iff)
+  then obtain \<gamma> where \<gamma>: "pathin X \<gamma>" "\<gamma> 0 = a" "\<gamma> 1 = b"
+    by (meson \<open>a \<in> topspace X\<close> \<open>b \<in> topspace X\<close> \<open>path_connected_space X\<close> path_connected_space_def)
+  let ?Y = "subtopology X (\<gamma> ` (topspace (subtopology euclidean {0..1})))"
+  have "(UNIV::real set) \<lesssim>  topspace ?Y"
+  proof (intro compact_Hausdorff_or_regular_imp_normal_space connected_space_imp_card_ge)
+    show "connected_space ?Y"
+      using \<open>pathin X \<gamma>\<close> connectedin_def connectedin_path_image by auto
+    show "Hausdorff_space ?Y \<or> regular_space ?Y"
+      using Hausdorff_space_subtopology \<open>Hausdorff_space X\<close> by blast
+    show "t1_space ?Y"
+      using Hausdorff_imp_t1_space \<open>Hausdorff_space X\<close> t1_space_subtopology by blast
+    show "compact_space ?Y"
+      by (simp add: \<open>pathin X \<gamma>\<close> compact_space_subtopology compactin_path_image)
+    have "a \<in> topspace ?Y" "b \<in> topspace ?Y"
+      using \<gamma> pathin_subtopology by fastforce+
+    with \<open>a \<noteq> b\<close> show "\<nexists>x. topspace ?Y \<subseteq> {x}"
+      by blast
+  qed
+  also have "\<dots> \<lesssim> \<gamma> ` {0..1}"
+    by (simp add: subset_imp_lepoll)
+  also have "\<dots> \<lesssim> topspace X"
+    by (meson \<gamma> path_image_subset_topspace subset_imp_lepoll image_subset_iff_funcset)
+  finally show ?thesis .
+qed
+
+lemma connected_space_imp_uncountable:
+  assumes "connected_space X" "regular_space X" "Hausdorff_space X" "\<not> (\<exists>a. topspace X \<subseteq> {a})"
+  shows "\<not> countable(topspace X)"
+proof
+  assume coX: "countable (topspace X)"
+  with \<open>regular_space X\<close> have "normal_space X"
+    using countable_imp_Lindelof_space regular_Lindelof_imp_normal_space by blast
+  then have "(UNIV::real set) \<lesssim> topspace X"
+    by (simp add: Hausdorff_imp_t1_space assms connected_space_imp_card_ge)
+  with coX show False
+    using countable_lepoll uncountable_UNIV_real by blast
+qed
+
+lemma path_connected_space_imp_uncountable:
+  assumes "path_connected_space X" "t1_space X" and nosing: "\<not> (\<exists>a. topspace X \<subseteq> {a})"
+  shows "\<not> countable(topspace X)"
+proof 
+  assume coX: "countable (topspace X)"
+  obtain a b where "a \<in> topspace X" "b \<in> topspace X" "a \<noteq> b"
+    by (metis nosing singletonI subset_iff)
+  then obtain \<gamma> where "pathin X \<gamma>" "\<gamma> 0 = a" "\<gamma> 1 = b"
+    by (meson \<open>a \<in> topspace X\<close> \<open>b \<in> topspace X\<close> \<open>path_connected_space X\<close> path_connected_space_def)
+  then have "\<gamma> ` {0..1} \<lesssim> topspace X"
+    by (meson path_image_subset_topspace subset_imp_lepoll image_subset_iff_funcset)
+  define \<A> where "\<A> \<equiv> ((\<lambda>a. {x \<in> {0..1}. \<gamma> x \<in> {a}}) ` topspace X) - {{}}"
+  have \<A>01: "\<A> = {{0..1}}"
+  proof (rule real_Sierpinski_lemma)
+    show "countable \<A>"
+      using \<A>_def coX by blast
+    show "disjoint \<A>"
+      by (auto simp: \<A>_def disjnt_iff pairwise_def)
+    show "\<Union>\<A> = {0..1}"
+      using \<open>pathin X \<gamma>\<close> path_image_subset_topspace by (fastforce simp: \<A>_def Bex_def)
+    fix C
+    assume "C \<in> \<A>"
+    then obtain a where "a \<in> topspace X" and C: "C = {x \<in> {0..1}. \<gamma> x \<in> {a}}" "C \<noteq> {}"
+      by (auto simp: \<A>_def)
+    then have "closedin X {a}"
+      by (meson \<open>t1_space X\<close> closedin_t1_singleton)
+    then have "closedin (top_of_set {0..1}) C"
+      using C \<open>pathin X \<gamma>\<close> closedin_continuous_map_preimage pathin_def by fastforce
+    then show "closed C \<and> C \<noteq> {}"
+      using C closedin_closed_trans by blast
+  qed auto
+  then have "{0..1} \<in> \<A>"
+    by blast
+  then have "\<exists>a \<in> topspace X. {0..1} \<subseteq> {x. \<gamma> x = a}"
+    using \<A>_def image_iff by auto
+  then show False
+    using \<open>\<gamma> 0 = a\<close> \<open>\<gamma> 1 = b\<close> \<open>a \<noteq> b\<close> atLeastAtMost_iff zero_less_one_class.zero_le_one by blast
+qed
+
+
+subsection\<open>Lavrentiev extension etc\<close>
+
+lemma (in Metric_space) convergent_eq_zero_oscillation_gen:
+  assumes "mcomplete" and fim: "f \<in> (topspace X \<inter> S) \<rightarrow> M"
+  shows "(\<exists>l. limitin mtopology f l (atin_within X a S)) \<longleftrightarrow>
+         M \<noteq> {} \<and>
+         (a \<in> topspace X
+            \<longrightarrow> (\<forall>\<epsilon>>0. \<exists>U. openin X U \<and> a \<in> U \<and>
+                           (\<forall>x \<in> (S \<inter> U) - {a}. \<forall>y \<in> (S \<inter> U) - {a}. d (f x) (f y) < \<epsilon>)))"
+proof (cases "M = {}")
+  case True
+  with limitin_mspace show ?thesis
+    by blast
+next
+  case False
+  show ?thesis
+  proof (cases "a \<in> topspace X")
+    case True
+    let ?R = "\<forall>\<epsilon>>0. \<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x\<in>S \<inter> U - {a}. \<forall>y\<in>S \<inter> U - {a}. d (f x) (f y) < \<epsilon>)"
+    show ?thesis
+    proof (cases "a \<in> X derived_set_of S")
+      case True
+      have ?R
+        if "limitin mtopology f l (atin_within X a S)" for l
+      proof (intro strip)
+        fix \<epsilon>::real
+        assume "\<epsilon>>0"
+        with that \<open>a \<in> topspace X\<close> 
+        obtain U where U: "openin X U" "a \<in> U" "l \<in> M"
+          and Uless: "\<forall>x\<in>U - {a}. x \<in> S \<longrightarrow> f x \<in> M \<and> d (f x) l < \<epsilon>/2"
+          unfolding limitin_metric eventually_within_imp eventually_atin
+          using half_gt_zero by blast
+        show "\<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x\<in>S \<inter> U - {a}. \<forall>y\<in>S \<inter> U - {a}. d (f x) (f y) < \<epsilon>)"
+        proof (intro exI strip conjI)
+          fix x y
+          assume x: "x \<in> S \<inter> U - {a}" and y: "y \<in> S \<inter> U - {a}"
+          then have "d (f x) l < \<epsilon>/2" "d (f y) l < \<epsilon>/2" "f x \<in> M" "f y \<in> M"
+            using Uless by auto
+          then show "d (f x) (f y) < \<epsilon>"
+            using triangle' \<open>l \<in> M\<close> by fastforce
+        qed (auto simp add: U)
+      qed
+      moreover have "\<exists>l. limitin mtopology f l (atin_within X a S)" 
+        if R [rule_format]: ?R
+      proof -
+        define F where "F \<equiv> \<lambda>U. mtopology closure_of f ` (S \<inter> U - {a})"
+        define \<C> where "\<C> \<equiv> F ` {U. openin X U \<and> a \<in> U}"
+        have \<C>_clo: "\<forall>C \<in> \<C>. closedin mtopology C"
+          by (force simp add: \<C>_def F_def)
+        moreover have sub_mcball: "\<exists>C a. C \<in> \<C> \<and> C \<subseteq> mcball a \<epsilon>" if "\<epsilon>>0" for \<epsilon>
+        proof -
+          obtain U where U: "openin X U" "a \<in> U" 
+            and Uless: "\<forall>x\<in>S \<inter> U - {a}. \<forall>y\<in>S \<inter> U - {a}. d (f x) (f y) < \<epsilon>"
+            using R [OF \<open>\<epsilon>>0\<close>] by blast
+          then obtain b where b: "b \<noteq> a" "b \<in> S" "b \<in> U"
+            using True by (auto simp add: in_derived_set_of)
+          have "U \<subseteq> topspace X"
+            by (simp add: U(1) openin_subset)
+          have "f b \<in> M"
+            using b \<open>openin X U\<close> by (metis image_subset_iff_funcset Int_iff fim image_eqI openin_subset subsetD)
+          moreover
+          have "mtopology closure_of f ` ((S \<inter> U) - {a}) \<subseteq> mcball (f b) \<epsilon>"
+          proof (rule closure_of_minimal)
+            have "f y \<in> M" if "y \<in> S" and "y \<in> U" for y
+              using \<open>U \<subseteq> topspace X\<close> fim that by (auto simp: Pi_iff)
+            moreover
+            have "d (f b) (f y) \<le> \<epsilon>" if "y \<in> S" "y \<in> U" "y \<noteq> a" for y
+              using that Uless b by force
+            ultimately show "f ` (S \<inter> U - {a}) \<subseteq> mcball (f b) \<epsilon>"
+              by (force simp: \<open>f b \<in> M\<close>)
+          qed auto
+          ultimately show ?thesis
+            using U by (auto simp add: \<C>_def F_def)
+        qed
+        moreover have "\<Inter>\<F> \<noteq> {}" if "finite \<F>" "\<F> \<subseteq> \<C>" for \<F>
+        proof -
+          obtain \<G> where sub: "\<G> \<subseteq> {U. openin X U \<and> a \<in> U}" and eq: "\<F> = F ` \<G>" and "finite \<G>"
+            by (metis (no_types, lifting) \<C>_def \<open>\<F> \<subseteq> \<C>\<close> \<open>finite \<F>\<close> finite_subset_image)
+          then have "U \<subseteq> topspace X" if "U \<in> \<G>" for U
+            using openin_subset that by auto
+          then have "T \<subseteq> mtopology closure_of T" 
+            if "T \<in> (\<lambda>U. f ` (S \<inter> U - {a})) ` \<G>" for T
+            using that fim by (fastforce simp add: intro!: closure_of_subset)
+          moreover
+          have ain: "a \<in> \<Inter> (insert (topspace X) \<G>)" "openin X (\<Inter> (insert (topspace X) \<G>))"
+            using True in_derived_set_of sub \<open>finite \<G>\<close> by (fastforce intro!: openin_Inter)+
+          then obtain y where "y \<noteq> a" "y \<in> S" and y: "y \<in> \<Inter> (insert (topspace X) \<G>)"
+            by (meson \<open>a \<in> X derived_set_of S\<close> sub in_derived_set_of) 
+          then have "f y \<in> \<Inter>\<F>"
+            using eq that ain fim by (auto simp add: F_def image_subset_iff in_closure_of)
+          then show ?thesis by blast
+        qed
+        ultimately have "\<Inter>\<C> \<noteq> {}"
+          using \<open>mcomplete\<close> mcomplete_fip by metis
+        then obtain b where "b \<in> \<Inter>\<C>"
+          by auto
+        then have "b \<in> M"
+          using sub_mcball \<C>_clo mbounded_alt_pos mbounded_empty metric_closedin_iff_sequentially_closed by force
+        have "limitin mtopology f b (atin_within X a S)"
+        proof (clarsimp simp: limitin_metric \<open>b \<in> M\<close>)
+          fix \<epsilon> :: real
+          assume "\<epsilon> > 0"
+          then obtain U where U: "openin X U" "a \<in> U" and subU: "U \<subseteq> topspace X"
+            and Uless: "\<forall>x\<in>S \<inter> U - {a}. \<forall>y\<in>S \<inter> U - {a}. d (f x) (f y) < \<epsilon>/2"
+            by (metis R half_gt_zero openin_subset) 
+          then obtain x where x: "x \<in> S" "x \<in> U" "x \<noteq> a" and fx: "f x \<in> mball b (\<epsilon>/2)"
+            using \<open>b \<in> \<Inter>\<C>\<close> 
+            apply (simp add: \<C>_def F_def closure_of_def del: divide_const_simps)
+            by (metis Diff_iff Int_iff centre_in_mball_iff in_mball openin_mball singletonI zero_less_numeral)
+          moreover
+          have "d (f y) b < \<epsilon>" if "y \<in> U" "y \<noteq> a" "y \<in> S" for y
+          proof -
+            have "d (f x) (f y) < \<epsilon>/2"
+              using Uless that x by force
+            moreover have "d b (f x)  < \<epsilon>/2"
+              using fx by simp
+            ultimately show ?thesis
+              using triangle [of b "f x" "f y"] subU that \<open>b \<in> M\<close> commute fim fx by fastforce
+          qed
+          ultimately show "\<forall>\<^sub>F x in atin_within X a S. f x \<in> M \<and> d (f x) b < \<epsilon>"
+            using fim U
+            apply (simp add: eventually_atin eventually_within_imp del: divide_const_simps flip: image_subset_iff_funcset)
+            by (smt (verit, del_insts) Diff_iff Int_iff imageI insertI1 openin_subset subsetD)
+        qed
+        then show ?thesis ..
+      qed
+      ultimately
+      show ?thesis
+        by (meson True \<open>M \<noteq> {}\<close> in_derived_set_of)
+    next
+      case False
+      have "(\<exists>l. limitin mtopology f l (atin_within X a S))"
+        by (metis \<open>M \<noteq> {}\<close> False derived_set_of_trivial_limit equals0I limitin_trivial topspace_mtopology)
+      moreover have "\<forall>e>0. \<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x\<in>S \<inter> U - {a}. \<forall>y\<in>S \<inter> U - {a}. d (f x) (f y) < e)"
+        by (metis Diff_iff False IntE True in_derived_set_of insert_iff)
+      ultimately show ?thesis
+        using limitin_mspace by blast
+    qed
+  next
+    case False
+    then show ?thesis
+      by (metis derived_set_of_trivial_limit ex_in_conv in_derived_set_of limitin_mspace limitin_trivial topspace_mtopology)
+  qed
+qed
+
+text \<open>The HOL Light proof uses some ugly tricks to share common parts of what are two separate proofs for the two cases\<close>
+lemma (in Metric_space) gdelta_in_points_of_convergence_within:
+  assumes "mcomplete"
+    and f: "continuous_map (subtopology X S) mtopology f \<or> t1_space X \<and> f \<in> S \<rightarrow> M"
+  shows "gdelta_in X {x \<in> topspace X. \<exists>l. limitin mtopology f l (atin_within X x S)}"
+proof -
+  have fim: "f \<in> (topspace X \<inter> S) \<rightarrow> M"
+    using continuous_map_image_subset_topspace f by force
+  show ?thesis
+  proof (cases "M={}")
+    case True
+    then show ?thesis
+      by (smt (verit) Collect_cong empty_def empty_iff gdelta_in_empty limitin_mspace)
+  next
+    case False
+    define A where "A \<equiv> {a \<in> topspace X. \<forall>\<epsilon>>0. \<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x\<in>S \<inter> U - {a}. \<forall>y\<in>S \<inter> U - {a}. d (f x) (f y) < \<epsilon>)}"
+    have "gdelta_in X A"
+      using f 
+    proof (elim disjE conjE)
+      assume cm: "continuous_map (subtopology X S) mtopology f"
+      define C where "C \<equiv> \<lambda>r. \<Union>{U. openin X U \<and> (\<forall>x \<in> S\<inter>U. \<forall>y \<in> S\<inter>U. d (f x) (f y) < r)}"
+      define B where "B \<equiv> (\<Inter>n. C(inverse(Suc n)))"
+      define D where "D \<equiv> (\<Inter> (C ` {0<..}))"
+      have "D=B"
+        unfolding B_def C_def D_def
+        apply (intro Inter_eq_Inter_inverse_Suc Sup_subset_mono)
+        by (smt (verit, ccfv_threshold) Collect_mono_iff)
+      have "B \<subseteq> topspace X"
+        using openin_subset by (force simp add: B_def C_def)
+      have "(countable intersection_of openin X) B"
+        unfolding B_def C_def 
+        by (intro relative_to_inc countable_intersection_of_Inter countable_intersection_of_inc) auto
+      then have "gdelta_in X B"
+        unfolding gdelta_in_def by (intro relative_to_subset_inc \<open>B \<subseteq> topspace X\<close>)
+      moreover have "A=D"
+      proof (intro equalityI subsetI)
+        fix a
+        assume x: "a \<in> A"
+        then have "a \<in> topspace X"
+          using A_def by blast
+        show "a \<in> D"
+        proof (clarsimp simp: D_def C_def \<open>a \<in> topspace X\<close>)
+          fix \<epsilon>::real assume "\<epsilon> > 0"
+          then obtain U where "openin X U" "a \<in> U" and U: "(\<forall>x\<in>S \<inter> U - {a}. \<forall>y\<in>S \<inter> U - {a}. d (f x) (f y) < \<epsilon>)"
+            using x by (force simp: A_def)
+          show "\<exists>T. openin X T \<and> (\<forall>x\<in>S \<inter> T. \<forall>y\<in>S \<inter> T. d (f x) (f y) < \<epsilon>) \<and> a \<in> T"
+          proof (cases "a \<in> S")
+            case True
+            then obtain V where "openin X V" "a \<in> V" and V: "\<forall>x. x \<in> S \<and> x \<in> V \<longrightarrow> f a \<in> M \<and> f x \<in> M \<and> d (f a) (f x) < \<epsilon>"
+              using \<open>a \<in> topspace X\<close> \<open>\<epsilon> > 0\<close> cm
+              by (force simp add: continuous_map_to_metric openin_subtopology_alt Ball_def)
+            show ?thesis
+            proof (intro exI conjI strip)
+              show "openin X (U \<inter> V)"
+                using \<open>openin X U\<close> \<open>openin X V\<close> by blast 
+              show "a \<in> U \<inter> V"
+                using \<open>a \<in> U\<close> \<open>a \<in> V\<close> by blast
+              show "\<And>x y. \<lbrakk>x \<in> S \<inter> (U \<inter> V); y \<in> S \<inter> (U \<inter> V)\<rbrakk> \<Longrightarrow> d (f x) (f y) < \<epsilon>"
+                by (metis DiffI Int_iff U V commute singletonD)
+            qed
+          next
+            case False then show ?thesis
+              using U \<open>a \<in> U\<close> \<open>openin X U\<close> by auto
+          qed
+        qed
+      next
+        fix x
+        assume x: "x \<in> D"
+        then have "x \<in> topspace X"
+          using \<open>B \<subseteq> topspace X\<close> \<open>D=B\<close> by blast
+        with x show "x \<in> A"
+          apply (clarsimp simp: D_def C_def A_def)
+          by (meson DiffD1 greaterThan_iff)
+      qed
+      ultimately show ?thesis
+        by (simp add: \<open>D=B\<close>)
+    next
+      assume "t1_space X" "f \<in> S \<rightarrow> M"
+      define C where "C \<equiv> \<lambda>r. \<Union>{U. openin X U \<and> 
+                           (\<exists>b \<in> topspace X. \<forall>x \<in> S\<inter>U - {b}. \<forall>y \<in> S\<inter>U - {b}. d (f x) (f y) < r)}"
+      define B where "B \<equiv> (\<Inter>n. C(inverse(Suc n)))"
+      define D where "D \<equiv> (\<Inter> (C ` {0<..}))"
+      have "D=B"
+        unfolding B_def C_def D_def
+        apply (intro Inter_eq_Inter_inverse_Suc Sup_subset_mono)
+        by (smt (verit, ccfv_threshold) Collect_mono_iff)
+      have "B \<subseteq> topspace X"
+        using openin_subset by (force simp add: B_def C_def)
+      have "(countable intersection_of openin X) B"
+        unfolding B_def C_def 
+        by (intro relative_to_inc countable_intersection_of_Inter countable_intersection_of_inc) auto
+      then have "gdelta_in X B"
+        unfolding gdelta_in_def by (intro relative_to_subset_inc \<open>B \<subseteq> topspace X\<close>)
+      moreover have "A=D"
+      proof (intro equalityI subsetI)
+        fix x
+        assume x: "x \<in> D"
+        then have "x \<in> topspace X"
+          using \<open>B \<subseteq> topspace X\<close> \<open>D=B\<close> by blast
+        show "x \<in> A"
+        proof (clarsimp simp: A_def \<open>x \<in> topspace X\<close>)
+          fix \<epsilon> :: real
+          assume "\<epsilon>>0"
+          then obtain U b where "openin X U" "b \<in> topspace X"
+                  and U: "\<forall>x\<in>S \<inter> U - {b}. \<forall>y\<in>S \<inter> U - {b}. d (f x) (f y) < \<epsilon>" and "x \<in> U"
+            using x by (auto simp: D_def C_def A_def Ball_def)
+          then have "openin X (U-{b})"
+            by (meson \<open>t1_space X\<close> t1_space_openin_delete_alt)
+          then show "\<exists>U. openin X U \<and> x \<in> U \<and> (\<forall>xa\<in>S \<inter> U - {x}. \<forall>y\<in>S \<inter> U - {x}. d (f xa) (f y) < \<epsilon>)"
+            using U \<open>openin X U\<close> \<open>x \<in> U\<close> by auto
+        qed
+      next
+        show "\<And>x. x \<in> A \<Longrightarrow> x \<in> D"
+          unfolding A_def D_def C_def
+          by clarsimp meson
+      qed
+      ultimately show ?thesis
+        by (simp add: \<open>D=B\<close>)
+    qed
+    then show ?thesis
+      by (simp add: A_def convergent_eq_zero_oscillation_gen False fim \<open>mcomplete\<close> cong: conj_cong)
+  qed
+qed
+
+
+lemma gdelta_in_points_of_convergence_within:
+  assumes Y: "completely_metrizable_space Y"
+    and f: "continuous_map (subtopology X S) Y f \<or> t1_space X \<and> f \<in> S \<rightarrow> topspace Y"
+  shows "gdelta_in X {x \<in> topspace X. \<exists>l. limitin Y f l (atin_within X x S)}"
+  using assms
+  unfolding completely_metrizable_space_def
+  using Metric_space.gdelta_in_points_of_convergence_within Metric_space.topspace_mtopology by fastforce
+
+
+lemma Lavrentiev_extension_gen:
+  assumes "S \<subseteq> topspace X" and Y: "completely_metrizable_space Y" 
+    and contf: "continuous_map (subtopology X S) Y f"
+  obtains U g where "gdelta_in X U" "S \<subseteq> U" 
+            "continuous_map (subtopology X (X closure_of S \<inter> U)) Y g" 
+             "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+proof -
+  define U where "U \<equiv> {x \<in> topspace X. \<exists>l. limitin Y f l (atin_within X x S)}"
+  have "S \<subseteq> U"
+    using that contf limit_continuous_map_within subsetD [OF \<open>S \<subseteq> topspace X\<close>] 
+    by (fastforce simp: U_def)
+  then have "S \<subseteq> X closure_of S \<inter> U"
+    by (simp add: \<open>S \<subseteq> topspace X\<close> closure_of_subset)
+  moreover
+  have "\<And>t. t \<in> X closure_of S \<inter> U - S \<Longrightarrow> \<exists>l. limitin Y f l (atin_within X t S)"
+    using U_def by blast
+  moreover have "regular_space Y"
+    by (simp add: Y completely_metrizable_imp_metrizable_space metrizable_imp_regular_space)
+  ultimately
+  obtain g where g: "continuous_map (subtopology X (X closure_of S \<inter> U)) Y g" 
+    and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+    using continuous_map_extension_pointwise_alt assms by blast 
+  show thesis
+  proof
+    show "gdelta_in X U"
+      by (simp add: U_def Y contf gdelta_in_points_of_convergence_within)
+    show "continuous_map (subtopology X (X closure_of S \<inter> U)) Y g"
+      by (simp add: g)
+  qed (use \<open>S \<subseteq> U\<close> gf in auto)
+qed
+
+lemma Lavrentiev_extension:
+  assumes "S \<subseteq> topspace X" 
+    and X: "metrizable_space X \<or> topspace X \<subseteq> X closure_of S" 
+    and Y: "completely_metrizable_space Y" 
+    and contf: "continuous_map (subtopology X S) Y f"
+  obtains U g where "gdelta_in X U" "S \<subseteq> U" "U \<subseteq> X closure_of S"
+            "continuous_map (subtopology X U) Y g"  "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+proof -
+  obtain U g where "gdelta_in X U" "S \<subseteq> U" 
+    and contg: "continuous_map (subtopology X (X closure_of S \<inter> U)) Y g" 
+    and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+    using Lavrentiev_extension_gen Y assms(1) contf by blast
+  define V where "V \<equiv> X closure_of S \<inter> U"
+  show thesis
+  proof
+    show "gdelta_in X V"
+      by (metis V_def X \<open>gdelta_in X U\<close> closed_imp_gdelta_in closedin_closure_of closure_of_subset_topspace gdelta_in_Int gdelta_in_topspace subset_antisym)
+    show "S \<subseteq> V"
+      by (simp add: V_def \<open>S \<subseteq> U\<close> assms(1) closure_of_subset)
+    show "continuous_map (subtopology X V) Y g"
+      by (simp add: V_def contg)
+  qed (auto simp: gf V_def)
+qed
+
+subsection\<open>Embedding in products and hence more about completely metrizable spaces\<close>
+
+lemma (in Metric_space) gdelta_homeomorphic_space_closedin_product:
+  assumes S: "\<And>i. i \<in> I \<Longrightarrow> openin mtopology (S i)"
+  obtains T where "closedin (prod_topology mtopology (powertop_real I)) T"
+                  "subtopology mtopology (\<Inter>i \<in> I. S i) homeomorphic_space
+                   subtopology (prod_topology mtopology (powertop_real I)) T"
+proof (cases "I={}")
+  case True
+  then have top: "topspace (prod_topology mtopology (powertop_real I)) = (M \<times> {(\<lambda>x. undefined)})"
+    by simp
+  show ?thesis
+  proof
+    show "closedin (prod_topology mtopology (powertop_real I)) (M \<times> {(\<lambda>x. undefined)})"
+      by (metis top closedin_topspace)
+    have "subtopology mtopology (\<Inter>(S ` I)) homeomorphic_space mtopology"
+      by (simp add: True product_topology_empty_discrete)
+    also have "\<dots> homeomorphic_space (prod_topology mtopology (powertop_real {}))"
+      by (metis PiE_empty_domain homeomorphic_space_sym prod_topology_homeomorphic_space_left topspace_product_topology)
+    finally
+    show "subtopology mtopology (\<Inter>(S ` I)) homeomorphic_space subtopology (prod_topology mtopology (powertop_real I)) (M \<times> {(\<lambda>x. undefined)})"
+      by (smt (verit) True subtopology_topspace top)
+  qed   
+next
+  case False
+  have SM: "\<And>i. i \<in> I \<Longrightarrow> S i \<subseteq> M"
+    using assms openin_mtopology by blast
+  then have "(\<Inter>i \<in> I. S i) \<subseteq> M"
+    using False by blast
+  define dd where "dd \<equiv> \<lambda>i. if i\<notin>I \<or> S i = M then \<lambda>u. 1 else (\<lambda>u. INF x \<in> M - S i. d u x)"
+  have [simp]: "bdd_below (d u ` A)" for u A
+    by (meson bdd_belowI2 nonneg)
+  have cont_dd: "continuous_map (subtopology mtopology (S i)) euclidean (dd i)" if "i \<in> I" for i
+  proof -
+    have "dist (Inf (d x ` (M - S i))) (Inf (d y ` (M - S i))) \<le> d x y" 
+      if "x \<in> S i" "x \<in> M" "y \<in> S i" "y \<in> M" "S i \<noteq> M" for x y
+    proof -
+      have [simp]: "\<not> M \<subseteq> S i"
+        using SM \<open>S i \<noteq> M\<close> \<open>i \<in> I\<close> by auto
+      have "\<And>u. \<lbrakk>u \<in> M; u \<notin> S i\<rbrakk> \<Longrightarrow> Inf (d x ` (M - S i)) \<le> d x y + d y u"
+        apply (clarsimp simp add: cInf_le_iff_less)
+        by (smt (verit) DiffI triangle \<open>x \<in> M\<close> \<open>y \<in> M\<close>)
+      then have "Inf (d x ` (M - S i)) - d x y \<le> Inf (d y ` (M - S i))"
+        by (force simp add: le_cInf_iff)
+      moreover
+      have "\<And>u. \<lbrakk>u \<in> M; u \<notin> S i\<rbrakk> \<Longrightarrow> Inf (d y ` (M - S i)) \<le> d x u + d x y"
+        apply (clarsimp simp add: cInf_le_iff_less)
+        by (smt (verit) DiffI triangle'' \<open>x \<in> M\<close> \<open>y \<in> M\<close>)
+      then have "Inf (d y ` (M - S i)) - d x y \<le> Inf (d x ` (M - S i))"
+        by (force simp add: le_cInf_iff)
+      ultimately show ?thesis
+        by (simp add: dist_real_def abs_le_iff)
+    qed
+    then have *: "Lipschitz_continuous_map (submetric Self (S i)) euclidean_metric (\<lambda>u. Inf (d u ` (M - S i)))"
+      unfolding Lipschitz_continuous_map_def by (force intro!: exI [where x=1])
+    then show ?thesis
+      using Lipschitz_continuous_imp_continuous_map [OF *]
+      by (simp add: dd_def Self_def mtopology_of_submetric )
+  qed 
+  have dd_pos: "0 < dd i x" if "x \<in> S i" for i x
+  proof (clarsimp simp add: dd_def)
+    assume "i \<in> I" and "S i \<noteq> M"
+    have opeS: "openin mtopology (S i)"
+      by (simp add: \<open>i \<in> I\<close> assms)
+    then obtain r where "r>0" and r: "\<And>y. \<lbrakk>y \<in> M; d x y < r\<rbrakk> \<Longrightarrow> y \<in> S i"
+      by (meson \<open>x \<in> S i\<close> in_mball openin_mtopology subsetD)
+    then have "\<And>y. y \<in> M - S i \<Longrightarrow> d x y \<ge> r"
+      by (meson Diff_iff linorder_not_le)
+    then have "Inf (d x ` (M - S i)) \<ge> r"
+      by (meson Diff_eq_empty_iff SM \<open>S i \<noteq> M\<close> \<open>i \<in> I\<close> cINF_greatest set_eq_subset)
+    with \<open>r>0\<close> show "0 < Inf (d x ` (M - S i))" by simp
+  qed
+  define f where "f \<equiv> \<lambda>x. (x, \<lambda>i\<in>I. inverse(dd i x))"
+  define T where "T \<equiv> f ` (\<Inter>i \<in> I. S i)"
+  show ?thesis
+  proof
+    show "closedin (prod_topology mtopology (powertop_real I)) T"
+      unfolding closure_of_subset_eq [symmetric]
+    proof
+      show "T \<subseteq> topspace (prod_topology mtopology (powertop_real I))"
+        using False SM by (auto simp: T_def f_def)
+
+      have "(x,ds) \<in> T"
+        if \<section>: "\<And>U. \<lbrakk>(x, ds) \<in> U; openin (prod_topology mtopology (powertop_real I)) U\<rbrakk> \<Longrightarrow> \<exists>y\<in>T. y \<in> U"
+          and "x \<in> M" and ds: "ds \<in> I \<rightarrow>\<^sub>E UNIV" for x ds
+      proof -
+        have ope: "\<exists>x. x \<in> \<Inter>(S ` I) \<and> f x \<in> U \<times> V"
+          if "x \<in> U" and "ds \<in> V" and "openin mtopology U" and "openin (powertop_real I) V" for U V
+          using \<section> [of "U\<times>V"] that by (force simp add: T_def openin_prod_Times_iff)
+        have x_in_INT: "x \<in> \<Inter>(S ` I)"
+        proof clarify
+          fix i
+          assume "i \<in> I"
+          show "x \<in> S i"
+          proof (rule ccontr)
+            assume "x \<notin> S i"
+            have "openin (powertop_real I) {z \<in> topspace (powertop_real I). z i \<in> {ds i - 1 <..< ds i + 1}}"
+            proof (rule openin_continuous_map_preimage)
+              show "continuous_map (powertop_real I) euclidean (\<lambda>x. x i)"
+                by (metis \<open>i \<in> I\<close> continuous_map_product_projection)
+            qed auto
+            then obtain y where "y \<in> S i" "y \<in> M" and dxy: "d x y < inverse (\<bar>ds i\<bar> + 1)"
+                          and intvl: "inverse (dd i y) \<in> {ds i - 1 <..< ds i + 1}"
+              using ope [of "mball x (inverse(abs(ds i) + 1))" "{z \<in> topspace(powertop_real I). z i \<in> {ds i - 1<..<ds i + 1}}"]
+                    \<open>x \<in> M\<close> \<open>ds \<in> I \<rightarrow>\<^sub>E UNIV\<close> \<open>i \<in> I\<close>
+              by (fastforce simp add: f_def)
+            have "\<not> M \<subseteq> S i"
+              using \<open>x \<notin> S i\<close> \<open>x \<in> M\<close> by blast
+            have "inverse (\<bar>ds i\<bar> + 1) \<le> dd i y"
+              using intvl \<open>y \<in> S i\<close> dd_pos [of y i]
+              by (smt (verit, ccfv_threshold) greaterThanLessThan_iff inverse_inverse_eq le_imp_inverse_le)
+            also have "\<dots> \<le> d x y"
+              using \<open>i \<in> I\<close> \<open>\<not> M \<subseteq> S i\<close> \<open>x \<notin> S i\<close> \<open>x \<in> M\<close>
+              apply (simp add: dd_def cInf_le_iff_less)
+              using commute by force
+            finally show False
+              using dxy by linarith
+          qed
+        qed
+        moreover have "ds = (\<lambda>i\<in>I. inverse (dd i x))"
+        proof (rule PiE_ext [OF ds])
+          fix i
+          assume "i \<in> I"
+          define e where "e \<equiv> \<bar>ds i - inverse (dd i x)\<bar>"
+          { assume con: "e > 0"
+            have "continuous_map (subtopology mtopology (S i)) euclidean (\<lambda>x. inverse (dd i x))" 
+              using dd_pos cont_dd \<open>i \<in> I\<close> 
+              by (fastforce simp:  intro!: continuous_map_real_inverse)
+             then have "openin (subtopology mtopology (S i))
+                         {z \<in> topspace (subtopology mtopology (S i)). 
+                          inverse (dd i z) \<in> {inverse(dd i x) - e/2<..<inverse(dd i x) + e/2}}"
+               using openin_continuous_map_preimage open_greaterThanLessThan open_openin by blast
+             then obtain U where "openin mtopology U"
+                  and U: "{z \<in> S i. inverse (dd i x) - e/2 < inverse (dd i z) \<and>
+                           inverse (dd i z) < inverse (dd i x) + e/2}
+                         = U \<inter> S i"
+               using SM \<open>i \<in> I\<close>  by (auto simp: openin_subtopology)
+             have "x \<in> U"
+               using U x_in_INT \<open>i \<in> I\<close> con by fastforce
+             have "ds \<in> {z \<in> topspace (powertop_real I). z i \<in> {ds i - e / 2<..<ds i + e/2}}"
+               by (simp add: con ds)
+             moreover
+             have  "openin (powertop_real I) {z \<in> topspace (powertop_real I). z i \<in> {ds i - e / 2<..<ds i + e/2}}"
+             proof (rule openin_continuous_map_preimage)
+               show "continuous_map (powertop_real I) euclidean (\<lambda>x. x i)"
+                 by (metis \<open>i \<in> I\<close> continuous_map_product_projection)
+             qed auto
+             ultimately obtain y where "y \<in> \<Inter>(S ` I) \<and> f y \<in> U \<times> {z \<in> topspace (powertop_real I). z i \<in> {ds i - e / 2<..<ds i + e/2}}"
+               using ope \<open>x \<in> U\<close> \<open>openin mtopology U\<close> \<open>x \<in> U\<close>
+               by presburger 
+             with \<open>i \<in> I\<close> U 
+             have False unfolding set_eq_iff f_def e_def by simp (smt (verit) field_sum_of_halves)
+          }
+          then show "ds i = (\<lambda>i\<in>I. inverse (dd i x)) i"
+            using \<open>i \<in> I\<close> by (force simp: e_def)
+        qed auto
+        ultimately show ?thesis
+          by (auto simp: T_def f_def)
+      qed
+      then show "prod_topology mtopology (powertop_real I) closure_of T \<subseteq> T"
+        by (auto simp: closure_of_def)
+    qed
+    have eq: "(\<Inter>(S ` I) \<times> (I \<rightarrow>\<^sub>E UNIV) \<inter> f ` (M \<inter> \<Inter>(S ` I))) = (f ` \<Inter>(S ` I))"
+      using False SM by (force simp: f_def image_iff)
+    have "continuous_map (subtopology mtopology (\<Inter>(S ` I))) euclidean (dd i)" if "i \<in> I" for i
+      by (meson INT_lower cont_dd continuous_map_from_subtopology_mono that)
+    then have "continuous_map (subtopology mtopology (\<Inter>(S ` I))) (powertop_real I) (\<lambda>x. \<lambda>i\<in>I. inverse (dd i x))"
+      using dd_pos by (fastforce simp: continuous_map_componentwise intro!: continuous_map_real_inverse)
+    then have "embedding_map (subtopology mtopology (\<Inter>(S ` I))) (prod_topology (subtopology mtopology (\<Inter>(S ` I))) (powertop_real I)) f"
+      by (simp add: embedding_map_graph f_def)
+    moreover have "subtopology (prod_topology (subtopology mtopology (\<Inter>(S ` I))) (powertop_real I))
+                     (f ` topspace (subtopology mtopology (\<Inter>(S ` I)))) =
+                   subtopology (prod_topology mtopology (powertop_real I)) T"
+      by (simp add: prod_topology_subtopology subtopology_subtopology T_def eq)
+    ultimately
+    show "subtopology mtopology (\<Inter>(S ` I)) homeomorphic_space subtopology (prod_topology mtopology (powertop_real I)) T"
+      by (metis embedding_map_imp_homeomorphic_space)
+  qed
+qed
+
+
+lemma gdelta_homeomorphic_space_closedin_product:
+  assumes "metrizable_space X" and "\<And>i. i \<in> I \<Longrightarrow> openin X (S i)"
+  obtains T where "closedin (prod_topology X (powertop_real I)) T"
+                  "subtopology X (\<Inter>i \<in> I. S i) homeomorphic_space
+                   subtopology (prod_topology X (powertop_real I)) T"
+  using Metric_space.gdelta_homeomorphic_space_closedin_product
+  by (metis assms metrizable_space_def)
+
+lemma open_homeomorphic_space_closedin_product:
+  assumes "metrizable_space X" and "openin X S"
+  obtains T where "closedin (prod_topology X euclideanreal) T"
+    "subtopology X S homeomorphic_space
+                   subtopology (prod_topology X euclideanreal) T"
+proof -
+  obtain T where cloT: "closedin (prod_topology X (powertop_real {()})) T"
+    and homT: "subtopology X S homeomorphic_space
+                   subtopology (prod_topology X (powertop_real {()})) T"
+    using gdelta_homeomorphic_space_closedin_product [of X "{()}" "\<lambda>i. S"] assms
+    by auto
+  have "prod_topology X (powertop_real {()}) homeomorphic_space prod_topology X euclideanreal"
+    by (meson homeomorphic_space_prod_topology homeomorphic_space_refl homeomorphic_space_singleton_product)
+  then obtain f where f: "homeomorphic_map (prod_topology X (powertop_real {()})) (prod_topology X euclideanreal) f"
+    unfolding homeomorphic_space by metis
+  show thesis
+  proof
+    show "closedin (prod_topology X euclideanreal) (f ` T)"
+      using cloT f homeomorphic_map_closedness_eq by blast
+    moreover have "T = topspace (subtopology (prod_topology X (powertop_real {()})) T)"
+      by (metis cloT closedin_subset topspace_subtopology_subset)
+    ultimately show "subtopology X S homeomorphic_space subtopology (prod_topology X euclideanreal) (f ` T)"
+      by (smt (verit, best) closedin_subset f homT homeomorphic_map_subtopologies homeomorphic_space 
+          homeomorphic_space_trans topspace_subtopology topspace_subtopology_subset)
+  qed
+qed
+
+lemma completely_metrizable_space_gdelta_in_alt:
+  assumes X: "completely_metrizable_space X" 
+    and S: "(countable intersection_of openin X) S"
+  shows "completely_metrizable_space (subtopology X S)"
+proof -
+  obtain \<U> where "countable \<U>" "S = \<Inter>\<U>" and ope: "\<And>U. U \<in> \<U> \<Longrightarrow> openin X U"
+    using S by (force simp add: intersection_of_def)
+  then have \<U>: "completely_metrizable_space (powertop_real \<U>)"
+    by (simp add: completely_metrizable_space_euclidean completely_metrizable_space_product_topology)
+  obtain C where "closedin (prod_topology X (powertop_real \<U>)) C"
+                and sub: "subtopology X (\<Inter>\<U>) homeomorphic_space
+                   subtopology (prod_topology X (powertop_real \<U>)) C"
+    by (metis gdelta_homeomorphic_space_closedin_product  X completely_metrizable_imp_metrizable_space ope INF_identity_eq)
+  moreover have "completely_metrizable_space (prod_topology X (powertop_real \<U>))"
+    by (simp add: completely_metrizable_space_prod_topology X \<U>)
+  ultimately have "completely_metrizable_space (subtopology (prod_topology X (powertop_real \<U>)) C)"
+    using completely_metrizable_space_closedin by blast
+  then show ?thesis
+    using \<open>S = \<Inter>\<U>\<close> sub homeomorphic_completely_metrizable_space by blast
+qed
+
+lemma completely_metrizable_space_gdelta_in:
+   "\<lbrakk>completely_metrizable_space X; gdelta_in X S\<rbrakk>
+        \<Longrightarrow> completely_metrizable_space (subtopology X S)"
+  by (simp add: completely_metrizable_space_gdelta_in_alt gdelta_in_alt)
+
+lemma completely_metrizable_space_openin:
+   "\<lbrakk>completely_metrizable_space X; openin X S\<rbrakk>
+        \<Longrightarrow> completely_metrizable_space (subtopology X S)"
+  by (simp add: completely_metrizable_space_gdelta_in open_imp_gdelta_in)
+
+
+lemma (in Metric_space) locally_compact_imp_completely_metrizable_space:
+  assumes "locally_compact_space mtopology"
+  shows "completely_metrizable_space mtopology"
+proof -
+  obtain f :: "['a,'a] \<Rightarrow> real" and m' where
+    "mcomplete_of m'" and fim: "f \<in> M \<rightarrow> mspace m'"
+    and clo: "mtopology_of m' closure_of f ` M = mspace m'"
+    and d: "\<And>x y. \<lbrakk>x \<in> M; y \<in> M\<rbrakk> \<Longrightarrow> mdist m' (f x) (f y) = d x y"
+    by (metis metric_completion)
+  then have "embedding_map mtopology (mtopology_of m') f"
+    unfolding mtopology_of_def
+    by (metis Metric_space12.isometry_imp_embedding_map Metric_space12_mspace_mdist mdist_metric mspace_metric)
+  then have hom: "mtopology homeomorphic_space subtopology (mtopology_of m') (f ` M)"
+    by (metis embedding_map_imp_homeomorphic_space topspace_mtopology)
+  have "locally_compact_space (subtopology (mtopology_of m') (f ` M))"
+    using assms hom homeomorphic_locally_compact_space by blast
+  moreover have "Hausdorff_space (mtopology_of m')"
+    by (simp add: Metric_space.Hausdorff_space_mtopology mtopology_of_def)
+  ultimately have "openin (mtopology_of m') (f ` M)"
+    by (simp add: clo dense_locally_compact_openin_Hausdorff_space fim image_subset_iff_funcset)
+  then
+  have "completely_metrizable_space (subtopology (mtopology_of m') (f ` M))"
+    using \<open>mcomplete_of m'\<close> unfolding mcomplete_of_def mtopology_of_def
+    by (metis Metric_space.completely_metrizable_space_mtopology Metric_space_mspace_mdist completely_metrizable_space_openin )
+  then show ?thesis
+    using hom homeomorphic_completely_metrizable_space by blast
+qed
+
+lemma locally_compact_imp_completely_metrizable_space:
+  assumes "metrizable_space X" and "locally_compact_space X"
+  shows "completely_metrizable_space X"
+  by (metis Metric_space.locally_compact_imp_completely_metrizable_space assms metrizable_space_def)
+
+
+lemma completely_metrizable_space_imp_gdelta_in:
+  assumes X: "metrizable_space X" and "S \<subseteq> topspace X" 
+    and XS: "completely_metrizable_space (subtopology X S)"
+  shows "gdelta_in X S"
+proof -
+  obtain U f where "gdelta_in X U" "S \<subseteq> U" and U: "U \<subseteq> X closure_of S"
+            and contf: "continuous_map (subtopology X U) (subtopology X S) f" 
+            and fid: "\<And>x. x \<in> S \<Longrightarrow> f x = x"
+    using Lavrentiev_extension[of S X "subtopology X S" id] assms by auto
+  then have "f ` topspace (subtopology X U) \<subseteq> topspace (subtopology X S)"
+    using continuous_map_image_subset_topspace by blast
+  then have "f`U \<subseteq> S"
+    by (metis \<open>gdelta_in X U\<close> \<open>S \<subseteq> topspace X\<close> gdelta_in_subset topspace_subtopology_subset)
+  moreover 
+  have "Hausdorff_space (subtopology X U)"
+    by (simp add: Hausdorff_space_subtopology X metrizable_imp_Hausdorff_space)
+  then have "\<And>x. x \<in> U \<Longrightarrow> f x = x"
+    using U fid contf forall_in_closure_of_eq [of _ "subtopology X U" S "subtopology X U" f id]
+    by (metis \<open>S \<subseteq> U\<close> closure_of_subtopology_open continuous_map_id continuous_map_in_subtopology id_apply inf.orderE subtopology_subtopology)
+  ultimately have "U \<subseteq> S"
+    by auto
+  then show ?thesis
+    using \<open>S \<subseteq> U\<close> \<open>gdelta_in X U\<close> by auto
+qed
+
+lemma completely_metrizable_space_eq_gdelta_in:
+   "\<lbrakk>completely_metrizable_space X; S \<subseteq> topspace X\<rbrakk>
+        \<Longrightarrow> completely_metrizable_space (subtopology X S) \<longleftrightarrow> gdelta_in X S"
+  using completely_metrizable_imp_metrizable_space completely_metrizable_space_gdelta_in completely_metrizable_space_imp_gdelta_in by blast
+
+lemma gdelta_in_eq_completely_metrizable_space:
+   "completely_metrizable_space X
+    \<Longrightarrow> gdelta_in X S \<longleftrightarrow> S \<subseteq> topspace X \<and> completely_metrizable_space (subtopology X S)"
+  by (metis completely_metrizable_space_eq_gdelta_in gdelta_in_alt)
+
 end
--- a/src/HOL/Library/Equipollence.thy	Wed Jul 05 14:33:32 2023 +0200
+++ b/src/HOL/Library/Equipollence.thy	Wed Jul 05 15:01:46 2023 +0200
@@ -18,6 +18,20 @@
 lemma lepoll_empty_iff_empty [simp]: "A \<lesssim> {} \<longleftrightarrow> A = {}"
   by (auto simp: lepoll_def)
 
+(*The HOL Light CARD_LE_RELATIONAL_FULL*)
+lemma lepoll_relational_full:
+  assumes "\<And>y. y \<in> B \<Longrightarrow> \<exists>x. x \<in> A \<and> R x y"
+    and "\<And>x y y'. \<lbrakk>x \<in> A; y \<in> B; y' \<in> B; R x y; R x y'\<rbrakk> \<Longrightarrow> y = y'"
+  shows "B \<lesssim> A"
+proof -
+  obtain f where f: "\<And>y. y \<in> B \<Longrightarrow> f y \<in> A \<and> R (f y) y"
+    using assms by metis
+  with assms have "inj_on f B"
+    by (metis inj_onI)
+  with f show ?thesis
+    unfolding lepoll_def by blast
+qed
+
 lemma eqpoll_iff_card_of_ordIso: "A \<approx> B \<longleftrightarrow> ordIso2 (card_of A) (card_of B)"
   by (simp add: card_of_ordIso eqpoll_def)
 
@@ -190,6 +204,18 @@
 lemma countable_lesspoll: "\<lbrakk>countable A; B \<prec> A\<rbrakk> \<Longrightarrow> countable B"
   using countable_lepoll lesspoll_def by blast
 
+lemma lepoll_iff_card_le: "\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> A \<lesssim> B \<longleftrightarrow> card A \<le> card B"
+  by (simp add: inj_on_iff_card_le lepoll_def)
+
+lemma lepoll_iff_finite_card: "A \<lesssim> {..<n::nat} \<longleftrightarrow> finite A \<and> card A \<le> n"
+  by (metis card_lessThan finite_lessThan finite_surj lepoll_iff lepoll_iff_card_le)
+
+lemma eqpoll_iff_finite_card: "A \<approx> {..<n::nat} \<longleftrightarrow> finite A \<and> card A = n"
+  by (metis card_lessThan eqpoll_finite_iff eqpoll_iff_card finite_lessThan)
+
+lemma lesspoll_iff_finite_card: "A \<prec> {..<n::nat} \<longleftrightarrow> finite A \<and> card A < n"
+  by (metis eqpoll_iff_finite_card lepoll_iff_finite_card lesspoll_def order_less_le)
+
 subsection\<open>Mapping by an injection\<close>
 
 lemma inj_on_image_eqpoll_self: "inj_on f A \<Longrightarrow> f ` A \<approx> A"
--- a/src/HOL/Library/Set_Idioms.thy	Wed Jul 05 14:33:32 2023 +0200
+++ b/src/HOL/Library/Set_Idioms.thy	Wed Jul 05 15:01:46 2023 +0200
@@ -340,12 +340,8 @@
   unfolding relative_to_def
   by (metis Diff_Diff_Int Diff_eq double_compl inf.absorb_iff2)
 
-lemma relative_to_subset:
-   "S \<subseteq> T \<and> P S \<Longrightarrow> (P relative_to T) S"
-  unfolding relative_to_def by auto
-
 lemma relative_to_subset_trans:
-   "(P relative_to U) S \<and> S \<subseteq> T \<and> T \<subseteq> U \<Longrightarrow> (P relative_to T) S"
+   "\<lbrakk>(P relative_to U) S; S \<subseteq> T; T \<subseteq> U\<rbrakk> \<Longrightarrow> (P relative_to T) S"
   unfolding relative_to_def by auto
 
 lemma relative_to_mono:
--- a/src/HOL/Real.thy	Wed Jul 05 14:33:32 2023 +0200
+++ b/src/HOL/Real.thy	Wed Jul 05 15:01:46 2023 +0200
@@ -1095,7 +1095,6 @@
   shows "x = 0"
   by (metis reals_Archimedean3 dual_order.order_iff_strict le0 le_less_trans not_le x0 xc)
 
-
 lemma inverse_Suc: "inverse (Suc n) > 0"
   using of_nat_0_less_iff positive_imp_inverse_positive zero_less_Suc by blast
 
@@ -1117,6 +1116,24 @@
     using order_le_less_trans by blast
 qed
 
+(*HOL Light's FORALL_POS_MONO_1_EQ*)
+text \<open>On the relationship between two different ways of converting to 0\<close> 
+lemma Inter_eq_Inter_inverse_Suc:
+  assumes "\<And>r' r. r' < r \<Longrightarrow> A r' \<subseteq> A r"
+  shows "\<Inter> (A ` {0<..}) = (\<Inter>n. A(inverse(Suc n)))"
+proof 
+  have "x \<in> A \<epsilon>"
+    if x: "\<forall>n. x \<in> A (inverse (Suc n))" and "\<epsilon>>0" for x and \<epsilon> :: real
+  proof -
+    obtain n where "inverse (Suc n) < \<epsilon>"
+      using \<open>\<epsilon>>0\<close> reals_Archimedean by blast
+    with assms x show ?thesis
+      by blast
+  qed
+  then show "(\<Inter>n. A(inverse(Suc n))) \<subseteq> (\<Inter>\<epsilon>\<in>{0<..}. A \<epsilon>)"
+    by auto    
+qed (use inverse_Suc in fastforce)
+
 subsection \<open>Rationals\<close>
 
 lemma Rats_abs_iff[simp]:
--- a/src/HOL/Transcendental.thy	Wed Jul 05 14:33:32 2023 +0200
+++ b/src/HOL/Transcendental.thy	Wed Jul 05 15:01:46 2023 +0200
@@ -2716,42 +2716,48 @@
 lemma floor_log_eq_powr_iff: "x > 0 \<Longrightarrow> b > 1 \<Longrightarrow> \<lfloor>log b x\<rfloor> = k \<longleftrightarrow> b powr k \<le> x \<and> x < b powr (k + 1)"
   by (auto simp: floor_eq_iff powr_le_iff less_powr_iff)
 
-lemma floor_log_nat_eq_powr_iff: fixes b n k :: nat
-  shows "\<lbrakk> b \<ge> 2; k > 0 \<rbrakk> \<Longrightarrow>
-  floor (log b (real k)) = n \<longleftrightarrow> b^n \<le> k \<and> k < b^(n+1)"
+lemma power_of_nat_log_ge: "b > 1 \<Longrightarrow> b ^ nat \<lceil>log b x\<rceil> \<ge> x"
+  by (smt (verit) less_log_of_power of_nat_ceiling)
+
+lemma floor_log_nat_eq_powr_iff: 
+  fixes b n k :: nat
+  shows "\<lbrakk> b \<ge> 2; k > 0 \<rbrakk> \<Longrightarrow> floor (log b (real k)) = n \<longleftrightarrow> b^n \<le> k \<and> k < b^(n+1)"
 by (auto simp: floor_log_eq_powr_iff powr_add powr_realpow
                of_nat_power[symmetric] of_nat_mult[symmetric] ac_simps
          simp del: of_nat_power of_nat_mult)
 
-lemma floor_log_nat_eq_if: fixes b n k :: nat
+lemma floor_log_nat_eq_if: 
+  fixes b n k :: nat
   assumes "b^n \<le> k" "k < b^(n+1)" "b \<ge> 2"
-  shows "floor (log b (real k)) = n"
-proof -
-  have "k \<ge> 1" using assms(1,3) one_le_power[of b n] by linarith
-  with assms show ?thesis by(simp add: floor_log_nat_eq_powr_iff)
-qed
-
-lemma ceiling_log_eq_powr_iff: "\<lbrakk> x > 0; b > 1 \<rbrakk>
-  \<Longrightarrow> \<lceil>log b x\<rceil> = int k + 1 \<longleftrightarrow> b powr k < x \<and> x \<le> b powr (k + 1)"
-by (auto simp: ceiling_eq_iff powr_less_iff le_powr_iff)
-
-lemma ceiling_log_nat_eq_powr_iff: fixes b n k :: nat
-  shows "\<lbrakk> b \<ge> 2; k > 0 \<rbrakk> \<Longrightarrow>
-  ceiling (log b (real k)) = int n + 1 \<longleftrightarrow> (b^n < k \<and> k \<le> b^(n+1))"
-using ceiling_log_eq_powr_iff
-by (auto simp: powr_add powr_realpow of_nat_power[symmetric] of_nat_mult[symmetric] ac_simps
-         simp del: of_nat_power of_nat_mult)
-
-lemma ceiling_log_nat_eq_if: fixes b n k :: nat
+  shows "floor (log b (real k)) = n" 
+proof -
+  have "k \<ge> 1"
+    using assms linorder_le_less_linear by force
+  with assms show ?thesis 
+    by(simp add: floor_log_nat_eq_powr_iff)
+qed
+
+lemma ceiling_log_eq_powr_iff: 
+  "\<lbrakk> x > 0; b > 1 \<rbrakk> \<Longrightarrow> \<lceil>log b x\<rceil> = int k + 1 \<longleftrightarrow> b powr k < x \<and> x \<le> b powr (k + 1)"
+  by (auto simp: ceiling_eq_iff powr_less_iff le_powr_iff)
+
+lemma ceiling_log_nat_eq_powr_iff: 
+  fixes b n k :: nat
+  shows "\<lbrakk> b \<ge> 2; k > 0 \<rbrakk> \<Longrightarrow> ceiling (log b (real k)) = int n + 1 \<longleftrightarrow> (b^n < k \<and> k \<le> b^(n+1))"
+  using ceiling_log_eq_powr_iff
+  by (auto simp: powr_add powr_realpow of_nat_power[symmetric] of_nat_mult[symmetric] ac_simps
+      simp del: of_nat_power of_nat_mult)
+
+lemma ceiling_log_nat_eq_if: 
+  fixes b n k :: nat
   assumes "b^n < k" "k \<le> b^(n+1)" "b \<ge> 2"
-  shows "ceiling (log b (real k)) = int n + 1"
-proof -
-  have "k \<ge> 1" using assms(1,3) one_le_power[of b n] by linarith
-  with assms show ?thesis by(simp add: ceiling_log_nat_eq_powr_iff)
-qed
-
-lemma floor_log2_div2: fixes n :: nat assumes "n \<ge> 2"
-shows "floor(log 2 n) = floor(log 2 (n div 2)) + 1"
+  shows "\<lceil>log (real b) (real k)\<rceil> = int n + 1"
+  using assms ceiling_log_nat_eq_powr_iff by force
+
+lemma floor_log2_div2: 
+  fixes n :: nat 
+  assumes "n \<ge> 2"
+  shows "\<lfloor>log 2 (real n)\<rfloor> = \<lfloor>log 2 (n div 2)\<rfloor> + 1"
 proof cases
   assume "n=2" thus ?thesis by simp
 next
@@ -2768,8 +2774,9 @@
   show ?thesis by simp
 qed
 
-lemma ceiling_log2_div2: assumes "n \<ge> 2"
-shows "ceiling(log 2 (real n)) = ceiling(log 2 ((n-1) div 2 + 1)) + 1"
+lemma ceiling_log2_div2: 
+  assumes "n \<ge> 2"
+  shows "ceiling(log 2 (real n)) = ceiling(log 2 ((n-1) div 2 + 1)) + 1"
 proof cases
   assume "n=2" thus ?thesis by simp
 next
@@ -2797,17 +2804,7 @@
 lemma powr_int:
   assumes "x > 0"
   shows "x powr i = (if i \<ge> 0 then x ^ nat i else 1 / x ^ nat (-i))"
-proof (cases "i < 0")
-  case True
-  have r: "x powr i = 1 / x powr (- i)"
-    by (simp add: powr_minus field_simps)
-  show ?thesis using \<open>i < 0\<close> \<open>x > 0\<close>
-    by (simp add: r field_simps powr_realpow[symmetric])
-next
-  case False
-  then show ?thesis
-    by (simp add: assms powr_realpow[symmetric])
-qed
+  by (simp add: assms inverse_eq_divide powr_real_of_int)
 
 definition powr_real :: "real \<Rightarrow> real \<Rightarrow> real"
   where [code_abbrev, simp]: "powr_real = Transcendental.powr"