:: Formalization of Ortholattices via Orthoposets
:: by Adam Grabowski and Markus Moschner
::
:: Received December 28, 2004
:: Copyright (c) 2004 Association of Mizar Users
:: 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 defines TrivLattRelStr ROBBINS3:def 4 :
theorem :: ROBBINS3:8
Lm1:
TrivLattRelStr is Lattice-like
;
:: deftheorem 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 :: ROBBINS3:15
theorem :: ROBBINS3:16
theorem :: ROBBINS3:17
theorem Th18: :: ROBBINS3:18
theorem Th19: :: ROBBINS3:19
theorem Th20: :: ROBBINS3:20
theorem Th21: :: ROBBINS3:21
:: deftheorem 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 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 #)
end;
:: deftheorem Def12 defines CLatAugmentation ROBBINS3:def 12 :
theorem Th24: :: ROBBINS3:24
theorem Th25: :: ROBBINS3:25
theorem Th26: :: ROBBINS3:26
theorem :: ROBBINS3:27
theorem Th28: :: ROBBINS3:28
theorem :: ROBBINS3:29
theorem Th30: :: ROBBINS3:30