Nuprl Definition : mk-s-subgroup
mk-s-subgroup(sg;x.P[x]) ==  mk-s-group(set-ss(sg;x.P[x]); 1; λx.x^-1; λx,y. (x y); sg."opsep"; sg."invsep")
Definitions occuring in Statement : 
mk-s-group: mk-s-group(ss; e; i; o; sep; invsep)
, 
sg-op: (x y)
, 
sg-inv: x^-1
, 
sg-id: 1
, 
set-ss: set-ss(ss;x.P[x])
, 
lambda: λx.A[x]
, 
token: "$token"
, 
record-select: r.x
Definitions occuring in definition : 
mk-s-group: mk-s-group(ss; e; i; o; sep; invsep)
, 
set-ss: set-ss(ss;x.P[x])
, 
sg-id: 1
, 
sg-inv: x^-1
, 
lambda: λx.A[x]
, 
sg-op: (x y)
, 
record-select: r.x
, 
token: "$token"
FDL editor aliases : 
mk-s-subgroup
Latex:
mk-s-subgroup(sg;x.P[x])  ==
    mk-s-group(set-ss(sg;x.P[x]);  1;  \mlambda{}x.x\^{}-1;  \mlambda{}x,y.  (x  y);  sg."opsep";  sg."invsep")
Date html generated:
2017_10_02-PM-03_25_11
Last ObjectModification:
2017_06_22-PM-04_41_55
Theory : constructive!algebra
Home
Index