:: Complete Lattices
:: by Grzegorz Bancerek
::
:: Received May 13, 1992
:: Copyright (c) 1992-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, STRUCT_0, ZFMISC_1, SUBSET_1, FUNCT_1, XBOOLE_0,
BINOP_1, EQREL_1, PBOOLE, TARSKI, FILTER_1, ORDERS_1, RELAT_1, RELAT_2,
ORDERS_2, XXREAL_0, REWRITE1, FILTER_0, XBOOLEAN, SETFAM_1, LATTICE3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, DOMAIN_1, STRUCT_0,
FUNCT_1, FUNCT_2, BINOP_1, LATTICES, FILTER_0, LATTICE2, FILTER_1,
RELAT_1, RELAT_2, RELSET_1, ORDERS_1, ORDERS_2;
constructors BINOP_1, DOMAIN_1, ORDERS_2, LATTICE2, FILTER_1, RELSET_1,
FILTER_0;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, LATTICES, ORDERS_2,
LATTICE2, RELAT_2;
requirements SUBSET, BOOLE;
begin
definition
let X be set;
func BooleLatt X -> strict LattStr means
:: LATTICE3:def 1
the carrier of it = bool X & for Y,Z being Subset of X holds
(the L_join of it).(Y,Z) = Y \/ Z & (the L_meet of it).(Y,Z) = Y /\ Z;
end;
reserve X for set,
x,y,z for Element of BooleLatt X,
s for set;
registration
let X be set;
cluster BooleLatt X -> non empty;
end;
registration
let X;
let x,y;
let x9,y9 be set;
identify x "\/" y with x9 \/ y9 when x = x9, y = y9;
identify x "/\" y with x9 /\ y9 when x = x9, y = y9;
end;
theorem :: LATTICE3:1
x "\/" y = x \/ y & x "/\" y = x /\ y;
theorem :: LATTICE3:2
x [= y iff x c= y;
registration
let X;
cluster BooleLatt X -> Lattice-like;
end;
reserve y for Element of BooleLatt X;
theorem :: LATTICE3:3
BooleLatt X is lower-bounded & Bottom BooleLatt X = {};
theorem :: LATTICE3:4
BooleLatt X is upper-bounded & Top BooleLatt X = X;
registration
let X;
cluster BooleLatt X -> Boolean;
end;
theorem :: LATTICE3:5
for x being Element of BooleLatt X holds x` = X \ x;
begin :: Correspondence Between Lattices and Posets
definition
let L be Lattice;
redefine func LattRel L -> Order of the carrier of L;
end;
definition
let L be Lattice;
func LattPOSet L -> strict Poset equals
:: LATTICE3:def 2
RelStr(#the carrier of L, LattRel L#);
end;
registration
let L be Lattice;
cluster LattPOSet L -> non empty;
end;
theorem :: LATTICE3:6
for L1,L2 being Lattice st LattPOSet L1 = LattPOSet L2 holds
the LattStr of L1 = the LattStr of L2;
definition
let L be Lattice, p be Element of L;
func p% -> Element of LattPOSet L equals
:: LATTICE3:def 3
p;
end;
definition
let L be Lattice, p be Element of LattPOSet L;
func %p -> Element of L equals
:: LATTICE3:def 4
p;
end;
reserve L for Lattice,
p,q for Element of L;
theorem :: LATTICE3:7
p [= q iff p% <= q%;
definition
let X be set, O be Order of X;
redefine func O~ -> Order of X;
end;
definition
let A be RelStr;
func A~ -> strict RelStr equals
:: LATTICE3:def 5
RelStr(#the carrier of A, (the InternalRel of A)~#);
end;
registration
let A be Poset;
cluster A~ -> reflexive transitive antisymmetric;
end;
registration
let A be non empty RelStr;
cluster A~ -> non empty;
end;
reserve A for RelStr,
a,b,c for Element of A;
theorem :: LATTICE3:8
A~~ = the RelStr of A;
definition
let A be RelStr, a be Element of A;
func a~ -> Element of A~ equals
:: LATTICE3:def 6
a;
end;
definition
let A be RelStr, a be Element of A~;
func ~a -> Element of A equals
:: LATTICE3:def 7
a;
end;
theorem :: LATTICE3:9
a <= b iff b~ <= a~;
definition
let A be RelStr, X be set, a be Element of A;
pred a is_<=_than X means
:: LATTICE3:def 8
for b being Element of A st b in X holds a <= b;
pred X is_<=_than a means
:: LATTICE3:def 9
for b being Element of A st b in X holds b <= a;
end;
notation
let A be RelStr, X be set, a be Element of A;
synonym X is_>=_than a for a is_<=_than X; synonym a is_>=_than X for
X is_<=_than a;
end;
definition
let IT be RelStr;
attr IT is with_suprema means
:: LATTICE3:def 10
for x,y being Element of IT ex z being Element of IT st x <= z & y <= z &
for z9 being Element of IT st x <= z9 & y <= z9 holds z <= z9;
attr IT is with_infima means
:: LATTICE3:def 11
for x,y being Element of IT ex z being Element of IT st z <= x & z <= y &
for z9 being Element of IT st z9 <= x & z9 <= y holds z9 <= z;
end;
registration
cluster with_suprema -> non empty for RelStr;
cluster with_infima -> non empty for RelStr;
end;
theorem :: LATTICE3:10
A is with_suprema iff A~ is with_infima;
theorem :: LATTICE3:11
for L being Lattice holds LattPOSet L is with_suprema with_infima;
definition
let IT be RelStr;
attr IT is complete means
:: LATTICE3:def 12
for X being set ex a being Element of IT st X is_<=_than a &
for b being Element of IT st X is_<=_than b holds a <= b;
end;
registration
cluster strict complete non empty for Poset;
end;
reserve A for non empty RelStr,
a,b,c,c9 for Element of A;
theorem :: LATTICE3:12
A is complete implies A is with_suprema with_infima;
registration
cluster complete with_suprema with_infima strict non empty for Poset;
end;
definition
let A be RelStr such that
A is antisymmetric;
let a,b be Element of A such that
ex x being Element of A st a <= x & b <= x &
for c being Element of A st a <= c & b <= c holds x <= c;
func a"\/"b -> Element of A means
:: LATTICE3:def 13
a <= it & b <= it &
for c being Element of A st a <= c & b <= c holds it <= c;
end;
definition
let A be RelStr such that
A is antisymmetric;
let a,b be Element of A such that
ex x being Element of A st a >= x & b >= x &
for c being Element of A st a >= c & b >= c holds x >= c;
func a"/\"b -> Element of A means
:: LATTICE3:def 14
it <= a & it <= b &
for c being Element of A st c <= a & c <= b holds c <= it;
end;
reserve V for with_suprema antisymmetric RelStr,
u1,u2,u3,u4 for Element of V;
reserve N for with_infima antisymmetric RelStr,
n1,n2,n3,n4 for Element of N;
reserve K for with_suprema with_infima reflexive antisymmetric RelStr,
k1,k2,k3 for Element of K;
theorem :: LATTICE3:13
u1 "\/" u2 = u2 "\/" u1;
theorem :: LATTICE3:14
V is transitive implies (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3);
theorem :: LATTICE3:15
n1 "/\" n2 = n2 "/\" n1;
theorem :: LATTICE3:16
N is transitive implies (n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3);
definition
let L be with_infima antisymmetric RelStr, x, y be Element of L;
redefine func x "/\" y;
commutativity;
end;
definition
let L be with_suprema antisymmetric RelStr, x, y be Element of L;
redefine func x "\/" y;
commutativity;
end;
theorem :: LATTICE3:17
(k1 "/\" k2) "\/" k2 = k2;
theorem :: LATTICE3:18
k1 "/\" (k1 "\/" k2) = k1;
theorem :: LATTICE3:19
for A being with_suprema with_infima Poset
ex L being strict Lattice st the RelStr of A = LattPOSet L;
definition
let A be RelStr such that
A is with_suprema with_infima Poset;
func latt A -> strict Lattice means
:: LATTICE3:def 15
the RelStr of A = LattPOSet it;
end;
theorem :: LATTICE3:20
(LattRel L)~ = LattRel (L.:) & (LattPOSet L)~ = LattPOSet (L.:);
begin :: Complete Lattice
definition
let L be non empty LattStr, p be Element of L, X be set;
pred p is_less_than X means
:: LATTICE3:def 16
for q being Element of L st q in X holds p [= q;
pred X is_less_than p means
:: LATTICE3:def 17
for q being Element of L st q in X holds q [= p;
end;
notation
let L be non empty LattStr, p be Element of L, X be set;
synonym X is_greater_than p for p is_less_than X;
synonym p is_greater_than X for X is_less_than p;
end;
theorem :: LATTICE3:21
for L being Lattice, p,q,r being Element of L holds
p is_less_than {q,r} iff p [= q"/\"r;
theorem :: LATTICE3:22
for L being Lattice, p,q,r being Element of L holds
p is_greater_than {q,r} iff q"\/"r [= p;
definition
let IT be non empty LattStr;
attr IT is complete means
:: LATTICE3:def 18
for X being set ex p being Element of IT st X is_less_than p &
for r being Element of IT st X is_less_than r holds p [= r;
attr IT is \/-distributive means
:: LATTICE3:def 19
for X for a,b,c being Element of IT st X is_less_than a &
(for d being Element of IT st X is_less_than d holds a [= d)
& {b"/\"a9 where a9 is Element of IT: a9 in X} is_less_than c &
for d being Element of IT st
{b"/\"a9 where a9 is Element of IT: a9 in X} is_less_than d holds c [= d
holds b"/\"a [= c;
attr IT is /\-distributive means
:: LATTICE3:def 20
for X for a,b,c being Element of IT st X is_greater_than a &
(for d being Element of IT st X is_greater_than d holds d [= a)
& {b"\/"a9 where a9 is Element of IT: a9 in X} is_greater_than c &
for d being Element of IT st
{b"\/"a9 where a9 is Element of IT: a9 in X} is_greater_than d holds d [= c
holds c [= b"\/"a;
end;
theorem :: LATTICE3:23
for B being B_Lattice, a being Element of B holds
X is_less_than a iff {b` where b is Element of B: b in X} is_greater_than a`;
theorem :: LATTICE3:24
for B being B_Lattice, a being Element of B holds
X is_greater_than a iff {b` where b is Element of B: b in X} is_less_than a`;
theorem :: LATTICE3:25
BooleLatt X is complete;
registration
let X be set;
cluster BooleLatt X -> complete;
end;
theorem :: LATTICE3:26
BooleLatt X is \/-distributive;
theorem :: LATTICE3:27
BooleLatt X is /\-distributive;
registration
cluster complete \/-distributive /\-distributive strict for Lattice;
end;
reserve p9,q9 for Element of LattPOSet L;
theorem :: LATTICE3:28
p is_less_than X iff p% is_<=_than X;
theorem :: LATTICE3:29
p9 is_<=_than X iff %p9 is_less_than X;
theorem :: LATTICE3:30
X is_less_than p iff X is_<=_than p%;
theorem :: LATTICE3:31
X is_<=_than p9 iff X is_less_than %p9;
registration
let A be complete non empty Poset;
cluster latt A -> complete;
end;
definition
let L be non empty LattStr such that
L is complete Lattice;
let X be set;
func "\/"(X,L) -> Element of L means
:: LATTICE3:def 21
X is_less_than it &
for r being Element of L st X is_less_than r holds it [= r;
end;
definition
let L be non empty LattStr, X be set;
func "/\"(X,L) -> Element of L equals
:: LATTICE3:def 22
"\/"({p where p is Element of L: p is_less_than X},L);
end;
notation
let L be non empty LattStr, X be Subset of L;
synonym "\/" X for "\/"(X,L); synonym "/\" X for "/\"(X,L);
end;
reserve C for complete Lattice,
a,a9,b,b9,c,d for Element of C,
X,Y for set;
theorem :: LATTICE3:32
"\/"({a"/\"b: b in X}, C) [= a"/\""\/"(X,C);
theorem :: LATTICE3:33
C is \/-distributive iff for X, a holds a"/\""\/"(X,C) [= "\/"({a"/\"
b: b in X}, C);
theorem :: LATTICE3:34
a = "/\"(X,C) iff a is_less_than X & for b st b is_less_than X holds b [= a;
theorem :: LATTICE3:35
a"\/""/\"(X,C) [= "/\"({a"\/"b: b in X}, C);
theorem :: LATTICE3:36
C is /\-distributive iff for X, a holds "/\"({a"\/"b: b in X}, C) [= a"\/""/\"
(X,C);
theorem :: LATTICE3:37
"\/"(X,C) = "/\"({a: a is_greater_than X}, C);
theorem :: LATTICE3:38
a in X implies a [= "\/"(X,C) & "/\"(X,C) [= a;
theorem :: LATTICE3:39
a is_less_than X implies a [= "/\"(X,C);
theorem :: LATTICE3:40
a in X & X is_less_than a implies "\/"(X,C) = a;
theorem :: LATTICE3:41
a in X & a is_less_than X implies "/\"(X,C) = a;
theorem :: LATTICE3:42
"\/"{a} = a & "/\"{a} = a;
theorem :: LATTICE3:43
a"\/"b = "\/"{a,b} & a"/\"b = "/\"{a,b};
theorem :: LATTICE3:44
a = "\/"({b: b [= a}, C) & a = "/\"({c: a [= c}, C);
theorem :: LATTICE3:45
X c= Y implies "\/"(X,C) [= "\/"(Y,C) & "/\"(Y,C) [= "/\"(X,C);
theorem :: LATTICE3:46
"\/"(X,C) = "\/"({a: ex b st a [= b & b in X}, C) &
"/\"(X,C) = "/\"({b: ex a st a [= b & a in X}, C);
theorem :: LATTICE3:47
(for a st a in X ex b st a [= b & b in Y) implies "\/"(X,C) [= "\/"(Y, C );
theorem :: LATTICE3:48
X c= bool the carrier of C implies "\/"(union X, C) = "\/"({"\/"
Y where Y is Subset of C: Y in X}, C);
theorem :: LATTICE3:49
C is 0_Lattice & Bottom C = "\/"({},C);
theorem :: LATTICE3:50
C is 1_Lattice & Top C = "\/"(the carrier of C, C);
theorem :: LATTICE3:51
C is I_Lattice implies a => b = "\/"({c: a"/\"c [= b}, C);
theorem :: LATTICE3:52
C is I_Lattice implies C is \/-distributive;
theorem :: LATTICE3:53
for D being complete \/-distributive Lattice, a being Element of D holds
a "/\" "\/"(X,D) = "\/"({a"/\" b1 where b1 is Element of D: b1 in X}, D) &
"\/"(X,D) "/\" a = "\/"({b2"/\" a where b2 is Element of D: b2 in X}, D);
theorem :: LATTICE3:54
for D being complete /\-distributive Lattice, a being Element of D holds
a "\/" "/\"(X,D) = "/\"({a"\/"b1 where b1 is Element of D: b1 in X}, D) &
"/\"(X,D) "\/" a = "/\"({b2"\/" a where b2 is Element of D: b2 in X}, D);
scheme :: LATTICE3:sch 1
SingleFraenkel{A()->set, B()->non empty set, P[set]}:
{A() where a is Element of B(): P[a]} = {A()}
provided
ex a being Element of B() st P[a];
scheme :: LATTICE3:sch 2
FuncFraenkel{B()->non empty set, C()->non empty set,
A(set)->Element of C(),f()->Function, P[set]}:
f().:{A(x) where x is Element of B(): P[x]} =
{f().A(x) where x is Element of B(): P[x]}
provided
C() c= dom f();
theorem :: LATTICE3:55
for D being non empty set, f being Function of bool D, D st
(for a being Element of D holds f.{a} = a) &
for X being Subset-Family of D holds f.(f.:X) = f.(union X)
ex L being complete strict Lattice st the carrier of L = D &
for X being Subset of L holds "\/" X = f.X;