Nuprl Lemma : qmin-list_wf

[L:ℚ List]. qmin-list(L) ∈ ℚ supposing 0 < ||L||


Proof




Definitions occuring in Statement :  qmin-list: qmin-list(L) rationals: length: ||as|| list: List less_than: a < b uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a qmin-list: qmin-list(L) so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] prop:
Lemmas referenced :  combine-list_wf rationals_wf qmin_wf 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 hypothesis lambdaEquality hypothesisEquality independent_isectElimination axiomEquality equalityTransitivity equalitySymmetry natural_numberEquality isect_memberEquality because_Cache

Latex:
\mforall{}[L:\mBbbQ{}  List].  qmin-list(L)  \mmember{}  \mBbbQ{}  supposing  0  <  ||L||



Date html generated: 2016_05_15-PM-10_43_17
Last ObjectModification: 2015_12_27-PM-07_56_14

Theory : rationals


Home Index