Theory Topology_ZF_10

theory Topology_ZF_10
imports Topology_ZF_7
(* 
    This file is a part of IsarMathLib - 
    a library of formalized mathematics written for Isabelle/Isar.

    Copyright (C) 2013 Daniel de la Concepcion

    This program is free software; Redistribution and use in source and binary forms, 
    with or without modification, are permitted provided that the following conditions are met:

   1. Redistributions of source code must retain the above copyright notice, 
   this list of conditions and the following disclaimer.
   2. Redistributions in binary form must reproduce the above copyright notice, 
   this list of conditions and the following disclaimer in the documentation and/or 
   other materials provided with the distribution.
   3. The name of the author may not be used to endorse or promote products 
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED 
WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF 
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. 
IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, 
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; 
OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, 
WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR 
OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, 
EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *)

section ‹Topology 10›

theory Topology_ZF_10
imports Topology_ZF_7
begin

text‹This file deals with properties of product spaces. We only consider
product of two spaces, and most of this proofs, can be used to prove
the results in product of a finite number of spaces.›

subsection‹Closure and closed sets in product space›

text‹The closure of a product, is the product of the closures.›

lemma cl_product:
  assumes "T{is a topology}" "S{is a topology}" "A⊆⋃T" "B⊆⋃S"
  shows "Closure(A×B,ProductTopology(T,S))=Closure(A,T)×Closure(B,S)"
proof
  have "A×B⊆⋃T×⋃S" using assms(3,4) by auto
  then have sub:"A×B⊆⋃ProductTopology(T,S)" using Top_1_4_T1(3) assms(1,2) by auto
  have top:"ProductTopology(T,S){is a topology}" using Top_1_4_T1(1) assms(1,2) by auto
  {
    fix x assume asx:"x∈Closure(A×B,ProductTopology(T,S))"
    then have reg:"∀U∈ProductTopology(T,S). x∈U ⟶ U∩(A×B)≠0" using topology0.cl_inter_neigh
      sub top unfolding topology0_def by blast
    from asx have "x∈⋃ProductTopology(T,S)" using topology0.Top_3_L11(1) top unfolding topology0_def
      using sub by blast
    then have xSigma:"x∈⋃T×⋃S" using Top_1_4_T1(3) assms(1,2) by auto
    then have "⟨fst(x),snd(x)⟩∈⋃T×⋃S" using Pair_fst_snd_eq by auto
    then have xT:"fst(x)∈⋃T" and xS:"snd(x)∈⋃S" by auto
    {
      fix U V assume as:"U∈T"  "fst(x)∈U"
      have "⋃S∈S" using assms(2) unfolding IsATopology_def by auto
      with as have "U×(⋃S)∈ProductCollection(T,S)" unfolding ProductCollection_def
        by auto
      then have P:"U×(⋃S)∈ProductTopology(T,S)" using Top_1_4_T1(2) assms(1,2) base_sets_open by blast
      with xS as(2) have "⟨fst(x),snd(x)⟩∈U×(⋃S)" by auto
      then have "x∈U×(⋃S)" using Pair_fst_snd_eq xSigma by auto
      with P reg have "U×(⋃S)∩A×B≠0" by auto
      then have noEm:"U∩A≠0" by auto
    }
    then have "∀U∈T. fst(x)∈U ⟶ U∩A≠0" by auto moreover
    {
      fix U V assume as:"U∈S"  "snd(x)∈U"
      have "⋃T∈T" using assms(1) unfolding IsATopology_def by auto
      with as have "(⋃T)×U∈ProductCollection(T,S)" unfolding ProductCollection_def
        by auto
      then have P:"(⋃T)×U∈ProductTopology(T,S)" using Top_1_4_T1(2) assms(1,2) base_sets_open by blast
      with xT as(2) have "⟨fst(x),snd(x)⟩∈(⋃T)×U" by auto
      then have "x∈(⋃T)×U" using Pair_fst_snd_eq xSigma by auto
      with P reg have "(⋃T)×U∩A×B≠0" by auto
      then have noEm:"U∩B≠0" by auto
    }
    then have "∀U∈S. snd(x)∈U ⟶ U∩B≠0" by auto
    ultimately have "fst(x)∈Closure(A,T)" "snd(x)∈Closure(B,S)" using 
      topology0.inter_neigh_cl assms(3,4) unfolding topology0_def
      using assms(1,2) xT xS by auto
    then have "⟨fst(x),snd(x)⟩∈Closure(A,T)×Closure(B,S)" by auto
    with xSigma have "x∈Closure(A,T)×Closure(B,S)" by auto
  }
  then show "Closure(A×B,ProductTopology(T,S))⊆Closure(A,T)×Closure(B,S)" by auto
  {
    fix x assume x:"x∈Closure(A,T)×Closure(B,S)"
    then have xcl:"fst(x)∈Closure(A,T)" "snd(x)∈Closure(B,S)" by auto
    from xcl(1) have regT:"∀U∈T. fst(x)∈U ⟶ U∩A≠0" using topology0.cl_inter_neigh
      unfolding topology0_def using assms(1,3) by blast
    from xcl(2) have regS:"∀U∈S. snd(x)∈U ⟶ U∩B≠0" using topology0.cl_inter_neigh
      unfolding topology0_def using assms(2,4) by blast
    from x assms(3,4) have "x∈⋃T×⋃S" using topology0.Top_3_L11(1) unfolding topology0_def
      using assms(1,2) by blast
    then have xtot:"x∈⋃ProductTopology(T,S)" using Top_1_4_T1(3) assms(1,2) by auto
    {
      fix PO assume as:"PO∈ProductTopology(T,S)" "x∈PO"
      then obtain POB where base:"POB∈ProductCollection(T,S)" "x∈POB""POB⊆PO" using point_open_base_neigh
        Top_1_4_T1(2) assms(1,2) base_sets_open by blast
      then obtain VT VS where V:"VT∈T" "VS∈S" "x∈VT×VS" "POB=VT×VS" unfolding ProductCollection_def
        by auto
      from V(3) have x:"fst(x)∈VT" "snd(x)∈VS" by auto
      from V(1) regT x(1) have "VT∩A≠0" by auto moreover
      from V(2) regS x(2) have "VS∩B≠0" by auto ultimately
      have "VT×VS∩A×B≠0" by auto
      with V(4) base(3) have "PO∩A×B≠0" by blast
    }
    then have "∀P∈ProductTopology(T,S). x∈P ⟶ P∩A×B≠0" by auto
    then have "x∈Closure(A×B,ProductTopology(T,S))" using topology0.inter_neigh_cl
      unfolding topology0_def using top sub xtot by auto
  }
  then show "Closure(A,T)×Closure(B,S)⊆Closure(A×B,ProductTopology(T,S))" by auto
qed

text‹The product of closed sets, is closed in the product topology.›

corollary closed_product:
  assumes "T{is a topology}" "S{is a topology}" "A{is closed in}T""B{is closed in}S"
  shows "(A×B) {is closed in}ProductTopology(T,S)"
proof-
  from assms(3,4) have sub:"A⊆⋃T""B⊆⋃S" unfolding IsClosed_def by auto
  then have "A×B⊆⋃T×⋃S" by auto
  then have sub1:"A×B⊆⋃ProductTopology(T,S)" using Top_1_4_T1(3) assms(1,2) by auto
  from sub assms have "Closure(A,T)=A""Closure(B,S)=B" using topology0.Top_3_L8
    unfolding topology0_def by auto
  then have "Closure(A×B,ProductTopology(T,S))=A×B" using cl_product
    assms(1,2) sub by auto
  then show ?thesis using topology0.Top_3_L8 unfolding topology0_def
    using sub1 Top_1_4_T1(1) assms(1,2) by auto
qed

subsection‹Separation properties in product space›

text‹The product of $T_0$ spaces is $T_0$.›

theorem T0_product:
  assumes "T{is a topology}""S{is a topology}""T{is T0}""S{is T0}"
  shows "ProductTopology(T,S){is T0}"
proof-
  {
    fix x y assume "x∈⋃ProductTopology(T,S)""y∈⋃ProductTopology(T,S)""x≠y"
    then have tot:"x∈⋃T×⋃S""y∈⋃T×⋃S""x≠y" using Top_1_4_T1(3) assms(1,2) by auto
    then have "⟨fst(x),snd(x)⟩∈⋃T×⋃S""⟨fst(y),snd(y)⟩∈⋃T×⋃S" and disj:"fst(x)≠fst(y)∨snd(x)≠snd(y)" 
      using Pair_fst_snd_eq by auto
    then have T:"fst(x)∈⋃T""fst(y)∈⋃T" and S:"snd(y)∈⋃S""snd(x)∈⋃S" and p:"fst(x)≠fst(y)∨snd(x)≠snd(y)"
      by auto
    {
      assume "fst(x)≠fst(y)"
      with T assms(3) have "(∃U∈T. (fst(x)∈U∧fst(y)∉U)∨(fst(y)∈U∧fst(x)∉U))" unfolding
        isT0_def by auto
      then obtain U where "U∈T" "(fst(x)∈U∧fst(y)∉U)∨(fst(y)∈U∧fst(x)∉U)" by auto
      with S have "(⟨fst(x),snd(x)⟩∈U×(⋃S) ∧ ⟨fst(y),snd(y)⟩∉U×(⋃S))∨(⟨fst(y),snd(y)⟩∈U×(⋃S) ∧ ⟨fst(x),snd(x)⟩∉U×(⋃S))"
        by auto
      then have "(x∈U×(⋃S) ∧ y∉U×(⋃S))∨(y∈U×(⋃S) ∧ x∉U×(⋃S))" using Pair_fst_snd_eq tot(1,2) by auto
      moreover have "(⋃S)∈S" using assms(2) unfolding IsATopology_def by auto
      with ‹U∈T› have "U×(⋃S)∈ProductTopology(T,S)" using prod_open_open_prod assms(1,2) by auto
      ultimately
      have "∃V∈ProductTopology(T,S). (x∈V ∧ y∉V)∨(y∈V ∧ x∉V)" proof qed
    } moreover
    {
      assume "snd(x)≠snd(y)"
      with S assms(4) have "(∃U∈S. (snd(x)∈U∧snd(y)∉U)∨(snd(y)∈U∧snd(x)∉U))" unfolding
        isT0_def by auto
      then obtain U where "U∈S" "(snd(x)∈U∧snd(y)∉U)∨(snd(y)∈U∧snd(x)∉U)" by auto
      with T have "(⟨fst(x),snd(x)⟩∈(⋃T)×U ∧ ⟨fst(y),snd(y)⟩∉(⋃T)×U)∨(⟨fst(y),snd(y)⟩∈(⋃T)×U ∧ ⟨fst(x),snd(x)⟩∉(⋃T)×U)"
        by auto
      then have "(x∈(⋃T)×U ∧ y∉(⋃T)×U)∨(y∈(⋃T)×U ∧ x∉(⋃T)×U)" using Pair_fst_snd_eq tot(1,2) by auto
      moreover have "(⋃T)∈T" using assms(1) unfolding IsATopology_def by auto
      with ‹U∈S› have "(⋃T)×U∈ProductTopology(T,S)" using prod_open_open_prod assms(1,2) by auto
      ultimately
      have "∃V∈ProductTopology(T,S). (x∈V ∧ y∉V)∨(y∈V ∧ x∉V)" proof qed
    }moreover
    note disj
    ultimately have "∃V∈ProductTopology(T,S). (x∈V ∧ y∉V)∨(y∈V ∧ x∉V)" by auto
  }
  then show ?thesis unfolding isT0_def by auto
qed

text‹The product of $T_1$ spaces is $T_1$.›

theorem T1_product:
  assumes "T{is a topology}""S{is a topology}""T{is T1}""S{is T1}"
  shows "ProductTopology(T,S){is T1}"
proof-
  {
    fix x y assume "x∈⋃ProductTopology(T,S)""y∈⋃ProductTopology(T,S)""x≠y"
    then have tot:"x∈⋃T×⋃S""y∈⋃T×⋃S""x≠y" using Top_1_4_T1(3) assms(1,2) by auto
    then have "⟨fst(x),snd(x)⟩∈⋃T×⋃S""⟨fst(y),snd(y)⟩∈⋃T×⋃S" and disj:"fst(x)≠fst(y)∨snd(x)≠snd(y)" 
      using Pair_fst_snd_eq by auto
    then have T:"fst(x)∈⋃T""fst(y)∈⋃T" and S:"snd(y)∈⋃S""snd(x)∈⋃S" and p:"fst(x)≠fst(y)∨snd(x)≠snd(y)"
      by auto
    {
      assume "fst(x)≠fst(y)"
      with T assms(3) have "(∃U∈T. (fst(x)∈U∧fst(y)∉U))" unfolding
        isT1_def by auto
      then obtain U where "U∈T" "(fst(x)∈U∧fst(y)∉U)" by auto
      with S have "(⟨fst(x),snd(x)⟩∈U×(⋃S) ∧ ⟨fst(y),snd(y)⟩∉U×(⋃S))" by auto
      then have "(x∈U×(⋃S) ∧ y∉U×(⋃S))" using Pair_fst_snd_eq tot(1,2) by auto
      moreover have "(⋃S)∈S" using assms(2) unfolding IsATopology_def by auto
      with ‹U∈T› have "U×(⋃S)∈ProductTopology(T,S)" using prod_open_open_prod assms(1,2) by auto
      ultimately
      have "∃V∈ProductTopology(T,S). (x∈V ∧ y∉V)" proof qed
    } moreover
    {
      assume "snd(x)≠snd(y)"
      with S assms(4) have "(∃U∈S. (snd(x)∈U∧snd(y)∉U))" unfolding
        isT1_def by auto
      then obtain U where "U∈S" "(snd(x)∈U∧snd(y)∉U)" by auto
      with T have "(⟨fst(x),snd(x)⟩∈(⋃T)×U ∧ ⟨fst(y),snd(y)⟩∉(⋃T)×U)" by auto
      then have "(x∈(⋃T)×U ∧ y∉(⋃T)×U)" using Pair_fst_snd_eq tot(1,2) by auto
      moreover have "(⋃T)∈T" using assms(1) unfolding IsATopology_def by auto
      with ‹U∈S› have "(⋃T)×U∈ProductTopology(T,S)" using prod_open_open_prod assms(1,2) by auto
      ultimately
      have "∃V∈ProductTopology(T,S). (x∈V ∧ y∉V)" proof qed
    }moreover
    note disj
    ultimately have "∃V∈ProductTopology(T,S). (x∈V ∧ y∉V)" by auto
  }
  then show ?thesis unfolding isT1_def by auto
qed

text‹The product of $T_2$ spaces is $T_2$.›

theorem T2_product:
  assumes "T{is a topology}""S{is a topology}""T{is T2}""S{is T2}"
  shows "ProductTopology(T,S){is T2}"
proof-
  {
    fix x y assume "x∈⋃ProductTopology(T,S)""y∈⋃ProductTopology(T,S)""x≠y"
    then have tot:"x∈⋃T×⋃S""y∈⋃T×⋃S""x≠y" using Top_1_4_T1(3) assms(1,2) by auto
    then have "⟨fst(x),snd(x)⟩∈⋃T×⋃S""⟨fst(y),snd(y)⟩∈⋃T×⋃S" and disj:"fst(x)≠fst(y)∨snd(x)≠snd(y)" 
      using Pair_fst_snd_eq by auto
    then have T:"fst(x)∈⋃T""fst(y)∈⋃T" and S:"snd(y)∈⋃S""snd(x)∈⋃S" and p:"fst(x)≠fst(y)∨snd(x)≠snd(y)"
      by auto
    {
      assume "fst(x)≠fst(y)"
      with T assms(3) have "(∃U∈T. ∃V∈T. (fst(x)∈U∧fst(y)∈V) ∧ U∩V=0)" unfolding
        isT2_def by auto
      then obtain U V where "U∈T" "V∈T" "fst(x)∈U" "fst(y)∈V" "U∩V=0" by auto
      with S have "⟨fst(x),snd(x)⟩∈U×(⋃S)" "⟨fst(y),snd(y)⟩∈V×(⋃S)" and disjoint:"(U×⋃S)∩(V×⋃S)=0" by auto
      then have "x∈U×(⋃S)""y∈V×(⋃S)" using Pair_fst_snd_eq tot(1,2) by auto
      moreover have "(⋃S)∈S" using assms(2) unfolding IsATopology_def by auto
      with ‹U∈T›‹V∈T› have P:"U×(⋃S)∈ProductTopology(T,S)" "V×(⋃S)∈ProductTopology(T,S)" 
        using prod_open_open_prod assms(1,2) by auto
      note disjoint ultimately 
      have "x∈U×(⋃S) ∧ y∈V×(⋃S) ∧ (U×(⋃S))∩(V×(⋃S))=0" by auto
      with P(2) have "∃UU∈ProductTopology(T,S). (x∈U×(⋃S) ∧ y∈UU ∧ (U×(⋃S))∩UU=0)"
        using exI[where x="V×(⋃S)" and P="λt. t∈ProductTopology(T,S) ∧ (x∈U×(⋃S) ∧ y∈t ∧ (U×(⋃S))∩t=0)"] by auto
      with P(1) have "∃VV∈ProductTopology(T,S). ∃UU∈ProductTopology(T,S). (x∈VV ∧ y∈UU ∧ VV∩UU=0)" 
        using exI[where x="U×(⋃S)" and P="λt. t∈ProductTopology(T,S) ∧ (∃UU∈ProductTopology(T,S). (x∈t ∧ y∈UU ∧ (t)∩UU=0))"] by auto
    } moreover
    {
      assume "snd(x)≠snd(y)"
      with S assms(4) have "(∃U∈S. ∃V∈S. (snd(x)∈U∧snd(y)∈V) ∧ U∩V=0)" unfolding
        isT2_def by auto
      then obtain U V where "U∈S" "V∈S" "snd(x)∈U" "snd(y)∈V" "U∩V=0" by auto
      with T have "⟨fst(x),snd(x)⟩∈(⋃T)×U" "⟨fst(y),snd(y)⟩∈(⋃T)×V" and disjoint:"((⋃T)×U)∩((⋃T)×V)=0" by auto
      then have "x∈(⋃T)×U""y∈(⋃T)×V" using Pair_fst_snd_eq tot(1,2) by auto
      moreover have "(⋃T)∈T" using assms(1) unfolding IsATopology_def by auto
      with ‹U∈S›‹V∈S› have P:"(⋃T)×U∈ProductTopology(T,S)" "(⋃T)×V∈ProductTopology(T,S)" 
        using prod_open_open_prod assms(1,2) by auto
      note disjoint ultimately 
      have "x∈(⋃T)×U ∧ y∈(⋃T)×V ∧ ((⋃T)×U)∩((⋃T)×V)=0" by auto
      with P(2) have "∃UU∈ProductTopology(T,S). (x∈(⋃T)×U ∧ y∈UU ∧ ((⋃T)×U)∩UU=0)"
        using exI[where x="(⋃T)×V" and P="λt. t∈ProductTopology(T,S) ∧ (x∈(⋃T)×U ∧ y∈t ∧ ((⋃T)×U)∩t=0)"] by auto
      with P(1) have "∃VV∈ProductTopology(T,S). ∃UU∈ProductTopology(T,S). (x∈VV ∧ y∈UU ∧ VV∩UU=0)" 
        using exI[where x="(⋃T)×U" and P="λt. t∈ProductTopology(T,S) ∧ (∃UU∈ProductTopology(T,S). (x∈t ∧ y∈UU ∧ (t)∩UU=0))"] by auto
    } moreover
    note disj
    ultimately have "∃VV∈ProductTopology(T, S). ∃UU∈ProductTopology(T, S). x ∈ VV ∧ y ∈ UU ∧ VV ∩ UU = 0" by auto
  }
  then show ?thesis unfolding isT2_def by auto
qed

text‹The product of regular spaces is regular.›

theorem regular_product:
  assumes "T{is a topology}" "S{is a topology}" "T{is regular}" "S{is regular}"
  shows "ProductTopology(T,S){is regular}"
proof-
  {
    fix x U assume "x∈⋃ProductTopology(T,S)" "U∈ProductTopology(T,S)" "x∈U"
    then obtain V W where VW:"V∈T""W∈S" "V×W⊆U" and x:"x∈V×W" using prod_top_point_neighb 
      assms(1,2) by blast
    then have p:"fst(x)∈V""snd(x)∈W" by auto
    from p(1) ‹V∈T› obtain VV where VV:"fst(x)∈VV" "Closure(VV,T)⊆V" "VV∈T" using 
      assms(1,3) topology0.regular_imp_exist_clos_neig unfolding topology0_def
      by force moreover
    from p(2) ‹W∈S› obtain WW where WW:"snd(x)∈WW" "Closure(WW,S)⊆W" "WW∈S" using 
      assms(2,4) topology0.regular_imp_exist_clos_neig unfolding topology0_def
      by force ultimately
    have  "x∈VV×WW" using x by auto
    moreover from  ‹Closure(VV,T)⊆V› ‹Closure(WW,S)⊆W› have "Closure(VV,T)×Closure(WW,S) ⊆ V×W"
      by auto 
    moreover from VV(3) WW(3) have "VV⊆⋃T""WW⊆⋃S" by auto
    ultimately have "x∈VV×WW" "Closure(VV×WW,ProductTopology(T,S)) ⊆ V×W" using cl_product assms(1,2)
      by auto
    moreover have "VV×WW∈ProductTopology(T,S)" using prod_open_open_prod assms(1,2)
      VV(3) WW(3) by auto
    ultimately have "∃Z∈ProductTopology(T,S). x∈Z ∧ Closure(Z,ProductTopology(T,S))⊆V×W" by auto
    with VW(3) have "∃Z∈ProductTopology(T,S). x∈Z ∧ Closure(Z,ProductTopology(T,S))⊆U" by auto
  }
  then have "∀x∈⋃ProductTopology(T,S). ∀U∈ProductTopology(T,S).x∈U ⟶ (∃Z∈ProductTopology(T,S). x∈Z ∧ Closure(Z,ProductTopology(T,S))⊆U)"
    by auto
  then show ?thesis using topology0.exist_clos_neig_imp_regular unfolding topology0_def
    using assms(1,2) Top_1_4_T1(1) by auto
qed

subsection‹Connection properties in product space›

text‹First, we prove that the projection functions are open.›

lemma projection_open:
  assumes "T{is a topology}""S{is a topology}""B∈ProductTopology(T,S)"
  shows "{y∈⋃T. ∃x∈⋃S. ⟨y,x⟩∈B}∈T"
proof-
  {
    fix z assume "z∈{y∈⋃T. ∃x∈⋃S. ⟨y,x⟩∈B}"
    then obtain x where x:"x∈⋃S" and z:"z∈⋃T" and p:"⟨z,x⟩∈B" by auto
    then have "z∈{y∈⋃T. ⟨y,x⟩∈B}" "{y∈⋃T. ⟨y,x⟩∈B}⊆{y∈⋃T. ∃x∈⋃S. ⟨y,x⟩∈B}" by auto moreover
    from x have "{y∈⋃T. ⟨y,x⟩∈B}∈T" using prod_sec_open2 assms by auto
    ultimately have "∃V∈T. z∈V ∧ V⊆{y∈⋃T. ∃x∈⋃S. ⟨y,x⟩∈B}" unfolding Bex_def by auto
  }   
  then show "{y∈⋃T. ∃x∈⋃S. ⟨y,x⟩∈B}∈T" using topology0.open_neigh_open unfolding topology0_def
    using assms(1) by blast
qed

lemma projection_open2:
  assumes "T{is a topology}""S{is a topology}""B∈ProductTopology(T,S)"
  shows "{y∈⋃S. ∃x∈⋃T. ⟨x,y⟩∈B}∈S"
proof-
  {
    fix z assume "z∈{y∈⋃S. ∃x∈⋃T. ⟨x,y⟩∈B}"
    then obtain x where x:"x∈⋃T" and z:"z∈⋃S" and p:"⟨x,z⟩∈B" by auto
    then have "z∈{y∈⋃S. ⟨x,y⟩∈B}" "{y∈⋃S. ⟨x,y⟩∈B}⊆{y∈⋃S. ∃x∈⋃T. ⟨x,y⟩∈B}" by auto moreover
    from x have "{y∈⋃S. ⟨x,y⟩∈B}∈S" using prod_sec_open1 assms by auto
    ultimately have "∃V∈S. z∈V ∧ V⊆{y∈⋃S. ∃x∈⋃T. ⟨x,y⟩∈B}" unfolding Bex_def by auto
  }   
  then show "{y∈⋃S. ∃x∈⋃T. ⟨x,y⟩∈B}∈S" using topology0.open_neigh_open unfolding topology0_def
    using assms(2) by blast
qed

text‹The product of connected spaces is connected.›

theorem compact_product:
  assumes "T{is a topology}""S{is a topology}""T{is connected}""S{is connected}"
  shows "ProductTopology(T,S){is connected}"
proof-
  {
    fix U assume U:"U∈ProductTopology(T,S)" "U{is closed in}ProductTopology(T,S)"
    then have P:"U∈ProductTopology(T,S)" "⋃ProductTopology(T,S)-U∈ProductTopology(T,S)"
      unfolding IsClosed_def by auto
    {
      fix s assume s:"s∈⋃S" 
      with P(1) have p:"{x∈⋃T. ⟨x,s⟩∈U}∈T" using prod_sec_open2 assms(1,2) by auto
      from s P(2) have oop:"{y∈⋃T. ⟨y,s⟩∈(⋃ProductTopology(T,S)-U)}∈T" using prod_sec_open2
        assms(1,2) by blast
      then have "⋃T-(⋃T-{y∈⋃T. ⟨y,s⟩∈(⋃ProductTopology(T,S)-U)})={y∈⋃T. ⟨y,s⟩∈(⋃ProductTopology(T,S)-U)}" by auto
      with oop have cl:"(⋃T-{y∈⋃T. ⟨y,s⟩∈(⋃ProductTopology(T,S)-U)}) {is closed in}T" unfolding IsClosed_def by auto
      {
        fix t assume "t∈⋃T-{y∈⋃T. ⟨y,s⟩∈(⋃ProductTopology(T,S)-U)}"
        then have tt:"t∈⋃T" "t∉{y∈⋃T. ⟨y,s⟩∈(⋃ProductTopology(T,S)-U)}" by auto
        then have "⟨t,s⟩∉(⋃ProductTopology(T,S)-U)" by auto
        then have "⟨t,s⟩∈U ∨ ⟨t,s⟩∉⋃ProductTopology(T,S)" by auto
        then have "⟨t,s⟩∈U ∨ ⟨t,s⟩∉⋃T×⋃S" using Top_1_4_T1(3) assms(1,2) by auto
        with tt(1) s have "⟨t,s⟩∈U" by auto
        with tt(1) have "t∈{x∈⋃T. ⟨x,s⟩∈U}" by auto
      } moreover
      {
        fix t assume "t∈{x∈⋃T. ⟨x,s⟩∈U}"
        then have tt:"t∈⋃T" "⟨t,s⟩∈U" by auto
        then have "⟨t,s⟩∉⋃ProductTopology(T,S)-U" by auto
        then have "t∉{y∈⋃T. ⟨y,s⟩∈(⋃ProductTopology(T,S)-U)}" by auto
        with tt(1) have "t∈⋃T-{y∈⋃T. ⟨y,s⟩∈(⋃ProductTopology(T,S)-U)}" by auto
      }
      ultimately have "{x∈⋃T. ⟨x,s⟩∈U}=⋃T-{y∈⋃T. ⟨y,s⟩∈(⋃ProductTopology(T,S)-U)}" by blast
      with cl have "{x∈⋃T. ⟨x,s⟩∈U}{is closed in}T" by auto
      with p assms(3) have "{x∈⋃T. ⟨x,s⟩∈U}=0 ∨ {x∈⋃T. ⟨x,s⟩∈U}=⋃T" unfolding IsConnected_def
        by auto moreover
      {
        assume "{x∈⋃T. ⟨x,s⟩∈U}=0"
        then have "∀x∈⋃T. ⟨x,s⟩∉U" by auto
      }
      moreover
      {
        assume AA:"{x∈⋃T. ⟨x,s⟩∈U}=⋃T"
        {
          fix x assume "x∈⋃T"
          with AA have "x∈{x∈⋃T. ⟨x,s⟩∈U}" by auto
          then have "⟨x,s⟩∈U" by auto
        }
        then have "∀x∈⋃T. ⟨x,s⟩∈U" by auto
      }
      ultimately have "(∀x∈⋃T. ⟨x,s⟩∉U) ∨ (∀x∈⋃T. ⟨x,s⟩∈U)" by blast
    }
    then have reg:"∀s∈⋃S. (∀x∈⋃T. ⟨x,s⟩∉U) ∨ (∀x∈⋃T. ⟨x,s⟩∈U)" by auto
    {
      fix q assume qU:"q∈⋃T×{snd(qq). qq∈U}"
      then obtain t u where t:"t∈⋃T" "u∈U" "q=⟨t,snd(u)⟩" by auto
      with U(1) have "u∈⋃ProductTopology(T,S)" by auto
      then have "u∈⋃T×⋃S" using Top_1_4_T1(3) assms(1,2) by auto moreover
      then have uu:"u=⟨fst(u),snd(u)⟩" using Pair_fst_snd_eq by auto ultimately
      have fu:"fst(u)∈⋃T""snd(u)∈⋃S" by (safe,auto)
      with reg have "(∀tt∈⋃T. ⟨tt,snd(u)⟩∉U)∨(∀tt∈⋃T. ⟨tt,snd(u)⟩∈U)" by auto
      with ‹u∈U› uu fu(1) have "∀tt∈⋃T. ⟨tt,snd(u)⟩∈U" by force
      with t(1,3) have "q∈U" by auto
    }
    then have U1:"⋃T×{snd(qq). qq∈U}⊆U" by auto
    {
      fix t assume t:"t∈⋃T" 
      with P(1) have p:"{x∈⋃S. ⟨t,x⟩∈U}∈S" using prod_sec_open1 assms(1,2) by auto
      from t P(2) have oop:"{x∈⋃S. ⟨t,x⟩∈(⋃ProductTopology(T,S)-U)}∈S" using prod_sec_open1
        assms(1,2) by blast
      then have "⋃S-(⋃S-{x∈⋃S. ⟨t,x⟩∈(⋃ProductTopology(T,S)-U)})={y∈⋃S. ⟨t,y⟩∈(⋃ProductTopology(T,S)-U)}" by auto
      with oop have cl:"(⋃S-{y∈⋃S. ⟨t,y⟩∈(⋃ProductTopology(T,S)-U)}) {is closed in}S" unfolding IsClosed_def by auto
      {
        fix s assume "s∈⋃S-{y∈⋃S. ⟨t,y⟩∈(⋃ProductTopology(T,S)-U)}"
        then have tt:"s∈⋃S" "s∉{y∈⋃S. ⟨t,y⟩∈(⋃ProductTopology(T,S)-U)}" by auto
        then have "⟨t,s⟩∉(⋃ProductTopology(T,S)-U)" by auto
        then have "⟨t,s⟩∈U ∨ ⟨t,s⟩∉⋃ProductTopology(T,S)" by auto
        then have "⟨t,s⟩∈U ∨ ⟨t,s⟩∉⋃T×⋃S" using Top_1_4_T1(3) assms(1,2) by auto
        with tt(1) t have "⟨t,s⟩∈U" by auto
        with tt(1) have "s∈{x∈⋃S. ⟨t,x⟩∈U}" by auto
      } moreover
      {
        fix s assume "s∈{x∈⋃S. ⟨t,x⟩∈U}"
        then have tt:"s∈⋃S" "⟨t,s⟩∈U" by auto
        then have "⟨t,s⟩∉⋃ProductTopology(T,S)-U" by auto
        then have "s∉{y∈⋃S. ⟨t,y⟩∈(⋃ProductTopology(T,S)-U)}" by auto
        with tt(1) have "s∈⋃S-{y∈⋃S. ⟨t,y⟩∈(⋃ProductTopology(T,S)-U)}" by auto
      }
      ultimately have "{x∈⋃S. ⟨t,x⟩∈U}=⋃S-{y∈⋃S. ⟨t,y⟩∈(⋃ProductTopology(T,S)-U)}" by blast
      with cl have "{x∈⋃S. ⟨t,x⟩∈U}{is closed in}S" by auto
      with p assms(4) have "{x∈⋃S. ⟨t,x⟩∈U}=0 ∨ {x∈⋃S. ⟨t,x⟩∈U}=⋃S" unfolding IsConnected_def
        by auto moreover
      {
        assume "{x∈⋃S. ⟨t,x⟩∈U}=0"
        then have "∀x∈⋃S. ⟨t,x⟩∉U" by auto
      }
      moreover
      {
        assume AA:"{x∈⋃S. ⟨t,x⟩∈U}=⋃S"
        {
          fix x assume "x∈⋃S"
          with AA have "x∈{x∈⋃S. ⟨t,x⟩∈U}" by auto
          then have "⟨t,x⟩∈U" by auto
        }
        then have "∀x∈⋃S. ⟨t,x⟩∈U" by auto
      }
      ultimately have "(∀x∈⋃S. ⟨t,x⟩∉U) ∨ (∀x∈⋃S. ⟨t,x⟩∈U)" by blast
    }
    then have reg:"∀s∈⋃T. (∀x∈⋃S. ⟨s,x⟩∉U) ∨ (∀x∈⋃S. ⟨s,x⟩∈U)" by auto
    {
      fix q assume qU:"q∈{fst(qq). qq∈U}×⋃S"
      then obtain qq s where t:"q=⟨fst(qq),s⟩" "qq∈U" "s∈⋃S" by auto
      with U(1) have "qq∈⋃ProductTopology(T,S)" by auto
      then have "qq∈⋃T×⋃S" using Top_1_4_T1(3) assms(1,2) by auto moreover
      then have qq:"qq=⟨fst(qq),snd(qq)⟩" using Pair_fst_snd_eq by auto ultimately
      have fq:"fst(qq)∈⋃T""snd(qq)∈⋃S" by (safe,auto)
      from fq(1) reg have "(∀tt∈⋃S. ⟨fst(qq),tt⟩∉U)∨(∀tt∈⋃S. ⟨fst(qq),tt⟩∈U)" by auto moreover
      with ‹qq∈U› qq fq(2) have "∀tt∈⋃S. ⟨fst(qq),tt⟩∈U" by force
      with t(1,3) have "q∈U" by auto
    }
    then have U2:"{fst(qq). qq∈U}×⋃S⊆U" by blast
    {
      assume "U≠0"
      then obtain u where u:"u∈U" by auto
      {
        fix aa assume "aa∈⋃T×⋃S"
        then obtain t s where "t∈⋃T""s∈⋃S""aa=⟨t,s⟩" by auto
        with u have "⟨t,snd(u)⟩∈⋃T×{snd(qq). qq∈U}" by auto
        with U1 have "⟨t,snd(u)⟩∈U" by auto
        moreover have "t=fst(⟨t,snd(u)⟩)" by auto moreover note ‹s∈⋃S› ultimately
        have "⟨t,s⟩∈{fst(qq). qq∈U}×⋃S" by blast
        with U2 have "⟨t,s⟩∈U" by auto
        with ‹aa=⟨t,s⟩› have "aa∈U" by auto
      }
      then have "⋃T×⋃S⊆U" by auto moreover
      with U(1) have "U⊆⋃ProductTopology(T,S)" by auto ultimately
      have "⋃T×⋃S=U" using Top_1_4_T1(3) assms(1,2) by auto
    }
    then have "(U=0)∨(U=⋃T×⋃S)" by auto
  }
  then show ?thesis unfolding IsConnected_def using Top_1_4_T1(3) assms(1,2) by auto
qed

end