# IsarMathLib

## Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory Topology_ZF_8 imports Topology_ZF_6 EquivClass1
begin

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.

### Definition of quotient topology

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.

For a topological space $$X=\bigcup T$$ and a surjection $$f:X\rightarrow Y$$ we define $$\text{ quotient topology in } Y\text{ by } f$$ as the collection of subsets of $$Y$$ whose inverse images by $$f$$ are open.

definition (in topology0)

$$f\in \text{surj}(\bigcup T,Y) \Longrightarrow \text{ quotient topology in } Y\text{ by } f \equiv$$ $$\{U\in Pow(Y).\ f^{-1}U\in T\}$$

Outside of the topology0 context we will indicate also the generating topology and write $$\text{ quotient topology in } Y\text{ by } f\text{ from } X$$.

abbreviation

$$\text{ quotient topology in } Y\text{ by } f\text{ from } T \equiv topology0.\ \text{QuotientTop}(T,Y,f)$$

The quotient topology is indeed a topology.

theorem (in topology0) quotientTop_is_top:

assumes $$f\in \text{surj}(\bigcup T,Y)$$

shows $$(\text{ quotient topology in } Y\text{ by } f) \text{ is a topology }$$proof
have $$(\text{ quotient topology in } Y\text{ by } f)=\{U \in Pow(Y) .\ f^{-1}(U) \in T\}$$ using QuotientTop_def, assms
moreover {
fix $$M$$ $$x$$ $$B$$
assume M: $$M \subseteq \{U \in Pow(Y) .\ f^{-1}(U) \in T\}$$
then have $$\bigcup M\subseteq Y$$
moreover
have A1: $$f^{-1}(\bigcup M) = (\bigcup y\in (\bigcup M).\ f^{-1}\{y\})$$ using vimage_eq_UN
moreover {
fix $$A$$
assume $$A\in M$$
with M have $$A\in Pow(Y)$$, $$f^{-1}(A) \in T$$
have $$f^{-1}(A) = (\bigcup y\in A.\ f^{-1}\{y\})$$ using vimage_eq_UN
}
hence $$(\bigcup A\in M.\ f^{-1}(A)) = (\bigcup y\in \bigcup M.\ f^{-1}\{y\})$$
with A1 have A2: $$f^{-1}(\bigcup M)=\bigcup \{f^{-1} A.\ A\in M\}$$
moreover {
fix $$A$$
assume $$A\in M$$
with M have $$f^{-1}(A)\in T$$
}
hence $$\{f^{-1}(A).\ A\in M\}\subseteq T$$
then have $$(\bigcup \{f^{-1}(A).\ A\in M\})\in T$$ using topSpaceAssum unfolding IsATopology_def
with A2 have $$(f^{-1}(\bigcup M))\in T$$
ultimately have $$\bigcup M\in \{U\in Pow(Y).\ f^{-1}U\in T\}$$
} moreover {
fix $$U$$ $$V$$
assume $$U \in \{U\in Pow(Y).\ f^{-1}U\in T\}$$, $$V\in \{U\in Pow(Y).\ f^{-1}U\in T\}$$
then have $$U\in Pow(Y)$$, $$V\in Pow(Y)$$, $$f^{-1}U\in T$$, $$f^{-1}V\in T$$
then have $$f^{-1}(U\cap V)\in T$$ using topSpaceAssum, invim_inter_inter_invim, assms unfolding IsATopology_def, surj_def
with $$U\in Pow(Y)$$, $$V\in Pow(Y)$$ have $$U\cap V\in \{U\in Pow(Y).\ f^{-1}(U)\in T\}$$
} ultimately show $$thesis$$ using IsATopology_def
qed

The quotient function is continuous.

lemma (in topology0) quotient_func_cont:

assumes $$f\in \text{surj}(\bigcup T,Y)$$

shows $$\text{IsContinuous}(T,(\text{ quotient topology in } Y\text{ by } f),f)$$ unfolding IsContinuous_def using QuotientTop_def, assms

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\in \text{surj}(\bigcup \tau _1,Y)$$, $$g:Y\rightarrow \bigcup \tau _2$$, $$\text{IsContinuous}(\tau _1,\tau _2,g\circ h)$$

shows $$\text{IsContinuous}((\text{ quotient topology in } Y\text{ by } h\text{ from } \tau _1),\tau _2,g)$$proof
{
fix $$U$$
assume $$U\in \tau _2$$
with assms(3) have $$(g\circ h)^{-1}(U)\in \tau _1$$ unfolding IsContinuous_def
then have $$h^{-1}(g^{-1}(U))\in \tau _1$$ using vimage_comp
with assms(1) have $$g^{-1}(U)\in (\text{ quotient topology in } Y\text{ by } h\text{ from } \tau _1)$$ using QuotientTop_def, tau1_is_top, func1_1_L3, assms(2) unfolding topology0_def
}
then show $$thesis$$ unfolding IsContinuous_def
qed

The underlying set of the quotient topology is $$Y$$.

lemma (in topology0) total_quo_func:

assumes $$f\in \text{surj}(\bigcup T,Y)$$

shows $$(\bigcup (\text{ quotient topology in } Y\text{ by } f))=Y$$proof
from assms have $$f^{-1}Y=\bigcup T$$ using func1_1_L4 unfolding surj_def
moreover
have $$\bigcup T\in T$$ using topSpaceAssum unfolding IsATopology_def
ultimately have $$Y\in (\text{ quotient topology in }Y\{by\}f\{from\}T)$$ using QuotientTop_def, assms
then show $$thesis$$ using QuotientTop_def, assms
qed

### Quotient topologies from equivalence relations

In this section we will show that the quotient topologies come from an equivalence relation.

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 $$\{\langle b,r\{b\}\rangle .\ b\in A\}:A\rightarrow A//r$$ unfolding Pi_def, function_def, domain_def unfolding quotient_def

The quotient projection is a surjection. Again $$r$$ does not need to be an equivalence relation here

lemma quotient_proj_surj:

shows $$\{\langle b,r\{b\}\rangle .\ b\in A\}\in \text{surj}(A,A//r)$$proof
{
fix $$y$$
assume $$y\in A//r$$
then obtain $$x$$ where $$x\in A$$, $$y=r\{x\}$$ unfolding quotient_def
then have $$\exists x\in A.\ \{\langle b,r\{b\}\rangle .\ b\in A\}(x) = y$$ using ZF_fun_from_tot_val1
}
then show $$thesis$$ using quotient_proj_fun unfolding surj_def
qed

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\subseteq A//r$$, $$\text{equiv}(A,r)$$

shows $$\{\langle b,r\{b\}\rangle .\ b\in A\}^{-1}(U) = \bigcup U$$proof
{
fix $$y$$
assume $$y\in \bigcup U$$
then obtain $$V$$ where $$y\in V$$ and $$V\in U$$
with assms have $$y \in \{\langle b,r\{b\}\rangle .\ b\in A\}^{-1}(U)$$ using EquivClass_1_L1, EquivClass_1_L2
}
thus $$\bigcup U\subseteq \{\langle b,r\{b\}\rangle .\ b\in A\}^{-1}U$$
{
fix $$y$$
assume $$y\in \{\langle b,r\{b\}\rangle .\ b\in A\}^{-1}U$$
then have yy: $$y\in \{x\in A.\ r\{x\}\in U\}$$
hence $$r\{y\}\in U$$
moreover
from yy have $$y\in r\{y\}$$ using assms, equiv_class_self
ultimately have $$y\in \bigcup U$$
}
thus $$\{\langle b,r\{b\}\rangle .\ b\in A\}^{-1}U\subseteq \bigcup U$$
qed

Now we define what a quotient topology from an equivalence relation is:

definition (in topology0)

$$\text{equiv}(\bigcup T,r)\Longrightarrow (\text{ quotient by } r) \equiv \text{ quotient topology in } (\bigcup T)//r\text{ by } \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}$$

Outside of the topology0 context we need to indicate the original topology.

abbreviation

$$T \text{ quotient by } r \equiv topology0.\ \text{EquivQuo}(T,r)$$

First, another description of the topology (more intuitive):

theorem (in topology0) quotient_equiv_rel:

assumes $$\text{equiv}(\bigcup T,r)$$

shows $$(\text{ quotient by }r)=\{U\in Pow((\bigcup T)//r).\ \bigcup U\in T\}$$proof
have $$(\text{ quotient topology in }(\bigcup T)//r\{by}\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\})=$$ $$\{U\in Pow((\bigcup T)//r).\ \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}^{-1}U\in T\\}$$ using QuotientTop_def, quotient_proj_surj
moreover
have $$\{U\in Pow((\bigcup T)//r).\ \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}^{-1}U\in T\}=\{U\in Pow((\bigcup T)//r).\ \bigcup U\in T\}$$proof
{
fix $$U$$
assume $$U\in \{U\in Pow((\bigcup T)//r).\ \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}^{-1}U\in T\}$$
with assms have $$U\in \{U\in Pow((\bigcup T)//r).\ \bigcup U\in T\}$$ using preim_equi_proj
}
thus $$\{U\in Pow((\bigcup T)//r).\ \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}^{-1}U\in T\}\subseteq \{U\in Pow((\bigcup T)//r).\ \bigcup U\in T\}$$
{
fix $$U$$
assume $$U\in \{U\in Pow((\bigcup T)//r).\ \bigcup U\in T\}$$
with assms have $$U\in \{U\in Pow((\bigcup T)//r).\ \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}^{-1}U\in T\}$$ using preim_equi_proj
}
thus $$\{U\in Pow((\bigcup T)//r).\ \bigcup U\in T\}\subseteq \{U\in Pow((\bigcup T)//r).\ \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}^{-1}U\in T\}$$
qed
ultimately show $$thesis$$ using EquivQuo_def, assms
qed

We apply previous results to this topology.

theorem (in topology0) total_quo_equi:

assumes $$\text{equiv}(\bigcup T,r)$$

shows $$\bigcup (\text{ quotient by }r)=(\bigcup T)//r$$ using total_quo_func, quotient_proj_surj, EquivQuo_def, assms

The quotient by an equivalence relation is indeed a topology.

theorem (in topology0) equiv_quo_is_top:

assumes $$\text{equiv}(\bigcup T,r)$$

shows $$(\text{ quotient by }r)\text{ is a topology }$$ using quotientTop_is_top, quotient_proj_surj, EquivQuo_def, assms

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\in \text{surj}(\bigcup T,Y)$$

defines $$r\equiv \{\langle x,y\rangle \in \bigcup T\times \bigcup T.\ f(x)=f(y)\}$$

defines $$g\equiv \{\langle y,f^{-1}\{y\}\rangle .\ y\in Y\}$$

shows $$\text{equiv}(\bigcup T,r)$$ and $$\text{IsAhomeomorphism}((\text{ quotient topology in }Y\{by\}f),(\text{ quotient by }r),g)$$proof
from assms(1) have ff: $$f:\bigcup T\rightarrow Y$$ unfolding surj_def
from assms(2) show B: $$\text{equiv}(\bigcup T,r)$$ unfolding equiv_def, refl_def, sym_def, trans_def, r_def
have gg: $$g:Y\rightarrow ((\bigcup T)//r)$$proof
{
fix $$B$$
assume $$B\in g$$
then obtain $$y$$ where Y: $$y\in Y$$, $$B=\langle y,f^{-1}\{y\}\rangle$$ unfolding g_def
then have $$f^{-1}\{y\}\subseteq \bigcup T$$ using func1_1_L3, ff
then have eq: $$f^{-1}\{y\}=\{x\in \bigcup T.\ \langle x,y\rangle \in f\}$$ using vimage_iff
from assms(1), Y obtain $$A$$ where A1: $$A\in \bigcup T$$, $$f(A)=y$$ unfolding surj_def
with ff have A: $$A \in f^{-1}\{y\}$$ using func1_1_L15
{
fix $$t$$
assume $$t\in f^{-1}\{y\}$$
with A, eq have $$t\in \bigcup T$$, $$A\in \bigcup T$$, $$\langle t,y\rangle \in f$$, $$\langle A,y\rangle \in f$$
then have $$ft=fA$$ using apply_equality, assms(1) unfolding surj_def
with assms(2), $$t\in \bigcup T$$, $$A\in \bigcup T$$ have $$\langle A,t\rangle \in r$$
then have $$t\in r\{A\}$$ using image_iff
}
hence $$f^{-1}\{y\}\subseteq r\{A\}$$
moreover {
fix $$t$$
assume $$t\in r\{A\}$$
with assms(2) have un: $$t\in \bigcup T$$, $$A\in \bigcup T$$ and eq2: $$f(t)=f(A)$$ using image_iff
from ff, un have $$\langle t,f(t)\rangle \in f$$ using func1_1_L5A(1)
with eq2, A1, un, eq have $$t\in f^{-1}\{y\}$$
}
hence $$r\{A\}\subseteq f^{-1}\{y\}$$
ultimately have $$f^{-1}\{y\}=r\{A\}$$
with A1(1) have $$f^{-1}\{y\} \in (\bigcup T)//r$$ using A1(1) unfolding quotient_def
with Y have $$B\in Y\times (\bigcup T)//r$$
}
then show $$thesis$$ unfolding Pi_def, function_def, domain_def, g_def
qed
then have gg2: $$g:Y\rightarrow (\bigcup (\text{ quotient by }r))$$ using total_quo_equi, B
{
fix $$s$$
assume S: $$s\in (\text{ quotient topology in }Y\{by\}f)$$
then have $$s\in Pow(Y)$$ and P: $$f^{-1}(s)\in T$$ using QuotientTop_def, topSpaceAssum, assms(1)
have $$f^{-1}s=(\bigcup y\in s.\ f^{-1}\{y\})$$ using vimage_eq_UN
moreover
from $$s\in Pow(Y)$$ have $$\forall y\in s.\ \langle y,f^{-1}\{y\}\rangle \in g$$ unfolding g_def
then have $$\forall y\in s.\ gy=f^{-1}\{y\}$$ using apply_equality, gg
ultimately have $$f^{-1}s=(\bigcup y\in s.\ gy)$$
with P have $$(\bigcup y\in s.\ gy)\in T$$
moreover
from $$s\in Pow(Y)$$ have $$\forall y\in s.\ gy\in (\bigcup T)//r$$ using apply_type, gg
ultimately have $$\{gy.\ y\in s\}\in (\text{ quotient by }r)$$ using quotient_equiv_rel, B
with $$s\in Pow(Y)$$ have $$gs\in (\text{ quotient by }r)$$ using func_imagedef, gg
}
hence gopen: $$\forall s\in (\text{ quotient topology in }Y\{by\}f).\ gs\in (T\text{ quotient by }r)$$
have pr_fun: $$\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}:\bigcup T\rightarrow (\bigcup T)//r$$ using quotient_proj_fun
{
fix $$b$$
assume b: $$b\in \bigcup T$$
have bY: $$f(b)\in Y$$ using apply_funtype, ff, b
with b have com: $$(g\circ f)b=g(fb)$$ using comp_fun_apply, ff
from bY have pg: $$\langle fb,f^{-1}(\{fb\})\rangle \in g$$ unfolding g_def
then have $$g(fb) = f^{-1}(\{fb\})$$ using apply_equality, gg
with com have comeq: $$(g\circ f)b=f^{-1}(\{fb\})$$
from b have A: $$f\{b\}=\{fb\}$$, $$\{b\}\subseteq \bigcup T$$ using func_imagedef, ff
from A(2) have $$b \in f^{-1}(f \{b\})$$ using func1_1_L9, ff
with A(1) have $$b\in f^{-1}(\{fb\})$$
moreover
from pg have $$f^{-1}(\{fb\})\in (\bigcup T)//r$$ using gg unfolding Pi_def
ultimately have $$r\{b\}=f^{-1}(\{fb\})$$ using EquivClass_1_L2, B
then have $$(g\circ f)b=r\{b\}$$ using comeq
moreover
from b, pr_fun have $$\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}b=r\{b\}$$ using apply_equality
ultimately have $$(g\circ f)b=\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}b$$
}
hence reg: $$\forall b\in \bigcup T.\ (g\circ f)(b)=\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}(b)$$
moreover
have compp: $$g\circ f\in \bigcup T\rightarrow (\bigcup T)//r$$ using comp_fun, ff, gg
moreover
from compp, pr_fun, reg have feq: $$(g\circ f)=\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}$$ by (rule func_eq )
then have $$\text{IsContinuous}(T,\text{ quotient by }r,(g\circ f))$$ using quotient_func_cont, quotient_proj_surj, EquivQuo_def, topSpaceAssum, B
moreover
have $$(g\circ f):\bigcup T\rightarrow \bigcup (\text{ quotient by }r)$$ using comp_fun, ff, gg2
ultimately have gcont: $$\text{IsContinuous}(\text{ quotient topology in }Y\{by\}f,\text{ quotient by }r,g)$$ using cont_quotient_top, assms(1), gg2, topSpaceAssum, equiv_quo_is_top, B unfolding two_top_spaces0_def
{
fix $$x$$ $$y$$
assume T: $$x\in Y$$, $$y\in Y$$, $$g(x)=g(y)$$
with assms(3) have $$f(f^{-1}\{x\})=f(f^{-1}\{y\})$$ using apply_equality, gg
with assms(1), T(1,2) have $$x=y$$ using surj_image_vimage
}
with gg2 have $$g\in \text{inj}(Y,\bigcup (\text{ quotient by }r))$$ unfolding inj_def
moreover
have $$g\circ f\in \text{surj}(\bigcup T, (\bigcup T)//r)$$ using feq, quotient_proj_surj
with ff, gg, B have $$g\in \text{surj}(Y,\bigcup (T\text{ quotient by }r))$$ using comp_mem_surjD1, total_quo_equi
ultimately have $$g\in \text{bij}(\bigcup (\text{ quotient topology in }Y\{by\}f),\bigcup (\text{ quotient by }r))$$ unfolding bij_def using total_quo_func, assms(1)
with gcont, gopen show $$\text{IsAhomeomorphism}((\text{ quotient topology in }Y\{by\}f),(\text{ quotient by }r),g)$$ using bij_cont_open_homeo
qed

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 $$\{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}:(\bigcup T\times \bigcup T)\rightarrow ((\bigcup T)//r\times (\bigcup T)//r)$$proof
have $$\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}\in \bigcup T\rightarrow (\bigcup T)//r$$ using quotient_proj_fun
moreover
have $$\forall A\in \bigcup T.\ \langle A,r\{A\}\rangle \in \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}$$
ultimately have $$\forall A\in \bigcup T.\ \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}A=r\{A\}$$ using apply_equality
hence $$\{\langle \langle b,c\rangle ,r\{b\},r\{c\}\rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\} =$$ $$\{\langle \langle x,y\rangle ,\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}(x),\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}(y)\rangle .\ \langle x,y\rangle \in \bigcup T\times \bigcup T\}$$
then show $$thesis$$ using prod_fun, quotient_proj_fun
qed

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 $$\{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}\in \text{surj}(\bigcup (T\times _tT),((\bigcup T)//r\times (\bigcup T)//r))$$proof
have fun: $$\{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}:(\bigcup T\times \bigcup T)\rightarrow ((\bigcup T)//r\times (\bigcup T)//r)$$ using product_equiv_rel_fun
moreover {
fix $$M$$
assume $$M\in ((\bigcup T)//r\times (\bigcup T)//r)$$
then obtain $$M1$$ $$M2$$ where M: $$M=\langle M1,M2\rangle$$, $$M1\in (\bigcup T)//r$$, $$M2\in (\bigcup T)//r$$
then obtain $$m1$$ $$m2$$ where m: $$m1\in \bigcup T$$, $$m2\in \bigcup T$$, $$M1=r\{m1\}$$, $$M2=r\{m2\}$$ unfolding quotient_def
then have mm: $$\langle m1,m2\rangle \in (\bigcup T\times \bigcup T)$$
hence $$\langle \langle m1,m2\rangle ,\langle r\{m1\},r\{m2\}\rangle \rangle \in \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}$$
with fun have $$\{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}\langle m1,m2\rangle =\langle r\{m1\},r\{m2\}\rangle$$ using apply_equality
with M(1), m(3,4), mm have $$\exists R\in (\bigcup T\times \bigcup T).\ \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}(R) = M$$
} ultimately show $$thesis$$ unfolding surj_def using Top_1_4_T1(3), topSpaceAssum
qed

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 $$\text{equiv}(\bigcup T,r)$$

shows $$\text{IsContinuous}(T\times _tT,(\text{ quotient by } r)\times _t(\text{ quotient by } r),\{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\})$$proof
have $$\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}:\bigcup T\rightarrow (\bigcup T)//r$$ using quotient_proj_fun
moreover
have $$\forall A\in \bigcup T.\ \langle A,r\{A\}\rangle \in \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}$$
ultimately have $$\forall A\in \bigcup T.\ \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}A=r\{A\}$$ using apply_equality
hence IN: $$\{\langle \langle b,c\rangle ,r\{b\},r\{c\}\rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\} =$$ $$\{\langle \langle x,y\rangle ,\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}(x),\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}(y)\rangle .\ \langle x,y\rangle \in \bigcup T\times \bigcup T\}$$
with assms have cont: $$\text{IsContinuous}(T,\text{ quotient by }r,\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\})$$ using quotient_func_cont, quotient_proj_surj, EquivQuo_def
with assms have tot: $$\bigcup (T\text{ quotient by }r) = (\bigcup T) // r$$ and top: $$(\text{ quotient by }r) \text{ is a topology }$$ using total_quo_equi, equiv_quo_is_top
then have fun: $$\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}:\bigcup T\rightarrow \bigcup (\text{ quotient by }r)$$ using quotient_proj_fun
then have $$two\_top\_spaces0(T,\text{ quotient by }r,\{\langle b,r\{b\}\rangle .\ b\in \bigcup T\})$$ unfolding two_top_spaces0_def using topSpaceAssum, top
with fun, cont, top, IN show $$thesis$$ using product_cont_functions, topSpaceAssum
qed

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 $$\text{equiv}(\bigcup T,r)$$, $$\forall A\in T.\ \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}(A) \in (\text{ quotient by } r)$$

shows $$((\text{ quotient by } r)\times _t\text{ quotient by } r) =$$ $$(\text{ quotient topology in } (((\bigcup T)//r)\times ((\bigcup T)//r))\text{ by } (\{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\})\text{ from } (T\times _tT))$$proof
let $$T_r = \text{ quotient by } r$$
let $$R = (\text{ quotient topology in } (((\bigcup T)//r)\times ((\bigcup T)//r))\text{ by } (\{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\})\text{ from } (T\times _tT))$$
{
fix $$A$$
assume A: $$A\in T_r\times _tT_r$$
with assms(1) have $$\{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}^{-1}(A) \in T\times _tT$$ using product_quo_fun unfolding IsContinuous_def
moreover
from A have $$A\subseteq \bigcup ((T_r)\times _t(T_r))$$
with assms(1) have $$A\in Pow(((\bigcup T)//r)\times ((\bigcup T)//r))$$ using Top_1_4_T1(3), equiv_quo_is_top, total_quo_equi
ultimately have $$A\in R$$ using QuotientTop_def, Top_1_4_T1(1), topSpaceAssum, prod_equiv_rel_surj unfolding topology0_def
}
thus $$(T_r)\times _t(T_r) \subseteq R$$
{
fix $$A$$
assume $$A\in R$$
with assms(1) have A: $$A \subseteq ((\bigcup T)//r)\times ((\bigcup T)//r)$$, $$\{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}^{-1}(A) \in T\times _tT$$ using QuotientTop_def, Top_1_4_T1(1), topSpaceAssum, prod_equiv_rel_surj unfolding topology0_def
{
fix $$C$$
assume $$C\in A$$
with A(1) obtain $$C_1$$ $$C_2$$ where CC: $$C=\langle C_1,C_2\rangle$$, $$C_1\in ((\bigcup T)//r)$$, $$C_2\in ((\bigcup T)//r)$$
then obtain $$c_1$$ $$c_2$$ where CC1: $$c_1\in \bigcup T$$, $$c_2\in \bigcup T$$ and CC2: $$C_1=r\{c_1\}$$, $$C_2=r\{c_2\}$$ unfolding quotient_def
with $$C\in A$$, CC have $$\langle c_1,c_2\rangle \in \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}^{-1}(A)$$ using vimage_iff
with A(2) have $$\exists V W.\ V\in T \wedge W\in T \wedge V\times W \subseteq \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}^{-1}(A) \wedge \langle c_1,c_2\rangle \in V\times W$$ using prod_top_point_neighb, topSpaceAssum
then obtain $$V$$ $$W$$ where VW: $$V\in T$$, $$W\in T$$, $$V\times W \subseteq \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}^{-1}(A)$$, $$c_1\in V$$, $$c_2\in W$$
let $$V_r = \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}(V)$$
let $$W_r = \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}(W)$$
from VW, assms have P: $$(V_r\times W_r) \in (T_r)\times _t(T_r)$$ using prod_open_open_prod, equiv_quo_is_top
{
fix $$S$$
assume $$S\in (V_r\times W_r)$$
then obtain $$s_1$$ $$s_2$$ where S: $$S=\langle s_1,s_2\rangle$$, $$s_1\in V_r$$, $$s_2\in W_r$$
then obtain $$t_1$$ $$t_2$$ where T: $$\langle t_1,s_1\rangle \in \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}$$, $$\langle t_2,s_2\rangle \in \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}$$, $$t_1\in V$$, $$t_2\in W$$ using image_iff
with VW(3) have $$\exists S_0\in A.\ \langle \langle t_1,t_2\rangle ,S_0\rangle \in \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}$$ using vimage_iff
then obtain $$S_0$$ where $$S_0\in A$$ and $$\langle \langle t_1,t_2\rangle ,S_0\rangle \in \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}$$
moreover
from S(1), T, VW(1,2) have $$\langle \langle t_1,t_2\rangle ,S\rangle \in \{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}$$
ultimately have $$S\in A$$ using product_equiv_rel_fun unfolding Pi_def, function_def
}
hence sub: $$V_r\times W_r \subseteq A$$
from CC, CC2, CC1, $$c_1\in V$$, $$c_2\in W$$ have $$C \in V_r\times W_r$$ using image_iff
with P, sub have $$\exists U\in (T_r)\times _t(T_r).\ U\subseteq A \wedge C\in U$$ by (rule witness_exists1 )
}
hence $$\forall C\in A.\ \exists U\in (T_r)\times _t(T_r).\ C\in U \wedge U\subseteq A$$
with assms(1) have $$A\in (T_r)\times _t(T_r)$$ using open_neigh_open, Top_1_4_T1, equiv_quo_is_top, assms unfolding topology0_def
}
thus $$R \subseteq (T_r)\times _t(T_r)$$
qed
end
Definition of QuotientTop: $$f\in \text{surj}(\bigcup T,Y) \Longrightarrow \text{ quotient topology in } Y\text{ by } f \equiv$$ $$\{U\in Pow(Y).\ f^{-1}U\in T\}$$
Definition of IsATopology: $$T \text{ is a topology } \equiv ( \forall M \in Pow(T).\ \bigcup M \in T ) \wedge$$ $$( \forall U\in T.\ \forall V\in T.\ U\cap V \in T)$$
lemma invim_inter_inter_invim:

assumes $$f:X\rightarrow Y$$

shows $$f^{-1}(A\cap B) = f^{-1}(A) \cap f^{-1}(B)$$
Definition of IsContinuous: $$\text{IsContinuous}(\tau _1,\tau _2,f) \equiv (\forall U\in \tau _2.\ f^{-1}(U) \in \tau _1)$$
lemma vimage_comp: shows $$(r\circ s)^{-1}(A) = s^{-1}(r^{-1}(A))$$
lemma func1_1_L3:

assumes $$f:X\rightarrow Y$$

shows $$f^{-1}(D) \subseteq X$$
lemma func1_1_L4:

assumes $$f:X\rightarrow Y$$

shows $$f^{-1}(Y) = X$$
lemma ZF_fun_from_tot_val1:

assumes $$x\in X$$

shows $$\{\langle x,b(x)\rangle .\ x\in X\}(x)=b(x)$$
lemma quotient_proj_fun: shows $$\{\langle b,r\{b\}\rangle .\ b\in A\}:A\rightarrow A//r$$
lemma EquivClass_1_L1:

assumes $$\text{equiv}(A,r)$$ and $$C \in A//r$$ and $$x\in C$$

shows $$x\in A$$
lemma EquivClass_1_L2:

assumes $$\text{equiv}(A,r)$$, $$C \in A//r$$ and $$x\in C$$

shows $$r\{x\} = C$$
lemma quotient_proj_surj: shows $$\{\langle b,r\{b\}\rangle .\ b\in A\}\in \text{surj}(A,A//r)$$
lemma preim_equi_proj:

assumes $$U\subseteq A//r$$, $$\text{equiv}(A,r)$$

shows $$\{\langle b,r\{b\}\rangle .\ b\in A\}^{-1}(U) = \bigcup U$$
Definition of EquivQuo: $$\text{equiv}(\bigcup T,r)\Longrightarrow (\text{ quotient by } r) \equiv \text{ quotient topology in } (\bigcup T)//r\text{ by } \{\langle b,r\{b\}\rangle .\ b\in \bigcup T\}$$
lemma (in topology0) total_quo_func:

assumes $$f\in \text{surj}(\bigcup T,Y)$$

shows $$(\bigcup (\text{ quotient topology in } Y\text{ by } f))=Y$$
theorem (in topology0) quotientTop_is_top:

assumes $$f\in \text{surj}(\bigcup T,Y)$$

shows $$(\text{ quotient topology in } Y\text{ by } f) \text{ is a topology }$$
lemma func1_1_L15:

assumes $$f:X\rightarrow Y$$

shows $$f^{-1}(A) = \{x\in X.\ f(x) \in A\}$$
lemma func1_1_L5A:

assumes $$f:X\rightarrow Y$$, $$x\in X$$, $$y = f(x)$$

shows $$\langle x,y\rangle \in f$$, $$y \in \text{range}(f)$$
theorem (in topology0) total_quo_equi:

assumes $$\text{equiv}(\bigcup T,r)$$

shows $$\bigcup (\text{ quotient by }r)=(\bigcup T)//r$$
theorem (in topology0) quotient_equiv_rel:

assumes $$\text{equiv}(\bigcup T,r)$$

shows $$(\text{ quotient by }r)=\{U\in Pow((\bigcup T)//r).\ \bigcup U\in T\}$$
lemma func_imagedef:

assumes $$f:X\rightarrow Y$$ and $$A\subseteq X$$

shows $$f(A) = \{f(x).\ x \in A\}$$
lemma func1_1_L9:

assumes $$f:X\rightarrow Y$$ and $$A\subseteq X$$

shows $$A \subseteq f^{-1}(f(A))$$
lemma func_eq:

assumes $$f: X\rightarrow Y$$, $$g: X\rightarrow Z$$ and $$\forall x\in X.\ f(x) = g(x)$$

shows $$f = g$$
lemma (in topology0) quotient_func_cont:

assumes $$f\in \text{surj}(\bigcup T,Y)$$

shows $$\text{IsContinuous}(T,(\text{ quotient topology in } Y\text{ by } f),f)$$
theorem (in two_top_spaces0) cont_quotient_top:

assumes $$h\in \text{surj}(\bigcup \tau _1,Y)$$, $$g:Y\rightarrow \bigcup \tau _2$$, $$\text{IsContinuous}(\tau _1,\tau _2,g\circ h)$$

shows $$\text{IsContinuous}((\text{ quotient topology in } Y\text{ by } h\text{ from } \tau _1),\tau _2,g)$$
theorem (in topology0) equiv_quo_is_top:

assumes $$\text{equiv}(\bigcup T,r)$$

shows $$(\text{ quotient by }r)\text{ is a topology }$$
lemma surj_image_vimage:

assumes $$f \in \text{surj}(X,Y)$$ and $$A\subseteq Y$$

shows $$f(f^{-1}(A)) = A$$
lemma bij_cont_open_homeo:

assumes $$f \in \text{bij}(\bigcup T,\bigcup S)$$ and $$\text{IsContinuous}(T,S,f)$$ and $$\forall U\in T.\ f(U) \in S$$

shows $$\text{IsAhomeomorphism}(T,S,f)$$
lemma prod_fun:

assumes $$f:X_1\rightarrow X_2$$, $$g:X_3\rightarrow X_4$$

shows $$\{\langle \langle x,y\rangle ,\langle f(x),g(y)\rangle \rangle .\ \langle x,y\rangle \in X_1\times X_3\}:X_1\times X_3\rightarrow X_2\times X_4$$
lemma product_equiv_rel_fun: shows $$\{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}:(\bigcup T\times \bigcup T)\rightarrow ((\bigcup T)//r\times (\bigcup T)//r)$$
theorem Top_1_4_T1:

assumes $$T \text{ is a topology }$$, $$S \text{ is a topology }$$

shows $$(T\times _tS) \text{ is a topology }$$, $$\text{ProductCollection}(T,S) \text{ is a base for } (T\times _tS)$$, $$\bigcup (T\times _tS) = \bigcup T \times \bigcup S$$
theorem (in two_top_spaces0) product_cont_functions:

assumes $$f:X_1\rightarrow X_2$$, $$g:\bigcup \tau _3\rightarrow \bigcup \tau _4$$, $$\text{IsContinuous}(\tau _1,\tau _2,f)$$, $$\text{IsContinuous}(\tau _3,\tau _4,g)$$, $$\tau _4\text{ is a topology }$$, $$\tau _3\text{ is a topology }$$

shows $$\text{IsContinuous}( \text{ProductTopology}(\tau _1,\tau _3), \text{ProductTopology}(\tau _2,\tau _4),\{\langle \langle x,y\rangle ,\langle fx,gy\rangle \rangle .\ \langle x,y\rangle \in X_1\times \bigcup \tau _3\})$$
lemma (in topology0) product_quo_fun:

assumes $$\text{equiv}(\bigcup T,r)$$

shows $$\text{IsContinuous}(T\times _tT,(\text{ quotient by } r)\times _t(\text{ quotient by } r),\{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\})$$
theorem Top_1_4_T1:

assumes $$T \text{ is a topology }$$, $$S \text{ is a topology }$$

shows $$(T\times _tS) \text{ is a topology }$$, $$\text{ProductCollection}(T,S) \text{ is a base for } (T\times _tS)$$, $$\bigcup (T\times _tS) = \bigcup T \times \bigcup S$$
lemma (in topology0) prod_equiv_rel_surj: shows $$\{\langle \langle b,c\rangle ,\langle r\{b\},r\{c\}\rangle \rangle .\ \langle b,c\rangle \in \bigcup T\times \bigcup T\}\in \text{surj}(\bigcup (T\times _tT),((\bigcup T)//r\times (\bigcup T)//r))$$
lemma prod_top_point_neighb:

assumes $$T \text{ is a topology }$$, $$S \text{ is a topology }$$ and $$U \in \text{ProductTopology}(T,S)$$ and $$x \in U$$

shows $$\exists V W.\ V\in T \wedge W\in S \wedge V\times W \subseteq U \wedge x \in V\times W$$
lemma prod_open_open_prod:

assumes $$T \text{ is a topology }$$, $$S \text{ is a topology }$$ and $$U\in T$$, $$V\in S$$

shows $$U\times V \in \text{ProductTopology}(T,S)$$
lemma witness_exists1:

assumes $$x\in X$$, $$\phi (x)$$, $$\psi (x)$$

shows $$\exists x\in X.\ \phi (x) \wedge \psi (x)$$
lemma (in topology0) open_neigh_open:

assumes $$\forall x\in V.\ \exists U\in T.\ (x\in U \wedge U\subseteq V)$$

shows $$V\in T$$
theorem Top_1_4_T1:

assumes $$T \text{ is a topology }$$, $$S \text{ is a topology }$$

shows $$(T\times _tS) \text{ is a topology }$$, $$\text{ProductCollection}(T,S) \text{ is a base for } (T\times _tS)$$, $$\bigcup (T\times _tS) = \bigcup T \times \bigcup S$$