### Nuprl Lemma : implies-filter-equal

`∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L1,L2:T List].`
`  (filter(P;L1) = L2 ∈ (T List)) supposing `
`     (((∀x:T. ((x ∈ L2) `⇐⇒` (x ∈ L1) ∧ (↑(P x)))) ∧ (∀x,y:T.  (x before y ∈ L2 `` x before y ∈ L1))) and `
`     no_repeats(T;L1))`

Proof

Definitions occuring in Statement :  l_before: `x before y ∈ l` no_repeats: `no_repeats(T;l)` l_member: `(x ∈ l)` filter: `filter(P;l)` list: `T List` assert: `↑b` bool: `𝔹` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uiff: `uiff(P;Q)` not: `¬A` false: `False` guard: `{T}`
Lemmas referenced :  filter-equals all_wf iff_wf l_member_wf assert_wf l_before_wf no_repeats_wf list_wf bool_wf no_repeats_iff equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin extract_by_obid isectElimination hypothesisEquality dependent_functionElimination independent_isectElimination hypothesis independent_functionElimination independent_pairFormation productEquality cumulativity sqequalRule lambdaEquality applyEquality functionExtensionality functionEquality isect_memberEquality axiomEquality because_Cache equalityTransitivity equalitySymmetry universeEquality lambdaFormation voidElimination

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L1,L2:T  List].
(filter(P;L1)  =  L2)  supposing
(((\mforall{}x:T.  ((x  \mmember{}  L2)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L1)  \mwedge{}  (\muparrow{}(P  x))))
\mwedge{}  (\mforall{}x,y:T.    (x  before  y  \mmember{}  L2  {}\mRightarrow{}  x  before  y  \mmember{}  L1)))  and
no\_repeats(T;L1))

Date html generated: 2017_04_17-AM-08_35_35
Last ObjectModification: 2017_02_27-PM-04_55_03

Theory : list_1

Home Index