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