:: Orthomodular Lattices
:: by El\.zbieta M\c{a}dra and Adam Grabowski
::
:: Received June 27, 2008
:: Copyright (c) 2008 Association of Mizar Users
theorem Strict: :: ROBBINS4:1
theorem yy: :: ROBBINS4:2
theorem 3ort: :: ROBBINS4:3
theorem theo: :: ROBBINS4:4
:: deftheorem DefModular defines orthomodular ROBBINS4:def 1 :
theorem twMod: :: ROBBINS4:5
theorem tw1: :: ROBBINS4:6
:: deftheorem DefMod3 defines Orthomodular ROBBINS4:def 2 :
definition
func B_6 -> RelStr equals :: ROBBINS4:def 3
InclPoset {0 ,1,(3 \ 1),2,(3 \ 2),3};
coherence
InclPoset {0 ,1,(3 \ 1),2,(3 \ 2),3} is RelStr
;
end;
:: deftheorem defines B_6 ROBBINS4:def 3 :
L1:
3 \ 2 misses 2
by XBOOLE_1:79;
L2:
1 c= 2
by NAT_1:40;
then Lem1:
3 \ 2 misses 1
by L1, XBOOLE_1:63;
theorem LemBA: :: ROBBINS4:7
theorem CosikX1: :: ROBBINS4:8
:: deftheorem BenDef defines Benzene ROBBINS4:def 4 :
theorem LemBen: :: ROBBINS4:9
theorem LemBen2: :: ROBBINS4:10
theorem CosikX: :: ROBBINS4:11
theorem Strict2: :: ROBBINS4:12
theorem HiHi: :: ROBBINS4:13
theorem Ha0: :: ROBBINS4:14
theorem Ha1: :: ROBBINS4:15
theorem Ha11: :: ROBBINS4:16
theorem Hax: :: ROBBINS4:17
theorem Hax2: :: ROBBINS4:18
theorem Haczyk1: :: ROBBINS4:19
theorem :: ROBBINS4:20
theorem Haczyk3: :: ROBBINS4:21
theorem Haczyk4: :: ROBBINS4:22
theorem twU: :: ROBBINS4:23
for
a being
Element of
Benzene holds
( (
a = 0 implies
a ` = 3 ) & (
a = 3 implies
a ` = 0 ) & (
a = 1 implies
a ` = 3
\ 1 ) & (
a = 3
\ 1 implies
a ` = 1 ) & (
a = 2 implies
a ` = 3
\ 2 ) & (
a = 3
\ 2 implies
a ` = 2 ) )
theorem Inkl: :: ROBBINS4:24
theorem KL1: :: ROBBINS4:25
theorem Bot2: :: ROBBINS4:26
theorem Bot1: :: ROBBINS4:27
theorem :: ROBBINS4:28
theorem Stan0: :: ROBBINS4:29
:: deftheorem orthogonal defines are_orthogonal ROBBINS4:def 5 :
theorem :: ROBBINS4:30
theorem :: ROBBINS4:31
theorem :: ROBBINS4:32
theorem :: ROBBINS4:33
theorem twDual: :: ROBBINS4:34
theorem :: ROBBINS4:35
theorem dziw: :: ROBBINS4:36
theorem :: ROBBINS4:37
theorem :: ROBBINS4:38
theorem :: ROBBINS4:39