# Theory Topology_ZF_1

Up to index of Isabelle/ZF/IsarMathLib

theory Topology_ZF_1
imports Topology_ZF
(*     This file is a part of IsarMathLib -     a library of formalized mathematics for Isabelle/Isar.    Copyright (C) 2005 - 2008  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\_1.thy}*}theory Topology_ZF_1 imports Topology_ZFbegintext{*In this theory file we study separation axioms and the notion of base and  subbase. Using the products of open sets as a subbase we define a natural  topology on a product of two topological spaces. *}section{*Separation axioms.*}text{*Topological spaces cas be classified according to certain properties  called "separation axioms". In this section we define what it means that a   topological space is $T_0$, $T_1$ or $T_2$.*}text{*A topology on $X$ is $T_0$ if for every pair of distinct points of $X$  there is an open set that contains only one of them. *}definition  isT0 ("_ {is T⇣0}" [90] 91) where  "T {is T⇣0} ≡ ∀ x y. ((x ∈ \<Union>T ∧ y ∈ \<Union>T ∧  x≠y) -->   (∃U∈T. (x∈U ∧ y∉U) ∨ (y∈U ∧ x∉U)))"text{* A topology is $T_1$ if for every such pair there exist an open set that   contains the first point but not the second.*}definition  isT1 ("_ {is T⇣1}" [90] 91) where  "T {is T⇣1} ≡ ∀ x y. ((x ∈ \<Union>T ∧ y ∈ \<Union>T ∧  x≠y) -->   (∃U∈T. (x∈U ∧ y∉U)))"text{* A topology is $T_2$ (Hausdorff) if for every pair of points there exist a   pair of disjoint open sets each containing one of the points.   This is an important class of topological spaces. In particular, metric   spaces are Hausdorff.*}definition  isT2 ("_ {is T⇣2}" [90] 91) where  "T {is T⇣2} ≡ ∀ x y. ((x ∈ \<Union>T ∧ y ∈ \<Union>T ∧  x≠y) -->  (∃U∈T. ∃V∈T. x∈U ∧ y∈V ∧ U∩V=0))"text{*If a topology is $T_1$ then it is $T_0$.   We don't really assume here that $T$ is a topology on $X$.   Instead, we prove the relation between isT0 condition and isT1. *}lemma T1_is_T0: assumes A1: "T {is T⇣1}" shows "T {is T⇣0}"proof -  from A1 have "∀ x y. x ∈ \<Union>T ∧ y ∈ \<Union>T ∧ x≠y -->     (∃U∈T. x∈U ∧ y∉U)"    using isT1_def by simp  then have "∀ x y. x ∈ \<Union>T ∧ y ∈ \<Union>T ∧ x≠y -->     (∃U∈T. x∈U ∧ y∉U ∨ y∈U ∧ x∉U)"    by auto  then show "T {is T⇣0}" using isT0_def by simpqedtext{*If a topology is $T_2$ then it is $T_1$.*}lemma T2_is_T1: assumes A1: "T {is T⇣2}" shows "T {is T⇣1}"proof -  { fix x y assume "x ∈ \<Union>T"  "y ∈ \<Union>T"  "x≠y"    with A1 have "∃U∈T. ∃V∈T. x∈U ∧ y∈V ∧ U∩V=0"      using isT2_def by auto    then have "∃U∈T. x∈U ∧ y∉U" by auto  } then have "∀ x y. x ∈ \<Union>T ∧ y ∈ \<Union>T ∧  x≠y -->       (∃U∈T. x∈U ∧ y∉U)" by simp  then show "T {is T⇣1}" using isT1_def by simpqedtext{*In a $T_0$ space two points that can not be separated   by an open set are equal. Proof by contradiction.*}lemma Top_1_1_L1: assumes A1: "T {is T⇣0}" and A2: "x ∈ \<Union>T"  "y ∈ \<Union>T"  and A3: "∀U∈T. (x∈U <-> y∈U)"   shows "x=y"proof -  { assume "x≠y"    with A1 A2 have "∃U∈T. x∈U ∧ y∉U ∨ y∈U ∧ x∉U"      using isT0_def by simp    with A3 have False by auto  } then show "x=y" by autoqedsection{*Bases and subbases.*}text{*Sometimes it is convenient to talk about topologies in terms of their bases  and subbases. These are certain collections of open sets that define  the whole topology.*}text{*A base of topology is a collection of open sets such that every   open set is a union of the sets from the base.*}definition  IsAbaseFor (infixl "{is a base for}" 65) where   "B {is a base for} T ≡ B⊆T ∧ T = {\<Union>A. A∈Pow(B)}"text{* A subbase is a collection   of open sets such that finite intersection of those sets form a base.*}definition  IsAsubBaseFor (infixl "{is a subbase for}" 65) where  "B {is a subbase for} T ≡   B ⊆ T ∧ {\<Inter>A. A ∈ FinPow(B)} {is a base for} T"text{*Below we formulate a condition that we will prove to be necessary and   sufficient for a collection $B$ of open sets to form a base.   It says that for any two sets $U,V$ from the collection $B$ we can  find a point $x\in U\cap V$ with a neighboorhod   from $B$ contained in $U\cap V$.*}definition  SatisfiesBaseCondition ("_ {satisfies the base condition}" [50] 50)  where  "B {satisfies the base condition} ≡   ∀U V. ((U∈B ∧ V∈B) --> (∀x ∈ U∩V. ∃W∈B. x∈W ∧ W ⊆ U∩V))"text{*A collection that is closed with respect to intersection  satisfies the base condition.*}lemma inter_closed_base: assumes "∀U∈B.(∀V∈B. U∩V ∈ B)"  shows  "B {satisfies the base condition}" proof -    { fix U V x assume "U∈B" and "V∈B" and "x ∈ U∩V"      with assms have "∃W∈B. x∈W ∧ W ⊆ U∩V" by blast    } then show ?thesis using SatisfiesBaseCondition_def by simpqedtext{*Each open set is a union of some sets from the base.*}lemma Top_1_2_L1: assumes "B {is a base for} T"  and "U∈T"   shows "∃A∈Pow(B). U = \<Union>A"  using assms IsAbaseFor_def by simptext{* Elements of base are open. *}lemma base_sets_open:   assumes "B {is a base for} T" and "U ∈ B"  shows "U ∈ T"  using assms IsAbaseFor_def by auto;text{*A base defines topology uniquely.*}lemma same_base_same_top:   assumes "B {is a base for} T" and "B {is a base for} S"   shows "T = S"  using assms IsAbaseFor_def by simp;text{*Every point from an open set has a neighboorhood from the base  that is contained in the set.*}lemma point_open_base_neigh:   assumes A1: "B {is a base for} T" and A2: "U∈T" and A3: "x∈U"  shows "∃V∈B. V⊆U ∧ x∈V"proof -  from A1 A2 obtain A where "A ∈ Pow(B)" and "U = \<Union>A"    using Top_1_2_L1 by blast;  with A3 obtain V where "V∈A" and "x∈V" by auto;  with A ∈ Pow(B) U = \<Union>A show ?thesis by auto;qed;text{* A criterion for a collection to be a base for a topology  that is a slight reformulation of the definition. The only thing  different that in the definition is that we assume only that  every open set is a union of some sets from the base. The definition  requires also the opposite inclusion that every union of the   sets from the base is open, but that we can prove if we assume that  $T$ is a topology.*}lemma is_a_base_criterion: assumes A1: "T {is a topology}"  and A2: "B ⊆ T" and A3: "∀V ∈ T. ∃A ∈ Pow(B). V = \<Union>A"  shows "B {is a base for} T"proof -  from A3 have "T ⊆ {\<Union>A. A∈Pow(B)}" by auto;  moreover have "{\<Union>A. A∈Pow(B)} ⊆ T"  proof;    fix U assume "U ∈ {\<Union>A. A∈Pow(B)}"    then obtain A where "A ∈ Pow(B)" and "U = \<Union>A"      by auto;    with B ⊆ T have "A ∈ Pow(T)" by auto;    with A1 U = \<Union>A show "U ∈ T"      unfolding IsATopology_def by simp;  qed  ultimately have "T = {\<Union>A. A∈Pow(B)}" by auto;  with A2 show "B {is a base for} T"     unfolding IsAbaseFor_def by simp;qed;    text{*A necessary condition for a collection of sets to be a base for some   topology : every point in the intersection  of two sets in the base has a neighboorhood from the base contained  in the intersection.*}lemma Top_1_2_L2:   assumes A1:"∃T. T {is a topology} ∧ B {is a base for} T"  and A2: "V∈B"  "W∈B"  shows "∀ x ∈ V∩W. ∃U∈B. x∈U ∧ U ⊆ V ∩ W"proof -  from A1 obtain T where     D1: "T {is a topology}"   "B {is a base for} T"    by auto  then have "B ⊆ T" using IsAbaseFor_def by auto  with A2 have "V∈T" and "W∈T" using IsAbaseFor_def by auto  with D1 have "∃A∈Pow(B). V∩W = \<Union>A" using IsATopology_def Top_1_2_L1    by auto  then obtain A where "A ⊆ B" and "V ∩ W = \<Union>A" by auto  then show "∀ x ∈ V∩W. ∃U∈B. (x∈U ∧ U ⊆ V ∩ W)" by autoqedtext{*We will construct a topology as the collection of unions of (would-be)  base. First we prove that if the collection of sets satisfies the   condition we want to show to be sufficient, the the intersection belongs  to what we will define as topology (am I clear here?). Having this fact   ready simplifies the proof of the next lemma. There is not much topology  here, just some set theory.*}lemma Top_1_2_L3:  assumes A1: "∀x∈ V∩W . ∃U∈B. x∈U ∧ U ⊆ V∩W"  shows "V∩W ∈ {\<Union>A. A∈Pow(B)}"proof  let ?A = "\<Union>x∈V∩W. {U∈B. x∈U ∧ U ⊆ V∩W}"  show "?A∈Pow(B)" by auto  from A1 show "V∩W = \<Union>?A" by blastqedtext{*The next lemma is needed when proving that the would-be topology is  closed with respect to taking intersections. We show here that intersection  of two sets from this (would-be) topology can be written as union of sets   from the topology.*}lemma Top_1_2_L4:  assumes A1:  "U⇣1 ∈ {\<Union>A. A∈Pow(B)}"   "U⇣2 ∈ {\<Union>A. A∈Pow(B)}"  and A2: "B {satisfies the base condition}"  shows "∃C. C ⊆ {\<Union>A. A∈Pow(B)} ∧ U⇣1∩U⇣2 = \<Union>C"proof -  from A1 A2 obtain A⇣1 A⇣2 where     D1: "A⇣1∈ Pow(B)"  "U⇣1 = \<Union>A⇣1"  "A⇣2 ∈ Pow(B)"  "U⇣2 = \<Union>A⇣2"     by auto  let ?C = "\<Union>U∈A⇣1.{U∩V. V∈A⇣2}"  from D1 have "(∀U∈A⇣1. U∈B) ∧ (∀V∈A⇣2. V∈B)" by auto  with A2 have "?C ⊆ {\<Union>A . A ∈ Pow(B)}"    using Top_1_2_L3 SatisfiesBaseCondition_def by auto  moreover from D1 have "U⇣1 ∩ U⇣2 = \<Union>?C" by auto  ultimately show ?thesis by autoqedtext{*If $B$ satisfies the base condition, then the collection of unions  of sets from $B$ is a topology and $B$ is a base for this topology.*}theorem Top_1_2_T1:  assumes A1: "B {satisfies the base condition}"  and A2: "T = {\<Union>A. A∈Pow(B)}"  shows "T {is a topology}" and "B {is a base for} T"proof -  show "T {is a topology}"  proof -    have I: "∀C∈Pow(T). \<Union>C ∈ T"    proof -      { fix C assume A3: "C ∈ Pow(T)"        let ?Q = "\<Union> {\<Union>{A∈Pow(B). U = \<Union>A}. U∈C}"        from A2 A3 have "∀U∈C. ∃A∈Pow(B). U = \<Union>A" by auto        then have "\<Union>?Q = \<Union>C" using ZF1_1_L10 by simp        moreover from A2 have "\<Union>?Q ∈ T" by auto        ultimately have "\<Union>C ∈ T" by simp      } thus "∀C∈Pow(T). \<Union>C ∈ T" by auto    qed    moreover have "∀U∈T. ∀ V∈T. U∩V ∈ T"    proof -      { fix U V assume  "U ∈ T"  "V ∈ T"        with A1 A2 have "∃C.(C ⊆ T ∧ U∩V = \<Union>C)"        using Top_1_2_L4 by simp        then obtain C where "C ⊆ T" and  "U∩V = \<Union>C"          by auto          with I have "U∩V ∈ T" by simp      } then show "∀U∈T. ∀ V∈T. U∩V ∈ T" by simp    qed    ultimately show "T {is a topology}" using IsATopology_def      by simp  qed  from A2 have "B⊆T" by auto  with A2 show "B {is a base for} T" using IsAbaseFor_def     by simpqed;text{*The carrier of the base and topology are the same.*}lemma Top_1_2_L5: assumes "B {is a base for} T"  shows "\<Union>T = \<Union>B"  using assms IsAbaseFor_def by autotext{*If $B$ is a base for $T$, then $T$ is the smallest topology containing $B$.  *}lemma base_smallest_top:   assumes A1: "B {is a base for} T" and  A2: "S {is a topology}" and A3: "B⊆S"  shows "T⊆S"proof  fix U assume "U∈T"  with A1 obtain B⇣U where "B⇣U ⊆ B" and "U = \<Union>B⇣U" using IsAbaseFor_def by auto  with A3 have "B⇣U ⊆ S" by auto   with A2 U = \<Union>B⇣U show "U∈S" using IsATopology_def by simpqedtext{*If $B$ is a base for $T$ and $B$ is a topology, then $B=T$.*}lemma base_topology: assumes "B {is a topology}" and "B {is a base for} T"  shows "B=T" using assms base_sets_open base_smallest_top by blast section{*Product topology*}text{*In this section we consider a topology defined on a product of two sets.*}text{*Given two topological spaces we can define a topology on the product of   the carriers such that the cartesian products of the sets of the topologies   are a base for the product topology. Recall that for two collections $S,T$   of sets the product collection  is defined (in @{text "ZF1.thy"}) as the collections of cartesian   products $A\times B$, where $A\in S, B\in T$.*}definition  "ProductTopology(T,S) ≡ {\<Union>W. W ∈ Pow(ProductCollection(T,S))}"text{*The product collection satisfies the base condition.*}lemma Top_1_4_L1:   assumes A1: "T {is a topology}"   "S {is a topology}"  and A2: "A ∈ ProductCollection(T,S)"  "B ∈ ProductCollection(T,S)"  shows "∀x∈(A∩B). ∃W∈ProductCollection(T,S). (x∈W ∧ W ⊆ A ∩ B)"proof  fix x assume A3: "x ∈ A∩B"  from A2 obtain U⇣1 V⇣1 U⇣2 V⇣2 where     D1: "U⇣1∈T"  "V⇣1∈S"   "A=U⇣1×V⇣1"  "U⇣2∈T"  "V⇣2∈S"   "B=U⇣2×V⇣2"    using ProductCollection_def by auto  let ?W = "(U⇣1∩U⇣2) × (V⇣1∩V⇣2)"  from A1 D1 have "U⇣1∩U⇣2 ∈ T" and "V⇣1∩V⇣2 ∈ S"    using IsATopology_def by auto  then have "?W ∈ ProductCollection(T,S)" using ProductCollection_def     by auto  moreover from A3 D1 have "x∈?W" and "?W ⊆ A∩B" by auto  ultimately have "∃W. (W ∈ ProductCollection(T,S) ∧ x∈W ∧ W ⊆ A∩B)"    by auto  thus "∃W∈ProductCollection(T,S). (x∈W ∧ W ⊆ A ∩ B)" by autoqedtext{*The product topology is indeed a topology on the product.*}theorem Top_1_4_T1: assumes A1: "T {is a topology}"  "S {is a topology}"  shows   "ProductTopology(T,S) {is a topology}"  "ProductCollection(T,S) {is a base for} ProductTopology(T,S)"  "\<Union> ProductTopology(T,S) = \<Union>T × \<Union>S"proof -  from A1 show     "ProductTopology(T,S) {is a topology}"    "ProductCollection(T,S) {is a base for} ProductTopology(T,S)"    using Top_1_4_L1 ProductCollection_def       SatisfiesBaseCondition_def ProductTopology_def Top_1_2_T1     by auto  then show "\<Union> ProductTopology(T,S) = \<Union>T × \<Union>S"    using Top_1_2_L5 ZF1_1_L6 by simpqedtext{*Each point of a set open in the product topology has a neighborhood  which is a cartesian product of open sets.*}lemma prod_top_point_neighb:   assumes A1: "T {is a topology}"  "S {is a topology}" and   A2: "U ∈ ProductTopology(T,S)" and A3: "x ∈ U"  shows "∃V W. V∈T ∧ W∈S ∧ V×W ⊆ U ∧ x ∈ V×W"proof -  from A1 have     "ProductCollection(T,S) {is a base for} ProductTopology(T,S)"    using Top_1_4_T1 by simp;  with A2 A3 obtain Z where     "Z ∈ ProductCollection(T,S)" and "Z ⊆ U ∧ x∈Z"    using point_open_base_neigh by blast;  then obtain V W where "V ∈ T" and "W∈S" and" V×W ⊆ U ∧ x ∈ V×W"    using ProductCollection_def by auto;  thus ?thesis by auto;qedtext{*Products of open sets are open in the product topology.*}lemma prod_open_open_prod:   assumes A1: "T {is a topology}"  "S {is a topology}" and  A2: "U∈T" "V∈S"  shows "U×V ∈ ProductTopology(T,S)"proof -  from A1 have     "ProductCollection(T,S) {is a base for} ProductTopology(T,S)"    using Top_1_4_T1 by simp;  moreover from A2 have "U×V ∈ ProductCollection(T,S)"    unfolding ProductCollection_def by auto;  ultimately show "U×V ∈ ProductTopology(T,S)"    using base_sets_open by simp;qedtext{*Sets that are open in th product topology are contained in the product  of the carrier.*}lemma prod_open_type: assumes A1: "T {is a topology}"  "S {is a topology}" and  A2: "V ∈ ProductTopology(T,S)"  shows "V ⊆ \<Union>T × \<Union>S"proof -  from A2 have "V ⊆ \<Union> ProductTopology(T,S)" by auto  with A1 show ?thesis using Top_1_4_T1 by simpqedtext{*Suppose we have subsets $A\subseteq X, B\subseteq Y$, where  $X,Y$ are topological spaces with topologies $T,S$. We can the consider  relative topologies on $T_A, S_B$ on sets $A,B$ and the collection  of cartesian products of sets open in $T_A, S_B$, (namely   $\{U\times V: U\in T_A, V\in S_B\}$. The next lemma states that  this collection is a base of the product topology on $X\times Y$  restricted to the product $A\times B$.  *}lemma prod_restr_base_restr:  assumes A1: "T {is a topology}"  "S {is a topology}"  shows   "ProductCollection(T {restricted to} A, S {restricted to} B)  {is a base for} (ProductTopology(T,S) {restricted to} A×B)"proof -;  let ?\<B> = "ProductCollection(T {restricted to} A, S {restricted to} B)"  let ?τ = "ProductTopology(T,S)"  from A1 have "(?τ {restricted to} A×B) {is a topology}"    using Top_1_4_T1 topology0_def topology0.Top_1_L4    by simp;  moreover have "?\<B> ⊆ (?τ {restricted to} A×B)"  proof    fix U assume "U ∈ ?\<B>"    then obtain U⇣A U⇣B where "U = U⇣A × U⇣B" and      "U⇣A ∈ (T {restricted to} A)" and "U⇣B ∈ (S {restricted to} B)"      using ProductCollection_def by auto;    then obtain W⇣A W⇣B where       "W⇣A ∈ T"  "U⇣A = W⇣A ∩ A" and "W⇣B ∈ S"  "U⇣B = W⇣B ∩ B"      using RestrictedTo_def by auto;    with U = U⇣A × U⇣B have "U = W⇣A×W⇣B ∩ (A×B)" by auto;    moreover from A1 W⇣A ∈ T and W⇣B ∈ S have "W⇣A×W⇣B ∈ ?τ"      using prod_open_open_prod by simp;    ultimately show "U ∈ ?τ {restricted to} A×B"      using RestrictedTo_def by auto;  qed;  moreover have "∀U ∈ ?τ {restricted to} A×B.    ∃C ∈ Pow(?\<B>). U = \<Union>C"  proof;    fix U assume "U ∈ ?τ {restricted to} A×B"    then obtain W where "W ∈ ?τ" and "U = W ∩ (A×B)"      using RestrictedTo_def by auto;    from A1 W ∈ ?τ obtain A⇣W  where       "A⇣W ∈ Pow(ProductCollection(T,S))" and "W = \<Union>A⇣W"       using Top_1_4_T1 IsAbaseFor_def by auto;    let ?C = "{V ∩ A×B. V ∈ A⇣W}"     have "?C ∈ Pow(?\<B>)" and "U = \<Union>?C"    proof -      { fix R assume "R ∈ ?C"	then obtain V where "V ∈ A⇣W" and "R = V ∩ A×B"	  by auto;	with A⇣W ∈ Pow(ProductCollection(T,S)) obtain V⇣T V⇣S where 	  "V⇣T ∈ T" and "V⇣S ∈ S" and "V = V⇣T × V⇣S"	  using ProductCollection_def by auto;	with R = V ∩ A×B have "R ∈ ?\<B>"	  using ProductCollection_def RestrictedTo_def	  by auto;      } then show "?C ∈ Pow(?\<B>)" by auto;      from U = W ∩ (A×B) and W = \<Union>A⇣W      show "U = \<Union>?C" by auto;    qed;    thus "∃C ∈ Pow(?\<B>). U = \<Union>C" by blast;  qed;  ultimately show ?thesis by (rule is_a_base_criterion);qed;    text{*We can commute taking restriction (relative topology) and  product topology. The reason the two topologies are the same is  that they have the same base.*}lemma prod_top_restr_comm:   assumes A1: "T {is a topology}"  "S {is a topology}"  shows  "ProductTopology(T {restricted to} A,S {restricted to} B) =  ProductTopology(T,S) {restricted to} (A×B)"proof -  let ?\<B> = "ProductCollection(T {restricted to} A, S {restricted to} B)"  from A1 have    "?\<B> {is a base for} ProductTopology(T {restricted to} A,S {restricted to} B)"    using topology0_def topology0.Top_1_L4 Top_1_4_T1 by simp;  moreover from A1 have     "?\<B> {is a base for} ProductTopology(T,S) {restricted to} (A×B)"    using prod_restr_base_restr by simp;  ultimately show ?thesis by (rule same_base_same_top);qedtext{*Projection of a section of an open set is open.*}lemma prod_sec_open1: assumes A1: "T {is a topology}"  "S {is a topology}" and  A2: "V ∈ ProductTopology(T,S)" and A3: "x ∈ \<Union>T"  shows "{y ∈ \<Union>S. ⟨x,y⟩ ∈ V} ∈ S"proof -  let ?A = "{y ∈ \<Union>S. ⟨x,y⟩ ∈ V}"  from A1 have "topology0(S)" using topology0_def by simp  moreover have "∀y∈?A.∃W∈S. (y∈W ∧ W⊆?A)"    proof      fix y assume "y ∈ ?A"      then have "⟨x,y⟩ ∈ V" by simp      with A1 A2 have "⟨x,y⟩ ∈ \<Union>T × \<Union>S" using prod_open_type by blast      hence "x ∈ \<Union>T" and "y ∈ \<Union>S" by auto      from A1 A2 ⟨x,y⟩ ∈ V have "∃U W. U∈T ∧ W∈S ∧ U×W ⊆ V ∧ ⟨x,y⟩ ∈ U×W"        by (rule prod_top_point_neighb)      then obtain U W where  "U∈T" "W∈S" "U×W ⊆ V" "⟨x,y⟩ ∈ U×W"        by auto      with A1 A2 show "∃W∈S. (y∈W ∧ W⊆?A)" using prod_open_type section_proj        by auto    qed  ultimately show ?thesis by (rule topology0.open_neigh_open)qedtext{*Projection of a section of an open set is open. This is dual of @{text "prod_sec_open1"} with a very similar proof.*}lemma prod_sec_open2: assumes A1: "T {is a topology}"  "S {is a topology}" and  A2: "V ∈ ProductTopology(T,S)" and A3: "y ∈ \<Union>S"  shows "{x ∈ \<Union>T. ⟨x,y⟩ ∈ V} ∈ T"proof -  let ?A = "{x ∈ \<Union>T. ⟨x,y⟩ ∈ V}"  from A1 have "topology0(T)" using topology0_def by simp  moreover have "∀x∈?A.∃W∈T. (x∈W ∧ W⊆?A)"    proof      fix x assume "x ∈ ?A"      then have "⟨x,y⟩ ∈ V" by simp      with A1 A2 have "⟨x,y⟩ ∈ \<Union>T × \<Union>S" using prod_open_type by blast      hence "x ∈ \<Union>T" and "y ∈ \<Union>S" by auto      from A1 A2 ⟨x,y⟩ ∈ V have "∃U W. U∈T ∧ W∈S ∧ U×W ⊆ V ∧ ⟨x,y⟩ ∈ U×W"        by (rule prod_top_point_neighb)      then obtain U W where  "U∈T" "W∈S" "U×W ⊆ V" "⟨x,y⟩ ∈ U×W"        by auto      with A1 A2 show "∃W∈T. (x∈W ∧ W⊆?A)" using prod_open_type section_proj        by auto    qed  ultimately show ?thesis by (rule topology0.open_neigh_open)qedend