### Nuprl Lemma : bag-combine-restrict_wf

`∀[A,B:Type]. ∀[b:bag(A)]. ∀[f:{a:A| a ↓∈ b}  ⟶ bag(B)].  (bag-combine-restrict(b;x.f[x]) ∈ bag(B))`

Proof

Definitions occuring in Statement :  bag-combine-restrict: `bag-combine-restrict(b;x.f[x])` bag-member: `x ↓∈ bs` bag: `bag(T)` uall: `∀[x:A]. B[x]` so_apply: `x[s]` member: `t ∈ T` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` bag-combine-restrict: `bag-combine-restrict(b;x.f[x])` bag-combine: `⋃x∈bs.f[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]`
Lemmas referenced :  bag-union_wf bag-map_wf bag_wf bag-member_wf bag-subtype
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setEquality lambdaEquality applyEquality cumulativity dependent_functionElimination equalityTransitivity equalitySymmetry sqequalRule axiomEquality functionEquality isect_memberEquality because_Cache universeEquality

Latex:
\mforall{}[A,B:Type].  \mforall{}[b:bag(A)].  \mforall{}[f:\{a:A|  a  \mdownarrow{}\mmember{}  b\}    {}\mrightarrow{}  bag(B)].    (bag-combine-restrict(b;x.f[x])  \mmember{}  bag(B))

Date html generated: 2016_05_15-PM-02_49_00
Last ObjectModification: 2015_12_27-AM-09_35_19

Theory : bags

Home Index