(* 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‹Suppose $T$ is a topology, $r$ is an equivalence relation on $X = \bigcup T$ and $P_r : X \rightarrow X/r$ maps an element of $X$ to its equivalence class $r\{x \}$. Then we can define a topology (on $X/r$) by taking the collection of those subsets $V$ of $X/r$ for which the inverse image by the projection $P_r$ is in $T$. This is the weakest topology on $X/r$ such that $P_r$ is continuous. In this theory we consider a seemingly more general situation where we start with a topology $T$ on $X=\bigcup T$ and a surjection $f:X\rightarrow Y$ and define a topology on $Y$ by taking those subsets $V$ of $Y$ for which the inverse image by the mapping $f$ is in $T$. Turns out that this construction is in a way equivalent to the previous one as the topology defined this way is homeomorphic to the topology defined by the equivalence relation $r_f$ on $X$ that relates two elements of $X$ if $f$ has the same value on them. › subsection‹Definition of quotient topology› text‹ In this section we define the quotient topology generated by a topology $T$ and a surjection $f:\bigcup T \rightarrow Y$, and show its basic properties. › text‹For a topological space $X=\bigcup T$ and a surjection $f:X\rightarrow Y$ we define ‹{quotient topology in} Y {by} f› as the collection of subsets of $Y$ whose inverse images by $f$ are open. › 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}" text‹Outside of the ‹topology0› context we will indicate also the generating topology and write ‹{quotient topology in} Y {by} f {from} X›. › abbreviation QuotientTopTop ("{quotient topology in}_{by}_{from}_") where "{quotient topology in} Y {by} f {from} 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 moreover { 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 } hence "(⋃A∈M. f-``(A)) = (⋃y∈⋃M. f-``{y})" by auto with A1 have A2: "f-``(⋃M)=⋃{f-`` A. A∈M}" by auto moreover { fix A assume "A∈M" with M have "f-``(A)∈T" by auto } hence "{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∩V)∈T" using topSpaceAssum invim_inter_inter_invim assms unfolding IsATopology_def 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 with assms(1) have "g-``(U)∈({quotient topology in} Y {by} h {from} τ⇩_{1})" using topology0.QuotientTop_def tau1_is_top 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‹The quotient projection $b\mapsto r\{ b\}$ is a function that maps the domain of the relation to the quotient. Note we do not need to assume that $r$ is an equivalence relation. › 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 text‹The quotient projection is a surjection. Again $r$ does not need to be an equivalence relation here › lemma quotient_proj_surj: shows "{⟨b,r``{b}⟩. b∈A}∈surj(A,A//r)" proof- { fix y assume "y∈A//r" then obtain x where "x∈A" "y=r``{x}" unfolding quotient_def by auto then have "∃x∈A. {⟨b,r``{b}⟩. b∈A}`(x) = y" using ZF_fun_from_tot_val1 by auto } then show ?thesis using quotient_proj_fun unfolding surj_def by auto qed text‹The inverse image of a subset $U$ of the quotient by the quotient projection is the union of $U$. Note since $U$ is a subset of $A/r$ it is a collection of equivalence classes.› 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 "y∈V" and "V∈U" by auto with assms have "y ∈ {⟨b,r``{b}⟩. b∈A}-``(U)" using EquivClass_1_L1 EquivClass_1_L2 by blast } thus "⋃U⊆{⟨b,r``{b}⟩. b∈A}-``U" by blast { fix y assume "y∈{⟨b,r``{b}⟩. b∈A}-``U" then have yy: "y∈{x∈A. r``{x}∈U}" by auto hence "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 } thus "{⟨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}" text‹Outside of the ‹topology0› context we need to indicate the original topology. › abbreviation EquivQuoTop ("_{quotient by}_") where "T {quotient by} 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}" with assms have "U∈{U∈Pow((⋃T)//r). ⋃U∈T}" using preim_equi_proj by auto } thus "{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}" with assms have "U∈{U∈Pow((⋃T)//r). {⟨b,r``{b}⟩. b∈⋃T}-``U∈T}" using preim_equi_proj by auto } thus "{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 text‹The quotient by an equivalence relation is indeed a topology. › 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‹The next theorem is the main result of this section: 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- from assms(1) have ff: "f:⋃T→Y" unfolding surj_def by auto from assms(2) show B: "equiv(⋃T,r)" unfolding equiv_def refl_def sym_def trans_def 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 assms(1) Y obtain A where A1: "A∈⋃T" "f`(A)=y" unfolding surj_def by blast with ff have A: "A ∈ f-``{y}" using func1_1_L15 by simp { fix t assume "t∈f-``{y}" with A eq have "t∈⋃T" "A∈⋃T" "⟨t,y⟩∈f" "⟨A,y⟩∈f" by auto then have "f`t=f`A" using apply_equality assms(1) unfolding surj_def by auto with assms(2) ‹t∈⋃T›‹A∈⋃T› have "⟨A,t⟩∈r" by auto then have "t∈r``{A}" using image_iff by auto } hence "f-``{y}⊆r``{A}" by auto moreover { fix t assume "t∈r``{A}" with assms(2) have un: "t∈⋃T" "A∈⋃T" and eq2: "f`(t)=f`(A)" using image_iff by simp_all from ff un have "⟨t,f`(t)⟩∈f" using func1_1_L5A(1) by simp with eq2 A1 un eq have "t∈f-``{y}" by simp } hence "r``{A}⊆f-``{y}" by auto ultimately have "f-``{y}=r``{A}" by auto with A1(1) have "f-``{y} ∈ (⋃T)//r" using A1(1) unfolding quotient_def by auto with Y have "B∈Y×(⋃T)//r" by auto } 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 P: "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 P 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 } hence 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 with A(1) have "b∈f-``({f`b})" 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 pr_fun have "{⟨b,r``{b}⟩. b∈⋃T}`b=r``{b}" using apply_equality by simp ultimately have "(g O f)`b={⟨b,r``{b}⟩. b∈⋃T}`b" by simp } hence reg: "∀b∈⋃T. (g O f)`(b)={⟨b,r``{b}⟩. b∈⋃T}`(b)" by blast moreover have compp: "g O f∈⋃T→(⋃T)//r" using comp_fun ff gg by blast moreover from compp pr_fun reg have feq: "(g O f)={⟨b,r``{b}⟩. b∈⋃T}" by (rule func_eq) 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 topSpaceAssum equiv_quo_is_top B unfolding two_top_spaces0_def by auto { fix x y assume T: "x∈Y" "y∈Y" "g`(x)=g`(y)" with assms(3) have "f``(f-``{x})=f``(f-``{y})" using apply_equality gg by simp with assms(1) T(1,2) have "x=y" using surj_image_vimage 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 with ff gg B have "g∈surj(Y,⋃(T{quotient by}r))" using comp_mem_surjD1 total_quo_equi 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 text‹The mapping $\langle b,c \rangle \mapsto \langle r\{ a\},r\{ b\}\rangle$ is a function that maps the product of the carrier by itself to the product of the quotients. Note $r$ does not have to be an equivalence relation. › 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 hence "{⟨⟨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 text‹The mapping $\langle b,c \rangle \mapsto \langle r\{ a\},r\{ b\}\rangle$ is a surjection of the product of the carrier by itself onto the carrier of the product topology. Again $r$ does not have to be an equivalence relation for this. › lemma (in topology0) prod_equiv_rel_surj: shows "{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}∈surj(⋃(T×⇩_{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 hence "⟨⟨m1,m2⟩,⟨r``{m1},r``{m2}⟩⟩∈{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}" by auto with fun have "{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}`⟨m1,m2⟩=⟨r``{m1},r``{m2}⟩" using apply_equality by auto with M(1) m(3,4) mm have "∃R∈(⋃T×⋃T). {⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}`(R) = M" by auto } ultimately show ?thesis unfolding surj_def using Top_1_4_T1(3) topSpaceAssum by auto qed text‹The product quotient projection (i.e. the mapping the mapping $\langle b,c \rangle \mapsto \langle r\{ a\},r\{ b\}\rangle$ is continuous.› lemma (in topology0) product_quo_fun: assumes "equiv(⋃T,r)" shows "IsContinuous(T×⇩_{t}T,({quotient by} r)×⇩_{t}({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 hence 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 with assms have cont: "IsContinuous(T,{quotient by}r,{⟨b,r``{b}⟩. b∈⋃T})" using quotient_func_cont quotient_proj_surj EquivQuo_def by auto with assms have tot: "⋃(T{quotient by}r) = (⋃T) // r" and top: "({quotient by}r) {is a topology}" using total_quo_equi equiv_quo_is_top by auto then have fun: "{⟨b,r``{b}⟩. b∈⋃T}:⋃T→⋃({quotient by}r)" using quotient_proj_fun by auto then have "two_top_spaces0(T,{quotient by}r,{⟨b,r``{b}⟩. b∈⋃T})" unfolding two_top_spaces0_def using topSpaceAssum top by auto with fun cont top IN show ?thesis using two_top_spaces0.product_cont_functions topSpaceAssum 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 "(({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} (T×⇩_{t}T))" proof let ?T⇩_{r}= "{quotient by} r" let ?R = "({quotient topology in} (((⋃T)//r)×((⋃T)//r)) {by} ({⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}) {from} (T×⇩_{t}T))" { fix A assume A: "A∈?T⇩_{r}×⇩_{t}?T⇩_{r}" with assms(1) have "{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}-``(A) ∈ T×⇩_{t}T" using product_quo_fun unfolding IsContinuous_def by auto moreover from A have "A⊆⋃((?T⇩_{r})×⇩_{t}(?T⇩_{r}))" by auto with assms(1) have "A∈Pow(((⋃T)//r)×((⋃T)//r))" using Top_1_4_T1(3) equiv_quo_is_top total_quo_equi by auto ultimately have "A∈?R" using topology0.QuotientTop_def Top_1_4_T1(1) topSpaceAssum prod_equiv_rel_surj unfolding topology0_def by auto } thus "(?T⇩_{r})×⇩_{t}(?T⇩_{r}) ⊆ ?R" by auto { fix A assume "A∈?R" with assms(1) have A: "A ⊆ ((⋃T)//r)×((⋃T)//r)" "{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}-``(A) ∈ T×⇩_{t}T" using topology0.QuotientTop_def Top_1_4_T1(1) topSpaceAssum prod_equiv_rel_surj unfolding topology0_def by auto { fix C assume "C∈A" with A(1) obtain C⇩_{1}C⇩_{2}where CC: "C=⟨C⇩_{1},C⇩_{2}⟩" "C⇩_{1}∈((⋃T)//r)" "C⇩_{2}∈((⋃T)//r)" by auto then obtain c⇩_{1}c⇩_{2}where CC1: "c⇩_{1}∈⋃T" "c⇩_{2}∈⋃T" and CC2: "C⇩_{1}=r``{c⇩_{1}}" "C⇩_{2}=r``{c⇩_{2}}" unfolding quotient_def by auto with ‹C∈A› CC have "⟨c⇩_{1},c⇩_{2}⟩∈{⟨⟨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) ∧ ⟨c⇩_{1},c⇩_{2}⟩ ∈ 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)" "c⇩_{1}∈V" "c⇩_{2}∈W" by blast let ?V⇩_{r}= "{⟨b,r``{b}⟩. b∈⋃T}``(V)" let ?W⇩_{r}= "{⟨b,r``{b}⟩. b∈⋃T}``(W)" from VW assms have P: "(?V⇩_{r}×?W⇩_{r}) ∈ (?T⇩_{r})×⇩_{t}(?T⇩_{r})" using prod_open_open_prod equiv_quo_is_top by auto { fix S assume "S∈(?V⇩_{r}×?W⇩_{r})" then obtain s⇩_{1}s⇩_{2}where S: "S=⟨s⇩_{1},s⇩_{2}⟩" "s⇩_{1}∈?V⇩_{r}" "s⇩_{2}∈?W⇩_{r}" by blast then obtain t⇩_{1}t⇩_{2}where T: "⟨t⇩_{1},s⇩_{1}⟩∈{⟨b,r``{b}⟩. b∈⋃T}" "⟨t⇩_{2},s⇩_{2}⟩∈{⟨b,r``{b}⟩. b∈⋃T}" "t⇩_{1}∈V" "t⇩_{2}∈W" using image_iff by auto with VW(3) have "∃S⇩_{0}∈A. ⟨⟨t⇩_{1},t⇩_{2}⟩,S⇩_{0}⟩∈{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}" using vimage_iff by auto then obtain S⇩_{0}where "S⇩_{0}∈A" and "⟨⟨t⇩_{1},t⇩_{2}⟩,S⇩_{0}⟩∈{⟨⟨b,c⟩,⟨r``{b},r``{c}⟩⟩. ⟨b,c⟩∈⋃T×⋃T}" by auto moreover from S(1) T VW(1,2) have "⟨⟨t⇩_{1},t⇩_{2}⟩,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 } hence sub: "?V⇩_{r}×?W⇩_{r}⊆ A" by blast from CC CC2 CC1 ‹c⇩_{1}∈V› ‹c⇩_{2}∈W› have "C ∈ ?V⇩_{r}×?W⇩_{r}" using image_iff by auto with P sub have "∃U∈(?T⇩_{r})×⇩_{t}(?T⇩_{r}). U⊆A ∧ C∈U " by (rule witness_exists1) } hence "∀C∈A. ∃U∈(?T⇩_{r})×⇩_{t}(?T⇩_{r}). C∈U ∧ U⊆A" by blast with assms(1) have "A∈(?T⇩_{r})×⇩_{t}(?T⇩_{r})" using topology0.open_neigh_open Top_1_4_T1 equiv_quo_is_top assms unfolding topology0_def by auto } thus "?R ⊆ (?T⇩_{r})×⇩_{t}(?T⇩_{r})" by auto qed end