more stuff from HOL Light: Euclidean spaces and n-spheres, Hausdorff spaces, etc.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Abstract_Euclidean_Space.thy Wed Mar 27 14:08:26 2019 +0000
@@ -0,0 +1,345 @@
+(* Author: LCP, ported from HOL Light
+*)
+
+section\<open>Euclidean space and n-spheres, as subtopologies of n-dimensional space\<close>
+
+theory Abstract_Euclidean_Space
+imports Homotopy Locally T1_Spaces
+begin
+
+subsection \<open>Euclidean spaces as abstract topologies\<close>
+
+definition Euclidean_space :: "nat \<Rightarrow> (nat \<Rightarrow> real) topology"
+ where "Euclidean_space n \<equiv> subtopology (powertop_real UNIV) {x. \<forall>i\<ge>n. x i = 0}"
+
+lemma topspace_Euclidean_space:
+ "topspace(Euclidean_space n) = {x. \<forall>i\<ge>n. x i = 0}"
+ by (simp add: Euclidean_space_def)
+
+lemma nonempty_Euclidean_space: "topspace(Euclidean_space n) \<noteq> {}"
+ by (force simp: topspace_Euclidean_space)
+
+lemma subset_Euclidean_space [simp]:
+ "topspace(Euclidean_space m) \<subseteq> topspace(Euclidean_space n) \<longleftrightarrow> m \<le> n"
+ apply (simp add: topspace_Euclidean_space subset_iff, safe)
+ apply (drule_tac x="(\<lambda>i. if i < m then 1 else 0)" in spec)
+ apply auto
+ using not_less by fastforce
+
+lemma topspace_Euclidean_space_alt:
+ "topspace(Euclidean_space n) = (\<Inter>i \<in> {n..}. {x. x \<in> topspace(powertop_real UNIV) \<and> x i \<in> {0}})"
+ by (auto simp: topspace_Euclidean_space)
+
+lemma closedin_Euclidean_space:
+ "closedin (powertop_real UNIV) (topspace(Euclidean_space n))"
+proof -
+ have "closedin (powertop_real UNIV) {x. x i = 0}" if "n \<le> i" for i
+ proof -
+ have "closedin (powertop_real UNIV) {x \<in> topspace (powertop_real UNIV). x i \<in> {0}}"
+ proof (rule closedin_continuous_map_preimage)
+ show "continuous_map (powertop_real UNIV) euclideanreal (\<lambda>x. x i)"
+ by (metis UNIV_I continuous_map_product_coordinates)
+ show "closedin euclideanreal {0}"
+ by simp
+ qed
+ then show ?thesis
+ by auto
+ qed
+ then show ?thesis
+ unfolding topspace_Euclidean_space_alt
+ by force
+qed
+
+lemma closedin_Euclidean_imp_closed: "closedin (Euclidean_space m) S \<Longrightarrow> closed S"
+ by (metis Euclidean_space_def closed_closedin closedin_Euclidean_space closedin_closed_subtopology euclidean_product_topology topspace_Euclidean_space)
+
+lemma closedin_Euclidean_space_iff:
+ "closedin (Euclidean_space m) S \<longleftrightarrow> closed S \<and> S \<subseteq> topspace (Euclidean_space m)"
+ (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+ show "?lhs \<Longrightarrow> ?rhs"
+ using closedin_closed_subtopology topspace_Euclidean_space
+ by (fastforce simp: topspace_Euclidean_space_alt closedin_Euclidean_imp_closed)
+ show "?rhs \<Longrightarrow> ?lhs"
+ apply (simp add: closedin_subtopology Euclidean_space_def)
+ by (metis (no_types) closed_closedin euclidean_product_topology inf.orderE)
+qed
+
+lemma continuous_map_componentwise_Euclidean_space:
+ "continuous_map X (Euclidean_space n) (\<lambda>x i. if i < n then f x i else 0) \<longleftrightarrow>
+ (\<forall>i < n. continuous_map X euclideanreal (\<lambda>x. f x i))"
+proof -
+ have *: "continuous_map X euclideanreal (\<lambda>x. if k < n then f x k else 0)"
+ if "\<And>i. i<n \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x i)" for k
+ by (intro continuous_intros that)
+ show ?thesis
+ unfolding Euclidean_space_def continuous_map_in_subtopology
+ by (fastforce simp: continuous_map_componentwise_UNIV * elim: continuous_map_eq)
+qed
+
+lemma continuous_map_Euclidean_space_add [continuous_intros]:
+ "\<lbrakk>continuous_map X (Euclidean_space n) f; continuous_map X (Euclidean_space n) g\<rbrakk>
+ \<Longrightarrow> continuous_map X (Euclidean_space n) (\<lambda>x i. f x i + g x i)"
+ unfolding Euclidean_space_def continuous_map_in_subtopology
+ by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_real_add)
+
+lemma continuous_map_Euclidean_space_diff [continuous_intros]:
+ "\<lbrakk>continuous_map X (Euclidean_space n) f; continuous_map X (Euclidean_space n) g\<rbrakk>
+ \<Longrightarrow> continuous_map X (Euclidean_space n) (\<lambda>x i. f x i - g x i)"
+ unfolding Euclidean_space_def continuous_map_in_subtopology
+ by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_real_diff)
+
+lemma homeomorphic_Euclidean_space_product_topology:
+ "Euclidean_space n homeomorphic_space product_topology (\<lambda>i. euclideanreal) {..<n}"
+proof -
+ have cm: "continuous_map (product_topology (\<lambda>i. euclideanreal) {..<n})
+ euclideanreal (\<lambda>x. if k < n then x k else 0)" for k
+ by (auto intro: continuous_map_if continuous_map_product_projection)
+ show ?thesis
+ unfolding homeomorphic_space_def homeomorphic_maps_def
+ apply (rule_tac x="\<lambda>f. restrict f {..<n}" in exI)
+ apply (rule_tac x="\<lambda>f i. if i < n then f i else 0" in exI)
+ apply (simp add: Euclidean_space_def topspace_subtopology continuous_map_in_subtopology)
+ apply (intro conjI continuous_map_from_subtopology)
+ apply (force simp: continuous_map_componentwise cm intro: continuous_map_product_projection)+
+ done
+qed
+
+lemma contractible_Euclidean_space [simp]: "contractible_space (Euclidean_space n)"
+ using homeomorphic_Euclidean_space_product_topology contractible_space_euclideanreal
+ contractible_space_product_topology homeomorphic_space_contractibility by blast
+
+lemma path_connected_Euclidean_space: "path_connected_space (Euclidean_space n)"
+ by (simp add: contractible_imp_path_connected_space)
+
+lemma connected_Euclidean_space: "connected_space (Euclidean_space n)"
+ by (simp add: contractible_Euclidean_space contractible_imp_connected_space)
+
+lemma locally_path_connected_Euclidean_space:
+ "locally_path_connected_space (Euclidean_space n)"
+ apply (simp add: homeomorphic_locally_path_connected_space [OF homeomorphic_Euclidean_space_product_topology [of n]]
+ locally_path_connected_space_product_topology)
+ using locally_path_connected_space_euclideanreal by auto
+
+lemma compact_Euclidean_space:
+ "compact_space (Euclidean_space n) \<longleftrightarrow> n = 0"
+ by (auto simp: homeomorphic_compact_space [OF homeomorphic_Euclidean_space_product_topology] compact_space_product_topology)
+
+subsection\<open>n-dimensional spheres\<close>
+
+definition nsphere where
+ "nsphere n \<equiv> subtopology (Euclidean_space (Suc n)) { x. (\<Sum>i\<le>n. x i ^ 2) = 1 }"
+
+lemma nsphere:
+ "nsphere n = subtopology (powertop_real UNIV)
+ {x. (\<Sum>i\<le>n. x i ^ 2) = 1 \<and> (\<forall>i>n. x i = 0)}"
+ by (simp add: nsphere_def Euclidean_space_def subtopology_subtopology Suc_le_eq Collect_conj_eq Int_commute)
+
+lemma continuous_map_nsphere_projection: "continuous_map (nsphere n) euclideanreal (\<lambda>x. x k)"
+ unfolding nsphere
+ by (blast intro: continuous_map_from_subtopology [OF continuous_map_product_projection])
+
+lemma in_topspace_nsphere: "(\<lambda>n. if n = 0 then 1 else 0) \<in> topspace (nsphere n)"
+ by (simp add: nsphere_def topspace_Euclidean_space power2_eq_square if_distrib [where f = "\<lambda>x. x * _"] cong: if_cong)
+
+lemma nonempty_nsphere [simp]: "~ (topspace(nsphere n) = {})"
+ using in_topspace_nsphere by auto
+
+lemma subtopology_nsphere_equator:
+ "subtopology (nsphere (Suc n)) {x. x(Suc n) = 0} = nsphere n"
+proof -
+ have "({x. (\<Sum>i\<le>n. (x i)\<^sup>2) + (x (Suc n))\<^sup>2 = 1 \<and> (\<forall>i>Suc n. x i = 0)} \<inter> {x. x (Suc n) = 0})
+ = {x. (\<Sum>i\<le>n. (x i)\<^sup>2) = 1 \<and> (\<forall>i>n. x i = (0::real))}"
+ using Suc_lessI [of n] by (fastforce simp: set_eq_iff)
+ then show ?thesis
+ by (simp add: nsphere subtopology_subtopology)
+qed
+
+lemma continuous_map_nsphere_reflection:
+ "continuous_map (nsphere n) (nsphere n) (\<lambda>x i. if i = k then -x i else x i)"
+proof -
+ have cm: "continuous_map (powertop_real UNIV)
+ euclideanreal (\<lambda>x. if j = k then - x j else x j)" for j
+ proof (cases "j=k")
+ case True
+ then show ?thesis
+ by simp (metis UNIV_I continuous_map_product_projection continuous_map_real_minus)
+ next
+ case False
+ then show ?thesis
+ by (auto intro: continuous_map_product_projection)
+ qed
+ have eq: "(if i = k then x k * x k else x i * x i) = x i * x i" for i and x :: "nat \<Rightarrow> real"
+ by simp
+ show ?thesis
+ apply (simp add: nsphere continuous_map_in_subtopology continuous_map_componentwise_UNIV
+ continuous_map_from_subtopology cm topspace_subtopology)
+ apply (intro conjI allI impI continuous_intros continuous_map_from_subtopology continuous_map_product_projection)
+ apply (auto simp: power2_eq_square if_distrib [where f = "\<lambda>x. x * _"] eq cong: if_cong)
+ done
+qed
+
+
+proposition contractible_space_upper_hemisphere:
+ assumes "k \<le> n"
+ shows "contractible_space(subtopology (nsphere n) {x. x k \<ge> 0})"
+proof -
+ define p:: "nat \<Rightarrow> real" where "p \<equiv> \<lambda>i. if i = k then 1 else 0"
+ have "p \<in> topspace(nsphere n)"
+ using assms
+ by (simp add: nsphere topspace_subtopology p_def power2_eq_square if_distrib [where f = "\<lambda>x. x * _"] cong: if_cong)
+ let ?g = "\<lambda>x i. x i / sqrt(\<Sum>j\<le>n. x j ^ 2)"
+ let ?h = "\<lambda>(t,q) i. (1 - t) * q i + t * p i"
+ let ?Y = "subtopology (Euclidean_space (Suc n)) {x. 0 \<le> x k \<and> (\<exists>i\<le>n. x i \<noteq> 0)}"
+ have "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (nsphere n) {x. 0 \<le> x k}))
+ (subtopology (nsphere n) {x. 0 \<le> x k}) (?g \<circ> ?h)"
+ proof (rule continuous_map_compose)
+ have *: "\<lbrakk>0 \<le> b k; (\<Sum>i\<le>n. (b i)\<^sup>2) = 1; \<forall>i>n. b i = 0; 0 \<le> a; a \<le> 1\<rbrakk>
+ \<Longrightarrow> \<exists>i. (i = k \<longrightarrow> (1 - a) * b k + a \<noteq> 0) \<and>
+ (i \<noteq> k \<longrightarrow> i \<le> n \<and> a \<noteq> 1 \<and> b i \<noteq> 0)" for a::real and b
+ apply (cases "a \<noteq> 1 \<and> b k = 0"; simp)
+ apply (metis (no_types, lifting) atMost_iff sum.neutral zero_power2)
+ by (metis add.commute add_le_same_cancel2 diff_ge_0_iff_ge diff_zero less_eq_real_def mult_eq_0_iff mult_nonneg_nonneg not_le numeral_One zero_neq_numeral)
+ show "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (nsphere n) {x. 0 \<le> x k})) ?Y ?h"
+ using assms
+ apply (auto simp: * nsphere topspace_subtopology continuous_map_componentwise_UNIV
+ prod_topology_subtopology subtopology_subtopology case_prod_unfold
+ continuous_map_in_subtopology Euclidean_space_def p_def if_distrib [where f = "\<lambda>x. _ * x"] cong: if_cong)
+ apply (intro continuous_map_prod_snd continuous_intros continuous_map_from_subtopology)
+ apply auto
+ done
+ next
+ have 1: "\<And>x i. \<lbrakk> i \<le> n; x i \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i\<le>n. (x i / sqrt (\<Sum>j\<le>n. (x j)\<^sup>2))\<^sup>2) = 1"
+ by (force simp: sum_nonneg sum_nonneg_eq_0_iff divide_simps simp flip: sum_divide_distrib)
+ have cm: "continuous_map ?Y (nsphere n) (\<lambda>x i. x i / sqrt (\<Sum>j\<le>n. (x j)\<^sup>2))"
+ unfolding Euclidean_space_def nsphere subtopology_subtopology continuous_map_in_subtopology
+ proof (intro continuous_intros conjI)
+ show "continuous_map
+ (subtopology (powertop_real UNIV) ({x. \<forall>i\<ge>Suc n. x i = 0} \<inter> {x. 0 \<le> x k \<and> (\<exists>i\<le>n. x i \<noteq> 0)}))
+ (powertop_real UNIV) (\<lambda>x i. x i / sqrt (\<Sum>j\<le>n. (x j)\<^sup>2))"
+ unfolding continuous_map_componentwise
+ by (intro continuous_intros conjI ballI) (auto simp: sum_nonneg_eq_0_iff)
+ qed (auto simp: 1)
+ show "continuous_map ?Y (subtopology (nsphere n) {x. 0 \<le> x k}) (\<lambda>x i. x i / sqrt (\<Sum>j\<le>n. (x j)\<^sup>2))"
+ by (force simp: cm sum_nonneg continuous_map_in_subtopology if_distrib [where f = "\<lambda>x. _ * x"] cong: if_cong)
+ qed
+ moreover have "(?g \<circ> ?h) (0, x) = x"
+ if "x \<in> topspace (subtopology (nsphere n) {x. 0 \<le> x k})" for x
+ using that
+ by (simp add: assms topspace_subtopology nsphere)
+ moreover
+ have "(?g \<circ> ?h) (1, x) = p"
+ if "x \<in> topspace (subtopology (nsphere n) {x. 0 \<le> x k})" for x
+ by (force simp: assms p_def power2_eq_square if_distrib [where f = "\<lambda>x. x * _"] cong: if_cong)
+ ultimately
+ show ?thesis
+ apply (simp add: contractible_space_def homotopic_with)
+ apply (rule_tac x=p in exI)
+ apply (rule_tac x="?g \<circ> ?h" in exI, force)
+ done
+qed
+
+
+corollary contractible_space_lower_hemisphere:
+ assumes "k \<le> n"
+ shows "contractible_space(subtopology (nsphere n) {x. x k \<le> 0})"
+proof -
+ have "contractible_space (subtopology (nsphere n) {x. 0 \<le> x k}) = ?thesis"
+ proof (rule homeomorphic_space_contractibility)
+ show "subtopology (nsphere n) {x. 0 \<le> x k} homeomorphic_space subtopology (nsphere n) {x. x k \<le> 0}"
+ unfolding homeomorphic_space_def homeomorphic_maps_def
+ apply (rule_tac x="\<lambda>x i. if i = k then -(x i) else x i" in exI)+
+ apply (auto simp: continuous_map_in_subtopology continuous_map_from_subtopology
+ continuous_map_nsphere_reflection)
+ done
+ qed
+ then show ?thesis
+ using contractible_space_upper_hemisphere [OF assms] by metis
+qed
+
+
+proposition nullhomotopic_nonsurjective_sphere_map:
+ assumes f: "continuous_map (nsphere p) (nsphere p) f"
+ and fim: "f ` (topspace(nsphere p)) \<noteq> topspace(nsphere p)"
+ obtains a where "homotopic_with (\<lambda>x. True) (nsphere p) (nsphere p) f (\<lambda>x. a)"
+proof -
+ obtain a where a: "a \<in> topspace(nsphere p)" "a \<notin> f ` (topspace(nsphere p))"
+ using fim continuous_map_image_subset_topspace f by blast
+ then have a1: "(\<Sum>i\<le>p. (a i)\<^sup>2) = 1" and a0: "\<And>i. i > p \<Longrightarrow> a i = 0"
+ by (simp_all add: nsphere)
+ have f1: "(\<Sum>j\<le>p. (f x j)\<^sup>2) = 1" if "x \<in> topspace (nsphere p)" for x
+ proof -
+ have "f x \<in> topspace (nsphere p)"
+ using continuous_map_image_subset_topspace f that by blast
+ then show ?thesis
+ by (simp add: nsphere)
+ qed
+ show thesis
+ proof
+ let ?g = "\<lambda>x i. x i / sqrt(\<Sum>j\<le>p. x j ^ 2)"
+ let ?h = "\<lambda>(t,x) i. (1 - t) * f x i - t * a i"
+ let ?Y = "subtopology (Euclidean_space(Suc p)) (- {\<lambda>i. 0})"
+ let ?T01 = "top_of_set {0..1::real}"
+ have 1: "continuous_map (prod_topology ?T01 (nsphere p)) (nsphere p) (?g \<circ> ?h)"
+ proof (rule continuous_map_compose)
+ have "continuous_map (prod_topology ?T01 (nsphere p)) euclideanreal ((\<lambda>x. f x k) \<circ> snd)" for k
+ unfolding nsphere
+ apply (simp add: continuous_map_of_snd)
+ apply (rule continuous_map_compose [of _ "nsphere p" f, unfolded o_def])
+ using f apply (simp add: nsphere)
+ by (simp add: continuous_map_nsphere_projection)
+ then have "continuous_map (prod_topology ?T01 (nsphere p)) euclideanreal (\<lambda>r. ?h r k)"
+ for k
+ unfolding case_prod_unfold o_def
+ by (intro continuous_map_into_fulltopology [OF continuous_map_fst] continuous_intros) auto
+ moreover have "?h ` ({0..1} \<times> topspace (nsphere p)) \<subseteq> {x. \<forall>i\<ge>Suc p. x i = 0}"
+ using continuous_map_image_subset_topspace [OF f]
+ by (auto simp: nsphere image_subset_iff a0)
+ moreover have "(\<lambda>i. 0) \<notin> ?h ` ({0..1} \<times> topspace (nsphere p))"
+ proof clarify
+ fix t b
+ assume eq: "(\<lambda>i. 0) = (\<lambda>i. (1 - t) * f b i - t * a i)" and "t \<in> {0..1}" and b: "b \<in> topspace (nsphere p)"
+ have "(1 - t)\<^sup>2 = (\<Sum>i\<le>p. ((1 - t) * f b i)^2)"
+ using f1 [OF b] by (simp add: power_mult_distrib flip: sum_distrib_left)
+ also have "\<dots> = (\<Sum>i\<le>p. (t * a i)^2)"
+ using eq by (simp add: fun_eq_iff)
+ also have "\<dots> = t\<^sup>2"
+ using a1 by (simp add: power_mult_distrib flip: sum_distrib_left)
+ finally have "1 - t = t"
+ by (simp add: power2_eq_iff)
+ then have *: "t = 1/2"
+ by simp
+ have fba: "f b \<noteq> a"
+ using a(2) b by blast
+ then show False
+ using eq unfolding * by (simp add: fun_eq_iff)
+ qed
+ ultimately show "continuous_map (prod_topology ?T01 (nsphere p)) ?Y ?h"
+ by (simp add: Euclidean_space_def continuous_map_in_subtopology continuous_map_componentwise_UNIV)
+ next
+ have *: "\<lbrakk>\<forall>i\<ge>Suc p. x i = 0; x \<noteq> (\<lambda>i. 0)\<rbrakk> \<Longrightarrow> (\<Sum>j\<le>p. (x j)\<^sup>2) \<noteq> 0" for x :: "nat \<Rightarrow> real"
+ by (force simp: fun_eq_iff not_less_eq_eq sum_nonneg_eq_0_iff)
+ show "continuous_map ?Y (nsphere p) ?g"
+ apply (simp add: Euclidean_space_def continuous_map_in_subtopology continuous_map_componentwise_UNIV
+ nsphere continuous_map_componentwise subtopology_subtopology)
+ apply (intro conjI allI continuous_intros continuous_map_from_subtopology [OF continuous_map_product_projection])
+ apply (simp_all add: *)
+ apply (force simp: sum_nonneg fun_eq_iff not_less_eq_eq sum_nonneg_eq_0_iff power_divide simp flip: sum_divide_distrib)
+ done
+ qed
+ have 2: "(?g \<circ> ?h) (0, x) = f x" if "x \<in> topspace (nsphere p)" for x
+ using that f1 by simp
+ have 3: "(?g \<circ> ?h) (1, x) = (\<lambda>i. - a i)" for x
+ using a by (force simp: divide_simps nsphere)
+ then show "homotopic_with (\<lambda>x. True) (nsphere p) (nsphere p) f (\<lambda>x. (\<lambda>i. - a i))"
+ by (force simp: homotopic_with intro: 1 2 3)
+ qed
+qed
+
+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)
+
+end
+
--- a/src/HOL/Analysis/Abstract_Topology.thy Tue Mar 26 22:18:30 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy Wed Mar 27 14:08:26 2019 +0000
@@ -161,6 +161,12 @@
apply (metis openin_subset subset_eq)
done
+lemma topology_finer_closedin:
+ "topspace X = topspace Y \<Longrightarrow> (\<forall>S. openin Y S \<longrightarrow> openin X S) \<longleftrightarrow> (\<forall>S. closedin Y S \<longrightarrow> closedin X S)"
+ apply safe
+ apply (simp add: closedin_def)
+ by (simp add: openin_closedin_eq)
+
lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))"
by (simp add: openin_closedin_eq)
@@ -1611,7 +1617,7 @@
declare continuous_map_const [THEN iffD2, continuous_intros]
-lemma continuous_map_compose:
+lemma continuous_map_compose [continuous_intros]:
assumes f: "continuous_map X X' f" and g: "continuous_map X' X'' g"
shows "continuous_map X X'' (g \<circ> f)"
unfolding continuous_map_def
@@ -1711,10 +1717,10 @@
"continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. sqrt(f x))"
by (meson continuous_map_compose continuous_map_eq continuous_map_square_root o_apply)
-lemma continuous_map_id [simp]: "continuous_map X X id"
+lemma continuous_map_id [simp, continuous_intros]: "continuous_map X X id"
unfolding continuous_map_def using openin_subopen topspace_def by fastforce
-declare continuous_map_id [unfolded id_def, simp]
+declare continuous_map_id [unfolded id_def, simp, continuous_intros]
lemma continuous_map_id_subt [simp]: "continuous_map (subtopology X S) X id"
by (simp add: continuous_map_from_subtopology)
--- a/src/HOL/Analysis/Analysis.thy Tue Mar 26 22:18:30 2019 +0100
+++ b/src/HOL/Analysis/Analysis.thy Wed Mar 27 14:08:26 2019 +0000
@@ -6,7 +6,7 @@
(* Topology *)
Connected
Abstract_Limits
- Locally
+ Abstract_Euclidean_Space
(* Functional Analysis *)
Elementary_Normed_Spaces
Norm_Arith
--- a/src/HOL/Analysis/Function_Topology.thy Tue Mar 26 22:18:30 2019 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy Wed Mar 27 14:08:26 2019 +0000
@@ -78,6 +78,9 @@
where "product_topology T I =
topology_generated_by {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
+abbreviation powertop_real :: "'a set \<Rightarrow> ('a \<Rightarrow> real) topology"
+ where "powertop_real \<equiv> product_topology (\<lambda>i. euclideanreal)"
+
text \<open>The total set of the product topology is the product of the total sets
along each coordinate.\<close>
@@ -1994,5 +1997,55 @@
PiE I S = {} \<or> (\<forall>i \<in> I. path_connectedin (X i) (S i))"
by (fastforce simp add: path_connectedin_def subtopology_PiE path_connected_space_product_topology subset_PiE PiE_eq_empty_iff topspace_subtopology_subset)
+subsection \<open>Projections from a function topology to a component\<close>
+
+lemma quotient_map_product_projection:
+ assumes "i \<in> I"
+ shows "quotient_map(product_topology X I) (X i) (\<lambda>x. x i) \<longleftrightarrow>
+ (topspace(product_topology X I) = {} \<longrightarrow> topspace(X i) = {})"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs with assms show ?rhs
+ by (auto simp: continuous_open_quotient_map open_map_product_projection)
+next
+ assume ?rhs with assms show ?lhs
+ by (auto simp: Abstract_Topology.retraction_imp_quotient_map retraction_map_product_projection)
+qed
+
+lemma product_topology_homeomorphic_component:
+ assumes "i \<in> I" "\<And>j. \<lbrakk>j \<in> I; j \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>a. topspace(X j) = {a}"
+ shows "product_topology X I homeomorphic_space (X i)"
+proof -
+ have "quotient_map (product_topology X I) (X i) (\<lambda>x. x i)"
+ using assms by (force simp add: quotient_map_product_projection PiE_eq_empty_iff)
+ moreover
+ have "inj_on (\<lambda>x. x i) (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+ using assms by (auto simp: inj_on_def PiE_iff) (metis extensionalityI singletonD)
+ ultimately show ?thesis
+ unfolding homeomorphic_space_def
+ by (rule_tac x="\<lambda>x. x i" in exI) (simp add: homeomorphic_map_def flip: homeomorphic_map_maps)
+qed
+
+lemma topological_property_of_product_component:
+ assumes major: "P (product_topology X I)"
+ and minor: "\<And>z i. \<lbrakk>z \<in> (\<Pi>\<^sub>E i\<in>I. topspace(X i)); P(product_topology X I); i \<in> I\<rbrakk>
+ \<Longrightarrow> P(subtopology (product_topology X I) (PiE I (\<lambda>j. if j = i then topspace(X i) else {z j})))"
+ (is "\<And>z i. \<lbrakk>_; _; _\<rbrakk> \<Longrightarrow> P (?SX z i)")
+ and PQ: "\<And>X X'. X homeomorphic_space X' \<Longrightarrow> (P X \<longleftrightarrow> Q X')"
+ shows "(\<Pi>\<^sub>E i\<in>I. topspace(X i)) = {} \<or> (\<forall>i \<in> I. Q(X i))"
+proof -
+ have "Q(X i)" if "(\<Pi>\<^sub>E i\<in>I. topspace(X i)) \<noteq> {}" "i \<in> I" for i
+ proof -
+ from that obtain f where f: "f \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+ by force
+ have "?SX f i homeomorphic_space X i"
+ apply (simp add: subtopology_PiE )
+ using product_topology_homeomorphic_component [OF \<open>i \<in> I\<close>, of "\<lambda>j. subtopology (X j) (if j = i then topspace (X i) else {f j})"]
+ using f by fastforce
+ then show ?thesis
+ using minor [OF f major \<open>i \<in> I\<close>] PQ by auto
+ qed
+ then show ?thesis by metis
+qed
end
--- a/src/HOL/Analysis/Product_Topology.thy Tue Mar 26 22:18:30 2019 +0100
+++ b/src/HOL/Analysis/Product_Topology.thy Wed Mar 27 14:08:26 2019 +0000
@@ -214,6 +214,14 @@
lemma continuous_map_snd_of [continuous_intros]:
"continuous_map Z (prod_topology X Y) f \<Longrightarrow> continuous_map Z Y (snd \<circ> f)"
by (simp add: continuous_map_pairwise)
+
+lemma continuous_map_prod_fst:
+ "i \<in> I \<Longrightarrow> continuous_map (prod_topology (product_topology (\<lambda>i. Y) I) X) Y (\<lambda>x. fst x i)"
+ using continuous_map_componentwise_UNIV continuous_map_fst by fastforce
+
+lemma continuous_map_prod_snd:
+ "i \<in> I \<Longrightarrow> continuous_map (prod_topology X (product_topology (\<lambda>i. Y) I)) Y (\<lambda>x. snd x i)"
+ using continuous_map_componentwise_UNIV continuous_map_snd by fastforce
lemma continuous_map_if_iff [simp]: "continuous_map X Y (\<lambda>x. if P then f x else g x) \<longleftrightarrow> continuous_map X Y (if P then f else g)"
by simp
--- a/src/HOL/Analysis/T1_Spaces.thy Tue Mar 26 22:18:30 2019 +0100
+++ b/src/HOL/Analysis/T1_Spaces.thy Wed Mar 27 14:08:26 2019 +0000
@@ -1,9 +1,11 @@
-section\<open>T1 spaces with equivalences to many naturally "nice" properties. \<close>
+section\<open>T1 and Hausdorff spaces\<close>
theory T1_Spaces
imports Product_Topology
begin
+section\<open>T1 spaces with equivalences to many naturally "nice" properties. \<close>
+
definition t1_space where
"t1_space X \<equiv> \<forall>x \<in> topspace X. \<forall>y \<in> topspace X. x\<noteq>y \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> y \<notin> U)"
@@ -214,4 +216,442 @@
by simp
qed
+subsection\<open>Hausdorff Spaces\<close>
+
+definition Hausdorff_space
+ where
+ "Hausdorff_space X \<equiv>
+ \<forall>x y. x \<in> topspace X \<and> y \<in> topspace X \<and> (x \<noteq> y)
+ \<longrightarrow> (\<exists>U V. openin X U \<and> openin X V \<and> x \<in> U \<and> y \<in> V \<and> disjnt U V)"
+
+lemma Hausdorff_space_expansive:
+ "\<lbrakk>Hausdorff_space X; topspace X = topspace Y; \<And>U. openin X U \<Longrightarrow> openin Y U\<rbrakk> \<Longrightarrow> Hausdorff_space Y"
+ by (metis Hausdorff_space_def)
+
+lemma Hausdorff_space_topspace_empty:
+ "topspace X = {} \<Longrightarrow> Hausdorff_space X"
+ by (simp add: Hausdorff_space_def)
+
+lemma Hausdorff_imp_t1_space:
+ "Hausdorff_space X \<Longrightarrow> t1_space X"
+ by (metis Hausdorff_space_def disjnt_iff t1_space_def)
+
+lemma closedin_derived_set_of:
+ "Hausdorff_space X \<Longrightarrow> closedin X (X derived_set_of S)"
+ by (simp add: Hausdorff_imp_t1_space closedin_derived_set_of_gen)
+
+lemma t1_or_Hausdorff_space:
+ "t1_space X \<or> Hausdorff_space X \<longleftrightarrow> t1_space X"
+ using Hausdorff_imp_t1_space by blast
+
+lemma Hausdorff_space_sing_Inter_opens:
+ "\<lbrakk>Hausdorff_space X; a \<in> topspace X\<rbrakk> \<Longrightarrow> \<Inter>{u. openin X u \<and> a \<in> u} = {a}"
+ using Hausdorff_imp_t1_space t1_space_singleton_Inter_open by force
+
+lemma Hausdorff_space_subtopology:
+ assumes "Hausdorff_space X" shows "Hausdorff_space(subtopology X S)"
+proof -
+ have *: "disjnt U V \<Longrightarrow> disjnt (S \<inter> U) (S \<inter> V)" for U V
+ by (simp add: disjnt_iff)
+ from assms show ?thesis
+ apply (simp add: Hausdorff_space_def openin_subtopology_alt)
+ apply (fast intro: * elim!: all_forward)
+ done
+qed
+
+lemma Hausdorff_space_compact_separation:
+ assumes X: "Hausdorff_space X" and S: "compactin X S" and T: "compactin X T" and "disjnt S T"
+ obtains U V where "openin X U" "openin X V" "S \<subseteq> U" "T \<subseteq> V" "disjnt U V"
+proof (cases "S = {}")
+ case True
+ then show thesis
+ by (metis \<open>compactin X T\<close> compactin_subset_topspace disjnt_empty1 empty_subsetI openin_empty openin_topspace that)
+next
+ case False
+ have "\<forall>x \<in> S. \<exists>U V. openin X U \<and> openin X V \<and> x \<in> U \<and> T \<subseteq> V \<and> disjnt U V"
+ proof
+ fix a
+ assume "a \<in> S"
+ then have "a \<notin> T"
+ by (meson assms(4) disjnt_iff)
+ have a: "a \<in> topspace X"
+ using S \<open>a \<in> S\<close> compactin_subset_topspace by blast
+ show "\<exists>U V. openin X U \<and> openin X V \<and> a \<in> U \<and> T \<subseteq> V \<and> disjnt U V"
+ proof (cases "T = {}")
+ case True
+ then show ?thesis
+ using a disjnt_empty2 openin_empty by blast
+ next
+ case False
+ have "\<forall>x \<in> topspace X - {a}. \<exists>U V. openin X U \<and> openin X V \<and> x \<in> U \<and> a \<in> V \<and> disjnt U V"
+ using X a by (simp add: Hausdorff_space_def)
+ then obtain U V where UV: "\<forall>x \<in> topspace X - {a}. openin X (U x) \<and> openin X (V x) \<and> x \<in> U x \<and> a \<in> V x \<and> disjnt (U x) (V x)"
+ by metis
+ with \<open>a \<notin> T\<close> compactin_subset_topspace [OF T]
+ have Topen: "\<forall>W \<in> U ` T. openin X W" and Tsub: "T \<subseteq> \<Union> (U ` T)"
+ by (auto simp: )
+ then obtain \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> U ` T" and "T \<subseteq> \<Union>\<F>"
+ using T unfolding compactin_def by meson
+ then obtain F where F: "finite F" "F \<subseteq> T" "\<F> = U ` F" and SUF: "T \<subseteq> \<Union>(U ` F)" and "a \<notin> F"
+ using finite_subset_image [OF \<F>] \<open>a \<notin> T\<close> by (metis subsetD)
+ have U: "\<And>x. \<lbrakk>x \<in> topspace X; x \<noteq> a\<rbrakk> \<Longrightarrow> openin X (U x)"
+ and V: "\<And>x. \<lbrakk>x \<in> topspace X; x \<noteq> a\<rbrakk> \<Longrightarrow> openin X (V x)"
+ and disj: "\<And>x. \<lbrakk>x \<in> topspace X; x \<noteq> a\<rbrakk> \<Longrightarrow> disjnt (U x) (V x)"
+ using UV by blast+
+ show ?thesis
+ proof (intro exI conjI)
+ have "F \<noteq> {}"
+ using False SUF by blast
+ with \<open>a \<notin> F\<close> show "openin X (\<Inter>(V ` F))"
+ using F compactin_subset_topspace [OF T] by (force intro: V)
+ show "openin X (\<Union>(U ` F))"
+ using F Topen Tsub by (force intro: U)
+ show "disjnt (\<Inter>(V ` F)) (\<Union>(U ` F))"
+ using disj
+ apply (auto simp: disjnt_def)
+ using \<open>F \<subseteq> T\<close> \<open>a \<notin> F\<close> compactin_subset_topspace [OF T] by blast
+ show "a \<in> (\<Inter>(V ` F))"
+ using \<open>F \<subseteq> T\<close> T UV \<open>a \<notin> T\<close> compactin_subset_topspace by blast
+ qed (auto simp: SUF)
+ qed
+ qed
+ then obtain U V where UV: "\<forall>x \<in> S. openin X (U x) \<and> openin X (V x) \<and> x \<in> U x \<and> T \<subseteq> V x \<and> disjnt (U x) (V x)"
+ by metis
+ then have "S \<subseteq> \<Union> (U ` S)"
+ by auto
+ moreover have "\<forall>W \<in> U ` S. openin X W"
+ using UV by blast
+ ultimately obtain I where I: "S \<subseteq> \<Union> (U ` I)" "I \<subseteq> S" "finite I"
+ by (metis S compactin_def finite_subset_image)
+ show thesis
+ proof
+ show "openin X (\<Union>(U ` I))"
+ using \<open>I \<subseteq> S\<close> UV by blast
+ show "openin X (\<Inter> (V ` I))"
+ using False UV \<open>I \<subseteq> S\<close> \<open>S \<subseteq> \<Union> (U ` I)\<close> \<open>finite I\<close> by blast
+ show "disjnt (\<Union>(U ` I)) (\<Inter> (V ` I))"
+ by simp (meson UV \<open>I \<subseteq> S\<close> disjnt_subset2 in_mono le_INF_iff order_refl)
+ qed (use UV I in auto)
+qed
+
+
+lemma Hausdorff_space_compact_sets:
+ "Hausdorff_space X \<longleftrightarrow>
+ (\<forall>S T. compactin X S \<and> compactin X T \<and> disjnt S T
+ \<longrightarrow> (\<exists>U V. openin X U \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V))"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then show ?rhs
+ by (meson Hausdorff_space_compact_separation)
+next
+ assume R [rule_format]: ?rhs
+ show ?lhs
+ proof (clarsimp simp add: Hausdorff_space_def)
+ fix x y
+ assume "x \<in> topspace X" "y \<in> topspace X" "x \<noteq> y"
+ then show "\<exists>U. openin X U \<and> (\<exists>V. openin X V \<and> x \<in> U \<and> y \<in> V \<and> disjnt U V)"
+ using R [of "{x}" "{y}"] by auto
+ qed
+qed
+
+lemma compactin_imp_closedin:
+ assumes X: "Hausdorff_space X" and S: "compactin X S" shows "closedin X S"
+proof -
+ have "S \<subseteq> topspace X"
+ by (simp add: assms compactin_subset_topspace)
+ moreover
+ have "\<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> topspace X - S" if "x \<in> topspace X" "x \<notin> S" for x
+ using Hausdorff_space_compact_separation [OF X _ S, of "{x}"] that
+ apply (simp add: disjnt_def)
+ by (metis Diff_mono Diff_triv openin_subset)
+ ultimately show ?thesis
+ using closedin_def openin_subopen by force
+qed
+
+lemma closedin_Hausdorff_singleton:
+ "\<lbrakk>Hausdorff_space X; x \<in> topspace X\<rbrakk> \<Longrightarrow> closedin X {x}"
+ by (simp add: Hausdorff_imp_t1_space closedin_t1_singleton)
+
+lemma closedin_Hausdorff_sing_eq:
+ "Hausdorff_space X \<Longrightarrow> closedin X {x} \<longleftrightarrow> x \<in> topspace X"
+ by (meson closedin_Hausdorff_singleton closedin_subset insert_subset)
+
+lemma Hausdorff_space_discrete_topology [simp]:
+ "Hausdorff_space (discrete_topology U)"
+ unfolding Hausdorff_space_def
+ apply safe
+ by (metis discrete_topology_unique_alt disjnt_empty2 disjnt_insert2 insert_iff mk_disjoint_insert topspace_discrete_topology)
+
+lemma compactin_Int:
+ "\<lbrakk>Hausdorff_space X; compactin X S; compactin X T\<rbrakk> \<Longrightarrow> compactin X (S \<inter> T)"
+ by (simp add: closed_Int_compactin compactin_imp_closedin)
+
+lemma finite_topspace_imp_discrete_topology:
+ "\<lbrakk>topspace X = U; finite U; Hausdorff_space X\<rbrakk> \<Longrightarrow> X = discrete_topology U"
+ using Hausdorff_imp_t1_space finite_t1_space_imp_discrete_topology by blast
+
+lemma derived_set_of_finite:
+ "\<lbrakk>Hausdorff_space X; finite S\<rbrakk> \<Longrightarrow> X derived_set_of S = {}"
+ using Hausdorff_imp_t1_space t1_space_derived_set_of_finite by auto
+
+lemma derived_set_of_singleton:
+ "Hausdorff_space X \<Longrightarrow> X derived_set_of {x} = {}"
+ by (simp add: derived_set_of_finite)
+
+lemma closedin_Hausdorff_finite:
+ "\<lbrakk>Hausdorff_space X; S \<subseteq> topspace X; finite S\<rbrakk> \<Longrightarrow> closedin X S"
+ by (simp add: compactin_imp_closedin finite_imp_compactin_eq)
+
+lemma open_in_Hausdorff_delete:
+ "\<lbrakk>Hausdorff_space X; openin X S\<rbrakk> \<Longrightarrow> openin X (S - {x})"
+ using Hausdorff_imp_t1_space t1_space_openin_delete_alt by auto
+
+lemma closedin_Hausdorff_finite_eq:
+ "\<lbrakk>Hausdorff_space X; finite S\<rbrakk> \<Longrightarrow> closedin X S \<longleftrightarrow> S \<subseteq> topspace X"
+ by (meson closedin_Hausdorff_finite closedin_def)
+
+lemma derived_set_of_infinite_open_in:
+ "Hausdorff_space X
+ \<Longrightarrow> X derived_set_of S =
+ {x \<in> topspace X. \<forall>U. x \<in> U \<and> openin X U \<longrightarrow> infinite(S \<inter> U)}"
+ using Hausdorff_imp_t1_space t1_space_derived_set_of_infinite_openin by fastforce
+
+lemma Hausdorff_space_discrete_compactin:
+ "Hausdorff_space X
+ \<Longrightarrow> S \<inter> X derived_set_of S = {} \<and> compactin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> finite S"
+ using derived_set_of_finite discrete_compactin_eq_finite by fastforce
+
+lemma Hausdorff_space_finite_topspace:
+ "Hausdorff_space X \<Longrightarrow> X derived_set_of (topspace X) = {} \<and> compact_space X \<longleftrightarrow> finite(topspace X)"
+ using derived_set_of_finite discrete_compact_space_eq_finite by auto
+
+lemma derived_set_of_derived_set_subset:
+ "Hausdorff_space X \<Longrightarrow> X derived_set_of (X derived_set_of S) \<subseteq> X derived_set_of S"
+ by (simp add: Hausdorff_imp_t1_space derived_set_of_derived_set_subset_gen)
+
+
+lemma Hausdorff_space_injective_preimage:
+ assumes "Hausdorff_space Y" and cmf: "continuous_map X Y f" and "inj_on f (topspace X)"
+ shows "Hausdorff_space X"
+ unfolding Hausdorff_space_def
+proof clarify
+ fix x y
+ assume x: "x \<in> topspace X" and y: "y \<in> topspace X" and "x \<noteq> y"
+ then obtain U V where "openin Y U" "openin Y V" "f x \<in> U" "f y \<in> V" "disjnt U V"
+ using assms unfolding Hausdorff_space_def continuous_map_def by (meson inj_onD)
+ show "\<exists>U V. openin X U \<and> openin X V \<and> x \<in> U \<and> y \<in> V \<and> disjnt U V"
+ proof (intro exI conjI)
+ show "openin X {x \<in> topspace X. f x \<in> U}"
+ using \<open>openin Y U\<close> cmf continuous_map by fastforce
+ show "openin X {x \<in> topspace X. f x \<in> V}"
+ using \<open>openin Y V\<close> cmf openin_continuous_map_preimage by blast
+ show "disjnt {x \<in> topspace X. f x \<in> U} {x \<in> topspace X. f x \<in> V}"
+ using \<open>disjnt U V\<close> by (auto simp add: disjnt_def)
+ qed (use x \<open>f x \<in> U\<close> y \<open>f y \<in> V\<close> in auto)
+qed
+
+lemma homeomorphic_Hausdorff_space:
+ "X homeomorphic_space Y \<Longrightarrow> Hausdorff_space X \<longleftrightarrow> Hausdorff_space Y"
+ unfolding homeomorphic_space_def homeomorphic_maps_map
+ by (auto simp: homeomorphic_eq_everything_map Hausdorff_space_injective_preimage)
+
+lemma Hausdorff_space_retraction_map_image:
+ "\<lbrakk>retraction_map X Y r; Hausdorff_space X\<rbrakk> \<Longrightarrow> Hausdorff_space Y"
+ unfolding retraction_map_def
+ using Hausdorff_space_subtopology homeomorphic_Hausdorff_space retraction_maps_section_image2 by blast
+
+lemma compact_Hausdorff_space_optimal:
+ assumes eq: "topspace Y = topspace X" and XY: "\<And>U. openin X U \<Longrightarrow> openin Y U"
+ and "Hausdorff_space X" "compact_space Y"
+ shows "Y = X"
+proof -
+ have "\<And>U. closedin X U \<Longrightarrow> closedin Y U"
+ using XY using topology_finer_closedin [OF eq]
+ by metis
+ have "openin Y S = openin X S" for S
+ by (metis XY assms(3) assms(4) closedin_compact_space compactin_contractive compactin_imp_closedin eq openin_closedin_eq)
+ then show ?thesis
+ by (simp add: topology_eq)
+qed
+
+lemma continuous_imp_closed_map:
+ "\<lbrakk>compact_space X; Hausdorff_space Y; continuous_map X Y f\<rbrakk> \<Longrightarrow> closed_map X Y f"
+ by (meson closed_map_def closedin_compact_space compactin_imp_closedin image_compactin)
+
+lemma continuous_imp_quotient_map:
+ "\<lbrakk>compact_space X; Hausdorff_space Y; continuous_map X Y f; f ` (topspace X) = topspace Y\<rbrakk>
+ \<Longrightarrow> quotient_map X Y f"
+ by (simp add: continuous_imp_closed_map continuous_closed_imp_quotient_map)
+
+lemma continuous_imp_homeomorphic_map:
+ "\<lbrakk>compact_space X; Hausdorff_space Y; continuous_map X Y f;
+ f ` (topspace X) = topspace Y; inj_on f (topspace X)\<rbrakk>
+ \<Longrightarrow> homeomorphic_map X Y f"
+ by (simp add: continuous_imp_closed_map bijective_closed_imp_homeomorphic_map)
+
+lemma continuous_imp_embedding_map:
+ "\<lbrakk>compact_space X; Hausdorff_space Y; continuous_map X Y f; inj_on f (topspace X)\<rbrakk>
+ \<Longrightarrow> embedding_map X Y f"
+ by (simp add: continuous_imp_closed_map injective_closed_imp_embedding_map)
+
+lemma continuous_inverse_map:
+ assumes "compact_space X" "Hausdorff_space Y"
+ and cmf: "continuous_map X Y f" and gf: "\<And>x. x \<in> topspace X \<Longrightarrow> g(f x) = x"
+ and Sf: "S \<subseteq> f ` (topspace X)"
+ shows "continuous_map (subtopology Y S) X g"
+proof (rule continuous_map_from_subtopology_mono [OF _ \<open>S \<subseteq> f ` (topspace X)\<close>])
+ show "continuous_map (subtopology Y (f ` (topspace X))) X g"
+ unfolding continuous_map_closedin
+ proof (intro conjI ballI allI impI)
+ fix x
+ assume "x \<in> topspace (subtopology Y (f ` topspace X))"
+ then show "g x \<in> topspace X"
+ by (auto simp: gf)
+ next
+ fix C
+ assume C: "closedin X C"
+ show "closedin (subtopology Y (f ` topspace X))
+ {x \<in> topspace (subtopology Y (f ` topspace X)). g x \<in> C}"
+ proof (rule compactin_imp_closedin)
+ show "Hausdorff_space (subtopology Y (f ` topspace X))"
+ using Hausdorff_space_subtopology [OF \<open>Hausdorff_space Y\<close>] by blast
+ have "compactin Y (f ` C)"
+ using C cmf image_compactin closedin_compact_space [OF \<open>compact_space X\<close>] by blast
+ moreover have "{x \<in> topspace Y. x \<in> f ` topspace X \<and> g x \<in> C} = f ` C"
+ using closedin_subset [OF C] cmf by (auto simp: gf continuous_map_def)
+ ultimately have "compactin Y {x \<in> topspace Y. x \<in> f ` topspace X \<and> g x \<in> C}"
+ by simp
+ then show "compactin (subtopology Y (f ` topspace X))
+ {x \<in> topspace (subtopology Y (f ` topspace X)). g x \<in> C}"
+ by (auto simp add: compactin_subtopology)
+ qed
+ qed
+qed
+
+
+lemma Hausdorff_space_euclidean: "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")
+proof
+ assume ?lhs
+ then show ?rhs
+ by (rule topological_property_of_prod_component) (auto simp: Hausdorff_space_subtopology homeomorphic_Hausdorff_space)
+next
+ assume R: ?rhs
+ show ?lhs
+ proof (cases "(topspace X \<times> topspace Y) = {}")
+ case False
+ with R have ne: "topspace X \<noteq> {}" "topspace Y \<noteq> {}" and X: "Hausdorff_space X" and Y: "Hausdorff_space Y"
+ by auto
+ show ?thesis
+ unfolding Hausdorff_space_def
+ proof clarify
+ fix x y x' y'
+ assume xy: "(x, y) \<in> topspace (prod_topology X Y)"
+ and xy': "(x',y') \<in> topspace (prod_topology X Y)"
+ and *: "\<nexists>U V. openin (prod_topology X Y) U \<and> openin (prod_topology X Y) V
+ \<and> (x, y) \<in> U \<and> (x', y') \<in> V \<and> disjnt U V"
+ have False if "x \<noteq> x' \<or> y \<noteq> y'"
+ using that
+ proof
+ assume "x \<noteq> x'"
+ then obtain U V where "openin X U" "openin X V" "x \<in> U" "x' \<in> V" "disjnt U V"
+ by (metis Hausdorff_space_def X mem_Sigma_iff topspace_prod_topology xy xy')
+ let ?U = "U \<times> topspace Y"
+ let ?V = "V \<times> topspace Y"
+ have "openin (prod_topology X Y) ?U" "openin (prod_topology X Y) ?V"
+ by (simp_all add: openin_prod_Times_iff \<open>openin X U\<close> \<open>openin X V\<close>)
+ moreover have "disjnt ?U ?V"
+ by (simp add: \<open>disjnt U V\<close>)
+ ultimately show False
+ using * \<open>x \<in> U\<close> \<open>x' \<in> V\<close> xy xy' by (metis SigmaD2 SigmaI topspace_prod_topology)
+ next
+ assume "y \<noteq> y'"
+ then obtain U V where "openin Y U" "openin Y V" "y \<in> U" "y' \<in> V" "disjnt U V"
+ by (metis Hausdorff_space_def Y mem_Sigma_iff topspace_prod_topology xy xy')
+ let ?U = "topspace X \<times> U"
+ let ?V = "topspace X \<times> V"
+ have "openin (prod_topology X Y) ?U" "openin (prod_topology X Y) ?V"
+ by (simp_all add: openin_prod_Times_iff \<open>openin Y U\<close> \<open>openin Y V\<close>)
+ moreover have "disjnt ?U ?V"
+ by (simp add: \<open>disjnt U V\<close>)
+ ultimately show False
+ using "*" \<open>y \<in> U\<close> \<open>y' \<in> V\<close> xy xy' by (metis SigmaD1 SigmaI topspace_prod_topology)
+ qed
+ then show "x = x' \<and> y = y'"
+ by blast
+ qed
+ qed (simp add: Hausdorff_space_topspace_empty)
+qed
+
+
+lemma Hausdorff_space_product_topology:
+ "Hausdorff_space (product_topology X I) \<longleftrightarrow> (\<Pi>\<^sub>E i\<in>I. topspace(X i)) = {} \<or> (\<forall>i \<in> I. Hausdorff_space (X i))"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then show ?rhs
+ apply (rule topological_property_of_product_component)
+ apply (blast dest: Hausdorff_space_subtopology homeomorphic_Hausdorff_space)+
+ done
+next
+ assume R: ?rhs
+ show ?lhs
+ proof (cases "(\<Pi>\<^sub>E i\<in>I. topspace(X i)) = {}")
+ case True
+ then show ?thesis
+ by (simp add: Hausdorff_space_topspace_empty)
+ next
+ case False
+ have "\<exists>U V. openin (product_topology X I) U \<and> openin (product_topology X I) V \<and> f \<in> U \<and> g \<in> V \<and> disjnt U V"
+ if f: "f \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))" and g: "g \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))" and "f \<noteq> g"
+ for f g :: "'a \<Rightarrow> 'b"
+ proof -
+ obtain m where "f m \<noteq> g m"
+ using \<open>f \<noteq> g\<close> by blast
+ then have "m \<in> I"
+ using f g by fastforce
+ then have "Hausdorff_space (X m)"
+ using False that R by blast
+ then obtain U V where U: "openin (X m) U" and V: "openin (X m) V" and "f m \<in> U" "g m \<in> V" "disjnt U V"
+ by (metis Hausdorff_space_def PiE_mem \<open>f m \<noteq> g m\<close> \<open>m \<in> I\<close> f g)
+ show ?thesis
+ proof (intro exI conjI)
+ let ?U = "(\<Pi>\<^sub>E i\<in>I. topspace(X i)) \<inter> {x. x m \<in> U}"
+ let ?V = "(\<Pi>\<^sub>E i\<in>I. topspace(X i)) \<inter> {x. x m \<in> V}"
+ show "openin (product_topology X I) ?U" "openin (product_topology X I) ?V"
+ using \<open>m \<in> I\<close> U V
+ by (force simp add: openin_product_topology intro: arbitrary_union_of_inc relative_to_inc finite_intersection_of_inc)+
+ show "f \<in> ?U"
+ using \<open>f m \<in> U\<close> f by blast
+ show "g \<in> ?V"
+ using \<open>g m \<in> V\<close> g by blast
+ show "disjnt ?U ?V"
+ using \<open>disjnt U V\<close> by (auto simp: PiE_def Pi_def disjnt_def)
+ qed
+ qed
+ then show ?thesis
+ by (simp add: Hausdorff_space_def)
+ qed
+qed
+
end
--- a/src/HOL/Product_Type.thy Tue Mar 26 22:18:30 2019 +0100
+++ b/src/HOL/Product_Type.thy Wed Mar 27 14:08:26 2019 +0000
@@ -1272,6 +1272,17 @@
proc = K Set_Comprehension_Pointfree.code_simproc}])
\<close>
+subsection \<open>Lemmas about disjointness\<close>
+
+lemma disjnt_Times1_iff [simp]: "disjnt (C \<times> A) (C \<times> B) \<longleftrightarrow> C = {} \<or> disjnt A B"
+ by (auto simp: disjnt_def)
+
+lemma disjnt_Times2_iff [simp]: "disjnt (A \<times> C) (B \<times> C) \<longleftrightarrow> C = {} \<or> disjnt A B"
+ by (auto simp: disjnt_def)
+
+lemma disjnt_Sigma_iff: "disjnt (Sigma A C) (Sigma B C) \<longleftrightarrow> (\<forall>i \<in> A\<inter>B. C i = {}) \<or> disjnt A B"
+ by (auto simp: disjnt_def)
+
subsection \<open>Inductively defined sets\<close>