Nuprl Lemma : length-filter-pos-iff

[A:Type]. ∀P:A ⟶ 𝔹. ∀L:A List.  ((∃x∈L. ↑(P x)) ⇐⇒ 0 < ||filter(P;L)||)


Proof




Definitions occuring in Statement :  l_exists: (∃x∈L. P[x]) length: ||as|| filter: filter(P;l) list: List assert: b bool: 𝔹 less_than: a < b uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q apply: a function: x:A ⟶ B[x] natural_number: $n universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T prop: so_lambda: λ2x.t[x] so_apply: x[s] rev_implies:  Q subtype_rel: A ⊆B uimplies: supposing a or: P ∨ Q less_than: a < b squash: T less_than': less_than'(a;b) false: False cons: [a b] top: Top exists: x:A. B[x] l_member: (x ∈ l) l_exists: (∃x∈L. P[x]) nat: int_seg: {i..j-} lelt: i ≤ j < k le: A ≤ B cand: c∧ B sq_type: SQType(T) guard: {T} assert: b ifthenelse: if then else fi  btrue: tt true: True ge: i ≥  decidable: Dec(P) satisfiable_int_formula: satisfiable_int_formula(fmla) not: ¬A
Lemmas referenced :  l_exists_wf assert_wf l_member_wf less_than_wf length_wf filter_wf5 subtype_rel_dep_function bool_wf subtype_rel_self set_wf list_wf length-filter-pos equal_wf member_exists list-cases length_of_nil_lemma product_subtype_list length_of_cons_lemma cons_wf cons_neq_nil member_filter lelt_wf and_wf assert_elim subtype_base_sq bool_subtype_base select_wf int_seg_properties nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf decidable__lt intformless_wf int_formula_prop_less_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation independent_pairFormation cut hypothesis introduction extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality sqequalRule lambdaEquality applyEquality functionExtensionality setElimination rename setEquality natural_numberEquality independent_isectElimination because_Cache functionEquality universeEquality equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination unionElimination imageElimination productElimination voidElimination promote_hyp hypothesis_subsumption isect_memberEquality voidEquality dependent_pairFormation dependent_set_memberEquality applyLambdaEquality instantiate int_eqEquality intEquality computeAll

Latex:
\mforall{}[A:Type].  \mforall{}P:A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:A  List.    ((\mexists{}x\mmember{}L.  \muparrow{}(P  x))  \mLeftarrow{}{}\mRightarrow{}  0  <  ||filter(P;L)||)



Date html generated: 2017_04_17-AM-07_48_14
Last ObjectModification: 2017_02_27-PM-04_22_02

Theory : list_1


Home Index