Nuprl Lemma : vs-double-bag-add
∀[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[T:Type]. ∀[A:T ⟶ Type]. ∀[f:x:T ⟶ bag(A[x])]. ∀[h:x:T ⟶ A[x] ⟶ Point(vs)].
∀[b:bag(T)].
(Σ{Σ{h[x;y] | y ∈ f[x]} | x ∈ b} = Σ{h[fst(p);snd(p)] | p ∈ ⋃x∈b.bag-map(λy.<x, y>;f[x])} ∈ Point(vs))
Proof
Definitions occuring in Statement :
vs-bag-add: Σ{f[b] | b ∈ bs},
vector-space: VectorSpace(K),
vs-point: Point(vs),
uall: ∀[x:A]. B[x],
so_apply: x[s1;s2],
so_apply: x[s],
pi1: fst(t),
pi2: snd(t),
lambda: λx.A[x],
function: x:A ⟶ B[x],
pair: <a, b>,
universe: Type,
equal: s = t ∈ T,
rng: Rng,
bag-combine: ⋃x∈bs.f[x],
bag-map: bag-map(f;bs),
bag: bag(T)
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
vs-bag-add: Σ{f[b] | b ∈ bs},
rng: Rng,
uimplies: b supposing a,
and: P ∧ Q,
cand: A c∧ B,
monoid_p: IsMonoid(T;op;id),
assoc: Assoc(T;op),
infix_ap: x f y,
ident: Ident(T;op;id),
squash: ↓T,
prop: ℙ,
all: ∀x:A. B[x],
true: True,
subtype_rel: A ⊆r B,
guard: {T},
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
implies: P ⇒ Q,
comm: Comm(T;op),
so_apply: x[s]
Lemmas referenced :
bag-double-summation1,
vs-point_wf,
vs-add_wf,
vs-0_wf,
vs-mon_assoc,
vs-mon_ident,
equal_wf,
squash_wf,
true_wf,
istype-universe,
vs-add-comm-nu,
subtype_rel_self,
iff_weakening_equal,
bag_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
setElimination,
rename,
because_Cache,
hypothesis,
hypothesisEquality,
lambdaEquality_alt,
inhabitedIsType,
universeIsType,
independent_isectElimination,
independent_pairFormation,
isect_memberEquality_alt,
axiomEquality,
isectIsTypeImplies,
productElimination,
applyEquality,
imageElimination,
equalityTransitivity,
equalitySymmetry,
instantiate,
universeEquality,
dependent_functionElimination,
natural_numberEquality,
imageMemberEquality,
baseClosed,
independent_functionElimination,
independent_pairEquality,
functionIsType
Latex:
\mforall{}[K:Rng]. \mforall{}[vs:VectorSpace(K)]. \mforall{}[T:Type]. \mforall{}[A:T {}\mrightarrow{} Type]. \mforall{}[f:x:T {}\mrightarrow{} bag(A[x])]. \mforall{}[h:x:T
{}\mrightarrow{} A[x]
{}\mrightarrow{} Point(vs)].
\mforall{}[b:bag(T)].
(\mSigma{}\{\mSigma{}\{h[x;y] | y \mmember{} f[x]\} | x \mmember{} b\} = \mSigma{}\{h[fst(p);snd(p)] | p \mmember{} \mcup{}x\mmember{}b.bag-map(\mlambda{}y.<x, y>f[x])\})
Date html generated:
2019_10_31-AM-06_25_55
Last ObjectModification:
2019_08_09-PM-01_29_08
Theory : linear!algebra
Home
Index