Nuprl Definition : mcopower_sig
mcopower_sig{i:l}(s;g) == mon:AbMon × inj:|s| ⟶ |g| ⟶ |mon| × (h:AbMon ⟶ (|s| ⟶ |g| ⟶ |h|) ⟶ |mon| ⟶ |h|)
Definitions occuring in Statement :
function: x:A ⟶ B[x],
product: x:A × B[x],
abmonoid: AbMon,
grp_car: |g|,
set_car: |p|
Definitions occuring in definition :
product: x:A × B[x],
abmonoid: AbMon,
set_car: |p|,
function: x:A ⟶ B[x],
grp_car: |g|
FDL editor aliases :
mcopower_sig
Latex:
mcopower\_sig\{i:l\}(s;g) ==
mon:AbMon \mtimes{} inj:|s| {}\mrightarrow{} |g| {}\mrightarrow{} |mon| \mtimes{} (h:AbMon {}\mrightarrow{} (|s| {}\mrightarrow{} |g| {}\mrightarrow{} |h|) {}\mrightarrow{} |mon| {}\mrightarrow{} |h|)
Date html generated:
2016_05_16-AM-08_12_48
Last ObjectModification:
2015_09_23-AM-09_52_27
Theory : polynom_1
Home
Index