Nuprl Definition : qv-constrained-sup

qv-constrained-sup(n;S;lfs;p;r) ==
  qv-constrained(S;p)
  ∧ (qlfs-min-val(lfs;p) r ∈ ℚ)
  ∧ (∀q:ℚ^n. (qv-constrained(S;q)  (qlfs-min-val(lfs;q) ≤ qlfs-min-val(lfs;p))))



Definitions occuring in Statement :  qlfs-min-val: qlfs-min-val(lfs;p) qv-constrained: qv-constrained(S;p) qvn: ^n qle: r ≤ s rationals: all: x:A. B[x] implies:  Q and: P ∧ Q equal: t ∈ T
Definitions occuring in definition :  and: P ∧ Q equal: t ∈ T rationals: all: x:A. B[x] qvn: ^n implies:  Q qv-constrained: qv-constrained(S;p) qle: r ≤ s qlfs-min-val: qlfs-min-val(lfs;p)
FDL editor aliases :  qv-constrained-sup

Latex:
qv-constrained-sup(n;S;lfs;p;r)  ==
    qv-constrained(S;p)
    \mwedge{}  (qlfs-min-val(lfs;p)  =  r)
    \mwedge{}  (\mforall{}q:\mBbbQ{}\^{}n.  (qv-constrained(S;q)  {}\mRightarrow{}  (qlfs-min-val(lfs;q)  \mleq{}  qlfs-min-val(lfs;p))))



Date html generated: 2016_05_15-PM-11_23_25
Last ObjectModification: 2015_09_23-AM-08_29_35

Theory : rationals


Home Index