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

end;
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;

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;

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;

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;

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;

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;

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

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

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

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

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

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

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

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

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

:: deftheorem Def9 defines reflexive RELAT_2:def 9 :

for R being Relation holds

( R is reflexive iff R is_reflexive_in field R );

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

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

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

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

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

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

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

for R being Relation holds

( R is transitive iff R is_transitive_in field R );

registration

for b_{1} being Relation st b_{1} is empty holds

( b_{1} is reflexive & b_{1} is irreflexive & b_{1} is symmetric & b_{1} is antisymmetric & b_{1} is asymmetric & b_{1} is connected & b_{1} is strongly_connected & b_{1} is transitive )
end;

cluster empty Relation-like -> reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive for set ;

coherence for b

( b

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 )

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

for R being Relation st R is_asymmetric_in X holds

R \/ (id X) is_antisymmetric_in X

proof end;

::$CT 7

registration

coherence

for b_{1} being Relation st b_{1} is symmetric & b_{1} is transitive holds

b_{1} is reflexive

end;
for b

b

proof end;

registration

let X be set ;

coherence

( id X is symmetric & id X is transitive & id X is antisymmetric )

end;
coherence

( id X is symmetric & id X is transitive & id X is antisymmetric )

proof end;

registration

coherence

for b_{1} being Relation st b_{1} is irreflexive & b_{1} is transitive holds

b_{1} is asymmetric

for b_{1} being Relation st b_{1} is asymmetric holds

( b_{1} is irreflexive & b_{1} is antisymmetric )

end;
for b

b

proof end;

coherence for b

( b

proof end;

registration
end;

registration
end;

registration

let P, R be reflexive Relation;

coherence

P \/ R is reflexive

P /\ R is reflexive

end;
coherence

P \/ R is reflexive

proof end;

coherence P /\ R is reflexive

proof end;

registration

let P, R be irreflexive Relation;

coherence

P \/ R is irreflexive

P /\ R is irreflexive

end;
coherence

P \/ R is irreflexive

proof end;

coherence P /\ R is irreflexive

proof end;

registration
end;

registration
end;

registration

let P, R be symmetric Relation;

coherence

P \/ R is symmetric

P /\ R is symmetric

P \ R is symmetric

end;
coherence

P \/ R is symmetric

proof end;

coherence P /\ R is symmetric

proof end;

coherence P \ R is symmetric

proof end;

registration
end;

registration

let P be Relation;

let R be asymmetric Relation;

coherence

P /\ R is asymmetric

R /\ P is asymmetric ;

end;
let R be asymmetric Relation;

coherence

P /\ R is asymmetric

proof end;

coherence R /\ P is asymmetric ;

registration
end;

::$CT 8

registration

let P be antisymmetric Relation;

let R be Relation;

coherence

P /\ R is antisymmetric

R /\ P is antisymmetric ;

coherence

P \ R is antisymmetric

end;
let R be Relation;

coherence

P /\ R is antisymmetric

proof end;

coherence R /\ P is antisymmetric ;

coherence

P \ R is antisymmetric

proof end;

registration
end;

::$CT 4

theorem :: RELAT_2:28

for R being Relation holds

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

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

proof end;

registration

coherence

for b_{1} being Relation st b_{1} is strongly_connected holds

( b_{1} is connected & b_{1} is reflexive )

end;
for b

( b

proof end;

::$CT

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 )

( 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;