Nuprl Lemma : bag-map-member-wf

`∀[A,B:Type]. ∀[bs:bag(A)]. ∀[f:{a:A| a ↓∈ bs}  ⟶ B].  (bag-map(f;bs) ∈ bag(B))`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` bag-map: `bag-map(f;bs)` bag: `bag(T)` uall: `∀[x:A]. B[x]` 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` prop: `ℙ` all: `∀x:A. B[x]`
Lemmas referenced :  bag-map_wf bag-member_wf bag-subtype bag_wf
Rules used in proof :  cut lemma_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesisEquality setEquality hypothesis cumulativity dependent_functionElimination equalityTransitivity equalitySymmetry functionEquality because_Cache universeEquality isect_memberFormation introduction sqequalRule axiomEquality isect_memberEquality

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

Date html generated: 2016_05_15-PM-02_47_01
Last ObjectModification: 2015_12_27-AM-09_36_29

Theory : bags

Home Index