The Mizar article:

Basic Notions and Properties of Orthoposets

by
Markus Moschner

Received February 11, 2003

Copyright (c) 2003 Association of Mizar Users

MML identifier: OPOSET_1
[ 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;
 definitions RELAT_2, STRUCT_0;
 theorems FUNCT_1, FUNCT_2, LATTICE3, ORDERS_1, PARTIT_2, RELAT_1, RELAT_2,
      RELSET_1, TARSKI, TOLER_1, WAYBEL_0, WAYBEL_1, XBOOLE_0, XBOOLE_1,
      YELLOW_0, ZFMISC_1, ENUMSET1, SYSREL, NECKLACE, REALSET1;

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 :Def1:
    {};
  correctness by RELSET_1:25;
  func [#](A,B) -> Relation of A,B equals
      [:A,B:];
  correctness by RELSET_1:def 1;
end;

theorem Th1:
  field id X = X
  proof
    dom id X = X & rng id X = X by RELAT_1:71;
    then field id X = X \/ X by RELAT_1:def 6;
    hence thesis;
  end;

theorem Th2:
  id {{}} = {[{},{}]} by SYSREL:30;

theorem Th3:
  op1 = {[{},{}]}
  proof
    op1 c= [:{{}},{{}}:];
    then A1: op1 c= {[{},{}]} by ZFMISC_1:35;
    A2: {{}} = dom op1 by FUNCT_2:def 1;
    rng op1 = {op1.{}} by FUNCT_2:62;
    then A3: op1.{} = {} by ZFMISC_1:24;
    {} in dom op1 by A2,TARSKI:def 1;
    then [{},op1.{}] in op1 by FUNCT_1:def 4;
    then {[{},op1.{}]} c= op1 by ZFMISC_1:37;
    hence thesis by A1,A3,XBOOLE_0:def 10;
  end;

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;
    assume A1: a <= b;
    A2: b is_>=_than {a,b}
    proof
        for x being Element of R st x in {a,b} holds x <= b
        by A1,TARSKI:def 2;
      hence thesis by LATTICE3:def 9;
    end;
    A3: a is_<=_than {a,b}
    proof
      for x being Element of {a,b} holds x >= a
      proof
        let a0 be Element of {a,b};
          a <= a0 or a <= a0 by A1,TARSKI:def 2;
        hence thesis;
      end;
      then for x being Element of R st x in {a,b} holds x >= a;
      hence thesis by LATTICE3:def 8;
    end;
    A4: for x being Element of R st x is_>=_than {a,b} holds b <= x
    proof
      let a0 be Element of R;
      assume A5: a0 is_>=_than {a,b};
      a0 >= a & a0 >= b
      proof
        A6: a in {a,b} by TARSKI:def 2;
        b in {a,b} by TARSKI:def 2;
        hence thesis by A5,A6,LATTICE3:def 9;
      end;
      hence thesis;
    end;
    for x being Element of R st x is_<=_than {a,b} holds a >= x
    proof
      let a0 be Element of R;
      assume A7: a0 is_<=_than {a,b};
      a0 <= a & a0 <= b
      proof
        A8: a in {a,b} by TARSKI:def 2;
        b in {a,b} by TARSKI:def 2;
        hence thesis by A7,A8,LATTICE3:def 8;
      end;
      hence thesis;
    end;
    hence thesis by A2,A3,A4,YELLOW_0:30,31;
  end;

:: for various types of relations needed for Posets

theorem
  for R being Relation holds dom R c= field R & rng R c= field R
    by RELAT_1:29;

theorem Th6:
  for A,B being set holds field {}(A,B) = {}
  proof
    let A,B being set;
    A1: {}(A,B) = {} by Def1;
    then dom {}(A,B) \/ rng {}(A,B) = rng {}(A,B) by RELAT_1:60;
    hence thesis by A1,RELAT_1:60,def 6;
  end;

theorem Th7:
  R is_reflexive_in X implies R is reflexive & field R = X
  proof
    assume A1: R is_reflexive_in X;
    then X = field R by PARTIT_2:9;
    hence thesis by A1,RELAT_2:def 9;
  end;

theorem Th8:
  R is_symmetric_in X implies R is symmetric
  proof
    assume A1: R is_symmetric_in X;
A2: field R c= X \/ X by RELSET_1:19;
    let x,y be set;
    assume A3: x in field R;
    assume A4: y in field R;
    assume [x,y] in R;
    hence thesis by A1,A2,A3,A4,RELAT_2:def 3;
  end;

theorem Th9:
  R is symmetric & field R c= S implies R is_symmetric_in S
  proof
    assume R is symmetric & field R c= S;
    then A1: R is_symmetric_in field R by RELAT_2:def 11;
    let x,y be set;
    assume x in S & y in S;
    assume A2: [x,y] in R;
    then x in field R & y in field R by RELAT_1:30;
    hence thesis by A1,A2,RELAT_2:def 3;
  end;

theorem Th10:
  R is antisymmetric & field R c= S implies R is_antisymmetric_in S
  proof
    assume R is antisymmetric & field R c= S;
    then A1: R is_antisymmetric_in field R by RELAT_2:def 12;
    let x,y be set;
    assume x in S & y in S;
    assume A2: [x,y] in R;
    assume A3: [y,x] in R;
    x in field R & y in field R by A2,RELAT_1:30;
    hence thesis by A1,A2,A3,RELAT_2:def 4;
  end;

theorem Th11:
  R is_antisymmetric_in X implies R is antisymmetric
  proof
    assume A1: R is_antisymmetric_in X;
A2: field R c= X \/ X by RELSET_1:19;
    let x,y be set;
    assume A3: x in field R;
    assume A4: y in field R;
    assume [x,y] in R & [y,x] in R;
    hence thesis by A1,A2,A3,A4,RELAT_2:def 4;
  end;

theorem Th12:
  R is transitive & field R c= S implies R is_transitive_in S
  proof
    assume R is transitive & field R c= S;
    then A1: R is_transitive_in field R by RELAT_2:def 16;
    let x,y,z be set;
    assume x in S & y in S & z in S;
    assume A2: [x,y] in R;
    assume A3: [y,z] in R;
    then x in field R & y in field R & z in field R by A2,RELAT_1:30;
    hence thesis by A1,A2,A3,RELAT_2:def 8;
  end;

theorem Th13:
  R is_transitive_in X implies R is transitive
  proof
    assume A1: R is_transitive_in X;
A2: field R c= X \/ X by RELSET_1:19;
    let x,y,z be set;
    assume A3: x in field R;
    assume A4: y in field R;
    assume A5: z in field R;
    assume [x,y] in R & [y,z] in R;
    hence thesis by A1,A2,A3,A4,A5,RELAT_2:def 8;
  end;

theorem Th14:
   R is asymmetric & field R c= S implies R is_asymmetric_in S
   proof
    assume R is asymmetric & field R c= S;
    then A1: R is_asymmetric_in field R by RELAT_2:def 13;
    let x,y be set;
    assume x in S & y in S;
    assume A2: [x,y] in R;
    then x in field R & y in field R by RELAT_1:30;
    hence thesis by A1,A2,RELAT_2:def 5;
  end;

theorem Th15:
  R is_asymmetric_in X implies R is asymmetric
  proof
    assume A1: R is_asymmetric_in X;
A2: field R c= X \/ X by RELSET_1:19;
    let x,y be set;
    assume A3: x in field R;
    assume A4: y in field R;
    assume [x,y] in R;
    hence thesis by A1,A2,A3,A4,RELAT_2:def 5;
  end;

theorem Th16:
  R is irreflexive & field R c= S implies R is_irreflexive_in S
  proof
    assume A1: R is irreflexive & field R c= S;
    then A2: R is_irreflexive_in field R by RELAT_2:def 10;
    let x be set;
    assume A3: x in S;
      S = field R \/ ( S \ (field R) ) by A1,XBOOLE_1:45;
    then A4: x in S implies x in field R or ( x in S \ (field R) )
         by XBOOLE_0:def 2;
      x in S \ (field R) implies not [x,x] in R
    proof
      assume x in S \ (field R);
      then x in S \ (dom R \/ rng R) by RELAT_1:def 6;
      then x in (S \ dom R) /\ (S \ rng R) by XBOOLE_1:53;
      then x in (S \ dom R) & x in (S \ rng R) by XBOOLE_0:def 3;
      then x in S & not x in dom R & not x in rng R by XBOOLE_0:def 4;
      hence thesis by RELAT_1:def 5;
    end;
    hence thesis by A2,A3,A4,RELAT_2:def 2;
  end;

theorem Th17:
  R is_irreflexive_in X implies R is irreflexive
  proof
    assume A1: R is_irreflexive_in X;
  field R c= X \/ X by RELSET_1:19;
    then for x being set holds x in field R implies not [x,x] in R
      by A1,RELAT_2:def 2;
    then R is_irreflexive_in field R by RELAT_2:def 2;
    hence thesis by RELAT_2:def 10;
  end;

:: Some existence conditions on non-empty relations

definition let X be set;
  cluster irreflexive asymmetric transitive Relation of X;
  existence
   proof
     {}(X,X) = {} by Def1;
     hence thesis by TOLER_1:4,6,9;
   end;
end;

canceled;

definition let X, R;
  let C be UnOp of X;
  cluster OrthoRelStr(#X,R,C#) -> non empty;
  coherence
  proof
    thus the carrier of OrthoRelStr(#X,R,C#) is non empty;
  end;
end;

definition
  cluster non empty strict OrthoRelStr;
  existence
  proof
    consider X be non empty set, R be (Relation of X), C be UnOp of X;
    take OrthoRelStr(#X,R,C#);
    thus thesis;
  end;
end;

:: Double negation property of the internal Complement

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

theorem Th19:
  op1 is dneg
  proof
    let a be Element of {{}};
    a = {} by TARSKI:def 1;
    hence thesis by FUNCT_2:65;
  end;

theorem Th20:
  id X is dneg
  proof
    set f = id X;
    for x being Element of X holds f.(f.x) = x
    proof
      let a be Element of X;
      f.a = a by FUNCT_1:34;
      hence thesis;
    end;
    hence thesis by Def3;
  end;

definition let O be non empty OrthoRelStr;
  canceled;
  cluster dneg map of O,O;
  existence
  proof
    set C = the carrier of O;
    reconsider g = id C as Function of C,C;
    reconsider g as map of O,O;
    g is dneg by Th20;
    hence thesis;
  end;
end;

:: Small example structures

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

Lm1: TrivOrthoRelStr is trivial
  proof
    the carrier of TrivOrthoRelStr is trivial by Def5, REALSET1:def 12;
    hence thesis by REALSET1:def 13;
  end;

definition
  cluster TrivOrthoRelStr -> non empty trivial;
  coherence by Def5, Lm1;
end;

definition
  func TrivAsymOrthoRelStr -> strict OrthoRelStr equals :Def6:
       OrthoRelStr (# {{}}, {}({{}},{{}}), op1 #);
  coherence;
end;

definition
  cluster TrivAsymOrthoRelStr -> non empty;
  coherence by Def6;
end;

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

theorem Th21:
  TrivOrthoRelStr is Dneg by Def5,Th19,Def7;

definition
  cluster TrivOrthoRelStr -> Dneg;
  coherence by Th21;
end;

definition
  cluster Dneg (non empty OrthoRelStr);
  existence by Th21;
end;

:: InternalRel based properties

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

 reserve O for non empty RelStr;

theorem
  O is reflexive implies O is SubReFlexive
  proof
    set RO = the InternalRel of O;
    assume O is reflexive;
    then RO is_reflexive_in the carrier of O by ORDERS_1:def 4;
    then RO is reflexive by Th7;
    hence thesis by Def10;
  end;

theorem Th23:
  TrivOrthoRelStr is reflexive
  proof
A1: id {{}} is_reflexive_in (field id {{}}) by RELAT_2:def 9;
A2: dom id {{}} = {{}} by RELAT_1:71;
A3: rng id {{}} = {{}} by RELAT_1:71;
    field id {{}} = dom id {{}} \/ rng id {{}} by RELAT_1:def 6;
    hence thesis by A1,A2,A3,Def5,ORDERS_1:def 4;
end;

definition
  cluster TrivOrthoRelStr -> reflexive;
  coherence by Th23;
end;

definition
  cluster reflexive strict (non empty OrthoRelStr);
  existence by Th23;
end;

definition let O;
  attr O is SubIrreFlexive means :Def12:
       the InternalRel of O is irreflexive;
  redefine attr O is irreflexive means :Def13:
    the InternalRel of O is_irreflexive_in the carrier of O;
  compatibility
  proof
    thus O is irreflexive implies
      the InternalRel of O is_irreflexive_in the carrier of O
    proof
      assume O is irreflexive; then
      for x being set st x in the carrier of O holds
      not [x,x] in the InternalRel of O by NECKLACE:def 6;
      hence thesis by RELAT_2:def 2;
    end;
    assume the InternalRel of O is_irreflexive_in the carrier of O; then
    for x being set st x in the carrier of O holds
      not [x,x] in the InternalRel of O by RELAT_2:def 2;
    hence thesis by NECKLACE:def 6;
  end;
end;

theorem Th24:
  O is irreflexive implies O is SubIrreFlexive
  proof
    set RO = the InternalRel of O;
    assume O is irreflexive;
    then RO is_irreflexive_in the carrier of O by Def13;
    then RO is irreflexive by Th17;
    hence thesis by Def12;
  end;

theorem Th25:
  TrivAsymOrthoRelStr is irreflexive
  proof
    set IntRel = {}({{}},{{}});
    for x being set st x in {{}} holds not [x,x] in IntRel by Def1;
    then IntRel is_irreflexive_in {{}} by RELAT_2:def 2;
    hence thesis by Def6,Def13;
end;

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

definition
  cluster TrivAsymOrthoRelStr -> irreflexive;
  coherence by Th25;
end;

definition
  cluster irreflexive strict (non empty OrthoRelStr);
  existence by Th25;
end;

:: Symmetry

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

theorem Th26:
  O is symmetric implies O is SubSymmetric
  proof
    set RO = the InternalRel of O;
    assume O is symmetric;
    then RO is_symmetric_in the carrier of O by NECKLACE:def 4;
    then RO is symmetric by Th8;
    hence thesis by Def14;
  end;

theorem Th27:
  TrivOrthoRelStr is symmetric
  proof
    field id {{}} = {{}} by Th1;
    then id {{}} is_symmetric_in {{}} by Th9;
    hence thesis by Def5,NECKLACE:def 4;
  end;

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

definition
  cluster symmetric strict (non empty OrthoRelStr);
  existence by Th27;
end;

:: Antisymmetry

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

theorem Th28:
  O is antisymmetric implies O is SubAntisymmetric
  proof
    set RO = the InternalRel of O;
    assume O is antisymmetric;
    then RO is_antisymmetric_in the carrier of O by ORDERS_1:def 6;
    then RO is antisymmetric by Th11;
    hence thesis by Def16;
  end;

theorem Th29:
  TrivOrthoRelStr is antisymmetric;

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

definition
  cluster TrivOrthoRelStr -> symmetric;
  coherence by Th27;
end;

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

:: Asymmetry

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

theorem Th30:
  O is Asymmetric implies O is asymmetric
  proof
    set RO = the InternalRel of O;
    assume O is Asymmetric;
    then RO is_asymmetric_in the carrier of O by Def19;
    then RO is asymmetric by Th15;
    hence thesis by NECKLACE:def 5;
  end;

theorem Th31:
  TrivAsymOrthoRelStr is Asymmetric
  proof
    set IntRel = {}({{}},{{}});
    A1: field IntRel = {} by Th6;
    A2:IntRel is asymmetric by Def1,TOLER_1:6;
    field IntRel c= {{}} by A1,XBOOLE_1:2;
    then IntRel is_asymmetric_in {{}} by A2,Th14;
    hence thesis by Def6,Def19;
end;

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

definition
  cluster TrivAsymOrthoRelStr -> Asymmetric;
  coherence by Th31;
end;

definition
  cluster Asymmetric strict (non empty OrthoRelStr);
  existence by Th31;
end;

:: Transitivity

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

theorem Th32:
  O is transitive implies O is SubTransitive
  proof
    set RO = the InternalRel of O;
    set CO = the carrier of O;
    assume O is transitive;
    then RO is_transitive_in CO by ORDERS_1:def 5;
    then RO is transitive by Th13;
    hence thesis by Def20;
  end;

theorem
  TrivOrthoRelStr is transitive;

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

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

theorem Th34:
  TrivAsymOrthoRelStr is transitive
  proof
    set IntRel = the InternalRel of TrivAsymOrthoRelStr;
    A1: IntRel is transitive by Def1,Def6,TOLER_1:9;
    field IntRel = {} by Def6,Th6;
    then field IntRel c= {{}} by XBOOLE_1:2;
    then IntRel is_transitive_in {{}} by A1,Th12;
    hence thesis by Def6,ORDERS_1:def 5;
  end;

definition
  cluster TrivAsymOrthoRelStr -> irreflexive Asymmetric transitive;
  coherence by Th34;
end;

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

theorem
  O is SubSymmetric SubTransitive implies O is SubReFlexive
  proof
    set R = the InternalRel of O;
    assume A1: O is SubSymmetric & O is SubTransitive;
    then A2: R is symmetric by Def14;
      R is transitive by A1,Def20;
    then R is reflexive by A2,RELAT_2:22;
    hence thesis by Def10;
  end;

theorem
  O is SubIrreFlexive SubTransitive implies O is asymmetric
  proof
    assume A1: O is SubIrreFlexive & O is SubTransitive;
    set R = the InternalRel of O;
    A2: R is irreflexive by A1,Def12;
    R is transitive by A1,Def20;
    then R is asymmetric by A2,RELAT_2:25;
    hence thesis by NECKLACE:def 5;
  end;

theorem Th37:
  O is asymmetric implies O is SubIrreFlexive
  proof
    assume A1: O is asymmetric;
    set R = the InternalRel of O;
      R is asymmetric by A1,NECKLACE:def 5;
    then R is irreflexive by RELAT_2:26;
    hence thesis by Def12;
  end;

theorem Th38:
  O is reflexive SubSymmetric implies O is symmetric
  proof
    assume A1: O is reflexive SubSymmetric;
    set IntRel = the InternalRel of O;
    set CO = the carrier of O;
    A2: IntRel is_reflexive_in CO by A1,ORDERS_1:def 4;
    A3: IntRel is symmetric by A1,Def14;
      CO = field IntRel by A2,Th7;
    then IntRel is_symmetric_in CO by A3,Th9;
    hence thesis by NECKLACE:def 4;
  end;

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

theorem Th39:
  O is reflexive SubAntisymmetric implies O is antisymmetric
  proof
    assume A1: O is reflexive SubAntisymmetric;
    set IntRel = the InternalRel of O;
    set CO = the carrier of O;
    A2: IntRel is_reflexive_in CO by A1,ORDERS_1:def 4;
    A3: IntRel is antisymmetric by A1,Def16;
    CO = field IntRel by A2,Th7;
    then IntRel is_antisymmetric_in CO by A3,Th10;
    hence thesis by ORDERS_1:def 6;
  end;

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

theorem Th40:
  O is reflexive SubTransitive implies O is transitive
  proof
    assume A1: O is reflexive SubTransitive;
    set IntRel = the InternalRel of O;
    set CO = the carrier of O;
    A2: IntRel is_reflexive_in CO by A1,ORDERS_1:def 4;
    A3: IntRel is transitive by A1,Def20;
    CO = field IntRel by A2,Th7;
    then IntRel is_transitive_in CO by A3,Th12;
    hence thesis by ORDERS_1:def 5;
  end;

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

theorem Th41:
  O is irreflexive SubTransitive implies O is transitive
  proof
    assume A1: O is irreflexive SubTransitive;
    set IntRel = the InternalRel of O;
    set CO = the carrier of O;
    A2: field IntRel c= CO \/ CO by RELSET_1:19;
    IntRel is transitive by A1,Def20;
    then IntRel is_transitive_in CO by A2,Th12;
    hence thesis by ORDERS_1:def 5;
  end;

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

theorem Th42:
  O is irreflexive asymmetric implies O is Asymmetric
  proof
    assume A1: O is irreflexive asymmetric;
    set IntRel = the InternalRel of O;
    set CO = the carrier of O;
    A2: field IntRel c= CO \/ CO by RELSET_1:19;
    IntRel is asymmetric by A1,NECKLACE:def 5;
    then IntRel is_asymmetric_in CO by A2,Th14;
    hence thesis by Def19;
  end;

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

begin
:: Quasiorder (Preorder)

definition let O;
  attr O is SubQuasiOrdered means :Def22:
       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 :Def23:
       O is reflexive transitive;
  synonym O is Quasiordered;
  synonym O is PreOrdered;
  synonym O is Preordered;
end;

theorem Th43:
  O is QuasiOrdered implies O is SubQuasiOrdered
  proof
    assume A1: O is QuasiOrdered;
    set IntRel = the InternalRel of O;
    set CO = the carrier of O;
    A2: O is reflexive & O is transitive by A1,Def23;
    then IntRel is_reflexive_in CO by ORDERS_1:def 4;
    then A3: IntRel is reflexive & field IntRel = CO by Th7;
    IntRel is_transitive_in CO by A2,ORDERS_1:def 5;
    then A4: IntRel is transitive by Th13;
    A5: O is SubReFlexive by A3,Def10;
    O is SubTransitive by A4,Def20;
    hence thesis by A5,Def22;
  end;

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

definition
  cluster TrivOrthoRelStr -> QuasiOrdered;
  coherence by Def23;
end;

 reserve O for non empty OrthoRelStr;

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

definition
  cluster QuasiPure Dneg QuasiOrdered strict (non empty OrthoRelStr);
  existence
  proof
    TrivOrthoRelStr is QuasiPure by Def24;
    hence thesis;
  end;
end;

definition
  cluster TrivOrthoRelStr -> QuasiPure;
  coherence by Def24;
end;

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

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

definition let O;
  attr O is PartialOrdered means :Def26:
       O is reflexive antisymmetric transitive;
  synonym O is Partialordered;
end;

theorem Th44:
  O is SubPartialOrdered iff O is PartialOrdered
  proof
    set IntRel = the InternalRel of O;
    set CO = the carrier of O;
    A1: O is SubPartialOrdered implies O is PartialOrdered
    proof
      assume O is SubPartialOrdered;
      then A2: O is reflexive & O is SubAntisymmetric & O is SubTransitive
           by Def25;
      then IntRel is_reflexive_in CO by ORDERS_1:def 4;
      then A3: field IntRel = CO by Th7;
        IntRel is antisymmetric by A2,Def16;
      then IntRel is_antisymmetric_in CO by A3,Th10;
      then A4: O is antisymmetric by ORDERS_1:def 6;
      IntRel is transitive by A2,Def20;
      then IntRel is_transitive_in CO by A3,Th12;
      then O is transitive by ORDERS_1:def 5;
      hence thesis by A2,A4,Def26;
    end;
    O is PartialOrdered implies O is SubPartialOrdered
    proof
      assume O is PartialOrdered;
      then A5: O is reflexive & O is antisymmetric & O is transitive
           by Def26;
      then A6: O is SubAntisymmetric by Th28;
      O is SubTransitive by A5,Th32;
      hence thesis by A5,A6,Def25;
    end;
    hence thesis by A1;
  end;

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

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

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

definition
  cluster Pure Dneg PartialOrdered strict (non empty OrthoRelStr);
  existence
  proof
    TrivOrthoRelStr is Pure by Def27;
    hence thesis;
  end;
end;

definition
  cluster TrivOrthoRelStr -> Pure;
  coherence by Def27;
end;

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

:: Strict Poset
definition let O;
  attr O is SubStrictPartialOrdered means :Def28:
       O is asymmetric SubTransitive;
end;

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

theorem Th45:
  O is StrictPartialOrdered implies O is SubStrictPartialOrdered
  proof
    assume O is StrictPartialOrdered;
    then A1: O is Asymmetric transitive by Def29;
    then A2: O is asymmetric by Th30;
    O is SubTransitive by A1,Th32;
    hence thesis by A2,Def28;
  end;

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

theorem Th46:
  O is SubStrictPartialOrdered implies O is SubIrreFlexive
  proof
    assume O is SubStrictPartialOrdered;
    then O is asymmetric SubTransitive by Def28;
    hence thesis by Th37;
  end;

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

theorem Th47:
  O is irreflexive SubStrictPartialOrdered implies O is StrictPartialOrdered
  proof
    assume A1: O is irreflexive SubStrictPartialOrdered;
    then A2: O is asymmetric SubTransitive by Def28;
    then A3: O is Asymmetric by A1,Th42;
    O is transitive by A1,A2,Th41;
    hence thesis by A3,Def29;
  end;

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

theorem Th48:
  O is StrictPartialOrdered implies O is irreflexive
  proof
    set IntRel = the InternalRel of O;
    set CO = the carrier of O;
    assume O is StrictPartialOrdered;
    then O is Asymmetric by Def29;
    then O is asymmetric by Th30;
    then O is SubIrreFlexive by Th37;
    then A1: IntRel is irreflexive by Def12;
    field IntRel c= CO \/ CO by RELSET_1:19;
    then IntRel is_irreflexive_in CO by A1,Th16;
    hence thesis by Def13;
  end;

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

definition
  cluster TrivAsymOrthoRelStr -> irreflexive StrictPartialOrdered;
  coherence by Def29;
end;

definition
  cluster irreflexive StrictPartialOrdered (non empty strict OrthoRelStr);
  existence
  proof
    TrivAsymOrthoRelStr is StrictPartialOrdered;
    hence thesis;
  end;
end;

:: Quasiorder to Partial Order

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

theorem
  QO is SubAntisymmetric implies QO is PartialOrdered
  proof
    assume A1: QO is SubAntisymmetric;
    A2: QO is reflexive & QO is transitive by Def23;
    then QO is antisymmetric by A1,Th39;
    hence thesis by A2,Def26;
  end;

theorem Th50:
  PO is Poset;

definition
  cluster PartialOrdered -> reflexive transitive antisymmetric
          (non empty OrthoRelStr);
  correctness by Th50;
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 :Def33:
       f is dneg map of PO,PO & f is antitone map of PO,PO;
end;

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

theorem Th51:
  the Compl of TrivOrthoRelStr is Orderinvolutive
  proof
    set O = TrivOrthoRelStr;
    set C = the Compl of O;
    A1: C is dneg map of O,O by Def5,Th19;
    reconsider Emp = {} as Element of O by Def5,TARSKI:def 1;
    C is antitone map of O,O
    proof
      reconsider f = C as map 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 Def5,FUNCT_2:65;
        then f.a2 <= b1 by Def5,FUNCT_2:65;
        hence thesis;
      end;
      hence thesis by WAYBEL_0:def 5;
    end;
    hence thesis by A1,Def33;
  end;

definition
  cluster TrivOrthoRelStr -> OrderInvolutive;
  coherence by Th51,Def34;
end;

definition
   cluster OrderInvolutive Pure (PartialOrdered (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;
           let f be UnOp of the carrier of PO;
  pred f QuasiOrthoComplement_on PO means :Def35:
     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 :Def36:
       ex f being map of PO,PO st
          f = the Compl of PO & f QuasiOrthoComplement_on PO;
end;

theorem Th52:
  TrivOrthoRelStr is QuasiOrthocomplemented
  proof
    set O = TrivOrthoRelStr;
    set C = the Compl of O;
    set S = the carrier of O;
    A1: C QuasiOrthoComplement_on O
    proof
A2:  for x being Element of S holds {x,op1.x} = {x}
      proof
        let a be Element of S;
          a = op1.a by Def5,Th2,Th3,FUNCT_1:34;
        hence thesis by ENUMSET1:69;
      end;
      reconsider f = C as map of O,O;
        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;
        A3: {a,f.a} = {a} by A2,Def5;
        A4: sup {a,f.a} = a & ex_sup_of {a,f.a},O
        proof
          thus thesis by A3,YELLOW_0:38,39;
        end;
        inf {a,f.a} = a & ex_inf_of {a,f.a},O
        proof
          thus thesis by A3,YELLOW_0:38,39;
        end;
        hence thesis by A4;
      end;
      hence thesis by Def35,Th51;
    end;
    reconsider f = C as map of O,O;
      f QuasiOrthoComplement_on O by A1;
    hence thesis by Def36;
  end;

definition let PO;
           let f be UnOp of the carrier of PO;
  pred f OrthoComplement_on PO means :Def37:
       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 :Def38:
       ex f being map of PO,PO st
          f = the Compl of PO & f OrthoComplement_on PO;
  synonym PO is Ocompl;
end;

theorem
  for f being UnOp of the carrier of PO holds
  f OrthoComplement_on PO implies f QuasiOrthoComplement_on PO
  proof
    let g be UnOp of the carrier of PO;
    assume A1: g OrthoComplement_on PO;
    then A2: for x being Element of PO holds
      ex_sup_of {x,g.x},PO & ex_inf_of {x,g.x},PO by Def37;
      g is Orderinvolutive by A1,Def37;
    hence thesis by A2,Def35;
  end;

:: PartialOrdered (non empty OrthoRelStr)

theorem Th54:
  TrivOrthoRelStr is Orthocomplemented
  proof
    set O = TrivOrthoRelStr;
    set C = the Compl of O;
    set S = the carrier of O;
    reconsider f = C as map of O,O;
    f OrthoComplement_on O
    proof
      A1: for x being Element of S holds {x,op1.x} = {x}
      proof
        let a be Element of S;
          a = op1.a by Def5,Th2,Th3,FUNCT_1:34;
        hence thesis by ENUMSET1:69;
      end;
      reconsider f = C as map of O,O;
      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;
        A3: {a,f.a} = {a} by A1,Def5;
        A4: ex_sup_of {a,f.a},O & sup {a,f.a} = a
        proof
          {a,f.a} = {a} by A1,Def5;
          hence thesis by YELLOW_0:38,39;
        end;
        ex_inf_of {a,f.a},O & inf {a,f.a} = a
        proof
          thus thesis by A3,YELLOW_0:38,39;
        end;
        hence thesis by A4;
      end;
      A5: 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;
        A6: sup {a,f.a} = a by A2;
          inf {a,f.a} = a by A2;
        hence thesis by A6,TARSKI:def 2;
      end;
      A7: 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;
        A8: sup {a,f.a} = a & ex_sup_of {a,f.a},O by A2;
        A9: sup {a,f.a} in {a,f.a} by A5;
        inf {a,f.a} = a & ex_inf_of {a,f.a},O by A2;
        hence thesis by A8,A9,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;
        A10: a is_maximum_of {a,f.a} by A7;
        A11: a is_minimum_of {a,f.a} by A7;
        reconsider a0 = a as Element of S;
        {a0,f.a0} = {a0} by A1,Def5;
        then {a0,f.a0} = S by Def5,TARSKI:def 1;
        hence thesis by A2,A10,A11;
      end;
      hence thesis by A2,Def37,Th51;
    end;
    hence thesis by Def38;
  end;

definition
  cluster TrivOrthoRelStr -> QuasiOrthocomplemented Orthocomplemented;
  coherence by Th52,Th54;
end;

definition
  cluster Orthocomplemented QuasiOrthocomplemented
      (PartialOrdered (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;


Back to top