:: Some Properties of Binary Relations :: by Waldemar Korczy\'nski :: :: Received January 17, 1992 :: Copyright (c) 1992-2012 Association of Mizar Users begin Lm1: for X, Y being set st X <> {} & Y <> {} holds ( dom [:X,Y:] = X & rng [:X,Y:] = Y ) by RELAT_1:160; theorem Th1: :: SYSREL:1 for X, Y being set for R being Relation holds ( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y ) proofend; theorem :: SYSREL:2 for X, Y being set for R being Relation st X misses Y holds dom (R /\ [:X,Y:]) misses rng (R /\ [:X,Y:]) proofend; theorem Th3: :: SYSREL:3 for X, Y being set for R being Relation st R c= [:X,Y:] holds ( dom R c= X & rng R c= Y ) proofend; theorem :: SYSREL:4 for X, Y being set for R being Relation st R c= [:X,Y:] holds R ~ c= [:Y,X:] proofend; theorem :: SYSREL:5 for X, Y being set holds [:X,Y:] ~ = [:Y,X:] proofend; theorem Th6: :: SYSREL:6 for R, S, T being Relation holds (R \/ S) * T = (R * T) \/ (S * T) proofend; theorem :: SYSREL:7 for X, Y, x, y being set for R being Relation holds ( ( 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 ) ) ) proofend; theorem Th8: :: SYSREL:8 for X, Y, Z being set for R being Relation st R c= [:X,Y:] holds ( R | Z = R /\ [:Z,Y:] & Z |` R = R /\ [:X,Z:] ) proofend; theorem :: SYSREL:9 for X, Y, Z, W being set for R being Relation st R c= [:X,Y:] & X = Z \/ W holds R = (R | Z) \/ (R | W) proofend; theorem :: SYSREL:10 for X, Y being set for R being Relation st X misses Y & R c= [:X,Y:] \/ [:Y,X:] holds R | X c= [:X,Y:] proofend; theorem :: SYSREL:11 for R, S being Relation st R c= S holds R ~ c= S ~ proofend; Lm2: for X being set holds id X c= [:X,X:] proofend; theorem Th12: :: SYSREL:12 for X being set holds (id X) * (id X) = id X proofend; theorem :: SYSREL:13 for x being set holds id {x} = {[x,x]} proofend; theorem Th14: :: SYSREL:14 for X, Y being set holds ( id (X \/ Y) = (id X) \/ (id Y) & id (X /\ Y) = (id X) /\ (id Y) & id (X \ Y) = (id X) \ (id Y) ) proofend; theorem Th15: :: SYSREL:15 for X, Y being set st X c= Y holds id X c= id Y proofend; theorem :: SYSREL:16 for X, Y being set holds (id (X \ Y)) \ (id X) = {} proofend; theorem :: SYSREL:17 for R being Relation st R c= id (dom R) holds R = id (dom R) proofend; theorem :: SYSREL:18 for X being set for R being Relation st id X c= R \/ (R ~) holds ( id X c= R & id X c= R ~ ) proofend; theorem :: SYSREL:19 for X being set for R being Relation st id X c= R holds id X c= R ~ proofend; :: CLOSURE RELATION theorem :: SYSREL:20 for X being set for R being Relation st R c= [:X,X:] holds ( R \ (id (dom R)) = R \ (id X) & R \ (id (rng R)) = R \ (id X) ) proofend; theorem :: SYSREL:21 for X being set for R being Relation holds ( ( (id X) * (R \ (id X)) = {} implies dom (R \ (id X)) = (dom R) \ X ) & ( (R \ (id X)) * (id X) = {} implies rng (R \ (id X)) = (rng R) \ X ) ) proofend; theorem Th22: :: SYSREL:22 for R being Relation holds ( ( 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 ) ) proofend; theorem :: SYSREL:23 for R being Relation holds ( ( 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) ) ) by Th22, XBOOLE_1:28; theorem :: SYSREL:24 for X being set for R being Relation holds ( ( R * (R \ (id X)) = {} implies R * (R \ (id (rng R))) = {} ) & ( (R \ (id X)) * R = {} implies (R \ (id (dom R))) * R = {} ) ) proofend; :: OPERATION CL definition let R be Relation; func CL R -> Relation equals :: SYSREL:def 1 R /\ (id (dom R)); correctness coherence R /\ (id (dom R)) is Relation; ; end; :: deftheorem defines CL SYSREL:def_1_:_ for R being Relation holds CL R = R /\ (id (dom R)); theorem Th25: :: SYSREL:25 for x, y being set for R being Relation st [x,y] in CL R holds ( x in dom (CL R) & x = y ) proofend; theorem Th26: :: SYSREL:26 for R being Relation holds dom (CL R) = rng (CL R) proofend; theorem Th27: :: SYSREL:27 for x being set for R being Relation holds ( ( x in dom (CL R) implies ( x in dom R & [x,x] in R ) ) & ( x in dom R & [x,x] in R implies x in dom (CL R) ) & ( x in rng (CL R) implies ( x in dom R & [x,x] in R ) ) & ( x in dom R & [x,x] in R implies x in rng (CL R) ) & ( x in rng (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in rng (CL R) ) & ( x in dom (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in dom (CL R) ) ) proofend; theorem Th28: :: SYSREL:28 for R being Relation holds CL R = id (dom (CL R)) proofend; theorem Th29: :: SYSREL:29 for x, y being set for R being Relation holds ( ( 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) ) ) ) proofend; theorem :: SYSREL:30 for x, y being set for R being Relation holds ( ( 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) ) ) ) proofend; theorem :: SYSREL:31 for R being Relation holds ( ( 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 ) ) ) proofend; theorem Th32: :: SYSREL:32 for R being Relation holds ( dom (CL R) c= dom R & rng (CL R) c= rng R & rng (CL R) c= dom R & dom (CL R) c= rng R ) proofend; theorem :: SYSREL:33 for R being Relation holds ( id (dom (CL R)) c= id (dom R) & id (rng (CL R)) c= id (dom R) ) proofend; theorem Th34: :: SYSREL:34 for R being Relation holds ( id (dom (CL R)) c= R & id (rng (CL R)) c= R ) proofend; theorem Th35: :: SYSREL:35 for X being set for R being Relation holds ( ( 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 ) ) proofend; theorem :: SYSREL:36 for R being Relation holds ( ( (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)) ) ) ) proofend; theorem :: SYSREL:37 for R being Relation holds ( ( 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))) = {} ) ) proofend; theorem Th38: :: SYSREL:38 for S, R being Relation holds ( ( 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 = {} ) ) proofend; theorem Th39: :: SYSREL:39 for S, R being Relation holds ( ( 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 ) ) proofend; theorem :: SYSREL:40 for S, R being Relation holds ( ( 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 ) ) proofend;