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