The Mizar abstract of RELAT

Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users
The abstract of the Mizar article:: Relations and Their Basic Properties
by
Edmund Woronowicz
Received March 15, 1989
MML identifier: RELAT_1
[ Mizar article, MML identifier index ]
environ

 vocabulary BOOLE, TARSKI, RELAT_1, ZF_REFLE, FUNCT_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1;
 constructors TARSKI, SUBSET_1, XBOOLE_0;
 clusters XBOOLE_0, SUBSET_1, ZFMISC_1;
 requirements SUBSET, BOOLE;


begin

reserve A,X,X1,X2,Y,Y1,Y2,a,b,c,d,x,y,z for set;

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;

definition
 cluster Relation-like empty set;
end;

definition
 mode Relation is Relation-like set;
end;

reserve P,P1,P2,Q,R,S for Relation;

canceled 2;

theorem :: RELAT_1:3
  A c= R implies A is Relation-like;

theorem :: RELAT_1:4
    {[x,y]} is Relation-like;

theorem :: RELAT_1:5
    {[a,b],[c,d]} is Relation-like;

theorem :: RELAT_1:6
    [:X,Y:] is Relation-like;

scheme Rel_Existence{A,B() -> set, P[set,set]}:
  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;

definition let P,R;
 cluster P /\ R -> Relation-like;

 cluster P \/ R -> Relation-like;

 cluster P \ R -> Relation-like;
end;

definition let P,R;
 redefine pred P c= R means
:: RELAT_1:def 3
 for a,b holds [a,b] in P implies [a,b] in R;
end;

canceled 2;

theorem :: RELAT_1:9
  X /\ R is Relation;

theorem :: RELAT_1:10
    R \ X is Relation;


::             DOMAIN OF RELATION
::             __________________

definition let R;
   func dom R -> set means
:: RELAT_1:def 4
 x in it iff ex y st [x,y] in R;
 end;

canceled 2;

theorem :: RELAT_1:13
  dom(P \/ R) = dom P \/ dom R;

theorem :: RELAT_1:14
  dom(P /\ R) c= dom P /\ dom R;

theorem :: RELAT_1:15
    dom P \ dom R c= dom(P \ R);

::            CODOMAIN OF RELATION
::            ____________________

definition let R;
  func rng R -> set means
:: RELAT_1:def 5
 y in it iff ex x st [x,y] in R;
end;

canceled 2;

theorem :: RELAT_1:18
    x in dom R implies ex y st y in rng R;

theorem :: RELAT_1:19
    y in rng R implies ex x st x in dom R;

theorem :: RELAT_1:20
    [x,y] in R implies x in dom R & y in rng R;

theorem :: RELAT_1:21
  R c= [:dom R, rng R:];

theorem :: RELAT_1:22
    R /\ [:dom R, rng R:] = R;

theorem :: RELAT_1:23
  R = {[x,y]} implies dom R = {x} & rng R = {y};

theorem :: RELAT_1:24
    R = {[a,b],[x,y]} implies dom R = {a,x} & rng R = {b,y};

theorem :: RELAT_1:25
  P c= R implies dom P c= dom R & rng P c= rng R;

theorem :: RELAT_1:26
  rng(P \/ R) = rng P \/ rng R;

theorem :: RELAT_1:27
  rng(P /\ R) c= rng P /\ rng R;

theorem :: RELAT_1:28
    rng P \ rng R c= rng(P \ R);

::                  FIELD OF RELATION
::                  _________________

definition let R;
  func field R -> set equals
:: RELAT_1:def 6
 dom R \/ rng R;
end;

theorem :: RELAT_1:29
  dom R c= field R & rng R c= field R;

theorem :: RELAT_1:30
    [a,b] in R implies a in field R & b in field R;

theorem :: RELAT_1:31
    P c= R implies field P c= field R;

theorem :: RELAT_1:32
    R = {[x,y]} implies field R = {x,y};

theorem :: RELAT_1:33
    field(P \/ R) = field P \/ field R;

theorem :: RELAT_1:34
    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;

canceled 2;

theorem :: RELAT_1:37
   rng R = dom(R~) & dom R = rng(R~);

theorem :: RELAT_1:38
    field R = field(R~);

theorem :: RELAT_1:39
    (P /\ R)~ = P~ /\ R~;

theorem :: RELAT_1:40
    (P \/ R)~ = P~ \/ R~;

theorem :: RELAT_1:41
    (P \ R)~ = P~ \ R~;


::               COMPOSITION OF RELATIONS
::               ________________________

definition
 let P,R;
   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;

canceled 2;

theorem :: RELAT_1:44
  dom(P*R) c= dom P;

theorem :: RELAT_1:45
  rng(P*R) c= rng R;

theorem :: RELAT_1:46
    rng R c= dom P implies dom(R*P)=dom R;

theorem :: RELAT_1:47
    dom P c= rng R implies rng(R*P)=rng P;

theorem :: RELAT_1:48
  P c= R implies Q*P c= Q*R;

theorem :: RELAT_1:49
  P c= Q implies P*R c= Q*R;

theorem :: RELAT_1:50
    P c= R & Q c= S implies P*Q c= R*S;

theorem :: RELAT_1:51
    P*(R \/ Q) = (P*R) \/ (P*Q);

theorem :: RELAT_1:52
    P*(R /\ Q) c= (P*R) /\ (P*Q);

theorem :: RELAT_1:53
    (P*R) \ (P*Q) c= P*(R \ Q);

theorem :: RELAT_1:54
    (P*R)~ = R~*P~;

theorem :: RELAT_1:55
  (P*R)*Q = P*(R*Q);


::               EMPTY RELATION
::               ______________

definition
 cluster empty -> Relation-like set;
end;

definition
 cluster {} -> Relation-like;
end;

definition
  cluster non empty Relation;
end;

definition
 let f be non empty Relation;
 cluster dom f -> non empty;
 cluster rng f -> non empty;
end;

theorem :: RELAT_1:56
 (for x,y holds not [x,y] in R) implies R = {};

canceled 3;

theorem :: RELAT_1:60
  dom {} = {} & rng {} = {};

canceled;

theorem :: RELAT_1:62
  {}*R = {} & R*{} = {};

definition 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:63
    R*{} = {}*R;

theorem :: RELAT_1:64
  dom R = {} or rng R = {} implies R = {};

theorem :: RELAT_1:65
    dom R = {} iff rng R = {};

theorem :: RELAT_1:66
  {}~ = {};

definition let X be empty set;
 cluster X~ -> empty;
end;

theorem :: RELAT_1:67
    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;

::             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;

canceled 3;

theorem :: RELAT_1:71
  dom id X = X & rng id X = X;

theorem :: RELAT_1:72
    (id X)~ = id X;

theorem :: RELAT_1:73
    (for x st x in X holds [x,x] in R) implies id X c=R;

theorem :: RELAT_1:74
  [x,y] in (id X)*R iff x in X & [x,y] in R;

theorem :: RELAT_1:75
  [x,y] in R*id Y iff y in Y & [x,y] in R;

theorem :: RELAT_1:76
  R*(id X) c= R & (id X)*R c= R;

theorem :: RELAT_1:77
  dom R c= X implies (id X)*R = R;

theorem :: RELAT_1:78
    (id dom R)*R = R;

theorem :: RELAT_1:79
  rng R c= Y implies R*(id Y) = R;

theorem :: RELAT_1:80
    R*(id rng R) = R;

theorem :: RELAT_1:81
    id {} = {};

theorem :: RELAT_1:82
    dom R = X & 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;

canceled 3;

theorem :: RELAT_1:86
  x in dom(R|X) iff x in X & x in dom R;

theorem :: RELAT_1:87
    dom(R|X) c= X;

theorem :: RELAT_1:88
  R|X c= R;

theorem :: RELAT_1:89
    dom(R|X) c= dom R;

theorem :: RELAT_1:90
  dom(R|X) = dom R /\ X;

theorem :: RELAT_1:91
    X c= dom R implies dom(R|X) = X;

theorem :: RELAT_1:92
    (R|X)*P c= R*P;

theorem :: RELAT_1:93
    P*(R|X) c= P*R;

theorem :: RELAT_1:94
    R|X = (id X)*R;

theorem :: RELAT_1:95
    R|X = {} iff dom R misses X;

theorem :: RELAT_1:96
  R|X = R /\ [:X,rng R:];

theorem :: RELAT_1:97
  dom R c= X implies R|X = R;

theorem :: RELAT_1:98
    R|dom R = R;

theorem :: RELAT_1:99
    rng(R|X) c= rng R;

theorem :: RELAT_1:100
  (R|X)|Y = R|(X /\ Y);

theorem :: RELAT_1:101
    (R|X)|X = R|X;

theorem :: RELAT_1:102
    X c= Y implies (R|X)|Y = R|X;

theorem :: RELAT_1:103
    Y c= X implies (R|X)|Y = R|Y;

theorem :: RELAT_1:104
  X c= Y implies R|X c= R|Y;

theorem :: RELAT_1:105
  P c= R implies P|X c= R|X;

theorem :: RELAT_1:106
    P c= R & X c= Y implies P|X c= R|Y;

theorem :: RELAT_1:107
    R|(X \/ Y) = (R|X) \/ (R|Y);

theorem :: RELAT_1:108
    R|(X /\ Y) = (R|X) /\ (R|Y);

theorem :: RELAT_1:109
    R|(X \ Y) = R|X \ R|Y;

theorem :: RELAT_1:110
    R|{} = {};

theorem :: RELAT_1:111
    {}|X = {};

theorem :: RELAT_1:112
    (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;

canceled 2;

theorem :: RELAT_1:115
  y in rng(Y|R) iff y in Y & y in rng R;

theorem :: RELAT_1:116
  rng(Y|R) c= Y;

theorem :: RELAT_1:117
  Y|R c= R;

theorem :: RELAT_1:118
  rng(Y|R) c= rng R;

theorem :: RELAT_1:119
  rng(Y|R) = rng R /\ Y;

theorem :: RELAT_1:120
    Y c= rng R implies rng(Y|R) = Y;

theorem :: RELAT_1:121
    (Y|R)*P c= R*P;

theorem :: RELAT_1:122
    P*(Y|R) c= P*R;

theorem :: RELAT_1:123
    Y|R = R*(id Y);

theorem :: RELAT_1:124
  Y|R = R /\ [:dom R,Y:];

theorem :: RELAT_1:125
  rng R c= Y implies Y|R = R;

theorem :: RELAT_1:126
    rng R|R=R;

theorem :: RELAT_1:127
   Y|(X|R) = (Y /\ X)|R;

theorem :: RELAT_1:128
    Y|(Y|R) = Y|R;

theorem :: RELAT_1:129
    X c= Y implies Y|(X|R) = X|R;

theorem :: RELAT_1:130
    Y c= X implies Y|(X|R) = Y|R;

theorem :: RELAT_1:131
  X c= Y implies X|R c= Y|R;

theorem :: RELAT_1:132
  P1 c= P2 implies Y|P1 c= Y|P2;

theorem :: RELAT_1:133
    P1 c= P2 & Y1 c= Y2 implies Y1|P1 c= Y2|P2;

theorem :: RELAT_1:134
    (X \/ Y)|R = (X|R) \/ (Y|R);

theorem :: RELAT_1:135
    (X /\ Y)|R = X|R /\ Y|R;

theorem :: RELAT_1:136
    (X \ Y)|R = X|R \ Y|R;

theorem :: RELAT_1:137
    {}|R = {};

theorem :: RELAT_1:138
    Y|{} = {};

theorem :: RELAT_1:139
    Y|(P*R) = P*(Y|R);

theorem :: RELAT_1:140
    (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;

canceled 2;

theorem :: RELAT_1:143
  y in R.:X iff ex x st x in dom R & [x,y] in R & x in X;

theorem :: RELAT_1:144
  R.:X c= rng R;

theorem :: RELAT_1:145
    R.:X = R.:(dom R /\ X);

theorem :: RELAT_1:146
  R.:dom R = rng R;

theorem :: RELAT_1:147
    R.:X c= R.:(dom R);

theorem :: RELAT_1:148
    rng(R|X) = R.:X;

theorem :: RELAT_1:149
    R.:{} = {};

theorem :: RELAT_1:150
    {}.:X = {};

theorem :: RELAT_1:151
    R.:X = {} iff dom R misses X;

theorem :: RELAT_1:152
    X <> {} & X c= dom R implies R.:X <> {};

theorem :: RELAT_1:153
    R.:(X \/ Y) = R.:X \/ R.:Y;

theorem :: RELAT_1:154
    R.:(X /\ Y) c= R.:X /\ R.:Y;

theorem :: RELAT_1:155
    R.:X \ R.:Y c= R.:(X \ Y);

theorem :: RELAT_1:156
  X c= Y implies R.:X c= R.:Y;

theorem :: RELAT_1:157
  P c= R implies P.:X c= R.:X;

theorem :: RELAT_1:158
    P c= R & X c= Y implies P.:X c= R.:Y;

theorem :: RELAT_1:159
    (P*R).:X=R.:(P.:X);

theorem :: RELAT_1:160
    rng(P*R) = R.:(rng P);

theorem :: RELAT_1:161
    (R|X).:Y c= R.:Y;

canceled;

theorem :: RELAT_1:163
    (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;

canceled 2;

theorem :: RELAT_1:166
  x in R"Y iff ex y st y in rng R & [x,y] in R & y in Y;

theorem :: RELAT_1:167
  R"Y c= dom R;

theorem :: RELAT_1:168
    R"Y = R"(rng R /\ Y);

theorem :: RELAT_1:169
  R"rng R = dom R;

theorem :: RELAT_1:170
    R"Y c= R"rng R;

theorem :: RELAT_1:171
    R"{} = {};

theorem :: RELAT_1:172
    {}"Y = {};

theorem :: RELAT_1:173
    R"Y = {} iff rng R misses Y;

theorem :: RELAT_1:174
    Y <> {} & Y c= rng R implies R"Y <> {};

theorem :: RELAT_1:175
    R"(X \/ Y) = R"X \/ R"Y;

theorem :: RELAT_1:176
    R"(X /\ Y) c= R"X /\ R"Y;

theorem :: RELAT_1:177
    R"X \ R"Y c= R"(X \ Y);

theorem :: RELAT_1:178
  X c= Y implies R"X c= R"Y;

theorem :: RELAT_1:179
  P c= R implies P"Y c= R"Y;

theorem :: RELAT_1:180
    P c= R & X c= Y implies P"X c= R"Y;

theorem :: RELAT_1:181
    (P*R)"Y = P"(R"Y);

theorem :: RELAT_1:182
    dom(P*R) = P"(dom R);

theorem :: RELAT_1:183
    (rng R) /\ Y c= (R~)"(R"Y);
The abstract of the Mizar article:

Relations and Their Basic Properties
