(* 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 op:"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 op 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 op:"(⋃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 op 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 T⇩_{0}}""S{is T⇩_{0}}" shows "ProductTopology(T,S){is T⇩_{0}}" 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 T⇩_{1}}""S{is T⇩_{1}}" shows "ProductTopology(T,S){is T⇩_{1}}" 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 T⇩_{2}}""S{is T⇩_{2}}" shows "ProductTopology(T,S){is T⇩_{2}}" 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 op:"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 op(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 op(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 op:"(⋃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 op(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 op(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 op:"U∈ProductTopology(T,S)" "⋃ProductTopology(T,S)-U∈ProductTopology(T,S)" unfolding IsClosed_def by auto { fix s assume s:"s∈⋃S" with op(1) have p:"{x∈⋃T. ⟨x,s⟩∈U}∈T" using prod_sec_open2 assms(1,2) by auto from s op(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 op(1) have p:"{x∈⋃S. ⟨t,x⟩∈U}∈S" using prod_sec_open1 assms(1,2) by auto from t op(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