Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

### Basic Notions and Properties of Orthoposets

by
Markus Moschner

MML identifier: OPOSET_1
[ Mizar article, MML identifier index ]

```environ

vocabulary OPOSET_1, ORDERS_1, RELAT_1, FUNCT_1, ROBBINS1, BINOP_1, SUBSET_1,
LATTICE3, LATTICES, BOOLE, ORDINAL2, RELAT_2, VECTSP_2, WAYBEL_0,
WAYBEL_1, YELLOW_0, PRE_TOPC, REALSET1;
notation TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, FUNCT_1, RELAT_1, RELAT_2,
FUNCT_2, RELSET_1, PARTFUN1, BINOP_1, STRUCT_0, ORDERS_1, REALSET1,
VECTSP_2, LATTICE3, ROBBINS1, PRE_TOPC, WAYBEL_0, WAYBEL_1, YELLOW_0,
NECKLACE;
constructors LATTICE3, ROBBINS1, VECTSP_2, WAYBEL_1, NECKLACE, REALSET1;
clusters ORDERS_1, RELSET_1, STRUCT_0, SUBSET_1, PARTFUN1, FUNCT_2, XBOOLE_0,
WAYBEL24, NECKLACE, YELLOW_0;
requirements BOOLE, SUBSET;

begin

reserve S, X for non empty set,
R for Relation of X;

definition
struct(RelStr,ComplStr) OrthoRelStr (# carrier -> set,
InternalRel -> (Relation of the carrier),
Compl -> UnOp of the carrier #);
end;

:: Some basic definitions and theorems for later examples;
definition let A,B be set;
func {}(A,B) -> Relation of A,B equals
:: OPOSET_1:def 1
{};
func [#](A,B) -> Relation of A,B equals
:: OPOSET_1:def 2
[:A,B:];
end;

theorem :: OPOSET_1:1
field id X = X;

theorem :: OPOSET_1:2
id {{}} = {[{},{}]};

theorem :: OPOSET_1:3
op1 = {[{},{}]};

theorem :: OPOSET_1:4
for L being non empty reflexive antisymmetric RelStr
for x,y being Element of L holds x <= y implies
sup {x,y} = y & inf {x,y} = x;

:: for various types of relations needed for Posets

theorem :: OPOSET_1:5
for R being Relation holds dom R c= field R & rng R c= field R;

theorem :: OPOSET_1:6
for A,B being set holds field {}(A,B) = {};

theorem :: OPOSET_1:7
R is_reflexive_in X implies R is reflexive & field R = X;

theorem :: OPOSET_1:8
R is_symmetric_in X implies R is symmetric;

theorem :: OPOSET_1:9
R is symmetric & field R c= S implies R is_symmetric_in S;

theorem :: OPOSET_1:10
R is antisymmetric & field R c= S implies R is_antisymmetric_in S;

theorem :: OPOSET_1:11
R is_antisymmetric_in X implies R is antisymmetric;

theorem :: OPOSET_1:12
R is transitive & field R c= S implies R is_transitive_in S;

theorem :: OPOSET_1:13
R is_transitive_in X implies R is transitive;

theorem :: OPOSET_1:14
R is asymmetric & field R c= S implies R is_asymmetric_in S;

theorem :: OPOSET_1:15
R is_asymmetric_in X implies R is asymmetric;

theorem :: OPOSET_1:16
R is irreflexive & field R c= S implies R is_irreflexive_in S;

theorem :: OPOSET_1:17
R is_irreflexive_in X implies R is irreflexive;

:: Some existence conditions on non-empty relations

definition let X be set;
cluster irreflexive asymmetric transitive Relation of X;
end;

canceled;

definition let X, R;
let C be UnOp of X;
cluster OrthoRelStr(#X,R,C#) -> non empty;
end;

definition
cluster non empty strict OrthoRelStr;
end;

:: Double negation property of the internal Complement

definition let X;
let f be Function of X,X;
attr f is dneg means
:: OPOSET_1:def 3
for x being Element of X holds f.(f.x) = x;
synonym f is involutive;
end;

theorem :: OPOSET_1:19
op1 is dneg;

theorem :: OPOSET_1:20
id X is dneg;

definition let O be non empty OrthoRelStr;
canceled;
cluster dneg map of O,O;
end;

:: Small example structures

definition
func TrivOrthoRelStr -> strict OrthoRelStr equals
:: OPOSET_1:def 5
OrthoRelStr (# {{}}, id {{}}, op1 #);
synonym TrivPoset;
end;

definition
cluster TrivOrthoRelStr -> non empty trivial;
end;

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

definition
cluster TrivAsymOrthoRelStr -> non empty;
end;

definition let O be non empty OrthoRelStr;
attr O is Dneg means
:: OPOSET_1:def 7
ex f being map of O,O st f = the Compl of O & f is dneg;
end;

theorem :: OPOSET_1:21
TrivOrthoRelStr is Dneg;

definition
cluster TrivOrthoRelStr -> Dneg;
end;

definition
cluster Dneg (non empty OrthoRelStr);
end;

:: InternalRel based properties

definition let O be non empty RelStr;
canceled 2;
attr O is SubReFlexive means
:: OPOSET_1:def 10
the InternalRel of O is reflexive;
canceled;
end;

reserve O for non empty RelStr;

theorem :: OPOSET_1:22
O is reflexive implies O is SubReFlexive;

theorem :: OPOSET_1:23
TrivOrthoRelStr is reflexive;

definition
cluster TrivOrthoRelStr -> reflexive;
end;

definition
cluster reflexive strict (non empty OrthoRelStr);
end;

definition let O;
attr O is SubIrreFlexive means
:: OPOSET_1:def 12
the InternalRel of O is irreflexive;
redefine attr O is irreflexive means
:: OPOSET_1:def 13
the InternalRel of O is_irreflexive_in the carrier of O;
end;

theorem :: OPOSET_1:24
O is irreflexive implies O is SubIrreFlexive;

theorem :: OPOSET_1:25
TrivAsymOrthoRelStr is irreflexive;

definition
cluster irreflexive -> SubIrreFlexive (non empty OrthoRelStr);
end;

definition
cluster TrivAsymOrthoRelStr -> irreflexive;
end;

definition
cluster irreflexive strict (non empty OrthoRelStr);
end;

:: Symmetry

definition let O be non empty RelStr;
attr O is SubSymmetric means
:: OPOSET_1:def 14
the InternalRel of O is symmetric Relation of the carrier of O;
canceled;
end;

theorem :: OPOSET_1:26
O is symmetric implies O is SubSymmetric;

theorem :: OPOSET_1:27
TrivOrthoRelStr is symmetric;

definition
cluster symmetric -> SubSymmetric (non empty OrthoRelStr);
end;

definition
cluster symmetric strict (non empty OrthoRelStr);
end;

:: Antisymmetry

definition let O;
attr O is SubAntisymmetric means
:: OPOSET_1:def 16
the InternalRel of O is antisymmetric Relation of the carrier of O;
canceled;
end;

theorem :: OPOSET_1:28
O is antisymmetric implies O is SubAntisymmetric;

theorem :: OPOSET_1:29
TrivOrthoRelStr is antisymmetric;

definition
cluster antisymmetric -> SubAntisymmetric (non empty OrthoRelStr);
end;

definition
cluster TrivOrthoRelStr -> symmetric;
end;

definition
cluster symmetric antisymmetric strict (non empty OrthoRelStr);
end;

:: Asymmetry

definition let O;
canceled;
attr O is Asymmetric means
:: OPOSET_1:def 19
the InternalRel of O is_asymmetric_in the carrier of O;
end;

theorem :: OPOSET_1:30
O is Asymmetric implies O is asymmetric;

theorem :: OPOSET_1:31
TrivAsymOrthoRelStr is Asymmetric;

definition
cluster Asymmetric -> asymmetric (non empty OrthoRelStr);
end;

definition
cluster TrivAsymOrthoRelStr -> Asymmetric;
end;

definition
cluster Asymmetric strict (non empty OrthoRelStr);
end;

:: Transitivity

definition let O;
attr O is SubTransitive means
:: OPOSET_1:def 20
the InternalRel of O is transitive Relation of the carrier of O;
canceled;
end;

theorem :: OPOSET_1:32
O is transitive implies O is SubTransitive;

theorem :: OPOSET_1:33
TrivOrthoRelStr is transitive;

definition
cluster transitive -> SubTransitive (non empty OrthoRelStr);
end;

definition
cluster reflexive symmetric antisymmetric transitive strict
(non empty OrthoRelStr);
end;

theorem :: OPOSET_1:34
TrivAsymOrthoRelStr is transitive;

definition
cluster TrivAsymOrthoRelStr -> irreflexive Asymmetric transitive;
end;

definition
cluster irreflexive Asymmetric transitive strict (non empty OrthoRelStr);
end;

theorem :: OPOSET_1:35
O is SubSymmetric SubTransitive implies O is SubReFlexive;

theorem :: OPOSET_1:36
O is SubIrreFlexive SubTransitive implies O is asymmetric;

theorem :: OPOSET_1:37
O is asymmetric implies O is SubIrreFlexive;

theorem :: OPOSET_1:38
O is reflexive SubSymmetric implies O is symmetric;

definition
cluster reflexive SubSymmetric -> symmetric (non empty OrthoRelStr);
end;

theorem :: OPOSET_1:39
O is reflexive SubAntisymmetric implies O is antisymmetric;

definition
cluster reflexive SubAntisymmetric -> antisymmetric (non empty OrthoRelStr);
end;

theorem :: OPOSET_1:40
O is reflexive SubTransitive implies O is transitive;

definition
cluster reflexive SubTransitive -> transitive (non empty OrthoRelStr);
end;

theorem :: OPOSET_1:41
O is irreflexive SubTransitive implies O is transitive;

definition
cluster irreflexive SubTransitive ->
transitive (non empty OrthoRelStr);
end;

theorem :: OPOSET_1:42
O is irreflexive asymmetric implies O is Asymmetric;

definition
cluster irreflexive asymmetric -> Asymmetric (non empty OrthoRelStr);
end;

begin
:: Quasiorder (Preorder)

definition let O;
attr O is SubQuasiOrdered means
:: OPOSET_1:def 22
O is SubReFlexive SubTransitive;
synonym O is SubQuasiordered;
synonym O is SubPreOrdered;
synonym O is SubPreordered;
synonym O is Subpreordered;
end;

definition let O;
attr O is QuasiOrdered means
:: OPOSET_1:def 23
O is reflexive transitive;
synonym O is Quasiordered;
synonym O is PreOrdered;
synonym O is Preordered;
end;

theorem :: OPOSET_1:43
O is QuasiOrdered implies O is SubQuasiOrdered;

definition
cluster QuasiOrdered -> SubQuasiOrdered (non empty OrthoRelStr);
end;

definition
cluster TrivOrthoRelStr -> QuasiOrdered;
end;

reserve O for non empty OrthoRelStr;

:: QuasiPure means complementation-order-like combination of properties
definition let O;
attr O is QuasiPure means
:: OPOSET_1:def 24
O is Dneg QuasiOrdered;
end;

definition
cluster QuasiPure Dneg QuasiOrdered strict (non empty OrthoRelStr);
end;

definition
cluster TrivOrthoRelStr -> QuasiPure;
end;

definition
mode QuasiPureOrthoRelStr is QuasiPure (non empty OrthoRelStr);
end;

:: Partial Order ---> Poset
definition let O;
attr O is SubPartialOrdered means
:: OPOSET_1:def 25
O is reflexive SubAntisymmetric SubTransitive;
synonym O is SubPartialordered;
end;

definition let O;
attr O is PartialOrdered means
:: OPOSET_1:def 26
O is reflexive antisymmetric transitive;
synonym O is Partialordered;
end;

theorem :: OPOSET_1:44
O is SubPartialOrdered iff O is PartialOrdered;

definition
cluster SubPartialOrdered -> PartialOrdered (non empty OrthoRelStr);
cluster PartialOrdered -> SubPartialOrdered (non empty OrthoRelStr);
end;

definition
cluster PartialOrdered -> reflexive antisymmetric transitive
(non empty OrthoRelStr);
cluster reflexive antisymmetric transitive -> PartialOrdered
(non empty OrthoRelStr);
end;

:: Pureness for partial orders
definition let O;
attr O is Pure means
:: OPOSET_1:def 27
O is Dneg PartialOrdered;
end;

definition
cluster Pure Dneg PartialOrdered strict (non empty OrthoRelStr);
end;

definition
cluster TrivOrthoRelStr -> Pure;
end;

definition
mode PureOrthoRelStr is Pure (non empty OrthoRelStr);
end;

:: Strict Poset
definition let O;
attr O is SubStrictPartialOrdered means
:: OPOSET_1:def 28
O is asymmetric SubTransitive;
end;

definition let O;
attr O is StrictPartialOrdered means
:: OPOSET_1:def 29
O is Asymmetric transitive;
synonym O is Strictpartialordered;
synonym O is StrictOrdered;
synonym O is Strictordered;
end;

theorem :: OPOSET_1:45
O is StrictPartialOrdered implies O is SubStrictPartialOrdered;

definition
cluster StrictPartialOrdered ->
SubStrictPartialOrdered (non empty OrthoRelStr);
end;

theorem :: OPOSET_1:46
O is SubStrictPartialOrdered implies O is SubIrreFlexive;

definition
cluster SubStrictPartialOrdered -> SubIrreFlexive (non empty OrthoRelStr);
end;

theorem :: OPOSET_1:47
O is irreflexive SubStrictPartialOrdered implies O is StrictPartialOrdered;

definition
cluster irreflexive SubStrictPartialOrdered ->
StrictPartialOrdered (non empty OrthoRelStr);
end;

theorem :: OPOSET_1:48
O is StrictPartialOrdered implies O is irreflexive;

definition
cluster StrictPartialOrdered -> irreflexive (non empty OrthoRelStr);
end;

definition
cluster TrivAsymOrthoRelStr -> irreflexive StrictPartialOrdered;
end;

definition
cluster irreflexive StrictPartialOrdered (non empty strict OrthoRelStr);
end;

:: Quasiorder to Partial Order

reserve PO for PartialOrdered (non empty OrthoRelStr),
QO for QuasiOrdered (non empty OrthoRelStr);

theorem :: OPOSET_1:49
QO is SubAntisymmetric implies QO is PartialOrdered;

theorem :: OPOSET_1:50
PO is Poset;

definition
cluster PartialOrdered -> reflexive transitive antisymmetric
(non empty OrthoRelStr);
end;

definition let PO be PartialOrdered (non empty OrthoRelStr);
let f be UnOp of the carrier of PO;
canceled 3;
attr f is Orderinvolutive means
:: OPOSET_1:def 33
f is dneg map of PO,PO & f is antitone map of PO,PO;
end;

definition let PO;
attr PO is OrderInvolutive means
:: OPOSET_1:def 34
ex f being map of PO,PO st f = the Compl of PO & f is Orderinvolutive;
end;

theorem :: OPOSET_1:51
the Compl of TrivOrthoRelStr is Orderinvolutive;

definition
cluster TrivOrthoRelStr -> OrderInvolutive;
end;

definition
cluster OrderInvolutive Pure (PartialOrdered (non empty OrthoRelStr));
end;

definition
mode PreOrthoPoset is
OrderInvolutive Pure (PartialOrdered (non empty OrthoRelStr));
end;

definition let PO;
let f be UnOp of the carrier of PO;
pred f QuasiOrthoComplement_on PO means
:: OPOSET_1:def 35
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;

definition let PO;
attr PO is QuasiOrthocomplemented means
:: OPOSET_1:def 36
ex f being map of PO,PO st
f = the Compl of PO & f QuasiOrthoComplement_on PO;
end;

theorem :: OPOSET_1:52
TrivOrthoRelStr is QuasiOrthocomplemented;

definition let PO;
let f be UnOp of the carrier of PO;
pred f OrthoComplement_on PO means
:: OPOSET_1:def 37
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;
synonym f Ocompl_on PO;
end;

definition let PO;
attr PO is Orthocomplemented means
:: OPOSET_1:def 38
ex f being map of PO,PO st
f = the Compl of PO & f OrthoComplement_on PO;
synonym PO is Ocompl;
end;

theorem :: OPOSET_1:53
for f being UnOp of the carrier of PO holds
f OrthoComplement_on PO implies f QuasiOrthoComplement_on PO;

:: PartialOrdered (non empty OrthoRelStr)

theorem :: OPOSET_1:54
TrivOrthoRelStr is Orthocomplemented;

definition
cluster TrivOrthoRelStr -> QuasiOrthocomplemented Orthocomplemented;
end;

definition
cluster Orthocomplemented QuasiOrthocomplemented
(PartialOrdered (non empty OrthoRelStr));
end;

definition
mode QuasiOrthoPoset is
QuasiOrthocomplemented (PartialOrdered (non empty OrthoRelStr));
mode OrthoPoset is
Orthocomplemented (PartialOrdered (non empty OrthoRelStr));
end;

```