Nuprl Lemma : bag-combine-single-right-as-map
∀[bs,f:Top]. (⋃x∈bs.{f[x]} ~ bag-map(λx.f[x];bs))
Proof
Definitions occuring in Statement :
bag-combine: ⋃x∈bs.f[x],
bag-map: bag-map(f;bs),
single-bag: {x},
uall: ∀[x:A]. B[x],
top: Top,
so_apply: x[s],
lambda: λx.A[x],
sqequal: s ~ t
Definitions unfolded in proof :
bag-map: bag-map(f;bs),
single-bag: {x},
bag-combine: ⋃x∈bs.f[x],
bag-union: bag-union(bbs),
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
member: t ∈ T,
top: Top,
so_apply: x[s]
Lemmas referenced :
concat-map-single,
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
isect_memberEquality,
voidElimination,
voidEquality,
hypothesis,
isect_memberFormation,
introduction,
sqequalAxiom,
hypothesisEquality,
because_Cache
Latex:
\mforall{}[bs,f:Top]. (\mcup{}x\mmember{}bs.\{f[x]\} \msim{} bag-map(\mlambda{}x.f[x];bs))
Date html generated:
2016_05_15-PM-02_28_32
Last ObjectModification:
2015_12_27-AM-09_50_16
Theory : bags
Home
Index