(*

This file is a part of IsarMathLib -

a library of formalized mathematics for Isabelle/Isar.

Copyright (C) 2011, 2012 Slawomir Kolodynski

This program is free software Redistribution and use in source and binary forms,

with or without modification, are permitted provided that the following conditions are met:

1. Redistributions of source code must retain the above copyright notice,

this list of conditions and the following disclaimer.

2. Redistributions in binary form must reproduce the above copyright notice,

this list of conditions and the following disclaimer in the documentation and/or

other materials provided with the distribution.

3. The name of the author may not be used to endorse or promote products

derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES,

INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A

PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT,

INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT

LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES LOSS OF USE, DATA, OR PROFITS OR

BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,

STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE

USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

*)

header{*\isaheader{Topology\_ZF\_3.thy}*}

theory Topology_ZF_3 imports Topology_ZF_2 FiniteSeq_ZF

begin

text{* @{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.*}

section{*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(\<X>,W) ≡ {x∈\<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) ≡ \<Union>N∈FinPow(I).{FinProd(I->\<Union>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) ≡ {\<Union>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 ?\<X> = "I->\<Union>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(?\<X>,W⇩_{1})" and

II: "N⇩_{2}∈ FinPow(I)" "W⇩_{2}∈N⇩_{2}->T" "V = FinProd(?\<X>,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(?\<X>,?W⇩_{3}) ∈ ProductTopBase(I,T)" using union_finpow ProductTopBase_def

by auto

moreover have "U∩V = FinProd(?\<X>,?W⇩_{3})"

proof

{ fix x assume "x∈U" and "x∈V"

with `U = FinProd(?\<X>,W⇩_{1})` `W⇩_{1}∈N⇩_{1}->T` and `V = FinProd(?\<X>,W⇩_{2})` `W⇩_{2}∈N⇩_{2}->T`

have "x∈?\<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∈?\<X>` have "x ∈ FinProd(?\<X>,?W⇩_{3})"

using ZF_fun_from_tot_val func1_1_L1 FinProd_def by auto

} thus "U∩V ⊆ FinProd(?\<X>,?W⇩_{3})" by auto

{ fix x assume "x ∈ FinProd(?\<X>,?W⇩_{3})"

with `?W⇩_{3}:?N⇩_{3}->T` have "x:I->\<Union>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->\<Union>T` `U = FinProd(?\<X>,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->\<Union>T` `V = FinProd(?\<X>,W⇩_{2})` have "x∈V"

using func1_1_L1 FinProd_def by auto

ultimately have "x ∈ U∩V" by simp

} thus "FinProd(?\<X>,?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

@{text "ProductTopBase(\<X>,T)"} satisfies the base condition. This is a condition, defined in

@{text "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

"\<Union>SeqProductTopology(I,T) = (I->\<Union>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 "\<Union>SeqProductTopology(I,T) = \<Union>ProductTopBase(I,T)"

using Top_1_2_L5 by simp

also have "\<Union>ProductTopBase(I,T) = (I->\<Union>T)"

proof

show "\<Union>ProductTopBase(I,T) ⊆ (I->\<Union>T)" using ProductTopBase_def FinProd_def

by auto

have "0 ∈ FinPow(I)" using empty_in_finpow by simp

hence "{FinProd(I->\<Union>T,W). W∈0->T} ⊆ (\<Union>N∈FinPow(I).{FinProd(I->\<Union>T,W). W∈N->T})"

by blast

then show "(I->\<Union>T) ⊆ \<Union>ProductTopBase(I,T)" using ProductTopBase_def FinProd_def

by auto

qed

finally show "\<Union>SeqProductTopology(I,T) = (I->\<Union>T)" by simp

qed

section{*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 @{text "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->\<Union>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->\<Union>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->\<Union>T,W)"

using ProductTopBase_def by auto

let ?W⇩_{n}= "{⟨i,if i∈N then W`(i) else \<Union>T⟩. i∈n}"

from A2 `N ∈ FinPow(n)` `W∈N->T` have "∀i∈n. (if i∈N then W`(i) else \<Union>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->\<Union>T,?W⇩_{n})"

proof

{ fix x assume "x∈B"

with `B = FinProd(n->\<Union>T,W)` have "x ∈ n->\<Union>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->\<Union>T` have "x`(i) ∈ \<Union>T" using apply_funtype by blast

with `x∈B` `B = FinProd(n->\<Union>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->\<Union>T,?W⇩_{n})" using FinProd_def by simp

} thus "B ⊆ FinProd(n->\<Union>T,?W⇩_{n})" by auto

next

{ fix x assume "x ∈ FinProd(n->\<Union>T,?W⇩_{n})"

then have "x ∈ n->\<Union>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->\<Union>T` `B = FinProd(n->\<Union>T,W)` have "x∈B"

using func1_1_L1 FinProd_def by simp

} thus "FinProd(n->\<Union>T,?W⇩_{n}) ⊆ B" by auto

qed

ultimately have "B ∈ {FinProd(n->\<Union>T,W). W∈n->T}" by auto

} thus "ProductTopBase(n,T) ⊆ {FinProd(n->\<Union>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->\<Union>τ,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->\<Union>τ,W) = {x ∈ 1->\<Union>τ. x`(0) ∈ W`(0)}"

using FinProd_def by simp

also have "{x ∈ 1->\<Union>τ. x`(0) ∈ W`(0)} = { {⟨0,y⟩}. y ∈ W`(0)}"

proof

from `1 = {0}` show "{x ∈ 1->\<Union>τ. 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 ∈ \<Union>τ" using apply_funtype by auto

with `x = {⟨0,y⟩}` `1 = {0}` have "x:1->\<Union>τ" using pair_func_singleton

by auto

with `x = {⟨0,y⟩}` II have "x ∈ {x ∈ 1->\<Union>τ. x`(0) ∈ W`(0)}"

using pair_val by simp

} thus "{ {⟨0,y⟩}. y ∈ W`(0)} ⊆ {x ∈ 1->\<Union>τ. 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 ∈ \<Union>τ})"

proof -

have "{0} = 1" by auto

let ?b = "{⟨y,{⟨0,y⟩}⟩.y ∈ \<Union>τ}"

have "?b ∈ bij(\<Union>τ,1->\<Union>τ)" 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(\<Union>τ,1->\<Union>τ)` have "?b:\<Union>τ->(1->\<Union>τ)" using bij_def inj_def

by simp

{ fix y assume "y ∈ \<Union>τ"

with `?b:\<Union>τ->(1->\<Union>τ)` have "?b`(y) = {⟨0,y⟩}" using ZF_fun_from_tot_val

by simp

} hence "∀y ∈ \<Union>τ. ?b`(y) = {⟨0,y⟩}" by auto

with `U∈τ` `?b:\<Union>τ->(1->\<Union>τ)` 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->\<Union>τ,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->\<Union>τ,?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 ∈ \<Union>τ})" by auto

qed

text{* A special corner case of @{text "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->\<Union>τ})"

proof -

have "{⟨x,x`(0)⟩. x∈1->\<Union>τ} = converse({⟨y,{⟨0,y⟩}⟩.y∈\<Union>τ})"

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 "(\<Union>ProductTopology(T,τ)) = (n->\<Union>τ)×\<Union>τ"

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)->\<Union>τ. Init(x) ∈ U ∧ x`(n) ∈ V} ∈ ProductTopBase(succ(n),τ)"

proof -

let ?B = "{x ∈ succ(n)->\<Union>τ. Init(x) ∈ U ∧ x`(n) ∈ V}"

from A1 A2 have "ProductTopBase(n,τ) = {FinProd(n->\<Union>τ,W). W∈n->τ}"

using fin_prod_def_nat by simp

with A3 obtain W⇩_{U}where "W⇩_{U}:n->τ" and "U =FinProd(n->\<Union>τ,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)->\<Union>τ,?W)"

proof

{ fix x assume "x∈?B"

with `?W:succ(n)->τ` have "x ∈ succ(n)->\<Union>τ" and "domain(?W) = succ(n)" using func1_1_L1

by auto

moreover from A2 A4 `x∈?B` `U =FinProd(n->\<Union>τ,W⇩_{U})` `W⇩_{U}:n->τ` `x ∈ succ(n)->\<Union>τ`

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)->\<Union>τ,?W)" using FinProd_def by simp

} thus "?B ⊆ FinProd(succ(n)->\<Union>τ,?W)" by auto

next

{ fix x assume "x ∈ FinProd(succ(n)->\<Union>τ,?W)"

then have "x:succ(n)->\<Union>τ" 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)->\<Union>τ` have "Init(x):n->\<Union>τ" using init_props by simp

moreover have "∀i∈domain(W⇩_{U}). Init(x)`(i) ∈ W⇩_{U}`(i)"

proof -

from A2 `x ∈ FinProd(succ(n)->\<Union>τ,?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)->\<Union>τ` 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->\<Union>τ,W⇩_{U})" using FinProd_def by simp

with `U =FinProd(n->\<Union>τ,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)->\<Union>τ,?W) ⊆ ?B" by auto

qed

moreover from A1 A2 have

"ProductTopBase(succ(n),τ) = {FinProd(succ(n)->\<Union>τ,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)->\<Union>τ. 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 "∃\<B> ∈ Pow(ProductTopBase(n,τ)). U = \<Union>\<B>" using Top_1_2_L1 by simp

then obtain \<B> where "\<B> ⊆ ProductTopBase(n,τ)" and "U = \<Union>\<B>" by auto

then have

"{x:succ(n)->\<Union>τ. Init(x) ∈ U ∧ x`(n) ∈ V} = (\<Union>B∈\<B>.{x:succ(n)->\<Union>τ. Init(x) ∈ B ∧ x`(n) ∈ V})"

by auto

moreover from A1 A2 A4 `\<B> ⊆ ProductTopBase(n,τ)` have

"∀B∈\<B>. ({x:succ(n)->\<Union>τ. Init(x) ∈ B ∧ x`(n) ∈ V} ∈ ProductTopBase(succ(n),τ))"

using finite_prod_succ_base by auto

with I II have

"(\<Union>B∈\<B>.{x:succ(n)->\<Union>τ. 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 @{text "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 @{text "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)->\<Union>τ}" 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(\<Union>S,\<Union>ProductTopology(T,τ))"

using lists_cart_prod seq_prod_top_is_top Top_1_4_T1 by simp

then have "f: \<Union>S->\<Union>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(\<Union>S,\<Union>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: \<Union>S->\<Union>ProductTopology(T,τ)` have "f: (succ(n)->\<Union>τ)->\<Union>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)->\<Union>τ,W⇩_{V})"

using fin_prod_def_nat by auto

let ?U = "FinProd(n->\<Union>τ,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 ⊆ \<Union>S" using IsAbaseFor_def by auto

with `f: \<Union>S->\<Union>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)->\<Union>τ,W⇩_{V})` have "V ⊆ \<Union>S" and

fdef: "f = {⟨x,⟨Init(x),x`(n)⟩⟩. x ∈ \<Union>S}" using seq_prod_top_is_top FinProd_def

by auto

from `f: \<Union>S->\<Union>ProductTopology(T,τ)` fdef have "∀x ∈ \<Union>S. f`(x) = ⟨Init(x),x`(n)⟩"

by (rule ZF_fun_from_tot_val0)

with `V ⊆ \<Union>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)->\<Union>τ,W⇩_{V})` have

"x:succ(n)->\<Union>τ" 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)->\<Union>τ` have "Init(x): n->\<Union>τ" 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->\<Union>τ" 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) ∈ \<Union>τ" by auto

let ?x = "Append(fst(y),snd(y))"

have "?x∈V"

proof -

from `fst(y): n->\<Union>τ` `snd(y) ∈ \<Union>τ` have "?x:succ(n)->\<Union>τ" using append_props by simp

moreover have "∀i∈domain(W⇩_{V}). ?x`(i) ∈ W⇩_{V}`(i)"

proof -

from `fst(y): n->\<Union>τ` `snd(y) ∈ \<Union>τ`

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)->\<Union>τ,W⇩_{V})" using FinProd_def by simp

with `V = FinProd(succ(n)->\<Union>τ,W⇩_{V})` show "?x∈V" by simp

qed

moreover from A2 `y ∈ ?U×?W` `fst(y): n->\<Union>τ` `snd(y) ∈ \<Union>τ` 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