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
qed
have \( U\subseteq N \)
moreover from areNeigh have \( \forall y\in U.\ (N\in \mathcal{M} (y)) \)
ultimately show \( thesis \)
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 {
}
ultimately show \( \bigcup \mathfrak{U} \in T \) using Tdef
qed
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
moreover {
}
ultimately show \( T \text{ is a topology } \) unfolding IsATopology_def
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 {
}
ultimately show \( U\cap V \in T \) using Tdef
qed
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
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_defThe 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) \)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
qed
have \( X\in \mathfrak{F} \)proof
moreover 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
have \( \forall A\in \mathfrak{F} .\ \forall B\in \mathfrak{F} .\ A\cap B \in \mathfrak{F} \)proof
moreover {
}
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
have \( \forall B\in \mathfrak{F} .\ \forall C\in Pow(X).\ B\subseteq C \longrightarrow C\in \mathfrak{F} \)proof
ultimately have \( \mathfrak{F} \text{ is a filter on } X \) unfolding IsFilter_def
{
}
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
with Mdef, \( x\in X \) show \( \mathcal{M} (x) \text{ is a filter on } X \) using ZF_fun_from_tot_val1, NeighSystem_def
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
qed
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
ultimately show \( thesis \) unfolding IsNeighSystem_def
{
}
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) \)
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
qed
have \( \forall y\in U.\ U\in \mathcal{M} (y) \)proof
ultimately have \( U \in \{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
with assms(4) show \( U\in T \)
moreover
qed
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 )
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 {
}
qed
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 )
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_defThe 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_defA 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_valIf \(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
qed
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
moreover {
}
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
have \( \forall B\in \mathcal{F} .\ \forall C\in Pow(X).\ B\subseteq C \longrightarrow C\in \mathcal{F} \)proof
ultimately show \( \mathcal{F} \text{ is a filter on } X \) unfolding IsFilter_def
{
}
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) \)
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_neiAn 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_neiThe 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 {
}
ultimately show \( thesis \)
qed
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
qed
have \( C\times D \subseteq \bigcup (T\times _tS) \)proof
moreover 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
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
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)
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 (\emptyset \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 \setminus A) = \bigcup T \setminus 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 \( \emptyset \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 \( \emptyset \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 \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8