:: Monoids
:: by Grzegorz Bancerek
::
:: Received December 29, 1992
:: Copyright (c) 1992 Association of Mizar Users
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 :: MONOID_0:def 3
for
a,
b being
Element of
D ex
l being
Element of
D st
IT . l,
a = b;
attr IT is
right-invertible means :: MONOID_0:def 4
for
a,
b being
Element of
D ex
r being
Element of
D st
IT . a,
r = b;
attr IT is
invertible means :
Def5:
:: MONOID_0:def 5
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 :: MONOID_0:def 6
for
a,
b,
c being
Element of
D st
IT . a,
b = IT . a,
c holds
b = c;
attr IT is
right-cancelable means :: MONOID_0:def 7
for
a,
b,
c being
Element of
D st
IT . b,
a = IT . c,
a holds
b = c;
attr IT is
cancelable means :: MONOID_0:def 8
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 :: MONOID_0:def 9
(
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: :: MONOID_0:1
theorem Th2: :: MONOID_0:2
theorem Th3: :: MONOID_0:3
:: deftheorem Def10 defines unital MONOID_0:def 10 :
:: deftheorem 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: :: MONOID_0:4
theorem :: MONOID_0:5
theorem Th6: :: MONOID_0:6
Lm1:
for G being non empty multMagma holds
( G is commutative iff for a, b being Element of G holds a * b = b * a )
Lm2:
for G being non empty multMagma holds
( G is associative iff for a, b, c being Element of G holds (a * b) * c = a * (b * c) )
theorem :: MONOID_0:7
canceled;
theorem :: MONOID_0:8
canceled;
theorem Th9: :: MONOID_0:9
theorem :: MONOID_0:10
theorem :: MONOID_0:11
theorem Th12: :: MONOID_0:12
theorem :: MONOID_0:13
theorem :: MONOID_0:14
theorem Th15: :: MONOID_0:15
theorem Th16: :: MONOID_0:16
theorem Th17: :: MONOID_0:17
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
deffunc H3( multLoopStr ) -> Element of the carrier of $1 = 1. $1;
:: deftheorem Def21 defines well-unital MONOID_0:def 21 :
theorem Th18: :: MONOID_0:18
theorem Th19: :: MONOID_0:19
:: deftheorem Def22 defines MonoidalExtension MONOID_0:def 22 :
theorem Th20: :: MONOID_0:20
theorem Th21: :: MONOID_0:21
theorem Th22: :: MONOID_0:22
:: 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: :: MONOID_0:23
theorem :: MONOID_0:24
theorem Th25: :: MONOID_0:25
theorem Th26: :: MONOID_0:26
theorem Th27: :: MONOID_0:27
theorem Th28: :: MONOID_0:28
theorem :: MONOID_0:29
theorem Th30: :: MONOID_0:30
theorem :: MONOID_0:31
theorem Th32: :: MONOID_0:32
theorem Th33: :: MONOID_0:33
theorem Th34: :: MONOID_0:34
theorem Th35: :: MONOID_0:35
theorem Th36: :: MONOID_0:36
theorem Th37: :: MONOID_0:37
theorem Th38: :: MONOID_0:38
theorem Th39: :: MONOID_0:39
:: deftheorem defines <REAL,+> MONOID_0:def 26 :
theorem :: MONOID_0:40
canceled;
theorem :: MONOID_0:41
theorem :: MONOID_0:42
canceled;
theorem Th43: :: MONOID_0:43
theorem Th44: :: MONOID_0:44
theorem :: MONOID_0:45
canceled;
theorem :: MONOID_0:46
theorem :: MONOID_0:47
:: deftheorem Def27 defines <NAT,+> MONOID_0:def 27 :
:: deftheorem defines <NAT,+,0> MONOID_0:def 28 :
:: deftheorem defines addnat MONOID_0:def 29 :
theorem :: MONOID_0:48
canceled;
theorem Th49: :: MONOID_0:49
theorem :: MONOID_0:50
theorem :: MONOID_0:51
theorem :: MONOID_0:52
theorem :: MONOID_0:53
theorem :: MONOID_0:54
:: deftheorem defines <REAL,*> MONOID_0:def 30 :
theorem :: MONOID_0:55
canceled;
theorem :: MONOID_0:56
theorem :: MONOID_0:57
canceled;
theorem Th58: :: MONOID_0:58
theorem :: MONOID_0:59
canceled;
theorem :: MONOID_0:60
:: 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: :: MONOID_0:61
theorem :: MONOID_0:62
theorem Th63: :: MONOID_0:63
theorem :: MONOID_0:64
theorem :: MONOID_0:65
theorem :: MONOID_0:66
theorem :: MONOID_0:67
:: deftheorem Def34 defines *+^ MONOID_0:def 34 :
:: deftheorem defines *+^+<0> MONOID_0:def 35 :
:: deftheorem defines -concatenation MONOID_0:def 36 :
theorem :: MONOID_0:68
theorem Th69: :: MONOID_0:69
theorem :: MONOID_0:70
theorem :: MONOID_0:71
theorem Th72: :: MONOID_0:72
theorem :: MONOID_0:73
theorem :: MONOID_0:74
theorem :: MONOID_0:75
theorem :: MONOID_0:76
:: deftheorem Def37 defines GPFuncs MONOID_0:def 37 :
:: deftheorem defines MPFuncs MONOID_0:def 38 :
:: deftheorem defines -composition MONOID_0:def 39 :
theorem :: MONOID_0:77
theorem Th78: :: MONOID_0:78
theorem Th79: :: MONOID_0:79
theorem Th80: :: MONOID_0:80
theorem :: MONOID_0:81
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 :: MONOID_0:82
theorem Th83: :: MONOID_0:83
theorem Th84: :: MONOID_0:84
theorem :: MONOID_0:85
:: deftheorem Def42 defines GPerms MONOID_0:def 42 :
theorem Th86: :: MONOID_0:86
theorem Th87: :: MONOID_0:87
theorem :: MONOID_0:88
theorem :: MONOID_0:89