IsarMathLib

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

theory Topology_ZF_3 imports Topology_ZF_2 FiniteSeq_ZF
begin

Topology_ZF_1 theory describes how we can define a topology on a product of two topological spaces. One way to generalize that is to construct topology for a cartesian product of \(n\) topological spaces. The cartesian product approach is somewhat inconvenient though. Another way to approach product topology on \(X^n\) is to model cartesian product as sets of sequences (of length \(n\)) of elements of \(X\). This means that having a topology on \(X\) we want to define a toplogy on the space \(n\rightarrow X\), where \(n\) is a natural number (recall that \(n = \{ 0,1,...,n-1\}\) in ZF). However, this in turn can be done more generally by defining a topology on any function space \(I\rightarrow X\), where \(I\) is any set of indices. This is what we do in this theory.

The base of the product topology

In this section we define the base of the product topology.

Suppose \(\mathcal{X} = I\rightarrow \bigcup T\) is a space of functions from some index set \(I\) to the carrier of a topology \(T\). Then take a finite collection of open sets \(W:N\rightarrow T\) indexed by \(N\subseteq I\). We can define a subset of \(\mathcal{X}\) that models the cartesian product of \(W\).

definition

\( \text{FinProd}(\mathcal{X} ,W) \equiv \{x\in \mathcal{X} .\ \forall i\in domain(W).\ x(i) \in W(i)\} \)

Now we define the base of the product topology as the collection of all finite products (in the sense defined above) of open sets.

definition

\( \text{ProductTopBase}(I,T) \equiv \bigcup N\in \text{FinPow}(I).\ \{ \text{FinProd}(I\rightarrow \bigcup T,W).\ W\in N\rightarrow T\} \)

Finally, we define the product topology on sequences. We use the ''Seq'' prefix although the definition is good for any index sets, not only natural numbers.

definition

\( \text{SeqProductTopology}(I,T) \equiv \{\bigcup B.\ B \in Pow( \text{ProductTopBase}(I,T))\} \)

Product topology base is closed with respect to intersections.

lemma prod_top_base_inter:

assumes A1: \( T \text{ is a topology } \) and A2: \( U \in \text{ProductTopBase}(I,T) \), \( V \in \text{ProductTopBase}(I,T) \)

shows \( U\cap V \in \text{ProductTopBase}(I,T) \)proof
let \( \mathcal{X} = I\rightarrow \bigcup T \)
from A2 obtain \( N_1 \) \( W_1 \) \( N_2 \) \( W_2 \) where I: \( N_1 \in \text{FinPow}(I) \), \( W_1\in N_1\rightarrow T \), \( U = \text{FinProd}(\mathcal{X} ,W_1) \) and II: \( N_2 \in \text{FinPow}(I) \), \( W_2\in N_2\rightarrow T \), \( V = \text{FinProd}(\mathcal{X} ,W_2) \) using ProductTopBase_def
let \( N_3 = N_1 \cup N_2 \)
let \( W_3 = \{\langle i,\text{if }i \in N_1-N_2\text{ then }W_1(i) \) \( \text{ else }\text{if }i \in N_2-N_1\text{ then } W_2(i) \) \( \text{ else }(W_1(i)) \cap (W_2(i))\rangle .\ i \in N_3\} \)
from A1, I, II have \( \forall i \in N_1 \cap N_2.\ (W_1(i) \cap W_2(i)) \in T \) using apply_funtype, IsATopology_def
moreover
from I, II have \( \forall i\in N_1-N_2.\ W_1(i) \in T \) and \( \forall i\in N_2-N_1.\ W_2(i) \in T \) using apply_funtype
ultimately have \( W_3:N_3\rightarrow T \) by (rule fun_union_overlap )
with I, II have \( \text{FinProd}(\mathcal{X} ,W_3) \in \text{ProductTopBase}(I,T) \) using union_finpow, ProductTopBase_def
moreover
have \( U\cap V = \text{FinProd}(\mathcal{X} ,W_3) \)proof
{
fix \( x \)
assume \( x\in U \) and \( x\in V \)
with \( U = \text{FinProd}(\mathcal{X} ,W_1) \), \( W_1\in N_1\rightarrow T \), and, \( V = \text{FinProd}(\mathcal{X} ,W_2) \), \( W_2\in N_2\rightarrow T \) have \( x\in \mathcal{X} \) and \( \forall i\in N_1.\ x(i) \in W_1(i) \) and \( \forall i\in N_2.\ x(i) \in W_2(i) \) using func1_1_L1, FinProd_def
with \( W_3:N_3\rightarrow T \), \( x\in \mathcal{X} \) have \( x \in \text{FinProd}(\mathcal{X} ,W_3) \) using ZF_fun_from_tot_val, func1_1_L1, FinProd_def
}
thus \( U\cap V \subseteq \text{FinProd}(\mathcal{X} ,W_3) \)
{
fix \( x \)
assume \( x \in \text{FinProd}(\mathcal{X} ,W_3) \)
with \( W_3:N_3\rightarrow T \) have \( x:I\rightarrow \bigcup T \) and III: \( \forall i\in N_3.\ x(i) \in W_3(i) \) using FinProd_def, func1_1_L1
{
fix \( i \)
assume \( i\in N_1 \)
with \( W_3:N_3\rightarrow T \) have \( W_3(i) \subseteq W_1(i) \) using ZF_fun_from_tot_val
with III, \( i\in N_1 \) have \( x(i) \in W_1(i) \)
}
with \( W_1\in N_1\rightarrow T \), \( x:I\rightarrow \bigcup T \), \( U = \text{FinProd}(\mathcal{X} ,W_1) \) have \( x \in U \) using func1_1_L1, FinProd_def
moreover {
fix \( i \)
assume \( i\in N_2 \)
with \( W_3:N_3\rightarrow T \) have \( W_3(i) \subseteq W_2(i) \) using ZF_fun_from_tot_val
with III, \( i\in N_2 \) have \( x(i) \in W_2(i) \)
}
with \( W_2\in N_2\rightarrow T \), \( x:I\rightarrow \bigcup T \), \( V = \text{FinProd}(\mathcal{X} ,W_2) \) have \( x\in V \) using func1_1_L1, FinProd_def
ultimately have \( x \in U\cap V \)
}
thus \( \text{FinProd}(\mathcal{X} ,W_3) \subseteq U\cap V \)
qed
ultimately show \( thesis \)
qed

In the next theorem we show the collection of sets defined above as \( \text{ProductTopBase}(\mathcal{X} ,T) \) satisfies the base condition. This is a condition, defined in Topology_ZF_1 that allows to claim that this collection is a base for some topology.

theorem prod_top_base_is_base:

assumes \( T \text{ is a topology } \)

shows \( \text{ProductTopBase}(I,T) \text{ satisfies the base condition } \) using assms, prod_top_base_inter, inter_closed_base

The (sequence) product topology is indeed a topology on the space of sequences. In the proof we are using the fact that \((\emptyset\rightarrow X) = \{\emptyset\}\).

theorem seq_prod_top_is_top:

assumes \( T \text{ is a topology } \)

shows \( \text{SeqProductTopology}(I,T) \text{ is a topology } \) and \( \text{ProductTopBase}(I,T) \text{ is a base for } \text{SeqProductTopology}(I,T) \) and \( \bigcup \text{SeqProductTopology}(I,T) = (I\rightarrow \bigcup T) \)proof
from assms show \( \text{SeqProductTopology}(I,T) \text{ is a topology } \) and I: \( \text{ProductTopBase}(I,T) \text{ is a base for } \text{SeqProductTopology}(I,T) \) using prod_top_base_is_base, SeqProductTopology_def, Top_1_2_T1
from I have \( \bigcup \text{SeqProductTopology}(I,T) = \bigcup \text{ProductTopBase}(I,T) \) using Top_1_2_L5
also
have \( \bigcup \text{ProductTopBase}(I,T) = (I\rightarrow \bigcup T) \)proof
show \( \bigcup \text{ProductTopBase}(I,T) \subseteq (I\rightarrow \bigcup T) \) using ProductTopBase_def, FinProd_def
have \( 0 \in \text{FinPow}(I) \) using empty_in_finpow
hence \( \{ \text{FinProd}(I\rightarrow \bigcup T,W).\ W\in 0\rightarrow T\} \subseteq (\bigcup N\in \text{FinPow}(I).\ \{ \text{FinProd}(I\rightarrow \bigcup T,W).\ W\in N\rightarrow T\}) \)
then show \( (I\rightarrow \bigcup T) \subseteq \bigcup \text{ProductTopBase}(I,T) \) using ProductTopBase_def, FinProd_def
qed
finally show \( \bigcup \text{SeqProductTopology}(I,T) = (I\rightarrow \bigcup T) \)
qed

Finite product of topologies

As a special case of the space of functions \(I\rightarrow X\) we can consider space of lists of elements of \(X\), i.e. space \(n\rightarrow X\), where \(n\) is a natural number (recall that in ZF set theory \(n=\{0,1,...,n-1\}\)). Such spaces model finite cartesian products \(X^n\) but are easier to deal with in formalized way (than the said products). This section discusses natural topology defined on \(n\rightarrow X\) where \(X\) is a topological space.

When the index set is finite, the definition of \( \text{ProductTopBase}(I,T) \) can be simplifed.

lemma fin_prod_def_nat:

assumes A1: \( n\in nat \) and A2: \( T \text{ is a topology } \)

shows \( \text{ProductTopBase}(n,T) = \{ \text{FinProd}(n\rightarrow \bigcup T,W).\ W\in n\rightarrow T\} \)proof
from A1 have \( n \in \text{FinPow}(n) \) using nat_finpow_nat, fin_finpow_self
then show \( \{ \text{FinProd}(n\rightarrow \bigcup T,W).\ W\in n\rightarrow T\} \subseteq \text{ProductTopBase}(n,T) \) using ProductTopBase_def
{
fix \( B \)
assume \( B \in \text{ProductTopBase}(n,T) \)
then obtain \( N \) \( W \) where \( N \in \text{FinPow}(n) \) and \( W \in N\rightarrow T \) and \( B = \text{FinProd}(n\rightarrow \bigcup T,W) \) using ProductTopBase_def
let \( W_n = \{\langle i,\text{if }i\in N\text{ then }W(i)\text{ else }\bigcup T\rangle .\ i\in n\} \)
from A2, \( N \in \text{FinPow}(n) \), \( W\in N\rightarrow T \) have \( \forall i\in n.\ (\text{if }i\in N\text{ then }W(i)\text{ else }\bigcup T) \in T \) using apply_funtype, FinPow_def, IsATopology_def
then have \( W_n:n\rightarrow T \) by (rule ZF_fun_from_total )
moreover
have \( B = \text{FinProd}(n\rightarrow \bigcup T,W_n) \)proof
{
fix \( x \)
assume \( x\in B \)
with \( B = \text{FinProd}(n\rightarrow \bigcup T,W) \) have \( x \in n\rightarrow \bigcup T \) using FinProd_def
moreover
have \( \forall i\in domain(W_n).\ x(i) \in W_n(i) \)proof
fix \( i \)
assume \( i \in domain(W_n) \)
with \( W_n:n\rightarrow T \) have \( i\in n \) using func1_1_L1
with \( x:n\rightarrow \bigcup T \) have \( x(i) \in \bigcup T \) using apply_funtype
with \( x\in B \), \( B = \text{FinProd}(n\rightarrow \bigcup T,W) \), \( W \in N\rightarrow T \), \( W_n:n\rightarrow T \), \( i\in n \) show \( x(i) \in W_n(i) \) using func1_1_L1, FinProd_def, ZF_fun_from_tot_val
qed
ultimately have \( x \in \text{FinProd}(n\rightarrow \bigcup T,W_n) \) using FinProd_def
}
thus \( B \subseteq \text{FinProd}(n\rightarrow \bigcup T,W_n) \)
next
{
fix \( x \)
assume \( x \in \text{FinProd}(n\rightarrow \bigcup T,W_n) \)
then have \( x \in n\rightarrow \bigcup T \) and \( \forall i\in domain(W_n).\ x(i) \in W_n(i) \) using FinProd_def
with \( W_n:n\rightarrow T \), and, \( N \in \text{FinPow}(n) \) have \( \forall i\in N.\ x(i) \in W_n(i) \) using func1_1_L1, FinPow_def
moreover
from \( W_n:n\rightarrow T \), and, \( N \in \text{FinPow}(n) \) have \( \forall i\in N.\ W_n(i) = W(i) \) using ZF_fun_from_tot_val, FinPow_def
ultimately have \( \forall i\in N.\ x(i) \in W(i) \)
with \( W \in N\rightarrow T \), \( x \in n\rightarrow \bigcup T \), \( B = \text{FinProd}(n\rightarrow \bigcup T,W) \) have \( x\in B \) using func1_1_L1, FinProd_def
}
thus \( \text{FinProd}(n\rightarrow \bigcup T,W_n) \subseteq B \)
qed
ultimately have \( B \in \{ \text{FinProd}(n\rightarrow \bigcup T,W).\ W\in n\rightarrow T\} \)
}
thus \( \text{ProductTopBase}(n,T) \subseteq \{ \text{FinProd}(n\rightarrow \bigcup T,W).\ W\in n\rightarrow T\} \)
qed

A technical lemma providing a formula for finite product on one topological space.

lemma single_top_prod:

assumes A1: \( W:1\rightarrow \tau \)

shows \( \text{FinProd}(1\rightarrow \bigcup \tau ,W) = \{ \{\langle 0,y\rangle \}.\ y \in W(0)\} \)proof
have \( 1 = \{0\} \)
from A1 have \( domain(W) = \{0\} \) using func1_1_L1
then have \( \text{FinProd}(1\rightarrow \bigcup \tau ,W) = \{x \in 1\rightarrow \bigcup \tau .\ x(0) \in W(0)\} \) using FinProd_def
also
have \( \{x \in 1\rightarrow \bigcup \tau .\ x(0) \in W(0)\} = \{ \{\langle 0,y\rangle \}.\ y \in W(0)\} \)proof
from \( 1 = \{0\} \) show \( \{x \in 1\rightarrow \bigcup \tau .\ x(0) \in W(0)\} \subseteq \{ \{\langle 0,y\rangle \}.\ y \in W(0)\} \) using func_singleton_pair
{
fix \( x \)
assume \( x \in \{ \{\langle 0,y\rangle \}.\ y \in W(0)\} \)
then obtain \( y \) where \( x = \{\langle 0,y\rangle \} \) and II: \( y \in W(0) \)
with A1 have \( y \in \bigcup \tau \) using apply_funtype
with \( x = \{\langle 0,y\rangle \} \), \( 1 = \{0\} \) have \( x:1\rightarrow \bigcup \tau \) using pair_func_singleton
with \( x = \{\langle 0,y\rangle \} \), II have \( x \in \{x \in 1\rightarrow \bigcup \tau .\ x(0) \in W(0)\} \) using pair_val
}
thus \( \{ \{\langle 0,y\rangle \}.\ y \in W(0)\} \subseteq \{x \in 1\rightarrow \bigcup \tau .\ x(0) \in W(0)\} \)
qed
finally show \( thesis \)
qed

Intuitively, the topological space of singleton lists valued in \(X\) is the same as \(X\). However, each element of this space is a list of length one, i.e a set consisting of a pair \(\langle 0, x\rangle\) where \(x\) is an element of \(X\). The next lemma provides a formula for the product topology in the corner case when we have only one factor and shows that the product topology of one space is essentially the same as the space.

lemma singleton_prod_top:

assumes A1: \( \tau \text{ is a topology } \)

shows \( \text{SeqProductTopology}(1,\tau ) = \{ \{ \{\langle 0,y\rangle \}.\ y\in U \}.\ U\in \tau \} \) and \( \text{IsAhomeomorphism}(\tau , \text{SeqProductTopology}(1,\tau ),\{\langle y,\{\langle 0,y\rangle \}\rangle .\ y \in \bigcup \tau \}) \)proof
have \( \{0\} = 1 \)
let \( b = \{\langle y,\{\langle 0,y\rangle \}\rangle .\ y \in \bigcup \tau \} \)
have \( b \in \text{bij}(\bigcup \tau ,1\rightarrow \bigcup \tau ) \) using list_singleton_bij
with A1 have \( \{b(U).\ U\in \tau \} \text{ is a topology } \) and \( \text{IsAhomeomorphism}(\tau , \{b(U).\ U\in \tau \},b) \) using bij_induced_top
moreover
have \( \forall U\in \tau .\ b(U) = \{ \{\langle 0,y\rangle \}.\ y\in U \} \)proof
fix \( U \)
assume \( U\in \tau \)
from \( b \in \text{bij}(\bigcup \tau ,1\rightarrow \bigcup \tau ) \) have \( b:\bigcup \tau \rightarrow (1\rightarrow \bigcup \tau ) \) using bij_def, inj_def
{
fix \( y \)
assume \( y \in \bigcup \tau \)
with \( b:\bigcup \tau \rightarrow (1\rightarrow \bigcup \tau ) \) have \( b(y) = \{\langle 0,y\rangle \} \) using ZF_fun_from_tot_val
}
hence \( \forall y \in \bigcup \tau .\ b(y) = \{\langle 0,y\rangle \} \)
with \( U\in \tau \), \( b:\bigcup \tau \rightarrow (1\rightarrow \bigcup \tau ) \) show \( b(U) = \{ \{\langle 0,y\rangle \}.\ y\in U \} \) using func_imagedef
qed
moreover
have \( \text{ProductTopBase}(1,\tau ) = \{ \{ \{\langle 0,y\rangle \}.\ y\in U \}.\ U\in \tau \} \)proof
{
fix \( V \)
assume \( V \in \text{ProductTopBase}(1,\tau ) \)
with A1 obtain \( W \) where \( W:1\rightarrow \tau \) and \( V = \text{FinProd}(1\rightarrow \bigcup \tau ,W) \) using fin_prod_def_nat
then have \( V \in \{ \{ \{\langle 0,y\rangle \}.\ y\in U \}.\ U\in \tau \} \) using apply_funtype, single_top_prod
}
thus \( \text{ProductTopBase}(1,\tau ) \subseteq \{ \{ \{\langle 0,y\rangle \}.\ y\in U \}.\ U\in \tau \} \)
{
fix \( V \)
assume \( V \in \{ \{ \{\langle 0,y\rangle \}.\ y\in U \}.\ U\in \tau \} \)
then obtain \( U \) where \( U\in \tau \) and \( V = \{ \{\langle 0,y\rangle \}.\ y\in U \} \)
let \( W = \{\langle 0,U\rangle \} \)
from \( U\in \tau \) have \( W:\{0\}\rightarrow \tau \) using pair_func_singleton
with \( \{0\} = 1 \) have \( W:1\rightarrow \tau \) and \( W(0) = U \) using pair_val
with \( V = \{ \{\langle 0,y\rangle \}.\ y\in U \} \) have \( V = \text{FinProd}(1\rightarrow \bigcup \tau ,W) \) using single_top_prod
with A1, \( W:1\rightarrow \tau \) have \( V \in \text{ProductTopBase}(1,\tau ) \) using fin_prod_def_nat
}
thus \( \{ \{ \{\langle 0,y\rangle \}.\ y\in U \}.\ U\in \tau \} \subseteq \text{ProductTopBase}(1,\tau ) \)
qed
ultimately have I: \( \text{ProductTopBase}(1,\tau ) \text{ is a topology } \) and II: \( \text{IsAhomeomorphism}(\tau , \text{ProductTopBase}(1,\tau ),b) \)
from A1 have \( \text{ProductTopBase}(1,\tau ) \text{ is a base for } \text{SeqProductTopology}(1,\tau ) \) using seq_prod_top_is_top
with I have \( \text{ProductTopBase}(1,\tau ) = \text{SeqProductTopology}(1,\tau ) \) by (rule base_topology )
with \( \text{ProductTopBase}(1,\tau ) = \{ \{ \{\langle 0,y\rangle \}.\ y\in U \}.\ U\in \tau \} \), II show \( \text{SeqProductTopology}(1,\tau ) = \{ \{ \{\langle 0,y\rangle \}.\ y\in U \}.\ U\in \tau \} \) and \( \text{IsAhomeomorphism}(\tau , \text{SeqProductTopology}(1,\tau ),\{\langle y,\{\langle 0,y\rangle \}\rangle .\ y \in \bigcup \tau \}) \)
qed

A special corner case of finite_top_prod_homeo: a space \(X\) is homeomorphic to the space of one element lists of \(X\).

theorem singleton_prod_top1:

assumes A1: \( \tau \text{ is a topology } \)

shows \( \text{IsAhomeomorphism}( \text{SeqProductTopology}(1,\tau ),\tau ,\{\langle x,x(0)\rangle .\ x\in 1\rightarrow \bigcup \tau \}) \)proof
have \( \{\langle x,x(0)\rangle .\ x\in 1\rightarrow \bigcup \tau \} = converse(\{\langle y,\{\langle 0,y\rangle \}\rangle .\ y\in \bigcup \tau \}) \) using list_singleton_bij
with A1 show \( thesis \) using singleton_prod_top, homeo_inv
qed

A technical lemma describing the carrier of a (cartesian) product topology of the (sequence) product topology of \(n\) copies of topology \(\tau\) and another copy of \(\tau\).

lemma finite_prod_top:

assumes \( \tau \text{ is a topology } \) and \( T = \text{SeqProductTopology}(n,\tau ) \)

shows \( (\bigcup \text{ProductTopology}(T,\tau )) = (n\rightarrow \bigcup \tau )\times \bigcup \tau \) using assms, Top_1_4_T1, seq_prod_top_is_top

If \(U\) is a set from the base of \(X^n\) and \(V\) is open in \(X\), then \(U\times V\) is in the base of \(X^{n+1}\). The next lemma is an analogue of this fact for the function space approach.

lemma finite_prod_succ_base:

assumes A1: \( \tau \text{ is a topology } \) and A2: \( n \in nat \) and A3: \( U \in \text{ProductTopBase}(n,\tau ) \) and A4: \( V\in \tau \)

shows \( \{x \in succ(n)\rightarrow \bigcup \tau .\ \text{Init}(x) \in U \wedge x(n) \in V\} \in \text{ProductTopBase}(succ(n),\tau ) \)proof
let \( B = \{x \in succ(n)\rightarrow \bigcup \tau .\ \text{Init}(x) \in U \wedge x(n) \in V\} \)
from A1, A2 have \( \text{ProductTopBase}(n,\tau ) = \{ \text{FinProd}(n\rightarrow \bigcup \tau ,W).\ W\in n\rightarrow \tau \} \) using fin_prod_def_nat
with A3 obtain \( W_U \) where \( W_U:n\rightarrow \tau \) and \( U = \text{FinProd}(n\rightarrow \bigcup \tau ,W_U) \)
let \( W = \text{Append}(W_U,V) \)
from A4, and, \( W_U:n\rightarrow \tau \) have \( W:succ(n)\rightarrow \tau \) using append_props
moreover
have \( B = \text{FinProd}(succ(n)\rightarrow \bigcup \tau ,W) \)proof
{
fix \( x \)
assume \( x\in B \)
with \( W:succ(n)\rightarrow \tau \) have \( x \in succ(n)\rightarrow \bigcup \tau \) and \( domain(W) = succ(n) \) using func1_1_L1
moreover
from A2, A4, \( x\in B \), \( U = \text{FinProd}(n\rightarrow \bigcup \tau ,W_U) \), \( W_U:n\rightarrow \tau \), \( x \in succ(n)\rightarrow \bigcup \tau \) have \( \forall i\in succ(n).\ x(i) \in W(i) \) using func1_1_L1, FinProd_def, init_props, append_props
ultimately have \( x \in \text{FinProd}(succ(n)\rightarrow \bigcup \tau ,W) \) using FinProd_def
}
thus \( B \subseteq \text{FinProd}(succ(n)\rightarrow \bigcup \tau ,W) \)
next
{
fix \( x \)
assume \( x \in \text{FinProd}(succ(n)\rightarrow \bigcup \tau ,W) \)
then have \( x:succ(n)\rightarrow \bigcup \tau \) and I: \( \forall i \in domain(W).\ x(i) \in W(i) \) using FinProd_def
moreover
have \( \text{Init}(x) \in U \)proof
from A2, and, \( x:succ(n)\rightarrow \bigcup \tau \) have \( \text{Init}(x):n\rightarrow \bigcup \tau \) using init_props
moreover
have \( \forall i\in domain(W_U).\ \text{Init}(x)(i) \in W_U(i) \)proof
from A2, \( x \in \text{FinProd}(succ(n)\rightarrow \bigcup \tau ,W) \), \( W:succ(n)\rightarrow \tau \) have \( \forall i\in n.\ x(i) \in W(i) \) using FinProd_def, func1_1_L1
moreover
from A2, \( x: succ(n)\rightarrow \bigcup \tau \) have \( \forall i\in n.\ \text{Init}(x)(i) = x(i) \) using init_props
moreover
from A4, and, \( W_U:n\rightarrow \tau \) have \( \forall i\in n.\ W(i) = W_U(i) \) using append_props
ultimately have \( \forall i\in n.\ \text{Init}(x)(i) \in W_U(i) \)
with \( W_U:n\rightarrow \tau \) show \( thesis \) using func1_1_L1
qed
ultimately have \( \text{Init}(x) \in \text{FinProd}(n\rightarrow \bigcup \tau ,W_U) \) using FinProd_def
with \( U = \text{FinProd}(n\rightarrow \bigcup \tau ,W_U) \) show \( thesis \)
qed
moreover
have \( x(n) \in V \)proof
from \( W:succ(n)\rightarrow \tau \), I have \( x(n) \in W(n) \) using func1_1_L1
moreover
from A4, \( W_U:n\rightarrow \tau \) have \( W(n) = V \) using append_props
ultimately show \( thesis \)
qed
ultimately have \( x\in B \)
}
thus \( \text{FinProd}(succ(n)\rightarrow \bigcup \tau ,W) \subseteq B \)
qed
moreover
from A1, A2 have \( \text{ProductTopBase}(succ(n),\tau ) = \{ \text{FinProd}(succ(n)\rightarrow \bigcup \tau ,W).\ W\in succ(n)\rightarrow \tau \} \) using fin_prod_def_nat
ultimately show \( thesis \)
qed

If \(U\) is open in \(X^n\) and \(V\) is open in \(X\), then \(U\times V\) is open in \(X^{n+1}\). The next lemma is an analogue of this fact for the function space approach.

lemma finite_prod_succ:

assumes A1: \( \tau \text{ is a topology } \) and A2: \( n \in nat \) and A3: \( U \in \text{SeqProductTopology}(n,\tau ) \) and A4: \( V\in \tau \)

shows \( \{x \in succ(n)\rightarrow \bigcup \tau .\ \text{Init}(x) \in U \wedge x(n) \in V\} \in \text{SeqProductTopology}(succ(n),\tau ) \)proof
from A1 have \( \text{ProductTopBase}(n,\tau ) \text{ is a base for } \text{SeqProductTopology}(n,\tau ) \) and I: \( \text{ProductTopBase}(succ(n),\tau ) \text{ is a base for } \text{SeqProductTopology}(succ(n),\tau ) \) and II: \( \text{SeqProductTopology}(succ(n),\tau ) \text{ is a topology } \) using seq_prod_top_is_top
with A3 have \( \exists \mathcal{B} \in Pow( \text{ProductTopBase}(n,\tau )).\ U = \bigcup \mathcal{B} \) using Top_1_2_L1
then obtain \( \mathcal{B} \) where \( \mathcal{B} \subseteq \text{ProductTopBase}(n,\tau ) \) and \( U = \bigcup \mathcal{B} \)
then have \( \{x:succ(n)\rightarrow \bigcup \tau .\ \text{Init}(x) \in U \wedge x(n) \in V\} = (\bigcup B\in \mathcal{B} .\ \{x:succ(n)\rightarrow \bigcup \tau .\ \text{Init}(x) \in B \wedge x(n) \in V\}) \)
moreover
from A1, A2, A4, \( \mathcal{B} \subseteq \text{ProductTopBase}(n,\tau ) \) have \( \forall B\in \mathcal{B} .\ (\{x:succ(n)\rightarrow \bigcup \tau .\ \text{Init}(x) \in B \wedge x(n) \in V\} \in \text{ProductTopBase}(succ(n),\tau )) \) using finite_prod_succ_base
with I, II have \( (\bigcup B\in \mathcal{B} .\ \{x:succ(n)\rightarrow \bigcup \tau .\ \text{Init}(x) \in B \wedge x(n) \in V\}) \in \text{SeqProductTopology}(succ(n),\tau ) \) using base_sets_open, union_indexed_open
ultimately show \( thesis \)
qed

In the Topology_ZF_2 theory we define product topology of two topological spaces. The next lemma explains in what sense the topology on finite lists of length \(n\) of elements of topological space \(X\) can be thought as a model of the product topology on the cartesian product of \(n\) copies of that space. Namely, we show that the space of lists of length \(n+1\) of elements of \(X\) is homeomorphic to the product topology (as defined in Topology_ZF_2) of two spaces: the space of lists of length \(n\) and \(X\). Recall that if \(\mathcal{B}\) is a base (i.e. satisfies the base condition), then the collection \(\{\bigcup B| B \in Pow(\mathcal{B})\}\) is a topology (generated by \(\mathcal{B}\)).

theorem finite_top_prod_homeo:

assumes A1: \( \tau \text{ is a topology } \) and A2: \( n \in nat \) and A3: \( f = \{\langle x,\langle \text{Init}(x),x(n)\rangle \rangle .\ x \in succ(n)\rightarrow \bigcup \tau \} \) and A4: \( T = \text{SeqProductTopology}(n,\tau ) \) and A5: \( S = \text{SeqProductTopology}(succ(n),\tau ) \)

shows \( \text{IsAhomeomorphism}(S, \text{ProductTopology}(T,\tau ),f) \)proof
let \( C = \text{ProductCollection}(T,\tau ) \)
let \( B = \text{ProductTopBase}(succ(n),\tau ) \)
from A1, A4 have \( T \text{ is a topology } \) using seq_prod_top_is_top
with A1, A5 have \( S \text{ is a topology } \) and \( \text{ProductTopology}(T,\tau ) \text{ is a topology } \) using seq_prod_top_is_top, Top_1_4_T1
moreover
from assms have \( f \in \text{bij}(\bigcup S,\bigcup \text{ProductTopology}(T,\tau )) \) using lists_cart_prod, seq_prod_top_is_top, Top_1_4_T1
then have \( f: \bigcup S\rightarrow \bigcup \text{ProductTopology}(T,\tau ) \) using bij_is_fun
ultimately have \( two\_top\_spaces0(S, \text{ProductTopology}(T,\tau ),f) \) using two_top_spaces0_def
moreover
note \( f \in \text{bij}(\bigcup S,\bigcup \text{ProductTopology}(T,\tau )) \)
moreover
from A1, A5 have \( B \text{ is a base for } S \) using seq_prod_top_is_top
moreover
from A1, \( T \text{ is a topology } \) have \( C \text{ is a base for } \text{ProductTopology}(T,\tau ) \) using Top_1_4_T1
moreover
have \( \forall W\in C.\ f^{-1}(W) \in S \)proof
fix \( W \)
assume \( W\in C \)
then obtain \( U \) \( V \) where \( U\in T \), \( V\in \tau \) and \( W = U\times V \) using ProductCollection_def
from A1, A5, \( f: \bigcup S\rightarrow \bigcup \text{ProductTopology}(T,\tau ) \) have \( f: (succ(n)\rightarrow \bigcup \tau )\rightarrow \bigcup \text{ProductTopology}(T,\tau ) \) using seq_prod_top_is_top
with assms, \( W = U\times V \), \( U\in T \), \( V\in \tau \) show \( f^{-1}(W) \in S \) using ZF_fun_from_tot_val, func1_1_L15, finite_prod_succ
qed
moreover
have \( \forall V\in B.\ f(V) \in \text{ProductTopology}(T,\tau ) \)proof
fix \( V \)
assume \( V\in B \)
with A1, A2 obtain \( W_V \) where \( W_V \in succ(n)\rightarrow \tau \) and \( V = \text{FinProd}(succ(n)\rightarrow \bigcup \tau ,W_V) \) using fin_prod_def_nat
let \( U = \text{FinProd}(n\rightarrow \bigcup \tau , \text{Init}(W_V)) \)
let \( W = W_V(n) \)
have \( U \in T \)proof
from A1, A2, \( W_V \in succ(n)\rightarrow \tau \) have \( U \in \text{ProductTopBase}(n,\tau ) \) using fin_prod_def_nat, init_props
with A1, A4 show \( thesis \) using seq_prod_top_is_top, base_sets_open
qed
from A1, \( W_V \in succ(n)\rightarrow \tau \), \( T \text{ is a topology } \), \( U \in T \) have \( U\times W \in \text{ProductTopology}(T,\tau ) \) using apply_funtype, prod_open_open_prod
moreover
have \( f(V) = U\times W \)proof
from A2, \( W_V: succ(n)\rightarrow \tau \) have \( \text{Init}(W_V): n\rightarrow \tau \) and III: \( \forall k\in n.\ \text{Init}(W_V)(k) = W_V(k) \) using init_props
then have \( domain( \text{Init}(W_V)) = n \) using func1_1_L1
have \( f(V) = \{\langle \text{Init}(x),x(n)\rangle .\ x\in V\} \)proof
have \( f(V) = \{f(x).\ x\in V\} \)proof
from A1, A5 have \( B \text{ is a base for } S \) using seq_prod_top_is_top
with \( V\in B \) have \( V \subseteq \bigcup S \) using IsAbaseFor_def
with \( f: \bigcup S\rightarrow \bigcup \text{ProductTopology}(T,\tau ) \) show \( thesis \) using func_imagedef
qed
moreover
have \( \forall x\in V.\ f(x) = \langle \text{Init}(x),x(n)\rangle \)proof
from A1, A3, A5, \( V = \text{FinProd}(succ(n)\rightarrow \bigcup \tau ,W_V) \) have \( V \subseteq \bigcup S \) and fdef: \( f = \{\langle x,\langle \text{Init}(x),x(n)\rangle \rangle .\ x \in \bigcup S\} \) using seq_prod_top_is_top, FinProd_def
from \( f: \bigcup S\rightarrow \bigcup \text{ProductTopology}(T,\tau ) \), fdef have \( \forall x \in \bigcup S.\ f(x) = \langle \text{Init}(x),x(n)\rangle \) by (rule ZF_fun_from_tot_val0 )
with \( V \subseteq \bigcup S \) show \( thesis \)
qed
ultimately show \( thesis \)
qed
also
have \( \{\langle \text{Init}(x),x(n)\rangle .\ x\in V\} = U\times W \)proof
{
fix \( y \)
assume \( y \in \{\langle \text{Init}(x),x(n)\rangle .\ x\in V\} \)
then obtain \( x \) where I: \( y = \langle \text{Init}(x),x(n)\rangle \) and \( x\in V \)
with \( V = \text{FinProd}(succ(n)\rightarrow \bigcup \tau ,W_V) \) have \( x:succ(n)\rightarrow \bigcup \tau \) and II: \( \forall k\in domain(W_V).\ x(k) \in W_V(k) \) unfolding FinProd_def
with A2, \( W_V: succ(n)\rightarrow \tau \) have IV: \( \forall k\in n.\ \text{Init}(x)(k) = x(k) \) using init_props
have \( \text{Init}(x) \in U \)proof
from A2, \( x:succ(n)\rightarrow \bigcup \tau \) have \( \text{Init}(x): n\rightarrow \bigcup \tau \) using init_props
moreover
have \( \forall k\in domain( \text{Init}(W_V)).\ \text{Init}(x)(k) \in \text{Init}(W_V)(k) \)proof
from A2, \( W_V: succ(n)\rightarrow \tau \) have \( \text{Init}(W_V): n\rightarrow \tau \) using init_props
then have \( domain( \text{Init}(W_V)) = n \) using func1_1_L1
note III, IV, \( domain( \text{Init}(W_V)) = n \)
moreover
from II, \( W_V \in succ(n)\rightarrow \tau \) have \( \forall k\in n.\ x(k) \in W_V(k) \) using func1_1_L1
ultimately show \( thesis \)
qed
ultimately show \( \text{Init}(x) \in U \) using FinProd_def
qed
moreover
from \( W_V: succ(n)\rightarrow \tau \), II have \( x(n) \in W \) using func1_1_L1
ultimately have \( \langle \text{Init}(x),x(n)\rangle \in U\times W \)
with I have \( y \in U\times W \)
}
thus \( \{\langle \text{Init}(x),x(n)\rangle .\ x\in V\} \subseteq U\times W \)
{
fix \( y \)
assume \( y \in U\times W \)
then have \( \text{fst}(y) \in U \) and \( \text{snd}(y) \in W \)
with \( domain( \text{Init}(W_V)) = n \) have \( \text{fst}(y): n\rightarrow \bigcup \tau \) and V: \( \forall k\in n.\ \text{fst}(y)(k) \in \text{Init}(W_V)(k) \) using FinProd_def
from \( W_V: succ(n)\rightarrow \tau \) have \( W \in \tau \) using apply_funtype
with \( \text{snd}(y) \in W \) have \( \text{snd}(y) \in \bigcup \tau \)
let \( x = \text{Append}(\text{fst}(y),\text{snd}(y)) \)
have \( x\in V \)proof
from \( \text{fst}(y): n\rightarrow \bigcup \tau \), \( \text{snd}(y) \in \bigcup \tau \) have \( x:succ(n)\rightarrow \bigcup \tau \) using append_props
moreover
have \( \forall i\in domain(W_V).\ x(i) \in W_V(i) \)proof
from \( \text{fst}(y): n\rightarrow \bigcup \tau \), \( \text{snd}(y) \in \bigcup \tau \) have \( \forall k\in n.\ x(k) = \text{fst}(y)(k) \) and \( x(n) = \text{snd}(y) \) using append_props
moreover
from III, V have \( \forall k\in n.\ \text{fst}(y)(k) \in W_V(k) \)
moreover
note \( \text{snd}(y) \in W \)
ultimately have \( \forall i\in succ(n).\ x(i) \in W_V(i) \)
with \( W_V \in succ(n)\rightarrow \tau \) show \( thesis \) using func1_1_L1
qed
ultimately have \( x \in \text{FinProd}(succ(n)\rightarrow \bigcup \tau ,W_V) \) using FinProd_def
with \( V = \text{FinProd}(succ(n)\rightarrow \bigcup \tau ,W_V) \) show \( x\in V \)
qed
moreover
from A2, \( y \in U\times W \), \( \text{fst}(y): n\rightarrow \bigcup \tau \), \( \text{snd}(y) \in \bigcup \tau \) have \( y = \langle \text{Init}(x),x(n)\rangle \) using init_append, append_props
ultimately have \( y \in \{\langle \text{Init}(x),x(n)\rangle .\ x\in V\} \)
}
thus \( U\times W \subseteq \{\langle \text{Init}(x),x(n)\rangle .\ x\in V\} \)
qed
finally show \( f(V) = U\times W \)
qed
ultimately show \( f(V) \in \text{ProductTopology}(T,\tau ) \)
qed
ultimately show \( thesis \) using bij_base_open_homeo
qed
end
Definition of ProductTopBase: \( \text{ProductTopBase}(I,T) \equiv \bigcup N\in \text{FinPow}(I).\ \{ \text{FinProd}(I\rightarrow \bigcup T,W).\ W\in N\rightarrow 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 fun_union_overlap:

assumes \( \forall x\in A\cap B.\ h(x) \in Y \), \( \forall x\in A\setminus B.\ f(x) \in Y \), \( \forall x\in B\setminus A.\ g(x) \in Y \)

shows \( \{\langle x,\text{if }x\in A\setminus B\text{ then }f(x)\text{ else }\text{if }x\in B\setminus A\text{ then }g(x)\text{ else }h(x)\rangle .\ x \in A\cup B\}: A\cup B \rightarrow Y \)
lemma union_finpow:

assumes \( A \in \text{FinPow}(X) \) and \( B \in \text{FinPow}(X) \)

shows \( A \cup B \in \text{FinPow}(X) \)
lemma func1_1_L1:

assumes \( f:A\rightarrow C \)

shows \( domain(f) = A \)
Definition of FinProd: \( \text{FinProd}(\mathcal{X} ,W) \equiv \{x\in \mathcal{X} .\ \forall i\in domain(W).\ x(i) \in W(i)\} \)
lemma ZF_fun_from_tot_val:

assumes \( f:X\rightarrow Y \), \( x\in X \) and \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)

shows \( f(x) = b(x) \) and \( b(x)\in Y \)
lemma prod_top_base_inter:

assumes \( T \text{ is a topology } \) and \( U \in \text{ProductTopBase}(I,T) \), \( V \in \text{ProductTopBase}(I,T) \)

shows \( U\cap V \in \text{ProductTopBase}(I,T) \)
lemma inter_closed_base:

assumes \( \forall U\in B.\ (\forall V\in B.\ U\cap V \in B) \)

shows \( B \text{ satisfies the base condition } \)
theorem prod_top_base_is_base:

assumes \( T \text{ is a topology } \)

shows \( \text{ProductTopBase}(I,T) \text{ satisfies the base condition } \)
Definition of SeqProductTopology: \( \text{SeqProductTopology}(I,T) \equiv \{\bigcup B.\ B \in Pow( \text{ProductTopBase}(I,T))\} \)
theorem Top_1_2_T1:

assumes \( B \text{ satisfies the base condition } \) and \( T = \{\bigcup A.\ A\in Pow(B)\} \)

shows \( T \text{ is a topology } \) and \( B \text{ is a base for } T \)
lemma Top_1_2_L5:

assumes \( B \text{ is a base for } T \)

shows \( \bigcup T = \bigcup B \)
lemma empty_in_finpow: shows \( 0 \in \text{FinPow}(X) \)
lemma nat_finpow_nat:

assumes \( n \in nat \)

shows \( n \in \text{FinPow}(nat) \)
lemma fin_finpow_self:

assumes \( A \in \text{FinPow}(X) \)

shows \( A \in \text{FinPow}(A) \)
Definition of FinPow: \( \text{FinPow}(X) \equiv \{A \in Pow(X).\ Finite(A)\} \)
lemma ZF_fun_from_total:

assumes \( \forall x\in X.\ b(x) \in Y \)

shows \( \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y \)
lemma func_singleton_pair:

assumes \( f : \{a\}\rightarrow X \)

shows \( f = \{\langle a, f(a)\rangle \} \)
lemma pair_func_singleton:

assumes \( y \in Y \)

shows \( \{\langle x,y\rangle \} : \{x\} \rightarrow Y \)
lemma pair_val: shows \( \{\langle x,y\rangle \}(x) = y \)
lemma list_singleton_bij: shows \( \{\langle x,\{\langle 0,x\rangle \}\rangle .\ x\in X\} \in \text{bij}(X,1\rightarrow X) \) and \( \{\langle y,y(0)\rangle .\ y\in 1\rightarrow X\} = converse(\{\langle x,\{\langle 0,x\rangle \}\rangle .\ x\in X\}) \) and \( \{\langle x,\{\langle 0,x\rangle \}\rangle .\ x\in X\} = converse(\{\langle y,y(0)\rangle .\ y\in 1\rightarrow X\}) \)
theorem bij_induced_top:

assumes \( T \text{ is a topology } \) and \( f \in \text{bij}(\bigcup T,Y) \)

shows \( \{f(U).\ U\in T\} \text{ is a topology } \) and \( \{ \{f(x).\ x\in U\}.\ U\in T\} \text{ is a topology } \) and \( (\bigcup \{f(U).\ U\in T\}) = Y \) and \( \text{IsAhomeomorphism}(T, \{f(U).\ U\in T\},f) \)
lemma func_imagedef:

assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)

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

assumes \( n\in nat \) and \( T \text{ is a topology } \)

shows \( \text{ProductTopBase}(n,T) = \{ \text{FinProd}(n\rightarrow \bigcup T,W).\ W\in n\rightarrow T\} \)
lemma single_top_prod:

assumes \( W:1\rightarrow \tau \)

shows \( \text{FinProd}(1\rightarrow \bigcup \tau ,W) = \{ \{\langle 0,y\rangle \}.\ y \in W(0)\} \)
theorem seq_prod_top_is_top:

assumes \( T \text{ is a topology } \)

shows \( \text{SeqProductTopology}(I,T) \text{ is a topology } \) and \( \text{ProductTopBase}(I,T) \text{ is a base for } \text{SeqProductTopology}(I,T) \) and \( \bigcup \text{SeqProductTopology}(I,T) = (I\rightarrow \bigcup T) \)
lemma base_topology:

assumes \( B \text{ is a topology } \) and \( B \text{ is a base for } T \)

shows \( B=T \)
lemma singleton_prod_top:

assumes \( \tau \text{ is a topology } \)

shows \( \text{SeqProductTopology}(1,\tau ) = \{ \{ \{\langle 0,y\rangle \}.\ y\in U \}.\ U\in \tau \} \) and \( \text{IsAhomeomorphism}(\tau , \text{SeqProductTopology}(1,\tau ),\{\langle y,\{\langle 0,y\rangle \}\rangle .\ y \in \bigcup \tau \}) \)
lemma homeo_inv:

assumes \( \text{IsAhomeomorphism}(T,S,f) \)

shows \( \text{IsAhomeomorphism}(S,T,converse(f)) \)
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 append_props:

assumes \( a: n \rightarrow X \) and \( x\in X \) and \( b = \text{Append}(a,x) \)

shows \( b : succ(n) \rightarrow X \), \( \forall k\in n.\ b(k) = a(k) \), \( b(n) = x \)
theorem init_props:

assumes \( n \in nat \) and \( a: succ(n) \rightarrow X \)

shows \( \text{Init}(a) : n \rightarrow X \), \( \forall k\in n.\ \text{Init}(a)(k) = a(k) \), \( a = \text{Append}( \text{Init}(a), a(n)) \)
lemma Top_1_2_L1:

assumes \( B \text{ is a base for } T \) and \( U\in T \)

shows \( \exists A\in Pow(B).\ U = \bigcup A \)
lemma finite_prod_succ_base:

assumes \( \tau \text{ is a topology } \) and \( n \in nat \) and \( U \in \text{ProductTopBase}(n,\tau ) \) and \( V\in \tau \)

shows \( \{x \in succ(n)\rightarrow \bigcup \tau .\ \text{Init}(x) \in U \wedge x(n) \in V\} \in \text{ProductTopBase}(succ(n),\tau ) \)
lemma base_sets_open:

assumes \( B \text{ is a base for } T \) and \( U \in B \)

shows \( U \in T \)
lemma union_indexed_open:

assumes \( T \text{ is a topology } \) and \( \forall i\in I.\ P(i) \in T \)

shows \( (\bigcup i\in I.\ P(i)) \in T \)
lemma lists_cart_prod:

assumes \( n \in nat \)

shows \( \{\langle x,\langle \text{Init}(x),x(n)\rangle \rangle .\ x \in succ(n)\rightarrow X\} \in \text{bij}(succ(n)\rightarrow X,(n\rightarrow X)\times X) \)
Definition of ProductCollection: \( \text{ProductCollection}(T,S) \equiv \bigcup U\in T.\ \{U\times V.\ V\in S\} \)
lemma func1_1_L15:

assumes \( f:X\rightarrow Y \)

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

assumes \( \tau \text{ is a topology } \) and \( n \in nat \) and \( U \in \text{SeqProductTopology}(n,\tau ) \) and \( V\in \tau \)

shows \( \{x \in succ(n)\rightarrow \bigcup \tau .\ \text{Init}(x) \in U \wedge x(n) \in V\} \in \text{SeqProductTopology}(succ(n),\tau ) \)
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) \)
Definition of IsAbaseFor: \( B \text{ is a base for } T \equiv B\subseteq T \wedge T = \{\bigcup A.\ A\in Pow(B)\} \)
lemma ZF_fun_from_tot_val0:

assumes \( f:X\rightarrow Y \) and \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)

shows \( \forall x\in X.\ f(x) = b(x) \)
lemma init_append:

assumes \( n \in nat \) and \( a:n\rightarrow X \) and \( x \in X \)

shows \( \text{Init}( \text{Append}(a,x)) = a \)
lemma (in two_top_spaces0) bij_base_open_homeo:

assumes \( f \in \text{bij}(X_1,X_2) \) and \( \mathcal{B} \text{ is a base for } \tau _1 \) and \( \mathcal{C} \text{ is a base for } \tau _2 \) and \( \forall U\in \mathcal{C} .\ f^{-1}(U) \in \tau _1 \) and \( \forall V\in \mathcal{B} .\ f(V) \in \tau _2 \)

shows \( \text{IsAhomeomorphism}(\tau _1,\tau _2,f) \)