### Nuprl Lemma : sv-bag-only-map2

`∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[b:bag(A)].`
`  (sv-bag-only(bag-map(f;b)) = (f sv-bag-only(b)) ∈ B) supposing (0 < #(b) and single-valued-bag(b;A))`

Proof

Definitions occuring in Statement :  sv-bag-only: `sv-bag-only(b)` single-valued-bag: `single-valued-bag(b;T)` bag-size: `#(bs)` bag-map: `bag-map(f;bs)` bag: `bag(T)` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` so_apply: `x[s]` prop: `ℙ` subtype_rel: `A ⊆r B` nat: `ℕ`
Lemmas referenced :  sv-bag-only-map less_than_wf bag-size_wf nat_wf single-valued-bag_wf bag_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_isectElimination hypothesis natural_numberEquality applyEquality lambdaEquality setElimination rename sqequalRule isect_memberEquality axiomEquality because_Cache equalityTransitivity equalitySymmetry functionEquality universeEquality

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[b:bag(A)].
(sv-bag-only(bag-map(f;b))  =  (f  sv-bag-only(b)))  supposing  (0  <  \#(b)  and  single-valued-bag(b;A))

Date html generated: 2016_05_15-PM-02_44_09
Last ObjectModification: 2015_12_27-AM-09_38_33

Theory : bags

Home Index