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