This theory considers the relations between topology and systems of neighborhood filters.

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) \)

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) \)

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)\} \)

{
** 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 \)

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

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 \)

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 \)

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

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

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 } \)

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

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

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) \)

** assumes **\( x\in 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 \} \)

** assumes **\( \forall x\in X.\ b(x) \in Y \)

** assumes **\( T \text{ is a topology } \)** and **\( x \in \bigcup T \)

** defines **\( \mathcal{M} \equiv \text{ neighborhood system of } T \)

** assumes **\( U\in T \), \( x\in U \)