Theory Topology_ZF_3

theory Topology_ZF_3
imports Topology_ZF_2 FiniteSeq_ZF
(* 
    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 N1  W1 N2 W2 where 
    I: "N1 ∈ FinPow(I)"  "W1∈N1->T"  "U = FinProd(?\<X>,W1)" and
    II: "N2 ∈ FinPow(I)"  "W2∈N2->T"  "V = FinProd(?\<X>,W2)"
    using ProductTopBase_def by auto
  let ?N3 = "N1 ∪ N2"
  let ?W3 = "{⟨i,if i ∈ N1-N2 then W1`(i) 
        else if i ∈ N2-N1 then  W2`(i) 
        else (W1`(i)) ∩ (W2`(i))⟩. i ∈ ?N3}"
  from A1 I II have "∀i ∈ N1 ∩ N2.  (W1`(i) ∩ W2`(i)) ∈ T"
      using apply_funtype IsATopology_def by auto
  moreover from I II have "∀i∈N1-N2. W1`(i) ∈ T" and "∀i∈N2-N1. W2`(i) ∈ T" 
      using apply_funtype by auto
  ultimately have  "?W3:?N3->T" by (rule fun_union_overlap)
  with I II have "FinProd(?\<X>,?W3) ∈ ProductTopBase(I,T)" using union_finpow ProductTopBase_def
    by auto
  moreover have "U∩V = FinProd(?\<X>,?W3)"
  proof
    { fix x assume "x∈U" and "x∈V"
      with `U = FinProd(?\<X>,W1)`  `W1∈N1->T` and  `V = FinProd(?\<X>,W2)`  `W2∈N2->T`
      have "x∈?\<X>" and "∀i∈N1. x`(i) ∈ W1`(i)" and "∀i∈N2. x`(i) ∈ W2`(i)"
        using func1_1_L1 FinProd_def by auto
      with `?W3:?N3->T` `x∈?\<X>` have "x ∈ FinProd(?\<X>,?W3)"  
        using ZF_fun_from_tot_val func1_1_L1 FinProd_def by auto
    } thus "U∩V ⊆ FinProd(?\<X>,?W3)" by auto
    { fix x assume "x ∈ FinProd(?\<X>,?W3)"
      with `?W3:?N3->T` have "x:I->\<Union>T" and III: "∀i∈?N3. x`(i) ∈ ?W3`(i)"
        using FinProd_def func1_1_L1 by auto
     { fix i assume "i∈N1" 
       with `?W3:?N3->T` have "?W3`(i) ⊆ W1`(i)" using ZF_fun_from_tot_val by auto
       with III `i∈N1` have "x`(i) ∈ W1`(i)" by auto
     } with `W1∈N1->T` `x:I->\<Union>T` `U = FinProd(?\<X>,W1)` 
      have "x ∈ U" using func1_1_L1 FinProd_def by auto
      moreover
      { fix i assume "i∈N2" 
        with `?W3:?N3->T` have "?W3`(i) ⊆ W2`(i)" using ZF_fun_from_tot_val by auto
        with III `i∈N2` have "x`(i) ∈ W2`(i)" by auto
      } with `W2∈N2->T` `x:I->\<Union>T` `V = FinProd(?\<X>,W2)` have "x∈V" 
          using func1_1_L1 FinProd_def by auto 
      ultimately have "x ∈ U∩V" by simp
    } thus "FinProd(?\<X>,?W3) ⊆ 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 ?Wn = "{⟨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 "?Wn:n->T" by (rule ZF_fun_from_total)
    moreover have "B = FinProd(n->\<Union>T,?Wn)"
    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(?Wn). x`(i) ∈ ?Wn`(i)"
        proof
          fix i assume "i ∈ domain(?Wn)"
          with `?Wn: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` `?Wn:n->T` `i∈n`
          show "x`(i) ∈ ?Wn`(i)" using func1_1_L1 FinProd_def ZF_fun_from_tot_val 
            by simp
        qed
        ultimately have "x ∈ FinProd(n->\<Union>T,?Wn)" using FinProd_def by simp
      } thus "B ⊆ FinProd(n->\<Union>T,?Wn)" by auto
      next
      { fix x assume "x ∈ FinProd(n->\<Union>T,?Wn)"    
        then have "x ∈ n->\<Union>T" and "∀i∈domain(?Wn). x`(i) ∈ ?Wn`(i)" 
          using  FinProd_def by auto
        with `?Wn:n->T` and `N ∈ FinPow(n)` have "∀i∈N. x`(i) ∈ ?Wn`(i)"
          using func1_1_L1 FinPow_def by auto
        moreover from `?Wn:n->T` and `N ∈ FinPow(n)` 
        have "∀i∈N. ?Wn`(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,?Wn) ⊆ 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 WU where "WU:n->τ" and "U =FinProd(n->\<Union>τ,WU)" by auto
    let ?W = "Append(WU,V)"
    from A4 and `WU: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>τ,WU)` `WU: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(WU). Init(x)`(i) ∈ WU`(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 `WU:n->τ` have "∀i∈n. ?W`(i) =  WU`(i)"
              using append_props by simp
            ultimately have "∀i∈n. Init(x)`(i) ∈ WU`(i)" by simp
            with `WU:n->τ` show ?thesis using func1_1_L1 by simp 
          qed
          ultimately have "Init(x) ∈ FinProd(n->\<Union>τ,WU)" using FinProd_def by simp
          with `U =FinProd(n->\<Union>τ,WU)` 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 `WU: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 WV where "WV ∈ succ(n)->τ" and "V = FinProd(succ(n)->\<Union>τ,WV)" 
      using fin_prod_def_nat by auto
    let ?U = "FinProd(n->\<Union>τ,Init(WV))"
    let ?W = "WV`(n)"
    have "?U ∈ T"
    proof - 
      from A1 A2 `WV ∈ 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 `WV ∈ 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 `WV: succ(n)->τ` have "Init(WV): n->τ" and III: "∀k∈n. Init(WV)`(k) = WV`(k)" 
        using init_props by auto
      then have "domain(Init(WV)) = 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>τ,WV)` 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>τ,WV)` have 
            "x:succ(n)->\<Union>τ" and II: "∀k∈domain(WV). x`(k) ∈ WV`(k)" 
            unfolding FinProd_def by auto
          with A2 `WV: 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(WV)). Init(x)`(k) ∈ Init(WV)`(k)"
            proof -
              from A2 `WV: succ(n)->τ` have "Init(WV): n->τ" using init_props by simp
              then have "domain(Init(WV)) = n" using func1_1_L1 by simp
              note III IV  `domain(Init(WV)) = n`
              moreover from II `WV ∈ succ(n)->τ` have "∀k∈n. x`(k) ∈ WV`(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 `WV: 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(WV)) = n` have "fst(y): n->\<Union>τ" and 
            V: "∀k∈n. fst(y)`(k) ∈ Init(WV)`(k)"
            using FinProd_def by auto
          from `WV: 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(WV). ?x`(i) ∈ WV`(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) ∈ WV`(k)" by simp 
              moreover note `snd(y) ∈ ?W`
              ultimately have "∀i∈succ(n). ?x`(i) ∈ WV`(i)" by simp
              with `WV ∈ succ(n)->τ` show ?thesis using func1_1_L1 by simp 
            qed
            ultimately have "?x ∈ FinProd(succ(n)->\<Union>τ,WV)" using FinProd_def by simp
            with `V = FinProd(succ(n)->\<Union>τ,WV)` 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