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-op: (x y),
implies: P ⇒ Q,
ss-point: Point,
all: ∀x:A. B[x],
sg-inv: x^-1,
and: P ∧ Q,
sg-id: 1
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:
2016_11_08-AM-09_12_29
Last ObjectModification:
2016_11_03-PM-00_17_40
Theory : inner!product!spaces
Home
Index