:: A theory of partitions, { I }
:: by Shunichi Kobayashi and Kui Jia
::
:: Received October 5, 1998
:: Copyright (c) 1998-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, EQREL_1, SUBSET_1, TARSKI, SETFAM_1, FUNCT_1,
RELAT_1, ZFMISC_1, FINSEQ_1, XXREAL_0, ARYTM_3, CARD_1, ORDINAL4,
PARTIT1, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
NAT_1, RELAT_1, FUNCT_1, FUNCT_2, SETFAM_1, FINSEQ_1, FINSEQ_4, EQREL_1,
XXREAL_0;
constructors SETFAM_1, FUNCT_2, XXREAL_0, XREAL_0, NAT_1, MEMBERED, EQREL_1,
FINSEQ_4, RELSET_1, DOMAIN_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELSET_1, PARTFUN1, MEMBERED, EQREL_1,
NAT_1, XXREAL_0;
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;
notation
let SFX,SFY;
synonym SFX '<' SFY for SFX is_finer_than SFY;
synonym SFY '>' SFX for SFX is_finer_than SFY;
end;
theorem :: PARTIT1:2
union (SFX \ {{}}) = union SFX;
theorem :: PARTIT1:3
for PA,PB being a_partition of Y st PA '>' PB & PB '>' PA holds PB c= PA;
theorem :: PARTIT1:4
for PA,PB being a_partition of Y st PA '>' PB & PB '>' PA holds PA = PB;
theorem :: PARTIT1:5
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:6
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:7
for PA being a_partition of Y holds Y is_a_dependent_set_of PA;
theorem :: PARTIT1:8
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:9
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:10
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:11
for y being Element of Y
ex X being Subset of Y st y in X & X is_min_depend PA,PB;
theorem :: PARTIT1:12
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 set;
func PARTITIONS(Y) -> set means
:: PARTIT1:def 3
for x being set holds x in it iff x is a_partition of Y;
end;
registration
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:13
for PA being a_partition of Y holds PA '/\' PA = PA;
theorem :: PARTIT1:14
for PA,PB,PC being a_partition of Y holds
(PA '/\' PB) '/\' PC = PA '/\' (PB '/\' PC);
theorem :: PARTIT1:15
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;
theorem :: PARTIT1:16
for PA,PB being a_partition of Y holds PA '<' PA '\/' PB;
theorem :: PARTIT1:17
for PA being a_partition of Y holds PA '\/' PA = PA;
theorem :: PARTIT1:18
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:19
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
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 object 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 being object st x in PARTITIONS(Y) ex PA st PA = x & it.x = ERl PA;
end;
theorem :: PARTIT1:20
for PA,PB being a_partition of Y holds PA '<' PB iff ERl(PA) c= ERl(PB);
theorem :: PARTIT1:21
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' PC & PB '>' PC holds PA '/\' PB '>' PC;
notation
let Y;
synonym %I(Y) for SmallestPartition Y;
end;
definition let Y; ::: technical type update
redefine func %I Y -> a_partition of Y;
end;
definition
let Y;
func %O(Y) -> a_partition of Y equals
:: PARTIT1:def 8
{Y};
end;
theorem :: PARTIT1:31
%I(Y)={B:ex x being set st B={x} & x in Y};
theorem :: PARTIT1:32
for PA being a_partition of Y holds %O(Y) '>' PA & PA '>' %I(Y);
theorem :: PARTIT1:33
ERl(%O(Y)) = nabla Y;
theorem :: PARTIT1:34
ERl(%I(Y)) = id Y;
theorem :: PARTIT1:35
%I(Y) '<' %O(Y);
theorem :: PARTIT1:36
for PA being a_partition of Y holds
%O(Y) '\/' PA = %O(Y) & %O(Y) '/\' PA = PA;
theorem :: PARTIT1:37
for PA being a_partition of Y holds
%I(Y) '\/' PA = PA & %I(Y) '/\' PA = %I(Y);