Theory Topology_ZF_4
section ‹Topology 4›
theory Topology_ZF_4 imports Topology_ZF_1 Order_ZF func1 NatOrder_ZF
begin
text‹This theory deals with convergence in topological spaces.
Contributed by Daniel de la Concepcion.›
subsection‹Nets›
text‹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.›
text‹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
IsDirectedSet ("_ directs _" 90)
where "r directs X ≡ refl(X,r) ∧ trans(r) ∧ (∀x∈X. ∀y∈X. ∃z∈X. ⟨x,z⟩∈r ∧ ⟨y,z⟩∈r)"
text‹Any linear order is a directed set; in particular $(\mathbb{N},\leq)$.›
lemma linorder_imp_directed:
assumes "IsLinOrder(X,r)"
shows "r directs X"
proof-
from assms have "trans(r)" using IsLinOrder_def by auto
moreover
from assms have r:"refl(X,r)" using IsLinOrder_def total_is_refl by auto
moreover
{
fix x y
assume R: "x∈X" "y∈X"
with assms have "⟨x,y⟩∈r ∨ ⟨y,x⟩∈r" using IsLinOrder_def IsTotal_def by auto
with r have "(⟨x,y⟩∈r ∧ ⟨y,y⟩∈r)∨(⟨y,x⟩∈r ∧ ⟨x,x⟩∈r)" using R refl_def by auto
then have "∃z∈X. ⟨x,z⟩∈r ∧ ⟨y,z⟩∈r" using R by auto
}
ultimately show ?thesis using IsDirectedSet_def function_def by auto
qed
text‹ Natural numbers are a directed set.›
corollary Le_directs_nat:
shows "IsLinOrder(nat,Le)" "Le directs nat"
proof -
show "IsLinOrder(nat,Le)" by (rule NatOrder_ZF_1_L2)
then show "Le directs nat" using linorder_imp_directed by auto
qed
text‹We are able to define the concept of net, now that we now what a directed set is.›
definition
IsNet ("_ {is a net on} _" 90)
where "N {is a net on} X ≡ fst(N):domain(fst(N))→X ∧ (snd(N) directs domain(fst(N))) ∧ domain(fst(N))≠0"
text‹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)
NetConverges ("_ →⇩N _" 90)
where "N {is a net on} ⋃T ⟹ N →⇩N x ≡
(x∈⋃T) ∧ (∀U∈Pow(⋃T). (x∈int(U) ⟶ (∃t∈domain(fst(N)). ∀m∈domain(fst(N)).
(⟨t,m⟩∈snd(N) ⟶ fst(N)`m∈U))))"
text‹One of the most important directed sets, is the neighborhoods of a point.›
theorem (in topology0) directedset_neighborhoods:
assumes "x∈⋃T"
defines "Neigh≡{U∈Pow(⋃T). x∈int(U)}"
defines "r≡{⟨U,V⟩∈(Neigh × Neigh). V⊆U}"
shows "r directs Neigh"
proof-
{
fix U
assume "U ∈ Neigh"
then have "⟨U,U⟩ ∈ r" using r_def by auto
}
then have "refl(Neigh,r)" using refl_def by auto
moreover
{
fix U V W
assume "⟨U,V⟩ ∈ r" "⟨V,W⟩ ∈ r"
then have "U ∈ Neigh" "W ∈ Neigh" "W⊆U" using r_def by auto
then have "⟨U,W⟩∈r" using r_def by auto
}
then have "trans(r)" using trans_def by blast
moreover
{
fix A B
assume p: "A∈Neigh" "B∈Neigh"
have "A∩B ∈ Neigh"
proof-
from p have "A∩B ∈ Pow(⋃T)" using Neigh_def by auto
moreover
{ from p have "x∈int(A)""x∈int(B)" using Neigh_def by auto
then have "x∈int(A)∩int(B)" by auto
moreover
{ have "int(A)∩int(B)⊆A∩B" using Top_2_L1 by auto
moreover have "int(A)∩int(B)∈T"
using Top_2_L2 Top_2_L2 topSpaceAssum IsATopology_def by blast
ultimately have "int(A)∩int(B)⊆int(A∩B)"
using Top_2_L5 by auto
}
ultimately have "x ∈ int(A∩B)" by auto
}
ultimately show ?thesis using Neigh_def by auto
qed
moreover from ‹A∩B ∈ Neigh› have "⟨A,A∩B⟩∈r ∧ ⟨B,A∩B⟩∈r"
using r_def p by auto
ultimately
have "∃z∈Neigh. ⟨A,z⟩∈r ∧ ⟨B,z⟩∈r" by auto
}
ultimately show ?thesis using IsDirectedSet_def by auto
qed
text‹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∈⋃T"
defines "Neigh≡{U∈Pow(⋃T). x∈int(U)}"
defines "r≡{⟨U,V⟩∈(Neigh × Neigh). V⊆U}"
assumes "f:Neigh→⋃T" "∀U∈Neigh. f`(U) ∈ U"
shows "⟨f,r⟩ →⇩N x"
proof -
from assms(4) have dom_def: "Neigh = domain(f)" using Pi_def by auto
moreover
have "⋃T∈T" using topSpaceAssum IsATopology_def by auto
then have "int(⋃T)=⋃T" using Top_2_L3 by auto
with assms(1) have "⋃T∈Neigh" using Neigh_def by auto
then have "⋃T∈domain(fst(⟨f,r⟩))" using dom_def by auto
moreover from assms(4) dom_def have "fst(⟨f,r⟩):domain(fst(⟨f,r⟩))→⋃T"
by auto
moreover from assms(1,2,3) dom_def have "snd(⟨f,r⟩) directs domain(fst(⟨f,r⟩))"
using directedset_neighborhoods by simp
ultimately have Net: "⟨f,r⟩ {is a net on} ⋃T" unfolding IsNet_def by auto
{
fix U
assume "U ∈ Pow(⋃T)" "x ∈ int(U)"
then have "U ∈ Neigh" using Neigh_def by auto
then have t: "U ∈ domain(f)" using dom_def by auto
{
fix W
assume A: "W∈domain(f)" "⟨U,W⟩∈r"
then have "W∈Neigh" using dom_def by auto
with assms(5) have "f`W∈W" by auto
with A(2) r_def have "f`W∈U" by auto
}
then have "∀W∈domain(f). (⟨U,W⟩∈r ⟶ f`W∈U)" by auto
with t have "∃V∈domain(f). ∀W∈domain(f). (⟨V,W⟩∈r ⟶ f`W∈U)" by auto
}
then have "∀U∈Pow(⋃T). (x∈int(U) ⟶ (∃V∈domain(f). ∀W∈domain(f). (⟨V,W⟩∈r ⟶ f`(W) ∈ U)))"
by auto
with assms(1) Net show ?thesis using NetConverges_def by auto
qed
subsection‹Filters›
text‹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.›
text‹The topological tools to deal with convergence are what is called filters.›
definition
IsFilter ("_ {is a filter on} _" 90)
where "𝔉 {is a filter on} X ≡ (0∉𝔉) ∧ (X∈𝔉) ∧ 𝔉⊆Pow(X) ∧
(∀A∈𝔉. ∀B∈𝔉. A∩B∈𝔉) ∧ (∀B∈𝔉. ∀C∈Pow(X). B⊆C ⟶ C∈𝔉)"
text‹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 "𝔉 {is a filter on} X"
shows "0∉𝔉" "X∈𝔉" "𝔉⊆Pow(X)"
"∀A∈𝔉. ∀B∈𝔉. A∩B∈𝔉" and "∀B∈𝔉. ∀C∈Pow(X). B⊆C ⟶ C∈𝔉"
using assms unfolding IsFilter_def by auto
text‹Not 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
IsBaseFilter ("_ {is a base filter} _" 90)
where "C {is a base filter} 𝔉 ≡ C⊆𝔉 ∧ 𝔉={A∈Pow(⋃𝔉). (∃D∈C. D⊆A)}"
text‹Not every set is a base for a filter, as it happens with topologies, there
is a condition to be satisfied.›
definition
SatisfiesFilterBase ("_ {satisfies the filter base condition}" 90)
where "C {satisfies the filter base condition} ≡ (∀A∈C. ∀B∈C. ∃D∈C. D⊆A∩B) ∧ C≠0 ∧ 0∉C"
text‹Every set of a filter contains a set from the filter's base.›
lemma basic_element_filter:
assumes "A∈𝔉" and "C {is a base filter} 𝔉"
shows "∃D∈C. D⊆A"
proof-
from assms(2) have t:"𝔉={A∈Pow(⋃𝔉). (∃D∈C. D⊆A)}" using IsBaseFilter_def by auto
with assms(1) have "A∈{A∈Pow(⋃𝔉). (∃D∈C. D⊆A)}" by auto
then have "A∈Pow(⋃𝔉)" "∃D∈C. D⊆A" by auto
then show ?thesis by auto
qed
text‹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 {is a base filter} 𝔉" and "C {satisfies the filter base condition}"
shows "𝔉 {is a filter on} ⋃𝔉"
proof-
{
fix A B
assume AF: "A∈𝔉" and BF: "B∈𝔉"
with assms(1) have "∃DA∈C. DA⊆A" using basic_element_filter by simp
then obtain DA where perA: "DA∈C" and subA: "DA⊆A" by auto
from BF assms have "∃DB∈C. DB⊆B" using basic_element_filter by simp
then obtain DB where perB: "DB∈C" and subB: "DB⊆B" by auto
from assms(2) perA perB have "∃D∈C. D⊆DA∩DB"
unfolding SatisfiesFilterBase_def by auto
then obtain D where "D∈C" "D⊆DA∩DB" by auto
with subA subB AF BF have "A∩B∈{A ∈ Pow(⋃𝔉) . ∃D∈C. D ⊆ A}" by auto
with assms(1) have "A∩B∈𝔉" unfolding IsBaseFilter_def by auto
}
moreover
{
fix A B
assume AF: "A∈𝔉" and BS: "B∈Pow(⋃𝔉)" and sub: "A⊆B"
from assms(1) AF have "∃D∈C. D⊆A" using basic_element_filter by auto
then obtain D where "D⊆A" "D∈C" by auto
with sub BS have "B∈{A∈Pow(⋃𝔉). ∃D∈C. D⊆A}" by auto
with assms(1) have "B∈𝔉" unfolding IsBaseFilter_def by auto
}
moreover
from assms(2) have "C≠0" using SatisfiesFilterBase_def by auto
then obtain D where "D∈C" by auto
with assms(1) have "D⊆⋃𝔉" using IsBaseFilter_def by auto
with ‹D∈C› have "⋃𝔉∈{A∈Pow(⋃𝔉). ∃D∈C. D⊆A}" by auto
with assms(1) have "⋃𝔉∈𝔉" unfolding IsBaseFilter_def by auto
moreover
{
assume "0∈𝔉"
with assms(1) have "∃D∈C. D⊆0" using basic_element_filter by simp
then obtain D where "D∈C""D⊆0" by auto
then have "D∈C" "D=0" by auto
with assms(2) have "False" using SatisfiesFilterBase_def by auto
}
then have "0∉𝔉" by auto
ultimately show ?thesis using IsFilter_def by auto
qed
text‹A base filter satisfies the filter base condition.›
theorem basic_filter_2:
assumes "C {is a base filter} 𝔉" and "𝔉 {is a filter on} ⋃𝔉"
shows "C {satisfies the filter base condition}"
proof-
{
fix A B
assume AF: "A∈C" and BF: "B∈C"
then have "A∈𝔉" and "B∈𝔉" using assms(1) IsBaseFilter_def by auto
then have "A∩B∈𝔉" using assms(2) IsFilter_def by auto
then have "∃D∈C. D⊆A∩B" using assms(1) basic_element_filter by blast
}
then have "∀A∈C. ∀B∈C. ∃D∈C. D⊆A∩B" by auto
moreover
{
assume "0∈C"
then have "0∈𝔉" using assms(1) IsBaseFilter_def by auto
then have "False" using assms(2) IsFilter_def by auto
}
then have "0∉C" by auto
moreover
{
assume "C=0"
then have "𝔉=0" using assms(1) IsBaseFilter_def by auto
then have "False" using assms(2) IsFilter_def by auto
}
then have "C≠0" by auto
ultimately show ?thesis using SatisfiesFilterBase_def by auto
qed
text‹A base filter for a collection satisfies the filter base condition iff that collection
is in fact a filter.›
theorem basic_filter:
assumes "C {is a base filter} 𝔉"
shows "(C {satisfies the filter base condition}) ⟷ (𝔉 {is a filter on} ⋃𝔉)"
using assms basic_filter_1 basic_filter_2 by auto
text‹A base for a filter determines a filter up to the underlying set.›
theorem base_unique_filter:
assumes "C {is a base filter} 𝔉1"and "C {is a base filter} 𝔉2"
shows "𝔉1=𝔉2 ⟷ ⋃𝔉1=⋃𝔉2"
using assms unfolding IsBaseFilter_def by auto
text‹Suppose 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 ⊆ Pow(X)" and "C≠0"
shows "C {is a base filter} {A∈Pow(X). ∃D∈C. D⊆A}" and "⋃{A∈Pow(X). ∃D∈C. D⊆A}=X"
proof-
from assms(1) have "C⊆{A∈Pow(X). ∃D∈C. D⊆A}" by auto
moreover
from assms(2) obtain D where "D∈C" by auto
then have "D⊆X" using assms(1) by auto
with ‹D∈C› have "X∈{A∈Pow(X). ∃D∈C. D⊆A}" by auto
then show "⋃{A∈Pow(X). ∃D∈C. D⊆A}=X" by auto
ultimately
show "C {is a base filter} {A∈Pow(X). ∃D∈C. D⊆A}" using IsBaseFilter_def by auto
qed
text‹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⊆Pow(X)" and "C {satisfies the filter base condition}"
shows "((C {is a base filter} 𝔉) ∧ ⋃𝔉=X) ⟷ 𝔉={A∈Pow(X). ∃D∈C. D⊆A}"
using assms IsBaseFilter_def SatisfiesFilterBase_def base_unique_filter_set1
by auto
text‹A simple corollary from the previous lemma.›
corollary base_unique_filter_set3:
assumes "C⊆Pow(X)" and "C {satisfies the filter base condition}"
shows "C {is a base filter} {A∈Pow(X). ∃D∈C. D⊆A}" and "⋃{A∈Pow(X). ∃D∈C. D⊆A} = X"
proof -
let ?𝔉 = "{A∈Pow(X). ∃D∈C. D⊆A}"
from assms have "(C {is a base filter} ?𝔉) ∧ ⋃?𝔉=X"
using base_unique_filter_set2 by simp
thus "C {is a base filter} ?𝔉" and "⋃?𝔉 = X"
by auto
qed
text‹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)
FilterConverges ("_ →⇩F _" 50) where
"𝔉{is a filter on}⋃T ⟹ 𝔉→⇩Fx ≡
x∈⋃T ∧ ({U∈Pow(⋃T). x∈int(U)} ⊆ 𝔉)"
text‹The neighborhoods of a point form a filter that converges to that point.›
lemma (in topology0) neigh_filter:
assumes "x∈⋃T"
defines "Neigh≡{U∈Pow(⋃T). x∈int(U)}"
shows "Neigh {is a filter on}⋃T" and "Neigh →⇩F x"
proof-
{
fix A B
assume p:"A∈Neigh" "B∈Neigh"
have "A∩B∈Neigh"
proof-
from p have "A∩B∈Pow(⋃T)" using Neigh_def by auto
moreover
{from p have "x∈int(A)" "x∈int(B)" using Neigh_def by auto
then have "x∈int(A)∩int(B)" by auto
moreover
{ have "int(A)∩int(B)⊆A∩B" using Top_2_L1 by auto
moreover have "int(A)∩int(B)∈T"
using Top_2_L2 topSpaceAssum IsATopology_def by blast
ultimately have "int(A)∩int(B)⊆int(A∩B)" using Top_2_L5 by auto}
ultimately have "x∈int(A∩B)" by auto
}
ultimately show ?thesis using Neigh_def by auto
qed
}
moreover
{
fix A B
assume A: "A∈Neigh" and B: "B∈Pow(⋃T)" and sub: "A⊆B"
from sub have "int(A)∈T" "int(A)⊆B" using Top_2_L2 Top_2_L1
by auto
then have "int(A)⊆int(B)" using Top_2_L5 by auto
with A have "x∈int(B)" using Neigh_def by auto
with B have "B∈Neigh" using Neigh_def by auto
}
moreover
{
assume "0∈Neigh"
then have "x∈Interior(0,T)" using Neigh_def by auto
then have "x∈0" using Top_2_L1 by auto
then have "False" by auto
}
then have "0∉Neigh" by auto
moreover
have "⋃T∈T" using topSpaceAssum IsATopology_def by auto
then have "Interior(⋃T,T)=⋃T" using Top_2_L3 by auto
with assms(1) have ab: "⋃T∈Neigh" unfolding Neigh_def by auto
moreover have "Neigh⊆Pow(⋃T)" using Neigh_def by auto
ultimately show "Neigh {is a filter on} ⋃T" using IsFilter_def
by auto
moreover from ab have "⋃Neigh=⋃T" unfolding Neigh_def by auto
ultimately show "Neigh →⇩F x" using FilterConverges_def assms(1) Neigh_def by auto
qed
text‹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 "𝔉 {is a filter on} ⋃T" and "C {is a base filter} 𝔉" and "𝔉 →⇩F x"
shows "∀U∈Pow(⋃T). x∈int(U) ⟶ (∃D∈C. D⊆U)" and "x∈⋃T"
proof -
{ fix U
assume "U⊆(⋃T)" and "x∈int(U)"
with assms(1,3) have "U∈𝔉" using FilterConverges_def by auto
with assms(2) have "∃D∈C. D⊆U" using basic_element_filter by blast
} thus "∀U∈Pow(⋃T). x∈int(U) ⟶ (∃D∈C. D⊆U)" by auto
from assms(1,3) show "x∈⋃T" using FilterConverges_def by auto
qed
text‹A sufficient condition for a filter to converge to a point.›
theorem (in topology0) convergence_filter_base2:
assumes "𝔉 {is a filter on} ⋃T" and "C {is a base filter} 𝔉"
and "∀U∈Pow(⋃T). x∈int(U) ⟶ (∃D∈C. D⊆U)" and "x∈⋃T"
shows "𝔉 →⇩F x"
proof-
{
fix U
assume AS: "U∈Pow(⋃T)" "x∈int(U)"
then obtain D where pD:"D∈C" and s:"D⊆U" using assms(3) by blast
with assms(2) AS have "D∈𝔉" and "D⊆U" and "U∈Pow(⋃T)"
using IsBaseFilter_def by auto
with assms(1) have "U∈𝔉" using IsFilter_def by auto
}
with assms(1,4) show ?thesis using FilterConverges_def by auto
qed
text‹A necessary and sufficient condition for a filter to converge to a point.›
theorem (in topology0) convergence_filter_base_eq:
assumes "𝔉 {is a filter on} ⋃T" and "C {is a base filter} 𝔉"
shows "(𝔉 →⇩F x) ⟷ ((∀U∈Pow(⋃T). x∈int(U) ⟶ (∃D∈C. D⊆U)) ∧ x∈⋃T)"
proof
assume "𝔉 →⇩F x"
with assms show "((∀U∈Pow(⋃T). x∈int(U) ⟶ (∃D∈C. D⊆U)) ∧ x∈⋃T)"
using convergence_filter_base1 by simp
next
assume "(∀U∈Pow(⋃T). x∈int(U) ⟶ (∃D∈C. D⊆U)) ∧ x∈⋃T"
with assms show "𝔉 →⇩F x" using convergence_filter_base2
by auto
qed
subsection‹Relation between nets and filters›
text‹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.›
text‹Let's build now a net from a filter, such that both converge to the same points.›
definition
NetOfFilter ("Net(_)" 40) where
"𝔉 {is a filter on} ⋃𝔉 ⟹ Net(𝔉) ≡
⟨{⟨A,fst(A)⟩. A∈{⟨x,F⟩∈(⋃𝔉)×𝔉. x∈F}},{⟨A,B⟩∈{⟨x,F⟩∈(⋃𝔉)×𝔉. x∈F}×{⟨x,F⟩∈(⋃𝔉)×𝔉. x∈F}. snd(B)⊆snd(A)}⟩"
text‹Net of a filter is indeed a net.›
theorem net_of_filter_is_net:
assumes "𝔉 {is a filter on} X"
shows "(Net(𝔉)) {is a net on} X"
proof-
from assms have "X∈𝔉" "𝔉⊆Pow(X)" using IsFilter_def by auto
then have uu:"⋃𝔉=X" by blast
let ?f = "{⟨A,fst(A)⟩. A∈{⟨x,F⟩∈(⋃𝔉)×𝔉. x∈F}}"
let ?r = "{⟨A,B⟩∈{⟨x,F⟩∈(⋃𝔉)×𝔉. x∈F}×{⟨x,F⟩∈(⋃𝔉)×𝔉. x∈F}. snd(B)⊆snd(A)}"
have "function(?f)" using function_def by auto
moreover have "relation(?f)" using relation_def by auto
ultimately have "?f:domain(?f)→range(?f)" using function_imp_Pi
by auto
have dom:"domain(?f)={⟨x,F⟩∈(⋃𝔉)×𝔉. x∈F}" by auto
have "range(?f)⊆⋃𝔉" by auto
with ‹?f:domain(?f)→range(?f)› have "?f:domain(?f)→⋃𝔉" using fun_weaken_type by auto
moreover
{
{
fix t
assume pp:"t∈domain(?f)"
then have "snd(t)⊆snd(t)" by auto
with dom pp have "⟨t,t⟩∈?r" by auto
}
then have "refl(domain(?f),?r)" using refl_def by auto
moreover
{
fix t1 t2 t3
assume "⟨t1,t2⟩∈?r" "⟨t2,t3⟩∈?r"
then have "snd(t3)⊆snd(t1)" "t1∈domain(?f)" "t3∈domain(?f)" using dom by auto
then have "⟨t1,t3⟩∈?r" by auto
}
then have "trans(?r)" using trans_def by auto
moreover
{
fix x y
assume as:"x∈domain(?f)""y∈domain(?f)"
then have "snd(x)∈𝔉" "snd(y)∈𝔉" by auto
then have p:"snd(x)∩snd(y)∈𝔉" using assms IsFilter_def by auto
{
assume "snd(x)∩snd(y)=0"
with p have "0∈𝔉" by auto
then have "False" using assms IsFilter_def by auto
}
then have "snd(x)∩snd(y)≠0" by auto
then obtain xy where "xy∈snd(x)∩snd(y)" by auto
then have "xy∈snd(x)∩snd(y)" "⟨xy,snd(x)∩snd(y)⟩∈(⋃𝔉)×𝔉" using p by auto
then have "⟨xy,snd(x)∩snd(y)⟩∈{⟨x,F⟩∈(⋃𝔉)×𝔉. x∈F}" by auto
with dom have d:"⟨xy,snd(x)∩snd(y)⟩∈domain(?f)" by auto
with as have "⟨x,⟨xy,snd(x)∩snd(y)⟩⟩∈?r ∧ ⟨y,⟨xy,snd(x)∩snd(y)⟩⟩∈?r" by auto
with d have "∃z∈domain(?f). ⟨x,z⟩∈?r ∧ ⟨y,z⟩∈?r" by blast
}
then have "∀x∈domain(?f). ∀y∈domain(?f). ∃z∈domain(?f). ⟨x,z⟩∈?r ∧ ⟨y,z⟩∈?r" by blast
ultimately have "?r directs domain(?f)" using IsDirectedSet_def by blast
}
moreover
{
have p:"X∈𝔉" and "0∉𝔉" using assms IsFilter_def by auto
then have "X≠0" by auto
then obtain q where "q∈X" by auto
with p dom have "⟨q,X⟩∈domain(?f)" by auto
then have "domain(?f)≠0" by blast
}
ultimately have "⟨?f,?r⟩ {is a net on}⋃𝔉" using IsNet_def by auto
then show "(Net(𝔉)) {is a net on} X" using NetOfFilter_def assms uu by auto
qed
text‹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 "𝔉 {is a filter on} ⋃T" and "𝔉 →⇩F x"
shows "(Net(𝔉)) →⇩N x"
proof-
from assms have "⋃T∈𝔉" "𝔉⊆Pow(⋃T)" using IsFilter_def by auto
then have uu: "⋃𝔉=⋃T" by blast
from assms(1) have func: "fst(Net(𝔉))={⟨A,fst(A)⟩. A∈{⟨x,F⟩∈(⋃𝔉)×𝔉. x∈F}}"
and dir: "snd(Net(𝔉))={⟨A,B⟩∈{⟨x,F⟩∈(⋃𝔉)×𝔉. x∈F}×{⟨x,F⟩∈(⋃𝔉)×𝔉. x∈F}. snd(B)⊆snd(A)}"
using NetOfFilter_def uu by auto
then have dom_def: "domain(fst(Net(𝔉)))={⟨x,F⟩∈(⋃𝔉)×𝔉. x∈F}" by auto
from func have fun: "fst(Net(𝔉)): {⟨x,F⟩∈(⋃𝔉)×𝔉. x∈F} → (⋃𝔉)"
using ZF_fun_from_total by simp
from assms(1) have NN: "(Net(𝔉)) {is a net on}⋃T" using net_of_filter_is_net
by auto
moreover from assms have "x∈⋃T" using FilterConverges_def
by auto
moreover
{
fix U
assume AS: "U∈Pow(⋃T)" "x∈int(U)"
with assms have "U∈𝔉" "x∈U" using Top_2_L1 FilterConverges_def by auto
then have pp: "⟨x,U⟩∈domain(fst(Net(𝔉)))" using dom_def by auto
{
fix m
assume ASS: "m∈domain(fst(Net(𝔉)))" "⟨⟨x,U⟩,m⟩∈snd(Net(𝔉))"
from ASS(1) fun func have "fst(Net(𝔉))`(m) = fst(m)"
using func1_1_L1 ZF_fun_from_tot_val by simp
with dir ASS have "fst(Net(𝔉))`(m) ∈ U" using dom_def by auto
}
then have "∀m∈domain(fst(Net(𝔉))). (⟨⟨x,U⟩,m⟩∈snd(Net(𝔉)) ⟶ fst(Net(𝔉))`m∈U)" by auto
with pp have "∃t∈domain(fst(Net(𝔉))). ∀m∈domain(fst(Net(𝔉))). (⟨t,m⟩∈snd(Net(𝔉)) ⟶ fst(Net(𝔉))`m∈U)"
by auto
}
then have "∀U∈Pow(⋃T).
(x∈int(U) ⟶ (∃t∈domain(fst(Net(𝔉))). ∀m∈domain(fst(Net(𝔉))). (⟨t,m⟩∈snd(Net(𝔉)) ⟶ fst(Net(𝔉))`m∈U)))"
by auto
ultimately show ?thesis using NetConverges_def by auto
qed
text‹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 "𝔉 {is a filter on}⋃T" and "(Net(𝔉)) →⇩N x"
shows "𝔉 →⇩F x"
proof-
from assms have "⋃T∈𝔉" "𝔉⊆Pow(⋃T)" using IsFilter_def by auto
then have uu: "⋃𝔉=⋃T" by blast
have "x∈⋃T" using assms NetConverges_def net_of_filter_is_net by auto
moreover
{
fix U
assume "U∈Pow(⋃T)" "x∈int(U)"
then obtain t where t: "t∈domain(fst(Net(𝔉)))" and
reg: "∀m∈domain(fst(Net(𝔉))). ⟨t,m⟩∈snd(Net(𝔉)) ⟶ fst(Net(𝔉))`m∈U"
using assms net_of_filter_is_net NetConverges_def by blast
with assms(1) uu obtain t1 t2 where t_def: "t=⟨t1,t2⟩" and "t1∈t2" and tFF: "t2∈𝔉"
using NetOfFilter_def by auto
{
fix s
assume "s∈t2"
then have "⟨s,t2⟩∈{⟨q1,q2⟩∈⋃𝔉×𝔉. q1∈q2}" using tFF by auto
moreover
from assms(1) uu have "domain(fst(Net(𝔉)))={⟨q1,q2⟩∈⋃𝔉×𝔉. q1∈q2}" using NetOfFilter_def
by auto
ultimately
have tt: "⟨s,t2⟩∈domain(fst(Net(𝔉)))" by auto
moreover
from assms(1) uu t t_def tt have "⟨⟨t1,t2⟩,⟨s,t2⟩⟩∈snd(Net(𝔉))" using NetOfFilter_def
by auto
ultimately
have "fst(Net(𝔉))`⟨s,t2⟩∈U" using reg t_def by auto
moreover
from assms(1) uu have "function(fst(Net(𝔉)))" using NetOfFilter_def function_def
by auto
moreover
from tt assms(1) uu have "⟨⟨s,t2⟩,s⟩∈fst(Net(𝔉))" using NetOfFilter_def by auto
ultimately
have "s∈U" using NetOfFilter_def function_apply_equality by auto
}
then have "t2⊆U" by auto
with tFF assms(1) ‹U∈Pow(⋃T)› have "U∈𝔉" using IsFilter_def by auto
}
then have "{U∈Pow(⋃T). x∈int(U)} ⊆ 𝔉" by auto
ultimately
show ?thesis using FilterConverges_def assms(1) by auto
qed
text‹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 "𝔉 {is a filter on}⋃T"
shows "(𝔉 →⇩F x) ⟷ ((Net(𝔉)) →⇩N x)"
using filter_conver_net_of_filter_conver net_of_filter_conver_filter_conver assms
by auto
text‹The 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 ‹Net(𝔉)› 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
FilterOfNet ("Filter (_ .. _)" 40) where
"(N {is a net on} X) ⟹ Filter N..X ≡ {A∈Pow(X). ∃D∈{{fst(N)`snd(s). s∈{s∈domain(fst(N))×domain(fst(N)). s∈snd(N) ∧ fst(s)=t0}}. t0∈domain(fst(N))}. D⊆A}"
text‹Filter of a net is indeed a filter›
theorem filter_of_net_is_filter:
assumes "N {is a net on} X"
shows "(Filter N..X) {is a filter on} X" and
"{{fst(N)`snd(s). s∈{s∈domain(fst(N))×domain(fst(N)). s∈snd(N) ∧ fst(s)=t0}}. t0∈domain(fst(N))} {is a base filter} (Filter N..X)"
proof -
let ?C = "{{fst(N)`(snd(s)). s∈{s∈domain(fst(N))×domain(fst(N)). s∈snd(N) ∧ fst(s)=t0}}. t0∈domain(fst(N))}"
have "?C⊆Pow(X)"
proof -
{
fix t
assume "t∈?C"
then obtain t1 where "t1∈domain(fst(N))" and
t_Def: "t={fst(N)`snd(s). s∈{s∈domain(fst(N))×domain(fst(N)). s∈snd(N) ∧ fst(s)=t1}}"
by auto
{
fix x
assume "x∈t"
with t_Def obtain ss where "ss∈{s∈domain(fst(N))×domain(fst(N)). s∈snd(N) ∧ fst(s)=t1}" and
x_def: "x = fst(N)`(snd(ss))" by blast
then have "snd(ss) ∈ domain(fst(N))" by auto
from assms have "fst(N):domain(fst(N))→X" unfolding IsNet_def by simp
with ‹snd(ss) ∈ domain(fst(N))› have "x∈X" using apply_funtype x_def
by auto
}
hence "t⊆X" by auto
}
thus ?thesis by blast
qed
have sat: "?C {satisfies the filter base condition}"
proof -
from assms obtain t1 where "t1∈domain(fst(N))" using IsNet_def by blast
hence "{fst(N)`snd(s). s∈{s∈domain(fst(N))×domain(fst(N)). s∈snd(N) ∧ fst(s)=t1}}∈?C"
by auto
hence "?C≠0" by auto
moreover
{
fix U
assume "U∈?C"
then obtain q where q_dom: "q∈domain(fst(N))" and
U_def: "U={fst(N)`snd(s). s∈{s∈domain(fst(N))×domain(fst(N)). s∈snd(N) ∧ fst(s)=q}}"
by blast
with assms have "⟨q,q⟩∈snd(N) ∧ fst(⟨q,q⟩)=q" unfolding IsNet_def IsDirectedSet_def refl_def
by auto
with q_dom have "⟨q,q⟩∈{s∈domain(fst(N))×domain(fst(N)). s∈snd(N) ∧ fst(s)=q}"
by auto
with U_def have "fst(N)`(snd(⟨q,q⟩)) ∈ U" by blast
hence "U≠0" by auto
}
then have "0∉?C" by auto
moreover
have "∀A∈?C. ∀B∈?C. (∃D∈?C. D⊆A∩B)"
proof
fix A
assume pA: "A∈?C"
show "∀B∈?C. ∃D∈?C. D⊆A∩B"
proof
{
fix B
assume "B∈?C"
with pA obtain qA qB where per: "qA∈domain(fst(N))" "qB∈domain(fst(N))" and
A_def: "A={fst(N)`snd(s). s∈{s∈domain(fst(N))×domain(fst(N)). s∈snd(N) ∧ fst(s)=qA}}" and
B_def: "B={fst(N)`snd(s). s∈{s∈domain(fst(N))×domain(fst(N)). s∈snd(N) ∧ fst(s)=qB}}"
by blast
have dir: "snd(N) directs domain(fst(N))" using assms IsNet_def by auto
with per obtain qD where ine: "⟨qA,qD⟩∈snd(N)" "⟨qB,qD⟩∈snd(N)" and
perD: "qD∈domain(fst(N))" unfolding IsDirectedSet_def
by blast
let ?D = "{fst(N)`snd(s). s∈{s∈domain(fst(N))×domain(fst(N)). s∈snd(N) ∧ fst(s)=qD}}"
from perD have "?D∈?C" by auto
moreover
{
fix d
assume "d∈?D"
then obtain sd where "sd∈{s∈domain(fst(N))×domain(fst(N)). s∈snd(N) ∧ fst(s)=qD}" and
d_def: "d=fst(N)`snd(sd)" by blast
then have sdN: "sd∈snd(N)" and qdd: "fst(sd)=qD" and "sd∈domain(fst(N))×domain(fst(N))"
by auto
then obtain qI aa where "sd = ⟨aa,qI⟩" "qI ∈ domain(fst(N))" "aa ∈ domain(fst(N))"
by auto
with qdd have sd_def: "sd=⟨qD,qI⟩" and qIdom: "qI∈domain(fst(N))" by auto
with sdN have "⟨qD,qI⟩∈snd(N)" by auto
from dir have "trans(snd(N))" unfolding IsDirectedSet_def by auto
then have "⟨qA,qD⟩∈snd(N) ∧ ⟨qD,qI⟩∈snd(N) ⟶ ⟨qA,qI⟩∈snd(N)" and
"⟨qB,qD⟩∈snd(N) ∧ ⟨qD,qI⟩∈snd(N)⟶⟨qB,qI⟩∈snd(N)"
using trans_def by auto
with ine ‹⟨qD,qI⟩∈snd(N)› have "⟨qA,qI⟩∈snd(N)" "⟨qB,qI⟩∈snd(N)" by auto
with qIdom per have "⟨qA,qI⟩∈{s∈domain(fst(N))×domain(fst(N)). s∈snd(N) ∧ fst(s)=qA}"
"⟨qB,qI⟩∈{s∈domain(fst(N))×domain(fst(N)). s∈snd(N) ∧ fst(s)=qB}"
by auto
then have "fst(N)`(qI) ∈ A∩B" using A_def B_def by auto
then have "fst(N)`(snd(sd)) ∈ A∩B" using sd_def by auto
then have "d ∈ A∩B" using d_def by auto
}
then have "?D ⊆ A∩B" by blast
ultimately show "∃D∈?C. D⊆A∩B" by blast
}
qed
qed
ultimately
show ?thesis unfolding SatisfiesFilterBase_def by blast
qed
have
Base: "?C {is a base filter} {A∈Pow(X). ∃D∈?C. D⊆A}" "⋃{A∈Pow(X). ∃D∈?C. D⊆A}=X"
proof -
from ‹?C⊆Pow(X)› sat show "?C {is a base filter} {A∈Pow(X). ∃D∈?C. D⊆A}"
by (rule base_unique_filter_set3)
from ‹?C⊆Pow(X)› sat show "⋃{A∈Pow(X). ∃D∈?C. D⊆A}=X"
by (rule base_unique_filter_set3)
qed
with sat show "(Filter N..X) {is a filter on} X"
using sat basic_filter FilterOfNet_def assms by auto
from Base(1) show "?C {is a base filter} (Filter N..X)"
using FilterOfNet_def assms by auto
qed
text‹Convergence of a net implies the convergence of the corresponding filter.›
theorem (in topology0) net_conver_filter_of_net_conver:
assumes "N {is a net on} ⋃T" and "N →⇩N x"
shows "(Filter N..(⋃T)) →⇩F x"
proof -
let ?C = "{{fst(N)`snd(s). s∈{s∈domain(fst(N))×domain(fst(N)). s∈snd(N) ∧ fst(s)=t}}.
t∈domain(fst(N))}"
from assms(1) have
"(Filter N..(⋃T)) {is a filter on} (⋃T)" and "?C {is a base filter} Filter N..(⋃T)"
using filter_of_net_is_filter by auto
moreover have "∀U∈Pow(⋃T). x∈int(U) ⟶ (∃D∈?C. D⊆U)"
proof -
{
fix U
assume "U∈Pow(⋃T)" "x∈int(U)"
with assms have "∃t∈domain(fst(N)). (∀m∈domain(fst(N)). (⟨t,m⟩∈snd(N) ⟶ fst(N)`m∈U))"
using NetConverges_def by auto
then obtain t where "t∈domain(fst(N))" and
reg: "∀m∈domain(fst(N)). (⟨t,m⟩∈snd(N) ⟶ fst(N)`m∈U)" by auto
{
fix f
assume "f∈{fst(N)`snd(s). s∈{s∈domain(fst(N))×domain(fst(N)). s∈snd(N) ∧ fst(s)=t}}"
then obtain s where "s∈{s∈domain(fst(N))×domain(fst(N)). s∈snd(N) ∧ fst(s)=t}" and
f_def: "f=fst(N)`snd(s)" by blast
hence "s∈domain(fst(N))×domain(fst(N))" and "s∈snd(N)" and "fst(s)=t"
by auto
hence "s=⟨t,snd(s)⟩" and "snd(s)∈domain(fst(N))" by auto
with ‹s∈snd(N)› reg have "fst(N)`snd(s)∈U" by auto
with f_def have "f∈U" by auto
}
hence "{fst(N)`snd(s). s∈{s∈domain(fst(N))×domain(fst(N)). s∈snd(N) ∧ fst(s)=t}} ⊆ U"
by blast
with ‹t∈domain(fst(N))› have "∃D∈?C. D⊆U"
by auto
} thus "∀U∈Pow(⋃T). x∈int(U) ⟶ (∃D∈?C. D⊆U)" by auto
qed
moreover from assms have "x∈⋃T" using NetConverges_def by auto
ultimately show "(Filter N..(⋃T)) →⇩F x" by (rule convergence_filter_base2)
qed
text‹Convergence of a filter corresponding to a net implies convergence of the net.›
theorem (in topology0) filter_of_net_conver_net_conver:
assumes "N {is a net on} ⋃T" and "(Filter N..(⋃T)) →⇩F x"
shows "N →⇩N x"
proof -
let ?C = "{{fst(N)`snd(s). s∈{s∈domain(fst(N))×domain(fst(N)). s∈snd(N) ∧ fst(s)=t}}.
t∈domain(fst(N))}"
from assms have I: "(Filter N..(⋃T)) {is a filter on} (⋃T)"
"?C {is a base filter} (Filter N..(⋃T))" "(Filter N..(⋃T)) →⇩F x"
using filter_of_net_is_filter by auto
then have reg: "∀U∈Pow(⋃T). x∈int(U) ⟶ (∃D∈?C. D⊆U)"
by (rule convergence_filter_base1)
from I have "x∈⋃T" by (rule convergence_filter_base1)
moreover
{
fix U
assume "U∈Pow(⋃T)" "x∈int(U)"
with reg have "∃D∈?C. D⊆U" by auto
then obtain D where "D∈?C" "D⊆U"
by auto
then obtain td where "td∈domain(fst(N))" and
D_def: "D={fst(N)`snd(s). s∈{s∈domain(fst(N))×domain(fst(N)). s∈snd(N) ∧ fst(s)=td}}"
by auto
{
fix m
assume "m∈domain(fst(N))" "⟨td,m⟩∈snd(N)"
with ‹td∈domain(fst(N))› have
"⟨td,m⟩∈{s∈domain(fst(N))×domain(fst(N)). s∈snd(N) ∧ fst(s)=td}"
by auto
with D_def have "fst(N)`m∈D" by auto
with ‹D⊆U› have "fst(N)`m∈U" by auto
}
then have "∀m∈domain(fst(N)). ⟨td,m⟩∈snd(N) ⟶ fst(N)`m∈U" by auto
with ‹td∈domain(fst(N))› have
"∃t∈domain(fst(N)). ∀m∈domain(fst(N)). ⟨t,m⟩∈snd(N) ⟶ fst(N)`m∈U"
by auto
}
then have
"∀U∈Pow(⋃T). x∈int(U) ⟶
(∃t∈domain(fst(N)). ∀m∈domain(fst(N)). ⟨t,m⟩∈snd(N) ⟶ fst(N)`m∈U)"
by auto
ultimately show "?thesis" using NetConverges_def assms(1) by auto
qed
text‹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 {is a net on} ⋃T"
shows "((Filter N..(⋃T)) →⇩F x) ⟷ (N →⇩N x)"
using assms filter_of_net_conver_net_conver net_conver_filter_of_net_conver
by auto
text‹We 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 "𝔉 {is a filter on} ⋃𝔉"
shows "(𝔉 ∪ {0}) {is a topology}"
proof -
{
fix A B
assume "A∈(𝔉 ∪ {0})""B∈(𝔉 ∪ {0})"
then have "(A∈𝔉 ∧ B∈𝔉) ∨ (A∩B=0)" by auto
with assms have "A∩B∈(𝔉 ∪ {0})" unfolding IsFilter_def
by blast
}
then have "∀A∈(𝔉 ∪ {0}). ∀B∈(𝔉 ∪ {0}). A∩B∈(𝔉 ∪ {0})" by auto
moreover
{
fix M
assume A:"M∈Pow(𝔉 ∪ {0})"
then have "M=0∨M={0}∨(∃T∈M. T∈𝔉)" by blast
then have "⋃M=0∨(∃T∈M. T∈𝔉)" by auto
then obtain T where "⋃M=0∨(T∈𝔉 ∧ T∈M)" by auto
then have "⋃M=0∨(T∈𝔉 ∧ T⊆⋃M)" by auto
moreover from this A have "⋃M⊆⋃𝔉" by auto
ultimately have "⋃M∈(𝔉∪{0})" using IsFilter_def assms by auto
}
then have "∀M∈Pow(𝔉∪{0}). ⋃M∈(𝔉∪{0})" by auto
ultimately show ?thesis using IsATopology_def by auto
qed
text‹We can use ‹topology0› locale with filters.›
lemma topology0_filter:
assumes "𝔉 {is a filter on} ⋃𝔉"
shows "topology0(𝔉 ∪ {0})"
using top_of_filter topology0_def assms by auto
text‹The next abbreviation introduces notation where we want to specify the space where
the filter convergence takes place.›
abbreviation FilConvTop("_ →⇩F _ {in} _")
where "𝔉 →⇩F x {in} T ≡ topology0.FilterConverges(T,𝔉,x)"
text‹The next abbreviation introduces notation where we want to specify the space where
the net convergence takes place.›
abbreviation NetConvTop("_ →⇩N _ {in} _")
where "N →⇩N x {in} T ≡ topology0.NetConverges(T,N,x)"
text‹Each point of a the union of a filter is a limit of that filter.›
lemma lim_filter_top_of_filter:
assumes "𝔉 {is a filter on} ⋃𝔉" and "x∈⋃𝔉"
shows "𝔉 →⇩F x {in} (𝔉∪{0})"
proof-
have "⋃𝔉=⋃(𝔉∪{0})" by auto
with assms(1) have assms1: "𝔉 {is a filter on} ⋃(𝔉∪{0})" by auto
{
fix U
assume "U∈Pow(⋃(𝔉∪{0}))" "x∈Interior(U,(𝔉∪{0}))"
with assms(1) have "Interior(U,(𝔉∪{0}))∈𝔉" using topology0_def top_of_filter
topology0.Top_2_L2 by blast
moreover
from assms(1) have "Interior(U,(𝔉∪{0}))⊆U" using topology0_def top_of_filter
topology0.Top_2_L1 by auto
moreover
from ‹U∈Pow(⋃(𝔉∪{0}))› have "U∈Pow(⋃𝔉)" by auto
ultimately have "U∈𝔉" using assms(1) IsFilter_def by auto
}
with assms assms1 show ?thesis using topology0.FilterConverges_def top_of_filter
topology0_def by auto
qed
end