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 A1: ( F is_convex_on X & Y c= X ) ; :: thesis: F is_convex_on Y
then X c= dom F by Def13;
hence Y c= dom F by A1, XBOOLE_1:1; :: according to RFUNCT_3:def 13 :: 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 A2: ( 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, Def13; :: thesis: verum