Nuprl Lemma : lookup_omral_scale_d
∀g:OCMon. ∀r:CDRng. ∀z,k:|g|. ∀v:|r|. ∀ps:|omral(g;r)|.
(((<k,v>* ps)[z]) = (Σy ∈ dom(ps). (when (k * y) =b z. (v * (ps[y])))) ∈ |r|)
Proof
Definitions occuring in Statement :
omral_scale: <k,v>* ps,
omral_dom: dom(ps),
omralist: omral(g;r),
lookup: as[k],
rng_mssum: rng_mssum,
infix_ap: x f y,
all: ∀x:A. B[x],
equal: s = t ∈ T,
rng_when: rng_when,
cdrng: CDRng,
rng_times: *,
rng_zero: 0,
rng_car: |r|,
oset_of_ocmon: g↓oset,
ocmon: OCMon,
dset_of_mon: g↓set,
grp_op: *,
grp_eq: =b,
grp_car: |g|,
set_car: |p|
Definitions unfolded in proof :
rng_mssum: rng_mssum,
oset_of_ocmon: g↓oset,
infix_ap: x f y,
rng_when: rng_when,
all: ∀x:A. B[x]
Lemmas referenced :
lookup_omral_scale_c
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
cut,
lemma_by_obid,
sqequalHypSubstitution,
hypothesis
Latex:
\mforall{}g:OCMon. \mforall{}r:CDRng. \mforall{}z,k:|g|. \mforall{}v:|r|. \mforall{}ps:|omral(g;r)|.
(((<k,v>* ps)[z]) = (\mSigma{}y \mmember{} dom(ps). (when (k * y) =\msubb{} z. (v * (ps[y])))))
Date html generated:
2016_05_16-AM-08_25_21
Last ObjectModification:
2015_12_28-PM-06_38_40
Theory : polynom_3
Home
Index