### Nuprl Lemma : mapfilter_wf

`∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ 𝔹]. ∀[T':Type]. ∀[f:{x:T| ↑(P x)}  ⟶ T'].  (mapfilter(f;P;L) ∈ T' List)`

Proof

Definitions occuring in Statement :  mapfilter: `mapfilter(f;P;L)` list: `T List` assert: `↑b` bool: `𝔹` uall: `∀[x:A]. B[x]` member: `t ∈ T` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` mapfilter: `mapfilter(f;P;L)` prop: `ℙ`
Lemmas referenced :  filter_type map_wf assert_wf bool_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality setEquality applyEquality hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry Error :functionIsType,  Error :setIsType,  Error :universeIsType,  isect_memberEquality functionEquality Error :inhabitedIsType,  because_Cache universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[T':Type].  \mforall{}[f:\{x:T|  \muparrow{}(P  x)\}    {}\mrightarrow{}  T'].
(mapfilter(f;P;L)  \mmember{}  T'  List)

Date html generated: 2019_06_20-PM-01_24_59
Last ObjectModification: 2018_09_26-PM-05_28_58

Theory : list_1

Home Index