Nuprl Definition : ocgrp
OGrp == {g:OCMon| Inverse(|g|;*;e;~)}
Definitions occuring in Statement :
ocmon: OCMon
,
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]}
,
ocmon: OCMon
,
inverse: Inverse(T;op;id;inv)
,
grp_car: |g|
,
grp_op: *
,
grp_id: e
,
grp_inv: ~
Latex:
OGrp == \{g:OCMon| Inverse(|g|;*;e;\msim{})\}
Date html generated:
2016_05_15-PM-00_12_55
Last ObjectModification:
2015_09_23-AM-06_24_48
Theory : groups_1
Home
Index