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

deffunc H₁( LattStr ) -> set = the carrier of $1;

deffunc H₂( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_join of $1;

deffunc H₃( 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 b₁ being strict LattStr st
( the carrier of b₁ = bool X & ( for Y, Z being Subset of X holds
( the L_join of b₁ . (Y,Z) = Y \/ Z & the L_meet of b₁ . (Y,Z) = Y /\ Z ) ) )

proof end;

uniqueness
for b₁, b₂ being strict LattStr st the carrier of b₁ = bool X & ( for Y, Z being Subset of X holds
( the L_join of b₁ . (Y,Z) = Y \/ Z & the L_meet of b₁ . (Y,Z) = Y /\ Z ) ) & the carrier of b₂ = bool X & ( for Y, Z being Subset of X holds
( the L_join of b₂ . (Y,Z) = Y \/ Z & the L_meet of b₂ . (Y,Z) = Y /\ Z ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines BooleLatt LATTICE3:def 1 :
for X being set
for b₂ being strict LattStr holds
( b₂ = BooleLatt X iff ( the carrier of b₂ = bool X & ( for Y, Z being Subset of X holds
( the L_join of b₂ . (Y,Z) = Y \/ Z & the L_meet of b₂ . (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 b₁ being RelStr st b₁ is with_suprema holds
not b₁ is empty

proof end;

cluster with_infima -> non empty for RelStr ;

coherence
for b₁ being RelStr st b₁ is with_infima holds
not b₁ 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 b₁ being Poset st
( b₁ is strict & b₁ is complete & not b₁ 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 b₁ being Poset st
( b₁ is complete & b₁ is with_suprema & b₁ is with_infima & b₁ is strict & not b₁ 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 b₁ being Element of A st
( a <= b₁ & b <= b₁ & ( for c being Element of A st a <= c & b <= c holds
b₁ <= c ) ) by A2;
uniqueness
for b₁, b₂ being Element of A st a <= b₁ & b <= b₁ & ( for c being Element of A st a <= c & b <= c holds
b₁ <= c ) & a <= b₂ & b <= b₂ & ( for c being Element of A st a <= c & b <= c holds
b₂ <= c ) holds
b₁ = b₂

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 b₄ being Element of A holds
( b₄ = a "\/" b iff ( a <= b₄ & b <= b₄ & ( for c being Element of A st a <= c & b <= c holds
b₄ <= 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 b₁ being Element of A st
( b₁ <= a & b₁ <= b & ( for c being Element of A st c <= a & c <= b holds
c <= b₁ ) ) by A2;
uniqueness
for b₁, b₂ being Element of A st b₁ <= a & b₁ <= b & ( for c being Element of A st c <= a & c <= b holds
c <= b₁ ) & b₂ <= a & b₂ <= b & ( for c being Element of A st c <= a & c <= b holds
c <= b₂ ) holds
b₁ = b₂

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 b₄ being Element of A holds
( b₄ = a "/\" b iff ( b₄ <= a & b₄ <= b & ( for c being Element of A st c <= a & c <= b holds
c <= b₄ ) ) );

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 b₁ being strict Lattice st RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet b₁ by A1, Th19;
uniqueness
for b₁, b₂ being strict Lattice st RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet b₁ & RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet b₂ holds
b₁ = b₂ by Th6;

end;

:: deftheorem Def15 defines latt LATTICE3:def 15 :
for A being RelStr st A is with_suprema with_infima Poset holds
for b₂ being strict Lattice holds
( b₂ = latt A iff RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet b₂ );

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 b₁ being Lattice st
( b₁ is complete & b₁ is \/-distributive & b₁ is /\-distributive & b₁ 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 b₁ being Element of L st
( X is_less_than b₁ & ( for r being Element of L st X is_less_than r holds
b₁ [= r ) ) by A1, Def18;
uniqueness
for b₁, b₂ being Element of L st X is_less_than b₁ & ( for r being Element of L st X is_less_than r holds
b₁ [= r ) & X is_less_than b₂ & ( for r being Element of L st X is_less_than r holds
b₂ [= r ) holds
b₁ = b₂

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 b₃ being Element of L holds
( b₃ = "\/" (X,L) iff ( X is_less_than b₃ & ( for r being Element of L st X is_less_than r holds
b₃ [= 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{ F₁() -> set , F₂() -> non empty set , P₁[ set ] } :

{ F₁() where a is Element of F₂() : P₁[a] } = {F₁()}

provided

A1: ex a being Element of F₂() st P₁[a]

proof end;

scheme :: LATTICE3:sch 2
FuncFraenkel{ F₁() -> non empty set , F₂() -> non empty set , F₃( set ) -> Element of F₂(), F₄() -> Function, P₁[ set ] } :

F₄() .: { F₃(x) where x is Element of F₁() : P₁[x] } = { (F₄() . F₃(x)) where x is Element of F₁() : P₁[x] }

provided

A1: F₂() c= dom F₄()

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
( H₁(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
( H₁(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
( H₁(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
( H₁(L) = D & ( for X being Subset of L holds "\/" X = f . X ) )
defpred S₁[ 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 & S₁[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 S₂[ set ] means $1 in X;
deffunc H₄( Element of D) -> Element of bool D = {$1,x};
A13: bool D c= dom f by FUNCT_2:def 1;
f .: { H₄(t) where t is Element of D : S₂[t] } = { (f . H₄(t)) where t is Element of D : S₂[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 H₄( Element of D) -> set = f . {$1,b};
deffunc H₅( Element of D) -> Element of RelStr(# D,R #) = b;
defpred S₂[ set ] means $1 in Y;
A31: for t being Element of D st S₂[t] holds
H₄(t) = H₅(t)

proof

let t be Element of D; :: thesis: ( S₂[t] implies H₄(t) = H₅(t) )
reconsider s = t as Element of RelStr(# D,R #) ;
reconsider y = b as Element of D ;
assume t in Y ; :: thesis: H₄(t) = H₅(t)
then t in X by XBOOLE_0:def 4;
then s <= b by A28;
then [t,y] in R ;
hence H₄(t) = H₅(t) by A3; :: thesis: verum

end;

A32: s in Y by A30;
then A33: ex t being Element of D st S₂[t] ;
{ H₄(t) where t is Element of D : S₂[t] } = { H₅(t) where t is Element of D : S₂[t] } from FRAENKEL:sch 6(A31)
.= { b where t is Element of D : S₂[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: ( H₁(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 H₁(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 H₄( Element of D) -> set = f . {$1,b};
deffunc H₅( Element of D) -> Element of (LattPOSet L) = b;
defpred S₂[ set ] means $1 in Y;
A41: for t being Element of D st S₂[t] holds
H₄(t) = H₅(t)

proof

let t be Element of D; :: thesis: ( S₂[t] implies H₄(t) = H₅(t) )
reconsider s = t as Element of (LattPOSet L) by A34, Def15;
assume t in Y ; :: thesis: H₄(t) = H₅(t)
then s <= b by A38;
then [t,y] in R by A35;
hence H₄(t) = H₅(t) by A3; :: thesis: verum

end;

A42: s in Y by A40;
then A43: ex t being Element of D st S₂[t] ;
{ H₄(t) where t is Element of D : S₂[t] } = { H₅(t) where t is Element of D : S₂[t] } from FRAENKEL:sch 6(A41)
.= { b where t is Element of D : S₂[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;