:: A theory of partitions, { I }
:: by Shunichi Kobayashi and Kui Jia
::
:: Received October 5, 1998
:: Copyright (c) 1998-2012 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
proofend;

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 Th2: :: PARTIT1:2
for SFX being set holds union (SFX \ {{}}) = union SFX
proofend;

theorem Th3: :: PARTIT1:3
for Y being non empty set
for PA, PB being a_partition of Y st PA '>' PB &amp; PB '>' PA holds
PB c= PA
proofend;

theorem Th4: :: PARTIT1:4
for Y being non empty set
for PA, PB being a_partition of Y st PA '>' PB &amp; PB '>' PA holds
PA = PB
proofend;

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
proofend;

definition
let Y be non empty set ;
let PA be a_partition of Y;
let b be set ;
predb is_a_dependent_set_of PA means :Def1: :: PARTIT1:def 1
 ex B being set st
( B c= PA &amp; B <> {} &amp; 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 &amp; B <> {} &amp; b = union B ) );

definition
let Y be non empty set ;
let PA, PB be a_partition of Y;
let b be set ;
predb is_min_depend PA,PB means :Def2: :: PARTIT1:def 2
( b is_a_dependent_set_of PA &amp; b is_a_dependent_set_of PB &amp; ( for d being set st d c= b &amp; d is_a_dependent_set_of PA &amp; 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 &amp; b is_a_dependent_set_of PB &amp; ( for d being set st d c= b &amp; d is_a_dependent_set_of PA &amp; 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
proofend;

theorem Th7: :: PARTIT1:7
for Y being non empty set
for PA being a_partition of Y holds Y is_a_dependent_set_of PA
proofend;

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 <> {} &amp; ( 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
proofend;

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 &amp; X1 is_a_dependent_set_of PA &amp; X0 meets X1 holds
X0 /\ X1 is_a_dependent_set_of PA
proofend;

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 &amp; X <> Y holds
X ` is_a_dependent_set_of PA
proofend;

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 &amp; X is_min_depend PA,PB )
proofend;

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 &amp; A in P )
proofend;

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 b1 being set st
for x being set holds
( x in b1 iff x is a_partition of Y )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is a_partition of Y ) ) &amp; ( for x being set holds
( x in b2 iff x is a_partition of Y ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines PARTITIONS PARTIT1:def_3_:_
 for Y being set
for b2 being set holds
( b2 = PARTITIONS Y iff for x being set holds
( x in b2 iff x is a_partition of Y ) );

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

begin

::Chap. 2 Join and Meet Operation between Partitions
definition
let Y be non empty set ;
let PA, PB be a_partition of Y;
funcPA '/\' PB ->  a_partition of Y equals :: PARTIT1:def 4
(INTERSECTION (PA,PB)) \ {{}};
correctness
coherence
(INTERSECTION (PA,PB)) \ {{}} is a_partition of Y;
proofend;
commutativity
 for b1, PA, PB being a_partition of Y st b1 = (INTERSECTION (PA,PB)) \ {{}} holds
b1 = (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:13
for Y being non empty set
for PA being a_partition of Y holds PA '/\' PA = PA
proofend;

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)
proofend;

theorem Th15: :: PARTIT1:15
for Y being non empty set
for PA, PB being a_partition of Y holds PA '>' PA '/\' PB
proofend;

definition
let Y be non empty set ;
let PA, PB be a_partition of Y;
funcPA '\/' 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 b1 being a_partition of Y st
for d being set holds
( d in b1 iff d is_min_depend PA,PB )
proofend;
uniqueness
 for b1, b2 being a_partition of Y st ( for d being set holds
( d in b1 iff d is_min_depend PA,PB ) ) &amp; ( for d being set holds
( d in b2 iff d is_min_depend PA,PB ) ) holds
b1 = b2
proofend;
commutativity
 for b1, PA, PB being a_partition of Y st ( for d being set holds
( d in b1 iff d is_min_depend PA,PB ) ) holds
for d being set holds
( d in b1 iff d is_min_depend PB,PA )
proofend;
end;

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

theorem Th16: :: PARTIT1:16
for Y being non empty set
for PA, PB being a_partition of Y holds PA '<' PA '\/' PB
proofend;

theorem :: PARTIT1:17
for Y being non empty set
for PA being a_partition of Y holds PA '\/' PA = PA
proofend;

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 &amp; x in PC &amp; z0 in PA &amp; t in x &amp; t in z0 holds
z0 c= x
proofend;

theorem :: PARTIT1:19
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 &amp; z0 in PA &amp; t in x &amp; t in z0 holds
z0 c= x by Th16, Th18;

begin

::Chap. 3 Partitions and Equivalence Relations
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 &amp; x1 in A &amp; x2 in A ) );
existence
 ex b1 being Equivalence_Relation of Y st
for x1, x2 being set holds
( [x1,x2] in b1 iff ex A being Subset of Y st
( A in PA &amp; x1 in A &amp; x2 in A ) )
proofend;
uniqueness
 for b1, b2 being Equivalence_Relation of Y st ( for x1, x2 being set holds
( [x1,x2] in b1 iff ex A being Subset of Y st
( A in PA &amp; x1 in A &amp; x2 in A ) ) ) &amp; ( for x1, x2 being set holds
( [x1,x2] in b2 iff ex A being Subset of Y st
( A in PA &amp; x1 in A &amp; x2 in A ) ) ) holds
b1 = b2
proofend;
end;

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

definition
let Y be non empty set ;
defpred S1[ set , set ] means  ex PA being a_partition of Y st
( PA = $1 &amp; $2 = ERl PA );
A1: for x being set st x in PARTITIONS Y holds
ex z being set st S1[x,z]
proofend;
func Rel Y ->  Function means :: PARTIT1:def 7
( dom it = PARTITIONS Y &amp; ( for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x &amp; it . x = ERl PA ) ) );
existence
 ex b1 being Function st
( dom b1 = PARTITIONS Y &amp; ( for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x &amp; b1 . x = ERl PA ) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = PARTITIONS Y &amp; ( for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x &amp; b1 . x = ERl PA ) ) &amp; dom b2 = PARTITIONS Y &amp; ( for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x &amp; b2 . x = ERl PA ) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines Rel PARTIT1:def_7_:_
 for Y being non empty set
for b2 being Function holds
( b2 = Rel Y iff ( dom b2 = PARTITIONS Y &amp; ( for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x &amp; b2 . x = ERl PA ) ) ) );

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 )
proofend;

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 &amp; x in p0 &amp; f . 1 = x &amp; f . (len f) = y &amp; 1 <= len f &amp; ( for i being Element of NAT st 1 <= i &amp; i < len f holds
ex p2, p3, u being set st
( p2 in PA &amp; p3 in PB &amp; f . i in p2 &amp; u in p2 &amp; u in p3 &amp; f . (i + 1) in p3 ) ) &amp; p0 is_a_dependent_set_of PA &amp; p0 is_a_dependent_set_of PB holds
y in p0
proofend;

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 &amp; f . 1 = x &amp; f . (len f) = y &amp; 1 <= len f &amp; ( for i being Element of NAT st 1 <= i &amp; i < len f holds
ex u being set st
( u in Y &amp; [(f . i),u] in R1 \/ R2 &amp; [u,(f . (i + 1))] in R1 \/ R2 ) ) holds
[x,y] in R1 "\/" R2
proofend;

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)
proofend;

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)
proofend;

theorem Th25: :: PARTIT1:25
for Y being non empty set
for PA, PB being a_partition of Y st ERl PA = ERl PB holds
PA = PB
proofend;

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)
proofend;

theorem :: PARTIT1:27
for Y being non empty set
for PA, PB being a_partition of Y holds PA '/\' (PA '\/' PB) = PA
proofend;

theorem :: PARTIT1:28
for Y being non empty set
for PA, PB being a_partition of Y holds PA '\/' (PA '/\' PB) = PA
proofend;

theorem Th29: :: PARTIT1:29
for Y being non empty set
for PA, PB, PC being a_partition of Y st PA '<' PC &amp; PB '<' PC holds
PA '\/' PB '<' PC
proofend;

theorem :: PARTIT1:30
for Y being non empty set
for PA, PB, PC being a_partition of Y st PA '>' PC &amp; PB '>' PC holds
PA '/\' PB '>' PC
proofend;

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

definition
let Y be non empty set ;
func %O Y ->  a_partition of Y equals :: PARTIT1:def 8
{Y};
correctness
coherence
{Y} is a_partition of Y;
proofend;
end;

:: deftheorem  defines %O PARTIT1:def_8_:_
 for Y being non empty set holds %O Y = {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} &amp; x in Y )  }
proofend;

theorem Th32: :: PARTIT1:32
for Y being non empty set
for PA being a_partition of Y holds
( %O Y '>' PA &amp; PA '>' %I Y )
proofend;

theorem Th33: :: PARTIT1:33
for Y being non empty set holds ERl (%O Y) = nabla Y
proofend;

theorem Th34: :: PARTIT1:34
for Y being non empty set holds ERl (%I Y) = id Y
proofend;

theorem :: PARTIT1:35
for Y being non empty set holds %I Y '<' %O Y
proofend;

theorem :: PARTIT1:36
for Y being non empty set
for PA being a_partition of Y holds
( (%O Y) '\/' PA = %O Y &amp; (%O Y) '/\' PA = PA )
proofend;

theorem :: PARTIT1:37
for Y being non empty set
for PA being a_partition of Y holds
( (%I Y) '\/' PA = PA &amp; (%I Y) '/\' PA = %I Y )
proofend;