Nuprl Lemma : equipollent-filter

`∀[A:Type]. ∀P:A ⟶ 𝔹. ∀L:A List.  {x:ℕ||L||| ↑P[L[x]]}  ~ ℕ||filter(P;L)||`

Proof

Definitions occuring in Statement :  equipollent: `A ~ B` select: `L[n]` length: `||as||` filter: `filter(P;l)` list: `T List` int_seg: `{i..j-}` assert: `↑b` bool: `𝔹` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` so_apply: `x[s]` int_seg: `{i..j-}` uimplies: `b supposing a` guard: `{T}` lelt: `i ≤ j < k` and: `P ∧ Q` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` implies: `P `` Q` not: `¬A` top: `Top` prop: `ℙ` less_than: `a < b` squash: `↓T` subtype_rel: `A ⊆r B` select: `L[n]` nil: `[]` it: `⋅` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` bool: `𝔹` unit: `Unit` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` bfalse: `ff` nat: `ℕ` le: `A ≤ B` less_than': `less_than'(a;b)` sq_stable: `SqStable(P)` ext-eq: `A ≡ B` rev_uimplies: `rev_uimplies(P;Q)` ge: `i ≥ j ` sq_type: `SQType(T)` true: `True`
Lemmas referenced :  last_induction equipollent_wf int_seg_wf length_wf assert_wf select_wf int_seg_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 filter_wf5 subtype_rel_dep_function bool_wf l_member_wf subtype_rel_self set_wf list_wf length_of_nil_lemma stuck-spread base_wf filter_nil_lemma equipollent-zero filter_append cons_wf nil_wf length-append length_of_cons_lemma filter_cons_lemma equal-wf-T-base bnot_wf not_wf eqtt_to_assert uiff_transitivity eqff_to_assert assert_of_bnot equal_wf equipollent-add length_wf_nat false_wf le_wf append_wf add-is-int-iff itermAdd_wf int_term_value_add_lemma equipollent_functionality_wrt_equipollent2 equipollent_inversion union_functionality_wrt_equipollent equipollent_weakening_ext-eq ext-eq_weakening equipollent-split sq_stable_from_decidable decidable__assert less_than_wf decidable__squash equipollent_functionality_wrt_equipollent lelt_wf assert_functionality_wrt_uiff select_append_front subtype_rel_sets subtype_rel_set int_seg_subtype equal-wf-base-T int_subtype_base decidable__equal_int intformeq_wf int_formula_prop_eq_lemma non_neg_length subtract_wf itermSubtract_wf int_term_value_subtract_lemma length-singleton select_append_back select-cons-hd ext-eq_wf equipollent_transitivity equipollent-one add-zero add-commutes subtype_base_sq set_subtype_base squash_wf true_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule lambdaEquality setEquality natural_numberEquality cumulativity hypothesis applyEquality functionExtensionality because_Cache setElimination rename independent_isectElimination productElimination dependent_functionElimination unionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll imageElimination independent_functionElimination baseClosed functionEquality universeEquality equalityTransitivity equalitySymmetry equalityElimination dependent_set_memberEquality addEquality pointwiseFunctionality promote_hyp baseApply closedConclusion unionEquality imageMemberEquality instantiate addLevel hyp_replacement levelHypothesis

Latex:
\mforall{}[A:Type].  \mforall{}P:A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:A  List.    \{x:\mBbbN{}||L|||  \muparrow{}P[L[x]]\}    \msim{}  \mBbbN{}||filter(P;L)||

Date html generated: 2017_04_17-AM-09_35_10
Last ObjectModification: 2017_02_27-PM-05_35_25

Theory : equipollence!!cardinality!

Home Index