Theory Topology_ZF_1

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 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\_1.thy}*}

theory Topology_ZF_1 imports Topology_ZF

begin

text{*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 T0}" [90] 91) where
  "T {is T0} ≡ ∀ 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 T1}" [90] 91) where
  "T {is T1} ≡ ∀ 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 T2}" [90] 91) where
  "T {is T2} ≡ ∀ 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 T1}" shows "T {is T0}"
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 T0}" using isT0_def by simp
qed

text{*If a topology is $T_2$ then it is $T_1$.*}

lemma T2_is_T1: assumes A1: "T {is T2}" shows "T {is T1}"
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 T1}" using isT1_def by simp
qed

text{*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 T0}" 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 auto
qed

section{*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 simp
qed

text{*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 simp

text{* 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 auto
qed

text{*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 blast
qed

text{*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:  "U1 ∈ {\<Union>A. A∈Pow(B)}"   "U2 ∈ {\<Union>A. A∈Pow(B)}"
  and A2: "B {satisfies the base condition}"
  shows "∃C. C ⊆ {\<Union>A. A∈Pow(B)} ∧ U1∩U2 = \<Union>C"
proof -
  from A1 A2 obtain A1 A2 where 
    D1: "A1∈ Pow(B)"  "U1 = \<Union>A1"  "A2 ∈ Pow(B)"  "U2 = \<Union>A2" 
    by auto
  let ?C = "\<Union>U∈A1.{U∩V. V∈A2}"
  from D1 have "(∀U∈A1. U∈B) ∧ (∀V∈A2. 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 "U1 ∩ U2 = \<Union>?C" by auto
  ultimately show ?thesis by auto
qed

text{*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 simp
qed;

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 auto

text{*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 BU where "BU ⊆ B" and "U = \<Union>BU" using IsAbaseFor_def by auto
  with A3 have "BU ⊆ S" by auto 
  with A2 `U = \<Union>BU` show "U∈S" using IsATopology_def by simp
qed

text{*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 U1 V1 U2 V2 where 
    D1: "U1∈T"  "V1∈S"   "A=U1×V1"  "U2∈T"  "V2∈S"   "B=U2×V2"
    using ProductCollection_def by auto
  let ?W = "(U1∩U2) × (V1∩V2)"
  from A1 D1 have "U1∩U2 ∈ T" and "V1∩V2 ∈ 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 auto
qed

text{*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 simp
qed

text{*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;
qed

text{*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;
qed

text{*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 simp
qed

text{*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 UA UB where "U = UA × UB" and
      "UA ∈ (T {restricted to} A)" and "UB ∈ (S {restricted to} B)"
      using ProductCollection_def by auto;
    then obtain WA WB where 
      "WA ∈ T"  "UA = WA ∩ A" and "WB ∈ S"  "UB = WB ∩ B"
      using RestrictedTo_def by auto;
    with `U = UA × UB` have "U = WA×WB ∩ (A×B)" by auto;
    moreover from A1 `WA ∈ T` and `WB ∈ S` have "WA×WB ∈ ?τ"
      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 AW  where 
      "AW ∈ Pow(ProductCollection(T,S))" and "W = \<Union>AW"
       using Top_1_4_T1 IsAbaseFor_def by auto;
    let ?C = "{V ∩ A×B. V ∈ AW}" 
    have "?C ∈ Pow(?\<B>)" and "U = \<Union>?C"
    proof -
      { fix R assume "R ∈ ?C"
	then obtain V where "V ∈ AW" and "R = V ∩ A×B"
	  by auto;
	with `AW ∈ Pow(ProductCollection(T,S))` obtain VT VS where 
	  "VT ∈ T" and "VS ∈ S" and "V = VT × VS"
	  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>AW`
      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);
qed

text{*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)
qed

text{*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)
qed


end