:: by Edmund Woronowicz

::

:: Received March 15, 1989

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

definition

let IT be set ;

end;
attr IT is Relation-like means :Def1: :: RELAT_1:def 1

for x being set st x in IT holds

ex y, z being set st x = [y,z];

for x being set st x in IT holds

ex y, z being set st x = [y,z];

:: deftheorem Def1 defines Relation-like RELAT_1:def 1 :

for IT being set holds

( IT is Relation-like iff for x being set st x in IT holds

ex y, z being set st x = [y,z] );

for IT being set holds

( IT is Relation-like iff for x being set st x in IT holds

ex y, z being set st x = [y,z] );

registration
end;

registration
end;

definition

let P, R be Relation;

compatibility

( P = R iff for a, b being set holds

( [a,b] in P iff [a,b] in R ) )

end;
compatibility

( P = R iff for a, b being set holds

( [a,b] in P iff [a,b] in R ) )

proof end;

:: deftheorem defines = RELAT_1:def 2 :

for P, R being Relation holds

( P = R iff for a, b being set holds

( [a,b] in P iff [a,b] in R ) );

for P, R being Relation holds

( P = R iff for a, b being set holds

( [a,b] in P iff [a,b] in R ) );

registration

let P be Relation;

let X be set ;

coherence

P /\ X is Relation-like

P \ X is Relation-like ;

end;
let X be set ;

coherence

P /\ X is Relation-like

proof end;

coherence P \ X is Relation-like ;

registration
end;

registration

let a, b be set ;

coherence

{[a,b]} is Relation-like

[:a,b:] is Relation-like

end;
coherence

{[a,b]} is Relation-like

proof end;

coherence [:a,b:] is Relation-like

proof end;

definition

let P be Relation;

let A be set ;

compatibility

( P c= A iff for a, b being set st [a,b] in P holds

[a,b] in A )

end;
let A be set ;

compatibility

( P c= A iff for a, b being set st [a,b] in P holds

[a,b] in A )

proof end;

:: deftheorem defines c= RELAT_1:def 3 :

for P being Relation

for A being set holds

( P c= A iff for a, b being set st [a,b] in P holds

[a,b] in A );

for P being Relation

for A being set holds

( P c= A iff for a, b being set st [a,b] in P holds

[a,b] in A );

theorem :: RELAT_1:10

for a, b, x, y being set

for R being Relation st R = {[a,b],[x,y]} holds

( dom R = {a,x} & rng R = {b,y} )

for R being Relation st R = {[a,b],[x,y]} holds

( dom R = {a,x} & rng R = {b,y} )

proof end;

theorem Th11: :: RELAT_1:11

for P, R being Relation st P c= R holds

( dom P c= dom R & rng P c= rng R ) by XTUPLE_0:8, XTUPLE_0:9;

( dom P c= dom R & rng P c= rng R ) by XTUPLE_0:8, XTUPLE_0:9;

theorem :: RELAT_1:14

:: FIELD OF RELATION

:: deftheorem defines field RELAT_1:def 6 :

for R being Relation holds field R = (dom R) \/ (rng R);

for R being Relation holds field R = (dom R) \/ (rng R);

:: CONVERSE RELATION

definition

let R be Relation;

ex b_{1} being Relation st

for x, y being set holds

( [x,y] in b_{1} iff [y,x] in R )

for b_{1}, b_{2} being Relation st ( for x, y being set holds

( [x,y] in b_{1} iff [y,x] in R ) ) & ( for x, y being set holds

( [x,y] in b_{2} iff [y,x] in R ) ) holds

b_{1} = b_{2}

for b_{1}, b_{2} being Relation st ( for x, y being set holds

( [x,y] in b_{1} iff [y,x] in b_{2} ) ) holds

for x, y being set holds

( [x,y] in b_{2} iff [y,x] in b_{1} )
;

end;
func R ~ -> Relation means :Def7: :: RELAT_1:def 7

for x, y being set holds

( [x,y] in it iff [y,x] in R );

existence for x, y being set holds

( [x,y] in it iff [y,x] in R );

ex b

for x, y being set holds

( [x,y] in b

proof end;

uniqueness for b

( [x,y] in b

( [x,y] in b

b

proof end;

involutiveness for b

( [x,y] in b

for x, y being set holds

( [x,y] in b

:: deftheorem Def7 defines ~ RELAT_1:def 7 :

for R, b_{2} being Relation holds

( b_{2} = R ~ iff for x, y being set holds

( [x,y] in b_{2} iff [y,x] in R ) );

for R, b

( b

( [x,y] in b

:: COMPOSITION OF RELATIONS

definition

let P, R be set ;

ex b_{1} being Relation st

for x, y being set holds

( [x,y] in b_{1} iff ex z being set st

( [x,z] in P & [z,y] in R ) )

for b_{1}, b_{2} being Relation st ( for x, y being set holds

( [x,y] in b_{1} iff ex z being set st

( [x,z] in P & [z,y] in R ) ) ) & ( for x, y being set holds

( [x,y] in b_{2} iff ex z being set st

( [x,z] in P & [z,y] in R ) ) ) holds

b_{1} = b_{2}

end;
func P (#) R -> Relation means :Def8: :: RELAT_1:def 8

for x, y being set holds

( [x,y] in it iff ex z being set st

( [x,z] in P & [z,y] in R ) );

existence for x, y being set holds

( [x,y] in it iff ex z being set st

( [x,z] in P & [z,y] in R ) );

ex b

for x, y being set holds

( [x,y] in b

( [x,z] in P & [z,y] in R ) )

proof end;

uniqueness for b

( [x,y] in b

( [x,z] in P & [z,y] in R ) ) ) & ( for x, y being set holds

( [x,y] in b

( [x,z] in P & [z,y] in R ) ) ) holds

b

proof end;

:: deftheorem Def8 defines (#) RELAT_1:def 8 :

for P, R being set

for b_{3} being Relation holds

( b_{3} = P (#) R iff for x, y being set holds

( [x,y] in b_{3} iff ex z being set st

( [x,z] in P & [z,y] in R ) ) );

for P, R being set

for b

( b

( [x,y] in b

( [x,z] in P & [z,y] in R ) ) );

:: EMPTY RELATION

registration

let f be non empty Relation;

coherence

not dom f is empty

not rng f is empty

end;
coherence

not dom f is empty

proof end;

coherence not rng f is empty

proof end;

registration

let X be empty set ;

coherence

dom X is empty ;

coherence

rng X is empty ;

let R be Relation;

coherence

X * R is empty by Th39;

coherence

R * X is empty by Th39;

end;
coherence

dom X is empty ;

coherence

rng X is empty ;

let R be Relation;

coherence

X * R is empty by Th39;

coherence

R * X is empty by Th39;

definition
end;

:: deftheorem Def9 defines non-empty RELAT_1:def 9 :

for R being Relation holds

( R is non-empty iff not {} in rng R );

for R being Relation holds

( R is non-empty iff not {} in rng R );

registration
end;

:: IDENTITY RELATION

definition

let X be set ;

ex b_{1} being Relation st

for x, y being set holds

( [x,y] in b_{1} iff ( x in X & x = y ) )

for b_{1}, b_{2} being Relation st ( for x, y being set holds

( [x,y] in b_{1} iff ( x in X & x = y ) ) ) & ( for x, y being set holds

( [x,y] in b_{2} iff ( x in X & x = y ) ) ) holds

b_{1} = b_{2}

end;
func id X -> Relation means :Def10: :: RELAT_1:def 10

for x, y being set holds

( [x,y] in it iff ( x in X & x = y ) );

existence for x, y being set holds

( [x,y] in it iff ( x in X & x = y ) );

ex b

for x, y being set holds

( [x,y] in b

proof end;

uniqueness for b

( [x,y] in b

( [x,y] in b

b

proof end;

:: deftheorem Def10 defines id RELAT_1:def 10 :

for X being set

for b_{2} being Relation holds

( b_{2} = id X iff for x, y being set holds

( [x,y] in b_{2} iff ( x in X & x = y ) ) );

for X being set

for b

( b

( [x,y] in b

registration
end;

theorem :: RELAT_1:47

for X being set

for R being Relation st ( for x being set st x in X holds

[x,x] in R ) holds

id X c= R

for R being Relation st ( for x being set st x in X holds

[x,x] in R ) holds

id X c= R

proof end;

theorem Th48: :: RELAT_1:48

for x, y, X being set

for R being Relation holds

( [x,y] in (id X) * R iff ( x in X & [x,y] in R ) )

for R being Relation holds

( [x,y] in (id X) * R iff ( x in X & [x,y] in R ) )

proof end;

theorem Th49: :: RELAT_1:49

for x, y, Y being set

for R being Relation holds

( [x,y] in R * (id Y) iff ( y in Y & [x,y] in R ) )

for R being Relation holds

( [x,y] in R * (id Y) iff ( y in Y & [x,y] in R ) )

proof end;

theorem :: RELAT_1:56

for X being set

for P2, R, P1 being Relation st rng P2 c= X & P2 * R = id (dom P1) & R * P1 = id X holds

P1 = P2

for P2, R, P1 being Relation st rng P2 c= X & P2 * R = id (dom P1) & R * P1 = id X holds

P1 = P2

proof end;

definition

let R be Relation;

let X be set ;

ex b_{1} being Relation st

for x, y being set holds

( [x,y] in b_{1} iff ( x in X & [x,y] in R ) )

for b_{1}, b_{2} being Relation st ( for x, y being set holds

( [x,y] in b_{1} iff ( x in X & [x,y] in R ) ) ) & ( for x, y being set holds

( [x,y] in b_{2} iff ( x in X & [x,y] in R ) ) ) holds

b_{1} = b_{2}

end;
let X be set ;

func R | X -> Relation means :Def11: :: RELAT_1:def 11

for x, y being set holds

( [x,y] in it iff ( x in X & [x,y] in R ) );

existence for x, y being set holds

( [x,y] in it iff ( x in X & [x,y] in R ) );

ex b

for x, y being set holds

( [x,y] in b

proof end;

uniqueness for b

( [x,y] in b

( [x,y] in b

b

proof end;

:: deftheorem Def11 defines | RELAT_1:def 11 :

for R being Relation

for X being set

for b_{3} being Relation holds

( b_{3} = R | X iff for x, y being set holds

( [x,y] in b_{3} iff ( x in X & [x,y] in R ) ) );

for R being Relation

for X being set

for b

( b

( [x,y] in b

registration
end;

theorem :: RELAT_1:63

theorem :: RELAT_1:64

registration
end;

definition

let Y be set ;

let R be Relation;

ex b_{1} being Relation st

for x, y being set holds

( [x,y] in b_{1} iff ( y in Y & [x,y] in R ) )

for b_{1}, b_{2} being Relation st ( for x, y being set holds

( [x,y] in b_{1} iff ( y in Y & [x,y] in R ) ) ) & ( for x, y being set holds

( [x,y] in b_{2} iff ( y in Y & [x,y] in R ) ) ) holds

b_{1} = b_{2}

end;
let R be Relation;

func Y |` R -> Relation means :Def12: :: RELAT_1:def 12

for x, y being set holds

( [x,y] in it iff ( y in Y & [x,y] in R ) );

existence for x, y being set holds

( [x,y] in it iff ( y in Y & [x,y] in R ) );

ex b

for x, y being set holds

( [x,y] in b

proof end;

uniqueness for b

( [x,y] in b

( [x,y] in b

b

proof end;

:: deftheorem Def12 defines |` RELAT_1:def 12 :

for Y being set

for R, b_{3} being Relation holds

( b_{3} = Y |` R iff for x, y being set holds

( [x,y] in b_{3} iff ( y in Y & [x,y] in R ) ) );

for Y being set

for R, b

( b

( [x,y] in b

theorem :: RELAT_1:90

theorem :: RELAT_1:91

registration
end;

:: IMAGE OF SET IN RELATION

definition

let R be Relation;

let X be set ;

ex b_{1} being set st

for y being set holds

( y in b_{1} iff ex x being set st

( [x,y] in R & x in X ) )

for b_{1}, b_{2} being set st ( for y being set holds

( y in b_{1} iff ex x being set st

( [x,y] in R & x in X ) ) ) & ( for y being set holds

( y in b_{2} iff ex x being set st

( [x,y] in R & x in X ) ) ) holds

b_{1} = b_{2}

end;
let X be set ;

func R .: X -> set means :Def13: :: RELAT_1:def 13

for y being set holds

( y in it iff ex x being set st

( [x,y] in R & x in X ) );

existence for y being set holds

( y in it iff ex x being set st

( [x,y] in R & x in X ) );

ex b

for y being set holds

( y in b

( [x,y] in R & x in X ) )

proof end;

uniqueness for b

( y in b

( [x,y] in R & x in X ) ) ) & ( for y being set holds

( y in b

( [x,y] in R & x in X ) ) ) holds

b

proof end;

:: deftheorem Def13 defines .: RELAT_1:def 13 :

for R being Relation

for X, b_{3} being set holds

( b_{3} = R .: X iff for y being set holds

( y in b_{3} iff ex x being set st

( [x,y] in R & x in X ) ) );

for R being Relation

for X, b

( b

( y in b

( [x,y] in R & x in X ) ) );

theorem Th110: :: RELAT_1:110

for y, X being set

for R being Relation holds

( y in R .: X iff ex x being set st

( x in dom R & [x,y] in R & x in X ) )

for R being Relation holds

( y in R .: X iff ex x being set st

( x in dom R & [x,y] in R & x in X ) )

proof end;

theorem :: RELAT_1:128

:: INVERSE IMAGE OF SET IN RELATION

definition

let R be Relation;

let Y be set ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ex y being set st

( [x,y] in R & y in Y ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ex y being set st

( [x,y] in R & y in Y ) ) ) & ( for x being set holds

( x in b_{2} iff ex y being set st

( [x,y] in R & y in Y ) ) ) holds

b_{1} = b_{2}

end;
let Y be set ;

func R " Y -> set means :Def14: :: RELAT_1:def 14

for x being set holds

( x in it iff ex y being set st

( [x,y] in R & y in Y ) );

existence for x being set holds

( x in it iff ex y being set st

( [x,y] in R & y in Y ) );

ex b

for x being set holds

( x in b

( [x,y] in R & y in Y ) )

proof end;

uniqueness for b

( x in b

( [x,y] in R & y in Y ) ) ) & ( for x being set holds

( x in b

( [x,y] in R & y in Y ) ) ) holds

b

proof end;

:: deftheorem Def14 defines " RELAT_1:def 14 :

for R being Relation

for Y, b_{3} being set holds

( b_{3} = R " Y iff for x being set holds

( x in b_{3} iff ex y being set st

( [x,y] in R & y in Y ) ) );

for R being Relation

for Y, b

( b

( x in b

( [x,y] in R & y in Y ) ) );

theorem Th131: :: RELAT_1:131

for x, Y being set

for R being Relation holds

( x in R " Y iff ex y being set st

( y in rng R & [x,y] in R & y in Y ) )

for R being Relation holds

( x in R " Y iff ex y being set st

( y in rng R & [x,y] in R & y in Y ) )

proof end;

registration
end;

registration
end;

begin

definition
end;

:: deftheorem Def15 defines empty-yielding RELAT_1:def 15 :

for R being Relation holds

( R is empty-yielding iff rng R c= {{}} );

for R being Relation holds

( R is empty-yielding iff rng R c= {{}} );

:: from AMI_3

theorem :: RELAT_1:150

for f, g being Relation

for A, B being set st f | A = g | A & f | B = g | B holds

f | (A \/ B) = g | (A \/ B)

for A, B being set st f | A = g | A & f | B = g | B holds

f | (A \/ B) = g | (A \/ B)

proof end;

:: from AMI_5

:: missing, 2005.07.11, A.T.

:: missing, 2005.11.13, A.T.

registration
end;

registration
end;

theorem :: RELAT_1:155

:: from EQREL_1 (Class), 2007.02.06

:: deftheorem defines Im RELAT_1:def 16 :

for R being Relation

for x being set holds Im (R,x) = R .: {x};

for R being Relation

for x being set holds Im (R,x) = R .: {x};

:: missing, 2007.04.13, A.T.

:: from YELLOW_3, 2007.06.13, A.T.

:: from YELLOW_3, 2007.06.13, A.T.

:: from SCMFSA6A, 2007.07.23, A.T.

:: missing, 2007.11.07, A.T.

:: from FUNCOP_1, 2008.02.19, A.T.

:: from RELSET_2 (R"x, generalized), 2008.07.16, A.T.

:: deftheorem defines Coim RELAT_1:def 17 :

for R being Relation

for x being set holds Coim (R,x) = R " {x};

for R being Relation

for x being set holds Coim (R,x) = R " {x};

:: from NECKLACE, 2008.07.25, A.T.

registration
end;

registration
end;

:: comp. RFUNCT_2:34, CFCONT_1:31, 2008.08.07, A.T.

:: from LATTICE2, 2008.09.14, A.T.

:: new, 2009.01.21, A.T

:: deftheorem Def18 defines -defined RELAT_1:def 18 :

for X being set

for R being Relation holds

( R is X -defined iff dom R c= X );

for X being set

for R being Relation holds

( R is X -defined iff dom R c= X );

:: deftheorem Def19 defines -valued RELAT_1:def 19 :

for X being set

for R being Relation holds

( R is X -valued iff rng R c= X );

for X being set

for R being Relation holds

( R is X -valued iff rng R c= X );

Lm1: for X, Y being set holds

( {} is X -defined & {} is Y -valued )

proof end;

registration

let X, Y be set ;

existence

ex b_{1} being Relation st

( b_{1} is X -defined & b_{1} is Y -valued )

end;
existence

ex b

( b

proof end;

:: from QC_LANG4, 2009.01.23, A.T

:: new, 2009.02.07, A.T.

registration
end;

registration

let X, A be set ;

let R be A -defined Relation;

coherence

( R | X is A -defined & R | X is X -defined )

end;
let R be A -defined Relation;

coherence

( R | X is A -defined & R | X is X -defined )

proof end;

:: 2009.02.16, A.T.

registration

let A be set ;

let R be A -valued Relation;

let S be Relation;

coherence

S * R is A -valued

end;
let R be A -valued Relation;

let S be Relation;

coherence

S * R is A -valued

proof end;

registration

let A be set ;

let R be A -defined Relation;

let S be Relation;

coherence

R * S is A -defined

end;
let R be A -defined Relation;

let S be Relation;

coherence

R * S is A -defined

proof end;

:: 2009.02.16, A.T.

:: 2009.10.02, A.T.

registration
end;

registration

let X be set ;

let R be X -defined Relation;

coherence

for b_{1} being Subset of R holds b_{1} is X -defined

end;
let R be X -defined Relation;

coherence

for b

proof end;

registration

let X be set ;

let R be X -valued Relation;

coherence

for b_{1} being Subset of R holds b_{1} is X -valued

end;
let R be X -valued Relation;

coherence

for b

proof end;

:: missing, 2010.01.02, A.T

:: from AMISTD_3, 2010.01.10, A.T.

registration
end;

registration
end;

:: missing, 2010.04.07, A.T.

:: new, 20011.06.11, A.T.

registration
end;

registration

let X, A be set ;

let R be A -valued Relation;

coherence

( X |` R is A -valued & X |` R is X -valued )

end;
let R be A -valued Relation;

coherence

( X |` R is A -valued & X |` R is X -valued )

proof end;

registration

let X be empty set ;

coherence

for b_{1} being X -defined Relation holds b_{1} is empty

for b_{1} being X -valued Relation holds b_{1} is empty

end;
coherence

for b

proof end;

coherence for b

proof end;