begin
This theory deals with convergence in topological spaces. Contributed by Daniel de la Concepcion.
Nets
Nets are a generalization of sequences. It is known that sequences do not determine the behavior of the topological spaces that are not first countable; i.e., have a countable neighborhood base for each point. To solve this problem, nets were defined so that the behavior of any topological space can be thought in terms of convergence of nets.
We say that a relation \(r\) directs a set \(X\) if the relation is reflexive, transitive on \(X\) and for every two elements \(x,y\) of \(X\) there is some element \(z\) such that both \(x\) and \(y\) are in the relation with \(z\). Note that this naming is a bit inconsistent with what is defined in Order_ZF where we define what it means that \(r\) \( up-directs \) \(X\) (the third condition in the definition below) or \(r\) \( down-directs \) \(X\). This naming inconsistency will be fixed in the future (maybe).
definition
\( r\text{ directs }X \equiv \text{refl}(X,r) \wedge \text{trans}(r) \wedge (\forall x\in X.\ \forall y\in X.\ \exists z\in X.\ \langle x,z\rangle \in r \wedge \langle y,z\rangle \in r) \)
Any linear order is a directed set; in particular \((\mathbb{N},\leq)\).
lemma linorder_imp_directed:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( r\text{ directs }X \)proof from assms have \( \text{trans}(r) \) using IsLinOrder_def
moreover
}
ultimately show \( thesis \) using IsDirectedSet_def, function_def
qed
from assms have r: \( \text{refl}(X,r) \) using IsLinOrder_def, total_is_refl
moreover {
fix \( x \) \( y \)
assume R: \( x\in X \), \( y\in X \)
with assms have \( \langle x,y\rangle \in r \vee \langle y,x\rangle \in r \) using IsLinOrder_def, IsTotal_def
with r have \( (\langle x,y\rangle \in r \wedge \langle y,y\rangle \in r)\vee (\langle y,x\rangle \in r \wedge \langle x,x\rangle \in r) \) using R, refl_def
then have \( \exists z\in X.\ \langle x,z\rangle \in r \wedge \langle y,z\rangle \in r \) using R
Natural numbers are a directed set.
corollary Le_directs_nat:
shows \( \text{IsLinOrder}(nat,Le) \), \( Le\text{ directs }nat \)proof show \( \text{IsLinOrder}(nat,Le) \) by (rule NatOrder_ZF_1_L2 )
then show \( Le\text{ directs }nat \) using linorder_imp_directed
qed
We are able to define the concept of net, now that we now what a directed set is.
definition
\( N \text{ is a net on } X \equiv \text{fst}(N):domain(\text{fst}(N))\rightarrow X \wedge (\text{snd}(N)\text{ directs }domain(\text{fst}(N))) \wedge domain(\text{fst}(N))\neq 0 \)
Provided a topology and a net directed on its underlying set, we can talk about convergence of the net in the topology.
definition (in topology0)
\( N \text{ is a net on } \bigcup T \Longrightarrow N \rightarrow _N x \equiv \) \( (x\in \bigcup T) \wedge (\forall U\in Pow(\bigcup T).\ (x\in int(U) \longrightarrow (\exists t\in domain(\text{fst}(N)).\ \forall m\in domain(\text{fst}(N)).\ \) \( (\langle t,m\rangle \in \text{snd}(N) \longrightarrow \text{fst}(N)m\in U)))) \)
One of the most important directed sets, is the neighborhoods of a point.
theorem (in topology0) directedset_neighborhoods:
assumes \( x\in \bigcup T \)
defines \( \text{Neigh}\equiv \{U\in Pow(\bigcup T).\ x\in int(U)\} \)
defines \( r\equiv \{\langle U,V\rangle \in (\text{Neigh} \times \text{Neigh}).\ V\subseteq U\} \)
shows \( r\text{ directs }\text{Neigh} \)proof{
}
fix \( U \)
assume \( U \in \text{Neigh} \)
then have \( \langle U,U\rangle \in r \) using r_def
then have \( \text{refl}(\text{Neigh},r) \) using refl_def
moreover {
}
}
ultimately show \( thesis \) using IsDirectedSet_def
qed
fix \( U \) \( V \) \( W \)
assume \( \langle U,V\rangle \in r \), \( \langle V,W\rangle \in r \)
then have \( U \in \text{Neigh} \), \( W \in \text{Neigh} \), \( W\subseteq U \) using r_def
then have \( \langle U,W\rangle \in r \) using r_def
then have \( \text{trans}(r) \) using trans_def
moreover {
fix \( A \) \( B \)
assume p: \( A\in \text{Neigh} \), \( B\in \text{Neigh} \)
have \( A\cap B \in \text{Neigh} \)proof
from p have \( A\cap B \in Pow(\bigcup T) \) using Neigh_def
moreover {
}
ultimately show \( thesis \) using Neigh_def
qed
from p have \( x\in int(A) \), \( x\in int(B) \) using Neigh_def
then have \( x\in int(A)\cap int(B) \)
moreover {
}
ultimately have \( x \in int(A\cap B) \)
have \( int(A)\cap int(B)\subseteq A\cap B \) using Top_2_L1
moreover
have \( int(A)\cap int(B)\in T \) using Top_2_L2, Top_2_L2, topSpaceAssum, IsATopology_def
ultimately have \( int(A)\cap int(B)\subseteq int(A\cap B) \) using Top_2_L5
moreover
from \( A\cap B \in \text{Neigh} \) have \( \langle A,A\cap B\rangle \in r \wedge \langle B,A\cap B\rangle \in r \) using r_def, p
ultimately have \( \exists z\in \text{Neigh}.\ \langle A,z\rangle \in r \wedge \langle B,z\rangle \in r \)
There can be nets directed by the neighborhoods that converge to the point; if there is a choice function.
theorem (in topology0) net_direct_neigh_converg:
assumes \( x\in \bigcup T \)
defines \( \text{Neigh}\equiv \{U\in Pow(\bigcup T).\ x\in int(U)\} \)
defines \( r\equiv \{\langle U,V\rangle \in (\text{Neigh} \times \text{Neigh}).\ V\subseteq U\} \)
assumes \( f:\text{Neigh}\rightarrow \bigcup T \), \( \forall U\in \text{Neigh}.\ f(U) \in U \)
shows \( \langle f,r\rangle \rightarrow _N x \)proof from assms(4) have dom_def: \( \text{Neigh} = domain(f) \) using Pi_def
moreover
{
have \( \bigcup T\in T \) using topSpaceAssum, IsATopology_def
then have \( int(\bigcup T)=\bigcup T \) using Top_2_L3
with assms(1) have \( \bigcup T\in \text{Neigh} \) using Neigh_def
then have \( \bigcup T\in domain(\text{fst}(\langle f,r\rangle )) \) using dom_def
moreover from assms(4), dom_def have \( \text{fst}(\langle f,r\rangle ):domain(\text{fst}(\langle f,r\rangle ))\rightarrow \bigcup T \)
moreover from assms(1,2,3), dom_def have \( \text{snd}(\langle f,r\rangle )\text{ directs }domain(\text{fst}(\langle f,r\rangle )) \) using directedset_neighborhoods
ultimately have Net: \( \langle f,r\rangle \text{ is a net on } \bigcup T \) unfolding IsNet_def
fix \( U \)
assume \( U \in Pow(\bigcup T) \), \( x \in int(U) \)
then have \( U \in \text{Neigh} \) using Neigh_def
then have t: \( U \in domain(f) \) using dom_def
{
fix \( W \)
assume A: \( W\in domain(f) \), \( \langle U,W\rangle \in r \)
then have \( W\in \text{Neigh} \) using dom_def
with assms(5) have \( fW\in W \)
with A(2), r_def have \( fW\in U \)
then have \( \forall W\in domain(f).\ (\langle U,W\rangle \in r \longrightarrow fW\in U) \)
with t have \( \exists V\in domain(f).\ \forall W\in domain(f).\ (\langle V,W\rangle \in r \longrightarrow fW\in U) \)
then have \( \forall U\in Pow(\bigcup T).\ (x\in int(U) \longrightarrow (\exists V\in domain(f).\ \forall W\in domain(f).\ (\langle V,W\rangle \in r \longrightarrow f(W) \in U))) \)
with assms(1), Net show \( thesis \) using NetConverges_def
qed
Filters
Nets are a generalization of sequences that can make us see that not all topological spaces can be described by sequences. Nevertheless, nets are not always the tool used to deal with convergence. The reason is that they make use of directed sets which are completely unrelated with the topology.
The topological tools to deal with convergence are what is called filters.
definition
\( \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} ) \)
The next lemma splits the the definition of a filter into four conditions to make it easier to reference each one separately in proofs.
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} \) using assms unfolding IsFilter_defNot all the sets of a filter are needed to be consider at all times; as it happens with a topology we can consider bases.
definition
\( C \text{ is a base filter } \mathfrak{F} \equiv C\subseteq \mathfrak{F} \wedge \mathfrak{F} =\{A\in Pow(\bigcup \mathfrak{F} ).\ (\exists D\in C.\ D\subseteq A)\} \)
Not every set is a base for a filter, as it happens with topologies, there is a condition to be satisfied.
definition
\( C \text{ satisfies the filter base condition } \equiv (\forall A\in C.\ \forall B\in C.\ \exists D\in C.\ D\subseteq A\cap B) \wedge C\neq 0 \wedge 0\notin C \)
Every set of a filter contains a set from the filter's base.
lemma basic_element_filter:
assumes \( A\in \mathfrak{F} \) and \( C \text{ is a base filter } \mathfrak{F} \)
shows \( \exists D\in C.\ D\subseteq A \)proof from assms(2) have t: \( \mathfrak{F} =\{A\in Pow(\bigcup \mathfrak{F} ).\ (\exists D\in C.\ D\subseteq A)\} \) using IsBaseFilter_def
with assms(1) have \( A\in \{A\in Pow(\bigcup \mathfrak{F} ).\ (\exists D\in C.\ D\subseteq A)\} \)
then have \( A\in Pow(\bigcup \mathfrak{F} ) \), \( \exists D\in C.\ D\subseteq A \)
then show \( thesis \)
qed
The following two results state that the filter base condition is necessary and sufficient for the filter generated by a base, to be an actual filter. The third result, rewrites the previous two.
theorem basic_filter_1:
assumes \( C \text{ is a base filter } \mathfrak{F} \) and \( C \text{ satisfies the filter base condition } \)
shows \( \mathfrak{F} \text{ is a filter on } \bigcup \mathfrak{F} \)proof{
}
fix \( A \) \( B \)
assume AF: \( A\in \mathfrak{F} \) and BF: \( B\in \mathfrak{F} \)
with assms(1) have \( \exists DA\in C.\ DA\subseteq A \) using basic_element_filter
then obtain \( DA \) where perA: \( DA\in C \) and subA: \( DA\subseteq A \)
from BF, assms have \( \exists DB\in C.\ DB\subseteq B \) using basic_element_filter
then obtain \( DB \) where perB: \( DB\in C \) and subB: \( DB\subseteq B \)
from assms(2), perA, perB have \( \exists D\in C.\ D\subseteq DA\cap DB \) unfolding SatisfiesFilterBase_def
then obtain \( D \) where \( D\in C \), \( D\subseteq DA\cap DB \)
with subA, subB, AF, BF have \( A\cap B\in \{A \in Pow(\bigcup \mathfrak{F} ) .\ \exists D\in C.\ D \subseteq A\} \)
with assms(1) have \( A\cap B\in \mathfrak{F} \) unfolding IsBaseFilter_def
moreover {
}
moreover
}
qed
fix \( A \) \( B \)
assume AF: \( A\in \mathfrak{F} \) and BS: \( B\in Pow(\bigcup \mathfrak{F} ) \) and sub: \( A\subseteq B \)
from assms(1), AF have \( \exists D\in C.\ D\subseteq A \) using basic_element_filter
then obtain \( D \) where \( D\subseteq A \), \( D\in C \)
with sub, BS have \( B\in \{A\in Pow(\bigcup \mathfrak{F} ).\ \exists D\in C.\ D\subseteq A\} \)
with assms(1) have \( B\in \mathfrak{F} \) unfolding IsBaseFilter_def
from assms(2) have \( C\neq 0 \) using SatisfiesFilterBase_def
then obtain \( D \) where \( D\in C \)
with assms(1) have \( D\subseteq \bigcup \mathfrak{F} \) using IsBaseFilter_def
with \( D\in C \) have \( \bigcup \mathfrak{F} \in \{A\in Pow(\bigcup \mathfrak{F} ).\ \exists D\in C.\ D\subseteq A\} \)
with assms(1) have \( \bigcup \mathfrak{F} \in \mathfrak{F} \) unfolding IsBaseFilter_def
moreover {
assume \( 0\in \mathfrak{F} \)
with assms(1) have \( \exists D\in C.\ D\subseteq 0 \) using basic_element_filter
then obtain \( D \) where \( D\in C \), \( D\subseteq 0 \)
then have \( D\in C \), \( D=0 \)
with assms(2) have \( False \) using SatisfiesFilterBase_def
then have \( 0\notin \mathfrak{F} \)
ultimately show \( thesis \) using IsFilter_def
A base filter satisfies the filter base condition.
theorem basic_filter_2:
assumes \( C \text{ is a base filter } \mathfrak{F} \) and \( \mathfrak{F} \text{ is a filter on } \bigcup \mathfrak{F} \)
shows \( C \text{ satisfies the filter base condition } \)proof{
}
fix \( A \) \( B \)
assume AF: \( A\in C \) and BF: \( B\in C \)
then have \( A\in \mathfrak{F} \) and \( B\in \mathfrak{F} \) using assms(1), IsBaseFilter_def
then have \( A\cap B\in \mathfrak{F} \) using assms(2), IsFilter_def
then have \( \exists D\in C.\ D\subseteq A\cap B \) using assms(1), basic_element_filter
then have \( \forall A\in C.\ \forall B\in C.\ \exists D\in C.\ D\subseteq A\cap B \)
moreover {
}
}
qed
assume \( 0\in C \)
then have \( 0\in \mathfrak{F} \) using assms(1), IsBaseFilter_def
then have \( False \) using assms(2), IsFilter_def
then have \( 0\notin C \)
moreover {
assume \( C=0 \)
then have \( \mathfrak{F} =0 \) using assms(1), IsBaseFilter_def
then have \( False \) using assms(2), IsFilter_def
then have \( C\neq 0 \)
ultimately show \( thesis \) using SatisfiesFilterBase_def
A base filter for a collection satisfies the filter base condition iff that collection is in fact a filter.
theorem basic_filter:
assumes \( C \text{ is a base filter } \mathfrak{F} \)
shows \( (C \text{ satisfies the filter base condition }) \longleftrightarrow (\mathfrak{F} \text{ is a filter on } \bigcup \mathfrak{F} ) \) using assms, basic_filter_1, basic_filter_2A base for a filter determines a filter up to the underlying set.
theorem base_unique_filter:
assumes \( C \text{ is a base filter } \mathfrak{F} 1 \) and \( C \text{ is a base filter } \mathfrak{F} 2 \)
shows \( \mathfrak{F} 1=\mathfrak{F} 2 \longleftrightarrow \bigcup \mathfrak{F} 1=\bigcup \mathfrak{F} 2 \) using assms unfolding IsBaseFilter_defSuppose that we take any nonempty collection \(C\) of subsets of some set \(X\). Then this collection is a base filter for the collection of all supersets (in \(X\)) of sets from \(C\).
theorem base_unique_filter_set1:
assumes \( C \subseteq Pow(X) \) and \( C\neq 0 \)
shows \( C \text{ is a base filter } \{A\in Pow(X).\ \exists D\in C.\ D\subseteq A\} \) and \( \bigcup \{A\in Pow(X).\ \exists D\in C.\ D\subseteq A\}=X \)proof from assms(1) have \( C\subseteq \{A\in Pow(X).\ \exists D\in C.\ D\subseteq A\} \)
moreover
qed
from assms(2) obtain \( D \) where \( D\in C \)
then have \( D\subseteq X \) using assms(1)
with \( D\in C \) have \( X\in \{A\in Pow(X).\ \exists D\in C.\ D\subseteq A\} \)
then show \( \bigcup \{A\in Pow(X).\ \exists D\in C.\ D\subseteq A\}=X \)
ultimately show \( C \text{ is a base filter } \{A\in Pow(X).\ \exists D\in C.\ D\subseteq A\} \) using IsBaseFilter_def
A collection \(C\) that satisfies the filter base condition is a base filter for some other collection \(\frak F\) iff \(\frak F\) is the collection of supersets of \(C\).
theorem base_unique_filter_set2:
assumes \( C\subseteq Pow(X) \) and \( C \text{ satisfies the filter base condition } \)
shows \( ((C \text{ is a base filter } \mathfrak{F} ) \wedge \bigcup \mathfrak{F} =X) \longleftrightarrow \mathfrak{F} =\{A\in Pow(X).\ \exists D\in C.\ D\subseteq A\} \) using assms, IsBaseFilter_def, SatisfiesFilterBase_def, base_unique_filter_set1A simple corollary from the previous lemma.
corollary base_unique_filter_set3:
assumes \( C\subseteq Pow(X) \) and \( C \text{ satisfies the filter base condition } \)
shows \( C \text{ is a base filter } \{A\in Pow(X).\ \exists D\in C.\ D\subseteq A\} \) and \( \bigcup \{A\in Pow(X).\ \exists D\in C.\ D\subseteq A\} = X \)proof let \( \mathfrak{F} = \{A\in Pow(X).\ \exists D\in C.\ D\subseteq A\} \)
from assms have \( (C \text{ is a base filter } \mathfrak{F} ) \wedge \bigcup \mathfrak{F} =X \) using base_unique_filter_set2
thus \( C \text{ is a base filter } \mathfrak{F} \) and \( \bigcup \mathfrak{F} = X \)
qed
The convergence for filters is much easier concept to write. Given a topology and a filter on the same underlying set, we can define convergence as containing all the neighborhoods of the point.
definition (in topology0)
\( \mathfrak{F} \text{ is a filter on }\bigcup T \Longrightarrow \mathfrak{F} \rightarrow _Fx \equiv \) \( x\in \bigcup T \wedge (\{U\in Pow(\bigcup T).\ x\in int(U)\} \subseteq \mathfrak{F} ) \)
The neighborhoods of a point form a filter that converges to that point.
lemma (in topology0) neigh_filter:
assumes \( x\in \bigcup T \)
defines \( \text{Neigh}\equiv \{U\in Pow(\bigcup T).\ x\in int(U)\} \)
shows \( \text{Neigh} \text{ is a filter on }\bigcup T \) and \( \text{Neigh} \rightarrow _F x \)proof{
}
fix \( A \) \( B \)
assume p: \( A\in \text{Neigh} \), \( B\in \text{Neigh} \)
have \( A\cap B\in \text{Neigh} \)proof
from p have \( A\cap B\in Pow(\bigcup T) \) using Neigh_def
moreover {
}
ultimately show \( thesis \) using Neigh_def
qed
from p have \( x\in int(A) \), \( x\in int(B) \) using Neigh_def
then have \( x\in int(A)\cap int(B) \)
moreover {
}
ultimately have \( x\in int(A\cap B) \)
have \( int(A)\cap int(B)\subseteq A\cap B \) using Top_2_L1
moreover
have \( int(A)\cap int(B)\in T \) using Top_2_L2, topSpaceAssum, IsATopology_def
ultimately have \( int(A)\cap int(B)\subseteq int(A\cap B) \) using Top_2_L5
moreover {
}
moreover {
}
fix \( A \) \( B \)
assume A: \( A\in \text{Neigh} \) and B: \( B\in Pow(\bigcup T) \) and sub: \( A\subseteq B \)
from sub have \( int(A)\in T \), \( int(A)\subseteq B \) using Top_2_L2, Top_2_L1
then have \( int(A)\subseteq int(B) \) using Top_2_L5
with A have \( x\in int(B) \) using Neigh_def
with B have \( B\in \text{Neigh} \) using Neigh_def
assume \( 0\in \text{Neigh} \)
then have \( x\in \text{Interior}(0,T) \) using Neigh_def
then have \( x\in 0 \) using Top_2_L1
then have \( False \)
then have \( 0\notin \text{Neigh} \)
moreover have \( \bigcup T\in T \) using topSpaceAssum, IsATopology_def
then have \( \text{Interior}(\bigcup T,T)=\bigcup T \) using Top_2_L3
with assms(1) have ab: \( \bigcup T\in \text{Neigh} \) unfolding Neigh_def
moreover have \( \text{Neigh}\subseteq Pow(\bigcup T) \) using Neigh_def
ultimately show \( \text{Neigh} \text{ is a filter on } \bigcup T \) using IsFilter_def
moreover
qed
from ab have \( \bigcup \text{Neigh}=\bigcup T \) unfolding Neigh_def
ultimately show \( \text{Neigh} \rightarrow _F x \) using FilterConverges_def, assms(1), Neigh_def
Note that with the net we built in a previous result, it wasn't clear that we could construct an actual net that converged to the given point without the axiom of choice. With filters, there is no problem.
Another positive point of filters is due to the existence of filter basis. If we have a basis for a filter, then the filter converges to a point iff every neighborhood of that point contains a basic filter element.
theorem (in topology0) convergence_filter_base1:
assumes \( \mathfrak{F} \text{ is a filter on } \bigcup T \) and \( C \text{ is a base filter } \mathfrak{F} \) and \( \mathfrak{F} \rightarrow _F x \)
shows \( \forall U\in Pow(\bigcup T).\ x\in int(U) \longrightarrow (\exists D\in C.\ D\subseteq U) \) and \( x\in \bigcup T \)proof{
}
fix \( U \)
assume \( U\subseteq (\bigcup T) \) and \( x\in int(U) \)
with assms(1,3) have \( U\in \mathfrak{F} \) using FilterConverges_def
with assms(2) have \( \exists D\in C.\ D\subseteq U \) using basic_element_filter
thus \( \forall U\in Pow(\bigcup T).\ x\in int(U) \longrightarrow (\exists D\in C.\ D\subseteq U) \)
from assms(1,3) show \( x\in \bigcup T \) using FilterConverges_def
qed
A sufficient condition for a filter to converge to a point.
theorem (in topology0) convergence_filter_base2:
assumes \( \mathfrak{F} \text{ is a filter on } \bigcup T \) and \( C \text{ is a base filter } \mathfrak{F} \) and \( \forall U\in Pow(\bigcup T).\ x\in int(U) \longrightarrow (\exists D\in C.\ D\subseteq U) \) and \( x\in \bigcup T \)
shows \( \mathfrak{F} \rightarrow _F x \)proof{
}
fix \( U \)
assume AS: \( U\in Pow(\bigcup T) \), \( x\in int(U) \)
then obtain \( D \) where pD: \( D\in C \) and s: \( D\subseteq U \) using assms(3)
with assms(2), AS have \( D\in \mathfrak{F} \) and \( D\subseteq U \) and \( U\in Pow(\bigcup T) \) using IsBaseFilter_def
with assms(1) have \( U\in \mathfrak{F} \) using IsFilter_def
with assms(1,4) show \( thesis \) using FilterConverges_def
qed
A necessary and sufficient condition for a filter to converge to a point.
theorem (in topology0) convergence_filter_base_eq:
assumes \( \mathfrak{F} \text{ is a filter on } \bigcup T \) and \( C \text{ is a base filter } \mathfrak{F} \)
shows \( (\mathfrak{F} \rightarrow _F x) \longleftrightarrow ((\forall U\in Pow(\bigcup T).\ x\in int(U) \longrightarrow (\exists D\in C.\ D\subseteq U)) \wedge x\in \bigcup T) \)proof assume \( \mathfrak{F} \rightarrow _F x \)
with assms show \( ((\forall U\in Pow(\bigcup T).\ x\in int(U) \longrightarrow (\exists D\in C.\ D\subseteq U)) \wedge x\in \bigcup T) \) using convergence_filter_base1
next
assume \( (\forall U\in Pow(\bigcup T).\ x\in int(U) \longrightarrow (\exists D\in C.\ D\subseteq U)) \wedge x\in \bigcup T \)
with assms show \( \mathfrak{F} \rightarrow _F x \) using convergence_filter_base2
qed
Relation between nets and filters
In this section we show that filters do not generalize nets, but still nets and filter are in w way equivalent as far as convergence is considered.
Let's build now a net from a filter, such that both converge to the same points.
definition
\( \mathfrak{F} \text{ is a filter on } \bigcup \mathfrak{F} \Longrightarrow \text{Net}(\mathfrak{F} ) \equiv \) \( \langle \{\langle A,\text{fst}(A)\rangle .\ A\in \{\langle x,F\rangle \in (\bigcup \mathfrak{F} )\times \mathfrak{F} .\ x\in F\}\},\{\langle A,B\rangle \in \{\langle x,F\rangle \in (\bigcup \mathfrak{F} )\times \mathfrak{F} .\ x\in F\}\times \{\langle x,F\rangle \in (\bigcup \mathfrak{F} )\times \mathfrak{F} .\ x\in F\}.\ \text{snd}(B)\subseteq \text{snd}(A)\}\rangle \)
Net of a filter is indeed a net.
theorem net_of_filter_is_net:
assumes \( \mathfrak{F} \text{ is a filter on } X \)
shows \( (\text{Net}(\mathfrak{F} )) \text{ is a net on } X \)proof from assms have \( X\in \mathfrak{F} \), \( \mathfrak{F} \subseteq Pow(X) \) using IsFilter_def
then have uu: \( \bigcup \mathfrak{F} =X \)
let \( f = \{\langle A,\text{fst}(A)\rangle .\ A\in \{\langle x,F\rangle \in (\bigcup \mathfrak{F} )\times \mathfrak{F} .\ x\in F\}\} \)
let \( r = \{\langle A,B\rangle \in \{\langle x,F\rangle \in (\bigcup \mathfrak{F} )\times \mathfrak{F} .\ x\in F\}\times \{\langle x,F\rangle \in (\bigcup \mathfrak{F} )\times \mathfrak{F} .\ x\in F\}.\ \text{snd}(B)\subseteq \text{snd}(A)\} \)
have \( function(f) \) using function_def
moreover
have \( relation(f) \) using relation_def
ultimately have \( f:domain(f)\rightarrow \text{range}(f) \) using function_imp_Pi
have dom: \( domain(f)=\{\langle x,F\rangle \in (\bigcup \mathfrak{F} )\times \mathfrak{F} .\ x\in F\} \)
have \( \text{range}(f)\subseteq \bigcup \mathfrak{F} \)
with \( f:domain(f)\rightarrow \text{range}(f) \) have \( f:domain(f)\rightarrow \bigcup \mathfrak{F} \) using fun_weaken_type
moreover {
}
ultimately have \( \langle f,r\rangle \text{ is a net on }\bigcup \mathfrak{F} \) using IsNet_def
qed
{
}
}
moreover {
fix \( t \)
assume pp: \( t\in domain(f) \)
then have \( \text{snd}(t)\subseteq \text{snd}(t) \)
with dom, pp have \( \langle t,t\rangle \in r \)
then have \( \text{refl}(domain(f),r) \) using refl_def
moreover {
}
}
}
fix \( t1 \) \( t2 \) \( t3 \)
assume \( \langle t1,t2\rangle \in r \), \( \langle t2,t3\rangle \in r \)
then have \( \text{snd}(t3)\subseteq \text{snd}(t1) \), \( t1\in domain(f) \), \( t3\in domain(f) \) using dom
then have \( \langle t1,t3\rangle \in r \)
then have \( \text{trans}(r) \) using trans_def
moreover {
fix \( x \) \( y \)
assume as: \( x\in domain(f) \), \( y\in domain(f) \)
then have \( \text{snd}(x)\in \mathfrak{F} \), \( \text{snd}(y)\in \mathfrak{F} \)
then have p: \( \text{snd}(x)\cap \text{snd}(y)\in \mathfrak{F} \) using assms, IsFilter_def
{
assume \( \text{snd}(x)\cap \text{snd}(y)=0 \)
with p have \( 0\in \mathfrak{F} \)
then have \( False \) using assms, IsFilter_def
then have \( \text{snd}(x)\cap \text{snd}(y)\neq 0 \)
then obtain \( xy \) where \( xy\in \text{snd}(x)\cap \text{snd}(y) \)
then have \( xy\in \text{snd}(x)\cap \text{snd}(y) \), \( \langle xy,\text{snd}(x)\cap \text{snd}(y)\rangle \in (\bigcup \mathfrak{F} )\times \mathfrak{F} \) using p
then have \( \langle xy,\text{snd}(x)\cap \text{snd}(y)\rangle \in \{\langle x,F\rangle \in (\bigcup \mathfrak{F} )\times \mathfrak{F} .\ x\in F\} \)
with dom have d: \( \langle xy,\text{snd}(x)\cap \text{snd}(y)\rangle \in domain(f) \)
with as have \( \langle x,\langle xy,\text{snd}(x)\cap \text{snd}(y)\rangle \rangle \in r \wedge \langle y,\langle xy,\text{snd}(x)\cap \text{snd}(y)\rangle \rangle \in r \)
with d have \( \exists z\in domain(f).\ \langle x,z\rangle \in r \wedge \langle y,z\rangle \in r \)
then have \( \forall x\in domain(f).\ \forall y\in domain(f).\ \exists z\in domain(f).\ \langle x,z\rangle \in r \wedge \langle y,z\rangle \in r \)
ultimately have \( r\text{ directs }domain(f) \) using IsDirectedSet_def
have p: \( X\in \mathfrak{F} \) and \( 0\notin \mathfrak{F} \) using assms, IsFilter_def
then have \( X\neq 0 \)
then obtain \( q \) where \( q\in X \)
with p, dom have \( \langle q,X\rangle \in domain(f) \)
then have \( domain(f)\neq 0 \)
then show \( (\text{Net}(\mathfrak{F} )) \text{ is a net on } X \) using NetOfFilter_def, assms, uu
If a filter converges to some point then its net converges to the same point.
theorem (in topology0) filter_conver_net_of_filter_conver:
assumes \( \mathfrak{F} \text{ is a filter on } \bigcup T \) and \( \mathfrak{F} \rightarrow _F x \)
shows \( (\text{Net}(\mathfrak{F} )) \rightarrow _N x \)proof from assms have \( \bigcup T\in \mathfrak{F} \), \( \mathfrak{F} \subseteq Pow(\bigcup T) \) using IsFilter_def
then have uu: \( \bigcup \mathfrak{F} =\bigcup T \)
from assms(1) have func: \( \text{fst}(\text{Net}(\mathfrak{F} ))=\{\langle A,\text{fst}(A)\rangle .\ A\in \{\langle x,F\rangle \in (\bigcup \mathfrak{F} )\times \mathfrak{F} .\ x\in F\}\} \) and dir: \( \text{snd}(\text{Net}(\mathfrak{F} ))=\{\langle A,B\rangle \in \{\langle x,F\rangle \in (\bigcup \mathfrak{F} )\times \mathfrak{F} .\ x\in F\}\times \{\langle x,F\rangle \in (\bigcup \mathfrak{F} )\times \mathfrak{F} .\ x\in F\}.\ \text{snd}(B)\subseteq \text{snd}(A)\} \) using NetOfFilter_def, uu
then have dom_def: \( domain(\text{fst}(\text{Net}(\mathfrak{F} )))=\{\langle x,F\rangle \in (\bigcup \mathfrak{F} )\times \mathfrak{F} .\ x\in F\} \)
from func have fun: \( \text{fst}(\text{Net}(\mathfrak{F} )): \{\langle x,F\rangle \in (\bigcup \mathfrak{F} )\times \mathfrak{F} .\ x\in F\} \rightarrow (\bigcup \mathfrak{F} ) \) using ZF_fun_from_total
from assms(1) have NN: \( (\text{Net}(\mathfrak{F} )) \text{ is a net on }\bigcup T \) using net_of_filter_is_net
moreover
}
}
qed
from assms have \( x\in \bigcup T \) using FilterConverges_def
moreover {
fix \( U \)
assume AS: \( U\in Pow(\bigcup T) \), \( x\in int(U) \)
with assms have \( U\in \mathfrak{F} \), \( x\in U \) using Top_2_L1, FilterConverges_def
then have pp: \( \langle x,U\rangle \in domain(\text{fst}(\text{Net}(\mathfrak{F} ))) \) using dom_def
{
fix \( m \)
assume ASS: \( m\in domain(\text{fst}(\text{Net}(\mathfrak{F} ))) \), \( \langle \langle x,U\rangle ,m\rangle \in \text{snd}(\text{Net}(\mathfrak{F} )) \)
from ASS(1), fun, func have \( \text{fst}(\text{Net}(\mathfrak{F} ))(m) = \text{fst}(m) \) using func1_1_L1, ZF_fun_from_tot_val
with dir, ASS have \( \text{fst}(\text{Net}(\mathfrak{F} ))(m) \in U \) using dom_def
then have \( \forall m\in domain(\text{fst}(\text{Net}(\mathfrak{F} ))).\ (\langle \langle x,U\rangle ,m\rangle \in \text{snd}(\text{Net}(\mathfrak{F} )) \longrightarrow \text{fst}(\text{Net}(\mathfrak{F} ))m\in U) \)
with pp have \( \exists t\in domain(\text{fst}(\text{Net}(\mathfrak{F} ))).\ \forall m\in domain(\text{fst}(\text{Net}(\mathfrak{F} ))).\ (\langle t,m\rangle \in \text{snd}(\text{Net}(\mathfrak{F} )) \longrightarrow \text{fst}(\text{Net}(\mathfrak{F} ))m\in U) \)
then have \( \forall U\in Pow(\bigcup T).\ \)
\( (x\in int(U) \longrightarrow (\exists t\in domain(\text{fst}(\text{Net}(\mathfrak{F} ))).\ \forall m\in domain(\text{fst}(\text{Net}(\mathfrak{F} ))).\ (\langle t,m\rangle \in \text{snd}(\text{Net}(\mathfrak{F} )) \longrightarrow \text{fst}(\text{Net}(\mathfrak{F} ))m\in U))) \)
ultimately show \( thesis \) using NetConverges_def
If a net converges to a point, then a filter also converges to a point.
theorem (in topology0) net_of_filter_conver_filter_conver:
assumes \( \mathfrak{F} \text{ is a filter on }\bigcup T \) and \( (\text{Net}(\mathfrak{F} )) \rightarrow _N x \)
shows \( \mathfrak{F} \rightarrow _F x \)proof from assms have \( \bigcup T\in \mathfrak{F} \), \( \mathfrak{F} \subseteq Pow(\bigcup T) \) using IsFilter_def
then have uu: \( \bigcup \mathfrak{F} =\bigcup T \)
have \( x\in \bigcup T \) using assms, NetConverges_def, net_of_filter_is_net
moreover {
}
}
qed
fix \( U \)
assume \( U\in Pow(\bigcup T) \), \( x\in int(U) \)
then obtain \( t \) where t: \( t\in domain(\text{fst}(\text{Net}(\mathfrak{F} ))) \) and reg: \( \forall m\in domain(\text{fst}(\text{Net}(\mathfrak{F} ))).\ \langle t,m\rangle \in \text{snd}(\text{Net}(\mathfrak{F} )) \longrightarrow \text{fst}(\text{Net}(\mathfrak{F} ))m\in U \) using assms, net_of_filter_is_net, NetConverges_def
with assms(1), uu obtain \( t1 \) \( t2 \) where t_def: \( t=\langle t1,t2\rangle \) and \( t1\in t2 \) and tFF: \( t2\in \mathfrak{F} \) using NetOfFilter_def
{
fix \( s \)
assume \( s\in t2 \)
then have \( \langle s,t2\rangle \in \{\langle q1,q2\rangle \in \bigcup \mathfrak{F} \times \mathfrak{F} .\ q1\in q2\} \) using tFF
moreover
from assms(1), uu have \( domain(\text{fst}(\text{Net}(\mathfrak{F} )))=\{\langle q1,q2\rangle \in \bigcup \mathfrak{F} \times \mathfrak{F} .\ q1\in q2\} \) using NetOfFilter_def
ultimately have tt: \( \langle s,t2\rangle \in domain(\text{fst}(\text{Net}(\mathfrak{F} ))) \)
moreover
from assms(1), uu, t, t_def, tt have \( \langle \langle t1,t2\rangle ,\langle s,t2\rangle \rangle \in \text{snd}(\text{Net}(\mathfrak{F} )) \) using NetOfFilter_def
ultimately have \( \text{fst}(\text{Net}(\mathfrak{F} ))\langle s,t2\rangle \in U \) using reg, t_def
moreover
from assms(1), uu have \( function(\text{fst}(\text{Net}(\mathfrak{F} ))) \) using NetOfFilter_def, function_def
moreover from tt, assms(1), uu have \( \langle \langle s,t2\rangle ,s\rangle \in \text{fst}(\text{Net}(\mathfrak{F} )) \) using NetOfFilter_def
ultimately have \( s\in U \) using NetOfFilter_def, function_apply_equality
then have \( t2\subseteq U \)
with tFF, assms(1), \( U\in Pow(\bigcup T) \) have \( U\in \mathfrak{F} \) using IsFilter_def
then have \( \{U\in Pow(\bigcup T).\ x\in int(U)\} \subseteq \mathfrak{F} \)
ultimately show \( thesis \) using FilterConverges_def, assms(1)
A filter converges to a point if and only if its net converges to the point.
theorem (in topology0) filter_conver_iff_net_of_filter_conver:
assumes \( \mathfrak{F} \text{ is a filter on }\bigcup T \)
shows \( (\mathfrak{F} \rightarrow _F x) \longleftrightarrow ((\text{Net}(\mathfrak{F} )) \rightarrow _N x) \) using filter_conver_net_of_filter_conver, net_of_filter_conver_filter_conver, assmsThe previous result states that, when considering convergence, the filters do not generalize nets. When considering a filter, there is always a net that converges to the same points of the original filter.
Now we see that with nets, results come naturally applying the axiom of choice; but with filters, the results come, may be less natural, but with no choice. The reason is that \( \text{Net}(\mathfrak{F} ) \) is a net that doesn't come into our attention as a first choice; maybe because we restrict ourselves to the anti-symmetry property of orders without realizing that a directed set is not an order.
The following results will state that filters are not just a subclass of nets, but that nets and filters are equivalent on convergence: for every filter there is a net converging to the same points, and also, for every net there is a filter converging to the same points.
definition
\( (N \text{ is a net on } X) \Longrightarrow Filter N.\ .\ X \equiv \{A\in Pow(X).\ \exists D\in \{\{\text{fst}(N)\text{snd}(s).\ s\in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=t0\}\}.\ t0\in domain(\text{fst}(N))\}.\ D\subseteq A\} \)
Filter of a net is indeed a filter
theorem filter_of_net_is_filter:
assumes \( N \text{ is a net on } X \)
shows \( (Filter N.\ .\ X) \text{ is a filter on } X \) and \( \{\{\text{fst}(N)\text{snd}(s).\ s\in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=t0\}\}.\ t0\in domain(\text{fst}(N))\} \text{ is a base filter } (Filter N.\ .\ X) \)proof let \( C = \{\{\text{fst}(N)(\text{snd}(s)).\ s\in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=t0\}\}.\ t0\in domain(\text{fst}(N))\} \)
have \( C\subseteq Pow(X) \)proof
{
}
}
fix \( t \)
assume \( t\in C \)
then obtain \( t1 \) where \( t1\in domain(\text{fst}(N)) \) and t_Def: \( t=\{\text{fst}(N)\text{snd}(s).\ s\in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=t1\}\} \)
{
fix \( x \)
assume \( x\in t \)
with t_Def obtain \( ss \) where \( ss\in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=t1\} \) and x_def: \( x = \text{fst}(N)(\text{snd}(ss)) \)
then have \( \text{snd}(ss) \in domain(\text{fst}(N)) \)
from assms have \( \text{fst}(N):domain(\text{fst}(N))\rightarrow X \) unfolding IsNet_def
with \( \text{snd}(ss) \in domain(\text{fst}(N)) \) have \( x\in X \) using apply_funtype, x_def
hence \( t\subseteq X \)
thus \( thesis \)
qed
have sat: \( C \text{ satisfies the filter base condition } \)proof
from assms obtain \( t1 \) where \( t1\in domain(\text{fst}(N)) \) using IsNet_def
hence \( \{\text{fst}(N)\text{snd}(s).\ s\in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=t1\}\}\in C \)
hence \( C\neq 0 \)
moreover {
}
qed
fix \( U \)
assume \( U\in C \)
then obtain \( q \) where q_dom: \( q\in domain(\text{fst}(N)) \) and U_def: \( U=\{\text{fst}(N)\text{snd}(s).\ s\in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=q\}\} \)
with assms have \( \langle q,q\rangle \in \text{snd}(N) \wedge \text{fst}(\langle q,q\rangle )=q \) unfolding IsNet_def, IsDirectedSet_def, refl_def
with q_dom have \( \langle q,q\rangle \in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=q\} \)
with U_def have \( \text{fst}(N)(\text{snd}(\langle q,q\rangle )) \in U \)
hence \( U\neq 0 \)
then have \( 0\notin C \)
moreover have \( \forall A\in C.\ \forall B\in C.\ (\exists D\in C.\ D\subseteq A\cap B) \)proof
ultimately show \( thesis \) unfolding SatisfiesFilterBase_def
fix \( A \)
assume pA: \( A\in C \)
show \( \forall B\in C.\ \exists D\in C.\ D\subseteq A\cap B \)proof
qed
{
}
qed
fix \( B \)
assume \( B\in C \)
with pA obtain \( qA \) \( qB \) where per: \( qA\in domain(\text{fst}(N)) \), \( qB\in domain(\text{fst}(N)) \) and A_def: \( A=\{\text{fst}(N)\text{snd}(s).\ s\in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=qA\}\} \) and B_def: \( B=\{\text{fst}(N)\text{snd}(s).\ s\in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=qB\}\} \)
have dir: \( \text{snd}(N)\text{ directs }domain(\text{fst}(N)) \) using assms, IsNet_def
with per obtain \( qD \) where ine: \( \langle qA,qD\rangle \in \text{snd}(N) \), \( \langle qB,qD\rangle \in \text{snd}(N) \) and perD: \( qD\in domain(\text{fst}(N)) \) unfolding IsDirectedSet_def
let \( D = \{\text{fst}(N)\text{snd}(s).\ s\in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=qD\}\} \)
from perD have \( D\in C \)
moreover {
}
fix \( d \)
assume \( d\in D \)
then obtain \( sd \) where \( sd\in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=qD\} \) and d_def: \( d=\text{fst}(N)\text{snd}(sd) \)
then have sdN: \( sd\in \text{snd}(N) \) and qdd: \( \text{fst}(sd)=qD \) and \( sd\in domain(\text{fst}(N))\times domain(\text{fst}(N)) \)
then obtain \( qI \) \( aa \) where \( sd = \langle aa,qI\rangle \), \( qI \in domain(\text{fst}(N)) \), \( aa \in domain(\text{fst}(N)) \)
with qdd have sd_def: \( sd=\langle qD,qI\rangle \) and qIdom: \( qI\in domain(\text{fst}(N)) \)
with sdN have \( \langle qD,qI\rangle \in \text{snd}(N) \)
from dir have \( \text{trans}(\text{snd}(N)) \) unfolding IsDirectedSet_def
then have \( \langle qA,qD\rangle \in \text{snd}(N) \wedge \langle qD,qI\rangle \in \text{snd}(N) \longrightarrow \langle qA,qI\rangle \in \text{snd}(N) \) and \( \langle qB,qD\rangle \in \text{snd}(N) \wedge \langle qD,qI\rangle \in \text{snd}(N)\longrightarrow \langle qB,qI\rangle \in \text{snd}(N) \) using trans_def
with ine, \( \langle qD,qI\rangle \in \text{snd}(N) \) have \( \langle qA,qI\rangle \in \text{snd}(N) \), \( \langle qB,qI\rangle \in \text{snd}(N) \)
with qIdom, per have \( \langle qA,qI\rangle \in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=qA\} \), \( \langle qB,qI\rangle \in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=qB\} \)
then have \( \text{fst}(N)(qI) \in A\cap B \) using A_def, B_def
then have \( \text{fst}(N)(\text{snd}(sd)) \in A\cap B \) using sd_def
then have \( d \in A\cap B \) using d_def
then have \( D \subseteq A\cap B \)
ultimately show \( \exists D\in C.\ D\subseteq A\cap B \)
have Base: \( C \text{ is a base filter } \{A\in Pow(X).\ \exists D\in C.\ D\subseteq A\} \), \( \bigcup \{A\in Pow(X).\ \exists D\in C.\ D\subseteq A\}=X \)proof
from \( C\subseteq Pow(X) \), sat show \( C \text{ is a base filter } \{A\in Pow(X).\ \exists D\in C.\ D\subseteq A\} \) by (rule base_unique_filter_set3 )
from \( C\subseteq Pow(X) \), sat show \( \bigcup \{A\in Pow(X).\ \exists D\in C.\ D\subseteq A\}=X \) by (rule base_unique_filter_set3 )
qed
with sat show \( (Filter N.\ .\ X) \text{ is a filter on } X \) using sat, basic_filter, FilterOfNet_def, assms
from Base(1) show \( C \text{ is a base filter } (Filter N.\ .\ X) \) using FilterOfNet_def, assms
qed
Convergence of a net implies the convergence of the corresponding filter.
theorem (in topology0) net_conver_filter_of_net_conver:
assumes \( N \text{ is a net on } \bigcup T \) and \( N \rightarrow _N x \)
shows \( (Filter N.\ .\ (\bigcup T)) \rightarrow _F x \)proof let \( C = \{\{\text{fst}(N)\text{snd}(s).\ s\in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=t\}\}.\ \)
\( t\in domain(\text{fst}(N))\} \)
from assms(1) have \( (Filter N.\ .\ (\bigcup T)) \text{ is a filter on } (\bigcup T) \) and \( C \text{ is a base filter } Filter N.\ .\ (\bigcup T) \) using filter_of_net_is_filter
moreover
qed
have \( \forall U\in Pow(\bigcup T).\ x\in int(U) \longrightarrow (\exists D\in C.\ D\subseteq U) \)proof
moreover {
}
}
fix \( U \)
assume \( U\in Pow(\bigcup T) \), \( x\in int(U) \)
with assms have \( \exists t\in domain(\text{fst}(N)).\ (\forall m\in domain(\text{fst}(N)).\ (\langle t,m\rangle \in \text{snd}(N) \longrightarrow \text{fst}(N)m\in U)) \) using NetConverges_def
then obtain \( t \) where \( t\in domain(\text{fst}(N)) \) and reg: \( \forall m\in domain(\text{fst}(N)).\ (\langle t,m\rangle \in \text{snd}(N) \longrightarrow \text{fst}(N)m\in U) \)
{
fix \( f \)
assume \( f\in \{\text{fst}(N)\text{snd}(s).\ s\in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=t\}\} \)
then obtain \( s \) where \( s\in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=t\} \) and f_def: \( f=\text{fst}(N)\text{snd}(s) \)
hence \( s\in domain(\text{fst}(N))\times domain(\text{fst}(N)) \) and \( s\in \text{snd}(N) \) and \( \text{fst}(s)=t \)
hence \( s=\langle t,\text{snd}(s)\rangle \) and \( \text{snd}(s)\in domain(\text{fst}(N)) \)
with \( s\in \text{snd}(N) \), reg have \( \text{fst}(N)\text{snd}(s)\in U \)
with f_def have \( f\in U \)
hence \( \{\text{fst}(N)\text{snd}(s).\ s\in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=t\}\} \subseteq U \)
with \( t\in domain(\text{fst}(N)) \) have \( \exists D\in C.\ D\subseteq U \)
thus \( \forall U\in Pow(\bigcup T).\ x\in int(U) \longrightarrow (\exists D\in C.\ D\subseteq U) \)
qed
from assms have \( x\in \bigcup T \) using NetConverges_def
ultimately show \( (Filter N.\ .\ (\bigcup T)) \rightarrow _F x \) by (rule convergence_filter_base2 )
Convergence of a filter corresponding to a net implies convergence of the net.
theorem (in topology0) filter_of_net_conver_net_conver:
assumes \( N \text{ is a net on } \bigcup T \) and \( (Filter N.\ .\ (\bigcup T)) \rightarrow _F x \)
shows \( N \rightarrow _N x \)proof let \( C = \{\{\text{fst}(N)\text{snd}(s).\ s\in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=t\}\}.\ \)
\( t\in domain(\text{fst}(N))\} \)
from assms have I: \( (Filter N.\ .\ (\bigcup T)) \text{ is a filter on } (\bigcup T) \), \( C \text{ is a base filter } (Filter N.\ .\ (\bigcup T)) \), \( (Filter N.\ .\ (\bigcup T)) \rightarrow _F x \) using filter_of_net_is_filter
then have reg: \( \forall U\in Pow(\bigcup T).\ x\in int(U) \longrightarrow (\exists D\in C.\ D\subseteq U) \) by (rule convergence_filter_base1 )
from I have \( x\in \bigcup T \) by (rule convergence_filter_base1 )
moreover {
}
}
qed
fix \( U \)
assume \( U\in Pow(\bigcup T) \), \( x\in int(U) \)
with reg have \( \exists D\in C.\ D\subseteq U \)
then obtain \( D \) where \( D\in C \), \( D\subseteq U \)
then obtain \( td \) where \( td\in domain(\text{fst}(N)) \) and D_def: \( D=\{\text{fst}(N)\text{snd}(s).\ s\in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=td\}\} \)
{
fix \( m \)
assume \( m\in domain(\text{fst}(N)) \), \( \langle td,m\rangle \in \text{snd}(N) \)
with \( td\in domain(\text{fst}(N)) \) have \( \langle td,m\rangle \in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=td\} \)
with D_def have \( \text{fst}(N)m\in D \)
with \( D\subseteq U \) have \( \text{fst}(N)m\in U \)
then have \( \forall m\in domain(\text{fst}(N)).\ \langle td,m\rangle \in \text{snd}(N) \longrightarrow \text{fst}(N)m\in U \)
with \( td\in domain(\text{fst}(N)) \) have \( \exists t\in domain(\text{fst}(N)).\ \forall m\in domain(\text{fst}(N)).\ \langle t,m\rangle \in \text{snd}(N) \longrightarrow \text{fst}(N)m\in U \)
then have \( \forall U\in Pow(\bigcup T).\ x\in int(U) \longrightarrow \)
\( (\exists t\in domain(\text{fst}(N)).\ \forall m\in domain(\text{fst}(N)).\ \langle t,m\rangle \in \text{snd}(N) \longrightarrow \text{fst}(N)m\in U) \)
ultimately show \( thesis \) using NetConverges_def, assms(1)
Filter of net converges to a point \(x\) if and only the net converges to \(x\).
theorem (in topology0) filter_of_net_conv_iff_net_conv:
assumes \( N \text{ is a net on } \bigcup T \)
shows \( ((Filter N.\ .\ (\bigcup T)) \rightarrow _F x) \longleftrightarrow (N \rightarrow _N x) \) using assms, filter_of_net_conver_net_conver, net_conver_filter_of_net_converWe know now that filters and nets are the same thing, when working convergence of topological spaces. Sometimes, the nature of filters makes it easier to generalized them as follows.
Instead of considering all subsets of some set \(X\), we can consider only open sets (we get an open filter) or closed sets (we get a closed filter). There are many more useful examples that characterize topological properties.
This type of generalization cannot be done with nets.
Also a filter can give us a topology in the following way:
theorem top_of_filter:
assumes \( \mathfrak{F} \text{ is a filter on } \bigcup \mathfrak{F} \)
shows \( (\mathfrak{F} \cup \{0\}) \text{ is a topology } \)proof{
}
fix \( A \) \( B \)
assume \( A\in (\mathfrak{F} \cup \{0\}) \), \( B\in (\mathfrak{F} \cup \{0\}) \)
then have \( (A\in \mathfrak{F} \wedge B\in \mathfrak{F} ) \vee (A\cap B=0) \)
with assms have \( A\cap B\in (\mathfrak{F} \cup \{0\}) \) unfolding IsFilter_def
then have \( \forall A\in (\mathfrak{F} \cup \{0\}).\ \forall B\in (\mathfrak{F} \cup \{0\}).\ A\cap B\in (\mathfrak{F} \cup \{0\}) \)
moreover {
}
qed
fix \( M \)
assume A: \( M\in Pow(\mathfrak{F} \cup \{0\}) \)
then have \( M=0\vee M=\{0\}\vee (\exists T\in M.\ T\in \mathfrak{F} ) \)
then have \( \bigcup M=0\vee (\exists T\in M.\ T\in \mathfrak{F} ) \)
then obtain \( T \) where \( \bigcup M=0\vee (T\in \mathfrak{F} \wedge T\in M) \)
then have \( \bigcup M=0\vee (T\in \mathfrak{F} \wedge T\subseteq \bigcup M) \)
moreover
from this, A have \( \bigcup M\subseteq \bigcup \mathfrak{F} \)
ultimately have \( \bigcup M\in (\mathfrak{F} \cup \{0\}) \) using IsFilter_def, assms
then have \( \forall M\in Pow(\mathfrak{F} \cup \{0\}).\ \bigcup M\in (\mathfrak{F} \cup \{0\}) \)
ultimately show \( thesis \) using IsATopology_def
We can use topology0 locale with filters.
lemma topology0_filter:
assumes \( \mathfrak{F} \text{ is a filter on } \bigcup \mathfrak{F} \)
shows \( topology0(\mathfrak{F} \cup \{0\}) \) using top_of_filter, topology0_def, assmsThe next abbreviation introduces notation where we want to specify the space where the filter convergence takes place.
abbreviation
\( \mathfrak{F} \rightarrow _F x\text{ in }T \equiv topology0.\ \text{FilterConverges}(T,\mathfrak{F} ,x) \)
The next abbreviation introduces notation where we want to specify the space where the net convergence takes place.
abbreviation
\( N \rightarrow _N x\text{ in }T \equiv topology0.\ \text{NetConverges}(T,N,x) \)
Each point of a the union of a filter is a limit of that filter.
lemma lim_filter_top_of_filter:
assumes \( \mathfrak{F} \text{ is a filter on } \bigcup \mathfrak{F} \) and \( x\in \bigcup \mathfrak{F} \)
shows \( \mathfrak{F} \rightarrow _F x\text{ in }(\mathfrak{F} \cup \{0\}) \)proof have \( \bigcup \mathfrak{F} =\bigcup (\mathfrak{F} \cup \{0\}) \)
with assms(1) have assms1: \( \mathfrak{F} \text{ is a filter on } \bigcup (\mathfrak{F} \cup \{0\}) \)
{
fix \( U \)
assume \( U\in Pow(\bigcup (\mathfrak{F} \cup \{0\})) \), \( x\in \text{Interior}(U,(\mathfrak{F} \cup \{0\})) \)
with assms(1) have \( \text{Interior}(U,(\mathfrak{F} \cup \{0\}))\in \mathfrak{F} \) using topology0_def, top_of_filter, Top_2_L2
moreover
from assms(1) have \( \text{Interior}(U,(\mathfrak{F} \cup \{0\}))\subseteq U \) using topology0_def, top_of_filter, Top_2_L1
moreover from \( U\in Pow(\bigcup (\mathfrak{F} \cup \{0\})) \) have \( U\in Pow(\bigcup \mathfrak{F} ) \)
ultimately have \( U\in \mathfrak{F} \) using assms(1), IsFilter_def
with assms, assms1 show \( thesis \) using FilterConverges_def, top_of_filter, topology0_def
qed
end
Definition of IsLinOrder:
\( \text{IsLinOrder}(X,r) \equiv \text{antisym}(r) \wedge \text{trans}(r) \wedge (r \text{ is total on } X) \)
lemma total_is_refl:
assumes \( r \text{ is total on } X \)
shows \( \text{refl}(X,r) \)Definition of IsTotal:
\( r \text{ is total on } X \equiv (\forall a\in X.\ \forall b\in X.\ \langle a,b\rangle \in r \vee \langle b,a\rangle \in r) \)
Definition of IsDirectedSet:
\( r\text{ directs }X \equiv \text{refl}(X,r) \wedge \text{trans}(r) \wedge (\forall x\in X.\ \forall y\in X.\ \exists z\in X.\ \langle x,z\rangle \in r \wedge \langle y,z\rangle \in r) \)
lemma NatOrder_ZF_1_L2: shows \( \text{antisym}(Le) \), \( \text{trans}(Le) \), \( Le \text{ is total on } nat \), \( \text{IsLinOrder}(nat,Le) \)
lemma linorder_imp_directed:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( r\text{ directs }X \) lemma (in topology0) Top_2_L1: shows \( int(A) \subseteq A \)
lemma (in topology0) Top_2_L2: shows \( int(A) \in T \)
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 (in topology0) Top_2_L5:
assumes \( U\subseteq A \) and \( U\in T \)
shows \( U \subseteq int(A) \) lemma (in topology0) Top_2_L3: shows \( U\in T \longleftrightarrow int(U) = U \)
theorem (in topology0) directedset_neighborhoods:
assumes \( x\in \bigcup T \)
defines \( \text{Neigh}\equiv \{U\in Pow(\bigcup T).\ x\in int(U)\} \)
defines \( r\equiv \{\langle U,V\rangle \in (\text{Neigh} \times \text{Neigh}).\ V\subseteq U\} \)
shows \( r\text{ directs }\text{Neigh} \)Definition of IsNet:
\( N \text{ is a net on } X \equiv \text{fst}(N):domain(\text{fst}(N))\rightarrow X \wedge (\text{snd}(N)\text{ directs }domain(\text{fst}(N))) \wedge domain(\text{fst}(N))\neq 0 \)
Definition of NetConverges:
\( N \text{ is a net on } \bigcup T \Longrightarrow N \rightarrow _N x \equiv \)
\( (x\in \bigcup T) \wedge (\forall U\in Pow(\bigcup T).\ (x\in int(U) \longrightarrow (\exists t\in domain(\text{fst}(N)).\ \forall m\in domain(\text{fst}(N)).\ \)
\( (\langle t,m\rangle \in \text{snd}(N) \longrightarrow \text{fst}(N)m\in U)))) \)
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 IsBaseFilter:
\( C \text{ is a base filter } \mathfrak{F} \equiv C\subseteq \mathfrak{F} \wedge \mathfrak{F} =\{A\in Pow(\bigcup \mathfrak{F} ).\ (\exists D\in C.\ D\subseteq A)\} \)
lemma basic_element_filter:
assumes \( A\in \mathfrak{F} \) and \( C \text{ is a base filter } \mathfrak{F} \)
shows \( \exists D\in C.\ D\subseteq A \)Definition of SatisfiesFilterBase:
\( C \text{ satisfies the filter base condition } \equiv (\forall A\in C.\ \forall B\in C.\ \exists D\in C.\ D\subseteq A\cap B) \wedge C\neq 0 \wedge 0\notin C \)
theorem basic_filter_1:
assumes \( C \text{ is a base filter } \mathfrak{F} \) and \( C \text{ satisfies the filter base condition } \)
shows \( \mathfrak{F} \text{ is a filter on } \bigcup \mathfrak{F} \) theorem basic_filter_2:
assumes \( C \text{ is a base filter } \mathfrak{F} \) and \( \mathfrak{F} \text{ is a filter on } \bigcup \mathfrak{F} \)
shows \( C \text{ satisfies the filter base condition } \) theorem base_unique_filter_set1:
assumes \( C \subseteq Pow(X) \) and \( C\neq 0 \)
shows \( C \text{ is a base filter } \{A\in Pow(X).\ \exists D\in C.\ D\subseteq A\} \) and \( \bigcup \{A\in Pow(X).\ \exists D\in C.\ D\subseteq A\}=X \) theorem base_unique_filter_set2:
assumes \( C\subseteq Pow(X) \) and \( C \text{ satisfies the filter base condition } \)
shows \( ((C \text{ is a base filter } \mathfrak{F} ) \wedge \bigcup \mathfrak{F} =X) \longleftrightarrow \mathfrak{F} =\{A\in Pow(X).\ \exists D\in C.\ D\subseteq A\} \)Definition of FilterConverges:
\( \mathfrak{F} \text{ is a filter on }\bigcup T \Longrightarrow \mathfrak{F} \rightarrow _Fx \equiv \)
\( x\in \bigcup T \wedge (\{U\in Pow(\bigcup T).\ x\in int(U)\} \subseteq \mathfrak{F} ) \)
theorem (in topology0) convergence_filter_base1:
assumes \( \mathfrak{F} \text{ is a filter on } \bigcup T \) and \( C \text{ is a base filter } \mathfrak{F} \) and \( \mathfrak{F} \rightarrow _F x \)
shows \( \forall U\in Pow(\bigcup T).\ x\in int(U) \longrightarrow (\exists D\in C.\ D\subseteq U) \) and \( x\in \bigcup T \) theorem (in topology0) convergence_filter_base2:
assumes \( \mathfrak{F} \text{ is a filter on } \bigcup T \) and \( C \text{ is a base filter } \mathfrak{F} \) and \( \forall U\in Pow(\bigcup T).\ x\in int(U) \longrightarrow (\exists D\in C.\ D\subseteq U) \) and \( x\in \bigcup T \)
shows \( \mathfrak{F} \rightarrow _F x \)Definition of NetOfFilter:
\( \mathfrak{F} \text{ is a filter on } \bigcup \mathfrak{F} \Longrightarrow \text{Net}(\mathfrak{F} ) \equiv \)
\( \langle \{\langle A,\text{fst}(A)\rangle .\ A\in \{\langle x,F\rangle \in (\bigcup \mathfrak{F} )\times \mathfrak{F} .\ x\in F\}\},\{\langle A,B\rangle \in \{\langle x,F\rangle \in (\bigcup \mathfrak{F} )\times \mathfrak{F} .\ x\in F\}\times \{\langle x,F\rangle \in (\bigcup \mathfrak{F} )\times \mathfrak{F} .\ x\in F\}.\ \text{snd}(B)\subseteq \text{snd}(A)\}\rangle \)
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 \) theorem net_of_filter_is_net:
assumes \( \mathfrak{F} \text{ is a filter on } X \)
shows \( (\text{Net}(\mathfrak{F} )) \text{ is a net on } X \) lemma func1_1_L1:
assumes \( f:A\rightarrow C \)
shows \( domain(f) = A \) lemma ZF_fun_from_tot_val:
assumes \( f:X\rightarrow Y \), \( x\in X \) and \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)
shows \( f(x) = b(x) \) and \( b(x)\in Y \) theorem (in topology0) filter_conver_net_of_filter_conver:
assumes \( \mathfrak{F} \text{ is a filter on } \bigcup T \) and \( \mathfrak{F} \rightarrow _F x \)
shows \( (\text{Net}(\mathfrak{F} )) \rightarrow _N x \) theorem (in topology0) net_of_filter_conver_filter_conver:
assumes \( \mathfrak{F} \text{ is a filter on }\bigcup T \) and \( (\text{Net}(\mathfrak{F} )) \rightarrow _N x \)
shows \( \mathfrak{F} \rightarrow _F x \) corollary base_unique_filter_set3:
assumes \( C\subseteq Pow(X) \) and \( C \text{ satisfies the filter base condition } \)
shows \( C \text{ is a base filter } \{A\in Pow(X).\ \exists D\in C.\ D\subseteq A\} \) and \( \bigcup \{A\in Pow(X).\ \exists D\in C.\ D\subseteq A\} = X \) theorem basic_filter:
assumes \( C \text{ is a base filter } \mathfrak{F} \)
shows \( (C \text{ satisfies the filter base condition }) \longleftrightarrow (\mathfrak{F} \text{ is a filter on } \bigcup \mathfrak{F} ) \)Definition of FilterOfNet:
\( (N \text{ is a net on } X) \Longrightarrow Filter N.\ .\ X \equiv \{A\in Pow(X).\ \exists D\in \{\{\text{fst}(N)\text{snd}(s).\ s\in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=t0\}\}.\ t0\in domain(\text{fst}(N))\}.\ D\subseteq A\} \)
theorem filter_of_net_is_filter:
assumes \( N \text{ is a net on } X \)
shows \( (Filter N.\ .\ X) \text{ is a filter on } X \) and \( \{\{\text{fst}(N)\text{snd}(s).\ s\in \{s\in domain(\text{fst}(N))\times domain(\text{fst}(N)).\ s\in \text{snd}(N) \wedge \text{fst}(s)=t0\}\}.\ t0\in domain(\text{fst}(N))\} \text{ is a base filter } (Filter N.\ .\ X) \) theorem (in topology0) filter_of_net_conver_net_conver:
assumes \( N \text{ is a net on } \bigcup T \) and \( (Filter N.\ .\ (\bigcup T)) \rightarrow _F x \)
shows \( N \rightarrow _N x \) theorem (in topology0) net_conver_filter_of_net_conver:
assumes \( N \text{ is a net on } \bigcup T \) and \( N \rightarrow _N x \)
shows \( (Filter N.\ .\ (\bigcup T)) \rightarrow _F x \) theorem top_of_filter:
assumes \( \mathfrak{F} \text{ is a filter on } \bigcup \mathfrak{F} \)
shows \( (\mathfrak{F} \cup \{0\}) \text{ is a topology } \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8