:: by Grzegorz Bancerek, Artur Korni\l owicz and Andrzej Trybulec

::

:: Received December 9, 2011

:: Copyright (c) 2011-2015 Association of Mizar Users

:: deftheorem Def1 defines pair XTUPLE_0:def 1 :

for x being object holds

( x is pair iff ex x1, x2 being object st x = [x1,x2] );

for x being object holds

( x is pair iff ex x1, x2 being object st x = [x1,x2] );

Lm1: for x, y1, y2 being object st {x} = {y1,y2} holds

x = y1

proof end;

Lm2: for x, y1, y2 being object st {x} = {y1,y2} holds

y1 = y2

proof end;

Lm3: for x1, x2, y1, y2 being object holds

( not {x1,x2} = {y1,y2} or x1 = y1 or x1 = y2 )

proof end;

definition

let x be object ;

assume x is pair ;

then consider x1, x2 being object such that

A1: x = [x1,x2] ;

ex b_{1} being object st

for y1, y2 being object st x = [y1,y2] holds

b_{1} = y1

for b_{1}, b_{2} being object st ( for y1, y2 being object st x = [y1,y2] holds

b_{1} = y1 ) & ( for y1, y2 being object st x = [y1,y2] holds

b_{2} = y1 ) holds

b_{1} = b_{2}

ex b_{1} being object st

for y1, y2 being object st x = [y1,y2] holds

b_{1} = y2

for b_{1}, b_{2} being object st ( for y1, y2 being object st x = [y1,y2] holds

b_{1} = y2 ) & ( for y1, y2 being object st x = [y1,y2] holds

b_{2} = y2 ) holds

b_{1} = b_{2}

end;
assume x is pair ;

then consider x1, x2 being object such that

A1: x = [x1,x2] ;

func x `1 -> object means :Def2: :: XTUPLE_0:def 2

for y1, y2 being object st x = [y1,y2] holds

it = y1;

existence for y1, y2 being object st x = [y1,y2] holds

it = y1;

ex b

for y1, y2 being object st x = [y1,y2] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `2 -> object means :Def3: :: XTUPLE_0:def 3

for y1, y2 being object st x = [y1,y2] holds

it = y2;

existence for y1, y2 being object st x = [y1,y2] holds

it = y2;

ex b

for y1, y2 being object st x = [y1,y2] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines `1 XTUPLE_0:def 2 :

for x being object st x is pair holds

for b_{2} being object holds

( b_{2} = x `1 iff for y1, y2 being object st x = [y1,y2] holds

b_{2} = y1 );

for x being object st x is pair holds

for b

( b

b

:: deftheorem Def3 defines `2 XTUPLE_0:def 3 :

for x being object st x is pair holds

for b_{2} being object holds

( b_{2} = x `2 iff for y1, y2 being object st x = [y1,y2] holds

b_{2} = y2 );

for x being object st x is pair holds

for b

( b

b

registration
end;

registration
end;

registration
end;

:: deftheorem defines [ XTUPLE_0:def 4 :

for x1, x2, x3 being object holds [x1,x2,x3] = [[x1,x2],x3];

for x1, x2, x3 being object holds [x1,x2,x3] = [[x1,x2],x3];

:: deftheorem Def5 defines triple XTUPLE_0:def 5 :

for x being object holds

( x is triple iff ex x1, x2, x3 being object st x = [x1,x2,x3] );

for x being object holds

( x is triple iff ex x1, x2, x3 being object st x = [x1,x2,x3] );

registration
end;

theorem Th3: :: XTUPLE_0:3

for x1, x2, x3, y1, y2, y3 being object st [x1,x2,x3] = [y1,y2,y3] holds

( x1 = y1 & x2 = y2 & x3 = y3 )

( x1 = y1 & x2 = y2 & x3 = y3 )

proof end;

registration

existence

ex b_{1} being object st b_{1} is triple

for b_{1} being object st b_{1} is triple holds

b_{1} is pair
;

end;
ex b

proof end;

coherence for b

b

registration

let x1, x2, x3 be object ;

reducibility

[x1,x2,x3] `1_3 = x1 ;

reducibility

[x1,x2,x3] `2_3 = x2 ;

reducibility

[x1,x2,x3] `3_3 = x3 ;

end;
reducibility

[x1,x2,x3] `1_3 = x1 ;

reducibility

[x1,x2,x3] `2_3 = x2 ;

reducibility

[x1,x2,x3] `3_3 = x3 ;

:: deftheorem defines [ XTUPLE_0:def 8 :

for x1, x2, x3, x4 being object holds [x1,x2,x3,x4] = [[x1,x2,x3],x4];

for x1, x2, x3, x4 being object holds [x1,x2,x3,x4] = [[x1,x2,x3],x4];

:: deftheorem Def9 defines quadruple XTUPLE_0:def 9 :

for x being object holds

( x is quadruple iff ex x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] );

for x being object holds

( x is quadruple iff ex x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] );

theorem :: XTUPLE_0:5

for x1, x2, x3, x4, y1, y2, y3, y4 being object st [x1,x2,x3,x4] = [y1,y2,y3,y4] holds

( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 )

( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 )

proof end;

registration

existence

ex b_{1} being object st b_{1} is quadruple

for b_{1} being object st b_{1} is quadruple holds

b_{1} is triple

end;
ex b

proof end;

coherence for b

b

proof end;

definition
end;

registration

let x1, x2, x3, x4 be object ;

reducibility

[x1,x2,x3,x4] `1_4 = x1 ;

reducibility

[x1,x2,x3,x4] `2_4 = x2 ;

reducibility

[x1,x2,x3,x4] `3_4 = x3 ;

reducibility

[x1,x2,x3,x4] `4_4 = x4 ;

end;
reducibility

[x1,x2,x3,x4] `1_4 = x1 ;

reducibility

[x1,x2,x3,x4] `2_4 = x2 ;

reducibility

[x1,x2,x3,x4] `3_4 = x3 ;

reducibility

[x1,x2,x3,x4] `4_4 = x4 ;

registration
end;

:: Preliminaries

:: Projections

definition

let X be set ;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff ex y being object st [x,y] in X )

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

( x in b_{1} iff ex y being object st [x,y] in X ) ) & ( for x being object holds

( x in b_{2} iff ex y being object st [x,y] in X ) ) holds

b_{1} = b_{2}

ex b_{1} being set st

for x being object holds

( x in b_{1} iff ex y being object st [y,x] in X )

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

( x in b_{1} iff ex y being object st [y,x] in X ) ) & ( for x being object holds

( x in b_{2} iff ex y being object st [y,x] in X ) ) holds

b_{1} = b_{2}

end;
func proj1 X -> set means :Def12: :: XTUPLE_0:def 12

for x being object holds

( x in it iff ex y being object st [x,y] in X );

existence for x being object holds

( x in it iff ex y being object st [x,y] in X );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

func proj2 X -> set means :Def13: :: XTUPLE_0:def 13

for x being object holds

( x in it iff ex y being object st [y,x] in X );

existence for x being object holds

( x in it iff ex y being object st [y,x] in X );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def12 defines proj1 XTUPLE_0:def 12 :

for X, b_{2} being set holds

( b_{2} = proj1 X iff for x being object holds

( x in b_{2} iff ex y being object st [x,y] in X ) );

for X, b

( b

( x in b

:: deftheorem Def13 defines proj2 XTUPLE_0:def 13 :

for X, b_{2} being set holds

( b_{2} = proj2 X iff for x being object holds

( x in b_{2} iff ex y being object st [y,x] in X ) );

for X, b

( b

( x in b

definition
end;

definition
end;

:: deftheorem defines proj1_4 XTUPLE_0:def 16 :

for X being set holds proj1_4 X = proj1 (proj1_3 X);

for X being set holds proj1_4 X = proj1 (proj1_3 X);

:: deftheorem defines proj2_4 XTUPLE_0:def 17 :

for X being set holds proj2_4 X = proj2 (proj1_3 X);

for X being set holds proj2_4 X = proj2 (proj1_3 X);

theorem Th18: :: XTUPLE_0:18

for x being object

for X being set st x in proj1_4 X holds

ex x1, x2, x3 being object st [x,x1,x2,x3] in X

for X being set st x in proj1_4 X holds

ex x1, x2, x3 being object st [x,x1,x2,x3] in X

proof end;

theorem Th20: :: XTUPLE_0:20

for x being object

for X being set st x in proj2_4 X holds

ex x1, x2, x3 being object st [x1,x,x2,x3] in X

for X being set st x in proj2_4 X holds

ex x1, x2, x3 being object st [x1,x,x2,x3] in X

proof end;

theorem :: XTUPLE_0:22

for a, b being quadruple object st a `1_4 = b `1_4 & a `2_4 = b `2_4 & a `3_4 = b `3_4 & a `4_4 = b `4_4 holds

a = b

a = b

proof end;

registration
end;

registration
end;