### Nuprl Lemma : list-max_wf

`∀[T:Type]. ∀[f:T ⟶ ℤ]. ∀[L:T List].  list-max(x.f[x];L) ∈ i:ℤ × {x:T| f[x] = i ∈ ℤ}  supposing 0 < ||L||`

Proof

Definitions occuring in Statement :  list-max: `list-max(x.f[x];L)` length: `||as||` list: `T List` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` member: `t ∈ T` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` product: `x:A × B[x]` natural_number: `\$n` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` list-max: `list-max(x.f[x];L)` so_apply: `x[s]` subtype_rel: `A ⊆r B` prop: `ℙ` so_lambda: `λ2x.t[x]` all: `∀x:A. B[x]` and: `P ∧ Q`
Lemmas referenced :  outl_wf equal-wf-T-base top_wf list-max-aux_wf list-max-aux-property less_than_wf length_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin productEquality intEquality setEquality cumulativity hypothesisEquality applyEquality because_Cache hypothesis lambdaEquality independent_isectElimination dependent_functionElimination productElimination axiomEquality equalityTransitivity equalitySymmetry natural_numberEquality isect_memberEquality functionEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[L:T  List].    list-max(x.f[x];L)  \mmember{}  i:\mBbbZ{}  \mtimes{}  \{x:T|  f[x]  =  i\}    supposing  0  <  ||L|\000C|

Date html generated: 2016_05_14-PM-01_43_07
Last ObjectModification: 2015_12_26-PM-05_31_36

Theory : list_1

Home Index