:: Monoids
:: by Grzegorz Bancerek
::
:: Received December 29, 1992
:: Copyright (c) 1992-2017 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 STRUCT_0, ALGSTR_0, BINOP_1, SUBSET_1, FUNCT_1, FINSEQ_1,
RELAT_1, ORDINAL4, XBOOLE_0, ALGSTR_1, SETWISEO, FUNCOP_1, ZFMISC_1,
GROUP_1, FINSEQOP, MESFUNC1, VECTSP_1, TARSKI, REALSET1, MCART_1,
NUMBERS, BINOP_2, REAL_1, ARYTM_3, CARD_1, GR_CY_1, INT_1, PARTFUN1,
FUNCT_2, MONOID_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, XTUPLE_0, MCART_1, DOMAIN_1, BINOP_2, REALSET1, STRUCT_0,
RELAT_1, FINSEQOP, FUNCT_1, FINSEQ_1, PARTFUN1, FUNCT_2, BINOP_1,
FINSEQ_2, INT_1, GROUP_1, VECTSP_1, SETWISEO, FUNCOP_1, GR_CY_1,
ALGSTR_0;
constructors RELAT_2, PARTFUN1, BINOP_1, SETWISEO, BINOP_2, FINSEQOP,
REALSET1, VECTSP_2, GR_CY_1, RELSET_1, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1,
FUNCT_2, NUMBERS, BINOP_2, MEMBERED, FINSEQ_1, REALSET1, STRUCT_0,
GROUP_1, ALGSTR_0, GR_CY_1, XREAL_0, NAT_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Updating
reserve x,y,X,Y for set;
definition
let G be 1-sorted;
mode BinOp of G is BinOp of the carrier of G;
end;
definition
let IT be 1-sorted;
attr IT is constituted-Functions means
:: MONOID_0:def 1
for a being Element of IT holds a is Function;
attr IT is constituted-FinSeqs means
:: MONOID_0:def 2
for a being Element of IT holds a is FinSequence;
end;
registration
cluster constituted-Functions for 1-sorted;
cluster constituted-FinSeqs for 1-sorted;
end;
registration
let X be constituted-Functions 1-sorted;
cluster -> Function-like Relation-like for Element of X;
end;
registration
cluster constituted-FinSeqs -> constituted-Functions for 1-sorted;
end;
registration
let X be constituted-FinSeqs 1-sorted;
cluster -> FinSequence-like for Element of X;
end;
definition
let D be set, p,q be FinSequence of D;
redefine func p^q -> Element of D*;
end;
notation
let g,f be Function;
synonym f(*)g for f*g;
end;
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
:: 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;
theorem :: MONOID_0:1
for D be non empty set, f being BinOp of D holds f is invertible
iff f is left-invertible right-invertible;
theorem :: MONOID_0:2
for D be non empty set, f being BinOp of D holds f is cancelable
iff f is left-cancelable right-cancelable;
theorem :: MONOID_0:3
for f being BinOp of {x} holds f = (x,x) .--> x & f is
having_a_unity & f is commutative & f is associative & f is idempotent & f is
invertible cancelable uniquely-decomposable;
begin :: Semigroups
reserve G for non empty multMagma,
D for non empty set,
a,b,c,r,l for Element of G;
definition
let IT be non empty multMagma;
redefine attr IT is unital means
:: MONOID_0:def 10
the multF of IT is having_a_unity;
end;
definition
let G;
redefine attr G is commutative means
:: MONOID_0:def 11
the multF of G is commutative;
redefine attr G is associative means
:: MONOID_0:def 12
the multF of G is associative;
end;
definition
let IT be non empty multMagma;
attr IT is idempotent means
:: MONOID_0:def 13
the multF of IT is idempotent;
attr IT is left-invertible means
:: MONOID_0:def 14
the multF of IT is left-invertible;
attr IT is right-invertible means
:: MONOID_0:def 15
the multF of IT is right-invertible;
attr IT is invertible means
:: MONOID_0:def 16
the multF of IT is invertible;
attr IT is left-cancelable means
:: MONOID_0:def 17
the multF of IT is left-cancelable;
attr IT is right-cancelable means
:: MONOID_0:def 18
the multF of IT is right-cancelable;
attr IT is cancelable means
:: MONOID_0:def 19
the multF of IT is cancelable;
attr IT is uniquely-decomposable means
:: MONOID_0:def 20
the multF of IT is uniquely-decomposable;
end;
registration
cluster unital commutative associative cancelable idempotent invertible
uniquely-decomposable constituted-Functions constituted-FinSeqs strict for
non
empty multMagma;
end;
theorem :: MONOID_0:4
G is unital implies the_unity_wrt the multF of G is_a_unity_wrt
the multF of G;
theorem :: MONOID_0:5
G is unital iff for a holds (the_unity_wrt the multF of G)*a = a & a*(
the_unity_wrt the multF of G) = a;
theorem :: MONOID_0:6
G is unital iff ex a st for b holds a*b = b & b*a = b;
theorem :: MONOID_0:7
G is idempotent iff for a holds a*a = a;
theorem :: MONOID_0:8
G is left-invertible iff for a,b ex l st l*a = b;
theorem :: MONOID_0:9
G is right-invertible iff for a,b ex r st a*r = b;
theorem :: MONOID_0:10
G is invertible iff for a,b ex r,l st a*r = b & l*a = b;
theorem :: MONOID_0:11
G is left-cancelable iff for a,b,c st a*b = a*c holds b = c;
theorem :: MONOID_0:12
G is right-cancelable iff for a,b,c st b*a = c*a holds b = c;
theorem :: MONOID_0:13
G is cancelable iff for a,b,c st a*b = a*c or b*a = c*a holds b = c;
theorem :: MONOID_0:14
G is uniquely-decomposable iff the multF of G is having_a_unity
& for a,b being Element of G st a*b = the_unity_wrt the multF of G holds a = b
& b = the_unity_wrt the multF of G;
theorem :: MONOID_0:15
G is associative implies (G is invertible iff G is unital & the
multF of G is having_an_inverseOp);
registration
cluster associative Group-like -> invertible for non empty multMagma;
cluster associative invertible -> Group-like for non empty multMagma;
end;
registration
cluster invertible -> left-invertible right-invertible for
non empty multMagma;
cluster left-invertible right-invertible -> invertible for
non empty multMagma;
cluster cancelable -> left-cancelable right-cancelable for
non empty multMagma;
cluster left-cancelable right-cancelable -> cancelable for
non empty multMagma;
cluster associative invertible -> unital cancelable for
non empty multMagma;
end;
begin
reserve M for non empty multLoopStr;
definition
let IT be non empty multLoopStr;
redefine attr IT is well-unital means
:: MONOID_0:def 21
1.IT is_a_unity_wrt the multF of IT;
end;
theorem :: MONOID_0:16
M is well-unital iff for a being Element of M holds (1.M)*a = a & a*(1.M) = a
;
theorem :: MONOID_0:17
for M being non empty multLoopStr st M is well-unital holds 1.M
= the_unity_wrt the multF of M;
registration
cluster well-unital commutative associative cancelable idempotent invertible
uniquely-decomposable unital constituted-Functions constituted-FinSeqs strict
for
non empty multLoopStr;
end;
definition
mode Monoid is well-unital associative non empty multLoopStr;
end;
definition
let G be multMagma;
mode MonoidalExtension of G -> multLoopStr means
:: MONOID_0:def 22
the multMagma of it = the multMagma of G;
end;
registration
let G be non empty multMagma;
cluster -> non empty for MonoidalExtension of G;
end;
theorem :: MONOID_0:18
for M being MonoidalExtension of G holds the carrier of M = the
carrier of G & the multF of M = the multF of G & for a,b being Element of M, a9
,b9 being Element of G st a = a9 & b = b9 holds a*b = a9*b9;
registration
let G be multMagma;
cluster strict for MonoidalExtension of G;
end;
theorem :: MONOID_0:19
for G being non empty multMagma, M being MonoidalExtension of G
holds (G is unital implies M is unital) & (G is commutative implies M is
commutative) & (G is associative implies M is associative) & (G is invertible
implies M is invertible) & (G is uniquely-decomposable implies M is
uniquely-decomposable) & (G is cancelable implies M is cancelable);
registration
let G be constituted-Functions multMagma;
cluster -> constituted-Functions for MonoidalExtension of G;
end;
registration
let G be constituted-FinSeqs multMagma;
cluster -> constituted-FinSeqs for MonoidalExtension of G;
end;
registration
let G be unital non empty multMagma;
cluster -> unital for MonoidalExtension of G;
end;
registration
let G be associative non empty multMagma;
cluster -> associative for MonoidalExtension of G;
end;
registration
let G be commutative non empty multMagma;
cluster -> commutative for MonoidalExtension of G;
end;
registration
let G be invertible non empty multMagma;
cluster -> invertible for MonoidalExtension of G;
end;
registration
let G be cancelable non empty multMagma;
cluster -> cancelable for MonoidalExtension of G;
end;
registration
let G be uniquely-decomposable non empty multMagma;
cluster -> uniquely-decomposable for MonoidalExtension of G;
end;
registration
let G be unital non empty multMagma;
cluster well-unital strict for MonoidalExtension of G;
end;
theorem :: MONOID_0:20
for G being unital non empty multMagma for M1,M2 being
well-unital strict MonoidalExtension of G holds M1 = M2;
begin :: Subsystems
definition
let G be multMagma;
mode SubStr of G -> multMagma means
:: MONOID_0:def 23
the multF of it c= the multF of G;
end;
registration
let G be multMagma;
cluster strict for SubStr of G;
end;
registration
let G be non empty multMagma;
cluster strict non empty for SubStr of G;
end;
registration
let G be unital non empty multMagma;
cluster unital associative commutative cancelable idempotent invertible
uniquely-decomposable strict for non empty SubStr of G;
end;
definition
let G be multMagma;
mode MonoidalSubStr of G -> multLoopStr means
:: MONOID_0:def 24
the multF of it c= the
multF of G & for M being multLoopStr st G = M holds 1.it = 1.M;
end;
registration
let G be multMagma;
cluster strict for MonoidalSubStr of G;
end;
registration
let G be non empty multMagma;
cluster strict non empty for MonoidalSubStr of G;
end;
definition
let M be multLoopStr;
redefine mode MonoidalSubStr of M means
:: MONOID_0:def 25
the multF of it c= the multF of M & 1.it = 1.M;
end;
registration
let G be well-unital non empty multLoopStr;
cluster well-unital associative commutative cancelable idempotent invertible
uniquely-decomposable strict for non empty MonoidalSubStr of G;
end;
theorem :: MONOID_0:21
for G being multMagma, M being MonoidalSubStr of G holds M is SubStr of G;
definition
let G be multMagma, M be MonoidalExtension of G;
redefine mode SubStr of M -> SubStr of G;
end;
definition
let G1 be multMagma, G2 be SubStr of G1;
redefine mode SubStr of G2 -> SubStr of G1;
end;
definition
let G1 be multMagma, G2 be MonoidalSubStr of G1;
redefine mode SubStr of G2 -> SubStr of G1;
end;
definition
let G be multMagma, M be MonoidalSubStr of G;
redefine mode MonoidalSubStr of M -> MonoidalSubStr of G;
end;
theorem :: MONOID_0:22
G is SubStr of G & M is MonoidalSubStr of M;
reserve H for non empty SubStr of G,
N for non empty MonoidalSubStr of G;
theorem :: MONOID_0:23
the carrier of H c= the carrier of G & the carrier of N c= the carrier of G;
theorem :: MONOID_0:24
for G being non empty multMagma, H being non empty SubStr of G
holds the multF of H = (the multF of G)||the carrier of H;
theorem :: MONOID_0:25
for a,b being Element of H, a9,b9 being Element of G st a = a9 &
b = b9 holds a*b = a9*b9;
theorem :: MONOID_0:26
for H1,H2 being non empty SubStr of G st the carrier of H1 = the
carrier of H2 holds the multMagma of H1 = the multMagma of H2;
theorem :: MONOID_0:27
for H1,H2 being non empty MonoidalSubStr of M st the carrier of H1 =
the carrier of H2 holds the multLoopStr of H1 = the multLoopStr of H2;
theorem :: MONOID_0:28
for H1,H2 being non empty SubStr of G st the carrier of H1 c=
the carrier of H2 holds H1 is SubStr of H2;
theorem :: MONOID_0:29
for H1,H2 being non empty MonoidalSubStr of M st the carrier of H1 c=
the carrier of H2 holds H1 is MonoidalSubStr of H2;
theorem :: MONOID_0:30
G is unital & the_unity_wrt the multF of G in the carrier of H
implies H is unital & the_unity_wrt the multF of G = the_unity_wrt the multF of
H;
theorem :: MONOID_0:31
for M being well-unital non empty multLoopStr for N being non
empty MonoidalSubStr of M holds N is well-unital;
theorem :: MONOID_0:32
G is commutative implies H is commutative;
theorem :: MONOID_0:33
G is associative implies H is associative;
theorem :: MONOID_0:34
G is idempotent implies H is idempotent;
theorem :: MONOID_0:35
G is cancelable implies H is cancelable;
theorem :: MONOID_0:36
the_unity_wrt the multF of G in the carrier of H & G is
uniquely-decomposable implies H is uniquely-decomposable;
theorem :: MONOID_0:37
for M being well-unital uniquely-decomposable non empty
multLoopStr for N being non empty MonoidalSubStr of M holds N is
uniquely-decomposable;
registration
let G be constituted-Functions non empty multMagma;
cluster -> constituted-Functions for non empty SubStr of G;
cluster -> constituted-Functions for non empty MonoidalSubStr of G;
end;
registration
let G be constituted-FinSeqs non empty multMagma;
cluster -> constituted-FinSeqs for non empty SubStr of G;
cluster -> constituted-FinSeqs for non empty MonoidalSubStr of G;
end;
registration
let M be well-unital non empty multLoopStr;
cluster -> well-unital for non empty MonoidalSubStr of M;
end;
registration
let G be commutative non empty multMagma;
cluster -> commutative for non empty SubStr of G;
cluster -> commutative for non empty MonoidalSubStr of G;
end;
registration
let G be associative non empty multMagma;
cluster -> associative for non empty SubStr of G;
cluster -> associative for non empty MonoidalSubStr of G;
end;
registration
let G be idempotent non empty multMagma;
cluster -> idempotent for non empty SubStr of G;
cluster -> idempotent for non empty MonoidalSubStr of G;
end;
registration
let G be cancelable non empty multMagma;
cluster -> cancelable for non empty SubStr of G;
cluster -> cancelable for non empty MonoidalSubStr of G;
end;
registration
let M be well-unital uniquely-decomposable non empty multLoopStr;
cluster -> uniquely-decomposable for non empty MonoidalSubStr of M;
end;
scheme :: MONOID_0:sch 1
SubStrEx2 {G() -> non empty multMagma, P[object]}
: ex H being strict non empty
SubStr of G() st for x being Element of G()
holds x in the carrier of H iff P[x]
provided
for x,y being Element of G() holds P[x] & P[y] implies P[x*y] and
ex x being Element of G() st P[x];
scheme :: MONOID_0:sch 2
MonoidalSubStrEx2 {G() -> non empty multLoopStr, P[set]}: ex M being strict
non empty MonoidalSubStr of G() st for x being Element of G() holds x in the
carrier of M iff P[x]
provided
for x,y being Element of G() holds P[x] & P[y] implies P[x*y] and
P[1.G()];
notation
let G be multMagma, a,b be Element of G;
synonym a [*] b for a*b;
end;
begin :: Monoids on Nats
definition
func -> non empty multMagma equals
:: MONOID_0:def 26
multMagma(#REAL, addreal#);
end;
registration
cluster -> unital associative invertible commutative cancelable
strict;
end;
theorem :: MONOID_0:38
x is Element of iff x is Element of REAL;
theorem :: MONOID_0:39
for N being non empty SubStr of for a,b being Element
of N, x,y being Real st a = x & b = y holds a*b = x+y;
theorem :: MONOID_0:40
for N being unital non empty SubStr of holds
the_unity_wrt the multF of N = 0;
registration
let G be unital non empty multMagma;
cluster associative invertible -> unital cancelable Group-like for non empty
SubStr of G;
end;
definition
redefine func INT.Group -> strict non empty SubStr of ;
end;
:: corollary
:: INT.Group is unital commutative associative cancelable invertible;
theorem :: MONOID_0:41
for G being strict non empty SubStr of holds G = INT.Group
iff the carrier of G = INT;
theorem :: MONOID_0:42
x is Element of INT.Group iff x is Integer;
definition
func -> unital uniquely-decomposable strict non empty SubStr of
INT.Group means
:: MONOID_0:def 27
the carrier of it = NAT;
end;
:: corollary
:: is unital commutative associative cancelable uniquely-decomposable;
definition
func -> well-unital strict non empty MonoidalExtension of
means
:: MONOID_0:def 28
not contradiction;
end;
:: corollary
:: is
:: well-unital commutative associative cancelable uniquely-decomposable;
definition
redefine func addnat equals
:: MONOID_0:def 29
the multF of ;
end;
theorem :: MONOID_0:43
= multMagma(#NAT,addnat#);
theorem :: MONOID_0:44
x is Element of iff x is Element of NAT;
theorem :: MONOID_0:45
for n1,n2 being Element of NAT, m1,m2 being Element of st n1
= m1 & n2 = m2 holds m1*m2 = n1+n2;
theorem :: MONOID_0:46
= multLoopStr(#NAT,addnat,0#);
theorem :: MONOID_0:47
addnat = addreal||NAT & addnat = addint||NAT;
theorem :: MONOID_0:48
0 is_a_unity_wrt addnat & addnat is uniquely-decomposable;
definition
func -> unital commutative associative strict non empty multMagma
equals
:: MONOID_0:def 30
multMagma(#REAL,multreal#);
end;
theorem :: MONOID_0:49
x is Element of iff x is Element of REAL;
theorem :: MONOID_0:50
for N being non empty SubStr of for a,b being Element
of N, x,y being Real st a = x & b = y holds a*b = x*y;
theorem :: MONOID_0:51
for N being unital non empty SubStr of holds the_unity_wrt
the multF of N = 0 or the_unity_wrt the multF of N = 1;
definition
func -> unital uniquely-decomposable strict non empty SubStr of
means
:: MONOID_0:def 31
the carrier of it = NAT;
end;
:: corollary
:: is unital commutative associative uniquely-decomposable;
definition
func -> well-unital strict non empty MonoidalExtension of
means
:: MONOID_0:def 32
not contradiction;
end;
:: corollary
:: is well-unital commutative associative uniquely-decomposable;
definition
redefine func multnat equals
:: MONOID_0:def 33
the multF of ;
end;
theorem :: MONOID_0:52
= multMagma(#NAT,multnat#);
theorem :: MONOID_0:53
for n1,n2 being Element of NAT, m1,m2 being Element of st n1 =
m1 & n2 = m2 holds m1*m2 = n1*n2;
theorem :: MONOID_0:54
the_unity_wrt the multF of = 1;
theorem :: MONOID_0:55
for n1,n2 being Element of NAT, m1,m2 being Element of st n1
= m1 & n2 = m2 holds m1*m2 = n1*n2;
theorem :: MONOID_0:56
= multLoopStr(#NAT,multnat,1#);
theorem :: MONOID_0:57
multnat = multreal||NAT;
theorem :: MONOID_0:58
1 is_a_unity_wrt multnat & multnat is uniquely-decomposable;
begin :: Monoid of finite sequences
definition
let D be non empty set;
func D*+^ -> unital associative cancelable uniquely-decomposable
constituted-FinSeqs strict non empty multMagma means
:: MONOID_0:def 34
the carrier of it = D* & for p,q being Element of it holds p [*] q = p^q;
end;
definition
let D;
func D*+^+<0> -> well-unital strict non empty MonoidalExtension of D*+^
means
:: MONOID_0:def 35
not contradiction;
func D-concatenation -> BinOp of D* equals
:: MONOID_0:def 36
the multF of D*+^;
end;
theorem :: MONOID_0:59
D*+^ = multMagma(#D*, D-concatenation#);
theorem :: MONOID_0:60
the_unity_wrt the multF of D*+^ = {};
theorem :: MONOID_0:61
the carrier of D*+^+<0> = D* & the multF of D*+^+<0> = D-concatenation
& 1.(D*+^+<0>) = {};
theorem :: MONOID_0:62
for a,b being Element of D*+^+<0> holds a [*] b = a^b;
theorem :: MONOID_0:63
for F being non empty SubStr of D*+^ for p,q being Element of F
holds p[*]q = p^q;
theorem :: MONOID_0:64
for F being unital non empty SubStr of D*+^ holds the_unity_wrt the
multF of F = {};
theorem :: MONOID_0:65
for F being non empty SubStr of D*+^ st {} is Element of F holds F is
unital & the_unity_wrt the multF of F = {};
theorem :: MONOID_0:66
for A,B being non empty set st A c= B holds A*+^ is SubStr of B*+^;
theorem :: MONOID_0:67
D-concatenation is having_a_unity & the_unity_wrt (D-concatenation) =
{} & D-concatenation is associative;
begin :: Monoids of mappings
definition
let X be set;
func GPFuncs X -> constituted-Functions strict multMagma means
:: MONOID_0:def 37
the carrier of it = PFuncs(X,X) &
for f,g being Element of it holds f [*] g = g (*) f;
end;
registration
let X be set;
cluster GPFuncs X -> unital associative non empty;
end;
definition
let X be set;
func MPFuncs X -> well-unital strict non empty MonoidalExtension of GPFuncs
X means
:: MONOID_0:def 38
not contradiction;
func X-composition -> BinOp of PFuncs(X,X) equals
:: MONOID_0:def 39
the multF of GPFuncs X;
end;
:: corollary
:: MPFuncs X is constituted-Functions strict Monoid;
theorem :: MONOID_0:68
x is Element of GPFuncs X iff x is PartFunc of X,X;
theorem :: MONOID_0:69
the_unity_wrt the multF of GPFuncs X = id X;
theorem :: MONOID_0:70
for F being non empty SubStr of GPFuncs X for f,g being Element
of F holds f [*] g = g (*) f;
theorem :: MONOID_0:71
for F being non empty SubStr of GPFuncs X st id X is Element of
F holds F is unital & the_unity_wrt the multF of F = id X;
theorem :: MONOID_0:72
Y c= X implies GPFuncs Y is SubStr of GPFuncs X;
definition
let X be set;
func GFuncs X -> strict SubStr of GPFuncs X means
:: MONOID_0:def 40
the carrier of it = Funcs(X,X);
end;
registration
let X be set;
cluster GFuncs X -> unital non empty;
end;
:: corollary
:: GFuncs X is unital associative constituted-Functions;
definition
let X be set;
func MFuncs X -> well-unital strict MonoidalExtension of GFuncs X means
:: MONOID_0:def 41
not contradiction;
end;
:: corollary
:: GFuncs X is constituted-Functions Monoid;
theorem :: MONOID_0:73
x is Element of GFuncs X iff x is Function of X,X;
theorem :: MONOID_0:74
the multF of GFuncs X = (X-composition)||Funcs(X,X);
theorem :: MONOID_0:75
the_unity_wrt the multF of GFuncs X = id X;
theorem :: MONOID_0:76
the carrier of MFuncs X = Funcs(X,X) & the multF of MFuncs X = (X
-composition)||Funcs(X,X) & 1.MFuncs X = id X;
definition
let X be set;
func GPerms X -> strict non empty SubStr of GFuncs X
means
:: MONOID_0:def 42
for f being Element of GFuncs X holds f in the carrier of it iff
f is Permutation of X;
end;
registration
let X be set;
cluster GPerms X -> unital invertible;
end;
:: corollary
:: GPerms X is constituted-Functions Group;
theorem :: MONOID_0:77
x is Element of GPerms X iff x is Permutation of X;
theorem :: MONOID_0:78
the_unity_wrt the multF of GPerms X = id X & 1_GPerms X = id X;
theorem :: MONOID_0:79
for f being Element of GPerms X holds f" = (f qua Function)";
:: 2005.05.13, A.T.
theorem :: MONOID_0:80
for S being 1-sorted st the carrier of S is functional holds S is
constituted-Functions;
theorem :: MONOID_0:81
for G be non empty multMagma, D be non empty Subset of G st
for x,y being Element of D holds x*y in D
ex H being strict non empty SubStr of G st the carrier of H = D;
theorem :: MONOID_0:82
for G be non empty multLoopStr, D be non empty Subset of G st
(for x,y being Element of D holds x*y in D) & 1.G in D
ex H being strict non empty MonoidalSubStr of G st the carrier of H = D;