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: 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-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