Volume 4, 1992

University of Bialystok

Copyright (c) 1992 Association of Mizar Users

### The abstract of the Mizar article:

### Some Properties of Binary Relations

**by****Waldemar Korczynski**- Received January 17, 1992
- MML identifier: SYSREL

- [ Mizar article, MML identifier index ]

environ vocabulary RELAT_1, BOOLE, SYSREL, FUNCT_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1; constructors TARSKI, RELSET_1, XBOOLE_0; clusters RELAT_1, ZFMISC_1, XBOOLE_0; requirements BOOLE, SUBSET; begin reserve x,y,z,t,X,Y,Z,W for set; reserve R,S,T for Relation; definition let X,Y; cluster [:X,Y:] -> Relation-like; end; canceled 11; theorem :: SYSREL:12 X <> {} & Y <> {} implies dom [:X,Y:] = X & rng [:X,Y:] = Y; theorem :: SYSREL:13 dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y; theorem :: SYSREL:14 X misses Y implies dom (R /\ [:X,Y:]) misses rng (R /\ [:X,Y:]) & dom (R~ /\ [:X,Y:]) misses rng (R~ /\ [:X,Y:]); theorem :: SYSREL:15 R c= [:X,Y:] implies dom R c= X & rng R c= Y; theorem :: SYSREL:16 R c= [:X,Y:] implies R~ c= [:Y,X:]; canceled; theorem :: SYSREL:18 [:X,Y:]~ = [:Y,X:]; canceled; theorem :: SYSREL:20 (R \/ S) * T = (R * T) \/ (S * T) & R * (S \/ T) = (R * S) \/ (R * T); canceled; theorem :: SYSREL:22 (X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in X implies not x in Y & not y in X & y in Y) & (X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in Y implies not y in X & not x in Y & x in X) & (X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y implies not x in X & not y in Y & y in X) & (X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X implies not x in X & not y in Y & x in Y); canceled; theorem :: SYSREL:24 (R c= [:X,Y:] & Z c= X implies (R|Z) = R /\ [:Z,Y:]) & (R c= [:X,Y:] & Z c= Y implies (Z|R) = R /\ [:X,Z:]); theorem :: SYSREL:25 R c= [:X,Y:] & X = Z \/ W implies R = (R|Z) \/ (R|W); theorem :: SYSREL:26 X misses Y & R c= [:X,Y:] \/ [:Y,X:] implies R|X c= [:X,Y:]; theorem :: SYSREL:27 R c= S implies R~ c= S~; canceled; theorem :: SYSREL:29 id(X) * id(X) = id(X); theorem :: SYSREL:30 id({x}) = {[x,x]}; theorem :: SYSREL:31 [x,y] in id(X) iff [y,x] in id(X); theorem :: SYSREL:32 id(X \/ Y) = id(X) \/ id(Y) & id(X /\ Y) = id(X) /\ id(Y) & id(X \ Y) = id(X) \ id(Y); theorem :: SYSREL:33 X c= Y implies id(X) c= id(Y); theorem :: SYSREL:34 id(X \ Y) \ id(X) = {}; theorem :: SYSREL:35 R c= id(dom R) implies R = id(dom R); theorem :: SYSREL:36 id(X) c= R \/ R~ implies id(X) c= R & id(X) c= R~; theorem :: SYSREL:37 id(X) c= R implies id(X) c= R~; :: CLOSURE RELATION theorem :: SYSREL:38 R c= [:X,X:] implies R \ id(dom R) = R \ id(X) & R \ id(rng R) = R \ id(X); theorem :: SYSREL:39 (id(X) * (R \ id(X)) = {} implies dom (R \ id(X)) = dom R \ dom (id(X))) & ((R \ id(X)) * id(X) = {} implies rng (R \ id(X)) = rng R \ rng (id(X))); theorem :: SYSREL:40 (R c= R * R & R * (R \ id(rng(R))) = {} implies id(rng(R)) c= R) & (R c= R * R & (R \ id(dom(R))) * R = {} implies id(dom(R)) c= R); theorem :: SYSREL:41 (R c= R * R & R * (R \ id(rng(R))) = {} implies R /\ (id(rng(R))) = id(rng(R))) & (R c= R * R & (R \ id(dom(R))) * R = {} implies R /\ (id(dom(R))) = id(dom(R))); theorem :: SYSREL:42 (R * (R \ id(X)) = {} & rng R c= X implies R * (R \ id(rng R)) = {}) & ((R \ id(X)) * R = {} & dom R c= X implies (R \ id(dom R)) * R = {}); :: OPERATION CL definition let R; func CL(R) -> Relation equals :: SYSREL:def 1 R /\ id(dom R); end; theorem :: SYSREL:43 CL(R) c= R & CL(R) c= id(dom R); theorem :: SYSREL:44 [x,y] in CL(R) implies x in dom( CL(R)) & x = y; theorem :: SYSREL:45 dom(CL(R)) = rng(CL(R)); theorem :: SYSREL:46 (x in dom(CL(R)) iff x in dom R & [x,x] in R) & (x in rng(CL(R)) iff x in dom R & [x,x] in R) & (x in rng(CL(R)) iff x in rng R & [x,x] in R) & (x in dom(CL(R)) iff x in rng R & [x,x] in R); theorem :: SYSREL:47 CL(R) = id(dom CL(R)); theorem :: SYSREL:48 (R * R = R & R * (R \ CL(R)) = {} & [x,y] in R & x <> y implies x in (dom R \ dom(CL(R))) & y in dom(CL(R))) & (R * R = R & (R \ CL(R)) * R = {} & [x,y] in R & x <> y implies y in (rng R \ dom(CL(R))) & x in dom(CL(R))); theorem :: SYSREL:49 (R * R = R & R * (R \ id(dom R)) = {} & [x,y] in R & x <> y implies x in ((dom R) \ dom(CL(R))) & y in dom(CL(R))) & (R * R = R & (R \ id(dom R)) * R = {} & [x,y] in R & x <> y implies y in ((rng R) \ dom(CL(R))) & x in dom(CL(R))); theorem :: SYSREL:50 (R * R = R & R * (R \ id(dom R)) = {} implies dom(CL(R)) = rng(R) & rng(CL(R)) = rng(R)) & (R * R = R & (R \ id(dom R)) * R = {} implies dom(CL(R)) = dom(R) & rng(CL(R)) = dom(R)); theorem :: SYSREL:51 dom(CL(R)) c= dom R & rng(CL(R)) c= rng R & rng(CL(R)) c= dom R & dom(CL(R)) c= rng R; theorem :: SYSREL:52 id(dom(CL(R))) c= id(dom R) & id(rng(CL(R))) c= id(dom R); theorem :: SYSREL:53 id(dom(CL(R))) c= R & id(rng(CL(R))) c= R; theorem :: SYSREL:54 (id(X) c= R & id(X) * (R \ id(X)) = {} implies R|X = id(X)) & (id(X) c= R & (R \ id(X)) * id(X) = {} implies X|R = id(X)); theorem :: SYSREL:55 (id(dom(CL(R))) * (R \ id(dom(CL(R)))) = {} implies R|(dom(CL(R))) = id(dom(CL(R))) & R|(rng(CL(R))) = id(dom(CL(R)))) & ((R \ id(rng(CL(R)))) * id(rng(CL(R))) = {} implies (dom(CL(R)))|R = id(dom(CL(R))) & (rng(CL(R)))|R = id(rng(CL(R)))); theorem :: SYSREL:56 (R * (R \ id(dom R)) = {} implies id(dom(CL(R))) * (R \ id(dom(CL(R)))) = {}) & ((R \ id(dom R)) * R = {} implies (R \ id(dom(CL(R)))) * id(dom(CL(R))) = {}); theorem :: SYSREL:57 (S * R = S & R * (R \ id(dom R)) = {} implies S * (R \ id(dom R)) = {}) & (R * S = S & (R \ id(dom R)) * R = {} implies (R \ id(dom R)) * S = {}); theorem :: SYSREL:58 (S * R = S & R * (R \ id(dom R)) = {} implies CL(S) c= CL(R)) & (R * S = S & (R \ id(dom R)) * R = {} implies CL(S) c= CL(R)); theorem :: SYSREL:59 (S * R = S & R * (R \ id(dom R)) = {} & R * S = R & S * (S \ id(dom S)) = {} implies CL(S) = CL(R)) & (R * S = S & (R \ id(dom R)) * R = {} & S * R = R & (S \ id(dom S)) * S = {} implies CL(S) = CL(R));

Back to top