:: Complete Lattices
:: by Grzegorz Bancerek
::
:: Received May 13, 1992
:: 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 (BooleLatt X);
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 (BooleLatt X) holds
( x "\/" y = x \/ y & x "/\" y = x /\ y ) ;

theorem Th2: :: LATTICE3:2
for X being set
for x, y being Element of (BooleLatt X) holds
( x [= y iff x c= y ) by XBOOLE_1:7, XBOOLE_1:12;

registration
let X be set ;
cluster BooleLatt X -> strict Lattice-like ;
coherence
BooleLatt X is Lattice-like
proof end;
end;

theorem Th3: :: LATTICE3:3
for X being set holds
( BooleLatt X is lower-bounded & Bottom (BooleLatt X) = {} )
proof end;

theorem Th4: :: LATTICE3:4
for X being set holds
( BooleLatt X is upper-bounded & Top (BooleLatt X) = X )
proof end;

registration
let X be set ;
cluster BooleLatt X -> strict Boolean ;
coherence
BooleLatt X is Boolean
proof end;
end;

theorem :: LATTICE3:5
for X being set
for x being Element of (BooleLatt X) 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,(LattRel L) #);
correctness
coherence
RelStr(# the carrier of L,(LattRel L) #) is strict Poset;
;
end;

:: deftheorem defines LattPOSet LATTICE3:def 2 :
for L being Lattice holds LattPOSet L = RelStr(# the carrier of L,(LattRel 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 (LattPOSet L) equals :: LATTICE3:def 3
p;
correctness
coherence
p is Element of (LattPOSet L);
;
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 (LattPOSet L);
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 (LattPOSet L) 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;
cluster A ~ -> strict reflexive transitive antisymmetric ;
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
cluster non empty strict V69() reflexive transitive antisymmetric complete for RelStr ;
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
cluster non empty strict V69() reflexive transitive antisymmetric with_suprema with_infima complete for RelStr ;
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 A1, Th19;
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) ~ = LattRel (L .:) & (LattPOSet 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 ;
cluster BooleLatt X -> strict complete ;
coherence
BooleLatt X is complete 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
cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete \/-distributive /\-distributive for LattStr ;
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 (LattPOSet L) 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 (LattPOSet L) holds
( X is_<=_than p9 iff X is_less_than % p9 )
proof end;

registration
let A be non empty complete Poset;
cluster latt A -> strict complete ;
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 A1, Def18;
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
"\/" ((union X),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 . (union X) ) 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 . (union X) ) 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 . (union X) ) 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 . (union X) ; :: 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 RELSET_1:sch 1();
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 A4, FUNCT_1:60
.= 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 A7, TARSKI:def 2;
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 A9, A11, TARSKI:def 1, TARSKI:def 2;
hence s in X \/ {x} by A12, XBOOLE_0:def 3; :: 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 A8, ZFMISC_1:74;
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 LATTICE3:sch 2(A13);
 then f . (union Y) = 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 A3, A15; :: 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 A3, A17;
hence x = y by A3, A18; :: 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 A20, A21, A22;
A25: f . {x,y} = y by A3, A23;
A26: f . {y,z} = z by A3, A24;
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 A14, ORDERS_1:13;
field R = D by A14, ORDERS_1:13;
then reconsider R = R as Order of D by A14, A16, A19, A27, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;
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 A30, TARSKI:def 3;
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 FRAENKEL:sch 6(A31)
.= { b where t is Element of D : S2[t] }
.= {b} from LATTICE3:sch 1(A33) ;
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 A1, A29; :: 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 (LattPOSet L) by A34, Def15;
set p = % a;
X is_<=_than a
proof
let b be Element of (LattPOSet L); :: according to LATTICE3:def 9 :: thesis: ( b in X implies b <= a )
reconsider y = b as Element of D by A34, Def15;
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 A5, A36 ;
hence [b,a] in the InternalRel of (LattPOSet L) by A3, A35; :: 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 (LattPOSet L) ;
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 A40, TARSKI:def 3;
deffunc H4( Element of D) -> set = f . {$1,b};
deffunc H5( Element of D) -> Element of (LattPOSet L) = 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 (LattPOSet L) by A34, Def15;
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 FRAENKEL:sch 6(A41)
.= { b where t is Element of D : S2[t] }
.= {b} from LATTICE3:sch 1(A43) ;
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 A1, A39; :: thesis: verum
end;
end;
end;
then [a,b] in the InternalRel of (LattPOSet L) by A3, A35;
then A44: a <= b ;
A45: (% a) % = % a ;
q % = b ;
hence % a [= q by A44, A45, Th7; :: thesis: verum
end;
hence "\/" X = f . X by A37, Def21; :: 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 . (union X) ) 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;