theory Topology_ZF_1 imports Topology_ZF
begin
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.
Separation axioms
Topological spaces can 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\).
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
\( T \text{ is }T_0 \equiv \forall x y.\ ((x \in \bigcup T \wedge y \in \bigcup T \wedge x\neq y) \longrightarrow \) \( (\exists U\in T.\ (x\in U \wedge y\notin U) \vee (y\in U \wedge x\notin U))) \)
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
\( T \text{ is }T_1 \equiv \forall x y.\ ((x \in \bigcup T \wedge y \in \bigcup T \wedge x\neq y) \longrightarrow \) \( (\exists U\in T.\ (x\in U \wedge y\notin U))) \)
\(T_1\) topological spaces are exactly those in which all singletons are closed.
lemma (in topology0) t1_def_alt:
shows \( T \text{ is }T_1 \longleftrightarrow (\forall x\in \bigcup T.\ \{x\} \text{ is closed in } T) \)proof let \( X = \bigcup T \)
assume T1: \( T \text{ is }T_1 \)
{
fix \( x \)
assume \( x\in X \)
let \( U = X-\{x\} \)
have \( U \in T \)proof
}
let \( W = \bigcup y\in U.\ \bigcup \{V\in T.\ y\in V \wedge x\notin V\} \)
{
fix \( y \)
assume \( y\in U \)
with topSpaceAssum have \( (\bigcup \{V\in T.\ y\in V \wedge x\notin V\}) \in T \) unfolding IsATopology_def
hence \( \forall y\in U.\ (\bigcup \{V\in T.\ y\in V \wedge x\notin V\}) \in T \)
with topSpaceAssum have \( W\in T \) by (rule union_indexed_open )
have \( U = W \)proof
}
show \( W\subseteq U \)
{
fix \( y \)
assume \( y\in U \)
hence \( y\in X \) and \( y\neq x \)
with T1, \( x\in X \) have \( y \in \bigcup \{V\in T.\ y\in V \wedge x\notin V\} \) unfolding isT1_def
hence \( y\in W \)
thus \( U \subseteq W \)
qed
with \( W\in T \) show \( U\in T \)
qed
with \( x\in X \) have \( (X-U) \text{ is closed in } T \) and \( X-U = \{x\} \) using Top_3_L9
hence \( \{x\} \text{ is closed in } T \)
thus \( \forall x\in X.\ \{x\} \text{ is closed in } T \)
next
let \( X = \bigcup T \)
assume scl: \( \forall x\in \bigcup T.\ \{x\} \text{ is closed in } T \)
{
fix \( x \) \( y \)
assume \( x\in X \), \( y\in X \), \( x\neq y \)
let \( U = X-\{y\} \)
from scl, \( x\in X \), \( y\in X \), \( x\neq y \) have \( U \in T \), \( x\in U \wedge y\notin U \) unfolding IsClosed_def
then have \( \exists U\in T.\ (x\in U \wedge y\notin U) \) by (rule witness_exists )
then show \( T \text{ is }T_1 \) unfolding isT1_def
qed
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
\( T \text{ is }T_2 \equiv \forall x y.\ ((x \in \bigcup T \wedge y \in \bigcup T \wedge x\neq y) \longrightarrow \) \( (\exists U\in T.\ \exists V\in T.\ x\in U \wedge y\in V \wedge U\cap V=0)) \)
A topology is regular if every closed set can be separated from a point in its complement by (disjoint) opens sets.
definition
\( T \text{ is regular } \equiv \forall D.\ D \text{ is closed in } T \longrightarrow (\forall x\in \bigcup T-D.\ \exists U\in T.\ \exists V\in T.\ D\subseteq U\wedge x\in V\wedge U\cap V=0) \)
Some sources (e.g. Metamath) use a different definition of regularity: any open neighborhood has a closed subneighborhood. The next lemma shows the equivalence of this with our definition.
lemma is_regular_def_alt:
assumes \( T \text{ is a topology } \)
shows \( T \text{ is regular } \longleftrightarrow (\forall W\in T.\ \forall x\in W.\ \exists V\in T.\ x\in V \wedge \text{Closure}(V,T)\subseteq W) \)proof let \( X = \bigcup T \)
from assms(1) have cntx: \( topology0(T) \) unfolding topology0_def
assume \( T \text{ is regular } \)
{
fix \( W \) \( x \)
assume \( W\in T \), \( x\in W \)
have \( \exists V\in T.\ x\in V \wedge \text{Closure}(V,T)\subseteq W \)proof
let \( D = X-W \)
from cntx, \( W\in T \), \( T \text{ is regular } \), \( x\in W \) have \( \exists U\in T.\ \exists V\in T.\ D\subseteq U\wedge x\in V\wedge U\cap V=0 \) using Top_3_L9 unfolding IsRegular_def
then obtain \( U \) \( V \) where \( U\in T \), \( V\in T \), \( D\subseteq U \), \( x\in V \), \( V\cap U=0 \)
from cntx, \( V\in T \) have \( \text{Closure}(V,T) \subseteq X \) using Top_3_L11(1)
from cntx, \( V\in T \), \( U\in T \), \( V\cap U=0 \), \( D\subseteq U \) have \( \text{Closure}(V,T) \cap D = 0 \) using disj_open_cl_disj
with \( \text{Closure}(V,T) \subseteq X \), \( V\in T \), \( x\in V \) show \( thesis \)
qed
thus \( \forall W\in T.\ \forall x\in W.\ \exists V\in T.\ x\in V \wedge \text{Closure}(V,T)\subseteq W \)
next
let \( X = \bigcup T \)
from assms(1) have cntx: \( topology0(T) \) unfolding topology0_def
assume regAlt: \( \forall W\in T.\ \forall x\in W.\ \exists V\in T.\ x\in V \wedge \text{Closure}(V,T)\subseteq W \)
{
fix \( A \)
assume \( A \text{ is closed in } T \)
have \( \forall x\in X-A.\ \exists U\in T.\ \exists V\in T.\ A\subseteq U \wedge x\in V \wedge U\cap V=0 \)proof
{
}
let \( W = X-A \)
from \( A \text{ is closed in } T \) have \( A\subseteq X \) and \( W\in T \) unfolding IsClosed_def
fix \( x \)
assume \( x\in W \)
with regAlt, \( W\in T \) have \( \exists V\in T.\ x\in V \wedge \text{Closure}(V,T)\subseteq W \)
then obtain \( V \) where \( V\in T \), \( x\in V \), \( \text{Closure}(V,T)\subseteq W \)
let \( U = X- \text{Closure}(V,T) \)
from cntx, \( V\in T \) have \( V\subseteq X \) and \( V\subseteq \text{Closure}(V,T) \) using cl_contains_set
with cntx, \( A\subseteq X \), \( \text{Closure}(V,T)\subseteq W \) have \( U\in T \), \( A\subseteq U \), \( U\cap V = 0 \) using cl_is_closed(2)
with \( V\in T \), \( x\in V \) have \( \exists U\in T.\ \exists V\in T.\ A\subseteq U \wedge x\in V \wedge U\cap V=0 \)
thus \( thesis \)
qed
then show \( T \text{ is regular } \) unfolding IsRegular_def
qed
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 \text{ is }T_1 \)
shows \( T \text{ is }T_0 \)proof from A1 have \( \forall x y.\ x \in \bigcup T \wedge y \in \bigcup T \wedge x\neq y \longrightarrow \)
\( (\exists U\in T.\ x\in U \wedge y\notin U) \) using isT1_def
then have \( \forall x y.\ x \in \bigcup T \wedge y \in \bigcup T \wedge x\neq y \longrightarrow \)
\( (\exists U\in T.\ x\in U \wedge y\notin U \vee y\in U \wedge x\notin U) \)
then show \( T \text{ is }T_0 \) using isT0_def
qed
If a topology is \(T_2\) then it is \(T_1\).
lemma T2_is_T1:
assumes A1: \( T \text{ is }T_2 \)
shows \( T \text{ is }T_1 \)proof{
}
fix \( x \) \( y \)
assume \( x \in \bigcup T \), \( y \in \bigcup T \), \( x\neq y \)
with A1 have \( \exists U\in T.\ \exists V\in T.\ x\in U \wedge y\in V \wedge U\cap V=0 \) using isT2_def
then have \( \exists U\in T.\ x\in U \wedge y\notin U \)
then have \( \forall x y.\ x \in \bigcup T \wedge y \in \bigcup T \wedge x\neq y \longrightarrow \)
\( (\exists U\in T.\ x\in U \wedge y\notin U) \)
then show \( T \text{ is }T_1 \) using isT1_def
qed
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 \text{ is }T_0 \) and A2: \( x \in \bigcup T \), \( y \in \bigcup T \) and A3: \( \forall U\in T.\ (x\in U \longleftrightarrow y\in U) \)
shows \( x=y \)proof{
}
assume \( x\neq y \)
with A1, A2 have \( \exists U\in T.\ x\in U \wedge y\notin U \vee y\in U \wedge x\notin U \) using isT0_def
with A3 have \( False \)
then show \( x=y \)
qed
Bases and subbases
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.
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
\( B \text{ is a base for } T \equiv B\subseteq T \wedge T = \{\bigcup A.\ A\in Pow(B)\} \)
A subbase is a collection of open sets such that finite intersection of those sets form a base.
definition
\( B \text{ is a subbase for } T \equiv \) \( B \subseteq T \wedge \{\bigcap A.\ A \in \text{FinPow}(B)\} \text{ is a base for } T \)
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
\( B \text{ satisfies the base condition } \equiv \) \( \forall U V.\ ((U\in B \wedge V\in B) \longrightarrow (\forall x \in U\cap V.\ \exists W\in B.\ x\in W \wedge W \subseteq U\cap V)) \)
A collection that is closed with respect to intersection satisfies the base condition.
lemma inter_closed_base:
assumes \( \forall U\in B.\ (\forall V\in B.\ U\cap V \in B) \)
shows \( B \text{ satisfies the base condition } \)proof{
}
fix \( U \) \( V \) \( x \)
assume \( U\in B \) and \( V\in B \) and \( x \in U\cap V \)
with assms have \( \exists W\in B.\ x\in W \wedge W \subseteq U\cap V \)
then show \( thesis \) using SatisfiesBaseCondition_def
qed
Each open set is a union of some sets from the base.
lemma Top_1_2_L1:
assumes \( B \text{ is a base for } T \) and \( U\in T \)
shows \( \exists A\in Pow(B).\ U = \bigcup A \) using assms, IsAbaseFor_defElements of base are open.
lemma base_sets_open:
assumes \( B \text{ is a base for } T \) and \( U \in B \)
shows \( U \in T \) using assms, IsAbaseFor_defA base defines topology uniquely.
lemma same_base_same_top:
assumes \( B \text{ is a base for } T \) and \( B \text{ is a base for } S \)
shows \( T = S \) using assms, IsAbaseFor_defEvery 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 \text{ is a base for } T \) and A2: \( U\in T \) and A3: \( x\in U \)
shows \( \exists V\in B.\ V\subseteq U \wedge x\in V \)proof from A1, A2 obtain \( A \) where \( A \in Pow(B) \) and \( U = \bigcup A \) using Top_1_2_L1
with A3 obtain \( V \) where \( V\in A \) and \( x\in V \)
with \( A \in Pow(B) \), \( U = \bigcup A \) show \( thesis \)
qed
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 \text{ is a topology } \) and A2: \( B \subseteq T \) and A3: \( \forall V \in T.\ \exists A \in Pow(B).\ V = \bigcup A \)
shows \( B \text{ is a base for } T \)proof from A3 have \( T \subseteq \{\bigcup A.\ A\in Pow(B)\} \)
moreover
qed
have \( \{\bigcup A.\ A\in Pow(B)\} \subseteq T \)proof
ultimately have \( T = \{\bigcup A.\ A\in Pow(B)\} \)
fix \( U \)
assume \( U \in \{\bigcup A.\ A\in Pow(B)\} \)
then obtain \( A \) where \( A \in Pow(B) \) and \( U = \bigcup A \)
with \( B \subseteq T \) have \( A \in Pow(T) \)
with A1, \( U = \bigcup A \) show \( U \in T \) unfolding IsATopology_def
qed
with A2 show \( B \text{ is a base for } T \) unfolding IsAbaseFor_def
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: \( \exists T.\ T \text{ is a topology } \wedge B \text{ is a base for } T \) and A2: \( V\in B \), \( W\in B \)
shows \( \forall x \in V\cap W.\ \exists U\in B.\ x\in U \wedge U \subseteq V \cap W \)proof from A1 obtain \( T \) where D1: \( T \text{ is a topology } \), \( B \text{ is a base for } T \)
then have \( B \subseteq T \) using IsAbaseFor_def
with A2 have \( V\in T \) and \( W\in T \) using IsAbaseFor_def
with D1 have \( \exists A\in Pow(B).\ V\cap W = \bigcup A \) using IsATopology_def, Top_1_2_L1
then obtain \( A \) where \( A \subseteq B \) and \( V \cap W = \bigcup A \)
then show \( \forall x \in V\cap W.\ \exists U\in B.\ (x\in U \wedge U \subseteq V \cap W) \)
qed
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: \( \forall x\in V\cap W .\ \exists U\in B.\ x\in U \wedge U \subseteq V\cap W \)
shows \( V\cap W \in \{\bigcup A.\ A\in Pow(B)\} \)proof let \( A = \bigcup x\in V\cap W.\ \{U\in B.\ x\in U \wedge U \subseteq V\cap W\} \)
show \( A\in Pow(B) \)
from A1 show \( V\cap W = \bigcup A \)
qed
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 \in \{\bigcup A.\ A\in Pow(B)\} \), \( U_2 \in \{\bigcup A.\ A\in Pow(B)\} \) and A2: \( B \text{ satisfies the base condition } \)
shows \( \exists C.\ C \subseteq \{\bigcup A.\ A\in Pow(B)\} \wedge U_1\cap U_2 = \bigcup C \)proof from A1, A2 obtain \( A_1 \) \( A_2 \) where D1: \( A_1\in Pow(B) \), \( U_1 = \bigcup A_1 \), \( A_2 \in Pow(B) \), \( U_2 = \bigcup A_2 \)
let \( C = \bigcup U\in A_1.\ \{U\cap V.\ V\in A_2\} \)
from D1 have \( (\forall U\in A_1.\ U\in B) \wedge (\forall V\in A_2.\ V\in B) \)
with A2 have \( C \subseteq \{\bigcup A .\ A \in Pow(B)\} \) using Top_1_2_L3, SatisfiesBaseCondition_def
moreover
qed
from D1 have \( U_1 \cap U_2 = \bigcup C \)
ultimately show \( thesis \)
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 \text{ satisfies the base condition } \) and A2: \( T = \{\bigcup A.\ A\in Pow(B)\} \)
shows \( T \text{ is a topology } \) and \( B \text{ is a base for } T \)proof show \( T \text{ is a topology } \)proof
have I: \( \forall C\in Pow(T).\ \bigcup C \in T \)proof
{
}
fix \( C \)
assume A3: \( C \in Pow(T) \)
let \( Q = \bigcup \{\bigcup \{A\in Pow(B).\ U = \bigcup A\}.\ U\in C\} \)
from A2, A3 have \( \forall U\in C.\ \exists A\in Pow(B).\ U = \bigcup A \)
then have \( \bigcup Q = \bigcup C \) using ZF1_1_L10
moreover
from A2 have \( \bigcup Q \in T \)
ultimately have \( \bigcup C \in T \)
thus \( \forall C\in Pow(T).\ \bigcup C \in T \)
qed
moreover
qed
have \( \forall U\in T.\ \forall V\in T.\ U\cap V \in T \)proof
ultimately show \( T \text{ is a topology } \) using IsATopology_def
{
}
fix \( U \) \( V \)
assume \( U \in T \), \( V \in T \)
with A1, A2 have \( \exists C.\ (C \subseteq T \wedge U\cap V = \bigcup C) \) using Top_1_2_L4
then obtain \( C \) where \( C \subseteq T \) and \( U\cap V = \bigcup C \)
with I have \( U\cap V \in T \)
then show \( \forall U\in T.\ \forall V\in T.\ U\cap V \in T \)
qed
from A2 have \( B\subseteq T \)
with A2 show \( B \text{ is a base for } T \) using IsAbaseFor_def
qed
The carrier of the base and topology are the same.
lemma Top_1_2_L5:
assumes \( B \text{ is a base for } T \)
shows \( \bigcup T = \bigcup B \) using assms, IsAbaseFor_defIf \(B\) is a base for \(T\), then \(T\) is the smallest topology containing \(B\).
lemma base_smallest_top:
assumes A1: \( B \text{ is a base for } T \) and A2: \( S \text{ is a topology } \) and A3: \( B\subseteq S \)
shows \( T\subseteq S \)proof fix \( U \)
assume \( U\in T \)
with A1 obtain \( B_U \) where \( B_U \subseteq B \) and \( U = \bigcup B_U \) using IsAbaseFor_def
with A3 have \( B_U \subseteq S \)
with A2, \( U = \bigcup B_U \) show \( U\in S \) using IsATopology_def
qed
If \(B\) is a base for \(T\) and \(B\) is a topology, then \(B=T\).
lemma base_topology:
assumes \( B \text{ is a topology } \) and \( B \text{ is a base for } T \)
shows \( B=T \) using assms, base_sets_open, base_smallest_topProduct topology
In this section we consider a topology defined on a product of two sets.
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 ZF1.thy) as the collections of cartesian products \(A\times B\), where \(A\in S, B\in T\). The \(T\times_tS\) notation is defined as an alternative to the verbose \( \text{ProductTopology}(T,S) \)).
definition
\( T \times _t S \equiv \{\bigcup W.\ W \in Pow( \text{ProductCollection}(T,S))\} \)
The product collection satisfies the base condition.
lemma Top_1_4_L1:
assumes A1: \( T \text{ is a topology } \), \( S \text{ is a topology } \) and A2: \( A \in \text{ProductCollection}(T,S) \), \( B \in \text{ProductCollection}(T,S) \)
shows \( \forall x\in (A\cap B).\ \exists W\in \text{ProductCollection}(T,S).\ (x\in W \wedge W \subseteq A \cap B) \)proof fix \( x \)
assume A3: \( x \in A\cap B \)
from A2 obtain \( U_1 \) \( V_1 \) \( U_2 \) \( V_2 \) where D1: \( U_1\in T \), \( V_1\in S \), \( A=U_1\times V_1 \), \( U_2\in T \), \( V_2\in S \), \( B=U_2\times V_2 \) using ProductCollection_def
let \( W = (U_1\cap U_2) \times (V_1\cap V_2) \)
from A1, D1 have \( U_1\cap U_2 \in T \) and \( V_1\cap V_2 \in S \) using IsATopology_def
then have \( W \in \text{ProductCollection}(T,S) \) using ProductCollection_def
moreover
qed
from A3, D1 have \( x\in W \) and \( W \subseteq A\cap B \)
ultimately have \( \exists W.\ (W \in \text{ProductCollection}(T,S) \wedge x\in W \wedge W \subseteq A\cap B) \)
thus \( \exists W\in \text{ProductCollection}(T,S).\ (x\in W \wedge W \subseteq A \cap B) \)
The product topology is indeed a topology on the product.
theorem Top_1_4_T1:
assumes A1: \( T \text{ is a topology } \), \( S \text{ is a topology } \)
shows \( (T\times _tS) \text{ is a topology } \), \( \text{ProductCollection}(T,S) \text{ is a base for } (T\times _tS) \), \( \bigcup (T\times _tS) = \bigcup T \times \bigcup S \)proof from A1 show \( (T\times _tS) \text{ is a topology } \), \( \text{ProductCollection}(T,S) \text{ is a base for } (T\times _tS) \) using Top_1_4_L1, ProductCollection_def, SatisfiesBaseCondition_def, ProductTopology_def, Top_1_2_T1
then show \( \bigcup (T\times _tS) = \bigcup T \times \bigcup S \) using Top_1_2_L5, ZF1_1_L6
qed
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 \text{ is a topology } \), \( S \text{ is a topology } \) and A2: \( U \in \text{ProductTopology}(T,S) \) and A3: \( x \in U \)
shows \( \exists V W.\ V\in T \wedge W\in S \wedge V\times W \subseteq U \wedge x \in V\times W \)proof from A1 have \( \text{ProductCollection}(T,S) \text{ is a base for } \text{ProductTopology}(T,S) \) using Top_1_4_T1
with A2, A3 obtain \( Z \) where \( Z \in \text{ProductCollection}(T,S) \) and \( Z \subseteq U \wedge x\in Z \) using point_open_base_neigh
then obtain \( V \) \( W \) where \( V \in T \) and \( W\in S \) and \( V\times W \subseteq U \wedge x \in V\times W \) using ProductCollection_def
thus \( thesis \)
qed
Products of open sets are open in the product topology.
lemma prod_open_open_prod:
assumes A1: \( T \text{ is a topology } \), \( S \text{ is a topology } \) and A2: \( U\in T \), \( V\in S \)
shows \( U\times V \in \text{ProductTopology}(T,S) \)proof from A1 have \( \text{ProductCollection}(T,S) \text{ is a base for } \text{ProductTopology}(T,S) \) using Top_1_4_T1
moreover
qed
from A2 have \( U\times V \in \text{ProductCollection}(T,S) \) unfolding ProductCollection_def
ultimately show \( U\times V \in \text{ProductTopology}(T,S) \) using base_sets_open
Sets that are open in the product topology are contained in the product of the carrier.
lemma prod_open_type:
assumes A1: \( T \text{ is a topology } \), \( S \text{ is a topology } \) and A2: \( V \in \text{ProductTopology}(T,S) \)
shows \( V \subseteq \bigcup T \times \bigcup S \)proof from A2 have \( V \subseteq \bigcup \text{ProductTopology}(T,S) \)
with A1 show \( thesis \) using Top_1_4_T1
qed
A reverse of prod_top_point_neighb: if each point of set has an neighborhood in the set that is a cartesian product of open sets, then the set is open.
lemma point_neighb_prod_top:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \) and \( \forall p\in V.\ \exists U\in T.\ \exists W\in S.\ p\in U\times W \wedge U\times W \subseteq V \)
shows \( V \in \text{ProductTopology}(T,S) \)proof from assms(1,2) have I: \( topology0( \text{ProductTopology}(T,S)) \) using Top_1_4_T1(1), topology0_def
moreover {
}
qed
fix \( p \)
assume \( p\in V \)
with assms(3) obtain \( U \) \( W \) where \( U\in T \), \( W\in S \), \( p\in U\times W \), \( U\times W \subseteq V \)
with assms(1,2) have \( \exists N\in \text{ProductTopology}(T,S).\ p\in N \wedge N\subseteq V \) using prod_open_open_prod
hence \( \forall p\in V.\ \exists N\in \text{ProductTopology}(T,S).\ p\in N \wedge N\subseteq V \)
ultimately show \( thesis \) using open_neigh_open
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 \text{ is a topology } \), \( S \text{ is a topology } \)
shows \( \text{ProductCollection}(T \text{ restricted to } A, S \text{ restricted to } B)\) \( \text{ is a base for } ( \text{ProductTopology}(T,S) \text{ restricted to } A\times B) \)proof let \( \mathcal{B} = \text{ProductCollection}(T \text{ restricted to } A, S \text{ restricted to } B) \)
let \( \tau = \text{ProductTopology}(T,S) \)
from A1 have \( (\tau \text{ restricted to } A\times B) \text{ is a topology } \) using Top_1_4_T1, topology0_def, Top_1_L4
moreover
qed
have \( \mathcal{B} \subseteq (\tau \text{ restricted to } A\times B) \)proof
moreover fix \( U \)
assume \( U \in \mathcal{B} \)
then obtain \( U_A \) \( U_B \) where \( U = U_A \times U_B \) and \( U_A \in (T \text{ restricted to } A) \) and \( U_B \in (S \text{ restricted to } B) \) using ProductCollection_def
then obtain \( W_A \) \( W_B \) where \( W_A \in T \), \( U_A = W_A \cap A \) and \( W_B \in S \), \( U_B = W_B \cap B \) using RestrictedTo_def
with \( U = U_A \times U_B \) have \( U = W_A\times W_B \cap (A\times B) \)
moreover
qed
from A1, \( W_A \in T \), and, \( W_B \in S \) have \( W_A\times W_B \in \tau \) using prod_open_open_prod
ultimately show \( U \in \tau \text{ restricted to } A\times B \) using RestrictedTo_def
have \( \forall U \in \tau \text{ restricted to } A\times B.\ \)
\( \exists C \in Pow(\mathcal{B} ).\ U = \bigcup C \)proof
ultimately show \( thesis \) by (rule is_a_base_criterion )
fix \( U \)
assume \( U \in \tau \text{ restricted to } A\times B \)
then obtain \( W \) where \( W \in \tau \) and \( U = W \cap (A\times B) \) using RestrictedTo_def
from A1, \( W \in \tau \) obtain \( A_W \) where \( A_W \in Pow( \text{ProductCollection}(T,S)) \) and \( W = \bigcup A_W \) using Top_1_4_T1, IsAbaseFor_def
let \( C = \{V \cap A\times B.\ V \in A_W\} \)
have \( C \in Pow(\mathcal{B} ) \) and \( U = \bigcup C \)proof
{
}
fix \( R \)
assume \( R \in C \)
then obtain \( V \) where \( V \in A_W \) and \( R = V \cap A\times B \)
with \( A_W \in Pow( \text{ProductCollection}(T,S)) \) obtain \( V_T \) \( V_S \) where \( V_T \in T \) and \( V_S \in S \) and \( V = V_T \times V_S \) using ProductCollection_def
with \( R = V \cap A\times B \) have \( R \in \mathcal{B} \) using ProductCollection_def, RestrictedTo_def
then show \( C \in Pow(\mathcal{B} ) \)
from \( U = W \cap (A\times B) \), and, \( W = \bigcup A_W \) show \( U = \bigcup C \)
qed
thus \( \exists C \in Pow(\mathcal{B} ).\ U = \bigcup C \)
qed
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 \text{ is a topology } \), \( S \text{ is a topology } \)
shows \( \text{ProductTopology}(T \text{ restricted to } A,S \text{ restricted to } B) =\) \( \text{ProductTopology}(T,S) \text{ restricted to } (A\times B) \)proof let \( \mathcal{B} = \text{ProductCollection}(T \text{ restricted to } A, S \text{ restricted to } B) \)
from A1 have \( \mathcal{B} \text{ is a base for } \text{ProductTopology}(T \text{ restricted to } A,S \text{ restricted to } B) \) using topology0_def, Top_1_L4, Top_1_4_T1
moreover
qed
from A1 have \( \mathcal{B} \text{ is a base for } \text{ProductTopology}(T,S) \text{ restricted to } (A\times B) \) using prod_restr_base_restr
ultimately show \( thesis \) by (rule same_base_same_top )
Projection of a section of an open set is open.
lemma prod_sec_open1:
assumes A1: \( T \text{ is a topology } \), \( S \text{ is a topology } \) and A2: \( V \in \text{ProductTopology}(T,S) \) and A3: \( x \in \bigcup T \)
shows \( \{y \in \bigcup S.\ \langle x,y\rangle \in V\} \in S \)proof let \( A = \{y \in \bigcup S.\ \langle x,y\rangle \in V\} \)
from A1 have \( topology0(S) \) using topology0_def
moreover
qed
have \( \forall y\in A.\ \exists W\in S.\ (y\in W \wedge W\subseteq A) \)proof
ultimately show \( thesis \) by (rule open_neigh_open )
fix \( y \)
assume \( y \in A \)
then have \( \langle x,y\rangle \in V \)
with A1, A2 have \( \langle x,y\rangle \in \bigcup T \times \bigcup S \) using prod_open_type
hence \( x \in \bigcup T \) and \( y \in \bigcup S \)
from A1, A2, \( \langle x,y\rangle \in V \) have \( \exists U W.\ U\in T \wedge W\in S \wedge U\times W \subseteq V \wedge \langle x,y\rangle \in U\times W \) by (rule prod_top_point_neighb )
then obtain \( U \) \( W \) where \( U\in T \), \( W\in S \), \( U\times W \subseteq V \), \( \langle x,y\rangle \in U\times W \)
with A1, A2 show \( \exists W\in S.\ (y\in W \wedge W\subseteq A) \) using prod_open_type, section_proj
qed
Projection of a section of an open set is open. This is dual of prod_sec_open1 with a very similar proof.
lemma prod_sec_open2:
assumes A1: \( T \text{ is a topology } \), \( S \text{ is a topology } \) and A2: \( V \in \text{ProductTopology}(T,S) \) and A3: \( y \in \bigcup S \)
shows \( \{x \in \bigcup T.\ \langle x,y\rangle \in V\} \in T \)proof let \( A = \{x \in \bigcup T.\ \langle x,y\rangle \in V\} \)
from A1 have \( topology0(T) \) using topology0_def
moreover
qed
have \( \forall x\in A.\ \exists W\in T.\ (x\in W \wedge W\subseteq A) \)proof
ultimately show \( thesis \) by (rule open_neigh_open )
fix \( x \)
assume \( x \in A \)
then have \( \langle x,y\rangle \in V \)
with A1, A2 have \( \langle x,y\rangle \in \bigcup T \times \bigcup S \) using prod_open_type
hence \( x \in \bigcup T \) and \( y \in \bigcup S \)
from A1, A2, \( \langle x,y\rangle \in V \) have \( \exists U W.\ U\in T \wedge W\in S \wedge U\times W \subseteq V \wedge \langle x,y\rangle \in U\times W \) by (rule prod_top_point_neighb )
then obtain \( U \) \( W \) where \( U\in T \), \( W\in S \), \( U\times W \subseteq V \), \( \langle x,y\rangle \in U\times W \)
with A1, A2 show \( \exists W\in T.\ (x\in W \wedge W\subseteq A) \) using prod_open_type, section_proj
qed
Hausdorff spaces
In this section we study properties of Hausdorff spaces (sometimes called separated spaces) These are topological spaces that are \(T_2\) as defined above.
A space is Hausdorff if and only if the diagonal \(\Delta = \{\langle x,x\rangle : x\in X\}\) is closed in the product topology on \(X\times X\).
theorem t2_iff_diag_closed:
assumes \( T \text{ is a topology } \)
shows \( T \text{ is }T_2 \longleftrightarrow \{\langle x,x\rangle .\ x\in \bigcup T\} \text{ is closed in } \text{ProductTopology}(T,T) \)proof let \( X = \bigcup T \)
from assms(1) have I: \( topology0( \text{ProductTopology}(T,T)) \) using Top_1_4_T1(1), topology0_def
assume \( T \text{ is }T_2 \)
show \( \{\langle x,x\rangle .\ x\in X\} \text{ is closed in } \text{ProductTopology}(T,T) \)proof
let \( D_c = X\times X - \{\langle x,x\rangle .\ x\in X\} \)
have \( \forall p\in D_c.\ \exists U\in T.\ \exists V\in T.\ p\in U\times V \wedge U\times V \subseteq D_c \)proof
{
}
fix \( p \)
assume \( p\in D_c \)
then obtain \( x \) \( y \) where \( p=\langle x,y\rangle \), \( x\in X \), \( y\in X \), \( x\neq y \)
with \( T \text{ is }T_2 \) obtain \( U \) \( V \) where \( U\in T \), \( V\in T \), \( x\in U \), \( y\in V \), \( U\cap V = 0 \) unfolding isT2_def
with assms, \( p=\langle x,y\rangle \) have \( \exists U\in T.\ \exists V\in T.\ p\in U\times V \wedge U\times V \subseteq D_c \)
hence \( \forall p.\ p\in D_c \longrightarrow (\exists U\in T.\ \exists V\in T.\ p\in U\times V \wedge U\times V \subseteq D_c) \)
then show \( thesis \) by (rule exists_in_set )
qed
with assms show \( thesis \) using Top_1_4_T1(3), point_neighb_prod_top unfolding IsClosed_def
qed
next
let \( X = \bigcup T \)
assume A: \( \{\langle x,x\rangle .\ x\in X\} \text{ is closed in } \text{ProductTopology}(T,T) \)
show \( T \text{ is }T_2 \)proof
qed
{
}
let \( D_c = X\times X - \{\langle x,x\rangle .\ x\in X\} \)
fix \( x \) \( y \)
assume \( x\in X \), \( y\in X \), \( x\neq y \)
with assms, A have \( D_c \in \text{ProductTopology}(T,T) \) and \( \langle x,y\rangle \in D_c \) using Top_1_4_T1(3) unfolding IsClosed_def
with assms obtain \( U \) \( V \) where \( U\in T \), \( V\in T \), \( U\times V \subseteq D_c \), \( \langle x,y\rangle \in U\times V \) using prod_top_point_neighb
moreover
from \( U\times V \subseteq D_c \) have \( U\cap V = 0 \)
ultimately have \( \exists U\in T.\ \exists V\in T.\ x\in U \wedge y\in V \wedge U\cap V=0 \)
then show \( T \text{ is }T_2 \) unfolding isT2_def
qed
end
Definition of IsATopology:
\( T \text{ is a topology } \equiv ( \forall M \in Pow(T).\ \bigcup M \in T ) \wedge \)
\( ( \forall U\in T.\ \forall V\in T.\ U\cap V \in T) \)
lemma union_indexed_open:
assumes \( T \text{ is a topology } \) and \( \forall i\in I.\ P(i) \in T \)
shows \( (\bigcup i\in I.\ P(i)) \in T \)Definition of isT1:
\( T \text{ is }T_1 \equiv \forall x y.\ ((x \in \bigcup T \wedge y \in \bigcup T \wedge x\neq y) \longrightarrow \)
\( (\exists U\in T.\ (x\in U \wedge y\notin U))) \)
lemma (in topology0) Top_3_L9:
assumes \( A\in T \)
shows \( (\bigcup T - A) \text{ is closed in } T \)Definition of IsClosed:
\( D \text{ is closed in } T \equiv (D \subseteq \bigcup T \wedge \bigcup T - D \in T) \)
lemma witness_exists:
assumes \( x\in X \) and \( \phi (x) \)
shows \( \exists x\in X.\ \phi (x) \)Definition of IsRegular:
\( T \text{ is regular } \equiv \forall D.\ D \text{ is closed in } T \longrightarrow (\forall x\in \bigcup T-D.\ \exists U\in T.\ \exists V\in T.\ D\subseteq U\wedge x\in V\wedge U\cap V=0) \)
lemma (in topology0) Top_3_L11:
assumes \( A \subseteq \bigcup T \)
shows \( cl(A) \subseteq \bigcup T \), \( cl(\bigcup T - A) = \bigcup T - int(A) \) lemma (in topology0) disj_open_cl_disj:
assumes \( A \subseteq \bigcup T \), \( V\in T \) and \( A\cap V = 0 \)
shows \( cl(A) \cap V = 0 \) lemma (in topology0) cl_contains_set:
assumes \( A \subseteq \bigcup T \)
shows \( A \subseteq cl(A) \) lemma (in topology0) cl_is_closed:
assumes \( A \subseteq \bigcup T \)
shows \( cl(A) \text{ is closed in } T \) and \( \bigcup T - cl(A) \in T \)Definition of isT0:
\( T \text{ is }T_0 \equiv \forall x y.\ ((x \in \bigcup T \wedge y \in \bigcup T \wedge x\neq y) \longrightarrow \)
\( (\exists U\in T.\ (x\in U \wedge y\notin U) \vee (y\in U \wedge x\notin U))) \)
Definition of isT2:
\( T \text{ is }T_2 \equiv \forall x y.\ ((x \in \bigcup T \wedge y \in \bigcup T \wedge x\neq y) \longrightarrow \)
\( (\exists U\in T.\ \exists V\in T.\ x\in U \wedge y\in V \wedge U\cap V=0)) \)
Definition of SatisfiesBaseCondition:
\( B \text{ satisfies the base condition } \equiv \)
\( \forall U V.\ ((U\in B \wedge V\in B) \longrightarrow (\forall x \in U\cap V.\ \exists W\in B.\ x\in W \wedge W \subseteq U\cap V)) \)
Definition of IsAbaseFor:
\( B \text{ is a base for } T \equiv B\subseteq T \wedge T = \{\bigcup A.\ A\in Pow(B)\} \)
lemma Top_1_2_L1:
assumes \( B \text{ is a base for } T \) and \( U\in T \)
shows \( \exists A\in Pow(B).\ U = \bigcup A \) lemma Top_1_2_L3:
assumes \( \forall x\in V\cap W .\ \exists U\in B.\ x\in U \wedge U \subseteq V\cap W \)
shows \( V\cap W \in \{\bigcup A.\ A\in Pow(B)\} \) lemma ZF1_1_L10:
assumes \( \forall U\in C.\ \exists A\in B.\ U = \bigcup A \)
shows \( \bigcup \bigcup \{\bigcup \{A\in B.\ U = \bigcup A\}.\ U\in C\} = \bigcup C \) lemma Top_1_2_L4:
assumes \( U_1 \in \{\bigcup A.\ A\in Pow(B)\} \), \( U_2 \in \{\bigcup A.\ A\in Pow(B)\} \) and \( B \text{ satisfies the base condition } \)
shows \( \exists C.\ C \subseteq \{\bigcup A.\ A\in Pow(B)\} \wedge U_1\cap U_2 = \bigcup C \) lemma base_sets_open:
assumes \( B \text{ is a base for } T \) and \( U \in B \)
shows \( U \in T \) lemma base_smallest_top:
assumes \( B \text{ is a base for } T \) and \( S \text{ is a topology } \) and \( B\subseteq S \)
shows \( T\subseteq S \)Definition of ProductCollection:
\( \text{ProductCollection}(T,S) \equiv \bigcup U\in T.\ \{U\times V.\ V\in S\} \)
lemma Top_1_4_L1:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \) and \( A \in \text{ProductCollection}(T,S) \), \( B \in \text{ProductCollection}(T,S) \)
shows \( \forall x\in (A\cap B).\ \exists W\in \text{ProductCollection}(T,S).\ (x\in W \wedge W \subseteq A \cap B) \)Definition of ProductTopology:
\( T \times _t S \equiv \{\bigcup W.\ W \in Pow( \text{ProductCollection}(T,S))\} \)
theorem Top_1_2_T1:
assumes \( B \text{ satisfies the base condition } \) and \( T = \{\bigcup A.\ A\in Pow(B)\} \)
shows \( T \text{ is a topology } \) and \( B \text{ is a base for } T \) lemma Top_1_2_L5:
assumes \( B \text{ is a base for } T \)
shows \( \bigcup T = \bigcup B \) lemma ZF1_1_L6: shows \( \bigcup \text{ProductCollection}(S,T) = \bigcup S \times \bigcup T \)
theorem Top_1_4_T1:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \)
shows \( (T\times _tS) \text{ is a topology } \), \( \text{ProductCollection}(T,S) \text{ is a base for } (T\times _tS) \), \( \bigcup (T\times _tS) = \bigcup T \times \bigcup S \) lemma point_open_base_neigh:
assumes \( B \text{ is a base for } T \) and \( U\in T \) and \( x\in U \)
shows \( \exists V\in B.\ V\subseteq U \wedge x\in V \) theorem Top_1_4_T1:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \)
shows \( (T\times _tS) \text{ is a topology } \), \( \text{ProductCollection}(T,S) \text{ is a base for } (T\times _tS) \), \( \bigcup (T\times _tS) = \bigcup T \times \bigcup S \) lemma prod_open_open_prod:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \) and \( U\in T \), \( V\in S \)
shows \( U\times V \in \text{ProductTopology}(T,S) \) lemma (in topology0) open_neigh_open:
assumes \( \forall x\in V.\ \exists U\in T.\ (x\in U \wedge U\subseteq V) \)
shows \( V\in T \) lemma (in topology0) Top_1_L4: shows \( (T \text{ restricted to } X) \text{ is a topology } \)
Definition of RestrictedTo:
\( M \text{ restricted to } X \equiv \{X \cap A .\ A \in M\} \)
lemma is_a_base_criterion:
assumes \( T \text{ is a topology } \) and \( B \subseteq T \) and \( \forall V \in T.\ \exists A \in Pow(B).\ V = \bigcup A \)
shows \( B \text{ is a base for } T \) lemma prod_restr_base_restr:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \)
shows \( \text{ProductCollection}(T \text{ restricted to } A, S \text{ restricted to } B)\) \( \text{ is a base for } ( \text{ProductTopology}(T,S) \text{ restricted to } A\times B) \) lemma same_base_same_top:
assumes \( B \text{ is a base for } T \) and \( B \text{ is a base for } S \)
shows \( T = S \) lemma prod_open_type:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \) and \( V \in \text{ProductTopology}(T,S) \)
shows \( V \subseteq \bigcup T \times \bigcup S \) lemma prod_top_point_neighb:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \) and \( U \in \text{ProductTopology}(T,S) \) and \( x \in U \)
shows \( \exists V W.\ V\in T \wedge W\in S \wedge V\times W \subseteq U \wedge x \in V\times W \) lemma section_proj:
assumes \( A \subseteq X\times Y \) and \( U\times V \subseteq A \) and \( x \in U \), \( y \in V \)
shows \( U \subseteq \{t\in X.\ \langle t,y\rangle \in A\} \) and \( V \subseteq \{t\in Y.\ \langle x,t\rangle \in A\} \) lemma exists_in_set:
assumes \( \forall x.\ x\in A \longrightarrow \phi (x) \)
shows \( \forall x\in A.\ \phi (x) \) theorem Top_1_4_T1:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \)
shows \( (T\times _tS) \text{ is a topology } \), \( \text{ProductCollection}(T,S) \text{ is a base for } (T\times _tS) \), \( \bigcup (T\times _tS) = \bigcup T \times \bigcup S \) lemma point_neighb_prod_top:
assumes \( T \text{ is a topology } \), \( S \text{ is a topology } \) and \( \forall p\in V.\ \exists U\in T.\ \exists W\in S.\ p\in U\times W \wedge U\times W \subseteq V \)
shows \( V \in \text{ProductTopology}(T,S) \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8