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 :
set-ss: set-ss(ss;x.P[x]),
mk-s-group: mk-s-group(ss; e; i; o; sep; invsep),
sg-op: (x y),
sg-inv: x^-1,
sg-id: 1,
lambda: λx.A[x],
token: "$token",
record-select: r.x
Definitions occuring in definition :
token: "$token",
record-select: r.x,
sg-op: (x y),
lambda: λx.A[x],
sg-inv: x^-1,
sg-id: 1,
set-ss: set-ss(ss;x.P[x]),
mk-s-group: mk-s-group(ss; e; i; o; sep; invsep)
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:
2016_11_08-AM-09_12_33
Last ObjectModification:
2016_11_03-AM-00_12_06
Theory : inner!product!spaces
Home
Index