### Nuprl Lemma : l_exists_filter

`∀[T:Type]. ∀[Q:T ⟶ ℙ].  ∀P:T ⟶ 𝔹. ∀L:T List.  ((∃x∈filter(P;L). Q[x]) `⇐⇒` ∃x:T. ((x ∈ L) ∧ (↑(P x)) ∧ Q[x]))`

Proof

Definitions occuring in Statement :  l_exists: `(∃x∈L. P[x])` l_member: `(x ∈ l)` filter: `filter(P;l)` list: `T List` assert: `↑b` bool: `𝔹` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` exists: `∃x:A. B[x]` member: `t ∈ T` cand: `A c∧ B` prop: `ℙ` so_apply: `x[s]` subtype_rel: `A ⊆r B` rev_implies: `P `` Q` so_lambda: `λ2x.t[x]` uimplies: `b supposing a` istype: `istype(T)`
Lemmas referenced :  l_member_wf istype-assert subtype_rel_self l_exists_iff filter_wf5 subtype_rel_dep_function bool_wf member_filter l_exists_wf list_wf istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt cut independent_pairFormation sqequalHypSubstitution productElimination thin dependent_pairFormation_alt hypothesisEquality hypothesis sqequalRule productIsType universeIsType introduction extract_by_obid isectElimination applyEquality instantiate because_Cache independent_functionElimination dependent_functionElimination lambdaEquality_alt setEquality setIsType independent_isectElimination setElimination rename inhabitedIsType promote_hyp functionIsType universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[Q:T  {}\mrightarrow{}  \mBbbP{}].
\mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:T  List.    ((\mexists{}x\mmember{}filter(P;L).  Q[x])  \mLeftarrow{}{}\mRightarrow{}  \mexists{}x:T.  ((x  \mmember{}  L)  \mwedge{}  (\muparrow{}(P  x))  \mwedge{}  Q[x]))

Date html generated: 2020_05_19-PM-09_45_26
Last ObjectModification: 2019_10_23-PM-03_58_14

Theory : list_1

Home Index