begin
deffunc H1( 1-sorted ) -> set = the carrier of $1;
deffunc H2( multMagma ) -> Element of bool [:[:the carrier of $1,the carrier of $1:],the carrier of $1:] = the multF of $1;
:: deftheorem Def1 defines constituted-Functions MONOID_0:def 1 :
:: deftheorem Def2 defines constituted-FinSeqs MONOID_0:def 2 :
definition
let D be non
empty set ;
let IT be
BinOp of
D;
attr IT is
left-invertible means
for
a,
b being
Element of
D ex
l being
Element of
D st
IT . l,
a = b;
attr IT is
right-invertible means
for
a,
b being
Element of
D ex
r being
Element of
D st
IT . a,
r = b;
attr IT is
invertible means :
Def5:
for
a,
b being
Element of
D ex
r,
l being
Element of
D st
(
IT . a,
r = b &
IT . l,
a = b );
attr IT is
left-cancelable means
for
a,
b,
c being
Element of
D st
IT . a,
b = IT . a,
c holds
b = c;
attr IT is
right-cancelable means
for
a,
b,
c being
Element of
D st
IT . b,
a = IT . c,
a holds
b = c;
attr IT is
cancelable means
for
a,
b,
c being
Element of
D st (
IT . a,
b = IT . a,
c or
IT . b,
a = IT . c,
a ) holds
b = c;
attr IT is
uniquely-decomposable means
(
IT is
having_a_unity & ( for
a,
b being
Element of
D st
IT . a,
b = the_unity_wrt IT holds
(
a = b &
b = the_unity_wrt IT ) ) );
end;
:: deftheorem defines left-invertible MONOID_0:def 3 :
:: deftheorem defines right-invertible MONOID_0:def 4 :
:: deftheorem Def5 defines invertible MONOID_0:def 5 :
:: deftheorem defines left-cancelable MONOID_0:def 6 :
:: deftheorem defines right-cancelable MONOID_0:def 7 :
:: deftheorem defines cancelable MONOID_0:def 8 :
:: deftheorem defines uniquely-decomposable MONOID_0:def 9 :
theorem Th1:
theorem Th2:
theorem Th3:
begin
:: deftheorem Def10 defines unital MONOID_0:def 10 :
:: deftheorem Def11 defines commutative MONOID_0:def 11 :
:: deftheorem Def12 defines associative MONOID_0:def 12 :
:: deftheorem defines idempotent MONOID_0:def 13 :
:: deftheorem defines left-invertible MONOID_0:def 14 :
:: deftheorem defines right-invertible MONOID_0:def 15 :
:: deftheorem Def16 defines invertible MONOID_0:def 16 :
:: deftheorem defines left-cancelable MONOID_0:def 17 :
:: deftheorem defines right-cancelable MONOID_0:def 18 :
:: deftheorem defines cancelable MONOID_0:def 19 :
:: deftheorem Def20 defines uniquely-decomposable MONOID_0:def 20 :
theorem Th4:
theorem
theorem Th6:
Lm1:
for G being non empty multMagma holds
( G is commutative iff for a, b being Element of holds a * b = b * a )
Lm2:
for G being non empty multMagma holds
( G is associative iff for a, b, c being Element of holds (a * b) * c = a * (b * c) )
theorem
canceled;
theorem
canceled;
theorem Th9:
theorem
theorem
theorem Th12:
theorem
theorem
theorem Th15:
theorem Th16:
theorem Th17:
Lm3:
for G being non empty multMagma holds
( G is invertible iff ( G is left-invertible & G is right-invertible ) )
Lm4:
for G being non empty multMagma holds
( G is cancelable iff ( G is left-cancelable & G is right-cancelable ) )
Lm5:
for G being non empty multMagma st G is associative & G is invertible holds
G is Group-like
begin
deffunc H3( multLoopStr ) -> Element of the carrier of $1 = 1. $1;
:: deftheorem Def21 defines well-unital MONOID_0:def 21 :
theorem Th18:
theorem Th19:
:: deftheorem Def22 defines MonoidalExtension MONOID_0:def 22 :
theorem Th20:
theorem Th21:
theorem Th22:
begin
:: deftheorem Def23 defines SubStr MONOID_0:def 23 :
:: deftheorem Def24 defines MonoidalSubStr MONOID_0:def 24 :
:: deftheorem Def25 defines MonoidalSubStr MONOID_0:def 25 :
theorem Th23:
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem
theorem Th30:
theorem
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
begin
:: deftheorem defines <REAL,+> MONOID_0:def 26 :
theorem
canceled;
theorem
theorem
canceled;
theorem Th43:
theorem Th44:
theorem
canceled;
theorem
theorem
:: deftheorem Def27 defines <NAT,+> MONOID_0:def 27 :
:: deftheorem defines <NAT,+,0> MONOID_0:def 28 :
:: deftheorem defines addnat MONOID_0:def 29 :
theorem
canceled;
theorem Th49:
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines <REAL,*> MONOID_0:def 30 :
theorem
canceled;
theorem
theorem
canceled;
theorem Th58:
theorem
canceled;
theorem
:: deftheorem Def31 defines <NAT,*> MONOID_0:def 31 :
:: deftheorem defines <NAT,*,1> MONOID_0:def 32 :
:: deftheorem defines multnat MONOID_0:def 33 :
theorem Th61:
theorem
theorem Th63:
theorem
theorem
theorem
theorem
begin
:: deftheorem Def34 defines *+^ MONOID_0:def 34 :
:: deftheorem defines *+^+<0> MONOID_0:def 35 :
:: deftheorem defines -concatenation MONOID_0:def 36 :
theorem
theorem Th69:
theorem
theorem
theorem Th72:
theorem
theorem
theorem
theorem
begin
:: deftheorem Def37 defines GPFuncs MONOID_0:def 37 :
:: deftheorem defines MPFuncs MONOID_0:def 38 :
:: deftheorem defines -composition MONOID_0:def 39 :
theorem
theorem Th78:
theorem Th79:
theorem Th80:
theorem
Lm6:
for x, X being set st x in Funcs X,X holds
x is Function of X,X
:: deftheorem Def40 defines GFuncs MONOID_0:def 40 :
:: deftheorem defines MFuncs MONOID_0:def 41 :
theorem
theorem Th83:
theorem Th84:
theorem
:: deftheorem Def42 defines GPerms MONOID_0:def 42 :
theorem Th86:
theorem Th87:
theorem
theorem