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 the collection of supersets of open sets containing \(x\). We call that the "neighborhood system of \(T\)"

** definition **

\( \text{ neighborhood system of } T \equiv \{ \langle x,\{N\in Pow(\bigcup T).\ \exists U\in T.\ (x\in U \wedge U\subseteq N)\}\rangle .\ x \in \bigcup T \} \)

The way we defined the neighborhood system of \(T\) means that it is a function on \(\bigcup T\).

** lemma ** neigh_fun:

The value of the neighborhood system of \(T\) at \(x\in \bigcup T\) is the collection of supersets of open sets containing \(x\).

** lemma ** neigh_val:

** assumes **\( 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 **

Any neighborhood of an element of the closure of a subset intersects the subset.

** lemma ** neigh_inter_nempty:

** assumes **\( T \text{ is a topology } \), \( A\subseteq \bigcup T \), \( x \in \text{Closure}(A,T) \)** and **\( N \in (\text{ neighborhood system of } T)(x) \)

We can create a topology from a neighborhood system and neighborhood system from topology. The question is then if we start from a neighborhood system, create a topology from it then create the topology's natural neighborhood system, do we get back the neighborhood system we started from? Similarly, if we start from a topology, create its neighborhood system and then create a topology from that, do we get the original topology? This section provides the affirmative answer (for now only for the first question). This means that there is a one-to-one correspondence between the set of topologies on a set and the set of abstract neighborhood systems on the set.

Each abstract neighborhood of \(x\) contains an open neighborhood of \(x\).

** lemma ** open_nei_in_nei:

** assumes **\( \mathcal{M} \text{ is a neighborhood system on } X \), \( x\in X \), \( N\in \mathcal{M} (x) \)

** defines **Tdef: \( T \equiv \{U\in Pow(X).\ \forall x\in U.\ U \in \mathcal{M} (x)\} \)

{
** fix **\( y \) ** assume **\( y\in U \)
** then **** have ** \( y\in X \)** and **\( N\in \mathcal{M} (y) \)
** with **assms(1) ** obtain **\( V \)** where **\( V\in \mathcal{M} (y) \)** and **\( \forall z\in V.\ N \in \mathcal{M} (z) \)** unfolding ** IsNeighSystem_def
** with **assms(1), \( y\in X \), \( V\in \mathcal{M} (y) \) ** have ** \( V\subseteq U \)** using ** neighborhood_subset(1)
** with **assms(1), \( y\in X \), \( V\in \mathcal{M} (y) \), \( U \in Pow(X) \) ** have ** \( U\in \mathcal{M} (y) \)** unfolding ** IsNeighSystem_def** using ** is_filter_def_split(5)
** } **
** thus ** \( thesis \)
** qed **

In the the next theorem we show that if we start from a neighborhood system, create a topology from it, then create it's natural neighborhood system, we get back the original neighborhood system.

** theorem ** nei_top_nei_round_trip:

** 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 **\( V \) ** assume **\( V\in M(x) \)
** with **I ** obtain **\( U \)** where **\( U\in T \), \( x\in U \), \( U\subseteq V \)
** from **assms(2), \( U\in T \), \( x\in U \) ** have ** \( U \in \mathcal{M} (x) \)
** from **assms(1), \( x\in X \) ** have ** \( \mathcal{M} (x) \text{ is a filter on } X \)** unfolding ** IsNeighSystem_def
** with **\( U \in \mathcal{M} (x) \), \( V\in M(x) \), I, \( U\subseteq V \) ** have ** \( V \in \mathcal{M} (x) \)** unfolding ** IsFilter_def
** } **
** thus ** \( M(x) \subseteq \mathcal{M} (x) \)
{
** fix **\( N \) ** assume **\( N\in \mathcal{M} (x) \)
** with **assms, \( x\in X \), \( \bigcup T = X \), I ** have ** \( N\in M(x) \)** using ** open_nei_in_nei
** } **
** thus ** \( \mathcal{M} (x) \subseteq M(x) \)
** qed **

Some sources (like Metamath) take a somewhat different approach where instead of defining the collection of neighborhoods of a point \(x\in X\) they define a collection of neighborhoods of a subset of \(X\) (where \(X\) is the carrier of a topology \(T\) (i.e. \(X=\bigcup T\)). In this approach a neighborhood system is a function whose domain is the powerset of \(X\), i.e. the set of subsets of \(X\). The two approaches are equivalent in a sense as having a neighborhood system we can create a set neighborhood system and vice versa.

We define a set neighborhood system as a function that takes a subset \(A\) of the carrier of the topology and assigns it the collection of supersets of all open sets that contain \(A\).

** definition **

\( \text{ set neighborhood system of } T \) \( \equiv \{\langle A,\{N\in Pow(\bigcup T).\ \exists U\in T.\ (A\subseteq U \wedge U\subseteq N)\}\rangle .\ A\in Pow(\bigcup T)\} \)

Given a set neighborhood system we can recover the (standard) neighborhood system by taking the values of the set neighborhood system at singletons \({x}\) where \(x\in X=\bigcup T\).

** lemma ** neigh_from_nei:

** assumes **\( x\in \bigcup T \)

The set neighborhood system of \(T\) is a function mapping subsets of \(\bigcup T\) to collections of subsets of \(\bigcup T\).

** lemma ** nei_fun:

The value of the set neighborhood system of \(T\) at subset \(A\) of \(\bigcup T\) is the collection of subsets \(N\) of \(\bigcup T\) for which exists an open subset \(U\subseteq N\) that contains \(A\).

** lemma ** nei_val:

** assumes **\( A \subseteq \bigcup T \)

A member of the value of the set neighborhood system of \(T\) at \(A\) is a subset of \(\bigcup T\). The interesting part is that we can show it without any assumption on \(A\).

** lemma ** nei_val_subset:

** assumes **\( N \in (\text{ set neighborhood system of } T)(A) \)

If \(T\) is a topology, then every subset of its carrier (i.e. \(\bigcup T\)) is a (set) neighborhood of the empty set.

** lemma ** nei_empty:

** assumes **\( T \text{ is a topology } \), \( N \subseteq \bigcup T \)

If \(T\) is a topology, then the (set) neighborhoods of a nonempty subset of \(\bigcup T\) form a filter on \(X=\bigcup T\).

** theorem ** nei_filter:

** assumes **\( T \text{ is a topology } \), \( D \subseteq (\bigcup T) \), \( D\neq 0 \)

{
** fix **\( A \) \( B \) ** assume **\( A\in \mathcal{F} \), \( B\in \mathcal{F} \)
** with **I ** obtain **\( U_A \) \( U_B \)** where **\( U_A\in T \), \( D\subseteq U_A \), \( U_A\subseteq A \)** and **\( U_B\in T \), \( D\subseteq U_B \), \( U_B\subseteq B \)
** let **\( U = U_A\cap U_B \) ** from **assms(1), \( U_A\in T \), \( U_B\in T \), \( D\subseteq U_A \), \( D\subseteq U_B \), \( U_A\subseteq A \), \( U_B\subseteq B \) ** have ** \( U \in T \), \( D\subseteq U \), \( U \subseteq A\cap B \)** unfolding ** IsATopology_def
** with **I, \( A\in \mathcal{F} \), \( B\in \mathcal{F} \) ** have ** \( A\cap B \in \mathcal{F} \)
** } **
** thus ** \( thesis \)
** qed **

{
** fix **\( B \) \( C \) ** assume **\( B\in \mathcal{F} \), \( C\in Pow(X) \), \( B\subseteq C \)
** from **I, \( B\in \mathcal{F} \) ** obtain **\( U \)** where **\( U\in T \), \( D\subseteq U \)** and **\( U\subseteq B \)
** with **\( B\subseteq C \) ** have ** \( \exists U\in T.\ (D\subseteq U \wedge U\subseteq C) \)
** with **I, \( C\in Pow(X) \) ** have ** \( C\in \mathcal{F} \)
** } **
** thus ** \( thesis \)
** qed **

If \(N\) is a (set) neighborhood of \(A\) in \(T\), then exist an open set \(U\) such that \(N\) contains \(U\) which contains \(A\). This is similar to the Metamath's theorem with the same name, except that here we do not need assume that \(T\) is a topology (which is a bit worrying).

** lemma ** neii2:

** assumes **\( N \in (\text{ set neighborhood system of } T)(A) \)

An open set \(U\) covering a set \(A\) is a set neighborhood of \(A\).

** lemma ** open_superset_nei:

** assumes **\( V\in T \), \( A\subseteq V \)

An open set is a set neighborhood of itself.

** corollary ** open_is_nei:

** assumes **\( V\in T \)

An open neighborhood of \(x\) is a set neighborhood of \(\{ x\}\).

** corollary ** open_nei_singl:

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

The Cartesian product of two neighborhoods is a neighborhood in the product topology. Similar to the Metamath's theorem with the same name.

** lemma ** neitx:

** assumes **\( T \text{ is a topology } \), \( S \text{ is a topology } \)** and **\( A \in (\text{ set neighborhood system of } T)(C) \)** and **\( B \in (\text{ set neighborhood system of } S)(D) \)

Any neighborhood of an element of the closure of a subset intersects the subset.
This is practically the same as *neigh_inter_nempty*, just formulated in terms
of set neighborhoods of singletons.
Compare with Metamath's theorem with the same name.

** lemma ** neindisj:

** assumes **\( T \text{ is a topology } \), \( A\subseteq \bigcup T \), \( x \in \text{Closure}(A,T) \)** and **\( N \in (\text{ set neighborhood system of } T)\{x\} \)

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

Definition of NeighSystem:
\( \text{ neighborhood system of } T \equiv \{ \langle x,\{N\in Pow(\bigcup T).\ \exists U\in T.\ (x\in U \wedge U\subseteq N)\}\rangle .\ x \in \bigcup T \} \)

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

** assumes **\( x\in X \)

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

** assumes **\( A \subseteq \bigcup T \)

** assumes **\( x\in \bigcup T \)

** assumes **\( A \subseteq \bigcup T \)** and **\( U\in T \)** and **\( x \in cl(A) \cap U \)

** assumes **\( \mathcal{M} \text{ is a neighborhood system on } X \)** and **\( x\in X \)** and **\( N\in \mathcal{M} (x) \)

** assumes **\( \mathfrak{F} \text{ is a filter on } X \)

** assumes **\( \mathcal{M} \text{ is a neighborhood system on } X \)** and **\( x\in X \)** and **\( N\in \mathcal{M} (x) \)

** assumes **\( \mathcal{M} \text{ is a neighborhood system on } X \)

** defines **\( T \equiv \{U\in Pow(X).\ \forall x\in U.\ U \in \mathcal{M} (x)\} \)

** assumes **\( T \text{ is a topology } \)

** assumes **\( \mathcal{M} \text{ is a neighborhood system on } X \), \( x\in X \), \( N\in \mathcal{M} (x) \)

** defines **\( T \equiv \{U\in Pow(X).\ \forall x\in U.\ U \in \mathcal{M} (x)\} \)

** assumes **\( f: X\rightarrow Y \), \( g: X\rightarrow Z \)** and **\( \forall x\in X.\ f(x) = g(x) \)

Definition of SetNeighSystem:
\( \text{ set neighborhood system of } T \)
\( \equiv \{\langle A,\{N\in Pow(\bigcup T).\ \exists U\in T.\ (A\subseteq U \wedge U\subseteq N)\}\rangle .\ A\in Pow(\bigcup T)\} \)

** assumes **\( A \subseteq \bigcup T \)

** assumes **\( V\in T \), \( A\subseteq V \)

** assumes **\( N \in (\text{ set neighborhood system of } T)(A) \)

** assumes **\( T \text{ is a topology } \), \( S \text{ is a topology } \)

** assumes **\( T \text{ is a topology } \), \( S \text{ is a topology } \)

** assumes **\( T \text{ is a topology } \), \( N \subseteq \bigcup T \)

** assumes **\( N \in (\text{ set neighborhood system of } T)(A) \)

** assumes **\( T \text{ is a topology } \), \( S \text{ is a topology } \)** and **\( U\in T \), \( V\in S \)

** assumes **\( N \in (\text{ set neighborhood system of } T)(A) \)

** assumes **\( T \text{ is a topology } \), \( S \text{ is a topology } \)

** assumes **\( T \text{ is a topology } \), \( D \subseteq (\bigcup T) \), \( D\neq 0 \)

** assumes **\( x\in \bigcup T \)

** assumes **\( T \text{ is a topology } \), \( A\subseteq \bigcup T \), \( x \in \text{Closure}(A,T) \)** and **\( N \in (\text{ neighborhood system of } T)(x) \)