Nuprl Lemma : filter_is_singleton

[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List]. ∀[x:T].
  (filter(P;L) [x] ∈ (T List)) supposing ((∀y∈L.(↑P[y])  (y x ∈ T)) and (↑P[x]) and (x ∈L))


Definitions occuring in Statement :  l_member!: (x ∈l) l_all: (∀x∈L.P[x]) filter: filter(P;l) cons: [a b] nil: [] list: List assert: b bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] implies:  Q function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] subtype_rel: A ⊆B implies:  Q so_apply: x[s] prop: uimplies: supposing a so_lambda: λ2x.t[x] member: t ∈ T uall: [x:A]. B[x] false: False satisfiable_int_formula: satisfiable_int_formula(fmla) not: ¬A ge: i ≥  nat: and: P ∧ Q so_apply: x[s1;s2] top: Top so_lambda: λ2y.t[x; y] it: nil: [] select: L[n] cand: c∧ B exists: x:A. B[x] l_member!: (x ∈l) iff: ⇐⇒ Q assert: b bnot: ¬bb guard: {T} sq_type: SQType(T) or: P ∨ Q bfalse: ff ifthenelse: if then else fi  uiff: uiff(P;Q) btrue: tt unit: Unit bool: 𝔹 true: True squash: T rev_implies:  Q
Lemmas referenced :  l_all_wf_nil nil_wf cons_wf set_wf subtype_rel_self bool_wf subtype_rel_dep_function filter_wf5 list_wf l_member_wf equal_wf l_all_wf assert_wf l_member!_wf isect_wf uall_wf list_induction int_formula_prop_wf int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_and_lemma intformle_wf itermConstant_wf itermVar_wf intformless_wf intformand_wf full-omega-unsat nat_properties filter_nil_lemma length_of_nil_lemma base_wf stuck-spread l_all_cons cons_member! assert-bnot bool_subtype_base subtype_base_sq bool_cases_sqequal eqff_to_assert eqtt_to_assert filter_cons_lemma true_wf squash_wf filter_is_nil not_wf l_all_iff and_wf iff_weakening_equal
Rules used in proof :  universeEquality Error :functionIsType,  dependent_functionElimination Error :inhabitedIsType,  equalitySymmetry equalityTransitivity axiomEquality isect_memberEquality voidEquality voidElimination Error :universeIsType,  independent_functionElimination lambdaFormation independent_isectElimination setEquality because_Cache rename setElimination functionEquality applyEquality hypothesis lambdaEquality sqequalRule hypothesisEquality isectElimination sqequalHypSubstitution extract_by_obid thin cut introduction Error :isect_memberFormation_alt,  sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution independent_pairFormation intEquality int_eqEquality dependent_pairFormation approximateComputation natural_numberEquality baseClosed productElimination cumulativity instantiate promote_hyp equalityElimination unionElimination imageMemberEquality imageElimination applyLambdaEquality dependent_set_memberEquality hyp_replacement

\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].  \mforall{}[x:T].
    (filter(P;L)  =  [x])  supposing  ((\mforall{}y\mmember{}L.(\muparrow{}P[y])  {}\mRightarrow{}  (y  =  x))  and  (\muparrow{}P[x])  and  (x  \mmember{}!  L))

Date html generated: 2019_06_20-PM-01_26_07
Last ObjectModification: 2019_01_28-PM-10_41_08

Theory : list_1

Home Index