:: Monoid of Multisets and Subsets
:: by Grzegorz Bancerek
::
:: Received December 29, 1992
:: Copyright (c) 1992-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 SUBSET_1, NUMBERS, ALGSTR_0, MESFUNC1, XBOOLE_0, FUNCT_1,
ZFMISC_1, FINSEQ_4, FUNCT_2, RELAT_1, PARTFUN1, TARSKI, FUNCOP_1,
FINSEQ_2, FINSEQ_1, BINOP_1, SETWISEO, ALGSTR_1, MONOID_0, LATTICE2,
MCART_1, STRUCT_0, GROUP_1, VECTSP_1, BINOP_2, CARD_1, ARYTM_3, FUNCT_3,
FINSET_1, ORDINAL4, COMPLEX1, ARYTM_1, MONOID_1, NAT_1, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XXREAL_0, XCMPLX_0, REAL_1, NAT_1, RELAT_1, STRUCT_0, FUNCT_1, FINSEQ_1,
MONOID_0, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, RECDEF_1,
SETWISEO, FINSET_1, FUNCT_3, FINSEQ_2, LATTICE2, FUNCT_6, DOMAIN_1,
ALGSTR_0;
constructors BINOP_1, DOMAIN_1, FUNCT_3, SETWISEO, REAL_1, BINOP_2, RECDEF_1,
FUNCT_5, FUNCT_6, LATTICE2, MONOID_0, RELSET_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
FUNCOP_1, FINSET_1, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, MONOID_0, CARD_1,
RELSET_1, XTUPLE_0, VALUED_0;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Updating
reserve x,y,z, X,Y,Z for set,
n for Element of NAT;
definition
let f be Function, x1,x2,y be set;
func f..(x1,x2,y) -> set equals
:: MONOID_1:def 1
f..([x1,x2],y);
end;
definition
let A,D1,D2,D be non empty set;
let f be Function of [:D1, D2:], Funcs(A,D);
let x1 be Element of D1;
let x2 be Element of D2;
let x be Element of A;
redefine func f..(x1,x2,x) -> Element of D;
end;
definition
let A be set;
let D1,D2,D be non empty set, f be Function of [:D1,D2:],D;
let g1 be Function of A,D1;
let g2 be Function of A,D2;
redefine func f.:(g1,g2) -> Element of Funcs(A,D);
end;
notation
let A be non empty set;
let n be Element of NAT, x be Element of A;
synonym n .--> x for n |-> x;
end;
definition
let A be non empty set;
let n be Element of NAT, x be Element of A;
redefine func n .--> x -> FinSequence of A;
end;
definition
let D be non empty set, A be set, d be Element of D;
redefine func A --> d -> Element of Funcs(A,D);
end;
definition
let A be set;
let D1,D2,D be non empty set, f be Function of [:D1,D2:],D;
let d be Element of D1;
let g be Function of A,D2;
redefine func f[;](d,g) -> Element of Funcs(A,D);
end;
definition
let A be set;
let D1,D2,D be non empty set, f be Function of [:D1,D2:],D;
let g be Function of A,D1;
let d be Element of D2;
redefine func f[:](g,d) -> Element of Funcs(A,D);
end;
theorem :: MONOID_1:1
for f,g being Function, X being set holds (f|X)*g = f*(X|`g);
scheme :: MONOID_1:sch 1
NonUniqFuncDEx { X() -> set, Y() -> non empty set, P[object,object] }:
ex f being
Function of X(), Y() st for x being object st x in X() holds P[x,f.x]
provided
for x being object st x in X() ex y being Element of Y() st P[x,y];
begin :: Monoid of functions into a semigroup
definition
let D1,D2,D be non empty set;
let f be Function of [:D1,D2:],D;
let A be set;
func (f,D).:A -> Function of [:Funcs(A,D1), Funcs(A,D2):], Funcs(A,D)
means
:: MONOID_1:def 2
for f1 being Element of Funcs(A,D1) for f2 being Element of Funcs(A,D2)
holds it.(f1,f2) = f.:(f1,f2);
end;
theorem :: MONOID_1:2
for D1,D2,D being non empty set for f being Function of [:D1,D2:],D for A
being set, f1 being (Function of A,D1), f2 being Function of A,D2 for x st x in
A holds ((f,D).:A)..(f1,f2,x) = f.(f1.x,f2.x);
reserve A for set,
D for non empty set,
a,b,c,l,r for Element of D,
o,o9 for BinOp of D,
f,g,h for Function of A,D;
theorem :: MONOID_1:3
o is commutative implies o.:(f,g) = o.:(g,f);
theorem :: MONOID_1:4
o is associative implies o.:(o.:(f,g),h) = o.:(f,o.:(g,h));
theorem :: MONOID_1:5
a is_a_unity_wrt o implies o[;](a,f) = f & o[:](f,a) = f;
theorem :: MONOID_1:6
o is idempotent implies o.:(f,f) = f;
theorem :: MONOID_1:7
o is commutative implies (o,D).:A is commutative;
theorem :: MONOID_1:8
o is associative implies (o,D).:A is associative;
theorem :: MONOID_1:9
a is_a_unity_wrt o implies A --> a is_a_unity_wrt (o,D).:A;
theorem :: MONOID_1:10
o is having_a_unity implies the_unity_wrt (o,D).:A = A -->
the_unity_wrt o & (o,D).:A is having_a_unity;
theorem :: MONOID_1:11
o is idempotent implies (o,D).:A is idempotent;
theorem :: MONOID_1:12
o is invertible implies (o,D).:A is invertible;
theorem :: MONOID_1:13
o is cancelable implies (o,D).:A is cancelable;
theorem :: MONOID_1:14
o is uniquely-decomposable implies (o,D).:A is uniquely-decomposable;
theorem :: MONOID_1:15
o absorbs o9 implies (o,D).:A absorbs (o9,D).:A;
theorem :: MONOID_1:16
for D1, D2, D, E1, E2, E being non empty set, o1 being Function
of [:D1, D2:], D, o2 being Function of [:E1, E2:], E st o1 c= o2
holds (o1,D).:A c= (o2,E).:A;
definition
let G be non empty multMagma;
let A be set;
func .:(G,A) -> multMagma equals
:: MONOID_1:def 3
multLoopStr (# Funcs(A, the carrier
of G), (the multF of G,the carrier of G).:A, A --> the_unity_wrt the multF of G
#) if G is unital otherwise multMagma (# Funcs(A, the carrier of G), (the multF
of G,the carrier of G).:A #);
end;
registration
let G be non empty multMagma;
let A be set;
cluster .:(G,A) -> non empty;
end;
reserve G for non empty multMagma;
theorem :: MONOID_1:17
the carrier of .:(G,X) = Funcs(X, the carrier of G) & the multF
of .:(G,X) = (the multF of G, the carrier of G).:X;
theorem :: MONOID_1:18
x is Element of .: (G,X) iff x is Function of X, the carrier of G;
registration
let G be non empty multMagma, A be set;
cluster .:(G,A) -> constituted-Functions;
end;
theorem :: MONOID_1:19
for f being Element of .:(G,X) holds dom f = X & rng f c= the carrier of G;
theorem :: MONOID_1:20
for f,g being Element of .:(G,X) st
for x being object st x in X holds f.x = g.x holds f = g;
definition
let G be non empty multMagma, A be non empty set;
let f be Element of .:(G,A);
let a be Element of A;
redefine func f.a -> Element of G;
end;
registration
let G be non empty multMagma, A be non empty set;
let f be Element of .:(G,A);
cluster rng f -> non empty;
end;
theorem :: MONOID_1:21
for f1,f2 being Element of .:(G,D), a being Element of D holds (
f1*f2).a = (f1.a)*(f2.a);
definition
let G be unital non empty multMagma;
let A be set;
redefine func .:(G,A) -> well-unital constituted-Functions strict non empty
multLoopStr;
end;
theorem :: MONOID_1:22
for G being unital non empty multMagma holds 1..:(G,X) = X -->
the_unity_wrt the multF of G;
theorem :: MONOID_1:23
for G being non empty multMagma, A being set holds (G is
commutative implies .:(G,A) is commutative) & (G is associative implies .:(G,A)
is associative) & (G is idempotent implies .:(G,A) is idempotent) & (G is
invertible implies .:(G,A) is invertible) & (G is cancelable implies .:(G,A) is
cancelable) & (G is uniquely-decomposable implies .:(G,A) is
uniquely-decomposable);
theorem :: MONOID_1:24
for H being non empty SubStr of G holds .:(H,X) is SubStr of .:(G,X);
theorem :: MONOID_1:25
for G being unital non empty multMagma, H being non empty SubStr of
G st the_unity_wrt the multF of G in the carrier of H holds .:(H,X) is
MonoidalSubStr of .:(G,X);
definition
let G be unital associative commutative cancelable uniquely-decomposable
non empty multMagma;
let A be set;
redefine func .:(G,A) -> commutative cancelable uniquely-decomposable
constituted-Functions strict Monoid;
end;
begin :: Monoid of multisets over a set
definition
let A be set;
func MultiSet_over A -> commutative cancelable uniquely-decomposable
constituted-Functions strict Monoid equals
:: MONOID_1:def 4
.:(, A);
end;
theorem :: MONOID_1:26
the carrier of MultiSet_over X = Funcs(X,NAT) & the multF of
MultiSet_over X = (addnat,NAT).:X & 1.MultiSet_over X = X --> 0;
definition
let A be set;
mode Multiset of A is Element of MultiSet_over A;
end;
theorem :: MONOID_1:27
x is Multiset of X iff x is Function of X,NAT;
theorem :: MONOID_1:28
for m being Multiset of X holds dom m = X & rng m c= NAT;
registration
let X;
cluster -> NAT-valued for Multiset of X;
end;
theorem :: MONOID_1:29
for m1,m2 being Multiset of D, a being Element of D holds
(m1 [*] m2).a = (m1.a)+(m2.a);
theorem :: MONOID_1:30
chi(Y,X) is Multiset of X;
definition
let Y,X;
redefine func chi(Y,X) -> Multiset of X;
end;
definition
let X;
let n be Element of NAT;
redefine func X --> n -> Multiset of X;
end;
definition
let A be non empty set, a be Element of A;
func chi a -> Multiset of A equals
:: MONOID_1:def 5
chi({a},A);
end;
theorem :: MONOID_1:31
for A being non empty set, a,b being Element of A holds
(chi a).a = 1 & (b <> a implies (chi a).b = 0);
reserve A for non empty set,
a for Element of A,
p for FinSequence of A,
m1,m2 for Multiset of A;
theorem :: MONOID_1:32
(for a holds m1.a = m2.a) implies m1 = m2;
definition
let A be set;
func finite-MultiSet_over A -> strict non empty MonoidalSubStr of
MultiSet_over A means
:: MONOID_1:def 6
for f being Multiset of A holds f in the carrier
of it iff f"(NAT\{0}) is finite;
end;
theorem :: MONOID_1:33
chi a is Element of finite-MultiSet_over A;
theorem :: MONOID_1:34
dom ({x}|`(p^<*x*>)) = dom ({x}|`p) \/ {len p+1};
theorem :: MONOID_1:35
x <> y implies dom ({x}|`(p^<*y*>)) = dom ({x}|`p);
definition
let A be non empty set, p be FinSequence of A;
func |.p.| -> Multiset of A means
:: MONOID_1:def 7
for a being Element of A holds it. a = card dom ({a}|`p);
end;
theorem :: MONOID_1:36
|.<*> A.|.a = 0;
theorem :: MONOID_1:37
|.<*> A.| = A --> 0;
theorem :: MONOID_1:38
|.<*a*>.| = chi a;
reserve p,q for FinSequence of A;
theorem :: MONOID_1:39
|.p^<*a*>.| = |.p.| [*] chi a;
theorem :: MONOID_1:40
|.p^q.| = |.p.|[*]|.q.|;
theorem :: MONOID_1:41
|.n .--> a.|.a = n & for b being Element of A st b <> a holds |.
n .--> a.|.b = 0;
reserve fm for Element of finite-MultiSet_over A;
theorem :: MONOID_1:42
|.p.| is Element of finite-MultiSet_over A;
theorem :: MONOID_1:43
x is Element of finite-MultiSet_over A implies ex p st x = |.p.|;
begin :: Monoid of subsets of a semigroup
reserve a,b,c for Element of D;
definition
let D1,D2,D be non empty set, f be Function of [:D1,D2:],D;
func f.:^2 -> Function of [:bool D1, bool D2:], bool D means
:: MONOID_1:def 8
for x being Element of [:bool D1, bool D2:] holds it.x = f.:[:x`1,x`2:];
end;
theorem :: MONOID_1:44
for D1,D2,D being non empty set, f being Function of [:D1,D2:],D for
X1 being Subset of D1, X2 being Subset of D2 holds (f.:^2).(X1,X2) = f.:[:X1,X2
:];
theorem :: MONOID_1:45
for D1,D2,D being non empty set, f being Function of [:D1,D2:],D for
X1 being Subset of D1, X2 being Subset of D2, x1,x2 being set st x1 in X1 & x2
in X2 holds f.(x1,x2) in (f.:^2).(X1,X2);
theorem :: MONOID_1:46
for D1,D2,D being non empty set, f being Function of [:D1,D2:],D for X1
being Subset of D1, X2 being Subset of D2 holds (f.:^2).(X1,X2) = {f.(a,b)
where a is Element of D1, b is Element of D2: a in X1 & b in X2};
theorem :: MONOID_1:47
o is commutative implies o.:[:X,Y:] = o.:[:Y,X:];
theorem :: MONOID_1:48
o is associative implies o.:[:o.:[:X,Y:],Z:] = o.:[:X,o.:[:Y,Z:] :];
theorem :: MONOID_1:49
o is commutative implies o.:^2 is commutative;
theorem :: MONOID_1:50
o is associative implies o.:^2 is associative;
theorem :: MONOID_1:51
a is_a_unity_wrt o implies o.:[:{a},X:] = D /\ X & o.:[:X,{a}:] = D /\ X;
theorem :: MONOID_1:52
a is_a_unity_wrt o implies {a} is_a_unity_wrt o.:^2 & o.:^2 is
having_a_unity & the_unity_wrt o.:^2 = {a};
theorem :: MONOID_1:53
o is having_a_unity implies o.:^2 is having_a_unity & {
the_unity_wrt o} is_a_unity_wrt o.:^2 & the_unity_wrt o.:^2 = {the_unity_wrt o}
;
theorem :: MONOID_1:54
o is uniquely-decomposable implies o.:^2 is uniquely-decomposable;
definition
let G be non empty multMagma;
func bool G -> multMagma equals
:: MONOID_1:def 9
multLoopStr(#bool the carrier of G,
(the multF of G).:^2, {the_unity_wrt the multF of G}#) if G is unital otherwise
multMagma(#bool the carrier of G, (the multF of G).:^2#);
end;
registration
let G be non empty multMagma;
cluster bool G -> non empty;
end;
definition
let G be unital non empty multMagma;
redefine func bool G -> well-unital strict non empty multLoopStr;
end;
theorem :: MONOID_1:55
the carrier of bool G = bool the carrier of G & the multF of
bool G = (the multF of G).:^2;
theorem :: MONOID_1:56
for G being unital non empty multMagma holds 1.bool G = {
the_unity_wrt the multF of G};
theorem :: MONOID_1:57
for G being non empty multMagma holds (G is commutative implies bool G
is commutative) & (G is associative implies bool G is associative) & (G is
uniquely-decomposable implies bool G is uniquely-decomposable);