Nuprl Definition : subgrp_p
s SubGrp of g == (s e) ∧ (∀a:|g|. ((s a) ⇒ (s (~ a)))) ∧ (∀a,b:|g|. ((s a) ⇒ (s b) ⇒ (s (a * b))))
Definitions occuring in Statement :
grp_inv: ~,
grp_id: e,
grp_op: *,
grp_car: |g|,
infix_ap: x f y,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a
Definitions occuring in definition :
grp_id: e,
and: P ∧ Q,
grp_inv: ~,
all: ∀x:A. B[x],
grp_car: |g|,
implies: P ⇒ Q,
apply: f a,
infix_ap: x f y,
grp_op: *
Latex:
s SubGrp of g ==
(s e) \mwedge{} (\mforall{}a:|g|. ((s a) {}\mRightarrow{} (s (\msim{} a)))) \mwedge{} (\mforall{}a,b:|g|. ((s a) {}\mRightarrow{} (s b) {}\mRightarrow{} (s (a * b))))
Date html generated:
2016_05_15-PM-00_08_47
Last ObjectModification:
2015_09_23-AM-06_24_20
Theory : groups_1
Home
Index