The abstract of the Mizar article:

Properties of Binary Relations

by

Edmund Woronowicz, and

Anna Zalewska

Received March 15, 1989

MML identifier: RELAT_2

[ Mizar article, MML identifier index ]

environ

 vocabulary RELAT_1, BOOLE, RELAT_2, FUNCT_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1;
 constructors TARSKI, RELAT_1, SUBSET_1, XBOOLE_0;
 clusters RELAT_1, ZFMISC_1, XBOOLE_0;
 requirements SUBSET;


begin

reserve X for set;
reserve a,b,c,x,y,z for set;
reserve P,R for Relation;

definition
 let R,X;
   pred R is_reflexive_in X means
:: RELAT_2:def 1

      x in X implies [x,x] in R;

   pred R is_irreflexive_in X means
:: RELAT_2:def 2

      x in X implies not [x,x] in R;

   pred R is_symmetric_in X means
:: RELAT_2:def 3

      x in X & y in X & [x,y] in R implies [y,x] in R;

   pred R is_antisymmetric_in X means
:: RELAT_2:def 4

      x in X & y in X & [x,y] in R & [y,x] in R implies x = y;

   pred R is_asymmetric_in X means
:: RELAT_2:def 5

      x in X & y in X & [x,y] in R implies not [y,x] in R;

   pred R is_connected_in X means
:: RELAT_2:def 6

      x in X & y in X & x <>y implies [x,y] in R or [y,x] in R;

   pred R is_strongly_connected_in X means
:: RELAT_2:def 7

      x in X & y in X implies [x,y] in R or [y,x] in R;

   pred R is_transitive_in X means
:: RELAT_2:def 8

      x in X & y in X & z in X & [x,y] in R & [y,z] in R implies [x,z] in R;
end;

definition
 let R;
   attr R is reflexive means
:: RELAT_2:def 9

      R is_reflexive_in field R;

   attr R is irreflexive means
:: RELAT_2:def 10

      R is_irreflexive_in field R;

   attr R is symmetric means
:: RELAT_2:def 11

      R is_symmetric_in field R;

   attr R is antisymmetric means
:: RELAT_2:def 12

      R is_antisymmetric_in field R;

   attr R is asymmetric means
:: RELAT_2:def 13

      R is_asymmetric_in field R;

   attr R is connected means
:: RELAT_2:def 14

      R is_connected_in field R;

   attr R is strongly_connected means
:: RELAT_2:def 15

      R is_strongly_connected_in field R;

   attr R is transitive means
:: RELAT_2:def 16

      R is_transitive_in field R;
end;

canceled 16;

theorem :: RELAT_2:17
    R is reflexive iff id field R c= R;

theorem :: RELAT_2:18
    R is irreflexive iff id field R misses R;

theorem :: RELAT_2:19
  R is_antisymmetric_in X iff R \ id X is_asymmetric_in X;

theorem :: RELAT_2:20
    R is_asymmetric_in X implies R \/ id X is_antisymmetric_in X;

theorem :: RELAT_2:21
    R is_antisymmetric_in X implies R \ id X is_asymmetric_in X;

theorem :: RELAT_2:22

  R is symmetric & R is transitive implies R is reflexive;

theorem :: RELAT_2:23

  id X is symmetric & id X is transitive;

theorem :: RELAT_2:24
    id X is antisymmetric & id X is reflexive;

theorem :: RELAT_2:25
    R is irreflexive & R is transitive implies R is asymmetric;

theorem :: RELAT_2:26
    R is asymmetric implies R is irreflexive & R is antisymmetric;

theorem :: RELAT_2:27

  R is reflexive implies R~ is reflexive;

theorem :: RELAT_2:28
    R is irreflexive implies R~ is irreflexive;

theorem :: RELAT_2:29
    R is reflexive implies dom R = dom(R~) & rng R = rng(R~);

theorem :: RELAT_2:30
  R is symmetric iff R = R~;

theorem :: RELAT_2:31
    P is reflexive & R is reflexive implies P \/ R is reflexive &
                                         P /\ R is reflexive;

theorem :: RELAT_2:32
    P is irreflexive & R is irreflexive implies P \/ R is irreflexive &
                                             P /\ R is irreflexive;

theorem :: RELAT_2:33
    P is irreflexive implies P \ R is irreflexive;

theorem :: RELAT_2:34
    R is symmetric implies R~ is symmetric;

theorem :: RELAT_2:35
    P is symmetric & R is symmetric implies P \/ R is symmetric &
                                          P /\ R is symmetric &
                                          P \ R is symmetric;

theorem :: RELAT_2:36
    R is asymmetric implies R~ is asymmetric;

theorem :: RELAT_2:37
    P is asymmetric & R is asymmetric implies P /\ R is asymmetric;

theorem :: RELAT_2:38
    P is asymmetric implies P \ R is asymmetric;

theorem :: RELAT_2:39
    R is antisymmetric iff R /\ (R~) c= id (dom R);

theorem :: RELAT_2:40
    R is antisymmetric implies R~ is antisymmetric;

theorem :: RELAT_2:41
    P is antisymmetric implies P /\ R is antisymmetric &
                            P \ R is antisymmetric;

theorem :: RELAT_2:42
    R is transitive implies R~ is transitive;

theorem :: RELAT_2:43
    P is transitive & R is transitive implies P /\ R is transitive;

theorem :: RELAT_2:44
    R is transitive iff R*R c= R;

theorem :: RELAT_2:45
    R is connected iff [:field R,field R:] \ id (field R) c= R \/ R~;

theorem :: RELAT_2:46
    R is strongly_connected implies R is connected &
                                  R is reflexive;

theorem :: RELAT_2:47
    R is strongly_connected iff [:field R, field R:] = R \/ R~;