:: ROBBINS3 semantic presentation
begin
definition
let L be non empty \/-SemiLattStr ;
attrL is join-Associative means :Def1: :: ROBBINS3:def 1
for x, y, z being Element of L holds x "\/" (y "\/" z) = y "\/" (x "\/" z);
end;
:: deftheorem Def1 defines join-Associative ROBBINS3:def_1_:_
for L being non empty \/-SemiLattStr holds
( L is join-Associative iff for x, y, z being Element of L holds x "\/" (y "\/" z) = y "\/" (x "\/" z) );
definition
let L be non empty /\-SemiLattStr ;
attrL is meet-Associative means :Def2: :: ROBBINS3:def 2
for x, y, z being Element of L holds x "/\" (y "/\" z) = y "/\" (x "/\" z);
end;
:: deftheorem Def2 defines meet-Associative ROBBINS3:def_2_:_
for L being non empty /\-SemiLattStr holds
( L is meet-Associative iff for x, y, z being Element of L holds x "/\" (y "/\" z) = y "/\" (x "/\" z) );
definition
let L be non empty LattStr ;
attrL is meet-Absorbing means :Def3: :: ROBBINS3:def 3
for x, y being Element of L holds x "\/" (x "/\" y) = x;
end;
:: deftheorem Def3 defines meet-Absorbing ROBBINS3:def_3_:_
for L being non empty LattStr holds
( L is meet-Absorbing iff for x, y being Element of L holds x "\/" (x "/\" y) = x );
theorem Th1: :: ROBBINS3:1
for L being non empty LattStr st L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing holds
( L is meet-idempotent & L is join-idempotent )
proof
let L be non empty LattStr ; ::_thesis: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing implies ( L is meet-idempotent & L is join-idempotent ) )
assume A1: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ; ::_thesis: ( L is meet-idempotent & L is join-idempotent )
A2: for x being Element of L holds x "\/" x = x
proof
let a be Element of L; ::_thesis: a "\/" a = a
a = a "\/" (a "/\" a) by A1, Def3;
hence a "\/" a = a by A1, LATTICES:def_9; ::_thesis: verum
end;
for x being Element of L holds x "/\" x = x
proof
let a be Element of L; ::_thesis: a "/\" a = a
a = a "/\" (a "\/" a) by A1, LATTICES:def_9;
hence a "/\" a = a by A1, Def3; ::_thesis: verum
end;
hence ( L is meet-idempotent & L is join-idempotent ) by A2, ROBBINS1:def_7, SHEFFER1:def_9; ::_thesis: verum
end;
theorem Th2: :: ROBBINS3:2
for L being non empty LattStr st L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing holds
( L is meet-commutative & L is join-commutative )
proof
let L be non empty LattStr ; ::_thesis: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing implies ( L is meet-commutative & L is join-commutative ) )
assume A1: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ; ::_thesis: ( L is meet-commutative & L is join-commutative )
then A2: ( L is join-idempotent & L is meet-idempotent ) by Th1;
A3: for x, y being Element of L holds x "/\" y = y "/\" x
proof
let a, b be Element of L; ::_thesis: a "/\" b = b "/\" a
a "/\" b = a "/\" (b "/\" (b "\/" a)) by A1, LATTICES:def_9
.= b "/\" (a "/\" (b "\/" a)) by A1, Def2
.= b "/\" (a "/\" (b "\/" (a "\/" a))) by A2, ROBBINS1:def_7
.= b "/\" (a "/\" (a "\/" (b "\/" a))) by A1, Def1
.= b "/\" a by A1, LATTICES:def_9 ;
hence a "/\" b = b "/\" a ; ::_thesis: verum
end;
for x, y being Element of L holds x "\/" y = y "\/" x
proof
let a, b be Element of L; ::_thesis: a "\/" b = b "\/" a
a "\/" b = a "\/" (b "\/" (b "/\" a)) by A1, Def3
.= b "\/" (a "\/" (b "/\" a)) by A1, Def1
.= b "\/" (a "\/" (b "/\" (a "/\" a))) by A2, SHEFFER1:def_9
.= b "\/" (a "\/" (a "/\" (b "/\" a))) by A1, Def2
.= b "\/" a by A1, Def3 ;
hence a "\/" b = b "\/" a ; ::_thesis: verum
end;
hence ( L is meet-commutative & L is join-commutative ) by A3, LATTICES:def_4, LATTICES:def_6; ::_thesis: verum
end;
theorem Th3: :: ROBBINS3:3
for L being non empty LattStr st L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing holds
L is meet-absorbing
proof
let L be non empty LattStr ; ::_thesis: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing implies L is meet-absorbing )
assume A1: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ; ::_thesis: L is meet-absorbing
then A2: ( L is meet-commutative & L is join-commutative ) by Th2;
for x, y being Element of L holds (x "/\" y) "\/" y = y
proof
let a, b be Element of L; ::_thesis: (a "/\" b) "\/" b = b
b = b "\/" (b "/\" a) by A1, Def3
.= b "\/" (a "/\" b) by A2, LATTICES:def_6
.= (a "/\" b) "\/" b by A2, LATTICES:def_4 ;
hence (a "/\" b) "\/" b = b ; ::_thesis: verum
end;
hence L is meet-absorbing by LATTICES:def_8; ::_thesis: verum
end;
theorem Th4: :: ROBBINS3:4
for L being non empty LattStr st L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing holds
( L is meet-associative & L is join-associative )
proof
let L be non empty LattStr ; ::_thesis: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing implies ( L is meet-associative & L is join-associative ) )
assume A1: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ; ::_thesis: ( L is meet-associative & L is join-associative )
then A2: ( L is meet-commutative & L is join-commutative ) by Th2;
A3: for x, y, z being Element of L holds x "\/" (y "\/" z) = (x "\/" y) "\/" z
proof
let a, b, c be Element of L; ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
a "\/" (b "\/" c) = a "\/" (c "\/" b) by A2, LATTICES:def_4
.= c "\/" (a "\/" b) by A1, Def1
.= (a "\/" b) "\/" c by A2, LATTICES:def_4 ;
hence a "\/" (b "\/" c) = (a "\/" b) "\/" c ; ::_thesis: verum
end;
for x, y, z being Element of L holds x "/\" (y "/\" z) = (x "/\" y) "/\" z
proof
let a, b, c be Element of L; ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
a "/\" (b "/\" c) = a "/\" (c "/\" b) by A2, LATTICES:def_6
.= c "/\" (a "/\" b) by A1, Def2
.= (a "/\" b) "/\" c by A2, LATTICES:def_6 ;
hence a "/\" (b "/\" c) = (a "/\" b) "/\" c ; ::_thesis: verum
end;
hence ( L is meet-associative & L is join-associative ) by A3, LATTICES:def_5, LATTICES:def_7; ::_thesis: verum
end;
theorem Th5: :: ROBBINS3:5
for L being non empty LattStr holds
( L is Lattice-like iff ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) )
proof
let L be non empty LattStr ; ::_thesis: ( L is Lattice-like iff ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) )
A1: ( L is Lattice-like implies ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) )
proof
assume A2: L is Lattice-like ; ::_thesis: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing )
A3: for x, y, z being Element of L holds x "/\" (y "/\" z) = y "/\" (x "/\" z)
proof
let a, b, c be Element of L; ::_thesis: a "/\" (b "/\" c) = b "/\" (a "/\" c)
a "/\" (b "/\" c) = (a "/\" b) "/\" c by A2, LATTICES:def_7
.= (b "/\" a) "/\" c by A2, LATTICES:def_6
.= b "/\" (a "/\" c) by A2, LATTICES:def_7 ;
hence a "/\" (b "/\" c) = b "/\" (a "/\" c) ; ::_thesis: verum
end;
A4: for x, y being Element of L holds x "\/" (x "/\" y) = x
proof
let a, b be Element of L; ::_thesis: a "\/" (a "/\" b) = a
a = (b "/\" a) "\/" a by A2, LATTICES:def_8
.= (a "/\" b) "\/" a by A2, LATTICES:def_6
.= a "\/" (a "/\" b) by A2, LATTICES:def_4 ;
hence a "\/" (a "/\" b) = a ; ::_thesis: verum
end;
for x, y, z being Element of L holds x "\/" (y "\/" z) = y "\/" (x "\/" z)
proof
let a, b, c be Element of L; ::_thesis: a "\/" (b "\/" c) = b "\/" (a "\/" c)
a "\/" (b "\/" c) = (a "\/" b) "\/" c by A2, LATTICES:def_5
.= (b "\/" a) "\/" c by A2, LATTICES:def_4
.= b "\/" (a "\/" c) by A2, LATTICES:def_5 ;
hence a "\/" (b "\/" c) = b "\/" (a "\/" c) ; ::_thesis: verum
end;
hence ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) by A2, A3, A4, Def1, Def2, Def3; ::_thesis: verum
end;
( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing implies L is Lattice-like )
proof
assume A5: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ; ::_thesis: L is Lattice-like
then A6: L is meet-absorbing by Th3;
( L is meet-commutative & L is join-commutative & L is meet-associative & L is join-associative ) by A5, Th2, Th4;
hence L is Lattice-like by A5, A6; ::_thesis: verum
end;
hence ( L is Lattice-like iff ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ) by A1; ::_thesis: verum
end;
registration
cluster non empty Lattice-like -> non empty join-Associative meet-Associative meet-Absorbing for LattStr ;
coherence
for b1 being non empty LattStr st b1 is Lattice-like holds
( b1 is meet-Associative & b1 is join-Associative & b1 is meet-Absorbing ) by Th5;
cluster non empty join-absorbing join-Associative meet-Associative meet-Absorbing -> non empty Lattice-like for LattStr ;
coherence
for b1 being non empty LattStr st b1 is meet-Associative & b1 is join-Associative & b1 is meet-Absorbing & b1 is join-absorbing holds
b1 is Lattice-like by Th5;
end;
begin
registration
cluster non empty PartialOrdered OrderInvolutive -> non empty Dneg PartialOrdered for OrthoRelStr ;
coherence
for b1 being non empty PartialOrdered OrthoRelStr st b1 is OrderInvolutive holds
b1 is Dneg
proof
let L be non empty PartialOrdered OrthoRelStr ; ::_thesis: ( L is OrderInvolutive implies L is Dneg )
assume L is OrderInvolutive ; ::_thesis: L is Dneg
then consider f being Function of L,L such that
A1: f = the Compl of L and
A2: f is Orderinvolutive by OPOSET_1:def_18;
( f is V296() & f is antitone ) by A2, OPOSET_1:def_17;
hence L is Dneg by A1, OPOSET_1:def_3; ::_thesis: verum
end;
end;
theorem Th6: :: ROBBINS3:6
for L being non empty Dneg OrthoRelStr
for x being Element of L holds (x `) ` = x
proof
let L be non empty Dneg OrthoRelStr ; ::_thesis: for x being Element of L holds (x `) ` = x
let x be Element of L; ::_thesis: (x `) ` = x
consider f being Function of L,L such that
A1: f = the Compl of L and
A2: f is V296() by OPOSET_1:def_3;
( f . x = x ` & f . (f . x) = x ) by A1, A2, PARTIT_2:def_3, ROBBINS1:def_3;
hence (x `) ` = x by A1, ROBBINS1:def_3; ::_thesis: verum
end;
theorem Th7: :: ROBBINS3:7
for O being non empty PartialOrdered OrderInvolutive OrthoRelStr
for x, y being Element of O st x <= y holds
y ` <= x `
proof
let O be non empty PartialOrdered OrderInvolutive OrthoRelStr ; ::_thesis: for x, y being Element of O st x <= y holds
y ` <= x `
let x, y be Element of O; ::_thesis: ( x <= y implies y ` <= x ` )
assume A1: x <= y ; ::_thesis: y ` <= x `
consider f being Function of O,O such that
A2: f = the Compl of O and
A3: f is Orderinvolutive by OPOSET_1:def_18;
( f is V296() & f is antitone ) by A3, OPOSET_1:def_17;
then f . x >= f . y by A1, WAYBEL_9:def_1;
then x ` >= f . y by A2, ROBBINS1:def_3;
hence y ` <= x ` by A2, ROBBINS1:def_3; ::_thesis: verum
end;
registration
cluster non empty reflexive transitive antisymmetric with_suprema with_infima strict Dneg PartialOrdered Pure OrderInvolutive for OrthoRelStr ;
existence
ex b1 being PreOrthoPoset st
( b1 is with_infima & b1 is with_suprema & b1 is strict )
proof
take TrivOrthoRelStr ; ::_thesis: ( TrivOrthoRelStr is with_infima & TrivOrthoRelStr is with_suprema & TrivOrthoRelStr is strict )
thus ( TrivOrthoRelStr is with_infima & TrivOrthoRelStr is with_suprema & TrivOrthoRelStr is strict ) ; ::_thesis: verum
end;
end;
notation
let L be non empty \/-SemiLattStr ;
let x, y be Element of L;
synonym x |_| y for x "\/" y;
end;
notation
let L be non empty /\-SemiLattStr ;
let x, y be Element of L;
synonym x |^| y for x "/\" y;
end;
notation
let L be non empty RelStr ;
let x, y be Element of L;
synonym x "|^|" y for x "/\" y;
synonym x "|_|" y for x "\/" y;
end;
begin
definition
attrc1 is strict ;
struct \/-SemiLattRelStr -> \/-SemiLattStr , RelStr ;
aggr\/-SemiLattRelStr(# carrier, L_join, InternalRel #) -> \/-SemiLattRelStr ;
end;
definition
attrc1 is strict ;
struct /\-SemiLattRelStr -> /\-SemiLattStr , RelStr ;
aggr/\-SemiLattRelStr(# carrier, L_meet, InternalRel #) -> /\-SemiLattRelStr ;
end;
definition
attrc1 is strict ;
struct LattRelStr -> /\-SemiLattRelStr , \/-SemiLattRelStr , LattStr ;
aggrLattRelStr(# carrier, L_join, L_meet, InternalRel #) -> LattRelStr ;
end;
definition
func TrivLattRelStr -> LattRelStr equals :: ROBBINS3:def 4
LattRelStr(# 1,op2,op2,(id 1) #);
coherence
LattRelStr(# 1,op2,op2,(id 1) #) is LattRelStr ;
end;
:: deftheorem defines TrivLattRelStr ROBBINS3:def_4_:_
TrivLattRelStr = LattRelStr(# 1,op2,op2,(id 1) #);
registration
cluster TrivLattRelStr -> 1 -element ;
coherence
TrivLattRelStr is 1 -element
proof
the carrier of TrivLattRelStr = {0} by CARD_1:49;
hence the carrier of TrivLattRelStr is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum
end;
end;
registration
cluster non empty for \/-SemiLattRelStr ;
existence
not for b1 being \/-SemiLattRelStr holds b1 is empty
proof
take TrivLattRelStr ; ::_thesis: not TrivLattRelStr is empty
thus not TrivLattRelStr is empty ; ::_thesis: verum
end;
cluster non empty for /\-SemiLattRelStr ;
existence
not for b1 being /\-SemiLattRelStr holds b1 is empty
proof
take TrivLattRelStr ; ::_thesis: not TrivLattRelStr is empty
thus not TrivLattRelStr is empty ; ::_thesis: verum
end;
cluster non empty for LattRelStr ;
existence
not for b1 being LattRelStr holds b1 is empty
proof
take TrivLattRelStr ; ::_thesis: not TrivLattRelStr is empty
thus not TrivLattRelStr is empty ; ::_thesis: verum
end;
end;
theorem :: ROBBINS3:8
for R being non empty RelStr st the InternalRel of R is_reflexive_in the carrier of R & the InternalRel of R is antisymmetric & the InternalRel of R is transitive holds
( R is reflexive & R is antisymmetric & R is transitive )
proof
let r be non empty RelStr ; ::_thesis: ( the InternalRel of r is_reflexive_in the carrier of r & the InternalRel of r is antisymmetric & the InternalRel of r is transitive implies ( r is reflexive & r is antisymmetric & r is transitive ) )
set i = the InternalRel of r;
set c = the carrier of r;
assume that
A1: the InternalRel of r is_reflexive_in the carrier of r and
A2: ( the InternalRel of r is antisymmetric & the InternalRel of r is transitive ) ; ::_thesis: ( r is reflexive & r is antisymmetric & r is transitive )
A3: the InternalRel of r is_transitive_in field the InternalRel of r by A2, RELAT_2:def_16;
A4: field the InternalRel of r = the carrier of r by A1, PARTIT_2:21;
then the InternalRel of r is_antisymmetric_in the carrier of r by A2, RELAT_2:def_12;
hence ( r is reflexive & r is antisymmetric & r is transitive ) by A1, A4, A3, ORDERS_2:def_2, ORDERS_2:def_3, ORDERS_2:def_4; ::_thesis: verum
end;
registration
cluster TrivLattRelStr -> reflexive ;
coherence
TrivLattRelStr is reflexive
proof
set T = TrivLattRelStr ;
set C = the carrier of TrivLattRelStr;
set I = the InternalRel of TrivLattRelStr;
field the InternalRel of TrivLattRelStr = the carrier of TrivLattRelStr by PARTIT_2:18;
then the InternalRel of TrivLattRelStr is_reflexive_in the carrier of TrivLattRelStr by RELAT_2:def_9;
hence TrivLattRelStr is reflexive by ORDERS_2:def_2; ::_thesis: verum
end;
end;
registration
cluster reflexive transitive antisymmetric with_suprema with_infima for LattRelStr ;
existence
ex b1 being LattRelStr st
( b1 is antisymmetric & b1 is reflexive & b1 is transitive & b1 is with_suprema & b1 is with_infima )
proof
take TrivLattRelStr ; ::_thesis: ( TrivLattRelStr is antisymmetric & TrivLattRelStr is reflexive & TrivLattRelStr is transitive & TrivLattRelStr is with_suprema & TrivLattRelStr is with_infima )
thus ( TrivLattRelStr is antisymmetric & TrivLattRelStr is reflexive & TrivLattRelStr is transitive & TrivLattRelStr is with_suprema & TrivLattRelStr is with_infima ) ; ::_thesis: verum
end;
end;
registration
cluster TrivLattRelStr -> meet-Absorbing ;
coherence
TrivLattRelStr is meet-Absorbing ;
end;
Lm1: TrivLattRelStr is Lattice-like
;
registration
cluster non empty Lattice-like for LattRelStr ;
existence
ex b1 being non empty LattRelStr st b1 is Lattice-like by Lm1;
end;
definition
let L be Lattice;
:: original: LattRel
redefine func LattRel L -> Order of the carrier of L;
coherence
LattRel L is Order of the carrier of L
proof
A1: LattRel L = { [p,q] where p, q is Element of L : p [= q } by FILTER_1:def_8;
LattRel L c= [: the carrier of L, the carrier of L:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LattRel L or x in [: the carrier of L, the carrier of L:] )
assume x in LattRel L ; ::_thesis: x in [: the carrier of L, the carrier of L:]
then ex p, q being Element of L st
( x = [p,q] & p [= q ) by A1;
hence x in [: the carrier of L, the carrier of L:] by ZFMISC_1:87; ::_thesis: verum
end;
then reconsider R = LattRel L as Relation of the carrier of L ;
A2: R is_antisymmetric_in the carrier of L
proof
let x, y be set ; :: according to RELAT_2:def_4 ::_thesis: ( not x in the carrier of L or not y in the carrier of L or not [x,y] in R or not [y,x] in R or x = y )
assume ( x in the carrier of L & y in the carrier of L ) ; ::_thesis: ( not [x,y] in R or not [y,x] in R or x = y )
then reconsider x9 = x, y9 = y as Element of L ;
assume ( [x,y] in R & [y,x] in R ) ; ::_thesis: x = y
then ( x9 [= y9 & y9 [= x9 ) by FILTER_1:31;
hence x = y by LATTICES:8; ::_thesis: verum
end;
A3: R is_transitive_in the carrier of L
proof
let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in the carrier of L or not y in the carrier of L or not z in the carrier of L or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume ( x in the carrier of L & y in the carrier of L & z in the carrier of L ) ; ::_thesis: ( not [x,y] in R or not [y,z] in R or [x,z] in R )
then reconsider x9 = x, y9 = y, z9 = z as Element of L ;
assume ( [x,y] in R & [y,z] in R ) ; ::_thesis: [x,z] in R
then ( x9 [= y9 & y9 [= z9 ) by FILTER_1:31;
then x9 [= z9 by LATTICES:7;
hence [x,z] in R by FILTER_1:31; ::_thesis: verum
end;
A4: R is_reflexive_in the carrier of L
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in the carrier of L or [x,x] in R )
assume x in the carrier of L ; ::_thesis: [x,x] in R
then reconsider x = x as Element of L ;
x [= x ;
hence [x,x] in R by FILTER_1:31; ::_thesis: verum
end;
then ( dom R = the carrier of L & field R = the carrier of L ) by ORDERS_1:13;
hence LattRel L is Order of the carrier of L by A4, A2, A3, PARTFUN1:def_2, RELAT_2:def_9, RELAT_2:def_12, RELAT_2:def_16; ::_thesis: verum
end;
end;
begin
definition
attrc1 is strict ;
struct OrthoLattRelStr -> LattRelStr , OrthoLattStr , OrthoRelStr ;
aggrOrthoLattRelStr(# carrier, L_join, L_meet, InternalRel, Compl #) -> OrthoLattRelStr ;
end;
definition
func TrivCLRelStr -> OrthoLattRelStr equals :: ROBBINS3:def 5
OrthoLattRelStr(# 1,op2,op2,(id 1),op1 #);
coherence
OrthoLattRelStr(# 1,op2,op2,(id 1),op1 #) is OrthoLattRelStr ;
end;
:: deftheorem defines TrivCLRelStr ROBBINS3:def_5_:_
TrivCLRelStr = OrthoLattRelStr(# 1,op2,op2,(id 1),op1 #);
definition
let L be non empty ComplStr ;
attrL is involutive means :Def6: :: ROBBINS3:def 6
for x being Element of L holds (x `) ` = x;
end;
:: deftheorem Def6 defines involutive ROBBINS3:def_6_:_
for L being non empty ComplStr holds
( L is involutive iff for x being Element of L holds (x `) ` = x );
definition
let L be non empty ComplLLattStr ;
attrL is with_Top means :Def7: :: ROBBINS3:def 7
for x, y being Element of L holds x |_| (x `) = y |_| (y `);
end;
:: deftheorem Def7 defines with_Top ROBBINS3:def_7_:_
for L being non empty ComplLLattStr holds
( L is with_Top iff for x, y being Element of L holds x |_| (x `) = y |_| (y `) );
registration
cluster TrivOrtLat -> involutive with_Top ;
coherence
( TrivOrtLat is involutive & TrivOrtLat is with_Top )
proof
thus TrivOrtLat is involutive ::_thesis: TrivOrtLat is with_Top
proof
let x be Element of TrivOrtLat; :: according to ROBBINS3:def_6 ::_thesis: (x `) ` = x
thus (x `) ` = x by STRUCT_0:def_10; ::_thesis: verum
end;
thus TrivOrtLat is with_Top ::_thesis: verum
proof
let x, y be Element of TrivOrtLat; :: according to ROBBINS3:def_7 ::_thesis: x |_| (x `) = y |_| (y `)
thus x |_| (x `) = y |_| (y `) by STRUCT_0:def_10; ::_thesis: verum
end;
end;
end;
registration
cluster TrivCLRelStr -> 1 -element ;
coherence
TrivCLRelStr is 1 -element
proof
the carrier of TrivCLRelStr = {0} by CARD_1:49;
hence the carrier of TrivCLRelStr is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum
end;
end;
registration
cluster TrivCLRelStr -> reflexive ;
coherence
TrivCLRelStr is reflexive
proof
for x being Element of TrivCLRelStr holds x <= x
proof
let x be Element of TrivCLRelStr; ::_thesis: x <= x
[x,x] in id {{}} by CARD_1:49, RELAT_1:def_10;
hence x <= x by CARD_1:49, ORDERS_2:def_5; ::_thesis: verum
end;
hence TrivCLRelStr is reflexive by YELLOW_0:def_1; ::_thesis: verum
end;
end;
registration
cluster TrivCLRelStr -> involutive with_Top ;
coherence
( TrivCLRelStr is involutive & TrivCLRelStr is with_Top )
proof
set L = TrivCLRelStr ;
thus TrivCLRelStr is involutive ::_thesis: TrivCLRelStr is with_Top
proof
let x be Element of TrivCLRelStr; :: according to ROBBINS3:def_6 ::_thesis: (x `) ` = x
thus (x `) ` = x by STRUCT_0:def_10; ::_thesis: verum
end;
thus TrivCLRelStr is with_Top ::_thesis: verum
proof
let x, y be Element of TrivCLRelStr; :: according to ROBBINS3:def_7 ::_thesis: x |_| (x `) = y |_| (y `)
thus x |_| (x `) = y |_| (y `) by STRUCT_0:def_10; ::_thesis: verum
end;
end;
end;
registration
cluster non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean de_Morgan upper-bounded' lower-bounded' distributive' complemented' join-Associative meet-Associative meet-Absorbing involutive with_Top for OrthoLattStr ;
existence
ex b1 being 1 -element OrthoLattStr st
( b1 is involutive & b1 is with_Top & b1 is de_Morgan & b1 is Lattice-like )
proof
take TrivOrtLat ; ::_thesis: ( TrivOrtLat is involutive & TrivOrtLat is with_Top & TrivOrtLat is de_Morgan & TrivOrtLat is Lattice-like )
thus ( TrivOrtLat is involutive & TrivOrtLat is with_Top & TrivOrtLat is de_Morgan & TrivOrtLat is Lattice-like ) ; ::_thesis: verum
end;
end;
definition
mode Ortholattice is non empty Lattice-like de_Morgan involutive with_Top OrthoLattStr ;
end;
begin
theorem Th9: :: ROBBINS3:9
for K, L being non empty LattStr st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is join-commutative holds
L is join-commutative
proof
let K, L be non empty LattStr ; ::_thesis: ( LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is join-commutative implies L is join-commutative )
assume that
A1: LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) and
A2: K is join-commutative ; ::_thesis: L is join-commutative
L is join-commutative
proof
let x, y be Element of L; :: according to LATTICES:def_4 ::_thesis: x |_| y = y |_| x
reconsider x9 = x, y9 = y as Element of K by A1;
x9 |_| y9 = y9 |_| x9 by A2, LATTICES:def_4;
hence x |_| y = y |_| x by A1; ::_thesis: verum
end;
hence L is join-commutative ; ::_thesis: verum
end;
theorem Th10: :: ROBBINS3:10
for K, L being non empty LattStr st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is meet-commutative holds
L is meet-commutative
proof
let K, L be non empty LattStr ; ::_thesis: ( LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is meet-commutative implies L is meet-commutative )
assume that
A1: LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) and
A2: K is meet-commutative ; ::_thesis: L is meet-commutative
L is meet-commutative
proof
let x, y be Element of L; :: according to LATTICES:def_6 ::_thesis: x |^| y = y |^| x
reconsider x9 = x, y9 = y as Element of K by A1;
x9 "/\" y9 = y9 "/\" x9 by A2, LATTICES:def_6;
hence x |^| y = y |^| x by A1; ::_thesis: verum
end;
hence L is meet-commutative ; ::_thesis: verum
end;
theorem Th11: :: ROBBINS3:11
for K, L being non empty LattStr st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is join-associative holds
L is join-associative
proof
let K, L be non empty LattStr ; ::_thesis: ( LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is join-associative implies L is join-associative )
assume that
A1: LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) and
A2: K is join-associative ; ::_thesis: L is join-associative
L is join-associative
proof
let x, y, z be Element of L; :: according to LATTICES:def_5 ::_thesis: x |_| (y |_| z) = (x |_| y) |_| z
reconsider x9 = x, y9 = y, z9 = z as Element of K by A1;
(x9 |_| y9) |_| z9 = x9 |_| (y9 |_| z9) by A2, LATTICES:def_5;
hence x |_| (y |_| z) = (x |_| y) |_| z by A1; ::_thesis: verum
end;
hence L is join-associative ; ::_thesis: verum
end;
theorem Th12: :: ROBBINS3:12
for K, L being non empty LattStr st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is meet-associative holds
L is meet-associative
proof
let K, L be non empty LattStr ; ::_thesis: ( LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is meet-associative implies L is meet-associative )
assume that
A1: LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) and
A2: K is meet-associative ; ::_thesis: L is meet-associative
L is meet-associative
proof
let x, y, z be Element of L; :: according to LATTICES:def_7 ::_thesis: x |^| (y |^| z) = (x |^| y) |^| z
reconsider x9 = x, y9 = y, z9 = z as Element of K by A1;
(x9 "/\" y9) "/\" z9 = x9 "/\" (y9 "/\" z9) by A2, LATTICES:def_7;
hence x |^| (y |^| z) = (x |^| y) |^| z by A1; ::_thesis: verum
end;
hence L is meet-associative ; ::_thesis: verum
end;
theorem Th13: :: ROBBINS3:13
for K, L being non empty LattStr st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is join-absorbing holds
L is join-absorbing
proof
let K, L be non empty LattStr ; ::_thesis: ( LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is join-absorbing implies L is join-absorbing )
assume that
A1: LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) and
A2: K is join-absorbing ; ::_thesis: L is join-absorbing
L is join-absorbing
proof
let x, y be Element of L; :: according to LATTICES:def_9 ::_thesis: x |^| (x |_| y) = x
reconsider x9 = x, y9 = y as Element of K by A1;
x9 "/\" (x9 "\/" y9) = x9 by A2, LATTICES:def_9;
hence x |^| (x |_| y) = x by A1; ::_thesis: verum
end;
hence L is join-absorbing ; ::_thesis: verum
end;
theorem Th14: :: ROBBINS3:14
for K, L being non empty LattStr st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is meet-absorbing holds
L is meet-absorbing
proof
let K, L be non empty LattStr ; ::_thesis: ( LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is meet-absorbing implies L is meet-absorbing )
assume that
A1: LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) and
A2: K is meet-absorbing ; ::_thesis: L is meet-absorbing
L is meet-absorbing
proof
let x, y be Element of L; :: according to LATTICES:def_8 ::_thesis: (x |^| y) |_| y = y
reconsider x9 = x, y9 = y as Element of K by A1;
(x9 "/\" y9) "\/" y9 = y9 by A2, LATTICES:def_8;
hence (x |^| y) |_| y = y by A1; ::_thesis: verum
end;
hence L is meet-absorbing ; ::_thesis: verum
end;
theorem :: ROBBINS3:15
for K, L being non empty LattStr st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is Lattice-like holds
L is Lattice-like
proof
let K, L be non empty LattStr ; ::_thesis: ( LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is Lattice-like implies L is Lattice-like )
assume ( LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is Lattice-like ) ; ::_thesis: L is Lattice-like
then ( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing ) by Th9, Th10, Th11, Th12, Th13, Th14;
hence L is Lattice-like ; ::_thesis: verum
end;
theorem :: ROBBINS3:16
for L1, L2 being non empty \/-SemiLattStr st \/-SemiLattStr(# the carrier of L1, the L_join of L1 #) = \/-SemiLattStr(# the carrier of L2, the L_join of L2 #) holds
for a1, b1 being Element of L1
for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds
a1 "\/" b1 = a2 "\/" b2 ;
theorem :: ROBBINS3:17
for L1, L2 being non empty /\-SemiLattStr st /\-SemiLattStr(# the carrier of L1, the L_meet of L1 #) = /\-SemiLattStr(# the carrier of L2, the L_meet of L2 #) holds
for a1, b1 being Element of L1
for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds
a1 "/\" b1 = a2 "/\" b2 ;
theorem Th18: :: ROBBINS3:18
for K, L being non empty ComplStr
for x being Element of K
for y being Element of L st the Compl of K = the Compl of L & x = y holds
x ` = y `
proof
let K, L be non empty ComplStr ; ::_thesis: for x being Element of K
for y being Element of L st the Compl of K = the Compl of L & x = y holds
x ` = y `
let x be Element of K; ::_thesis: for y being Element of L st the Compl of K = the Compl of L & x = y holds
x ` = y `
let y be Element of L; ::_thesis: ( the Compl of K = the Compl of L & x = y implies x ` = y ` )
assume ( the Compl of K = the Compl of L & x = y ) ; ::_thesis: x ` = y `
then x ` = the Compl of L . y by ROBBINS1:def_3
.= y ` by ROBBINS1:def_3 ;
hence x ` = y ` ; ::_thesis: verum
end;
theorem Th19: :: ROBBINS3:19
for K, L being non empty ComplLLattStr st ComplLLattStr(# the carrier of K, the L_join of K, the Compl of K #) = ComplLLattStr(# the carrier of L, the L_join of L, the Compl of L #) & K is with_Top holds
L is with_Top
proof
let K, L be non empty ComplLLattStr ; ::_thesis: ( ComplLLattStr(# the carrier of K, the L_join of K, the Compl of K #) = ComplLLattStr(# the carrier of L, the L_join of L, the Compl of L #) & K is with_Top implies L is with_Top )
assume that
A1: ComplLLattStr(# the carrier of K, the L_join of K, the Compl of K #) = ComplLLattStr(# the carrier of L, the L_join of L, the Compl of L #) and
A2: K is with_Top ; ::_thesis: L is with_Top
for x, y being Element of L holds x |_| (x `) = y |_| (y `)
proof
let x, y be Element of L; ::_thesis: x |_| (x `) = y |_| (y `)
reconsider x9 = x, y9 = y as Element of K by A1;
x |_| (x `) = x9 |_| (x9 `) by A1, Th18
.= y9 |_| (y9 `) by A2, Def7
.= y |_| (y `) by A1, Th18 ;
hence x |_| (x `) = y |_| (y `) ; ::_thesis: verum
end;
hence L is with_Top by Def7; ::_thesis: verum
end;
theorem Th20: :: ROBBINS3:20
for K, L being non empty OrthoLattStr st OrthoLattStr(# the carrier of K, the L_join of K, the L_meet of K, the Compl of K #) = OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) & K is de_Morgan holds
L is de_Morgan
proof
let K, L be non empty OrthoLattStr ; ::_thesis: ( OrthoLattStr(# the carrier of K, the L_join of K, the L_meet of K, the Compl of K #) = OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) & K is de_Morgan implies L is de_Morgan )
assume that
A1: OrthoLattStr(# the carrier of K, the L_join of K, the L_meet of K, the Compl of K #) = OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) and
A2: K is de_Morgan ; ::_thesis: L is de_Morgan
for x, y being Element of L holds x "/\" y = ((x `) "\/" (y `)) `
proof
let x, y be Element of L; ::_thesis: x "/\" y = ((x `) "\/" (y `)) `
reconsider x9 = x, y9 = y as Element of K by A1;
A3: ( x ` = x9 ` & y ` = y9 ` ) by A1, Th18;
x "/\" y = x9 "/\" y9 by A1
.= ((x9 `) "\/" (y9 `)) ` by A2, ROBBINS1:def_23
.= ((x `) "\/" (y `)) ` by A1, A3, Th18 ;
hence x "/\" y = ((x `) "\/" (y `)) ` ; ::_thesis: verum
end;
hence L is de_Morgan by ROBBINS1:def_23; ::_thesis: verum
end;
theorem Th21: :: ROBBINS3:21
for K, L being non empty OrthoLattStr st OrthoLattStr(# the carrier of K, the L_join of K, the L_meet of K, the Compl of K #) = OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) & K is involutive holds
L is involutive
proof
let K, L be non empty OrthoLattStr ; ::_thesis: ( OrthoLattStr(# the carrier of K, the L_join of K, the L_meet of K, the Compl of K #) = OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) & K is involutive implies L is involutive )
assume that
A1: OrthoLattStr(# the carrier of K, the L_join of K, the L_meet of K, the Compl of K #) = OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) and
A2: K is involutive ; ::_thesis: L is involutive
for x being Element of L holds (x `) ` = x
proof
let x be Element of L; ::_thesis: (x `) ` = x
reconsider x9 = x as Element of K by A1;
x ` = x9 ` by A1, Th18;
then (x `) ` = (x9 `) ` by A1, Th18
.= x by A2, Def6 ;
hence (x `) ` = x ; ::_thesis: verum
end;
hence L is involutive by Def6; ::_thesis: verum
end;
begin
definition
let R be RelStr ;
mode RelAugmentation of R -> LattRelStr means :: ROBBINS3:def 8
RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of R, the InternalRel of R #);
existence
ex b1 being LattRelStr st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of R, the InternalRel of R #)
proof
set A = the BinOp of the carrier of R;
set L = LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #);
take LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #) ; ::_thesis: RelStr(# the carrier of LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #), the InternalRel of LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #) #) = RelStr(# the carrier of R, the InternalRel of R #)
thus RelStr(# the carrier of LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #), the InternalRel of LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #) #) = RelStr(# the carrier of R, the InternalRel of R #) ; ::_thesis: verum
end;
end;
:: deftheorem defines RelAugmentation ROBBINS3:def_8_:_
for R being RelStr
for b2 being LattRelStr holds
( b2 is RelAugmentation of R iff RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of R, the InternalRel of R #) );
definition
let R be LattStr ;
mode LatAugmentation of R -> LattRelStr means :Def9: :: ROBBINS3:def 9
LattStr(# the carrier of it, the L_join of it, the L_meet of it #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #);
existence
ex b1 being LattRelStr st LattStr(# the carrier of b1, the L_join of b1, the L_meet of b1 #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #)
proof
set IR = the Relation of the carrier of R;
set L = LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #);
take LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #) ; ::_thesis: LattStr(# the carrier of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #), the L_join of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #), the L_meet of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #) #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #)
thus LattStr(# the carrier of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #), the L_join of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #), the L_meet of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #) #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) ; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines LatAugmentation ROBBINS3:def_9_:_
for R being LattStr
for b2 being LattRelStr holds
( b2 is LatAugmentation of R iff LattStr(# the carrier of b2, the L_join of b2, the L_meet of b2 #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) );
registration
let L be non empty LattStr ;
cluster -> non empty for LatAugmentation of L;
coherence
for b1 being LatAugmentation of L holds not b1 is empty
proof
let R be LatAugmentation of L; ::_thesis: not R is empty
LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) by Def9;
hence not R is empty ; ::_thesis: verum
end;
end;
registration
let L be non empty meet-associative LattStr ;
cluster -> meet-associative for LatAugmentation of L;
coherence
for b1 being LatAugmentation of L holds b1 is meet-associative
proof
let R be LatAugmentation of L; ::_thesis: R is meet-associative
LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) by Def9;
hence R is meet-associative by Th12; ::_thesis: verum
end;
end;
registration
let L be non empty join-associative LattStr ;
cluster -> join-associative for LatAugmentation of L;
coherence
for b1 being LatAugmentation of L holds b1 is join-associative
proof
let R be LatAugmentation of L; ::_thesis: R is join-associative
LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) by Def9;
hence R is join-associative by Th11; ::_thesis: verum
end;
end;
registration
let L be non empty meet-commutative LattStr ;
cluster -> meet-commutative for LatAugmentation of L;
coherence
for b1 being LatAugmentation of L holds b1 is meet-commutative
proof
let R be LatAugmentation of L; ::_thesis: R is meet-commutative
LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) by Def9;
hence R is meet-commutative by Th10; ::_thesis: verum
end;
end;
registration
let L be non empty join-commutative LattStr ;
cluster -> join-commutative for LatAugmentation of L;
coherence
for b1 being LatAugmentation of L holds b1 is join-commutative
proof
let R be LatAugmentation of L; ::_thesis: R is join-commutative
LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) by Def9;
hence R is join-commutative by Th9; ::_thesis: verum
end;
end;
registration
let L be non empty join-absorbing LattStr ;
cluster -> join-absorbing for LatAugmentation of L;
coherence
for b1 being LatAugmentation of L holds b1 is join-absorbing
proof
let R be LatAugmentation of L; ::_thesis: R is join-absorbing
LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) by Def9;
hence R is join-absorbing by Th13; ::_thesis: verum
end;
end;
registration
let L be non empty meet-absorbing LattStr ;
cluster -> meet-absorbing for LatAugmentation of L;
coherence
for b1 being LatAugmentation of L holds b1 is meet-absorbing
proof
let R be LatAugmentation of L; ::_thesis: R is meet-absorbing
LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) by Def9;
hence R is meet-absorbing by Th14; ::_thesis: verum
end;
end;
definition
let L be non empty \/-SemiLattRelStr ;
attrL is naturally_sup-generated means :Def10: :: ROBBINS3:def 10
for x, y being Element of L holds
( x <= y iff x |_| y = y );
end;
:: deftheorem Def10 defines naturally_sup-generated ROBBINS3:def_10_:_
for L being non empty \/-SemiLattRelStr holds
( L is naturally_sup-generated iff for x, y being Element of L holds
( x <= y iff x |_| y = y ) );
definition
let L be non empty /\-SemiLattRelStr ;
attrL is naturally_inf-generated means :Def11: :: ROBBINS3:def 11
for x, y being Element of L holds
( x <= y iff x |^| y = x );
end;
:: deftheorem Def11 defines naturally_inf-generated ROBBINS3:def_11_:_
for L being non empty /\-SemiLattRelStr holds
( L is naturally_inf-generated iff for x, y being Element of L holds
( x <= y iff x |^| y = x ) );
registration
let L be Lattice;
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like join-Associative meet-Associative meet-Absorbing naturally_sup-generated naturally_inf-generated for LatAugmentation of L;
existence
ex b1 being LatAugmentation of L st
( b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is Lattice-like )
proof
set R = LattRel L;
set S = LattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L) #);
LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of LattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L) #), the L_join of LattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L) #), the L_meet of LattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L) #) #) ;
then reconsider S = LattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L) #) as LatAugmentation of L by Def9;
for x, y being Element of S holds
( x <= y iff x |^| y = x )
proof
let x, y be Element of S; ::_thesis: ( x <= y iff x |^| y = x )
reconsider x9 = x, y9 = y as Element of L ;
hereby ::_thesis: ( x |^| y = x implies x <= y )
assume x <= y ; ::_thesis: x |^| y = x
then [x,y] in the InternalRel of S by ORDERS_2:def_5;
then x9 [= y9 by FILTER_1:31;
then x9 |^| y9 = x9 by LATTICES:4;
hence x |^| y = x ; ::_thesis: verum
end;
A1: x9 |^| y9 = x |^| y ;
assume x |^| y = x ; ::_thesis: x <= y
then x9 [= y9 by A1, LATTICES:4;
then [x9,y9] in LattRel L by FILTER_1:31;
hence x <= y by ORDERS_2:def_5; ::_thesis: verum
end;
then A2: S is naturally_inf-generated by Def11;
for x, y being Element of S holds
( x <= y iff x |_| y = y )
proof
let x, y be Element of S; ::_thesis: ( x <= y iff x |_| y = y )
reconsider x9 = x, y9 = y as Element of L ;
hereby ::_thesis: ( x |_| y = y implies x <= y )
assume x <= y ; ::_thesis: x |_| y = y
then [x,y] in the InternalRel of S by ORDERS_2:def_5;
then x9 [= y9 by FILTER_1:31;
then x9 |_| y9 = y9 by LATTICES:def_3;
hence x |_| y = y ; ::_thesis: verum
end;
A3: x9 |_| y9 = x |_| y ;
assume x |_| y = y ; ::_thesis: x <= y
then x9 [= y9 by A3, LATTICES:def_3;
then [x9,y9] in LattRel L by FILTER_1:31;
hence x <= y by ORDERS_2:def_5; ::_thesis: verum
end;
then S is naturally_sup-generated by Def10;
hence ex b1 being LatAugmentation of L st
( b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is Lattice-like ) by A2; ::_thesis: verum
end;
end;
registration
cluster1 -element reflexive for LattRelStr ;
existence
ex b1 being LattRelStr st
( b1 is 1 -element & b1 is reflexive )
proof
take TrivLattRelStr ; ::_thesis: ( TrivLattRelStr is 1 -element & TrivLattRelStr is reflexive )
thus ( TrivLattRelStr is 1 -element & TrivLattRelStr is reflexive ) ; ::_thesis: verum
end;
end;
registration
cluster1 -element reflexive for OrthoLattRelStr ;
existence
ex b1 being OrthoLattRelStr st
( b1 is 1 -element & b1 is reflexive )
proof
take TrivCLRelStr ; ::_thesis: ( TrivCLRelStr is 1 -element & TrivCLRelStr is reflexive )
thus ( TrivCLRelStr is 1 -element & TrivCLRelStr is reflexive ) ; ::_thesis: verum
end;
end;
registration
cluster1 -element reflexive for OrthoRelStr ;
existence
ex b1 being OrthoRelStr st
( b1 is 1 -element & b1 is reflexive )
proof
take TrivOrthoRelStr ; ::_thesis: ( TrivOrthoRelStr is 1 -element & TrivOrthoRelStr is reflexive )
thus ( TrivOrthoRelStr is 1 -element & TrivOrthoRelStr is reflexive ) ; ::_thesis: verum
end;
end;
registration
cluster1 -element -> 1 -element well-complemented de_Morgan involutive with_Top for OrthoLattStr ;
coherence
for b1 being 1 -element OrthoLattStr holds
( b1 is involutive & b1 is with_Top & b1 is de_Morgan & b1 is well-complemented )
proof
let L be 1 -element OrthoLattStr ; ::_thesis: ( L is involutive & L is with_Top & L is de_Morgan & L is well-complemented )
reconsider L9 = L as 1 -element OrthoLattStr ;
A1: for x being Element of L9 holds (x `) ` = x by STRUCT_0:def_10;
A2: for x being Element of L9 holds x ` is_a_complement_of x
proof
let x be Element of L9; ::_thesis: x ` is_a_complement_of x
A3: ( (x `) |_| x = Top L9 & (x `) |^| x = Bottom L9 ) by STRUCT_0:def_10;
( x |_| (x `) = Top L9 & x |^| (x `) = Bottom L9 ) by STRUCT_0:def_10;
hence x ` is_a_complement_of x by A3, LATTICES:def_18; ::_thesis: verum
end;
( ( for x, y being Element of L9 holds x |_| (x `) = y |_| (y `) ) & ( for x, y being Element of L9 holds x |^| y = ((x `) |_| (y `)) ` ) ) by STRUCT_0:def_10;
hence ( L is involutive & L is with_Top & L is de_Morgan & L is well-complemented ) by A1, A2, Def6, Def7, ROBBINS1:def_10, ROBBINS1:def_23; ::_thesis: verum
end;
end;
registration
cluster1 -element reflexive -> 1 -element reflexive PartialOrdered Pure OrderInvolutive for OrthoRelStr ;
coherence
for b1 being 1 -element reflexive OrthoRelStr holds
( b1 is OrderInvolutive & b1 is Pure & b1 is PartialOrdered )
proof
let L be 1 -element reflexive OrthoRelStr ; ::_thesis: ( L is OrderInvolutive & L is Pure & L is PartialOrdered )
reconsider L9 = L as 1 -element reflexive OrthoRelStr ;
reconsider f = the Compl of L9 as Function of L9,L9 ;
consider x being set such that
A1: the carrier of L9 = {x} by ZFMISC_1:131;
f = id {x} by A1, FUNCT_2:51;
then A2: f is V296() ;
then A3: L9 is Dneg by OPOSET_1:def_3;
for z, y being Element of L9 st z <= y holds
f . z >= f . y
proof
let z, y be Element of L9; ::_thesis: ( z <= y implies f . z >= f . y )
assume z <= y ; ::_thesis: f . z >= f . y
( f . z = x & f . y = x ) by A1, FUNCT_2:50;
hence f . z >= f . y by YELLOW_0:def_1; ::_thesis: verum
end;
then f is antitone by WAYBEL_9:def_1;
then f is Orderinvolutive by A2, OPOSET_1:def_17;
hence ( L is OrderInvolutive & L is Pure & L is PartialOrdered ) by A3, OPOSET_1:def_15, OPOSET_1:def_18; ::_thesis: verum
end;
end;
registration
cluster1 -element reflexive -> 1 -element reflexive naturally_sup-generated naturally_inf-generated for LattRelStr ;
coherence
for b1 being 1 -element reflexive LattRelStr holds
( b1 is naturally_sup-generated & b1 is naturally_inf-generated )
proof
let L be 1 -element reflexive LattRelStr ; ::_thesis: ( L is naturally_sup-generated & L is naturally_inf-generated )
reconsider L9 = L as 1 -element reflexive LattRelStr ;
( ( for x, y being Element of L9 holds
( x <= y iff x |_| y = y ) ) & ( for x, y being Element of L9 holds
( x <= y iff x |^| y = x ) ) ) by STRUCT_0:def_10;
hence ( L is naturally_sup-generated & L is naturally_inf-generated ) by Def10, Def11; ::_thesis: verum
end;
end;
registration
cluster non empty Lattice-like with_suprema with_infima de_Morgan PartialOrdered Pure OrderInvolutive naturally_sup-generated naturally_inf-generated for OrthoLattRelStr ;
existence
ex b1 being non empty OrthoLattRelStr st
( b1 is with_infima & b1 is with_suprema & b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is de_Morgan & b1 is Lattice-like & b1 is OrderInvolutive & b1 is Pure & b1 is PartialOrdered )
proof
take TrivCLRelStr ; ::_thesis: ( TrivCLRelStr is with_infima & TrivCLRelStr is with_suprema & TrivCLRelStr is naturally_sup-generated & TrivCLRelStr is naturally_inf-generated & TrivCLRelStr is de_Morgan & TrivCLRelStr is Lattice-like & TrivCLRelStr is OrderInvolutive & TrivCLRelStr is Pure & TrivCLRelStr is PartialOrdered )
thus ( TrivCLRelStr is with_infima & TrivCLRelStr is with_suprema & TrivCLRelStr is naturally_sup-generated & TrivCLRelStr is naturally_inf-generated & TrivCLRelStr is de_Morgan & TrivCLRelStr is Lattice-like & TrivCLRelStr is OrderInvolutive & TrivCLRelStr is Pure & TrivCLRelStr is PartialOrdered ) ; ::_thesis: verum
end;
end;
registration
cluster non empty Lattice-like with_suprema with_infima naturally_sup-generated naturally_inf-generated for LattRelStr ;
existence
ex b1 being non empty LattRelStr st
( b1 is with_infima & b1 is with_suprema & b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is Lattice-like )
proof
take TrivLattRelStr ; ::_thesis: ( TrivLattRelStr is with_infima & TrivLattRelStr is with_suprema & TrivLattRelStr is naturally_sup-generated & TrivLattRelStr is naturally_inf-generated & TrivLattRelStr is Lattice-like )
thus ( TrivLattRelStr is with_infima & TrivLattRelStr is with_suprema & TrivLattRelStr is naturally_sup-generated & TrivLattRelStr is naturally_inf-generated & TrivLattRelStr is Lattice-like ) ; ::_thesis: verum
end;
end;
theorem Th22: :: ROBBINS3:22
for L being non empty naturally_sup-generated LattRelStr
for x, y being Element of L holds
( x <= y iff x [= y )
proof
let L be non empty naturally_sup-generated LattRelStr ; ::_thesis: for x, y being Element of L holds
( x <= y iff x [= y )
let x, y be Element of L; ::_thesis: ( x <= y iff x [= y )
hereby ::_thesis: ( x [= y implies x <= y )
assume x <= y ; ::_thesis: x [= y
then x |_| y = y by Def10;
hence x [= y by LATTICES:def_3; ::_thesis: verum
end;
assume x [= y ; ::_thesis: x <= y
then x |_| y = y by LATTICES:def_3;
hence x <= y by Def10; ::_thesis: verum
end;
theorem Th23: :: ROBBINS3:23
for L being non empty Lattice-like naturally_sup-generated LattRelStr holds RelStr(# the carrier of L, the InternalRel of L #) = LattPOSet L
proof
let L be non empty Lattice-like naturally_sup-generated LattRelStr ; ::_thesis: RelStr(# the carrier of L, the InternalRel of L #) = LattPOSet L
A1: for x, y being set holds
( [x,y] in the InternalRel of L iff [x,y] in LattRel L )
proof
let x, y be set ; ::_thesis: ( [x,y] in the InternalRel of L iff [x,y] in LattRel L )
hereby ::_thesis: ( [x,y] in LattRel L implies [x,y] in the InternalRel of L )
assume A2: [x,y] in the InternalRel of L ; ::_thesis: [x,y] in LattRel L
then reconsider x9 = x, y9 = y as Element of L by ZFMISC_1:87;
x9 <= y9 by A2, ORDERS_2:def_5;
then x9 [= y9 by Th22;
hence [x,y] in LattRel L by FILTER_1:31; ::_thesis: verum
end;
assume A3: [x,y] in LattRel L ; ::_thesis: [x,y] in the InternalRel of L
then reconsider x9 = x, y9 = y as Element of L by ZFMISC_1:87;
x9 [= y9 by A3, FILTER_1:31;
then x9 <= y9 by Th22;
hence [x,y] in the InternalRel of L by ORDERS_2:def_5; ::_thesis: verum
end;
LattPOSet L = RelStr(# the carrier of L,(LattRel L) #) by LATTICE3:def_2;
hence RelStr(# the carrier of L, the InternalRel of L #) = LattPOSet L by A1, RELAT_1:def_2; ::_thesis: verum
end;
registration
cluster non empty Lattice-like naturally_sup-generated -> non empty with_suprema with_infima for LattRelStr ;
coherence
for b1 being non empty LattRelStr st b1 is naturally_sup-generated & b1 is Lattice-like holds
( b1 is with_infima & b1 is with_suprema )
proof
let L be non empty LattRelStr ; ::_thesis: ( L is naturally_sup-generated & L is Lattice-like implies ( L is with_infima & L is with_suprema ) )
assume ( L is naturally_sup-generated & L is Lattice-like ) ; ::_thesis: ( L is with_infima & L is with_suprema )
then reconsider L9 = L as non empty Lattice-like naturally_sup-generated LattRelStr ;
( LattPOSet L9 is with_suprema & LattPOSet L9 is with_infima ) ;
then ( RelStr(# the carrier of L9, the InternalRel of L9 #) is with_suprema & RelStr(# the carrier of L9, the InternalRel of L9 #) is with_infima ) by Th23;
hence ( L is with_infima & L is with_suprema ) by YELLOW_7:14, YELLOW_7:15; ::_thesis: verum
end;
end;
begin
definition
let R be OrthoLattStr ;
mode CLatAugmentation of R -> OrthoLattRelStr means :Def12: :: ROBBINS3:def 12
OrthoLattStr(# the carrier of it, the L_join of it, the L_meet of it, the Compl of it #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #);
existence
ex b1 being OrthoLattRelStr st OrthoLattStr(# the carrier of b1, the L_join of b1, the L_meet of b1, the Compl of b1 #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #)
proof
set IR = the Relation of the carrier of R;
set L = OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #);
take OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #) ; ::_thesis: OrthoLattStr(# the carrier of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the L_join of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the L_meet of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the Compl of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #) #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #)
thus OrthoLattStr(# the carrier of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the L_join of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the L_meet of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the Compl of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #) #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) ; ::_thesis: verum
end;
end;
:: deftheorem Def12 defines CLatAugmentation ROBBINS3:def_12_:_
for R being OrthoLattStr
for b2 being OrthoLattRelStr holds
( b2 is CLatAugmentation of R iff OrthoLattStr(# the carrier of b2, the L_join of b2, the L_meet of b2, the Compl of b2 #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) );
registration
let L be non empty OrthoLattStr ;
cluster -> non empty for CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds not b1 is empty
proof
let R be CLatAugmentation of L; ::_thesis: not R is empty
OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12;
hence not R is empty ; ::_thesis: verum
end;
end;
registration
let L be non empty meet-associative OrthoLattStr ;
cluster -> meet-associative for CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds b1 is meet-associative
proof
let R be CLatAugmentation of L; ::_thesis: R is meet-associative
OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12;
then LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) ;
hence R is meet-associative by Th12; ::_thesis: verum
end;
end;
registration
let L be non empty join-associative OrthoLattStr ;
cluster -> join-associative for CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds b1 is join-associative
proof
let R be CLatAugmentation of L; ::_thesis: R is join-associative
OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12;
then LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) ;
hence R is join-associative by Th11; ::_thesis: verum
end;
end;
registration
let L be non empty meet-commutative OrthoLattStr ;
cluster -> meet-commutative for CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds b1 is meet-commutative
proof
let R be CLatAugmentation of L; ::_thesis: R is meet-commutative
OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12;
then LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) ;
hence R is meet-commutative by Th10; ::_thesis: verum
end;
end;
registration
let L be non empty join-commutative OrthoLattStr ;
cluster -> join-commutative for CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds b1 is join-commutative
proof
let R be CLatAugmentation of L; ::_thesis: R is join-commutative
OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12;
then LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) ;
hence R is join-commutative by Th9; ::_thesis: verum
end;
end;
registration
let L be non empty meet-absorbing OrthoLattStr ;
cluster -> meet-absorbing for CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds b1 is meet-absorbing
proof
let R be CLatAugmentation of L; ::_thesis: R is meet-absorbing
OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12;
then LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) ;
hence R is meet-absorbing by Th14; ::_thesis: verum
end;
end;
registration
let L be non empty join-absorbing OrthoLattStr ;
cluster -> join-absorbing for CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds b1 is join-absorbing
proof
let R be CLatAugmentation of L; ::_thesis: R is join-absorbing
OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12;
then LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) ;
hence R is join-absorbing by Th13; ::_thesis: verum
end;
end;
registration
let L be non empty with_Top OrthoLattStr ;
cluster -> with_Top for CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds b1 is with_Top
proof
let R be CLatAugmentation of L; ::_thesis: R is with_Top
OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12;
then ComplLLattStr(# the carrier of L, the L_join of L, the Compl of L #) = ComplLLattStr(# the carrier of R, the L_join of R, the Compl of R #) ;
hence R is with_Top by Th19; ::_thesis: verum
end;
end;
registration
let L be Ortholattice;
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like join-Associative meet-Associative meet-Absorbing with_Top naturally_sup-generated naturally_inf-generated for CLatAugmentation of L;
existence
ex b1 being CLatAugmentation of L st
( b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is Lattice-like )
proof
set R = LattRel L;
set S = OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #);
OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #), the L_join of OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #), the L_meet of OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #), the Compl of OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #) #) ;
then reconsider S = OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #) as CLatAugmentation of L by Def12;
for x, y being Element of S holds
( x <= y iff x |^| y = x )
proof
let x, y be Element of S; ::_thesis: ( x <= y iff x |^| y = x )
reconsider x9 = x, y9 = y as Element of L ;
hereby ::_thesis: ( x |^| y = x implies x <= y )
assume x <= y ; ::_thesis: x |^| y = x
then [x9,y9] in the InternalRel of S by ORDERS_2:def_5;
then x9 [= y9 by FILTER_1:31;
then x9 |^| y9 = x9 by LATTICES:4;
hence x |^| y = x ; ::_thesis: verum
end;
A1: x9 |^| y9 = x |^| y ;
assume x |^| y = x ; ::_thesis: x <= y
then x9 [= y9 by A1, LATTICES:4;
then [x9,y9] in LattRel L by FILTER_1:31;
hence x <= y by ORDERS_2:def_5; ::_thesis: verum
end;
then A2: S is naturally_inf-generated by Def11;
for x, y being Element of S holds
( x <= y iff x |_| y = y )
proof
let x, y be Element of S; ::_thesis: ( x <= y iff x |_| y = y )
reconsider x9 = x, y9 = y as Element of L ;
hereby ::_thesis: ( x |_| y = y implies x <= y )
assume x <= y ; ::_thesis: x |_| y = y
then [x,y] in the InternalRel of S by ORDERS_2:def_5;
then x9 [= y9 by FILTER_1:31;
then x9 |_| y9 = y9 by LATTICES:def_3;
hence x |_| y = y ; ::_thesis: verum
end;
A3: x9 |_| y9 = x |_| y ;
assume x |_| y = y ; ::_thesis: x <= y
then x9 [= y9 by A3, LATTICES:def_3;
then [x9,y9] in LattRel L by FILTER_1:31;
hence x <= y by ORDERS_2:def_5; ::_thesis: verum
end;
then S is naturally_sup-generated by Def10;
hence ex b1 being CLatAugmentation of L st
( b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is Lattice-like ) by A2; ::_thesis: verum
end;
end;
registration
cluster non empty Lattice-like well-complemented de_Morgan involutive with_Top naturally_sup-generated for OrthoLattRelStr ;
existence
ex b1 being non empty OrthoLattRelStr st
( b1 is involutive & b1 is with_Top & b1 is de_Morgan & b1 is Lattice-like & b1 is naturally_sup-generated & b1 is well-complemented )
proof
take TrivCLRelStr ; ::_thesis: ( TrivCLRelStr is involutive & TrivCLRelStr is with_Top & TrivCLRelStr is de_Morgan & TrivCLRelStr is Lattice-like & TrivCLRelStr is naturally_sup-generated & TrivCLRelStr is well-complemented )
thus ( TrivCLRelStr is involutive & TrivCLRelStr is with_Top & TrivCLRelStr is de_Morgan & TrivCLRelStr is Lattice-like & TrivCLRelStr is naturally_sup-generated & TrivCLRelStr is well-complemented ) ; ::_thesis: verum
end;
end;
theorem Th24: :: ROBBINS3:24
for L being non empty with_suprema with_infima PartialOrdered OrthoRelStr
for x, y being Element of L st x <= y holds
( y = x "|_|" y & x = x "|^|" y )
proof
let L be non empty with_suprema with_infima PartialOrdered OrthoRelStr ; ::_thesis: for x, y being Element of L st x <= y holds
( y = x "|_|" y & x = x "|^|" y )
let a, b be Element of L; ::_thesis: ( a <= b implies ( b = a "|_|" b & a = a "|^|" b ) )
assume A1: a <= b ; ::_thesis: ( b = a "|_|" b & a = a "|^|" b )
then b = b "|_|" a by YELLOW_0:24;
hence ( b = a "|_|" b & a = a "|^|" b ) by A1, LATTICE3:13, YELLOW_0:25; ::_thesis: verum
end;
definition
let L be non empty meet-commutative /\-SemiLattStr ;
let a, b be Element of L;
:: original: |^|
redefine funca |^| b -> M2( the carrier of L);
commutativity
for a, b being Element of L holds a |^| b = b |^| a by LATTICES:def_6;
end;
definition
let L be non empty join-commutative \/-SemiLattStr ;
let a, b be Element of L;
:: original: |_|
redefine funca |_| b -> M2( the carrier of L);
commutativity
for a, b being Element of L holds a |_| b = b |_| a by LATTICES:def_4;
end;
registration
cluster non empty meet-commutative meet-absorbing join-absorbing naturally_sup-generated -> non empty reflexive for LattRelStr ;
coherence
for b1 being non empty LattRelStr st b1 is meet-absorbing & b1 is join-absorbing & b1 is meet-commutative & b1 is naturally_sup-generated holds
b1 is reflexive
proof
let L be non empty LattRelStr ; ::_thesis: ( L is meet-absorbing & L is join-absorbing & L is meet-commutative & L is naturally_sup-generated implies L is reflexive )
assume ( L is meet-absorbing & L is join-absorbing & L is meet-commutative & L is naturally_sup-generated ) ; ::_thesis: L is reflexive
then reconsider L9 = L as non empty meet-commutative meet-absorbing join-absorbing naturally_sup-generated LattRelStr ;
for x being Element of L9 holds x <= x
proof
let x be Element of L9; ::_thesis: x <= x
x [= x ;
hence x <= x by Th22; ::_thesis: verum
end;
hence L is reflexive by YELLOW_0:def_1; ::_thesis: verum
end;
end;
registration
cluster non empty join-associative naturally_sup-generated -> non empty transitive for LattRelStr ;
coherence
for b1 being non empty LattRelStr st b1 is join-associative & b1 is naturally_sup-generated holds
b1 is transitive
proof
let L be non empty LattRelStr ; ::_thesis: ( L is join-associative & L is naturally_sup-generated implies L is transitive )
assume ( L is join-associative & L is naturally_sup-generated ) ; ::_thesis: L is transitive
then reconsider L9 = L as non empty join-associative naturally_sup-generated LattRelStr ;
for x, y, z being Element of L9 st x <= y & y <= z holds
x <= z
proof
let x, y, z be Element of L9; ::_thesis: ( x <= y & y <= z implies x <= z )
assume ( x <= y & y <= z ) ; ::_thesis: x <= z
then ( x [= y & y [= z ) by Th22;
then x [= z by LATTICES:7;
hence x <= z by Th22; ::_thesis: verum
end;
hence L is transitive by YELLOW_0:def_2; ::_thesis: verum
end;
end;
registration
cluster non empty join-commutative naturally_sup-generated -> non empty antisymmetric for LattRelStr ;
coherence
for b1 being non empty LattRelStr st b1 is join-commutative & b1 is naturally_sup-generated holds
b1 is antisymmetric
proof
let L be non empty LattRelStr ; ::_thesis: ( L is join-commutative & L is naturally_sup-generated implies L is antisymmetric )
assume ( L is join-commutative & L is naturally_sup-generated ) ; ::_thesis: L is antisymmetric
then reconsider L9 = L as non empty join-commutative naturally_sup-generated LattRelStr ;
for x, y being Element of L9 st x <= y & y <= x holds
x = y
proof
let x, y be Element of L9; ::_thesis: ( x <= y & y <= x implies x = y )
assume ( x <= y & y <= x ) ; ::_thesis: x = y
then ( x [= y & y [= x ) by Th22;
hence x = y by LATTICES:8; ::_thesis: verum
end;
hence L is antisymmetric by YELLOW_0:def_3; ::_thesis: verum
end;
end;
theorem Th25: :: ROBBINS3:25
for L being non empty Lattice-like with_suprema with_infima naturally_sup-generated OrthoLattRelStr
for x, y being Element of L holds x "|_|" y = x |_| y
proof
let L be non empty Lattice-like with_suprema with_infima naturally_sup-generated OrthoLattRelStr ; ::_thesis: for x, y being Element of L holds x "|_|" y = x |_| y
let x, y be Element of L; ::_thesis: x "|_|" y = x |_| y
x <= x "|_|" y by YELLOW_0:22;
then A1: x [= x "|_|" y by Th22;
y <= x "|_|" y by YELLOW_0:22;
then A2: y [= x "|_|" y by Th22;
x [= x |_| y by LATTICES:5;
then A3: x <= x |_| y by Th22;
y [= x |_| y by LATTICES:5;
then A4: y <= x |_| y by Th22;
(x |_| y) "|_|" (x "|_|" y) = ((x |_| y) "|_|" x) "|_|" y by LATTICE3:14
.= (x |_| y) "|_|" y by A3, YELLOW_0:24
.= x |_| y by A4, YELLOW_0:24 ;
then x "|_|" y <= x |_| y by YELLOW_0:24;
then A5: x "|_|" y [= x |_| y by Th22;
(x "|_|" y) |_| (x |_| y) = ((x "|_|" y) |_| x) |_| y by LATTICES:def_5
.= (x "|_|" y) |_| y by A1, LATTICES:def_3
.= x "|_|" y by A2, LATTICES:def_3 ;
hence x "|_|" y = x |_| y by A5, LATTICES:def_3; ::_thesis: verum
end;
theorem Th26: :: ROBBINS3:26
for L being non empty Lattice-like with_suprema with_infima naturally_sup-generated OrthoLattRelStr
for x, y being Element of L holds x "|^|" y = x |^| y
proof
let L be non empty Lattice-like with_suprema with_infima naturally_sup-generated OrthoLattRelStr ; ::_thesis: for x, y being Element of L holds x "|^|" y = x |^| y
let x, y be Element of L; ::_thesis: x "|^|" y = x |^| y
x "|^|" y <= x by YELLOW_0:23;
then A1: x "|^|" y [= x by Th22;
x "|^|" y <= y by YELLOW_0:23;
then A2: x "|^|" y [= y by Th22;
x |^| y [= x by LATTICES:6;
then A3: x |^| y <= x by Th22;
x |^| y [= y by LATTICES:6;
then A4: x |^| y <= y by Th22;
(x |^| y) "|^|" (x "|^|" y) = ((x |^| y) "|^|" x) "|^|" y by LATTICE3:16
.= (x |^| y) "|^|" y by A3, YELLOW_0:25
.= x |^| y by A4, YELLOW_0:25 ;
then x |^| y <= x "|^|" y by YELLOW_0:25;
then A5: x |^| y [= x "|^|" y by Th22;
(x "|^|" y) |^| (x |^| y) = ((x "|^|" y) |^| x) |^| y by LATTICES:def_7
.= (x "|^|" y) |^| y by A1, LATTICES:4
.= x "|^|" y by A2, LATTICES:4 ;
hence x "|^|" y = x |^| y by A5, LATTICES:4; ::_thesis: verum
end;
theorem :: ROBBINS3:27
for L being non empty Lattice-like with_suprema with_infima PartialOrdered OrderInvolutive naturally_sup-generated naturally_inf-generated OrthoLattRelStr holds L is de_Morgan
proof
let L be non empty Lattice-like with_suprema with_infima PartialOrdered OrderInvolutive naturally_sup-generated naturally_inf-generated OrthoLattRelStr ; ::_thesis: L is de_Morgan
A1: for x, y being Element of L holds (x `) "|_|" (y `) <= (x "|^|" y) `
proof
let a, b be Element of L; ::_thesis: (a `) "|_|" (b `) <= (a "|^|" b) `
set i = a "|^|" b;
set s = (a `) "|_|" (b `);
a "|^|" b <= a by YELLOW_0:23;
then a ` <= (a "|^|" b) ` by Th7;
then A2: (a `) "|_|" (b `) <= ((a "|^|" b) `) "|_|" (b `) by WAYBEL_1:2;
a "|^|" b <= b by YELLOW_0:23;
then b ` <= (a "|^|" b) ` by Th7;
then (a "|^|" b) ` = (b `) "|_|" ((a "|^|" b) `) by Th24;
hence (a `) "|_|" (b `) <= (a "|^|" b) ` by A2, LATTICE3:13; ::_thesis: verum
end;
A3: for x, y being Element of L holds (x "|_|" y) ` <= (x `) "|^|" (y `)
proof
let a, b be Element of L; ::_thesis: (a "|_|" b) ` <= (a `) "|^|" (b `)
set i = (a `) "|^|" (b `);
set s = a "|_|" b;
a <= a "|_|" b by YELLOW_0:22;
then (a "|_|" b) ` <= a ` by Th7;
then A4: ((a "|_|" b) `) "|^|" (b `) <= (a `) "|^|" (b `) by WAYBEL_1:1;
b <= a "|_|" b by YELLOW_0:22;
then (a "|_|" b) ` <= b ` by Th7;
hence (a "|_|" b) ` <= (a `) "|^|" (b `) by A4, Th24; ::_thesis: verum
end;
for x, y being Element of L holds ((x `) |_| (y `)) ` = x |^| y
proof
let a, b be Element of L; ::_thesis: ((a `) |_| (b `)) ` = a |^| b
set s = (a `) "|_|" (b `);
set i = a "|^|" b;
( (a `) ` = a & (b `) ` = b ) by Th6;
then A5: ((a `) "|_|" (b `)) ` <= a "|^|" b by A3;
((a "|^|" b) `) ` <= ((a `) "|_|" (b `)) ` by A1, Th7;
then A6: a "|^|" b <= ((a `) "|_|" (b `)) ` by Th6;
( a "|^|" b = a |^| b & (a `) "|_|" (b `) = (a `) |_| (b `) ) by Th25, Th26;
hence ((a `) |_| (b `)) ` = a |^| b by A5, A6, ORDERS_2:2; ::_thesis: verum
end;
hence L is de_Morgan by ROBBINS1:def_23; ::_thesis: verum
end;
registration
let L be Ortholattice;
cluster -> involutive for CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds b1 is involutive
proof
let R be CLatAugmentation of L; ::_thesis: R is involutive
OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12;
hence R is involutive by Th21; ::_thesis: verum
end;
end;
registration
let L be Ortholattice;
cluster -> de_Morgan for CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds b1 is de_Morgan
proof
let R be CLatAugmentation of L; ::_thesis: R is de_Morgan
OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12;
hence R is de_Morgan by Th20; ::_thesis: verum
end;
end;
theorem Th28: :: ROBBINS3:28
for L being non empty OrthoLattRelStr st L is involutive & L is with_Top & L is de_Morgan & L is Lattice-like & L is naturally_sup-generated holds
( L is Orthocomplemented & L is PartialOrdered )
proof
let L be non empty OrthoLattRelStr ; ::_thesis: ( L is involutive & L is with_Top & L is de_Morgan & L is Lattice-like & L is naturally_sup-generated implies ( L is Orthocomplemented & L is PartialOrdered ) )
assume ( L is involutive & L is with_Top & L is de_Morgan & L is Lattice-like & L is naturally_sup-generated ) ; ::_thesis: ( L is Orthocomplemented & L is PartialOrdered )
then reconsider L9 = L as non empty Lattice-like de_Morgan involutive with_Top naturally_sup-generated OrthoLattRelStr ;
reconsider f = the Compl of L9 as Function of L9,L9 ;
for x, y being Element of L9 st x <= y holds
f . x >= f . y
proof
let x, y be Element of L9; ::_thesis: ( x <= y implies f . x >= f . y )
assume x <= y ; ::_thesis: f . x >= f . y
then x [= y by Th22;
then A1: x ` = (x |^| y) ` by LATTICES:4
.= (((x `) |_| (y `)) `) ` by ROBBINS1:def_23
.= (x `) |_| (y `) by Def6 ;
( f . x = x ` & f . y = y ` ) by ROBBINS1:def_3;
hence f . x >= f . y by A1, Def10; ::_thesis: verum
end;
then A2: f is antitone by WAYBEL_9:def_1;
A3: for y being Element of L9 holds
( ex_sup_of {y,(f . y)},L9 & ex_inf_of {y,(f . y)},L9 & "\/" ({y,(f . y)},L9) is_maximum_of the carrier of L9 & "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9 )
proof
set xx = "\/" ( the carrier of L9,L9);
let y be Element of L9; ::_thesis: ( ex_sup_of {y,(f . y)},L9 & ex_inf_of {y,(f . y)},L9 & "\/" ({y,(f . y)},L9) is_maximum_of the carrier of L9 & "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9 )
thus ex_sup_of {y,(f . y)},L9 by YELLOW_0:20; ::_thesis: ( ex_inf_of {y,(f . y)},L9 & "\/" ({y,(f . y)},L9) is_maximum_of the carrier of L9 & "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9 )
thus ex_inf_of {y,(f . y)},L9 by YELLOW_0:21; ::_thesis: ( "\/" ({y,(f . y)},L9) is_maximum_of the carrier of L9 & "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9 )
set t = y |_| (y `);
for b being Element of L9 st b in the carrier of L9 holds
b <= y |_| (y `)
proof
let b be Element of L9; ::_thesis: ( b in the carrier of L9 implies b <= y |_| (y `) )
assume b in the carrier of L9 ; ::_thesis: b <= y |_| (y `)
b |_| (y |_| (y `)) = b |_| (b |_| (b `)) by Def7
.= (b |_| b) |_| (b `) by LATTICES:def_5
.= b |_| (b `)
.= y |_| (y `) by Def7 ;
then b [= y |_| (y `) by LATTICES:def_3;
hence b <= y |_| (y `) by Th22; ::_thesis: verum
end;
then A4: y |_| (y `) is_>=_than the carrier of L9 by LATTICE3:def_9;
then L9 is upper-bounded by YELLOW_0:def_5;
then A5: ex_sup_of the carrier of L9,L9 by YELLOW_0:43;
reconsider t = y |_| (y `) as Element of L9 ;
A6: for a being Element of L9 st the carrier of L9 is_<=_than a holds
t <= a by LATTICE3:def_9;
"\/" ({y,(f . y)},L9) = "\/" ({y,(y `)},L9) by ROBBINS1:def_3
.= y "|_|" (y `) by YELLOW_0:41
.= y |_| (y `) by Th25
.= "\/" ( the carrier of L9,L9) by A4, A5, A6, YELLOW_0:def_9 ;
hence "\/" ({y,(f . y)},L9) is_maximum_of the carrier of L9 by A5, WAYBEL_1:def_7; ::_thesis: "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9
set xx = "/\" ( the carrier of L9,L9);
set t = y |^| (y `);
A7: for a, b being Element of L9 holds a |^| (a `) = b |^| (b `)
proof
let a, b be Element of L9; ::_thesis: a |^| (a `) = b |^| (b `)
a |^| (a `) = ((a `) |_| ((a `) `)) ` by ROBBINS1:def_23
.= ((b `) |_| ((b `) `)) ` by Def7
.= b |^| (b `) by ROBBINS1:def_23 ;
hence a |^| (a `) = b |^| (b `) ; ::_thesis: verum
end;
for b being Element of L9 st b in the carrier of L9 holds
b >= y |^| (y `)
proof
let b be Element of L9; ::_thesis: ( b in the carrier of L9 implies b >= y |^| (y `) )
assume b in the carrier of L9 ; ::_thesis: b >= y |^| (y `)
b |^| (y |^| (y `)) = b |^| (b |^| (b `)) by A7
.= (b |^| b) |^| (b `) by LATTICES:def_7
.= b |^| (b `)
.= y |^| (y `) by A7 ;
then y |^| (y `) [= b by LATTICES:4;
hence b >= y |^| (y `) by Th22; ::_thesis: verum
end;
then A8: y |^| (y `) is_<=_than the carrier of L9 by LATTICE3:def_8;
then L9 is lower-bounded by YELLOW_0:def_4;
then A9: ex_inf_of the carrier of L9,L9 by YELLOW_0:42;
reconsider t = y |^| (y `) as Element of L9 ;
A10: for a being Element of L9 st the carrier of L9 is_>=_than a holds
t >= a by LATTICE3:def_8;
"/\" ({y,(f . y)},L9) = "/\" ({y,(y `)},L9) by ROBBINS1:def_3
.= y "|^|" (y `) by YELLOW_0:40
.= y |^| (y `) by Th26
.= "/\" ( the carrier of L9,L9) by A8, A9, A10, YELLOW_0:def_10 ;
hence "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9 by A9, WAYBEL_1:def_6; ::_thesis: verum
end;
for x being Element of L9 holds f . (f . x) = x
proof
let x be Element of L9; ::_thesis: f . (f . x) = x
f . (f . x) = f . (x `) by ROBBINS1:def_3
.= (x `) ` by ROBBINS1:def_3
.= x by Def6 ;
hence f . (f . x) = x ; ::_thesis: verum
end;
then f is V296() by PARTIT_2:def_3;
then f is Orderinvolutive by A2, OPOSET_1:def_17;
then f OrthoComplement_on L9 by A3, OPOSET_1:def_21;
hence ( L is Orthocomplemented & L is PartialOrdered ) by OPOSET_1:def_22; ::_thesis: verum
end;
theorem :: ROBBINS3:29
for L being Ortholattice
for E being naturally_sup-generated CLatAugmentation of L holds E is Orthocomplemented by Th28;
registration
let L be Ortholattice;
cluster naturally_sup-generated -> Orthocomplemented naturally_sup-generated for CLatAugmentation of L;
coherence
for b1 being naturally_sup-generated CLatAugmentation of L holds b1 is Orthocomplemented by Th28;
end;
theorem Th30: :: ROBBINS3:30
for L being non empty OrthoLattStr st L is Boolean & L is well-complemented & L is Lattice-like holds
L is Ortholattice
proof
let L be non empty OrthoLattStr ; ::_thesis: ( L is Boolean & L is well-complemented & L is Lattice-like implies L is Ortholattice )
assume ( L is Boolean & L is well-complemented & L is Lattice-like ) ; ::_thesis: L is Ortholattice
then reconsider L9 = L as non empty Lattice-like Boolean well-complemented OrthoLattStr ;
A1: for x, y being Element of L9 holds x "/\" y = ((x `) "\/" (y `)) ` by ROBBINS1:33;
( ( for x being Element of L9 holds (x `) ` = x ) & ( for x, y being Element of L9 holds x |_| (x `) = y |_| (y `) ) ) by ROBBINS1:3, ROBBINS1:4;
hence L is Ortholattice by A1, Def6, Def7, ROBBINS1:def_23; ::_thesis: verum
end;
registration
cluster non empty Lattice-like Boolean well-complemented -> non empty de_Morgan involutive with_Top for OrthoLattStr ;
coherence
for b1 being non empty OrthoLattStr st b1 is Boolean & b1 is well-complemented & b1 is Lattice-like holds
( b1 is involutive & b1 is with_Top & b1 is de_Morgan ) by Th30;
end;