:: Properties of Binary Relations
:: by Edmund Woronowicz and Anna Zalewska
::
:: Received March 15, 1989
:: Copyright (c) 1990 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;