### Nuprl Lemma : l_all-mapfilter

`∀[T,A:Type].`
`  ∀as:T List. ∀p:{a:T| (a ∈ as)}  ⟶ 𝔹. ∀f:{a:T| (a ∈ as) ∧ (↑(p a))}  ⟶ A. ∀P:A ⟶ ℙ.`
`    ((∀x∈mapfilter(f;p;as).P[x]) `⇐⇒` (∀x∈as.(↑(p x)) `` P[f x]))`

Proof

Definitions occuring in Statement :  mapfilter: `mapfilter(f;P;L)` l_all: `(∀x∈L.P[x])` l_member: `(x ∈ l)` list: `T List` assert: `↑b` bool: `𝔹` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` and: `P ∧ Q` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` prop: `ℙ` and: `P ∧ Q` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uimplies: `b supposing a` istype: `istype(T)` iff: `P `⇐⇒` Q` implies: `P `` Q` rev_implies: `P `` Q` cand: `A c∧ B` exists: `∃x:A. B[x]` guard: `{T}`
Lemmas referenced :  l_all_wf mapfilter_wf l_member_wf list-subtype assert_wf subtype_rel_dep_function istype-universe l_all_iff subtype_rel_self bool_wf list_wf member-mapfilter
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality setEquality hypothesis equalityTransitivity equalitySymmetry functionExtensionality applyEquality setElimination rename Error :dependent_set_memberEquality_alt,  independent_pairFormation sqequalRule Error :productIsType,  Error :universeIsType,  instantiate cumulativity Error :lambdaEquality_alt,  universeEquality because_Cache Error :setIsType,  independent_isectElimination dependent_functionElimination functionEquality productEquality productElimination independent_functionElimination Error :functionIsType,  Error :inhabitedIsType,  Error :dependent_pairFormation_alt,  Error :equalityIsType1,  hyp_replacement applyLambdaEquality

Latex:
\mforall{}[T,A:Type].
\mforall{}as:T  List.  \mforall{}p:\{a:T|  (a  \mmember{}  as)\}    {}\mrightarrow{}  \mBbbB{}.  \mforall{}f:\{a:T|  (a  \mmember{}  as)  \mwedge{}  (\muparrow{}(p  a))\}    {}\mrightarrow{}  A.  \mforall{}P:A  {}\mrightarrow{}  \mBbbP{}.
((\mforall{}x\mmember{}mapfilter(f;p;as).P[x])  \mLeftarrow{}{}\mRightarrow{}  (\mforall{}x\mmember{}as.(\muparrow{}(p  x))  {}\mRightarrow{}  P[f  x]))

Date html generated: 2019_06_20-PM-01_27_40
Last ObjectModification: 2018_10_05-AM-10_53_17

Theory : list_1

Home Index