theory Topology_ZF_4a imports Topology_ZF_4
begin
This theory considers the relations between topology and systems of neighborhood filters.
Neighborhood systems
The standard way of defining a topological space is by specifying a collection of sets that we consider "open" (see the Topology_ZF theory). An alternative of this approach is to define a collection of neighborhoods for each point of the space.
We define a neighborhood system as a function that takes each point \(x\in X\) and assigns it a collection of subsets of \(X\) which is called the neighborhoods of \(x\). The neighborhoods of a point \(x\) form a filter that satisfies an additional axiom that for every neighborhood \(N\) of \(x\) we can find another one \(U\) such that \(N\) is a neighborhood of every point of \(U\).
Definition
\( \mathcal{M} \text{ is a neighborhood system on } X \equiv (\mathcal{M} : X\rightarrow Pow(Pow(X))) \wedge \) \( (\forall x\in X.\ (\mathcal{M} (x) \text{ is a filter on } X) \wedge (\forall N\in \mathcal{M} (x).\ x\in N \wedge (\exists U\in \mathcal{M} (x).\ \forall y\in U.\ (N\in \mathcal{M} (y)) ) )) \)
A neighborhood system on \(X\) consists of collections of subsets of \(X\).
lemma neighborhood_subset:
assumes \( \mathcal{M} \text{ is a neighborhood system on } X \) and \( x\in X \) and \( N\in \mathcal{M} (x) \)
shows \( N\subseteq X \) and \( x\in N \)proof from \( \mathcal{M} \text{ is a neighborhood system on } X \) have \( \mathcal{M} : X\rightarrow Pow(Pow(X)) \) unfolding IsNeighSystem_def
with \( x\in X \) have \( \mathcal{M} (x) \in Pow(Pow(X)) \) using apply_funtype
with \( N\in \mathcal{M} (x) \) show \( N\subseteq X \)
from assms show \( x\in N \) using IsNeighSystem_def
qed
Some sources (like Wikipedia) use a bit different definition of neighborhood systems where the \(U\) is required to be contained in \(N\). The next lemma shows that this stronger version can be recovered from our definition.
lemma neigh_def_stronger:
assumes \( \mathcal{M} \text{ is a neighborhood system on } X \) and \( x\in X \) and \( N\in \mathcal{M} (x) \)
shows \( \exists U\in \mathcal{M} (x).\ U\subseteq N \wedge (\forall y\in U.\ (N\in \mathcal{M} (y))) \)proof from assms obtain \( W \) where \( W\in \mathcal{M} (x) \) and areNeigh: \( \forall y\in W.\ (N\in \mathcal{M} (y)) \) using IsNeighSystem_def
let \( U = N\cap W \)
from assms, \( W\in \mathcal{M} (x) \) have \( U \in \mathcal{M} (x) \) unfolding IsNeighSystem_def , IsFilter_def
moreover
qed
have \( U\subseteq N \)
moreover from areNeigh have \( \forall y\in U.\ (N\in \mathcal{M} (y)) \)
ultimately show \( thesis \)
Topology from neighborhood systems
Given a neighborhood system \(\{\mathcal{M}_x\}_{x\in X}\) we can define a topology on \(X\). Namely, we consider a subset of \(X\) open if \(U \in \mathcal{M}_x\) for every element \(x\) of \(U\).
The collection of sets defined as above is indeed a topology.
theorem topology_from_neighs:
assumes \( \mathcal{M} \text{ is a neighborhood system on } X \)
defines Tdef: \( T \equiv \{U\in Pow(X).\ \forall x\in U.\ U \in \mathcal{M} (x)\} \)
shows \( T \text{ is a topology } \) and \( \bigcup T = X \)proof{
}
fix \( \mathfrak{U} \)
assume \( \mathfrak{U} \in Pow(T) \)
have \( \bigcup \mathfrak{U} \in T \)proof
from \( \mathfrak{U} \in Pow(T) \), Tdef have \( \bigcup \mathfrak{U} \in Pow(X) \)
moreover {
}
ultimately show \( \bigcup \mathfrak{U} \in T \) using Tdef
qed
fix \( x \)
assume \( x \in \bigcup \mathfrak{U} \)
then obtain \( U \) where \( U\in \mathfrak{U} \) and \( x\in U \)
with assms, \( \mathfrak{U} \in Pow(T) \) have \( U \in \mathcal{M} (x) \) and \( U \subseteq \bigcup \mathfrak{U} \) and \( \mathcal{M} (x) \text{ is a filter on } X \) unfolding IsNeighSystem_def
with \( \bigcup \mathfrak{U} \in Pow(X) \) have \( \bigcup \mathfrak{U} \in \mathcal{M} (x) \) unfolding IsFilter_def
moreover {
}
ultimately show \( T \text{ is a topology } \) unfolding IsATopology_def
fix \( U \) \( V \)
assume \( U\in T \) and \( V\in T \)
have \( U\cap V \in T \)proof
from Tdef, \( U\in T \), \( U\in T \) have \( U\cap V \in Pow(X) \)
moreover {
}
ultimately show \( U\cap V \in T \) using Tdef
qed
fix \( x \)
assume \( x \in U\cap V \)
with assms, \( U\in T \), \( V\in T \), Tdef have \( U \in \mathcal{M} (x) \), \( V \in \mathcal{M} (x) \) and \( \mathcal{M} (x) \text{ is a filter on } X \) unfolding IsNeighSystem_def
then have \( U\cap V \in \mathcal{M} (x) \) unfolding IsFilter_def
from assms show \( \bigcup T = X \) unfolding IsNeighSystem_def , IsFilter_def
qed
Some sources (like Wikipedia) define the open sets generated by a neighborhood system "as those sets containing a neighborhood of each of their points". The next lemma shows that this definition is equivalent to the one we are using.
lemma topology_from_neighs1:
assumes \( \mathcal{M} \text{ is a neighborhood system on } X \)
shows \( \{U\in Pow(X).\ \forall x\in U.\ U \in \mathcal{M} (x)\} = \{U\in Pow(X).\ \forall x\in U.\ \exists V \in \mathcal{M} (x).\ V\subseteq U\} \)proof let \( T = \{U\in Pow(X).\ \forall x\in U.\ U \in \mathcal{M} (x)\} \)
let \( S = \{U\in Pow(X).\ \forall x\in U.\ \exists V \in \mathcal{M} (x).\ V\subseteq U\} \)
show \( S\subseteq T \)proof
{
}
fix \( U \)
assume \( U\in S \)
then have \( U\in Pow(X) \)
moreover
from assms, \( U\in S \), \( U\in Pow(X) \) have \( \forall x\in U.\ U \in \mathcal{M} (x) \) unfolding IsNeighSystem_def , IsFilter_def
ultimately have \( U\in T \)
thus \( thesis \)
qed
show \( T\subseteq S \)
qed
Neighborhood system from topology
Once we have a topology \(T\) we can define a natural neighborhood system on \(X=\bigcup T\). In this section we define such neighborhood system and prove its basic properties.
For a topology \(T\) we define a neighborhood system of \(T\) as a function that takes an \(x\in X=\bigcup T\) and assigns it a collection supersets of open sets containing \(x\). We call that the "neighborhood system of \(T\)"
Definition
\( \text{ neighborhood system of } T \equiv \{ \langle x,\{V\in Pow(\bigcup T).\ \exists U\in T.\ (x\in U \wedge U\subseteq V)\}\rangle .\ x \in \bigcup T \} \)
The next lemma shows that open sets are members of (what we will prove later to be) the natural neighborhood system on \(X=\bigcup T\).
lemma open_are_neighs:
assumes \( U\in T \), \( x\in U \)
shows \( x \in \bigcup T \) and \( U \in \{V\in Pow(\bigcup T).\ \exists U\in T.\ (x\in U \wedge U\subseteq V)\} \) using assmsAnother fact we will need is that for every \(x\in X=\bigcup T\) the neighborhoods of \(x\) form a filter
lemma neighs_is_filter:
assumes \( T \text{ is a topology } \) and \( x \in \bigcup T \)
defines Mdef: \( \mathcal{M} \equiv \text{ neighborhood system of } T \)
shows \( \mathcal{M} (x) \text{ is a filter on } (\bigcup T) \)proof let \( X = \bigcup T \)
let \( \mathfrak{F} = \{V\in Pow(X).\ \exists U\in T.\ (x\in U \wedge U\subseteq V)\} \)
have \( 0\notin \mathfrak{F} \)
moreover
qed
have \( X\in \mathfrak{F} \)proof
moreover from assms, \( x\in X \) have \( X \in Pow(X) \), \( X\in T \) and \( x\in X \wedge X\subseteq X \) using carr_open
hence \( \exists U\in T.\ (x\in U \wedge U\subseteq X) \)
thus \( thesis \)
qed
have \( \forall A\in \mathfrak{F} .\ \forall B\in \mathfrak{F} .\ A\cap B \in \mathfrak{F} \)proof
moreover {
}
fix \( A \) \( B \)
assume \( A\in \mathfrak{F} \), \( B\in \mathfrak{F} \)
then obtain \( U_A \) \( U_B \) where \( U_A\in T \), \( x\in U_A \), \( U_A\subseteq A \), \( U_B\in T \), \( x\in U_B \), \( U_B\subseteq B \)
with \( T \text{ is a topology } \), \( A\in \mathfrak{F} \), \( B\in \mathfrak{F} \) have \( A\cap B \in Pow(X) \) and \( U_A\cap U_B \in T \), \( x \in U_A\cap U_B \), \( U_A\cap U_B \subseteq A\cap B \) using IsATopology_def
hence \( A\cap B \in \mathfrak{F} \)
thus \( thesis \)
qed
have \( \forall B\in \mathfrak{F} .\ \forall C\in Pow(X).\ B\subseteq C \longrightarrow C\in \mathfrak{F} \)proof
ultimately have \( \mathfrak{F} \text{ is a filter on } X \) unfolding IsFilter_def
{
}
fix \( B \) \( C \)
assume \( B\in \mathfrak{F} \), \( C \in Pow(X) \), \( B\subseteq C \)
then obtain \( U \) where \( U\in T \) and \( x\in U \), \( U\subseteq B \)
with \( C \in Pow(X) \), \( B\subseteq C \) have \( C\in \mathfrak{F} \)
thus \( thesis \)
qed
with Mdef, \( x\in X \) show \( \mathcal{M} (x) \text{ is a filter on } X \) using ZF_fun_from_tot_val1 , NeighSystem_def
The next theorem states that the the natural neighborhood system on \(X=\bigcup T\) indeed is a neighborhood system.
theorem neigh_from_topology:
assumes \( T \text{ is a topology } \)
shows \( (\text{ neighborhood system of } T) \text{ is a neighborhood system on } (\bigcup T) \)proof let \( X = \bigcup T \)
let \( \mathcal{M} = \text{ neighborhood system of } T \)
have \( \mathcal{M} : X\rightarrow Pow(Pow(X)) \)proof
{
}
fix \( x \)
assume \( x\in X \)
hence \( \{V\in Pow(\bigcup T).\ \exists U\in T.\ (x\in U \wedge U\subseteq V)\} \in Pow(Pow(X)) \)
hence \( \forall x\in X.\ \{V\in Pow(\bigcup T).\ \exists U\in T.\ (x\in U \wedge U\subseteq V)\} \in Pow(Pow(X)) \)
then show \( thesis \) using ZF_fun_from_total , NeighSystem_def
qed
moreover
qed
from assms have \( \forall x\in X.\ (\mathcal{M} (x) \text{ is a filter on } X) \) using neighs_is_filter , NeighSystem_def
moreover have \( \forall x\in X.\ \forall N\in \mathcal{M} (x).\ x\in N \wedge (\exists U\in \mathcal{M} (x).\ \forall y\in U.\ (N\in \mathcal{M} (y))) \)proof
ultimately show \( thesis \) unfolding IsNeighSystem_def
{
}
fix \( x \) \( N \)
assume \( x\in X \), \( N \in \mathcal{M} (x) \)
let \( \mathfrak{F} = \{V\in Pow(X).\ \exists U\in T.\ (x\in U \wedge U\subseteq V)\} \)
from \( x\in X \) have \( \mathcal{M} (x) = \mathfrak{F} \) using ZF_fun_from_tot_val1 , NeighSystem_def
with \( N \in \mathcal{M} (x) \) have \( N\in \mathfrak{F} \)
hence \( x\in N \)
from \( N\in \mathfrak{F} \) obtain \( U \) where \( U\in T \), \( x\in U \) and \( U\subseteq N \)
with \( N\in \mathfrak{F} \), \( \mathcal{M} (x) = \mathfrak{F} \) have \( U \in \mathcal{M} (x) \)
moreover
from assms, \( U\in T \), \( U\subseteq N \), \( N\in \mathfrak{F} \) have \( \forall y\in U.\ (N \in \mathcal{M} (y)) \) using ZF_fun_from_tot_val1 , open_are_neighs , neighs_is_filter , NeighSystem_def , IsFilter_def
ultimately have \( \exists U\in \mathcal{M} (x).\ \forall y\in U.\ (N\in \mathcal{M} (y)) \)
with \( x\in N \) have \( x\in N \wedge (\exists U\in \mathcal{M} (x).\ \forall y\in U.\ (N\in \mathcal{M} (y))) \)
thus \( thesis \)
qed
end
Definition of IsNeighSystem:
\( \mathcal{M} \text{ is a neighborhood system on } X \equiv (\mathcal{M} : X\rightarrow Pow(Pow(X))) \wedge \)
\( (\forall x\in X.\ (\mathcal{M} (x) \text{ is a filter on } X) \wedge (\forall N\in \mathcal{M} (x).\ x\in N \wedge (\exists U\in \mathcal{M} (x).\ \forall y\in U.\ (N\in \mathcal{M} (y)) ) )) \)
Definition of IsFilter:
\( \mathfrak{F} \text{ is a filter on } X \equiv (0\notin \mathfrak{F} ) \wedge (X\in \mathfrak{F} ) \wedge (\mathfrak{F} \subseteq Pow(X)) \wedge \)
\( (\forall A\in \mathfrak{F} .\ \forall B\in \mathfrak{F} .\ A\cap B\in \mathfrak{F} ) \wedge (\forall B\in \mathfrak{F} .\ \forall C\in Pow(X).\ B\subseteq C \longrightarrow C\in \mathfrak{F} ) \)
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 carr_open:
assumes \( T \text{ is a topology } \)
shows \( (\bigcup T) \in T \) lemma ZF_fun_from_tot_val1:
assumes \( x\in X \)
shows \( \{\langle x,b(x)\rangle .\ x\in X\}(x)=b(x) \)Definition of NeighSystem:
\( \text{ neighborhood system of } T \equiv \{ \langle x,\{V\in Pow(\bigcup T).\ \exists U\in T.\ (x\in U \wedge U\subseteq V)\}\rangle .\ x \in \bigcup T \} \)
lemma ZF_fun_from_total:
assumes \( \forall x\in X.\ b(x) \in Y \)
shows \( \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y \) lemma neighs_is_filter:
assumes \( T \text{ is a topology } \) and \( x \in \bigcup T \)
defines \( \mathcal{M} \equiv \text{ neighborhood system of } T \)
shows \( \mathcal{M} (x) \text{ is a filter on } (\bigcup T) \) lemma open_are_neighs:
assumes \( U\in T \), \( x\in U \)
shows \( x \in \bigcup T \) and \( U \in \{V\in Pow(\bigcup T).\ \exists U\in T.\ (x\in U \wedge U\subseteq V)\} \)
This page by Slawomir Kolodynski is licensed under a Creative Commons Attribution 3.0 License. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8