Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998 Association of Mizar Users

### A Theory of Partitions. Part I

by
Shunichi Kobayashi, and
Kui Jia

MML identifier: PARTIT1
[ Mizar article, MML identifier index ]

```environ

vocabulary EQREL_1, BOOLE, SETFAM_1, TARSKI, CANTOR_1, FUNCT_1, RELAT_1,
T_1TOPSP, SUBSET_1, FINSEQ_1, ARYTM_1, LATTICES, PUA2MSS1, PARTIT1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1,
RELAT_1, FUNCT_1, FUNCT_2, SETFAM_1, PUA2MSS1, FINSEQ_1, FINSEQ_4,
EQREL_1, CANTOR_1, T_1TOPSP;
constructors NAT_1, FINSEQ_4, PUA2MSS1, CANTOR_1, T_1TOPSP, XREAL_0, MEMBERED;
clusters SUBSET_1, RELSET_1, ARYTM_3, SETFAM_1, MEMBERED, EQREL_1, PARTFUN1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;

begin

::Chap. 1  Preliminaries

reserve Y,Z for non empty set;
reserve PA,PB for a_partition of Y;
reserve A,B for Subset of Y;
reserve i,j,k for Nat;
reserve x,y,z,x1,x2,y1,z0,X,V,a,b,d,t,SFX,SFY for set;

theorem :: PARTIT1:1
X in PA & V in PA & X c= V implies X=V;

definition let SFX,SFY;
redefine pred SFX is_finer_than SFY;
synonym SFX '<' SFY;
synonym SFY '>' SFX;
end;

canceled;

theorem :: PARTIT1:3
union (SFX \ {{}}) = union SFX;

theorem :: PARTIT1:4
for PA,PB being a_partition of Y st
PA '>' PB & PB '>' PA holds PB c= PA;

theorem :: PARTIT1:5
for PA,PB being a_partition of Y st
PA '>' PB & PB '>' PA holds PA = PB;

canceled;

theorem :: PARTIT1:7
for PA,PB being a_partition of Y st
PA '>' PB holds PA is_coarser_than PB;

definition let Y;let PA be a_partition of Y,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;
end;

definition let Y;let PA,PB be a_partition of Y,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;
end;

theorem :: PARTIT1:8
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;

theorem :: PARTIT1:9
for PA being a_partition of Y holds
Y is_a_dependent_set_of PA;

theorem :: PARTIT1:10
for F being Subset-Family of Y st (Intersect(F)<>{} &
for X st X in F holds X is_a_dependent_set_of PA)
holds (Intersect(F) is_a_dependent_set_of PA);

theorem :: PARTIT1:11
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;

theorem :: PARTIT1:12
for X being Subset of Y holds
X is_a_dependent_set_of PA & X<>Y
implies X` is_a_dependent_set_of PA;

theorem :: PARTIT1:13
for y being Element of Y
ex X being Subset of Y st y in X & X is_min_depend PA,PB;

theorem :: PARTIT1:14
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;

definition
let Y be non empty set;
cluster -> non empty a_partition of Y;
end;

definition let Y be set;
func PARTITIONS(Y) means
:: PARTIT1:def 3
for x being set holds x in it iff x is a_partition of Y;
end;

definition
let Y be set;
cluster PARTITIONS(Y) -> non empty;
end;

begin

::Chap. 2  Join and Meet Operation between Partitions

definition let Y;let PA,PB be a_partition of Y;
func PA '/\' PB -> a_partition of Y equals
:: PARTIT1:def 4
INTERSECTION(PA,PB) \ {{}};
commutativity;
end;

theorem :: PARTIT1:15
for PA being a_partition of Y holds
PA '/\' PA = PA;

theorem :: PARTIT1:16
for PA,PB,PC being a_partition of Y holds
(PA '/\' PB) '/\' PC = PA '/\' (PB '/\' PC);

theorem :: PARTIT1:17
for PA,PB being a_partition of Y holds
PA '>' PA '/\' PB;

definition let Y;let PA,PB be a_partition of Y;
func PA '\/' PB -> a_partition of Y means
:: PARTIT1:def 5
for d holds d in it iff d is_min_depend PA,PB;
commutativity;
end;

canceled;

theorem :: PARTIT1:19
for PA,PB being a_partition of Y holds
PA '<' PA '\/' PB;

theorem :: PARTIT1:20
for PA being a_partition of Y holds
PA '\/' PA = PA;

theorem :: PARTIT1:21
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;

theorem :: PARTIT1:22
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;

begin

::Chap. 3  Partitions and Equivalence Relations

theorem :: PARTIT1:23
for PA being a_partition of Y
ex RA being Equivalence_Relation of Y st
for x,y holds [x,y] in RA iff ex A st A in PA & x in A & y in A;

definition let Y; let PA be a_partition of Y;
func ERl PA -> Equivalence_Relation of Y means
:: PARTIT1:def 6
for x1,x2 being set holds
[x1,x2] in it iff ex A st A in PA & x1 in A & x2 in A;
end;

definition let Y;
func Rel(Y) -> Function means
:: PARTIT1:def 7
dom it = PARTITIONS(Y) &
for x st x in PARTITIONS(Y) ex PA st PA = x & it.x = ERl PA;
end;

theorem :: PARTIT1:24
for PA,PB being a_partition of Y holds
PA '<' PB iff ERl(PA) c= ERl(PB);

theorem :: PARTIT1:25
for PA,PB being a_partition of Y,p0,x,y being set,
f being FinSequence of Y st p0 c= Y &
x in p0 & f.1=x & f.len f=y & 1 <= len f &
(for i st 1<=i & i<len f
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;

theorem :: PARTIT1:26
for R1,R2 being Equivalence_Relation of Y,f being FinSequence of Y,
x,y being set st x in Y & y in Y & f.1=x & f.len f=y & 1 <= len f &
(for i st 1<=i & i<len f
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);

theorem :: PARTIT1:27
for PA,PB being a_partition of Y holds
ERl(PA '\/' PB) = ERl(PA) "\/" ERl(PB);

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

theorem :: PARTIT1:29
for PA,PB being a_partition of Y st
ERl(PA) = ERl(PB) holds PA = PB;

theorem :: PARTIT1:30
for PA,PB,PC being a_partition of Y holds
(PA '\/' PB) '\/' PC = PA '\/' (PB '\/' PC);

theorem :: PARTIT1:31
for PA,PB being a_partition of Y holds
PA '/\' (PA '\/' PB) = PA;

theorem :: PARTIT1:32
for PA,PB being a_partition of Y holds
PA '\/' (PA '/\' PB) = PA;

theorem :: PARTIT1:33
for PA,PB,PC being a_partition of Y st
PA '<' PC & PB '<' PC holds PA '\/' PB '<' PC;

theorem :: PARTIT1:34
for PA,PB,PC being a_partition of Y st
PA '>' PC & PB '>' PC holds PA '/\' PB '>' PC;

definition let Y;
redefine func SmallestPartition Y;
synonym %I(Y);
end;

definition let Y;
canceled;

func %O(Y) -> a_partition of Y equals
:: PARTIT1:def 9
{Y};
end;

theorem :: PARTIT1:35
%I(Y)={B:ex x being set st B={x} & x in Y};

theorem :: PARTIT1:36
for PA being a_partition of Y holds
%O(Y) '>' PA & PA '>' %I(Y);

theorem :: PARTIT1:37
ERl(%O(Y)) = nabla Y;

theorem :: PARTIT1:38
ERl(%I(Y)) = id Y;

theorem :: PARTIT1:39
%I(Y) '<' %O(Y);

theorem :: PARTIT1:40
for PA being a_partition of Y holds
%O(Y) '\/' PA = %O(Y) & %O(Y) '/\' PA = PA;

theorem :: PARTIT1:41
for PA being a_partition of Y holds
%I(Y) '\/' PA = PA & %I(Y) '/\' PA = %I(Y);
```