:: Relations Defined on Sets
:: by Edmund Woronowicz
::
:: Received April 14, 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 RELAT_1, SUBSET_1, ZFMISC_1, TARSKI, XBOOLE_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1;
constructors TARSKI, SUBSET_1, RELAT_1, XTUPLE_0;
registrations XBOOLE_0, RELAT_1, SUBSET_1;
requirements SUBSET, BOOLE;
begin
reserve A,B,X,X1,Y,Y1,Y2,Z for set, a,x,y,z for object;
::
:: RELATION AS A SUBSET OF CARTESIAN PRODUCT OF TWO SETS
:: _____________________________________________________
definition
let X,Y;
mode Relation of X,Y is Subset of [:X,Y:];
end;
registration
let X,Y;
cluster -> Relation-like for Subset of [:X,Y:];
end;
registration
let X,Y;
cluster -> X-defined Y-valued for Relation of X,Y;
end;
reserve P,R for Relation of X,Y;
definition
let X,Y,R,Z;
redefine pred R c= Z means
:: RELSET_1:def 1
for x being Element of X, y being Element of Y
holds [x,y] in R implies [x,y] in Z;
end;
definition
let X,Y,P,R;
redefine pred P = R means
:: RELSET_1:def 2
for x being Element of X, y being Element of Y
holds [x,y] in P iff [x,y] in R;
end;
theorem :: RELSET_1:1
A c= R implies A is Relation of X,Y;
theorem :: RELSET_1:2
a in R implies ex x,y st a = [x,y] & x in X & y in Y;
theorem :: RELSET_1:3
x in X & y in Y implies {[x,y]} is Relation of X,Y;
theorem :: RELSET_1:4
for R being Relation st dom R c= X & rng R c= Y holds R is Relation of X,Y;
theorem :: RELSET_1:5
dom R c= X1 implies R is Relation of X1,Y;
theorem :: RELSET_1:6
rng R c= Y1 implies R is Relation of X,Y1;
theorem :: RELSET_1:7
X c= X1 & Y c= Y1 implies R is Relation of X1,Y1;
registration
let X;
let R,S be X-defined Relation;
cluster R \/ S -> X-defined;
end;
registration
let X;
let R be X-defined Relation, S be Relation;
cluster R /\ S -> X-defined;
cluster R \ S -> X-defined;
end;
registration
let X;
let R,S be X-valued Relation;
cluster R \/ S -> X-valued;
end;
registration
let X;
let R be X-valued Relation, S be Relation;
cluster R /\ S -> X-valued;
cluster R \ S -> X-valued;
end;
definition let X; let R be X-defined Relation;
redefine func dom R -> Subset of X;
end;
definition let X; let R be X-valued Relation;
redefine func rng R -> Subset of X;
end;
theorem :: RELSET_1:8
field R c= X \/ Y;
theorem :: RELSET_1:9
(for x being object st x in X
ex y being object st [x,y] in R) iff dom R = X;
theorem :: RELSET_1:10
(for y being object st y in Y
ex x being object st [x,y] in R) iff rng R = Y;
definition
let X,Y,R;
redefine func R~ -> Relation of Y,X;
end;
definition
let X,Y1,Y2,Z;
let P be Relation of X,Y1;
let R be Relation of Y2,Z;
redefine func P*R -> Relation of X,Z;
end;
theorem :: RELSET_1:11
dom (R~) = rng R & rng (R~) = dom R;
theorem :: RELSET_1:12
{} is Relation of X,Y;
registration
let A be empty set, B be set;
cluster -> empty for Relation of A,B;
cluster -> empty for Relation of B,A;
end;
theorem :: RELSET_1:13
id X c= [:X,X:];
theorem :: RELSET_1:14
id X is Relation of X,X;
theorem :: RELSET_1:15
id A c= R implies A c= dom R & A c= rng R;
theorem :: RELSET_1:16
id X c= R implies X = dom R & X c= rng R;
theorem :: RELSET_1:17
id Y c= R implies Y c= dom R & Y = rng R;
definition
let X,Y,R,A;
redefine func R|A -> Relation of X,Y;
end;
definition
let X,Y,B,R;
redefine func B|`R -> Relation of X,Y;
end;
theorem :: RELSET_1:18
R|X1 is Relation of X1,Y;
theorem :: RELSET_1:19
X c= X1 implies R|X1 = R;
theorem :: RELSET_1:20
Y1|`R is Relation of X,Y1;
theorem :: RELSET_1:21
Y c= Y1 implies Y1|`R = R;
definition
let X,Y,R,A;
redefine func R.:A -> Subset of Y;
redefine func R"A -> Subset of X;
end;
theorem :: RELSET_1:22
R.:X = rng R & R"Y = dom R;
theorem :: RELSET_1:23
R.:(R"Y) = rng R & R"(R.:X) = dom R;
scheme :: RELSET_1:sch 1
RelOnSetEx{A() -> set,B() -> set,P[object,object]}:
ex R being Relation of A(),B()
st for x,y holds [x,y] in R iff x in A() & y in B() & P[x,y];
:: Relation on a set
definition
let X;
mode Relation of X is Relation of X,X;
end;
reserve D,D1,D2,E,F for non empty set;
reserve R for Relation of D,E;
reserve x for Element of D;
reserve y for Element of E;
registration
let D be non empty set;
cluster id D -> non empty;
end;
theorem :: RELSET_1:24
for x being Element of D holds x in dom R iff ex y being Element of E
st [x,y] in R;
theorem :: RELSET_1:25
for y being object holds y in rng R iff
ex x being Element of D st [x,y] in R;
theorem :: RELSET_1:26
dom R <> {} implies ex y being Element of E st y in rng R;
theorem :: RELSET_1:27
rng R <> {} implies ex x being Element of D st x in dom R;
theorem :: RELSET_1:28
for P being Relation of D,E, R being Relation of E,F
for x, z being object holds [x,z] in P*R iff
ex y being Element of E st [x,y] in P & [y,z] in R;
theorem :: RELSET_1:29
y in R.:D1 iff ex x being Element of D st [x,y] in R & x in D1;
theorem :: RELSET_1:30
x in R"D2 iff ex y being Element of E st [x,y] in R & y in D2;
scheme :: RELSET_1:sch 2
RelOnDomEx{A,B() -> non empty set, P[object,object]}:
ex R being Relation of A(),B
() st for x being Element of A(), y being Element of B() holds [x,y] in R iff P
[x,y];
begin :: Addenda
:: missing, 2006.11.04, A.T.
scheme :: RELSET_1:sch 3
{ N()-> set, M() -> Subset of N(), F(object)->set }:
ex R being Relation of M()
st for i being Element of N() st i in M() holds Im(R,i) = F(i)
provided
for i being Element of N() st i in M() holds F(i) c= M();
theorem :: RELSET_1:31
for N being set, R,S being Relation of N st for i being set st i in N
holds Im(R,i) = Im(S,i) holds R = S;
:: from AMI_3, 2007.06.13, A.T. (generalized)
scheme :: RELSET_1:sch 4
{A,B() -> set, P[set,set], P,R()->Relation of A(), B()}: P() = R()
provided
for p being Element of A(), q being Element of B() holds [p,q] in P(
) iff P[p,q] and
for p being Element of A(), q being Element of B() holds [p,q] in R(
) iff P[p,q];
:: missing, 2007.06.14, A.T.
registration
let X,Y,Z;
let f be Relation of [:X,Y:], Z;
cluster dom f -> Relation-like;
end;
registration
let X,Y,Z;
let f be Relation of X, [:Y, Z:];
cluster rng f -> Relation-like;
end;
:: missing, 2008.04.30, A.T.
theorem :: RELSET_1:32
A misses X implies P|A = {};
:: missing, 2008.09.15, A.T.
registration
let R be non empty Relation, Y be non empty Subset of dom R;
cluster R|Y -> non empty;
end;
registration
let R be non empty Relation;
let Y be non empty Subset of dom R;
cluster R.:Y -> non empty;
end;
:: missing, 2008.11.29 A.T.
registration
let X,Y be set;
cluster empty for Relation of X,Y;
end;
scheme :: RELSET_1:sch 5
{A() -> set,B() -> set,P[object,object]}:
ex R being Relation of A(),B()
st for x,y being set holds [x,y] in R iff x in A() & y in B() & P[x,y];