Nuprl Lemma : fps-alg_wf
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng]. (fps-alg(X;eq;r) ∈ CAlg(r)) supposing valueall-type(X)
Proof
Definitions occuring in Statement :
fps-alg: fps-alg(X;eq;r),
calgebra: CAlg(A),
deq: EqDecider(T),
valueall-type: valueall-type(T),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
member: t ∈ T,
universe: Type,
crng: CRng
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
and: P ∧ Q,
crng: CRng,
rng: Rng,
prop: ℙ,
calgebra: CAlg(A),
algebra: algebra{i:l}(A),
module: A-Module,
cand: A c∧ B,
alg_car: a.car,
pi1: fst(t),
fps-alg: fps-alg(X;eq;r),
power-series: PowerSeries(X;r),
alg_act: a.act,
pi2: snd(t),
alg_plus: a.plus,
all: ∀x:A. B[x],
alg_times: a.times,
so_lambda: λ2x.t[x],
so_apply: x[s],
rng_car: |r|,
fps-rng: fps-rng(r),
rng_times: *,
ring_p: IsRing(T;plus;zero;neg;times;one),
rng_plus: +r,
rng_zero: 0,
rng_minus: -r,
alg_zero: a.zero,
alg_minus: a.minus,
rng_one: 1,
alg_one: a.one,
algebra_sig: algebra_sig{i:l}(A),
comm: Comm(T;op),
infix_ap: x f y,
guard: {T},
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
implies: P ⇒ Q
Latex:
\mforall{}[X:Type]. \mforall{}[eq:EqDecider(X)]. \mforall{}[r:CRng]. (fps-alg(X;eq;r) \mmember{} CAlg(r)) supposing valueall-type(X)
Date html generated:
2016_05_16-AM-08_12_31
Last ObjectModification:
2015_12_28-PM-06_07_36
Theory : instances
Home
Index