# 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 APARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT,INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOTLIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES LOSS OF USE, DATA, OR PROFITS ORBUSINESS 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 THEUSE 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_ZFbegintext{* @{text "Topology_ZF_1"} theory describes how we can define  a topology on a productof two topological spaces. One way to generalize that is to construct topology for a cartesianproduct 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 wantto 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 simpqed 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 simptext{*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 simpqedsection{*Finite product of topologies*}text{*As a special case of the space of functions $I\rightarrow X$ we can consider space of listsof 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 autoqedtext{*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 qedtext{*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 autoqedtext{* 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 simpqed  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 simptext{*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 qedtext{* 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