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) \)
shows \( N\subseteq X \) and \( x\in N \)proofSome 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))) \)proofGiven 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 \)proofSome 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\} \)proofOnce 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) \)proofThe 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) \)proofassumes \( T \text{ is a topology } \)
shows \( (\bigcup T) \in T \)assumes \( x\in X \)
shows \( \{\langle x,b(x)\rangle .\ x\in X\}(x)=b(x) \)assumes \( \forall x\in X.\ b(x) \in Y \)
shows \( \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y \)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) \)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)\} \)