:: Properties of Binary Relations
:: by Edmund Woronowicz and Anna Zalewska
::
:: Received March 15, 1989
:: Copyright (c) 1990-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies RELAT_1, TARSKI, XBOOLE_0, ZFMISC_1, RELAT_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1;
constructors TARSKI, SUBSET_1, RELAT_1, XTUPLE_0;
registrations RELAT_1, XBOOLE_0;
requirements BOOLE, SUBSET;
begin
reserve X for set, a,b,c,x,y,z for object;
reserve P,R for Relation;
definition
let R,X;
pred R is_reflexive_in X means
:: RELAT_2:def 1
x in X implies [x,x] in R;
pred R is_irreflexive_in X means
:: RELAT_2:def 2
x in X implies not [x,x] in R;
pred R is_symmetric_in X means
:: RELAT_2:def 3
x in X & y in X & [x,y] in R implies [ y,x] in R;
pred R is_antisymmetric_in X means
:: RELAT_2:def 4
x in X & y in X & [x,y] in R & [y, x] in R implies x = y;
pred R is_asymmetric_in X means
:: RELAT_2:def 5
x in X & y in X & [x,y] in R implies not [y,x] in R;
pred R is_connected_in X means
:: RELAT_2:def 6
x in X & y in X & x <>y implies [x,y] in R or [y,x] in R;
pred R is_strongly_connected_in X means
:: RELAT_2:def 7
x in X & y in X implies [x,y] in R or [y,x] in R;
pred R is_transitive_in X means
:: RELAT_2:def 8
x in X & y in X & z in X & [x,y] in R & [y,z] in R implies [x,z] in R;
end;
definition
let R;
attr R is reflexive means
:: RELAT_2:def 9
R is_reflexive_in field R;
attr R is irreflexive means
:: RELAT_2:def 10
R is_irreflexive_in field R;
attr R is symmetric means
:: RELAT_2:def 11
R is_symmetric_in field R;
attr R is antisymmetric means
:: RELAT_2:def 12
R is_antisymmetric_in field R;
attr R is asymmetric means
:: 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
:: RELAT_2:def 16
R is_transitive_in field R;
end;
registration
cluster empty -> reflexive irreflexive symmetric antisymmetric asymmetric
connected strongly_connected transitive for Relation;
end;
theorem :: RELAT_2:1
R is reflexive iff id field R c= R;
theorem :: RELAT_2:2
R is irreflexive iff id field R misses R;
theorem :: RELAT_2:3
R is_antisymmetric_in X iff R \ id X is_asymmetric_in X;
theorem :: RELAT_2:4
R is_asymmetric_in X implies R \/ id X is_antisymmetric_in X;
::$CT 7
registration
cluster symmetric transitive -> reflexive for Relation;
end;
registration
let X;
cluster id X -> symmetric transitive antisymmetric;
end;
registration
cluster irreflexive transitive -> asymmetric for Relation;
cluster asymmetric -> irreflexive antisymmetric for Relation;
end;
registration
let R be reflexive Relation;
cluster R~ -> reflexive;
end;
registration
let R be irreflexive Relation;
cluster R~ -> irreflexive;
end;
theorem :: RELAT_2:12
R is reflexive implies dom R = dom(R~) & rng R = rng(R~);
theorem :: RELAT_2:13
R is symmetric iff R = R~;
registration
let P,R be reflexive Relation;
cluster P \/ R -> reflexive;
cluster P /\ R -> reflexive;
end;
registration
let P,R be irreflexive Relation;
cluster P \/ R -> irreflexive;
cluster P /\ R -> irreflexive;
end;
registration
let P be irreflexive Relation;
let R be Relation;
cluster P \ R -> irreflexive;
end;
registration
let R be symmetric Relation;
cluster R~ -> symmetric;
end;
registration
let P,R be symmetric Relation;
cluster P \/ R -> symmetric;
cluster P /\ R -> symmetric;
cluster P \ R -> symmetric;
end;
registration
let R be asymmetric Relation;
cluster R~ -> asymmetric;
end;
registration
let P be Relation;
let R be asymmetric Relation;
cluster P /\ R -> asymmetric;
cluster R /\ P -> asymmetric;
end;
registration
let P be asymmetric Relation;
let R be Relation;
cluster P \ R -> asymmetric;
end;
::$CT 8
theorem :: RELAT_2:22
R is antisymmetric iff R /\ (R~) c= id (dom R);
registration
let R be antisymmetric Relation;
cluster R~ -> antisymmetric;
end;
registration
let P be antisymmetric Relation;
let R be Relation;
cluster P /\ R -> antisymmetric;
cluster R /\ P -> antisymmetric;
cluster P \ R -> antisymmetric;
end;
registration
let R be transitive Relation;
cluster R~ -> transitive;
end;
registration
let P,R be transitive Relation;
cluster P /\ R -> transitive;
end;
::$CT 4
theorem :: RELAT_2:27
R is transitive iff R*R c= R;
theorem :: RELAT_2:28
R is connected iff [:field R,field R:] \ id (field R) c= R \/ R~;
registration
cluster strongly_connected -> connected reflexive for Relation;
end;
::$CT
theorem :: RELAT_2:30
R is strongly_connected iff [:field R, field R:] = R \/ R~;
theorem :: RELAT_2:31
R is transitive iff for x,y,z st [x,y] in R & [y,z] in R holds [x,z] in R;