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
qed
have \( U\cap V = \text{FinProd}(\mathcal{X} ,W_3) \)proof
ultimately show \( thesis \)
{
}
}
}
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
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_baseThe (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
qed
have \( \bigcup \text{ProductTopBase}(I,T) = (I\rightarrow \bigcup T) \)proof
finally show \( \bigcup \text{SeqProductTopology}(I,T) = (I\rightarrow \bigcup T) \)
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
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
ultimately have \( B \in \{ \text{FinProd}(n\rightarrow \bigcup T,W).\ W\in n\rightarrow T\} \)
{
}
}
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
ultimately have \( x \in \text{FinProd}(n\rightarrow \bigcup T,W_n) \) using FinProd_def
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
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
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
qed
have \( \{x \in 1\rightarrow \bigcup \tau .\ x(0) \in W(0)\} = \{ \{\langle 0,y\rangle \}.\ y \in W(0)\} \)proof
}
finally show \( thesis \)
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
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
}
moreover 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
have \( \text{ProductTopBase}(1,\tau ) = \{ \{ \{\langle 0,y\rangle \}.\ y\in U \}.\ U\in \tau \} \)proof
ultimately have I: \( \text{ProductTopBase}(1,\tau ) \text{ is a topology } \) and II: \( \text{IsAhomeomorphism}(\tau , \text{ProductTopBase}(1,\tau ),b) \)
{
}
}
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
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_topIf \(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
qed
have \( B = \text{FinProd}(succ(n)\rightarrow \bigcup \tau ,W) \)proof
moreover {
}
}
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
moreover from A2, and, \( x:succ(n)\rightarrow \bigcup \tau \) have \( \text{Init}(x):n\rightarrow \bigcup \tau \) using init_props
moreover
qed
have \( \forall i\in domain(W_U).\ \text{Init}(x)(i) \in W_U(i) \)proof
ultimately have \( \text{Init}(x) \in \text{FinProd}(n\rightarrow \bigcup \tau ,W_U) \) using FinProd_def
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
qed
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
with \( U = \text{FinProd}(n\rightarrow \bigcup \tau ,W_U) \) show \( thesis \)
have \( x(n) \in V \)proof
ultimately have \( x\in B \)
from \( W:succ(n)\rightarrow \tau \), I have \( x(n) \in W(n) \) using func1_1_L1
moreover
qed
from A4, \( W_U:n\rightarrow \tau \) have \( W(n) = V \) using append_props
ultimately show \( thesis \)
thus \( \text{FinProd}(succ(n)\rightarrow \bigcup \tau ,W) \subseteq B \)
qed
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 \)
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
qed
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 \)
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
qed
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
moreover 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
have \( \forall V\in B.\ f(V) \in \text{ProductTopology}(T,\tau ) \)proof
ultimately show \( thesis \) using bij_base_open_homeo
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
qed
have \( f(V) = U\times W \)proof
ultimately show \( f(V) \in \text{ProductTopology}(T,\tau ) \)
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
qed
have \( \forall x\in V.\ f(x) = \langle \text{Init}(x),x(n)\rangle \)proof
ultimately show \( thesis \)
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
also
qed
have \( \{\langle \text{Init}(x),x(n)\rangle .\ x\in V\} = U\times W \)proof
finally show \( f(V) = U\times W \)
{
}
}
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
qed
have \( \forall k\in domain( \text{Init}(W_V)).\ \text{Init}(x)(k) \in \text{Init}(W_V)(k) \)proof
ultimately show \( \text{Init}(x) \in U \) using FinProd_def
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
qed
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 \)
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
qed
have \( \forall i\in domain(W_V).\ x(i) \in W_V(i) \)proof
ultimately have \( x \in \text{FinProd}(succ(n)\rightarrow \bigcup \tau ,W_V) \) using FinProd_def
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
qed
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
with \( V = \text{FinProd}(succ(n)\rightarrow \bigcup \tau ,W_V) \) show \( x\in V \)
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
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) \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8