:: deftheorem defines is_strictly_convex_on RFUNCT_4:def 1 :
for f being PartFunc of REAL,REAL
for X being set holds
( f is_strictly_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 & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ) ) );