diff -r eddcc7c726f3 -r 4a9167f377b0 src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Mon Mar 18 15:35:34 2019 +0000
+++ b/src/HOL/Analysis/Function_Topology.thy	Tue Mar 19 16:14:51 2019 +0000
@@ -7,9 +7,9 @@
 begin
 
 
-section \<open>Product Topology\<close> (* FIX  see comments by the author *)
+section \<open>Function Topology\<close> 
 
-text \<open>We want to define the product topology.
+text \<open>We want to define the general product topology.
 
 The product topology on a product of topological spaces is generated by
 the sets which are products of open sets along finitely many coordinates, and the whole
@@ -48,7 +48,7 @@
 be the natural continuity definition of a map from the topology \<open>T1\<close> to the topology \<open>T2\<close>. Then
 the current \<open>continuous_on\<close> (with type classes) can be redefined as
 @{text [display] \<open>continuous_on s f =
-    continuous_on_topo (subtopology euclidean s) (topology euclidean) f\<close>}
+    continuous_on_topo (top_of_set s) (topology euclidean) f\<close>}
 
 In fact, I need \<open>continuous_on_topo\<close> to express the continuity of the projection on subfactors
 for the product topology, in Lemma~\<open>continuous_on_restrict_product_topology\<close>, and I show
@@ -61,369 +61,6 @@
 I realized afterwards that this theory has a lot in common with \<^file>\<open>~~/src/HOL/Library/Finite_Map.thy\<close>.
 \<close>
 
-subsection \<open>Topology without type classes\<close>
-
-subsubsection%important \<open>The topology generated by some (open) subsets\<close>
-
-text \<open>In the definition below of a generated topology, the \<open>Empty\<close> case is not necessary,
-as it follows from \<open>UN\<close> taking for \<open>K\<close> the empty set. However, it is convenient to have,
-and is never a problem in proofs, so I prefer to write it down explicitly.
-
-We do not require \<open>UNIV\<close> to be an open set, as this will not be the case in applications. (We are
-thinking of a topology on a subset of \<open>UNIV\<close>, the remaining part of \<open>UNIV\<close> being irrelevant.)\<close>
-
-inductive generate_topology_on for S where
-  Empty: "generate_topology_on S {}"
-| Int: "generate_topology_on S a \<Longrightarrow> generate_topology_on S b \<Longrightarrow> generate_topology_on S (a \<inter> b)"
-| UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology_on S k) \<Longrightarrow> generate_topology_on S (\<Union>K)"
-| Basis: "s \<in> S \<Longrightarrow> generate_topology_on S s"
-
-lemma istopology_generate_topology_on:
-  "istopology (generate_topology_on S)"
-unfolding istopology_def by (auto intro: generate_topology_on.intros)
-
-text \<open>The basic property of the topology generated by a set \<open>S\<close> is that it is the
-smallest topology containing all the elements of \<open>S\<close>:\<close>
-
-lemma generate_topology_on_coarsest:
-  assumes "istopology T"
-          "\<And>s. s \<in> S \<Longrightarrow> T s"
-          "generate_topology_on S s0"
-  shows "T s0"
-using assms(3) apply (induct rule: generate_topology_on.induct)
-using assms(1) assms(2) unfolding istopology_def by auto
-
-abbreviation%unimportant topology_generated_by::"('a set set) \<Rightarrow> ('a topology)"
-  where "topology_generated_by S \<equiv> topology (generate_topology_on S)"
-
-lemma openin_topology_generated_by_iff:
-  "openin (topology_generated_by S) s \<longleftrightarrow> generate_topology_on S s"
-  using topology_inverse'[OF istopology_generate_topology_on[of S]] by simp
-
-lemma openin_topology_generated_by:
-  "openin (topology_generated_by S) s \<Longrightarrow> generate_topology_on S s"
-using openin_topology_generated_by_iff by auto
-
-lemma topology_generated_by_topspace:
-  "topspace (topology_generated_by S) = (\<Union>S)"
-proof
-  {
-    fix s assume "openin (topology_generated_by S) s"
-    then have "generate_topology_on S s" by (rule openin_topology_generated_by)
-    then have "s \<subseteq> (\<Union>S)" by (induct, auto)
-  }
-  then show "topspace (topology_generated_by S) \<subseteq> (\<Union>S)"
-    unfolding topspace_def by auto
-next
-  have "generate_topology_on S (\<Union>S)"
-    using generate_topology_on.UN[OF generate_topology_on.Basis, of S S] by simp
-  then show "(\<Union>S) \<subseteq> topspace (topology_generated_by S)"
-    unfolding topspace_def using openin_topology_generated_by_iff by auto
-qed
-
-lemma topology_generated_by_Basis:
-  "s \<in> S \<Longrightarrow> openin (topology_generated_by S) s"
-  by (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis)
-
-lemma generate_topology_on_Inter:
-  "\<lbrakk>finite \<F>; \<And>K. K \<in> \<F> \<Longrightarrow> generate_topology_on \<S> K; \<F> \<noteq> {}\<rbrakk> \<Longrightarrow> generate_topology_on \<S> (\<Inter>\<F>)"
-  by (induction \<F> rule: finite_induct; force intro: generate_topology_on.intros)
-
-subsection\<open>Topology bases and sub-bases\<close>
-
-lemma istopology_base_alt:
-   "istopology (arbitrary union_of P) \<longleftrightarrow>
-    (\<forall>S T. (arbitrary union_of P) S \<and> (arbitrary union_of P) T
-           \<longrightarrow> (arbitrary union_of P) (S \<inter> T))"
-  by (simp add: istopology_def) (blast intro: arbitrary_union_of_Union)
-
-lemma istopology_base_eq:
-   "istopology (arbitrary union_of P) \<longleftrightarrow>
-    (\<forall>S T. P S \<and> P T \<longrightarrow> (arbitrary union_of P) (S \<inter> T))"
-  by (simp add: istopology_base_alt arbitrary_union_of_Int_eq)
-
-lemma istopology_base:
-   "(\<And>S T. \<lbrakk>P S; P T\<rbrakk> \<Longrightarrow> P(S \<inter> T)) \<Longrightarrow> istopology (arbitrary union_of P)"
-  by (simp add: arbitrary_def istopology_base_eq union_of_inc)
-
-lemma openin_topology_base_unique:
-   "openin X = arbitrary union_of P \<longleftrightarrow>
-        (\<forall>V. P V \<longrightarrow> openin X V) \<and> (\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> (\<exists>V. P V \<and> x \<in> V \<and> V \<subseteq> U))"
-   (is "?lhs = ?rhs")
-proof
-  assume ?lhs
-  then show ?rhs
-    by (auto simp: union_of_def arbitrary_def)
-next
-  assume R: ?rhs
-  then have *: "\<exists>\<U>\<subseteq>Collect P. \<Union>\<U> = S" if "openin X S" for S
-    using that by (rule_tac x="{V. P V \<and> V \<subseteq> S}" in exI) fastforce
-  from R show ?lhs
-    by (fastforce simp add: union_of_def arbitrary_def intro: *)
-qed
-
-lemma topology_base_unique:
-   "\<lbrakk>\<And>S. P S \<Longrightarrow> openin X S;
-     \<And>U x. \<lbrakk>openin X U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>B. P B \<and> x \<in> B \<and> B \<subseteq> U\<rbrakk>
-    \<Longrightarrow> topology(arbitrary union_of P) = X"
-  by (metis openin_topology_base_unique openin_inverse [of X])
-
-lemma topology_bases_eq_aux:
-   "\<lbrakk>(arbitrary union_of P) S;
-     \<And>U x. \<lbrakk>P U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>V. Q V \<and> x \<in> V \<and> V \<subseteq> U\<rbrakk>
-        \<Longrightarrow> (arbitrary union_of Q) S"
-  by (metis arbitrary_union_of_alt arbitrary_union_of_idempot)
-
-lemma topology_bases_eq:
-   "\<lbrakk>\<And>U x. \<lbrakk>P U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>V. Q V \<and> x \<in> V \<and> V \<subseteq> U;
-    \<And>V x. \<lbrakk>Q V; x \<in> V\<rbrakk> \<Longrightarrow> \<exists>U. P U \<and> x \<in> U \<and> U \<subseteq> V\<rbrakk>
-        \<Longrightarrow> topology (arbitrary union_of P) =
-            topology (arbitrary union_of Q)"
-  by (fastforce intro:  arg_cong [where f=topology]  elim: topology_bases_eq_aux)
-
-lemma istopology_subbase:
-   "istopology (arbitrary union_of (finite intersection_of P relative_to S))"
-  by (simp add: finite_intersection_of_Int istopology_base relative_to_Int)
-
-lemma openin_subbase:
-  "openin (topology (arbitrary union_of (finite intersection_of B relative_to U))) S
-   \<longleftrightarrow> (arbitrary union_of (finite intersection_of B relative_to U)) S"
-  by (simp add: istopology_subbase topology_inverse')
-
-lemma topspace_subbase [simp]:
-   "topspace(topology (arbitrary union_of (finite intersection_of B relative_to U))) = U" (is "?lhs = _")
-proof
-  show "?lhs \<subseteq> U"
-    by (metis arbitrary_union_of_relative_to openin_subbase openin_topspace relative_to_imp_subset)
-  show "U \<subseteq> ?lhs"
-    by (metis arbitrary_union_of_inc finite_intersection_of_empty inf.orderE istopology_subbase 
-              openin_subset relative_to_inc subset_UNIV topology_inverse')
-qed
-
-lemma minimal_topology_subbase:
-   "\<lbrakk>\<And>S. P S \<Longrightarrow> openin X S; openin X U;
-     openin(topology(arbitrary union_of (finite intersection_of P relative_to U))) S\<rbrakk>
-    \<Longrightarrow> openin X S"
-  apply (simp add: istopology_subbase topology_inverse)
-  apply (simp add: union_of_def intersection_of_def relative_to_def)
-  apply (blast intro: openin_Int_Inter)
-  done
-
-lemma istopology_subbase_UNIV:
-   "istopology (arbitrary union_of (finite intersection_of P))"
-  by (simp add: istopology_base finite_intersection_of_Int)
-
-
-lemma generate_topology_on_eq:
-  "generate_topology_on S = arbitrary union_of finite' intersection_of (\<lambda>x. x \<in> S)" (is "?lhs = ?rhs")
-proof (intro ext iffI)
-  fix A
-  assume "?lhs A"
-  then show "?rhs A"
-  proof induction
-    case (Int a b)
-    then show ?case
-      by (metis (mono_tags, lifting) istopology_base_alt finite'_intersection_of_Int istopology_base)
-  next
-    case (UN K)
-    then show ?case
-      by (simp add: arbitrary_union_of_Union)
-  next
-    case (Basis s)
-    then show ?case
-      by (simp add: Sup_upper arbitrary_union_of_inc finite'_intersection_of_inc relative_to_subset)
-  qed auto
-next
-  fix A
-  assume "?rhs A"
-  then obtain \<U> where \<U>: "\<And>T. T \<in> \<U> \<Longrightarrow> \<exists>\<F>. finite' \<F> \<and> \<F> \<subseteq> S \<and> \<Inter>\<F> = T" and eq: "A = \<Union>\<U>"
-    unfolding union_of_def intersection_of_def by auto
-  show "?lhs A"
-    unfolding eq
-  proof (rule generate_topology_on.UN)
-    fix T
-    assume "T \<in> \<U>"
-    with \<U> obtain \<F> where "finite' \<F>" "\<F> \<subseteq> S" "\<Inter>\<F> = T"
-      by blast
-    have "generate_topology_on S (\<Inter>\<F>)"
-    proof (rule generate_topology_on_Inter)
-      show "finite \<F>" "\<F> \<noteq> {}"
-        by (auto simp: \<open>finite' \<F>\<close>)
-      show "\<And>K. K \<in> \<F> \<Longrightarrow> generate_topology_on S K"
-        by (metis \<open>\<F> \<subseteq> S\<close> generate_topology_on.simps subset_iff)
-    qed
-    then show "generate_topology_on S T"
-      using \<open>\<Inter>\<F> = T\<close> by blast
-  qed
-qed
-
-subsubsection%important \<open>Continuity\<close>
-
-text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
-of type classes, as defined below.\<close>
-
-definition%important continuous_on_topo::"'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
-  where "continuous_on_topo T1 T2 f = ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
-                                      \<and> (f`(topspace T1) \<subseteq> (topspace T2)))"
-
-lemma continuous_on_continuous_on_topo:
-  "continuous_on s f \<longleftrightarrow> continuous_on_topo (subtopology euclidean s) euclidean f"
-  by (auto simp: continuous_on_topo_def Int_commute continuous_openin_preimage_eq)
-
-lemma continuous_on_topo_UNIV:
-  "continuous_on UNIV f \<longleftrightarrow> continuous_on_topo euclidean euclidean f"
-using continuous_on_continuous_on_topo[of UNIV f] subtopology_UNIV[of euclidean] by auto
-
-lemma continuous_on_topo_open [intro]:
-  "continuous_on_topo T1 T2 f \<Longrightarrow> openin T2 U \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
-  unfolding continuous_on_topo_def by auto
-
-lemma continuous_on_topo_topspace [intro]:
-  "continuous_on_topo T1 T2 f \<Longrightarrow> f`(topspace T1) \<subseteq> (topspace T2)"
-unfolding continuous_on_topo_def by auto
-
-lemma continuous_on_generated_topo_iff:
-  "continuous_on_topo T1 (topology_generated_by S) f \<longleftrightarrow>
-      ((\<forall>U. U \<in> S \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1))) \<and> (f`(topspace T1) \<subseteq> (\<Union> S)))"
-unfolding continuous_on_topo_def topology_generated_by_topspace
-proof (auto simp add: topology_generated_by_Basis)
-  assume H: "\<forall>U. U \<in> S \<longrightarrow> openin T1 (f -` U \<inter> topspace T1)"
-  fix U assume "openin (topology_generated_by S) U"
-  then have "generate_topology_on S U" by (rule openin_topology_generated_by)
-  then show "openin T1 (f -` U \<inter> topspace T1)"
-  proof (induct)
-    fix a b
-    assume H: "openin T1 (f -` a \<inter> topspace T1)" "openin T1 (f -` b \<inter> topspace T1)"
-    have "f -` (a \<inter> b) \<inter> topspace T1 = (f-`a \<inter> topspace T1) \<inter> (f-`b \<inter> topspace T1)"
-      by auto
-    then show "openin T1 (f -` (a \<inter> b) \<inter> topspace T1)" using H by auto
-  next
-    fix K
-    assume H: "openin T1 (f -` k \<inter> topspace T1)" if "k\<in> K" for k
-    define L where "L = {f -` k \<inter> topspace T1|k. k \<in> K}"
-    have *: "openin T1 l" if "l \<in>L" for l using that H unfolding L_def by auto
-    have "openin T1 (\<Union>L)" using openin_Union[OF *] by simp
-    moreover have "(\<Union>L) = (f -` \<Union>K \<inter> topspace T1)" unfolding L_def by auto
-    ultimately show "openin T1 (f -` \<Union>K \<inter> topspace T1)" by simp
-  qed (auto simp add: H)
-qed
-
-lemma continuous_on_generated_topo:
-  assumes "\<And>U. U \<in>S \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
-          "f`(topspace T1) \<subseteq> (\<Union> S)"
-  shows "continuous_on_topo T1 (topology_generated_by S) f"
-  using assms continuous_on_generated_topo_iff by blast
-
-proposition continuous_on_topo_compose:
-  assumes "continuous_on_topo T1 T2 f" "continuous_on_topo T2 T3 g"
-  shows "continuous_on_topo T1 T3 (g o f)"
-  using assms unfolding continuous_on_topo_def
-proof (auto)
-  fix U :: "'c set"
-  assume H: "openin T3 U"
-  have "openin T1 (f -` (g -` U \<inter> topspace T2) \<inter> topspace T1)"
-    using H assms by blast
-  moreover have "f -` (g -` U \<inter> topspace T2) \<inter> topspace T1 = (g \<circ> f) -` U \<inter> topspace T1"
-    using H assms continuous_on_topo_topspace by fastforce
-  ultimately show "openin T1 ((g \<circ> f) -` U \<inter> topspace T1)"
-    by simp
-qed (blast)
-
-lemma continuous_on_topo_preimage_topspace [intro]:
-  assumes "continuous_on_topo T1 T2 f"
-  shows "f-`(topspace T2) \<inter> topspace T1 = topspace T1"
-using assms unfolding continuous_on_topo_def by auto
-
-
-subsubsection%important \<open>Pullback topology\<close>
-
-text \<open>Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
-a special case of this notion, pulling back by the identity. We introduce the general notion as
-we will need it to define the strong operator topology on the space of continuous linear operators,
-by pulling back the product topology on the space of all functions.\<close>
-
-text \<open>\<open>pullback_topology A f T\<close> is the pullback of the topology \<open>T\<close> by the map \<open>f\<close> on
-the set \<open>A\<close>.\<close>
-
-definition%important pullback_topology::"('a set) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b topology) \<Rightarrow> ('a topology)"
-  where "pullback_topology A f T = topology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"
-
-lemma istopology_pullback_topology:
-  "istopology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"
-  unfolding istopology_def proof (auto)
-  fix K assume "\<forall>S\<in>K. \<exists>U. openin T U \<and> S = f -` U \<inter> A"
-  then have "\<exists>U. \<forall>S\<in>K. openin T (U S) \<and> S = f-`(U S) \<inter> A"
-    by (rule bchoice)
-  then obtain U where U: "\<forall>S\<in>K. openin T (U S) \<and> S = f-`(U S) \<inter> A"
-    by blast
-  define V where "V = (\<Union>S\<in>K. U S)"
-  have "openin T V" "\<Union>K = f -` V \<inter> A" unfolding V_def using U by auto
-  then show "\<exists>V. openin T V \<and> \<Union>K = f -` V \<inter> A" by auto
-qed
-
-lemma openin_pullback_topology:
-  "openin (pullback_topology A f T) S \<longleftrightarrow> (\<exists>U. openin T U \<and> S = f-`U \<inter> A)"
-unfolding pullback_topology_def topology_inverse'[OF istopology_pullback_topology] by auto
-
-lemma topspace_pullback_topology:
-  "topspace (pullback_topology A f T) = f-`(topspace T) \<inter> A"
-by (auto simp add: topspace_def openin_pullback_topology)
-
-proposition continuous_on_topo_pullback [intro]:
-  assumes "continuous_on_topo T1 T2 g"
-  shows "continuous_on_topo (pullback_topology A f T1) T2 (g o f)"
-unfolding continuous_on_topo_def
-proof (auto)
-  fix U::"'b set" assume "openin T2 U"
-  then have "openin T1 (g-`U \<inter> topspace T1)"
-    using assms unfolding continuous_on_topo_def by auto
-  have "(g o f)-`U \<inter> topspace (pullback_topology A f T1) = (g o f)-`U \<inter> A \<inter> f-`(topspace T1)"
-    unfolding topspace_pullback_topology by auto
-  also have "... = f-`(g-`U \<inter> topspace T1) \<inter> A "
-    by auto
-  also have "openin (pullback_topology A f T1) (...)"
-    unfolding openin_pullback_topology using \<open>openin T1 (g-`U \<inter> topspace T1)\<close> by auto
-  finally show "openin (pullback_topology A f T1) ((g \<circ> f) -` U \<inter> topspace (pullback_topology A f T1))"
-    by auto
-next
-  fix x assume "x \<in> topspace (pullback_topology A f T1)"
-  then have "f x \<in> topspace T1"
-    unfolding topspace_pullback_topology by auto
-  then show "g (f x) \<in> topspace T2"
-    using assms unfolding continuous_on_topo_def by auto
-qed
-
-proposition continuous_on_topo_pullback' [intro]:
-  assumes "continuous_on_topo T1 T2 (f o g)" "topspace T1 \<subseteq> g-`A"
-  shows "continuous_on_topo T1 (pullback_topology A f T2) g"
-unfolding continuous_on_topo_def
-proof (auto)
-  fix U assume "openin (pullback_topology A f T2) U"
-  then have "\<exists>V. openin T2 V \<and> U = f-`V \<inter> A"
-    unfolding openin_pullback_topology by auto
-  then obtain V where "openin T2 V" "U = f-`V \<inter> A"
-    by blast
-  then have "g -` U \<inter> topspace T1 = g-`(f-`V \<inter> A) \<inter> topspace T1"
-    by blast
-  also have "... = (f o g)-`V \<inter> (g-`A \<inter> topspace T1)"
-    by auto
-  also have "... = (f o g)-`V \<inter> topspace T1"
-    using assms(2) by auto
-  also have "openin T1 (...)"
-    using assms(1) \<open>openin T2 V\<close> by auto
-  finally show "openin T1 (g -` U \<inter> topspace T1)" by simp
-next
-  fix x assume "x \<in> topspace T1"
-  have "(f o g) x \<in> topspace T2"
-    using assms(1) \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto
-  then have "g x \<in> f-`(topspace T2)"
-    unfolding comp_def by blast
-  moreover have "g x \<in> A" using assms(2) \<open>x \<in> topspace T1\<close> by blast
-  ultimately show "g x \<in> topspace (pullback_topology A f T2)"
-    unfolding topspace_pullback_topology by blast
-qed
-
-
 subsection \<open>The product topology\<close>
 
 text \<open>We can now define the product topology, as generated by
@@ -605,6 +242,9 @@
   then show ?thesis using \<open>x \<in> U\<close> by auto
 qed
 
+lemma product_topology_empty_discrete:
+   "product_topology T {} = discrete_topology {(\<lambda>x. undefined)}"
+  by (simp add: subtopology_eq_discrete_topology_sing)
 
 lemma openin_product_topology:
    "openin (product_topology X I) =
@@ -793,6 +433,15 @@
   using PiE_singleton closedin_product_topology [of X I]
   by (metis (no_types, lifting) all_not_in_conv insertI1)
 
+lemma product_topology_empty:
+   "product_topology X {} = topology (\<lambda>S. S \<in> {{},{\<lambda>k. undefined}})"
+  unfolding product_topology union_of_def intersection_of_def arbitrary_def relative_to_def
+  by (auto intro: arg_cong [where f=topology])
+
+lemma openin_product_topology_empty: "openin (product_topology X {}) S \<longleftrightarrow> S \<in> {{},{\<lambda>k. undefined}}"
+  unfolding union_of_def intersection_of_def arbitrary_def relative_to_def openin_product_topology
+  by auto
+
 
 subsubsection \<open>The basic property of the product topology is the continuity of projections:\<close>
 
@@ -949,10 +598,10 @@
   by (rule continuous_on_topo_product_coordinates, simp)
 
 lemma continuous_on_coordinatewise_then_product [intro, continuous_intros]:
-  fixes f :: "('a \<Rightarrow> real) \<Rightarrow> 'b \<Rightarrow> real"
+  fixes f :: "'a::topological_space \<Rightarrow> 'b \<Rightarrow> 'c::topological_space"
   assumes "\<And>i. continuous_on S (\<lambda>x. f x i)"
   shows "continuous_on S f"
-  using continuous_on_topo_coordinatewise_then_product [of UNIV, where T = "\<lambda>i. euclideanreal"]
+  using continuous_on_topo_coordinatewise_then_product [of UNIV, where T = "\<lambda>i. euclidean"]
   by (metis UNIV_I assms continuous_on_continuous_on_topo euclidean_product_topology)
 
 lemma continuous_on_product_then_coordinatewise_UNIV:
@@ -1583,4 +1232,354 @@
 instance "fun" :: (countable, polish_space) polish_space
 by standard
 
+
+subsection\<open>The Alexander subbase theorem\<close>
+
+theorem Alexander_subbase:
+  assumes X: "topology (arbitrary union_of (finite intersection_of (\<lambda>x. x \<in> \<B>) relative_to \<Union>\<B>)) = X"
+    and fin: "\<And>C. \<lbrakk>C \<subseteq> \<B>; \<Union>C = topspace X\<rbrakk> \<Longrightarrow> \<exists>C'. finite C' \<and> C' \<subseteq> C \<and> \<Union>C' = topspace X"
+  shows "compact_space X"
+proof -
+  have U\<B>: "\<Union>\<B> = topspace X"
+    by (simp flip: X)
+  have False if \<U>: "\<forall>U\<in>\<U>. openin X U" and sub: "topspace X \<subseteq> \<Union>\<U>"
+    and neg: "\<And>\<F>. \<lbrakk>\<F> \<subseteq> \<U>; finite \<F>\<rbrakk> \<Longrightarrow> \<not> topspace X \<subseteq> \<Union>\<F>" for \<U>
+  proof -
+    define \<A> where "\<A> \<equiv> {\<C>. (\<forall>U \<in> \<C>. openin X U) \<and> topspace X \<subseteq> \<Union>\<C> \<and> (\<forall>\<F>. finite \<F> \<longrightarrow> \<F> \<subseteq> \<C> \<longrightarrow> ~(topspace X \<subseteq> \<Union>\<F>))}"
+    have 1: "\<A> \<noteq> {}"
+      unfolding \<A>_def using sub \<U> neg by force
+    have 2: "\<Union>\<C> \<in> \<A>" if "\<C>\<noteq>{}" and \<C>: "subset.chain \<A> \<C>" for \<C>
+      unfolding \<A>_def
+    proof (intro CollectI conjI ballI allI impI notI)
+      show "openin X U" if U: "U \<in> \<Union>\<C>" for U
+        using U \<C> unfolding \<A>_def subset_chain_def by force
+      have "\<C> \<subseteq> \<A>"
+        using subset_chain_def \<C> by blast
+      with that \<A>_def show UUC: "topspace X \<subseteq> \<Union>(\<Union>\<C>)"
+        by blast
+      show "False" if "finite \<F>" and "\<F> \<subseteq> \<Union>\<C>" and "topspace X \<subseteq> \<Union>\<F>" for \<F>
+      proof -
+        obtain \<B> where "\<B> \<in> \<C>" "\<F> \<subseteq> \<B>"
+          by (metis Sup_empty \<C> \<open>\<F> \<subseteq> \<Union>\<C>\<close> \<open>finite \<F>\<close> UUC empty_subsetI finite.emptyI finite_subset_Union_chain neg)
+        then show False
+          using \<A>_def \<open>\<C> \<subseteq> \<A>\<close> \<open>finite \<F>\<close> \<open>topspace X \<subseteq> \<Union>\<F>\<close> by blast
+      qed
+    qed
+    obtain \<K> where "\<K> \<in> \<A>" and "\<And>X. \<lbrakk>X\<in>\<A>; \<K> \<subseteq> X\<rbrakk> \<Longrightarrow> X = \<K>"
+      using subset_Zorn_nonempty [OF 1 2] by metis
+    then have *: "\<And>\<W>. \<lbrakk>\<And>W. W\<in>\<W> \<Longrightarrow> openin X W; topspace X \<subseteq> \<Union>\<W>; \<K> \<subseteq> \<W>;
+                        \<And>\<F>. \<lbrakk>finite \<F>; \<F> \<subseteq> \<W>; topspace X \<subseteq> \<Union>\<F>\<rbrakk> \<Longrightarrow> False\<rbrakk>
+           \<Longrightarrow> \<W> = \<K>"
+      and ope: "\<forall>U\<in>\<K>. openin X U" and top: "topspace X \<subseteq> \<Union>\<K>"
+      and non: "\<And>\<F>. \<lbrakk>finite \<F>; \<F> \<subseteq> \<K>; topspace X \<subseteq> \<Union>\<F>\<rbrakk> \<Longrightarrow> False"
+      unfolding \<A>_def by simp_all metis+
+    then obtain x where "x \<in> topspace X" "x \<notin> \<Union>(\<B> \<inter> \<K>)"
+    proof -
+      have "\<Union>(\<B> \<inter> \<K>) \<noteq> \<Union>\<B>"
+        by (metis \<open>\<Union>\<B> = topspace X\<close> fin inf.bounded_iff non order_refl)
+      then have "\<exists>a. a \<notin> \<Union>(\<B> \<inter> \<K>) \<and> a \<in> \<Union>\<B>"
+        by blast
+      then show ?thesis
+        using that by (metis U\<B>)
+    qed
+    obtain C where C: "openin X C" "C \<in> \<K>" "x \<in> C"
+      using \<open>x \<in> topspace X\<close> ope top by auto
+    then have "C \<subseteq> topspace X"
+      by (metis openin_subset)
+    then have "(arbitrary union_of (finite intersection_of (\<lambda>x. x \<in> \<B>) relative_to \<Union>\<B>)) C"
+      using openin_subbase C unfolding X [symmetric] by blast
+    moreover have "C \<noteq> topspace X"
+      using \<open>\<K> \<in> \<A>\<close> \<open>C \<in> \<K>\<close> unfolding \<A>_def by blast
+    ultimately obtain \<V> W where W: "(finite intersection_of (\<lambda>x. x \<in> \<B>) relative_to topspace X) W"
+      and "x \<in> W" "W \<in> \<V>" "\<Union>\<V> \<noteq> topspace X" "C = \<Union>\<V>"
+      using C  by (auto simp: union_of_def U\<B>)
+    then have "\<Union>\<V> \<subseteq> topspace X"
+      by (metis \<open>C \<subseteq> topspace X\<close>)
+    then have "topspace X \<notin> \<V>"
+      using \<open>\<Union>\<V> \<noteq> topspace X\<close> by blast
+    then obtain \<B>' where \<B>': "finite \<B>'" "\<B>' \<subseteq> \<B>" "x \<in> \<Inter>\<B>'" "W = topspace X \<inter> \<Inter>\<B>'"
+      using W \<open>x \<in> W\<close> unfolding relative_to_def intersection_of_def by auto
+    then have "\<Inter>\<B>' \<subseteq> \<Union>\<B>"
+      using \<open>W \<in> \<V>\<close> \<open>\<Union>\<V> \<noteq> topspace X\<close> \<open>\<Union>\<V> \<subseteq> topspace X\<close> by blast
+    then have "\<Inter>\<B>' \<subseteq> C"
+      using U\<B> \<open>C = \<Union>\<V>\<close> \<open>W = topspace X \<inter> \<Inter>\<B>'\<close> \<open>W \<in> \<V>\<close> by auto
+    have "\<forall>b \<in> \<B>'. \<exists>C'. finite C' \<and> C' \<subseteq> \<K> \<and> topspace X \<subseteq> \<Union>(insert b C')"
+    proof
+      fix b
+      assume "b \<in> \<B>'"
+      have "insert b \<K> = \<K>" if neg: "\<not> (\<exists>C'. finite C' \<and> C' \<subseteq> \<K> \<and> topspace X \<subseteq> \<Union>(insert b C'))"
+      proof (rule *)
+        show "openin X W" if "W \<in> insert b \<K>" for W
+          using that
+        proof
+          have "b \<in> \<B>"
+            using \<open>b \<in> \<B>'\<close> \<open>\<B>' \<subseteq> \<B>\<close> by blast
+          then have "\<exists>\<U>. finite \<U> \<and> \<U> \<subseteq> \<B> \<and> \<Inter>\<U> = b"
+            by (rule_tac x="{b}" in exI) auto
+          moreover have "\<Union>\<B> \<inter> b = b"
+            using \<B>'(2) \<open>b \<in> \<B>'\<close> by auto
+          ultimately show "openin X W" if "W = b"
+            using  that \<open>b \<in> \<B>'\<close>
+            apply (simp add: openin_subbase flip: X)
+            apply (auto simp: arbitrary_def intersection_of_def relative_to_def intro!: union_of_inc)
+            done
+          show "openin X W" if "W \<in> \<K>"
+            by (simp add: \<open>W \<in> \<K>\<close> ope)
+        qed
+      next
+        show "topspace X \<subseteq> \<Union> (insert b \<K>)"
+          using top by auto
+      next
+        show False if "finite \<F>" and "\<F> \<subseteq> insert b \<K>" "topspace X \<subseteq> \<Union>\<F>" for \<F>
+        proof -
+          have "insert b (\<F> \<inter> \<K>) = \<F>"
+            using non that by blast
+          then show False
+            by (metis Int_lower2 finite_insert neg that(1) that(3))
+        qed
+      qed auto
+      then show "\<exists>C'. finite C' \<and> C' \<subseteq> \<K> \<and> topspace X \<subseteq> \<Union>(insert b C')"
+        using \<open>b \<in> \<B>'\<close> \<open>x \<notin> \<Union>(\<B> \<inter> \<K>)\<close> \<B>'
+        by (metis IntI InterE Union_iff subsetD insertI1)
+    qed
+    then obtain F where F: "\<forall>b \<in> \<B>'. finite (F b) \<and> F b \<subseteq> \<K> \<and> topspace X \<subseteq> \<Union>(insert b (F b))"
+      by metis
+    let ?\<D> = "insert C (\<Union>(F ` \<B>'))"
+    show False
+    proof (rule non)
+      have "topspace X \<subseteq> (\<Inter>b \<in> \<B>'. \<Union>(insert b (F b)))"
+        using F by (simp add: INT_greatest)
+      also have "\<dots> \<subseteq> \<Union>?\<D>"
+        using \<open>\<Inter>\<B>' \<subseteq> C\<close> by force
+      finally show "topspace X \<subseteq> \<Union>?\<D>" .
+      show "?\<D> \<subseteq> \<K>"
+        using \<open>C \<in> \<K>\<close> F by auto
+      show "finite ?\<D>"
+        using \<open>finite \<B>'\<close> F by auto
+    qed
+  qed
+  then show ?thesis
+    by (force simp: compact_space_def compactin_def)
+qed
+
+
+corollary Alexander_subbase_alt:
+  assumes "U \<subseteq> \<Union>\<B>"
+  and fin: "\<And>C. \<lbrakk>C \<subseteq> \<B>; U \<subseteq> \<Union>C\<rbrakk> \<Longrightarrow> \<exists>C'. finite C' \<and> C' \<subseteq> C \<and> U \<subseteq> \<Union>C'"
+   and X: "topology
+              (arbitrary union_of
+                   (finite intersection_of (\<lambda>x. x \<in> \<B>) relative_to U)) = X"
+ shows "compact_space X"
+proof -
+  have "topspace X = U"
+    using X topspace_subbase by fastforce
+  have eq: "\<Union> (Collect ((\<lambda>x. x \<in> \<B>) relative_to U)) = U"
+    unfolding relative_to_def
+    using \<open>U \<subseteq> \<Union>\<B>\<close> by blast
+  have *: "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<C> \<and> \<Union>\<F> = topspace X"
+    if  "\<C> \<subseteq> Collect ((\<lambda>x. x \<in> \<B>) relative_to topspace X)" and UC: "\<Union>\<C> = topspace X" for \<C>
+  proof -
+    have "\<C> \<subseteq> (\<lambda>U. topspace X \<inter> U) ` \<B>"
+      using that by (auto simp: relative_to_def)
+    then obtain \<B>' where "\<B>' \<subseteq> \<B>" and \<B>': "\<C> = (\<inter>) (topspace X) ` \<B>'"
+      by (auto simp: subset_image_iff)
+    moreover have "U \<subseteq> \<Union>\<B>'"
+      using \<B>' \<open>topspace X = U\<close> UC by auto
+    ultimately obtain \<C>' where "finite \<C>'" "\<C>' \<subseteq> \<B>'" "U \<subseteq> \<Union>\<C>'"
+      using fin [of \<B>'] \<open>topspace X = U\<close> \<open>U \<subseteq> \<Union>\<B>\<close> by blast
+    then show ?thesis
+      unfolding \<B>' exists_finite_subset_image \<open>topspace X = U\<close> by auto
+  qed
+  show ?thesis
+    apply (rule Alexander_subbase [where \<B> = "Collect ((\<lambda>x. x \<in> \<B>) relative_to (topspace X))"])
+     apply (simp flip: X)
+     apply (metis finite_intersection_of_relative_to eq)
+    apply (blast intro: *)
+    done
+qed
+
+proposition continuous_map_componentwise:
+   "continuous_map X (product_topology Y I) f \<longleftrightarrow>
+    f ` (topspace X) \<subseteq> extensional I \<and> (\<forall>k \<in> I. continuous_map X (Y k) (\<lambda>x. f x k))"
+    (is "?lhs \<longleftrightarrow> _ \<and> ?rhs")
+proof (cases "\<forall>x \<in> topspace X. f x \<in> extensional I")
+  case True
+  then have "f ` (topspace X) \<subseteq> extensional I"
+    by force
+  moreover have ?rhs if L: ?lhs
+  proof -
+    have "openin X {x \<in> topspace X. f x k \<in> U}" if "k \<in> I" and "openin (Y k) U" for k U
+    proof -
+      have "openin (product_topology Y I) ({Y. Y k \<in> U} \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (Y i)))"
+        apply (simp add: openin_product_topology flip: arbitrary_union_of_relative_to)
+        apply (simp add: relative_to_def)
+        using that apply (blast intro: arbitrary_union_of_inc finite_intersection_of_inc)
+        done
+      with that have "openin X {x \<in> topspace X. f x \<in> ({Y. Y k \<in> U} \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (Y i)))}"
+        using L unfolding continuous_map_def by blast
+      moreover have "{x \<in> topspace X. f x \<in> ({Y. Y k \<in> U} \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (Y i)))} = {x \<in> topspace X. f x k \<in> U}"
+        using L by (auto simp: continuous_map_def)
+      ultimately show ?thesis
+        by metis
+    qed
+    with that
+    show ?thesis
+      by (auto simp: continuous_map_def)
+  qed
+  moreover have ?lhs if ?rhs
+  proof -
+    have 1: "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (Y i))"
+      using that True by (auto simp: continuous_map_def PiE_iff)
+    have 2: "{x \<in> S. \<exists>T\<in>\<T>. f x \<in> T} = (\<Union>T\<in>\<T>. {x \<in> S. f x \<in> T})" for S \<T>
+      by blast
+    have 3: "{x \<in> S. \<forall>U\<in>\<U>. f x \<in> U} = (\<Inter> (insert S ((\<lambda>U. {x \<in> S. f x \<in> U}) ` \<U>)))" for S \<U>
+      by blast
+    show ?thesis
+      unfolding continuous_map_def openin_product_topology arbitrary_def
+    proof (clarsimp simp: all_union_of 1 2)
+      fix \<T>
+      assume \<T>: "\<T> \<subseteq> Collect (finite intersection_of (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (Y i) U)
+                  relative_to (\<Pi>\<^sub>E i\<in>I. topspace (Y i)))"
+      show "openin X (\<Union>T\<in>\<T>. {x \<in> topspace X. f x \<in> T})"
+      proof (rule openin_Union; clarify)
+        fix S T
+        assume "T \<in> \<T>"
+        obtain \<U> where "T = (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> \<Inter>\<U>" and "finite \<U>"
+          "\<U> \<subseteq> {{f. f i \<in> U} |i U. i \<in> I \<and> openin (Y i) U}"
+          using subsetD [OF \<T> \<open>T \<in> \<T>\<close>] by (auto simp: intersection_of_def relative_to_def)
+        with that show "openin X {x \<in> topspace X. f x \<in> T}"
+          apply (simp add: continuous_map_def 1 cong: conj_cong)
+          unfolding 3
+          apply (rule openin_Inter; auto)
+          done
+      qed
+    qed
+  qed
+  ultimately show ?thesis
+    by metis
+next
+  case False
+  then show ?thesis
+    by (auto simp: continuous_map_def PiE_def)
+qed
+
+
+lemma continuous_map_componentwise_UNIV:
+   "continuous_map X (product_topology Y UNIV) f \<longleftrightarrow> (\<forall>k. continuous_map X (Y k) (\<lambda>x. f x k))"
+  by (simp add: continuous_map_componentwise)
+
+lemma continuous_map_product_projection [continuous_intros]:
+   "k \<in> I \<Longrightarrow> continuous_map (product_topology X I) (X k) (\<lambda>x. x k)"
+  using continuous_map_componentwise [of "product_topology X I" X I id] by simp
+
+proposition open_map_product_projection:
+  assumes "i \<in> I"
+  shows "open_map (product_topology Y I) (Y i) (\<lambda>f. f i)"
+  unfolding openin_product_topology all_union_of arbitrary_def open_map_def image_Union
+proof clarify
+  fix \<V>
+  assume \<V>: "\<V> \<subseteq> Collect
+               (finite intersection_of
+                (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (Y i) U) relative_to
+                           topspace (product_topology Y I))"
+  show "openin (Y i) (\<Union>x\<in>\<V>. (\<lambda>f. f i) ` x)"
+  proof (rule openin_Union, clarify)
+    fix S V
+    assume "V \<in> \<V>"
+    obtain \<F> where "finite \<F>"
+      and V: "V = (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> \<Inter>\<F>"
+      and \<F>: "\<F> \<subseteq> {{f. f i \<in> U} |i U. i \<in> I \<and> openin (Y i) U}"
+      using subsetD [OF \<V> \<open>V \<in> \<V>\<close>]
+      by (auto simp: intersection_of_def relative_to_def)
+    show "openin (Y i) ((\<lambda>f. f i) ` V)"
+    proof (subst openin_subopen; clarify)
+      fix x f
+      assume "f \<in> V"
+      let ?T = "{a \<in> topspace(Y i).
+                   (\<lambda>j. if j = i then a
+                        else if j \<in> I then f j else undefined) \<in> (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> \<Inter>\<F>}"
+      show "\<exists>T. openin (Y i) T \<and> f i \<in> T \<and> T \<subseteq> (\<lambda>f. f i) ` V"
+      proof (intro exI conjI)
+        show "openin (Y i) ?T"
+        proof (rule openin_continuous_map_preimage)
+          have "continuous_map (Y i) (Y k) (\<lambda>x. if k = i then x else f k)" if "k \<in> I" for k
+          proof (cases "k=i")
+            case True
+            then show ?thesis
+              by (metis (mono_tags) continuous_map_id eq_id_iff)
+          next
+            case False
+            then show ?thesis
+              by simp (metis IntD1 PiE_iff V \<open>f \<in> V\<close> that)
+          qed
+          then show "continuous_map (Y i) (product_topology Y I)
+                  (\<lambda>x j. if j = i then x else if j \<in> I then f j else undefined)"
+            by (auto simp: continuous_map_componentwise assms extensional_def)
+        next
+          have "openin (product_topology Y I) (\<Pi>\<^sub>E i\<in>I. topspace (Y i))"
+            by (metis openin_topspace topspace_product_topology)
+          moreover have "openin (product_topology Y I) (\<Inter>B\<in>\<F>. (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> B)"
+                         if "\<F> \<noteq> {}"
+          proof -
+            show ?thesis
+            proof (rule openin_Inter)
+              show "\<And>X. X \<in> (\<inter>) (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) ` \<F> \<Longrightarrow> openin (product_topology Y I) X"
+                unfolding openin_product_topology relative_to_def
+                apply (clarify intro!: arbitrary_union_of_inc)
+                apply (rename_tac F)
+                apply (rule_tac x=F in exI)
+                using subsetD [OF \<F>]
+                apply (force intro: finite_intersection_of_inc)
+                done
+            qed (use \<open>finite \<F>\<close> \<open>\<F> \<noteq> {}\<close> in auto)
+          qed
+          ultimately show "openin (product_topology Y I) ((\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> \<Inter>\<F>)"
+            by (auto simp only: Int_Inter_eq split: if_split)
+        qed
+      next
+        have eqf: "(\<lambda>j. if j = i then f i else if j \<in> I then f j else undefined) = f"
+          using PiE_arb V \<open>f \<in> V\<close> by force
+        show "f i \<in> ?T"
+          using V assms \<open>f \<in> V\<close> by (auto simp: PiE_iff eqf)
+      next
+        show "?T \<subseteq> (\<lambda>f. f i) ` V"
+          unfolding V by (auto simp: intro!: rev_image_eqI)
+      qed
+    qed
+  qed
+qed
+
+lemma retraction_map_product_projection:
+  assumes "i \<in> I"
+  shows "(retraction_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
+  then show ?rhs
+    using retraction_imp_surjective_map by force
+next
+  assume R: ?rhs
+  show ?lhs
+  proof (cases "topspace (product_topology X I) = {}")
+    case True
+    then show ?thesis
+      using R by (auto simp: retraction_map_def retraction_maps_def continuous_map_on_empty)
+  next
+    case False
+    have *: "\<exists>g. continuous_map (X i) (product_topology X I) g \<and> (\<forall>x\<in>topspace (X i). g x i = x)"
+      if z: "z \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))" for z
+    proof -
+      have cm: "continuous_map (X i) (X j) (\<lambda>x. if j = i then x else z j)" if "j \<in> I" for j
+        using \<open>j \<in> I\<close> z  by (case_tac "j = i") auto
+      show ?thesis
+        using \<open>i \<in> I\<close> that
+        by (rule_tac x="\<lambda>x j. if j = i then x else z j" in exI) (auto simp: continuous_map_componentwise PiE_iff extensional_def cm)
+    qed
+    show ?thesis
+      using \<open>i \<in> I\<close> False
+      by (auto simp: retraction_map_def retraction_maps_def assms continuous_map_product_projection *)
+  qed
+qed
+
 end