:: WAYBEL_2 semantic presentation
begin
registration
let X, Y be non empty set ;
let f be Function of X,Y;
let Z be non empty Subset of X;
clusterf .: Z -> non empty ;
coherence
not f .: Z is empty
proof
set x = the Element of Z;
A1: dom f = X by FUNCT_2:def_1;
thus not f .: Z is empty by A1; ::_thesis: verum
end;
end;
registration
cluster non empty reflexive connected -> non empty with_suprema with_infima for RelStr ;
coherence
for b1 being non empty RelStr st b1 is reflexive & b1 is connected holds
( b1 is with_infima & b1 is with_suprema )
proof
let L be non empty RelStr ; ::_thesis: ( L is reflexive & L is connected implies ( L is with_infima & L is with_suprema ) )
assume A1: ( L is reflexive & L is connected ) ; ::_thesis: ( L is with_infima & L is with_suprema )
thus L is with_infima ::_thesis: L is with_suprema
proof
let x, y be Element of L; :: according to LATTICE3:def_11 ::_thesis: ex b1 being Element of the carrier of L st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of L holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )
percases ( x <= y or y <= x ) by A1, WAYBEL_0:def_29;
supposeA2: x <= y ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of L holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )
take z = x; ::_thesis: ( z <= x & z <= y & ( for b1 being Element of the carrier of L holds
( not b1 <= x or not b1 <= y or b1 <= z ) ) )
thus ( z <= x & z <= y ) by A1, A2, YELLOW_0:def_1; ::_thesis: for b1 being Element of the carrier of L holds
( not b1 <= x or not b1 <= y or b1 <= z )
thus for b1 being Element of the carrier of L holds
( not b1 <= x or not b1 <= y or b1 <= z ) ; ::_thesis: verum
end;
supposeA3: y <= x ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of L holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )
take z = y; ::_thesis: ( z <= x & z <= y & ( for b1 being Element of the carrier of L holds
( not b1 <= x or not b1 <= y or b1 <= z ) ) )
thus ( z <= x & z <= y ) by A1, A3, YELLOW_0:def_1; ::_thesis: for b1 being Element of the carrier of L holds
( not b1 <= x or not b1 <= y or b1 <= z )
thus for b1 being Element of the carrier of L holds
( not b1 <= x or not b1 <= y or b1 <= z ) ; ::_thesis: verum
end;
end;
end;
let x, y be Element of L; :: according to LATTICE3:def_10 ::_thesis: ex b1 being Element of the carrier of L st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of L holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )
percases ( x <= y or y <= x ) by A1, WAYBEL_0:def_29;
supposeA4: x <= y ; ::_thesis: ex b1 being Element of the carrier of L st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of L holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )
take z = y; ::_thesis: ( x <= z & y <= z & ( for b1 being Element of the carrier of L holds
( not x <= b1 or not y <= b1 or z <= b1 ) ) )
thus ( z >= x & z >= y ) by A1, A4, YELLOW_0:def_1; ::_thesis: for b1 being Element of the carrier of L holds
( not x <= b1 or not y <= b1 or z <= b1 )
thus for b1 being Element of the carrier of L holds
( not x <= b1 or not y <= b1 or z <= b1 ) ; ::_thesis: verum
end;
supposeA5: y <= x ; ::_thesis: ex b1 being Element of the carrier of L st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of L holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )
take z = x; ::_thesis: ( x <= z & y <= z & ( for b1 being Element of the carrier of L holds
( not x <= b1 or not y <= b1 or z <= b1 ) ) )
thus ( z >= x & z >= y ) by A1, A5, YELLOW_0:def_1; ::_thesis: for b1 being Element of the carrier of L holds
( not x <= b1 or not y <= b1 or z <= b1 )
thus for b1 being Element of the carrier of L holds
( not x <= b1 or not y <= b1 or z <= b1 ) ; ::_thesis: verum
end;
end;
end;
end;
registration
let C be Chain;
cluster [#] C -> directed ;
coherence
[#] C is directed ;
end;
theorem Th1: :: WAYBEL_2:1
for L being up-complete Semilattice
for D being non empty directed Subset of L
for x being Element of L holds ex_sup_of {x} "/\" D,L
proof
let L be up-complete Semilattice; ::_thesis: for D being non empty directed Subset of L
for x being Element of L holds ex_sup_of {x} "/\" D,L
let D be non empty directed Subset of L; ::_thesis: for x being Element of L holds ex_sup_of {x} "/\" D,L
let x be Element of L; ::_thesis: ex_sup_of {x} "/\" D,L
reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;
ex_sup_of xx "/\" D,L by WAYBEL_0:75;
hence ex_sup_of {x} "/\" D,L ; ::_thesis: verum
end;
theorem :: WAYBEL_2:2
for L being up-complete sup-Semilattice
for D being non empty directed Subset of L
for x being Element of L holds ex_sup_of {x} "\/" D,L
proof
let L be up-complete sup-Semilattice; ::_thesis: for D being non empty directed Subset of L
for x being Element of L holds ex_sup_of {x} "\/" D,L
let D be non empty directed Subset of L; ::_thesis: for x being Element of L holds ex_sup_of {x} "\/" D,L
let x be Element of L; ::_thesis: ex_sup_of {x} "\/" D,L
reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;
ex_sup_of xx "\/" D,L by WAYBEL_0:75;
hence ex_sup_of {x} "\/" D,L ; ::_thesis: verum
end;
theorem Th3: :: WAYBEL_2:3
for L being up-complete sup-Semilattice
for A, B being non empty directed Subset of L holds A is_<=_than sup (A "\/" B)
proof
let L be up-complete sup-Semilattice; ::_thesis: for A, B being non empty directed Subset of L holds A is_<=_than sup (A "\/" B)
let A, B be non empty directed Subset of L; ::_thesis: A is_<=_than sup (A "\/" B)
A1: A "\/" B = { (x "\/" y) where x, y is Element of L : ( x in A & y in B ) } by YELLOW_4:def_3;
set b = the Element of B;
let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in A or x <= sup (A "\/" B) )
assume x in A ; ::_thesis: x <= sup (A "\/" B)
then A2: x "\/" the Element of B in A "\/" B by A1;
ex xx being Element of L st
( x <= xx & the Element of B <= xx & ( for c being Element of L st x <= c & the Element of B <= c holds
xx <= c ) ) by LATTICE3:def_10;
then A3: x <= x "\/" the Element of B by LATTICE3:def_13;
ex_sup_of A "\/" B,L by WAYBEL_0:75;
then A "\/" B is_<=_than sup (A "\/" B) by YELLOW_0:def_9;
then x "\/" the Element of B <= sup (A "\/" B) by A2, LATTICE3:def_9;
hence x <= sup (A "\/" B) by A3, YELLOW_0:def_2; ::_thesis: verum
end;
theorem Th4: :: WAYBEL_2:4
for L being up-complete sup-Semilattice
for A, B being non empty directed Subset of L holds sup (A "\/" B) = (sup A) "\/" (sup B)
proof
let L be up-complete sup-Semilattice; ::_thesis: for A, B being non empty directed Subset of L holds sup (A "\/" B) = (sup A) "\/" (sup B)
let A, B be non empty directed Subset of L; ::_thesis: sup (A "\/" B) = (sup A) "\/" (sup B)
A1: ex_sup_of B,L by WAYBEL_0:75;
then A2: B is_<=_than sup B by YELLOW_0:30;
A3: ex_sup_of A,L by WAYBEL_0:75;
then A is_<=_than sup A by YELLOW_0:30;
then ( ex_sup_of A "\/" B,L & A "\/" B is_<=_than (sup A) "\/" (sup B) ) by A2, WAYBEL_0:75, YELLOW_4:27;
then A4: sup (A "\/" B) <= (sup A) "\/" (sup B) by YELLOW_0:def_9;
B is_<=_than sup (A "\/" B) by Th3;
then A5: sup B <= sup (A "\/" B) by A1, YELLOW_0:30;
A is_<=_than sup (A "\/" B) by Th3;
then sup A <= sup (A "\/" B) by A3, YELLOW_0:30;
then A6: (sup A) "\/" (sup B) <= (sup (A "\/" B)) "\/" (sup (A "\/" B)) by A5, YELLOW_3:3;
sup (A "\/" B) <= sup (A "\/" B) ;
then (sup (A "\/" B)) "\/" (sup (A "\/" B)) = sup (A "\/" B) by YELLOW_0:24;
hence sup (A "\/" B) = (sup A) "\/" (sup B) by A4, A6, ORDERS_2:2; ::_thesis: verum
end;
theorem Th5: :: WAYBEL_2:5
for L being up-complete Semilattice
for D being non empty directed Subset of [:L,L:] holds { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } = { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) }
proof
let L be up-complete Semilattice; ::_thesis: for D being non empty directed Subset of [:L,L:] holds { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } = { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) }
let D be non empty directed Subset of [:L,L:]; ::_thesis: { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } = { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) }
defpred S1[ set ] means ex x being Element of L st
( $1 = {x} "/\" (proj2 D) & x in proj1 D );
reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22;
thus { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } c= { (sup X) where X is non empty directed Subset of L : S1[X] } :: according to XBOOLE_0:def_10 ::_thesis: { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } c= { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D }
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } or q in { (sup X) where X is non empty directed Subset of L : S1[X] } )
assume q in { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } ; ::_thesis: q in { (sup X) where X is non empty directed Subset of L : S1[X] }
then consider x being Element of L such that
A1: ( q = sup ({x} "/\" D2) & x in D1 ) ;
reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;
( not xx "/\" D2 is empty & xx "/\" D2 is directed ) ;
hence q in { (sup X) where X is non empty directed Subset of L : S1[X] } by A1; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } or q in { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } )
assume q in { (sup X) where X is non empty directed Subset of L : S1[X] } ; ::_thesis: q in { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D }
then ex X being non empty directed Subset of L st
( q = sup X & S1[X] ) ;
hence q in { (sup ({x} "/\" (proj2 D))) where x is Element of L : x in proj1 D } ; ::_thesis: verum
end;
theorem Th6: :: WAYBEL_2:6
for L being Semilattice
for D being non empty directed Subset of [:L,L:] holds union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } = (proj1 D) "/\" (proj2 D)
proof
let L be Semilattice; ::_thesis: for D being non empty directed Subset of [:L,L:] holds union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } = (proj1 D) "/\" (proj2 D)
let D be non empty directed Subset of [:L,L:]; ::_thesis: union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } = (proj1 D) "/\" (proj2 D)
set D1 = proj1 D;
set D2 = proj2 D;
defpred S1[ set ] means ex x being Element of L st
( $1 = {x} "/\" (proj2 D) & x in proj1 D );
reconsider T = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22;
A1: (proj1 D) "/\" (proj2 D) = { (x "/\" y) where x, y is Element of L : ( x in proj1 D & y in proj2 D ) } by YELLOW_4:def_4;
thus union { X where X is non empty directed Subset of L : S1[X] } c= (proj1 D) "/\" (proj2 D) :: according to XBOOLE_0:def_10 ::_thesis: (proj1 D) "/\" (proj2 D) c= union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) }
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in union { X where X is non empty directed Subset of L : S1[X] } or q in (proj1 D) "/\" (proj2 D) )
assume q in union { X where X is non empty directed Subset of L : S1[X] } ; ::_thesis: q in (proj1 D) "/\" (proj2 D)
then consider w being set such that
A2: q in w and
A3: w in { X where X is non empty directed Subset of L : S1[X] } by TARSKI:def_4;
consider e being non empty directed Subset of L such that
A4: w = e and
A5: S1[e] by A3;
consider p being Element of L such that
A6: e = {p} "/\" (proj2 D) and
A7: p in proj1 D by A5;
{p} "/\" (proj2 D) = { (p "/\" y) where y is Element of L : y in proj2 D } by YELLOW_4:42;
then ex y being Element of L st
( q = p "/\" y & y in proj2 D ) by A2, A4, A6;
hence q in (proj1 D) "/\" (proj2 D) by A1, A7; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (proj1 D) "/\" (proj2 D) or q in union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } )
assume q in (proj1 D) "/\" (proj2 D) ; ::_thesis: q in union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) }
then consider x, y being Element of L such that
A8: q = x "/\" y and
A9: x in proj1 D and
A10: y in proj2 D by A1;
reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;
( not xx "/\" T is empty & xx "/\" T is directed ) ;
then A11: {x} "/\" (proj2 D) in { X where X is non empty directed Subset of L : S1[X] } by A9;
{x} "/\" (proj2 D) = { (x "/\" d) where d is Element of L : d in proj2 D } by YELLOW_4:42;
then q in {x} "/\" (proj2 D) by A8, A10;
hence q in union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } by A11, TARSKI:def_4; ::_thesis: verum
end;
theorem Th7: :: WAYBEL_2:7
for L being up-complete Semilattice
for D being non empty directed Subset of [:L,L:] holds ex_sup_of union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L
proof
let L be up-complete Semilattice; ::_thesis: for D being non empty directed Subset of [:L,L:] holds ex_sup_of union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L
let D be non empty directed Subset of [:L,L:]; ::_thesis: ex_sup_of union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L
reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22;
set A = { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" D2 & x in D1 ) } ;
union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" D2 & x in D1 ) } c= the carrier of L
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" D2 & x in D1 ) } or q in the carrier of L )
assume q in union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" D2 & x in D1 ) } ; ::_thesis: q in the carrier of L
then consider r being set such that
A1: q in r and
A2: r in { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" D2 & x in D1 ) } by TARSKI:def_4;
ex s being non empty directed Subset of L st
( r = s & ex x being Element of L st
( s = {x} "/\" D2 & x in D1 ) ) by A2;
hence q in the carrier of L by A1; ::_thesis: verum
end;
then reconsider S = union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" D2 & x in D1 ) } as Subset of L ;
S = D1 "/\" D2 by Th6;
hence ex_sup_of union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L by WAYBEL_0:75; ::_thesis: verum
end;
theorem Th8: :: WAYBEL_2:8
for L being up-complete Semilattice
for D being non empty directed Subset of [:L,L:] holds ex_sup_of { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L
proof
let L be up-complete Semilattice; ::_thesis: for D being non empty directed Subset of [:L,L:] holds ex_sup_of { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L
let D be non empty directed Subset of [:L,L:]; ::_thesis: ex_sup_of { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L
reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22;
defpred S1[ set ] means ex x being Element of L st
( $1 = {x} "/\" D2 & x in D1 );
set A = { (sup X) where X is non empty directed Subset of L : S1[X] } ;
{ (sup X) where X is non empty directed Subset of L : S1[X] } c= the carrier of L
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (sup X) where X is non empty directed Subset of L : S1[X] } or q in the carrier of L )
assume q in { (sup X) where X is non empty directed Subset of L : S1[X] } ; ::_thesis: q in the carrier of L
then ex X being non empty directed Subset of L st
( q = sup X & S1[X] ) ;
hence q in the carrier of L ; ::_thesis: verum
end;
then reconsider A = { (sup X) where X is non empty directed Subset of L : S1[X] } as Subset of L ;
set R = { X where X is non empty directed Subset of L : S1[X] } ;
union { X where X is non empty directed Subset of L : S1[X] } c= the carrier of L
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in union { X where X is non empty directed Subset of L : S1[X] } or q in the carrier of L )
assume q in union { X where X is non empty directed Subset of L : S1[X] } ; ::_thesis: q in the carrier of L
then consider r being set such that
A1: q in r and
A2: r in { X where X is non empty directed Subset of L : S1[X] } by TARSKI:def_4;
ex s being non empty directed Subset of L st
( r = s & ex x being Element of L st
( s = {x} "/\" D2 & x in D1 ) ) by A2;
hence q in the carrier of L by A1; ::_thesis: verum
end;
then reconsider UR = union { X where X is non empty directed Subset of L : S1[X] } as Subset of L ;
set a = sup UR;
A3: ex_sup_of UR,L by Th7;
A4: for b being Element of L st A is_<=_than b holds
sup UR <= b
proof
let b be Element of L; ::_thesis: ( A is_<=_than b implies sup UR <= b )
assume A5: A is_<=_than b ; ::_thesis: sup UR <= b
UR is_<=_than b
proof
let k be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not k in UR or k <= b )
assume k in UR ; ::_thesis: k <= b
then consider k1 being set such that
A6: k in k1 and
A7: k1 in { X where X is non empty directed Subset of L : S1[X] } by TARSKI:def_4;
consider s being non empty directed Subset of L such that
A8: k1 = s and
A9: S1[s] by A7;
consider x being Element of L such that
A10: s = {x} "/\" D2 and
x in D1 by A9;
A11: {x} "/\" D2 = { (x "/\" d2) where d2 is Element of L : d2 in D2 } by YELLOW_4:42;
sup s in A by A9;
then A12: sup s <= b by A5, LATTICE3:def_9;
consider d2 being Element of L such that
A13: k = x "/\" d2 and
d2 in D2 by A6, A8, A10, A11;
x "/\" d2 <= sup s by A6, A8, A10, A13, Th1, YELLOW_4:1;
hence k <= b by A13, A12, YELLOW_0:def_2; ::_thesis: verum
end;
hence sup UR <= b by A3, YELLOW_0:def_9; ::_thesis: verum
end;
A is_<=_than sup UR
proof
let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in A or b <= sup UR )
assume b in A ; ::_thesis: b <= sup UR
then consider X being non empty directed Subset of L such that
A14: b = sup X and
A15: S1[X] ;
( ex_sup_of X,L & X in { X where X is non empty directed Subset of L : S1[X] } ) by A15, WAYBEL_0:75;
hence b <= sup UR by A3, A14, YELLOW_0:34, ZFMISC_1:74; ::_thesis: verum
end;
hence ex_sup_of { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L by A4, YELLOW_0:15; ::_thesis: verum
end;
theorem Th9: :: WAYBEL_2:9
for L being up-complete Semilattice
for D being non empty directed Subset of [:L,L:] holds "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L) <= "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ),L)
proof
let L be up-complete Semilattice; ::_thesis: for D being non empty directed Subset of [:L,L:] holds "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L) <= "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ),L)
let D be non empty directed Subset of [:L,L:]; ::_thesis: "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L) <= "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ),L)
defpred S1[ set ] means ex x being Element of L st
( $1 = {x} "/\" (proj2 D) & x in proj1 D );
A1: "\/" ((union { X where X is non empty directed Subset of L : S1[X] } ),L) is_>=_than { (sup X) where X is non empty directed Subset of L : S1[X] }
proof
let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in { (sup X) where X is non empty directed Subset of L : S1[X] } or a <= "\/" ((union { X where X is non empty directed Subset of L : S1[X] } ),L) )
assume a in { (sup X) where X is non empty directed Subset of L : S1[X] } ; ::_thesis: a <= "\/" ((union { X where X is non empty directed Subset of L : S1[X] } ),L)
then consider q being non empty directed Subset of L such that
A2: a = sup q and
A3: S1[q] ;
A4: q in { X where X is non empty directed Subset of L : S1[X] } by A3;
( ex_sup_of q,L & ex_sup_of union { X where X is non empty directed Subset of L : S1[X] } ,L ) by Th7, WAYBEL_0:75;
hence a <= "\/" ((union { X where X is non empty directed Subset of L : S1[X] } ),L) by A2, A4, YELLOW_0:34, ZFMISC_1:74; ::_thesis: verum
end;
ex_sup_of { (sup X) where X is non empty directed Subset of L : S1[X] } ,L by Th8;
hence "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L) <= "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ),L) by A1, YELLOW_0:def_9; ::_thesis: verum
end;
theorem Th10: :: WAYBEL_2:10
for L being up-complete Semilattice
for D being non empty directed Subset of [:L,L:] holds "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L) = "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ),L)
proof
let L be up-complete Semilattice; ::_thesis: for D being non empty directed Subset of [:L,L:] holds "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L) = "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ),L)
let D be non empty directed Subset of [:L,L:]; ::_thesis: "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L) = "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ),L)
defpred S1[ set ] means ex x being Element of L st
( $1 = {x} "/\" (proj2 D) & x in proj1 D );
A1: "\/" ( { (sup X) where X is non empty directed Subset of L : S1[X] } ,L) <= "\/" ((union { X where X is non empty directed Subset of L : S1[X] } ),L) by Th9;
A2: union { X where X is non empty directed Subset of L : S1[X] } is_<=_than "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,L)
proof
let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in union { X where X is non empty directed Subset of L : S1[X] } or a <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,L) )
assume a in union { X where X is non empty directed Subset of L : S1[X] } ; ::_thesis: a <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,L)
then consider b being set such that
A3: a in b and
A4: b in { X where X is non empty directed Subset of L : S1[X] } by TARSKI:def_4;
consider c being non empty directed Subset of L such that
A5: b = c and
A6: S1[c] by A4;
"\/" (c,L) in { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } by A6;
then A7: "\/" (c,L) <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,L) by Th8, YELLOW_4:1;
ex_sup_of c,L by WAYBEL_0:75;
then a <= "\/" (c,L) by A3, A5, YELLOW_4:1;
hence a <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,L) by A7, YELLOW_0:def_2; ::_thesis: verum
end;
ex_sup_of union { X where X is non empty directed Subset of L : S1[X] } ,L by Th7;
then "\/" ((union { X where X is non empty directed Subset of L : S1[X] } ),L) <= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,L) by A2, YELLOW_0:def_9;
hence "\/" ( { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L) = "\/" ((union { X where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ),L) by A1, ORDERS_2:2; ::_thesis: verum
end;
registration
let S, T be non empty reflexive up-complete RelStr ;
cluster[:S,T:] -> up-complete ;
coherence
[:S,T:] is up-complete
proof
let X be non empty directed Subset of [:S,T:]; :: according to WAYBEL_0:def_39 ::_thesis: ex b1 being Element of the carrier of [:S,T:] st
( X is_<=_than b1 & ( for b2 being Element of the carrier of [:S,T:] holds
( not X is_<=_than b2 or b1 <= b2 ) ) )
reconsider X1 = proj1 X as non empty directed Subset of S by YELLOW_3:21, YELLOW_3:22;
reconsider X2 = proj2 X as non empty directed Subset of T by YELLOW_3:21, YELLOW_3:22;
consider x being Element of S such that
A1: x is_>=_than X1 and
A2: for z being Element of S st z is_>=_than X1 holds
x <= z by WAYBEL_0:def_39;
consider y being Element of T such that
A3: y is_>=_than X2 and
A4: for z being Element of T st z is_>=_than X2 holds
y <= z by WAYBEL_0:def_39;
take [x,y] ; ::_thesis: ( X is_<=_than [x,y] & ( for b1 being Element of the carrier of [:S,T:] holds
( not X is_<=_than b1 or [x,y] <= b1 ) ) )
thus [x,y] is_>=_than X by A1, A3, YELLOW_3:31; ::_thesis: for b1 being Element of the carrier of [:S,T:] holds
( not X is_<=_than b1 or [x,y] <= b1 )
let z be Element of [:S,T:]; ::_thesis: ( not X is_<=_than z or [x,y] <= z )
assume A5: z is_>=_than X ; ::_thesis: [x,y] <= z
the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then A6: z = [(z `1),(z `2)] by MCART_1:21;
then z `2 is_>=_than X2 by A5, YELLOW_3:31;
then A7: y <= z `2 by A4;
z `1 is_>=_than X1 by A5, A6, YELLOW_3:31;
then x <= z `1 by A2;
hence [x,y] <= z by A6, A7, YELLOW_3:11; ::_thesis: verum
end;
end;
theorem :: WAYBEL_2:11
for S, T being non empty reflexive antisymmetric RelStr st [:S,T:] is up-complete holds
( S is up-complete & T is up-complete )
proof
let S, T be non empty reflexive antisymmetric RelStr ; ::_thesis: ( [:S,T:] is up-complete implies ( S is up-complete & T is up-complete ) )
assume A1: [:S,T:] is up-complete ; ::_thesis: ( S is up-complete & T is up-complete )
thus S is up-complete ::_thesis: T is up-complete
proof
set D = the non empty directed Subset of T;
let X be non empty directed Subset of S; :: according to WAYBEL_0:def_39 ::_thesis: ex b1 being Element of the carrier of S st
( X is_<=_than b1 & ( for b2 being Element of the carrier of S holds
( not X is_<=_than b2 or b1 <= b2 ) ) )
consider x being Element of [:S,T:] such that
A2: x is_>=_than [:X, the non empty directed Subset of T:] and
A3: for y being Element of [:S,T:] st y is_>=_than [:X, the non empty directed Subset of T:] holds
x <= y by A1, WAYBEL_0:def_39;
take x `1 ; ::_thesis: ( X is_<=_than x `1 & ( for b1 being Element of the carrier of S holds
( not X is_<=_than b1 or x `1 <= b1 ) ) )
the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then A4: x = [(x `1),(x `2)] by MCART_1:21;
hence x `1 is_>=_than X by A2, YELLOW_3:29; ::_thesis: for b1 being Element of the carrier of S holds
( not X is_<=_than b1 or x `1 <= b1 )
ex_sup_of [:X, the non empty directed Subset of T:],[:S,T:] by A1, WAYBEL_0:75;
then ex_sup_of the non empty directed Subset of T,T by YELLOW_3:39;
then A5: sup the non empty directed Subset of T is_>=_than the non empty directed Subset of T by YELLOW_0:def_9;
let y be Element of S; ::_thesis: ( not X is_<=_than y or x `1 <= y )
assume y is_>=_than X ; ::_thesis: x `1 <= y
then x <= [y,(sup the non empty directed Subset of T)] by A3, A5, YELLOW_3:30;
hence x `1 <= y by A4, YELLOW_3:11; ::_thesis: verum
end;
set D = the non empty directed Subset of S;
let X be non empty directed Subset of T; :: according to WAYBEL_0:def_39 ::_thesis: ex b1 being Element of the carrier of T st
( X is_<=_than b1 & ( for b2 being Element of the carrier of T holds
( not X is_<=_than b2 or b1 <= b2 ) ) )
consider x being Element of [:S,T:] such that
A6: x is_>=_than [: the non empty directed Subset of S,X:] and
A7: for y being Element of [:S,T:] st y is_>=_than [: the non empty directed Subset of S,X:] holds
x <= y by A1, WAYBEL_0:def_39;
ex_sup_of [: the non empty directed Subset of S,X:],[:S,T:] by A1, WAYBEL_0:75;
then ex_sup_of the non empty directed Subset of S,S by YELLOW_3:39;
then A8: sup the non empty directed Subset of S is_>=_than the non empty directed Subset of S by YELLOW_0:def_9;
take x `2 ; ::_thesis: ( X is_<=_than x `2 & ( for b1 being Element of the carrier of T holds
( not X is_<=_than b1 or x `2 <= b1 ) ) )
the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then A9: x = [(x `1),(x `2)] by MCART_1:21;
hence x `2 is_>=_than X by A6, YELLOW_3:29; ::_thesis: for b1 being Element of the carrier of T holds
( not X is_<=_than b1 or x `2 <= b1 )
let y be Element of T; ::_thesis: ( not X is_<=_than y or x `2 <= y )
assume y is_>=_than X ; ::_thesis: x `2 <= y
then x <= [(sup the non empty directed Subset of S),y] by A7, A8, YELLOW_3:30;
hence x `2 <= y by A9, YELLOW_3:11; ::_thesis: verum
end;
theorem Th12: :: WAYBEL_2:12
for L being non empty reflexive antisymmetric up-complete RelStr
for D being non empty directed Subset of [:L,L:] holds sup D = [(sup (proj1 D)),(sup (proj2 D))]
proof
let L be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: for D being non empty directed Subset of [:L,L:] holds sup D = [(sup (proj1 D)),(sup (proj2 D))]
let D be non empty directed Subset of [:L,L:]; ::_thesis: sup D = [(sup (proj1 D)),(sup (proj2 D))]
reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22;
reconsider C = the carrier of L as non empty set ;
reconsider D9 = D as non empty Subset of [:C,C:] by YELLOW_3:def_2;
A1: ex_sup_of D1,L by WAYBEL_0:75;
the carrier of [:L,L:] = [:C,C:] by YELLOW_3:def_2;
then consider d1, d2 being set such that
A2: ( d1 in C & d2 in C ) and
A3: sup D = [d1,d2] by ZFMISC_1:def_2;
A4: ex_sup_of D2,L by WAYBEL_0:75;
reconsider d1 = d1, d2 = d2 as Element of L by A2;
A5: ex_sup_of D,[:L,L:] by WAYBEL_0:75;
D2 is_<=_than d2
proof
let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in D2 or b <= d2 )
assume b in D2 ; ::_thesis: b <= d2
then consider x being set such that
A6: [x,b] in D by XTUPLE_0:def_13;
reconsider x = x as Element of D1 by A6, XTUPLE_0:def_12;
D is_<=_than [d1,d2] by A5, A3, YELLOW_0:def_9;
then [x,b] <= [d1,d2] by A6, LATTICE3:def_9;
hence b <= d2 by YELLOW_3:11; ::_thesis: verum
end;
then A7: sup D2 <= d2 by A4, YELLOW_0:def_9;
D1 is_<=_than d1
proof
let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in D1 or b <= d1 )
assume b in D1 ; ::_thesis: b <= d1
then consider x being set such that
A8: [b,x] in D by XTUPLE_0:def_12;
reconsider x = x as Element of D2 by A8, XTUPLE_0:def_13;
D is_<=_than [d1,d2] by A5, A3, YELLOW_0:def_9;
then [b,x] <= [d1,d2] by A8, LATTICE3:def_9;
hence b <= d1 by YELLOW_3:11; ::_thesis: verum
end;
then sup D1 <= d1 by A1, YELLOW_0:def_9;
then A9: [(sup D1),(sup D2)] <= sup D by A3, A7, YELLOW_3:11;
A10: ex_sup_of [:D1,D2:],[:L,L:] by WAYBEL_0:75;
reconsider D1 = D1, D2 = D2 as non empty Subset of L ;
D9 c= [:D1,D2:] by YELLOW_3:1;
then sup D <= sup [:D1,D2:] by A5, A10, YELLOW_0:34;
then sup D <= [(sup (proj1 D)),(sup (proj2 D))] by A1, A4, YELLOW_3:43;
hence sup D = [(sup (proj1 D)),(sup (proj2 D))] by A9, ORDERS_2:2; ::_thesis: verum
end;
theorem Th13: :: WAYBEL_2:13
for S1, S2 being RelStr
for D being Subset of S1
for f being Function of S1,S2 st f is monotone holds
f .: (downarrow D) c= downarrow (f .: D)
proof
let S1, S2 be RelStr ; ::_thesis: for D being Subset of S1
for f being Function of S1,S2 st f is monotone holds
f .: (downarrow D) c= downarrow (f .: D)
let D be Subset of S1; ::_thesis: for f being Function of S1,S2 st f is monotone holds
f .: (downarrow D) c= downarrow (f .: D)
let f be Function of S1,S2; ::_thesis: ( f is monotone implies f .: (downarrow D) c= downarrow (f .: D) )
assume A1: f is monotone ; ::_thesis: f .: (downarrow D) c= downarrow (f .: D)
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in f .: (downarrow D) or q in downarrow (f .: D) )
assume A2: q in f .: (downarrow D) ; ::_thesis: q in downarrow (f .: D)
then consider x being set such that
A3: x in dom f and
A4: x in downarrow D and
A5: q = f . x by FUNCT_1:def_6;
reconsider s1 = S1, s2 = S2 as non empty RelStr by A2;
reconsider x = x as Element of s1 by A3;
consider y being Element of s1 such that
A6: x <= y and
A7: y in D by A4, WAYBEL_0:def_15;
reconsider f1 = f as Function of s1,s2 ;
f1 . x is Element of s2 ;
then reconsider q1 = q, fy = f1 . y as Element of s2 by A5;
the carrier of s2 <> {} ;
then dom f = the carrier of s1 by FUNCT_2:def_1;
then A8: f . y in f .: D by A7, FUNCT_1:def_6;
q1 <= fy by A1, A5, A6, ORDERS_3:def_5;
hence q in downarrow (f .: D) by A8, WAYBEL_0:def_15; ::_thesis: verum
end;
theorem Th14: :: WAYBEL_2:14
for S1, S2 being RelStr
for D being Subset of S1
for f being Function of S1,S2 st f is monotone holds
f .: (uparrow D) c= uparrow (f .: D)
proof
let S1, S2 be RelStr ; ::_thesis: for D being Subset of S1
for f being Function of S1,S2 st f is monotone holds
f .: (uparrow D) c= uparrow (f .: D)
let D be Subset of S1; ::_thesis: for f being Function of S1,S2 st f is monotone holds
f .: (uparrow D) c= uparrow (f .: D)
let f be Function of S1,S2; ::_thesis: ( f is monotone implies f .: (uparrow D) c= uparrow (f .: D) )
assume A1: f is monotone ; ::_thesis: f .: (uparrow D) c= uparrow (f .: D)
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in f .: (uparrow D) or q in uparrow (f .: D) )
assume A2: q in f .: (uparrow D) ; ::_thesis: q in uparrow (f .: D)
then consider x being set such that
A3: x in dom f and
A4: x in uparrow D and
A5: q = f . x by FUNCT_1:def_6;
reconsider s1 = S1, s2 = S2 as non empty RelStr by A2;
reconsider x = x as Element of s1 by A3;
consider y being Element of s1 such that
A6: y <= x and
A7: y in D by A4, WAYBEL_0:def_16;
reconsider f1 = f as Function of s1,s2 ;
f1 . x is Element of s2 ;
then reconsider q1 = q, fy = f1 . y as Element of s2 by A5;
the carrier of s2 <> {} ;
then dom f = the carrier of s1 by FUNCT_2:def_1;
then A8: f . y in f .: D by A7, FUNCT_1:def_6;
fy <= q1 by A1, A5, A6, ORDERS_3:def_5;
hence q in uparrow (f .: D) by A8, WAYBEL_0:def_16; ::_thesis: verum
end;
registration
cluster1 -element reflexive -> 1 -element reflexive distributive complemented for RelStr ;
coherence
for b1 being 1 -element reflexive RelStr holds
( b1 is distributive & b1 is complemented )
proof
let L be 1 -element reflexive RelStr ; ::_thesis: ( L is distributive & L is complemented )
thus L is distributive ::_thesis: L is complemented
proof
let x, y, z be Element of L; :: according to WAYBEL_1:def_3 ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
thus x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by STRUCT_0:def_10; ::_thesis: verum
end;
let x be Element of L; :: according to WAYBEL_1:def_24 ::_thesis: ex b1 being Element of the carrier of L st b1 is_a_complement_of x
take y = x; ::_thesis: y is_a_complement_of x
thus x "\/" y = Top L by STRUCT_0:def_10; :: according to WAYBEL_1:def_23 ::_thesis: x "/\" y = Bottom L
thus x "/\" y = Bottom L by STRUCT_0:def_10; ::_thesis: verum
end;
end;
registration
cluster non empty 1 -element strict V70() reflexive transitive antisymmetric non void with_suprema with_infima for RelStr ;
existence
ex b1 being LATTICE st
( b1 is strict & b1 is 1 -element )
proof
set B = the 1 -element strict reflexive RelStr ;
take the 1 -element strict reflexive RelStr ; ::_thesis: ( the 1 -element strict reflexive RelStr is strict & the 1 -element strict reflexive RelStr is 1 -element )
thus ( the 1 -element strict reflexive RelStr is strict & the 1 -element strict reflexive RelStr is 1 -element ) ; ::_thesis: verum
end;
end;
theorem Th15: :: WAYBEL_2:15
for H being distributive complete LATTICE
for a being Element of H
for X being finite Subset of H holds sup ({a} "/\" X) = a "/\" (sup X)
proof
let H be distributive complete LATTICE; ::_thesis: for a being Element of H
for X being finite Subset of H holds sup ({a} "/\" X) = a "/\" (sup X)
let a be Element of H; ::_thesis: for X being finite Subset of H holds sup ({a} "/\" X) = a "/\" (sup X)
let X be finite Subset of H; ::_thesis: sup ({a} "/\" X) = a "/\" (sup X)
defpred S1[ set ] means ex A being Subset of H st
( A = $1 & a "/\" (sup A) = sup ({a} "/\" A) );
A1: S1[ {} ]
proof
reconsider A = {} as Subset of H by XBOOLE_1:2;
take A ; ::_thesis: ( A = {} & a "/\" (sup A) = sup ({a} "/\" A) )
thus A = {} ; ::_thesis: a "/\" (sup A) = sup ({a} "/\" A)
( Bottom H <= a & {a} "/\" ({} H) = {} ) by YELLOW_0:44, YELLOW_4:36;
hence a "/\" (sup A) = sup ({a} "/\" A) by YELLOW_0:25; ::_thesis: verum
end;
A2: for x, B being set st x in X & B c= X & S1[B] holds
S1[B \/ {x}]
proof
let x, B be set ; ::_thesis: ( x in X & B c= X & S1[B] implies S1[B \/ {x}] )
assume that
A3: x in X and
A4: B c= X and
A5: S1[B] ; ::_thesis: S1[B \/ {x}]
reconsider x1 = x as Element of H by A3;
A6: {x1} c= the carrier of H ;
B c= the carrier of H by A4, XBOOLE_1:1;
then reconsider C = B \/ {x} as Subset of H by A6, XBOOLE_1:8;
take C ; ::_thesis: ( C = B \/ {x} & a "/\" (sup C) = sup ({a} "/\" C) )
thus C = B \/ {x} ; ::_thesis: a "/\" (sup C) = sup ({a} "/\" C)
consider A being Subset of H such that
A7: A = B and
A8: a "/\" (sup A) = sup ({a} "/\" A) by A5;
A9: {a} "/\" C = ({a} "/\" A) \/ ({a} "/\" {x1}) by A7, YELLOW_4:43
.= ({a} "/\" A) \/ {(a "/\" x1)} by YELLOW_4:46 ;
A10: ( ex_sup_of {a} "/\" A,H & ex_sup_of {(a "/\" x1)},H ) by YELLOW_0:17;
( ex_sup_of B,H & ex_sup_of {x},H ) by YELLOW_0:17;
hence a "/\" (sup C) = a "/\" (("\/" (B,H)) "\/" ("\/" ({x},H))) by YELLOW_2:3
.= (sup ({a} "/\" A)) "\/" (a "/\" ("\/" ({x},H))) by A7, A8, WAYBEL_1:def_3
.= (sup ({a} "/\" A)) "\/" (a "/\" x1) by YELLOW_0:39
.= (sup ({a} "/\" A)) "\/" (sup {(a "/\" x1)}) by YELLOW_0:39
.= sup ({a} "/\" C) by A10, A9, YELLOW_2:3 ;
::_thesis: verum
end;
A11: X is finite ;
S1[X] from FINSET_1:sch_2(A11, A1, A2);
hence sup ({a} "/\" X) = a "/\" (sup X) ; ::_thesis: verum
end;
theorem :: WAYBEL_2:16
for H being distributive complete LATTICE
for a being Element of H
for X being finite Subset of H holds inf ({a} "\/" X) = a "\/" (inf X)
proof
let H be distributive complete LATTICE; ::_thesis: for a being Element of H
for X being finite Subset of H holds inf ({a} "\/" X) = a "\/" (inf X)
let a be Element of H; ::_thesis: for X being finite Subset of H holds inf ({a} "\/" X) = a "\/" (inf X)
let X be finite Subset of H; ::_thesis: inf ({a} "\/" X) = a "\/" (inf X)
defpred S1[ set ] means ex A being Subset of H st
( A = $1 & a "\/" (inf A) = inf ({a} "\/" A) );
A1: S1[ {} ]
proof
reconsider A = {} as Subset of H by XBOOLE_1:2;
take A ; ::_thesis: ( A = {} & a "\/" (inf A) = inf ({a} "\/" A) )
thus A = {} ; ::_thesis: a "\/" (inf A) = inf ({a} "\/" A)
( a <= Top H & {a} "\/" ({} H) = {} ) by YELLOW_0:45, YELLOW_4:9;
hence a "\/" (inf A) = inf ({a} "\/" A) by YELLOW_0:24; ::_thesis: verum
end;
A2: for x, B being set st x in X & B c= X & S1[B] holds
S1[B \/ {x}]
proof
let x, B be set ; ::_thesis: ( x in X & B c= X & S1[B] implies S1[B \/ {x}] )
assume that
A3: x in X and
A4: B c= X and
A5: S1[B] ; ::_thesis: S1[B \/ {x}]
reconsider x1 = x as Element of H by A3;
A6: {x1} c= the carrier of H ;
B c= the carrier of H by A4, XBOOLE_1:1;
then reconsider C = B \/ {x} as Subset of H by A6, XBOOLE_1:8;
take C ; ::_thesis: ( C = B \/ {x} & a "\/" (inf C) = inf ({a} "\/" C) )
thus C = B \/ {x} ; ::_thesis: a "\/" (inf C) = inf ({a} "\/" C)
consider A being Subset of H such that
A7: A = B and
A8: a "\/" (inf A) = inf ({a} "\/" A) by A5;
A9: {a} "\/" C = ({a} "\/" A) \/ ({a} "\/" {x1}) by A7, YELLOW_4:16
.= ({a} "\/" A) \/ {(a "\/" x1)} by YELLOW_4:19 ;
A10: ( ex_inf_of {a} "\/" A,H & ex_inf_of {(a "\/" x1)},H ) by YELLOW_0:17;
( ex_inf_of B,H & ex_inf_of {x},H ) by YELLOW_0:17;
hence a "\/" (inf C) = a "\/" (("/\" (B,H)) "/\" ("/\" ({x},H))) by YELLOW_2:4
.= (inf ({a} "\/" A)) "/\" (a "\/" ("/\" ({x},H))) by A7, A8, WAYBEL_1:5
.= (inf ({a} "\/" A)) "/\" (a "\/" x1) by YELLOW_0:39
.= (inf ({a} "\/" A)) "/\" (inf {(a "\/" x1)}) by YELLOW_0:39
.= inf ({a} "\/" C) by A10, A9, YELLOW_2:4 ;
::_thesis: verum
end;
A11: X is finite ;
S1[X] from FINSET_1:sch_2(A11, A1, A2);
hence inf ({a} "\/" X) = a "\/" (inf X) ; ::_thesis: verum
end;
theorem Th17: :: WAYBEL_2:17
for H being distributive complete LATTICE
for a being Element of H
for X being finite Subset of H holds a "/\" preserves_sup_of X
proof
let H be distributive complete LATTICE; ::_thesis: for a being Element of H
for X being finite Subset of H holds a "/\" preserves_sup_of X
let a be Element of H; ::_thesis: for X being finite Subset of H holds a "/\" preserves_sup_of X
let X be finite Subset of H; ::_thesis: a "/\" preserves_sup_of X
assume ex_sup_of X,H ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (a "/\") .: X,H & "\/" (((a "/\") .: X),H) = (a "/\") . ("\/" (X,H)) )
thus ex_sup_of (a "/\") .: X,H by YELLOW_0:17; ::_thesis: "\/" (((a "/\") .: X),H) = (a "/\") . ("\/" (X,H))
thus sup ((a "/\") .: X) = "\/" ( { (a "/\" y) where y is Element of H : y in X } ,H) by WAYBEL_1:61
.= sup ({a} "/\" X) by YELLOW_4:42
.= a "/\" (sup X) by Th15
.= (a "/\") . (sup X) by WAYBEL_1:def_18 ; ::_thesis: verum
end;
begin
scheme :: WAYBEL_2:sch 1
ExNet{ F1() -> non empty RelStr , F2() -> prenet of F1(), F3( set ) -> Element of F1() } :
ex M being prenet of F1() st
( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of F2(), the InternalRel of F2() #) & ( for i being Element of M holds the mapping of M . i = F3(( the mapping of F2() . i)) ) )
proof
deffunc H1( Element of F2()) -> Element of F1() = F3(( the mapping of F2() . $1));
A1: for i being Element of F2() holds H1(i) in the carrier of F1() ;
consider f being Function of the carrier of F2(), the carrier of F1() such that
A2: for i being Element of F2() holds f . i = H1(i) from FUNCT_2:sch_8(A1);
set M = NetStr(# the carrier of F2(), the InternalRel of F2(),f #);
( RelStr(# the carrier of NetStr(# the carrier of F2(), the InternalRel of F2(),f #), the InternalRel of NetStr(# the carrier of F2(), the InternalRel of F2(),f #) #) = RelStr(# the carrier of F2(), the InternalRel of F2() #) & [#] F2() is directed ) by WAYBEL_0:def_6;
then [#] NetStr(# the carrier of F2(), the InternalRel of F2(),f #) is directed by WAYBEL_0:3;
then reconsider M = NetStr(# the carrier of F2(), the InternalRel of F2(),f #) as prenet of F1() by WAYBEL_0:def_6;
take M ; ::_thesis: ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of F2(), the InternalRel of F2() #) & ( for i being Element of M holds the mapping of M . i = F3(( the mapping of F2() . i)) ) )
thus ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of F2(), the InternalRel of F2() #) & ( for i being Element of M holds the mapping of M . i = F3(( the mapping of F2() . i)) ) ) by A2; ::_thesis: verum
end;
theorem Th18: :: WAYBEL_2:18
for L being non empty RelStr
for N being prenet of L st N is eventually-directed holds
rng (netmap (N,L)) is directed
proof
let L be non empty RelStr ; ::_thesis: for N being prenet of L st N is eventually-directed holds
rng (netmap (N,L)) is directed
let N be prenet of L; ::_thesis: ( N is eventually-directed implies rng (netmap (N,L)) is directed )
assume A1: N is eventually-directed ; ::_thesis: rng (netmap (N,L)) is directed
set f = netmap (N,L);
let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in rng (netmap (N,L)) or not y in rng (netmap (N,L)) or ex b1 being Element of the carrier of L st
( b1 in rng (netmap (N,L)) & x <= b1 & y <= b1 ) )
assume that
A2: x in rng (netmap (N,L)) and
A3: y in rng (netmap (N,L)) ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in rng (netmap (N,L)) & x <= b1 & y <= b1 )
consider a being set such that
A4: a in dom (netmap (N,L)) and
A5: (netmap (N,L)) . a = x by A2, FUNCT_1:def_3;
consider b being set such that
A6: b in dom (netmap (N,L)) and
A7: (netmap (N,L)) . b = y by A3, FUNCT_1:def_3;
reconsider a = a, b = b as Element of N by A4, A6;
consider ja being Element of N such that
A8: for k being Element of N st ja <= k holds
N . a <= N . k by A1, WAYBEL_0:11;
consider jb being Element of N such that
A9: for k being Element of N st jb <= k holds
N . b <= N . k by A1, WAYBEL_0:11;
[#] N is directed by WAYBEL_0:def_6;
then consider c being Element of N such that
c in [#] N and
A10: ( ja <= c & jb <= c ) by WAYBEL_0:def_1;
take z = (netmap (N,L)) . c; ::_thesis: ( z in rng (netmap (N,L)) & x <= z & y <= z )
dom (netmap (N,L)) = the carrier of N by FUNCT_2:def_1;
hence z in rng (netmap (N,L)) by FUNCT_1:def_3; ::_thesis: ( x <= z & y <= z )
N . c = (netmap (N,L)) . c ;
hence ( x <= z & y <= z ) by A5, A7, A8, A9, A10; ::_thesis: verum
end;
theorem Th19: :: WAYBEL_2:19
for L being non empty reflexive RelStr
for D being non empty directed Subset of L
for n being Function of D, the carrier of L holds NetStr(# D,( the InternalRel of L |_2 D),n #) is prenet of L
proof
let L be non empty reflexive RelStr ; ::_thesis: for D being non empty directed Subset of L
for n being Function of D, the carrier of L holds NetStr(# D,( the InternalRel of L |_2 D),n #) is prenet of L
let D be non empty directed Subset of L; ::_thesis: for n being Function of D, the carrier of L holds NetStr(# D,( the InternalRel of L |_2 D),n #) is prenet of L
let n be Function of D, the carrier of L; ::_thesis: NetStr(# D,( the InternalRel of L |_2 D),n #) is prenet of L
set N = NetStr(# D,( the InternalRel of L |_2 D),n #);
NetStr(# D,( the InternalRel of L |_2 D),n #) is directed
proof
let x, y be Element of NetStr(# D,( the InternalRel of L |_2 D),n #); :: according to WAYBEL_0:def_1,WAYBEL_0:def_6 ::_thesis: ( not x in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) or not y in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) or ex b1 being Element of the carrier of NetStr(# D,( the InternalRel of L |_2 D),n #) st
( b1 in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) & x <= b1 & y <= b1 ) )
assume that
x in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) and
y in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) ; ::_thesis: ex b1 being Element of the carrier of NetStr(# D,( the InternalRel of L |_2 D),n #) st
( b1 in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) & x <= b1 & y <= b1 )
reconsider x1 = x, y1 = y as Element of D ;
consider z1 being Element of L such that
A1: z1 in D and
A2: ( x1 <= z1 & y1 <= z1 ) by WAYBEL_0:def_1;
reconsider z = z1 as Element of NetStr(# D,( the InternalRel of L |_2 D),n #) by A1;
take z ; ::_thesis: ( z in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) & x <= z & y <= z )
thus z in [#] NetStr(# D,( the InternalRel of L |_2 D),n #) ; ::_thesis: ( x <= z & y <= z )
the InternalRel of NetStr(# D,( the InternalRel of L |_2 D),n #) c= the InternalRel of L by XBOOLE_1:17;
then reconsider N = NetStr(# D,( the InternalRel of L |_2 D),n #) as SubRelStr of L by YELLOW_0:def_13;
N is full by YELLOW_0:def_14;
hence ( x <= z & y <= z ) by A2, YELLOW_0:60; ::_thesis: verum
end;
hence NetStr(# D,( the InternalRel of L |_2 D),n #) is prenet of L ; ::_thesis: verum
end;
theorem Th20: :: WAYBEL_2:20
for L being non empty reflexive RelStr
for D being non empty directed Subset of L
for n being Function of D, the carrier of L
for N being prenet of L st n = id D & N = NetStr(# D,( the InternalRel of L |_2 D),n #) holds
N is eventually-directed
proof
let L be non empty reflexive RelStr ; ::_thesis: for D being non empty directed Subset of L
for n being Function of D, the carrier of L
for N being prenet of L st n = id D & N = NetStr(# D,( the InternalRel of L |_2 D),n #) holds
N is eventually-directed
let D be non empty directed Subset of L; ::_thesis: for n being Function of D, the carrier of L
for N being prenet of L st n = id D & N = NetStr(# D,( the InternalRel of L |_2 D),n #) holds
N is eventually-directed
let n be Function of D, the carrier of L; ::_thesis: for N being prenet of L st n = id D & N = NetStr(# D,( the InternalRel of L |_2 D),n #) holds
N is eventually-directed
let N be prenet of L; ::_thesis: ( n = id D & N = NetStr(# D,( the InternalRel of L |_2 D),n #) implies N is eventually-directed )
assume that
A1: n = id D and
A2: N = NetStr(# D,( the InternalRel of L |_2 D),n #) ; ::_thesis: N is eventually-directed
for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds
N . i <= N . k
proof
let i be Element of N; ::_thesis: ex j being Element of N st
for k being Element of N st j <= k holds
N . i <= N . k
take j = i; ::_thesis: for k being Element of N st j <= k holds
N . i <= N . k
let k be Element of N; ::_thesis: ( j <= k implies N . i <= N . k )
assume A3: j <= k ; ::_thesis: N . i <= N . k
the InternalRel of N c= the InternalRel of L by A2, XBOOLE_1:17;
then A4: N is SubRelStr of L by A2, YELLOW_0:def_13;
reconsider nj = n . j, nk = n . k as Element of L by A2, FUNCT_2:5;
( nj = j & nk = k ) by A1, A2, FUNCT_1:18;
hence N . i <= N . k by A2, A3, A4, YELLOW_0:59; ::_thesis: verum
end;
hence N is eventually-directed by WAYBEL_0:11; ::_thesis: verum
end;
definition
let L be non empty RelStr ;
let N be NetStr over L;
func sup N -> Element of L equals :: WAYBEL_2:def 1
Sup ;
coherence
Sup is Element of L ;
end;
:: deftheorem defines sup WAYBEL_2:def_1_:_
for L being non empty RelStr
for N being NetStr over L holds sup N = Sup ;
definition
let L be non empty RelStr ;
let J be set ;
let f be Function of J, the carrier of L;
func FinSups f -> prenet of L means :Def2: :: WAYBEL_2:def 2
ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & it = NetStr(# (Fin J),(RelIncl (Fin J)),g #) );
existence
ex b1 being prenet of L ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & b1 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) )
proof
deffunc H1( Element of Fin J) -> Element of the carrier of L = sup (f .: $1);
A1: for x being Element of Fin J holds H1(x) in the carrier of L ;
consider g being Function of (Fin J), the carrier of L such that
A2: for x being Element of Fin J holds g . x = H1(x) from FUNCT_2:sch_8(A1);
set M = NetStr(# (Fin J),(RelIncl (Fin J)),g #);
NetStr(# (Fin J),(RelIncl (Fin J)),g #) is directed
proof
let x, y be Element of NetStr(# (Fin J),(RelIncl (Fin J)),g #); :: according to WAYBEL_0:def_1,WAYBEL_0:def_6 ::_thesis: ( not x in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) or not y in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) or ex b1 being Element of the carrier of NetStr(# (Fin J),(RelIncl (Fin J)),g #) st
( b1 in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) & x <= b1 & y <= b1 ) )
assume that
x in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) and
y in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) ; ::_thesis: ex b1 being Element of the carrier of NetStr(# (Fin J),(RelIncl (Fin J)),g #) st
( b1 in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) & x <= b1 & y <= b1 )
reconsider x1 = x, y1 = y as Element of Fin J ;
reconsider z = x1 \/ y1 as Element of NetStr(# (Fin J),(RelIncl (Fin J)),g #) ;
take z ; ::_thesis: ( z in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) & x <= z & y <= z )
thus z in [#] NetStr(# (Fin J),(RelIncl (Fin J)),g #) ; ::_thesis: ( x <= z & y <= z )
A3: InclPoset (Fin J) = RelStr(# (Fin J),(RelIncl (Fin J)) #) by YELLOW_1:def_1;
then reconsider x2 = x, y2 = y, z1 = z as Element of (InclPoset (Fin J)) ;
y c= z by XBOOLE_1:7;
then A4: y2 <= z1 by YELLOW_1:3;
x c= z by XBOOLE_1:7;
then x2 <= z1 by YELLOW_1:3;
hence ( x <= z & y <= z ) by A3, A4, YELLOW_0:1; ::_thesis: verum
end;
then reconsider M = NetStr(# (Fin J),(RelIncl (Fin J)),g #) as prenet of L ;
take M ; ::_thesis: ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & M = NetStr(# (Fin J),(RelIncl (Fin J)),g #) )
thus ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & M = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being prenet of L st ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & b1 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) & ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & b2 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) holds
b1 = b2
proof
let A, B be prenet of L; ::_thesis: ( ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & A = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) & ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & B = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) implies A = B )
assume that
A5: ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & A = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) and
A6: ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & B = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) ; ::_thesis: A = B
consider g1 being Function of (Fin J), the carrier of L such that
A7: for x being Element of Fin J holds
( g1 . x = sup (f .: x) & A = NetStr(# (Fin J),(RelIncl (Fin J)),g1 #) ) by A5;
consider g2 being Function of (Fin J), the carrier of L such that
A8: for x being Element of Fin J holds
( g2 . x = sup (f .: x) & B = NetStr(# (Fin J),(RelIncl (Fin J)),g2 #) ) by A6;
for x being set st x in Fin J holds
g1 . x = g2 . x
proof
let x be set ; ::_thesis: ( x in Fin J implies g1 . x = g2 . x )
assume A9: x in Fin J ; ::_thesis: g1 . x = g2 . x
hence g1 . x = sup (f .: x) by A7
.= g2 . x by A8, A9 ;
::_thesis: verum
end;
hence A = B by A7, A8, FUNCT_2:12; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines FinSups WAYBEL_2:def_2_:_
for L being non empty RelStr
for J being set
for f being Function of J, the carrier of L
for b4 being prenet of L holds
( b4 = FinSups f iff ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & b4 = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) );
theorem :: WAYBEL_2:21
for L being non empty RelStr
for J, x being set
for f being Function of J, the carrier of L holds
( x is Element of (FinSups f) iff x is Element of Fin J )
proof
let L be non empty RelStr ; ::_thesis: for J, x being set
for f being Function of J, the carrier of L holds
( x is Element of (FinSups f) iff x is Element of Fin J )
let J, x be set ; ::_thesis: for f being Function of J, the carrier of L holds
( x is Element of (FinSups f) iff x is Element of Fin J )
let f be Function of J, the carrier of L; ::_thesis: ( x is Element of (FinSups f) iff x is Element of Fin J )
ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & FinSups f = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) by Def2;
hence ( x is Element of (FinSups f) iff x is Element of Fin J ) ; ::_thesis: verum
end;
registration
let L be non empty reflexive antisymmetric complete RelStr ;
let J be set ;
let f be Function of J, the carrier of L;
cluster FinSups f -> monotone ;
coherence
FinSups f is monotone
proof
let x, y be Element of (FinSups f); :: according to ORDERS_3:def_5,WAYBEL_0:def_9 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of L holds
( not b1 = (netmap ((FinSups f),L)) . x or not b2 = (netmap ((FinSups f),L)) . y or b1 <= b2 ) )
assume A1: x <= y ; ::_thesis: for b1, b2 being Element of the carrier of L holds
( not b1 = (netmap ((FinSups f),L)) . x or not b2 = (netmap ((FinSups f),L)) . y or b1 <= b2 )
consider g being Function of (Fin J), the carrier of L such that
A2: for x being Element of Fin J holds
( g . x = sup (f .: x) & FinSups f = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) by Def2;
g . x = sup (f .: x) by A2;
then reconsider fx = g . x as Element of L ;
A3: InclPoset (Fin J) = RelStr(# (Fin J),(RelIncl (Fin J)) #) by YELLOW_1:def_1;
then reconsider x1 = x, y1 = y as Element of (InclPoset (Fin J)) by A2;
A4: ( ex_sup_of f .: x,L & ex_sup_of f .: y,L ) by YELLOW_0:17;
x1 <= y1 by A1, A2, A3, YELLOW_0:1;
then x c= y by YELLOW_1:3;
then sup (f .: x) <= sup (f .: y) by A4, RELAT_1:123, YELLOW_0:34;
then A5: fx <= sup (f .: y) by A2;
let a, b be Element of L; ::_thesis: ( not a = (netmap ((FinSups f),L)) . x or not b = (netmap ((FinSups f),L)) . y or a <= b )
assume ( a = (netmap ((FinSups f),L)) . x & b = (netmap ((FinSups f),L)) . y ) ; ::_thesis: a <= b
hence a <= b by A2, A5; ::_thesis: verum
end;
end;
definition
let L be non empty RelStr ;
let x be Element of L;
let N be non empty NetStr over L;
funcx "/\" N -> strict NetStr over L means :Def3: :: WAYBEL_2:def 3
( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of it ex y being Element of L st
( y = the mapping of N . i & the mapping of it . i = x "/\" y ) ) );
existence
ex b1 being strict NetStr over L st
( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of b1 ex y being Element of L st
( y = the mapping of N . i & the mapping of b1 . i = x "/\" y ) ) )
proof
defpred S1[ set , set ] means ex y being Element of L st
( y = the mapping of N . $1 & $2 = x "/\" y );
A1: for e being Element of N ex u being Element of L st S1[e,u]
proof
let e be Element of N; ::_thesis: ex u being Element of L st S1[e,u]
take x "/\" ( the mapping of N . e) ; ::_thesis: S1[e,x "/\" ( the mapping of N . e)]
take the mapping of N . e ; ::_thesis: ( the mapping of N . e = the mapping of N . e & x "/\" ( the mapping of N . e) = x "/\" ( the mapping of N . e) )
thus ( the mapping of N . e = the mapping of N . e & x "/\" ( the mapping of N . e) = x "/\" ( the mapping of N . e) ) ; ::_thesis: verum
end;
ex g being Function of the carrier of N, the carrier of L st
for i being Element of N holds S1[i,g . i] from FUNCT_2:sch_3(A1);
then consider g being Function of the carrier of N, the carrier of L such that
A2: for i being Element of N ex y being Element of L st
( y = the mapping of N . i & g . i = x "/\" y ) ;
take NetStr(# the carrier of N, the InternalRel of N,g #) ; ::_thesis: ( RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,g #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,g #) #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of NetStr(# the carrier of N, the InternalRel of N,g #) ex y being Element of L st
( y = the mapping of N . i & the mapping of NetStr(# the carrier of N, the InternalRel of N,g #) . i = x "/\" y ) ) )
thus ( RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,g #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,g #) #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of NetStr(# the carrier of N, the InternalRel of N,g #) ex y being Element of L st
( y = the mapping of N . i & the mapping of NetStr(# the carrier of N, the InternalRel of N,g #) . i = x "/\" y ) ) ) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict NetStr over L st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of b1 ex y being Element of L st
( y = the mapping of N . i & the mapping of b1 . i = x "/\" y ) ) & RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of b2 ex y being Element of L st
( y = the mapping of N . i & the mapping of b2 . i = x "/\" y ) ) holds
b1 = b2
proof
let A, B be strict NetStr over L; ::_thesis: ( RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of A ex y being Element of L st
( y = the mapping of N . i & the mapping of A . i = x "/\" y ) ) & RelStr(# the carrier of B, the InternalRel of B #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of B ex y being Element of L st
( y = the mapping of N . i & the mapping of B . i = x "/\" y ) ) implies A = B )
assume that
A3: RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of N, the InternalRel of N #) and
A4: for i being Element of A ex y being Element of L st
( y = the mapping of N . i & the mapping of A . i = x "/\" y ) and
A5: RelStr(# the carrier of B, the InternalRel of B #) = RelStr(# the carrier of N, the InternalRel of N #) and
A6: for i being Element of B ex y being Element of L st
( y = the mapping of N . i & the mapping of B . i = x "/\" y ) ; ::_thesis: A = B
reconsider C = the carrier of A as non empty set by A3;
reconsider f1 = the mapping of A, f2 = the mapping of B as Function of C, the carrier of L by A3, A5;
for c being Element of C holds f1 . c = f2 . c
proof
let c be Element of C; ::_thesis: f1 . c = f2 . c
( ex ya being Element of L st
( ya = the mapping of N . c & f1 . c = x "/\" ya ) & ex yb being Element of L st
( yb = the mapping of N . c & f2 . c = x "/\" yb ) ) by A3, A4, A5, A6;
hence f1 . c = f2 . c ; ::_thesis: verum
end;
hence A = B by A3, A5, FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines "/\" WAYBEL_2:def_3_:_
for L being non empty RelStr
for x being Element of L
for N being non empty NetStr over L
for b4 being strict NetStr over L holds
( b4 = x "/\" N iff ( RelStr(# the carrier of b4, the InternalRel of b4 #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of b4 ex y being Element of L st
( y = the mapping of N . i & the mapping of b4 . i = x "/\" y ) ) ) );
theorem Th22: :: WAYBEL_2:22
for L being non empty RelStr
for N being non empty NetStr over L
for x being Element of L
for y being set holds
( y is Element of N iff y is Element of (x "/\" N) )
proof
let L be non empty RelStr ; ::_thesis: for N being non empty NetStr over L
for x being Element of L
for y being set holds
( y is Element of N iff y is Element of (x "/\" N) )
let N be non empty NetStr over L; ::_thesis: for x being Element of L
for y being set holds
( y is Element of N iff y is Element of (x "/\" N) )
let x be Element of L; ::_thesis: for y being set holds
( y is Element of N iff y is Element of (x "/\" N) )
let y be set ; ::_thesis: ( y is Element of N iff y is Element of (x "/\" N) )
RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def3;
hence ( y is Element of N iff y is Element of (x "/\" N) ) ; ::_thesis: verum
end;
registration
let L be non empty RelStr ;
let x be Element of L;
let N be non empty NetStr over L;
clusterx "/\" N -> non empty strict ;
coherence
not x "/\" N is empty
proof
RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def3;
hence not x "/\" N is empty ; ::_thesis: verum
end;
end;
registration
let L be non empty RelStr ;
let x be Element of L;
let N be prenet of L;
clusterx "/\" N -> strict directed ;
coherence
x "/\" N is directed
proof
( RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) = RelStr(# the carrier of N, the InternalRel of N #) & [#] N is directed ) by Def3, WAYBEL_0:def_6;
hence [#] (x "/\" N) is directed by WAYBEL_0:3; :: according to WAYBEL_0:def_6 ::_thesis: verum
end;
end;
theorem Th23: :: WAYBEL_2:23
for L being non empty RelStr
for x being Element of L
for F being non empty NetStr over L holds rng the mapping of (x "/\" F) = {x} "/\" (rng the mapping of F)
proof
let L be non empty RelStr ; ::_thesis: for x being Element of L
for F being non empty NetStr over L holds rng the mapping of (x "/\" F) = {x} "/\" (rng the mapping of F)
let x be Element of L; ::_thesis: for F being non empty NetStr over L holds rng the mapping of (x "/\" F) = {x} "/\" (rng the mapping of F)
let F be non empty NetStr over L; ::_thesis: rng the mapping of (x "/\" F) = {x} "/\" (rng the mapping of F)
set f = the mapping of F;
set h = the mapping of (x "/\" F);
set A = rng the mapping of F;
A1: {x} "/\" (rng the mapping of F) = { (x "/\" y) where y is Element of L : y in rng the mapping of F } by YELLOW_4:42;
A2: RelStr(# the carrier of (x "/\" F), the InternalRel of (x "/\" F) #) = RelStr(# the carrier of F, the InternalRel of F #) by Def3;
then A3: dom the mapping of (x "/\" F) = the carrier of F by FUNCT_2:def_1;
A4: dom the mapping of F = the carrier of F by FUNCT_2:def_1;
thus rng the mapping of (x "/\" F) c= {x} "/\" (rng the mapping of F) :: according to XBOOLE_0:def_10 ::_thesis: {x} "/\" (rng the mapping of F) c= rng the mapping of (x "/\" F)
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in rng the mapping of (x "/\" F) or q in {x} "/\" (rng the mapping of F) )
assume q in rng the mapping of (x "/\" F) ; ::_thesis: q in {x} "/\" (rng the mapping of F)
then consider a being set such that
A5: a in dom the mapping of (x "/\" F) and
A6: q = the mapping of (x "/\" F) . a by FUNCT_1:def_3;
reconsider a = a as Element of (x "/\" F) by A5;
consider y being Element of L such that
A7: y = the mapping of F . a and
A8: the mapping of (x "/\" F) . a = x "/\" y by Def3;
y in rng the mapping of F by A2, A4, A7, FUNCT_1:def_3;
hence q in {x} "/\" (rng the mapping of F) by A1, A6, A8; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {x} "/\" (rng the mapping of F) or q in rng the mapping of (x "/\" F) )
assume q in {x} "/\" (rng the mapping of F) ; ::_thesis: q in rng the mapping of (x "/\" F)
then consider y being Element of L such that
A9: q = x "/\" y and
A10: y in rng the mapping of F by A1;
consider z being set such that
A11: z in dom the mapping of F and
A12: y = the mapping of F . z by A10, FUNCT_1:def_3;
reconsider z = z as Element of (x "/\" F) by A2, A11;
ex w being Element of L st
( w = the mapping of F . z & the mapping of (x "/\" F) . z = x "/\" w ) by Def3;
hence q in rng the mapping of (x "/\" F) by A3, A9, A11, A12, FUNCT_1:def_3; ::_thesis: verum
end;
theorem Th24: :: WAYBEL_2:24
for L being non empty RelStr
for J being set
for f being Function of J, the carrier of L st ( for x being set holds ex_sup_of f .: x,L ) holds
rng (netmap ((FinSups f),L)) c= finsups (rng f)
proof
let L be non empty RelStr ; ::_thesis: for J being set
for f being Function of J, the carrier of L st ( for x being set holds ex_sup_of f .: x,L ) holds
rng (netmap ((FinSups f),L)) c= finsups (rng f)
let J be set ; ::_thesis: for f being Function of J, the carrier of L st ( for x being set holds ex_sup_of f .: x,L ) holds
rng (netmap ((FinSups f),L)) c= finsups (rng f)
let f be Function of J, the carrier of L; ::_thesis: ( ( for x being set holds ex_sup_of f .: x,L ) implies rng (netmap ((FinSups f),L)) c= finsups (rng f) )
assume A1: for x being set holds ex_sup_of f .: x,L ; ::_thesis: rng (netmap ((FinSups f),L)) c= finsups (rng f)
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in rng (netmap ((FinSups f),L)) or q in finsups (rng f) )
set h = netmap ((FinSups f),L);
assume q in rng (netmap ((FinSups f),L)) ; ::_thesis: q in finsups (rng f)
then consider x being set such that
A2: x in dom (netmap ((FinSups f),L)) and
A3: (netmap ((FinSups f),L)) . x = q by FUNCT_1:def_3;
A4: ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & FinSups f = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) by Def2;
then reconsider x = x as Element of Fin J by A2;
A5: ( f .: x is finite Subset of (rng f) & ex_sup_of f .: x,L ) by A1, RELAT_1:111;
(netmap ((FinSups f),L)) . x = sup (f .: x) by A4;
hence q in finsups (rng f) by A3, A5; ::_thesis: verum
end;
theorem Th25: :: WAYBEL_2:25
for L being non empty reflexive antisymmetric RelStr
for J being set
for f being Function of J, the carrier of L holds rng f c= rng (netmap ((FinSups f),L))
proof
let L be non empty reflexive antisymmetric RelStr ; ::_thesis: for J being set
for f being Function of J, the carrier of L holds rng f c= rng (netmap ((FinSups f),L))
let J be set ; ::_thesis: for f being Function of J, the carrier of L holds rng f c= rng (netmap ((FinSups f),L))
let f be Function of J, the carrier of L; ::_thesis: rng f c= rng (netmap ((FinSups f),L))
percases ( not J is empty or J is empty ) ;
supposeA1: not J is empty ; ::_thesis: rng f c= rng (netmap ((FinSups f),L))
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng f or a in rng (netmap ((FinSups f),L)) )
assume a in rng f ; ::_thesis: a in rng (netmap ((FinSups f),L))
then consider b being set such that
A2: b in dom f and
A3: a = f . b by FUNCT_1:def_3;
reconsider b = b as Element of J by A2;
f . b in rng f by A2, FUNCT_1:def_3;
then reconsider fb = f . b as Element of L ;
A4: Im (f,b) = {fb} by A2, FUNCT_1:59;
{b} c= J by A1, ZFMISC_1:31;
then reconsider x = {b} as Element of Fin J by FINSUB_1:def_5;
consider g being Function of (Fin J), the carrier of L such that
A5: for x being Element of Fin J holds
( g . x = sup (f .: x) & FinSups f = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) by Def2;
dom g = Fin J by FUNCT_2:def_1;
then A6: x in dom g ;
g . {b} = sup (f .: x) by A5
.= a by A3, A4, YELLOW_0:39 ;
hence a in rng (netmap ((FinSups f),L)) by A5, A6, FUNCT_1:def_3; ::_thesis: verum
end;
supposeA7: J is empty ; ::_thesis: rng f c= rng (netmap ((FinSups f),L))
rng f = {} by A7;
hence rng f c= rng (netmap ((FinSups f),L)) by XBOOLE_1:2; ::_thesis: verum
end;
end;
end;
theorem Th26: :: WAYBEL_2:26
for L being non empty reflexive antisymmetric RelStr
for J being set
for f being Function of J, the carrier of L st ex_sup_of rng f,L & ex_sup_of rng (netmap ((FinSups f),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) holds
Sup = sup (FinSups f)
proof
let L be non empty reflexive antisymmetric RelStr ; ::_thesis: for J being set
for f being Function of J, the carrier of L st ex_sup_of rng f,L & ex_sup_of rng (netmap ((FinSups f),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) holds
Sup = sup (FinSups f)
let J be set ; ::_thesis: for f being Function of J, the carrier of L st ex_sup_of rng f,L & ex_sup_of rng (netmap ((FinSups f),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) holds
Sup = sup (FinSups f)
let f be Function of J, the carrier of L; ::_thesis: ( ex_sup_of rng f,L & ex_sup_of rng (netmap ((FinSups f),L)),L & ( for x being Element of Fin J holds ex_sup_of f .: x,L ) implies Sup = sup (FinSups f) )
assume that
A1: ex_sup_of rng f,L and
A2: ex_sup_of rng (netmap ((FinSups f),L)),L and
A3: for x being Element of Fin J holds ex_sup_of f .: x,L ; ::_thesis: Sup = sup (FinSups f)
set h = netmap ((FinSups f),L);
A4: "\/" ((rng f),L) <= sup (rng (netmap ((FinSups f),L))) by A1, A2, Th25, YELLOW_0:34;
rng (netmap ((FinSups f),L)) is_<=_than "\/" ((rng f),L)
proof
let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in rng (netmap ((FinSups f),L)) or a <= "\/" ((rng f),L) )
assume a in rng (netmap ((FinSups f),L)) ; ::_thesis: a <= "\/" ((rng f),L)
then consider x being set such that
A5: x in dom (netmap ((FinSups f),L)) and
A6: a = (netmap ((FinSups f),L)) . x by FUNCT_1:def_3;
A7: ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & FinSups f = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) by Def2;
then reconsider x = x as Element of Fin J by A5;
ex_sup_of f .: x,L by A3;
then sup (f .: x) <= "\/" ((rng f),L) by A1, RELAT_1:111, YELLOW_0:34;
hence a <= "\/" ((rng f),L) by A6, A7; ::_thesis: verum
end;
then A8: sup (rng (netmap ((FinSups f),L))) <= "\/" ((rng f),L) by A2, YELLOW_0:def_9;
thus Sup = "\/" ((rng f),L) by YELLOW_2:def_5
.= sup (rng (netmap ((FinSups f),L))) by A4, A8, ORDERS_2:2
.= sup (FinSups f) by YELLOW_2:def_5 ; ::_thesis: verum
end;
theorem Th27: :: WAYBEL_2:27
for L being transitive antisymmetric with_infima RelStr
for N being prenet of L
for x being Element of L st N is eventually-directed holds
x "/\" N is eventually-directed
proof
let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for N being prenet of L
for x being Element of L st N is eventually-directed holds
x "/\" N is eventually-directed
let N be prenet of L; ::_thesis: for x being Element of L st N is eventually-directed holds
x "/\" N is eventually-directed
let x be Element of L; ::_thesis: ( N is eventually-directed implies x "/\" N is eventually-directed )
assume A1: N is eventually-directed ; ::_thesis: x "/\" N is eventually-directed
A2: RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def3;
for i being Element of (x "/\" N) ex j being Element of (x "/\" N) st
for k being Element of (x "/\" N) st j <= k holds
(x "/\" N) . i <= (x "/\" N) . k
proof
let i1 be Element of (x "/\" N); ::_thesis: ex j being Element of (x "/\" N) st
for k being Element of (x "/\" N) st j <= k holds
(x "/\" N) . i1 <= (x "/\" N) . k
reconsider i = i1 as Element of N by Th22;
consider j being Element of N such that
A3: for k being Element of N st j <= k holds
N . i <= N . k by A1, WAYBEL_0:11;
reconsider j1 = j as Element of (x "/\" N) by Th22;
take j1 ; ::_thesis: for k being Element of (x "/\" N) st j1 <= k holds
(x "/\" N) . i1 <= (x "/\" N) . k
let k1 be Element of (x "/\" N); ::_thesis: ( j1 <= k1 implies (x "/\" N) . i1 <= (x "/\" N) . k1 )
reconsider k = k1 as Element of N by Th22;
assume j1 <= k1 ; ::_thesis: (x "/\" N) . i1 <= (x "/\" N) . k1
then j <= k by A2, YELLOW_0:1;
then A4: N . i <= N . k by A3;
( ex yi being Element of L st
( yi = the mapping of N . i1 & the mapping of (x "/\" N) . i1 = x "/\" yi ) & ex yk being Element of L st
( yk = the mapping of N . k1 & the mapping of (x "/\" N) . k1 = x "/\" yk ) ) by Def3;
hence (x "/\" N) . i1 <= (x "/\" N) . k1 by A4, WAYBEL_1:1; ::_thesis: verum
end;
hence x "/\" N is eventually-directed by WAYBEL_0:11; ::_thesis: verum
end;
theorem Th28: :: WAYBEL_2:28
for L being up-complete Semilattice st ( for x being Element of L
for E being non empty directed Subset of L st x <= sup E holds
x <= sup ({x} "/\" E) ) holds
for D being non empty directed Subset of L
for x being Element of L holds x "/\" (sup D) = sup ({x} "/\" D)
proof
let L be up-complete Semilattice; ::_thesis: ( ( for x being Element of L
for E being non empty directed Subset of L st x <= sup E holds
x <= sup ({x} "/\" E) ) implies for D being non empty directed Subset of L
for x being Element of L holds x "/\" (sup D) = sup ({x} "/\" D) )
assume A1: for x being Element of L
for E being non empty directed Subset of L st x <= sup E holds
x <= sup ({x} "/\" E) ; ::_thesis: for D being non empty directed Subset of L
for x being Element of L holds x "/\" (sup D) = sup ({x} "/\" D)
let D be non empty directed Subset of L; ::_thesis: for x being Element of L holds x "/\" (sup D) = sup ({x} "/\" D)
let x be Element of L; ::_thesis: x "/\" (sup D) = sup ({x} "/\" D)
ex w being Element of L st
( x >= w & sup D >= w & ( for c being Element of L st x >= c & sup D >= c holds
w >= c ) ) by LATTICE3:def_11;
then x "/\" (sup D) <= sup D by LATTICE3:def_14;
then A2: x "/\" (sup D) <= sup ({(x "/\" (sup D))} "/\" D) by A1;
reconsider T = {(x "/\" (sup D))} as non empty directed Subset of L by WAYBEL_0:5;
ex_sup_of D,L by WAYBEL_0:75;
then A3: sup D is_>=_than D by YELLOW_0:30;
( ex_sup_of T "/\" D,L & {(x "/\" (sup D))} "/\" D is_<=_than x "/\" (sup D) ) by WAYBEL_0:75, YELLOW_4:52;
then sup ({(x "/\" (sup D))} "/\" D) <= x "/\" (sup D) by YELLOW_0:30;
hence x "/\" (sup D) = sup ({(x "/\" (sup D))} "/\" D) by A2, ORDERS_2:2
.= sup (({x} "/\" {(sup D)}) "/\" D) by YELLOW_4:46
.= sup ({x} "/\" ({(sup D)} "/\" D)) by YELLOW_4:41
.= sup ({x} "/\" D) by A3, YELLOW_4:51 ;
::_thesis: verum
end;
theorem :: WAYBEL_2:29
for L being with_suprema Poset st ( for X being directed Subset of L
for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X) ) holds
for X being Subset of L
for x being Element of L st ex_sup_of X,L holds
x "/\" (sup X) = sup ({x} "/\" (finsups X))
proof
let L be with_suprema Poset; ::_thesis: ( ( for X being directed Subset of L
for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X) ) implies for X being Subset of L
for x being Element of L st ex_sup_of X,L holds
x "/\" (sup X) = sup ({x} "/\" (finsups X)) )
assume A1: for X being directed Subset of L
for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X) ; ::_thesis: for X being Subset of L
for x being Element of L st ex_sup_of X,L holds
x "/\" (sup X) = sup ({x} "/\" (finsups X))
let X be Subset of L; ::_thesis: for x being Element of L st ex_sup_of X,L holds
x "/\" (sup X) = sup ({x} "/\" (finsups X))
let x be Element of L; ::_thesis: ( ex_sup_of X,L implies x "/\" (sup X) = sup ({x} "/\" (finsups X)) )
assume ex_sup_of X,L ; ::_thesis: x "/\" (sup X) = sup ({x} "/\" (finsups X))
hence x "/\" (sup X) = x "/\" (sup (finsups X)) by WAYBEL_0:55
.= sup ({x} "/\" (finsups X)) by A1 ;
::_thesis: verum
end;
theorem :: WAYBEL_2:30
for L being up-complete LATTICE st ( for X being Subset of L
for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" (finsups X)) ) holds
for X being non empty directed Subset of L
for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X)
proof
let L be up-complete LATTICE; ::_thesis: ( ( for X being Subset of L
for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" (finsups X)) ) implies for X being non empty directed Subset of L
for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X) )
assume A1: for X being Subset of L
for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" (finsups X)) ; ::_thesis: for X being non empty directed Subset of L
for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X)
let X be non empty directed Subset of L; ::_thesis: for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X)
let x be Element of L; ::_thesis: x "/\" (sup X) = sup ({x} "/\" X)
reconsider T = {x} as non empty directed Subset of L by WAYBEL_0:5;
A2: ex_sup_of T "/\" X,L by WAYBEL_0:75;
A3: {x} "/\" (finsups X) = { (x "/\" y) where y is Element of L : y in finsups X } by YELLOW_4:42;
A4: {x} "/\" (finsups X) is_<=_than sup ({x} "/\" X)
proof
let q be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not q in {x} "/\" (finsups X) or q <= sup ({x} "/\" X) )
A5: x <= x ;
assume q in {x} "/\" (finsups X) ; ::_thesis: q <= sup ({x} "/\" X)
then consider y being Element of L such that
A6: q = x "/\" y and
A7: y in finsups X by A3;
consider Y being finite Subset of X such that
A8: y = "\/" (Y,L) and
A9: ex_sup_of Y,L by A7;
consider z being Element of L such that
A10: z in X and
A11: z is_>=_than Y by WAYBEL_0:1;
"\/" (Y,L) <= z by A9, A11, YELLOW_0:30;
then A12: x "/\" y <= x "/\" z by A8, A5, YELLOW_3:2;
x in {x} by TARSKI:def_1;
then x "/\" z <= sup ({x} "/\" X) by A2, A10, YELLOW_4:1, YELLOW_4:37;
hence q <= sup ({x} "/\" X) by A6, A12, YELLOW_0:def_2; ::_thesis: verum
end;
ex_sup_of T "/\" (finsups X),L by WAYBEL_0:75;
then sup ({x} "/\" (finsups X)) <= sup ({x} "/\" X) by A4, YELLOW_0:30;
then A13: x "/\" (sup X) <= sup ({x} "/\" X) by A1;
ex_sup_of X,L by WAYBEL_0:75;
then sup ({x} "/\" X) <= x "/\" (sup X) by A2, YELLOW_4:53;
hence x "/\" (sup X) = sup ({x} "/\" X) by A13, ORDERS_2:2; ::_thesis: verum
end;
begin
definition
let L be non empty RelStr ;
func inf_op L -> Function of [:L,L:],L means :Def4: :: WAYBEL_2:def 4
for x, y being Element of L holds it . (x,y) = x "/\" y;
existence
ex b1 being Function of [:L,L:],L st
for x, y being Element of L holds b1 . (x,y) = x "/\" y
proof
deffunc H1( Element of L, Element of L) -> Element of the carrier of L = $1 "/\" $2;
A1: for x, y being Element of L holds H1(x,y) is Element of L ;
consider f being Function of [:L,L:],L such that
A2: for x, y being Element of L holds f . (x,y) = H1(x,y) from YELLOW_3:sch_6(A1);
take f ; ::_thesis: for x, y being Element of L holds f . (x,y) = x "/\" y
thus for x, y being Element of L holds f . (x,y) = x "/\" y by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of [:L,L:],L st ( for x, y being Element of L holds b1 . (x,y) = x "/\" y ) & ( for x, y being Element of L holds b2 . (x,y) = x "/\" y ) holds
b1 = b2
proof
let f, g be Function of [:L,L:],L; ::_thesis: ( ( for x, y being Element of L holds f . (x,y) = x "/\" y ) & ( for x, y being Element of L holds g . (x,y) = x "/\" y ) implies f = g )
assume that
A3: for x, y being Element of L holds f . (x,y) = x "/\" y and
A4: for x, y being Element of L holds g . (x,y) = x "/\" y ; ::_thesis: f = g
now__::_thesis:_for_x,_y_being_Element_of_L_holds_f_._(x,y)_=_g_._(x,y)
let x, y be Element of L; ::_thesis: f . (x,y) = g . (x,y)
thus f . (x,y) = x "/\" y by A3
.= g . (x,y) by A4 ; ::_thesis: verum
end;
hence f = g by YELLOW_3:13; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines inf_op WAYBEL_2:def_4_:_
for L being non empty RelStr
for b2 being Function of [:L,L:],L holds
( b2 = inf_op L iff for x, y being Element of L holds b2 . (x,y) = x "/\" y );
theorem Th31: :: WAYBEL_2:31
for L being non empty RelStr
for x being Element of [:L,L:] holds (inf_op L) . x = (x `1) "/\" (x `2)
proof
let L be non empty RelStr ; ::_thesis: for x being Element of [:L,L:] holds (inf_op L) . x = (x `1) "/\" (x `2)
let x be Element of [:L,L:]; ::_thesis: (inf_op L) . x = (x `1) "/\" (x `2)
the carrier of [:L,L:] = [: the carrier of L, the carrier of L:] by YELLOW_3:def_2;
then ex a, b being set st
( a in the carrier of L & b in the carrier of L & x = [a,b] ) by ZFMISC_1:def_2;
hence (inf_op L) . x = (inf_op L) . ((x `1),(x `2)) by MCART_1:8
.= (x `1) "/\" (x `2) by Def4 ;
::_thesis: verum
end;
registration
let L be transitive antisymmetric with_infima RelStr ;
cluster inf_op L -> monotone ;
coherence
inf_op L is monotone
proof
let x, y be Element of [:L,L:]; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of L holds
( not b1 = (inf_op L) . x or not b2 = (inf_op L) . y or b1 <= b2 ) )
set f = inf_op L;
assume x <= y ; ::_thesis: for b1, b2 being Element of the carrier of L holds
( not b1 = (inf_op L) . x or not b2 = (inf_op L) . y or b1 <= b2 )
then A1: ( x `1 <= y `1 & x `2 <= y `2 ) by YELLOW_3:12;
A2: ( (inf_op L) . x = (x `1) "/\" (x `2) & (inf_op L) . y = (y `1) "/\" (y `2) ) by Th31;
let a, b be Element of L; ::_thesis: ( not a = (inf_op L) . x or not b = (inf_op L) . y or a <= b )
assume ( a = (inf_op L) . x & b = (inf_op L) . y ) ; ::_thesis: a <= b
hence a <= b by A1, A2, YELLOW_3:2; ::_thesis: verum
end;
end;
theorem Th32: :: WAYBEL_2:32
for S being non empty RelStr
for D1, D2 being Subset of S holds (inf_op S) .: [:D1,D2:] = D1 "/\" D2
proof
let S be non empty RelStr ; ::_thesis: for D1, D2 being Subset of S holds (inf_op S) .: [:D1,D2:] = D1 "/\" D2
let D1, D2 be Subset of S; ::_thesis: (inf_op S) .: [:D1,D2:] = D1 "/\" D2
set f = inf_op S;
reconsider X = [:D1,D2:] as set ;
thus (inf_op S) .: [:D1,D2:] c= D1 "/\" D2 :: according to XBOOLE_0:def_10 ::_thesis: D1 "/\" D2 c= (inf_op S) .: [:D1,D2:]
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (inf_op S) .: [:D1,D2:] or q in D1 "/\" D2 )
assume A1: q in (inf_op S) .: [:D1,D2:] ; ::_thesis: q in D1 "/\" D2
then reconsider q1 = q as Element of S ;
consider c being Element of [:S,S:] such that
A2: c in [:D1,D2:] and
A3: q1 = (inf_op S) . c by A1, FUNCT_2:65;
consider x, y being set such that
A4: ( x in D1 & y in D2 ) and
A5: c = [x,y] by A2, ZFMISC_1:def_2;
reconsider x = x, y = y as Element of S by A4;
q = (inf_op S) . (x,y) by A3, A5
.= x "/\" y by Def4 ;
then q in { (a "/\" b) where a, b is Element of S : ( a in D1 & b in D2 ) } by A4;
hence q in D1 "/\" D2 by YELLOW_4:def_4; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D1 "/\" D2 or q in (inf_op S) .: [:D1,D2:] )
assume q in D1 "/\" D2 ; ::_thesis: q in (inf_op S) .: [:D1,D2:]
then q in { (x "/\" y) where x, y is Element of S : ( x in D1 & y in D2 ) } by YELLOW_4:def_4;
then consider x, y being Element of S such that
A6: ( q = x "/\" y & x in D1 & y in D2 ) ;
( q = (inf_op S) . (x,y) & [x,y] in X ) by A6, Def4, ZFMISC_1:87;
hence q in (inf_op S) .: [:D1,D2:] by FUNCT_2:35; ::_thesis: verum
end;
theorem Th33: :: WAYBEL_2:33
for L being up-complete Semilattice
for D being non empty directed Subset of [:L,L:] holds sup ((inf_op L) .: D) = sup ((proj1 D) "/\" (proj2 D))
proof
let L be up-complete Semilattice; ::_thesis: for D being non empty directed Subset of [:L,L:] holds sup ((inf_op L) .: D) = sup ((proj1 D) "/\" (proj2 D))
let D be non empty directed Subset of [:L,L:]; ::_thesis: sup ((inf_op L) .: D) = sup ((proj1 D) "/\" (proj2 D))
reconsider C = the carrier of L as non empty set ;
reconsider D9 = D as non empty Subset of [:C,C:] by YELLOW_3:def_2;
reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22;
set f = inf_op L;
A1: ex_sup_of D1 "/\" D2,L by WAYBEL_0:75;
A2: (inf_op L) .: [:D1,D2:] = D1 "/\" D2 by Th32;
A3: ( (inf_op L) .: [:D1,D2:] c= (inf_op L) .: (downarrow D) & (inf_op L) .: (downarrow D) c= downarrow ((inf_op L) .: D) ) by Th13, RELAT_1:123, YELLOW_3:48;
A4: (inf_op L) .: D is directed by YELLOW_2:15;
then A5: ex_sup_of (inf_op L) .: D,L by WAYBEL_0:75;
ex_sup_of downarrow ((inf_op L) .: D),L by A4, WAYBEL_0:75;
then sup (D1 "/\" D2) <= sup (downarrow ((inf_op L) .: D)) by A1, A3, A2, XBOOLE_1:1, YELLOW_0:34;
then A6: sup (D1 "/\" D2) <= sup ((inf_op L) .: D) by A5, WAYBEL_0:33;
(inf_op L) .: D9 c= (inf_op L) .: [:D1,D2:] by RELAT_1:123, YELLOW_3:1;
then (inf_op L) .: D9 c= D1 "/\" D2 by Th32;
then sup ((inf_op L) .: D) <= sup (D1 "/\" D2) by A5, A1, YELLOW_0:34;
hence sup ((inf_op L) .: D) = sup ((proj1 D) "/\" (proj2 D)) by A6, ORDERS_2:2; ::_thesis: verum
end;
definition
let L be non empty RelStr ;
func sup_op L -> Function of [:L,L:],L means :Def5: :: WAYBEL_2:def 5
for x, y being Element of L holds it . (x,y) = x "\/" y;
existence
ex b1 being Function of [:L,L:],L st
for x, y being Element of L holds b1 . (x,y) = x "\/" y
proof
deffunc H1( Element of L, Element of L) -> Element of the carrier of L = $1 "\/" $2;
A1: for x, y being Element of L holds H1(x,y) is Element of L ;
consider f being Function of [:L,L:],L such that
A2: for x, y being Element of L holds f . (x,y) = H1(x,y) from YELLOW_3:sch_6(A1);
take f ; ::_thesis: for x, y being Element of L holds f . (x,y) = x "\/" y
thus for x, y being Element of L holds f . (x,y) = x "\/" y by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of [:L,L:],L st ( for x, y being Element of L holds b1 . (x,y) = x "\/" y ) & ( for x, y being Element of L holds b2 . (x,y) = x "\/" y ) holds
b1 = b2
proof
let f, g be Function of [:L,L:],L; ::_thesis: ( ( for x, y being Element of L holds f . (x,y) = x "\/" y ) & ( for x, y being Element of L holds g . (x,y) = x "\/" y ) implies f = g )
assume that
A3: for x, y being Element of L holds f . (x,y) = x "\/" y and
A4: for x, y being Element of L holds g . (x,y) = x "\/" y ; ::_thesis: f = g
now__::_thesis:_for_x,_y_being_Element_of_L_holds_f_._(x,y)_=_g_._(x,y)
let x, y be Element of L; ::_thesis: f . (x,y) = g . (x,y)
thus f . (x,y) = x "\/" y by A3
.= g . (x,y) by A4 ; ::_thesis: verum
end;
hence f = g by YELLOW_3:13; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines sup_op WAYBEL_2:def_5_:_
for L being non empty RelStr
for b2 being Function of [:L,L:],L holds
( b2 = sup_op L iff for x, y being Element of L holds b2 . (x,y) = x "\/" y );
theorem Th34: :: WAYBEL_2:34
for L being non empty RelStr
for x being Element of [:L,L:] holds (sup_op L) . x = (x `1) "\/" (x `2)
proof
let L be non empty RelStr ; ::_thesis: for x being Element of [:L,L:] holds (sup_op L) . x = (x `1) "\/" (x `2)
let x be Element of [:L,L:]; ::_thesis: (sup_op L) . x = (x `1) "\/" (x `2)
the carrier of [:L,L:] = [: the carrier of L, the carrier of L:] by YELLOW_3:def_2;
then ex a, b being set st
( a in the carrier of L & b in the carrier of L & x = [a,b] ) by ZFMISC_1:def_2;
hence (sup_op L) . x = (sup_op L) . ((x `1),(x `2)) by MCART_1:8
.= (x `1) "\/" (x `2) by Def5 ;
::_thesis: verum
end;
registration
let L be transitive antisymmetric with_suprema RelStr ;
cluster sup_op L -> monotone ;
coherence
sup_op L is monotone
proof
let x, y be Element of [:L,L:]; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of L holds
( not b1 = (sup_op L) . x or not b2 = (sup_op L) . y or b1 <= b2 ) )
set f = sup_op L;
assume x <= y ; ::_thesis: for b1, b2 being Element of the carrier of L holds
( not b1 = (sup_op L) . x or not b2 = (sup_op L) . y or b1 <= b2 )
then A1: ( x `1 <= y `1 & x `2 <= y `2 ) by YELLOW_3:12;
A2: ( (sup_op L) . x = (x `1) "\/" (x `2) & (sup_op L) . y = (y `1) "\/" (y `2) ) by Th34;
let a, b be Element of L; ::_thesis: ( not a = (sup_op L) . x or not b = (sup_op L) . y or a <= b )
assume ( a = (sup_op L) . x & b = (sup_op L) . y ) ; ::_thesis: a <= b
hence a <= b by A1, A2, YELLOW_3:3; ::_thesis: verum
end;
end;
theorem Th35: :: WAYBEL_2:35
for S being non empty RelStr
for D1, D2 being Subset of S holds (sup_op S) .: [:D1,D2:] = D1 "\/" D2
proof
let S be non empty RelStr ; ::_thesis: for D1, D2 being Subset of S holds (sup_op S) .: [:D1,D2:] = D1 "\/" D2
let D1, D2 be Subset of S; ::_thesis: (sup_op S) .: [:D1,D2:] = D1 "\/" D2
set f = sup_op S;
reconsider X = [:D1,D2:] as set ;
thus (sup_op S) .: [:D1,D2:] c= D1 "\/" D2 :: according to XBOOLE_0:def_10 ::_thesis: D1 "\/" D2 c= (sup_op S) .: [:D1,D2:]
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (sup_op S) .: [:D1,D2:] or q in D1 "\/" D2 )
assume A1: q in (sup_op S) .: [:D1,D2:] ; ::_thesis: q in D1 "\/" D2
then reconsider q1 = q as Element of S ;
consider c being Element of [:S,S:] such that
A2: c in [:D1,D2:] and
A3: q1 = (sup_op S) . c by A1, FUNCT_2:65;
consider x, y being set such that
A4: ( x in D1 & y in D2 ) and
A5: c = [x,y] by A2, ZFMISC_1:def_2;
reconsider x = x, y = y as Element of S by A4;
q = (sup_op S) . (x,y) by A3, A5
.= x "\/" y by Def5 ;
then q in { (a "\/" b) where a, b is Element of S : ( a in D1 & b in D2 ) } by A4;
hence q in D1 "\/" D2 by YELLOW_4:def_3; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D1 "\/" D2 or q in (sup_op S) .: [:D1,D2:] )
assume q in D1 "\/" D2 ; ::_thesis: q in (sup_op S) .: [:D1,D2:]
then q in { (x "\/" y) where x, y is Element of S : ( x in D1 & y in D2 ) } by YELLOW_4:def_3;
then consider x, y being Element of S such that
A6: ( q = x "\/" y & x in D1 & y in D2 ) ;
( q = (sup_op S) . (x,y) & [x,y] in X ) by A6, Def5, ZFMISC_1:87;
hence q in (sup_op S) .: [:D1,D2:] by FUNCT_2:35; ::_thesis: verum
end;
theorem :: WAYBEL_2:36
for L being non empty complete Poset
for D being non empty filtered Subset of [:L,L:] holds inf ((sup_op L) .: D) = inf ((proj1 D) "\/" (proj2 D))
proof
let L be non empty complete Poset; ::_thesis: for D being non empty filtered Subset of [:L,L:] holds inf ((sup_op L) .: D) = inf ((proj1 D) "\/" (proj2 D))
let D be non empty filtered Subset of [:L,L:]; ::_thesis: inf ((sup_op L) .: D) = inf ((proj1 D) "\/" (proj2 D))
reconsider C = the carrier of L as non empty set ;
reconsider D9 = D as non empty Subset of [:C,C:] by YELLOW_3:def_2;
set D1 = proj1 D;
set D2 = proj2 D;
set f = sup_op L;
A1: ex_inf_of (proj1 D) "\/" (proj2 D),L by YELLOW_0:17;
A2: ( ex_inf_of uparrow ((sup_op L) .: D),L & (sup_op L) .: [:(proj1 D),(proj2 D):] c= (sup_op L) .: (uparrow D) ) by RELAT_1:123, YELLOW_0:17, YELLOW_3:49;
( (sup_op L) .: (uparrow D) c= uparrow ((sup_op L) .: D) & (sup_op L) .: [:(proj1 D),(proj2 D):] = (proj1 D) "\/" (proj2 D) ) by Th14, Th35;
then inf ((proj1 D) "\/" (proj2 D)) >= inf (uparrow ((sup_op L) .: D)) by A1, A2, XBOOLE_1:1, YELLOW_0:35;
then A3: inf ((proj1 D) "\/" (proj2 D)) >= inf ((sup_op L) .: D) by WAYBEL_0:38, YELLOW_0:17;
(sup_op L) .: D9 c= (sup_op L) .: [:(proj1 D),(proj2 D):] by RELAT_1:123, YELLOW_3:1;
then ( ex_inf_of (sup_op L) .: D9,L & (sup_op L) .: D9 c= (proj1 D) "\/" (proj2 D) ) by Th35, YELLOW_0:17;
then inf ((sup_op L) .: D) >= inf ((proj1 D) "\/" (proj2 D)) by A1, YELLOW_0:35;
hence inf ((sup_op L) .: D) = inf ((proj1 D) "\/" (proj2 D)) by A3, ORDERS_2:2; ::_thesis: verum
end;
begin
definition
let R be non empty reflexive RelStr ;
attrR is satisfying_MC means :Def6: :: WAYBEL_2:def 6
for x being Element of R
for D being non empty directed Subset of R holds x "/\" (sup D) = sup ({x} "/\" D);
end;
:: deftheorem Def6 defines satisfying_MC WAYBEL_2:def_6_:_
for R being non empty reflexive RelStr holds
( R is satisfying_MC iff for x being Element of R
for D being non empty directed Subset of R holds x "/\" (sup D) = sup ({x} "/\" D) );
definition
let R be non empty reflexive RelStr ;
attrR is meet-continuous means :Def7: :: WAYBEL_2:def 7
( R is up-complete & R is satisfying_MC );
end;
:: deftheorem Def7 defines meet-continuous WAYBEL_2:def_7_:_
for R being non empty reflexive RelStr holds
( R is meet-continuous iff ( R is up-complete & R is satisfying_MC ) );
registration
cluster1 -element reflexive -> 1 -element reflexive satisfying_MC for RelStr ;
coherence
for b1 being 1 -element reflexive RelStr holds b1 is satisfying_MC
proof
let I be 1 -element reflexive RelStr ; ::_thesis: I is satisfying_MC
let x be Element of I; :: according to WAYBEL_2:def_6 ::_thesis: for D being non empty directed Subset of I holds x "/\" (sup D) = sup ({x} "/\" D)
let D be non empty directed Subset of I; ::_thesis: x "/\" (sup D) = sup ({x} "/\" D)
thus x "/\" (sup D) = sup ({x} "/\" D) by STRUCT_0:def_10; ::_thesis: verum
end;
end;
registration
cluster non empty reflexive meet-continuous -> non empty reflexive up-complete satisfying_MC for RelStr ;
coherence
for b1 being non empty reflexive RelStr st b1 is meet-continuous holds
( b1 is up-complete & b1 is satisfying_MC ) by Def7;
cluster non empty reflexive up-complete satisfying_MC -> non empty reflexive meet-continuous for RelStr ;
coherence
for b1 being non empty reflexive RelStr st b1 is up-complete & b1 is satisfying_MC holds
b1 is meet-continuous by Def7;
end;
theorem Th37: :: WAYBEL_2:37
for S being non empty reflexive RelStr st ( for X being Subset of S
for x being Element of S holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ) holds
S is satisfying_MC
proof
let S be non empty reflexive RelStr ; ::_thesis: ( ( for X being Subset of S
for x being Element of S holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ) implies S is satisfying_MC )
assume A1: for X being Subset of S
for x being Element of S holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ; ::_thesis: S is satisfying_MC
let y be Element of S; :: according to WAYBEL_2:def_6 ::_thesis: for D being non empty directed Subset of S holds y "/\" (sup D) = sup ({y} "/\" D)
let D be non empty directed Subset of S; ::_thesis: y "/\" (sup D) = sup ({y} "/\" D)
thus sup ({y} "/\" D) = "\/" ( { (y "/\" z) where z is Element of S : z in D } ,S) by YELLOW_4:42
.= y "/\" (sup D) by A1 ; ::_thesis: verum
end;
theorem Th38: :: WAYBEL_2:38
for L being up-complete Semilattice st SupMap L is meet-preserving holds
for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2)
proof
let L be up-complete Semilattice; ::_thesis: ( SupMap L is meet-preserving implies for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) )
assume A1: SupMap L is meet-preserving ; ::_thesis: for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2)
set f = SupMap L;
let I1, I2 be Ideal of L; ::_thesis: (sup I1) "/\" (sup I2) = sup (I1 "/\" I2)
reconsider x = I1, y = I2 as Element of (InclPoset (Ids L)) by YELLOW_2:41;
A2: SupMap L preserves_inf_of {x,y} by A1, WAYBEL_0:def_34;
reconsider fx = (SupMap L) . x as Element of L ;
thus (sup I1) "/\" (sup I2) = fx "/\" (sup I2) by YELLOW_2:def_3
.= ((SupMap L) . x) "/\" ((SupMap L) . y) by YELLOW_2:def_3
.= (SupMap L) . (x "/\" y) by A2, YELLOW_3:8
.= (SupMap L) . (I1 "/\" I2) by YELLOW_4:58
.= sup (I1 "/\" I2) by YELLOW_2:def_3 ; ::_thesis: verum
end;
registration
let L be up-complete sup-Semilattice;
cluster SupMap L -> join-preserving ;
coherence
SupMap L is join-preserving
proof
let x, y be Element of (InclPoset (Ids L)); :: according to WAYBEL_0:def_35 ::_thesis: SupMap L preserves_sup_of {x,y}
set f = SupMap L;
assume ex_sup_of {x,y}, InclPoset (Ids L) ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (SupMap L) .: {x,y},L & "\/" (((SupMap L) .: {x,y}),L) = (SupMap L) . ("\/" ({x,y},(InclPoset (Ids L)))) )
reconsider x1 = x, y1 = y as Ideal of L by YELLOW_2:41;
A1: ex_sup_of x1 "\/" y1,L by WAYBEL_0:75;
A2: dom (SupMap L) = the carrier of (InclPoset (Ids L)) by FUNCT_2:def_1;
then (SupMap L) .: {x,y} = {((SupMap L) . x),((SupMap L) . y)} by FUNCT_1:60;
hence ex_sup_of (SupMap L) .: {x,y},L by YELLOW_0:20; ::_thesis: "\/" (((SupMap L) .: {x,y}),L) = (SupMap L) . ("\/" ({x,y},(InclPoset (Ids L))))
thus sup ((SupMap L) .: {x,y}) = sup {((SupMap L) . x),((SupMap L) . y)} by A2, FUNCT_1:60
.= ((SupMap L) . x) "\/" ((SupMap L) . y) by YELLOW_0:41
.= ((SupMap L) . x) "\/" (sup y1) by YELLOW_2:def_3
.= (sup x1) "\/" (sup y1) by YELLOW_2:def_3
.= sup (x1 "\/" y1) by Th4
.= sup (downarrow (x1 "\/" y1)) by A1, WAYBEL_0:33
.= (SupMap L) . (downarrow (x1 "\/" y1)) by YELLOW_2:def_3
.= (SupMap L) . (x "\/" y) by YELLOW_4:30
.= (SupMap L) . (sup {x,y}) by YELLOW_0:41 ; ::_thesis: verum
end;
end;
theorem Th39: :: WAYBEL_2:39
for L being up-complete Semilattice st ( for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ) holds
SupMap L is meet-preserving
proof
let L be up-complete Semilattice; ::_thesis: ( ( for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ) implies SupMap L is meet-preserving )
assume A1: for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ; ::_thesis: SupMap L is meet-preserving
let x, y be Element of (InclPoset (Ids L)); :: according to WAYBEL_0:def_34 ::_thesis: SupMap L preserves_inf_of {x,y}
set f = SupMap L;
assume ex_inf_of {x,y}, InclPoset (Ids L) ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (SupMap L) .: {x,y},L & "/\" (((SupMap L) .: {x,y}),L) = (SupMap L) . ("/\" ({x,y},(InclPoset (Ids L)))) )
reconsider x1 = x, y1 = y as Ideal of L by YELLOW_2:41;
A2: dom (SupMap L) = the carrier of (InclPoset (Ids L)) by FUNCT_2:def_1;
then (SupMap L) .: {x,y} = {((SupMap L) . x),((SupMap L) . y)} by FUNCT_1:60;
hence ex_inf_of (SupMap L) .: {x,y},L by YELLOW_0:21; ::_thesis: "/\" (((SupMap L) .: {x,y}),L) = (SupMap L) . ("/\" ({x,y},(InclPoset (Ids L))))
thus inf ((SupMap L) .: {x,y}) = inf {((SupMap L) . x),((SupMap L) . y)} by A2, FUNCT_1:60
.= ((SupMap L) . x) "/\" ((SupMap L) . y) by YELLOW_0:40
.= ((SupMap L) . x) "/\" (sup y1) by YELLOW_2:def_3
.= (sup x1) "/\" (sup y1) by YELLOW_2:def_3
.= sup (x1 "/\" y1) by A1
.= (SupMap L) . (x1 "/\" y1) by YELLOW_2:def_3
.= (SupMap L) . (x "/\" y) by YELLOW_4:58
.= (SupMap L) . (inf {x,y}) by YELLOW_0:40 ; ::_thesis: verum
end;
theorem Th40: :: WAYBEL_2:40
for L being up-complete Semilattice st ( for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ) holds
for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
proof
let L be up-complete Semilattice; ::_thesis: ( ( for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ) implies for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) )
assume A1: for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ; ::_thesis: for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
let D1, D2 be non empty directed Subset of L; ::_thesis: (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
A2: ex_sup_of D2,L by WAYBEL_0:75;
A3: ex_sup_of (downarrow D1) "/\" (downarrow D2),L by WAYBEL_0:75;
A4: ex_sup_of D1 "/\" D2,L by WAYBEL_0:75;
ex_sup_of D1,L by WAYBEL_0:75;
hence (sup D1) "/\" (sup D2) = (sup (downarrow D1)) "/\" (sup D2) by WAYBEL_0:33
.= (sup (downarrow D1)) "/\" (sup (downarrow D2)) by A2, WAYBEL_0:33
.= sup ((downarrow D1) "/\" (downarrow D2)) by A1
.= sup (downarrow ((downarrow D1) "/\" (downarrow D2))) by A3, WAYBEL_0:33
.= sup (downarrow (D1 "/\" D2)) by YELLOW_4:62
.= sup (D1 "/\" D2) by A4, WAYBEL_0:33 ;
::_thesis: verum
end;
theorem Th41: :: WAYBEL_2:41
for L being non empty reflexive RelStr st L is satisfying_MC holds
for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))
proof
let L be non empty reflexive RelStr ; ::_thesis: ( L is satisfying_MC implies for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) )
assume A1: L is satisfying_MC ; ::_thesis: for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))
let x be Element of L; ::_thesis: for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))
let N be prenet of L; ::_thesis: ( N is eventually-directed implies x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) )
assume N is eventually-directed ; ::_thesis: x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))
then A2: rng (netmap (N,L)) is directed by Th18;
thus x "/\" (sup N) = x "/\" (sup (rng (netmap (N,L)))) by YELLOW_2:def_5
.= sup ({x} "/\" (rng (netmap (N,L)))) by A1, A2, Def6 ; ::_thesis: verum
end;
theorem Th42: :: WAYBEL_2:42
for L being non empty reflexive RelStr st ( for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) holds
L is satisfying_MC
proof
let L be non empty reflexive RelStr ; ::_thesis: ( ( for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) implies L is satisfying_MC )
assume A1: for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ; ::_thesis: L is satisfying_MC
let x be Element of L; :: according to WAYBEL_2:def_6 ::_thesis: for D being non empty directed Subset of L holds x "/\" (sup D) = sup ({x} "/\" D)
let D be non empty directed Subset of L; ::_thesis: x "/\" (sup D) = sup ({x} "/\" D)
reconsider n = id D as Function of D, the carrier of L by FUNCT_2:7;
reconsider N = NetStr(# D,( the InternalRel of L |_2 D),n #) as prenet of L by Th19;
A2: Sup = sup N ;
D c= D ;
then A3: D = n .: D by FUNCT_1:92
.= rng (netmap (N,L)) by RELSET_1:22 ;
hence x "/\" (sup D) = x "/\" (Sup ) by YELLOW_2:def_5
.= sup ({x} "/\" D) by A1, A3, A2, Th20 ;
::_thesis: verum
end;
theorem Th43: :: WAYBEL_2:43
for L being non empty reflexive antisymmetric up-complete RelStr st inf_op L is directed-sups-preserving holds
for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
proof
let L be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: ( inf_op L is directed-sups-preserving implies for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) )
assume A1: inf_op L is directed-sups-preserving ; ::_thesis: for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
let D1, D2 be non empty directed Subset of L; ::_thesis: (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
set X = [:D1,D2:];
set f = inf_op L;
A2: inf_op L preserves_sup_of [:D1,D2:] by A1, WAYBEL_0:def_37;
A3: ex_sup_of [:D1,D2:],[:L,L:] by WAYBEL_0:75;
A4: ( ex_sup_of D1,L & ex_sup_of D2,L ) by WAYBEL_0:75;
thus (sup D1) "/\" (sup D2) = (inf_op L) . ((sup D1),(sup D2)) by Def4
.= (inf_op L) . (sup [:D1,D2:]) by A4, YELLOW_3:43
.= sup ((inf_op L) .: [:D1,D2:]) by A2, A3, WAYBEL_0:def_31
.= sup (D1 "/\" D2) by Th32 ; ::_thesis: verum
end;
theorem Th44: :: WAYBEL_2:44
for L being non empty reflexive antisymmetric RelStr st ( for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) ) holds
L is satisfying_MC
proof
let L be non empty reflexive antisymmetric RelStr ; ::_thesis: ( ( for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) ) implies L is satisfying_MC )
assume A1: for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) ; ::_thesis: L is satisfying_MC
let x be Element of L; :: according to WAYBEL_2:def_6 ::_thesis: for D being non empty directed Subset of L holds x "/\" (sup D) = sup ({x} "/\" D)
let D be non empty directed Subset of L; ::_thesis: x "/\" (sup D) = sup ({x} "/\" D)
A2: {x} is directed by WAYBEL_0:5;
thus x "/\" (sup D) = (sup {x}) "/\" (sup D) by YELLOW_0:39
.= sup ({x} "/\" D) by A1, A2 ; ::_thesis: verum
end;
theorem Th45: :: WAYBEL_2:45
for L being non empty reflexive antisymmetric with_infima satisfying_MC RelStr
for x being Element of L
for D being non empty directed Subset of L st x <= sup D holds
x = sup ({x} "/\" D)
proof
let L be non empty reflexive antisymmetric with_infima satisfying_MC RelStr ; ::_thesis: for x being Element of L
for D being non empty directed Subset of L st x <= sup D holds
x = sup ({x} "/\" D)
let x be Element of L; ::_thesis: for D being non empty directed Subset of L st x <= sup D holds
x = sup ({x} "/\" D)
let D be non empty directed Subset of L; ::_thesis: ( x <= sup D implies x = sup ({x} "/\" D) )
assume x <= sup D ; ::_thesis: x = sup ({x} "/\" D)
hence x = x "/\" (sup D) by YELLOW_0:25
.= sup ({x} "/\" D) by Def6 ;
::_thesis: verum
end;
theorem Th46: :: WAYBEL_2:46
for L being up-complete Semilattice st ( for x being Element of L
for E being non empty directed Subset of L st x <= sup E holds
x <= sup ({x} "/\" E) ) holds
inf_op L is directed-sups-preserving
proof
let L be up-complete Semilattice; ::_thesis: ( ( for x being Element of L
for E being non empty directed Subset of L st x <= sup E holds
x <= sup ({x} "/\" E) ) implies inf_op L is directed-sups-preserving )
assume A1: for x being Element of L
for E being non empty directed Subset of L st x <= sup E holds
x <= sup ({x} "/\" E) ; ::_thesis: inf_op L is directed-sups-preserving
let D be Subset of [:L,L:]; :: according to WAYBEL_0:def_37 ::_thesis: ( D is empty or not D is directed or inf_op L preserves_sup_of D )
assume ( not D is empty & D is directed ) ; ::_thesis: inf_op L preserves_sup_of D
then reconsider DD = D as non empty directed Subset of [:L,L:] ;
thus inf_op L preserves_sup_of D ::_thesis: verum
proof
reconsider D1 = proj1 DD, D2 = proj2 DD as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22;
reconsider C = the carrier of L as non empty set ;
set f = inf_op L;
assume ex_sup_of D,[:L,L:] ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (inf_op L) .: D,L & "\/" (((inf_op L) .: D),L) = (inf_op L) . ("\/" (D,[:L,L:])) )
set d2 = sup D2;
defpred S1[ set ] means ex x being Element of L st
( $1 = {x} "/\" D2 & x in D1 );
(inf_op L) .: DD is directed by YELLOW_2:15;
hence ex_sup_of (inf_op L) .: D,L by WAYBEL_0:75; ::_thesis: "\/" (((inf_op L) .: D),L) = (inf_op L) . ("\/" (D,[:L,L:]))
{ (x "/\" y) where x, y is Element of L : ( x in D1 & y in {(sup D2)} ) } c= C
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (x "/\" y) where x, y is Element of L : ( x in D1 & y in {(sup D2)} ) } or q in C )
assume q in { (x "/\" y) where x, y is Element of L : ( x in D1 & y in {(sup D2)} ) } ; ::_thesis: q in C
then ex x, y being Element of L st
( q = x "/\" y & x in D1 & y in {(sup D2)} ) ;
hence q in C ; ::_thesis: verum
end;
then reconsider F = { (x "/\" y) where x, y is Element of L : ( x in D1 & y in {(sup D2)} ) } as Subset of L ;
A2: "\/" ( { (sup X) where X is non empty directed Subset of L : S1[X] } ,L) = "\/" ((union { X where X is non empty directed Subset of L : S1[X] } ),L) by Th10;
A3: F = { (sup ({z} "/\" D2)) where z is Element of L : z in D1 }
proof
thus F c= { (sup ({z} "/\" D2)) where z is Element of L : z in D1 } :: according to XBOOLE_0:def_10 ::_thesis: { (sup ({z} "/\" D2)) where z is Element of L : z in D1 } c= F
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F or q in { (sup ({z} "/\" D2)) where z is Element of L : z in D1 } )
assume q in F ; ::_thesis: q in { (sup ({z} "/\" D2)) where z is Element of L : z in D1 }
then consider x, y being Element of L such that
A4: q = x "/\" y and
A5: x in D1 and
A6: y in {(sup D2)} ;
q = x "/\" (sup D2) by A4, A6, TARSKI:def_1
.= sup ({x} "/\" D2) by A1, Th28 ;
hence q in { (sup ({z} "/\" D2)) where z is Element of L : z in D1 } by A5; ::_thesis: verum
end;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (sup ({z} "/\" D2)) where z is Element of L : z in D1 } or q in F )
A7: sup D2 in {(sup D2)} by TARSKI:def_1;
assume q in { (sup ({z} "/\" D2)) where z is Element of L : z in D1 } ; ::_thesis: q in F
then consider z being Element of L such that
A8: q = sup ({z} "/\" D2) and
A9: z in D1 ;
q = z "/\" (sup D2) by A1, A8, Th28;
hence q in F by A9, A7; ::_thesis: verum
end;
thus sup ((inf_op L) .: D) = sup (D1 "/\" D2) by Th33
.= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,L) by A2, Th6
.= "\/" ( { (sup ({x} "/\" D2)) where x is Element of L : x in D1 } ,L) by Th5
.= sup ({(sup D2)} "/\" D1) by A3, YELLOW_4:def_4
.= (sup D1) "/\" (sup D2) by A1, Th28
.= (inf_op L) . ((sup D1),(sup D2)) by Def4
.= (inf_op L) . (sup D) by Th12 ; ::_thesis: verum
end;
end;
theorem Th47: :: WAYBEL_2:47
for L being non empty reflexive antisymmetric complete RelStr st ( for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) holds
for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f))
proof
let L be non empty reflexive antisymmetric complete RelStr ; ::_thesis: ( ( for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) implies for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) )
assume A1: for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ; ::_thesis: for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f))
let x be Element of L; ::_thesis: for J being set
for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f))
let J be set ; ::_thesis: for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f))
let f be Function of J, the carrier of L; ::_thesis: x "/\" (Sup ) = sup (x "/\" (FinSups f))
set F = FinSups f;
A2: for x being Element of Fin J holds ex_sup_of f .: x,L by YELLOW_0:17;
( ex_sup_of rng f,L & ex_sup_of rng (netmap ((FinSups f),L)),L ) by YELLOW_0:17;
hence x "/\" (Sup ) = x "/\" (sup (FinSups f)) by A2, Th26
.= sup ({x} "/\" (rng (netmap ((FinSups f),L)))) by A1
.= "\/" ((rng the mapping of (x "/\" (FinSups f))),L) by Th23
.= sup (x "/\" (FinSups f)) by YELLOW_2:def_5 ;
::_thesis: verum
end;
theorem Th48: :: WAYBEL_2:48
for L being complete Semilattice st ( for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ) holds
for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))
proof
let L be complete Semilattice; ::_thesis: ( ( for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ) implies for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) )
assume A1: for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ; ::_thesis: for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))
let x be Element of L; ::_thesis: for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))
let N be prenet of L; ::_thesis: ( N is eventually-directed implies x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) )
assume A2: N is eventually-directed ; ::_thesis: x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))
reconsider R = rng (netmap (N,L)) as non empty directed Subset of L by A2, Th18;
reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;
set f = the mapping of N;
set h = the mapping of (FinSups the mapping of N);
A3: ex_sup_of xx "/\" R,L by WAYBEL_0:75;
A4: rng the mapping of (x "/\" (FinSups the mapping of N)) is_<=_than sup ({x} "/\" (rng (netmap (N,L))))
proof
let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in rng the mapping of (x "/\" (FinSups the mapping of N)) or a <= sup ({x} "/\" (rng (netmap (N,L)))) )
A5: {x} "/\" (rng the mapping of (FinSups the mapping of N)) = { (x "/\" y) where y is Element of L : y in rng the mapping of (FinSups the mapping of N) } by YELLOW_4:42;
assume a in rng the mapping of (x "/\" (FinSups the mapping of N)) ; ::_thesis: a <= sup ({x} "/\" (rng (netmap (N,L))))
then a in {x} "/\" (rng the mapping of (FinSups the mapping of N)) by Th23;
then consider y being Element of L such that
A6: a = x "/\" y and
A7: y in rng the mapping of (FinSups the mapping of N) by A5;
for x being set holds ex_sup_of the mapping of N .: x,L by YELLOW_0:17;
then rng (netmap ((FinSups the mapping of N),L)) c= finsups (rng the mapping of N) by Th24;
then y in finsups (rng the mapping of N) by A7;
then consider Y being finite Subset of (rng the mapping of N) such that
A8: y = "\/" (Y,L) and
A9: ex_sup_of Y,L ;
rng (netmap (N,L)) is directed by A2, Th18;
then consider z being Element of L such that
A10: z in rng the mapping of N and
A11: z is_>=_than Y by WAYBEL_0:1;
A12: x <= x ;
"\/" (Y,L) <= z by A9, A11, YELLOW_0:30;
then A13: x "/\" y <= x "/\" z by A8, A12, YELLOW_3:2;
x in {x} by TARSKI:def_1;
then x "/\" z <= sup (xx "/\" (rng the mapping of N)) by A3, A10, YELLOW_4:1, YELLOW_4:37;
hence a <= sup ({x} "/\" (rng (netmap (N,L)))) by A6, A13, YELLOW_0:def_2; ::_thesis: verum
end;
x "/\" (FinSups the mapping of N) is eventually-directed by Th27;
then rng (netmap ((x "/\" (FinSups the mapping of N)),L)) is directed by Th18;
then ex_sup_of rng the mapping of (x "/\" (FinSups the mapping of N)),L by WAYBEL_0:75;
then ( sup (x "/\" (FinSups the mapping of N)) = "\/" ((rng the mapping of (x "/\" (FinSups the mapping of N))),L) & "\/" ((rng the mapping of (x "/\" (FinSups the mapping of N))),L) <= sup ({x} "/\" (rng (netmap (N,L)))) ) by A4, YELLOW_0:def_9, YELLOW_2:def_5;
then A14: x "/\" (Sup ) <= sup ({x} "/\" (rng (netmap (N,L)))) by A1;
( ex_sup_of R,L & Sup = "\/" ((rng (netmap (N,L))),L) ) by WAYBEL_0:75, YELLOW_2:def_5;
then sup ({x} "/\" (rng (netmap (N,L)))) <= x "/\" (Sup ) by A3, YELLOW_4:53;
hence x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) by A14, ORDERS_2:2; ::_thesis: verum
end;
theorem Th49: :: WAYBEL_2:49
for L being up-complete LATTICE holds
( L is meet-continuous iff ( SupMap L is meet-preserving & SupMap L is join-preserving ) )
proof
let L be up-complete LATTICE; ::_thesis: ( L is meet-continuous iff ( SupMap L is meet-preserving & SupMap L is join-preserving ) )
hereby ::_thesis: ( SupMap L is meet-preserving & SupMap L is join-preserving implies L is meet-continuous )
assume A1: L is meet-continuous ; ::_thesis: ( SupMap L is meet-preserving & SupMap L is join-preserving )
for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
proof
let D1, D2 be non empty directed Subset of L; ::_thesis: (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
for x being Element of L
for E being non empty directed Subset of L st x <= sup E holds
x <= sup ({x} "/\" E) by A1, Th45;
then inf_op L is directed-sups-preserving by Th46;
hence (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th43; ::_thesis: verum
end;
then for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ;
hence ( SupMap L is meet-preserving & SupMap L is join-preserving ) by Th39; ::_thesis: verum
end;
assume A2: ( SupMap L is meet-preserving & SupMap L is join-preserving ) ; ::_thesis: L is meet-continuous
thus L is up-complete ; :: according to WAYBEL_2:def_7 ::_thesis: L is satisfying_MC
for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) by A2, Th38;
then for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th40;
hence L is satisfying_MC by Th44; ::_thesis: verum
end;
registration
let L be meet-continuous LATTICE;
cluster SupMap L -> meet-preserving join-preserving ;
coherence
( SupMap L is meet-preserving & SupMap L is join-preserving ) by Th49;
end;
theorem Th50: :: WAYBEL_2:50
for L being up-complete LATTICE holds
( L is meet-continuous iff for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) )
proof
let L be up-complete LATTICE; ::_thesis: ( L is meet-continuous iff for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) )
hereby ::_thesis: ( ( for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ) implies L is meet-continuous )
assume L is meet-continuous ; ::_thesis: for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2)
then ( SupMap L is meet-preserving & SupMap L is join-preserving ) ;
hence for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) by Th38; ::_thesis: verum
end;
assume for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) ; ::_thesis: L is meet-continuous
then for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th40;
hence ( L is up-complete & L is satisfying_MC ) by Th44; :: according to WAYBEL_2:def_7 ::_thesis: verum
end;
theorem Th51: :: WAYBEL_2:51
for L being up-complete LATTICE holds
( L is meet-continuous iff for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) )
proof
let L be up-complete LATTICE; ::_thesis: ( L is meet-continuous iff for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) )
hereby ::_thesis: ( ( for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) ) implies L is meet-continuous )
assume L is meet-continuous ; ::_thesis: for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
then for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2) by Th50;
hence for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th40; ::_thesis: verum
end;
assume for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) ; ::_thesis: L is meet-continuous
hence ( L is up-complete & L is satisfying_MC ) by Th44; :: according to WAYBEL_2:def_7 ::_thesis: verum
end;
theorem :: WAYBEL_2:52
for L being up-complete LATTICE holds
( L is meet-continuous iff for x being Element of L
for D being non empty directed Subset of L st x <= sup D holds
x = sup ({x} "/\" D) )
proof
let L be up-complete LATTICE; ::_thesis: ( L is meet-continuous iff for x being Element of L
for D being non empty directed Subset of L st x <= sup D holds
x = sup ({x} "/\" D) )
thus ( L is meet-continuous implies for x being Element of L
for D being non empty directed Subset of L st x <= sup D holds
x = sup ({x} "/\" D) ) by Th45; ::_thesis: ( ( for x being Element of L
for D being non empty directed Subset of L st x <= sup D holds
x = sup ({x} "/\" D) ) implies L is meet-continuous )
assume for x being Element of L
for D being non empty directed Subset of L st x <= sup D holds
x = sup ({x} "/\" D) ; ::_thesis: L is meet-continuous
then for x being Element of L
for D being non empty directed Subset of L st x <= sup D holds
x <= sup ({x} "/\" D) ;
then inf_op L is directed-sups-preserving by Th46;
then for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th43;
hence L is meet-continuous by Th51; ::_thesis: verum
end;
theorem Th53: :: WAYBEL_2:53
for L being up-complete Semilattice holds
( L is meet-continuous iff inf_op L is directed-sups-preserving )
proof
let L be up-complete Semilattice; ::_thesis: ( L is meet-continuous iff inf_op L is directed-sups-preserving )
hereby ::_thesis: ( inf_op L is directed-sups-preserving implies L is meet-continuous )
assume L is meet-continuous ; ::_thesis: inf_op L is directed-sups-preserving
then for x being Element of L
for D being non empty directed Subset of L st x <= sup D holds
x <= sup ({x} "/\" D) by Th45;
hence inf_op L is directed-sups-preserving by Th46; ::_thesis: verum
end;
assume inf_op L is directed-sups-preserving ; ::_thesis: L is meet-continuous
then for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) by Th43;
hence ( L is up-complete & L is satisfying_MC ) by Th44; :: according to WAYBEL_2:def_7 ::_thesis: verum
end;
registration
let L be meet-continuous Semilattice;
cluster inf_op L -> directed-sups-preserving ;
coherence
inf_op L is directed-sups-preserving by Th53;
end;
theorem Th54: :: WAYBEL_2:54
for L being up-complete Semilattice holds
( L is meet-continuous iff for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) )
proof
let L be up-complete Semilattice; ::_thesis: ( L is meet-continuous iff for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) )
thus ( L is meet-continuous implies for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) by Th41; ::_thesis: ( ( for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) implies L is meet-continuous )
assume for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ; ::_thesis: L is meet-continuous
hence ( L is up-complete & L is satisfying_MC ) by Th42; :: according to WAYBEL_2:def_7 ::_thesis: verum
end;
theorem :: WAYBEL_2:55
for L being complete Semilattice holds
( L is meet-continuous iff for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) )
proof
let L be complete Semilattice; ::_thesis: ( L is meet-continuous iff for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) )
hereby ::_thesis: ( ( for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ) implies L is meet-continuous )
assume L is meet-continuous ; ::_thesis: for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f))
then for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) by Th54;
hence for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) by Th47; ::_thesis: verum
end;
assume for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ; ::_thesis: L is meet-continuous
then for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) by Th48;
hence ( L is up-complete & L is satisfying_MC ) by Th42; :: according to WAYBEL_2:def_7 ::_thesis: verum
end;
Lm1: for L being meet-continuous Semilattice
for x being Element of L holds x "/\" is directed-sups-preserving
proof
let L be meet-continuous Semilattice; ::_thesis: for x being Element of L holds x "/\" is directed-sups-preserving
let x be Element of L; ::_thesis: x "/\" is directed-sups-preserving
let X be Subset of L; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or x "/\" preserves_sup_of X )
assume A1: ( not X is empty & X is directed ) ; ::_thesis: x "/\" preserves_sup_of X
reconsider X1 = X as non empty Subset of L by A1;
assume ex_sup_of X,L ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (x "/\") .: X,L & "\/" (((x "/\") .: X),L) = (x "/\") . ("\/" (X,L)) )
A2: not (x "/\") .: X1 is empty ;
(x "/\") .: X is directed by A1, YELLOW_2:15;
hence ex_sup_of (x "/\") .: X,L by A2, WAYBEL_0:75; ::_thesis: "\/" (((x "/\") .: X),L) = (x "/\") . ("\/" (X,L))
A3: for x being Element of L
for E being non empty directed Subset of L st x <= sup E holds
x <= sup ({x} "/\" E) by Th45;
thus sup ((x "/\") .: X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) by WAYBEL_1:61
.= sup ({x} "/\" X) by YELLOW_4:42
.= x "/\" (sup X) by A1, A3, Th28
.= (x "/\") . (sup X) by WAYBEL_1:def_18 ; ::_thesis: verum
end;
registration
let L be meet-continuous Semilattice;
let x be Element of L;
clusterx "/\" -> directed-sups-preserving ;
coherence
x "/\" is directed-sups-preserving by Lm1;
end;
theorem Th56: :: WAYBEL_2:56
for H being non empty complete Poset holds
( H is Heyting iff ( H is meet-continuous & H is distributive ) )
proof
let H be non empty complete Poset; ::_thesis: ( H is Heyting iff ( H is meet-continuous & H is distributive ) )
hereby ::_thesis: ( H is meet-continuous & H is distributive implies H is Heyting )
assume A1: H is Heyting ; ::_thesis: ( H is meet-continuous & H is distributive )
then for x being Element of H holds x "/\" is lower_adjoint by WAYBEL_1:def_19;
then for X being Subset of H
for x being Element of H holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of H : y in X } ,H) by WAYBEL_1:64;
then ( H is up-complete & H is satisfying_MC ) by Th37;
hence H is meet-continuous ; ::_thesis: H is distributive
thus H is distributive by A1; ::_thesis: verum
end;
assume A2: ( H is meet-continuous & H is distributive ) ; ::_thesis: H is Heyting
thus H is LATTICE ; :: according to WAYBEL_1:def_19 ::_thesis: for b1 being Element of the carrier of H holds b1 "/\" is lower_adjoint
let a be Element of H; ::_thesis: a "/\" is lower_adjoint
( ( for X being finite Subset of H holds a "/\" preserves_sup_of X ) & ( for X being non empty directed Subset of H holds a "/\" preserves_sup_of X ) ) by A2, Th17, WAYBEL_0:def_37;
then a "/\" is sups-preserving by WAYBEL_0:74;
hence a "/\" is lower_adjoint by WAYBEL_1:17; ::_thesis: verum
end;
registration
cluster non empty reflexive transitive antisymmetric Heyting complete -> non empty distributive meet-continuous for RelStr ;
coherence
for b1 being non empty Poset st b1 is complete & b1 is Heyting holds
( b1 is meet-continuous & b1 is distributive ) by Th56;
cluster non empty reflexive transitive antisymmetric distributive complete meet-continuous -> non empty Heyting for RelStr ;
coherence
for b1 being non empty Poset st b1 is complete & b1 is meet-continuous & b1 is distributive holds
b1 is Heyting by Th56;
end;