:: Properties of Binary Relations
:: by Edmund Woronowicz and Anna Zalewska
::
:: Received March 15, 1989
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

definition

let R be Relation;
let X be set ;
pred R is_reflexive_in X means :Def1: :: RELAT_2:def 1
for x being set st x in X holds
[x,x] in R;
pred R is_irreflexive_in X means :Def2: :: RELAT_2:def 2
for x being set st x in X holds
not [x,x] in R;
pred R is_symmetric_in X means :Def3: :: RELAT_2:def 3
for x, y being set st x in X & y in X & [x,y] in R holds
[y,x] in R;
pred R is_antisymmetric_in X means :Def4: :: RELAT_2:def 4
for x, y being set st x in X & y in X & [x,y] in R & [y,x] in R holds
x = y;
pred R is_asymmetric_in X means :Def5: :: RELAT_2:def 5
for x, y being set st x in X & y in X & [x,y] in R holds
not [y,x] in R;
pred R is_connected_in X means :Def6: :: RELAT_2:def 6
for x, y being set st x in X & y in X & x <> y & not [x,y] in R holds
[y,x] in R;
pred R is_strongly_connected_in X means :Def7: :: RELAT_2:def 7
for x, y being set st x in X & y in X & not [x,y] in R holds
[y,x] in R;
pred R is_transitive_in X means :Def8: :: RELAT_2:def 8
for x, y, z being set st x in X & y in X & z in X & [x,y] in R & [y,z] in R holds
[x,z] in R;

end;

:: deftheorem Def1 defines is_reflexive_in RELAT_2:def 1 :
for R being Relation
for X being set holds
( R is_reflexive_in X iff for x being set st x in X holds
[x,x] in R );

:: deftheorem Def2 defines is_irreflexive_in RELAT_2:def 2 :
for R being Relation
for X being set holds
( R is_irreflexive_in X iff for x being set st x in X holds
not [x,x] in R );

:: deftheorem Def3 defines is_symmetric_in RELAT_2:def 3 :
for R being Relation
for X being set holds
( R is_symmetric_in X iff for x, y being set st x in X & y in X & [x,y] in R holds
[y,x] in R );

:: deftheorem Def4 defines is_antisymmetric_in RELAT_2:def 4 :
for R being Relation
for X being set holds
( R is_antisymmetric_in X iff for x, y being set st x in X & y in X & [x,y] in R & [y,x] in R holds
x = y );

:: deftheorem Def5 defines is_asymmetric_in RELAT_2:def 5 :
for R being Relation
for X being set holds
( R is_asymmetric_in X iff for x, y being set st x in X & y in X & [x,y] in R holds
not [y,x] in R );

:: deftheorem Def6 defines is_connected_in RELAT_2:def 6 :
for R being Relation
for X being set holds
( R is_connected_in X iff for x, y being set st x in X & y in X & x <> y & not [x,y] in R holds
[y,x] in R );

:: deftheorem Def7 defines is_strongly_connected_in RELAT_2:def 7 :
for R being Relation
for X being set holds
( R is_strongly_connected_in X iff for x, y being set st x in X & y in X & not [x,y] in R holds
[y,x] in R );

:: deftheorem Def8 defines is_transitive_in RELAT_2:def 8 :
for R being Relation
for X being set holds
( R is_transitive_in X iff for x, y, z being set st x in X & y in X & z in X & [x,y] in R & [y,z] in R holds
[x,z] in R );

definition

let R be Relation;
attr R is reflexive means :Def9: :: RELAT_2:def 9
R is_reflexive_in field R;
attr R is irreflexive means :Def10: :: RELAT_2:def 10
R is_irreflexive_in field R;
attr R is symmetric means :Def11: :: RELAT_2:def 11
R is_symmetric_in field R;
attr R is antisymmetric means :Def12: :: RELAT_2:def 12
R is_antisymmetric_in field R;
attr R is asymmetric means :Def13: :: RELAT_2:def 13
R is_asymmetric_in field R;
attr R is connected means :Def14: :: RELAT_2:def 14
R is_connected_in field R;
attr R is strongly_connected means :Def15: :: RELAT_2:def 15
R is_strongly_connected_in field R;
attr R is transitive means :Def16: :: RELAT_2:def 16
R is_transitive_in field R;

end;

:: deftheorem Def9 defines reflexive RELAT_2:def 9 :
for R being Relation holds
( R is reflexive iff R is_reflexive_in field R );

:: deftheorem Def10 defines irreflexive RELAT_2:def 10 :
for R being Relation holds
( R is irreflexive iff R is_irreflexive_in field R );

:: deftheorem Def11 defines symmetric RELAT_2:def 11 :
for R being Relation holds
( R is symmetric iff R is_symmetric_in field R );

:: deftheorem Def12 defines antisymmetric RELAT_2:def 12 :
for R being Relation holds
( R is antisymmetric iff R is_antisymmetric_in field R );

:: deftheorem Def13 defines asymmetric RELAT_2:def 13 :
for R being Relation holds
( R is asymmetric iff R is_asymmetric_in field R );

:: deftheorem Def14 defines connected RELAT_2:def 14 :
for R being Relation holds
( R is connected iff R is_connected_in field R );

:: deftheorem Def15 defines strongly_connected RELAT_2:def 15 :
for R being Relation holds
( R is strongly_connected iff R is_strongly_connected_in field R );

:: deftheorem Def16 defines transitive RELAT_2:def 16 :
for R being Relation holds
( R is transitive iff R is_transitive_in field R );

theorem :: RELAT_2:1

canceled;

theorem :: RELAT_2:2

canceled;

theorem :: RELAT_2:3

canceled;

theorem :: RELAT_2:4

canceled;

theorem :: RELAT_2:5

canceled;

theorem :: RELAT_2:6

canceled;

theorem :: RELAT_2:7

canceled;

theorem :: RELAT_2:8

canceled;

theorem :: RELAT_2:9

canceled;

theorem :: RELAT_2:10

canceled;

theorem :: RELAT_2:11

canceled;

theorem :: RELAT_2:12

canceled;

theorem :: RELAT_2:13

canceled;

theorem :: RELAT_2:14

canceled;

theorem :: RELAT_2:15

canceled;

theorem :: RELAT_2:16

canceled;

theorem :: RELAT_2:17

for R being Relation holds
( R is reflexive iff id (field R) c= R )

proof end;

theorem :: RELAT_2:18

for R being Relation holds
( R is irreflexive iff id (field R) misses R )

proof end;

theorem :: RELAT_2:19

for X being set
for R being Relation holds
( R is_antisymmetric_in X iff R \ (id X) is_asymmetric_in X )

proof end;

theorem :: RELAT_2:20

for X being set
for R being Relation st R is_asymmetric_in X holds
R \/ (id X) is_antisymmetric_in X

proof end;

theorem :: RELAT_2:21

canceled;

theorem Th22: :: RELAT_2:22

for R being Relation st R is symmetric & R is transitive holds
R is reflexive

proof end;

theorem Th23: :: RELAT_2:23

for X being set holds
( id X is symmetric & id X is transitive )

proof end;

theorem :: RELAT_2:24

for X being set holds
( id X is antisymmetric & id X is reflexive )

proof end;

theorem :: RELAT_2:25

for R being Relation st R is irreflexive & R is transitive holds
R is asymmetric

proof end;

theorem :: RELAT_2:26

for R being Relation st R is asymmetric holds
( R is irreflexive & R is antisymmetric )

proof end;

theorem Th27: :: RELAT_2:27

for R being Relation st R is reflexive holds
R ~ is reflexive

proof end;

theorem :: RELAT_2:28

for R being Relation st R is irreflexive holds
R ~ is irreflexive

proof end;

theorem :: RELAT_2:29

for R being Relation st R is reflexive holds
( dom R = dom (R ~) & rng R = rng (R ~) )

proof end;

theorem Th30: :: RELAT_2:30

for R being Relation holds
( R is symmetric iff R = R ~ )

proof end;

theorem :: RELAT_2:31

for P, R being Relation st P is reflexive & R is reflexive holds
( P \/ R is reflexive & P /\ R is reflexive )

proof end;

theorem :: RELAT_2:32

for P, R being Relation st P is irreflexive & R is irreflexive holds
( P \/ R is irreflexive & P /\ R is irreflexive )

proof end;

theorem :: RELAT_2:33

for P, R being Relation st P is irreflexive holds
P \ R is irreflexive

proof end;

theorem :: RELAT_2:34

for R being Relation st R is symmetric holds
R ~ is symmetric by Th30;

theorem :: RELAT_2:35

for P, R being Relation st P is symmetric & R is symmetric holds
( P \/ R is symmetric & P /\ R is symmetric & P \ R is symmetric )

proof end;

theorem :: RELAT_2:36

for R being Relation st R is asymmetric holds
R ~ is asymmetric

proof end;

theorem :: RELAT_2:37

for R, P being Relation st R is asymmetric holds
P /\ R is asymmetric

proof end;

theorem :: RELAT_2:38

for P, R being Relation st P is asymmetric holds
P \ R is asymmetric

proof end;

theorem :: RELAT_2:39

for R being Relation holds
( R is antisymmetric iff R /\ (R ~) c= id (dom R) )

proof end;

theorem :: RELAT_2:40

for R being Relation st R is antisymmetric holds
R ~ is antisymmetric

proof end;

theorem :: RELAT_2:41

for P, R being Relation st P is antisymmetric holds
( P /\ R is antisymmetric & P \ R is antisymmetric )

proof end;

theorem :: RELAT_2:42

for R being Relation st R is transitive holds
R ~ is transitive

proof end;

theorem :: RELAT_2:43

for P, R being Relation st P is transitive & R is transitive holds
P /\ R is transitive

proof end;

theorem :: RELAT_2:44

for R being Relation holds
( R is transitive iff R * R c= R )

proof end;

theorem :: RELAT_2:45

for R being Relation holds
( R is connected iff [:(field R),(field R):] \ (id (field R)) c= R \/ (R ~) )

proof end;

theorem :: RELAT_2:46

for R being Relation st R is strongly_connected holds
( R is connected & R is reflexive )

proof end;

theorem :: RELAT_2:47

for R being Relation holds
( R is strongly_connected iff [:(field R),(field R):] = R \/ (R ~) )

proof end;

theorem :: RELAT_2:48

for R being Relation holds
( R is transitive iff for x, y, z being set st [x,y] in R & [y,z] in R holds
[x,z] in R )

proof end;