:: Monoid of Multisets and Subsets :: by Grzegorz Bancerek :: :: Received December 29, 1992 :: Copyright (c) 1992-2021 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);