:: by Shunichi Kobayashi and Kui Jia

::

:: Received October 5, 1998

:: Copyright (c) 1998-2021 Association of Mizar Users

theorem Th1: :: PARTIT1:1

for Y being non empty set

for PA being a_partition of Y

for X, V being set st X in PA & V in PA & X c= V holds

X = V

for PA being a_partition of Y

for X, V being set st X in PA & V in PA & X c= V holds

X = V

proof end;

notation

let SFX, SFY be set ;

synonym SFX '<' SFY for SFX is_finer_than SFY;

synonym SFY '>' SFX for SFX is_finer_than SFY;

end;
synonym SFX '<' SFY for SFX is_finer_than SFY;

synonym SFY '>' SFX for SFX is_finer_than SFY;

theorem Th5: :: PARTIT1:5

for Y being non empty set

for PA, PB being a_partition of Y st PA '>' PB holds

PA is_coarser_than PB

for PA, PB being a_partition of Y st PA '>' PB holds

PA is_coarser_than PB

proof end;

definition

let Y be non empty set ;

let PA be a_partition of Y;

let b be set ;

end;
let PA be a_partition of Y;

let b be set ;

pred b is_a_dependent_set_of PA means :: PARTIT1:def 1

ex B being set st

( B c= PA & B <> {} & b = union B );

ex B being set st

( B c= PA & B <> {} & b = union B );

:: deftheorem defines is_a_dependent_set_of PARTIT1:def 1 :

for Y being non empty set

for PA being a_partition of Y

for b being set holds

( b is_a_dependent_set_of PA iff ex B being set st

( B c= PA & B <> {} & b = union B ) );

for Y being non empty set

for PA being a_partition of Y

for b being set holds

( b is_a_dependent_set_of PA iff ex B being set st

( B c= PA & B <> {} & b = union B ) );

definition

let Y be non empty set ;

let PA, PB be a_partition of Y;

let b be set ;

end;
let PA, PB be a_partition of Y;

let b be set ;

pred b is_min_depend PA,PB means :: PARTIT1:def 2

( b is_a_dependent_set_of PA & b is_a_dependent_set_of PB & ( for d being set st d c= b & d is_a_dependent_set_of PA & d is_a_dependent_set_of PB holds

d = b ) );

( b is_a_dependent_set_of PA & b is_a_dependent_set_of PB & ( for d being set st d c= b & d is_a_dependent_set_of PA & d is_a_dependent_set_of PB holds

d = b ) );

:: deftheorem defines is_min_depend PARTIT1:def 2 :

for Y being non empty set

for PA, PB being a_partition of Y

for b being set holds

( b is_min_depend PA,PB iff ( b is_a_dependent_set_of PA & b is_a_dependent_set_of PB & ( for d being set st d c= b & d is_a_dependent_set_of PA & d is_a_dependent_set_of PB holds

d = b ) ) );

for Y being non empty set

for PA, PB being a_partition of Y

for b being set holds

( b is_min_depend PA,PB iff ( b is_a_dependent_set_of PA & b is_a_dependent_set_of PB & ( for d being set st d c= b & d is_a_dependent_set_of PA & d is_a_dependent_set_of PB holds

d = b ) ) );

theorem Th6: :: PARTIT1:6

for Y being non empty set

for PA, PB being a_partition of Y st PA '>' PB holds

for b being set st b in PA holds

b is_a_dependent_set_of PB

for PA, PB being a_partition of Y st PA '>' PB holds

for b being set st b in PA holds

b is_a_dependent_set_of PB

proof end;

theorem Th8: :: PARTIT1:8

for Y being non empty set

for PA being a_partition of Y

for F being Subset-Family of Y st Intersect F <> {} & ( for X being set st X in F holds

X is_a_dependent_set_of PA ) holds

Intersect F is_a_dependent_set_of PA

for PA being a_partition of Y

for F being Subset-Family of Y st Intersect F <> {} & ( for X being set st X in F holds

X is_a_dependent_set_of PA ) holds

Intersect F is_a_dependent_set_of PA

proof end;

theorem Th9: :: PARTIT1:9

for Y being non empty set

for PA being a_partition of Y

for X0, X1 being Subset of Y st X0 is_a_dependent_set_of PA & X1 is_a_dependent_set_of PA & X0 meets X1 holds

X0 /\ X1 is_a_dependent_set_of PA

for PA being a_partition of Y

for X0, X1 being Subset of Y st X0 is_a_dependent_set_of PA & X1 is_a_dependent_set_of PA & X0 meets X1 holds

X0 /\ X1 is_a_dependent_set_of PA

proof end;

theorem Th10: :: PARTIT1:10

for Y being non empty set

for PA being a_partition of Y

for X being Subset of Y st X is_a_dependent_set_of PA & X <> Y holds

X ` is_a_dependent_set_of PA

for PA being a_partition of Y

for X being Subset of Y st X is_a_dependent_set_of PA & X <> Y holds

X ` is_a_dependent_set_of PA

proof end;

theorem Th11: :: PARTIT1:11

for Y being non empty set

for PA, PB being a_partition of Y

for y being Element of Y ex X being Subset of Y st

( y in X & X is_min_depend PA,PB )

for PA, PB being a_partition of Y

for y being Element of Y ex X being Subset of Y st

( y in X & X is_min_depend PA,PB )

proof end;

theorem :: PARTIT1:12

for Y being non empty set

for P being a_partition of Y

for y being Element of Y ex A being Subset of Y st

( y in A & A in P )

for P being a_partition of Y

for y being Element of Y ex A being Subset of Y st

( y in A & A in P )

proof end;

definition

let Y be set ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff x is a_partition of Y )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff x is a_partition of Y ) ) & ( for x being set holds

( x in b_{2} iff x is a_partition of Y ) ) holds

b_{1} = b_{2}

end;
func PARTITIONS Y -> set means :Def3: :: PARTIT1:def 3

for x being set holds

( x in it iff x is a_partition of Y );

existence for x being set holds

( x in it iff x is a_partition of Y );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def3 defines PARTITIONS PARTIT1:def 3 :

for Y, b_{2} being set holds

( b_{2} = PARTITIONS Y iff for x being set holds

( x in b_{2} iff x is a_partition of Y ) );

for Y, b

( b

( x in b

registration
end;

definition

let Y be non empty set ;

let PA, PB be a_partition of Y;

correctness

coherence

(INTERSECTION (PA,PB)) \ {{}} is a_partition of Y;

for b_{1}, PA, PB being a_partition of Y st b_{1} = (INTERSECTION (PA,PB)) \ {{}} holds

b_{1} = (INTERSECTION (PB,PA)) \ {{}}
;

end;
let PA, PB be a_partition of Y;

correctness

coherence

(INTERSECTION (PA,PB)) \ {{}} is a_partition of Y;

proof end;

commutativity for b

b

:: deftheorem defines '/\' PARTIT1:def 4 :

for Y being non empty set

for PA, PB being a_partition of Y holds PA '/\' PB = (INTERSECTION (PA,PB)) \ {{}};

for Y being non empty set

for PA, PB being a_partition of Y holds PA '/\' PB = (INTERSECTION (PA,PB)) \ {{}};

theorem :: PARTIT1:14

for Y being non empty set

for PA, PB, PC being a_partition of Y holds (PA '/\' PB) '/\' PC = PA '/\' (PB '/\' PC)

for PA, PB, PC being a_partition of Y holds (PA '/\' PB) '/\' PC = PA '/\' (PB '/\' PC)

proof end;

definition

let Y be non empty set ;

let PA, PB be a_partition of Y;

ex b_{1} being a_partition of Y st

for d being set holds

( d in b_{1} iff d is_min_depend PA,PB )

for b_{1}, b_{2} being a_partition of Y st ( for d being set holds

( d in b_{1} iff d is_min_depend PA,PB ) ) & ( for d being set holds

( d in b_{2} iff d is_min_depend PA,PB ) ) holds

b_{1} = b_{2}

for b_{1}, PA, PB being a_partition of Y st ( for d being set holds

( d in b_{1} iff d is_min_depend PA,PB ) ) holds

for d being set holds

( d in b_{1} iff d is_min_depend PB,PA )

end;
let PA, PB be a_partition of Y;

func PA '\/' PB -> a_partition of Y means :Def5: :: PARTIT1:def 5

for d being set holds

( d in it iff d is_min_depend PA,PB );

existence for d being set holds

( d in it iff d is_min_depend PA,PB );

ex b

for d being set holds

( d in b

proof end;

uniqueness for b

( d in b

( d in b

b

proof end;

commutativity for b

( d in b

for d being set holds

( d in b

proof end;

:: deftheorem Def5 defines '\/' PARTIT1:def 5 :

for Y being non empty set

for PA, PB, b_{4} being a_partition of Y holds

( b_{4} = PA '\/' PB iff for d being set holds

( d in b_{4} iff d is_min_depend PA,PB ) );

for Y being non empty set

for PA, PB, b

( b

( d in b

theorem Th18: :: PARTIT1:18

for Y being non empty set

for x, z0, t being set

for PA, PC being a_partition of Y st PA '<' PC & x in PC & z0 in PA & t in x & t in z0 holds

z0 c= x

for x, z0, t being set

for PA, PC being a_partition of Y st PA '<' PC & x in PC & z0 in PA & t in x & t in z0 holds

z0 c= x

proof end;

theorem :: PARTIT1:19

definition

let Y be set ;

let PA be a_partition of Y;

ex b_{1} being Equivalence_Relation of Y st

for x1, x2 being object holds

( [x1,x2] in b_{1} iff ex A being Subset of Y st

( A in PA & x1 in A & x2 in A ) )

for b_{1}, b_{2} being Equivalence_Relation of Y st ( for x1, x2 being object holds

( [x1,x2] in b_{1} iff ex A being Subset of Y st

( A in PA & x1 in A & x2 in A ) ) ) & ( for x1, x2 being object holds

( [x1,x2] in b_{2} iff ex A being Subset of Y st

( A in PA & x1 in A & x2 in A ) ) ) holds

b_{1} = b_{2}

end;
let PA be a_partition of Y;

func ERl PA -> Equivalence_Relation of Y means :Def6: :: PARTIT1:def 6

for x1, x2 being object holds

( [x1,x2] in it iff ex A being Subset of Y st

( A in PA & x1 in A & x2 in A ) );

existence for x1, x2 being object holds

( [x1,x2] in it iff ex A being Subset of Y st

( A in PA & x1 in A & x2 in A ) );

ex b

for x1, x2 being object holds

( [x1,x2] in b

( A in PA & x1 in A & x2 in A ) )

proof end;

uniqueness for b

( [x1,x2] in b

( A in PA & x1 in A & x2 in A ) ) ) & ( for x1, x2 being object holds

( [x1,x2] in b

( A in PA & x1 in A & x2 in A ) ) ) holds

b

proof end;

:: deftheorem Def6 defines ERl PARTIT1:def 6 :

for Y being set

for PA being a_partition of Y

for b_{3} being Equivalence_Relation of Y holds

( b_{3} = ERl PA iff for x1, x2 being object holds

( [x1,x2] in b_{3} iff ex A being Subset of Y st

( A in PA & x1 in A & x2 in A ) ) );

for Y being set

for PA being a_partition of Y

for b

( b

( [x1,x2] in b

( A in PA & x1 in A & x2 in A ) ) );

definition

let Y be non empty set ;

defpred S_{1}[ object , object ] means ex PA being a_partition of Y st

( PA = $1 & $2 = ERl PA );

A1: for x being object st x in PARTITIONS Y holds

ex z being object st S_{1}[x,z]

ex b_{1} being Function st

( dom b_{1} = PARTITIONS Y & ( for x being object st x in PARTITIONS Y holds

ex PA being a_partition of Y st

( PA = x & b_{1} . x = ERl PA ) ) )

for b_{1}, b_{2} being Function st dom b_{1} = PARTITIONS Y & ( for x being object st x in PARTITIONS Y holds

ex PA being a_partition of Y st

( PA = x & b_{1} . x = ERl PA ) ) & dom b_{2} = PARTITIONS Y & ( for x being object st x in PARTITIONS Y holds

ex PA being a_partition of Y st

( PA = x & b_{2} . x = ERl PA ) ) holds

b_{1} = b_{2}

end;
defpred S

( PA = $1 & $2 = ERl PA );

A1: for x being object st x in PARTITIONS Y holds

ex z being object st S

proof end;

func Rel Y -> Function means :: PARTIT1:def 7

( dom it = PARTITIONS Y & ( for x being object st x in PARTITIONS Y holds

ex PA being a_partition of Y st

( PA = x & it . x = ERl PA ) ) );

existence ( dom it = PARTITIONS Y & ( for x being object st x in PARTITIONS Y holds

ex PA being a_partition of Y st

( PA = x & it . x = ERl PA ) ) );

ex b

( dom b

ex PA being a_partition of Y st

( PA = x & b

proof end;

uniqueness for b

ex PA being a_partition of Y st

( PA = x & b

ex PA being a_partition of Y st

( PA = x & b

b

proof end;

:: deftheorem defines Rel PARTIT1:def 7 :

for Y being non empty set

for b_{2} being Function holds

( b_{2} = Rel Y iff ( dom b_{2} = PARTITIONS Y & ( for x being object st x in PARTITIONS Y holds

ex PA being a_partition of Y st

( PA = x & b_{2} . x = ERl PA ) ) ) );

for Y being non empty set

for b

( b

ex PA being a_partition of Y st

( PA = x & b

theorem Th20: :: PARTIT1:20

for Y being non empty set

for PA, PB being a_partition of Y holds

( PA '<' PB iff ERl PA c= ERl PB )

for PA, PB being a_partition of Y holds

( PA '<' PB iff ERl PA c= ERl PB )

proof end;

theorem Th21: :: PARTIT1:21

for Y being non empty set

for PA, PB being a_partition of Y

for p0, x, y being set

for f being FinSequence of Y st p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Nat st 1 <= i & i < len f holds

ex p2, p3, u being set st

( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB holds

y in p0

for PA, PB being a_partition of Y

for p0, x, y being set

for f being FinSequence of Y st p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Nat st 1 <= i & i < len f holds

ex p2, p3, u being set st

( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB holds

y in p0

proof end;

theorem Th22: :: PARTIT1:22

for Y being non empty set

for R1, R2 being Equivalence_Relation of Y

for f being FinSequence of Y

for x, y being set st x in Y & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Nat st 1 <= i & i < len f holds

ex u being set st

( u in Y & [(f . i),u] in R1 \/ R2 & [u,(f . (i + 1))] in R1 \/ R2 ) ) holds

[x,y] in R1 "\/" R2

for R1, R2 being Equivalence_Relation of Y

for f being FinSequence of Y

for x, y being set st x in Y & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Nat st 1 <= i & i < len f holds

ex u being set st

( u in Y & [(f . i),u] in R1 \/ R2 & [u,(f . (i + 1))] in R1 \/ R2 ) ) holds

[x,y] in R1 "\/" R2

proof end;

theorem Th23: :: PARTIT1:23

for Y being non empty set

for PA, PB being a_partition of Y holds ERl (PA '\/' PB) = (ERl PA) "\/" (ERl PB)

for PA, PB being a_partition of Y holds ERl (PA '\/' PB) = (ERl PA) "\/" (ERl PB)

proof end;

theorem Th24: :: PARTIT1:24

for Y being non empty set

for PA, PB being a_partition of Y holds ERl (PA '/\' PB) = (ERl PA) /\ (ERl PB)

for PA, PB being a_partition of Y holds ERl (PA '/\' PB) = (ERl PA) /\ (ERl PB)

proof end;

theorem :: PARTIT1:26

for Y being non empty set

for PA, PB, PC being a_partition of Y holds (PA '\/' PB) '\/' PC = PA '\/' (PB '\/' PC)

for PA, PB, PC being a_partition of Y holds (PA '\/' PB) '\/' PC = PA '\/' (PB '\/' PC)

proof end;

theorem Th29: :: PARTIT1:29

for Y being non empty set

for PA, PB, PC being a_partition of Y st PA '<' PC & PB '<' PC holds

PA '\/' PB '<' PC

for PA, PB, PC being a_partition of Y st PA '<' PC & PB '<' PC holds

PA '\/' PB '<' PC

proof end;

theorem :: PARTIT1:30

for Y being non empty set

for PA, PB, PC being a_partition of Y st PA '>' PC & PB '>' PC holds

PA '/\' PB '>' PC

for PA, PB, PC being a_partition of Y st PA '>' PC & PB '>' PC holds

PA '/\' PB '>' PC

proof end;

definition

let Y be non empty set ;

:: original: %I

redefine func %I Y -> a_partition of Y;

correctness

coherence

%I Y is a_partition of Y;

;

end;
:: original: %I

redefine func %I Y -> a_partition of Y;

correctness

coherence

%I Y is a_partition of Y;

;

theorem :: PARTIT1:31

for Y being non empty set holds %I Y = { B where B is Subset of Y : ex x being set st

( B = {x} & x in Y ) }

( B = {x} & x in Y ) }

proof end;

theorem :: PARTIT1:36

for Y being non empty set

for PA being a_partition of Y holds

( (%O Y) '\/' PA = %O Y & (%O Y) '/\' PA = PA )

for PA being a_partition of Y holds

( (%O Y) '\/' PA = %O Y & (%O Y) '/\' PA = PA )

proof end;

theorem :: PARTIT1:37

for Y being non empty set

for PA being a_partition of Y holds

( (%I Y) '\/' PA = PA & (%I Y) '/\' PA = %I Y )

for PA being a_partition of Y holds

( (%I Y) '\/' PA = PA & (%I Y) '/\' PA = %I Y )

proof end;