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


definition
let R be Relation;
let X be set ;
pred R is_reflexive_in X means :Def1: :: RELAT_2:def 1
 for x being object st x in X holds
[x,x] in R;
pred R is_irreflexive_in X means :Def2: :: RELAT_2:def 2
 for x being object 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 object 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 object 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 :: RELAT_2:def 5
 for x, y being object 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 object 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 object 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 object 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 object 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 object 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 object 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 object st x in X & y in X & [x,y] in R & [y,x] in R holds
x = y );

:: deftheorem 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 object 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 object 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 object 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 object 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 :: 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 :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 defines connected RELAT_2:def 14 :
for R being Relation holds
( R is connected iff R is_connected_in field R );

:: deftheorem 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 );

registration
cluster empty Relation-like -> reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive for set ;
coherence
for b1 being Relation st b1 is empty holds
( b1 is reflexive & b1 is irreflexive & b1 is symmetric & b1 is antisymmetric & b1 is asymmetric & b1 is connected & b1 is strongly_connected & b1 is transitive )
proof end;
end;

theorem :: RELAT_2:1
for R being Relation holds
( R is reflexive iff id (field R) c= R )
proof end;

theorem :: RELAT_2:2
for R being Relation holds
( R is irreflexive iff id (field R) misses R )
proof end;

theorem :: RELAT_2:3
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:4
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: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;

::$CT 7
registration
cluster Relation-like symmetric transitive -> reflexive for set ;
coherence
for b1 being Relation st b1 is symmetric & b1 is transitive holds
b1 is reflexive
proof end;
end;

registration
let X be set ;
cluster id X -> symmetric antisymmetric transitive ;
coherence
( id X is symmetric & id X is transitive & id X is antisymmetric )
proof end;
end;

registration
cluster Relation-like irreflexive transitive -> asymmetric for set ;
coherence
for b1 being Relation st b1 is irreflexive & b1 is transitive holds
b1 is asymmetric
proof end;
cluster Relation-like asymmetric -> irreflexive antisymmetric for set ;
coherence
for b1 being Relation st b1 is asymmetric holds
( b1 is irreflexive & b1 is antisymmetric )
proof end;
end;

registration
let R be reflexive Relation;
cluster R ~ -> reflexive ;
coherence
R ~ is reflexive
proof end;
end;

registration
let R be irreflexive Relation;
cluster R ~ -> irreflexive ;
coherence
R ~ is irreflexive
proof end;
end;

theorem :: RELAT_2:12
for R being Relation st R is reflexive holds
( dom R = dom (R ~) & rng R = rng (R ~) )
proof end;

theorem Th6: :: RELAT_2:13
for R being Relation holds
( R is symmetric iff R = R ~ )
proof end;

registration
let P, R be reflexive Relation;
cluster P \/ R -> reflexive ;
coherence
P \/ R is reflexive
proof end;
cluster P /\ R -> reflexive ;
coherence
P /\ R is reflexive
proof end;
end;

registration
let P, R be irreflexive Relation;
cluster P \/ R -> irreflexive ;
coherence
P \/ R is irreflexive
proof end;
cluster P /\ R -> irreflexive ;
coherence
P /\ R is irreflexive
proof end;
end;

registration
let P be irreflexive Relation;
let R be Relation;
cluster P \ R -> irreflexive ;
coherence
P \ R is irreflexive
proof end;
end;

registration
let R be symmetric Relation;
cluster R ~ -> symmetric ;
coherence
R ~ is symmetric by Th6;
end;

registration
let P, R be symmetric Relation;
cluster P \/ R -> symmetric ;
coherence
P \/ R is symmetric
proof end;
cluster P /\ R -> symmetric ;
coherence
P /\ R is symmetric
proof end;
cluster P \ R -> symmetric ;
coherence
P \ R is symmetric
proof end;
end;

registration
let R be asymmetric Relation;
cluster R ~ -> asymmetric ;
coherence
R ~ is asymmetric
proof end;
end;

registration
let P be Relation;
let R be asymmetric Relation;
cluster P /\ R -> asymmetric ;
coherence
P /\ R is asymmetric
proof end;
cluster R /\ P -> asymmetric ;
coherence
R /\ P is asymmetric ;
end;

registration
let P be asymmetric Relation;
let R be Relation;
cluster P \ R -> asymmetric ;
coherence
P \ R is asymmetric
proof end;
end;

theorem :: RELAT_2:14
canceled;

theorem :: RELAT_2:15
canceled;

theorem :: RELAT_2:16
canceled;

theorem :: RELAT_2:17
canceled;

theorem :: RELAT_2:18
canceled;

theorem :: RELAT_2:19
canceled;

theorem :: RELAT_2:20
canceled;

theorem :: RELAT_2:21
canceled;

::$CT 8
theorem :: RELAT_2:22
for R being Relation holds
( R is antisymmetric iff R /\ (R ~) c= id (dom R) )
proof end;

registration
let R be antisymmetric Relation;
cluster R ~ -> antisymmetric ;
coherence
R ~ is antisymmetric
proof end;
end;

registration
let P be antisymmetric Relation;
let R be Relation;
cluster P /\ R -> antisymmetric ;
coherence
P /\ R is antisymmetric
proof end;
cluster R /\ P -> antisymmetric ;
coherence
R /\ P is antisymmetric ;
cluster P \ R -> antisymmetric ;
coherence
P \ R is antisymmetric
proof end;
end;

registration
let R be transitive Relation;
cluster R ~ -> transitive ;
coherence
R ~ is transitive
proof end;
end;

registration
let P, R be transitive Relation;
cluster P /\ R -> transitive ;
coherence
P /\ R is transitive
proof end;
end;

theorem :: RELAT_2:23
canceled;

theorem :: RELAT_2:24
canceled;

theorem :: RELAT_2:25
canceled;

theorem :: RELAT_2:26
canceled;

::$CT 4
theorem :: RELAT_2:27
for R being Relation holds
( R is transitive iff R * R c= R )
proof end;

theorem :: RELAT_2:28
for R being Relation holds
( R is connected iff [:(field R),(field R):] \ (id (field R)) c= R \/ (R ~) )
proof end;

registration
cluster Relation-like strongly_connected -> reflexive connected for set ;
coherence
for b1 being Relation st b1 is strongly_connected holds
( b1 is connected & b1 is reflexive )
proof end;
end;

theorem :: RELAT_2:29
canceled;

::$CT
theorem :: RELAT_2:30
for R being Relation holds
( R is strongly_connected iff [:(field R),(field R):] = R \/ (R ~) )
proof end;

theorem :: RELAT_2:31
for R being Relation holds
( R is transitive iff for x, y, z being object st [x,y] in R & [y,z] in R holds
[x,z] in R )
proof end;