:: LATTICE3 semantic presentation
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 ) ) )
proof
deffunc H4( Subset of X, Subset of X) -> Element of bool X = $1 \/ $2;
consider j being BinOp of (bool X) such that
A1: for x, y being Subset of X holds j . (x,y) = H4(x,y) from BINOP_1:sch_4();
deffunc H5( Subset of X, Subset of X) -> Element of bool X = $1 /\ $2;
consider m being BinOp of (bool X) such that
A2: for x, y being Subset of X holds m . (x,y) = H5(x,y) from BINOP_1:sch_4();
take LattStr(# (bool X),j,m #) ; ::_thesis: ( the carrier of LattStr(# (bool X),j,m #) = bool X & ( for Y, Z being Subset of X holds
( the L_join of LattStr(# (bool X),j,m #) . (Y,Z) = Y \/ Z & the L_meet of LattStr(# (bool X),j,m #) . (Y,Z) = Y /\ Z ) ) )
thus ( the carrier of LattStr(# (bool X),j,m #) = bool X & ( for Y, Z being Subset of X holds
( the L_join of LattStr(# (bool X),j,m #) . (Y,Z) = Y \/ Z & the L_meet of LattStr(# (bool X),j,m #) . (Y,Z) = Y /\ Z ) ) ) by A1, A2; ::_thesis: verum
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
let L1, L2 be strict LattStr ; ::_thesis: ( the carrier of L1 = bool X & ( for Y, Z being Subset of X holds
( the L_join of L1 . (Y,Z) = Y \/ Z & the L_meet of L1 . (Y,Z) = Y /\ Z ) ) & the carrier of L2 = bool X & ( for Y, Z being Subset of X holds
( the L_join of L2 . (Y,Z) = Y \/ Z & the L_meet of L2 . (Y,Z) = Y /\ Z ) ) implies L1 = L2 )
assume that
A3: the carrier of L1 = bool X and
A4: for Y, Z being Subset of X holds
( H2(L1) . (Y,Z) = Y \/ Z & H3(L1) . (Y,Z) = Y /\ Z ) and
A5: the carrier of L2 = bool X and
A6: for Y, Z being Subset of X holds
( H2(L2) . (Y,Z) = Y \/ Z & H3(L2) . (Y,Z) = Y /\ Z ) ; ::_thesis: L1 = L2
reconsider j1 = H2(L1), j2 = H2(L2), m1 = H3(L1), m2 = H3(L2) as BinOp of (bool X) by A3, A5;
now__::_thesis:_for_x,_y_being_Subset_of_X_holds_j1_._(x,y)_=_j2_._(x,y)
let x, y be Subset of X; ::_thesis: j1 . (x,y) = j2 . (x,y)
thus j1 . (x,y) = x \/ y by A4
.= j2 . (x,y) by A6 ; ::_thesis: verum
end;
then A7: j1 = j2 by BINOP_1:2;
now__::_thesis:_for_x,_y_being_Subset_of_X_holds_m1_._(x,y)_=_m2_._(x,y)
let x, y be Subset of X; ::_thesis: m1 . (x,y) = m2 . (x,y)
thus m1 . (x,y) = x /\ y by A4
.= m2 . (x,y) by A6 ; ::_thesis: verum
end;
hence L1 = L2 by A3, A5, A7, BINOP_1:2; ::_thesis: verum
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
the carrier of (BooleLatt X) = bool X by Def1;
hence not the carrier of (BooleLatt X) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
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 )
proof
reconsider x99 = x, y99 = y as Subset of X by Def1;
assume that
A1: x = x9 and
A2: y = y9 ; ::_thesis: x "\/" y = x9 \/ y9
thus x "\/" y = H2( BooleLatt X) . (x99,y99)
.= x9 \/ y9 by A1, A2, Def1 ; ::_thesis: verum
end;
identifyx "/\" y with x9 /\ y9 when x = x9, y = y9;
compatibility
( x = x9 & y = y9 implies x "/\" y = x9 /\ y9 )
proof
reconsider x99 = x, y99 = y as Subset of X by Def1;
assume that
A3: x = x9 and
A4: y = y9 ; ::_thesis: x "/\" y = x9 /\ y9
thus x "/\" y = H3( BooleLatt X) . (x99,y99)
.= x9 /\ y9 by A3, A4, Def1 ; ::_thesis: verum
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 )
proof
let X be set ; ::_thesis: for x, y being Element of (BooleLatt X) holds
( x [= y iff x c= y )
let x, y be Element of (BooleLatt X); ::_thesis: ( x [= y iff x c= y )
( x [= y iff x "\/" y = y ) by LATTICES:def_3;
hence ( x [= y iff x c= y ) by XBOOLE_1:7, XBOOLE_1:12; ::_thesis: verum
end;
registration
let X be set ;
cluster BooleLatt X -> strict Lattice-like ;
coherence
BooleLatt X is Lattice-like
proof
A1: for x, y being Element of (BooleLatt X) holds x "\/" y = y "\/" x ;
A2: for x, y, z being Element of (BooleLatt X) holds x "\/" (y "\/" z) = (x "\/" y) "\/" z by XBOOLE_1:4;
A3: for x, y being Element of (BooleLatt X) holds (x "/\" y) "\/" y = y by XBOOLE_1:22;
A4: for x, y being Element of (BooleLatt X) holds x "/\" y = y "/\" x ;
A5: for x, y, z being Element of (BooleLatt X) holds x "/\" (y "/\" z) = (x "/\" y) "/\" z by XBOOLE_1:16;
for x, y being Element of (BooleLatt X) holds x "/\" (x "\/" y) = x by XBOOLE_1:21;
then ( BooleLatt X is join-commutative & BooleLatt X is join-associative & BooleLatt X is meet-absorbing & BooleLatt X is meet-commutative & BooleLatt X is meet-associative & BooleLatt X is join-absorbing ) by A1, A2, A3, A4, A5, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
hence BooleLatt X is Lattice-like ; ::_thesis: verum
end;
end;
theorem Th3: :: LATTICE3:3
for X being set holds
( BooleLatt X is lower-bounded & Bottom (BooleLatt X) = {} )
proof
let X be set ; ::_thesis: ( BooleLatt X is lower-bounded & Bottom (BooleLatt X) = {} )
{} c= X by XBOOLE_1:2;
then reconsider x = {} as Element of (BooleLatt X) by Def1;
A1: for y being Element of (BooleLatt X) holds x "/\" y = x ;
A2: for y being Element of (BooleLatt X) holds y "/\" x = x ;
thus BooleLatt X is lower-bounded ::_thesis: Bottom (BooleLatt X) = {}
proof
take x ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (BooleLatt X) holds
( x "/\" b1 = x & b1 "/\" x = x )
thus for b1 being Element of the carrier of (BooleLatt X) holds
( x "/\" b1 = x & b1 "/\" x = x ) ; ::_thesis: verum
end;
hence Bottom (BooleLatt X) = {} by A1, A2, LATTICES:def_16; ::_thesis: verum
end;
theorem Th4: :: LATTICE3:4
for X being set holds
( BooleLatt X is upper-bounded & Top (BooleLatt X) = X )
proof
let X be set ; ::_thesis: ( BooleLatt X is upper-bounded & Top (BooleLatt X) = X )
A1: bool X = H1( BooleLatt X) by Def1;
then reconsider x = X as Element of (BooleLatt X) by ZFMISC_1:def_1;
A2: for y being Element of (BooleLatt X) holds x "\/" y = x by A1, XBOOLE_1:12;
A3: for y being Element of (BooleLatt X) holds y "\/" x = x by A1, XBOOLE_1:12;
thus BooleLatt X is upper-bounded ::_thesis: Top (BooleLatt X) = X
proof
take x ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of (BooleLatt X) holds
( x "\/" b1 = x & b1 "\/" x = x )
thus for b1 being Element of the carrier of (BooleLatt X) holds
( x "\/" b1 = x & b1 "\/" x = x ) by A1, XBOOLE_1:12; ::_thesis: verum
end;
hence Top (BooleLatt X) = X by A2, A3, LATTICES:def_17; ::_thesis: verum
end;
registration
let X be set ;
cluster BooleLatt X -> strict Boolean ;
coherence
BooleLatt X is Boolean
proof
set B = BooleLatt X;
A1: BooleLatt X is 0_Lattice by Th3;
BooleLatt X is 1_Lattice by Th4;
then reconsider B = BooleLatt X as 01_Lattice by A1;
A2: B is complemented
proof
let x be Element of B; :: according to LATTICES:def_19 ::_thesis: ex b1 being Element of the carrier of B st b1 is_a_complement_of x
A3: H1(B) = bool X by Def1;
reconsider y = X \ x as Element of B by Def1;
take y ; ::_thesis: y is_a_complement_of x
thus y "\/" x = y \/ x by Th1
.= X \/ x by XBOOLE_1:39
.= X by A3, XBOOLE_1:12
.= Top B by Th4 ; :: according to LATTICES:def_18 ::_thesis: ( x "\/" y = Top B & y "/\" x = Bottom B & x "/\" y = Bottom B )
hence x "\/" y = Top B ; ::_thesis: ( y "/\" x = Bottom B & x "/\" y = Bottom B )
A4: y misses x by XBOOLE_1:79;
thus y "/\" x = y /\ x by Th1
.= {} by A4, XBOOLE_0:def_7
.= Bottom B by Th3 ; ::_thesis: x "/\" y = Bottom B
hence x "/\" y = Bottom B ; ::_thesis: verum
end;
B is distributive
proof
let x, y, z be Element of B; :: according to LATTICES:def_11 ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
thus x "/\" (y "\/" z) = x /\ (y "\/" z) by Th1
.= x /\ (y \/ z) by Th1
.= (x /\ y) \/ (x /\ z) by XBOOLE_1:23
.= (x "/\" y) \/ (x /\ z) by Th1
.= (x "/\" y) \/ (x "/\" z) by Th1
.= (x "/\" y) "\/" (x "/\" z) by Th1 ; ::_thesis: verum
end;
hence BooleLatt X is Boolean by A2; ::_thesis: verum
end;
end;
theorem :: LATTICE3:5
for X being set
for x being Element of (BooleLatt X) holds x ` = X \ x
proof
let X be set ; ::_thesis: for x being Element of (BooleLatt X) holds x ` = X \ x
set B = BooleLatt X;
let x be Element of (BooleLatt X); ::_thesis: x ` = X \ x
A1: (x `) "/\" x = Bottom (BooleLatt X) by LATTICES:20;
A2: x "\/" (x `) = Top (BooleLatt X) by LATTICES:21;
A3: Bottom (BooleLatt X) = {} by Th3;
A4: Top (BooleLatt X) = X by Th4;
A5: x ` misses x by A1, A3, XBOOLE_0:def_7;
A6: X \ x = (x \ x) \/ ((x `) \ x) by A2, A4, XBOOLE_1:42;
x \ x = {} by XBOOLE_1:37;
hence x ` = X \ x by A5, A6, XBOOLE_1:83; ::_thesis: verum
end;
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
proof
A1: LattRel L = { [p,q] where p, q is Element of L : p [= q } by FILTER_1:def_8;
LattRel L c= [:H1(L),H1(L):]
proof
let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in LattRel L or [x,y] in [:H1(L),H1(L):] )
assume [x,y] in LattRel L ; ::_thesis: [x,y] in [:H1(L),H1(L):]
then ex p, q being Element of L st
( [x,y] = [p,q] & p [= q ) by A1;
hence [x,y] in [:H1(L),H1(L):] by ZFMISC_1:87; ::_thesis: verum
end;
then reconsider R = LattRel L as Relation of H1(L) ;
A2: R is_reflexive_in H1(L)
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in H1(L) or [x,x] in R )
assume x in H1(L) ; ::_thesis: [x,x] in R
then reconsider x = x as Element of L ;
x [= x ;
hence [x,x] in R by FILTER_1:31; ::_thesis: verum
end;
A3: R is_antisymmetric_in H1(L)
proof
let x, y be set ; :: according to RELAT_2:def_4 ::_thesis: ( not x in H1(L) or not y in H1(L) or not [x,y] in R or not [y,x] in R or x = y )
assume that
A4: x in H1(L) and
A5: y in H1(L) ; ::_thesis: ( not [x,y] in R or not [y,x] in R or x = y )
reconsider x9 = x, y9 = y as Element of L by A4, A5;
assume that
A6: [x,y] in R and
A7: [y,x] in R ; ::_thesis: x = y
A8: x9 [= y9 by A6, FILTER_1:31;
y9 [= x9 by A7, FILTER_1:31;
hence x = y by A8, LATTICES:8; ::_thesis: verum
end;
A9: R is_transitive_in H1(L)
proof
let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in H1(L) or not y in H1(L) or not z in H1(L) or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume that
A10: x in H1(L) and
A11: y in H1(L) and
A12: z in H1(L) ; ::_thesis: ( not [x,y] in R or not [y,z] in R or [x,z] in R )
reconsider x9 = x, y9 = y, z9 = z as Element of L by A10, A11, A12;
assume that
A13: [x,y] in R and
A14: [y,z] in R ; ::_thesis: [x,z] in R
A15: x9 [= y9 by A13, FILTER_1:31;
y9 [= z9 by A14, FILTER_1:31;
then x9 [= z9 by A15, LATTICES:7;
hence [x,z] in R by FILTER_1:31; ::_thesis: verum
end;
A16: dom R = H1(L) by A2, ORDERS_1:13;
field R = H1(L) by A2, ORDERS_1:13;
hence LattRel L is Order of the carrier of L by A2, A3, A9, A16, PARTFUN1:def_2, RELAT_2:def_9, RELAT_2:def_12, RELAT_2:def_16; ::_thesis: verum
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
let L1, L2 be Lattice; ::_thesis: ( LattPOSet L1 = LattPOSet L2 implies 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 #) )
assume A1: LattPOSet L1 = LattPOSet L2 ; ::_thesis: 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 #)
reconsider j = H2(L2), m = H3(L2) as BinOp of H1(L1) by A1;
now__::_thesis:_for_a,_b_being_Element_of_L1_holds_H2(L1)_._(a,b)_=_j_._(a,b)
let a, b be Element of L1; ::_thesis: H2(L1) . (a,b) = j . (a,b)
reconsider x = a, y = b, xy = a "\/" b as Element of L2 by A1;
reconsider ab = x "\/" y as Element of L1 by A1;
A2: a [= a "\/" b by LATTICES:5;
A3: b [= b "\/" a by LATTICES:5;
A4: x [= x "\/" y by LATTICES:5;
A5: y [= y "\/" x by LATTICES:5;
A6: [x,xy] in LattRel L2 by A1, A2, FILTER_1:31;
A7: [y,xy] in LattRel L2 by A1, A3, FILTER_1:31;
A8: [a,ab] in LattRel L1 by A1, A4, FILTER_1:31;
A9: [b,ab] in LattRel L1 by A1, A5, FILTER_1:31;
A10: a [= ab by A8, FILTER_1:31;
A11: b [= ab by A9, FILTER_1:31;
A12: x [= xy by A6, FILTER_1:31;
A13: y [= xy by A7, FILTER_1:31;
A14: a "\/" b [= ab by A10, A11, FILTER_0:6;
x "\/" y [= xy by A12, A13, FILTER_0:6;
then [ab,(a "\/" b)] in LattRel L1 by A1, FILTER_1:31;
then ab [= a "\/" b by FILTER_1:31;
hence H2(L1) . (a,b) = j . (a,b) by A14, LATTICES:8; ::_thesis: verum
end;
then A15: H2(L1) = j by BINOP_1:2;
now__::_thesis:_for_a,_b_being_Element_of_L1_holds_H3(L1)_._(a,b)_=_m_._(a,b)
let a, b be Element of L1; ::_thesis: H3(L1) . (a,b) = m . (a,b)
reconsider x = a, y = b, xy = a "/\" b as Element of L2 by A1;
reconsider ab = x "/\" y as Element of L1 by A1;
A16: a "/\" b [= a by LATTICES:6;
A17: b "/\" a [= b by LATTICES:6;
A18: x "/\" y [= x by LATTICES:6;
A19: y "/\" x [= y by LATTICES:6;
A20: [xy,x] in LattRel L2 by A1, A16, FILTER_1:31;
A21: [xy,y] in LattRel L2 by A1, A17, FILTER_1:31;
A22: [ab,a] in LattRel L1 by A1, A18, FILTER_1:31;
A23: [ab,b] in LattRel L1 by A1, A19, FILTER_1:31;
A24: ab [= a by A22, FILTER_1:31;
A25: ab [= b by A23, FILTER_1:31;
A26: xy [= x by A20, FILTER_1:31;
A27: xy [= y by A21, FILTER_1:31;
A28: ab [= a "/\" b by A24, A25, FILTER_0:7;
xy [= x "/\" y by A26, A27, FILTER_0:7;
then [(a "/\" b),ab] in LattRel L1 by A1, FILTER_1:31;
then a "/\" b [= ab by FILTER_1:31;
hence H3(L1) . (a,b) = m . (a,b) by A28, LATTICES:8; ::_thesis: verum
end;
hence 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 #) by A1, A15, BINOP_1:2; ::_thesis: verum
end;
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 % )
proof
let L be Lattice; ::_thesis: for p, q being Element of L holds
( p [= q iff p % <= q % )
let p, q be Element of L; ::_thesis: ( p [= q iff p % <= q % )
( p [= q iff [p,q] in LattRel L ) by FILTER_1:31;
hence ( p [= q iff p % <= q % ) by ORDERS_2:def_5; ::_thesis: verum
end;
definition
let X be set ;
let O be Order of X;
:: original: ~
redefine funcO ~ -> Order of X;
coherence
O ~ is Order of X
proof
A1: dom O = dom (O ~) by RELAT_2:12;
dom O = X by PARTFUN1:def_2;
hence O ~ is Order of X by A1, PARTFUN1:def_2; ::_thesis: verum
end;
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 & A ~ is transitive & A ~ is antisymmetric )
proof
A ~ = RelStr(# the carrier of A,( the InternalRel of A ~) #) ;
hence ( A ~ is reflexive & A ~ is transitive & A ~ is antisymmetric ) ; ::_thesis: verum
end;
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 ~ )
proof
let A be RelStr ; ::_thesis: for a, b being Element of A holds
( a <= b iff b ~ <= a ~ )
let a, b be Element of A; ::_thesis: ( a <= b iff b ~ <= a ~ )
A1: ( a <= b iff [a,b] in the InternalRel of A ) by ORDERS_2:def_5;
( b ~ <= a ~ iff [(b ~),(a ~)] in the InternalRel of (A ~) ) by ORDERS_2:def_5;
hence ( a <= b iff b ~ <= a ~ ) by A1, RELAT_1:def_7; ::_thesis: verum
end;
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 & y <= z & ( for z9 being Element of IT st x <= z9 & 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 & 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
let A be RelStr ; ::_thesis: ( A is with_suprema implies not A is empty )
assume A1: for x, y being Element of A ex z being Element of A st
( x <= z & y <= z & ( for z9 being Element of A st x <= z9 & y <= z9 holds
z <= z9 ) ) ; :: according to LATTICE3:def_10 ::_thesis: not A is empty
set x = the Element of A;
consider z being Element of A such that
A2: the Element of A <= z and
the Element of A <= z and
for z9 being Element of A st the Element of A <= z9 & the Element of A <= z9 holds
z <= z9 by A1;
[ the Element of A,z] in the InternalRel of A by A2, ORDERS_2:def_5;
hence not A is empty ; ::_thesis: verum
end;
cluster with_infima -> non empty for RelStr ;
coherence
for b1 being RelStr st b1 is with_infima holds
not b1 is empty
proof
let A be RelStr ; ::_thesis: ( A is with_infima implies not A is empty )
assume A3: for x, y being Element of A ex z being Element of A st
( x >= z & y >= z & ( for z9 being Element of A st x >= z9 & y >= z9 holds
z >= z9 ) ) ; :: according to LATTICE3:def_11 ::_thesis: not A is empty
set x = the Element of A;
consider z being Element of A such that
A4: the Element of A >= z and
the Element of A >= z and
for z9 being Element of A st the Element of A >= z9 & the Element of A >= z9 holds
z >= z9 by A3;
[z, the Element of A] in the InternalRel of A by A4, ORDERS_2:def_5;
hence not A is empty ; ::_thesis: verum
end;
end;
theorem :: LATTICE3:10
for A being RelStr holds
( A is with_suprema iff A ~ is with_infima )
proof
let A be RelStr ; ::_thesis: ( A is with_suprema iff A ~ is with_infima )
thus ( A is with_suprema implies A ~ is with_infima ) ::_thesis: ( A ~ is with_infima implies A is with_suprema )
proof
assume A1: for a, b being Element of A ex c being Element of A st
( a <= c & b <= c & ( for c9 being Element of A st a <= c9 & b <= c9 holds
c <= c9 ) ) ; :: according to LATTICE3:def_10 ::_thesis: A ~ is with_infima
let x, y be Element of (A ~); :: according to LATTICE3:def_11 ::_thesis: ex z being Element of (A ~) st
( z <= x & z <= y & ( for z9 being Element of (A ~) st z9 <= x & z9 <= y holds
z9 <= z ) )
consider c being Element of A such that
A2: ~ x <= c and
A3: ~ y <= c and
A4: for c9 being Element of A st ~ x <= c9 & ~ y <= c9 holds
c <= c9 by A1;
take z = c ~ ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of (A ~) st z9 <= x & z9 <= y holds
z9 <= z ) )
A5: (~ x) ~ = ~ x ;
A6: (~ y) ~ = ~ y ;
hence ( z <= x & z <= y ) by A2, A3, A5, Th9; ::_thesis: for z9 being Element of (A ~) st z9 <= x & z9 <= y holds
z9 <= z
let z9 be Element of (A ~); ::_thesis: ( z9 <= x & z9 <= y implies z9 <= z )
A7: (~ z9) ~ = ~ z9 ;
assume that
A8: z9 <= x and
A9: z9 <= y ; ::_thesis: z9 <= z
A10: ~ x <= ~ z9 by A5, A7, A8, Th9;
~ y <= ~ z9 by A6, A7, A9, Th9;
then c <= ~ z9 by A4, A10;
hence z9 <= z by A7, Th9; ::_thesis: verum
end;
assume A11: for x, y being Element of (A ~) ex z being Element of (A ~) st
( z <= x & z <= y & ( for z9 being Element of (A ~) st z9 <= x & z9 <= y holds
z9 <= z ) ) ; :: according to LATTICE3:def_11 ::_thesis: A is with_suprema
let a be Element of A; :: according to LATTICE3:def_10 ::_thesis: for y being Element of A ex z being Element of A st
( a <= z & y <= z & ( for z9 being Element of A st a <= z9 & y <= z9 holds
z <= z9 ) )
let b be Element of A; ::_thesis: ex z being Element of A st
( a <= z & b <= z & ( for z9 being Element of A st a <= z9 & b <= z9 holds
z <= z9 ) )
consider z being Element of (A ~) such that
A12: z <= a ~ and
A13: z <= b ~ and
A14: for z9 being Element of (A ~) st z9 <= a ~ & z9 <= b ~ holds
z9 <= z by A11;
take c = ~ z; ::_thesis: ( a <= c & b <= c & ( for z9 being Element of A st a <= z9 & b <= z9 holds
c <= z9 ) )
A15: (~ z) ~ = ~ z ;
hence ( a <= c & b <= c ) by A12, A13, Th9; ::_thesis: for z9 being Element of A st a <= z9 & b <= z9 holds
c <= z9
let c9 be Element of A; ::_thesis: ( a <= c9 & b <= c9 implies c <= c9 )
assume that
A16: a <= c9 and
A17: b <= c9 ; ::_thesis: c <= c9
A18: c9 ~ <= a ~ by A16, Th9;
c9 ~ <= b ~ by A17, Th9;
then c9 ~ <= z by A14, A18;
hence c <= c9 by A15, Th9; ::_thesis: verum
end;
theorem :: LATTICE3:11
for L being Lattice holds
( LattPOSet L is with_suprema & LattPOSet L is with_infima )
proof
let L be Lattice; ::_thesis: ( LattPOSet L is with_suprema & LattPOSet L is with_infima )
thus LattPOSet L is with_suprema ::_thesis: LattPOSet L is with_infima
proof
let x, y be Element of (LattPOSet L); :: according to LATTICE3:def_10 ::_thesis: ex z being Element of (LattPOSet L) st
( x <= z & y <= z & ( for z9 being Element of (LattPOSet L) st x <= z9 & y <= z9 holds
z <= z9 ) )
take z = ((% x) "\/" (% y)) % ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of (LattPOSet L) st x <= z9 & y <= z9 holds
z <= z9 ) )
A1: % x [= (% x) "\/" (% y) by LATTICES:5;
A2: % y [= (% y) "\/" (% x) by LATTICES:5;
A3: (% x) % = % x ;
A4: (% y) % = % y ;
hence ( x <= z & y <= z ) by A1, A2, A3, Th7; ::_thesis: for z9 being Element of (LattPOSet L) st x <= z9 & y <= z9 holds
z <= z9
let z9 be Element of (LattPOSet L); ::_thesis: ( x <= z9 & y <= z9 implies z <= z9 )
A5: (% z9) % = % z9 ;
assume that
A6: x <= z9 and
A7: y <= z9 ; ::_thesis: z <= z9
A8: % x [= % z9 by A3, A5, A6, Th7;
% y [= % z9 by A4, A5, A7, Th7;
then (% x) "\/" (% y) [= % z9 by A8, FILTER_0:6;
hence z <= z9 by A5, Th7; ::_thesis: verum
end;
let x, y be Element of (LattPOSet L); :: according to LATTICE3:def_11 ::_thesis: ex z being Element of (LattPOSet L) st
( z <= x & z <= y & ( for z9 being Element of (LattPOSet L) st z9 <= x & z9 <= y holds
z9 <= z ) )
take z = ((% x) "/\" (% y)) % ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of (LattPOSet L) st z9 <= x & z9 <= y holds
z9 <= z ) )
A9: (% x) "/\" (% y) [= % x by LATTICES:6;
A10: (% y) "/\" (% x) [= % y by LATTICES:6;
A11: (% x) % = % x ;
A12: (% y) % = % y ;
hence ( z <= x & z <= y ) by A9, A10, A11, Th7; ::_thesis: for z9 being Element of (LattPOSet L) st z9 <= x & z9 <= y holds
z9 <= z
let z9 be Element of (LattPOSet L); ::_thesis: ( z9 <= x & z9 <= y implies z9 <= z )
A13: (% z9) % = % z9 ;
assume that
A14: z9 <= x and
A15: z9 <= y ; ::_thesis: z9 <= z
A16: % z9 [= % x by A11, A13, A14, Th7;
% z9 [= % y by A12, A13, A15, Th7;
then % z9 [= (% x) "/\" (% y) by A16, FILTER_0:7;
hence z9 <= z by A13, Th7; ::_thesis: verum
end;
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 & ( 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 V58() reflexive transitive antisymmetric complete for RelStr ;
existence
ex b1 being Poset st
( b1 is strict & b1 is complete & not b1 is empty )
proof
set s = the set ;
set D = { the set };
set R = the Order of { the set };
take A = RelStr(# { the set }, the Order of { the set } #); ::_thesis: ( A is strict & A is complete & not A is empty )
thus A is strict ; ::_thesis: ( A is complete & not A is empty )
hereby :: according to LATTICE3:def_12 ::_thesis: not A is empty
let X be set ; ::_thesis: ex s being Element of A st
( X is_<=_than s & ( for b being Element of A st X is_<=_than b holds
s <= b ) )
reconsider s = the set as Element of A by TARSKI:def_1;
take s = s; ::_thesis: ( X is_<=_than s & ( for b being Element of A st X is_<=_than b holds
s <= b ) )
thus X is_<=_than s ::_thesis: for b being Element of A st X is_<=_than b holds
s <= b
proof
let a be Element of A; :: according to LATTICE3:def_9 ::_thesis: ( a in X implies a <= s )
assume a in X ; ::_thesis: a <= s
thus a <= s by TARSKI:def_1; ::_thesis: verum
end;
let b be Element of A; ::_thesis: ( X is_<=_than b implies s <= b )
assume X is_<=_than b ; ::_thesis: s <= b
thus s <= b by TARSKI:def_1; ::_thesis: verum
end;
thus not A is empty ; ::_thesis: verum
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
let A be non empty RelStr ; ::_thesis: ( A is complete implies ( A is with_suprema & A is with_infima ) )
assume A1: for X being set ex a being Element of A st
( X is_<=_than a & ( for b being Element of A st X is_<=_than b holds
a <= b ) ) ; :: according to LATTICE3:def_12 ::_thesis: ( A is with_suprema & A is with_infima )
thus A is with_suprema ::_thesis: A is with_infima
proof
let a be Element of A; :: according to LATTICE3:def_10 ::_thesis: for y being Element of A ex z being Element of A st
( a <= z & y <= z & ( for z9 being Element of A st a <= z9 & y <= z9 holds
z <= z9 ) )
let b be Element of A; ::_thesis: ex z being Element of A st
( a <= z & b <= z & ( for z9 being Element of A st a <= z9 & b <= z9 holds
z <= z9 ) )
consider c being Element of A such that
A2: {a,b} is_<=_than c and
A3: for c9 being Element of A st {a,b} is_<=_than c9 holds
c <= c9 by A1;
take c ; ::_thesis: ( a <= c & b <= c & ( for z9 being Element of A st a <= z9 & b <= z9 holds
c <= z9 ) )
A4: a in {a,b} by TARSKI:def_2;
b in {a,b} by TARSKI:def_2;
hence ( a <= c & b <= c ) by A2, A4, Def9; ::_thesis: for z9 being Element of A st a <= z9 & b <= z9 holds
c <= z9
let c9 be Element of A; ::_thesis: ( a <= c9 & b <= c9 implies c <= c9 )
assume that
A5: a <= c9 and
A6: b <= c9 ; ::_thesis: c <= c9
{a,b} is_<=_than c9
proof
let d be Element of A; :: according to LATTICE3:def_9 ::_thesis: ( d in {a,b} implies d <= c9 )
assume d in {a,b} ; ::_thesis: d <= c9
hence d <= c9 by A5, A6, TARSKI:def_2; ::_thesis: verum
end;
hence c <= c9 by A3; ::_thesis: verum
end;
let a be Element of A; :: according to LATTICE3:def_11 ::_thesis: for y being Element of A ex z being Element of A st
( z <= a & z <= y & ( for z9 being Element of A st z9 <= a & z9 <= y holds
z9 <= z ) )
let b be Element of A; ::_thesis: ex z being Element of A st
( z <= a & z <= b & ( for z9 being Element of A st z9 <= a & z9 <= b holds
z9 <= z ) )
set X = { c where c is Element of A : ( c <= a & c <= b ) } ;
consider c being Element of A such that
A7: { c where c is Element of A : ( c <= a & c <= b ) } is_<=_than c and
A8: for c9 being Element of A st { c where c is Element of A : ( c <= a & c <= b ) } is_<=_than c9 holds
c <= c9 by A1;
take c ; ::_thesis: ( c <= a & c <= b & ( for z9 being Element of A st z9 <= a & z9 <= b holds
z9 <= c ) )
{ c where c is Element of A : ( c <= a & c <= b ) } is_<=_than a
proof
let c be Element of A; :: according to LATTICE3:def_9 ::_thesis: ( c in { c where c is Element of A : ( c <= a & c <= b ) } implies c <= a )
assume c in { c where c is Element of A : ( c <= a & c <= b ) } ; ::_thesis: c <= a
then ex c9 being Element of A st
( c = c9 & c9 <= a & c9 <= b ) ;
hence c <= a ; ::_thesis: verum
end;
hence c <= a by A8; ::_thesis: ( c <= b & ( for z9 being Element of A st z9 <= a & z9 <= b holds
z9 <= c ) )
{ c where c is Element of A : ( c <= a & c <= b ) } is_<=_than b
proof
let c be Element of A; :: according to LATTICE3:def_9 ::_thesis: ( c in { c where c is Element of A : ( c <= a & c <= b ) } implies c <= b )
assume c in { c where c is Element of A : ( c <= a & c <= b ) } ; ::_thesis: c <= b
then ex c9 being Element of A st
( c = c9 & c9 <= a & c9 <= b ) ;
hence c <= b ; ::_thesis: verum
end;
hence c <= b by A8; ::_thesis: for z9 being Element of A st z9 <= a & z9 <= b holds
z9 <= c
let c9 be Element of A; ::_thesis: ( c9 <= a & c9 <= b implies c9 <= c )
assume that
A9: c9 <= a and
A10: c9 <= b ; ::_thesis: c9 <= c
c9 in { c where c is Element of A : ( c <= a & c <= b ) } by A9, A10;
hence c9 <= c by A7, Def9; ::_thesis: verum
end;
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 & b1 is with_suprema & b1 is with_infima & b1 is strict & not b1 is empty )
proof
set A = the non empty strict complete Poset;
take the non empty strict complete Poset ; ::_thesis: ( the non empty strict complete Poset is complete & the non empty strict complete Poset is with_suprema & the non empty strict complete Poset is with_infima & the non empty strict complete Poset is strict & not the non empty strict complete Poset is empty )
thus ( the non empty strict complete Poset is complete & the non empty strict complete Poset is with_suprema & the non empty strict complete Poset is with_infima & the non empty strict complete Poset is strict & not the non empty strict complete Poset is empty ) by Th12; ::_thesis: verum
end;
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 & b <= x & ( for c being Element of A st a <= c & b <= c holds
x <= c ) ) ;
funca "\/" 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 B2;
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
let c1, c2 be Element of A; ::_thesis: ( a <= c1 & b <= c1 & ( for c being Element of A st a <= c & b <= c holds
c1 <= c ) & a <= c2 & b <= c2 & ( for c being Element of A st a <= c & b <= c holds
c2 <= c ) implies c1 = c2 )
assume that
A1: a <= c1 and
A2: b <= c1 and
A3: for c being Element of A st a <= c & b <= c holds
c1 <= c and
A4: a <= c2 and
A5: b <= c2 and
A6: for c being Element of A st a <= c & b <= c holds
c2 <= c ; ::_thesis: c1 = c2
A7: c1 <= c2 by A3, A4, A5;
c2 <= c1 by A1, A2, A6;
hence c1 = c2 by B1, A7, ORDERS_2:2; ::_thesis: verum
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 B1: A is antisymmetric ;
let a, b be Element of A;
assume B2: 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 ) ) ;
funca "/\" 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 B2;
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
let c1, c2 be Element of A; ::_thesis: ( c1 <= a & c1 <= b & ( for c being Element of A st c <= a & c <= b holds
c <= c1 ) & c2 <= a & c2 <= b & ( for c being Element of A st c <= a & c <= b holds
c <= c2 ) implies c1 = c2 )
assume that
A1: c1 <= a and
A2: c1 <= b and
A3: for c being Element of A st c <= a & c <= b holds
c <= c1 and
A4: c2 <= a and
A5: c2 <= b and
A6: for c being Element of A st c <= a & c <= b holds
c <= c2 ; ::_thesis: c1 = c2
A7: c1 <= c2 by A1, A2, A6;
c2 <= c1 by A3, A4, A5;
hence c1 = c2 by B1, A7, ORDERS_2:2; ::_thesis: verum
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
let V be antisymmetric with_suprema RelStr ; ::_thesis: for u1, u2 being Element of V holds u1 "\/" u2 = u2 "\/" u1
let u1, u2 be Element of V; ::_thesis: u1 "\/" u2 = u2 "\/" u1
A1: u1 <= u1 "\/" u2 by Lm1;
A2: u2 <= u1 "\/" u2 by Lm1;
for u3 being Element of V st u2 <= u3 & u1 <= u3 holds
u1 "\/" u2 <= u3 by Lm1;
hence u1 "\/" u2 = u2 "\/" u1 by A1, A2, Def13; ::_thesis: verum
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
let V be antisymmetric with_suprema RelStr ; ::_thesis: for u1, u2, u3 being Element of V st V is transitive holds
(u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3)
let u1, u2, u3 be Element of V; ::_thesis: ( V is transitive implies (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3) )
assume A1: V is transitive ; ::_thesis: (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3)
A2: u1 <= u1 "\/" u2 by Lm1;
A3: u2 <= u1 "\/" u2 by Lm1;
A4: u2 <= u2 "\/" u3 by Lm1;
A5: u3 <= u2 "\/" u3 by Lm1;
A6: u1 "\/" u2 <= (u1 "\/" u2) "\/" u3 by Lm1;
A7: u3 <= (u1 "\/" u2) "\/" u3 by Lm1;
A8: u1 <= (u1 "\/" u2) "\/" u3 by A1, A2, A6, ORDERS_2:3;
u2 <= (u1 "\/" u2) "\/" u3 by A1, A3, A6, ORDERS_2:3;
then A9: u2 "\/" u3 <= (u1 "\/" u2) "\/" u3 by A7, Lm1;
now__::_thesis:_for_u4_being_Element_of_V_st_u1_<=_u4_&_u2_"\/"_u3_<=_u4_holds_
(u1_"\/"_u2)_"\/"_u3_<=_u4
let u4 be Element of V; ::_thesis: ( u1 <= u4 & u2 "\/" u3 <= u4 implies (u1 "\/" u2) "\/" u3 <= u4 )
assume that
A10: u1 <= u4 and
A11: u2 "\/" u3 <= u4 ; ::_thesis: (u1 "\/" u2) "\/" u3 <= u4
A12: u2 <= u4 by A1, A4, A11, ORDERS_2:3;
A13: u3 <= u4 by A1, A5, A11, ORDERS_2:3;
u1 "\/" u2 <= u4 by A10, A12, Lm1;
hence (u1 "\/" u2) "\/" u3 <= u4 by A13, Lm1; ::_thesis: verum
end;
hence (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3) by A8, A9, Def13; ::_thesis: verum
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
let N be antisymmetric with_infima RelStr ; ::_thesis: for n1, n2 being Element of N holds n1 "/\" n2 = n2 "/\" n1
let n1, n2 be Element of N; ::_thesis: n1 "/\" n2 = n2 "/\" n1
A1: n1 "/\" n2 <= n1 by Lm2;
A2: n1 "/\" n2 <= n2 by Lm2;
for n3 being Element of N st n3 <= n2 & n3 <= n1 holds
n3 <= n1 "/\" n2 by Lm2;
hence n1 "/\" n2 = n2 "/\" n1 by A1, A2, Def14; ::_thesis: verum
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
let N be antisymmetric with_infima RelStr ; ::_thesis: for n1, n2, n3 being Element of N st N is transitive holds
(n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3)
let n1, n2, n3 be Element of N; ::_thesis: ( N is transitive implies (n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3) )
assume A1: N is transitive ; ::_thesis: (n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3)
A2: n1 "/\" n2 <= n1 by Lm2;
A3: n1 "/\" n2 <= n2 by Lm2;
A4: n2 "/\" n3 <= n2 by Lm2;
A5: n2 "/\" n3 <= n3 by Lm2;
A6: (n1 "/\" n2) "/\" n3 <= n1 "/\" n2 by Lm2;
A7: (n1 "/\" n2) "/\" n3 <= n3 by Lm2;
A8: (n1 "/\" n2) "/\" n3 <= n1 by A1, A2, A6, ORDERS_2:3;
(n1 "/\" n2) "/\" n3 <= n2 by A1, A3, A6, ORDERS_2:3;
then A9: (n1 "/\" n2) "/\" n3 <= n2 "/\" n3 by A7, Lm2;
now__::_thesis:_for_n4_being_Element_of_N_st_n4_<=_n1_&_n4_<=_n2_"/\"_n3_holds_
n4_<=_(n1_"/\"_n2)_"/\"_n3
let n4 be Element of N; ::_thesis: ( n4 <= n1 & n4 <= n2 "/\" n3 implies n4 <= (n1 "/\" n2) "/\" n3 )
assume that
A10: n4 <= n1 and
A11: n4 <= n2 "/\" n3 ; ::_thesis: n4 <= (n1 "/\" n2) "/\" n3
A12: n4 <= n2 by A1, A4, A11, ORDERS_2:3;
A13: n4 <= n3 by A1, A5, A11, ORDERS_2:3;
n4 <= n1 "/\" n2 by A10, A12, Lm2;
hence n4 <= (n1 "/\" n2) "/\" n3 by A13, Lm2; ::_thesis: verum
end;
hence (n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3) by A8, A9, Def14; ::_thesis: verum
end;
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
proof
let K be reflexive antisymmetric with_suprema with_infima RelStr ; ::_thesis: for k1, k2 being Element of K holds (k1 "/\" k2) "\/" k2 = k2
let k1, k2 be Element of K; ::_thesis: (k1 "/\" k2) "\/" k2 = k2
A1: k1 "/\" k2 <= k2 by Lm2;
A2: k2 <= k2 ;
for k3 being Element of K st k1 "/\" k2 <= k3 & k2 <= k3 holds
k2 <= k3 ;
hence (k1 "/\" k2) "\/" k2 = k2 by A1, A2, Def13; ::_thesis: verum
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
let K be reflexive antisymmetric with_suprema with_infima RelStr ; ::_thesis: for k1, k2 being Element of K holds k1 "/\" (k1 "\/" k2) = k1
let k1, k2 be Element of K; ::_thesis: k1 "/\" (k1 "\/" k2) = k1
A1: k1 <= k1 ;
A2: k1 <= k1 "\/" k2 by Lm1;
for k3 being Element of K st k3 <= k1 & k3 <= k1 "\/" k2 holds
k3 <= k1 ;
hence k1 "/\" (k1 "\/" k2) = k1 by A1, A2, Def14; ::_thesis: verum
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
let A be with_suprema with_infima Poset; ::_thesis: ex L being strict Lattice st RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet L
defpred S1[ Element of A, Element of A, set ] means for x9, y9 being Element of A st x9 = $1 & y9 = $2 holds
$3 = x9 "\/" y9;
A1: for x, y being Element of A ex u being Element of A st S1[x,y,u]
proof
let x, y be Element of A; ::_thesis: ex u being Element of A st S1[x,y,u]
reconsider x9 = x, y9 = y as Element of A ;
take x9 "\/" y9 ; ::_thesis: S1[x,y,x9 "\/" y9]
thus S1[x,y,x9 "\/" y9] ; ::_thesis: verum
end;
consider j being BinOp of the carrier of A such that
A2: for x, y being Element of A holds S1[x,y,j . (x,y)] from BINOP_1:sch_3(A1);
defpred S2[ Element of A, Element of A, set ] means for x9, y9 being Element of A st x9 = $1 & y9 = $2 holds
$3 = x9 "/\" y9;
A3: for x, y being Element of A ex u being Element of A st S2[x,y,u]
proof
let x, y be Element of A; ::_thesis: ex u being Element of A st S2[x,y,u]
reconsider x9 = x, y9 = y as Element of A ;
take x9 "/\" y9 ; ::_thesis: S2[x,y,x9 "/\" y9]
thus S2[x,y,x9 "/\" y9] ; ::_thesis: verum
end;
consider m being BinOp of the carrier of A such that
A4: for x, y being Element of A holds S2[x,y,m . (x,y)] from BINOP_1:sch_3(A3);
set L = LattStr(# the carrier of A,j,m #);
A5: now__::_thesis:_for_a,_b_being_Element_of_LattStr(#_the_carrier_of_A,j,m_#)_holds_a_"\/"_b_=_b_"\/"_a
let a, b be Element of LattStr(# the carrier of A,j,m #); ::_thesis: a "\/" b = b "\/" a
reconsider x = a, y = b as Element of A ;
j . (x,y) = x "\/" y by A2;
hence a "\/" b = b "\/" a by A2; ::_thesis: verum
end;
A6: now__::_thesis:_for_a,_b,_c_being_Element_of_LattStr(#_the_carrier_of_A,j,m_#)_holds_a_"\/"_(b_"\/"_c)_=_(a_"\/"_b)_"\/"_c
let a, b, c be Element of LattStr(# the carrier of A,j,m #); ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider x = a, y = b, z = c as Element of A ;
thus a "\/" (b "\/" c) = j . (x,(y "\/" z)) by A2
.= x "\/" (y "\/" z) by A2
.= (x "\/" y) "\/" z by Th14
.= j . ((x "\/" y),z) by A2
.= (a "\/" b) "\/" c by A2 ; ::_thesis: verum
end;
A7: now__::_thesis:_for_a,_b_being_Element_of_LattStr(#_the_carrier_of_A,j,m_#)_holds_(a_"/\"_b)_"\/"_b_=_b
let a, b be Element of LattStr(# the carrier of A,j,m #); ::_thesis: (a "/\" b) "\/" b = b
reconsider x = a, y = b as Element of A ;
thus (a "/\" b) "\/" b = j . ((x "/\" y),y) by A4
.= (x "/\" y) "\/" y by A2
.= b by Th17 ; ::_thesis: verum
end;
A8: now__::_thesis:_for_a,_b_being_Element_of_LattStr(#_the_carrier_of_A,j,m_#)_holds_a_"/\"_b_=_b_"/\"_a
let a, b be Element of LattStr(# the carrier of A,j,m #); ::_thesis: a "/\" b = b "/\" a
reconsider x = a, y = b as Element of A ;
m . (x,y) = x "/\" y by A4;
hence a "/\" b = b "/\" a by A4; ::_thesis: verum
end;
A9: now__::_thesis:_for_a,_b,_c_being_Element_of_LattStr(#_the_carrier_of_A,j,m_#)_holds_a_"/\"_(b_"/\"_c)_=_(a_"/\"_b)_"/\"_c
let a, b, c be Element of LattStr(# the carrier of A,j,m #); ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider x = a, y = b, z = c as Element of A ;
thus a "/\" (b "/\" c) = m . (x,(y "/\" z)) by A4
.= x "/\" (y "/\" z) by A4
.= (x "/\" y) "/\" z by Th16
.= m . ((x "/\" y),z) by A4
.= (a "/\" b) "/\" c by A4 ; ::_thesis: verum
end;
now__::_thesis:_for_a,_b_being_Element_of_LattStr(#_the_carrier_of_A,j,m_#)_holds_a_"/\"_(a_"\/"_b)_=_a
let a, b be Element of LattStr(# the carrier of A,j,m #); ::_thesis: a "/\" (a "\/" b) = a
reconsider x = a, y = b as Element of A ;
thus a "/\" (a "\/" b) = m . (x,(x "\/" y)) by A2
.= x "/\" (x "\/" y) by A4
.= a by Th18 ; ::_thesis: verum
end;
then ( LattStr(# the carrier of A,j,m #) is join-commutative & LattStr(# the carrier of A,j,m #) is join-associative & LattStr(# the carrier of A,j,m #) is meet-absorbing & LattStr(# the carrier of A,j,m #) is meet-commutative & LattStr(# the carrier of A,j,m #) is meet-associative & LattStr(# the carrier of A,j,m #) is join-absorbing ) by A5, A6, A7, A8, A9, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
then reconsider L = LattStr(# the carrier of A,j,m #) as strict Lattice ;
take L ; ::_thesis: RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet L
A10: LattRel L = { [p,q] where p, q is Element of L : p [= q } by FILTER_1:def_8;
LattRel L = the InternalRel of A
proof
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in LattRel L or [x,y] in the InternalRel of A ) & ( not [x,y] in the InternalRel of A or [x,y] in LattRel L ) )
thus ( [x,y] in LattRel L implies [x,y] in the InternalRel of A ) ::_thesis: ( not [x,y] in the InternalRel of A or [x,y] in LattRel L )
proof
assume [x,y] in LattRel L ; ::_thesis: [x,y] in the InternalRel of A
then consider p, q being Element of L such that
A11: [x,y] = [p,q] and
A12: p [= q by A10;
reconsider p9 = p, q9 = q as Element of A ;
p9 "\/" q9 = p "\/" q by A2
.= q by A12, LATTICES:def_3 ;
then p9 <= q9 by Lm1;
hence [x,y] in the InternalRel of A by A11, ORDERS_2:def_5; ::_thesis: verum
end;
assume A13: [x,y] in the InternalRel of A ; ::_thesis: [x,y] in LattRel L
then consider x1, x2 being set such that
A14: x1 in the carrier of A and
A15: x2 in the carrier of A and
A16: [x,y] = [x1,x2] by ZFMISC_1:84;
reconsider x1 = x1, x2 = x2 as Element of A by A14, A15;
reconsider y1 = x1, y2 = x2 as Element of L ;
A17: x1 <= x2 by A13, A16, ORDERS_2:def_5;
x2 <= x2 ;
then A18: x1 "\/" x2 <= x2 by A17, Lm1;
x2 <= x1 "\/" x2 by Lm1;
then x2 = x1 "\/" x2 by A18, ORDERS_2:2
.= y1 "\/" y2 by A2 ;
then y1 [= y2 by LATTICES:def_3;
hence [x,y] in LattRel L by A10, A16; ::_thesis: verum
end;
hence RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet L ; ::_thesis: verum
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
let L be Lattice; ::_thesis: ( (LattRel L) ~ = LattRel (L .:) & (LattPOSet L) ~ = LattPOSet (L .:) )
A1: LattRel L = { [p,q] where p, q is Element of L : p [= q } by FILTER_1:def_8;
A2: LattRel (L .:) = { [p9,q9] where p9, q9 is Element of (L .:) : p9 [= q9 } by FILTER_1:def_8;
A3: L .: = LattStr(# H1(L),H3(L),H2(L) #) by LATTICE2:def_2;
thus (LattRel L) ~ = LattRel (L .:) ::_thesis: (LattPOSet L) ~ = LattPOSet (L .:)
proof
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in (LattRel L) ~ or [x,y] in LattRel (L .:) ) & ( not [x,y] in LattRel (L .:) or [x,y] in (LattRel L) ~ ) )
thus ( [x,y] in (LattRel L) ~ implies [x,y] in LattRel (L .:) ) ::_thesis: ( not [x,y] in LattRel (L .:) or [x,y] in (LattRel L) ~ )
proof
assume [x,y] in (LattRel L) ~ ; ::_thesis: [x,y] in LattRel (L .:)
then [y,x] in LattRel L by RELAT_1:def_7;
then consider p, q being Element of L such that
A4: [y,x] = [p,q] and
A5: p [= q by A1;
reconsider p9 = p, q9 = q as Element of (L .:) by A3;
A6: x = q by A4, XTUPLE_0:1;
A7: y = p by A4, XTUPLE_0:1;
q9 [= p9 by A5, LATTICE2:38;
hence [x,y] in LattRel (L .:) by A2, A6, A7; ::_thesis: verum
end;
assume [x,y] in LattRel (L .:) ; ::_thesis: [x,y] in (LattRel L) ~
then consider p9, q9 being Element of (L .:) such that
A8: [x,y] = [p9,q9] and
A9: p9 [= q9 by A2;
reconsider p = p9, q = q9 as Element of L by A3;
A10: x = p by A8, XTUPLE_0:1;
A11: y = q by A8, XTUPLE_0:1;
q [= p by A9, LATTICE2:39;
then [y,x] in LattRel L by A1, A10, A11;
hence [x,y] in (LattRel L) ~ by RELAT_1:def_7; ::_thesis: verum
end;
hence (LattPOSet L) ~ = LattPOSet (L .:) by A3; ::_thesis: verum
end;
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 )
proof
let L be Lattice; ::_thesis: for p, q, r being Element of L holds
( p is_less_than {q,r} iff p [= q "/\" r )
let p, q, r be Element of L; ::_thesis: ( p is_less_than {q,r} iff p [= q "/\" r )
A1: q in {q,r} by TARSKI:def_2;
A2: r in {q,r} by TARSKI:def_2;
thus ( p is_less_than {q,r} implies p [= q "/\" r ) ::_thesis: ( p [= q "/\" r implies p is_less_than {q,r} )
proof
assume A3: p is_less_than {q,r} ; ::_thesis: p [= q "/\" r
then A4: p [= q by A1, Def16;
p [= r by A2, A3, Def16;
hence p [= q "/\" r by A4, FILTER_0:7; ::_thesis: verum
end;
assume A5: p [= q "/\" r ; ::_thesis: p is_less_than {q,r}
let a be Element of L; :: according to LATTICE3:def_16 ::_thesis: ( a in {q,r} implies p [= a )
assume a in {q,r} ; ::_thesis: p [= a
then A6: ( a = q or a = r ) by TARSKI:def_2;
A7: q "/\" r [= q by LATTICES:6;
r "/\" q [= r by LATTICES:6;
hence p [= a by A5, A6, A7, LATTICES:7; ::_thesis: verum
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
let L be Lattice; ::_thesis: for p, q, r being Element of L holds
( p is_greater_than {q,r} iff q "\/" r [= p )
let p, q, r be Element of L; ::_thesis: ( p is_greater_than {q,r} iff q "\/" r [= p )
A1: q in {q,r} by TARSKI:def_2;
A2: r in {q,r} by TARSKI:def_2;
thus ( p is_greater_than {q,r} implies q "\/" r [= p ) ::_thesis: ( q "\/" r [= p implies p is_greater_than {q,r} )
proof
assume A3: p is_greater_than {q,r} ; ::_thesis: q "\/" r [= p
then A4: q [= p by A1, Def17;
r [= p by A2, A3, Def17;
hence q "\/" r [= p by A4, FILTER_0:6; ::_thesis: verum
end;
assume A5: q "\/" r [= p ; ::_thesis: p is_greater_than {q,r}
let a be Element of L; :: according to LATTICE3:def_17 ::_thesis: ( a in {q,r} implies a [= p )
assume a in {q,r} ; ::_thesis: a [= p
then A6: ( a = q or a = r ) by TARSKI:def_2;
A7: q [= q "\/" r by LATTICES:5;
r [= r "\/" q by LATTICES:5;
hence a [= p by A5, A6, A7, LATTICES:7; ::_thesis: verum
end;
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 & ( 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 & ( 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;
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 & ( 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 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 & ( 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
let X be set ; ::_thesis: 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 ` )
let B be B_Lattice; ::_thesis: 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 ` )
let a be Element of B; ::_thesis: ( X is_less_than a iff { (b `) where b is Element of B : b in X } is_greater_than a ` )
set Y = { (b `) where b is Element of B : b in X } ;
thus ( X is_less_than a implies { (b `) where b is Element of B : b in X } is_greater_than a ` ) ::_thesis: ( { (b `) where b is Element of B : b in X } is_greater_than a ` implies X is_less_than a )
proof
assume A1: for b being Element of B st b in X holds
b [= a ; :: according to LATTICE3:def_17 ::_thesis: { (b `) where b is Element of B : b in X } is_greater_than a `
let b be Element of B; :: according to LATTICE3:def_16 ::_thesis: ( b in { (b `) where b is Element of B : b in X } implies a ` [= b )
assume b in { (b `) where b is Element of B : b in X } ; ::_thesis: a ` [= b
then ex c being Element of B st
( b = c ` & c in X ) ;
hence a ` [= b by A1, LATTICES:26; ::_thesis: verum
end;
assume A2: for b being Element of B st b in { (b `) where b is Element of B : b in X } holds
a ` [= b ; :: according to LATTICE3:def_16 ::_thesis: X is_less_than a
let b be Element of B; :: according to LATTICE3:def_17 ::_thesis: ( b in X implies b [= a )
assume b in X ; ::_thesis: b [= a
then A3: b ` in { (b `) where b is Element of B : b in X } ;
A4: (a `) ` = a ;
(b `) ` = b ;
hence b [= a by A2, A3, A4, LATTICES:26; ::_thesis: verum
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
let X be set ; ::_thesis: 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 ` )
let B be B_Lattice; ::_thesis: 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 ` )
let a be Element of B; ::_thesis: ( X is_greater_than a iff { (b `) where b is Element of B : b in X } is_less_than a ` )
set Y = { (b `) where b is Element of B : b in X } ;
thus ( X is_greater_than a implies { (b `) where b is Element of B : b in X } is_less_than a ` ) ::_thesis: ( { (b `) where b is Element of B : b in X } is_less_than a ` implies X is_greater_than a )
proof
assume A1: for b being Element of B st b in X holds
a [= b ; :: according to LATTICE3:def_16 ::_thesis: { (b `) where b is Element of B : b in X } is_less_than a `
let b be Element of B; :: according to LATTICE3:def_17 ::_thesis: ( b in { (b `) where b is Element of B : b in X } implies b [= a ` )
assume b in { (b `) where b is Element of B : b in X } ; ::_thesis: b [= a `
then ex c being Element of B st
( b = c ` & c in X ) ;
hence b [= a ` by A1, LATTICES:26; ::_thesis: verum
end;
assume A2: for b being Element of B st b in { (b `) where b is Element of B : b in X } holds
b [= a ` ; :: according to LATTICE3:def_17 ::_thesis: X is_greater_than a
let b be Element of B; :: according to LATTICE3:def_16 ::_thesis: ( b in X implies a [= b )
assume b in X ; ::_thesis: a [= b
then A3: b ` in { (b `) where b is Element of B : b in X } ;
A4: (a `) ` = a ;
(b `) ` = b ;
hence a [= b by A2, A3, A4, LATTICES:26; ::_thesis: verum
end;
theorem Th25: :: LATTICE3:25
for X being set holds BooleLatt X is complete
proof
let X be set ; ::_thesis: BooleLatt X is complete
set B = BooleLatt X;
let x be set ; :: according to LATTICE3:def_18 ::_thesis: ex p being Element of (BooleLatt X) st
( x is_less_than p & ( for r being Element of (BooleLatt X) st x is_less_than r holds
p [= r ) )
set p = union (x /\ (bool X));
A1: H1( BooleLatt X) = bool X by Def1;
reconsider p = union (x /\ (bool X)) as Element of (BooleLatt X) by Def1;
take p ; ::_thesis: ( x is_less_than p & ( for r being Element of (BooleLatt X) st x is_less_than r holds
p [= r ) )
thus x is_less_than p ::_thesis: for r being Element of (BooleLatt X) st x is_less_than r holds
p [= r
proof
let q be Element of (BooleLatt X); :: according to LATTICE3:def_17 ::_thesis: ( q in x implies q [= p )
assume q in x ; ::_thesis: q [= p
then q in x /\ (bool X) by A1, XBOOLE_0:def_4;
then q c= p by ZFMISC_1:74;
hence q [= p by Th2; ::_thesis: verum
end;
let r be Element of (BooleLatt X); ::_thesis: ( x is_less_than r implies p [= r )
assume A2: for q being Element of (BooleLatt X) st q in x holds
q [= r ; :: according to LATTICE3:def_17 ::_thesis: p [= r
now__::_thesis:_for_z_being_set_st_z_in_x_/\_(bool_X)_holds_
z_c=_r
let z be set ; ::_thesis: ( z in x /\ (bool X) implies z c= r )
assume A3: z in x /\ (bool X) ; ::_thesis: z c= r
then A4: z in x by XBOOLE_0:def_4;
reconsider z9 = z as Element of (BooleLatt X) by A1, A3;
z9 [= r by A2, A4;
hence z c= r by Th2; ::_thesis: verum
end;
then p c= r by ZFMISC_1:76;
hence p [= r by Th2; ::_thesis: verum
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
let X be set ; ::_thesis: BooleLatt X is \/-distributive
let x be set ; :: according to LATTICE3:def_19 ::_thesis: for a, b, c being Element of (BooleLatt X) st x is_less_than a & ( for d being Element of (BooleLatt X) st x is_less_than d holds
a [= d ) & { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_less_than c & ( for d being Element of (BooleLatt X) st { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_less_than d holds
c [= d ) holds
b "/\" a [= c
set B = BooleLatt X;
let a, b, c be Element of (BooleLatt X); ::_thesis: ( x is_less_than a & ( for d being Element of (BooleLatt X) st x is_less_than d holds
a [= d ) & { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_less_than c & ( for d being Element of (BooleLatt X) st { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_less_than d holds
c [= d ) implies b "/\" a [= c )
assume that
A1: x is_less_than a and
A2: for d being Element of (BooleLatt X) st x is_less_than d holds
a [= d and
A3: { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_less_than c and
A4: for d being Element of (BooleLatt X) st { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_less_than d holds
c [= d ; ::_thesis: b "/\" a [= c
set Y = { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } ;
A5: H1( BooleLatt X) = bool X by Def1;
A6: { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } c= bool X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } or z in bool X )
assume z in { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } ; ::_thesis: z in bool X
then ex a9 being Element of (BooleLatt X) st
( z = b "/\" a9 & a9 in x ) ;
hence z in bool X by A5; ::_thesis: verum
end;
A7: union { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } c= union (bool X) by A6, ZFMISC_1:77;
union (bool X) = X by ZFMISC_1:81;
then reconsider p = union (x /\ (bool X)), q = union { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } as Element of (BooleLatt X) by A7, Def1;
now__::_thesis:_for_y_being_set_st_y_in_x_/\_(bool_X)_holds_
y_c=_a
let y be set ; ::_thesis: ( y in x /\ (bool X) implies y c= a )
assume A8: y in x /\ (bool X) ; ::_thesis: y c= a
then A9: y in x by XBOOLE_0:def_4;
reconsider y9 = y as Element of (BooleLatt X) by A5, A8;
y9 [= a by A1, A9, Def17;
hence y c= a by Th2; ::_thesis: verum
end;
then A10: p c= a by ZFMISC_1:76;
A11: x is_less_than p
proof
let q be Element of (BooleLatt X); :: according to LATTICE3:def_17 ::_thesis: ( q in x implies q [= p )
assume q in x ; ::_thesis: q [= p
then q in x /\ (bool X) by A5, XBOOLE_0:def_4;
then q c= p by ZFMISC_1:74;
hence q [= p by Th2; ::_thesis: verum
end;
A12: p [= a by A10, Th2;
a [= p by A2, A11;
then A13: a = p by A12, LATTICES:8;
now__::_thesis:_for_y_being_set_st_y_in__{__(b_"/\"_a9)_where_a9_is_Element_of_(BooleLatt_X)_:_a9_in_x__}__holds_
y_c=_c
let y be set ; ::_thesis: ( y in { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } implies y c= c )
assume A14: y in { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } ; ::_thesis: y c= c
then consider a9 being Element of (BooleLatt X) such that
A15: y = b "/\" a9 and
a9 in x ;
b "/\" a9 [= c by A3, A14, A15, Def17;
hence y c= c by A15, Th2; ::_thesis: verum
end;
then A16: q c= c by ZFMISC_1:76;
A17: { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_less_than q
proof
let p be Element of (BooleLatt X); :: according to LATTICE3:def_17 ::_thesis: ( p in { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } implies p [= q )
assume p in { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } ; ::_thesis: p [= q
then p c= q by ZFMISC_1:74;
hence p [= q by Th2; ::_thesis: verum
end;
A18: q [= c by A16, Th2;
c [= q by A4, A17;
then A19: c = q by A18, LATTICES:8;
b /\ a c= c
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in b /\ a or z in c )
assume A20: z in b /\ a ; ::_thesis: z in c
then A21: z in b by XBOOLE_0:def_4;
z in a by A20, XBOOLE_0:def_4;
then consider y being set such that
A22: z in y and
A23: y in x /\ (bool X) by A13, TARSKI:def_4;
A24: y in x by A23, XBOOLE_0:def_4;
reconsider y = y as Element of (BooleLatt X) by A5, A23;
A25: b "/\" y in { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } by A24;
z in b /\ y by A21, A22, XBOOLE_0:def_4;
hence z in c by A19, A25, TARSKI:def_4; ::_thesis: verum
end;
hence b "/\" a [= c by Th2; ::_thesis: verum
end;
theorem Th27: :: LATTICE3:27
for X being set holds BooleLatt X is /\-distributive
proof
let X be set ; ::_thesis: BooleLatt X is /\-distributive
let x be set ; :: according to LATTICE3:def_20 ::_thesis: for a, b, c being Element of (BooleLatt X) st x is_greater_than a & ( for d being Element of (BooleLatt X) st x is_greater_than d holds
d [= a ) & { (b "\/" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_greater_than c & ( for d being Element of (BooleLatt X) st { (b "\/" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_greater_than d holds
d [= c ) holds
c [= b "\/" a
set B = BooleLatt X;
let a, b, c be Element of (BooleLatt X); ::_thesis: ( x is_greater_than a & ( for d being Element of (BooleLatt X) st x is_greater_than d holds
d [= a ) & { (b "\/" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_greater_than c & ( for d being Element of (BooleLatt X) st { (b "\/" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_greater_than d holds
d [= c ) implies c [= b "\/" a )
assume that
A1: x is_greater_than a and
A2: for d being Element of (BooleLatt X) st x is_greater_than d holds
d [= a and
A3: { (b "\/" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_greater_than c and
A4: for d being Element of (BooleLatt X) st { (b "\/" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_greater_than d holds
d [= c ; ::_thesis: c [= b "\/" a
set x9 = { (e `) where e is Element of (BooleLatt X) : e in x } ;
set y = { (b "\/" e) where e is Element of (BooleLatt X) : e in x } ;
set y9 = { (e `) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } ;
set z = { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } ;
A5: { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } = { (e `) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } }
proof
thus { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } c= { (e `) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } :: according to XBOOLE_0:def_10 ::_thesis: { (e `) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } c= { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } }
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } or s in { (e `) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } )
assume s in { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } ; ::_thesis: s in { (e `) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } }
then consider e being Element of (BooleLatt X) such that
A6: s = (b `) "/\" e and
A7: e in { (e `) where e is Element of (BooleLatt X) : e in x } ;
consider i being Element of (BooleLatt X) such that
A8: e = i ` and
A9: i in x by A7;
A10: b "\/" i in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } by A9;
(b "\/" i) ` = s by A6, A8, LATTICES:24;
hence s in { (e `) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } by A10; ::_thesis: verum
end;
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in { (e `) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } or s in { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } )
assume s in { (e `) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } ; ::_thesis: s in { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } }
then consider e being Element of (BooleLatt X) such that
A11: s = e ` and
A12: e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } ;
consider i being Element of (BooleLatt X) such that
A13: e = b "\/" i and
A14: i in x by A12;
A15: i ` in { (e `) where e is Element of (BooleLatt X) : e in x } by A14;
s = (b `) "/\" (i `) by A11, A13, LATTICES:24;
hence s in { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } by A15; ::_thesis: verum
end;
A18: (c `) ` = c ;
A19: { (e `) where e is Element of (BooleLatt X) : e in x } is_less_than a ` by A1, Th24;
A20: for d being Element of (BooleLatt X) st { (e `) where e is Element of (BooleLatt X) : e in x } is_less_than d holds
a ` [= d
proof
let d be Element of (BooleLatt X); ::_thesis: ( { (e `) where e is Element of (BooleLatt X) : e in x } is_less_than d implies a ` [= d )
A21: (d `) ` = d ;
assume { (e `) where e is Element of (BooleLatt X) : e in x } is_less_than d ; ::_thesis: a ` [= d
then x is_greater_than d ` by A21, Th24;
hence a ` [= d by A2, A21, LATTICES:26; ::_thesis: verum
end;
A22: { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } is_less_than c ` by A3, A5, Th24;
A23: for d being Element of (BooleLatt X) st { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } is_less_than d holds
c ` [= d
proof
let d be Element of (BooleLatt X); ::_thesis: ( { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } is_less_than d implies c ` [= d )
A24: (d `) ` = d ;
assume { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } is_less_than d ; ::_thesis: c ` [= d
then { (b "\/" e) where e is Element of (BooleLatt X) : e in x } is_greater_than d ` by A5, A24, Th24;
hence c ` [= d by A4, A24, LATTICES:26; ::_thesis: verum
end;
BooleLatt X is \/-distributive by Th26;
then A25: (b `) "/\" (a `) [= c ` by A19, A20, A22, A23, Def19;
((b `) "/\" (a `)) ` = ((b `) `) "\/" ((a `) `) by LATTICES:23;
hence c [= b "\/" a by A18, A25, LATTICES:26; ::_thesis: verum
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
set X = the set ;
( BooleLatt the set is complete & BooleLatt the set is \/-distributive & BooleLatt the set is /\-distributive ) by Th26, Th27;
hence ex b1 being Lattice st
( b1 is complete & b1 is \/-distributive & b1 is /\-distributive & b1 is strict ) ; ::_thesis: verum
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
let X be set ; ::_thesis: for L being Lattice
for p being Element of L holds
( p is_less_than X iff p % is_<=_than X )
let L be Lattice; ::_thesis: for p being Element of L holds
( p is_less_than X iff p % is_<=_than X )
let p be Element of L; ::_thesis: ( p is_less_than X iff p % is_<=_than X )
thus ( p is_less_than X implies p % is_<=_than X ) ::_thesis: ( p % is_<=_than X implies p is_less_than X )
proof
assume A1: for q being Element of L st q in X holds
p [= q ; :: according to LATTICE3:def_16 ::_thesis: p % is_<=_than X
let p9 be Element of (LattPOSet L); :: according to LATTICE3:def_8 ::_thesis: ( p9 in X implies p % <= p9 )
A2: (% p9) % = % p9 ;
assume p9 in X ; ::_thesis: p % <= p9
then p [= % p9 by A1;
hence p % <= p9 by A2, Th7; ::_thesis: verum
end;
assume A3: for q9 being Element of (LattPOSet L) st q9 in X holds
p % <= q9 ; :: according to LATTICE3:def_8 ::_thesis: p is_less_than X
let q be Element of L; :: according to LATTICE3:def_16 ::_thesis: ( q in X implies p [= q )
assume q in X ; ::_thesis: p [= q
then p % <= q % by A3;
hence p [= q by Th7; ::_thesis: verum
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
let X be set ; ::_thesis: for L being Lattice
for p9 being Element of (LattPOSet L) holds
( p9 is_<=_than X iff % p9 is_less_than X )
let L be Lattice; ::_thesis: for p9 being Element of (LattPOSet L) holds
( p9 is_<=_than X iff % p9 is_less_than X )
let p9 be Element of (LattPOSet L); ::_thesis: ( p9 is_<=_than X iff % p9 is_less_than X )
(% p9) % = % p9 ;
hence ( p9 is_<=_than X iff % p9 is_less_than X ) by Th28; ::_thesis: verum
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
let X be set ; ::_thesis: for L being Lattice
for p being Element of L holds
( X is_less_than p iff X is_<=_than p % )
let L be Lattice; ::_thesis: for p being Element of L holds
( X is_less_than p iff X is_<=_than p % )
let p be Element of L; ::_thesis: ( X is_less_than p iff X is_<=_than p % )
thus ( X is_less_than p implies X is_<=_than p % ) ::_thesis: ( X is_<=_than p % implies X is_less_than p )
proof
assume A1: for q being Element of L st q in X holds
q [= p ; :: according to LATTICE3:def_17 ::_thesis: X is_<=_than p %
let p9 be Element of (LattPOSet L); :: according to LATTICE3:def_9 ::_thesis: ( p9 in X implies p9 <= p % )
A2: (% p9) % = % p9 ;
assume p9 in X ; ::_thesis: p9 <= p %
then % p9 [= p by A1;
hence p9 <= p % by A2, Th7; ::_thesis: verum
end;
assume A3: for q9 being Element of (LattPOSet L) st q9 in X holds
q9 <= p % ; :: according to LATTICE3:def_9 ::_thesis: X is_less_than p
let q be Element of L; :: according to LATTICE3:def_17 ::_thesis: ( q in X implies q [= p )
assume q in X ; ::_thesis: q [= p
then q % <= p % by A3;
hence q [= p by Th7; ::_thesis: verum
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
let X be set ; ::_thesis: for L being Lattice
for p9 being Element of (LattPOSet L) holds
( X is_<=_than p9 iff X is_less_than % p9 )
let L be Lattice; ::_thesis: for p9 being Element of (LattPOSet L) holds
( X is_<=_than p9 iff X is_less_than % p9 )
let p9 be Element of (LattPOSet L); ::_thesis: ( X is_<=_than p9 iff X is_less_than % p9 )
(% p9) % = % p9 ;
hence ( X is_<=_than p9 iff X is_less_than % p9 ) by Th30; ::_thesis: verum
end;
registration
let A be non empty complete Poset;
cluster latt A -> strict complete ;
coherence
latt A is complete
proof
( A is with_suprema & A is with_infima ) by Th12;
then A1: RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet (latt A) by Def15;
set B = LattPOSet (latt A);
latt A is complete
proof
let X be set ; :: according to LATTICE3:def_18 ::_thesis: ex p being Element of (latt A) st
( X is_less_than p & ( for r being Element of (latt A) st X is_less_than r holds
p [= r ) )
consider a being Element of A such that
A2: X is_<=_than a and
A3: for b being Element of A st X is_<=_than b holds
a <= b by Def12;
reconsider a9 = a as Element of (LattPOSet (latt A)) by A1;
take p = % a9; ::_thesis: ( X is_less_than p & ( for r being Element of (latt A) st X is_less_than r holds
p [= r ) )
A4: p % = p ;
thus X is_less_than p ::_thesis: for r being Element of (latt A) st X is_less_than r holds
p [= r
proof
let q be Element of (latt A); :: according to LATTICE3:def_17 ::_thesis: ( q in X implies q [= p )
reconsider b = q as Element of A by A1;
assume q in X ; ::_thesis: q [= p
then b <= a by A2, Def9;
then [b,a] in the InternalRel of A by ORDERS_2:def_5;
then q % <= a9 by A1, ORDERS_2:def_5;
hence q [= p by A4, Th7; ::_thesis: verum
end;
let q be Element of (latt A); ::_thesis: ( X is_less_than q implies p [= q )
assume X is_less_than q ; ::_thesis: p [= q
then A5: X is_<=_than q % by Th30;
reconsider b = q % as Element of A by A1;
X is_<=_than b
proof
let c be Element of A; :: according to LATTICE3:def_9 ::_thesis: ( c in X implies c <= b )
reconsider c9 = c as Element of (LattPOSet (latt A)) by A1;
assume c in X ; ::_thesis: c <= b
then c9 <= q % by A5, Def9;
then [c,b] in the InternalRel of RelStr(# the carrier of A, the InternalRel of A #) by A1, ORDERS_2:def_5;
hence c <= b by ORDERS_2:def_5; ::_thesis: verum
end;
then a <= b by A3;
then [a,b] in the InternalRel of A by ORDERS_2:def_5;
then a9 <= q % by A1, ORDERS_2:def_5;
hence p [= q by A4, Th7; ::_thesis: verum
end;
hence latt A is complete ; ::_thesis: verum
end;
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 & ( 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 B1, 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
let p1, p2 be Element of L; ::_thesis: ( X is_less_than p1 & ( for r being Element of L st X is_less_than r holds
p1 [= r ) & X is_less_than p2 & ( for r being Element of L st X is_less_than r holds
p2 [= r ) implies p1 = p2 )
assume that
A1: X is_less_than p1 and
A2: for r being Element of L st X is_less_than r holds
p1 [= r and
A3: X is_less_than p2 and
A4: for r being Element of L st X is_less_than r holds
p2 [= r ; ::_thesis: p1 = p2
A5: p1 [= p2 by A2, A3;
p2 [= p1 by A1, A4;
hence p1 = p2 by B1, A5, LATTICES:8; ::_thesis: verum
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
let C be complete Lattice; ::_thesis: 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))
let a be Element of C; ::_thesis: for X being set holds "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) [= a "/\" ("\/" (X,C))
let X be set ; ::_thesis: "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) [= a "/\" ("\/" (X,C))
set Y = { (a "/\" b) where b is Element of C : b in X } ;
{ (a "/\" b) where b is Element of C : b in X } is_less_than a "/\" ("\/" (X,C))
proof
let c be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( c in { (a "/\" b) where b is Element of C : b in X } implies c [= a "/\" ("\/" (X,C)) )
assume c in { (a "/\" b) where b is Element of C : b in X } ; ::_thesis: c [= a "/\" ("\/" (X,C))
then consider b being Element of C such that
A1: c = a "/\" b and
A2: b in X ;
X is_less_than "\/" (X,C) by Def21;
then b [= "\/" (X,C) by A2, Def17;
hence c [= a "/\" ("\/" (X,C)) by A1, LATTICES:9; ::_thesis: verum
end;
hence "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) [= a "/\" ("\/" (X,C)) by Def21; ::_thesis: verum
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
let C be complete Lattice; ::_thesis: ( 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) )
thus ( C is \/-distributive implies 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) ) ::_thesis: ( ( 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) ) implies C is \/-distributive )
proof
assume A1: for X being set
for a, b, c being Element of C st X is_less_than a & ( for d being Element of C st X is_less_than d holds
a [= d ) & { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than c & ( for d being Element of C st { (b "/\" b9) where b9 is Element of C : b9 in X } is_less_than d holds
c [= d ) holds
b "/\" a [= c ; :: according to LATTICE3:def_19 ::_thesis: 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)
let X be set ; ::_thesis: for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C)
let a be Element of C; ::_thesis: a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C)
set Y = { (a "/\" b) where b is Element of C : b in X } ;
A2: X is_less_than "\/" (X,C) by Def21;
A3: for d being Element of C st X is_less_than d holds
"\/" (X,C) [= d by Def21;
A4: { (a "/\" b) where b is Element of C : b in X } is_less_than "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) by Def21;
for d being Element of C st { (a "/\" b) where b is Element of C : b in X } is_less_than d holds
"\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) [= d by Def21;
hence a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) by A1, A2, A3, A4; ::_thesis: verum
end;
assume A5: 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) ; ::_thesis: C is \/-distributive
let X be set ; :: according to LATTICE3:def_19 ::_thesis: for a, b, c being Element of C st X is_less_than a & ( for d being Element of C st X is_less_than d holds
a [= d ) & { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than c & ( for d being Element of C st { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than d holds
c [= d ) holds
b "/\" a [= c
let a, b, c be Element of C; ::_thesis: ( X is_less_than a & ( for d being Element of C st X is_less_than d holds
a [= d ) & { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than c & ( for d being Element of C st { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than d holds
c [= d ) implies b "/\" a [= c )
assume A6: ( X is_less_than a & ( for d being Element of C st X is_less_than d holds
a [= d ) & { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than c & ( for d being Element of C st { (b "/\" b9) where b9 is Element of C : b9 in X } is_less_than d holds
c [= d ) ) ; ::_thesis: b "/\" a [= c
then A7: a = "\/" (X,C) by Def21;
c = "\/" ( { (b "/\" a9) where a9 is Element of C : a9 in X } ,C) by A6, Def21;
hence b "/\" a [= c by A5, A7; ::_thesis: verum
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
let C be complete Lattice; ::_thesis: 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 ) ) )
let a be Element of C; ::_thesis: 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 ) ) )
let X be set ; ::_thesis: ( a = "/\" (X,C) iff ( a is_less_than X & ( for b being Element of C st b is_less_than X holds
b [= a ) ) )
set Y = { b where b is Element of C : b is_less_than X } ;
A1: ( a = "/\" (X,C) iff ( { b where b is Element of C : b is_less_than X } is_less_than a & ( for c being Element of C st { b where b is Element of C : b is_less_than X } is_less_than c holds
a [= c ) ) ) by Def21;
thus ( a = "/\" (X,C) implies ( a is_less_than X & ( for b being Element of C st b is_less_than X holds
b [= a ) ) ) ::_thesis: ( a is_less_than X & ( for b being Element of C st b is_less_than X holds
b [= a ) implies a = "/\" (X,C) )
proof
assume A2: a = "/\" (X,C) ; ::_thesis: ( a is_less_than X & ( for b being Element of C st b is_less_than X holds
b [= a ) )
then A3: { b where b is Element of C : b is_less_than X } is_less_than a by Def21;
thus a is_less_than X ::_thesis: for b being Element of C st b is_less_than X holds
b [= a
proof
let b be Element of C; :: according to LATTICE3:def_16 ::_thesis: ( b in X implies a [= b )
assume A4: b in X ; ::_thesis: a [= b
{ b where b is Element of C : b is_less_than X } is_less_than b
proof
let c be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( c in { b where b is Element of C : b is_less_than X } implies c [= b )
assume c in { b where b is Element of C : b is_less_than X } ; ::_thesis: c [= b
then ex d being Element of C st
( c = d & d is_less_than X ) ;
hence c [= b by A4, Def16; ::_thesis: verum
end;
hence a [= b by A2, Def21; ::_thesis: verum
end;
let b be Element of C; ::_thesis: ( b is_less_than X implies b [= a )
assume b is_less_than X ; ::_thesis: b [= a
then b in { b where b is Element of C : b is_less_than X } ;
hence b [= a by A3, Def17; ::_thesis: verum
end;
assume that
A5: a is_less_than X and
A6: for b being Element of C st b is_less_than X holds
b [= a ; ::_thesis: a = "/\" (X,C)
A7: { b where b is Element of C : b is_less_than X } is_less_than a
proof
let b be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( b in { b where b is Element of C : b is_less_than X } implies b [= a )
assume b in { b where b is Element of C : b is_less_than X } ; ::_thesis: b [= a
then ex c being Element of C st
( b = c & c is_less_than X ) ;
hence b [= a by A6; ::_thesis: verum
end;
a in { b where b is Element of C : b is_less_than X } by A5;
hence a = "/\" (X,C) by A1, A7, Def17; ::_thesis: verum
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
let C be complete Lattice; ::_thesis: 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)
let a be Element of C; ::_thesis: for X being set holds a "\/" ("/\" (X,C)) [= "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C)
let X be set ; ::_thesis: a "\/" ("/\" (X,C)) [= "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C)
set Y = { (a "\/" b) where b is Element of C : b in X } ;
{ (a "\/" b) where b is Element of C : b in X } is_greater_than a "\/" ("/\" (X,C))
proof
let c be Element of C; :: according to LATTICE3:def_16 ::_thesis: ( c in { (a "\/" b) where b is Element of C : b in X } implies a "\/" ("/\" (X,C)) [= c )
assume c in { (a "\/" b) where b is Element of C : b in X } ; ::_thesis: a "\/" ("/\" (X,C)) [= c
then consider b being Element of C such that
A1: c = a "\/" b and
A2: b in X ;
X is_greater_than "/\" (X,C) by Th34;
then "/\" (X,C) [= b by A2, Def16;
hence a "\/" ("/\" (X,C)) [= c by A1, FILTER_0:1; ::_thesis: verum
end;
hence a "\/" ("/\" (X,C)) [= "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) by Th34; ::_thesis: verum
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
let C be complete Lattice; ::_thesis: ( 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)) )
thus ( C is /\-distributive implies 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)) ) ::_thesis: ( ( 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)) ) implies C is /\-distributive )
proof
assume A1: for X being set
for a, b, c being Element of C st X is_greater_than a & ( for d being Element of C st X is_greater_than d holds
d [= a ) & { (b "\/" a9) where a9 is Element of C : a9 in X } is_greater_than c & ( for d being Element of C st { (b "\/" b9) where b9 is Element of C : b9 in X } is_greater_than d holds
d [= c ) holds
c [= b "\/" a ; :: according to LATTICE3:def_20 ::_thesis: 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))
let X be set ; ::_thesis: for a being Element of C holds "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) [= a "\/" ("/\" (X,C))
let a be Element of C; ::_thesis: "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) [= a "\/" ("/\" (X,C))
set Y = { (a "\/" b) where b is Element of C : b in X } ;
A2: X is_greater_than "/\" (X,C) by Th34;
A3: for d being Element of C st X is_greater_than d holds
d [= "/\" (X,C) by Th34;
A4: { (a "\/" b) where b is Element of C : b in X } is_greater_than "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) by Th34;
for d being Element of C st { (a "\/" b) where b is Element of C : b in X } is_greater_than d holds
d [= "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) by Th34;
hence "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) [= a "\/" ("/\" (X,C)) by A1, A2, A3, A4; ::_thesis: verum
end;
assume A5: 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)) ; ::_thesis: C is /\-distributive
let X be set ; :: according to LATTICE3:def_20 ::_thesis: for a, b, c being Element of C st X is_greater_than a & ( for d being Element of C st X is_greater_than d holds
d [= a ) & { (b "\/" a9) where a9 is Element of C : a9 in X } is_greater_than c & ( for d being Element of C st { (b "\/" a9) where a9 is Element of C : a9 in X } is_greater_than d holds
d [= c ) holds
c [= b "\/" a
let a, b, c be Element of C; ::_thesis: ( X is_greater_than a & ( for d being Element of C st X is_greater_than d holds
d [= a ) & { (b "\/" a9) where a9 is Element of C : a9 in X } is_greater_than c & ( for d being Element of C st { (b "\/" a9) where a9 is Element of C : a9 in X } is_greater_than d holds
d [= c ) implies c [= b "\/" a )
assume A6: ( X is_greater_than a & ( for d being Element of C st X is_greater_than d holds
d [= a ) & { (b "\/" a9) where a9 is Element of C : a9 in X } is_greater_than c & ( for d being Element of C st { (b "\/" b9) where b9 is Element of C : b9 in X } is_greater_than d holds
d [= c ) ) ; ::_thesis: c [= b "\/" a
then A7: a = "/\" (X,C) by Th34;
c = "/\" ( { (b "\/" a9) where a9 is Element of C : a9 in X } ,C) by A6, Th34;
hence c [= b "\/" a by A5, A7; ::_thesis: verum
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
let C be complete Lattice; ::_thesis: for X being set holds "\/" (X,C) = "/\" ( { a where a is Element of C : a is_greater_than X } ,C)
let X be set ; ::_thesis: "\/" (X,C) = "/\" ( { a where a is Element of C : a is_greater_than X } ,C)
set Y = { a where a is Element of C : a is_greater_than X } ;
A1: "\/" (X,C) is_less_than { a where a is Element of C : a is_greater_than X }
proof
let a be Element of C; :: according to LATTICE3:def_16 ::_thesis: ( a in { a where a is Element of C : a is_greater_than X } implies "\/" (X,C) [= a )
assume a in { a where a is Element of C : a is_greater_than X } ; ::_thesis: "\/" (X,C) [= a
then ex b being Element of C st
( a = b & b is_greater_than X ) ;
hence "\/" (X,C) [= a by Def21; ::_thesis: verum
end;
X is_less_than "\/" (X,C) by Def21;
then "\/" (X,C) in { a where a is Element of C : a is_greater_than X } ;
then for b being Element of C st b is_less_than { a where a is Element of C : a is_greater_than X } holds
b [= "\/" (X,C) by Def16;
hence "\/" (X,C) = "/\" ( { a where a is Element of C : a is_greater_than X } ,C) by A1, Th34; ::_thesis: verum
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
let C be complete Lattice; ::_thesis: for a being Element of C
for X being set st a in X holds
( a [= "\/" (X,C) & "/\" (X,C) [= a )
let a be Element of C; ::_thesis: for X being set st a in X holds
( a [= "\/" (X,C) & "/\" (X,C) [= a )
let X be set ; ::_thesis: ( a in X implies ( a [= "\/" (X,C) & "/\" (X,C) [= a ) )
assume A1: a in X ; ::_thesis: ( a [= "\/" (X,C) & "/\" (X,C) [= a )
X is_less_than "\/" (X,C) by Def21;
hence a [= "\/" (X,C) by A1, Def17; ::_thesis: "/\" (X,C) [= a
{ b where b is Element of C : b is_less_than X } is_less_than a
proof
let c be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( c in { b where b is Element of C : b is_less_than X } implies c [= a )
assume c in { b where b is Element of C : b is_less_than X } ; ::_thesis: c [= a
then ex b being Element of C st
( c = b & b is_less_than X ) ;
hence c [= a by A1, Def16; ::_thesis: verum
end;
hence "/\" (X,C) [= a by Def21; ::_thesis: verum
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
let C be complete Lattice; ::_thesis: for a being Element of C
for X being set st a is_less_than X holds
a [= "/\" (X,C)
let a be Element of C; ::_thesis: for X being set st a is_less_than X holds
a [= "/\" (X,C)
let X be set ; ::_thesis: ( a is_less_than X implies a [= "/\" (X,C) )
assume a is_less_than X ; ::_thesis: a [= "/\" (X,C)
then a in { b where b is Element of C : b is_less_than X } ;
hence a [= "/\" (X,C) by Th38; ::_thesis: verum
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
let C be complete Lattice; ::_thesis: for a being Element of C
for X being set st a in X & X is_less_than a holds
"\/" (X,C) = a
let a be Element of C; ::_thesis: for X being set st a in X & X is_less_than a holds
"\/" (X,C) = a
let X be set ; ::_thesis: ( a in X & X is_less_than a implies "\/" (X,C) = a )
assume that
A1: a in X and
A2: X is_less_than a ; ::_thesis: "\/" (X,C) = a
A3: "\/" (X,C) [= a by A2, Def21;
a [= "\/" (X,C) by A1, Th38;
hence "\/" (X,C) = a by A3, LATTICES:8; ::_thesis: verum
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
let C be complete Lattice; ::_thesis: for a being Element of C
for X being set st a in X & a is_less_than X holds
"/\" (X,C) = a
let a be Element of C; ::_thesis: for X being set st a in X & a is_less_than X holds
"/\" (X,C) = a
let X be set ; ::_thesis: ( a in X & a is_less_than X implies "/\" (X,C) = a )
assume that
A1: a in X and
A2: a is_less_than X ; ::_thesis: "/\" (X,C) = a
A3: "/\" (X,C) [= a by A1, Th38;
a [= "/\" (X,C) by A2, Th39;
hence "/\" (X,C) = a by A3, LATTICES:8; ::_thesis: verum
end;
theorem :: LATTICE3:42
for C being complete Lattice
for a being Element of C holds
( "\/" {a} = a & "/\" {a} = a )
proof
let C be complete Lattice; ::_thesis: for a being Element of C holds
( "\/" {a} = a & "/\" {a} = a )
let a be Element of C; ::_thesis: ( "\/" {a} = a & "/\" {a} = a )
A1: a in {a} by TARSKI:def_1;
{a} is_less_than a
proof
let b be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( b in {a} implies b [= a )
assume b in {a} ; ::_thesis: b [= a
hence b [= a by TARSKI:def_1; ::_thesis: verum
end;
hence "\/" {a} = a by A1, Th40; ::_thesis: "/\" {a} = a
a is_less_than {a}
proof
let b be Element of C; :: according to LATTICE3:def_16 ::_thesis: ( b in {a} implies a [= b )
assume b in {a} ; ::_thesis: a [= b
hence a [= b by TARSKI:def_1; ::_thesis: verum
end;
hence "/\" {a} = a by A1, Th41; ::_thesis: verum
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
let C be complete Lattice; ::_thesis: for a, b being Element of C holds
( a "\/" b = "\/" {a,b} & a "/\" b = "/\" {a,b} )
let a, b be Element of C; ::_thesis: ( a "\/" b = "\/" {a,b} & a "/\" b = "/\" {a,b} )
A1: {a,b} is_less_than a "\/" b
proof
let c be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( c in {a,b} implies c [= a "\/" b )
assume A2: c in {a,b} ; ::_thesis: c [= a "\/" b
A3: a [= a "\/" b by LATTICES:5;
b [= b "\/" a by LATTICES:5;
hence c [= a "\/" b by A2, A3, TARSKI:def_2; ::_thesis: verum
end;
A4: a in {a,b} by TARSKI:def_2;
A5: b in {a,b} by TARSKI:def_2;
now__::_thesis:_for_c_being_Element_of_C_st_{a,b}_is_less_than_c_holds_
a_"\/"_b_[=_c
let c be Element of C; ::_thesis: ( {a,b} is_less_than c implies a "\/" b [= c )
assume A6: {a,b} is_less_than c ; ::_thesis: a "\/" b [= c
then A7: a [= c by A4, Def17;
b [= c by A5, A6, Def17;
hence a "\/" b [= c by A7, FILTER_0:6; ::_thesis: verum
end;
hence a "\/" b = "\/" {a,b} by A1, Def21; ::_thesis: a "/\" b = "/\" {a,b}
a "/\" b is_less_than {a,b}
proof
let c be Element of C; :: according to LATTICE3:def_16 ::_thesis: ( c in {a,b} implies a "/\" b [= c )
assume c in {a,b} ; ::_thesis: a "/\" b [= c
then ( c = a or ( c = b & b "/\" a = a "/\" b ) ) by TARSKI:def_2;
hence a "/\" b [= c by LATTICES:6; ::_thesis: verum
end;
then A8: a "/\" b in { c where c is Element of C : c is_less_than {a,b} } ;
{ c where c is Element of C : c is_less_than {a,b} } is_less_than a "/\" b
proof
let d be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( d in { c where c is Element of C : c is_less_than {a,b} } implies d [= a "/\" b )
assume d in { c where c is Element of C : c is_less_than {a,b} } ; ::_thesis: d [= a "/\" b
then A9: ex c being Element of C st
( d = c & c is_less_than {a,b} ) ;
then A10: d [= a by A4, Def16;
d [= b by A5, A9, Def16;
hence d [= a "/\" b by A10, FILTER_0:7; ::_thesis: verum
end;
hence a "/\" b = "/\" {a,b} by A8, Th40; ::_thesis: verum
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
let C be complete Lattice; ::_thesis: 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) )
let a be Element of C; ::_thesis: ( a = "\/" ( { b where b is Element of C : b [= a } ,C) & a = "/\" ( { c where c is Element of C : a [= c } ,C) )
set X = { b where b is Element of C : b [= a } ;
set Y = { c where c is Element of C : a [= c } ;
A1: a in { b where b is Element of C : b [= a } ;
A2: a in { c where c is Element of C : a [= c } ;
{ b where b is Element of C : b [= a } is_less_than a
proof
let b be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( b in { b where b is Element of C : b [= a } implies b [= a )
assume b in { b where b is Element of C : b [= a } ; ::_thesis: b [= a
then ex c being Element of C st
( b = c & c [= a ) ;
hence b [= a ; ::_thesis: verum
end;
hence a = "\/" ( { b where b is Element of C : b [= a } ,C) by A1, Th40; ::_thesis: a = "/\" ( { c where c is Element of C : a [= c } ,C)
a is_less_than { c where c is Element of C : a [= c }
proof
let b be Element of C; :: according to LATTICE3:def_16 ::_thesis: ( b in { c where c is Element of C : a [= c } implies a [= b )
assume b in { c where c is Element of C : a [= c } ; ::_thesis: a [= b
then ex c being Element of C st
( b = c & a [= c ) ;
hence a [= b ; ::_thesis: verum
end;
hence a = "/\" ( { c where c is Element of C : a [= c } ,C) by A2, Th41; ::_thesis: verum
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
let C be complete Lattice; ::_thesis: for X, Y being set st X c= Y holds
( "\/" (X,C) [= "\/" (Y,C) & "/\" (Y,C) [= "/\" (X,C) )
let X, Y be set ; ::_thesis: ( X c= Y implies ( "\/" (X,C) [= "\/" (Y,C) & "/\" (Y,C) [= "/\" (X,C) ) )
assume A1: X c= Y ; ::_thesis: ( "\/" (X,C) [= "\/" (Y,C) & "/\" (Y,C) [= "/\" (X,C) )
X is_less_than "\/" (Y,C)
proof
let a be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( a in X implies a [= "\/" (Y,C) )
assume A2: a in X ; ::_thesis: a [= "\/" (Y,C)
Y is_less_than "\/" (Y,C) by Def21;
hence a [= "\/" (Y,C) by A1, A2, Def17; ::_thesis: verum
end;
hence "\/" (X,C) [= "\/" (Y,C) by Def21; ::_thesis: "/\" (Y,C) [= "/\" (X,C)
"/\" (Y,C) is_less_than X
proof
let a be Element of C; :: according to LATTICE3:def_16 ::_thesis: ( a in X implies "/\" (Y,C) [= a )
assume A3: a in X ; ::_thesis: "/\" (Y,C) [= a
"/\" (Y,C) is_less_than Y by Th34;
hence "/\" (Y,C) [= a by A1, A3, Def16; ::_thesis: verum
end;
hence "/\" (Y,C) [= "/\" (X,C) by Th34; ::_thesis: verum
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
let C be complete Lattice; ::_thesis: 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) )
let X be set ; ::_thesis: ( "\/" (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) )
set Y = { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ;
set Z = { a where a is Element of C : ex b being Element of C st
( b [= a & b in X ) } ;
X is_less_than "\/" ( { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ,C)
proof
let a be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( a in X implies a [= "\/" ( { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ,C) )
assume a in X ; ::_thesis: a [= "\/" ( { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ,C)
then a in { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ;
hence a [= "\/" ( { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ,C) by Th38; ::_thesis: verum
end;
then A1: "\/" (X,C) [= "\/" ( { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ,C) by Def21;
{ a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } is_less_than "\/" (X,C)
proof
let a be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( a in { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } implies a [= "\/" (X,C) )
assume a in { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ; ::_thesis: a [= "\/" (X,C)
then ex b being Element of C st
( a = b & ex c being Element of C st
( b [= c & c in X ) ) ;
then consider c being Element of C such that
A2: a [= c and
A3: c in X ;
c [= "\/" (X,C) by A3, Th38;
hence a [= "\/" (X,C) by A2, LATTICES:7; ::_thesis: verum
end;
then "\/" ( { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ,C) [= "\/" (X,C) by Def21;
hence "\/" (X,C) = "\/" ( { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ,C) by A1, LATTICES:8; ::_thesis: "/\" (X,C) = "/\" ( { b where b is Element of C : ex a being Element of C st
( a [= b & a in X ) } ,C)
X is_greater_than "/\" ( { a where a is Element of C : ex b being Element of C st
( b [= a & b in X ) } ,C)
proof
let a be Element of C; :: according to LATTICE3:def_16 ::_thesis: ( a in X implies "/\" ( { a where a is Element of C : ex b being Element of C st
( b [= a & b in X ) } ,C) [= a )
assume a in X ; ::_thesis: "/\" ( { a where a is Element of C : ex b being Element of C st
( b [= a & b in X ) } ,C) [= a
then a in { a where a is Element of C : ex b being Element of C st
( b [= a & b in X ) } ;
hence "/\" ( { a where a is Element of C : ex b being Element of C st
( b [= a & b in X ) } ,C) [= a by Th38; ::_thesis: verum
end;
then A4: "/\" ( { a where a is Element of C : ex b being Element of C st
( b [= a & b in X ) } ,C) [= "/\" (X,C) by Th34;
{ a where a is Element of C : ex b being Element of C st
( b [= a & b in X ) } is_greater_than "/\" (X,C)
proof
let a be Element of C; :: according to LATTICE3:def_16 ::_thesis: ( a in { a where a is Element of C : ex b being Element of C st
( b [= a & b in X ) } implies "/\" (X,C) [= a )
assume a in { a where a is Element of C : ex b being Element of C st
( b [= a & b in X ) } ; ::_thesis: "/\" (X,C) [= a
then ex b being Element of C st
( a = b & ex c being Element of C st
( c [= b & c in X ) ) ;
then consider c being Element of C such that
A5: c [= a and
A6: c in X ;
"/\" (X,C) [= c by A6, Th38;
hence "/\" (X,C) [= a by A5, LATTICES:7; ::_thesis: verum
end;
then "/\" (X,C) [= "/\" ( { a where a is Element of C : ex b being Element of C st
( b [= a & b in X ) } ,C) by Th34;
hence "/\" (X,C) = "/\" ( { b where b is Element of C : ex a being Element of C st
( a [= b & a in X ) } ,C) by A4, LATTICES:8; ::_thesis: verum
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
let C be complete Lattice; ::_thesis: 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)
let X, Y be set ; ::_thesis: ( ( for a being Element of C st a in X holds
ex b being Element of C st
( a [= b & b in Y ) ) implies "\/" (X,C) [= "\/" (Y,C) )
assume A1: for a being Element of C st a in X holds
ex b being Element of C st
( a [= b & b in Y ) ; ::_thesis: "\/" (X,C) [= "\/" (Y,C)
X is_less_than "\/" (Y,C)
proof
let a be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( a in X implies a [= "\/" (Y,C) )
assume a in X ; ::_thesis: a [= "\/" (Y,C)
then consider b being Element of C such that
A2: a [= b and
A3: b in Y by A1;
b [= "\/" (Y,C) by A3, Th38;
hence a [= "\/" (Y,C) by A2, LATTICES:7; ::_thesis: verum
end;
hence "\/" (X,C) [= "\/" (Y,C) by Def21; ::_thesis: verum
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
let C be complete Lattice; ::_thesis: 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)
let X be set ; ::_thesis: ( X c= bool the carrier of C implies "\/" ((union X),C) = "\/" ( { ("\/" Y) where Y is Subset of C : Y in X } ,C) )
set Z = { ("\/" Y) where Y is Subset of C : Y in X } ;
{ ("\/" Y) where Y is Subset of C : Y in X } is_less_than "\/" ((union X),C)
proof
let a be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( a in { ("\/" Y) where Y is Subset of C : Y in X } implies a [= "\/" ((union X),C) )
assume a in { ("\/" Y) where Y is Subset of C : Y in X } ; ::_thesis: a [= "\/" ((union X),C)
then consider Y being Subset of C such that
A1: a = "\/" Y and
A2: Y in X ;
Y c= union X by A2, ZFMISC_1:74;
hence a [= "\/" ((union X),C) by A1, Th45; ::_thesis: verum
end;
then A3: "\/" ( { ("\/" Y) where Y is Subset of C : Y in X } ,C) [= "\/" ((union X),C) by Def21;
set V = { a where a is Element of C : ex b being Element of C st
( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) } ;
assume A4: X c= bool the carrier of C ; ::_thesis: "\/" ((union X),C) = "\/" ( { ("\/" Y) where Y is Subset of C : Y in X } ,C)
union X c= { a where a is Element of C : ex b being Element of C st
( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union X or x in { a where a is Element of C : ex b being Element of C st
( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) } )
assume x in union X ; ::_thesis: x in { a where a is Element of C : ex b being Element of C st
( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) }
then consider Y being set such that
A5: x in Y and
A6: Y in X by TARSKI:def_4;
reconsider Y = Y as Subset of C by A4, A6;
reconsider a = x as Element of C by A4, A5, A6;
A7: a [= "\/" Y by A5, Th38;
"\/" Y in { ("\/" Y) where Y is Subset of C : Y in X } by A6;
hence x in { a where a is Element of C : ex b being Element of C st
( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) } by A7; ::_thesis: verum
end;
then "\/" ((union X),C) [= "\/" ( { a where a is Element of C : ex b being Element of C st
( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) } ,C) by Th45;
then "\/" ((union X),C) [= "\/" ( { ("\/" Y) where Y is Subset of C : Y in X } ,C) by Th46;
hence "\/" ((union X),C) = "\/" ( { ("\/" Y) where Y is Subset of C : Y in X } ,C) by A3, LATTICES:8; ::_thesis: verum
end;
theorem :: LATTICE3:49
for C being complete Lattice holds
( C is 0_Lattice & Bottom C = "\/" ({},C) )
proof
let C be complete Lattice; ::_thesis: ( C is 0_Lattice & Bottom C = "\/" ({},C) )
A1: now__::_thesis:_for_a_being_Element_of_C_holds_
(_("\/"_({},C))_"/\"_a_=_"\/"_({},C)_&_a_"/\"_("\/"_({},C))_=_"\/"_({},C)_)
let a be Element of C; ::_thesis: ( ("\/" ({},C)) "/\" a = "\/" ({},C) & a "/\" ("\/" ({},C)) = "\/" ({},C) )
{} is_less_than ("\/" ({},C)) "/\" a
proof
let b be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( b in {} implies b [= ("\/" ({},C)) "/\" a )
thus ( b in {} implies b [= ("\/" ({},C)) "/\" a ) ; ::_thesis: verum
end;
then A2: "\/" ({},C) [= ("\/" ({},C)) "/\" a by Def21;
A3: ("\/" ({},C)) "/\" a [= "\/" ({},C) by LATTICES:6;
hence ("\/" ({},C)) "/\" a = "\/" ({},C) by A2, LATTICES:8; ::_thesis: a "/\" ("\/" ({},C)) = "\/" ({},C)
thus a "/\" ("\/" ({},C)) = "\/" ({},C) by A2, A3, LATTICES:8; ::_thesis: verum
end;
then C is lower-bounded by LATTICES:def_13;
hence ( C is 0_Lattice & Bottom C = "\/" ({},C) ) by A1, LATTICES:def_16; ::_thesis: verum
end;
theorem :: LATTICE3:50
for C being complete Lattice holds
( C is 1_Lattice & Top C = "\/" ( the carrier of C,C) )
proof
let C be complete Lattice; ::_thesis: ( C is 1_Lattice & Top C = "\/" ( the carrier of C,C) )
set j = "\/" ( the carrier of C,C);
A1: now__::_thesis:_for_a_being_Element_of_C_holds_
(_("\/"_(_the_carrier_of_C,C))_"\/"_a_=_"\/"_(_the_carrier_of_C,C)_&_a_"\/"_("\/"_(_the_carrier_of_C,C))_=_"\/"_(_the_carrier_of_C,C)_)
let a be Element of C; ::_thesis: ( ("\/" ( the carrier of C,C)) "\/" a = "\/" ( the carrier of C,C) & a "\/" ("\/" ( the carrier of C,C)) = "\/" ( the carrier of C,C) )
A2: "\/" ( the carrier of C,C) [= ("\/" ( the carrier of C,C)) "\/" a by LATTICES:5;
A3: ("\/" ( the carrier of C,C)) "\/" a [= "\/" ( the carrier of C,C) by Th38;
hence ("\/" ( the carrier of C,C)) "\/" a = "\/" ( the carrier of C,C) by A2, LATTICES:8; ::_thesis: a "\/" ("\/" ( the carrier of C,C)) = "\/" ( the carrier of C,C)
thus a "\/" ("\/" ( the carrier of C,C)) = "\/" ( the carrier of C,C) by A2, A3, LATTICES:8; ::_thesis: verum
end;
then C is upper-bounded by LATTICES:def_14;
hence ( C is 1_Lattice & Top C = "\/" ( the carrier of C,C) ) by A1, LATTICES:def_17; ::_thesis: verum
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
let C be complete Lattice; ::_thesis: 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)
let a, b be Element of C; ::_thesis: ( C is I_Lattice implies a => b = "\/" ( { c where c is Element of C : a "/\" c [= b } ,C) )
set X = { a9 where a9 is Element of C : a "/\" a9 [= b } ;
assume A1: C is I_Lattice ; ::_thesis: a => b = "\/" ( { c where c is Element of C : a "/\" c [= b } ,C)
then a "/\" (a => b) [= b by FILTER_0:def_7;
then A2: a => b in { a9 where a9 is Element of C : a "/\" a9 [= b } ;
{ a9 where a9 is Element of C : a "/\" a9 [= b } is_less_than a => b
proof
let c be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( c in { a9 where a9 is Element of C : a "/\" a9 [= b } implies c [= a => b )
assume c in { a9 where a9 is Element of C : a "/\" a9 [= b } ; ::_thesis: c [= a => b
then ex a9 being Element of C st
( c = a9 & a "/\" a9 [= b ) ;
hence c [= a => b by A1, FILTER_0:def_7; ::_thesis: verum
end;
hence a => b = "\/" ( { c where c is Element of C : a "/\" c [= b } ,C) by A2, Th40; ::_thesis: verum
end;
theorem :: LATTICE3:52
for C being complete Lattice st C is I_Lattice holds
C is \/-distributive
proof
let C be complete Lattice; ::_thesis: ( C is I_Lattice implies C is \/-distributive )
assume A1: C is I_Lattice ; ::_thesis: C is \/-distributive
now__::_thesis:_for_X_being_set_
for_a_being_Element_of_C_holds_a_"/\"_("\/"_(X,C))_[=_"\/"_(_{__(a_"/\"_a9)_where_a9_is_Element_of_C_:_a9_in_X__}__,C)
let X be set ; ::_thesis: for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C)
let a be Element of C; ::_thesis: a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C)
set Y = { (a "/\" a9) where a9 is Element of C : a9 in X } ;
set b = "\/" (X,C);
set c = "\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C);
set Z = { b9 where b9 is Element of C : a "/\" b9 [= "\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C) } ;
X is_less_than a => ("\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C))
proof
let b9 be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( b9 in X implies b9 [= a => ("\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C)) )
assume b9 in X ; ::_thesis: b9 [= a => ("\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C))
then a "/\" b9 in { (a "/\" a9) where a9 is Element of C : a9 in X } ;
then a "/\" b9 [= "\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C) by Th38;
then A2: b9 in { b9 where b9 is Element of C : a "/\" b9 [= "\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C) } ;
a => ("\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C)) = "\/" ( { b9 where b9 is Element of C : a "/\" b9 [= "\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C) } ,C) by A1, Th51;
hence b9 [= a => ("\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C)) by A2, Th38; ::_thesis: verum
end;
then "\/" (X,C) [= a => ("\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C)) by Def21;
then A3: a "/\" ("\/" (X,C)) [= a "/\" (a => ("\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C))) by LATTICES:9;
a "/\" (a => ("\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C))) [= "\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C) by A1, FILTER_0:def_7;
hence a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C) by A3, LATTICES:7; ::_thesis: verum
end;
hence C is \/-distributive by Th33; ::_thesis: verum
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
let X be set ; ::_thesis: 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) )
let D be complete \/-distributive Lattice; ::_thesis: 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) )
let a be Element of D; ::_thesis: ( 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) )
A1: "\/" ( { (a "/\" b) where b is Element of D : b in X } ,D) [= a "/\" ("\/" (X,D)) by Th32;
A2: a "/\" ("\/" (X,D)) [= "\/" ( { (a "/\" b) where b is Element of D : b in X } ,D) by Th33;
hence a "/\" ("\/" (X,D)) = "\/" ( { (a "/\" b) where b is Element of D : b in X } ,D) by A1, LATTICES:8; ::_thesis: ("\/" (X,D)) "/\" a = "\/" ( { (b2 "/\" a) where b2 is Element of D : b2 in X } ,D)
deffunc H4( Element of D) -> Element of the carrier of D = $1 "/\" a;
deffunc H5( Element of D) -> Element of the carrier of D = a "/\" $1;
defpred S1[ set ] means $1 in X;
A3: for b being Element of D holds H5(b) = H4(b) ;
{ H5(b) where b is Element of D : S1[b] } = { H4(c) where c is Element of D : S1[c] } from FRAENKEL:sch_5(A3);
hence ("\/" (X,D)) "/\" a = "\/" ( { (b2 "/\" a) where b2 is Element of D : b2 in X } ,D) by A1, A2, LATTICES:8; ::_thesis: verum
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
let X be set ; ::_thesis: 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) )
let D be complete /\-distributive Lattice; ::_thesis: 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) )
let a be Element of D; ::_thesis: ( 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) )
defpred S1[ set ] means $1 in X;
A1: "/\" ( { (a "\/" b) where b is Element of D : b in X } ,D) [= a "\/" ("/\" (X,D)) by Th36;
A2: a "\/" ("/\" (X,D)) [= "/\" ( { (a "\/" b) where b is Element of D : b in X } ,D) by Th35;
hence a "\/" ("/\" (X,D)) = "/\" ( { (a "\/" b) where b is Element of D : b in X } ,D) by A1, LATTICES:8; ::_thesis: ("/\" (X,D)) "\/" a = "/\" ( { (b2 "\/" a) where b2 is Element of D : b2 in X } ,D)
deffunc H4( Element of D) -> Element of the carrier of D = $1 "\/" a;
deffunc H5( Element of D) -> Element of the carrier of D = a "\/" $1;
A3: for b being Element of D holds H5(b) = H4(b) ;
{ H5(b) where b is Element of D : S1[b] } = { H4(c) where c is Element of D : S1[c] } from FRAENKEL:sch_5(A3);
hence ("/\" (X,D)) "\/" a = "/\" ( { (b2 "\/" a) where b2 is Element of D : b2 in X } ,D) by A1, A2, LATTICES:8; ::_thesis: verum
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
thus { F1() where a is Element of F2() : P1[a] } c= {F1()} :: according to XBOOLE_0:def_10 ::_thesis: {F1()} c= { F1() where a is Element of F2() : P1[a] }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F1() where a is Element of F2() : P1[a] } or x in {F1()} )
assume x in { F1() where a is Element of F2() : P1[a] } ; ::_thesis: x in {F1()}
then ex a being Element of F2() st
( x = F1() & P1[a] ) ;
hence x in {F1()} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {F1()} or x in { F1() where a is Element of F2() : P1[a] } )
assume x in {F1()} ; ::_thesis: x in { F1() where a is Element of F2() : P1[a] }
then x = F1() by TARSKI:def_1;
hence x in { F1() where a is Element of F2() : P1[a] } by A1; ::_thesis: verum
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
set f = F4();
thus F4() .: { F3(x) where x is Element of F1() : P1[x] } c= { (F4() . F3(x)) where x is Element of F1() : P1[x] } :: according to XBOOLE_0:def_10 ::_thesis: { (F4() . F3(x)) where x is Element of F1() : P1[x] } c= F4() .: { F3(x) where x is Element of F1() : P1[x] }
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in F4() .: { F3(x) where x is Element of F1() : P1[x] } or y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } )
assume y in F4() .: { F3(x) where x is Element of F1() : P1[x] } ; ::_thesis: y in { (F4() . F3(x)) where x is Element of F1() : P1[x] }
then consider z being set such that
z in dom F4() and
A2: z in { F3(x) where x is Element of F1() : P1[x] } and
A3: y = F4() . z by FUNCT_1:def_6;
ex x being Element of F1() st
( z = F3(x) & P1[x] ) by A2;
hence y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } by A3; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } or y in F4() .: { F3(x) where x is Element of F1() : P1[x] } )
assume y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } ; ::_thesis: y in F4() .: { F3(x) where x is Element of F1() : P1[x] }
then consider x being Element of F1() such that
A4: y = F4() . F3(x) and
A5: P1[x] ;
A6: F3(x) in dom F4() by A1, TARSKI:def_3;
F3(x) in { F3(z) where z is Element of F1() : P1[z] } by A5;
hence y in F4() .: { F3(x) where x is Element of F1() : P1[x] } by A4, A6, FUNCT_1:def_6; ::_thesis: verum
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[ 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 & 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 set ; :: 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 set ; :: 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 set ; :: 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 )
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 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 set ; :: 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 set ; :: 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
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 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
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 ) & ( 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;