# HG changeset patch
# User paulson
# Date 1683195247 -3600
# Node ID 2b07535e0d2726a222fc4d8a267bfcb778ace1f7
# Parent  051b09437a6b496867dac21339ce7a80bcd61f17# Parent  98879407d33c86960f8dc343897dcb3fbc2d76e4
merged

diff -r 051b09437a6b -r 2b07535e0d27 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Thu May 04 08:53:45 2023 +1000
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Thu May 04 11:14:07 2023 +0100
@@ -1,5 +1,4 @@
-(*  Author:     L C Paulson, University of Cambridge [ported from HOL Light]
-*)
+(*  Author:     L C Paulson, University of Cambridge [ported from HOL Light] *)
 
 section \<open>Operators involving abstract topology\<close>
 
diff -r 051b09437a6b -r 2b07535e0d27 src/HOL/Analysis/Analysis.thy
--- a/src/HOL/Analysis/Analysis.thy	Thu May 04 08:53:45 2023 +1000
+++ b/src/HOL/Analysis/Analysis.thy	Thu May 04 11:14:07 2023 +0100
@@ -4,6 +4,8 @@
   Convex
   Determinants
   (* Topology *)
+  FSigma
+  Sum_Topology
   Connected
   Abstract_Limits
   Isolated
diff -r 051b09437a6b -r 2b07535e0d27 src/HOL/Analysis/FSigma.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/FSigma.thy	Thu May 04 11:14:07 2023 +0100
@@ -0,0 +1,236 @@
+(*  Author:     L C Paulson, University of Cambridge [ported from HOL Light, metric.ml] *)
+
+section \<open>$F$-Sigma and $G$-Delta sets in a Topological Space\<close>
+
+text \<open>An $F$-sigma set is a countable union of closed sets; a $G$-delta set is the dual.\<close>
+
+theory FSigma
+  imports Abstract_Topology
+begin
+
+
+definition fsigma_in 
+  where "fsigma_in X \<equiv> countable union_of closedin X"
+
+definition gdelta_in 
+  where "gdelta_in X \<equiv> (countable intersection_of openin X) relative_to topspace X"
+
+lemma fsigma_in_ascending:
+   "fsigma_in X S \<longleftrightarrow> (\<exists>C. (\<forall>n. closedin X (C n)) \<and> (\<forall>n. C n \<subseteq> C(Suc n)) \<and> \<Union> (range C) = S)"
+  unfolding fsigma_in_def
+  by (metis closedin_Un countable_union_of_ascending closedin_empty)
+
+lemma gdelta_in_alt:
+   "gdelta_in X S \<longleftrightarrow> S \<subseteq> topspace X \<and> (countable intersection_of openin X) S"
+proof -
+  have "(countable intersection_of openin X) (topspace X)"
+    by (simp add: countable_intersection_of_inc)
+  then show ?thesis
+    unfolding gdelta_in_def
+    by (metis countable_intersection_of_inter relative_to_def relative_to_imp_subset relative_to_subset)
+qed
+
+lemma fsigma_in_subset: "fsigma_in X S \<Longrightarrow> S \<subseteq> topspace X"
+  using closedin_subset by (fastforce simp: fsigma_in_def union_of_def subset_iff)
+
+lemma gdelta_in_subset: "gdelta_in X S \<Longrightarrow> S \<subseteq> topspace X"
+  by (simp add: gdelta_in_alt)
+
+lemma closed_imp_fsigma_in: "closedin X S \<Longrightarrow> fsigma_in X S"
+  by (simp add: countable_union_of_inc fsigma_in_def)
+
+lemma open_imp_gdelta_in: "openin X S \<Longrightarrow> gdelta_in X S"
+  by (simp add: countable_intersection_of_inc gdelta_in_alt openin_subset)
+
+lemma fsigma_in_empty [iff]: "fsigma_in X {}"
+  by (simp add: closed_imp_fsigma_in)
+
+lemma gdelta_in_empty [iff]: "gdelta_in X {}"
+  by (simp add: open_imp_gdelta_in)
+
+lemma fsigma_in_topspace [iff]: "fsigma_in X (topspace X)"
+  by (simp add: closed_imp_fsigma_in)
+
+lemma gdelta_in_topspace [iff]: "gdelta_in X (topspace X)"
+  by (simp add: open_imp_gdelta_in)
+
+lemma fsigma_in_Union:
+   "\<lbrakk>countable T; \<And>S. S \<in> T \<Longrightarrow> fsigma_in X S\<rbrakk> \<Longrightarrow> fsigma_in X (\<Union> T)"
+  by (simp add: countable_union_of_Union fsigma_in_def)
+
+lemma fsigma_in_Un:
+   "\<lbrakk>fsigma_in X S; fsigma_in X T\<rbrakk> \<Longrightarrow> fsigma_in X (S \<union> T)"
+  by (simp add: countable_union_of_Un fsigma_in_def)
+
+lemma fsigma_in_Int:
+   "\<lbrakk>fsigma_in X S; fsigma_in X T\<rbrakk> \<Longrightarrow> fsigma_in X (S \<inter> T)"
+  by (simp add: closedin_Int countable_union_of_Int fsigma_in_def)
+
+lemma gdelta_in_Inter:
+   "\<lbrakk>countable T; T\<noteq>{}; \<And>S. S \<in> T \<Longrightarrow> gdelta_in X S\<rbrakk> \<Longrightarrow> gdelta_in X (\<Inter> T)"
+  by (simp add: Inf_less_eq countable_intersection_of_Inter gdelta_in_alt)
+
+lemma gdelta_in_Int:
+   "\<lbrakk>gdelta_in X S; gdelta_in X T\<rbrakk> \<Longrightarrow> gdelta_in X (S \<inter> T)"
+  by (simp add: countable_intersection_of_inter gdelta_in_alt le_infI2)
+
+lemma gdelta_in_Un:
+   "\<lbrakk>gdelta_in X S; gdelta_in X T\<rbrakk> \<Longrightarrow> gdelta_in X (S \<union> T)"
+  by (simp add: countable_intersection_of_union gdelta_in_alt openin_Un)
+
+lemma fsigma_in_diff:
+  assumes "fsigma_in X S" "gdelta_in X T"
+  shows "fsigma_in X (S - T)"
+proof -
+  have [simp]: "S - (S \<inter> T) = S - T" for S T :: "'a set"
+    by auto
+  have [simp]: "topspace X - \<Inter>\<T> = (\<Union>T\<in>\<T>. topspace X - T)" for \<T>
+    by auto
+  have "\<And>\<T>. \<lbrakk>countable \<T>; \<T> \<subseteq> Collect (openin X)\<rbrakk> \<Longrightarrow>
+             (countable union_of closedin X) (\<Union> ((-) (topspace X) ` \<T>))"
+    by (metis Ball_Collect countable_union_of_UN countable_union_of_inc openin_closedin_eq)
+  then have "\<forall>S. gdelta_in X S \<longrightarrow> fsigma_in X (topspace X - S)"
+    by (simp add: fsigma_in_def gdelta_in_def all_relative_to all_intersection_of del: UN_simps)
+  then show ?thesis
+    by (metis Diff_Int2 Diff_Int_distrib2 assms fsigma_in_Int fsigma_in_subset inf.absorb_iff2)
+qed
+
+lemma gdelta_in_diff:
+  assumes "gdelta_in X S" "fsigma_in X T"
+  shows "gdelta_in X (S - T)"
+proof -
+  have [simp]: "topspace X - \<Union>\<T> = topspace X \<inter> (\<Inter>T\<in>\<T>. topspace X - T)" for \<T>
+    by auto
+  have "\<And>\<T>. \<lbrakk>countable \<T>; \<T> \<subseteq> Collect (closedin X)\<rbrakk>
+         \<Longrightarrow> (countable intersection_of openin X relative_to topspace X)
+              (topspace X \<inter> \<Inter> ((-) (topspace X) ` \<T>))"
+    by (metis Ball_Collect closedin_def countable_intersection_of_INT countable_intersection_of_inc relative_to_inc)
+  then have "\<forall>S. fsigma_in X S \<longrightarrow> gdelta_in X (topspace X - S)"
+    by (simp add: fsigma_in_def gdelta_in_def all_union_of del: INT_simps)
+  then show ?thesis
+    by (metis Diff_Int2 Diff_Int_distrib2 assms gdelta_in_Int gdelta_in_alt inf.orderE inf_commute)
+qed
+
+lemma gdelta_in_fsigma_in:
+   "gdelta_in X S \<longleftrightarrow> S \<subseteq> topspace X \<and> fsigma_in X (topspace X - S)"
+  by (metis double_diff fsigma_in_diff fsigma_in_topspace gdelta_in_alt gdelta_in_diff gdelta_in_topspace)
+
+lemma fsigma_in_gdelta_in:
+   "fsigma_in X S \<longleftrightarrow> S \<subseteq> topspace X \<and> gdelta_in X (topspace X - S)"
+  by (metis Diff_Diff_Int fsigma_in_subset gdelta_in_fsigma_in inf.absorb_iff2)
+
+lemma gdelta_in_descending:
+   "gdelta_in X S \<longleftrightarrow> (\<exists>C. (\<forall>n. openin X (C n)) \<and> (\<forall>n. C(Suc n) \<subseteq> C n) \<and> \<Inter>(range C) = S)" (is "?lhs=?rhs")
+proof
+  assume ?lhs
+  then obtain C where C: "S \<subseteq> topspace X" "\<And>n. closedin X (C n)" 
+                         "\<And>n. C n \<subseteq> C(Suc n)" "\<Union>(range C) = topspace X - S"
+    by (meson fsigma_in_ascending gdelta_in_fsigma_in)
+  define D where "D \<equiv> \<lambda>n. topspace X - C n"
+  have "\<And>n. openin X (D n) \<and> D (Suc n) \<subseteq> D n"
+    by (simp add: Diff_mono C D_def openin_diff)
+  moreover have "\<Inter>(range D) = S"
+    by (simp add: Diff_Diff_Int Int_absorb1 C D_def)
+  ultimately show ?rhs
+    by metis
+next
+  assume ?rhs
+  then obtain C where "S \<subseteq> topspace X" 
+                and C: "\<And>n. openin X (C n)" "\<And>n. C(Suc n) \<subseteq> C n" "\<Inter>(range C) = S"
+    using openin_subset by fastforce
+  define D where "D \<equiv> \<lambda>n. topspace X - C n"
+  have "\<And>n. closedin X (D n) \<and> D n \<subseteq> D(Suc n)"
+    by (simp add: Diff_mono C closedin_diff D_def)
+  moreover have "\<Union>(range D) = topspace X - S"
+    using C D_def by blast
+  ultimately show ?lhs
+    by (metis \<open>S \<subseteq> topspace X\<close> fsigma_in_ascending gdelta_in_fsigma_in)
+qed
+
+lemma homeomorphic_map_fsigmaness:
+  assumes f: "homeomorphic_map X Y f" and "U \<subseteq> topspace X"
+  shows "fsigma_in Y (f ` U) \<longleftrightarrow> fsigma_in X U"  (is "?lhs=?rhs")
+proof -
+  obtain g where g: "homeomorphic_maps X Y f g" and g: "homeomorphic_map Y X g"
+    and 1: "(\<forall>x \<in> topspace X. g(f x) = x)" and 2: "(\<forall>y \<in> topspace Y. f(g y) = y)"
+    using assms homeomorphic_map_maps by (metis homeomorphic_maps_map)
+  show ?thesis
+  proof
+    assume ?lhs
+    then obtain \<V> where "countable \<V>" and \<V>: "\<V> \<subseteq> Collect (closedin Y)" "\<Union>\<V> = f`U"
+      by (force simp: fsigma_in_def union_of_def)
+    define \<U> where "\<U> \<equiv> image (image g) \<V>"
+    have "countable \<U>"
+      using \<U>_def \<open>countable \<V>\<close> by blast
+    moreover have "\<U> \<subseteq> Collect (closedin X)"
+      using f g homeomorphic_map_closedness_eq \<V> unfolding \<U>_def by blast
+    moreover have "\<Union>\<U> \<subseteq> U"
+      unfolding \<U>_def  by (smt (verit) assms 1 \<V> image_Union image_iff in_mono subsetI)
+    moreover have "U \<subseteq> \<Union>\<U>"
+      unfolding \<U>_def using assms \<V>
+      by (smt (verit, del_insts) "1" imageI image_Union subset_iff)
+    ultimately show ?rhs
+      by (metis fsigma_in_def subset_antisym union_of_def)
+  next
+    assume ?rhs
+    then obtain \<V> where "countable \<V>" and \<V>: "\<V> \<subseteq> Collect (closedin X)" "\<Union>\<V> = U"
+      by (auto simp: fsigma_in_def union_of_def)
+    define \<U> where "\<U> \<equiv> image (image f) \<V>"
+    have "countable \<U>"
+      using \<U>_def \<open>countable \<V>\<close> by blast
+    moreover have "\<U> \<subseteq> Collect (closedin Y)"
+      using f g homeomorphic_map_closedness_eq \<V> unfolding \<U>_def by blast
+    moreover have "\<Union>\<U> = f`U"
+      unfolding \<U>_def using \<V> by blast
+    ultimately show ?lhs
+      by (metis fsigma_in_def union_of_def)
+  qed
+qed
+
+lemma homeomorphic_map_fsigmaness_eq:
+   "homeomorphic_map X Y f
+        \<Longrightarrow> (fsigma_in X U \<longleftrightarrow> U \<subseteq> topspace X \<and> fsigma_in Y (f ` U))"
+  by (metis fsigma_in_subset homeomorphic_map_fsigmaness)
+
+lemma homeomorphic_map_gdeltaness:
+  assumes "homeomorphic_map X Y f" "U \<subseteq> topspace X"
+  shows "gdelta_in Y (f ` U) \<longleftrightarrow> gdelta_in X U"
+proof -
+  have "topspace Y - f ` U = f ` (topspace X - U)"
+    by (metis (no_types, lifting) Diff_subset assms homeomorphic_eq_everything_map inj_on_image_set_diff)
+  then show ?thesis
+    using assms homeomorphic_imp_surjective_map
+    by (fastforce simp: gdelta_in_fsigma_in homeomorphic_map_fsigmaness_eq)
+qed
+
+lemma homeomorphic_map_gdeltaness_eq:
+   "homeomorphic_map X Y f
+    \<Longrightarrow> gdelta_in X U \<longleftrightarrow> U \<subseteq> topspace X \<and> gdelta_in Y (f ` U)"
+  by (meson gdelta_in_subset homeomorphic_map_gdeltaness)
+
+lemma fsigma_in_relative_to:
+   "(fsigma_in X relative_to S) = fsigma_in (subtopology X S)"
+  by (simp add: fsigma_in_def countable_union_of_relative_to closedin_relative_to)
+
+lemma fsigma_in_subtopology:
+   "fsigma_in (subtopology X U) S \<longleftrightarrow> (\<exists>T. fsigma_in X T \<and> S = T \<inter> U)"
+  by (metis fsigma_in_relative_to inf_commute relative_to_def)
+
+lemma gdelta_in_relative_to:
+   "(gdelta_in X relative_to S) = gdelta_in (subtopology X S)"
+  apply (simp add: gdelta_in_def)
+  by (metis countable_intersection_of_relative_to openin_relative_to subtopology_restrict)
+
+lemma gdelta_in_subtopology:
+   "gdelta_in (subtopology X U) S \<longleftrightarrow> (\<exists>T. gdelta_in X T \<and> S = T \<inter> U)"
+  by (metis gdelta_in_relative_to inf_commute relative_to_def)
+
+lemma fsigma_in_fsigma_subtopology:
+   "fsigma_in X S \<Longrightarrow> (fsigma_in (subtopology X S) T \<longleftrightarrow> fsigma_in X T \<and> T \<subseteq> S)"
+  by (metis fsigma_in_Int fsigma_in_gdelta_in fsigma_in_subtopology inf.orderE topspace_subtopology_subset)
+
+lemma gdelta_in_gdelta_subtopology:
+   "gdelta_in X S \<Longrightarrow> (gdelta_in (subtopology X S) T \<longleftrightarrow> gdelta_in X T \<and> T \<subseteq> S)"
+  by (metis gdelta_in_Int gdelta_in_subset gdelta_in_subtopology inf.orderE topspace_subtopology_subset)
+
+end
diff -r 051b09437a6b -r 2b07535e0d27 src/HOL/Analysis/Product_Topology.thy
--- a/src/HOL/Analysis/Product_Topology.thy	Thu May 04 08:53:45 2023 +1000
+++ b/src/HOL/Analysis/Product_Topology.thy	Thu May 04 11:14:07 2023 +0100
@@ -1,7 +1,7 @@
 section\<open>The binary product topology\<close>
 
 theory Product_Topology
-imports Function_Topology
+  imports Function_Topology
 begin
 
 section \<open>Product Topology\<close>
diff -r 051b09437a6b -r 2b07535e0d27 src/HOL/Analysis/Sum_Topology.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Sum_Topology.thy	Thu May 04 11:14:07 2023 +0100
@@ -0,0 +1,146 @@
+section\<open>Disjoint sum of arbitarily many spaces\<close>
+
+theory Sum_Topology
+  imports Abstract_Topology
+begin
+
+
+definition sum_topology :: "('a \<Rightarrow> 'b topology) \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'b) topology" where
+  "sum_topology X I \<equiv>
+    topology (\<lambda>U. U \<subseteq> Sigma I (topspace \<circ> X) \<and> (\<forall>i \<in> I. openin (X i) {x. (i,x) \<in> U}))"
+
+lemma is_sum_topology: "istopology (\<lambda>U. U \<subseteq> Sigma I (topspace \<circ> X) \<and> (\<forall>i\<in>I. openin (X i) {x. (i, x) \<in> U}))"
+proof -
+  have 1: "{x. (i, x) \<in> S \<inter> T} = {x. (i, x) \<in> S} \<inter> {x::'b. (i, x) \<in> T}" for S T and i::'a
+    by auto
+  have 2: "{x. (i, x) \<in> \<Union> \<K>} = (\<Union>K\<in>\<K>. {x::'b. (i, x) \<in> K})" for \<K> and i::'a
+    by auto
+  show ?thesis
+    unfolding istopology_def 1 2 by blast
+qed
+
+lemma openin_sum_topology:
+   "openin (sum_topology X I) U \<longleftrightarrow>
+        U \<subseteq> Sigma I (topspace \<circ> X) \<and> (\<forall>i \<in> I. openin (X i) {x. (i,x) \<in> U})"
+  by (auto simp: sum_topology_def is_sum_topology)
+
+lemma openin_disjoint_union:
+   "openin (sum_topology X I) (Sigma I U) \<longleftrightarrow> (\<forall>i \<in> I. openin (X i) (U i))"
+  using openin_subset by (force simp: openin_sum_topology)
+
+lemma topspace_sum_topology [simp]:
+   "topspace(sum_topology X I) = Sigma I (topspace \<circ> X)"
+  by (metis comp_apply openin_disjoint_union openin_subset openin_sum_topology openin_topspace subset_antisym)
+
+lemma openin_sum_topology_alt:
+   "openin (sum_topology X I) U \<longleftrightarrow> (\<exists>T. U = Sigma I T \<and> (\<forall>i \<in> I. openin (X i) (T i)))"
+  by (bestsimp simp: openin_sum_topology dest: openin_subset)
+
+lemma forall_openin_sum_topology:
+   "(\<forall>U. openin (sum_topology X I) U \<longrightarrow> P U) \<longleftrightarrow> (\<forall>T. (\<forall>i \<in> I. openin (X i) (T i)) \<longrightarrow> P(Sigma I T))"
+  by (auto simp: openin_sum_topology_alt)
+
+lemma exists_openin_sum_topology:
+   "(\<exists>U. openin (sum_topology X I) U \<and> P U) \<longleftrightarrow>
+    (\<exists>T. (\<forall>i \<in> I. openin (X i) (T i)) \<and> P(Sigma I T))"
+  by (auto simp: openin_sum_topology_alt)
+
+lemma closedin_sum_topology:
+   "closedin (sum_topology X I) U \<longleftrightarrow> U \<subseteq> Sigma I (topspace \<circ> X) \<and> (\<forall>i \<in> I. closedin (X i) {x. (i,x) \<in> U})"
+     (is "?lhs = ?rhs")
+proof
+  assume L: ?lhs
+  then have U: "U \<subseteq> Sigma I (topspace \<circ> X)"
+    using closedin_subset by fastforce
+  then have "\<forall>i\<in>I. {x. (i, x) \<in> U} \<subseteq> topspace (X i)"
+    by fastforce
+  moreover have "openin (X i) (topspace (X i) - {x. (i, x) \<in> U})" if "i\<in>I" for i
+    apply (subst openin_subopen)
+    using L that unfolding closedin_def openin_sum_topology
+    by (bestsimp simp: o_def subset_iff)
+  ultimately show ?rhs
+    by (simp add: U closedin_def)
+next
+  assume R: ?rhs
+  then have "openin (X i) {x. (i, x) \<in> topspace (sum_topology X I) - U}" if "i\<in>I" for i
+    apply (subst openin_subopen)
+    using that unfolding closedin_def openin_sum_topology
+    by (bestsimp simp: o_def subset_iff)
+  then show ?lhs
+    by (simp add: R closedin_def openin_sum_topology)
+qed
+
+lemma closedin_disjoint_union:
+   "closedin (sum_topology X I) (Sigma I U) \<longleftrightarrow> (\<forall>i \<in> I. closedin (X i) (U i))"
+  using closedin_subset by (force simp: closedin_sum_topology)
+
+lemma closedin_sum_topology_alt:
+   "closedin (sum_topology X I) U \<longleftrightarrow> (\<exists>T. U = Sigma I T \<and> (\<forall>i \<in> I. closedin (X i) (T i)))"
+  using closedin_subset unfolding closedin_sum_topology by auto blast
+
+lemma forall_closedin_sum_topology:
+   "(\<forall>U. closedin (sum_topology X I) U \<longrightarrow> P U) \<longleftrightarrow>
+        (\<forall>t. (\<forall>i \<in> I. closedin (X i) (t i)) \<longrightarrow> P(Sigma I t))"
+  by (metis closedin_sum_topology_alt)
+
+lemma exists_closedin_sum_topology:
+   "(\<exists>U. closedin (sum_topology X I) U \<and> P U) \<longleftrightarrow>
+    (\<exists>T. (\<forall>i \<in> I. closedin (X i) (T i)) \<and> P(Sigma I T))"
+  by (simp add: closedin_sum_topology_alt) blast
+
+lemma open_map_component_injection:
+   "i \<in> I \<Longrightarrow> open_map (X i) (sum_topology X I) (\<lambda>x. (i,x))"
+  unfolding open_map_def openin_sum_topology
+  using openin_subset openin_subopen by (force simp: image_iff)
+
+lemma closed_map_component_injection:
+  assumes "i \<in> I"
+  shows "closed_map(X i) (sum_topology X I) (\<lambda>x. (i,x))"
+proof -
+  have "closedin (X j) {x. j = i \<and> x \<in> U}"
+    if "\<And>U S. closedin U S \<Longrightarrow> S \<subseteq> topspace U" and "closedin (X i) U" and "j \<in> I" for U j
+    using that by (cases "j=i") auto
+  then show ?thesis
+    using closedin_subset assms by (force simp: closed_map_def closedin_sum_topology image_iff)
+qed
+
+lemma continuous_map_component_injection:
+   "i \<in> I \<Longrightarrow> continuous_map(X i) (sum_topology X I) (\<lambda>x. (i,x))"
+  apply (clarsimp simp: continuous_map_def openin_sum_topology)
+  by (smt (verit, best) Collect_cong mem_Collect_eq openin_subset subsetD)
+
+lemma subtopology_sum_topology:
+  "subtopology (sum_topology X I) (Sigma I S) =
+        sum_topology (\<lambda>i. subtopology (X i) (S i)) I"
+  unfolding topology_eq
+proof (intro strip iffI)
+  fix T
+  assume *: "openin (subtopology (sum_topology X I) (Sigma I S)) T"
+  then obtain U where U: "\<forall>i\<in>I. openin (X i) (U i) \<and> T = Sigma I U \<inter> Sigma I S" 
+    by (auto simp: openin_subtopology openin_sum_topology_alt)
+  have "T = (SIGMA i:I. U i \<inter> S i)"
+  proof
+    show "T \<subseteq> (SIGMA i:I. U i \<inter> S i)"
+      by (metis "*" SigmaE Sigma_Int_distrib2 U openin_imp_subset subset_iff)
+    show "(SIGMA i:I. U i \<inter> S i) \<subseteq> T"
+      using U by fastforce
+  qed
+  then show "openin (sum_topology (\<lambda>i. subtopology (X i) (S i)) I) T"
+    by (simp add: U openin_disjoint_union openin_subtopology_Int)
+next
+  fix T
+  assume *: "openin (sum_topology (\<lambda>i. subtopology (X i) (S i)) I) T"
+  then obtain U where "\<forall>i\<in>I. \<exists>T. openin (X i) T \<and> U i = T \<inter> S i" and Teq: "T = Sigma I U"
+    by (auto simp: openin_subtopology openin_sum_topology_alt)
+  then obtain B where "\<And>i. i\<in>I \<Longrightarrow> openin (X i) (B i) \<and> U i = B i \<inter> S i"
+    by metis
+  then show "openin (subtopology (sum_topology X I) (Sigma I S)) T"
+    by (auto simp: openin_subtopology openin_sum_topology_alt Teq)
+qed
+
+lemma embedding_map_component_injection:
+   "i \<in> I \<Longrightarrow> embedding_map (X i) (sum_topology X I) (\<lambda>x. (i,x))"
+  by (metis injective_open_imp_embedding_map continuous_map_component_injection
+            open_map_component_injection inj_onI prod.inject)
+
+end