Nuprl Lemma : filter-for-max

`∀[A:Type]. ∀[l:A List]. ∀[m:ℤ]. ∀[g:A ⟶ ℤ].`
`  (||filter(λe.(g[e] =z m);l)|| ≥ 1 ) supposing ((imax-list(map(λe.g[e];l)) = m ∈ ℤ) and 0 < ||l||)`

Proof

Definitions occuring in Statement :  imax-list: `imax-list(L)` length: `||as||` filter: `filter(P;l)` map: `map(f;as)` list: `T List` eq_int: `(i =z j)` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` ge: `i ≥ j ` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  so_apply: `x[s]` uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` ge: `i ≥ j ` le: `A ≤ B` and: `P ∧ Q` not: `¬A` implies: `P `` Q` false: `False` prop: `ℙ` top: `Top` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` sq_type: `SQType(T)` guard: `{T}` l_member: `(x ∈ l)` exists: `∃x:A. B[x]` cand: `A c∧ B` squash: `↓T` nat: `ℕ` true: `True` iff: `P `⇐⇒` Q` int_seg: `{i..j-}` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` rev_implies: `P `` Q` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)`
Lemmas referenced :  less_than'_wf length_wf filter_wf5 eq_int_wf l_member_wf equal-wf-T-base imax-list_wf map-length int_subtype_base less_than_wf pos_length imax-list-member map_wf subtype_base_sq list_wf squash_wf true_wf map_length iff_weakening_equal equal_wf map_select lelt_wf member_filter select_wf 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 select_member assert_of_eq_int eta_conv null_nil_lemma btrue_wf member-implies-null-eq-bfalse btrue_neq_bfalse
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin independent_pairEquality lambdaEquality dependent_functionElimination hypothesisEquality because_Cache extract_by_obid isectElimination cumulativity applyEquality functionExtensionality setElimination rename hypothesis setEquality natural_numberEquality axiomEquality equalityTransitivity equalitySymmetry independent_isectElimination isect_memberEquality voidElimination voidEquality functionEquality intEquality lambdaFormation instantiate independent_functionElimination baseClosed imageElimination imageMemberEquality universeEquality dependent_set_memberEquality independent_pairFormation unionElimination dependent_pairFormation int_eqEquality computeAll hyp_replacement applyLambdaEquality

Latex:
\mforall{}[A:Type].  \mforall{}[l:A  List].  \mforall{}[m:\mBbbZ{}].  \mforall{}[g:A  {}\mrightarrow{}  \mBbbZ{}].
(||filter(\mlambda{}e.(g[e]  =\msubz{}  m);l)||  \mgeq{}  1  )  supposing  ((imax-list(map(\mlambda{}e.g[e];l))  =  m)  and  0  <  ||l||)

Date html generated: 2017_04_17-AM-07_50_39
Last ObjectModification: 2017_02_27-PM-04_24_30

Theory : list_1

Home Index