summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | immler |

Mon, 02 Dec 2019 14:52:21 -0500 | |

changeset 71401 | 1c7e559eb9fa |

parent 71400 | 0aaf16a0f7cc |

split off metric spaces part of Function_Topology: subsequent theories Product_Topology, T1_Spaces, Lindelof_Spaces are purely topological

--- 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 14:52:21 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

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Analysis/Function_Metric.thy Mon Dec 02 14:52:21 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

--- 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 14:52:21 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>

--- 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 14:52:21 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>

--- 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 14:52:21 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>

--- 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 14:52:21 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")