:: Monoid of Multisets and Subsets
:: by Grzegorz Bancerek
::
:: Received December 29, 1992
:: Copyright (c) 1992 Association of Mizar Users
deffunc H1( multMagma ) -> Relation of [:the carrier of $1,the carrier of $1:],the carrier of $1 = the multF of $1;
deffunc H2( multLoopStr ) -> Element of the carrier of $1 = 1. $1;
:: deftheorem defines .. MONOID_1:def 1 :
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;
:: original: ..redefine func f .. x1,
x2,
x -> Element of
D;
coherence
f .. x1,x2,x is Element of D
end;
definition
let A be
set ;
let D1,
D2,
D be non
empty set ;
let f be
Function of
D1,
D2,
D;
let g1 be
Function of
A,
D1;
let g2 be
Function of
A,
D2;
:: original: .:redefine func f .: g1,
g2 -> Element of
Funcs A,
D;
coherence
f .: g1,g2 is Element of Funcs A,D
end;
theorem :: MONOID_1:1
canceled;
theorem :: MONOID_1:2
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 :
Def2:
:: 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;
existence
ex b1 being Function of (Funcs A,D1),(Funcs A,D2), Funcs A,D st
for f1 being Element of Funcs A,D1
for f2 being Element of Funcs A,D2 holds b1 . f1,f2 = f .: f1,f2
uniqueness
for b1, b2 being Function of (Funcs A,D1),(Funcs A,D2), Funcs A,D st ( for f1 being Element of Funcs A,D1
for f2 being Element of Funcs A,D2 holds b1 . f1,f2 = f .: f1,f2 ) & ( for f1 being Element of Funcs A,D1
for f2 being Element of Funcs A,D2 holds b2 . f1,f2 = f .: f1,f2 ) holds
b1 = b2
end;
:: deftheorem Def2 defines .: MONOID_1:def 2 :
for
D1,
D2,
D being non
empty set for
f being
Function of
D1,
D2,
D for
A being
set for
b6 being
Function of
(Funcs A,D1),
(Funcs A,D2),
Funcs A,
D holds
(
b6 = f,
D .: A iff for
f1 being
Element of
Funcs A,
D1 for
f2 being
Element of
Funcs A,
D2 holds
b6 . f1,
f2 = f .: f1,
f2 );
theorem :: MONOID_1:3
for
D1,
D2,
D being non
empty set for
f being
Function of
D1,
D2,
D for
A being
set for
f1 being
Function of
A,
D1 for
f2 being
Function of
A,
D2 for
x being
set st
x in A holds
(f,D .: A) .. f1,
f2,
x = f . (f1 . x),
(f2 . x)
theorem Th4: :: MONOID_1:4
theorem Th5: :: MONOID_1:5
theorem Th6: :: MONOID_1:6
theorem Th7: :: MONOID_1:7
theorem Th8: :: MONOID_1:8
theorem Th9: :: MONOID_1:9
theorem Th10: :: MONOID_1:10
theorem Th11: :: MONOID_1:11
theorem Th12: :: MONOID_1:12
theorem Th13: :: MONOID_1:13
theorem Th14: :: MONOID_1:14
theorem Th15: :: MONOID_1:15
theorem :: MONOID_1:16
theorem Th17: :: MONOID_1:17
for
A being
set for
D1,
D2,
D,
E1,
E2,
E being non
empty set for
o1 being
Function of
D1,
D2,
D for
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 :
Def3:
:: 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) #);
correctness
coherence
( ( G is unital implies multLoopStr(# (Funcs A,the carrier of G),(the multF of G,the carrier of G .: A),(A --> (the_unity_wrt the multF of G)) #) is multMagma ) & ( not G is unital implies multMagma(# (Funcs A,the carrier of G),(the multF of G,the carrier of G .: A) #) is multMagma ) );
consistency
for b1 being multMagma holds verum;
;
end;
:: deftheorem Def3 defines .: MONOID_1:def 3 :
deffunc H3( non empty multMagma ) -> set = the carrier of $1;
theorem Th18: :: MONOID_1:18
theorem :: MONOID_1:19
Lm1:
for X being set
for G being non empty multMagma holds .: G,X is constituted-Functions
theorem Th20: :: MONOID_1:20
theorem Th21: :: MONOID_1:21
theorem Th22: :: MONOID_1:22
theorem Th23: :: MONOID_1:23
theorem Th24: :: MONOID_1:24
theorem :: MONOID_1:25
theorem :: MONOID_1:26
:: deftheorem defines MultiSet_over MONOID_1:def 4 :
theorem Th27: :: MONOID_1:27
theorem Th28: :: MONOID_1:28
theorem Th29: :: MONOID_1:29
theorem Th30: :: MONOID_1:30
theorem Th31: :: MONOID_1:31
:: deftheorem defines chi MONOID_1:def 5 :
theorem Th32: :: MONOID_1:32
theorem Th33: :: MONOID_1:33
:: deftheorem Def6 defines finite-MultiSet_over MONOID_1:def 6 :
theorem Th34: :: MONOID_1:34
theorem Th35: :: MONOID_1:35
theorem Th36: :: MONOID_1:36
:: deftheorem Def7 defines |. MONOID_1:def 7 :
theorem :: MONOID_1:37
theorem Th38: :: MONOID_1:38
theorem :: MONOID_1:39
theorem Th40: :: MONOID_1:40
theorem Th41: :: MONOID_1:41
theorem Th42: :: MONOID_1:42
theorem :: MONOID_1:43
theorem :: MONOID_1:44
definition
let D1,
D2,
D be non
empty set ;
let f be
Function of
D1,
D2,
D;
func f .:^2 -> Function of
(bool D1),
(bool D2),
bool D means :
Def8:
:: MONOID_1:def 8
for
x being
Element of
[:(bool D1),(bool D2):] holds
it . x = f .: [:(x `1 ),(x `2 ):];
existence
ex b1 being Function of (bool D1),(bool D2), bool D st
for x being Element of [:(bool D1),(bool D2):] holds b1 . x = f .: [:(x `1 ),(x `2 ):]
uniqueness
for b1, b2 being Function of (bool D1),(bool D2), bool D st ( for x being Element of [:(bool D1),(bool D2):] holds b1 . x = f .: [:(x `1 ),(x `2 ):] ) & ( for x being Element of [:(bool D1),(bool D2):] holds b2 . x = f .: [:(x `1 ),(x `2 ):] ) holds
b1 = b2
end;
:: deftheorem Def8 defines .:^2 MONOID_1:def 8 :
theorem Th45: :: MONOID_1:45
theorem Th46: :: MONOID_1:46
theorem :: MONOID_1:47
theorem Th48: :: MONOID_1:48
theorem Th49: :: MONOID_1:49
theorem Th50: :: MONOID_1:50
theorem Th51: :: MONOID_1:51
theorem Th52: :: MONOID_1:52
theorem Th53: :: MONOID_1:53
theorem Th54: :: MONOID_1:54
theorem Th55: :: MONOID_1:55
:: deftheorem Def9 defines bool MONOID_1:def 9 :
theorem Th56: :: MONOID_1:56
theorem :: MONOID_1:57
theorem :: MONOID_1:58