(* This file is a part of IsarMathLib - a library of formalized mathematics written for Isabelle/Isar. Copyright (C) 2012 Daniel de la Concepcion This program is free software; Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) section ‹Topology 4› theory Topology_ZF_4 imports Topology_ZF_1 Order_ZF func1 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{*First we need to define what a directed set is:*} definition IsDirectedSet ("_ directs _" 90) where "r directs D ≡ refl(D,r) ∧ trans(r) ∧ (∀x∈D. ∀y∈D. ∃z∈D. ⟨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 corollary Le_directs_nat: shows "IsLinOrder(nat,Le)" "Le directs nat" proof- have "antisym(Le)" unfolding antisym_def Le_def using le_anti_sym by auto moreover have "trans(Le)" unfolding trans_def Le_def using le_trans by auto moreover { fix n m assume "n∈nat" "m∈nat" then have "Ord(n)" "Ord(m)" using nat_into_Ord by auto then have "n≤m ∨ m≤n" using Ord_linear_le[where thesis="n≤m ∨ m≤n"] by auto } then have "Le{is total on}nat" unfolding IsTotal_def Le_def by auto ultimately show "IsLinOrder(nat,Le)" unfolding IsLinOrder_def by auto 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{*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 ⟹ 𝔉→⇩_{F}x ≡ 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 @{text "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 @{text "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