:: Complete Lattices
:: by Grzegorz Bancerek
::
:: Copyright (c) 1992-2021 Association of Mizar Users

deffunc H1( LattStr ) -> set = the carrier of $1; deffunc H2( LattStr ) -> Element of bool [:[: the carrier of$1, the carrier of $1:], the carrier of$1:] = the L_join of $1; deffunc H3( LattStr ) -> Element of bool [:[: the carrier of$1, the carrier of $1:], the carrier of$1:] = the L_meet of $1; definition let X be set ; func BooleLatt X -> strict LattStr means :Def1: :: 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 ) ) ); existence ex b1 being strict LattStr st ( the carrier of b1 = bool X & ( for Y, Z being Subset of X holds ( the L_join of b1 . (Y,Z) = Y \/ Z & the L_meet of b1 . (Y,Z) = Y /\ Z ) ) ) proof end; uniqueness for b1, b2 being strict LattStr st the carrier of b1 = bool X & ( for Y, Z being Subset of X holds ( the L_join of b1 . (Y,Z) = Y \/ Z & the L_meet of b1 . (Y,Z) = Y /\ Z ) ) & the carrier of b2 = bool X & ( for Y, Z being Subset of X holds ( the L_join of b2 . (Y,Z) = Y \/ Z & the L_meet of b2 . (Y,Z) = Y /\ Z ) ) holds b1 = b2 proof end; end; :: deftheorem Def1 defines BooleLatt LATTICE3:def 1 : for X being set for b2 being strict LattStr holds ( b2 = BooleLatt X iff ( the carrier of b2 = bool X & ( for Y, Z being Subset of X holds ( the L_join of b2 . (Y,Z) = Y \/ Z & the L_meet of b2 . (Y,Z) = Y /\ Z ) ) ) ); registration let X be set ; cluster BooleLatt X -> non empty strict ; coherence not BooleLatt X is empty proof end; end; registration let X be set ; let x, y be Element of (); let x9, y9 be set ; identify x "\/" y with x9 \/ y9 when x = x9, y = y9; compatibility ( x = x9 & y = y9 implies x "\/" y = x9 \/ y9 ) proof end; identify x "/\" y with x9 /\ y9 when x = x9, y = y9; compatibility ( x = x9 & y = y9 implies x "/\" y = x9 /\ y9 ) proof end; end; theorem Th1: :: LATTICE3:1 for X being set for x, y being Element of () holds ( x "\/" y = x \/ y & x "/\" y = x /\ y ) ; theorem Th2: :: LATTICE3:2 for X being set for x, y being Element of () holds ( x [= y iff x c= y ) by ; registration let X be set ; coherence proof end; end; theorem Th3: :: LATTICE3:3 for X being set holds ( BooleLatt X is lower-bounded & Bottom () = {} ) proof end; theorem Th4: :: LATTICE3:4 for X being set holds ( BooleLatt X is upper-bounded & Top () = X ) proof end; registration let X be set ; coherence proof end; end; theorem :: LATTICE3:5 for X being set for x being Element of () holds x  = X \ x proof end; definition let L be Lattice; :: original: LattRel redefine func LattRel L -> Order of the carrier of L; coherence LattRel L is Order of the carrier of L proof end; end; definition let L be Lattice; func LattPOSet L -> strict Poset equals :: LATTICE3:def 2 RelStr(# the carrier of L,() #); correctness coherence RelStr(# the carrier of L,() #) is strict Poset ; ; end; :: deftheorem defines LattPOSet LATTICE3:def 2 : for L being Lattice holds LattPOSet L = RelStr(# the carrier of L,() #); registration let L be Lattice; cluster LattPOSet L -> non empty strict ; coherence not LattPOSet L is empty ; end; theorem Th6: :: LATTICE3:6 for L1, L2 being Lattice st LattPOSet L1 = LattPOSet L2 holds LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) proof end; definition let L be Lattice; let p be Element of L; func p % -> Element of () equals :: LATTICE3:def 3 p; correctness coherence p is Element of () ; ; end; :: deftheorem defines % LATTICE3:def 3 : for L being Lattice for p being Element of L holds p % = p; definition let L be Lattice; let p be Element of (); func % p -> Element of L equals :: LATTICE3:def 4 p; correctness coherence p is Element of L ; ; end; :: deftheorem defines % LATTICE3:def 4 : for L being Lattice for p being Element of () holds % p = p; theorem Th7: :: LATTICE3:7 for L being Lattice for p, q being Element of L holds ( p [= q iff p % <= q % ) by FILTER_1:31; definition let X be set ; let O be Order of X; :: original: ~ redefine func O ~ -> Order of X; coherence O ~ is Order of X proof end; end; definition let A be RelStr ; func A ~ -> strict RelStr equals :: LATTICE3:def 5 RelStr(# the carrier of A,( the InternalRel of A ~) #); correctness coherence RelStr(# the carrier of A,( the InternalRel of A ~) #) is strict RelStr ; ; end; :: deftheorem defines ~ LATTICE3:def 5 : for A being RelStr holds A ~ = RelStr(# the carrier of A,( the InternalRel of A ~) #); registration let A be Poset; coherence ( A ~ is reflexive & A ~ is transitive & A ~ is antisymmetric ) proof end; end; registration let A be non empty RelStr ; cluster A ~ -> non empty strict ; coherence not A ~ is empty ; end; theorem :: LATTICE3:8 for A being RelStr holds (A ~) ~ = RelStr(# the carrier of A, the InternalRel of A #) ; definition let A be RelStr ; let a be Element of A; func a ~ -> Element of (A ~) equals :: LATTICE3:def 6 a; correctness coherence a is Element of (A ~) ; ; end; :: deftheorem defines ~ LATTICE3:def 6 : for A being RelStr for a being Element of A holds a ~ = a; definition let A be RelStr ; let a be Element of (A ~); func ~ a -> Element of A equals :: LATTICE3:def 7 a; correctness coherence a is Element of A ; ; end; :: deftheorem defines ~ LATTICE3:def 7 : for A being RelStr for a being Element of (A ~) holds ~ a = a; theorem Th9: :: LATTICE3:9 for A being RelStr for a, b being Element of A holds ( a <= b iff b ~ <= a ~ ) by RELAT_1:def 7; definition let A be RelStr ; let X be set ; let 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; :: deftheorem defines is_<=_than LATTICE3:def 8 : for A being RelStr for X being set for a being Element of A holds ( a is_<=_than X iff for b being Element of A st b in X holds a <= b ); :: deftheorem defines is_<=_than LATTICE3:def 9 : for A being RelStr for X being set for a being Element of A holds ( X is_<=_than a iff for b being Element of A st b in X holds b <= a ); notation let A be RelStr ; let X be set ; let 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 :Def10: :: 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 :Def11: :: 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; :: deftheorem Def10 defines with_suprema LATTICE3:def 10 : for IT being RelStr holds ( IT is with_suprema iff 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 ) ) ); :: deftheorem Def11 defines with_infima LATTICE3:def 11 : for IT being RelStr holds ( IT is with_infima iff 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 ) ) ); registration cluster with_suprema -> non empty for RelStr ; coherence for b1 being RelStr st b1 is with_suprema holds not b1 is empty proof end; cluster with_infima -> non empty for RelStr ; coherence for b1 being RelStr st b1 is with_infima holds not b1 is empty proof end; end; theorem :: LATTICE3:10 for A being RelStr holds ( A is with_suprema iff A ~ is with_infima ) proof end; theorem :: LATTICE3:11 for L being Lattice holds ( LattPOSet L is with_suprema & LattPOSet L is with_infima ) proof end; definition let IT be RelStr ; attr IT is complete means :Def12: :: 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; :: deftheorem Def12 defines complete LATTICE3:def 12 : for IT being RelStr holds ( IT is complete iff 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 ) ) ); registration existence ex b1 being Poset st ( b1 is strict & b1 is complete & not b1 is empty ) proof end; end; theorem Th12: :: LATTICE3:12 for A being non empty RelStr st A is complete holds ( A is with_suprema & A is with_infima ) proof end; registration existence ex b1 being Poset st ( b1 is complete & b1 is with_suprema & b1 is with_infima & b1 is strict & not b1 is empty ) proof end; end; definition let A be RelStr ; assume A1: A is antisymmetric ; let a, b be Element of A; assume A2: 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 :Def13: :: LATTICE3:def 13 ( a <= it & b <= it & ( for c being Element of A st a <= c & b <= c holds it <= c ) ); existence ex b1 being Element of A st ( a <= b1 & b <= b1 & ( for c being Element of A st a <= c & b <= c holds b1 <= c ) ) by A2; uniqueness for b1, b2 being Element of A st a <= b1 & b <= b1 & ( for c being Element of A st a <= c & b <= c holds b1 <= c ) & a <= b2 & b <= b2 & ( for c being Element of A st a <= c & b <= c holds b2 <= c ) holds b1 = b2 proof end; end; :: deftheorem Def13 defines "\/" LATTICE3:def 13 : for A being RelStr st A is antisymmetric holds for a, b being Element of A st 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 ) ) holds for b4 being Element of A holds ( b4 = a "\/" b iff ( a <= b4 & b <= b4 & ( for c being Element of A st a <= c & b <= c holds b4 <= c ) ) ); Lm1: now :: thesis: for A being non empty antisymmetric with_suprema RelStr for a, b, c being Element of A holds ( c = a "\/" b iff ( a <= c & b <= c & ( for d being Element of A st a <= d & b <= d holds c <= d ) ) ) let A be non empty antisymmetric with_suprema RelStr ; :: thesis: for a, b, c being Element of A holds ( c = a "\/" b iff ( a <= c & b <= c & ( for d being Element of A st a <= d & b <= d holds c <= d ) ) ) let a, b be Element of A; :: thesis: for c being Element of A holds ( c = a "\/" b iff ( a <= c & b <= c & ( for d being Element of A st a <= d & b <= d holds c <= d ) ) ) 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 ) ) by Def10; hence for c being Element of A holds ( c = a "\/" b iff ( a <= c & b <= c & ( for d being Element of A st a <= d & b <= d holds c <= d ) ) ) by Def13; :: thesis: verum end; definition let A be RelStr ; assume A1: A is antisymmetric ; let a, b be Element of A; assume A2: 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 :Def14: :: LATTICE3:def 14 ( it <= a & it <= b & ( for c being Element of A st c <= a & c <= b holds c <= it ) ); existence ex b1 being Element of A st ( b1 <= a & b1 <= b & ( for c being Element of A st c <= a & c <= b holds c <= b1 ) ) by A2; uniqueness for b1, b2 being Element of A st b1 <= a & b1 <= b & ( for c being Element of A st c <= a & c <= b holds c <= b1 ) & b2 <= a & b2 <= b & ( for c being Element of A st c <= a & c <= b holds c <= b2 ) holds b1 = b2 proof end; end; :: deftheorem Def14 defines "/\" LATTICE3:def 14 : for A being RelStr st A is antisymmetric holds for a, b being Element of A st 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 ) ) holds for b4 being Element of A holds ( b4 = a "/\" b iff ( b4 <= a & b4 <= b & ( for c being Element of A st c <= a & c <= b holds c <= b4 ) ) ); Lm2: now :: thesis: for A being non empty antisymmetric with_infima RelStr for a, b, c being Element of A holds ( c = a "/\" b iff ( a >= c & b >= c & ( for d being Element of A st a >= d & b >= d holds c >= d ) ) ) let A be non empty antisymmetric with_infima RelStr ; :: thesis: for a, b, c being Element of A holds ( c = a "/\" b iff ( a >= c & b >= c & ( for d being Element of A st a >= d & b >= d holds c >= d ) ) ) let a, b be Element of A; :: thesis: for c being Element of A holds ( c = a "/\" b iff ( a >= c & b >= c & ( for d being Element of A st a >= d & b >= d holds c >= d ) ) ) 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 ) ) by Def11; hence for c being Element of A holds ( c = a "/\" b iff ( a >= c & b >= c & ( for d being Element of A st a >= d & b >= d holds c >= d ) ) ) by Def14; :: thesis: verum end; theorem Th13: :: LATTICE3:13 for V being antisymmetric with_suprema RelStr for u1, u2 being Element of V holds u1 "\/" u2 = u2 "\/" u1 proof end; theorem Th14: :: LATTICE3:14 for V being antisymmetric with_suprema RelStr for u1, u2, u3 being Element of V st V is transitive holds (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3) proof end; theorem Th15: :: LATTICE3:15 for N being antisymmetric with_infima RelStr for n1, n2 being Element of N holds n1 "/\" n2 = n2 "/\" n1 proof end; theorem Th16: :: LATTICE3:16 for N being antisymmetric with_infima RelStr for n1, n2, n3 being Element of N st N is transitive holds (n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3) proof end; definition let L be antisymmetric with_infima RelStr ; let x, y be Element of L; :: original: "/\" redefine func x "/\" y -> Element of L; commutativity for x, y being Element of L holds x "/\" y = y "/\" x by Th15; end; definition let L be antisymmetric with_suprema RelStr ; let x, y be Element of L; :: original: "\/" redefine func x "\/" y -> Element of L; commutativity for x, y being Element of L holds x "\/" y = y "\/" x by Th13; end; theorem Th17: :: LATTICE3:17 for K being reflexive antisymmetric with_suprema with_infima RelStr for k1, k2 being Element of K holds (k1 "/\" k2) "\/" k2 = k2 proof end; theorem Th18: :: LATTICE3:18 for K being reflexive antisymmetric with_suprema with_infima RelStr for k1, k2 being Element of K holds k1 "/\" (k1 "\/" k2) = k1 proof end; theorem Th19: :: LATTICE3:19 for A being with_suprema with_infima Poset ex L being strict Lattice st RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet L proof end; definition let A be RelStr ; assume A1: A is with_suprema with_infima Poset ; func latt A -> strict Lattice means :Def15: :: LATTICE3:def 15 RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet it; existence ex b1 being strict Lattice st RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet b1 by ; uniqueness for b1, b2 being strict Lattice st RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet b1 & RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet b2 holds b1 = b2 by Th6; end; :: deftheorem Def15 defines latt LATTICE3:def 15 : for A being RelStr st A is with_suprema with_infima Poset holds for b2 being strict Lattice holds ( b2 = latt A iff RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet b2 ); theorem :: LATTICE3:20 for L being Lattice holds ( () ~ = LattRel (L .:) & () ~ = LattPOSet (L .:) ) proof end; definition let L be non empty LattStr ; let p be Element of L; let 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; :: deftheorem defines is_less_than LATTICE3:def 16 : for L being non empty LattStr for p being Element of L for X being set holds ( p is_less_than X iff for q being Element of L st q in X holds p [= q ); :: deftheorem defines is_less_than LATTICE3:def 17 : for L being non empty LattStr for p being Element of L for X being set holds ( X is_less_than p iff for q being Element of L st q in X holds q [= p ); notation let L be non empty LattStr ; let p be Element of L; let 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 for p, q, r being Element of L holds ( p is_less_than {q,r} iff p [= q "/\" r ) proof end; theorem :: LATTICE3:22 for L being Lattice for p, q, r being Element of L holds ( p is_greater_than {q,r} iff q "\/" r [= p ) proof end; definition let IT be non empty LattStr ; attr IT is complete means :Def18: :: 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 being set 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 being set 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; :: deftheorem Def18 defines complete LATTICE3:def 18 : for IT being non empty LattStr holds ( IT is complete iff 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 ) ) ); :: deftheorem defines \/-distributive LATTICE3:def 19 : for IT being non empty LattStr holds ( IT is \/-distributive iff for X being set 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 ); :: deftheorem defines /\-distributive LATTICE3:def 20 : for IT being non empty LattStr holds ( IT is /\-distributive iff for X being set 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 ); theorem :: LATTICE3:23 for X being set for B being B_Lattice for 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  ) proof end; theorem Th24: :: LATTICE3:24 for X being set for B being B_Lattice for 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 ` ) proof end; theorem Th25: :: LATTICE3:25 for X being set holds BooleLatt X is complete proof end; registration let X be set ; coherence by Th25; end; theorem Th26: :: LATTICE3:26 for X being set holds BooleLatt X is \/-distributive proof end; theorem Th27: :: LATTICE3:27 for X being set holds BooleLatt X is /\-distributive proof end; registration existence ex b1 being Lattice st ( b1 is complete & b1 is \/-distributive & b1 is /\-distributive & b1 is strict ) proof end; end; theorem Th28: :: LATTICE3:28 for X being set for L being Lattice for p being Element of L holds ( p is_less_than X iff p % is_<=_than X ) proof end; theorem :: LATTICE3:29 for X being set for L being Lattice for p9 being Element of () holds ( p9 is_<=_than X iff % p9 is_less_than X ) proof end; theorem Th30: :: LATTICE3:30 for X being set for L being Lattice for p being Element of L holds ( X is_less_than p iff X is_<=_than p % ) proof end; theorem Th31: :: LATTICE3:31 for X being set for L being Lattice for p9 being Element of () holds ( X is_<=_than p9 iff X is_less_than % p9 ) proof end; registration let A be non empty complete Poset; coherence latt A is complete proof end; end; definition let L be non empty LattStr ; assume A1: L is complete Lattice ; let X be set ; func "\/" (X,L) -> Element of L means :Def21: :: LATTICE3:def 21 ( X is_less_than it & ( for r being Element of L st X is_less_than r holds it [= r ) ); existence ex b1 being Element of L st ( X is_less_than b1 & ( for r being Element of L st X is_less_than r holds b1 [= r ) ) by ; uniqueness for b1, b2 being Element of L st X is_less_than b1 & ( for r being Element of L st X is_less_than r holds b1 [= r ) & X is_less_than b2 & ( for r being Element of L st X is_less_than r holds b2 [= r ) holds b1 = b2 proof end; end; :: deftheorem Def21 defines "\/" LATTICE3:def 21 : for L being non empty LattStr st L is complete Lattice holds for X being set for b3 being Element of L holds ( b3 = "\/" (X,L) iff ( X is_less_than b3 & ( for r being Element of L st X is_less_than r holds b3 [= r ) ) ); definition let L be non empty LattStr ; let 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); correctness coherence "\/" ( { p where p is Element of L : p is_less_than X } ,L) is Element of L ; ; end; :: deftheorem defines "/\" LATTICE3:def 22 : for L being non empty LattStr for X being set holds "/\" (X,L) = "\/" ( { p where p is Element of L : p is_less_than X } ,L); notation let L be non empty LattStr ; let X be Subset of L; synonym "\/" X for "\/" (X,L); synonym "/\" X for "/\" (X,L); end; theorem Th32: :: LATTICE3:32 for C being complete Lattice for a being Element of C for X being set holds "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) [= a "/\" ("\/" (X,C)) proof end; theorem Th33: :: LATTICE3:33 for C being complete Lattice holds ( C is \/-distributive iff for X being set for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) ) proof end; theorem Th34: :: LATTICE3:34 for C being complete Lattice for a being Element of C for X being set holds ( a = "/\" (X,C) iff ( a is_less_than X & ( for b being Element of C st b is_less_than X holds b [= a ) ) ) proof end; theorem Th35: :: LATTICE3:35 for C being complete Lattice for a being Element of C for X being set holds a "\/" ("/\" (X,C)) [= "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) proof end; theorem Th36: :: LATTICE3:36 for C being complete Lattice holds ( C is /\-distributive iff for X being set for a being Element of C holds "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) [= a "\/" ("/\" (X,C)) ) proof end; theorem :: LATTICE3:37 for C being complete Lattice for X being set holds "\/" (X,C) = "/\" ( { a where a is Element of C : a is_greater_than X } ,C) proof end; theorem Th38: :: LATTICE3:38 for C being complete Lattice for a being Element of C for X being set st a in X holds ( a [= "\/" (X,C) & "/\" (X,C) [= a ) proof end; theorem Th39: :: LATTICE3:39 for C being complete Lattice for a being Element of C for X being set st a is_less_than X holds a [= "/\" (X,C) proof end; theorem Th40: :: LATTICE3:40 for C being complete Lattice for a being Element of C for X being set st a in X & X is_less_than a holds "\/" (X,C) = a proof end; theorem Th41: :: LATTICE3:41 for C being complete Lattice for a being Element of C for X being set st a in X & a is_less_than X holds "/\" (X,C) = a proof end; theorem :: LATTICE3:42 for C being complete Lattice for a being Element of C holds ( "\/" {a} = a & "/\" {a} = a ) proof end; theorem :: LATTICE3:43 for C being complete Lattice for a, b being Element of C holds ( a "\/" b = "\/" {a,b} & a "/\" b = "/\" {a,b} ) proof end; theorem :: LATTICE3:44 for C being complete Lattice for a being Element of C holds ( a = "\/" ( { b where b is Element of C : b [= a } ,C) & a = "/\" ( { c where c is Element of C : a [= c } ,C) ) proof end; theorem Th45: :: LATTICE3:45 for C being complete Lattice for X, Y being set st X c= Y holds ( "\/" (X,C) [= "\/" (Y,C) & "/\" (Y,C) [= "/\" (X,C) ) proof end; theorem Th46: :: LATTICE3:46 for C being complete Lattice for X being set holds ( "\/" (X,C) = "\/" ( { a where a is Element of C : ex b being Element of C st ( a [= b & b in X ) } ,C) & "/\" (X,C) = "/\" ( { b where b is Element of C : ex a being Element of C st ( a [= b & a in X ) } ,C) ) proof end; theorem :: LATTICE3:47 for C being complete Lattice for X, Y being set st ( for a being Element of C st a in X holds ex b being Element of C st ( a [= b & b in Y ) ) holds "\/" (X,C) [= "\/" (Y,C) proof end; theorem :: LATTICE3:48 for C being complete Lattice for X being set st X c= bool the carrier of C holds "\/" ((),C) = "\/" ( { ("\/" Y) where Y is Subset of C : Y in X } ,C) proof end; theorem :: LATTICE3:49 for C being complete Lattice holds ( C is 0_Lattice & Bottom C = "\/" ({},C) ) proof end; theorem :: LATTICE3:50 for C being complete Lattice holds ( C is 1_Lattice & Top C = "\/" ( the carrier of C,C) ) proof end; theorem Th51: :: LATTICE3:51 for C being complete Lattice for a, b being Element of C st C is I_Lattice holds a => b = "\/" ( { c where c is Element of C : a "/\" c [= b } ,C) proof end; theorem :: LATTICE3:52 for C being complete Lattice st C is I_Lattice holds C is \/-distributive proof end; theorem :: LATTICE3:53 for X being set for D being complete \/-distributive Lattice for 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) ) proof end; theorem :: LATTICE3:54 for X being set for D being complete /\-distributive Lattice for 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) ) proof end; scheme :: LATTICE3:sch 1 SingleFraenkel{ F1() -> set , F2() -> non empty set , P1[ set ] } : { F1() where a is Element of F2() : P1[a] } = {F1()} provided A1: ex a being Element of F2() st P1[a] proof end; scheme :: LATTICE3:sch 2 FuncFraenkel{ F1() -> non empty set , F2() -> non empty set , F3( set ) -> Element of F2(), F4() -> Function, P1[ set ] } : F4() .: { F3(x) where x is Element of F1() : P1[x] } = { (F4() . F3(x)) where x is Element of F1() : P1[x] } provided A1: F2() c= dom F4() proof end; Lm3: now :: thesis: for D being non empty set for 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 . () ) holds ex L being strict Lattice st ( H1(L) = D & ( for X being Subset of L holds "\/" X = f . X ) ) let D be non empty set ; :: thesis: for 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 . () ) holds ex L being strict Lattice st ( H1(L) = D & ( for X being Subset of L holds "\/" X = f . X ) ) let f be Function of (bool D),D; :: thesis: ( ( for a being Element of D holds f . {a} = a ) & ( for X being Subset-Family of D holds f . (f .: X) = f . () ) implies ex L being strict Lattice st ( H1(L) = D & ( for X being Subset of L holds "\/" X = f . X ) ) ) assume that A1: for a being Element of D holds f . {a} = a and A2: for X being Subset-Family of D holds f . (f .: X) = f . () ; :: thesis: ex L being strict Lattice st ( H1(L) = D & ( for X being Subset of L holds "\/" X = f . X ) ) defpred S1[ object , object ] means f . {$1,$2} =$2;
consider R being Relation of D such that
A3: for x, y being object holds
( [x,y] in R iff ( x in D & y in D & S1[x,y] ) ) from A4: dom f = bool D by FUNCT_2:def 1;
A5: now :: thesis: for x, y being Subset of D holds f . {(f . x),(f . y)} = f . (x \/ y)
let x, y be Subset of D; :: thesis: f . {(f . x),(f . y)} = f . (x \/ y)
thus f . {(f . x),(f . y)} = f . (f .: {x,y}) by
.= f . (union {x,y}) by A2
.= f . (x \/ y) by ZFMISC_1:75 ; :: thesis: verum
end;
A6: for x, y being Element of D
for X being Subset of D st y in X holds
f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X }
proof
let x, y be Element of D; :: thesis: for X being Subset of D st y in X holds
f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X }

let X be Subset of D; :: thesis: ( y in X implies f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X } )
assume A7: y in X ; :: thesis: f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X }
set Y = { {t,x} where t is Element of D : t in X } ;
A8: X \/ {x} = union { {t,x} where t is Element of D : t in X }
proof
thus X \/ {x} c= union { {t,x} where t is Element of D : t in X } :: according to XBOOLE_0:def 10 :: thesis: union { {t,x} where t is Element of D : t in X } c= X \/ {x}
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in X \/ {x} or s in union { {t,x} where t is Element of D : t in X } )
assume s in X \/ {x} ; :: thesis: s in union { {t,x} where t is Element of D : t in X }
then ( ( s in X & X c= D ) or s in {x} ) by XBOOLE_0:def 3;
then ( ( s in X & s is Element of D ) or s = x ) by TARSKI:def 1;
then ( ( s in {s,x} & {s,x} in { {t,x} where t is Element of D : t in X } ) or ( s in {y,x} & {y,x} in { {t,x} where t is Element of D : t in X } ) ) by ;
hence s in union { {t,x} where t is Element of D : t in X } by TARSKI:def 4; :: thesis: verum
end;
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in union { {t,x} where t is Element of D : t in X } or s in X \/ {x} )
assume s in union { {t,x} where t is Element of D : t in X } ; :: thesis: s in X \/ {x}
then consider Z being set such that
A9: s in Z and
A10: Z in { {t,x} where t is Element of D : t in X } by TARSKI:def 4;
consider t being Element of D such that
A11: Z = {t,x} and
A12: t in X by A10;
( s = t or ( s = x & x in {x} ) ) by ;
hence s in X \/ {x} by ; :: thesis: verum
end;
{ {t,x} where t is Element of D : t in X } c= bool D
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in { {t,x} where t is Element of D : t in X } or s in bool D )
reconsider ss = s as set by TARSKI:1;
assume s in { {t,x} where t is Element of D : t in X } ; :: thesis: s in bool D
then ss c= X \/ {x} by ;
then ss c= D by XBOOLE_1:1;
hence s in bool D ; :: thesis: verum
end;
then reconsider Y = { {t,x} where t is Element of D : t in X } as Subset-Family of D ;
defpred S2[ set ] means $1 in X; deffunc H4( Element of D) -> Element of bool D = {$1,x};
A13: bool D c= dom f by FUNCT_2:def 1;
f .: { H4(t) where t is Element of D : S2[t] } = { (f . H4(t)) where t is Element of D : S2[t] } from then f . () = f . { (f . {t,x}) where t is Element of D : t in X } by A2;
hence f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X } by A8; :: thesis: verum
end;
A14: R is_reflexive_in D
proof
let x be object ; :: according to RELAT_2:def 1 :: thesis: ( not x in D or [x,x] in R )
assume A15: x in D ; :: thesis: [x,x] in R
then x = f . {x} by A1
.= f . {x,x} by ENUMSET1:29 ;
hence [x,x] in R by ; :: thesis: verum
end;
A16: R is_antisymmetric_in D
proof
let x, y be object ; :: according to RELAT_2:def 4 :: thesis: ( not x in D or not y in D or not [x,y] in R or not [y,x] in R or x = y )
assume that
x in D and
y in D and
A17: [x,y] in R and
A18: [y,x] in R ; :: thesis: x = y
f . {x,y} = y by ;
hence x = y by ; :: thesis: verum
end;
A19: R is_transitive_in D
proof
let x, y, z be object ; :: according to RELAT_2:def 8 :: thesis: ( not x in D or not y in D or not z in D or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume that
A20: x in D and
A21: y in D and
A22: z in D and
A23: [x,y] in R and
A24: [y,z] in R ; :: thesis: [x,z] in R
reconsider a = x, b = y, c = z as Element of D by ;
A25: f . {x,y} = y by ;
A26: f . {y,z} = z by ;
then f . {a,c} = f . {(f . {a}),(f . {b,c})} by A1
.= f . ({a} \/ {b,c}) by A5
.= f . {a,b,c} by ENUMSET1:2
.= f . ({a,b} \/ {c}) by ENUMSET1:3
.= f . {(f . {a,b}),(f . {c})} by A5
.= c by A1, A25, A26 ;
hence [x,z] in R by A3; :: thesis: verum
end;
A27: dom R = D by ;
field R = D by ;
then reconsider R = R as Order of D by ;
set A = RelStr(# D,R #);
RelStr(# D,R #) is complete
proof
let X be set ; :: according to LATTICE3:def 12 :: thesis: ex a being Element of RelStr(# D,R #) st
( X is_<=_than a & ( for b being Element of RelStr(# D,R #) st X is_<=_than b holds
a <= b ) )

reconsider Y = X /\ D as Subset of D by XBOOLE_1:17;
reconsider a = f . Y as Element of RelStr(# D,R #) ;
take a ; :: thesis: ( X is_<=_than a & ( for b being Element of RelStr(# D,R #) st X is_<=_than b holds
a <= b ) )

thus X is_<=_than a :: thesis: for b being Element of RelStr(# D,R #) st X is_<=_than b holds
a <= b
proof
let b be Element of RelStr(# D,R #); :: according to LATTICE3:def 9 :: thesis: ( b in X implies b <= a )
assume b in X ; :: thesis: b <= a
then b in Y by XBOOLE_0:def 4;
then {b} \/ Y = Y by ZFMISC_1:40;
then a = f . {(f . {b}),a} by A5
.= f . {b,a} by A1 ;
hence [b,a] in the InternalRel of RelStr(# D,R #) by A3; :: according to ORDERS_2:def 5 :: thesis: verum
end;
let b be Element of RelStr(# D,R #); :: thesis: ( X is_<=_than b implies a <= b )
assume A28: X is_<=_than b ; :: thesis: a <= b
A29: f . {a,b} = f . {a,(f . {b})} by A1
.= f . (Y \/ {b}) by A5 ;
now :: thesis: f . {a,b} = b
per cases ( Y <> {} or Y = {} ) ;
suppose A30: Y <> {} ; :: thesis: f . {a,b} = b
set s = the Element of Y;
reconsider s = the Element of Y as Element of D by ;
deffunc H4( Element of D) -> set = f . {$1,b}; deffunc H5( Element of D) -> Element of RelStr(# D,R #) = b; defpred S2[ set ] means$1 in Y;
A31: for t being Element of D st S2[t] holds
H4(t) = H5(t)
proof
let t be Element of D; :: thesis: ( S2[t] implies H4(t) = H5(t) )
reconsider s = t as Element of RelStr(# D,R #) ;
reconsider y = b as Element of D ;
assume t in Y ; :: thesis: H4(t) = H5(t)
then t in X by XBOOLE_0:def 4;
then s <= b by A28;
then [t,y] in R ;
hence H4(t) = H5(t) by A3; :: thesis: verum
end;
A32: s in Y by A30;
then A33: ex t being Element of D st S2[t] ;
{ H4(t) where t is Element of D : S2[t] } = { H5(t) where t is Element of D : S2[t] } from
.= { b where t is Element of D : S2[t] }
.= {b} from ;
hence f . {a,b} = f . {b} by A6, A29, A32
.= b by A1 ;
:: thesis: verum
end;
suppose Y = {} ; :: thesis: f . {a,b} = b
hence f . {a,b} = b by ; :: thesis: verum
end;
end;
end;
hence [a,b] in the InternalRel of RelStr(# D,R #) by A3; :: according to ORDERS_2:def 5 :: thesis: verum
end;
then reconsider A = RelStr(# D,R #) as non empty strict complete Poset ;
take L = latt A; :: thesis: ( H1(L) = D & ( for X being Subset of L holds "\/" X = f . X ) )
A34: ( A is with_suprema & A is with_infima ) by Th12;
then A35: A = LattPOSet L by Def15;
hence H1(L) = D ; :: thesis: for X being Subset of L holds "\/" X = f . X
let X be Subset of L; :: thesis: "\/" X = f . X
reconsider Y = X as Subset of D by A35;
reconsider a = f . Y as Element of () by ;
set p = % a;
X is_<=_than a
proof
let b be Element of (); :: according to LATTICE3:def 9 :: thesis: ( b in X implies b <= a )
reconsider y = b as Element of D by ;
assume b in X ; :: thesis: b <= a
then A36: X = {b} \/ X by ZFMISC_1:40;
f . {y,(f . Y)} = f . {(f . {y}),(f . Y)} by A1
.= a by ;
hence [b,a] in the InternalRel of () by ; :: according to ORDERS_2:def 5 :: thesis: verum
end;
then A37: X is_less_than % a by Th31;
now :: thesis: for q being Element of L st X is_less_than q holds
% a [= q
let q be Element of L; :: thesis: ( X is_less_than q implies % a [= q )
reconsider y = q as Element of D by A35;
reconsider b = y as Element of () ;
assume X is_less_than q ; :: thesis: % a [= q
then A38: X is_<=_than q % by Th30;
A39: f . {(f . Y),b} = f . {(f . Y),(f . {y})} by A1
.= f . (Y \/ {b}) by A5 ;
now :: thesis: f . {a,b} = b
per cases ( Y <> {} or Y = {} ) ;
suppose A40: Y <> {} ; :: thesis: f . {a,b} = b
set s = the Element of Y;
reconsider s = the Element of Y as Element of D by ;
deffunc H4( Element of D) -> set = f . {$1,b}; deffunc H5( Element of D) -> Element of () = b; defpred S2[ set ] means$1 in Y;
A41: for t being Element of D st S2[t] holds
H4(t) = H5(t)
proof
let t be Element of D; :: thesis: ( S2[t] implies H4(t) = H5(t) )
reconsider s = t as Element of () by ;
assume t in Y ; :: thesis: H4(t) = H5(t)
then s <= b by A38;
then [t,y] in R by A35;
hence H4(t) = H5(t) by A3; :: thesis: verum
end;
A42: s in Y by A40;
then A43: ex t being Element of D st S2[t] ;
{ H4(t) where t is Element of D : S2[t] } = { H5(t) where t is Element of D : S2[t] } from
.= { b where t is Element of D : S2[t] }
.= {b} from ;
hence f . {a,b} = f . {b} by A6, A39, A42
.= b by A1 ;
:: thesis: verum
end;
suppose Y = {} ; :: thesis: f . {a,b} = b
hence f . {a,b} = b by ; :: thesis: verum
end;
end;
end;
then [a,b] in the InternalRel of () by ;
then A44: a <= b ;
A45: (% a) % = % a ;
q % = b ;
hence % a [= q by ; :: thesis: verum
end;
hence "\/" X = f . X by ; :: thesis: verum
end;

theorem :: LATTICE3:55
for D being non empty set
for 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 . () ) holds
ex L being strict complete Lattice st
( the carrier of L = D & ( for X being Subset of L holds "\/" X = f . X ) ) by Lm3;