Nuprl Lemma : last-mapfilter3

∀[A,B:Type]. ∀[L:A List]. ∀[P:A ⟶ 𝔹]. ∀[f:{x:A| ↑(P x)}  ⟶ B].
  (last(mapfilter(f;P;L)) = (f last(L)) ∈ B) supposing ((↑(P last(L))) and (¬↑null(mapfilter(f;P;L))))


Proof

Error : references
Latex:
\mforall{}[A,B:Type].  \mforall{}[L:A  List].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:\{x:A|  \muparrow{}(P  x)\}    {}\mrightarrow{}  B].
    (last(mapfilter(f;P;L))  =  (f  last(L)))  supposing  ((\muparrow{}(P  last(L)))  and  (\mneg{}\muparrow{}null(mapfilter(f;P;L))))


Date html generated: 2020_05_19-PM-09_45_47
Last ObjectModification: 2017_07_26-PM-02_34_43

Theory : list_1


Home Index