### Nuprl Lemma : imax-list-lb

`∀[L:ℤ List]. ∀[a:ℤ].  uiff(imax-list(L) ≤ a;(∀b∈L.b ≤ a)) supposing 0 < ||L||`

Proof

Definitions occuring in Statement :  imax-list: `imax-list(L)` l_all: `(∀x∈L.P[x])` length: `||as||` list: `T List` less_than: `a < b` uiff: `uiff(P;Q)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` le: `A ≤ B` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  assoc: `Assoc(T;op)` uall: `∀[x:A]. B[x]` member: `t ∈ T` infix_ap: `x f y` uimplies: `b supposing a` all: `∀x:A. B[x]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` guard: `{T}` prop: `ℙ` rev_implies: `P `` Q` cand: `A c∧ B` imax-list: `imax-list(L)` uiff: `uiff(P;Q)` l_all: `(∀x∈L.P[x])` le: `A ≤ B` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  imax_assoc istype-int combine-list-rel-and imax_wf le_wf iff_weakening_uiff imax_lb le_witness_for_triv imax-list_wf l_all_wf l_member_wf less_than_wf length_wf list_wf
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis Error :inhabitedIsType,  Error :isect_memberEquality_alt,  axiomEquality intEquality dependent_functionElimination Error :lambdaEquality_alt,  because_Cache independent_functionElimination Error :lambdaFormation_alt,  independent_pairFormation productElimination Error :universeIsType,  productEquality Error :productIsType,  promote_hyp independent_isectElimination equalityTransitivity equalitySymmetry Error :functionIsTypeImplies,  setElimination rename Error :setIsType,  independent_pairEquality natural_numberEquality

Latex:
\mforall{}[L:\mBbbZ{}  List].  \mforall{}[a:\mBbbZ{}].    uiff(imax-list(L)  \mleq{}  a;(\mforall{}b\mmember{}L.b  \mleq{}  a))  supposing  0  <  ||L||

Date html generated: 2019_06_20-PM-01_19_38
Last ObjectModification: 2018_10_07-AM-00_02_43

Theory : list_1

Home Index