IsarMathLib

A library of formalized mathematics for Isabelle/ZF theorem proving environment

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
have \( U\subseteq N \)
moreover
from areNeigh have \( \forall y\in U.\ (N\in \mathcal{M} (y)) \)
ultimately show \( thesis \)
qed

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 {
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
} ultimately show \( \bigcup \mathfrak{U} \in T \) using Tdef
qed
}
moreover {
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 {
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
} ultimately show \( U\cap V \in T \) using Tdef
qed
} ultimately show \( T \text{ is a topology } \) unfolding IsATopology_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 assms

Another 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
have \( X\in \mathfrak{F} \)proof
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
moreover
have \( \forall A\in \mathfrak{F} .\ \forall B\in \mathfrak{F} .\ A\cap B \in \mathfrak{F} \)proof
{
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
moreover
have \( \forall B\in \mathfrak{F} .\ \forall C\in Pow(X).\ B\subseteq C \longrightarrow C\in \mathfrak{F} \)proof
{
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
ultimately have \( \mathfrak{F} \text{ is a filter on } X \) unfolding IsFilter_def
with Mdef, \( x\in X \) show \( \mathcal{M} (x) \text{ is a filter on } X \) using ZF_fun_from_tot_val1 , NeighSystem_def
qed

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
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
{
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
ultimately show \( thesis \) unfolding IsNeighSystem_def
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)\} \)
86
31
23
23