### Nuprl Lemma : bag-map_wf

[B,A:Type]. ∀[f:A ⟶ B]. ∀[bs:bag(A)].  (bag-map(f;bs) ∈ bag(B))

Proof

Definitions occuring in Statement :  bag-map: bag-map(f;bs) bag: bag(T) uall: [x:A]. B[x] member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  bag: bag(T) member: t ∈ T uall: [x:A]. B[x] quotient: x,y:A//B[x; y] and: P ∧ Q bag-map: bag-map(f;bs) so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] uimplies: supposing a all: x:A. B[x] implies:  Q prop:
Lemmas referenced :  bag_wf quotient-member-eq list_wf permutation_wf permutation-equiv map_wf permutation-map equal-wf-base
Rules used in proof :  sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity pointwiseFunctionalityForEquality cut lemma_by_obid isectElimination thin hypothesisEquality hypothesis sqequalRule pertypeElimination productElimination lambdaEquality independent_isectElimination dependent_functionElimination independent_functionElimination equalityTransitivity equalitySymmetry productEquality because_Cache cumulativity functionEquality universeEquality isect_memberFormation introduction axiomEquality isect_memberEquality

Latex:
\mforall{}[B,A:Type].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[bs:bag(A)].    (bag-map(f;bs)  \mmember{}  bag(B))

Date html generated: 2016_05_15-PM-02_22_00
Last ObjectModification: 2015_12_27-AM-09_55_15

Theory : bags

Home Index