Nuprl Lemma : map-member-wf

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


Proof




Definitions occuring in Statement :  l_member: (x ∈ l) map: map(f;as) list: 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