:: Properties of First and Second Order Cutting of Binary Relations
:: by Krzysztof Retel
::
:: Received April 25, 2005
:: Copyright (c) 2005-2016 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