(* 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. *) section ‹Topology 3› 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.*} 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 @{text "ProductTopBase(𝒳,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 "⋃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 @{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→⋃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 @{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→⋃τ})" 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 @{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)→⋃τ}" 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