Nuprl Definition : generated-s-subgroup
generated-s-subgroup(sg;f.P[f]) == mk-s-subgroup(sg;g.∃L:Point List. ((∀f∈L.P[f]) ∧ g ≡ reduce(λx,y. (x y);1;L)))
Definitions occuring in Statement :
mk-s-subgroup: mk-s-subgroup(sg;x.P[x]),
sg-op: (x y),
sg-id: 1,
ss-eq: x ≡ y,
ss-point: Point,
l_all: (∀x∈L.P[x]),
reduce: reduce(f;k;as),
list: T List,
exists: ∃x:A. B[x],
and: P ∧ Q,
lambda: λx.A[x]
Definitions occuring in definition :
exists: ∃x:A. B[x],
list: T List,
and: P ∧ Q,
l_all: (∀x∈L.P[x]),
reduce: reduce(f;k;as),
lambda: λx.A[x]
FDL editor aliases :
generated-s-subgroup
Latex:
generated-s-subgroup(sg;f.P[f]) ==
mk-s-subgroup(sg;g.\mexists{}L:Point List. ((\mforall{}f\mmember{}L.P[f]) \mwedge{} g \mequiv{} reduce(\mlambda{}x,y. (x y);1;L)))
Date html generated:
2017_10_02-PM-03_25_25
Last ObjectModification:
2017_06_22-PM-04_40_17
Theory : constructive!algebra
Home
Index