Nuprl Definition : convex-on
convex-on(I;x.f[x]) ==
∀x,y,t:ℝ. ((x ∈ I) ⇒ (y ∈ I) ⇒ (t ∈ [r0, r1]) ⇒ (f[(t * x) + ((r1 - t) * y)] ≤ ((t * f[x]) + ((r1 - t) * f[y]))))
Definitions occuring in Statement :
rccint: [l, u],
i-member: r ∈ I,
rleq: x ≤ y,
rsub: x - y,
rmul: a * b,
radd: a + b,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
real: ℝ,
implies: P ⇒ Q,
i-member: r ∈ I,
rccint: [l, u],
rleq: x ≤ y,
radd: a + b,
rmul: a * b,
rsub: x - y,
int-to-real: r(n),
natural_number: $n
FDL editor aliases :
convex-on
Latex:
convex-on(I;x.f[x]) ==
\mforall{}x,y,t:\mBbbR{}.
((x \mmember{} I)
{}\mRightarrow{} (y \mmember{} I)
{}\mRightarrow{} (t \mmember{} [r0, r1])
{}\mRightarrow{} (f[(t * x) + ((r1 - t) * y)] \mleq{} ((t * f[x]) + ((r1 - t) * f[y]))))
Date html generated:
2018_05_22-PM-02_19_01
Last ObjectModification:
2017_10_20-PM-01_13_35
Theory : reals
Home
Index