Nuprl Definition : fabgrp_sig
fabgrp_sig{i:l}(s) == grp:AbGrp × inj:|s| ⟶ |grp| × (grp':AbGrp ⟶ (|s| ⟶ |grp'|) ⟶ |grp| ⟶ |grp'|)
Definitions occuring in Statement :
function: x:A ⟶ B[x],
product: x:A × B[x],
abgrp: AbGrp,
grp_car: |g|,
set_car: |p|
Definitions occuring in definition :
product: x:A × B[x],
abgrp: AbGrp,
set_car: |p|,
function: x:A ⟶ B[x],
grp_car: |g|
FDL editor aliases :
fabgrp_sig
Latex:
fabgrp\_sig\{i:l\}(s) ==
grp:AbGrp \mtimes{} inj:|s| {}\mrightarrow{} |grp| \mtimes{} (grp':AbGrp {}\mrightarrow{} (|s| {}\mrightarrow{} |grp'|) {}\mrightarrow{} |grp| {}\mrightarrow{} |grp'|)
Date html generated:
2016_05_16-AM-08_13_20
Last ObjectModification:
2015_09_23-AM-09_52_30
Theory : polynom_1
Home
Index