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