Nuprl Definition : s-group-axioms
s-group-axioms(sg) == (∀[x,y,z:Point]. (x (y z)) ≡ ((x y) z)) ∧ (∀[x:Point]. (x 1) ≡ x) ∧ (∀[x:Point]. (x x^-1) ≡ 1)
Definitions occuring in Statement :
sg-op: (x y),
sg-inv: x^-1,
sg-id: 1,
ss-eq: x ≡ y,
ss-point: Point,
uall: ∀[x:A]. B[x],
and: P ∧ Q
Definitions occuring in definition :
and: P ∧ Q,
uall: ∀[x:A]. B[x],
ss-point: Point,
ss-eq: x ≡ y,
sg-op: (x y),
sg-inv: x^-1,
sg-id: 1
FDL editor aliases :
s-group-axioms
Latex:
s-group-axioms(sg) ==
(\mforall{}[x,y,z:Point]. (x (y z)) \mequiv{} ((x y) z)) \mwedge{} (\mforall{}[x:Point]. (x 1) \mequiv{} x) \mwedge{} (\mforall{}[x:Point]. (x x\^{}-1) \mequiv{} 1)
Date html generated:
2017_10_02-PM-03_24_38
Last ObjectModification:
2017_06_23-AM-11_17_44
Theory : constructive!algebra
Home
Index