:: deftheorem defines is_convex_on RFUNCT_3:def 12 :
for F being PartFunc of REAL,REAL
for X being set holds
( F is_convex_on X iff ( X c= dom F & ( for p being Real st 0 <= p & p <= 1 holds
for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds
F . ((p * r) + ((1 - p) * s)) <= (p * (F . r)) + ((1 - p) * (F . s)) ) ) );