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