Nuprl Definition : fps-ucont
fps-ucont(X;eq;r;f.G[f]) == ∀b:bag(X). ∃d:bag(X). ∀f:PowerSeries(X;r). (G[f][b] = G[fps-restrict(eq;r;f;d)][b] ∈ |r|)
Definitions occuring in Statement :
fps-restrict: fps-restrict(eq;r;f;d),
fps-coeff: f[b],
power-series: PowerSeries(X;r),
bag: bag(T),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
equal: s = t ∈ T,
rng_car: |r|
Definitions occuring in definition :
exists: ∃x:A. B[x],
bag: bag(T),
all: ∀x:A. B[x],
power-series: PowerSeries(X;r),
equal: s = t ∈ T,
rng_car: |r|,
fps-coeff: f[b],
fps-restrict: fps-restrict(eq;r;f;d)
FDL editor aliases :
fps-ucont
Latex:
fps-ucont(X;eq;r;f.G[f]) ==
\mforall{}b:bag(X). \mexists{}d:bag(X). \mforall{}f:PowerSeries(X;r). (G[f][b] = G[fps-restrict(eq;r;f;d)][b])
Date html generated:
2016_05_15-PM-09_57_05
Last ObjectModification:
2015_09_23-AM-08_21_30
Theory : power!series
Home
Index