Nuprl Definition : fabmon_of_nat_mcp
fabmon_of_nat_mcp(m) == <m.mon, λu.(m.inj u zhgrp(1)), λm',f. (m.umap m' (λz,n. (nat(n) ⋅ (f z))))>
Definitions occuring in Statement :
mcopower_umap: m.umap,
mcopower_inj: m.inj,
mcopower_mon: m.mon,
apply: f a,
lambda: λx.A[x],
pair: <a, b>,
natural_number: $n,
int_hgrp_to_nat: nat(n),
int_hgrp_el: zhgrp(n),
mon_nat_op: n ⋅ e
Definitions occuring in definition :
mcopower_mon: m.mon,
pair: <a, b>,
mcopower_inj: m.inj,
int_hgrp_el: zhgrp(n),
natural_number: $n,
mcopower_umap: m.umap,
lambda: λx.A[x],
mon_nat_op: n ⋅ e,
int_hgrp_to_nat: nat(n),
apply: f a
Latex:
fabmon\_of\_nat\_mcp(m) == <m.mon, \mlambda{}u.(m.inj u zhgrp(1)), \mlambda{}m',f. (m.umap m' (\mlambda{}z,n. (nat(n) \mcdot{} (f z))))>
Date html generated:
2016_05_16-AM-08_13_14
Last ObjectModification:
2015_09_23-AM-09_52_29
Theory : polynom_1
Home
Index