(* 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 8› theory Topology_ZF_8 imports Topology_ZF_6 EquivClass1 begin text{*This theory deals with quotient topologies.*} subsection{*Definition of quotient topology*} text{*Given a surjective function $f:X\to Y$ and a topology $\tau$ in $X$, it is posible to consider a special topology in $Y$. $f$ is called quotient function.*} definition(in topology0) QuotientTop ("{quotient topology in}_{by}_" 80) where "f∈surj(⋃T,Y) ⟹{quotient topology in}Y{by}f≡ {U∈Pow(Y). f-``U∈T}" abbreviation QuotientTopTop ("{quotient topology in}_{by}_{from}_") where "QuotientTopTop(Y,f,T) ≡ topology0.QuotientTop(T,Y,f)" text{*The quotient topology is indeed a topology.*} theorem(in topology0) quotientTop_is_top: assumes "f∈surj(⋃T,Y)" shows "({quotient topology in} Y {by} f) {is a topology}" proof- have "({quotient topology in} Y {by} f)={U ∈ Pow(Y) . f -`` U ∈ T}" using QuotientTop_def assms by auto moreover { fix M x B assume M:"M ⊆ {U ∈ Pow(Y) . f -`` U ∈ T}" then have "⋃M⊆Y" by blast moreover have A1:"f -`` (⋃M)=(⋃y∈(⋃M). f-``{y})" using vimage_eq_UN by blast { fix A assume "A∈M" with M have "A∈Pow(Y)" "f -`` A∈T" by auto have "f -`` A=(⋃y∈A. f-``{y})" using vimage_eq_UN by blast } then have "(⋃A∈M. f-`` A)=(⋃A∈M. (⋃y∈A. f-``{y}))" by auto then have "(⋃A∈M. f-`` A)=(⋃y∈⋃M. f-``{y})" by auto with A1 have A2:"f -`` (⋃M)=⋃{f-`` A. A∈M}" by auto { fix A assume "A∈M" with M have "f -`` A∈T" by auto } then have "∀A∈M. f -`` A∈T" by auto then have "{f-`` A. A∈M}⊆T" by auto then have "(⋃{f-`` A. A∈M})∈T" using topSpaceAssum unfolding IsATopology_def by auto with A2 have "(f -`` (⋃M))∈T" by auto ultimately have "⋃M∈{U∈Pow(Y). f-``U∈T}" by auto } moreover { fix U V assume "U∈{U∈Pow(Y). f-``U∈T}""V∈{U∈Pow(Y). f-``U∈T}" then have "U∈Pow(Y)""V∈Pow(Y)""f-``U∈T""f-``V∈T" by auto then have "(f-``U)∩(f-``V)∈T" using topSpaceAssum unfolding IsATopology_def by auto then have "f-`` (U∩V)∈T" using invim_inter_inter_invim assms unfolding surj_def by auto with `U∈Pow(Y)``V∈Pow(Y)` have "U∩V∈{U∈Pow(Y). f-``U∈T}" by auto } ultimately show ?thesis using IsATopology_def by auto qed text{*The quotient function is continuous.*} lemma (in topology0) quotient_func_cont: assumes "f∈surj(⋃T,Y)" shows "IsContinuous(T,({quotient topology in} Y {by} f),f)" unfolding IsContinuous_def using QuotientTop_def assms by auto text{*One of the important properties of this topology, is that a function from the quotient space is continuous iff the composition with the quotient function is continuous.*} theorem(in two_top_spaces0) cont_quotient_top: assumes "h∈surj(⋃τ⇩_{1},Y)" "g:Y→⋃τ⇩_{2}" "IsContinuous(τ⇩_{1},τ⇩_{2},g O h)" shows "IsContinuous(({quotient topology in} Y {by} h {from} τ⇩_{1}),τ⇩_{2},g)" proof- { fix U assume "U∈τ⇩_{2}" with assms(3) have "(g O h)-``(U)∈τ⇩_{1}" unfolding IsContinuous_def by auto then have "h-``(g-``(U))∈τ⇩_{1}" using vimage_comp by auto then have "g-``(U)∈({quotient topology in} Y {by} h {from} τ⇩_{1})" using topology0.QuotientTop_def tau1_is_top assms(1) using func1_1_L3 assms(2) unfolding topology0_def by auto } then show ?thesis unfolding IsContinuous_def by auto qed text{*The underlying set of the quotient topology is $Y$.*} lemma(in topology0) total_quo_func: assumes "f∈surj(⋃T,Y)" shows "(⋃({quotient topology in}Y{by}f))=Y" proof- from assms have "f-``Y=⋃T" using func1_1_L4 unfolding surj_def by auto moreover have "⋃T∈T" using topSpaceAssum unfolding IsATopology_def by auto ultimately have "Y∈({quotient topology in}Y{by}f{from}T)" using QuotientTop_def assms by auto then show ?thesis using QuotientTop_def assms by auto qed subsection{*Quotient topologies from equivalence relations*} text{*In this section we will show that the quotient topologies come from an equivalence relation.*} text{*First, some lemmas for relations.*} lemma quotient_proj_fun: shows "{⟨b,r``{b}⟩. b∈A}:A→A//r" unfolding Pi_def function_def domain_def unfolding quotient_def by auto lemma quotient_proj_surj: shows "{⟨b,r``{b}⟩. b∈A}∈surj(A,A//r)" proof- { fix y assume "y∈A//r" then obtain yy where A:"yy∈A" "y=r``{yy}" unfolding quotient_def by auto then have "⟨yy,y⟩∈{⟨b,r``{b}⟩. b∈A}" by auto then have "{⟨b,r``{b}⟩. b∈A}`yy=y" using apply_equality[OF _ quotient_proj_fun] by auto with A(1) have "∃yy∈A. {⟨b,r``{b}⟩. b∈A}`yy=y" by auto } with quotient_proj_fun show ?thesis unfolding surj_def by auto qed lemma preim_equi_proj: assumes "U⊆A//r" "equiv(A,r)" shows "{⟨b,r``{b}⟩. b∈A}-``U=⋃U" proof { fix y assume "y∈⋃U" then obtain V where V:"y∈V""V∈U" by auto with `U⊆(A//r)` have "y∈A" using EquivClass_1_L1 assms(2) by auto moreover from `U⊆(A//r)` V have "r``{y}=V" using EquivClass_1_L2 assms(2) by auto moreover note V(2) ultimately have "y∈{x∈A. r``{x}∈U}" by auto then have "y∈{⟨b,r``{b}⟩. b∈A}-``U" by auto } then show "⋃U⊆{⟨b,r``{b}⟩. b∈A}-``U" by blast moreover { fix y assume "y∈{⟨b,r``{b}⟩. b∈A}-``U" then have yy:"y∈{x∈A. r``{x}∈U}" by auto then have "r``{y}∈U" by auto moreover from yy have "y∈r``{y}" using assms equiv_class_self by auto ultimately have "y∈⋃U" by auto } then show "{⟨b,r``{b}⟩. b∈A}-``U⊆⋃U" by blast qed text{*Now we define what a quotient topology from an equivalence relation is:*} definition(in topology0) EquivQuo ("{quotient by}_" 70) where "equiv(⋃T,r)⟹({quotient by}r)≡{quotient topology in}(⋃T)//r{by}{⟨b,r``{b}⟩. b∈⋃T}" abbreviation EquivQuoTop ("_{quotient by}_" 60) where "EquivQuoTop(T,r)≡topology0.EquivQuo(T,r)" text{*First, another description of the topology (more intuitive):*} theorem (in topology0) quotient_equiv_rel: assumes "equiv(⋃T,r)" shows "({quotient by}r)={U∈Pow((⋃T)//r). ⋃U∈T}" proof- have "({quotient topology in}(⋃T)//r{by}{⟨b,r``{b}⟩. b∈⋃T})={U∈Pow((⋃T)//r). {⟨b,r``{b}⟩. b∈⋃T}-``U∈T}" using QuotientTop_def quotient_proj_surj by auto moreover have "{U∈Pow((⋃T)//r). {⟨b,r``{b}⟩. b∈⋃T}-``U∈T}={U∈Pow((⋃T)//r). ⋃U∈T}" proof { fix U assume "U∈{U∈Pow((⋃T)//r). {⟨b,r``{b}⟩. b∈⋃T}-``U∈T}" then have "U∈{U∈Pow((⋃T)//r). ⋃U∈T}" using preim_equi_proj assms by auto } then show "{U∈Pow((⋃T)//r). {⟨b,r``{b}⟩. b∈⋃T}-``U∈T}⊆{U∈Pow((⋃T)//r). ⋃U∈T}" by auto { fix U assume "U∈{U∈Pow((⋃T)//r). ⋃U∈T}" then have "U∈{U∈Pow((⋃T)//r). {⟨b,r``{b}⟩. b∈⋃T}-``U∈T}" using preim_equi_proj assms by auto } then show "{U∈Pow((⋃T)//r). ⋃U∈T}⊆{U∈Pow((⋃T)//r). {⟨b,r``{b}⟩. b∈⋃T}-``U∈T}" by auto qed ultimately show ?thesis using EquivQuo_def assms by auto qed text{*We apply previous results to this topology.*} theorem(in topology0) total_quo_equi: assumes "equiv(⋃T,r)" shows "⋃({quotient by}r)=(⋃T)//r" using total_quo_func quotient_proj_surj EquivQuo_def assms by auto theorem(in topology0) equiv_quo_is_top: assumes "equiv(⋃T,r)" shows "({quotient by}r){is a topology}" using quotientTop_is_top quotient_proj_surj EquivQuo_def assms by auto text{*MAIN RESULT: All quotient topologies arise from an equivalence relation given by the quotient function $f:X\to Y$. This means that any quotient topology is homeomorphic to a topology given by an equivalence relation quotient.*} theorem(in topology0) equiv_quotient_top: assumes "f∈surj(⋃T,Y)" defines "r≡{⟨x,y⟩∈⋃T×⋃T. f`(x)=f`(y)}" defines "g≡{⟨y,f-``{y}⟩. y∈Y}" shows "equiv(⋃T,r)" and "IsAhomeomorphism(({quotient topology in}Y{by}f),({quotient by}r),g)" proof- have ff:"f:⋃T→Y" using assms(1) unfolding surj_def by auto show B:"equiv(⋃T,r)" unfolding equiv_def refl_def sym_def trans_def unfolding r_def by auto have gg:"g:Y→((⋃T)//r)" proof- { fix B assume "B∈g" then obtain y where Y:"y∈Y" "B=⟨y,f-``{y}⟩" unfolding g_def by auto then have "f-``{y}⊆⋃T" using func1_1_L3 ff by blast then have eq:"f-``{y}={x∈⋃T. ⟨x,y⟩∈f}" using vimage_iff by auto from Y obtain A where A1:"A∈⋃T""f`A=y" using assms(1) unfolding surj_def by blast with eq have A:"A∈f-``{y}" using apply_Pair[OF ff] by auto { fix t assume "t∈f-``{y}" with A have "t∈⋃T""A∈⋃T""⟨t,y⟩∈f""⟨A,y⟩∈f" using eq by auto then have "f`t=f`A" using apply_equality assms(1) unfolding surj_def by auto with `t∈⋃T``A∈⋃T` have "⟨A,t⟩∈r" using r_def by auto then have "t∈r``{A}" using image_iff by auto } then have "f-``{y}⊆r``{A}" by auto moreover { fix t assume "t∈r``{A}" then have "⟨A,t⟩∈r" using image_iff by auto then have un:"t∈⋃T""A∈⋃T" and eq2:"f`t=f`A" unfolding r_def by auto moreover from un have "⟨t,f`t⟩∈f" using apply_Pair[OF ff] by auto with eq2 A1 have "⟨t,y⟩∈f" by auto with un have "t∈f-``{y}" using eq by auto } then have "r``{A}⊆f-``{y}" by auto ultimately have "f-``{y}=r``{A}" by auto then have "f-``{y}∈ (⋃T)//r" using A1(1) unfolding quotient_def by auto with Y have "B∈Y×(⋃T)//r" by auto } then have "∀A∈g. A∈ Y×(⋃T)//r" by auto then have "g⊆(Y×(⋃T)//r)" by auto moreover then show ?thesis unfolding Pi_def function_def domain_def g_def by auto qed then have gg2:"g:Y→(⋃({quotient by}r))" using total_quo_equi B by auto { fix s assume S:"s∈({quotient topology in}Y{by}f)" then have "s∈Pow(Y)"and op:"f-``s∈T" using QuotientTop_def topSpaceAssum assms(1) by auto have "f-``s=(⋃y∈s. f-``{y})" using vimage_eq_UN by blast moreover from `s∈Pow(Y)` have "∀y∈s. ⟨y,f-``{y}⟩∈g" unfolding g_def by auto then have "∀y∈s. g`y=f-``{y}" using apply_equality gg by auto ultimately have "f-``s=(⋃y∈s. g`y)" by auto with op have "(⋃y∈s. g`y)∈T" by auto moreover from `s∈Pow(Y)` have "∀y∈s. g`y∈(⋃T)//r" using apply_type gg by auto ultimately have "{g`y. y∈s}∈({quotient by}r)" using quotient_equiv_rel B by auto with `s∈Pow(Y)` have "g``s∈({quotient by}r)" using func_imagedef gg by auto } then have gopen:"∀s∈({quotient topology in}Y{by}f). g``s∈(T{quotient by}r)" by auto have pr_fun:"{⟨b,r``{b}⟩. b∈⋃T}:⋃T→(⋃T)//r" using quotient_proj_fun by auto { fix b assume b:"b∈⋃T" have bY:"f`b∈Y" using apply_funtype ff b by auto with b have com:"(g O f)`b=g`(f`b)" using comp_fun_apply ff by auto from bY have pg:"⟨f`b,f-``({f`b})⟩∈g" unfolding g_def by auto then have "g`(f`b)=f-``({f`b})" using apply_equality gg by auto with com have comeq:"(g O f)`b=f-``({f`b})" by auto from b have A:"f``{b}={f`b}" "{b}⊆⋃T" using func_imagedef ff by auto from A(2) have "b∈f -`` (f `` {b})" using func1_1_L9 ff by blast then have "b∈f-``({f`b})" using A(1) by auto moreover from pg have "f-``({f`b})∈(⋃T)//r" using gg unfolding Pi_def by auto ultimately have "r``{b}=f-``({f`b})" using EquivClass_1_L2 B by auto then have "(g O f)`b=r``{b}" using comeq by auto moreover from b have "⟨b,r``{b}⟩∈{⟨b,r``{b}⟩. b∈⋃T}" by auto with pr_fun have "{⟨b,r``{b}⟩. b∈⋃T}`b=r``{b}" using apply_equality by auto ultimately have "(g O f)`b={⟨b,r``{b}⟩. b∈⋃T}`b" by auto } then have reg:"∀b∈⋃T. (g O f)`b={⟨b,r``{b}⟩. b∈⋃T}`b" by auto moreover have compp:"g O f∈⋃T→(⋃T)//r" using comp_fun ff gg by auto have feq:"(g O f)={⟨b,r``{b}⟩. b∈⋃T}" using fun_extension[OF compp pr_fun] reg by auto then have "IsContinuous(T,{quotient by}r,(g O f))" using quotient_func_cont quotient_proj_surj EquivQuo_def topSpaceAssum B by auto moreover have "(g O f):⋃T→⋃({quotient by}r)" using comp_fun ff gg2 by auto ultimately have gcont:"IsContinuous({quotient topology in}Y{by}f,{quotient by}r,g)" using two_top_spaces0.cont_quotient_top assms(1) gg2 unfolding two_top_spaces0_def using topSpaceAssum equiv_quo_is_top B by auto { fix x y assume T:"x∈Y""y∈Y""g`x=g`y" then have "f-``{x}=f-``{y}" using apply_equality gg unfolding g_def by auto then have "f``(f-``{x})=f``(f-``{y})" by auto with T(1,2) have "{x}={y}" using surj_image_vimage assms(1) by auto then have "x=y" by auto } with gg2 have "g∈inj(Y,⋃({quotient by}r))" unfolding inj_def by auto moreover have "g O f∈surj(⋃T, (⋃T)//r)" using feq quotient_proj_surj by auto then have "g∈surj(Y,(⋃T)//r)" using comp_mem_surjD1 ff gg by auto then have "g∈surj(Y,⋃(T{quotient by}r))" using total_quo_equi B by auto ultimately have "g∈bij(⋃({quotient topology in}Y{by}f),⋃({quotient by}r))" unfolding bij_def using total_quo_func assms(1) by auto with gcont gopen show "IsAhomeomorphism(({quotient topology in}Y{by}f),({quotient by}r),g)" using bij_cont_open_homeo by auto qed lemma product_equiv_rel_fun: shows "{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}:(⋃T×⋃T)→((⋃T)//r×(⋃T)//r)" proof- have " {⟨b,r``{b}⟩. b∈⋃T}∈⋃T→(⋃T)//r" using quotient_proj_fun by auto moreover have "∀A∈⋃T. ⟨A,r``{A}⟩∈{⟨b,r``{b}⟩. b∈⋃T}" by auto ultimately have "∀A∈⋃T. {⟨b,r``{b}⟩. b∈⋃T}`A=r``{A}" using apply_equality by auto then have IN:" {⟨⟨b, c⟩, r `` {b}, r `` {c}⟩ . ⟨b,c⟩ ∈ ⋃T × ⋃T}= {⟨⟨x, y⟩, {⟨b, r `` {b}⟩ . b ∈ ⋃T} ` x, {⟨b, r `` {b}⟩ . b ∈ ⋃T} ` y⟩ . ⟨x,y⟩ ∈ ⋃T × ⋃T}" by force then show ?thesis using prod_fun quotient_proj_fun by auto qed lemma(in topology0) prod_equiv_rel_surj: shows "{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}:surj(⋃(ProductTopology(T,T)),((⋃T)//r×(⋃T)//r))" proof- have fun:"{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}:(⋃T×⋃T)→((⋃T)//r×(⋃T)//r)" using product_equiv_rel_fun by auto moreover { fix M assume "M∈((⋃T)//r×(⋃T)//r)" then obtain M1 M2 where M:"M=⟨M1,M2⟩" "M1∈(⋃T)//r""M2∈(⋃T)//r" by auto then obtain m1 m2 where m:"m1∈⋃T""m2∈⋃T""M1=r``{m1}""M2=r``{m2}" unfolding quotient_def by auto then have mm:"⟨m1,m2⟩∈(⋃T×⋃T)" by auto then have "⟨⟨m1,m2⟩,⟨r``{m1},r``{m2}⟩⟩∈{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}" by auto then have "{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}`⟨m1,m2⟩=⟨r``{m1},r``{m2}⟩" using apply_equality fun by auto then have "{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}`⟨m1,m2⟩=M" using M(1) m(3,4) by auto then have "∃R∈(⋃T×⋃T). {⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}`R=M" using mm by auto } ultimately show ?thesis unfolding surj_def using Top_1_4_T1(3) topSpaceAssum by auto qed lemma(in topology0) product_quo_fun: assumes "equiv(⋃T,r)" shows "IsContinuous(ProductTopology(T,T),ProductTopology({quotient by}r,({quotient by}r)),{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T})" proof- have "{⟨b,r``{b}⟩. b∈⋃T}:⋃T→(⋃T)//r" using quotient_proj_fun by auto moreover have "∀A∈⋃T. ⟨A,r``{A}⟩∈{⟨b,r``{b}⟩. b∈⋃T}" by auto ultimately have "∀A∈⋃T. {⟨b,r``{b}⟩. b∈⋃T}`A=r``{A}" using apply_equality by auto then have IN:" {⟨⟨b, c⟩, r `` {b}, r `` {c}⟩ . ⟨b,c⟩ ∈ ⋃T × ⋃T}= {⟨⟨x, y⟩, {⟨b, r `` {b}⟩ . b ∈ ⋃T} ` x, {⟨b, r `` {b}⟩ . b ∈ ⋃T} ` y⟩ . ⟨x,y⟩ ∈ ⋃T × ⋃T}" by force have cont:"IsContinuous(T,{quotient by}r,{⟨b,r``{b}⟩. b∈⋃T})" using quotient_func_cont quotient_proj_surj EquivQuo_def assms by auto have tot:"⋃(T{quotient by}r) = (⋃T) // r" and top:"({quotient by}r) {is a topology}" using total_quo_equi equiv_quo_is_top assms by auto then have fun:"{⟨b,r``{b}⟩. b∈⋃T}:⋃T→⋃({quotient by}r)" using quotient_proj_fun by auto then have two:"two_top_spaces0(T,{quotient by}r,{⟨b,r``{b}⟩. b∈⋃T})" unfolding two_top_spaces0_def using topSpaceAssum top by auto show ?thesis using two_top_spaces0.product_cont_functions two fun fun cont cont top topSpaceAssum IN by auto qed text{*The product of quotient topologies is a quotient topology given that the quotient map is open. This isn't true in general.*} theorem(in topology0) prod_quotient: assumes "equiv(⋃T,r)" "∀A∈T. {⟨b,r``{b}⟩. b∈⋃T}``A∈({quotient by}r)" shows "(ProductTopology({quotient by}r,{quotient by}r)) = ({quotient topology in}(((⋃T)//r)×((⋃T)//r)){by}({⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}){from}(ProductTopology(T,T)))" proof { fix A assume A:"A∈ProductTopology({quotient by}r,{quotient by}r)" from assms have "IsContinuous(ProductTopology(T,T),ProductTopology({quotient by}r,({quotient by}r)),{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T})" using product_quo_fun by auto with A have "{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}-``A∈ProductTopology(T,T)" unfolding IsContinuous_def by auto moreover from A have "A⊆⋃ProductTopology(T{quotient by}r,T{quotient by}r)" by auto then have "A⊆⋃(T{quotient by}r)×⋃(T{quotient by}r)" using Top_1_4_T1(3) equiv_quo_is_top equiv_quo_is_top using assms by auto then have "A∈Pow(((⋃T)//r)×((⋃T)//r))" using total_quo_equi assms by auto ultimately have "A∈({quotient topology in}(((⋃T)//r)×((⋃T)//r)){by}{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}{from}(ProductTopology(T,T)))" using topology0.QuotientTop_def Top_1_4_T1(1) topSpaceAssum prod_equiv_rel_surj assms(1) unfolding topology0_def by auto } then show "ProductTopology(T{quotient by}r,T{quotient by}r)⊆({quotient topology in}(((⋃T)//r)×((⋃T)//r)){by}{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}{from}(ProductTopology(T,T)))" by auto { fix A assume "A∈({quotient topology in}(((⋃T)//r)×((⋃T)//r)){by}{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}{from}(ProductTopology(T,T)))" then have A:"A⊆((⋃T)//r)×((⋃T)//r)" "{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}-``A∈ProductTopology(T,T)" using topology0.QuotientTop_def Top_1_4_T1(1) topSpaceAssum prod_equiv_rel_surj assms(1) unfolding topology0_def by auto { fix CC assume "CC∈A" with A(1) obtain C1 C2 where CC:"CC=⟨C1,C2⟩" "C1∈((⋃T)//r)""C2∈((⋃T)//r)" by auto then obtain c1 c2 where CC1:"c1∈⋃T""c2∈⋃T" and CC2:"C1=r``{c1}""C2=r``{c2}" unfolding quotient_def by auto then have "⟨c1,c2⟩∈⋃T×⋃T" by auto then have "⟨⟨c1,c2⟩,⟨r``{c1},r``{c2}⟩⟩∈{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}" by auto with CC2 CC have "⟨⟨c1,c2⟩,CC⟩∈{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}" by auto with `CC∈A` have "⟨c1,c2⟩∈{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}-``A" using vimage_iff by auto with A(2) have " ∃V W. V ∈ T ∧ W ∈ T ∧ V × W ⊆ {⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}-``A ∧ ⟨c1,c2⟩ ∈ V × W" using prod_top_point_neighb topSpaceAssum by blast then obtain V W where VW:"V∈T""W∈T""V × W ⊆ {⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}-``A""c1∈V""c2∈W" by auto with assms(2) have "{⟨b,r``{b}⟩. b∈⋃T}``V∈(T{quotient by}r)""{⟨b,r``{b}⟩. b∈⋃T}``W∈(T{quotient by}r)" by auto then have op:"{⟨b,r``{b}⟩. b∈⋃T}``V×{⟨b,r``{b}⟩. b∈⋃T}``W∈ProductTopology(T{quotient by}r,T{quotient by}r)" using prod_open_open_prod equiv_quo_is_top assms(1) by auto { fix S assume "S∈{⟨b,r``{b}⟩. b∈⋃T}``V×{⟨b,r``{b}⟩. b∈⋃T}``W" then obtain s1 s2 where S:"S=⟨s1,s2⟩""s1∈{⟨b,r``{b}⟩. b∈⋃T}``V""s2∈{⟨b,r``{b}⟩. b∈⋃T}``W" by blast then obtain t1 t2 where T:"⟨t1,s1⟩∈{⟨b,r``{b}⟩. b∈⋃T}""⟨t2,s2⟩∈{⟨b,r``{b}⟩. b∈⋃T}""t1∈V""t2∈W" using image_iff by auto then have "⟨t1,t2⟩∈V×W" by auto with VW(3) have "⟨t1,t2⟩∈{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}-``A" by auto then have "∃SS∈A. ⟨⟨t1,t2⟩,SS⟩∈{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}" using vimage_iff by auto then obtain SS where "SS∈A""⟨⟨t1,t2⟩,SS⟩∈{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}" by auto moreover from T VW(1,2) have "⟨t1,t2⟩∈⋃T×⋃T""⟨s1,s2⟩=⟨r``{t1},r``{t2}⟩" by auto with S(1) have "⟨⟨t1,t2⟩,S⟩∈{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}" by auto ultimately have "S∈A" using product_equiv_rel_fun unfolding Pi_def function_def by auto } then have sub:"{⟨b,r``{b}⟩. b∈⋃T}``V×{⟨b,r``{b}⟩. b∈⋃T}``W⊆A" by blast have "⟨c1,C1⟩∈{⟨b,r``{b}⟩. b∈⋃T}""⟨c2,C2⟩∈{⟨b,r``{b}⟩. b∈⋃T}" using CC2 CC1 by auto with `c1∈V``c2∈W` have "C1∈{⟨b,r``{b}⟩. b∈⋃T}``V""C2∈{⟨b,r``{b}⟩. b∈⋃T}``W" using image_iff by auto then have "CC∈{⟨b,r``{b}⟩. b∈⋃T}``V×{⟨b,r``{b}⟩. b∈⋃T}``W" using CC by auto with sub op have "∃OO∈ProductTopology(T{quotient by}r,T{quotient by}r). CC∈OO∧ OO⊆A" using exI[where x="{⟨b,r``{b}⟩. b∈⋃T}``V×{⟨b,r``{b}⟩. b∈⋃T}``W" and P="λOO. OO∈ProductTopology(T{quotient by}r,T{quotient by}r)∧ CC∈OO∧ OO⊆A"] by auto } then have "∀C∈A. ∃OO∈ProductTopology(T{quotient by}r,T{quotient by}r). C∈OO∧ OO⊆A" by auto then have "A∈ProductTopology(T{quotient by}r,T{quotient by}r)" using topology0.open_neigh_open unfolding topology0_def using Top_1_4_T1 equiv_quo_is_top assms by auto } then show "({quotient topology in}(((⋃T)//r)×((⋃T)//r)){by}{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}{from}(ProductTopology(T,T)))⊆ProductTopology(T{quotient by}r,T{quotient by}r)" by auto qed end