:: Basic Notions and Properties of Orthoposets :: by Markus Moschner :: :: Received February 11, 2003 :: Copyright (c) 2003-2018 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, NUMERALS; definitions RELAT_2, ORDERS_2, NECKLACE, STRUCT_0; 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 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 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 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 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 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 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;