:: Kuratowski Pairs. {T}uples and Projections
:: by Grzegorz Bancerek, Artur Korni\l owicz and Andrzej Trybulec
::
:: Received December 9, 2011
:: Copyright (c) 2011-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 MCART_1, RECDEF_2, XTUPLE_0, FACIRC_1, RELAT_1, TARSKI, XBOOLE_0;
notations TARSKI, XBOOLE_0;
constructors TARSKI, XBOOLE_0;
registrations XBOOLE_0;
requirements BOOLE;
begin :: Pairs
reserve x,x1,x2,x3,x4,y,y1,y2,y3,y4,z,z1,z2,z2,z4 for object;
definition let x be object;
attr x is pair means
:: XTUPLE_0:def 1
ex x1,x2 st x = [x1,x2];
end;
registration let x1,x2 be object;
cluster [x1,x2] -> pair;
end;
theorem :: XTUPLE_0:1
[x1,x2] = [y1,y2] implies x1 = y1 & x2 = y2;
definition
let x be object;
assume x is pair;
func x`1 -> object means
:: XTUPLE_0:def 2
x = [y1,y2] implies it = y1;
func x`2 -> object means
:: XTUPLE_0:def 3
x = [y1,y2] implies it = y2;
end;
registration let x1,x2;
reduce [x1,x2]`1 to x1;
reduce [x1,x2]`2 to x2;
end;
registration
cluster pair for object;
end;
registration let x be pair object;
reduce [x`1,x`2] to x;
end;
theorem :: XTUPLE_0:2
for a,b being pair object st a`1 = b`1 & a`2 = b`2
holds a = b;
begin :: Triples
definition
let x1,x2,x3 be object;
func [x1,x2,x3] -> object equals
:: XTUPLE_0:def 4
[[x1,x2],x3];
end;
definition let x;
attr x is triple means
:: XTUPLE_0:def 5
ex x1,x2,x3 st x = [x1,x2,x3];
end;
registration let x1,x2,x3;
cluster [x1,x2,x3] -> triple;
end;
theorem :: XTUPLE_0:3
[x1,x2,x3] = [y1,y2,y3] implies x1 = y1 & x2 = y2 & x3 = y3;
registration
cluster triple for object;
cluster triple -> pair for object;
end;
definition
let x be object;
func x`1_3 -> object equals
:: XTUPLE_0:def 6
x`1`1;
func x`2_3 -> object equals
:: XTUPLE_0:def 7
x`1`2;
end;
notation
let x be object;
synonym x`3_3 for x`2;
end;
registration let x1,x2,x3;
reduce [x1,x2,x3]`1_3 to x1;
reduce [x1,x2,x3]`2_3 to x2;
reduce [x1,x2,x3]`3_3 to x3;
end;
registration let x be triple object;
reduce [x`1_3,x`2_3,x`3_3] to x;
end;
theorem :: XTUPLE_0:4
for a,b being triple object
st a`1_3 = b`1_3 & a`2_3 = b`2_3 & a`3_3 = b`3_3
holds a = b;
begin :: Quadruples
definition
let x1,x2,x3,x4 be object;
func [x1,x2,x3,x4] -> object equals
:: XTUPLE_0:def 8
[[x1,x2,x3],x4];
end;
definition let x;
attr x is quadruple means
:: XTUPLE_0:def 9
ex x1,x2,x3,x4 st x = [x1,x2,x3,x4];
end;
registration let x1,x2,x3,x4;
cluster [x1,x2,x3,x4] -> quadruple;
end;
theorem :: XTUPLE_0:5
[x1,x2,x3,x4] = [y1,y2,y3,y4]
implies x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4;
registration
cluster quadruple for object;
cluster quadruple -> triple for object;
end;
definition
let x be object;
func x`1_4 -> object equals
:: XTUPLE_0:def 10
x`1`1`1;
func x`2_4 -> object equals
:: XTUPLE_0:def 11
x`1`1`2;
end;
notation let x be object;
synonym x`3_4 for x`2_3;
synonym x`4_4 for x`2;
end;
registration let x1,x2,x3,x4;
reduce [x1,x2,x3,x4]`1_4 to x1;
reduce [x1,x2,x3,x4]`2_4 to x2;
reduce [x1,x2,x3,x4]`3_4 to x3;
reduce [x1,x2,x3,x4]`4_4 to x4;
end;
registration let x be quadruple object;
reduce [x`1_4,x`2_4,x`3_4,x`4_4] to x;
end;
reserve X,X1,X2,X3,X4,Y for set;
:: Preliminaries
theorem :: XTUPLE_0:6
[x,y] in X implies x in union union X;
theorem :: XTUPLE_0:7
[x,y] in X implies y in union union X;
:: Projections
definition
let X be set;
func proj1 X -> set means
:: XTUPLE_0:def 12
x in it iff ex y st [x,y] in X;
func proj2 X -> set means
:: XTUPLE_0:def 13
x in it iff ex y st [y,x] in X;
end;
theorem :: XTUPLE_0:8
X c= Y implies proj1 X c= proj1 Y;
theorem :: XTUPLE_0:9
X c= Y implies proj2 X c= proj2 Y;
definition
let X be set;
func proj1_3 X -> set equals
:: XTUPLE_0:def 14
proj1 proj1 X;
func proj2_3 X -> set equals
:: XTUPLE_0:def 15
proj2 proj1 X;
end;
notation let X be set;
synonym proj3_3 X for proj2 X;
end;
theorem :: XTUPLE_0:10
X c= Y implies proj1_3 X c= proj1_3 Y;
theorem :: XTUPLE_0:11
X c= Y implies proj2_3 X c= proj2_3 Y;
theorem :: XTUPLE_0:12
x in proj1_3 X implies ex y,z st [x,y,z] in X;
theorem :: XTUPLE_0:13
[x,y,z] in X implies x in proj1_3 X;
theorem :: XTUPLE_0:14
x in proj2_3 X implies ex y,z st [y,x,z] in X;
theorem :: XTUPLE_0:15
[x,y,z] in X implies y in proj2_3 X;
definition
let X be set;
func proj1_4 X -> set equals
:: XTUPLE_0:def 16
proj1 proj1_3 X;
func proj2_4 X -> set equals
:: XTUPLE_0:def 17
proj2 proj1_3 X;
end;
notation let X be set;
synonym proj3_4 X for proj2_3 X;
synonym proj4_4 X for proj2 X;
end;
theorem :: XTUPLE_0:16
X c= Y implies proj1_4 X c= proj1_4 Y;
theorem :: XTUPLE_0:17
X c= Y implies proj2_4 X c= proj2_4 Y;
theorem :: XTUPLE_0:18
x in proj1_4 X implies ex x1,x2,x3 st [x,x1,x2,x3] in X;
theorem :: XTUPLE_0:19
[x,x1,x2,x3] in X implies x in proj1_4 X;
theorem :: XTUPLE_0:20
x in proj2_4 X implies ex x1,x2,x3 st [x1,x,x2,x3] in X;
theorem :: XTUPLE_0:21
[x1,x,x2,x3] in X implies x in proj2_4 X;
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;
begin :: Boolean properties
registration let X be empty set;
cluster proj1 X -> empty;
end;
registration let X be empty set;
cluster proj2 X -> empty;
end;
registration let X be empty set;
cluster proj1_3 X -> empty;
end;
registration let X be empty set;
cluster proj2_3 X -> empty;
end;
registration let X be empty set;
cluster proj1_4 X -> empty;
end;
registration let X be empty set;
cluster proj2_4 X -> empty;
end;
theorem :: XTUPLE_0:23
proj1(X \/ Y) = proj1 X \/ proj1 Y;
theorem :: XTUPLE_0:24
proj1(X /\ Y) c= proj1 X /\ proj1 Y;
theorem :: XTUPLE_0:25
proj1 X \ proj1 Y c= proj1(X \ Y);
theorem :: XTUPLE_0:26
proj1 X \+\ proj1 Y c= proj1(X \+\ Y);
theorem :: XTUPLE_0:27
proj2(X \/ Y) = proj2 X \/ proj2 Y;
theorem :: XTUPLE_0:28
proj2(X /\ Y) c= proj2 X /\ proj2 Y;
theorem :: XTUPLE_0:29
proj2 X \ proj2 Y c= proj2(X \ Y);
theorem :: XTUPLE_0:30
proj2 X \+\ proj2 Y c= proj2(X \+\ Y);
theorem :: XTUPLE_0:31
proj1_3(X \/ Y) = proj1_3 X \/ proj1_3 Y;
theorem :: XTUPLE_0:32
proj1_3(X /\ Y) c= proj1_3 X /\ proj1_3 Y;
theorem :: XTUPLE_0:33
proj1_3 X \ proj1_3 Y c= proj1_3(X \ Y);
theorem :: XTUPLE_0:34
proj1_3 X \+\ proj1_3 Y c= proj1_3(X \+\ Y);
theorem :: XTUPLE_0:35
proj2_3(X \/ Y) = proj2_3 X \/ proj2_3 Y;
theorem :: XTUPLE_0:36
proj2_3(X /\ Y) c= proj2_3 X /\ proj2_3 Y;
theorem :: XTUPLE_0:37
proj2_3 X \ proj2_3 Y c= proj2_3(X \ Y);
theorem :: XTUPLE_0:38
proj2_3 X \+\ proj2_3 Y c= proj2_3(X \+\ Y);
theorem :: XTUPLE_0:39
proj1_4(X \/ Y) = proj1_4 X \/ proj1_4 Y;
theorem :: XTUPLE_0:40
proj1_4(X /\ Y) c= proj1_4 X /\ proj1_4 Y;
theorem :: XTUPLE_0:41
proj1_4 X \ proj1_4 Y c= proj1_4(X \ Y);
theorem :: XTUPLE_0:42
proj1_4 X \+\ proj1_4 Y c= proj1_4(X \+\ Y);
theorem :: XTUPLE_0:43
proj2_4(X \/ Y) = proj2_4 X \/ proj2_4 Y;
theorem :: XTUPLE_0:44
proj2_4(X /\ Y) c= proj2_4 X /\ proj2_4 Y;
theorem :: XTUPLE_0:45
proj2_4 X \ proj2_4 Y c= proj2_4(X \ Y);
theorem :: XTUPLE_0:46
proj2_4 X \+\ proj2_4 Y c= proj2_4(X \+\ Y);