### Nuprl Lemma : bag-map-list-map

`∀[T,U:Type].  ∀L1:T List. ∀L2:U List. ∀f:T ⟶ U.  ((L2 = map(f;L1) ∈ bag(U)) `` (∃L:U List. (L = map(f;L1) ∈ (U List))))`

Proof

Definitions occuring in Statement :  bag: `bag(T)` map: `map(f;as)` list: `T List` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` exists: `∃x:A. B[x]` member: `t ∈ T` prop: `ℙ` subtype_rel: `A ⊆r B` uimplies: `b supposing a`
Lemmas referenced :  map_wf equal_wf list_wf bag_wf list-subtype-bag
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation dependent_pairFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis because_Cache cumulativity applyEquality independent_isectElimination lambdaEquality sqequalRule functionEquality universeEquality

Latex:
\mforall{}[T,U:Type].    \mforall{}L1:T  List.  \mforall{}L2:U  List.  \mforall{}f:T  {}\mrightarrow{}  U.    ((L2  =  map(f;L1))  {}\mRightarrow{}  (\mexists{}L:U  List.  (L  =  map(f;L1))))

Date html generated: 2016_05_15-PM-02_38_18
Last ObjectModification: 2015_12_27-AM-09_42_58

Theory : bags

Home Index