:: Properties of First and Second Order Cutting of Binary Relations
::  by Krzysztof Retel
::
:: Received April 25, 2005
:: Copyright (c) 2005-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, EQREL_1, XBOOLE_0, SUBSET_1, TARSKI, SETFAM_1, ZFMISC_1,
      FUNCT_1, RELSET_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, SETFAM_1, RELAT_1,
      FUNCT_1, RELSET_1, FUNCT_2, EQREL_1;
 constructors SETFAM_1, FUNCT_2, EQREL_1, RELSET_1, DOMAIN_1, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, PARTFUN1, RELSET_1;
 requirements SUBSET, BOOLE;


begin :: Preliminaries
:: Formalisation of first paragraph from the article:
:: "Relations binaries, fermetures, correspondances de Galois" (1948),
:: Prof. Jacques Riguet,
:: Bulettin de la S.M.F., tome 76 (1948), p.114-155.

reserve x,y for object,X,Y,A,B,C,M for set;
reserve P,Q,R,R1,R2 for Relation;

notation
  let X be set;
  synonym {_{X}_} for SmallestPartition X;
end;

theorem :: RELSET_2:1
  y in {_{X}_} iff ex x st y = {x} & x in X;

theorem :: RELSET_2:2
  X = {} iff {_{X}_} = {};

theorem :: RELSET_2:3
  {_{X\/Y}_} = {_{X}_} \/ {_{Y}_};

theorem :: RELSET_2:4
  {_{X/\Y}_} = {_{X}_} /\ {_{Y}_};

theorem :: RELSET_2:5
  {_{X\Y}_} = {_{X}_} \ {_{Y}_};

theorem :: RELSET_2:6
  X c= Y iff {_{X}_} c= {_{Y}_};

theorem :: RELSET_2:7
  for B1, B2 being Subset-Family of M holds
  Intersect(B1) /\ Intersect(B2) c= Intersect(B1 /\ B2);

theorem :: RELSET_2:8 :: (27.2)
  (P /\ Q)*R c= (P*R) /\ (Q*R);

begin

theorem :: RELSET_2:9
  y in Im(R,x) iff [x,y] in R;

theorem :: RELSET_2:10
  Im(R1 \/ R2,x) = Im(R1,x) \/ Im(R2,x);

theorem :: RELSET_2:11
  Im(R1 /\ R2,x) = Im(R1,x) /\ Im(R2,x);

theorem :: RELSET_2:12
  Im(R1 \ R2,x) = Im(R1,x) \ Im(R2,x);

theorem :: RELSET_2:13
  (R1 /\ R2).:{_{X}_} c= R1.:{_{X}_} /\ R2.:{_{X}_};

definition
  let X,Y be set;
  let R be Relation of X,Y;
  let x be object;
  redefine func Im(R,x) -> Subset of Y;
  redefine func Coim(R,x) -> Subset of X;
end;

theorem :: RELSET_2:14
  for A being set, F being Subset-Family of A, R be Relation holds
  R.: union F = union {R.:X where X is Subset of A: X in F};

:: (3.1.2) - RELAT_1:149

theorem :: RELSET_2:15
  for A being set, X being Subset of A holds
    X = union {{x} where x is Element of A: x in X};

theorem :: RELSET_2:16
  for A being set, X being Subset of A holds
  {{x} where x is Element of A: x in X} is Subset-Family of A;

theorem :: RELSET_2:17 :: R(X) - original counterpart. The First Order Cutting.
  for A, B being set, X being Subset of A, R being Relation of A,B
  holds R.:X = union {Class(R,x) where x is Element of A: x in X};

theorem :: RELSET_2:18
  for A being non empty set, B being set, X being Subset of A,
  R being Relation of A,B holds
  {R.:x where x is Element of A: x in X} is Subset-Family of B;

definition
  let A be set, R be Relation;
  func .:(R,A) -> Function means
:: RELSET_2:def 1

  dom it = bool A & for X being set st X c= A holds it.X = R.:X;
end;

notation
  let B,A be set;
  let R be Subset of [:A,B:];
  synonym .:R for .:(R,A);
end;

theorem :: RELSET_2:19
  for A,B being set, R being Subset of [:A,B:] st
  X in dom(.:R) holds (.:R).X = R.:X;

theorem :: RELSET_2:20
  for A,B being set, R being Subset of [:A,B:] holds rng(.:R) c= bool rng R;

theorem :: RELSET_2:21
  for A,B being set, R being Subset of [:A,B:] holds
    .:R is Function of bool A, bool rng R;

definition
  let B,A be set;
  let R be Subset of [:A,B:];
  redefine func .:R -> Function of bool A, bool B;
end;

theorem :: RELSET_2:22 :: FUNCT_3:15
  for A,B being set, R being Subset of [:A,B:] holds
    union((.:R).:A) c= R.:(union A);

begin :: The second order cutting of binary relation of two sets A,B
      :: under a subset of the set A

reserve X,X1,X2 for Subset of A;
reserve Y for Subset of B;
reserve R,R1,R2 for Subset of [:A,B:];
reserve FR for Subset-Family of [:A,B:];

definition
  let A,B be set, X be Subset of A, R be Subset of [:A,B:];
  func R.:^X -> set equals
:: RELSET_2:def 2
  Intersect(.:R.:{_{X}_});
end;

definition
  let A,B be set;
  let X be Subset of A;
  let R be Subset of [:A,B:];
  redefine func R.:^X -> Subset of B;
end;

theorem :: RELSET_2:23
  .:R.:{_{X}_} = {} iff X = {};

theorem :: RELSET_2:24
  y in R.:^X implies for x being set st x in X holds y in Im(R,x);

theorem :: RELSET_2:25
  for B being non empty set, A being set, X being Subset of A,
  y being Element of B, R being Subset of [:A,B:] holds
  y in R.:^X iff for x being set st x in X holds y in Im(R,x);

theorem :: RELSET_2:26
  (.:R).:{_{X1}_} = {} implies R.:^(X1\/X2) = R.:^X2;

:: ksiazka S o R = SR a w MML jest to R*S
:: (1) S .:(R.:X) = (S o R).:X
:: w notacji uzytej w MML:  S.:(R.:X) = (R*S).:X

theorem :: RELSET_2:27 :: (2)
  R.:^(X1\/X2) = (R.:^X1) /\ (R.:^X2);

theorem :: RELSET_2:28
  for A being non empty set, B being set, F being Subset-Family of A,
  R being Relation of A,B
  holds {R.:^X where X is Subset of A: X in F} is Subset-Family of B;

theorem :: RELSET_2:29  :: (3.2.2)
  X = {} implies R.:^X = B;

theorem :: RELSET_2:30 :: (3.2.1)
  for A being set,B being non empty set, R being Relation of A,B,
  F being Subset-Family of A, G being Subset-Family of B st
  G = {R.:^Y where Y is Subset of A: Y in F} holds R.:^(union F) = Intersect G;

theorem :: RELSET_2:31  :: (4)
  X1 c= X2 implies R.:^X2 c= R.:^X1;

theorem :: RELSET_2:32 :: (5)
  R.:^X1 \/ R.:^X2 c= R.:^(X1/\X2);

theorem :: RELSET_2:33 :: (6)
  (R1 /\ R2).:^X = (R1.:^X) /\ (R2.:^X);

theorem :: RELSET_2:34 :: (7.1.1)
  (union FR).:X = union {R.:X where R is Subset of [:A,B:]: R in FR};

:: (7.1.2) - RELAT_1:150

theorem :: RELSET_2:35
  for FR being Subset-Family of [:A,B:], A,B being set,
  X being Subset of A holds
  {R.:^X where R is Subset of [:A,B:]: R in FR} is Subset-Family of B;

:: (11.2) theorem TH40.

theorem :: RELSET_2:36  :: (11.1)
  R = {} & X <> {} implies R.:^X = {};

theorem :: RELSET_2:37  :: (7.2.2)
  R = [:A,B:] implies R.:^X = B;

theorem :: RELSET_2:38 :: (7.2.1)
  for G being Subset-Family of B st
  G = {R.:^X where R is Subset of [:A,B:]: R in FR} holds
  (Intersect FR).:^X = Intersect G;

theorem :: RELSET_2:39 :: (8)
  R1 c= R2 implies R1.:^X c= R2.:^X;

theorem :: RELSET_2:40 :: (9)
  (R1.:^X) \/ (R2.:^X) c= (R1 \/ R2).:^X;

theorem :: RELSET_2:41
  y in Im(R`,x) iff not [x,y] in R & x in A & y in B;

theorem :: RELSET_2:42 :: (17)
  X <> {} implies R.:^X c= R.:X;

theorem :: RELSET_2:43
  for X, Y being set holds
  X meets R~.:Y iff ex x,y being set st x in X & y in Y & x in Im(R~,y);

theorem :: RELSET_2:44
  for X, Y being set holds
  (ex x,y being set st x in X & y in Y & x in Im(R~,y)) iff Y meets R.:X;

theorem :: RELSET_2:45  :: (19)
  X misses R~.:Y iff Y misses R.:X;

theorem :: RELSET_2:46  :: (14.1)
  for X being set holds R.:X = R.:(X /\ proj1 R);

theorem :: RELSET_2:47  :: (14.2)
  for Y being set holds (R~).:Y = (R~).:(Y /\ proj2 R);

theorem :: RELSET_2:48  :: (10.2)
  (R.:^X)` = R`.:X;

reserve R for Relation of A,B;
reserve S for Relation of B,C;

definition
  let A,B,C be set;
  let R be Subset of [:A,B:], S be Subset of [:B,C:];
  redefine func R*S -> Relation of A,C;
end;

theorem :: RELSET_2:49  :: (10.1)
  (R.:X)` = (R`).:^X;

:: (12) - FUNCT_5:20, RELAT_1:37

theorem :: RELSET_2:50
  proj1 R = (R~).:B & proj2 R = R.:A;

theorem :: RELSET_2:51 :: (13.1)
  proj1 (R*S) = (R~).:(proj1 S) & proj1 (R*S) c= proj1 R;

theorem :: RELSET_2:52 :: (13.2)
  proj2 (R*S) = S.:(proj2 R) & proj2 (R*S) c= proj2 S;

theorem :: RELSET_2:53 :: (15.1)
  X c= proj1 R iff X c= (R*(R~)).:X;

theorem :: RELSET_2:54 :: (15.2)
  Y c= proj2 R iff Y c= ((R~)*R).:Y;

theorem :: RELSET_2:55
  proj1 R = (R~).:B & (R~).:(R.:A) = (R~).:(proj2 R);

theorem :: RELSET_2:56 :: (16.1)
  (R~).:B = (R*(R~)).:A;

theorem :: RELSET_2:57 :: (16.2)
  R.:A = (R~*R).:B;

theorem :: RELSET_2:58 :: (18)
  S.:^(R.:X) = (R*S`)`.:^X;

theorem :: RELSET_2:59  :: (24.3)
  (R`)~ = (R~)`;

theorem :: RELSET_2:60  :: (20)
  X c= (R~).:^Y iff Y c= R.:^X;

theorem :: RELSET_2:61 :: (21)
  R.:(X`) c= Y` iff R~.:Y c= X;

theorem :: RELSET_2:62 :: (22)
  X c= (R~).:^(R.:^X) & Y c= R.:^((R~).:^Y);

theorem :: RELSET_2:63 :: (23)
  R.:^X = R.:^( R~.:^(R.:^X) ) & R~.:^Y = (R~).:^(R.:^((R~).:^Y));

theorem :: RELSET_2:64 :: (29.3)
  (id A)*R = R*(id B);

:: (24.1) - RELAT_1:40
:: (24.2) - RELAT_1:39
:: (24.4) - RELAT_1:54
:: (24.5) - R1 c= R2 implies R1~ c= R2~   :: SYSREL:27
:: (24.6) - R~~ = R; atomatically
:: (25.1) - RELAT_1:51
:: (25.2) - (S1 \/ S2)*R = S1*R \/ S2*R   :: SYSREL:20
:: (26) - RELAT_1:50
:: (27.1) - RELAT_1:52
:: (28.1) and (28.2) - RELAT_1:62
:: (29.1) and (29.2) - FUNCT_2:23