:: Filters - Part I. Implicative Lattices :: by Grzegorz Bancerek :: :: Received July 3, 1990 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies LATTICES, SUBSET_1, XBOOLE_0, PBOOLE, EQREL_1, CARD_FIL, STRUCT_0, TARSKI, ORDINAL1, ZFMISC_1, SETFAM_1, INT_2, XBOOLEAN, BINOP_1, REALSET1, FUNCT_1, RELAT_1, MCART_1, XXREAL_2, RELAT_2, FILTER_0; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, FUNCT_1, XTUPLE_0, MCART_1, ORDINAL1, RELAT_2, FUNCT_2, BINOP_1, REALSET1, STRUCT_0, LATTICES, DOMAIN_1, RELAT_1, RELSET_1, EQREL_1; constructors SETFAM_1, RELAT_2, ORDINAL1, PARTFUN1, BINOP_1, REALSET1, LATTICES, RELSET_1, XTUPLE_0; registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, LATTICES; requirements SUBSET, BOOLE; begin reserve L for Lattice, p,p1,q,q1,r,r1 for Element of L; reserve x,y,z,X,Y,Z,X1,X2 for set; theorem :: FILTER_0:1 for L being join-associative join-commutative meet-commutative join-absorbing meet-absorbing non empty LattStr, p, q, r being Element of L st p [= q holds r "\/" p [= r "\/" q; theorem :: FILTER_0:2 p [= r implies p "/\" q [= r; theorem :: FILTER_0:3 p [= r implies p [= q"\/"r; theorem :: FILTER_0:4 for L being join-absorbing join-commutative join-associative non empty LattStr, a, b, c, d being Element of L st a [= b & c [= d holds a "\/" c [= b "\/" d; theorem :: FILTER_0:5 for L being meet-absorbing meet-commutative join-absorbing meet-associative non empty LattStr, a, b, c, d being Element of L st a [= b & c [= d holds a "/\" c [= b "/\" d; theorem :: FILTER_0:6 for L being join-absorbing join-commutative join-associative meet-absorbing meet-commutative non empty LattStr, a, b, c being Element of L st a [= c & b [= c holds a "\/" b [= c; theorem :: FILTER_0:7 for L being meet-absorbing meet-commutative join-absorbing meet-associative non empty LattStr, a, b, c being Element of L st a [= b & a [= c holds a [= b "/\" c; definition let L; mode Filter of L is non empty meet-closed final Subset of L; end; theorem :: FILTER_0:8 for S being non empty Subset of L holds S is Filter of L iff for p,q being Element of L holds p in S & q in S iff p "/\" q in S; theorem :: FILTER_0:9 for D being non empty Subset of L holds D is Filter of L iff (for p,q st p in D & q in D holds p "/\" q in D) & for p,q st p in D & p [= q holds q in D; reserve H,F for Filter of L; theorem :: FILTER_0:10 p in H implies p"\/"q in H & q"\/"p in H; theorem :: FILTER_0:11 L is 1_Lattice implies Top L in H; theorem :: FILTER_0:12 L is 1_Lattice implies {Top L} is Filter of L; theorem :: FILTER_0:13 {p} is Filter of L implies L is upper-bounded; theorem :: FILTER_0:14 the carrier of L is Filter of L; definition let L; func <.L.) -> Filter of L equals :: FILTER_0:def 1 the carrier of L; end; definition let L,p; func <.p.) -> Filter of L equals :: FILTER_0:def 2 { q : p [= q }; end; theorem :: FILTER_0:15 q in <.p.) iff p [= q; theorem :: FILTER_0:16 p in <.p.) & p "\/" q in <.p.) & q "\/" p in <.p.); theorem :: FILTER_0:17 L is 0_Lattice implies <.L.) = <.Bottom L.); definition let L,F; attr F is being_ultrafilter means :: FILTER_0:def 3 F <> the carrier of L & for H st F c= H & H <> the carrier of L holds F = H; end; theorem :: FILTER_0:18 L is lower-bounded implies for F st F <> the carrier of L ex H st F c= H & H is being_ultrafilter; theorem :: FILTER_0:19 (ex r st p "/\" r <> p) implies <.p.) <> the carrier of L; theorem :: FILTER_0:20 L is 0_Lattice & p <> Bottom L implies ex H st p in H & H is being_ultrafilter; reserve D for non empty Subset of L; definition let L,D; func <.D.) -> Filter of L means :: FILTER_0:def 4 D c= it & for F st D c= F holds it c= F; end; theorem :: FILTER_0:21 <.F.) = F; reserve D1,D2 for non empty Subset of L; theorem :: FILTER_0:22 D1 c= D2 implies <.D1.) c= <.D2.); theorem :: FILTER_0:23 p in D implies <.p.) c= <.D.); theorem :: FILTER_0:24 D = {p} implies <.D.) = <.p.); theorem :: FILTER_0:25 L is 0_Lattice & Bottom L in D implies <.D.) = <.L.) & <.D.) = the carrier of L; theorem :: FILTER_0:26 L is 0_Lattice & Bottom L in F implies F = <.L.) & F = the carrier of L; definition let L,F; attr F is prime means :: FILTER_0:def 5 p "\/" q in F iff p in F or q in F; end; theorem :: FILTER_0:27 L is B_Lattice implies for p,q holds p "/\" (p` "\/" q) [= q & for r st p "/\" r [= q holds r [= p` "\/" q; definition let IT be non empty LattStr; attr IT is implicative means :: FILTER_0:def 6 for p,q being Element of IT ex r being Element of IT st p "/\" r [= q & for r1 being Element of IT st p "/\" r1 [= q holds r1 [= r; end; registration cluster strict implicative for Lattice; end; definition mode I_Lattice is implicative Lattice; end; definition let L,p,q; assume L is I_Lattice; func p => q -> Element of L means :: FILTER_0:def 7 p "/\" it [= q & for r st p "/\" r [= q holds r [= it; end; reserve I for I_Lattice, i,j,k for Element of I; registration cluster -> upper-bounded for I_Lattice; end; theorem :: FILTER_0:28 i => i = Top I; registration cluster -> distributive for I_Lattice; end; reserve B for B_Lattice, FB,HB for Filter of B; registration cluster -> implicative for B_Lattice; end; registration cluster implicative -> distributive for Lattice; end; reserve I for I_Lattice, i,j,k for Element of I, DI for non empty Subset of I, FI for Filter of I; theorem :: FILTER_0:29 i in FI & i => j in FI implies j in FI; theorem :: FILTER_0:30 j in FI implies i => j in FI; definition let L,D1,D2; func D1 "/\" D2 -> Subset of L equals :: FILTER_0:def 8 { p"/\"q : p in D1 & q in D2 }; end; registration let L,D1,D2; cluster D1 "/\" D2 -> non empty; end; theorem :: FILTER_0:31 p in D1 & q in D2 implies p"/\"q in D1 "/\" D2 & q"/\"p in D1 "/\" D2; theorem :: FILTER_0:32 x in D1 "/\" D2 implies ex p,q st x = p"/\"q & p in D1 & q in D2; theorem :: FILTER_0:33 D1 "/\" D2 = D2 "/\" D1; registration let L be D_Lattice; let F1,F2 be Filter of L; cluster F1 "/\" F2 -> final meet-closed; end; theorem :: FILTER_0:34 <.D1 \/ D2.) = <.<.D1.) \/ D2.) & <.D1 \/ D2.) = <.D1 \/ <.D2.) .); theorem :: FILTER_0:35 <.F \/ H.) = { r : ex p,q st p"/\"q [= r & p in F & q in H }; theorem :: FILTER_0:36 F c= F "/\" H & H c= F "/\" H; theorem :: FILTER_0:37 <.F \/ H.) = <.F "/\" H.); reserve F1,F2 for Filter of I; theorem :: FILTER_0:38 <.F1 \/ F2.) = F1 "/\" F2; theorem :: FILTER_0:39 <.FB \/ HB.) = FB "/\" HB; theorem :: FILTER_0:40 j in <.DI \/ {i}.) implies i => j in <.DI.); theorem :: FILTER_0:41 i => j in FI & j => k in FI implies i => k in FI; reserve a,b,c for Element of B; theorem :: FILTER_0:42 a => b = a` "\/" b; theorem :: FILTER_0:43 a [= b iff a"/\"b` = Bottom B; theorem :: FILTER_0:44 FB is being_ultrafilter iff FB <> the carrier of B & for a holds a in FB or a` in FB; theorem :: FILTER_0:45 FB <> <.B.) & FB is prime iff FB is being_ultrafilter; theorem :: FILTER_0:46 FB is being_ultrafilter implies for a holds a in FB iff not a` in FB; theorem :: FILTER_0:47 a <> b implies ex FB st FB is being_ultrafilter & (a in FB & not b in FB or not a in FB & b in FB); reserve o1,o2 for BinOp of F; definition let L,F; func latt F -> Lattice means :: FILTER_0:def 9 ex o1,o2 st o1 = (the L_join of L)||F & o2 = (the L_meet of L)||F & it = LattStr (#F, o1, o2#); end; registration let L,F; cluster latt F -> strict; end; theorem :: FILTER_0:48 for L being strict Lattice holds latt <.L.) = L; theorem :: FILTER_0:49 the carrier of latt F = F & the L_join of latt F = (the L_join of L)||F & the L_meet of latt F = (the L_meet of L)||F; theorem :: FILTER_0:50 for p9,q9 being Element of latt F st p = p9 & q = q9 holds p"\/" q = p9"\/"q9 & p"/\"q = p9"/\"q9; theorem :: FILTER_0:51 for p9,q9 being Element of latt F st p = p9 & q = q9 holds p [= q iff p9 [= q9; theorem :: FILTER_0:52 L is upper-bounded implies latt F is upper-bounded; theorem :: FILTER_0:53 L is modular implies latt F is modular; theorem :: FILTER_0:54 L is distributive implies latt F is distributive; theorem :: FILTER_0:55 L is I_Lattice implies latt F is implicative; registration let L,p; cluster latt <.p.) -> lower-bounded; end; theorem :: FILTER_0:56 Bottom latt <.p.) = p; theorem :: FILTER_0:57 L is upper-bounded implies Top latt <.p.) = Top L; theorem :: FILTER_0:58 L is 1_Lattice implies latt <.p.) is bounded; theorem :: FILTER_0:59 L is C_Lattice & L is M_Lattice implies latt <.p.) is C_Lattice; theorem :: FILTER_0:60 L is B_Lattice implies latt <.p.) is B_Lattice; definition let L,p,q; func p <=> q -> Element of L equals :: FILTER_0:def 10 (p => q)"/\"(q => p); end; theorem :: FILTER_0:61 p <=> q = q <=> p; theorem :: FILTER_0:62 i <=> j in FI & j <=> k in FI implies i <=> k in FI; definition let L,F; func equivalence_wrt F -> Relation means :: FILTER_0:def 11 field it c= the carrier of L & for p,q holds [p,q] in it iff p <=> q in F; end; theorem :: FILTER_0:63 equivalence_wrt F is Relation of the carrier of L; theorem :: FILTER_0:64 L is I_Lattice implies equivalence_wrt F is_reflexive_in the carrier of L; theorem :: FILTER_0:65 equivalence_wrt F is_symmetric_in the carrier of L; theorem :: FILTER_0:66 L is I_Lattice implies equivalence_wrt F is_transitive_in the carrier of L; theorem :: FILTER_0:67 L is I_Lattice implies equivalence_wrt F is Equivalence_Relation of the carrier of L; theorem :: FILTER_0:68 L is I_Lattice implies field equivalence_wrt F = the carrier of L; definition let I,FI; redefine func equivalence_wrt FI -> Equivalence_Relation of the carrier of I; end; definition let B,FB; redefine func equivalence_wrt FB -> Equivalence_Relation of the carrier of B; end; definition let L,F,p,q; pred p,q are_equivalence_wrt F means :: FILTER_0:def 12 p <=> q in F; end; theorem :: FILTER_0:69 p,q are_equivalence_wrt F iff [p,q] in equivalence_wrt F; theorem :: FILTER_0:70 i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB; theorem :: FILTER_0:71 p,q are_equivalence_wrt F implies q,p are_equivalence_wrt F; theorem :: FILTER_0:72 (i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI) & (a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB); begin :: Addenda :: missing, 2006.12.05, AT theorem :: FILTER_0:73 for L being meet-absorbing meet-commutative meet-associative join-absorbing join-commutative non empty LattStr for x,y,z being Element of L st z [= x & z [= y & for z9 being Element of L st z9 [= x & z9 [= y holds z9 [= z holds z = x "/\" y; theorem :: FILTER_0:74 for L being meet-absorbing meet-commutative join-associative join-absorbing join-commutative non empty LattStr for x,y,z being Element of L st x [= z & y [= z & for z9 being Element of L st x [= z9 & y [= z9 holds z [= z9 holds z = x "\/" y;