:: Basic Notions and Properties of Orthoposets
:: by Markus Moschner
::
:: Copyright (c) 2003-2019 Association of Mizar Users

:: Some basic definitions and theorems for later examples;
theorem :: OPOSET_1:1
for L being non empty reflexive antisymmetric RelStr
for x, y being Element of L st x <= y holds
( sup {x,y} = y & inf {x,y} = x )
proof end;

:: for various types of relations needed for Posets
:: Some existence conditions on non-empty relations
registration
let X be set ;
cluster Relation-like irreflexive asymmetric transitive for Element of K19(([#] (X,X)));
existence
ex b1 being Relation of X st
( b1 is irreflexive & b1 is asymmetric & b1 is transitive )
proof end;
end;

registration
let X be non empty set ;
let R be Relation of X;
let C be UnOp of X;
cluster OrthoRelStr(# X,R,C #) -> non empty ;
coherence
not OrthoRelStr(# X,R,C #) is empty
;
end;

registration
existence
ex b1 being OrthoRelStr st
( not b1 is empty & b1 is strict )
proof end;
end;

:: Double negation property of the internal Complement
registration
let O be set ;
cluster Relation-like Function-like V14(O) V18(O,O) involutive for Element of K19(([#] (O,O)));
existence
ex b1 being Function of O,O st b1 is involutive
proof end;
end;

:: Small example structures
definition
func TrivOrthoRelStr -> strict OrthoRelStr equals :Def1: :: OPOSET_1:def 1
OrthoRelStr(# ,(),op1 #);
coherence
OrthoRelStr(# ,(),op1 #) is strict OrthoRelStr
;
end;

:: deftheorem Def1 defines TrivOrthoRelStr OPOSET_1:def 1 :
TrivOrthoRelStr = OrthoRelStr(# ,(),op1 #);

notation end;

registration
coherence ;
end;

definition
func TrivAsymOrthoRelStr -> strict OrthoRelStr equals :: OPOSET_1:def 2
OrthoRelStr(# ,({} (,)),op1 #);
coherence
OrthoRelStr(# ,({} (,)),op1 #) is strict OrthoRelStr
;
end;

:: deftheorem defines TrivAsymOrthoRelStr OPOSET_1:def 2 :
TrivAsymOrthoRelStr = OrthoRelStr(# ,({} (,)),op1 #);

registration
coherence ;
end;

definition
let O be non empty OrthoRelStr ;
attr O is Dneg means :: OPOSET_1:def 3
ex f being Function of O,O st
( f = the Compl of O & f is V256() );
end;

:: deftheorem defines Dneg OPOSET_1:def 3 :
for O being non empty OrthoRelStr holds
( O is Dneg iff ex f being Function of O,O st
( f = the Compl of O & f is V256() ) );

registration
coherence ;
end;

registration
cluster non empty Dneg for OrthoRelStr ;
existence
ex b1 being non empty OrthoRelStr st b1 is Dneg
by Def1;
end;

:: InternalRel based properties
definition
let O be non empty RelStr ;
attr O is SubReFlexive means :Def4: :: OPOSET_1:def 4
the InternalRel of O is reflexive ;
end;

:: deftheorem Def4 defines SubReFlexive OPOSET_1:def 4 :
for O being non empty RelStr holds
( O is SubReFlexive iff the InternalRel of O is reflexive );

theorem :: OPOSET_1:2
for O being non empty RelStr st O is reflexive holds
O is SubReFlexive by PARTIT_2:21;

theorem Th3: :: OPOSET_1:3
proof end;

registration
coherence by Th3;
end;

registration
existence
ex b1 being non empty OrthoRelStr st
( b1 is reflexive & b1 is strict )
by Th3;
end;

definition
let O be non empty RelStr ;
redefine attr O is irreflexive means :: OPOSET_1:def 5
the InternalRel of O is irreflexive ;
compatibility
( O is irreflexive iff the InternalRel of O is irreflexive )
proof end;
redefine attr O is irreflexive means :: OPOSET_1:def 6
the InternalRel of O is_irreflexive_in the carrier of O;
compatibility
( O is irreflexive iff the InternalRel of O is_irreflexive_in the carrier of O )
;
end;

:: deftheorem defines irreflexive OPOSET_1:def 5 :
for O being non empty RelStr holds
( O is irreflexive iff the InternalRel of O is irreflexive );

:: deftheorem defines irreflexive OPOSET_1:def 6 :
for O being non empty RelStr holds
( O is irreflexive iff the InternalRel of O is_irreflexive_in the carrier of O );

theorem Th4: :: OPOSET_1:4

registration
coherence ;
end;

registration
existence
ex b1 being non empty OrthoRelStr st
( b1 is irreflexive & b1 is strict )
by Th4;
end;

:: Symmetry
definition
let O be non empty RelStr ;
redefine attr O is symmetric means :: OPOSET_1:def 7
the InternalRel of O is symmetric Relation of the carrier of O;
compatibility
( O is symmetric iff the InternalRel of O is symmetric Relation of the carrier of O )
by ;
end;

:: deftheorem defines symmetric OPOSET_1:def 7 :
for O being non empty RelStr holds
( O is symmetric iff the InternalRel of O is symmetric Relation of the carrier of O );

theorem Th5: :: OPOSET_1:5

registration
existence
ex b1 being non empty OrthoRelStr st
( b1 is symmetric & b1 is strict )
by Th5;
end;

:: Antisymmetry
definition
let O be non empty RelStr ;
redefine attr O is antisymmetric means :: OPOSET_1:def 8
the InternalRel of O is antisymmetric Relation of the carrier of O;
compatibility
( O is antisymmetric iff the InternalRel of O is antisymmetric Relation of the carrier of O )
by ;
end;

:: deftheorem defines antisymmetric OPOSET_1:def 8 :
for O being non empty RelStr holds
( O is antisymmetric iff the InternalRel of O is antisymmetric Relation of the carrier of O );

Lm1:
;

registration
coherence ;
end;

registration
existence
ex b1 being non empty OrthoRelStr st
( b1 is symmetric & b1 is antisymmetric & b1 is strict )
by Lm1;
end;

:: Asymmetry
definition
let O be non empty RelStr ;
redefine attr O is asymmetric means :: OPOSET_1:def 9
the InternalRel of O is_asymmetric_in the carrier of O;
compatibility
( O is asymmetric iff the InternalRel of O is_asymmetric_in the carrier of O )
by ;
end;

:: deftheorem defines asymmetric OPOSET_1:def 9 :
for O being non empty RelStr holds
( O is asymmetric iff the InternalRel of O is_asymmetric_in the carrier of O );

theorem Th6: :: OPOSET_1:6

registration
coherence ;
end;

registration
existence
ex b1 being non empty OrthoRelStr st
( b1 is asymmetric & b1 is strict )
by Th6;
end;

:: Transitivity
definition
let O be non empty RelStr ;
redefine attr O is transitive means :: OPOSET_1:def 10
the InternalRel of O is transitive Relation of the carrier of O;
compatibility
( O is transitive iff the InternalRel of O is transitive Relation of the carrier of O )
by ;
end;

:: deftheorem defines transitive OPOSET_1:def 10 :
for O being non empty RelStr holds
( O is transitive iff the InternalRel of O is transitive Relation of the carrier of O );

registration
existence
ex b1 being non empty OrthoRelStr st
( b1 is reflexive & b1 is symmetric & b1 is antisymmetric & b1 is transitive & b1 is strict )
by Lm1;
end;

theorem :: OPOSET_1:7

registration
coherence ;
end;

registration
existence
ex b1 being non empty OrthoRelStr st
( b1 is irreflexive & b1 is asymmetric & b1 is transitive & b1 is strict )
by Th4;
end;

theorem :: OPOSET_1:8
for O being non empty RelStr st O is symmetric & O is transitive holds
O is SubReFlexive ;

theorem :: OPOSET_1:9
for O being non empty RelStr st O is irreflexive & O is transitive holds
O is asymmetric ;

theorem :: OPOSET_1:10
for O being non empty RelStr st O is asymmetric holds
O is irreflexive ;

:: Quasiorder (Preorder)
definition
let O be non empty RelStr ;
attr O is SubQuasiOrdered means :: OPOSET_1:def 11
( O is SubReFlexive & O is transitive );
end;

:: deftheorem defines SubQuasiOrdered OPOSET_1:def 11 :
for O being non empty RelStr holds
( O is SubQuasiOrdered iff ( O is SubReFlexive & O is transitive ) );

notation
let O be non empty RelStr ;
synonym SubPreOrdered O for SubQuasiOrdered ;
end;

definition
let O be non empty RelStr ;
attr O is QuasiOrdered means :Def12: :: OPOSET_1:def 12
( O is reflexive & O is transitive );
end;

:: deftheorem Def12 defines QuasiOrdered OPOSET_1:def 12 :
for O being non empty RelStr holds
( O is QuasiOrdered iff ( O is reflexive & O is transitive ) );

notation
let O be non empty RelStr ;
synonym PreOrdered O for QuasiOrdered ;
end;

theorem Th11: :: OPOSET_1:11
for O being non empty RelStr st O is QuasiOrdered holds
O is SubQuasiOrdered
proof end;

registration
correctness
coherence
for b1 being non empty OrthoRelStr st b1 is QuasiOrdered holds
b1 is SubQuasiOrdered
;
by Th11;
end;

registration
coherence ;
end;

:: QuasiPure means complementation-order-like combination of properties
definition
let O be non empty OrthoRelStr ;
attr O is QuasiPure means :: OPOSET_1:def 13
( O is Dneg & O is QuasiOrdered );
end;

:: deftheorem defines QuasiPure OPOSET_1:def 13 :
for O being non empty OrthoRelStr holds
( O is QuasiPure iff ( O is Dneg & O is QuasiOrdered ) );

registration
existence
ex b1 being non empty OrthoRelStr st
( b1 is QuasiPure & b1 is Dneg & b1 is QuasiOrdered & b1 is strict )
proof end;
end;

registration
coherence ;
end;

definition end;

:: Partial Order ---> Poset
definition
let O be non empty OrthoRelStr ;
attr O is PartialOrdered means :: OPOSET_1:def 14
( O is reflexive & O is antisymmetric & O is transitive );
end;

:: deftheorem defines PartialOrdered OPOSET_1:def 14 :
for O being non empty OrthoRelStr holds
( O is PartialOrdered iff ( O is reflexive & O is antisymmetric & O is transitive ) );

registration
coherence
for b1 being non empty OrthoRelStr st b1 is PartialOrdered holds
( b1 is reflexive & b1 is antisymmetric & b1 is transitive )
;
coherence
for b1 being non empty OrthoRelStr st b1 is reflexive & b1 is antisymmetric & b1 is transitive holds
b1 is PartialOrdered
;
end;

:: Pureness for partial orders
definition
let O be non empty OrthoRelStr ;
attr O is Pure means :: OPOSET_1:def 15
( O is Dneg & O is PartialOrdered );
end;

:: deftheorem defines Pure OPOSET_1:def 15 :
for O being non empty OrthoRelStr holds
( O is Pure iff ( O is Dneg & O is PartialOrdered ) );

registration
existence
ex b1 being non empty OrthoRelStr st
( b1 is Pure & b1 is Dneg & b1 is PartialOrdered & b1 is strict )
proof end;
end;

registration
coherence ;
end;

definition end;

:: Strict Poset
definition
let O be non empty OrthoRelStr ;
attr O is StrictPartialOrdered means :: OPOSET_1:def 16
( O is asymmetric & O is transitive );
end;

:: deftheorem defines StrictPartialOrdered OPOSET_1:def 16 :
for O being non empty OrthoRelStr holds
( O is StrictPartialOrdered iff ( O is asymmetric & O is transitive ) );

notation
let O be non empty OrthoRelStr ;
synonym StrictOrdered O for StrictPartialOrdered ;
end;

theorem Th12: :: OPOSET_1:12
for O being non empty OrthoRelStr st O is StrictPartialOrdered holds
O is irreflexive
proof end;

registration
coherence
for b1 being non empty OrthoRelStr st b1 is StrictPartialOrdered holds
b1 is irreflexive
by Th12;
end;

registration
coherence
for b1 being non empty OrthoRelStr st b1 is StrictPartialOrdered holds
b1 is irreflexive
;
end;

registration
coherence ;
end;

registration
existence
ex b1 being non empty strict OrthoRelStr st
( b1 is irreflexive & b1 is StrictPartialOrdered )
proof end;
end;

theorem :: OPOSET_1:13
for QO being non empty QuasiOrdered OrthoRelStr st QO is antisymmetric holds
QO is PartialOrdered by Def12;

registration
correctness
coherence
for b1 being non empty OrthoRelStr st b1 is PartialOrdered holds
( b1 is reflexive & b1 is transitive & b1 is antisymmetric )
;
;
end;

definition
let PO be non empty RelStr ;
let f be UnOp of the carrier of PO;
attr f is Orderinvolutive means :: OPOSET_1:def 17
( f is V256() & f is antitone );
end;

:: deftheorem defines Orderinvolutive OPOSET_1:def 17 :
for PO being non empty RelStr
for f being UnOp of the carrier of PO holds
( f is Orderinvolutive iff ( f is V256() & f is antitone ) );

definition
let PO be non empty OrthoRelStr ;
attr PO is OrderInvolutive means :: OPOSET_1:def 18
the Compl of PO is Orderinvolutive ;
end;

:: deftheorem defines OrderInvolutive OPOSET_1:def 18 :
for PO being non empty OrthoRelStr holds
( PO is OrderInvolutive iff the Compl of PO is Orderinvolutive );

theorem Th14: :: OPOSET_1:14
proof end;

registration
coherence by Th14;
end;

registration
existence
ex b1 being non empty OrthoRelStr st
( b1 is OrderInvolutive & b1 is Pure & b1 is PartialOrdered )
proof end;
end;

definition end;

definition
let PO be non empty RelStr ;
let f be UnOp of the carrier of PO;
pred f QuasiOrthoComplement_on PO means :: OPOSET_1:def 19
( f is Orderinvolutive & ( for y being Element of PO holds
( ex_sup_of {y,(f . y)},PO & ex_inf_of {y,(f . y)},PO ) ) );
end;

:: deftheorem defines QuasiOrthoComplement_on OPOSET_1:def 19 :
for PO being non empty RelStr
for f being UnOp of the carrier of PO holds
( f QuasiOrthoComplement_on PO iff ( f is Orderinvolutive & ( for y being Element of PO holds
( ex_sup_of {y,(f . y)},PO & ex_inf_of {y,(f . y)},PO ) ) ) );

definition
let PO be non empty OrthoRelStr ;
attr PO is QuasiOrthocomplemented means :: OPOSET_1:def 20
ex f being Function of PO,PO st
( f = the Compl of PO & f QuasiOrthoComplement_on PO );
end;

:: deftheorem defines QuasiOrthocomplemented OPOSET_1:def 20 :
for PO being non empty OrthoRelStr holds
( PO is QuasiOrthocomplemented iff ex f being Function of PO,PO st
( f = the Compl of PO & f QuasiOrthoComplement_on PO ) );

Lm2:
by SYSREL:13;

theorem Th15: :: OPOSET_1:15
proof end;

definition
let PO be non empty RelStr ;
let f be UnOp of the carrier of PO;
pred f OrthoComplement_on PO means :: OPOSET_1:def 21
( f is Orderinvolutive & ( for y being Element of PO holds
( ex_sup_of {y,(f . y)},PO & ex_inf_of {y,(f . y)},PO & "\/" ({y,(f . y)},PO) is_maximum_of the carrier of PO & "/\" ({y,(f . y)},PO) is_minimum_of the carrier of PO ) ) );
end;

:: deftheorem defines OrthoComplement_on OPOSET_1:def 21 :
for PO being non empty RelStr
for f being UnOp of the carrier of PO holds
( f OrthoComplement_on PO iff ( f is Orderinvolutive & ( for y being Element of PO holds
( ex_sup_of {y,(f . y)},PO & ex_inf_of {y,(f . y)},PO & "\/" ({y,(f . y)},PO) is_maximum_of the carrier of PO & "/\" ({y,(f . y)},PO) is_minimum_of the carrier of PO ) ) ) );

definition
let PO be non empty OrthoRelStr ;
attr PO is Orthocomplemented means :: OPOSET_1:def 22
ex f being Function of PO,PO st
( f = the Compl of PO & f OrthoComplement_on PO );
end;

:: deftheorem defines Orthocomplemented OPOSET_1:def 22 :
for PO being non empty OrthoRelStr holds
( PO is Orthocomplemented iff ex f being Function of PO,PO st
( f = the Compl of PO & f OrthoComplement_on PO ) );

theorem :: OPOSET_1:16
for PO being non empty OrthoRelStr
for f being UnOp of the carrier of PO st f OrthoComplement_on PO holds
f QuasiOrthoComplement_on PO ;

:: PartialOrdered (non empty OrthoRelStr)
theorem Th17: :: OPOSET_1:17
proof end;

registration
coherence by ;
end;

registration
correctness
existence
ex b1 being non empty OrthoRelStr st
( b1 is Orthocomplemented & b1 is QuasiOrthocomplemented & b1 is PartialOrdered )
;
proof end;
end;

definition end;