:: Relations and Their Basic Properties :: by Edmund Woronowicz :: :: Received March 15, 1989 :: Copyright (c) 1990-2021 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 XBOOLE_0, TARSKI, ZFMISC_1, SUBSET_1, RELAT_1, VALUED_1; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1; constructors TARSKI, SUBSET_1, ZFMISC_1, XTUPLE_0, XBOOLE_0; registrations XBOOLE_0, ZFMISC_1, XTUPLE_0; requirements SUBSET, BOOLE; begin reserve A,X,X1,X2,Y,Y1,Y2 for set, a,b,c,d,x,y,z for object; definition let IT be set; attr IT is Relation-like means :: RELAT_1:def 1 x in IT implies ex y,z st x = [y,z]; end; registration cluster empty -> Relation-like for set; end; definition mode Relation is Relation-like set; end; reserve P,P1,P2,Q,R,S for Relation; registration let R be Relation; cluster -> Relation-like for Subset of R; end; scheme :: RELAT_1:sch 1 RelExistence{A,B() -> set, P[object,object]}: ex R being Relation st for x,y holds [x,y] in R iff x in A() & y in B() & P[x,y]; definition let P,R; redefine pred P = R means :: RELAT_1:def 2 for a,b holds [a,b] in P iff [a,b] in R; end; registration let P,X; cluster P /\ X -> Relation-like; cluster P \ X -> Relation-like; end; registration let P,R; cluster P \/ R -> Relation-like; end; registration let R,S be Relation; cluster R \+\ S -> Relation-like; end; registration let a, b be object; cluster {[a,b]} -> Relation-like; end; registration let a, b be set; cluster [:a,b:] -> Relation-like; end; registration let a, b, c, d be object; cluster {[a,b],[c,d]} -> Relation-like; end; definition let P,A; redefine pred P c= A means :: RELAT_1:def 3 for a,b holds [a,b] in P implies [a,b] in A; end; :: DOMAIN OF RELATION notation let R be Relation; synonym dom R for proj1 R; end; :: CODOMAIN OF RELATION notation let R be Relation; synonym rng R for proj2 R; end; ::$CT 6 theorem :: RELAT_1:7 R c= [:dom R, rng R:]; theorem :: RELAT_1:8 R /\ [:dom R, rng R:] = R; theorem :: RELAT_1:9 dom {[x,y]} = {x} & rng {[x,y]} = {y}; theorem :: RELAT_1:10 dom {[a,b],[x,y]} = {a,x} & rng {[a,b],[x,y]} = {b,y}; theorem :: RELAT_1:11 P c= R implies dom P c= dom R & rng P c= rng R; theorem :: RELAT_1:12 rng(P \/ R) = rng P \/ rng R; theorem :: RELAT_1:13 rng(P /\ R) c= rng P /\ rng R; theorem :: RELAT_1:14 rng P \ rng R c= rng(P \ R); :: FIELD OF RELATION definition ::$CD 2 let R; func field R -> set equals :: RELAT_1:def 6 dom R \/ rng R; end; theorem :: RELAT_1:15 [a,b] in R implies a in field R & b in field R; theorem :: RELAT_1:16 P c= R implies field P c= field R; theorem :: RELAT_1:17 field {[x,y]} = {x,y}; theorem :: RELAT_1:18 field(P \/ R) = field P \/ field R; theorem :: RELAT_1:19 field(P /\ R) c= field P /\ field R; :: CONVERSE RELATION definition let R; func R~ -> Relation means :: RELAT_1:def 7 [x,y] in it iff [y,x] in R; involutiveness; end; theorem :: RELAT_1:20 rng R = dom(R~) & dom R = rng(R~); theorem :: RELAT_1:21 field R = field(R~); theorem :: RELAT_1:22 (P /\ R)~ = P~ /\ R~; theorem :: RELAT_1:23 (P \/ R)~ = P~ \/ R~; theorem :: RELAT_1:24 (P \ R)~ = P~ \ R~; :: COMPOSITION OF RELATIONS definition let P,R be set; func P(#)R -> Relation means :: RELAT_1:def 8 [x,y] in it iff ex z st [x,z] in P & [z,y] in R; end; notation let P,R; synonym P*R for P(#)R; end; theorem :: RELAT_1:25 dom(P*R) c= dom P; theorem :: RELAT_1:26 rng(P*R) c= rng R; theorem :: RELAT_1:27 rng R c= dom P implies dom(R*P) = dom R; theorem :: RELAT_1:28 dom P c= rng R implies rng(R*P) = rng P; theorem :: RELAT_1:29 P c= R implies Q*P c= Q*R; theorem :: RELAT_1:30 P c= Q implies P*R c= Q*R; theorem :: RELAT_1:31 P c= R & Q c= S implies P*Q c= R*S; theorem :: RELAT_1:32 P*(R \/ Q) = (P*R) \/ (P*Q); theorem :: RELAT_1:33 P*(R /\ Q) c= (P*R) /\ (P*Q); theorem :: RELAT_1:34 (P*R) \ (P*Q) c= P*(R \ Q); theorem :: RELAT_1:35 (P*R)~ = R~*P~; theorem :: RELAT_1:36 (P*R)*Q = P*(R*Q); :: EMPTY RELATION registration cluster non empty for Relation; end; registration let f be non empty Relation; cluster dom f -> non empty; cluster rng f -> non empty; end; theorem :: RELAT_1:37 (for x,y holds not [x,y] in R) implies R = {}; theorem :: RELAT_1:38 dom {} = {} & rng {} = {}; theorem :: RELAT_1:39 {}*R = {} & R*{} = {}; registration let X be empty set; cluster dom X -> empty; cluster rng X -> empty; let R; cluster X*R -> empty; cluster R*X -> empty; end; theorem :: RELAT_1:40 field {} = {}; theorem :: RELAT_1:41 dom R = {} or rng R = {} implies R = {}; theorem :: RELAT_1:42 dom R = {} iff rng R = {}; registration let X be empty set; cluster X~ -> empty; end; theorem :: RELAT_1:43 {}~ = {}; theorem :: RELAT_1:44 rng R misses dom P implies R*P = {}; definition let R be Relation; attr R is non-empty means :: RELAT_1:def 9 not {} in rng R; end; registration cluster non-empty for Relation; end; registration let R be Relation, S be non-empty Relation; cluster R*S -> non-empty; end; :: IDENTITY RELATION definition let X; func id X -> Relation means :: RELAT_1:def 10 [x,y] in it iff x in X & x = y; end; registration let X; reduce dom id X to X; reduce rng id X to X; end; theorem :: RELAT_1:45 dom id X = X & rng id X = X; registration let X; reduce (id X)~ to id X; end; theorem :: RELAT_1:46 (id X)~ = id X; theorem :: RELAT_1:47 (for x st x in X holds [x,x] in R) implies id X c= R; theorem :: RELAT_1:48 [x,y] in (id X)*R iff x in X & [x,y] in R; theorem :: RELAT_1:49 [x,y] in R*id Y iff y in Y & [x,y] in R; theorem :: RELAT_1:50 R*(id X) c= R & (id X)*R c= R; theorem :: RELAT_1:51 dom R c= X implies (id X)*R = R; theorem :: RELAT_1:52 (id dom R)*R = R; theorem :: RELAT_1:53 rng R c= Y implies R*(id Y) = R; theorem :: RELAT_1:54 R*(id rng R) = R; theorem :: RELAT_1:55 id {} = {}; theorem :: RELAT_1:56 rng P2 c= X & P2*R = id dom P1 & R*P1 = id X implies P1 = P2; definition let R,X; func R|X -> Relation means :: RELAT_1:def 11 [x,y] in it iff x in X & [x,y] in R; end; registration let R be Relation, X be empty set; cluster R|X -> empty; end; theorem :: RELAT_1:57 x in dom(R|X) iff x in X & x in dom R; theorem :: RELAT_1:58 dom(R|X) c= X; theorem :: RELAT_1:59 R|X c= R; theorem :: RELAT_1:60 dom(R|X) c= dom R; theorem :: RELAT_1:61 dom(R|X) = dom R /\ X; theorem :: RELAT_1:62 X c= dom R implies dom(R|X) = X; theorem :: RELAT_1:63 (R|X)*P c= R*P; theorem :: RELAT_1:64 P*(R|X) c= P*R; theorem :: RELAT_1:65 R|X = (id X)*R; theorem :: RELAT_1:66 R|X = {} iff dom R misses X; theorem :: RELAT_1:67 R|X = R /\ [:X,rng R:]; theorem :: RELAT_1:68 dom R c= X implies R|X = R; registration let R; reduce R|dom R to R; end; theorem :: RELAT_1:69 R|dom R = R; theorem :: RELAT_1:70 rng(R|X) c= rng R; theorem :: RELAT_1:71 (R|X)|Y = R|(X /\ Y); registration let R,X; reduce R|X|X to R|X; end; theorem :: RELAT_1:72 (R|X)|X = R|X; theorem :: RELAT_1:73 X c= Y implies (R|X)|Y = R|X; theorem :: RELAT_1:74 Y c= X implies (R|X)|Y = R|Y; theorem :: RELAT_1:75 X c= Y implies R|X c= R|Y; theorem :: RELAT_1:76 P c= R implies P|X c= R|X; theorem :: RELAT_1:77 P c= R & X c= Y implies P|X c= R|Y; theorem :: RELAT_1:78 R|(X \/ Y) = (R|X) \/ (R|Y); theorem :: RELAT_1:79 R|(X /\ Y) = (R|X) /\ (R|Y); theorem :: RELAT_1:80 R|(X \ Y) = R|X \ R|Y; registration let R be empty Relation, X be set; cluster R|X -> empty; end; theorem :: RELAT_1:81 R|{} = {}; theorem :: RELAT_1:82 {}|X = {}; theorem :: RELAT_1:83 (P*R)|X = (P|X)*R; definition let Y,R; func Y|`R -> Relation means :: RELAT_1:def 12 [x,y] in it iff y in Y & [x,y] in R; end; registration let R be Relation, X be empty set; cluster X|`R -> empty; end; theorem :: RELAT_1:84 y in rng(Y|`R) iff y in Y & y in rng R; theorem :: RELAT_1:85 rng(Y|`R) c= Y; theorem :: RELAT_1:86 Y|`R c= R; theorem :: RELAT_1:87 rng(Y|`R) c= rng R; theorem :: RELAT_1:88 rng(Y|`R) = rng R /\ Y; theorem :: RELAT_1:89 Y c= rng R implies rng(Y|`R) = Y; theorem :: RELAT_1:90 (Y|`R)*P c= R*P; theorem :: RELAT_1:91 P*(Y|`R) c= P*R; theorem :: RELAT_1:92 Y|`R = R*(id Y); theorem :: RELAT_1:93 Y|`R = R /\ [:dom R,Y:]; theorem :: RELAT_1:94 rng R c= Y implies Y|`R = R; registration let R; reduce rng R|`R to R; end; theorem :: RELAT_1:95 rng R|`R=R; theorem :: RELAT_1:96 Y|`(X|`R) = (Y /\ X)|`R; registration let Y,R; reduce Y|`(Y|`R) to Y|`R; end; theorem :: RELAT_1:97 Y|`(Y|`R) = Y|`R; theorem :: RELAT_1:98 X c= Y implies Y|`(X|`R) = X|`R; theorem :: RELAT_1:99 Y c= X implies Y|`(X|`R) = Y|`R; theorem :: RELAT_1:100 X c= Y implies X|`R c= Y|`R; theorem :: RELAT_1:101 P1 c= P2 implies Y|`P1 c= Y|`P2; theorem :: RELAT_1:102 P1 c= P2 & Y1 c= Y2 implies Y1|`P1 c= Y2|`P2; theorem :: RELAT_1:103 (X \/ Y)|`R = (X|`R) \/ (Y|`R); theorem :: RELAT_1:104 (X /\ Y)|`R = X|`R /\ Y|`R; theorem :: RELAT_1:105 (X \ Y)|`R = X|`R \ Y|`R; theorem :: RELAT_1:106 {}|`R = {}; theorem :: RELAT_1:107 Y|`{} = {}; theorem :: RELAT_1:108 Y|`(P*R) = P*(Y|`R); theorem :: RELAT_1:109 (Y|`R)|X = Y|`(R|X); :: IMAGE OF SET IN RELATION definition let R,X; func R.:X -> set means :: RELAT_1:def 13 y in it iff ex x st [x,y] in R & x in X; end; theorem :: RELAT_1:110 y in R.:X iff ex x st x in dom R & [x,y] in R & x in X; theorem :: RELAT_1:111 R.:X c= rng R; theorem :: RELAT_1:112 R.:X = R.:(dom R /\ X); theorem :: RELAT_1:113 R.:dom R = rng R; theorem :: RELAT_1:114 R.:X c= R.:(dom R); theorem :: RELAT_1:115 rng(R|X) = R.:X; registration let R; let X be empty set; cluster R.:X -> empty; end; registration let R be empty Relation; let X; cluster R.:X -> empty; end; ::$CT 2 theorem :: RELAT_1:118 R.:X = {} iff dom R misses X; theorem :: RELAT_1:119 X <> {} & X c= dom R implies R.:X <> {}; theorem :: RELAT_1:120 R.:(X \/ Y) = R.:X \/ R.:Y; theorem :: RELAT_1:121 R.:(X /\ Y) c= R.:X /\ R.:Y; theorem :: RELAT_1:122 R.:X \ R.:Y c= R.:(X \ Y); theorem :: RELAT_1:123 X c= Y implies R.:X c= R.:Y; theorem :: RELAT_1:124 P c= R implies P.:X c= R.:X; theorem :: RELAT_1:125 P c= R & X c= Y implies P.:X c= R.:Y; theorem :: RELAT_1:126 (P*R).:X = R.:(P.:X); theorem :: RELAT_1:127 rng(P*R) = R.:(rng P); theorem :: RELAT_1:128 (R|X).:Y c= R.:Y; theorem :: RELAT_1:129 for R be Relation, X, Y be set st X c= Y holds (R|Y).:X = R.:X; theorem :: RELAT_1:130 (dom R) /\ X c= (R~).:(R.:X); :: INVERSE IMAGE OF SET IN RELATION definition let R,Y; func R"Y -> set means :: RELAT_1:def 14 x in it iff ex y st [x,y] in R & y in Y; end; theorem :: RELAT_1:131 x in R"Y iff ex y st y in rng R & [x,y] in R & y in Y; theorem :: RELAT_1:132 R"Y c= dom R; theorem :: RELAT_1:133 R"Y = R"(rng R /\ Y); theorem :: RELAT_1:134 R"rng R = dom R; theorem :: RELAT_1:135 R"Y c= R"rng R; registration let R; let Y be empty set; cluster R"Y -> empty; end; registration let R be empty Relation; let Y; cluster R"Y -> empty; end; ::$CT 2 theorem :: RELAT_1:138 R"Y = {} iff rng R misses Y; theorem :: RELAT_1:139 Y <> {} & Y c= rng R implies R"Y <> {}; theorem :: RELAT_1:140 R"(X \/ Y) = R"X \/ R"Y; theorem :: RELAT_1:141 R"(X /\ Y) c= R"X /\ R"Y; theorem :: RELAT_1:142 R"X \ R"Y c= R"(X \ Y); theorem :: RELAT_1:143 X c= Y implies R"X c= R"Y; theorem :: RELAT_1:144 P c= R implies P"Y c= R"Y; theorem :: RELAT_1:145 P c= R & X c= Y implies P"X c= R"Y; theorem :: RELAT_1:146 (P*R)"Y = P"(R"Y); theorem :: RELAT_1:147 dom(P*R) = P"(dom R); theorem :: RELAT_1:148 (rng R) /\ Y c= (R~)"(R"Y); begin :: Addenda definition let R; attr R is empty-yielding means :: RELAT_1:def 15 rng R c= {{}}; end; theorem :: RELAT_1:149 R is empty-yielding iff for X st X in rng R holds X = {}; :: from AMI_3 theorem :: RELAT_1:150 for f,g being Relation, A,B being set st f|A = g|A & f|B = g|B holds f|(A \/ B) = g|(A \/ B); theorem :: RELAT_1:151 for X being set, f,g being Relation st dom g c= X & g c= f holds g c= f|X; theorem :: RELAT_1:152 for f being Relation, X being set st X misses dom f holds f|X = {}; :: from AMI_5 theorem :: RELAT_1:153 for f,g being Relation, A,B being set st A c= B & f|B = g|B holds f|A = g|A; :: missing, 2005.07.11, A.T. theorem :: RELAT_1:154 R|dom S = R|dom(S|dom R); :: missing, 2005.11.13, A.T. registration cluster empty -> empty-yielding for Relation; end; registration let R be empty-yielding Relation; let X be set; cluster R|X -> empty-yielding; end; theorem :: RELAT_1:155 R|X is non empty-yielding implies R is non empty-yielding; :: from EQREL_1 (Class), 2007.02.06 definition let R be Relation, x be object; func Im(R,x) -> set equals :: RELAT_1:def 16 R.:{x}; end; :: from YELLOW_3, 2007.06.13, A.T. scheme :: RELAT_1:sch 2 ExtensionalityR { A, B() -> Relation, P[object,object] }: A() = B() provided for a, b being object holds [a,b] in A() iff P[a,b] and for a, b being object holds [a,b] in B() iff P[a,b]; :: from SCMFSA6A, 2007.07.23, A.T. theorem :: RELAT_1:156 dom (R | (dom R \ X)) = dom R \ X; theorem :: RELAT_1:157 R | X = R | (dom R /\ X); :: missing, 2007.11.07, A.T. theorem :: RELAT_1:158 dom [:X,Y:] c= X; theorem :: RELAT_1:159 rng [:X,Y:] c= Y; :: from FUNCOP_1, 2008.02.19, A.T. theorem :: RELAT_1:160 X <> {} & Y <> {} implies dom [:X,Y:] = X & rng [:X,Y:] = Y; theorem :: RELAT_1:161 dom R = {} & dom Q = {} implies R = Q; theorem :: RELAT_1:162 rng R = {} & rng Q = {} implies R = Q; theorem :: RELAT_1:163 dom R = dom Q implies dom(S*R) = dom (S*Q); theorem :: RELAT_1:164 rng R = rng Q implies rng(R*S) = rng (Q*S); :: from RELSET_2 (R"x, generalized), 2008.07.16, A.T. definition let R be Relation, x be object; func Coim(R,x) -> set equals :: RELAT_1:def 17 R"{x}; end; :: from NECKLACE, 2008.07.25, A.T. registration let R be trivial Relation; cluster dom R -> trivial; end; registration let R be trivial Relation; cluster rng R -> trivial; end; :: comp. RFUNCT_2:34, CFCONT_1:31, 2008.08.07, A.T. theorem :: RELAT_1:165 rng R c= dom (S|X) implies R*(S|X) = R*S; :: from LATTICE2, 2008.09.14, A.T. theorem :: RELAT_1:166 Q|A = R|A implies Q.:A = R.:A; :: new, 2009.01.21, A.T definition let X,R; attr R is X-defined means :: RELAT_1:def 18 dom R c= X; attr R is X-valued means :: RELAT_1:def 19 rng R c= X; end; registration let X,Y; cluster X-defined Y-valued for Relation; end; :: from QC_LANG4, 2009.01.23, A.T theorem :: RELAT_1:167 for D being set, R being D-valued Relation for y being object st y in rng R holds y in D; :: new, 2009.02.07, A.T. registration let X,A; let R be A-valued Relation; cluster R|X -> A-valued; end; registration let X,A; let R be A-defined Relation; cluster R|X -> A-defined X-defined; end; registration let X; cluster id X -> X-defined X-valued; end; :: 2009.02.16, A.T. registration let A be set; let R be A-valued Relation, S be Relation; cluster S*R -> A-valued; end; registration let A be set; let R be A-defined Relation, S be Relation; cluster R*S -> A-defined; end; :: 2009.02.16, A.T. theorem :: RELAT_1:168 x in X implies Im([:X,Y:],x) = Y; theorem :: RELAT_1:169 [x,y] in R iff y in Im(R,x); theorem :: RELAT_1:170 x in dom R iff Im(R,x) <> {}; theorem :: RELAT_1:171 {} is X-defined Y-valued; :: 2009.10.02, A.T. registration cluster empty -> non-empty for Relation; end; registration let X be set, R be X-defined Relation; cluster -> X-defined for Subset of R; end; registration let X be set, R be X-valued Relation; cluster -> X-valued for Subset of R; end; :: missing, 2010.01.02, A.T theorem :: RELAT_1:172 X misses Y implies R|X|Y = {}; :: from AMISTD_3, 2010.01.10, A.T. theorem :: RELAT_1:173 field {[x,x]} = {x}; registration let X; let R be X-defined Relation; reduce R|X to R; end; registration let Y; let R be Y-valued Relation; reduce Y|`R to R; end; theorem :: RELAT_1:174 for R being X-defined Relation holds R = R|X; theorem :: RELAT_1:175 for S being Relation, R being X-defined Relation st R c= S holds R c= S|X; :: missing, 2010.04.07, A.T. theorem :: RELAT_1:176 dom R c= X implies R \ (R|A) = R|(X\A); theorem :: RELAT_1:177 dom(R \ (R|A)) = dom R \ A; theorem :: RELAT_1:178 dom R \ dom(R|A) = dom(R \ (R|A)); theorem :: RELAT_1:179 dom R misses dom S implies R misses S; theorem :: RELAT_1:180 rng R misses rng S implies R misses S; theorem :: RELAT_1:181 X c= Y implies (R \ R|Y)|X = {}; theorem :: RELAT_1:182 X c= Y implies for R being X-defined Relation holds R is Y-defined; theorem :: RELAT_1:183 X c= Y implies for R being X-valued Relation holds R is Y-valued; theorem :: RELAT_1:184 R c= S iff R c= S|dom R; theorem :: RELAT_1:185 for R being X-defined Y-valued Relation holds R c= [:X,Y:]; :: new, 20011.06.11, A.T. theorem :: RELAT_1:186 dom(X|`R) c= dom R; registration let A,X; let R be A-defined Relation; cluster X|`R -> A-defined; end; registration let X,A; let R be A-valued Relation; cluster X|`R -> A-valued X-valued; end; registration let X be empty set; cluster -> empty for X-defined Relation; cluster -> empty for X-valued Relation; end; :: from PNPROC_1, 2012.02.20, A.T. theorem :: RELAT_1:187 for X,Y being set, P,R being Relation st X misses Y holds P|X misses R|Y; theorem :: RELAT_1:188 for Y being set, R being Relation holds Y|`R c= R|(R"Y); theorem :: RELAT_1:189 for f being Relation, x, y st dom f = {x} & rng f = {y} holds f = { [x,y] }; registration let X,Y; sethood of X-defined Y-valued Relation; end;