:: 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 b1 being set st
for x being set holds
( x in b1 iff x is a_partition of Y )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is a_partition of Y ) ) & ( for x being set holds
( x in b2 iff x is a_partition of Y ) ) holds
b1 = b2
proof end;
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
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 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: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 b1 being a_partition of Y st
for d being set holds
( d in b1 iff d is_min_depend PA,PB )
proof end;
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 ) ) & ( for d being set holds
( d in b2 iff d is_min_depend PA,PB ) ) holds
b1 = b2
proof end;
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 )
proof end;
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 :: 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 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 & x1 in A & x2 in A ) )
by Th23;
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 & x1 in A & x2 in A ) ) ) & ( for x1, x2 being set holds
( [x1,x2] in b2 iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) ) holds
b1 = b2
proof end;
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 & x1 in A & 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 & $2 = ERl PA );
A1: for x being set st x in PARTITIONS Y holds
ex z being set st S1[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 b1 being Function st
( dom b1 = PARTITIONS Y & ( for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x & b1 . x = ERl PA ) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = PARTITIONS Y & ( for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x & b1 . x = ERl PA ) ) & dom b2 = PARTITIONS Y & ( for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x & b2 . x = ERl PA ) ) holds
b1 = b2
proof end;
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 & ( for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x & b2 . 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;