### Nuprl Lemma : filter_wf5

`∀[T:Type]. ∀[l:T List]. ∀[P:{x:T| (x ∈ l)}  ⟶ 𝔹].  (filter(P;l) ∈ T List)`

Proof

Definitions occuring in Statement :  l_member: `(x ∈ l)` filter: `filter(P;l)` list: `T List` bool: `𝔹` uall: `∀[x:A]. B[x]` member: `t ∈ T` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` prop: `ℙ` subtype_rel: `A ⊆r B` uimplies: `b supposing a`
Lemmas referenced :  l_member_wf bool_wf list_wf filter_wf list-subtype subtype_rel_list
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry functionEquality setEquality hypothesisEquality lemma_by_obid isectElimination thin isect_memberEquality because_Cache universeEquality cumulativity applyEquality independent_isectElimination lambdaEquality setElimination rename

Latex:
\mforall{}[T:Type].  \mforall{}[l:T  List].  \mforall{}[P:\{x:T|  (x  \mmember{}  l)\}    {}\mrightarrow{}  \mBbbB{}].    (filter(P;l)  \mmember{}  T  List)

Date html generated: 2016_05_14-AM-06_39_43
Last ObjectModification: 2015_12_26-PM-00_31_49

Theory : list_0

Home Index