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: List uall: [x:A]. B[x] all: x:A. B[x] exists: x:A. B[x] implies:  Q function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] implies:  Q exists: x:A. B[x] member: t ∈ T prop: subtype_rel: A ⊆B uimplies: 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