src/HOL/Analysis/Function_Topology.thy

tuned;

(*  Author:  Sébastien Gouëzel   [e-mail] with additions from LCP
    License: BSD
*)

theory Function_Topology
  imports
    Elementary_Topology
    Abstract_Limits
    Connected
begin


section \<open>Function Topology\<close>

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
space along the other coordinates. This is the coarsest topology for which the projection
to each factor is continuous.

To form a product of objects in Isabelle/HOL, all these objects should be subsets of a common type
'a. The product is then \<^term>\<open>Pi\<^sub>E I X\<close>, the set of elements from \<open>'i\<close> to \<open>'a\<close> such that the \<open>i\<close>-th
coordinate belongs to \<open>X i\<close> for all \<open>i \<in> I\<close>.

Hence, to form a product of topological spaces, all these spaces should be subsets of a common type.
This means that type classes can not be used to define such a product if one wants to take the
product of different topological spaces (as the type 'a can only be given one structure of
topological space using type classes). On the other hand, one can define different topologies (as
introduced in \<open>thy\<close>) on one type, and these topologies do not need to
share the same maximal open set. Hence, one can form a product of topologies in this sense, and
this works well. The big caveat is that it does not interact well with the main body of
topology in Isabelle/HOL defined in terms of type classes... For instance, continuity of maps
is not defined in this setting.

As the product of different topological spaces is very important in several areas of
mathematics (for instance adeles), I introduce below the product topology in terms of topologies,
and reformulate afterwards the consequences in terms of type classes (which are of course very
handy for applications).

Given this limitation, it looks to me that it would be very beneficial to revamp the theory
of topological spaces in Isabelle/HOL in terms of topologies, and keep the statements involving
type classes as consequences of more general statements in terms of topologies (but I am
probably too naive here).

Here is an example of a reformulation using topologies. Let
@{text [display]
\<open>continuous_map T1 T2 f =
    ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
            \<and> (f`(topspace T1) \<subseteq> (topspace T2)))\<close>}
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_map (top_of_set s) (topology euclidean) f\<close>}

In fact, I need \<open>continuous_map\<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
the above equivalence in Lemma~\<open>continuous_map_iff_continuous\<close>.

I only develop the basics of the product topology in this theory. The most important missing piece
is Tychonov theorem, stating that a product of compact spaces is always compact for the product
topology, even when the product is not finite (or even countable).

I realized afterwards that this theory has a lot in common with \<^file>\<open>~~/src/HOL/Library/Finite_Map.thy\<close>.
\<close>

subsection \<open>The product topology\<close>

text \<open>We can now define the product topology, as generated by
the sets which are products of open sets along finitely many coordinates, and the whole
space along the other coordinates. Equivalently, it is generated by sets which are one open
set along one single coordinate, and the whole space along other coordinates. In fact, this is only
equivalent for nonempty products, but for the empty product the first formulation is better
(the second one gives an empty product space, while an empty product should have exactly one
point, equal to \<open>undefined\<close> along all coordinates.

So, we use the first formulation, which moreover seems to give rise to more straightforward proofs.
\<close>

definition\<^marker>\<open>tag important\<close> product_topology::"('i \<Rightarrow> ('a topology)) \<Rightarrow> ('i set) \<Rightarrow> (('i \<Rightarrow> 'a) topology)"
  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>

proposition product_topology:
  "product_topology X I =
   topology
    (arbitrary union_of
       ((finite intersection_of
        (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U))
        relative_to (\<Pi>\<^sub>E i\<in>I. topspace (X i))))"
  (is "_ = topology (_ union_of ((_ intersection_of ?\<Psi>) relative_to ?TOP))")
proof -
  let ?\<Omega> = "(\<lambda>F. \<exists>Y. F = Pi\<^sub>E I Y \<and> (\<forall>i. openin (X i) (Y i)) \<and> finite {i. Y i \<noteq> topspace (X i)})"
  have *: "(finite' intersection_of ?\<Omega>) A = (finite intersection_of ?\<Psi> relative_to ?TOP) A" for A
  proof -
    have 1: "\<exists>U. (\<exists>\<U>. finite \<U> \<and> \<U> \<subseteq> Collect ?\<Psi> \<and> \<Inter>\<U> = U) \<and> ?TOP \<inter> U = \<Inter>\<U>"
      if \<U>: "\<U> \<subseteq> Collect ?\<Omega>" and "finite' \<U>" "A = \<Inter>\<U>" "\<U> \<noteq> {}" for \<U>
    proof -
      have "\<forall>U \<in> \<U>. \<exists>Y. U = Pi\<^sub>E I Y \<and> (\<forall>i. openin (X i) (Y i)) \<and> finite {i. Y i \<noteq> topspace (X i)}"
        using \<U> by auto
      then obtain Y where Y: "\<And>U. U \<in> \<U> \<Longrightarrow> U = Pi\<^sub>E I (Y U) \<and> (\<forall>i. openin (X i) (Y U i)) \<and> finite {i. (Y U) i \<noteq> topspace (X i)}"
        by metis
      obtain U where "U \<in> \<U>"
        using \<open>\<U> \<noteq> {}\<close> by blast
      let ?F = "\<lambda>U. (\<lambda>i. {f. f i \<in> Y U i}) ` {i \<in> I. Y U i \<noteq> topspace (X i)}"
      show ?thesis
      proof (intro conjI exI)
        show "finite (\<Union>U\<in>\<U>. ?F U)"
          using Y \<open>finite' \<U>\<close> by auto
        show "?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U) = \<Inter>\<U>"
        proof
          have *: "f \<in> U"
            if "U \<in> \<U>" and "\<forall>V\<in>\<U>. \<forall>i. i \<in> I \<and> Y V i \<noteq> topspace (X i) \<longrightarrow> f i \<in> Y V i"
              and "\<forall>i\<in>I. f i \<in> topspace (X i)" and "f \<in> extensional I" for f U
            by (smt (verit) PiE_iff Y that)
          show "?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U) \<subseteq> \<Inter>\<U>"
            by (auto simp: PiE_iff *)
          show "\<Inter>\<U> \<subseteq> ?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U)"
            using Y openin_subset \<open>finite' \<U>\<close> by fastforce
        qed
      qed (use Y openin_subset in \<open>blast+\<close>)
    qed
    have 2: "\<exists>\<U>'. finite' \<U>' \<and> \<U>' \<subseteq> Collect ?\<Omega> \<and> \<Inter>\<U>' = ?TOP \<inter> \<Inter>\<U>"
      if \<U>: "\<U> \<subseteq> Collect ?\<Psi>" and "finite \<U>" for \<U>
    proof (cases "\<U>={}")
      case True
      then show ?thesis
        apply (rule_tac x="{?TOP}" in exI, simp)
        apply (rule_tac x="\<lambda>i. topspace (X i)" in exI)
        apply force
        done
    next
      case False
      then obtain U where "U \<in> \<U>"
        by blast
      have "\<forall>U \<in> \<U>. \<exists>i Y. U = {f. f i \<in> Y} \<and> i \<in> I \<and> openin (X i) Y"
        using \<U> by auto
      then obtain J Y where
        Y: "\<And>U. U \<in> \<U> \<Longrightarrow> U = {f. f (J U) \<in> Y U} \<and> J U \<in> I \<and> openin (X (J U)) (Y U)"
        by metis
      let ?G = "\<lambda>U. \<Pi>\<^sub>E i\<in>I. if i = J U then Y U else topspace (X i)"
      show ?thesis
      proof (intro conjI exI)
        show "finite (?G ` \<U>)" "?G ` \<U> \<noteq> {}"
          using \<open>finite \<U>\<close> \<open>U \<in> \<U>\<close> by blast+
        have *: "\<And>U. U \<in> \<U> \<Longrightarrow> openin (X (J U)) (Y U)"
          using Y by force
        show "?G ` \<U> \<subseteq> {Pi\<^sub>E I Y |Y. (\<forall>i. openin (X i) (Y i)) \<and> finite {i. Y i \<noteq> topspace (X i)}}"
          apply clarsimp
          apply (rule_tac x= "(\<lambda>i. if i = J U then Y U else topspace (X i))" in exI)
          apply (auto simp: *)
          done
      next
        show "(\<Inter>U\<in>\<U>. ?G U) = ?TOP \<inter> \<Inter>\<U>"
        proof
          have "(\<Pi>\<^sub>E i\<in>I. if i = J U then Y U else topspace (X i)) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
            by (simp add: PiE_mono Y \<open>U \<in> \<U>\<close> openin_subset)
          then have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP"
            using \<open>U \<in> \<U>\<close> by fastforce
          moreover have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> \<Inter>\<U>"
            using PiE_mem Y by fastforce
          ultimately show "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP \<inter> \<Inter>\<U>"
            by auto
        qed (use Y in fastforce)
      qed
    qed
    show ?thesis
      unfolding relative_to_def intersection_of_def
      by (safe; blast dest!: 1 2)
  qed
  show ?thesis
    unfolding product_topology_def generate_topology_on_eq
    apply (rule arg_cong [where f = topology])
    apply (rule arg_cong [where f = "(union_of)arbitrary"])
    apply (force simp: *)
    done
qed

lemma topspace_product_topology [simp]:
  "topspace (product_topology T I) = (\<Pi>\<^sub>E i\<in>I. topspace(T i))"
proof
  show "topspace (product_topology T I) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
    unfolding product_topology_def topology_generated_by_topspace
    unfolding topspace_def by auto
  have "(\<Pi>\<^sub>E i\<in>I. topspace (T i)) \<in> {(\<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)}}"
    using openin_topspace not_finite_existsD by auto
  then show "(\<Pi>\<^sub>E i\<in>I. topspace (T i)) \<subseteq> topspace (product_topology T I)"
    unfolding product_topology_def using PiE_def by (auto)
qed

lemma product_topology_basis:
  assumes "\<And>i. openin (T i) (X i)" "finite {i. X i \<noteq> topspace (T i)}"
  shows "openin (product_topology T I) (\<Pi>\<^sub>E i\<in>I. X i)"
  unfolding product_topology_def
  by (rule topology_generated_by_Basis) (use assms in auto)

proposition product_topology_open_contains_basis:
  assumes "openin (product_topology T I) U" "x \<in> U"
  shows "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
proof -
  define IT where "IT \<equiv> \<lambda>X. {i. X i \<noteq> topspace (T i)}"
  have "generate_topology_on {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite (IT X)} U"
    using assms unfolding product_topology_def IT_def by (intro openin_topology_generated_by) auto
  then have "\<And>x. x\<in>U \<Longrightarrow> \<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite (IT X) \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
  proof induction
    case (Int U V x)
    then obtain XU XV where H:
      "x \<in> Pi\<^sub>E I XU" "\<And>i. openin (T i) (XU i)" "finite (IT XU)" "Pi\<^sub>E I XU \<subseteq> U"
      "x \<in> Pi\<^sub>E I XV" "\<And>i. openin (T i) (XV i)" "finite (IT XV)" "Pi\<^sub>E I XV \<subseteq> V"
      by (meson Int_iff)
    define X where "X = (\<lambda>i. XU i \<inter> XV i)"
    have "Pi\<^sub>E I X \<subseteq> Pi\<^sub>E I XU \<inter> Pi\<^sub>E I XV"
      by (auto simp add: PiE_iff X_def)
    then have "Pi\<^sub>E I X \<subseteq> U \<inter> V" using H by auto
    moreover have "\<forall>i. openin (T i) (X i)"
      unfolding X_def using H by auto
    moreover have "finite (IT X)"
      apply (rule rev_finite_subset[of "IT XU \<union> IT XV"])
      using H by (auto simp: X_def IT_def)
    moreover have "x \<in> Pi\<^sub>E I X"
      unfolding X_def using H by auto
    ultimately show ?case
      by auto
  next
    case (UN K x)
    then obtain k where "k \<in> K" "x \<in> k" by auto
    with \<open>k \<in> K\<close> UN show ?case
      by (meson Sup_upper2)
  qed auto
  then show ?thesis using \<open>x \<in> U\<close> IT_def by blast
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) =
    arbitrary union_of
          ((finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U)))
           relative_to topspace (product_topology X I))"
  by (simp add: istopology_subbase product_topology)

lemma subtopology_PiE:
  "subtopology (product_topology X I) (\<Pi>\<^sub>E i\<in>I. (S i)) = product_topology (\<lambda>i. subtopology (X i) (S i)) I"
proof -
  let ?P = "\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U"
  let ?X = "\<Pi>\<^sub>E i\<in>I. topspace (X i)"
  have "finite intersection_of ?P relative_to ?X \<inter> Pi\<^sub>E I S =
        finite intersection_of (?P relative_to ?X \<inter> Pi\<^sub>E I S) relative_to ?X \<inter> Pi\<^sub>E I S"
    by (rule finite_intersection_of_relative_to)
  also have "\<dots> = finite intersection_of
                      ((\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> (openin (X i) relative_to S i) U)
                       relative_to ?X \<inter> Pi\<^sub>E I S)
                   relative_to ?X \<inter> Pi\<^sub>E I S"
    apply (rule arg_cong2 [where f = "(relative_to)"])
     apply (rule arg_cong [where f = "(intersection_of)finite"])
     apply (rule ext)
     apply (auto simp: relative_to_def intersection_of_def)
    done
  finally
  have "finite intersection_of ?P relative_to ?X \<inter> Pi\<^sub>E I S =
        finite intersection_of
          (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> (openin (X i) relative_to S i) U)
          relative_to ?X \<inter> Pi\<^sub>E I S"
    by (metis finite_intersection_of_relative_to)
  then show ?thesis
  unfolding topology_eq
  apply clarify
  apply (simp add: openin_product_topology flip: openin_relative_to)
  apply (simp add: arbitrary_union_of_relative_to flip: PiE_Int)
  done
qed

lemma product_topology_base_alt:
   "finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U))
    relative_to (\<Pi>\<^sub>E i\<in>I. topspace (X i)) =
    (\<lambda>F. (\<exists>U. F =  Pi\<^sub>E I U \<and> finite {i \<in> I. U i \<noteq> topspace(X i)} \<and> (\<forall>i \<in> I. openin (X i) (U i))))"
   (is "?lhs = ?rhs")
proof -
  have "(\<forall>F. ?lhs F \<longrightarrow> ?rhs F)"
    unfolding all_relative_to all_intersection_of topspace_product_topology
  proof clarify
    fix \<F>
    assume "finite \<F>" and "\<F> \<subseteq> {{f. f i \<in> U} |i U. i \<in> I \<and> openin (X i) U}"
    then show "\<exists>U. (\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>\<F> = Pi\<^sub>E I U \<and>
          finite {i \<in> I. U i \<noteq> topspace (X i)} \<and> (\<forall>i\<in>I. openin (X i) (U i))"
    proof (induction)
      case (insert F \<F>)
      then obtain U where eq: "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>\<F> = Pi\<^sub>E I U"
        and fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}"
        and ope: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (U i)"
        by auto
      obtain i V where "F = {f. f i \<in> V}" "i \<in> I" "openin (X i) V"
        using insert by auto
      let ?U = "\<lambda>j. U j \<inter> (if j = i then V else topspace(X j))"
      show ?case
      proof (intro exI conjI)
        show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>(insert F \<F>) = Pi\<^sub>E I ?U"
        using eq  PiE_mem \<open>i \<in> I\<close>  by (auto simp: \<open>F = {f. f i \<in> V}\<close>) fastforce
      next
        show "finite {i \<in> I. ?U i \<noteq> topspace (X i)}"
          by (rule rev_finite_subset [OF finite.insertI [OF fin]]) auto
      next
        show "\<forall>i\<in>I. openin (X i) (?U i)"
          by (simp add: \<open>openin (X i) V\<close> ope openin_Int)
      qed
    qed (auto intro: dest: not_finite_existsD)
  qed
  moreover have "(\<forall>F. ?rhs F \<longrightarrow> ?lhs F)"
  proof clarify
    fix U :: "'a \<Rightarrow> 'b set"
    assume fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}" and ope: "\<forall>i\<in>I. openin (X i) (U i)"
    let ?U = "\<Inter>i\<in>{i \<in> I. U i \<noteq> topspace (X i)}. {x. x i \<in> U i}"
    show "?lhs (Pi\<^sub>E I U)"
      unfolding relative_to_def topspace_product_topology
    proof (intro exI conjI)
      show "(finite intersection_of (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U)) ?U"
        using fin ope by (intro finite_intersection_of_Inter finite_intersection_of_inc) auto
      show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> ?U = Pi\<^sub>E I U"
        using ope openin_subset by fastforce
    qed
  qed
  ultimately show ?thesis
    by meson
qed

corollary openin_product_topology_alt:
  "openin (product_topology X I) S \<longleftrightarrow>
    (\<forall>x \<in> S. \<exists>U. finite {i \<in> I. U i \<noteq> topspace(X i)} \<and>
                 (\<forall>i \<in> I. openin (X i) (U i)) \<and> x \<in> Pi\<^sub>E I U \<and> Pi\<^sub>E I U \<subseteq> S)"
  unfolding openin_product_topology arbitrary_union_of_alt product_topology_base_alt topspace_product_topology
  by (smt (verit, best))

lemma closure_of_product_topology:
  "(product_topology X I) closure_of (PiE I S) = PiE I (\<lambda>i. (X i) closure_of (S i))"
proof -
  have *: "(\<forall>T. f \<in> T \<and> openin (product_topology X I) T \<longrightarrow> (\<exists>y\<in>Pi\<^sub>E I S. y \<in> T))
       \<longleftrightarrow> (\<forall>i \<in> I. \<forall>T. f i \<in> T \<and> openin (X i) T \<longrightarrow> S i \<inter> T \<noteq> {})"
    (is "?lhs = ?rhs")
    if top: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> topspace (X i)" and ext:  "f \<in> extensional I" for f
  proof
    assume L[rule_format]: ?lhs
    show ?rhs
    proof clarify
      fix i T
      assume "i \<in> I" "f i \<in> T" "openin (X i) T" "S i \<inter> T = {}"
      then have "openin (product_topology X I) ((\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> {x. x i \<in> T})"
        by (force simp: openin_product_topology intro: arbitrary_union_of_inc relative_to_inc finite_intersection_of_inc)
      then show "False"
        using L [of "topspace (product_topology X I) \<inter> {f. f i \<in> T}"] \<open>S i \<inter> T = {}\<close> \<open>f i \<in> T\<close> \<open>i \<in> I\<close>
        by (auto simp: top ext PiE_iff)
    qed
  next
    assume R [rule_format]: ?rhs
    show ?lhs
    proof (clarsimp simp: openin_product_topology union_of_def arbitrary_def)
      fix \<U> U
      assume
        \<U>: "\<U> \<subseteq> Collect
           (finite intersection_of (\<lambda>F. \<exists>i U. F = {x. x i \<in> U} \<and> i \<in> I \<and> openin (X i) U) relative_to
            (\<Pi>\<^sub>E i\<in>I. topspace (X i)))" and
        "f \<in> U" "U \<in> \<U>"
      then have "(finite intersection_of (\<lambda>F. \<exists>i U. F = {x. x i \<in> U} \<and> i \<in> I \<and> openin (X i) U)
                 relative_to (\<Pi>\<^sub>E i\<in>I. topspace (X i))) U"
        by blast
      with \<open>f \<in> U\<close> \<open>U \<in> \<U>\<close>
      obtain \<T> where "finite \<T>"
        and \<T>: "\<And>C. C \<in> \<T> \<Longrightarrow> \<exists>i \<in> I. \<exists>V. openin (X i) V \<and> C = {x. x i \<in> V}"
        and "topspace (product_topology X I) \<inter> \<Inter> \<T> \<subseteq> U" "f \<in> topspace (product_topology X I) \<inter> \<Inter> \<T>"
        apply (clarsimp simp add: relative_to_def intersection_of_def)
        apply (rule that, auto dest!: subsetD)
        done
      then have "f \<in> PiE I (topspace \<circ> X)" "f \<in> \<Inter>\<T>" and subU: "PiE I (topspace \<circ> X) \<inter> \<Inter>\<T> \<subseteq> U"
        by (auto simp: PiE_iff)
      have *: "f i \<in> topspace (X i) \<inter> \<Inter>{U. openin (X i) U \<and> {x. x i \<in> U} \<in> \<T>}
             \<and> openin (X i) (topspace (X i) \<inter> \<Inter>{U. openin (X i) U \<and> {x. x i \<in> U} \<in> \<T>})"
        if "i \<in> I" for i
      proof -
        have "finite ((\<lambda>U. {x. x i \<in> U}) -` \<T>)"
        proof (rule finite_vimageI [OF \<open>finite \<T>\<close>])
          show "inj (\<lambda>U. {x. x i \<in> U})"
            by (auto simp: inj_on_def)
        qed
        then have fin: "finite {U. openin (X i) U \<and> {x. x i \<in> U} \<in> \<T>}"
          by (rule rev_finite_subset) auto
        have "openin (X i) (\<Inter> (insert (topspace (X i)) {U. openin (X i) U \<and> {x. x i \<in> U} \<in> \<T>}))"
          by (rule openin_Inter) (auto simp: fin)
        then show ?thesis
          using \<open>f \<in> \<Inter> \<T>\<close> by (fastforce simp: that top)
      qed
      define \<Phi> where "\<Phi> \<equiv> \<lambda>i. topspace (X i) \<inter> \<Inter>{U. openin (X i) U \<and> {f. f i \<in> U} \<in> \<T>}"
      have "\<forall>i \<in> I. \<exists>x. x \<in> S i \<inter> \<Phi> i"
        using R [OF _ *] unfolding \<Phi>_def by blast
      then obtain \<theta> where \<theta> [rule_format]: "\<forall>i \<in> I. \<theta> i \<in> S i \<inter> \<Phi> i"
        by metis
      show "\<exists>y\<in>Pi\<^sub>E I S. \<exists>x\<in>\<U>. y \<in> x"
      proof
        show "\<exists>U \<in> \<U>. (\<lambda>i \<in> I. \<theta> i) \<in> U"
        proof
          have "restrict \<theta> I \<in> PiE I (topspace \<circ> X) \<inter> \<Inter>\<T>"
            using \<T> by (fastforce simp: \<Phi>_def PiE_def dest: \<theta>)
          then show "restrict \<theta> I \<in> U"
            using subU by blast
        qed (rule \<open>U \<in> \<U>\<close>)
      next
        show "(\<lambda>i \<in> I. \<theta> i) \<in> Pi\<^sub>E I S"
          using \<theta> by simp
      qed
    qed
  qed
  show ?thesis
    apply (simp add: * closure_of_def PiE_iff set_eq_iff cong: conj_cong)
    by metis
qed

corollary closedin_product_topology:
   "closedin (product_topology X I) (PiE I S) \<longleftrightarrow> PiE I S = {} \<or> (\<forall>i \<in> I. closedin (X i) (S i))"
  by (smt (verit, best) PiE_eq closedin_empty closure_of_eq closure_of_product_topology)

corollary closedin_product_topology_singleton:
   "f \<in> extensional I \<Longrightarrow> closedin (product_topology X I) {f} \<longleftrightarrow> (\<forall>i \<in> I. closedin (X i) {f i})"
  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>

lemma continuous_map_product_coordinates [simp]:
  assumes "i \<in> I"
  shows "continuous_map (product_topology T I) (T i) (\<lambda>x. x i)"
proof -
  {
    fix U assume "openin (T i) U"
    define X where "X = (\<lambda>j. if j = i then U else topspace (T j))"
    then have *: "(\<lambda>x. x i) -` U \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (T i)) = (\<Pi>\<^sub>E j\<in>I. X j)"
      unfolding X_def using assms openin_subset[OF \<open>openin (T i) U\<close>]
      by (auto simp add: PiE_iff, auto, metis subsetCE)
    have **: "(\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}"
      unfolding X_def using \<open>openin (T i) U\<close> by auto
    have "openin (product_topology T I) ((\<lambda>x. x i) -` U \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (T i)))"
      unfolding product_topology_def
      apply (rule topology_generated_by_Basis)
      apply (subst *)
      using ** by auto
  }
  then show ?thesis unfolding continuous_map_alt
    by (auto simp add: assms PiE_iff)
qed

lemma continuous_map_coordinatewise_then_product [intro]:
  assumes "\<And>i. i \<in> I \<Longrightarrow> continuous_map T1 (T i) (\<lambda>x. f x i)"
          "\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
  shows "continuous_map T1 (product_topology T I) f"
unfolding product_topology_def
proof (rule continuous_on_generated_topo)
  fix U assume "U \<in> {Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
  then obtain X where H: "U = Pi\<^sub>E I X" "\<And>i. openin (T i) (X i)" "finite {i. X i \<noteq> topspace (T i)}"
    by blast
  define J where "J = {i \<in> I. X i \<noteq> topspace (T i)}"
  have "finite J" "J \<subseteq> I" unfolding J_def using H(3) by auto
  have "(\<lambda>x. f x i)-`(topspace(T i)) \<inter> topspace T1 = topspace T1" if "i \<in> I" for i
    using that assms(1) by (simp add: continuous_map_preimage_topspace)
  then have *: "(\<lambda>x. f x i)-`(X i) \<inter> topspace T1 = topspace T1" if "i \<in> I-J" for i
    using that unfolding J_def by auto
  have "f-`U \<inter> topspace T1 = (\<Inter>i\<in>I. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
    by (subst H(1), auto simp add: PiE_iff assms)
  also have "... = (\<Inter>i\<in>J. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
    using * \<open>J \<subseteq> I\<close> by auto
  also have "openin T1 (...)"
    using H(2) \<open>J \<subseteq> I\<close> \<open>finite J\<close> assms(1) by blast
  ultimately show "openin T1 (f-`U \<inter> topspace T1)" by simp
next
  have "f ` topspace T1 \<subseteq> topspace (product_topology T I)"
    using assms continuous_map_def by fastforce
  then show "f `topspace T1 \<subseteq> \<Union>{Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
    by (simp add: product_topology_def)
qed

lemma continuous_map_product_then_coordinatewise [intro]:
  assumes "continuous_map T1 (product_topology T I) f"
  shows "\<And>i. i \<in> I \<Longrightarrow> continuous_map T1 (T i) (\<lambda>x. f x i)"
        "\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
proof -
  fix i assume "i \<in> I"
  have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f" by auto
  also have "continuous_map T1 (T i) (...)"
    by (metis \<open>i \<in> I\<close> assms continuous_map_compose continuous_map_product_coordinates)
  ultimately show "continuous_map T1 (T i) (\<lambda>x. f x i)"
    by simp
next
  fix i x assume "i \<notin> I" "x \<in> topspace T1"
  have "f x \<in> topspace (product_topology T I)"
    using assms \<open>x \<in> topspace T1\<close> unfolding continuous_map_def by auto
  then have "f x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
    using topspace_product_topology by metis
  then show "f x i = undefined"
    using \<open>i \<notin> I\<close> by (auto simp add: PiE_iff extensional_def)
qed

lemma continuous_on_restrict:
  assumes "J \<subseteq> I"
  shows "continuous_map (product_topology T I) (product_topology T J) (\<lambda>x. restrict x J)"
proof (rule continuous_map_coordinatewise_then_product)
  fix i assume "i \<in> J"
  then have "(\<lambda>x. restrict x J i) = (\<lambda>x. x i)" unfolding restrict_def by auto
  then show "continuous_map (product_topology T I) (T i) (\<lambda>x. restrict x J i)"
    using \<open>i \<in> J\<close> \<open>J \<subseteq> I\<close> by auto
next
  fix i assume "i \<notin> J"
  then show "restrict x J i = undefined" for x::"'a \<Rightarrow> 'b"
    unfolding restrict_def by auto
qed


subsubsection\<^marker>\<open>tag important\<close> \<open>Powers of a single topological space as a topological space, using type classes\<close>

instantiation "fun" :: (type, topological_space) topological_space
begin

definition\<^marker>\<open>tag important\<close> open_fun_def:
  "open U = openin (product_topology (\<lambda>i. euclidean) UNIV) U"

instance proof
  have "topspace (product_topology (\<lambda>(i::'a). euclidean::('b topology)) UNIV) = UNIV"
    unfolding topspace_product_topology topspace_euclidean by auto
  then show "open (UNIV::('a \<Rightarrow> 'b) set)"
    unfolding open_fun_def by (metis openin_topspace)
qed (auto simp add: open_fun_def)

end

lemma open_PiE [intro?]:
  fixes X::"'i \<Rightarrow> ('b::topological_space) set"
  assumes "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
  shows "open (Pi\<^sub>E UNIV X)"
    by (simp add: assms open_fun_def product_topology_basis)

lemma euclidean_product_topology:
  "product_topology (\<lambda>i. euclidean::('b::topological_space) topology) UNIV = euclidean"
by (metis open_openin topology_eq open_fun_def)

proposition product_topology_basis':
  fixes x::"'i \<Rightarrow> 'a" and U::"'i \<Rightarrow> ('b::topological_space) set"
  assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
  shows "open {f. \<forall>i\<in>I. f (x i) \<in> U i}"
proof -
  define V where "V \<equiv> (\<lambda>y. if y \<in> x`I then \<Inter>{U i|i. i\<in>I \<and> x i = y} else UNIV)"
  define X where "X \<equiv> (\<lambda>y. if y \<in> x`I then V y else UNIV)"
  have *: "open (X i)" for i
    unfolding X_def V_def using assms by auto
  then have "open (Pi\<^sub>E UNIV X)"
    by (simp add: X_def assms(1) open_PiE)
  moreover have "Pi\<^sub>E UNIV X = {f. \<forall>i\<in>I. f (x i) \<in> U i}"
    by (fastforce simp add: PiE_iff X_def V_def split: if_split_asm)
  ultimately show ?thesis by simp
qed

text \<open>The results proved in the general situation of products of possibly different
spaces have their counterparts in this simpler setting.\<close>

lemma continuous_on_product_coordinates [simp]:
  "continuous_on UNIV (\<lambda>x. x i::('b::topological_space))"
  using continuous_map_product_coordinates [of _ UNIV "\<lambda>i. euclidean"]
    by (metis (no_types) continuous_map_iff_continuous euclidean_product_topology iso_tuple_UNIV_I subtopology_UNIV)

lemma continuous_on_coordinatewise_then_product [continuous_intros]:
  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"
  by (metis UNIV_I assms continuous_map_iff_continuous euclidean_product_topology
      continuous_map_coordinatewise_then_product)

lemma continuous_on_product_then_coordinatewise:
  assumes "continuous_on S f"
  shows "continuous_on S (\<lambda>x. f x i)"
  by (metis UNIV_I assms continuous_map_iff_continuous continuous_map_product_then_coordinatewise(1) euclidean_product_topology)

lemma continuous_on_coordinatewise_iff:
  fixes f :: "('a \<Rightarrow> real) \<Rightarrow> 'b \<Rightarrow> real"
  shows "continuous_on (A \<inter> S) f \<longleftrightarrow> (\<forall>i. continuous_on (A \<inter> S) (\<lambda>x. f x i))"
  by (auto simp: continuous_on_product_then_coordinatewise continuous_on_coordinatewise_then_product)

lemma continuous_map_span_sum:
  fixes B :: "'a::real_normed_vector set"
  assumes biB: "\<And>i. i \<in> I \<Longrightarrow> b i \<in> B"
  shows "continuous_map euclidean (top_of_set (span B)) (\<lambda>x. \<Sum>i\<in>I. x i *\<^sub>R b i)"
proof (rule continuous_map_euclidean_top_of_set)
  show "(\<lambda>x. \<Sum>i\<in>I. x i *\<^sub>R b i) -` span B = UNIV"
    by auto (meson biB lessThan_iff span_base span_scale span_sum)
  show "continuous_on UNIV (\<lambda>x. \<Sum>i\<in> I. x i *\<^sub>R b i)"
    by (intro continuous_intros) auto
qed

subsubsection\<^marker>\<open>tag important\<close> \<open>Topological countability for product spaces\<close>

text \<open>The next two lemmas are useful to prove first or second countability
of product spaces, but they have more to do with countability and could
be put in the corresponding theory.\<close>

lemma countable_nat_product_event_const:
  fixes F::"'a set" and a::'a
  assumes "a \<in> F" "countable F"
  shows "countable {x::(nat \<Rightarrow> 'a). (\<forall>i. x i \<in> F) \<and> finite {i. x i \<noteq> a}}"
proof -
  have *: "{x::(nat \<Rightarrow> 'a). (\<forall>i. x i \<in> F) \<and> finite {i. x i \<noteq> a}}
                  \<subseteq> (\<Union>N. {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)})"
    using infinite_nat_iff_unbounded_le by fastforce
  have "countable {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)}" for N::nat
  proof (induction N)
    case 0
    have "{x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>(0::nat). x i = a)} = {(\<lambda>i. a)}"
      using \<open>a \<in> F\<close> by auto
    then show ?case by auto
  next
    case (Suc N)
    define f::"((nat \<Rightarrow> 'a) \<times> 'a) \<Rightarrow> (nat \<Rightarrow> 'a)"
      where "f = (\<lambda>(x, b). x(N:=b))"
    have "{x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>Suc N. x i = a)} \<subseteq> f`({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
    proof (auto)
      fix x assume H: "\<forall>i::nat. x i \<in> F" "\<forall>i\<ge>Suc N. x i = a"
      have "f (x(N:=a), x N) = x"
        unfolding f_def by auto
      moreover have "(x(N:=a), x N) \<in> {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F"
        using H \<open>a \<in> F\<close> by auto
      ultimately show "x \<in> f ` ({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
        by (metis (no_types, lifting) image_eqI)
    qed
    moreover have "countable ({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
      using Suc.IH assms(2) by auto
    ultimately show ?case
      by (meson countable_image countable_subset)
  qed
  then show ?thesis using countable_subset[OF *] by auto
qed

lemma countable_product_event_const:
  fixes F::"('a::countable) \<Rightarrow> 'b set" and b::'b
  assumes "\<And>i. countable (F i)"
  shows "countable {f::('a \<Rightarrow> 'b). (\<forall>i. f i \<in> F i) \<and> (finite {i. f i \<noteq> b})}"
proof -
  define G where "G = (\<Union>i. F i) \<union> {b}"
  have "countable G" unfolding G_def using assms by auto
  have "b \<in> G" unfolding G_def by auto
  define pi where "pi = (\<lambda>(x::(nat \<Rightarrow> 'b)). (\<lambda> i::'a. x ((to_nat::('a \<Rightarrow> nat)) i)))"
  have "{f::('a \<Rightarrow> 'b). (\<forall>i. f i \<in> F i) \<and> (finite {i. f i \<noteq> b})}
        \<subseteq> pi`{g::(nat \<Rightarrow> 'b). (\<forall>j. g j \<in> G) \<and> (finite {j. g j \<noteq> b})}"
  proof (auto)
    fix f assume H: "\<forall>i. f i \<in> F i" "finite {i. f i \<noteq> b}"
    define I where "I = {i. f i \<noteq> b}"
    define g where "g = (\<lambda>j. if j \<in> to_nat`I then f (from_nat j) else b)"
    have "{j. g j \<noteq> b} \<subseteq> to_nat`I" unfolding g_def by auto
    then have "finite {j. g j \<noteq> b}"
      unfolding I_def using H(2) using finite_surj by blast
    moreover have "g j \<in> G" for j
      unfolding g_def G_def using H by auto
    ultimately have "g \<in> {g::(nat \<Rightarrow> 'b). (\<forall>j. g j \<in> G) \<and> (finite {j. g j \<noteq> b})}"
      by auto
    moreover have "f = pi g"
      unfolding pi_def g_def I_def using H by fastforce
    ultimately show "f \<in> pi`{g. (\<forall>j. g j \<in> G) \<and> finite {j. g j \<noteq> b}}"
      by auto
  qed
  then show ?thesis
    using countable_nat_product_event_const[OF \<open>b \<in> G\<close> \<open>countable G\<close>]
    by (meson countable_image countable_subset)
qed

instance "fun" :: (countable, first_countable_topology) first_countable_topology
proof
  fix x::"'a \<Rightarrow> 'b"
  have "\<exists>A::('b \<Rightarrow> nat \<Rightarrow> 'b set). \<forall>x. (\<forall>i. x \<in> A x i \<and> open (A x i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A x i \<subseteq> S))"
    apply (rule choice) using first_countable_basis by auto
  then obtain A::"('b \<Rightarrow> nat \<Rightarrow> 'b set)" where A: "\<And>x i. x \<in> A x i"
                                                  "\<And>x i. open (A x i)"
                                                  "\<And>x S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>i. A x i \<subseteq> S)"
    by metis
  text \<open>\<open>B i\<close> is a countable basis of neighborhoods of \<open>x\<^sub>i\<close>.\<close>
  define B where "B = (\<lambda>i. (A (x i))`UNIV \<union> {UNIV})"
  have countB: "countable (B i)" for i unfolding B_def by auto
  have open_B: "\<And>X i. X \<in> B i \<Longrightarrow> open X"
    by (auto simp: B_def A)
  define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
  have "Pi\<^sub>E UNIV (\<lambda>i. UNIV) \<in> K"
    unfolding K_def B_def by auto
  then have "K \<noteq> {}" by auto
  have "countable {X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
    by (simp add: countB countable_product_event_const)
  moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X)`{X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
    unfolding K_def by auto
  ultimately have "countable K" by auto
  have I: "x \<in> k" if "k \<in> K" for k
    using that unfolding K_def B_def apply auto using A(1) by auto
  have II: "open k" if "k \<in> K" for k
    using that unfolding K_def by (blast intro: open_B open_PiE)
  have Inc: "\<exists>k\<in>K. k \<subseteq> U" if "open U \<and> x \<in> U" for U
  proof -
    have "openin (product_topology (\<lambda>i. euclidean) UNIV) U" "x \<in> U"
      using \<open>open U \<and> x \<in> U\<close> unfolding open_fun_def by auto
    with product_topology_open_contains_basis[OF this]
    have "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV} \<and> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
      by simp
    then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
                           "\<And>i. open (X i)"
                           "finite {i. X i \<noteq> UNIV}"
                           "(\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
      by auto
    define I where "I = {i. X i \<noteq> UNIV}"
    define Y where "Y = (\<lambda>i. if i \<in> I then (SOME y. y \<in> B i \<and> y \<subseteq> X i) else UNIV)"
    have *: "\<exists>y. y \<in> B i \<and> y \<subseteq> X i" for i
      unfolding B_def using A(3)[OF H(2)] H(1) by (metis PiE_E UNIV_I UnCI image_iff)
    have **: "Y i \<in> B i \<and> Y i \<subseteq> X i" for i
    proof (cases "i \<in> I")
      case True
      then show ?thesis  
        by (metis (mono_tags, lifting) "*" Nitpick.Eps_psimp Y_def)
    next
      case False
      then show ?thesis by (simp add: B_def I_def Y_def)
    qed
    have "{i. Y i \<noteq> UNIV} \<subseteq> I"
      unfolding Y_def by auto
    with ** have "(\<forall>i. Y i \<in> B i) \<and> finite {i. Y i \<noteq> UNIV}"
      using H(3) I_def finite_subset by blast
    then have "Pi\<^sub>E UNIV Y \<in> K"
      unfolding K_def by auto
    have "Y i \<subseteq> X i" for i
      using "**" by auto
    then have "Pi\<^sub>E UNIV Y \<subseteq> U"
      by (metis H(4) PiE_mono subset_trans)
    then show ?thesis using \<open>Pi\<^sub>E UNIV Y \<in> K\<close> by auto
  qed
  show "\<exists>L. (\<forall>(i::nat). x \<in> L i \<and> open (L i)) \<and> (\<forall>U. open U \<and> x \<in> U \<longrightarrow> (\<exists>i. L i \<subseteq> U))"
    using \<open>countable K\<close> I II Inc by (simp add: first_countableI) 
qed

proposition product_topology_countable_basis:
  shows "\<exists>K::(('a::countable \<Rightarrow> 'b::second_countable_topology) set set).
          topological_basis K \<and> countable K \<and>
          (\<forall>k\<in>K. \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV})"
proof -
  obtain B::"'b set set" where B: "countable B \<and> topological_basis B"
    using ex_countable_basis by auto
  then have "B \<noteq> {}" by (meson UNIV_I empty_iff open_UNIV topological_basisE)
  define B2 where "B2 = B \<union> {UNIV}"
  have "countable B2"
    unfolding B2_def using B by auto
  have "open U" if "U \<in> B2" for U
    using that unfolding B2_def using B topological_basis_open by auto

  define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i::'a. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
  have i: "\<forall>k\<in>K. \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
    unfolding K_def using \<open>\<And>U. U \<in> B2 \<Longrightarrow> open U\<close> by auto

  have "countable {X. (\<forall>(i::'a). X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
    using \<open>countable B2\<close>  by (intro countable_product_event_const) auto
  moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X)`{X. (\<forall>i. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
    unfolding K_def by auto
  ultimately have ii: "countable K" by auto

  have iii: "topological_basis K"
  proof (rule topological_basisI)
    fix U and x::"'a\<Rightarrow>'b" assume "open U" "x \<in> U"
    then have "openin (product_topology (\<lambda>i. euclidean) UNIV) U"
      unfolding open_fun_def by auto
    with product_topology_open_contains_basis[OF this \<open>x \<in> U\<close>]
    obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
                           "\<And>i. open (X i)"
                           "finite {i. X i \<noteq> UNIV}"
                           "(\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
      by auto
    then have "x i \<in> X i" for i by auto
    define I where "I = {i. X i \<noteq> UNIV}"
    define Y where "Y = (\<lambda>i. if i \<in> I then (SOME y. y \<in> B2 \<and> y \<subseteq> X i \<and> x i \<in> y) else UNIV)"
    have *: "\<exists>y. y \<in> B2 \<and> y \<subseteq> X i \<and> x i \<in> y" for i
      unfolding B2_def using B \<open>open (X i)\<close> \<open>x i \<in> X i\<close> by (meson UnCI topological_basisE)
    have **: "Y i \<in> B2 \<and> Y i \<subseteq> X i \<and> x i \<in> Y i" for i
      using someI_ex[OF *] by (simp add: B2_def I_def Y_def)
    have "{i. Y i \<noteq> UNIV} \<subseteq> I"
      unfolding Y_def by auto
    then have "(\<forall>i. Y i \<in> B2) \<and> finite {i. Y i \<noteq> UNIV}"
      using "**" H(3) I_def finite_subset by blast
    then have "Pi\<^sub>E UNIV Y \<in> K"
      unfolding K_def by auto
    then show "\<exists>V\<in>K. x \<in> V \<and> V \<subseteq> U"
      by (meson "**" H(4) PiE_I PiE_mono UNIV_I order.trans)
  next
    fix U assume "U \<in> K"
    show "open U"
      using \<open>U \<in> K\<close> unfolding open_fun_def K_def  by clarify (metis \<open>U \<in> K\<close> i open_PiE open_fun_def)
  qed

  show ?thesis using i ii iii by auto
qed

instance "fun" :: (countable, second_countable_topology) second_countable_topology
proof
  show "\<exists>B::('a \<Rightarrow> 'b) set set. countable B \<and> open = generate_topology B"
    using product_topology_countable_basis topological_basis_imp_subbasis 
    by auto
qed

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>' ex_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
qed (auto simp: continuous_map_def PiE_def)


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

declare continuous_map_from_subtopology [OF continuous_map_product_projection, continuous_intros]

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\<in>I. f j)(i:=a) \<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. (\<lambda>j\<in>I. f j)(i:=x))"
            by (auto simp: continuous_map_componentwise assms extensional_def restrict_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)
                using subsetD [OF \<F>]
                by (metis (mono_tags, lifting) finite_intersection_of_inc mem_Collect_eq topspace_product_topology)
            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\<in>I. f j)(i:=f i) = 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

subsection \<open>Open Pi-sets in the product topology\<close>

proposition openin_PiE_gen:
  "openin (product_topology X I) (PiE I S) \<longleftrightarrow>
        PiE I S = {} \<or>
        finite {i \<in> I. ~(S i = topspace(X i))} \<and> (\<forall>i \<in> I. openin (X i) (S i))"
  (is "?lhs \<longleftrightarrow> _ \<or> ?rhs")
proof (cases "PiE I S = {}")
  case False
  moreover have "?lhs = ?rhs"
  proof
    assume L: ?lhs
    moreover
    obtain z where z: "z \<in> PiE I S"
      using False by blast
    ultimately obtain U where fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}"
      and "Pi\<^sub>E I U \<noteq> {}"
      and sub: "Pi\<^sub>E I U \<subseteq> Pi\<^sub>E I S"
      by (fastforce simp add: openin_product_topology_alt)
    then have *: "\<And>i. i \<in> I \<Longrightarrow> U i \<subseteq> S i"
      by (simp add: subset_PiE)
    show ?rhs
    proof (intro conjI ballI)
      show "finite {i \<in> I. S i \<noteq> topspace (X i)}"
        apply (rule finite_subset [OF _ fin], clarify)
        using *
        by (metis False L openin_subset topspace_product_topology subset_PiE subset_antisym)
    next
      fix i :: "'a"
      assume "i \<in> I"
      then show "openin (X i) (S i)"
        using open_map_product_projection [of i I X] L
        apply (simp add: open_map_def)
        apply (drule_tac x="PiE I S" in spec)
        apply (simp add: False image_projection_PiE split: if_split_asm)
        done
    qed
  next
    assume ?rhs
    then show ?lhs
      unfolding openin_product_topology
      by (intro arbitrary_union_of_inc) (auto simp: product_topology_base_alt)
  qed
  ultimately show ?thesis
    by simp
qed simp


corollary openin_PiE:
   "finite I \<Longrightarrow> openin (product_topology X I) (PiE I S) \<longleftrightarrow> PiE I S = {} \<or> (\<forall>i \<in> I. openin (X i) (S i))"
  by (simp add: openin_PiE_gen)

proposition compact_space_product_topology:
   "compact_space(product_topology X I) \<longleftrightarrow>
    topspace(product_topology X I) = {} \<or> (\<forall>i \<in> I. compact_space(X i))"
    (is "?lhs = ?rhs")
proof (cases "topspace(product_topology X I) = {}")
  case False
  then obtain z where z: "z \<in> (\<Pi>\<^sub>E i\<in>I. topspace(X i))"
    by auto
  show ?thesis
  proof
    assume L: ?lhs
    show ?rhs
    proof (clarsimp simp add: False compact_space_def)
      fix i
      assume "i \<in> I"
      with L have "continuous_map (product_topology X I) (X i) (\<lambda>f. f i)"
        by (simp add: continuous_map_product_projection)
      moreover
      have "\<And>x. x \<in> topspace (X i) \<Longrightarrow> x \<in> (\<lambda>f. f i) ` (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
        using \<open>i \<in> I\<close> z by (rule_tac x="z(i:=x)" in image_eqI) auto
      then have "(\<lambda>f. f i) ` (\<Pi>\<^sub>E i\<in>I. topspace (X i)) = topspace (X i)"
        using \<open>i \<in> I\<close> z by auto
      ultimately show "compactin (X i) (topspace (X i))"
        by (metis L compact_space_def image_compactin topspace_product_topology)
    qed
  next
    assume R: ?rhs
    show ?lhs
    proof (cases "I = {}")
      case True
      with R show ?thesis
        by (simp add: compact_space_def)
    next
      case False
      then obtain i where "i \<in> I"
        by blast
      show ?thesis
        using R
      proof
        assume com [rule_format]: "\<forall>i\<in>I. compact_space (X i)"
        let ?\<C> = "{{f. f i \<in> U} |i U. i \<in> I \<and> openin (X i) U}"
        show "compact_space (product_topology X I)"
        proof (rule Alexander_subbase_alt)
          show "topspace (product_topology X I) \<subseteq> \<Union>?\<C>"
            unfolding topspace_product_topology using \<open>i \<in> I\<close> by blast
        next
          fix C
          assume Csub: "C \<subseteq> ?\<C>" and UC: "topspace (product_topology X I) \<subseteq> \<Union>C"
          define \<D> where "\<D> \<equiv> \<lambda>i. {U. openin (X i) U \<and> {f. f i \<in> U} \<in> C}"
          show "\<exists>C'. finite C' \<and> C' \<subseteq> C \<and> topspace (product_topology X I) \<subseteq> \<Union>C'"
          proof (cases "\<exists>i. i \<in> I \<and> topspace (X i) \<subseteq> \<Union>(\<D> i)")
            case True
            then obtain i where "i \<in> I"
                   and i: "topspace (X i) \<subseteq> \<Union>(\<D> i)"
              unfolding \<D>_def by blast
            then have *: "\<And>\<U>. \<lbrakk>Ball \<U> (openin (X i)); topspace (X i) \<subseteq> \<Union>\<U>\<rbrakk> \<Longrightarrow>
                            \<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> topspace (X i) \<subseteq> \<Union>\<F>"
              using com [OF \<open>i \<in> I\<close>] by (auto simp: compact_space_def compactin_def)
            have "topspace (X i) \<subseteq> \<Union>(\<D> i)"
              using i by auto
            with * obtain \<F> where "finite \<F> \<and> \<F> \<subseteq> (\<D> i) \<and> topspace (X i) \<subseteq> \<Union>\<F>"
              unfolding \<D>_def by fastforce
            with \<open>i \<in> I\<close> show ?thesis
              unfolding \<D>_def
              by (rule_tac x="(\<lambda>U. {x. x i \<in> U}) ` \<F>" in exI) auto
          next
            case False
            then have "\<forall>i \<in> I. \<exists>y. y \<in> topspace (X i) \<and> y \<notin> \<Union>(\<D> i)"
              by force
            then obtain g where g: "\<And>i. i \<in> I \<Longrightarrow> g i \<in> topspace (X i) \<and> g i \<notin> \<Union>(\<D> i)"
              by metis
            then have "(\<lambda>i. if i \<in> I then g i else undefined) \<in> topspace (product_topology X I)"
              by (simp add: PiE_I)
            moreover have "(\<lambda>i. if i \<in> I then g i else undefined) \<notin> \<Union>C"
              using Csub g unfolding \<D>_def by force
            ultimately show ?thesis
              using UC by blast
          qed
        qed (simp add: product_topology)
      qed (simp add: compact_space_topspace_empty)
    qed
  qed
qed (simp add: compact_space_topspace_empty)

corollary compactin_PiE:
   "compactin (product_topology X I) (PiE I S) \<longleftrightarrow>
        PiE I S = {} \<or> (\<forall>i \<in> I. compactin (X i) (S i))"
  by (auto simp: compactin_subspace subtopology_PiE subset_PiE compact_space_product_topology
       PiE_eq_empty_iff)

lemma in_product_topology_closure_of:
   "z \<in> (product_topology X I) closure_of S
        \<Longrightarrow> i \<in> I \<Longrightarrow> z i \<in> ((X i) closure_of ((\<lambda>x. x i) ` S))"
  using continuous_map_product_projection
  by (force simp: continuous_map_eq_image_closure_subset image_subset_iff)

lemma homeomorphic_space_singleton_product:
   "product_topology X {k} homeomorphic_space (X k)"
  unfolding homeomorphic_space
  apply (rule_tac x="\<lambda>x. x k" in exI)
  apply (rule bijective_open_imp_homeomorphic_map)
     apply (simp_all add: continuous_map_product_projection open_map_product_projection)
  unfolding PiE_over_singleton_iff
   apply (auto simp: image_iff inj_on_def)
  done

subsection\<open>Relationship with connected spaces, paths, etc.\<close>

proposition connected_space_product_topology:
   "connected_space(product_topology X I) \<longleftrightarrow>
    (\<Pi>\<^sub>E i\<in>I. topspace (X i)) = {} \<or> (\<forall>i \<in> I. connected_space(X i))"
  (is "?lhs \<longleftrightarrow> ?eq \<or> ?rhs")
proof (cases ?eq)
  case False
  moreover have "?lhs = ?rhs"
  proof
    assume ?lhs
    moreover
    have "connectedin(X i) (topspace(X i))"
      if "i \<in> I" and ci: "connectedin(product_topology X I) (topspace(product_topology X I))" for i
    proof -
      have cm: "continuous_map (product_topology X I) (X i) (\<lambda>f. f i)"
        by (simp add: \<open>i \<in> I\<close> continuous_map_product_projection)
      show ?thesis
        using connectedin_continuous_map_image [OF cm ci] \<open>i \<in> I\<close>
        by (simp add: False image_projection_PiE)
    qed
    ultimately show ?rhs
      by (meson connectedin_topspace)
  next
    assume cs [rule_format]: ?rhs
    have False
      if disj: "U \<inter> V = {}" and subUV: "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<subseteq> U \<union> V"
        and U: "openin (product_topology X I) U"
        and V: "openin (product_topology X I) V"
        and "U \<noteq> {}" "V \<noteq> {}"
      for U V
    proof -
      obtain f where "f \<in> U"
        using \<open>U \<noteq> {}\<close> by blast
      then have f: "f \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
        using U openin_subset by fastforce
      have "U \<subseteq> topspace(product_topology X I)" "V \<subseteq> topspace(product_topology X I)"
        using U V openin_subset by blast+
      moreover have "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<subseteq> U"
      proof -
        obtain C where "(finite intersection_of (\<lambda>F. \<exists>i U. F = {x. x i \<in> U} \<and> i \<in> I \<and> openin (X i) U) relative_to
            (\<Pi>\<^sub>E i\<in>I. topspace (X i))) C" "C \<subseteq> U" "f \<in> C"
          using U \<open>f \<in> U\<close> unfolding openin_product_topology union_of_def by auto
        then obtain \<T> where "finite \<T>"
          and t: "\<And>C. C \<in> \<T> \<Longrightarrow> \<exists>i u. (i \<in> I \<and> openin (X i) u) \<and> C = {x. x i \<in> u}"
          and subU: "topspace (product_topology X I) \<inter> \<Inter>\<T> \<subseteq> U"
          and ftop: "f \<in> topspace (product_topology X I)"
          and fint: "f \<in> \<Inter> \<T>"
          by (fastforce simp: relative_to_def intersection_of_def subset_iff)
        let ?L = "\<Union>C\<in>\<T>. {i. (\<lambda>x. x i) ` C \<subset> topspace (X i)}"
        obtain L where "finite L"
          and L: "\<And>i U. \<lbrakk>i \<in> I; openin (X i) U; U \<subset> topspace(X i); {x. x i \<in> U} \<in> \<T>\<rbrakk> \<Longrightarrow> i \<in> L"
        proof
          show "finite ?L"
          proof (rule finite_Union)
            fix M
            assume "M \<in> (\<lambda>C. {i. (\<lambda>x. x i) ` C \<subset> topspace (X i)}) ` \<T>"
            then obtain C where "C \<in> \<T>" and C: "M = {i. (\<lambda>x. x i) ` C \<subset> topspace (X i)}"
              by blast
            then obtain j V where "j \<in> I" and ope: "openin (X j) V" and Ceq: "C = {x. x j \<in> V}"
              using t by meson
            then have "f j \<in> V"
              using \<open>C \<in> \<T>\<close> fint by force
            then have "(\<lambda>x. x k) ` {x. x j \<in> V} = UNIV" if "k \<noteq> j" for k
              using that
              apply (clarsimp simp add: set_eq_iff)
              apply (rule_tac x="f(k:=x)" in image_eqI, auto)
              done
            then have "{i. (\<lambda>x. x i) ` C \<subset> topspace (X i)} \<subseteq> {j}"
              using Ceq by auto
            then show "finite M"
              using C finite_subset by fastforce
          qed (use \<open>finite \<T>\<close> in blast)
        next
          fix i U
          assume  "i \<in> I" and ope: "openin (X i) U" and psub: "U \<subset> topspace (X i)" and int: "{x. x i \<in> U} \<in> \<T>"
          then show "i \<in> ?L"
            by (rule_tac a="{x. x i \<in> U}" in UN_I) (force+)
        qed
        show ?thesis
        proof
          fix h
          assume h: "h \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
          define g where "g \<equiv> \<lambda>i. if i \<in> L then f i else h i"
          have gin: "g \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
            unfolding g_def using f h by auto
          moreover have "g \<in> X" if "X \<in> \<T>" for X
            using fint openin_subset t [OF that] L g_def h that by fastforce
          ultimately have "g \<in> U"
            using subU by auto
          have "h \<in> U" if "finite M" "h \<in> PiE I (topspace \<circ> X)" "{i \<in> I. h i \<noteq> g i} \<subseteq> M" for M h
            using that
          proof (induction arbitrary: h)
            case empty
            then show ?case
              using PiE_ext \<open>g \<in> U\<close> gin by force
          next
            case (insert i M)
            define f where "f \<equiv> h(i:=g i)"
            have fin: "f \<in> PiE I (topspace \<circ> X)"
              unfolding f_def using gin insert.prems(1) by auto
            have subM: "{j \<in> I. f j \<noteq> g j} \<subseteq> M"
              unfolding f_def using insert.prems(2) by auto
            have "f \<in> U"
              using insert.IH [OF fin subM] .
            show ?case
            proof (cases "h \<in> V")
              case True
              show ?thesis
              proof (cases "i \<in> I")
                case True
                let ?U = "{x \<in> topspace(X i). h(i:=x) \<in> U}"
                let ?V = "{x \<in> topspace(X i). h(i:=x) \<in> V}"
                have False
                proof (rule connected_spaceD [OF cs [OF \<open>i \<in> I\<close>]])
                  have "\<And>k. k \<in> I \<Longrightarrow> continuous_map (X i) (X k) (\<lambda>x. if k = i then x else h k)"
                    using continuous_map_eq_topcontinuous_at insert.prems(1) topcontinuous_at_def by fastforce
                  then have cm: "continuous_map (X i) (product_topology X I) (\<lambda>x. h(i:=x))"
                    using \<open>i \<in> I\<close> insert.prems(1)
                    by (auto simp: continuous_map_componentwise extensional_def)
                  show "openin (X i) ?U"
                    by (rule openin_continuous_map_preimage [OF cm U])
                  show "openin (X i) ?V"
                    by (rule openin_continuous_map_preimage [OF cm V])
                  show "topspace (X i) \<subseteq> ?U \<union> ?V"
                  proof clarsimp
                    fix x
                    assume "x \<in> topspace (X i)" and "h(i:=x) \<notin> V"
                    with True subUV \<open>h \<in> Pi\<^sub>E I (topspace \<circ> X)\<close>
                    show "h(i:=x) \<in> U"
                      by (force dest: subsetD [where c="h(i:=x)"])
                  qed
                  show "?U \<inter> ?V = {}"
                    using disj by blast
                  show "?U \<noteq> {}"
                    using True \<open>f \<in> U\<close> f_def gin by auto
                  show "?V \<noteq> {}"
                    using True \<open>h \<in> V\<close> V openin_subset by fastforce
                qed
                then show ?thesis ..
              next
                case False
                show ?thesis
                  using insert.prems(1) by (metis False gin PiE_E \<open>f \<in> U\<close> f_def fun_upd_triv)
              qed
            next
              case False
              then show ?thesis
                using subUV insert.prems(1) by auto
            qed
          qed
          then show "h \<in> U"
            unfolding g_def using PiE_iff \<open>finite L\<close> h by fastforce
        qed
      qed
      ultimately show ?thesis
        using disj inf_absorb2 \<open>V \<noteq> {}\<close> by fastforce
    qed
    then show ?lhs
      unfolding connected_space_def
      by auto
  qed
  ultimately show ?thesis
    by simp
qed (simp add: connected_space_topspace_empty)


lemma connectedin_PiE:
   "connectedin (product_topology X I) (PiE I S) \<longleftrightarrow>
        PiE I S = {} \<or> (\<forall>i \<in> I. connectedin (X i) (S i))"
  by (fastforce simp add: connectedin_def subtopology_PiE connected_space_product_topology subset_PiE PiE_eq_empty_iff)

lemma path_connected_space_product_topology:
   "path_connected_space(product_topology X I) \<longleftrightarrow>
    topspace(product_topology X I) = {} \<or> (\<forall>i \<in> I. path_connected_space(X i))"
 (is "?lhs \<longleftrightarrow> ?eq \<or> ?rhs")
proof (cases ?eq)
  case False
  moreover have "?lhs = ?rhs"
  proof
    assume L: ?lhs
    show ?rhs
    proof (clarsimp simp flip: path_connectedin_topspace)
      fix i :: "'a"
      assume "i \<in> I"
      have cm: "continuous_map (product_topology X I) (X i) (\<lambda>f. f i)"
        by (simp add: \<open>i \<in> I\<close> continuous_map_product_projection)
      show "path_connectedin (X i) (topspace (X i))"
        using path_connectedin_continuous_map_image [OF cm L [unfolded path_connectedin_topspace [symmetric]]]
        by (metis \<open>i \<in> I\<close> False retraction_imp_surjective_map retraction_map_product_projection)
    qed
  next
    assume R [rule_format]: ?rhs
    show ?lhs
      unfolding path_connected_space_def topspace_product_topology
    proof clarify
      fix x y
      assume x: "x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))" and y: "y \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
      have "\<forall>i. \<exists>g. i \<in> I \<longrightarrow> pathin (X i) g \<and> g 0 = x i \<and> g 1 = y i"
        using PiE_mem R path_connected_space_def x y by force
      then obtain g where g: "\<And>i. i \<in> I \<Longrightarrow> pathin (X i) (g i) \<and> g i 0 = x i \<and> g i 1 = y i"
        by metis
      with x y show "\<exists>g. pathin (product_topology X I) g \<and> g 0 = x \<and> g 1 = y"
        apply (rule_tac x="\<lambda>a. \<lambda>i \<in> I. g i a" in exI)
        apply (force simp: pathin_def continuous_map_componentwise)
        done
    qed
  qed
  ultimately show ?thesis
    by simp
qed (simp add: path_connected_space_topspace_empty)

lemma path_connectedin_PiE:
   "path_connectedin (product_topology X I) (PiE I S) \<longleftrightarrow>
    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) = {})"
  by (metis assms image_empty quotient_imp_surjective_map retraction_imp_quotient_map 
      retraction_map_product_projection)

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"
      using f 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})"]
      by (force simp add: subtopology_PiE)
    then show ?thesis
      using minor [OF f major \<open>i \<in> I\<close>] PQ by auto
  qed
  then show ?thesis by metis
qed

end