:: A theory of partitions, { I }
:: by Shunichi Kobayashi and Kui Jia
::
:: Received October 5, 1998
:: Copyright (c) 1998-2011 Association of Mizar Users

begin

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

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;

theorem :: PARTIT1:2

canceled;

theorem Th3: :: PARTIT1:3

for SFX being set holds union (SFX \ {{}}) = union SFX

proof end;

theorem Th4: :: PARTIT1:4

for Y being non empty set
for PA, PB being a_partition of Y st PA '>' PB & PB '>' PA holds
PB c= PA

proof end;

theorem Th5: :: PARTIT1:5

for Y being non empty set
for PA, PB being a_partition of Y st PA '>' PB & PB '>' PA holds
PA = PB

proof end;

theorem :: PARTIT1:6

canceled;

theorem Th7: :: PARTIT1:7

for Y being non empty set
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 ;
pred b is_a_dependent_set_of PA means :Def1: :: PARTIT1:def 1
ex B being set st
( B c= PA & B <> {} & b = union B );

end;

:: deftheorem Def1 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 ) );

definition

let Y be non empty set ;
let PA, PB be a_partition of Y;
let b be set ;
pred b is_min_depend PA,PB means :Def2: :: 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 ) );

end;

:: deftheorem Def2 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 ) ) );

theorem Th8: :: PARTIT1:8

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

proof end;

theorem Th9: :: PARTIT1:9

for Y being non empty set
for PA being a_partition of Y holds Y 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 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 Th11: :: PARTIT1:11

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

proof end;

theorem Th12: :: PARTIT1:12

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

proof end;

theorem Th13: :: PARTIT1:13

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 )

proof end;

theorem :: PARTIT1:14

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 )

proof end;

definition

let Y be set ;
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
ex b₁ being set st
for x being set holds
( x in b₁ iff x is a_partition of Y )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being set holds
( x in b₁ iff x is a_partition of Y ) ) & ( for x being set holds
( x in b₂ iff x is a_partition of Y ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines PARTITIONS PARTIT1:def 3 :
for Y being set
for b₂ being set holds
( b₂ = PARTITIONS Y iff for x being set holds
( x in b₂ iff x is a_partition of Y ) );

registration

let Y be set ;
cluster PARTITIONS Y -> non empty ;
coherence
not PARTITIONS Y is empty

proof end;

end;

begin

definition

let Y be non empty set ;
let PA, PB be a_partition of Y;
func PA '/\' PB -> a_partition of Y equals :: PARTIT1:def 4
(INTERSECTION (PA,PB)) \ {{}};
correctness
coherence
(INTERSECTION (PA,PB)) \ {{}} is a_partition of Y;

proof end;

commutativity
for b₁, PA, PB being a_partition of Y st b₁ = (INTERSECTION (PA,PB)) \ {{}} holds
b₁ = (INTERSECTION (PB,PA)) \ {{}} ;

end;

:: 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)) \ {{}};

theorem :: PARTIT1:15

for Y being non empty set
for PA being a_partition of Y holds PA '/\' PA = PA

proof end;

theorem :: PARTIT1:16

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

proof end;

theorem Th17: :: PARTIT1:17

for Y being non empty set
for PA, PB being a_partition of Y holds PA '>' PA '/\' PB

proof end;

definition

let Y be non empty set ;
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
ex b₁ being a_partition of Y st
for d being set holds
( d in b₁ iff d is_min_depend PA,PB )

proof end;

uniqueness
for b₁, b₂ being a_partition of Y st ( for d being set holds
( d in b₁ iff d is_min_depend PA,PB ) ) & ( for d being set holds
( d in b₂ iff d is_min_depend PA,PB ) ) holds
b₁ = b₂

proof end;

commutativity
for b₁, PA, PB being a_partition of Y st ( for d being set holds
( d in b₁ iff d is_min_depend PA,PB ) ) holds
for d being set holds
( d in b₁ iff d is_min_depend PB,PA )

proof end;

end;

:: deftheorem Def5 defines '\/' PARTIT1:def 5 :
for Y being non empty set
for PA, PB, b₄ being a_partition of Y holds
( b₄ = PA '\/' PB iff for d being set holds
( d in b₄ iff d is_min_depend PA,PB ) );

theorem :: PARTIT1:18

canceled;

theorem Th19: :: PARTIT1:19

for Y being non empty set
for PA, PB being a_partition of Y holds PA '<' PA '\/' PB

proof end;

theorem :: PARTIT1:20

for Y being non empty set
for PA being a_partition of Y holds PA '\/' PA = PA

proof end;

theorem Th21: :: PARTIT1:21

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

proof end;

theorem :: PARTIT1:22

for Y being non empty set
for x, z0, t being set
for PA, PB being a_partition of Y st x in PA '\/' PB & z0 in PA & t in x & t in z0 holds
z0 c= x by Th19, Th21;

begin

theorem Th23: :: PARTIT1:23

for Y being non empty set
for PA being a_partition of Y ex RA being Equivalence_Relation of Y st
for x, y being set holds
( [x,y] in RA iff ex A being Subset of Y st
( A in PA & x in A & y in A ) )

proof end;

definition

let Y be non empty set ;
let PA be a_partition of Y;
func ERl PA -> Equivalence_Relation of Y means :Def6: :: PARTIT1:def 6
for x1, x2 being set holds
( [x1,x2] in it iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) );
existence
ex b₁ being Equivalence_Relation of Y st
for x1, x2 being set holds
( [x1,x2] in b₁ iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) by Th23;
uniqueness
for b₁, b₂ being Equivalence_Relation of Y st ( for x1, x2 being set holds
( [x1,x2] in b₁ iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) ) & ( for x1, x2 being set holds
( [x1,x2] in b₂ iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines ERl PARTIT1:def 6 :
for Y being non empty set
for PA being a_partition of Y
for b₃ being Equivalence_Relation of Y holds
( b₃ = ERl PA iff for x1, x2 being set holds
( [x1,x2] in b₃ iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) );

definition

let Y be non empty set ;
defpred S₁[ set , set ] means ex PA being a_partition of Y st
( PA = $1 & $2 = ERl PA );
A1: for x being set st x in PARTITIONS Y holds
ex z being set st S₁[x,z]

proof end;

func Rel Y -> Function means :: PARTIT1:def 7
( dom it = PARTITIONS Y & ( for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x & it . x = ERl PA ) ) );
existence
ex b₁ being Function st
( dom b₁ = PARTITIONS Y & ( for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x & b₁ . x = ERl PA ) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = PARTITIONS Y & ( for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x & b₁ . x = ERl PA ) ) & dom b₂ = PARTITIONS Y & ( for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x & b₂ . x = ERl PA ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines Rel PARTIT1:def 7 :
for Y being non empty set
for b₂ being Function holds
( b₂ = Rel Y iff ( dom b₂ = PARTITIONS Y & ( for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x & b₂ . x = ERl PA ) ) ) );

theorem Th24: :: PARTIT1:24

for Y being non empty set
for PA, PB being a_partition of Y holds
( PA '<' PB iff ERl PA c= ERl PB )

proof end;

theorem Th25: :: PARTIT1:25

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 Element of 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 Th26: :: PARTIT1:26

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 Element of 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 Th27: :: PARTIT1:27

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

proof end;

theorem Th28: :: PARTIT1:28

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

proof end;

theorem Th29: :: PARTIT1:29

for Y being non empty set
for PA, PB being a_partition of Y st ERl PA = ERl PB holds
PA = PB

proof end;

theorem :: PARTIT1:30

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

proof end;

theorem :: PARTIT1:31

for Y being non empty set
for PA, PB being a_partition of Y holds PA '/\' (PA '\/' PB) = PA

proof end;

theorem :: PARTIT1:32

for Y being non empty set
for PA, PB being a_partition of Y holds PA '\/' (PA '/\' PB) = PA

proof end;

theorem Th33: :: PARTIT1:33

for Y being non empty set
for PA, PB, PC being a_partition of Y st PA '<' PC & PB '<' PC holds
PA '\/' PB '<' PC

proof end;

theorem :: PARTIT1:34

for Y being non empty set
for PA, PB, PC being a_partition of Y st PA '>' PC & PB '>' PC holds
PA '/\' PB '>' PC

proof end;

notation

let Y be non empty set ;
synonym %I Y for SmallestPartition Y;

end;

definition

let Y be non empty set ;
canceled;
func %O Y -> a_partition of Y equals :: PARTIT1:def 9
{Y};
correctness
coherence
{Y} is a_partition of Y;

proof end;

end;

:: deftheorem PARTIT1:def 8 :
canceled;

:: deftheorem defines %O PARTIT1:def 9 :
for Y being non empty set holds %O Y = {Y};

theorem :: PARTIT1:35

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 ) }

proof end;

theorem Th36: :: PARTIT1:36

for Y being non empty set
for PA being a_partition of Y holds
( %O Y '>' PA & PA '>' %I Y )

proof end;

theorem Th37: :: PARTIT1:37

for Y being non empty set holds ERl (%O Y) = nabla Y

proof end;

theorem Th38: :: PARTIT1:38

for Y being non empty set holds ERl (%I Y) = id Y

proof end;

theorem :: PARTIT1:39

for Y being non empty set holds %I Y '<' %O Y

proof end;

theorem :: PARTIT1:40

for Y being non empty set
for PA being a_partition of Y holds
( (%O Y) '\/' PA = %O Y & (%O Y) '/\' PA = PA )

proof end;

theorem :: PARTIT1:41

for Y being non empty set
for PA being a_partition of Y holds
( (%I Y) '\/' PA = PA & (%I Y) '/\' PA = %I Y )

proof end;