:: ROBBINS3 semantic presentation
:: deftheorem Def1 defines join-Associative ROBBINS3:def 1 :
:: deftheorem Def2 defines meet-Associative ROBBINS3:def 2 :
:: deftheorem Def3 defines meet-Absorbing ROBBINS3:def 3 :
theorem Th1: :: ROBBINS3:1
theorem Th2: :: ROBBINS3:2
theorem Th3: :: ROBBINS3:3
theorem Th4: :: ROBBINS3:4
theorem Th5: :: ROBBINS3:5
theorem Th6: :: ROBBINS3:6
theorem Th7: :: ROBBINS3:7
:: deftheorem Def4 defines TrivLattRelStr ROBBINS3:def 4 :
theorem Th8: :: ROBBINS3:8
Lemma11:
TrivLattRelStr is Lattice-like
;
:: deftheorem Def5 defines TrivCLRelStr ROBBINS3:def 5 :
:: deftheorem Def6 defines involutive ROBBINS3:def 6 :
:: deftheorem Def7 defines with_Top ROBBINS3:def 7 :
theorem Th9: :: ROBBINS3:9
theorem Th10: :: ROBBINS3:10
theorem Th11: :: ROBBINS3:11
theorem Th12: :: ROBBINS3:12
theorem Th13: :: ROBBINS3:13
theorem Th14: :: ROBBINS3:14
theorem Th15: :: ROBBINS3:15
theorem Th16: :: ROBBINS3:16
theorem Th17: :: ROBBINS3:17
theorem Th18: :: ROBBINS3:18
theorem Th19: :: ROBBINS3:19
theorem Th20: :: ROBBINS3:20
theorem Th21: :: ROBBINS3:21
:: deftheorem Def8 defines RelAugmentation ROBBINS3:def 8 :
:: deftheorem Def9 defines LatAugmentation ROBBINS3:def 9 :
:: deftheorem Def10 defines naturally_sup-generated ROBBINS3:def 10 :
:: deftheorem Def11 defines naturally_inf-generated ROBBINS3:def 11 :
theorem Th22: :: ROBBINS3:22
theorem Th23: :: ROBBINS3:23
definition
let c1 be
OrthoLattStr ;
mode CLatAugmentation of
c1 -> OrthoLattRelStr means :
Def12:
:: ROBBINS3:def 12
OrthoLattStr(# the
carrier of
a2,the
L_join of
a2,the
L_meet of
a2,the
Compl of
a2 #)
= OrthoLattStr(# the
carrier of
a1,the
L_join of
a1,the
L_meet of
a1,the
Compl of
a1 #);
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 c1,the L_join of c1,the L_meet of c1,the Compl of c1 #)
end;
:: deftheorem Def12 defines CLatAugmentation ROBBINS3:def 12 :
theorem Th24: :: ROBBINS3:24
theorem Th25: :: ROBBINS3:25
theorem Th26: :: ROBBINS3:26
theorem Th27: :: ROBBINS3:27
theorem Th28: :: ROBBINS3:28
theorem Th29: :: ROBBINS3:29
theorem Th30: :: ROBBINS3:30