Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Properties of Binary Relations

**by****Edmund Woronowicz, and****Anna Zalewska**- Received March 15, 1989
- MML identifier: RELAT_2

- [ Mizar article, MML identifier index ]

environ vocabulary RELAT_1, BOOLE, RELAT_2, FUNCT_1; notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1; constructors TARSKI, RELAT_1, SUBSET_1, XBOOLE_0; clusters RELAT_1, ZFMISC_1, XBOOLE_0; requirements SUBSET; begin reserve X for set; reserve a,b,c,x,y,z for set; 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; canceled 16; theorem :: RELAT_2:17 R is reflexive iff id field R c= R; theorem :: RELAT_2:18 R is irreflexive iff id field R misses R; theorem :: RELAT_2:19 R is_antisymmetric_in X iff R \ id X is_asymmetric_in X; theorem :: RELAT_2:20 R is_asymmetric_in X implies R \/ id X is_antisymmetric_in X; theorem :: RELAT_2:21 R is_antisymmetric_in X implies R \ id X is_asymmetric_in X; theorem :: RELAT_2:22 R is symmetric & R is transitive implies R is reflexive; theorem :: RELAT_2:23 id X is symmetric & id X is transitive; theorem :: RELAT_2:24 id X is antisymmetric & id X is reflexive; theorem :: RELAT_2:25 R is irreflexive & R is transitive implies R is asymmetric; theorem :: RELAT_2:26 R is asymmetric implies R is irreflexive & R is antisymmetric; theorem :: RELAT_2:27 R is reflexive implies R~ is reflexive; theorem :: RELAT_2:28 R is irreflexive implies R~ is irreflexive; theorem :: RELAT_2:29 R is reflexive implies dom R = dom(R~) & rng R = rng(R~); theorem :: RELAT_2:30 R is symmetric iff R = R~; theorem :: RELAT_2:31 P is reflexive & R is reflexive implies P \/ R is reflexive & P /\ R is reflexive; theorem :: RELAT_2:32 P is irreflexive & R is irreflexive implies P \/ R is irreflexive & P /\ R is irreflexive; theorem :: RELAT_2:33 P is irreflexive implies P \ R is irreflexive; theorem :: RELAT_2:34 R is symmetric implies R~ is symmetric; theorem :: RELAT_2:35 P is symmetric & R is symmetric implies P \/ R is symmetric & P /\ R is symmetric & P \ R is symmetric; theorem :: RELAT_2:36 R is asymmetric implies R~ is asymmetric; theorem :: RELAT_2:37 P is asymmetric & R is asymmetric implies P /\ R is asymmetric; theorem :: RELAT_2:38 P is asymmetric implies P \ R is asymmetric; theorem :: RELAT_2:39 R is antisymmetric iff R /\ (R~) c= id (dom R); theorem :: RELAT_2:40 R is antisymmetric implies R~ is antisymmetric; theorem :: RELAT_2:41 P is antisymmetric implies P /\ R is antisymmetric & P \ R is antisymmetric; theorem :: RELAT_2:42 R is transitive implies R~ is transitive; theorem :: RELAT_2:43 P is transitive & R is transitive implies P /\ R is transitive; theorem :: RELAT_2:44 R is transitive iff R*R c= R; theorem :: RELAT_2:45 R is connected iff [:field R,field R:] \ id (field R) c= R \/ R~; theorem :: RELAT_2:46 R is strongly_connected implies R is connected & R is reflexive; theorem :: RELAT_2:47 R is strongly_connected iff [:field R, field R:] = R \/ R~;

Back to top