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;