let f be PartFunc of REAL,REAL; :: thesis: for X, Y being set st f is_strictly_convex_on X & Y c= X holds
f is_strictly_convex_on Y
let X, Y be set ; :: thesis: ( f is_strictly_convex_on X & Y c= X implies f is_strictly_convex_on Y )
assume that
A1: f is_strictly_convex_on X and
A2: Y c= X ; :: thesis: f is_strictly_convex_on Y
X c= dom f by A1, Def1;
then A3: Y c= dom f by A2, XBOOLE_1:1;
for p being Real st 0 < p & p < 1 holds
for r, s being Real st r in Y & s in Y & (p * r) + ((1 - p) * s) in Y & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) by A1, A2, Def1;
hence f is_strictly_convex_on Y by A3, Def1; :: thesis: verum