Volume 15, 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

### The abstract of the Mizar article:

### Basic Notions and Properties of Orthoposets

**by****Markus Moschner**- Received February 11, 2003
- 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;

Back to top