### Nuprl Lemma : filter_wf2

`∀[T:Type]. ∀[l:T List]. ∀[P:{x:T| (x ∈ l)}  ⟶ 𝔹].  (filter(P;l) ∈ {x:T| (x ∈ l)}  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` so_lambda: `λ2x.t[x]` so_apply: `x[s]` all: `∀x:A. B[x]` uimplies: `b supposing a`
Lemmas referenced :  l_member_wf bool_wf list_wf filter_wf5 list-subtype subtype_rel_dep_function set_wf
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 applyEquality lambdaEquality lambdaFormation setElimination rename independent_isectElimination

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

Date html generated: 2016_05_14-AM-06_39_48
Last ObjectModification: 2015_12_26-PM-00_31_52

Theory : list_0

Home Index