### Nuprl Lemma : member-mapfilter

`∀[T:Type]`
`  ∀L:T List. ∀P:{x:T| (x ∈ L)}  ⟶ 𝔹.`
`    ∀[T':Type]`
`      ∀f:{x:T| (x ∈ L) c∧ (↑(P x))}  ⟶ T'. ∀x:T'.`
`        ((x ∈ mapfilter(f;P;L)) `⇐⇒` ∃y:T. ((y ∈ L) ∧ ((↑(P y)) c∧ (x = (f y) ∈ T'))))`

Proof

Definitions occuring in Statement :  mapfilter: `mapfilter(f;P;L)` l_member: `(x ∈ l)` list: `T List` assert: `↑b` bool: `𝔹` uall: `∀[x:A]. B[x]` cand: `A c∧ B` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  member: `t ∈ T`
Lemmas referenced :  member-mapfilter-witness_wf
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut lemma_by_obid hypothesis

Latex:
\mforall{}[T:Type]
\mforall{}L:T  List.  \mforall{}P:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbB{}.
\mforall{}[T':Type]
\mforall{}f:\{x:T|  (x  \mmember{}  L)  c\mwedge{}  (\muparrow{}(P  x))\}    {}\mrightarrow{}  T'.  \mforall{}x:T'.
((x  \mmember{}  mapfilter(f;P;L))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}y:T.  ((y  \mmember{}  L)  \mwedge{}  ((\muparrow{}(P  y))  c\mwedge{}  (x  =  (f  y)))))

Date html generated: 2016_05_14-AM-07_50_39
Last ObjectModification: 2015_12_26-PM-04_46_02

Theory : list_1

Home Index