:: Filters - Part I. Implicative Lattices
:: by Grzegorz Bancerek
::
:: Received July 3, 1990
:: Copyright (c) 1990-2017 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;