Theory Topology_ZF_3
section ‹Topology 3›
theory Topology_ZF_3 imports Topology_ZF_2 FiniteSeq_ZF
begin
text‹‹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.›
subsection‹The base of the product topology›
text‹In this section we define the base of the product topology.›
text‹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
"FinProd(𝒳,W) ≡ {x∈𝒳. ∀ i∈domain(W). x`(i) ∈ W`(i)}"
text‹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
"ProductTopBase(I,T) ≡ ⋃N∈FinPow(I).{FinProd(I→⋃T,W). W∈N→T}"
text‹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
"SeqProductTopology(I,T) ≡ {⋃B. B ∈ Pow(ProductTopBase(I,T))}"
text‹Product topology base is closed with respect to intersections.›
lemma prod_top_base_inter:
assumes A1: "T {is a topology}" and
A2: "U ∈ ProductTopBase(I,T)" "V ∈ ProductTopBase(I,T)"
shows "U∩V ∈ ProductTopBase(I,T)"
proof -
let ?𝒳 = "I→⋃T"
from A2 obtain N⇩1 W⇩1 N⇩2 W⇩2 where
I: "N⇩1 ∈ FinPow(I)" "W⇩1∈N⇩1→T" "U = FinProd(?𝒳,W⇩1)" and
II: "N⇩2 ∈ FinPow(I)" "W⇩2∈N⇩2→T" "V = FinProd(?𝒳,W⇩2)"
using ProductTopBase_def by auto
let ?N⇩3 = "N⇩1 ∪ N⇩2"
let ?W⇩3 = "{⟨i,if i ∈ N⇩1-N⇩2 then W⇩1`(i)
else if i ∈ N⇩2-N⇩1 then W⇩2`(i)
else (W⇩1`(i)) ∩ (W⇩2`(i))⟩. i ∈ ?N⇩3}"
from A1 I II have "∀i ∈ N⇩1 ∩ N⇩2. (W⇩1`(i) ∩ W⇩2`(i)) ∈ T"
using apply_funtype IsATopology_def by auto
moreover from I II have "∀i∈N⇩1-N⇩2. W⇩1`(i) ∈ T" and "∀i∈N⇩2-N⇩1. W⇩2`(i) ∈ T"
using apply_funtype by auto
ultimately have "?W⇩3:?N⇩3→T" by (rule fun_union_overlap)
with I II have "FinProd(?𝒳,?W⇩3) ∈ ProductTopBase(I,T)" using union_finpow ProductTopBase_def
by auto
moreover have "U∩V = FinProd(?𝒳,?W⇩3)"
proof
{ fix x assume "x∈U" and "x∈V"
with ‹U = FinProd(?𝒳,W⇩1)› ‹W⇩1∈N⇩1→T› and ‹V = FinProd(?𝒳,W⇩2)› ‹W⇩2∈N⇩2→T›
have "x∈?𝒳" and "∀i∈N⇩1. x`(i) ∈ W⇩1`(i)" and "∀i∈N⇩2. x`(i) ∈ W⇩2`(i)"
using func1_1_L1 FinProd_def by auto
with ‹?W⇩3:?N⇩3→T› ‹x∈?𝒳› have "x ∈ FinProd(?𝒳,?W⇩3)"
using ZF_fun_from_tot_val func1_1_L1 FinProd_def by auto
} thus "U∩V ⊆ FinProd(?𝒳,?W⇩3)" by auto
{ fix x assume "x ∈ FinProd(?𝒳,?W⇩3)"
with ‹?W⇩3:?N⇩3→T› have "x:I→⋃T" and III: "∀i∈?N⇩3. x`(i) ∈ ?W⇩3`(i)"
using FinProd_def func1_1_L1 by auto
{ fix i assume "i∈N⇩1"
with ‹?W⇩3:?N⇩3→T› have "?W⇩3`(i) ⊆ W⇩1`(i)" using ZF_fun_from_tot_val by auto
with III ‹i∈N⇩1› have "x`(i) ∈ W⇩1`(i)" by auto
} with ‹W⇩1∈N⇩1→T› ‹x:I→⋃T› ‹U = FinProd(?𝒳,W⇩1)›
have "x ∈ U" using func1_1_L1 FinProd_def by auto
moreover
{ fix i assume "i∈N⇩2"
with ‹?W⇩3:?N⇩3→T› have "?W⇩3`(i) ⊆ W⇩2`(i)" using ZF_fun_from_tot_val by auto
with III ‹i∈N⇩2› have "x`(i) ∈ W⇩2`(i)" by auto
} with ‹W⇩2∈N⇩2→T› ‹x:I→⋃T› ‹V = FinProd(?𝒳,W⇩2)› have "x∈V"
using func1_1_L1 FinProd_def by auto
ultimately have "x ∈ U∩V" by simp
} thus "FinProd(?𝒳,?W⇩3) ⊆ U∩V" by auto
qed
ultimately show ?thesis by simp
qed
text‹In the next theorem we show the collection of sets defined above as
‹ProductTopBase(𝒳,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 {is a topology}"
shows "ProductTopBase(I,T) {satisfies the base condition}"
using assms prod_top_base_inter inter_closed_base by simp
text‹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 {is a topology}"
shows
"SeqProductTopology(I,T) {is a topology}" and
"ProductTopBase(I,T) {is a base for} SeqProductTopology(I,T)" and
"⋃SeqProductTopology(I,T) = (I→⋃T)"
proof -
from assms show "SeqProductTopology(I,T) {is a topology}" and
I: "ProductTopBase(I,T) {is a base for} SeqProductTopology(I,T)"
using prod_top_base_is_base SeqProductTopology_def Top_1_2_T1
by auto
from I have "⋃SeqProductTopology(I,T) = ⋃ProductTopBase(I,T)"
using Top_1_2_L5 by simp
also have "⋃ProductTopBase(I,T) = (I→⋃T)"
proof
show "⋃ProductTopBase(I,T) ⊆ (I→⋃T)" using ProductTopBase_def FinProd_def
by auto
have "0 ∈ FinPow(I)" using empty_in_finpow by simp
hence "{FinProd(I→⋃T,W). W∈0→T} ⊆ (⋃N∈FinPow(I).{FinProd(I→⋃T,W). W∈N→T})"
by blast
then show "(I→⋃T) ⊆ ⋃ProductTopBase(I,T)" using ProductTopBase_def FinProd_def
by auto
qed
finally show "⋃SeqProductTopology(I,T) = (I→⋃T)" by simp
qed
subsection‹Finite product of topologies›
text‹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.
›
text‹When the index set is finite, the definition of ‹ProductTopBase(I,T)›
can be simplifed.›
lemma fin_prod_def_nat: assumes A1: "n∈nat" and A2: "T {is a topology}"
shows "ProductTopBase(n,T) = {FinProd(n→⋃T,W). W∈n→T}"
proof
from A1 have "n ∈ FinPow(n)" using nat_finpow_nat fin_finpow_self by auto
then show "{FinProd(n→⋃T,W). W∈n→T} ⊆ ProductTopBase(n,T)" using ProductTopBase_def
by auto
{ fix B assume "B ∈ ProductTopBase(n,T)"
then obtain N W where "N ∈ FinPow(n)" and "W ∈ N→T" and "B = FinProd(n→⋃T,W)"
using ProductTopBase_def by auto
let ?W⇩n = "{⟨i,if i∈N then W`(i) else ⋃T⟩. i∈n}"
from A2 ‹N ∈ FinPow(n)› ‹W∈N→T› have "∀i∈n. (if i∈N then W`(i) else ⋃T) ∈ T"
using apply_funtype FinPow_def IsATopology_def by auto
then have "?W⇩n:n→T" by (rule ZF_fun_from_total)
moreover have "B = FinProd(n→⋃T,?W⇩n)"
proof
{ fix x assume "x∈B"
with ‹B = FinProd(n→⋃T,W)› have "x ∈ n→⋃T" using FinProd_def by simp
moreover have "∀i∈domain(?W⇩n). x`(i) ∈ ?W⇩n`(i)"
proof
fix i assume "i ∈ domain(?W⇩n)"
with ‹?W⇩n:n→T› have "i∈n" using func1_1_L1 by simp
with ‹x:n→⋃T› have "x`(i) ∈ ⋃T" using apply_funtype by blast
with ‹x∈B› ‹B = FinProd(n→⋃T,W)› ‹W ∈ N→T› ‹?W⇩n:n→T› ‹i∈n›
show "x`(i) ∈ ?W⇩n`(i)" using func1_1_L1 FinProd_def ZF_fun_from_tot_val
by simp
qed
ultimately have "x ∈ FinProd(n→⋃T,?W⇩n)" using FinProd_def by simp
} thus "B ⊆ FinProd(n→⋃T,?W⇩n)" by auto
next
{ fix x assume "x ∈ FinProd(n→⋃T,?W⇩n)"
then have "x ∈ n→⋃T" and "∀i∈domain(?W⇩n). x`(i) ∈ ?W⇩n`(i)"
using FinProd_def by auto
with ‹?W⇩n:n→T› and ‹N ∈ FinPow(n)› have "∀i∈N. x`(i) ∈ ?W⇩n`(i)"
using func1_1_L1 FinPow_def by auto
moreover from ‹?W⇩n:n→T› and ‹N ∈ FinPow(n)›
have "∀i∈N. ?W⇩n`(i) = W`(i)"
using ZF_fun_from_tot_val FinPow_def by auto
ultimately have "∀i∈N. x`(i) ∈ W`(i)" by simp
with ‹W ∈ N→T› ‹x ∈ n→⋃T› ‹B = FinProd(n→⋃T,W)› have "x∈B"
using func1_1_L1 FinProd_def by simp
} thus "FinProd(n→⋃T,?W⇩n) ⊆ B" by auto
qed
ultimately have "B ∈ {FinProd(n→⋃T,W). W∈n→T}" by auto
} thus "ProductTopBase(n,T) ⊆ {FinProd(n→⋃T,W). W∈n→T}" by auto
qed
text‹A technical lemma providing a formula for finite product on one topological space.›
lemma single_top_prod: assumes A1: "W:1→τ"
shows "FinProd(1→⋃τ,W) = { {⟨0,y⟩}. y ∈ W`(0)}"
proof -
have "1 = {0}" by auto
from A1 have "domain(W) = {0}" using func1_1_L1 by auto
then have "FinProd(1→⋃τ,W) = {x ∈ 1→⋃τ. x`(0) ∈ W`(0)}"
using FinProd_def by simp
also have "{x ∈ 1→⋃τ. x`(0) ∈ W`(0)} = { {⟨0,y⟩}. y ∈ W`(0)}"
proof
from ‹1 = {0}› show "{x ∈ 1→⋃τ. x`(0) ∈ W`(0)} ⊆ { {⟨0,y⟩}. y ∈ W`(0)}"
using func_singleton_pair by auto
{ fix x assume "x ∈ { {⟨0,y⟩}. y ∈ W`(0)}"
then obtain y where "x = {⟨0,y⟩}" and II: "y ∈ W`(0)" by auto
with A1 have "y ∈ ⋃τ" using apply_funtype by auto
with ‹x = {⟨0,y⟩}› ‹1 = {0}› have "x:1→⋃τ" using pair_func_singleton
by auto
with ‹x = {⟨0,y⟩}› II have "x ∈ {x ∈ 1→⋃τ. x`(0) ∈ W`(0)}"
using pair_val by simp
} thus "{ {⟨0,y⟩}. y ∈ W`(0)} ⊆ {x ∈ 1→⋃τ. x`(0) ∈ W`(0)}" by auto
qed
finally show ?thesis by simp
qed
text‹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: "τ {is a topology}"
shows
"SeqProductTopology(1,τ) = { { {⟨0,y⟩}. y∈U }. U∈τ}" and
"IsAhomeomorphism(τ,SeqProductTopology(1,τ),{⟨y,{⟨0,y⟩}⟩.y ∈ ⋃τ})"
proof -
have "{0} = 1" by auto
let ?b = "{⟨y,{⟨0,y⟩}⟩.y ∈ ⋃τ}"
have "?b ∈ bij(⋃τ,1→⋃τ)" using list_singleton_bij by blast
with A1 have "{?b``(U). U∈τ} {is a topology}" and "IsAhomeomorphism(τ, {?b``(U). U∈τ},?b)"
using bij_induced_top by auto
moreover have "∀U∈τ. ?b``(U) = { {⟨0,y⟩}. y∈U }"
proof
fix U assume "U∈τ"
from ‹?b ∈ bij(⋃τ,1→⋃τ)› have "?b:⋃τ→(1→⋃τ)" using bij_def inj_def
by simp
{ fix y assume "y ∈ ⋃τ"
with ‹?b:⋃τ→(1→⋃τ)› have "?b`(y) = {⟨0,y⟩}" using ZF_fun_from_tot_val
by simp
} hence "∀y ∈ ⋃τ. ?b`(y) = {⟨0,y⟩}" by auto
with ‹U∈τ› ‹?b:⋃τ→(1→⋃τ)› show " ?b``(U) = { {⟨0,y⟩}. y∈U }"
using func_imagedef by auto
qed
moreover have "ProductTopBase(1,τ) = { { {⟨0,y⟩}. y∈U }. U∈τ}"
proof
{ fix V assume "V ∈ ProductTopBase(1,τ)"
with A1 obtain W where "W:1→τ" and "V = FinProd(1→⋃τ,W)"
using fin_prod_def_nat by auto
then have "V ∈ { { {⟨0,y⟩}. y∈U }. U∈τ}" using apply_funtype single_top_prod
by auto
} thus "ProductTopBase(1,τ) ⊆ { { {⟨0,y⟩}. y∈U }. U∈τ}" by auto
{ fix V assume "V ∈ { { {⟨0,y⟩}. y∈U }. U∈τ}"
then obtain U where "U∈τ" and "V = { {⟨0,y⟩}. y∈U }" by auto
let ?W = "{⟨0,U⟩}"
from ‹U∈τ› have "?W:{0}→τ" using pair_func_singleton by simp
with ‹{0} = 1› have "?W:1→τ" and "?W`(0) = U" using pair_val by auto
with ‹V = { {⟨0,y⟩}. y∈U }› have "V = FinProd(1→⋃τ,?W)"
using single_top_prod by simp
with A1 ‹?W:1→τ› have "V ∈ ProductTopBase(1,τ)" using fin_prod_def_nat
by auto
} thus "{ { {⟨0,y⟩}. y∈U }. U∈τ} ⊆ ProductTopBase(1,τ)" by auto
qed
ultimately have I: "ProductTopBase(1,τ) {is a topology}" and
II: "IsAhomeomorphism(τ, ProductTopBase(1,τ),?b)" by auto
from A1 have "ProductTopBase(1,τ) {is a base for} SeqProductTopology(1,τ)"
using seq_prod_top_is_top by simp
with I have "ProductTopBase(1,τ) = SeqProductTopology(1,τ)" by (rule base_topology)
with ‹ProductTopBase(1,τ) = { { {⟨0,y⟩}. y∈U }. U∈τ}› II show
"SeqProductTopology(1,τ) = { { {⟨0,y⟩}. y∈U }. U∈τ}" and
"IsAhomeomorphism(τ,SeqProductTopology(1,τ),{⟨y,{⟨0,y⟩}⟩.y ∈ ⋃τ})" by auto
qed
text‹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: "τ {is a topology}"
shows "IsAhomeomorphism(SeqProductTopology(1,τ),τ,{⟨x,x`(0)⟩. x∈1→⋃τ})"
proof -
have "{⟨x,x`(0)⟩. x∈1→⋃τ} = converse({⟨y,{⟨0,y⟩}⟩.y∈⋃τ})"
using list_singleton_bij by blast
with A1 show ?thesis using singleton_prod_top homeo_inv by simp
qed
text‹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 "τ {is a topology}" and "T = SeqProductTopology(n,τ)"
shows "(⋃ProductTopology(T,τ)) = (n→⋃τ)×⋃τ"
using assms Top_1_4_T1 seq_prod_top_is_top by simp
text‹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: "τ {is a topology}" and A2: "n ∈ nat" and
A3: "U ∈ ProductTopBase(n,τ)" and A4: "V∈τ"
shows "{x ∈ succ(n)→⋃τ. Init(x) ∈ U ∧ x`(n) ∈ V} ∈ ProductTopBase(succ(n),τ)"
proof -
let ?B = "{x ∈ succ(n)→⋃τ. Init(x) ∈ U ∧ x`(n) ∈ V}"
from A1 A2 have "ProductTopBase(n,τ) = {FinProd(n→⋃τ,W). W∈n→τ}"
using fin_prod_def_nat by simp
with A3 obtain W⇩U where "W⇩U:n→τ" and "U =FinProd(n→⋃τ,W⇩U)" by auto
let ?W = "Append(W⇩U,V)"
from A4 and ‹W⇩U:n→τ› have "?W:succ(n)→τ" using append_props by simp
moreover have "?B = FinProd(succ(n)→⋃τ,?W)"
proof
{ fix x assume "x∈?B"
with ‹?W:succ(n)→τ› have "x ∈ succ(n)→⋃τ" and "domain(?W) = succ(n)" using func1_1_L1
by auto
moreover from A2 A4 ‹x∈?B› ‹U =FinProd(n→⋃τ,W⇩U)› ‹W⇩U:n→τ› ‹x ∈ succ(n)→⋃τ›
have "∀i∈succ(n). x`(i) ∈ ?W`(i)" using func1_1_L1 FinProd_def init_props append_props
by simp
ultimately have "x ∈ FinProd(succ(n)→⋃τ,?W)" using FinProd_def by simp
} thus "?B ⊆ FinProd(succ(n)→⋃τ,?W)" by auto
next
{ fix x assume "x ∈ FinProd(succ(n)→⋃τ,?W)"
then have "x:succ(n)→⋃τ" and I: "∀i ∈ domain(?W). x`(i) ∈ ?W`(i)"
using FinProd_def by auto
moreover have "Init(x) ∈ U"
proof -
from A2 and ‹x:succ(n)→⋃τ› have "Init(x):n→⋃τ" using init_props by simp
moreover have "∀i∈domain(W⇩U). Init(x)`(i) ∈ W⇩U`(i)"
proof -
from A2 ‹x ∈ FinProd(succ(n)→⋃τ,?W)› ‹?W:succ(n)→τ› have "∀i∈n. x`(i) ∈ ?W`(i)"
using FinProd_def func1_1_L1 by simp
moreover from A2 ‹x: succ(n)→⋃τ› have "∀i∈n. Init(x)`(i) = x`(i)"
using init_props by simp
moreover from A4 and ‹W⇩U:n→τ› have "∀i∈n. ?W`(i) = W⇩U`(i)"
using append_props by simp
ultimately have "∀i∈n. Init(x)`(i) ∈ W⇩U`(i)" by simp
with ‹W⇩U:n→τ› show ?thesis using func1_1_L1 by simp
qed
ultimately have "Init(x) ∈ FinProd(n→⋃τ,W⇩U)" using FinProd_def by simp
with ‹U =FinProd(n→⋃τ,W⇩U)› show ?thesis by simp
qed
moreover have "x`(n) ∈ V"
proof -
from ‹?W:succ(n)→τ› I have "x`(n) ∈ ?W`(n)" using func1_1_L1 by simp
moreover from A4 ‹W⇩U:n→τ› have "?W`(n) = V" using append_props by simp
ultimately show ?thesis by simp
qed
ultimately have "x∈?B" by simp
} thus "FinProd(succ(n)→⋃τ,?W) ⊆ ?B" by auto
qed
moreover from A1 A2 have
"ProductTopBase(succ(n),τ) = {FinProd(succ(n)→⋃τ,W). W∈succ(n)→τ}"
using fin_prod_def_nat by simp
ultimately show ?thesis by auto
qed
text‹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: "τ {is a topology}" and A2: "n ∈ nat" and
A3: "U ∈ SeqProductTopology(n,τ)" and A4: "V∈τ"
shows "{x ∈ succ(n)→⋃τ. Init(x) ∈ U ∧ x`(n) ∈ V} ∈ SeqProductTopology(succ(n),τ)"
proof -
from A1 have "ProductTopBase(n,τ) {is a base for} SeqProductTopology(n,τ)" and
I: "ProductTopBase(succ(n),τ) {is a base for} SeqProductTopology(succ(n),τ)" and
II: "SeqProductTopology(succ(n),τ) {is a topology}"
using seq_prod_top_is_top by auto
with A3 have "∃ℬ ∈ Pow(ProductTopBase(n,τ)). U = ⋃ℬ" using Top_1_2_L1 by simp
then obtain ℬ where "ℬ ⊆ ProductTopBase(n,τ)" and "U = ⋃ℬ" by auto
then have
"{x:succ(n)→⋃τ. Init(x) ∈ U ∧ x`(n) ∈ V} = (⋃B∈ℬ.{x:succ(n)→⋃τ. Init(x) ∈ B ∧ x`(n) ∈ V})"
by auto
moreover from A1 A2 A4 ‹ℬ ⊆ ProductTopBase(n,τ)› have
"∀B∈ℬ. ({x:succ(n)→⋃τ. Init(x) ∈ B ∧ x`(n) ∈ V} ∈ ProductTopBase(succ(n),τ))"
using finite_prod_succ_base by auto
with I II have
"(⋃B∈ℬ.{x:succ(n)→⋃τ. Init(x) ∈ B ∧ x`(n) ∈ V}) ∈ SeqProductTopology(succ(n),τ)"
using base_sets_open union_indexed_open by auto
ultimately show ?thesis by simp
qed
text‹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: "τ {is a topology}" and A2: "n ∈ nat" and
A3: "f = {⟨x,⟨Init(x),x`(n)⟩⟩. x ∈ succ(n)→⋃τ}" and
A4: "T = SeqProductTopology(n,τ)" and
A5: "S = SeqProductTopology(succ(n),τ)"
shows "IsAhomeomorphism(S,ProductTopology(T,τ),f)"
proof -
let ?C = "ProductCollection(T,τ)"
let ?B = "ProductTopBase(succ(n),τ)"
from A1 A4 have "T {is a topology}" using seq_prod_top_is_top by simp
with A1 A5 have "S {is a topology}" and " ProductTopology(T,τ) {is a topology}"
using seq_prod_top_is_top Top_1_4_T1 by auto
moreover
from assms have "f ∈ bij(⋃S,⋃ProductTopology(T,τ))"
using lists_cart_prod seq_prod_top_is_top Top_1_4_T1 by simp
then have "f: ⋃S→⋃ProductTopology(T,τ)" using bij_is_fun by simp
ultimately have "two_top_spaces0(S,ProductTopology(T,τ),f)" using two_top_spaces0_def by simp
moreover note ‹f ∈ bij(⋃S,⋃ProductTopology(T,τ))›
moreover from A1 A5 have "?B {is a base for} S"
using seq_prod_top_is_top by simp
moreover from A1 ‹T {is a topology}› have "?C {is a base for} ProductTopology(T,τ)"
using Top_1_4_T1 by auto
moreover have "∀W∈?C. f-``(W) ∈ S"
proof
fix W assume "W∈?C"
then obtain U V where "U∈T" "V∈τ" and "W = U×V" using ProductCollection_def by auto
from A1 A5 ‹f: ⋃S→⋃ProductTopology(T,τ)› have "f: (succ(n)→⋃τ)→⋃ProductTopology(T,τ)"
using seq_prod_top_is_top by simp
with assms ‹W = U×V› ‹U∈T› ‹V∈τ› show "f-``(W) ∈ S"
using ZF_fun_from_tot_val func1_1_L15 finite_prod_succ by simp
qed
moreover have "∀V∈?B. f``(V) ∈ ProductTopology(T,τ)"
proof
fix V assume "V∈?B"
with A1 A2 obtain W⇩V where "W⇩V ∈ succ(n)→τ" and "V = FinProd(succ(n)→⋃τ,W⇩V)"
using fin_prod_def_nat by auto
let ?U = "FinProd(n→⋃τ,Init(W⇩V))"
let ?W = "W⇩V`(n)"
have "?U ∈ T"
proof -
from A1 A2 ‹W⇩V ∈ succ(n)→τ› have "?U ∈ ProductTopBase(n,τ)"
using fin_prod_def_nat init_props by auto
with A1 A4 show ?thesis using seq_prod_top_is_top base_sets_open by blast
qed
from A1 ‹W⇩V ∈ succ(n)→τ› ‹T {is a topology}› ‹?U ∈ T› have "?U×?W ∈ ProductTopology(T,τ)"
using apply_funtype prod_open_open_prod by simp
moreover have "f``(V) = ?U×?W"
proof -
from A2 ‹W⇩V: succ(n)→τ› have "Init(W⇩V): n→τ" and III: "∀k∈n. Init(W⇩V)`(k) = W⇩V`(k)"
using init_props by auto
then have "domain(Init(W⇩V)) = n" using func1_1_L1 by simp
have "f``(V) = {⟨Init(x),x`(n)⟩. x∈V}"
proof -
have "f``(V) = {f`(x). x∈V}"
proof -
from A1 A5 have "?B {is a base for} S" using seq_prod_top_is_top by simp
with ‹V∈?B› have "V ⊆ ⋃S" using IsAbaseFor_def by auto
with ‹f: ⋃S→⋃ProductTopology(T,τ)› show ?thesis using func_imagedef by simp
qed
moreover have "∀x∈V. f`(x) = ⟨Init(x),x`(n)⟩"
proof -
from A1 A3 A5 ‹V = FinProd(succ(n)→⋃τ,W⇩V)› have "V ⊆ ⋃S" and
fdef: "f = {⟨x,⟨Init(x),x`(n)⟩⟩. x ∈ ⋃S}" using seq_prod_top_is_top FinProd_def
by auto
from ‹f: ⋃S→⋃ProductTopology(T,τ)› fdef have "∀x ∈ ⋃S. f`(x) = ⟨Init(x),x`(n)⟩"
by (rule ZF_fun_from_tot_val0)
with ‹V ⊆ ⋃S› show ?thesis by auto
qed
ultimately show ?thesis by simp
qed
also have "{⟨Init(x),x`(n)⟩. x∈V} = ?U×?W"
proof
{ fix y assume "y ∈ {⟨Init(x),x`(n)⟩. x∈V}"
then obtain x where I: "y = ⟨Init(x),x`(n)⟩" and "x∈V" by auto
with ‹V = FinProd(succ(n)→⋃τ,W⇩V)› have
"x:succ(n)→⋃τ" and II: "∀k∈domain(W⇩V). x`(k) ∈ W⇩V`(k)"
unfolding FinProd_def by auto
with A2 ‹W⇩V: succ(n)→τ› have IV: "∀k∈n. Init(x)`(k) = x`(k)"
using init_props by simp
have "Init(x) ∈ ?U"
proof -
from A2 ‹x:succ(n)→⋃τ› have "Init(x): n→⋃τ" using init_props by simp
moreover have "∀k∈domain(Init(W⇩V)). Init(x)`(k) ∈ Init(W⇩V)`(k)"
proof -
from A2 ‹W⇩V: succ(n)→τ› have "Init(W⇩V): n→τ" using init_props by simp
then have "domain(Init(W⇩V)) = n" using func1_1_L1 by simp
note III IV ‹domain(Init(W⇩V)) = n›
moreover from II ‹W⇩V ∈ succ(n)→τ› have "∀k∈n. x`(k) ∈ W⇩V`(k)"
using func1_1_L1 by simp
ultimately show ?thesis by simp
qed
ultimately show "Init(x) ∈ ?U" using FinProd_def by simp
qed
moreover from ‹W⇩V: succ(n)→τ› II have "x`(n) ∈ ?W" using func1_1_L1 by simp
ultimately have "⟨Init(x),x`(n)⟩ ∈ ?U×?W" by simp
with I have "y ∈ ?U×?W" by simp
} thus "{⟨Init(x),x`(n)⟩. x∈V} ⊆ ?U×?W" by auto
{ fix y assume "y ∈ ?U×?W"
then have "fst(y) ∈ ?U" and "snd(y) ∈ ?W" by auto
with ‹domain(Init(W⇩V)) = n› have "fst(y): n→⋃τ" and
V: "∀k∈n. fst(y)`(k) ∈ Init(W⇩V)`(k)"
using FinProd_def by auto
from ‹W⇩V: succ(n)→τ› have "?W ∈ τ" using apply_funtype by simp
with ‹snd(y) ∈ ?W› have "snd(y) ∈ ⋃τ" by auto
let ?x = "Append(fst(y),snd(y))"
have "?x∈V"
proof -
from ‹fst(y): n→⋃τ› ‹snd(y) ∈ ⋃τ› have "?x:succ(n)→⋃τ" using append_props by simp
moreover have "∀i∈domain(W⇩V). ?x`(i) ∈ W⇩V`(i)"
proof -
from ‹fst(y): n→⋃τ› ‹snd(y) ∈ ⋃τ›
have "∀k∈n. ?x`(k) = fst(y)`(k)" and "?x`(n) = snd(y)"
using append_props by auto
moreover from III V have "∀k∈n. fst(y)`(k) ∈ W⇩V`(k)" by simp
moreover note ‹snd(y) ∈ ?W›
ultimately have "∀i∈succ(n). ?x`(i) ∈ W⇩V`(i)" by simp
with ‹W⇩V ∈ succ(n)→τ› show ?thesis using func1_1_L1 by simp
qed
ultimately have "?x ∈ FinProd(succ(n)→⋃τ,W⇩V)" using FinProd_def by simp
with ‹V = FinProd(succ(n)→⋃τ,W⇩V)› show "?x∈V" by simp
qed
moreover from A2 ‹y ∈ ?U×?W› ‹fst(y): n→⋃τ› ‹snd(y) ∈ ⋃τ› have "y = ⟨Init(?x),?x`(n)⟩"
using init_append append_props by auto
ultimately have "y ∈ {⟨Init(x),x`(n)⟩. x∈V}" by auto
} thus "?U×?W ⊆ {⟨Init(x),x`(n)⟩. x∈V}" by auto
qed
finally show "f``(V) = ?U×?W" by simp
qed
ultimately show "f``(V) ∈ ProductTopology(T,τ)" by simp
qed
ultimately show ?thesis using two_top_spaces0.bij_base_open_homeo by simp
qed
end