:: Complete Lattices :: by Grzegorz Bancerek :: :: Received May 13, 1992 :: Copyright (c) 1992-2018 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;