# 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

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