:: 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 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
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 () c= R )
proof end;

theorem :: RELAT_2:2
for R being Relation holds
( R is irreflexive iff id () 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 coherence for b1 being Relation st b1 is symmetric & b1 is transitive holds b1 is reflexive proof end; end; registration let X be set ; coherence ( id X is symmetric & id X is transitive & id X is antisymmetric ) proof end; end; registration coherence for b1 being Relation st b1 is irreflexive & b1 is transitive holds b1 is asymmetric proof end; 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; coherence R ~ is reflexive proof end; end; registration let R be irreflexive Relation; 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; 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; 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;
coherence
proof end;
end;

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

registration
let R be transitive Relation;
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 [:(),():] \ (id ()) c= R \/ (R ~) ) proof end; registration 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 [:(),():] = 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;