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