Nuprl Definition : grp

Group{i} ==  {g:Mon| Inverse(|g|;*;e;~)} 



Definitions occuring in Statement :  mon: Mon grp_inv: ~ grp_id: e grp_op: * grp_car: |g| inverse: Inverse(T;op;id;inv) set: {x:A| B[x]} 
Definitions occuring in definition :  set: {x:A| B[x]}  mon: Mon inverse: Inverse(T;op;id;inv) grp_car: |g| grp_op: * grp_id: e grp_inv: ~

Latex:
Group\{i\}  ==    \{g:Mon|  Inverse(|g|;*;e;\msim{})\} 



Date html generated: 2016_05_15-PM-00_08_32
Last ObjectModification: 2015_09_23-AM-06_24_19

Theory : groups_1


Home Index