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

notation

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

end;

theorem Th1: :: RELSET_2:1

for y being object
for X being set holds
( y in {_{X}_} iff ex x being object st
( y = {x} & x in X ) )

proof end;

theorem Th2: :: RELSET_2:2

for X being set holds
( X = {} iff {_{X}_} = {} )

proof end;

theorem Th3: :: RELSET_2:3

for X, Y being set holds {_{(X \/ Y)}_} = {_{X}_} \/ {_{Y}_}

proof end;

theorem Th4: :: RELSET_2:4

for X, Y being set holds {_{(X /\ Y)}_} = {_{X}_} /\ {_{Y}_}

proof end;

theorem :: RELSET_2:5

for X, Y being set holds {_{(X \ Y)}_} = {_{X}_} \ {_{Y}_}

proof end;

theorem Th6: :: RELSET_2:6

for X, Y being set holds
( X c= Y iff {_{X}_} c= {_{Y}_} )

proof end;

theorem :: RELSET_2:7

for M being set
for B1, B2 being Subset-Family of M holds (Intersect B1) /\ (Intersect B2) c= Intersect (B1 /\ B2)

proof end;

theorem :: RELSET_2:8

for P, Q, R being Relation holds (P /\ Q) * R c= (P * R) /\ (Q * R)

proof end;

theorem Th9: :: RELSET_2:9

for x, y being object
for R being Relation holds
( y in Im (R,x) iff [x,y] in R )

proof end;

theorem Th10: :: RELSET_2:10

for x being object
for R1, R2 being Relation holds Im ((R1 \/ R2),x) = (Im (R1,x)) \/ (Im (R2,x))

proof end;

theorem Th11: :: RELSET_2:11

for x being object
for R1, R2 being Relation holds Im ((R1 /\ R2),x) = (Im (R1,x)) /\ (Im (R2,x))

proof end;

theorem :: RELSET_2:12

for x being object
for R1, R2 being Relation holds Im ((R1 \ R2),x) = (Im (R1,x)) \ (Im (R2,x))

proof end;

theorem :: RELSET_2:13

for X being set
for R1, R2 being Relation holds (R1 /\ R2) .: {_{X}_} c= (R1 .: {_{X}_}) /\ (R2 .: {_{X}_})

proof end;

definition

let X, Y be set ;
let R be Relation of X,Y;
let x be object ;
:: original: Im
redefine func Im (R,x) -> Subset of Y;
coherence
Im (R,x) is Subset of Y

proof end;

:: original: Coim
redefine func Coim (R,x) -> Subset of X;
coherence
Coim (R,x) is Subset of X

proof end;

end;

theorem :: RELSET_2:14

for A being set
for F being Subset-Family of A
for R being Relation holds R .: (union F) = union { (R .: X) where X is Subset of A : X in F }

proof end;

:: (3.1.2) - RELAT_1:149

theorem Th15: :: RELSET_2:15

for A being set
for X being Subset of A holds X = union { {x} where x is Element of A : x in X }

proof end;

theorem :: RELSET_2:16

for A being set
for X being Subset of A holds { {x} where x is Element of A : x in X } is Subset-Family of A

proof end;

theorem :: RELSET_2:17

for A, B being set
for X being Subset of A
for R being Relation of A,B holds R .: X = union { (Class (R,x)) where x is Element of A : x in X }

proof end;

theorem :: RELSET_2:18

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

proof end;

definition

let A be set ;
let R be Relation;

func .: (R,A) -> Function means :Def1: :: RELSET_2:def 1
( dom it = bool A & ( for X being set st X c= A holds
it . X = R .: X ) );

existence
ex b₁ being Function st
( dom b₁ = bool A & ( for X being set st X c= A holds
b₁ . X = R .: X ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = bool A & ( for X being set st X c= A holds
b₁ . X = R .: X ) & dom b₂ = bool A & ( for X being set st X c= A holds
b₂ . X = R .: X ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines .: RELSET_2:def 1 :
for A being set
for R being Relation
for b₃ being Function holds
( b₃ = .: (R,A) iff ( dom b₃ = bool A & ( for X being set st X c= A holds
b₃ . X = R .: X ) ) );

notation

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

end;

theorem Th19: :: RELSET_2:19

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

proof end;

theorem Th20: :: RELSET_2:20

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

proof end;

theorem Th21: :: RELSET_2:21

for A, B being set
for R being Subset of [:A,B:] holds .: is Function of (bool A),(bool (rng R))

proof end;

definition

let B, A be set ;
let R be Subset of [:A,B:];
:: original: .:
redefine func .: R -> Function of (bool A),(bool B);
correctness
coherence
.: (R,A) is Function of (bool A),(bool B);

proof end;

end;

theorem :: RELSET_2:22

for A, B being set
for R being Subset of [:A,B:] holds union ((.: R) .: A) c= R .: (union A)

proof end;

definition

let A, B be set ;
let X be Subset of A;
let R be Subset of [:A,B:];

func R .:^ X -> set equals :: RELSET_2:def 2
Intersect ((.: R) .: {_{X}_});

correctness
coherence
Intersect ((.: R) .: {_{X}_}) is set ;
;

end;

:: deftheorem defines .:^ RELSET_2:def 2 :
for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] holds R .:^ X = Intersect ((.: R) .: {_{X}_});

definition

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

end;

theorem Th23: :: RELSET_2:23

for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] holds
( (.: R) .: {_{X}_} = {} iff X = {} )

proof end;

theorem Th24: :: RELSET_2:24

for y being object
for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] st y in R .:^ X holds
for x being set st x in X holds
y in Im (R,x)

proof end;

theorem Th25: :: RELSET_2:25

for B being non empty set
for A being set
for X being Subset of A
for y being Element of B
for 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) )

proof end;

theorem :: RELSET_2:26

for A, B being set
for X1, X2 being Subset of A
for R being Subset of [:A,B:] st (.: R) .: {_{X1}_} = {} holds
R .:^ (X1 \/ X2) = R .:^ X2

proof end;

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

for A, B being set
for X1, X2 being Subset of A
for R being Subset of [:A,B:] holds R .:^ (X1 \/ X2) = (R .:^ X1) /\ (R .:^ X2)

proof end;

theorem :: RELSET_2:28

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

proof end;

theorem Th29: :: RELSET_2:29

for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] st X = {} holds
R .:^ X = B by Th23, SETFAM_1:def 9;

theorem :: RELSET_2:30

for A being set
for B being non empty set
for R being Relation of A,B
for F being Subset-Family of A
for 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

proof end;

theorem Th31: :: RELSET_2:31

for A, B being set
for X1, X2 being Subset of A
for R being Subset of [:A,B:] st X1 c= X2 holds
R .:^ X2 c= R .:^ X1

proof end;

theorem :: RELSET_2:32

for A, B being set
for X1, X2 being Subset of A
for R being Subset of [:A,B:] holds (R .:^ X1) \/ (R .:^ X2) c= R .:^ (X1 /\ X2)

proof end;

theorem :: RELSET_2:33

for A, B being set
for X being Subset of A
for R1, R2 being Subset of [:A,B:] holds (R1 /\ R2) .:^ X = (R1 .:^ X) /\ (R2 .:^ X)

proof end;

theorem :: RELSET_2:34

for A, B being set
for X being Subset of A
for FR being Subset-Family of [:A,B:] holds (union FR) .: X = union { (R .: X) where R is Subset of [:A,B:] : R in FR }

proof end;

:: (7.1.2) - RELAT_1:150

theorem :: RELSET_2:35

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

proof end;

:: (11.2) theorem TH40.

theorem Th36: :: RELSET_2:36

for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] st R = {} & X <> {} holds
R .:^ X = {}

proof end;

theorem Th37: :: RELSET_2:37

for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] st R = [:A,B:] holds
R .:^ X = B

proof end;

theorem :: RELSET_2:38

for A, B being set
for X being Subset of A
for FR being Subset-Family of [:A,B:]
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

proof end;

theorem :: RELSET_2:39

for A, B being set
for X being Subset of A
for R1, R2 being Subset of [:A,B:] st R1 c= R2 holds
R1 .:^ X c= R2 .:^ X

proof end;

theorem :: RELSET_2:40

for A, B being set
for X being Subset of A
for R1, R2 being Subset of [:A,B:] holds (R1 .:^ X) \/ (R2 .:^ X) c= (R1 \/ R2) .:^ X

proof end;

theorem Th41: :: RELSET_2:41

for x, y being object
for A, B being set
for R being Subset of [:A,B:] holds
( y in Im ((R `),x) iff ( not [x,y] in R & x in A & y in B ) )

proof end;

theorem :: RELSET_2:42

for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] st X <> {} holds
R .:^ X c= R .: X

proof end;

theorem Th43: :: RELSET_2:43

for A, B being set
for R being Subset of [:A,B:]
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) ) )

proof end;

theorem Th44: :: RELSET_2:44

for A, B being set
for R being Subset of [:A,B:]
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 )

proof end;

theorem Th45: :: RELSET_2:45

for A, B being set
for X being Subset of A
for Y being Subset of B
for R being Subset of [:A,B:] holds
( X misses (R ~) .: Y iff Y misses R .: X )

proof end;

theorem Th46: :: RELSET_2:46

for A, B being set
for R being Subset of [:A,B:]
for X being set holds R .: X = R .: (X /\ (proj1 R))

proof end;

theorem Th47: :: RELSET_2:47

for A, B being set
for R being Subset of [:A,B:]
for Y being set holds (R ~) .: Y = (R ~) .: (Y /\ (proj2 R))

proof end;

theorem Th48: :: RELSET_2:48

for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] holds (R .:^ X) ` = (R `) .: X

proof end;

definition

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

proof end;

end;

theorem Th49: :: RELSET_2:49

for A, B being set
for X being Subset of A
for R being Relation of A,B holds (R .: X) ` = (R `) .:^ X

proof end;

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

theorem Th50: :: RELSET_2:50

for A, B being set
for R being Relation of A,B holds
( proj1 R = (R ~) .: B & proj2 R = R .: A )

proof end;

theorem :: RELSET_2:51

for A, B, C being set
for R being Relation of A,B
for S being Relation of B,C holds
( proj1 (R * S) = (R ~) .: (proj1 S) & proj1 (R * S) c= proj1 R )

proof end;

theorem :: RELSET_2:52

for A, B, C being set
for R being Relation of A,B
for S being Relation of B,C holds
( proj2 (R * S) = S .: (proj2 R) & proj2 (R * S) c= proj2 S )

proof end;

theorem :: RELSET_2:53

for A, B being set
for X being Subset of A
for R being Relation of A,B holds
( X c= proj1 R iff X c= (R * (R ~)) .: X )

proof end;

theorem :: RELSET_2:54

for A, B being set
for Y being Subset of B
for R being Relation of A,B holds
( Y c= proj2 R iff Y c= ((R ~) * R) .: Y )

proof end;

theorem :: RELSET_2:55

for A, B being set
for R being Relation of A,B holds
( proj1 R = (R ~) .: B & (R ~) .: (R .: A) = (R ~) .: (proj2 R) ) by Th50;

theorem :: RELSET_2:56

for A, B being set
for R being Relation of A,B holds (R ~) .: B = (R * (R ~)) .: A

proof end;

theorem :: RELSET_2:57

for A, B being set
for R being Relation of A,B holds R .: A = ((R ~) * R) .: B

proof end;

theorem :: RELSET_2:58

for A, B, C being set
for X being Subset of A
for R being Relation of A,B
for S being Relation of B,C holds S .:^ (R .: X) = ((R * (S `)) `) .:^ X

proof end;

theorem Th59: :: RELSET_2:59

for A, B being set
for R being Relation of A,B holds (R `) ~ = (R ~) `

proof end;

theorem Th60: :: RELSET_2:60

for A, B being set
for X being Subset of A
for Y being Subset of B
for R being Relation of A,B holds
( X c= (R ~) .:^ Y iff Y c= R .:^ X )

proof end;

theorem :: RELSET_2:61

for A, B being set
for X being Subset of A
for Y being Subset of B
for R being Relation of A,B holds
( R .: (X `) c= Y ` iff (R ~) .: Y c= X )

proof end;

theorem :: RELSET_2:62

for A, B being set
for X being Subset of A
for Y being Subset of B
for R being Relation of A,B holds
( X c= (R ~) .:^ (R .:^ X) & Y c= R .:^ ((R ~) .:^ Y) ) by Th60;

theorem :: RELSET_2:63

for A, B being set
for X being Subset of A
for Y being Subset of B
for R being Relation of A,B holds
( R .:^ X = R .:^ ((R ~) .:^ (R .:^ X)) & (R ~) .:^ Y = (R ~) .:^ (R .:^ ((R ~) .:^ Y)) )

proof end;

theorem :: RELSET_2:64

for A, B being set
for R being Relation of A,B holds (id A) * R = R * (id B)

proof end;