:: Basic Notions and Properties of Orthoposets
:: by Markus Moschner
::
:: Received February 11, 2003
:: Copyright (c) 2003 Association of Mizar Users
:: deftheorem defines {} OPOSET_1:def 1 :
:: deftheorem OPOSET_1:def 2 :
canceled;
theorem Th1: :: OPOSET_1:1
Lm1:
id {{} } = {[{} ,{} ]}
by SYSREL:30;
theorem :: OPOSET_1:2
canceled;
theorem Th3: :: OPOSET_1:3
theorem :: OPOSET_1:4
theorem :: OPOSET_1:5
canceled;
theorem Th6: :: OPOSET_1:6
theorem Th7: :: OPOSET_1:7
theorem Th8: :: OPOSET_1:8
theorem Th9: :: OPOSET_1:9
theorem Th10: :: OPOSET_1:10
theorem Th11: :: OPOSET_1:11
theorem Th12: :: OPOSET_1:12
theorem Th13: :: OPOSET_1:13
theorem Th14: :: OPOSET_1:14
theorem Th15: :: OPOSET_1:15
theorem Th16: :: OPOSET_1:16
theorem Th17: :: OPOSET_1:17
:: deftheorem Def3 defines dneg OPOSET_1:def 3 :
theorem :: OPOSET_1:18
canceled;
theorem Th19: :: OPOSET_1:19
theorem Th20: :: OPOSET_1:20
:: deftheorem Def4 defines TrivOrthoRelStr OPOSET_1:def 4 :
:: deftheorem defines TrivAsymOrthoRelStr OPOSET_1:def 5 :
:: deftheorem Def6 defines Dneg OPOSET_1:def 6 :
theorem :: OPOSET_1:21
:: deftheorem OPOSET_1:def 7 :
canceled;
:: deftheorem OPOSET_1:def 8 :
canceled;
:: deftheorem Def9 defines SubReFlexive OPOSET_1:def 9 :
theorem :: OPOSET_1:22
theorem Th23: :: OPOSET_1:23
:: deftheorem OPOSET_1:def 10 :
canceled;
:: deftheorem Def11 defines SubIrreFlexive OPOSET_1:def 11 :
:: deftheorem Def12 defines irreflexive OPOSET_1:def 12 :
theorem Th24: :: OPOSET_1:24
theorem Th25: :: OPOSET_1:25
:: deftheorem Def13 defines SubSymmetric OPOSET_1:def 13 :
theorem Th26: :: OPOSET_1:26
theorem Th27: :: OPOSET_1:27
:: deftheorem OPOSET_1:def 14 :
canceled;
:: deftheorem Def15 defines SubAntisymmetric OPOSET_1:def 15 :
theorem Th28: :: OPOSET_1:28
Lm3:
TrivOrthoRelStr is antisymmetric
;
:: deftheorem OPOSET_1:def 16 :
canceled;
:: deftheorem OPOSET_1:def 17 :
canceled;
:: deftheorem Def18 defines Asymmetric OPOSET_1:def 18 :
theorem :: OPOSET_1:29
canceled;
theorem Th30: :: OPOSET_1:30
theorem Th31: :: OPOSET_1:31
:: deftheorem Def19 defines SubTransitive OPOSET_1:def 19 :
theorem Th32: :: OPOSET_1:32
theorem :: OPOSET_1:33
canceled;
theorem Th34: :: OPOSET_1:34
theorem :: OPOSET_1:35
theorem :: OPOSET_1:36
theorem Th37: :: OPOSET_1:37
theorem Th38: :: OPOSET_1:38
theorem Th39: :: OPOSET_1:39
theorem Th40: :: OPOSET_1:40
theorem Th41: :: OPOSET_1:41
theorem Th42: :: OPOSET_1:42
:: deftheorem OPOSET_1:def 20 :
canceled;
:: deftheorem Def21 defines SubQuasiOrdered OPOSET_1:def 21 :
:: deftheorem Def22 defines QuasiOrdered OPOSET_1:def 22 :
theorem Th43: :: OPOSET_1:43
:: deftheorem Def23 defines QuasiPure OPOSET_1:def 23 :
:: deftheorem Def24 defines SubPartialOrdered OPOSET_1:def 24 :
:: deftheorem Def25 defines PartialOrdered OPOSET_1:def 25 :
theorem Th44: :: OPOSET_1:44
:: deftheorem Def26 defines Pure OPOSET_1:def 26 :
:: deftheorem Def27 defines SubStrictPartialOrdered OPOSET_1:def 27 :
:: deftheorem Def28 defines StrictPartialOrdered OPOSET_1:def 28 :
theorem Th45: :: OPOSET_1:45
theorem Th46: :: OPOSET_1:46
theorem Th47: :: OPOSET_1:47
theorem Th48: :: OPOSET_1:48
theorem :: OPOSET_1:49
:: deftheorem OPOSET_1:def 29 :
canceled;
:: deftheorem OPOSET_1:def 30 :
canceled;
:: deftheorem OPOSET_1:def 31 :
canceled;
:: deftheorem Def32 defines Orderinvolutive OPOSET_1:def 32 :
:: deftheorem Def33 defines OrderInvolutive OPOSET_1:def 33 :
theorem :: OPOSET_1:50
canceled;
theorem Th51: :: OPOSET_1:51
:: deftheorem Def34 defines QuasiOrthoComplement_on OPOSET_1:def 34 :
:: deftheorem Def35 defines QuasiOrthocomplemented OPOSET_1:def 35 :
theorem Th52: :: OPOSET_1:52
:: deftheorem Def36 defines OrthoComplement_on OPOSET_1:def 36 :
:: deftheorem Def37 defines Orthocomplemented OPOSET_1:def 37 :
theorem :: OPOSET_1:53
theorem Th54: :: OPOSET_1:54