# HG changeset patch
# User immler
# Date 1575344416 18000
# Node ID 3548d54ce3ee0973b63b58d7b1828eceea2cd488
# Parent  0aaf16a0f7cce99580c918f7a1988fe1940fe473
split off metric spaces part of Function_Topology: subsequent theories Product_Topology, T1_Spaces, Lindelof_Spaces are purely topological

diff -r 0aaf16a0f7cc -r 3548d54ce3ee src/HOL/Analysis/Abstract_Euclidean_Space.thy
--- a/src/HOL/Analysis/Abstract_Euclidean_Space.thy	Mon Dec 02 14:07:42 2019 -0500
+++ b/src/HOL/Analysis/Abstract_Euclidean_Space.thy	Mon Dec 02 22:40:16 2019 -0500
@@ -399,7 +399,7 @@
 lemma Hausdorff_Euclidean_space:
    "Hausdorff_space (Euclidean_space n)"
   unfolding Euclidean_space_def
-  by (rule Hausdorff_space_subtopology) (metis Hausdorff_space_euclidean euclidean_product_topology)
+  by (rule Hausdorff_space_subtopology) (metis Hausdorff_space_euclidean Hausdorff_space_product_topology)
 
 end
 
diff -r 0aaf16a0f7cc -r 3548d54ce3ee src/HOL/Analysis/Analysis.thy
--- a/src/HOL/Analysis/Analysis.thy	Mon Dec 02 14:07:42 2019 -0500
+++ b/src/HOL/Analysis/Analysis.thy	Mon Dec 02 22:40:16 2019 -0500
@@ -46,6 +46,7 @@
   FPS_Convergence
   Smooth_Paths
   Abstract_Euclidean_Space
+  Function_Metric
 begin
 
 end
diff -r 0aaf16a0f7cc -r 3548d54ce3ee src/HOL/Analysis/Function_Metric.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Function_Metric.thy	Mon Dec 02 22:40:16 2019 -0500
@@ -0,0 +1,386 @@
+(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr with additions from LCP
+    License: BSD
+*)
+
+section \<open>Metrics on product spaces\<close>
+
+theory Function_Metric
+  imports
+    Function_Topology
+    Elementary_Metric_Spaces
+begin
+
+text \<open>In general, the product topology is not metrizable, unless the index set is countable.
+When the index set is countable, essentially any (convergent) combination of the metrics on the
+factors will do. We use below the simplest one, based on \<open>L\<^sup>1\<close>, but \<open>L\<^sup>2\<close> would also work,
+for instance.
+
+What is not completely trivial is that the distance thus defined induces the same topology
+as the product topology. This is what we have to prove to show that we have an instance
+of \<^class>\<open>metric_space\<close>.
+
+The proofs below would work verbatim for general countable products of metric spaces. However,
+since distances are only implemented in terms of type classes, we only develop the theory
+for countable products of the same space.\<close>
+
+instantiation "fun" :: (countable, metric_space) metric_space
+begin
+
+definition\<^marker>\<open>tag important\<close> dist_fun_def:
+  "dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
+
+definition\<^marker>\<open>tag important\<close> uniformity_fun_def:
+  "(uniformity::(('a \<Rightarrow> 'b) \<times> ('a \<Rightarrow> 'b)) filter) = (INF e\<in>{0<..}. principal {(x, y). dist (x::('a\<Rightarrow>'b)) y < e})"
+
+text \<open>Except for the first one, the auxiliary lemmas below are only useful when proving the
+instance: once it is proved, they become trivial consequences of the general theory of metric
+spaces. It would thus be desirable to hide them once the instance is proved, but I do not know how
+to do this.\<close>
+
+lemma dist_fun_le_dist_first_terms:
+  "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
+proof -
+  have "(\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)
+          = (\<Sum>n. (1 / 2) ^ (Suc N) * ((1/2) ^ n * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1))"
+    by (rule suminf_cong, simp add: power_add)
+  also have "... = (1/2)^(Suc N) * (\<Sum>n. (1 / 2) ^ n * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)"
+    apply (rule suminf_mult)
+    by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
+  also have "... \<le> (1/2)^(Suc N) * (\<Sum>n. (1 / 2) ^ n)"
+    apply (simp, rule suminf_le, simp)
+    by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
+  also have "... = (1/2)^(Suc N) * 2"
+    using suminf_geometric[of "1/2"] by auto
+  also have "... = (1/2)^N"
+    by auto
+  finally have *: "(\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1) \<le> (1/2)^N"
+    by simp
+
+  define M where "M = Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N}"
+  have "dist (x (from_nat 0)) (y (from_nat 0)) \<le> M"
+    unfolding M_def by (rule Max_ge, auto)
+  then have [simp]: "M \<ge> 0" by (meson dual_order.trans zero_le_dist)
+  have "dist (x (from_nat n)) (y (from_nat n)) \<le> M" if "n\<le>N" for n
+    unfolding M_def apply (rule Max_ge) using that by auto
+  then have i: "min (dist (x (from_nat n)) (y (from_nat n))) 1 \<le> M" if "n\<le>N" for n
+    using that by force
+  have "(\<Sum>n< Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1) \<le>
+      (\<Sum>n< Suc N. M * (1 / 2) ^ n)"
+    by (rule sum_mono, simp add: i)
+  also have "... = M * (\<Sum>n<Suc N. (1 / 2) ^ n)"
+    by (rule sum_distrib_left[symmetric])
+  also have "... \<le> M * (\<Sum>n. (1 / 2) ^ n)"
+    by (rule mult_left_mono, rule sum_le_suminf, auto simp add: summable_geometric_iff)
+  also have "... = M * 2"
+    using suminf_geometric[of "1/2"] by auto
+  finally have **: "(\<Sum>n< Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1) \<le> 2 * M"
+    by simp
+
+  have "dist x y = (\<Sum>n. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
+    unfolding dist_fun_def by simp
+  also have "... = (\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)
+                  + (\<Sum>n<Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
+    apply (rule suminf_split_initial_segment)
+    by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
+  also have "... \<le> 2 * M + (1/2)^N"
+    using * ** by auto
+  finally show ?thesis unfolding M_def by simp
+qed
+
+lemma open_fun_contains_ball_aux:
+  assumes "open (U::(('a \<Rightarrow> 'b) set))"
+          "x \<in> U"
+  shows "\<exists>e>0. {y. dist x y < e} \<subseteq> U"
+proof -
+  have *: "openin (product_topology (\<lambda>i. euclidean) UNIV) U"
+    using open_fun_def assms by auto
+  obtain X where H: "Pi\<^sub>E UNIV X \<subseteq> U"
+                    "\<And>i. openin euclidean (X i)"
+                    "finite {i. X i \<noteq> topspace euclidean}"
+                    "x \<in> Pi\<^sub>E UNIV X"
+    using product_topology_open_contains_basis[OF * \<open>x \<in> U\<close>] by auto
+  define I where "I = {i. X i \<noteq> topspace euclidean}"
+  have "finite I" unfolding I_def using H(3) by auto
+  {
+    fix i
+    have "x i \<in> X i" using \<open>x \<in> U\<close> H by auto
+    then have "\<exists>e. e>0 \<and> ball (x i) e \<subseteq> X i"
+      using \<open>openin euclidean (X i)\<close> open_openin open_contains_ball by blast
+    then obtain e where "e>0" "ball (x i) e \<subseteq> X i" by blast
+    define f where "f = min e (1/2)"
+    have "f>0" "f<1" unfolding f_def using \<open>e>0\<close> by auto
+    moreover have "ball (x i) f \<subseteq> X i" unfolding f_def using \<open>ball (x i) e \<subseteq> X i\<close> by auto
+    ultimately have "\<exists>f. f > 0 \<and> f < 1 \<and> ball (x i) f \<subseteq> X i" by auto
+  } note * = this
+  have "\<exists>e. \<forall>i. e i > 0 \<and> e i < 1 \<and> ball (x i) (e i) \<subseteq> X i"
+    by (rule choice, auto simp add: *)
+  then obtain e where "\<And>i. e i > 0" "\<And>i. e i < 1" "\<And>i. ball (x i) (e i) \<subseteq> X i"
+    by blast
+  define m where "m = Min {(1/2)^(to_nat i) * e i|i. i \<in> I}"
+  have "m > 0" if "I\<noteq>{}"
+    unfolding m_def Min_gr_iff using \<open>finite I\<close> \<open>I \<noteq> {}\<close> \<open>\<And>i. e i > 0\<close> by auto
+  moreover have "{y. dist x y < m} \<subseteq> U"
+  proof (auto)
+    fix y assume "dist x y < m"
+    have "y i \<in> X i" if "i \<in> I" for i
+    proof -
+      have *: "summable (\<lambda>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
+        by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
+      define n where "n = to_nat i"
+      have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 < m"
+        using \<open>dist x y < m\<close> unfolding dist_fun_def using sum_le_suminf[OF *, of "{n}"] by auto
+      then have "(1/2)^(to_nat i) * min (dist (x i) (y i)) 1 < m"
+        using \<open>n = to_nat i\<close> by auto
+      also have "... \<le> (1/2)^(to_nat i) * e i"
+        unfolding m_def apply (rule Min_le) using \<open>finite I\<close> \<open>i \<in> I\<close> by auto
+      ultimately have "min (dist (x i) (y i)) 1 < e i"
+        by (auto simp add: field_split_simps)
+      then have "dist (x i) (y i) < e i"
+        using \<open>e i < 1\<close> by auto
+      then show "y i \<in> X i" using \<open>ball (x i) (e i) \<subseteq> X i\<close> by auto
+    qed
+    then have "y \<in> Pi\<^sub>E UNIV X" using H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)
+    then show "y \<in> U" using \<open>Pi\<^sub>E UNIV X \<subseteq> U\<close> by auto
+  qed
+  ultimately have *: "\<exists>m>0. {y. dist x y < m} \<subseteq> U" if "I \<noteq> {}" using that by auto
+
+  have "U = UNIV" if "I = {}"
+    using that H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)
+  then have "\<exists>m>0. {y. dist x y < m} \<subseteq> U" if "I = {}" using that zero_less_one by blast
+  then show "\<exists>m>0. {y. dist x y < m} \<subseteq> U" using * by blast
+qed
+
+lemma ball_fun_contains_open_aux:
+  fixes x::"('a \<Rightarrow> 'b)" and e::real
+  assumes "e>0"
+  shows "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> {y. dist x y < e}"
+proof -
+  have "\<exists>N::nat. 2^N > 8/e"
+    by (simp add: real_arch_pow)
+  then obtain N::nat where "2^N > 8/e" by auto
+  define f where "f = e/4"
+  have [simp]: "e>0" "f > 0" unfolding f_def using assms by auto
+  define X::"('a \<Rightarrow> 'b set)" where "X = (\<lambda>i. if (\<exists>n\<le>N. i = from_nat n) then {z. dist (x i) z < f} else UNIV)"
+  have "{i. X i \<noteq> UNIV} \<subseteq> from_nat`{0..N}"
+    unfolding X_def by auto
+  then have "finite {i. X i \<noteq> topspace euclidean}"
+    unfolding topspace_euclidean using finite_surj by blast
+  have "\<And>i. open (X i)"
+    unfolding X_def using metric_space_class.open_ball open_UNIV by auto
+  then have "\<And>i. openin euclidean (X i)"
+    using open_openin by auto
+  define U where "U = Pi\<^sub>E UNIV X"
+  have "open U"
+    unfolding open_fun_def product_topology_def apply (rule topology_generated_by_Basis)
+    unfolding U_def using \<open>\<And>i. openin euclidean (X i)\<close> \<open>finite {i. X i \<noteq> topspace euclidean}\<close>
+    by auto
+  moreover have "x \<in> U"
+    unfolding U_def X_def by (auto simp add: PiE_iff)
+  moreover have "dist x y < e" if "y \<in> U" for y
+  proof -
+    have *: "dist (x (from_nat n)) (y (from_nat n)) \<le> f" if "n \<le> N" for n
+      using \<open>y \<in> U\<close> unfolding U_def apply (auto simp add: PiE_iff)
+      unfolding X_def using that by (metis less_imp_le mem_Collect_eq)
+    have **: "Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} \<le> f"
+      apply (rule Max.boundedI) using * by auto
+
+    have "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
+      by (rule dist_fun_le_dist_first_terms)
+    also have "... \<le> 2 * f + e / 8"
+      apply (rule add_mono) using ** \<open>2^N > 8/e\<close> by(auto simp add: algebra_simps field_split_simps)
+    also have "... \<le> e/2 + e/8"
+      unfolding f_def by auto
+    also have "... < e"
+      by auto
+    finally show "dist x y < e" by simp
+  qed
+  ultimately show ?thesis by auto
+qed
+
+lemma fun_open_ball_aux:
+  fixes U::"('a \<Rightarrow> 'b) set"
+  shows "open U \<longleftrightarrow> (\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U)"
+proof (auto)
+  assume "open U"
+  fix x assume "x \<in> U"
+  then show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"
+    using open_fun_contains_ball_aux[OF \<open>open U\<close> \<open>x \<in> U\<close>] by auto
+next
+  assume H: "\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"
+  define K where "K = {V. open V \<and> V \<subseteq> U}"
+  {
+    fix x assume "x \<in> U"
+    then obtain e where e: "e>0" "{y. dist x y < e} \<subseteq> U" using H by blast
+    then obtain V where V: "open V" "x \<in> V" "V \<subseteq> {y. dist x y < e}"
+      using ball_fun_contains_open_aux[OF \<open>e>0\<close>, of x] by auto
+    have "V \<in> K"
+      unfolding K_def using e(2) V(1) V(3) by auto
+    then have "x \<in> (\<Union>K)" using \<open>x \<in> V\<close> by auto
+  }
+  then have "(\<Union>K) = U"
+    unfolding K_def by auto
+  moreover have "open (\<Union>K)"
+    unfolding K_def by auto
+  ultimately show "open U" by simp
+qed
+
+instance proof
+  fix x y::"'a \<Rightarrow> 'b" show "(dist x y = 0) = (x = y)"
+  proof
+    assume "x = y"
+    then show "dist x y = 0" unfolding dist_fun_def using \<open>x = y\<close> by auto
+  next
+    assume "dist x y = 0"
+    have *: "summable (\<lambda>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
+      by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
+    have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 = 0" for n
+      using \<open>dist x y = 0\<close> unfolding dist_fun_def by (simp add: "*" suminf_eq_zero_iff)
+    then have "dist (x (from_nat n)) (y (from_nat n)) = 0" for n
+      by (metis div_0 min_def nonzero_mult_div_cancel_left power_eq_0_iff
+                zero_eq_1_divide_iff zero_neq_numeral)
+    then have "x (from_nat n) = y (from_nat n)" for n
+      by auto
+    then have "x i = y i" for i
+      by (metis from_nat_to_nat)
+    then show "x = y"
+      by auto
+  qed
+next
+  text\<open>The proof of the triangular inequality is trivial, modulo the fact that we are dealing
+        with infinite series, hence we should justify the convergence at each step. In this
+        respect, the following simplification rule is extremely handy.\<close>
+  have [simp]: "summable (\<lambda>n. (1/2)^n * min (dist (u (from_nat n)) (v (from_nat n))) 1)" for u v::"'a \<Rightarrow> 'b"
+    by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
+  fix x y z::"'a \<Rightarrow> 'b"
+  {
+    fix n
+    have *: "dist (x (from_nat n)) (y (from_nat n)) \<le>
+            dist (x (from_nat n)) (z (from_nat n)) + dist (y (from_nat n)) (z (from_nat n))"
+      by (simp add: dist_triangle2)
+    have "0 \<le> dist (y (from_nat n)) (z (from_nat n))"
+      using zero_le_dist by blast
+    moreover
+    {
+      assume "min (dist (y (from_nat n)) (z (from_nat n))) 1 \<noteq> dist (y (from_nat n)) (z (from_nat n))"
+      then have "1 \<le> min (dist (x (from_nat n)) (z (from_nat n))) 1 + min (dist (y (from_nat n)) (z (from_nat n))) 1"
+        by (metis (no_types) diff_le_eq diff_self min_def zero_le_dist zero_le_one)
+    }
+    ultimately have "min (dist (x (from_nat n)) (y (from_nat n))) 1 \<le>
+            min (dist (x (from_nat n)) (z (from_nat n))) 1 + min (dist (y (from_nat n)) (z (from_nat n))) 1"
+      using * by linarith
+  } note ineq = this
+  have "dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
+    unfolding dist_fun_def by simp
+  also have "... \<le> (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1
+                        + (1/2)^n * min (dist (y (from_nat n)) (z (from_nat n))) 1)"
+    apply (rule suminf_le)
+    using ineq apply (metis (no_types, hide_lams) add.right_neutral distrib_left
+      le_divide_eq_numeral1(1) mult_2_right mult_left_mono zero_le_one zero_le_power)
+    by (auto simp add: summable_add)
+  also have "... = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1)
+                  + (\<Sum>n. (1/2)^n * min (dist (y (from_nat n)) (z (from_nat n))) 1)"
+    by (rule suminf_add[symmetric], auto)
+  also have "... = dist x z + dist y z"
+    unfolding dist_fun_def by simp
+  finally show "dist x y \<le> dist x z + dist y z"
+    by simp
+next
+  text\<open>Finally, we show that the topology generated by the distance and the product
+        topology coincide. This is essentially contained in Lemma \<open>fun_open_ball_aux\<close>,
+        except that the condition to prove is expressed with filters. To deal with this,
+        we copy some mumbo jumbo from Lemma \<open>eventually_uniformity_metric\<close> in
+        \<^file>\<open>~~/src/HOL/Real_Vector_Spaces.thy\<close>\<close>
+  fix U::"('a \<Rightarrow> 'b) set"
+  have "eventually P uniformity \<longleftrightarrow> (\<exists>e>0. \<forall>x (y::('a \<Rightarrow> 'b)). dist x y < e \<longrightarrow> P (x, y))" for P
+  unfolding uniformity_fun_def apply (subst eventually_INF_base)
+    by (auto simp: eventually_principal subset_eq intro: bexI[of _ "min _ _"])
+  then show "open U = (\<forall>x\<in>U. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U)"
+    unfolding fun_open_ball_aux by simp
+qed (simp add: uniformity_fun_def)
+
+end
+
+text \<open>Nice properties of spaces are preserved under countable products. In addition
+to first countability, second countability and metrizability, as we have seen above,
+completeness is also preserved, and therefore being Polish.\<close>
+
+instance "fun" :: (countable, complete_space) complete_space
+proof
+  fix u::"nat \<Rightarrow> ('a \<Rightarrow> 'b)" assume "Cauchy u"
+  have "Cauchy (\<lambda>n. u n i)" for i
+  unfolding cauchy_def proof (intro impI allI)
+    fix e assume "e>(0::real)"
+    obtain k where "i = from_nat k"
+      using from_nat_to_nat[of i] by metis
+    have "(1/2)^k * min e 1 > 0" using \<open>e>0\<close> by auto
+    then have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m) (u n) < (1/2)^k * min e 1"
+      using \<open>Cauchy u\<close> unfolding cauchy_def by blast
+    then obtain N::nat where C: "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m) (u n) < (1/2)^k * min e 1"
+      by blast
+    have "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"
+    proof (auto)
+      fix m n::nat assume "m \<ge> N" "n \<ge> N"
+      have "(1/2)^k * min (dist (u m i) (u n i)) 1
+              = sum (\<lambda>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1) {k}"
+        using \<open>i = from_nat k\<close> by auto
+      also have "... \<le> (\<Sum>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1)"
+        apply (rule sum_le_suminf)
+        by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
+      also have "... = dist (u m) (u n)"
+        unfolding dist_fun_def by auto
+      also have "... < (1/2)^k * min e 1"
+        using C \<open>m \<ge> N\<close> \<open>n \<ge> N\<close> by auto
+      finally have "min (dist (u m i) (u n i)) 1 < min e 1"
+        by (auto simp add: algebra_simps field_split_simps)
+      then show "dist (u m i) (u n i) < e" by auto
+    qed
+    then show "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"
+      by blast
+  qed
+  then have "\<exists>x. (\<lambda>n. u n i) \<longlonglongrightarrow> x" for i
+    using Cauchy_convergent convergent_def by auto
+  then have "\<exists>x. \<forall>i. (\<lambda>n. u n i) \<longlonglongrightarrow> x i"
+    using choice by force
+  then obtain x where *: "\<And>i. (\<lambda>n. u n i) \<longlonglongrightarrow> x i" by blast
+  have "u \<longlonglongrightarrow> x"
+  proof (rule metric_LIMSEQ_I)
+    fix e assume [simp]: "e>(0::real)"
+    have i: "\<exists>K. \<forall>n\<ge>K. dist (u n i) (x i) < e/4" for i
+      by (rule metric_LIMSEQ_D, auto simp add: *)
+    have "\<exists>K. \<forall>i. \<forall>n\<ge>K i. dist (u n i) (x i) < e/4"
+      apply (rule choice) using i by auto
+    then obtain K where K: "\<And>i n. n \<ge> K i \<Longrightarrow> dist (u n i) (x i) < e/4"
+      by blast
+
+    have "\<exists>N::nat. 2^N > 4/e"
+      by (simp add: real_arch_pow)
+    then obtain N::nat where "2^N > 4/e" by auto
+    define L where "L = Max {K (from_nat n)|n. n \<le> N}"
+    have "dist (u k) x < e" if "k \<ge> L" for k
+    proof -
+      have *: "dist (u k (from_nat n)) (x (from_nat n)) \<le> e / 4" if "n \<le> N" for n
+      proof -
+        have "K (from_nat n) \<le> L"
+          unfolding L_def apply (rule Max_ge) using \<open>n \<le> N\<close> by auto
+        then have "k \<ge> K (from_nat n)" using \<open>k \<ge> L\<close> by auto
+        then show ?thesis using K less_imp_le by auto
+      qed
+      have **: "Max {dist (u k (from_nat n)) (x (from_nat n)) |n. n \<le> N} \<le> e/4"
+        apply (rule Max.boundedI) using * by auto
+      have "dist (u k) x \<le> 2 * Max {dist (u k (from_nat n)) (x (from_nat n)) |n. n \<le> N} + (1/2)^N"
+        using dist_fun_le_dist_first_terms by auto
+      also have "... \<le> 2 * e/4 + e/4"
+        apply (rule add_mono)
+        using ** \<open>2^N > 4/e\<close> less_imp_le by (auto simp add: algebra_simps field_split_simps)
+      also have "... < e" by auto
+      finally show ?thesis by simp
+    qed
+    then show "\<exists>L. \<forall>k\<ge>L. dist (u k) x < e" by blast
+  qed
+  then show "convergent u" using convergent_def by blast
+qed
+
+instance "fun" :: (countable, polish_space) polish_space
+  by standard
+
+end
\ No newline at end of file
diff -r 0aaf16a0f7cc -r 3548d54ce3ee src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Mon Dec 02 14:07:42 2019 -0500
+++ b/src/HOL/Analysis/Function_Topology.thy	Mon Dec 02 22:40:16 2019 -0500
@@ -3,7 +3,10 @@
 *)
 
 theory Function_Topology
-imports Topology_Euclidean_Space Abstract_Limits
+  imports
+    Elementary_Topology
+    Abstract_Limits
+    Connected
 begin
 
 
@@ -643,7 +646,7 @@
   by (auto simp: continuous_on_product_then_coordinatewise continuous_on_coordinatewise_then_product)
 
 lemma continuous_map_span_sum:
-  fixes B :: "'a::real_inner set"
+  fixes B :: "'a::real_normed_vector set"
   assumes biB: "\<And>i. i \<in> I \<Longrightarrow> b i \<in> B"
   shows "continuous_map euclidean (top_of_set (span B)) (\<lambda>x. \<Sum>i\<in>I. x i *\<^sub>R b i)"
 proof (rule continuous_map_euclidean_top_of_set)
@@ -878,382 +881,6 @@
   apply standard
   using product_topology_countable_basis topological_basis_imp_subbasis by auto
 
-subsection \<open>Metrics on product spaces\<close>
-
-
-text \<open>In general, the product topology is not metrizable, unless the index set is countable.
-When the index set is countable, essentially any (convergent) combination of the metrics on the
-factors will do. We use below the simplest one, based on \<open>L\<^sup>1\<close>, but \<open>L\<^sup>2\<close> would also work,
-for instance.
-
-What is not completely trivial is that the distance thus defined induces the same topology
-as the product topology. This is what we have to prove to show that we have an instance
-of \<^class>\<open>metric_space\<close>.
-
-The proofs below would work verbatim for general countable products of metric spaces. However,
-since distances are only implemented in terms of type classes, we only develop the theory
-for countable products of the same space.\<close>
-
-instantiation "fun" :: (countable, metric_space) metric_space
-begin
-
-definition\<^marker>\<open>tag important\<close> dist_fun_def:
-  "dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
-
-definition\<^marker>\<open>tag important\<close> uniformity_fun_def:
-  "(uniformity::(('a \<Rightarrow> 'b) \<times> ('a \<Rightarrow> 'b)) filter) = (INF e\<in>{0<..}. principal {(x, y). dist (x::('a\<Rightarrow>'b)) y < e})"
-
-text \<open>Except for the first one, the auxiliary lemmas below are only useful when proving the
-instance: once it is proved, they become trivial consequences of the general theory of metric
-spaces. It would thus be desirable to hide them once the instance is proved, but I do not know how
-to do this.\<close>
-
-lemma dist_fun_le_dist_first_terms:
-  "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
-proof -
-  have "(\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)
-          = (\<Sum>n. (1 / 2) ^ (Suc N) * ((1/2) ^ n * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1))"
-    by (rule suminf_cong, simp add: power_add)
-  also have "... = (1/2)^(Suc N) * (\<Sum>n. (1 / 2) ^ n * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)"
-    apply (rule suminf_mult)
-    by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
-  also have "... \<le> (1/2)^(Suc N) * (\<Sum>n. (1 / 2) ^ n)"
-    apply (simp, rule suminf_le, simp)
-    by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
-  also have "... = (1/2)^(Suc N) * 2"
-    using suminf_geometric[of "1/2"] by auto
-  also have "... = (1/2)^N"
-    by auto
-  finally have *: "(\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1) \<le> (1/2)^N"
-    by simp
-
-  define M where "M = Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N}"
-  have "dist (x (from_nat 0)) (y (from_nat 0)) \<le> M"
-    unfolding M_def by (rule Max_ge, auto)
-  then have [simp]: "M \<ge> 0" by (meson dual_order.trans zero_le_dist)
-  have "dist (x (from_nat n)) (y (from_nat n)) \<le> M" if "n\<le>N" for n
-    unfolding M_def apply (rule Max_ge) using that by auto
-  then have i: "min (dist (x (from_nat n)) (y (from_nat n))) 1 \<le> M" if "n\<le>N" for n
-    using that by force
-  have "(\<Sum>n< Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1) \<le>
-      (\<Sum>n< Suc N. M * (1 / 2) ^ n)"
-    by (rule sum_mono, simp add: i)
-  also have "... = M * (\<Sum>n<Suc N. (1 / 2) ^ n)"
-    by (rule sum_distrib_left[symmetric])
-  also have "... \<le> M * (\<Sum>n. (1 / 2) ^ n)"
-    by (rule mult_left_mono, rule sum_le_suminf, auto simp add: summable_geometric_iff)
-  also have "... = M * 2"
-    using suminf_geometric[of "1/2"] by auto
-  finally have **: "(\<Sum>n< Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1) \<le> 2 * M"
-    by simp
-
-  have "dist x y = (\<Sum>n. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
-    unfolding dist_fun_def by simp
-  also have "... = (\<Sum>n. (1 / 2) ^ (n+Suc N) * min (dist (x (from_nat (n+Suc N))) (y (from_nat (n+Suc N)))) 1)
-                  + (\<Sum>n<Suc N. (1 / 2) ^ n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
-    apply (rule suminf_split_initial_segment)
-    by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
-  also have "... \<le> 2 * M + (1/2)^N"
-    using * ** by auto
-  finally show ?thesis unfolding M_def by simp
-qed
-
-lemma open_fun_contains_ball_aux:
-  assumes "open (U::(('a \<Rightarrow> 'b) set))"
-          "x \<in> U"
-  shows "\<exists>e>0. {y. dist x y < e} \<subseteq> U"
-proof -
-  have *: "openin (product_topology (\<lambda>i. euclidean) UNIV) U"
-    using open_fun_def assms by auto
-  obtain X where H: "Pi\<^sub>E UNIV X \<subseteq> U"
-                    "\<And>i. openin euclidean (X i)"
-                    "finite {i. X i \<noteq> topspace euclidean}"
-                    "x \<in> Pi\<^sub>E UNIV X"
-    using product_topology_open_contains_basis[OF * \<open>x \<in> U\<close>] by auto
-  define I where "I = {i. X i \<noteq> topspace euclidean}"
-  have "finite I" unfolding I_def using H(3) by auto
-  {
-    fix i
-    have "x i \<in> X i" using \<open>x \<in> U\<close> H by auto
-    then have "\<exists>e. e>0 \<and> ball (x i) e \<subseteq> X i"
-      using \<open>openin euclidean (X i)\<close> open_openin open_contains_ball by blast
-    then obtain e where "e>0" "ball (x i) e \<subseteq> X i" by blast
-    define f where "f = min e (1/2)"
-    have "f>0" "f<1" unfolding f_def using \<open>e>0\<close> by auto
-    moreover have "ball (x i) f \<subseteq> X i" unfolding f_def using \<open>ball (x i) e \<subseteq> X i\<close> by auto
-    ultimately have "\<exists>f. f > 0 \<and> f < 1 \<and> ball (x i) f \<subseteq> X i" by auto
-  } note * = this
-  have "\<exists>e. \<forall>i. e i > 0 \<and> e i < 1 \<and> ball (x i) (e i) \<subseteq> X i"
-    by (rule choice, auto simp add: *)
-  then obtain e where "\<And>i. e i > 0" "\<And>i. e i < 1" "\<And>i. ball (x i) (e i) \<subseteq> X i"
-    by blast
-  define m where "m = Min {(1/2)^(to_nat i) * e i|i. i \<in> I}"
-  have "m > 0" if "I\<noteq>{}"
-    unfolding m_def Min_gr_iff using \<open>finite I\<close> \<open>I \<noteq> {}\<close> \<open>\<And>i. e i > 0\<close> by auto
-  moreover have "{y. dist x y < m} \<subseteq> U"
-  proof (auto)
-    fix y assume "dist x y < m"
-    have "y i \<in> X i" if "i \<in> I" for i
-    proof -
-      have *: "summable (\<lambda>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
-        by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
-      define n where "n = to_nat i"
-      have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 < m"
-        using \<open>dist x y < m\<close> unfolding dist_fun_def using sum_le_suminf[OF *, of "{n}"] by auto
-      then have "(1/2)^(to_nat i) * min (dist (x i) (y i)) 1 < m"
-        using \<open>n = to_nat i\<close> by auto
-      also have "... \<le> (1/2)^(to_nat i) * e i"
-        unfolding m_def apply (rule Min_le) using \<open>finite I\<close> \<open>i \<in> I\<close> by auto
-      ultimately have "min (dist (x i) (y i)) 1 < e i"
-        by (auto simp add: field_split_simps)
-      then have "dist (x i) (y i) < e i"
-        using \<open>e i < 1\<close> by auto
-      then show "y i \<in> X i" using \<open>ball (x i) (e i) \<subseteq> X i\<close> by auto
-    qed
-    then have "y \<in> Pi\<^sub>E UNIV X" using H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)
-    then show "y \<in> U" using \<open>Pi\<^sub>E UNIV X \<subseteq> U\<close> by auto
-  qed
-  ultimately have *: "\<exists>m>0. {y. dist x y < m} \<subseteq> U" if "I \<noteq> {}" using that by auto
-
-  have "U = UNIV" if "I = {}"
-    using that H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)
-  then have "\<exists>m>0. {y. dist x y < m} \<subseteq> U" if "I = {}" using that zero_less_one by blast
-  then show "\<exists>m>0. {y. dist x y < m} \<subseteq> U" using * by blast
-qed
-
-lemma ball_fun_contains_open_aux:
-  fixes x::"('a \<Rightarrow> 'b)" and e::real
-  assumes "e>0"
-  shows "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> {y. dist x y < e}"
-proof -
-  have "\<exists>N::nat. 2^N > 8/e"
-    by (simp add: real_arch_pow)
-  then obtain N::nat where "2^N > 8/e" by auto
-  define f where "f = e/4"
-  have [simp]: "e>0" "f > 0" unfolding f_def using assms by auto
-  define X::"('a \<Rightarrow> 'b set)" where "X = (\<lambda>i. if (\<exists>n\<le>N. i = from_nat n) then {z. dist (x i) z < f} else UNIV)"
-  have "{i. X i \<noteq> UNIV} \<subseteq> from_nat`{0..N}"
-    unfolding X_def by auto
-  then have "finite {i. X i \<noteq> topspace euclidean}"
-    unfolding topspace_euclidean using finite_surj by blast
-  have "\<And>i. open (X i)"
-    unfolding X_def using metric_space_class.open_ball open_UNIV by auto
-  then have "\<And>i. openin euclidean (X i)"
-    using open_openin by auto
-  define U where "U = Pi\<^sub>E UNIV X"
-  have "open U"
-    unfolding open_fun_def product_topology_def apply (rule topology_generated_by_Basis)
-    unfolding U_def using \<open>\<And>i. openin euclidean (X i)\<close> \<open>finite {i. X i \<noteq> topspace euclidean}\<close>
-    by auto
-  moreover have "x \<in> U"
-    unfolding U_def X_def by (auto simp add: PiE_iff)
-  moreover have "dist x y < e" if "y \<in> U" for y
-  proof -
-    have *: "dist (x (from_nat n)) (y (from_nat n)) \<le> f" if "n \<le> N" for n
-      using \<open>y \<in> U\<close> unfolding U_def apply (auto simp add: PiE_iff)
-      unfolding X_def using that by (metis less_imp_le mem_Collect_eq)
-    have **: "Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} \<le> f"
-      apply (rule Max.boundedI) using * by auto
-
-    have "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
-      by (rule dist_fun_le_dist_first_terms)
-    also have "... \<le> 2 * f + e / 8"
-      apply (rule add_mono) using ** \<open>2^N > 8/e\<close> by(auto simp add: algebra_simps field_split_simps)
-    also have "... \<le> e/2 + e/8"
-      unfolding f_def by auto
-    also have "... < e"
-      by auto
-    finally show "dist x y < e" by simp
-  qed
-  ultimately show ?thesis by auto
-qed
-
-lemma fun_open_ball_aux:
-  fixes U::"('a \<Rightarrow> 'b) set"
-  shows "open U \<longleftrightarrow> (\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U)"
-proof (auto)
-  assume "open U"
-  fix x assume "x \<in> U"
-  then show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"
-    using open_fun_contains_ball_aux[OF \<open>open U\<close> \<open>x \<in> U\<close>] by auto
-next
-  assume H: "\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"
-  define K where "K = {V. open V \<and> V \<subseteq> U}"
-  {
-    fix x assume "x \<in> U"
-    then obtain e where e: "e>0" "{y. dist x y < e} \<subseteq> U" using H by blast
-    then obtain V where V: "open V" "x \<in> V" "V \<subseteq> {y. dist x y < e}"
-      using ball_fun_contains_open_aux[OF \<open>e>0\<close>, of x] by auto
-    have "V \<in> K"
-      unfolding K_def using e(2) V(1) V(3) by auto
-    then have "x \<in> (\<Union>K)" using \<open>x \<in> V\<close> by auto
-  }
-  then have "(\<Union>K) = U"
-    unfolding K_def by auto
-  moreover have "open (\<Union>K)"
-    unfolding K_def by auto
-  ultimately show "open U" by simp
-qed
-
-instance proof
-  fix x y::"'a \<Rightarrow> 'b" show "(dist x y = 0) = (x = y)"
-  proof
-    assume "x = y"
-    then show "dist x y = 0" unfolding dist_fun_def using \<open>x = y\<close> by auto
-  next
-    assume "dist x y = 0"
-    have *: "summable (\<lambda>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
-      by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
-    have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 = 0" for n
-      using \<open>dist x y = 0\<close> unfolding dist_fun_def by (simp add: "*" suminf_eq_zero_iff)
-    then have "dist (x (from_nat n)) (y (from_nat n)) = 0" for n
-      by (metis div_0 min_def nonzero_mult_div_cancel_left power_eq_0_iff
-                zero_eq_1_divide_iff zero_neq_numeral)
-    then have "x (from_nat n) = y (from_nat n)" for n
-      by auto
-    then have "x i = y i" for i
-      by (metis from_nat_to_nat)
-    then show "x = y"
-      by auto
-  qed
-next
-  text\<open>The proof of the triangular inequality is trivial, modulo the fact that we are dealing
-        with infinite series, hence we should justify the convergence at each step. In this
-        respect, the following simplification rule is extremely handy.\<close>
-  have [simp]: "summable (\<lambda>n. (1/2)^n * min (dist (u (from_nat n)) (v (from_nat n))) 1)" for u v::"'a \<Rightarrow> 'b"
-    by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
-  fix x y z::"'a \<Rightarrow> 'b"
-  {
-    fix n
-    have *: "dist (x (from_nat n)) (y (from_nat n)) \<le>
-            dist (x (from_nat n)) (z (from_nat n)) + dist (y (from_nat n)) (z (from_nat n))"
-      by (simp add: dist_triangle2)
-    have "0 \<le> dist (y (from_nat n)) (z (from_nat n))"
-      using zero_le_dist by blast
-    moreover
-    {
-      assume "min (dist (y (from_nat n)) (z (from_nat n))) 1 \<noteq> dist (y (from_nat n)) (z (from_nat n))"
-      then have "1 \<le> min (dist (x (from_nat n)) (z (from_nat n))) 1 + min (dist (y (from_nat n)) (z (from_nat n))) 1"
-        by (metis (no_types) diff_le_eq diff_self min_def zero_le_dist zero_le_one)
-    }
-    ultimately have "min (dist (x (from_nat n)) (y (from_nat n))) 1 \<le>
-            min (dist (x (from_nat n)) (z (from_nat n))) 1 + min (dist (y (from_nat n)) (z (from_nat n))) 1"
-      using * by linarith
-  } note ineq = this
-  have "dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
-    unfolding dist_fun_def by simp
-  also have "... \<le> (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1
-                        + (1/2)^n * min (dist (y (from_nat n)) (z (from_nat n))) 1)"
-    apply (rule suminf_le)
-    using ineq apply (metis (no_types, hide_lams) add.right_neutral distrib_left
-      le_divide_eq_numeral1(1) mult_2_right mult_left_mono zero_le_one zero_le_power)
-    by (auto simp add: summable_add)
-  also have "... = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (z (from_nat n))) 1)
-                  + (\<Sum>n. (1/2)^n * min (dist (y (from_nat n)) (z (from_nat n))) 1)"
-    by (rule suminf_add[symmetric], auto)
-  also have "... = dist x z + dist y z"
-    unfolding dist_fun_def by simp
-  finally show "dist x y \<le> dist x z + dist y z"
-    by simp
-next
-  text\<open>Finally, we show that the topology generated by the distance and the product
-        topology coincide. This is essentially contained in Lemma \<open>fun_open_ball_aux\<close>,
-        except that the condition to prove is expressed with filters. To deal with this,
-        we copy some mumbo jumbo from Lemma \<open>eventually_uniformity_metric\<close> in
-        \<^file>\<open>~~/src/HOL/Real_Vector_Spaces.thy\<close>\<close>
-  fix U::"('a \<Rightarrow> 'b) set"
-  have "eventually P uniformity \<longleftrightarrow> (\<exists>e>0. \<forall>x (y::('a \<Rightarrow> 'b)). dist x y < e \<longrightarrow> P (x, y))" for P
-  unfolding uniformity_fun_def apply (subst eventually_INF_base)
-    by (auto simp: eventually_principal subset_eq intro: bexI[of _ "min _ _"])
-  then show "open U = (\<forall>x\<in>U. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U)"
-    unfolding fun_open_ball_aux by simp
-qed (simp add: uniformity_fun_def)
-
-end
-
-text \<open>Nice properties of spaces are preserved under countable products. In addition
-to first countability, second countability and metrizability, as we have seen above,
-completeness is also preserved, and therefore being Polish.\<close>
-
-instance "fun" :: (countable, complete_space) complete_space
-proof
-  fix u::"nat \<Rightarrow> ('a \<Rightarrow> 'b)" assume "Cauchy u"
-  have "Cauchy (\<lambda>n. u n i)" for i
-  unfolding cauchy_def proof (intro impI allI)
-    fix e assume "e>(0::real)"
-    obtain k where "i = from_nat k"
-      using from_nat_to_nat[of i] by metis
-    have "(1/2)^k * min e 1 > 0" using \<open>e>0\<close> by auto
-    then have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m) (u n) < (1/2)^k * min e 1"
-      using \<open>Cauchy u\<close> unfolding cauchy_def by blast
-    then obtain N::nat where C: "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m) (u n) < (1/2)^k * min e 1"
-      by blast
-    have "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"
-    proof (auto)
-      fix m n::nat assume "m \<ge> N" "n \<ge> N"
-      have "(1/2)^k * min (dist (u m i) (u n i)) 1
-              = sum (\<lambda>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1) {k}"
-        using \<open>i = from_nat k\<close> by auto
-      also have "... \<le> (\<Sum>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1)"
-        apply (rule sum_le_suminf)
-        by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
-      also have "... = dist (u m) (u n)"
-        unfolding dist_fun_def by auto
-      also have "... < (1/2)^k * min e 1"
-        using C \<open>m \<ge> N\<close> \<open>n \<ge> N\<close> by auto
-      finally have "min (dist (u m i) (u n i)) 1 < min e 1"
-        by (auto simp add: algebra_simps field_split_simps)
-      then show "dist (u m i) (u n i) < e" by auto
-    qed
-    then show "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"
-      by blast
-  qed
-  then have "\<exists>x. (\<lambda>n. u n i) \<longlonglongrightarrow> x" for i
-    using Cauchy_convergent convergent_def by auto
-  then have "\<exists>x. \<forall>i. (\<lambda>n. u n i) \<longlonglongrightarrow> x i"
-    using choice by force
-  then obtain x where *: "\<And>i. (\<lambda>n. u n i) \<longlonglongrightarrow> x i" by blast
-  have "u \<longlonglongrightarrow> x"
-  proof (rule metric_LIMSEQ_I)
-    fix e assume [simp]: "e>(0::real)"
-    have i: "\<exists>K. \<forall>n\<ge>K. dist (u n i) (x i) < e/4" for i
-      by (rule metric_LIMSEQ_D, auto simp add: *)
-    have "\<exists>K. \<forall>i. \<forall>n\<ge>K i. dist (u n i) (x i) < e/4"
-      apply (rule choice) using i by auto
-    then obtain K where K: "\<And>i n. n \<ge> K i \<Longrightarrow> dist (u n i) (x i) < e/4"
-      by blast
-
-    have "\<exists>N::nat. 2^N > 4/e"
-      by (simp add: real_arch_pow)
-    then obtain N::nat where "2^N > 4/e" by auto
-    define L where "L = Max {K (from_nat n)|n. n \<le> N}"
-    have "dist (u k) x < e" if "k \<ge> L" for k
-    proof -
-      have *: "dist (u k (from_nat n)) (x (from_nat n)) \<le> e / 4" if "n \<le> N" for n
-      proof -
-        have "K (from_nat n) \<le> L"
-          unfolding L_def apply (rule Max_ge) using \<open>n \<le> N\<close> by auto
-        then have "k \<ge> K (from_nat n)" using \<open>k \<ge> L\<close> by auto
-        then show ?thesis using K less_imp_le by auto
-      qed
-      have **: "Max {dist (u k (from_nat n)) (x (from_nat n)) |n. n \<le> N} \<le> e/4"
-        apply (rule Max.boundedI) using * by auto
-      have "dist (u k) x \<le> 2 * Max {dist (u k (from_nat n)) (x (from_nat n)) |n. n \<le> N} + (1/2)^N"
-        using dist_fun_le_dist_first_terms by auto
-      also have "... \<le> 2 * e/4 + e/4"
-        apply (rule add_mono)
-        using ** \<open>2^N > 4/e\<close> less_imp_le by (auto simp add: algebra_simps field_split_simps)
-      also have "... < e" by auto
-      finally show ?thesis by simp
-    qed
-    then show "\<exists>L. \<forall>k\<ge>L. dist (u k) x < e" by blast
-  qed
-  then show "convergent u" using convergent_def by blast
-qed
-
-instance "fun" :: (countable, polish_space) polish_space
-  by standard
-
 
 subsection\<open>The Alexander subbase theorem\<close>
 
diff -r 0aaf16a0f7cc -r 3548d54ce3ee src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Mon Dec 02 14:07:42 2019 -0500
+++ b/src/HOL/Analysis/Path_Connected.thy	Mon Dec 02 22:40:16 2019 -0500
@@ -3874,6 +3874,24 @@
 
 subsubsection\<open>Special characterizations of classes of functions into and out of R.\<close>
 
+lemma Hausdorff_space_euclidean [simp]: "Hausdorff_space (euclidean :: 'a::metric_space topology)"
+proof -
+  have "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> disjnt U V"
+    if "x \<noteq> y"
+    for x y :: 'a
+  proof (intro exI conjI)
+    let ?r = "dist x y / 2"
+    have [simp]: "?r > 0"
+      by (simp add: that)
+    show "open (ball x ?r)" "open (ball y ?r)" "x \<in> (ball x ?r)" "y \<in> (ball y ?r)"
+      by (auto simp add: that)
+    show "disjnt (ball x ?r) (ball y ?r)"
+      unfolding disjnt_def by (simp add: disjoint_ballI)
+  qed
+  then show ?thesis
+    by (simp add: Hausdorff_space_def)
+qed
+
 proposition embedding_map_into_euclideanreal:
   assumes "path_connected_space X"
   shows "embedding_map X euclideanreal f \<longleftrightarrow>
diff -r 0aaf16a0f7cc -r 3548d54ce3ee src/HOL/Analysis/Product_Topology.thy
--- a/src/HOL/Analysis/Product_Topology.thy	Mon Dec 02 14:07:42 2019 -0500
+++ b/src/HOL/Analysis/Product_Topology.thy	Mon Dec 02 22:40:16 2019 -0500
@@ -1,10 +1,10 @@
 section\<open>The binary product topology\<close>
 
 theory Product_Topology
-imports Function_Topology Abstract_Limits
+imports Function_Topology
 begin
 
-section \<open>Product Topology\<close> 
+section \<open>Product Topology\<close>
 
 subsection\<open>Definition\<close>
 
diff -r 0aaf16a0f7cc -r 3548d54ce3ee src/HOL/Analysis/T1_Spaces.thy
--- a/src/HOL/Analysis/T1_Spaces.thy	Mon Dec 02 14:07:42 2019 -0500
+++ b/src/HOL/Analysis/T1_Spaces.thy	Mon Dec 02 22:40:16 2019 -0500
@@ -1,7 +1,7 @@
 section\<open>T1 and Hausdorff spaces\<close>
 
 theory T1_Spaces
-imports Product_Topology 
+imports Product_Topology
 begin
 
 section\<open>T1 spaces with equivalences to many naturally "nice" properties. \<close>
@@ -592,24 +592,6 @@
   using closed_injective_imp_proper_map closed_map_paired_continuous_map_left
   by (metis (mono_tags, lifting) Pair_inject inj_onI)
 
-lemma Hausdorff_space_euclidean [simp]: "Hausdorff_space (euclidean :: 'a::metric_space topology)"
-proof -
-  have "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> disjnt U V"
-    if "x \<noteq> y"
-    for x y :: 'a
-  proof (intro exI conjI)
-    let ?r = "dist x y / 2"
-    have [simp]: "?r > 0"
-      by (simp add: that)
-    show "open (ball x ?r)" "open (ball y ?r)" "x \<in> (ball x ?r)" "y \<in> (ball y ?r)"
-      by (auto simp add: that)
-    show "disjnt (ball x ?r) (ball y ?r)"
-      unfolding disjnt_def by (simp add: disjoint_ballI)
-  qed
-  then show ?thesis
-    by (simp add: Hausdorff_space_def)
-qed
-
 lemma Hausdorff_space_prod_topology:
   "Hausdorff_space(prod_topology X Y) \<longleftrightarrow> topspace(prod_topology X Y) = {} \<or> Hausdorff_space X \<and> Hausdorff_space Y"
   (is "?lhs = ?rhs")
diff -r 0aaf16a0f7cc -r 3548d54ce3ee src/HOL/Homology/Simplices.thy
--- a/src/HOL/Homology/Simplices.thy	Mon Dec 02 14:07:42 2019 -0500
+++ b/src/HOL/Homology/Simplices.thy	Mon Dec 02 22:40:16 2019 -0500
@@ -1,8 +1,10 @@
 section\<open>Homology, I: Simplices\<close>
 
 theory "Simplices"
-  imports "HOL-Analysis.Abstract_Euclidean_Space" "HOL-Algebra.Free_Abelian_Groups"
-
+  imports
+    "HOL-Analysis.Function_Metric"
+    "HOL-Analysis.Abstract_Euclidean_Space"
+    "HOL-Algebra.Free_Abelian_Groups"
 begin
 
 subsection\<open>Standard simplices, all of which are topological subspaces of @{text"R^n"}.      \<close>