Theory Topology_ZF_8
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×⇩tT),((⋃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×⇩tT,({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×⇩tT))"
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×⇩tT))"
{ 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×⇩tT"
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×⇩tT"
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