let F be PartFunc of REAL,REAL; :: thesis: for X, Y being set st F is_convex_on X & Y c= X holds
F is_convex_on Y
let X, Y be set ; :: thesis: ( F is_convex_on X & Y c= X implies F is_convex_on Y )
assume that
A1: F is_convex_on X and
A2: Y c= X ; :: thesis: F is_convex_on Y
X c= dom F by A1;
hence Y c= dom F by A2; :: according to RFUNCT_3:def 12 :: thesis: 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 holds
F . ((p * r) + ((1 - p) * s)) <= (p * (F . r)) + ((1 - p) * (F . s))
let p be Real; :: thesis: ( 0 <= p & p <= 1 implies for r, s being Real st r in Y & s in Y & (p * r) + ((1 - p) * s) in Y holds
F . ((p * r) + ((1 - p) * s)) <= (p * (F . r)) + ((1 - p) * (F . s)) )
assume A3: ( 0 <= p & p <= 1 ) ; :: thesis: for r, s being Real st r in Y & s in Y & (p * r) + ((1 - p) * s) in Y holds
F . ((p * r) + ((1 - p) * s)) <= (p * (F . r)) + ((1 - p) * (F . s))
let x, y be Real; :: thesis: ( x in Y & y in Y & (p * x) + ((1 - p) * y) in Y implies F . ((p * x) + ((1 - p) * y)) <= (p * (F . x)) + ((1 - p) * (F . y)) )
assume ( x in Y & y in Y & (p * x) + ((1 - p) * y) in Y ) ; :: thesis: F . ((p * x) + ((1 - p) * y)) <= (p * (F . x)) + ((1 - p) * (F . y))
hence F . ((p * x) + ((1 - p) * y)) <= (p * (F . x)) + ((1 - p) * (F . y)) by A1, A2, A3; :: thesis: verum