:: Basic Notions and Properties of Orthoposets
:: by Markus Moschner
::
:: Received February 11, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, RELAT_1, SUBSET_1, TARSKI, FUNCT_5, FUNCT_1, RELAT_2,
ORDERS_2, XXREAL_0, ORDINAL2, LATTICE3, BINOP_1, QMAX_1, STRUCT_0,
ROBBINS1, WAYBEL_0, YELLOW_0, EQREL_1, WAYBEL_1, LATTICES, OPOSET_1,
CARD_1;
notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, RELAT_1, RELAT_2, FUNCT_2,
RELSET_1, PARTFUN1, BINOP_1, DOMAIN_1, FUNCT_5, ORDINAL1, CARD_1,
STRUCT_0, ORDERS_2, LATTICE3, ROBBINS1, WAYBEL_0, WAYBEL_1, YELLOW_0,
NECKLACE, QMAX_1, PARTIT_2;
constructors REALSET2, LATTICE3, WAYBEL_1, NECKLACE, QMAX_1, FUNCT_5,
PARTIT_2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, STRUCT_0,
YELLOW_0, WAYBEL24, PARTIT_2, CARD_1, RELAT_2;
requirements BOOLE, SUBSET;
definitions RELAT_2, NECKLACE;
equalities RELAT_1, ORDINAL1;
expansions RELAT_2, ORDERS_2, NECKLACE, STRUCT_0;
theorems FUNCT_2, LATTICE3, PARTIT_2, RELAT_1, RELAT_2, RELSET_1, TARSKI,
WAYBEL_0, WAYBEL_1, YELLOW_0, ENUMSET1, SYSREL;
begin
reserve X for non empty set,
R for Relation of X;
:: Some basic definitions and theorems for later examples;
theorem
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
proof
let R be non empty reflexive antisymmetric RelStr;
let a,b be Element of R;
A1: for x being Element of R st x is_>=_than {a,b} holds b <= x
proof
let a0 be Element of R;
A2: b in {a,b} by TARSKI:def 2;
assume a0 is_>=_than {a,b};
hence thesis by A2,LATTICE3:def 9;
end;
A3: for x being Element of R st x is_<=_than {a,b} holds a >= x
proof
let a0 be Element of R;
A4: a in {a,b} by TARSKI:def 2;
assume a0 is_<=_than {a,b};
hence thesis by A4,LATTICE3:def 8;
end;
assume
A5: a <= b;
for x being Element of {a,b} holds x >= a
proof
let a0 be Element of {a,b};
a <= a0 or a <= a0 by A5,TARSKI:def 2;
hence thesis;
end;
then for x being Element of R st x in {a,b} holds x >= a;
then
A6: a is_<=_than {a,b} by LATTICE3:def 8;
for x being Element of R st x in {a,b} holds x <= b by A5,TARSKI:def 2;
then b is_>=_than {a,b} by LATTICE3:def 9;
hence thesis by A6,A1,A3,YELLOW_0:30,31;
end;
:: for various types of relations needed for Posets
:: Some existence conditions on non-empty relations
registration
let X be set;
cluster irreflexive asymmetric transitive for Relation of X;
existence
proof
{}(X,X) = {};
hence thesis;
end;
end;
registration
let X, R;
let C be UnOp of X;
cluster OrthoRelStr(#X,R,C#) -> non empty;
coherence;
end;
registration
cluster non empty strict for OrthoRelStr;
existence
proof
set X = the non empty set,R = the (Relation of X),C = the UnOp of X;
take OrthoRelStr(#X,R,C#);
thus thesis;
end;
end;
:: Double negation property of the internal Complement
registration
let O be set;
cluster involutive for Function of O,O;
existence
proof
take id O;
thus thesis;
end;
end;
:: Small example structures
definition
func TrivOrthoRelStr -> strict OrthoRelStr equals
:Def1:
OrthoRelStr (#{0}, id{0}, op1 #);
coherence;
end;
notation
synonym TrivPoset for TrivOrthoRelStr;
end;
registration
cluster TrivOrthoRelStr -> 1-element;
coherence;
end;
definition
func TrivAsymOrthoRelStr -> strict OrthoRelStr equals
OrthoRelStr (#{0},{}({0},{0}), op1 #);
coherence;
end;
registration
cluster TrivAsymOrthoRelStr -> non empty;
coherence;
end;
definition
let O be non empty OrthoRelStr;
attr O is Dneg means
ex f being Function of O,O st f = the Compl of O & f is involutive;
end;
registration
cluster TrivOrthoRelStr -> Dneg;
coherence;
end;
registration
cluster Dneg for non empty OrthoRelStr;
existence by Def1;
end;
:: InternalRel based properties
definition
let O be non empty RelStr;
attr O is SubReFlexive means
:Def4:
the InternalRel of O is reflexive;
end;
reserve O for non empty RelStr;
theorem
O is reflexive implies O is SubReFlexive
by PARTIT_2:21;
theorem Th3:
TrivOrthoRelStr is reflexive
proof
rng id {{}} = {{}} & field id {{}} = dom id {{}} \/ rng id {{}};
hence thesis by RELAT_2:def 9;
end;
registration
cluster TrivOrthoRelStr -> reflexive;
coherence by Th3;
end;
registration
cluster reflexive strict for non empty OrthoRelStr;
existence by Th3;
end;
definition
let O;
redefine attr O is irreflexive means :: redefines irreflexive (NECKLACE, definition)
the InternalRel of O is irreflexive;
compatibility
proof
set RO = the InternalRel of O;
A1: field RO c= (the carrier of O) \/ the carrier of O by RELSET_1:8;
thus O is irreflexive implies RO is irreflexive
proof
assume
A2: O is irreflexive;
let x be object;
thus thesis by A1,A2;
end;
assume
A3: RO is_irreflexive_in field RO;
let x be set;
assume x in the carrier of O;
per cases;
suppose x in field RO;
hence not [x,x] in RO by A3;
end;
suppose not x in field RO;
hence not [x,x] in RO by RELAT_1:15;
end;
end;
redefine attr O is irreflexive means :: redefines irreflexive (NECKLACE, definition)
the InternalRel of O is_irreflexive_in the carrier of O;
compatibility;
end;
theorem Th4:
TrivAsymOrthoRelStr is irreflexive;
registration
cluster TrivAsymOrthoRelStr -> irreflexive;
coherence;
end;
registration
cluster irreflexive strict for non empty OrthoRelStr;
existence by Th4;
end;
:: Symmetry
definition
let O be non empty RelStr;
redefine attr O is symmetric means :: redefines symmetric (NECKLACE, definition)
the InternalRel of O is symmetric Relation of the carrier of O;
compatibility
by PARTIT_2:22,PARTIT_2:23;
end;
theorem Th5:
TrivOrthoRelStr is symmetric;
registration
cluster symmetric strict for non empty OrthoRelStr;
existence by Th5;
end;
:: Antisymmetry
definition
let O;
redefine attr O is antisymmetric means :: redefines antisymmetric (YELLOW_0, redefinition) → antisymmetric (ORDERS_2, definition)
the InternalRel of O is antisymmetric Relation of the carrier of O;
compatibility
by PARTIT_2:25,PARTIT_2:24;
end;
Lm1: TrivOrthoRelStr is antisymmetric;
registration
cluster TrivOrthoRelStr -> symmetric;
coherence;
end;
registration
cluster symmetric antisymmetric strict for non empty OrthoRelStr;
existence by Lm1;
end;
:: Asymmetry
definition
let O;
redefine attr O is asymmetric means :: redefines asymmetric (NECKLACE, definition)
the InternalRel of O is_asymmetric_in the carrier of O;
compatibility
by PARTIT_2:28,PARTIT_2:29;
end;
theorem Th6:
TrivAsymOrthoRelStr is asymmetric;
registration
cluster TrivAsymOrthoRelStr -> asymmetric;
coherence;
end;
registration
cluster asymmetric strict for non empty OrthoRelStr;
existence by Th6;
end;
:: Transitivity
definition
let O;
redefine attr O is transitive means :: redefines transitive (YELLOW_0, redefinition) → transitive (ORDERS_2, definition)
the InternalRel of O is transitive Relation of the carrier of O;
compatibility
by PARTIT_2:27,PARTIT_2:26;
end;
registration
cluster reflexive symmetric antisymmetric transitive strict for non empty
OrthoRelStr;
existence by Lm1;
end;
theorem
TrivAsymOrthoRelStr is transitive;
registration
cluster TrivAsymOrthoRelStr -> irreflexive asymmetric transitive;
coherence;
end;
registration
cluster irreflexive asymmetric transitive strict for non empty OrthoRelStr;
existence by Th4;
end;
theorem
O is symmetric transitive implies O is SubReFlexive;
theorem
O is irreflexive transitive implies O is asymmetric;
theorem
O is asymmetric implies O is irreflexive;
begin
:: Quasiorder (Preorder)
definition
let O;
attr O is SubQuasiOrdered means
O is SubReFlexive transitive;
end;
notation
let O;
synonym O is SubPreOrdered for O is SubQuasiOrdered;
end;
definition
let O;
attr O is QuasiOrdered means
:Def12:
O is reflexive transitive;
end;
notation
let O;
synonym O is PreOrdered for O is QuasiOrdered;
end;
theorem Th11:
O is QuasiOrdered implies O is SubQuasiOrdered
proof
set IntRel = the InternalRel of O;
set CO = the carrier of O;
assume
A1: O is QuasiOrdered;
then
A2: O is transitive;
O is reflexive by A1;
then IntRel is_reflexive_in CO;
then IntRel is reflexive by PARTIT_2:21;
hence thesis by A2,Def4;
end;
registration
cluster QuasiOrdered -> SubQuasiOrdered for non empty OrthoRelStr;
correctness by Th11;
end;
registration
cluster TrivOrthoRelStr -> QuasiOrdered;
coherence;
end;
reserve O for non empty OrthoRelStr;
:: QuasiPure means complementation-order-like combination of properties
definition
let O;
attr O is QuasiPure means
O is Dneg QuasiOrdered;
end;
registration
cluster QuasiPure Dneg QuasiOrdered strict for non empty OrthoRelStr;
existence
proof
TrivOrthoRelStr is QuasiPure;
hence thesis;
end;
end;
registration
cluster TrivOrthoRelStr -> QuasiPure;
coherence;
end;
definition
mode QuasiPureOrthoRelStr is QuasiPure non empty OrthoRelStr;
end;
:: Partial Order ---> Poset
definition
let O;
attr O is PartialOrdered means
O is reflexive antisymmetric transitive;
end;
registration
cluster PartialOrdered -> reflexive antisymmetric transitive for non empty
OrthoRelStr;
coherence;
cluster reflexive antisymmetric transitive -> PartialOrdered for non empty
OrthoRelStr;
coherence;
end;
:: Pureness for partial orders
definition
let O;
attr O is Pure means
O is Dneg PartialOrdered;
end;
registration
cluster Pure Dneg PartialOrdered strict for non empty OrthoRelStr;
existence
proof
TrivOrthoRelStr is Pure;
hence thesis;
end;
end;
registration
cluster TrivOrthoRelStr -> Pure;
coherence;
end;
definition
mode PureOrthoRelStr is Pure non empty OrthoRelStr;
end;
:: Strict Poset
definition
let O;
attr O is StrictPartialOrdered means
O is asymmetric transitive;
end;
notation
let O;
synonym O is StrictOrdered for O is StrictPartialOrdered;
end;
theorem Th12:
O is StrictPartialOrdered implies O is irreflexive
proof
assume O is StrictPartialOrdered;
then O is asymmetric transitive;
hence thesis;
end;
registration
cluster StrictPartialOrdered -> irreflexive for non empty OrthoRelStr;
coherence by Th12;
end;
registration
cluster StrictPartialOrdered -> irreflexive for non empty OrthoRelStr;
coherence;
end;
registration
cluster TrivAsymOrthoRelStr -> irreflexive StrictPartialOrdered;
coherence;
end;
registration
cluster irreflexive StrictPartialOrdered for non empty strict OrthoRelStr;
existence
proof
TrivAsymOrthoRelStr is StrictPartialOrdered;
hence thesis;
end;
end;
:: Quasiorder to Partial Order
reserve QO for QuasiOrdered non empty OrthoRelStr;
theorem
QO is antisymmetric implies QO is PartialOrdered
by Def12;
registration
cluster PartialOrdered -> reflexive transitive antisymmetric for non empty
OrthoRelStr;
correctness;
end;
definition
let PO be non empty RelStr;
let f be UnOp of the carrier of PO;
attr f is Orderinvolutive means
f is involutive antitone;
end;
definition
let PO be non empty OrthoRelStr;
attr PO is OrderInvolutive means
the Compl of PO is Orderinvolutive;
end;
theorem Th14:
the Compl of TrivOrthoRelStr is Orderinvolutive
proof
set O = TrivOrthoRelStr;
set C = the Compl of O;
reconsider Emp = {} as Element of O by TARSKI:def 1;
C is antitone Function of O,O
proof
reconsider f = C as Function of O,O;
for x1,x2 being Element of O st x1 <= x2 for y1,y2 being Element of O
st y1 = f.x1 & y2 = f.x2 holds y1 >= y2
proof
let a1,a2 be Element of O;
set b1 = f.a1;
b1 = Emp by FUNCT_2:50;
then f.a2 <= b1 by FUNCT_2:50;
hence thesis;
end;
hence thesis by WAYBEL_0:def 5;
end;
hence thesis;
end;
registration
cluster TrivOrthoRelStr -> OrderInvolutive;
coherence by Th14;
end;
registration
cluster OrderInvolutive Pure PartialOrdered for non empty OrthoRelStr;
existence
proof
take TrivOrthoRelStr;
thus thesis;
end;
end;
definition
mode PreOrthoPoset is OrderInvolutive Pure PartialOrdered non empty
OrthoRelStr;
end;
definition
let PO be non empty RelStr;
let f be UnOp of the carrier of PO;
pred f QuasiOrthoComplement_on PO means
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 be non empty OrthoRelStr;
attr PO is QuasiOrthocomplemented means
ex f being Function of PO,PO
st f = the Compl of PO & f QuasiOrthoComplement_on PO;
end;
Lm2: id {{}} = {[{},{}]} by SYSREL:13;
theorem Th15:
TrivOrthoRelStr is QuasiOrthocomplemented
proof
set O = TrivOrthoRelStr;
set C = the Compl of O;
set S = the carrier of O;
C QuasiOrthoComplement_on O
proof
reconsider f = C as Function of O,O;
A1: for x being Element of S holds {x,op1.x} = {x}
by Lm2,PARTIT_2:19,ENUMSET1:29;
for x being Element of O holds sup {x,f.x} = x & inf {x,f.x} = x &
ex_sup_of {x,f.x},O & ex_inf_of {x,f.x},O
proof
let a be Element of O;
{a,f.a} = {a} by A1;
hence thesis by YELLOW_0:38,39;
end;
hence thesis by Th14;
end;
hence thesis;
end;
definition
let PO be non empty RelStr;
let f be UnOp of the carrier of PO;
pred f OrthoComplement_on PO means
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;
definition
let PO be non empty OrthoRelStr;
attr PO is Orthocomplemented means
ex f being Function of PO,PO st f
= the Compl of PO & f OrthoComplement_on PO;
end;
theorem
for PO being non empty OrthoRelStr, f being UnOp of the carrier of PO
st f OrthoComplement_on PO holds f QuasiOrthoComplement_on PO;
:: PartialOrdered (non empty OrthoRelStr)
theorem Th17:
TrivOrthoRelStr is Orthocomplemented
proof
set O = TrivOrthoRelStr;
set C = the Compl of O;
set S = the carrier of O;
reconsider f = C as Function of O,O;
f OrthoComplement_on O
proof
reconsider f = C as Function of O,O;
A1: for x being Element of S holds {x,op1.x} = {x}
by Lm2,PARTIT_2:19,ENUMSET1:29;
A2: for x being Element of O holds ex_sup_of {x,f.x},O & ex_inf_of {x,f.x}
,O & sup {x,f.x} = x & inf {x,f.x} = x
proof
let a be Element of O;
{a,f.a} = {a} by A1;
hence thesis by YELLOW_0:38,39;
end;
A3: for x being Element of O holds sup {x,f.x} in {x,f.x} & inf {x,f.x} in
{x,f.x}
proof
let a be Element of O;
sup {a,f.a} = a & inf {a,f.a} = a by A2;
hence thesis by TARSKI:def 2;
end;
A4: for x being Element of O holds x is_maximum_of {x,f.x} & x
is_minimum_of {x,f.x}
proof
let a be Element of O;
A5: sup {a,f.a} = a & ex_sup_of {a,f.a},O by A2;
sup {a,f.a} in {a,f.a} & inf {a,f.a} = a by A2,A3;
hence thesis by A5,A2,WAYBEL_1:def 6,def 7;
end;
for y being Element of O holds sup {y,f.y} is_maximum_of S & inf {y,f
.y} is_minimum_of S
proof
let a be Element of O;
reconsider a0 = a as Element of S;
{a0,f.a0} = {a0} by A1;
then
A6: {a0,f.a0} = S by TARSKI:def 1;
a is_maximum_of {a,f.a} & a is_minimum_of {a,f.a} by A4;
hence thesis by A2,A6;
end;
hence thesis by A2,Th14;
end;
hence thesis;
end;
registration
cluster TrivOrthoRelStr -> QuasiOrthocomplemented Orthocomplemented;
coherence by Th15,Th17;
end;
registration
cluster Orthocomplemented QuasiOrthocomplemented PartialOrdered for
non empty
OrthoRelStr;
correctness
proof
take TrivOrthoRelStr;
thus thesis;
end;
end;
definition
mode QuasiOrthoPoset is QuasiOrthocomplemented PartialOrdered non empty
OrthoRelStr;
mode OrthoPoset is Orthocomplemented PartialOrdered non empty OrthoRelStr;
end;