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