Nuprl Lemma : bag-combine-cons-left

[b,a,f:Top].  (⋃x∈a.b.f[x] f[a] + ⋃x∈b.f[x])


Proof




Definitions occuring in Statement :  bag-combine: x∈bs.f[x] bag-append: as bs cons-bag: x.b uall: [x:A]. B[x] top: Top so_apply: x[s] sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T bag-combine: x∈bs.f[x] top: Top all: x:A. B[x]
Lemmas referenced :  bag-map-cons bag_union_cons_lemma top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality isect_memberEquality voidElimination voidEquality hypothesis dependent_functionElimination sqequalAxiom because_Cache

Latex:
\mforall{}[b,a,f:Top].    (\mcup{}x\mmember{}a.b.f[x]  \msim{}  f[a]  +  \mcup{}x\mmember{}b.f[x])



Date html generated: 2016_05_15-PM-02_28_41
Last ObjectModification: 2015_12_27-AM-09_50_00

Theory : bags


Home Index