(*

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 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 simp

qed

text{*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 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 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 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: "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 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 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 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 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 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 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);

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