### Nuprl Lemma : map-member-wf

`∀[A,B:Type]. ∀[L:A List]. ∀[f:{a:A| (a ∈ L)}  ⟶ B].  (map(f;L) ∈ B List)`

Proof

Definitions occuring in Statement :  l_member: `(x ∈ l)` map: `map(f;as)` list: `T List` 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: `ℙ`
Lemmas referenced :  list-subtype map_wf l_member_wf list_wf
Rules used in proof :  cut lemma_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesisEquality setEquality hypothesis functionEquality because_Cache universeEquality isect_memberFormation introduction sqequalRule axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[A,B:Type].  \mforall{}[L:A  List].  \mforall{}[f:\{a:A|  (a  \mmember{}  L)\}    {}\mrightarrow{}  B].    (map(f;L)  \mmember{}  B  List)

Date html generated: 2016_05_15-PM-02_40_11
Last ObjectModification: 2015_12_27-AM-09_41_36

Theory : bags

Home Index