Nuprl Definition : sg-subgroup
sg-subgroup(sg;x.P[x]) == P[1] ∧ (∀x:Point. (P[x] ⇒ P[x^-1])) ∧ (∀x,y:Point. (P[x] ⇒ P[y] ⇒ P[(x y)]))
Definitions occuring in Statement :
sg-op: (x y),
sg-inv: x^-1,
sg-id: 1,
ss-point: Point,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
sg-id: 1,
and: P ∧ Q,
sg-inv: x^-1,
all: ∀x:A. B[x],
ss-point: Point,
implies: P ⇒ Q,
sg-op: (x y)
FDL editor aliases :
sg-subgroup
Latex:
sg-subgroup(sg;x.P[x]) ==
P[1] \mwedge{} (\mforall{}x:Point. (P[x] {}\mRightarrow{} P[x\^{}-1])) \mwedge{} (\mforall{}x,y:Point. (P[x] {}\mRightarrow{} P[y] {}\mRightarrow{} P[(x y)]))
Date html generated:
2017_10_02-PM-03_25_10
Last ObjectModification:
2017_06_22-PM-04_41_52
Theory : constructive!algebra
Home
Index