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  before y ∈ L1))) and 


Definitions occuring in Statement :  l_before: before y ∈ l no_repeats: no_repeats(T;l) l_member: (x ∈ l) filter: filter(P;l) list: List assert: b bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q implies:  Q and: P ∧ Q apply: a function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a and: P ∧ Q all: x:A. B[x] iff: ⇐⇒ Q rev_implies:  Q implies:  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

\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 

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

Theory : list_1

Home Index