Nuprl Definition : qv-constrained-no-inf
qv-constrained-no-inf(n;S;lfs) ==
(∃p:ℚ^n. qv-constrained(S;p))
∧ (∀p:ℚ^n. (qv-constrained(S;p) ⇒ (∃q:ℚ^n. (qv-constrained(S;q) ∧ qlfs-max-val(lfs;q) < qlfs-max-val(lfs;p)))))
Definitions occuring in Statement :
qlfs-max-val: qlfs-max-val(lfs;p),
qv-constrained: qv-constrained(S;p),
qvn: ℚ^n,
qless: r < s,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
exists: ∃x:A. B[x],
qvn: ℚ^n,
and: P ∧ Q,
qv-constrained: qv-constrained(S;p),
qless: r < s,
qlfs-max-val: qlfs-max-val(lfs;p)
FDL editor aliases :
qv-constrained-no-inf
Latex:
qv-constrained-no-inf(n;S;lfs) ==
(\mexists{}p:\mBbbQ{}\^{}n. qv-constrained(S;p))
\mwedge{} (\mforall{}p:\mBbbQ{}\^{}n
(qv-constrained(S;p)
{}\mRightarrow{} (\mexists{}q:\mBbbQ{}\^{}n. (qv-constrained(S;q) \mwedge{} qlfs-max-val(lfs;q) < qlfs-max-val(lfs;p)))))
Date html generated:
2016_05_15-PM-11_23_15
Last ObjectModification:
2015_09_23-AM-08_29_30
Theory : rationals
Home
Index