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 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
}
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 P:"{⟨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 P 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