Nuprl Lemma : qv-constrained-no-inf_wf

[n:ℕ]. ∀[S,lfs:q-linear-form(n) List].  qv-constrained-no-inf(n;S;lfs) ∈ ℙ supposing 0 < ||lfs||


Proof




Definitions occuring in Statement :  qv-constrained-no-inf: qv-constrained-no-inf(n;S;lfs) q-linear-form: q-linear-form(n) length: ||as|| list: List nat: less_than: a < b uimplies: supposing a uall: [x:A]. B[x] prop: member: t ∈ T natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a qv-constrained-no-inf: qv-constrained-no-inf(n;S;lfs) prop: and: P ∧ Q so_lambda: λ2x.t[x] so_apply: x[s] exists: x:A. B[x] implies:  Q all: x:A. B[x]
Lemmas referenced :  exists_wf qvn_wf qv-constrained_wf all_wf qless_wf qlfs-max-val_wf less_than_wf length_wf q-linear-form_wf list_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule productEquality lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaEquality because_Cache functionEquality independent_isectElimination axiomEquality equalityTransitivity equalitySymmetry natural_numberEquality isect_memberEquality

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[S,lfs:q-linear-form(n)  List].    qv-constrained-no-inf(n;S;lfs)  \mmember{}  \mBbbP{}  supposing  0  <  ||lfs||



Date html generated: 2016_05_15-PM-11_23_20
Last ObjectModification: 2015_12_27-PM-07_31_22

Theory : rationals


Home Index