### Nuprl Lemma : bag-combine-unit-left-top

`∀[f,a:Top].  (⋃x∈[a].f[x] ~ f[a] + {})`

Proof

Definitions occuring in Statement :  bag-combine: `⋃x∈bs.f[x]` bag-append: `as + bs` empty-bag: `{}` cons: `[a / b]` nil: `[]` uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s]` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` empty-bag: `{}` bag-append: `as + bs` bag-combine: `⋃x∈bs.f[x]` bag-map: `bag-map(f;bs)` bag-union: `bag-union(bbs)` all: `∀x:A. B[x]` top: `Top` concat: `concat(ll)`
Lemmas referenced :  map_cons_lemma map_nil_lemma reduce_cons_lemma reduce_nil_lemma top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis sqequalAxiom isectElimination hypothesisEquality because_Cache

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

Date html generated: 2016_05_15-PM-02_28_15
Last ObjectModification: 2015_12_27-AM-09_50_44

Theory : bags

Home Index