Nuprl Definition : qv-convex
qv-convex(p.S[p]) ==
∀p,q:ℚ List.
((dimension(p) = dimension(q) ∈ ℤ)
⇒ S[p]
⇒ S[q]
⇒ (∀t:ℚ. ((0 ≤ t) ⇒ (t ≤ 1) ⇒ S[qv-add(qv-mul(t;p);qv-mul(1 - t;q))])))
Definitions occuring in Statement :
qv-mul: qv-mul(r;bs),
qv-add: qv-add(as;bs),
qv-dim: dimension(as),
qle: r ≤ s,
qsub: r - s,
rationals: ℚ,
list: T List,
all: ∀x:A. B[x],
implies: P ⇒ Q,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
list: T List,
equal: s = t ∈ T,
int: ℤ,
qv-dim: dimension(as),
all: ∀x:A. B[x],
rationals: ℚ,
implies: P ⇒ Q,
qle: r ≤ s,
qv-add: qv-add(as;bs),
qv-mul: qv-mul(r;bs),
qsub: r - s,
natural_number: $n
FDL editor aliases :
qv-convex
Latex:
qv-convex(p.S[p]) ==
\mforall{}p,q:\mBbbQ{} List.
((dimension(p) = dimension(q))
{}\mRightarrow{} S[p]
{}\mRightarrow{} S[q]
{}\mRightarrow{} (\mforall{}t:\mBbbQ{}. ((0 \mleq{} t) {}\mRightarrow{} (t \mleq{} 1) {}\mRightarrow{} S[qv-add(qv-mul(t;p);qv-mul(1 - t;q))])))
Date html generated:
2016_05_15-PM-11_21_10
Last ObjectModification:
2015_09_23-AM-08_28_48
Theory : rationals
Home
Index