### Nuprl Lemma : maximal-in-list

`∀[A:Type]. ∀f:A ⟶ ℤ. ∀L:A List.  (∃a∈L. (∀x∈L.(f x) ≤ (f a))) supposing 0 < ||L||`

Proof

Definitions occuring in Statement :  l_exists: `(∃x∈L. P[x])` l_all: `(∀x∈L.P[x])` length: `||as||` list: `T List` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` le: `A ≤ B` all: `∀x:A. B[x]` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` uimplies: `b supposing a` so_lambda: `λ2x.t[x]` so_apply: `x[s]` implies: `P `` Q` and: `P ∧ Q` prop: `ℙ` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` exists: `∃x:A. B[x]` cand: `A c∧ B` sq_type: `SQType(T)`
Lemmas referenced :  list-max-property member-less_than length_wf istype-less_than list_wf istype-int istype-universe list-max_wf l_member_wf int_subtype_base l_all_wf le_wf l_exists_iff subtype_base_sq
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality Error :lambdaFormation_alt,  dependent_functionElimination natural_numberEquality independent_isectElimination rename Error :universeIsType,  Error :functionIsType,  instantiate universeEquality sqequalRule Error :lambdaEquality_alt,  applyEquality Error :inhabitedIsType,  productElimination Error :productIsType,  setElimination Error :equalityIstype,  because_Cache sqequalBase equalitySymmetry Error :setIsType,  equalityTransitivity independent_functionElimination Error :dependent_pairFormation_alt,  independent_pairFormation cumulativity intEquality

Latex:
\mforall{}[A:Type].  \mforall{}f:A  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}L:A  List.    (\mexists{}a\mmember{}L.  (\mforall{}x\mmember{}L.(f  x)  \mleq{}  (f  a)))  supposing  0  <  ||L||

Date html generated: 2019_06_20-PM-01_30_56
Last ObjectModification: 2018_11_28-PM-03_24_31

Theory : list_1

Home Index