Nuprl Definition : norm_subset_p
norm_subset_p(g;s) == ∀a,b:|g|. ((s b) ⇒ (s ((~ a) * (b * a))))
Definitions occuring in Statement :
grp_inv: ~,
grp_op: *,
grp_car: |g|,
infix_ap: x f y,
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a
Definitions occuring in definition :
all: ∀x:A. B[x],
grp_car: |g|,
implies: P ⇒ Q,
apply: f a,
grp_inv: ~,
infix_ap: x f y,
grp_op: *
Latex:
norm\_subset\_p(g;s) == \mforall{}a,b:|g|. ((s b) {}\mRightarrow{} (s ((\msim{} a) * (b * a))))
Date html generated:
2016_05_15-PM-00_08_51
Last ObjectModification:
2015_09_23-AM-06_24_21
Theory : groups_1
Home
Index