# IsarMathLib

## Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

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

### From a neighborhood system to topology

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

### From a topology to a neighborhood system

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:

shows $$(\text{ neighborhood system of } T): \bigcup T \rightarrow Pow(Pow(\bigcup T))$$proof
let $$X = \bigcup T$$
have $$\forall x\in X.\ \{N\in Pow(X).\ \exists U\in T.\ (x\in U \wedge U\subseteq N)\} \in Pow(Pow(X))$$
then show $$thesis$$ unfolding NeighSystem_def using ZF_fun_from_total
qed

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$$

shows $$(\text{ neighborhood system of } T)(x) = \{N\in Pow(\bigcup T).\ \exists U\in T.\ (x\in U \wedge U\subseteq N)\}$$ using assms, ZF_fun_from_tot_val1 unfolding NeighSystem_def

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

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

shows $$N\cap A \neq 0$$proof
let $$X = \bigcup T$$
from assms(1) have cntx: $$topology0(T)$$ unfolding topology0_def
with assms(2,3) have $$x\in X$$ using Top_3_L11(1)
with assms(4) obtain $$U$$ where $$U\in T$$, $$x\in U$$ and $$U\subseteq N$$ using neigh_val
from assms(2,3), cntx, $$U\in T$$, $$x\in U$$ have $$A\cap U \neq 0$$ using cl_inter_neigh
with $$U\subseteq N$$ show $$N\cap A \neq 0$$
qed

### Neighborhood systems are 1:1 with topologies

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

shows $$N\in Pow(X)$$ and $$\exists U\in T.\ (x\in U \wedge U\subseteq N)$$proof
from assms(1) have $$\mathcal{M} :X\rightarrow Pow(Pow(X))$$ unfolding IsNeighSystem_def
with assms(2,3) show $$N\in Pow(X)$$ using apply_funtype
let $$U = \{y\in X.\ N \in \mathcal{M} (y)\}$$
have $$U\in T$$proof
have $$U \in Pow(X)$$
moreover
have $$\forall y\in U.\ U\in \mathcal{M} (y)$$proof
{
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
ultimately have $$U \in \{U\in Pow(X).\ \forall x\in U.\ U \in \mathcal{M} (x)\}$$
with assms(4) show $$U\in T$$
qed
moreover
from assms(1,2), $$N\in \mathcal{M} (x)$$ have $$x\in U \wedge U \subseteq N$$ using neighborhood_subset(2)
ultimately show $$\exists U\in T.\ (x\in U \wedge U\subseteq N)$$ by (rule witness_exists )
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)\}$$

shows $$(\text{ neighborhood system of } T) = \mathcal{M}$$proof
let $$M = \text{ neighborhood system of } T$$
from assms have $$T \text{ is a topology }$$ and $$\bigcup T = X$$ using topology_from_neighs
then have $$M \text{ is a neighborhood system on } X$$ using neigh_from_topology
with assms(1) have $$M:X\rightarrow Pow(Pow(X))$$ and $$\mathcal{M} :X\rightarrow Pow(Pow(X))$$ unfolding IsNeighSystem_def
moreover {
fix $$x$$
assume $$x\in X$$
from $$\bigcup T = X$$, $$x\in X$$ have I: $$M(x) = \{V\in Pow(X).\ \exists U\in T.\ (x\in U \wedge U\subseteq V)\}$$ unfolding NeighSystem_def using ZF_fun_from_tot_val1
have $$M(x) = \mathcal{M} (x)$$proof
{
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
}
hence $$\forall x\in X.\ M(x) = \mathcal{M} (x)$$
ultimately show $$thesis$$ by (rule func_eq )
qed

### Set neighborhoods

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$$

shows $$(\text{ neighborhood system of } T)(x) = (\text{ set neighborhood system of } T)\{x\}$$ using assms, ZF_fun_from_tot_val1 unfolding NeighSystem_def, SetNeighSystem_def

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

lemma nei_fun:

shows $$(\text{ set neighborhood system of } T):Pow(\bigcup T) \rightarrow Pow(Pow(\bigcup T))$$proof
let $$X = \bigcup T$$
have $$\forall A\in Pow(X).\ \{N\in Pow(X).\ \exists U\in T.\ (A\subseteq U \wedge U\subseteq N)\} \in Pow(Pow(X))$$
then have $$\{\langle A,\{N\in Pow(X).\ \exists U\in T.\ (A\subseteq U \wedge U\subseteq N)\}\rangle .\ A\in Pow(X)\}:Pow(X)\rightarrow Pow(Pow(X))$$ by (rule ZF_fun_from_total )
then show $$thesis$$ unfolding SetNeighSystem_def
qed

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$$

shows $$(\text{ set neighborhood system of } T)(A) = \{N\in Pow(\bigcup T).\ \exists U\in T.\ (A\subseteq U \wedge U\subseteq N)\}$$ using assms, ZF_fun_from_tot_val1 unfolding SetNeighSystem_def

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

shows $$A \subseteq \bigcup T$$ and $$N \subseteq \bigcup T$$proof
let $$f = \text{ set neighborhood system of } T$$
have $$f:Pow(\bigcup T) \rightarrow Pow(Pow(\bigcup T))$$ using nei_fun
with assms show $$A \subseteq \bigcup T$$ using arg_in_domain
with assms show $$N \subseteq \bigcup T$$ using nei_val
qed

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$$

shows $$N \in (\text{ set neighborhood system of } T)(0)$$ using assms, empty_open, nei_val

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$$

shows $$(\text{ set neighborhood system of } T)(D) \text{ is a filter on } (\bigcup T)$$proof
let $$X = \bigcup T$$
let $$\mathcal{F} = (\text{ set neighborhood system of } T)(D)$$
from assms(2) have I: $$\mathcal{F} = \{N\in Pow(X).\ \exists U\in T.\ (D\subseteq U \wedge U\subseteq N)\}$$ using nei_val
with assms(3) have $$0 \notin \mathcal{F}$$
moreover
from assms(1,2), I have $$X\in \mathcal{F}$$ using carr_open
moreover
from I have $$\mathcal{F} \subseteq Pow(X)$$
moreover
have $$\forall A\in \mathcal{F} .\ \forall B\in \mathcal{F} .\ A\cap B \in \mathcal{F}$$proof
{
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
moreover
have $$\forall B\in \mathcal{F} .\ \forall C\in Pow(X).\ B\subseteq C \longrightarrow C\in \mathcal{F}$$proof
{
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
ultimately show $$\mathcal{F} \text{ is a filter on } X$$ unfolding IsFilter_def
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)$$

shows $$\exists U\in T.\ (A\subseteq U \wedge U\subseteq N)$$proof
from assms have $$A\in Pow(\bigcup T)$$ using nei_fun, arg_in_domain
with assms show $$thesis$$ unfolding SetNeighSystem_def using ZF_fun_from_tot_val1
qed

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$$

shows $$V \in (\text{ set neighborhood system of } T)(A)$$proof
from assms have $$(\text{ set neighborhood system of } T)(A) = \{N\in Pow(\bigcup T).\ \exists U\in T.\ (A\subseteq U \wedge U\subseteq N)\}$$ using nei_val
with assms show $$thesis$$
qed

An open set is a set neighborhood of itself.

corollary open_is_nei:

assumes $$V\in T$$

shows $$V \in (\text{ set neighborhood system of } T)(V)$$ using assms, open_superset_nei

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

corollary open_nei_singl:

assumes $$V\in T$$, $$x\in V$$

shows $$V \in (\text{ set neighborhood system of } T)\{x\}$$ using assms, open_superset_nei

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

shows $$A\times B \in (\text{ set neighborhood system of } (T\times _tS))(C\times D)$$proof
have $$A\times B \subseteq \bigcup (T\times _tS)$$proof
from assms(3,4) have $$A\times B \subseteq (\bigcup T)\times (\bigcup S)$$ using nei_val_subset(2)
with assms(1,2) show $$thesis$$ using Top_1_4_T1
qed
let $$\mathcal{F} = (\text{ set neighborhood system of } (T\times _tS))(C\times D)$$
{
assume $$C=0 \vee D=0$$
with assms(1,2), $$A\times B \subseteq \bigcup (T\times _tS)$$ have $$A\times B \in \mathcal{F}$$ using Top_1_4_T1(1), nei_empty
}
moreover {
assume $$C\neq 0$$, $$D\neq 0$$
from assms(3) obtain $$U_A$$ where $$U_A\in T$$, $$C\subseteq U_A$$, $$U_A\subseteq A$$ using neii2
from assms(4) obtain $$U_B$$ where $$U_B\in S$$, $$D\subseteq U_B$$, $$U_B\subseteq B$$ using neii2
from assms(1,2), $$U_A\in T$$, $$U_B\in S$$, $$C\subseteq U_A$$, $$D\subseteq U_B$$ have $$U_A\times U_B \in T\times _tS$$ and $$C\times D \subseteq U_A\times U_B$$ using prod_open_open_prod
then have $$U_A\times U_B \in \mathcal{F}$$ using open_superset_nei
from $$U_A\subseteq A$$, $$U_B\subseteq B$$ have $$U_A\times U_B \subseteq A\times B$$
have $$\mathcal{F} \text{ is a filter on } (\bigcup (T\times _tS))$$proof
from assms(1,2) have $$(T\times _tS) \text{ is a topology }$$ using Top_1_4_T1(1)
moreover
have $$C\times D \subseteq \bigcup (T\times _tS)$$proof
from assms(3,4) have $$C\times D \subseteq (\bigcup T)\times (\bigcup S)$$ using nei_val_subset(1)
with assms(1,2) show $$thesis$$ using Top_1_4_T1(3)
qed
moreover
from $$C\neq 0$$, $$D\neq 0$$ have $$C\times D \neq 0$$
ultimately show $$\mathcal{F} \text{ is a filter on } (\bigcup (T\times _tS))$$ using nei_filter
qed
with $$U_A\times U_B \in \mathcal{F}$$, $$A\times B \subseteq \bigcup (T\times _tS)$$, $$U_A\times U_B \subseteq A\times B$$ have $$A\times B \in \mathcal{F}$$ using is_filter_def_split(5)
} ultimately show $$thesis$$
qed

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

shows $$N\cap A \neq 0$$proof
let $$X = \bigcup T$$
from assms(1) have cntx: $$topology0(T)$$ unfolding topology0_def
with assms(2,3) have $$x\in X$$ using Top_3_L11(1)
with assms show $$thesis$$ using neigh_from_nei, neigh_inter_nempty
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)$$
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 \}$$
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 ZF_fun_from_tot_val1:

assumes $$x\in X$$

shows $$\{\langle x,b(x)\rangle .\ x\in X\}(x)=b(x)$$
lemma carr_open:

assumes $$T \text{ is a topology }$$

shows $$(\bigcup T) \in T$$
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)\}$$
lemma (in topology0) Top_3_L11:

assumes $$A \subseteq \bigcup T$$

shows $$cl(A) \subseteq \bigcup T$$, $$cl(\bigcup T - A) = \bigcup T - int(A)$$
lemma neigh_val:

assumes $$x\in \bigcup T$$

shows $$(\text{ neighborhood system of } T)(x) = \{N\in Pow(\bigcup T).\ \exists U\in T.\ (x\in U \wedge U\subseteq N)\}$$
lemma (in topology0) cl_inter_neigh:

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

shows $$A\cap U \neq 0$$
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$$
lemma is_filter_def_split:

assumes $$\mathfrak{F} \text{ is a filter on } X$$

shows $$0\notin \mathfrak{F}$$, $$X\in \mathfrak{F}$$, $$\mathfrak{F} \subseteq Pow(X)$$, $$\forall A\in \mathfrak{F} .\ \forall B\in \mathfrak{F} .\ A\cap B\in \mathfrak{F}$$ and $$\forall B\in \mathfrak{F} .\ \forall C\in Pow(X).\ B\subseteq C \longrightarrow C\in \mathfrak{F}$$
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$$
lemma witness_exists:

assumes $$x\in X$$ and $$\phi (x)$$

shows $$\exists x\in X.\ \phi (x)$$
theorem topology_from_neighs:

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

shows $$T \text{ is a topology }$$ and $$\bigcup T = X$$
theorem neigh_from_topology:

assumes $$T \text{ is a topology }$$

shows $$(\text{ neighborhood system of } T) \text{ is a neighborhood system on } (\bigcup T)$$
lemma open_nei_in_nei:

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

shows $$N\in Pow(X)$$ and $$\exists U\in T.\ (x\in U \wedge U\subseteq N)$$
lemma func_eq:

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

shows $$f = g$$
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)\}$$
lemma nei_fun: shows $$(\text{ set neighborhood system of } T):Pow(\bigcup T) \rightarrow Pow(Pow(\bigcup T))$$
lemma arg_in_domain:

assumes $$f:X\rightarrow Y$$, $$y\in f(x)$$

shows $$x\in X$$
lemma nei_val:

assumes $$A \subseteq \bigcup T$$

shows $$(\text{ set neighborhood system of } T)(A) = \{N\in Pow(\bigcup T).\ \exists U\in T.\ (A\subseteq U \wedge U\subseteq N)\}$$
lemma empty_open:

assumes $$T \text{ is a topology }$$

shows $$0 \in T$$
lemma open_superset_nei:

assumes $$V\in T$$, $$A\subseteq V$$

shows $$V \in (\text{ set neighborhood system of } T)(A)$$
lemma nei_val_subset:

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

shows $$A \subseteq \bigcup T$$ and $$N \subseteq \bigcup T$$
theorem Top_1_4_T1:

assumes $$T \text{ is a topology }$$, $$S \text{ is a topology }$$

shows $$(T\times _tS) \text{ is a topology }$$, $$\text{ProductCollection}(T,S) \text{ is a base for } (T\times _tS)$$, $$\bigcup (T\times _tS) = \bigcup T \times \bigcup S$$
theorem Top_1_4_T1:

assumes $$T \text{ is a topology }$$, $$S \text{ is a topology }$$

shows $$(T\times _tS) \text{ is a topology }$$, $$\text{ProductCollection}(T,S) \text{ is a base for } (T\times _tS)$$, $$\bigcup (T\times _tS) = \bigcup T \times \bigcup S$$
lemma nei_empty:

assumes $$T \text{ is a topology }$$, $$N \subseteq \bigcup T$$

shows $$N \in (\text{ set neighborhood system of } T)(0)$$
lemma neii2:

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

shows $$\exists U\in T.\ (A\subseteq U \wedge U\subseteq N)$$
lemma prod_open_open_prod:

assumes $$T \text{ is a topology }$$, $$S \text{ is a topology }$$ and $$U\in T$$, $$V\in S$$

shows $$U\times V \in \text{ProductTopology}(T,S)$$
lemma nei_val_subset:

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

shows $$A \subseteq \bigcup T$$ and $$N \subseteq \bigcup T$$
theorem Top_1_4_T1:

assumes $$T \text{ is a topology }$$, $$S \text{ is a topology }$$

shows $$(T\times _tS) \text{ is a topology }$$, $$\text{ProductCollection}(T,S) \text{ is a base for } (T\times _tS)$$, $$\bigcup (T\times _tS) = \bigcup T \times \bigcup S$$
theorem nei_filter:

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

shows $$(\text{ set neighborhood system of } T)(D) \text{ is a filter on } (\bigcup T)$$
lemma neigh_from_nei:

assumes $$x\in \bigcup T$$

shows $$(\text{ neighborhood system of } T)(x) = (\text{ set neighborhood system of } T)\{x\}$$
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)$$

shows $$N\cap A \neq 0$$