Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Properties of Binary Relations

by
Edmund Woronowicz, and
Anna Zalewska

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~;
```