theory Topology_ZF_4b imports Topology_ZF_4
begin
This theory continues Topology_ZF_4 with results relating the net and filter convergence notions introduced there.
Relation between nets and filters
In this section we show that filters do not generalize nets, but still nets and filters are in a 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 generalize 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 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 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 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) \)
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 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 \)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} ) \)
lemma (in topology0) Top_2_L1: shows \( int(A) \subseteq A \)
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 \)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)))) \)
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 \)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 \)
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) 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 \) 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) 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 \)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) \)
theorem top_of_filter:
assumes \( \mathfrak{F} \text{ is a filter on } \bigcup \mathfrak{F} \)
shows \( (\mathfrak{F} \cup \{0\}) \text{ is a topology } \) lemma (in topology0) Top_2_L2: shows \( int(A) \in T \)
This page by Sławomir Kołodyński is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8
