Nuprl Definition : fps-rng
fps-rng(r) == <PowerSeries(X;r), λf,g. tt, λf,g. tt, λf,g. (f+g), 0, λf.-(f), λf,g. (f*g), 1, λf,g. (inl f)>
Definitions occuring in Statement :
fps-mul: (f*g),
fps-neg: -(f),
fps-add: (f+g),
fps-one: 1,
fps-zero: 0,
power-series: PowerSeries(X;r),
btrue: tt,
lambda: λx.A[x],
pair: <a, b>,
inl: inl x
Definitions occuring in definition :
power-series: PowerSeries(X;r),
btrue: tt,
fps-add: (f+g),
fps-zero: 0,
fps-neg: -(f),
fps-mul: (f*g),
pair: <a, b>,
fps-one: 1,
lambda: λx.A[x],
inl: inl x
FDL editor aliases :
fps-rng
Latex:
fps-rng(r) == <PowerSeries(X;r), \mlambda{}f,g. tt, \mlambda{}f,g. tt, \mlambda{}f,g. (f+g), 0, \mlambda{}f.-(f), \mlambda{}f,g. (f*g), 1, \mlambda{}f,g.\000C (inl f)>
Date html generated:
2016_05_15-PM-09_47_59
Last ObjectModification:
2015_09_23-AM-08_21_14
Theory : power!series
Home
Index