Nuprl Definition : concave-on
concave-on(I;x.f[x]) ==
∀x,y,t:ℝ. ((x ∈ I) ⇒ (y ∈ I) ⇒ (t ∈ [r0, r1]) ⇒ (((t * f[x]) + ((r1 - t) * f[y])) ≤ f[(t * x) + ((r1 - t) * 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 :
concave-on
Latex:
concave-on(I;x.f[x]) ==
\mforall{}x,y,t:\mBbbR{}.
((x \mmember{} I)
{}\mRightarrow{} (y \mmember{} I)
{}\mRightarrow{} (t \mmember{} [r0, r1])
{}\mRightarrow{} (((t * f[x]) + ((r1 - t) * f[y])) \mleq{} f[(t * x) + ((r1 - t) * y)]))
Date html generated:
2018_05_22-PM-02_19_51
Last ObjectModification:
2017_10_20-PM-01_32_00
Theory : reals
Home
Index