Nuprl Lemma : vs-bag-add-map
∀[vs:Top]. ∀[S:Type]. ∀[f,g:Top]. ∀[bs:bag(S)]. (Σ{f[b] | b ∈ bag-map(g;bs)} ~ Σ{f[g b] | b ∈ bs})
Proof
Definitions occuring in Statement :
vs-bag-add: Σ{f[b] | b ∈ bs},
uall: ∀[x:A]. B[x],
top: Top,
so_apply: x[s],
apply: f a,
universe: Type,
sqequal: s ~ t,
bag-map: bag-map(f;bs),
bag: bag(T)
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
vs-bag-add: Σ{f[b] | b ∈ bs},
member: t ∈ T,
top: Top,
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
so_lambda: λ2x.t[x],
so_apply: x[s]
Lemmas referenced :
bag-summation-map,
istype-void,
bag-subtype-list,
bag_wf,
istype-universe,
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
sqequalRule,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
isect_memberEquality_alt,
voidElimination,
hypothesis,
hypothesisEquality,
applyEquality,
dependent_functionElimination,
universeIsType,
because_Cache,
inhabitedIsType,
instantiate,
universeEquality
Latex:
\mforall{}[vs:Top]. \mforall{}[S:Type]. \mforall{}[f,g:Top]. \mforall{}[bs:bag(S)]. (\mSigma{}\{f[b] | b \mmember{} bag-map(g;bs)\} \msim{} \mSigma{}\{f[g b] | b \mmember{} bs\})
Date html generated:
2019_10_31-AM-06_25_52
Last ObjectModification:
2019_08_08-AM-11_50_37
Theory : linear!algebra
Home
Index