:: Complete Lattices
:: by Grzegorz Bancerek
::
:: Received May 13, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

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 ) ) )
proofend;
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
proofend;
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
proofend;
end;

registration
let X be set ;
let x, y be Element of (BooleLatt X);
let x9, y9 be set ;
identifyx "\/" y with x9 \/ y9 when x = x9, y = y9;
compatibility
 ( x = x9 & y = y9 implies x "\/" y = x9 \/ y9 )
proofend;
identifyx "/\" y with x9 /\ y9 when x = x9, y = y9;
compatibility
 ( x = x9 & y = y9 implies x "/\" y = x9 /\ y9 )
proofend;
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 )
proofend;

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

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

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

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

theorem :: LATTICE3:5
for X being set
for x being Element of (BooleLatt X) holds x ` = X \ x
proofend;

begin

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
proofend;
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 #)
proofend;

definition
let L be Lattice;
let p be Element of L;
funcp %  ->  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 % )
proofend;

definition
let X be set ;
let O be Order of X;
:: original:~
redefine funcO ~  ->  Order of X;
coherence
 O ~ is Order of X
proofend;
end;

definition
let A be RelStr ;
funcA ~  ->  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;
clusterA ~  ->  strict reflexive transitive antisymmetric ;
coherence
 ( A ~ is reflexive &amp; A ~ is transitive &amp; A ~ is antisymmetric )
proofend;
end;

registration
let A be non empty RelStr ;
clusterA ~  ->  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;
funca ~  ->  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 ~ )
proofend;

definition
let A be RelStr ;
let X be set ;
let a be Element of A;
preda is_<=_than X means :: LATTICE3:def 8
 for b being Element of A st b in X holds
a <= b;
predX is_<=_than a means :Def9: :: 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 Def9 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 ;
attrIT is with_suprema  means :Def10: :: LATTICE3:def 10
 for x, y being Element of IT ex z being Element of IT st
( x <= z &amp; y <= z &amp; ( for z9 being Element of IT st x <= z9 &amp; y <= z9 holds
z <= z9 ) );
attrIT is with_infima  means :Def11: :: LATTICE3:def 11
 for x, y being Element of IT ex z being Element of IT st
( z <= x &amp; z <= y &amp; ( for z9 being Element of IT st z9 <= x &amp; 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 &amp; y <= z &amp; ( for z9 being Element of IT st x <= z9 &amp; 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 &amp; z <= y &amp; ( for z9 being Element of IT st z9 <= x &amp; 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
proofend;
cluster with_infima  ->  non empty for RelStr ;
coherence
 for b1 being RelStr st b1 is with_infima holds
not b1 is empty
proofend;
end;

theorem :: LATTICE3:10
for A being RelStr holds
( A is with_suprema iff A ~ is with_infima )
proofend;

theorem :: LATTICE3:11
for L being Lattice holds
( LattPOSet L is with_suprema &amp; LattPOSet L is with_infima )
proofend;

definition
let IT be RelStr ;
attrIT is complete  means :Def12: :: LATTICE3:def 12
 for X being set ex a being Element of IT st
( X is_<=_than a &amp; ( 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 &amp; ( for b being Element of IT st X is_<=_than b holds
a <= b ) ) );

registration
cluster non empty strict V58() reflexive transitive antisymmetric complete for RelStr ;
existence
 ex b1 being Poset st
( b1 is strict &amp; b1 is complete &amp; not b1 is empty )
proofend;
end;

theorem Th12: :: LATTICE3:12
for A being non empty RelStr st A is complete holds
( A is with_suprema &amp; A is with_infima )
proofend;

registration
cluster non empty strict V58() reflexive transitive antisymmetric with_suprema with_infima complete for RelStr ;
existence
 ex b1 being Poset st
( b1 is complete &amp; b1 is with_suprema &amp; b1 is with_infima &amp; b1 is strict &amp; not b1 is empty )
proofend;
end;

definition
let A be RelStr ;
assume B1: A is antisymmetric ;
let a, b be Element of A;
assume B2: ex x being Element of A st
( a <= x &amp; b <= x &amp; ( for c being Element of A st a <= c &amp; b <= c holds
x <= c ) ) ;
funca "\/" b ->  Element of A means :Def13: :: LATTICE3:def 13
( a <= it &amp; b <= it &amp; ( for c being Element of A st a <= c &amp; b <= c holds
it <= c ) );
existence
 ex b1 being Element of A st
( a <= b1 &amp; b <= b1 &amp; ( for c being Element of A st a <= c &amp; b <= c holds
b1 <= c ) ) by B2;
uniqueness
 for b1, b2 being Element of A st a <= b1 &amp; b <= b1 &amp; ( for c being Element of A st a <= c &amp; b <= c holds
b1 <= c ) &amp; a <= b2 &amp; b <= b2 &amp; ( for c being Element of A st a <= c &amp; b <= c holds
b2 <= c ) holds
b1 = b2
proofend;
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 &amp; b <= x &amp; ( for c being Element of A st a <= c &amp; b <= c holds
x <= c ) ) holds
for b4 being Element of A holds
( b4 = a "\/" b iff ( a <= b4 &amp; b <= b4 &amp; ( for c being Element of A st a <= c &amp; 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_&amp;_b_<=_c_&amp;_(_for_d_being_Element_of_A_st_a_<=_d_&amp;_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 &amp; b <= c &amp; ( for d being Element of A st a <= d &amp; 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 &amp; b <= c &amp; ( for d being Element of A st a <= d &amp; b <= d holds
c <= d ) ) )
 ex x being Element of A st
( a <= x &amp; b <= x &amp; ( for c being Element of A st a <= c &amp; b <= c holds
x <= c ) ) by Def10;
hence  for c being Element of A holds
( c = a "\/" b iff ( a <= c &amp; b <= c &amp; ( for d being Element of A st a <= d &amp; b <= d holds
c <= d ) ) ) by Def13; ::_thesis: verum
end;

definition
let A be RelStr ;
assume B1: A is antisymmetric ;
let a, b be Element of A;
assume B2: ex x being Element of A st
( a >= x &amp; b >= x &amp; ( for c being Element of A st a >= c &amp; b >= c holds
x >= c ) ) ;
funca "/\" b ->  Element of A means :Def14: :: LATTICE3:def 14
( it <= a &amp; it <= b &amp; ( for c being Element of A st c <= a &amp; c <= b holds
c <= it ) );
existence
 ex b1 being Element of A st
( b1 <= a &amp; b1 <= b &amp; ( for c being Element of A st c <= a &amp; c <= b holds
c <= b1 ) ) by B2;
uniqueness
 for b1, b2 being Element of A st b1 <= a &amp; b1 <= b &amp; ( for c being Element of A st c <= a &amp; c <= b holds
c <= b1 ) &amp; b2 <= a &amp; b2 <= b &amp; ( for c being Element of A st c <= a &amp; c <= b holds
c <= b2 ) holds
b1 = b2
proofend;
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 &amp; b >= x &amp; ( for c being Element of A st a >= c &amp; b >= c holds
x >= c ) ) holds
for b4 being Element of A holds
( b4 = a "/\" b iff ( b4 <= a &amp; b4 <= b &amp; ( for c being Element of A st c <= a &amp; 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_&amp;_b_>=_c_&amp;_(_for_d_being_Element_of_A_st_a_>=_d_&amp;_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 &amp; b >= c &amp; ( for d being Element of A st a >= d &amp; 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 &amp; b >= c &amp; ( for d being Element of A st a >= d &amp; b >= d holds
c >= d ) ) )
 ex x being Element of A st
( a >= x &amp; b >= x &amp; ( for c being Element of A st a >= c &amp; b >= c holds
x >= c ) ) by Def11;
hence  for c being Element of A holds
( c = a "/\" b iff ( a >= c &amp; b >= c &amp; ( for d being Element of A st a >= d &amp; 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
proofend;

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)
proofend;

theorem Th15: :: LATTICE3:15
for N being antisymmetric with_infima RelStr
for n1, n2 being Element of N holds n1 "/\" n2 = n2 "/\" n1
proofend;

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)
proofend;

definition
let L be antisymmetric with_infima RelStr ;
let x, y be Element of L;
:: original:"/\"
redefine funcx "/\" 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 funcx "\/" 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
proofend;

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
proofend;

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
proofend;

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 &amp; 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 .:) &amp; (LattPOSet L) ~ = LattPOSet (L .:) )
proofend;

begin

definition
let L be non empty LattStr ;
let p be Element of L;
let X be set ;
predp is_less_than X means :Def16: :: LATTICE3:def 16
 for q being Element of L st q in X holds
p [= q;
predX is_less_than p means :Def17: :: LATTICE3:def 17
 for q being Element of L st q in X holds
q [= p;
end;

:: deftheorem Def16 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 Def17 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 )
proofend;

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 )
proofend;

definition
let IT be non empty LattStr ;
attrIT is complete  means :Def18: :: LATTICE3:def 18
 for X being set ex p being Element of IT st
( X is_less_than p &amp; ( for r being Element of IT st X is_less_than r holds
p [= r ) );
attrIT is \/-distributive  means :Def19: :: LATTICE3:def 19
 for X being set
for a, b, c being Element of IT st X is_less_than a &amp; ( for d being Element of IT st X is_less_than d holds
a [= d ) &amp;  {  (b "/\" a9) where a9 is Element of IT : a9 in X  }  is_less_than c &amp; ( 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;
attrIT is /\-distributive  means :: LATTICE3:def 20
 for X being set
for a, b, c being Element of IT st X is_greater_than a &amp; ( for d being Element of IT st X is_greater_than d holds
d [= a ) &amp;  {  (b "\/" a9) where a9 is Element of IT : a9 in X  }  is_greater_than c &amp; ( 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 &amp; ( for r being Element of IT st X is_less_than r holds
p [= r ) ) );

:: deftheorem Def19 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 &amp; ( for d being Element of IT st X is_less_than d holds
a [= d ) &amp;  {  (b "/\" a9) where a9 is Element of IT : a9 in X  }  is_less_than c &amp; ( 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 &amp; ( for d being Element of IT st X is_greater_than d holds
d [= a ) &amp;  {  (b "\/" a9) where a9 is Element of IT : a9 in X  }  is_greater_than c &amp; ( 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 ` )
proofend;

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 ` )
proofend;

theorem Th25: :: LATTICE3:25
for X being set holds BooleLatt X is complete
proofend;

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
proofend;

theorem Th27: :: LATTICE3:27
for X being set holds BooleLatt X is /\-distributive
proofend;

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 &amp; b1 is \/-distributive &amp; b1 is /\-distributive &amp; b1 is strict )
proofend;
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 )
proofend;

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 )
proofend;

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 % )
proofend;

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 )
proofend;

registration
let A be non empty complete Poset;
cluster latt A ->  strict complete ;
coherence
 latt A is complete
proofend;
end;

definition
let L be non empty LattStr ;
assume B1: L is complete Lattice ;
let X be set ;
func "\/" (X,L) ->  Element of L means :Def21: :: LATTICE3:def 21
( X is_less_than it &amp; ( 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 &amp; ( for r being Element of L st X is_less_than r holds
b1 [= r ) ) by B1, Def18;
uniqueness
 for b1, b2 being Element of L st X is_less_than b1 &amp; ( for r being Element of L st X is_less_than r holds
b1 [= r ) &amp; X is_less_than b2 &amp; ( for r being Element of L st X is_less_than r holds
b2 [= r ) holds
b1 = b2
proofend;
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 &amp; ( 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))
proofend;

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) )
proofend;

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 &amp; ( for b being Element of C st b is_less_than X holds
b [= a ) ) )
proofend;

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)
proofend;

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)) )
proofend;

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)
proofend;

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) &amp; "/\" (X,C) [= a )
proofend;

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)
proofend;

theorem Th40: :: LATTICE3:40
for C being complete Lattice
for a being Element of C
for X being set st a in X &amp; X is_less_than a holds
"\/" (X,C) = a
proofend;

theorem Th41: :: LATTICE3:41
for C being complete Lattice
for a being Element of C
for X being set st a in X &amp; a is_less_than X holds
"/\" (X,C) = a
proofend;

theorem :: LATTICE3:42
for C being complete Lattice
for a being Element of C holds
( "\/" {a} = a &amp; "/\" {a} = a )
proofend;

theorem :: LATTICE3:43
for C being complete Lattice
for a, b being Element of C holds
( a "\/" b = "\/" {a,b} &amp; a "/\" b = "/\" {a,b} )
proofend;

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) &amp; a = "/\" ( {  c where c is Element of C : a [= c  }  ,C) )
proofend;

theorem Th45: :: LATTICE3:45
for C being complete Lattice
for X, Y being set st X c= Y holds
( "\/" (X,C) [= "\/" (Y,C) &amp; "/\" (Y,C) [= "/\" (X,C) )
proofend;

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 &amp; b in X )  }  ,C) &amp; "/\" (X,C) = "/\" ( {  b where b is Element of C : ex a being Element of C st
( a [= b &amp; a in X )  }  ,C) )
proofend;

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 &amp; b in Y ) ) holds
"\/" (X,C) [= "\/" (Y,C)
proofend;

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)
proofend;

theorem :: LATTICE3:49
for C being complete Lattice holds
( C is 0_Lattice &amp; Bottom C = "\/" ({},C) )
proofend;

theorem :: LATTICE3:50
for C being complete Lattice holds
( C is 1_Lattice &amp; Top C = "\/" ( the carrier of C,C) )
proofend;

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)
proofend;

theorem :: LATTICE3:52
for C being complete Lattice st C is I_Lattice holds
C is \/-distributive
proofend;

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) &amp; ("\/" (X,D)) "/\" a = "\/" ( {  (b2 "/\" a) where b2 is Element of D : b2 in X  }  ,D) )
proofend;

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) &amp; ("/\" (X,D)) "\/" a = "/\" ( {  (b2 "\/" a) where b2 is Element of D : b2 in X  }  ,D) )
proofend;

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]
proofend;

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()
proofend;

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_)_&amp;_(_for_X_being_Subset-Family_of_D_holds_f_._(f_.:_X)_=_f_._(union_X)_)_holds_
ex_L_being_strict_Lattice_st_
(_H1(L)_=_D_&amp;_(_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 ) &amp; ( for X being Subset-Family of D holds f . (f .: X) = f . (union X) ) holds
ex L being strict Lattice st
( H1(L) = D &amp; ( 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 ) &amp; ( for X being Subset-Family of D holds f . (f .: X) = f . (union X) ) implies ex L being strict Lattice st
( H1(L) = D &amp; ( 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 &amp; ( for X being Subset of L holds "\/" X = f . X ) )
defpred S1[ set , set ] means f . {$1,$2} = $2;
consider R being Relation of D such that
A3: for x, y being set holds
( [x,y] in R iff ( x in D &amp; y in D &amp; 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 toXBOOLE_0:def_10 ::_thesis: union  {  {t,x} where t is Element of D : t in X  }  c= X \/ {x}
proof
let s be set ; :: according toTARSKI: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 &amp; X c= D ) or s in {x} ) by XBOOLE_0:def_3;
then  ( ( s in X &amp; s is Element of D ) or s = x ) by TARSKI:def_1;
then  ( ( s in {s,x} &amp; {s,x} in  {  {t,x} where t is Element of D : t in X  }  ) or ( s in {y,x} &amp; {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 set ; :: according toTARSKI: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 &amp; 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 set ; :: according toTARSKI:def_3 ::_thesis: ( not s in  {  {t,x} where t is Element of D : t in X  }  or s in bool D )
assume  s in  {  {t,x} where t is Element of D : t in X  }  ; ::_thesis: s in bool D
then  s c= X \/ {x} by A8, ZFMISC_1:74;
then  s 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 set ; :: according toRELAT_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 set ; :: according toRELAT_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 set ; :: according toRELAT_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 toLATTICE3:def_12 ::_thesis: ex a being Element of RelStr(# D,R #) st
( X is_<=_than a &amp; ( 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 &amp; ( 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 toLATTICE3: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 toORDERS_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
percases ( Y <> {} or Y = {} ) ;
supposeA30: 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, Def9;
then  [t,y] in R by ORDERS_2:def_5;
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 toORDERS_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 &amp; ( for X being Subset of L holds "\/" X = f . X ) )
A34: ( A is with_suprema &amp; 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 toLATTICE3: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 toORDERS_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
percases ( Y <> {} or Y = {} ) ;
supposeA40: 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, Def9;
then  [t,y] in R by A35, ORDERS_2:def_5;
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 by ORDERS_2:def_5;
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 ) &amp; ( 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 &amp; ( for X being Subset of L holds "\/" X = f . X ) ) by Lm3;