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