Nuprl Definition : subgrp_p

SubGrp of ==  (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: y all: x:A. B[x] implies:  Q and: P ∧ Q apply: a
Definitions occuring in definition :  grp_id: e and: P ∧ Q grp_inv: ~ all: x:A. B[x] grp_car: |g| implies:  Q apply: a infix_ap: y grp_op: *

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