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 (\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} ) \)
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 \( \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} \) using assms unfolding IsFilter_defFilters are closed with respect to taking finite intersections.
lemma filter_fin_inter_closed:
assumes \( \mathfrak{F} \text{ is a filter on } X \), \( M\in \text{FinPow}(\mathfrak{F} )\setminus \{\emptyset \} \)
shows \( \bigcap M \in \mathfrak{F} \) using assms, is_filter_def_split(4), inter_two_inter_finFilters are closed with respect to taking supersets.
lemma filter_superset_closed:
assumes \( \mathfrak{F} \text{ is a filter on } X \), \( \mathcal{A} \subseteq \mathfrak{F} \)
shows \( \text{Supersets}(X,\mathcal{A} ) \subseteq \mathfrak{F} \) using assms, is_filter_def_split(5) unfolding Supersets_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
Every filter can be expanded by a set
lemma extend_filter:
assumes \( A\in Pow(X) \), \( \mathfrak{F} \text{ is a filter on } X \), \( A\neq 0 \), \( A\notin \mathfrak{F} \), \( X\setminus A\notin \mathfrak{F} \)
shows \( \exists \mathfrak{G} .\ (\mathfrak{G} \text{ is a filter on } X) \wedge A\in \mathfrak{G} \wedge \mathfrak{F} \subseteq \mathfrak{G} \)proof from assms(2,3) have ne: \( \{F\cap A.\ F\in \mathfrak{F} \}\neq \emptyset \) unfolding IsFilter_def
moreover {
}
}
assume \( \emptyset \in \{F\cap A.\ F\in \mathfrak{F} \} \)
then obtain \( F \) where F: \( F\in \mathfrak{F} \), \( F\cap A = \emptyset \)
with assms(2) have f: \( F \subseteq X\setminus A \) unfolding IsFilter_def
from assms(2), F(1) have \( \forall C\in Pow(X).\ F \subseteq C \longrightarrow C \in \mathfrak{F} \) unfolding IsFilter_def
with assms(5), \( F \subseteq X\setminus A \) have \( False \)
hence \( \emptyset \notin \{F\cap A.\ F\in \mathfrak{F} \} \)
moreover {
fix \( x \) \( y \)
assume as: \( x \in \{F\cap A.\ F\in \mathfrak{F} \} \), \( y \in \{F\cap A.\ F\in \mathfrak{F} \} \)
then obtain \( f_x \) \( f_y \) where ff: \( x=f_x\cap A \), \( y=f_y\cap A \), \( f_x\in \mathfrak{F} \), \( f_y\in \mathfrak{F} \)
hence \( x\cap y = f_x\cap f_y\cap A \)
with assms(2), ff have \( \exists D\in \{F\cap A.\ F\in \mathfrak{F} \}.\ D\subseteq x\cap y \) unfolding IsFilter_def
hence \( \forall A_a\in \{F\cap A.\ F\in \mathfrak{F} \}.\ \forall B\in \{F\cap A.\ F\in \mathfrak{F} \}.\ \exists D\in \{F\cap A.\ F\in \mathfrak{F} \}.\ D\subseteq A_a\cap B \)
ultimately have baseCond: \( \{F\cap A.\ F\in \mathfrak{F} \} \text{ satisfies the filter base condition } \) unfolding SatisfiesFilterBase_def
let \( F = \{A_A\in Pow(X).\ (\exists D\in \{F\cap A.\ F\in \mathfrak{F} \}.\ D\subseteq A_A)\} \)
have rule: \( \{F\cap A.\ F\in \mathfrak{F} \} \subseteq Pow(X) \wedge \{F\cap A.\ F\in \mathfrak{F} \} \neq \emptyset \longrightarrow \)
\( (\{F\cap A.\ F\in \mathfrak{F} \} \text{ is a base filter } \{A_A\in Pow(X).\ (\exists D\in \{F\cap A.\ F\in \mathfrak{F} \}.\ D\subseteq A_A)\}) \) using base_unique_filter_set1(1)
from assms(2) have p: \( \{F\cap A.\ F\in \mathfrak{F} \} \subseteq Pow(X) \) unfolding IsFilter_def
with ne, rule have base: \( \{F\cap A.\ F\in \mathfrak{F} \} \text{ is a base filter } F \)
have \( \{F\cap A.\ F\in \mathfrak{F} \}\subseteq Pow(X) \wedge (\{F\cap A.\ F\in \mathfrak{F} \} \text{ satisfies the filter base condition })\)
\( \longrightarrow \bigcup F = X \) using base_unique_filter_set3(2)
with p, base, baseCond have \( F \text{ is a filter on } X \) using basic_filter
moreover
qed
from assms(1,2) have \( A\in F \) and \( \mathfrak{F} \subseteq F \) unfolding IsFilter_def
ultimately show \( (F \text{ is a filter on } X) \wedge A \in F \wedge \mathfrak{F} \subseteq F \)
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
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 (\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} ) \)
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 inter_two_inter_fin:
assumes \( \forall V\in T.\ \forall W\in T.\ V \cap W \in T \) and \( N \neq 0 \) and \( N \in \text{FinPow}(T) \)
shows \( \bigcap N \in T \) 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} \)Definition of Supersets:
\( \text{Supersets}(X,\mathcal{A} ) \equiv \{B\in Pow(X).\ \exists A\in \mathcal{A} .\ A\subseteq B\} \)
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\} \) 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 \) 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 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 \)
This page by Sławomir Kołodyński is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8
