:: by Markus Moschner

::

:: Received February 11, 2003

:: Copyright (c) 2003-2017 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 )

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

:: Some existence conditions on non-empty relations

registration

let X be set ;

existence

ex b_{1} being Relation of X st

( b_{1} is irreflexive & b_{1} is asymmetric & b_{1} is transitive )

end;
existence

ex b

( b

proof end;

registration

let X be non empty set ;

let R be Relation of X;

let C be UnOp of X;

coherence

not OrthoRelStr(# X,R,C #) is empty ;

end;
let R be Relation of X;

let C be UnOp of X;

coherence

not OrthoRelStr(# X,R,C #) is empty ;

registration
end;

:: Double negation property of the internal Complement

registration
end;

:: Small example structures

definition

OrthoRelStr(# {0},(id {0}),op1 #) is strict OrthoRelStr ;

end;

func TrivOrthoRelStr -> strict OrthoRelStr equals :Def1: :: OPOSET_1:def 1

OrthoRelStr(# {0},(id {0}),op1 #);

coherence OrthoRelStr(# {0},(id {0}),op1 #);

OrthoRelStr(# {0},(id {0}),op1 #) is strict OrthoRelStr ;

:: deftheorem Def1 defines TrivOrthoRelStr OPOSET_1:def 1 :

TrivOrthoRelStr = OrthoRelStr(# {0},(id {0}),op1 #);

TrivOrthoRelStr = OrthoRelStr(# {0},(id {0}),op1 #);

registration
end;

definition

OrthoRelStr(# {0},({} ({0},{0})),op1 #) is strict OrthoRelStr ;

end;

func TrivAsymOrthoRelStr -> strict OrthoRelStr equals :: OPOSET_1:def 2

OrthoRelStr(# {0},({} ({0},{0})),op1 #);

coherence OrthoRelStr(# {0},({} ({0},{0})),op1 #);

OrthoRelStr(# {0},({} ({0},{0})),op1 #) is strict OrthoRelStr ;

:: deftheorem defines TrivAsymOrthoRelStr OPOSET_1:def 2 :

TrivAsymOrthoRelStr = OrthoRelStr(# {0},({} ({0},{0})),op1 #);

TrivAsymOrthoRelStr = OrthoRelStr(# {0},({} ({0},{0})),op1 #);

registration
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 V254() ) );

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 V254() ) );

:: InternalRel based properties

:: 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 );

for O being non empty RelStr holds

( O is SubReFlexive iff the InternalRel of O is reflexive );

theorem :: OPOSET_1:2

registration
end;

registration
end;

definition

let O be non empty RelStr ;

compatibility

( O is irreflexive iff the InternalRel of O is irreflexive )

( O is irreflexive iff the InternalRel of O is_irreflexive_in the carrier of O ) ;

end;
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 the InternalRel of O is_irreflexive_in the carrier of O;

( O is irreflexive iff the InternalRel of O is_irreflexive_in the carrier of O ) ;

:: deftheorem defines irreflexive OPOSET_1:def 5 :

for O being non empty RelStr holds

( O is irreflexive iff the InternalRel of O is irreflexive );

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 );

for O being non empty RelStr holds

( O is irreflexive iff the InternalRel of O is_irreflexive_in the carrier of O );

registration
end;

registration

existence

ex b_{1} being non empty OrthoRelStr st

( b_{1} is irreflexive & b_{1} is strict )
by Th4;

end;
ex b

( b

:: Symmetry

definition

let O be non empty RelStr ;

( O is symmetric iff the InternalRel of O is symmetric Relation of the carrier of O ) by PARTIT_2:22, PARTIT_2:23;

end;
redefine attr O is symmetric means :: OPOSET_1:def 7

the InternalRel of O is symmetric Relation of the carrier of O;

compatibility the InternalRel of O is symmetric Relation of the carrier of O;

( O is symmetric iff the InternalRel of O is symmetric Relation of the carrier of O ) by PARTIT_2:22, PARTIT_2:23;

:: 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 );

for O being non empty RelStr holds

( O is symmetric iff the InternalRel of O is symmetric Relation of the carrier of O );

registration
end;

:: Antisymmetry

definition

let O be non empty RelStr ;

( O is antisymmetric iff the InternalRel of O is antisymmetric Relation of the carrier of O ) by PARTIT_2:25, PARTIT_2:24;

end;
redefine attr O is antisymmetric means :: OPOSET_1:def 8

the InternalRel of O is antisymmetric Relation of the carrier of O;

compatibility the InternalRel of O is antisymmetric Relation of the carrier of O;

( O is antisymmetric iff the InternalRel of O is antisymmetric Relation of the carrier of O ) by PARTIT_2:25, PARTIT_2:24;

:: 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 );

for O being non empty RelStr holds

( O is antisymmetric iff the InternalRel of O is antisymmetric Relation of the carrier of O );

Lm1: TrivOrthoRelStr is antisymmetric

;

registration
end;

registration

existence

ex b_{1} being non empty OrthoRelStr st

( b_{1} is symmetric & b_{1} is antisymmetric & b_{1} is strict )
by Lm1;

end;
ex b

( b

:: Asymmetry

definition

let O be non empty RelStr ;

( O is asymmetric iff the InternalRel of O is_asymmetric_in the carrier of O ) by PARTIT_2:28, PARTIT_2:29;

end;
redefine attr O is asymmetric means :: OPOSET_1:def 9

the InternalRel of O is_asymmetric_in the carrier of O;

compatibility the InternalRel of O is_asymmetric_in the carrier of O;

( O is asymmetric iff the InternalRel of O is_asymmetric_in the carrier of O ) by PARTIT_2:28, PARTIT_2:29;

:: 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 );

for O being non empty RelStr holds

( O is asymmetric iff the InternalRel of O is_asymmetric_in the carrier of O );

registration
end;

registration
end;

:: Transitivity

definition

let O be non empty RelStr ;

( O is transitive iff the InternalRel of O is transitive Relation of the carrier of O ) by PARTIT_2:27, PARTIT_2:26;

end;
redefine attr O is transitive means :: OPOSET_1:def 10

the InternalRel of O is transitive Relation of the carrier of O;

compatibility the InternalRel of O is transitive Relation of the carrier of O;

( O is transitive iff the InternalRel of O is transitive Relation of the carrier of O ) by PARTIT_2:27, PARTIT_2:26;

:: 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 );

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 b_{1} being non empty OrthoRelStr st

( b_{1} is reflexive & b_{1} is symmetric & b_{1} is antisymmetric & b_{1} is transitive & b_{1} is strict )
by Lm1;

end;
ex b

( b

registration

coherence

( TrivAsymOrthoRelStr is irreflexive & TrivAsymOrthoRelStr is asymmetric & TrivAsymOrthoRelStr is transitive ) ;

end;
( TrivAsymOrthoRelStr is irreflexive & TrivAsymOrthoRelStr is asymmetric & TrivAsymOrthoRelStr is transitive ) ;

registration

existence

ex b_{1} being non empty OrthoRelStr st

( b_{1} is irreflexive & b_{1} is asymmetric & b_{1} is transitive & b_{1} is strict )
by Th4;

end;
ex b

( b

theorem :: OPOSET_1:8

theorem :: OPOSET_1:9

:: Quasiorder (Preorder)

:: deftheorem defines SubQuasiOrdered OPOSET_1:def 11 :

for O being non empty RelStr holds

( O is SubQuasiOrdered iff ( O is SubReFlexive & O is transitive ) );

for O being non empty RelStr holds

( O is SubQuasiOrdered iff ( O is SubReFlexive & O is transitive ) );

:: 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 ) );

for O being non empty RelStr holds

( O is QuasiOrdered iff ( O is reflexive & O is transitive ) );

registration

correctness

coherence

for b_{1} being non empty OrthoRelStr st b_{1} is QuasiOrdered holds

b_{1} is SubQuasiOrdered ;

by Th11;

end;
coherence

for b

b

by Th11;

registration
end;

:: QuasiPure means complementation-order-like combination of properties

:: deftheorem defines QuasiPure OPOSET_1:def 13 :

for O being non empty OrthoRelStr holds

( O is QuasiPure iff ( O is Dneg & O is QuasiOrdered ) );

for O being non empty OrthoRelStr holds

( O is QuasiPure iff ( O is Dneg & O is QuasiOrdered ) );

registration

existence

ex b_{1} being non empty OrthoRelStr st

( b_{1} is QuasiPure & b_{1} is Dneg & b_{1} is QuasiOrdered & b_{1} is strict )

end;
ex b

( b

proof end;

registration
end;

:: Partial Order ---> Poset

definition

let O be non empty OrthoRelStr ;

end;
attr O is PartialOrdered means :: OPOSET_1:def 14

( O is reflexive & O is antisymmetric & O is transitive );

( O is reflexive & O is antisymmetric & O is transitive );

:: 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 ) );

for O being non empty OrthoRelStr holds

( O is PartialOrdered iff ( O is reflexive & O is antisymmetric & O is transitive ) );

registration

coherence

for b_{1} being non empty OrthoRelStr st b_{1} is PartialOrdered holds

( b_{1} is reflexive & b_{1} is antisymmetric & b_{1} is transitive )
;

coherence

for b_{1} being non empty OrthoRelStr st b_{1} is reflexive & b_{1} is antisymmetric & b_{1} is transitive holds

b_{1} is PartialOrdered
;

end;
for b

( b

coherence

for b

b

:: Pureness for partial orders

:: deftheorem defines Pure OPOSET_1:def 15 :

for O being non empty OrthoRelStr holds

( O is Pure iff ( O is Dneg & O is PartialOrdered ) );

for O being non empty OrthoRelStr holds

( O is Pure iff ( O is Dneg & O is PartialOrdered ) );

registration

existence

ex b_{1} being non empty OrthoRelStr st

( b_{1} is Pure & b_{1} is Dneg & b_{1} is PartialOrdered & b_{1} is strict )

end;
ex b

( b

proof end;

:: Strict Poset

:: deftheorem defines StrictPartialOrdered OPOSET_1:def 16 :

for O being non empty OrthoRelStr holds

( O is StrictPartialOrdered iff ( O is asymmetric & O is transitive ) );

for O being non empty OrthoRelStr holds

( O is StrictPartialOrdered iff ( O is asymmetric & O is transitive ) );

registration

coherence

for b_{1} being non empty OrthoRelStr st b_{1} is StrictPartialOrdered holds

b_{1} is irreflexive
by Th12;

end;
for b

b

registration

coherence

for b_{1} being non empty OrthoRelStr st b_{1} is StrictPartialOrdered holds

b_{1} is irreflexive
;

end;
for b

b

registration
end;

registration

existence

ex b_{1} being non empty strict OrthoRelStr st

( b_{1} is irreflexive & b_{1} is StrictPartialOrdered )

end;
ex b

( b

proof end;

theorem :: OPOSET_1:13

for QO being non empty QuasiOrdered OrthoRelStr st QO is antisymmetric holds

QO is PartialOrdered by Def12;

QO is PartialOrdered by Def12;

registration

correctness

coherence

for b_{1} being non empty OrthoRelStr st b_{1} is PartialOrdered holds

( b_{1} is reflexive & b_{1} is transitive & b_{1} is antisymmetric );

;

end;
coherence

for b

( b

;

:: 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 V254() & f is antitone ) );

for PO being non empty RelStr

for f being UnOp of the carrier of PO holds

( f is Orderinvolutive iff ( f is V254() & f is antitone ) );

:: deftheorem defines OrderInvolutive OPOSET_1:def 18 :

for PO being non empty OrthoRelStr holds

( PO is OrderInvolutive iff the Compl of PO is Orderinvolutive );

for PO being non empty OrthoRelStr holds

( PO is OrderInvolutive iff the Compl of PO is Orderinvolutive );

registration

existence

ex b_{1} being non empty OrthoRelStr st

( b_{1} is OrderInvolutive & b_{1} is Pure & b_{1} is PartialOrdered )

end;
ex b

( b

proof end;

definition

let PO be non empty RelStr ;

let f be UnOp of the carrier of PO;

end;
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 ) ) );

( f is Orderinvolutive & ( for y being Element of PO holds

( ex_sup_of {y,(f . y)},PO & ex_inf_of {y,(f . y)},PO ) ) );

:: 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 ) ) ) );

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 ;

end;
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 );

ex f being Function of PO,PO st

( f = the Compl of PO & f QuasiOrthoComplement_on PO );

:: 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 ) );

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: id {{}} = {[{},{}]}

by SYSREL:13;

definition

let PO be non empty RelStr ;

let f be UnOp of the carrier of PO;

end;
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 ) ) );

( 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 ) ) );

:: 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 ) ) ) );

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 ;

end;
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 );

ex f being Function of PO,PO st

( f = the Compl of PO & f OrthoComplement_on PO );

:: 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 ) );

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 ;

for f being UnOp of the carrier of PO st f OrthoComplement_on PO holds

f QuasiOrthoComplement_on PO ;

:: PartialOrdered (non empty OrthoRelStr)

registration

coherence

( TrivOrthoRelStr is QuasiOrthocomplemented & TrivOrthoRelStr is Orthocomplemented ) by Th15, Th17;

end;
( TrivOrthoRelStr is QuasiOrthocomplemented & TrivOrthoRelStr is Orthocomplemented ) by Th15, Th17;

registration

correctness

existence

ex b_{1} being non empty OrthoRelStr st

( b_{1} is Orthocomplemented & b_{1} is QuasiOrthocomplemented & b_{1} is PartialOrdered );

end;
existence

ex b

( b

proof end;

definition

mode QuasiOrthoPoset is non empty PartialOrdered QuasiOrthocomplemented OrthoRelStr ;

mode OrthoPoset is non empty PartialOrdered Orthocomplemented OrthoRelStr ;

end;
mode OrthoPoset is non empty PartialOrdered Orthocomplemented OrthoRelStr ;