:: RFUNCT_4 semantic presentation

begin


theorem Th1: :: RFUNCT_4:1
for a, b being real number holds max (a,b) >= min (a,b)
proof
let a, b be real number ; ::_thesis: max (a,b) >= min (a,b)
percases ( min (a,b) = a or min (a,b) = b ) by XXREAL_0:15;
suppose min (a,b) = a ; ::_thesis: max (a,b) >= min (a,b)
hence  max (a,b) >= min (a,b) by XXREAL_0:25; ::_thesis: verum
end;
suppose min (a,b) = b ; ::_thesis: max (a,b) >= min (a,b)
hence  max (a,b) >= min (a,b) by XXREAL_0:25; ::_thesis: verum
end;
end;
end;

theorem Th2: :: RFUNCT_4:2
for n being Element of NAT
for R1, R2 being Element of n -tuples_on REAL
for r1, r2 being Real holds mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>)) = (mlt (R1,R2)) ^ <*(r1 * r2)*>
proof
let n be Element of NAT ; ::_thesis: for R1, R2 being Element of n -tuples_on REAL
for r1, r2 being Real holds mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>)) = (mlt (R1,R2)) ^ <*(r1 * r2)*>
let R1, R2 be Element of n -tuples_on REAL; ::_thesis: for r1, r2 being Real holds mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>)) = (mlt (R1,R2)) ^ <*(r1 * r2)*>
let r1, r2 be Real; ::_thesis: mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>)) = (mlt (R1,R2)) ^ <*(r1 * r2)*>
len (R1 ^ <*r1*>) = (len R1) + 1 by FINSEQ_2:16
.= n + 1 by CARD_1:def_7
.= (len R2) + 1 by CARD_1:def_7
.= len (R2 ^ <*r2*>) by FINSEQ_2:16 ;
then A1: len (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) = len (R1 ^ <*r1*>) by FINSEQ_2:72
.= (len R1) + 1 by FINSEQ_2:16
.= n + 1 by CARD_1:def_7 ;
A2: for k being Nat st k in Seg (n + 1) holds
(mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k
proof
let k be Nat; ::_thesis: ( k in Seg (n + 1) implies (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k )
assume A3: k in Seg (n + 1) ; ::_thesis: (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k
A4: k <= n + 1 by A3, FINSEQ_1:1;
now__::_thesis:_(mlt_((R1_^_<*r1*>),(R2_^_<*r2*>)))_._k_=_((mlt_(R1,R2))_^_<*(r1_*_r2)*>)_._k
percases ( k < n + 1 or k = n + 1 ) by A4, XXREAL_0:1;
suppose k < n + 1 ; ::_thesis: (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k
then A5: k <= n by NAT_1:13;
 1 <= k by A3, FINSEQ_1:1;
then A6: k in Seg n by A5, FINSEQ_1:1;
then  k in Seg (len R1) by CARD_1:def_7;
then  k in dom R1 by FINSEQ_1:def_3;
then A7: (R1 ^ <*r1*>) . k = R1 . k by FINSEQ_1:def_7;
 k in Seg (len R2) by A6, CARD_1:def_7;
then  k in dom R2 by FINSEQ_1:def_3;
then  (R2 ^ <*r2*>) . k = R2 . k by FINSEQ_1:def_7;
then A8: (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = (R1 . k) * (R2 . k) by A7, RVSUM_1:59;
 len (mlt (R1,R2)) = n by CARD_1:def_7;
then  k in dom (mlt (R1,R2)) by A6, FINSEQ_1:def_3;
then  ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k = (mlt (R1,R2)) . k by FINSEQ_1:def_7;
hence  (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k by A8, RVSUM_1:59; ::_thesis: verum
end;
supposeA9: k = n + 1 ; ::_thesis: (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k
then  k = (len R1) + 1 by CARD_1:def_7;
then A10: (R1 ^ <*r1*>) . k = r1 by FINSEQ_1:42;
A11: n + 1 = (len (mlt (R1,R2))) + 1 by CARD_1:def_7;
 k = (len R2) + 1 by A9, CARD_1:def_7;
then  (R2 ^ <*r2*>) . k = r2 by FINSEQ_1:42;
then  (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = r1 * r2 by A10, RVSUM_1:59;
hence  (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k by A9, A11, FINSEQ_1:42; ::_thesis: verum
end;
end;
end;
hence  (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k ; ::_thesis: verum
end;
 mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>)) is Element of (n + 1) -tuples_on REAL by A1, FINSEQ_2:92;
hence  mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>)) = (mlt (R1,R2)) ^ <*(r1 * r2)*> by A2, FINSEQ_2:119; ::_thesis: verum
end;

theorem Th3: :: RFUNCT_4:3
for n being Element of NAT
for R being Element of n -tuples_on REAL st Sum R = 0 & ( for i being Element of NAT st i in dom R holds
0 <= R . i ) holds
for i being Element of NAT st i in dom R holds
R . i = 0
proof
let n be Element of NAT ; ::_thesis: for R being Element of n -tuples_on REAL st Sum R = 0 & ( for i being Element of NAT st i in dom R holds
0 <= R . i ) holds
for i being Element of NAT st i in dom R holds
R . i = 0
let R be Element of n -tuples_on REAL; ::_thesis: ( Sum R = 0 & ( for i being Element of NAT st i in dom R holds
0 <= R . i ) implies for i being Element of NAT st i in dom R holds
R . i = 0 )
assume that
A1: Sum R = 0 and
A2: for i being Element of NAT st i in dom R holds
0 <= R . i ; ::_thesis: for i being Element of NAT st i in dom R holds
R . i = 0
A3: for i being Nat st i in dom R holds
0 <= R . i by A2;
given k being Element of NAT  such that A4: k in dom R and
A5: R . k <> 0 ; ::_thesis: contradiction
 0 <= R . k by A2, A4;
hence  contradiction by A1, A3, A4, A5, RVSUM_1:85; ::_thesis: verum
end;

theorem Th4: :: RFUNCT_4:4
for n being Element of NAT
for R being Element of n -tuples_on REAL st ( for i being Element of NAT st i in dom R holds
0 = R . i ) holds
R = n |-> 0
proof
let n be Element of NAT ; ::_thesis: for R being Element of n -tuples_on REAL st ( for i being Element of NAT st i in dom R holds
0 = R . i ) holds
R = n |-> 0
let R be Element of n -tuples_on REAL; ::_thesis: ( ( for i being Element of NAT st i in dom R holds
0 = R . i ) implies R = n |-> 0 )
assume A1: for i being Element of NAT st i in dom R holds
0 = R . i ; ::_thesis: R = n |-> 0
A2: for k being Nat st 1 <= k & k <= len R holds
R . k = (n |-> 0) . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= len R implies R . k = (n |-> 0) . k )
assume  ( 1 <= k & k <= len R ) ; ::_thesis: R . k = (n |-> 0) . k
then A3: k in Seg (len R) by FINSEQ_1:1;
then  k in dom R by FINSEQ_1:def_3;
then A4: R . k = 0 by A1;
 k in Seg n by A3, CARD_1:def_7;
hence  R . k = (n |-> 0) . k by A4, FUNCOP_1:7; ::_thesis: verum
end;
len R = n by CARD_1:def_7
.= len (n |-> 0) by CARD_1:def_7 ;
hence  R = n |-> 0 by A2, FINSEQ_1:14; ::_thesis: verum
end;

theorem Th5: :: RFUNCT_4:5
for n being Element of NAT
for R being Element of n -tuples_on REAL holds mlt ((n |-> 0),R) = n |-> 0
proof
let n be Element of NAT ; ::_thesis: for R being Element of n -tuples_on REAL holds mlt ((n |-> 0),R) = n |-> 0
let R be Element of n -tuples_on REAL; ::_thesis: mlt ((n |-> 0),R) = n |-> 0
A1: len (mlt ((n |-> 0),R)) = n by CARD_1:def_7;
A2: for k being Nat st 1 <= k & k <= len (mlt ((n |-> 0),R)) holds
(mlt ((n |-> 0),R)) . k = (n |-> 0) . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= len (mlt ((n |-> 0),R)) implies (mlt ((n |-> 0),R)) . k = (n |-> 0) . k )
assume  ( 1 <= k & k <= len (mlt ((n |-> 0),R)) ) ; ::_thesis: (mlt ((n |-> 0),R)) . k = (n |-> 0) . k
then A3: k in Seg (len (mlt ((n |-> 0),R))) by FINSEQ_1:1;
(mlt ((n |-> 0),R)) . k = ((n |-> 0) . k) * (R . k) by RVSUM_1:60
.= 0 * (R . k) by A1, A3, FUNCOP_1:7 ;
hence  (mlt ((n |-> 0),R)) . k = (n |-> 0) . k by A1, A3, FUNCOP_1:7; ::_thesis: verum
end;
 len (n |-> 0) = n by CARD_1:def_7;
hence  mlt ((n |-> 0),R) = n |-> 0 by A1, A2, FINSEQ_1:14; ::_thesis: verum
end;

begin

definition
let f be PartFunc of REAL,REAL;
let X be set ;
predf is_strictly_convex_on X means :Def1: :: RFUNCT_4:def 1
( 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)) ) );
end;

:: deftheorem Def1 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)) ) ) );

theorem :: RFUNCT_4:6
for f being PartFunc of REAL,REAL
for X being set st f is_strictly_convex_on X holds
f is_convex_on X
proof
let f be PartFunc of REAL,REAL; ::_thesis: for X being set st f is_strictly_convex_on X holds
f is_convex_on X
let X be set ; ::_thesis: ( f is_strictly_convex_on X implies f is_convex_on X )
assume A1: f is_strictly_convex_on X ; ::_thesis: f is_convex_on X
A2: 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))
proof
let p be Real; ::_thesis: ( 0 <= p & p <= 1 implies 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)) )
assume A3: ( 0 <= p & p <= 1 ) ; ::_thesis: 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))
 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))
proof
let r, s be Real; ::_thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X implies f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) )
assume A4: ( r in X & s in X & (p * r) + ((1 - p) * s) in X ) ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))
now__::_thesis:_f_._((p_*_r)_+_((1_-_p)_*_s))_<=_(p_*_(f_._r))_+_((1_-_p)_*_(f_._s))
percases ( p = 0 or p = 1 or ( 0 < p & p < 1 ) ) by A3, XXREAL_0:1;
suppose p = 0 ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))
hence  f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum
end;
suppose p = 1 ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))
hence  f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum
end;
supposeA5: ( 0 < p & p < 1 ) ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))
now__::_thesis:_f_._((p_*_r)_+_((1_-_p)_*_s))_<=_(p_*_(f_._r))_+_((1_-_p)_*_(f_._s))
percases ( r = s or r <> s ) ;
suppose r = s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))
hence  f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum
end;
suppose r <> s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))
hence  f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) by A1, A4, A5, Def1; ::_thesis: verum
end;
end;
end;
hence  f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum
end;
end;
end;
hence  f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum
end;
hence  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)) ; ::_thesis: verum
end;
 X c= dom f by A1, Def1;
hence  f is_convex_on X by A2, RFUNCT_3:def_12; ::_thesis: verum
end;

theorem :: RFUNCT_4:7
for a, b being Real
for f being PartFunc of REAL,REAL holds
( f is_strictly_convex_on [.a,b.] iff ( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds
for r, s being Real st r in [.a,b.] & s in [.a,b.] & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ) ) )
proof
let a, b be Real; ::_thesis: for f being PartFunc of REAL,REAL holds
( f is_strictly_convex_on [.a,b.] iff ( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds
for r, s being Real st r in [.a,b.] & s in [.a,b.] & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ) ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( f is_strictly_convex_on [.a,b.] iff ( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds
for r, s being Real st r in [.a,b.] & s in [.a,b.] & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ) ) )
set ab =  {  r where r is Real : ( a <= r & r <= b )  }  ;
A1: [.a,b.] =  {  r where r is Real : ( a <= r & r <= b )  }  by RCOMP_1:def_1;
thus  ( f is_strictly_convex_on [.a,b.] implies ( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds
for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds
f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) ) ) ) ::_thesis: ( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds
for r, s being Real st r in [.a,b.] & s in [.a,b.] & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ) implies f is_strictly_convex_on [.a,b.] )
proof
assume A2: f is_strictly_convex_on [.a,b.] ; ::_thesis: ( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds
for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds
f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) ) )
hence  [.a,b.] c= dom f by Def1; ::_thesis: for p being Real st 0 < p & p < 1 holds
for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds
f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y))
let p be Real; ::_thesis: ( 0 < p & p < 1 implies for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds
f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) )
assume that
A3: 0 < p and
A4: p < 1 ; ::_thesis: for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds
f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y))
A5: 0 <= 1 - p by A4, XREAL_1:48;
A6: (p * b) + ((1 - p) * b) = b ;
A7: (p * a) + ((1 - p) * a) = a ;
let x, y be Real; ::_thesis: ( x in [.a,b.] & y in [.a,b.] & x <> y implies f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) )
assume that
A8: x in [.a,b.] and
A9: y in [.a,b.] and
A10: x <> y ; ::_thesis: f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y))
A11: ex r2 being Real st
( r2 = y & a <= r2 & r2 <= b ) by A1, A9;
then A12: (1 - p) * y <= (1 - p) * b by A5, XREAL_1:64;
A13: ex r1 being Real st
( r1 = x & a <= r1 & r1 <= b ) by A1, A8;
then  p * x <= p * b by A3, XREAL_1:64;
then A14: (p * x) + ((1 - p) * y) <= b by A12, A6, XREAL_1:7;
A15: (1 - p) * a <= (1 - p) * y by A5, A11, XREAL_1:64;
 p * a <= p * x by A3, A13, XREAL_1:64;
then  a <= (p * x) + ((1 - p) * y) by A15, A7, XREAL_1:7;
then  (p * x) + ((1 - p) * y) in  {  r where r is Real : ( a <= r & r <= b )  }  by A14;
hence  f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) by A1, A2, A3, A4, A8, A9, A10, Def1; ::_thesis: verum
end;
assume that
A16: [.a,b.] c= dom f and
A17: for p being Real st 0 < p & p < 1 holds
for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds
f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) ; ::_thesis: f is_strictly_convex_on [.a,b.]
thus  [.a,b.] c= dom f by A16; :: according to RFUNCT_4:def_1 ::_thesis: for p being Real st 0 < p & p < 1 holds
for r, s being Real st r in [.a,b.] & s in [.a,b.] & (p * r) + ((1 - p) * s) in [.a,b.] & r <> s 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 [.a,b.] & s in [.a,b.] & (p * r) + ((1 - p) * s) in [.a,b.] & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) )
assume A18: ( 0 < p & p < 1 ) ; ::_thesis: for r, s being Real st r in [.a,b.] & s in [.a,b.] & (p * r) + ((1 - p) * s) in [.a,b.] & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s))
let x, y be Real; ::_thesis: ( x in [.a,b.] & y in [.a,b.] & (p * x) + ((1 - p) * y) in [.a,b.] & x <> y implies f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) )
assume that
A19: ( x in [.a,b.] & y in [.a,b.] ) and
 (p * x) + ((1 - p) * y) in [.a,b.] ; ::_thesis: ( not x <> y or f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) )
thus  ( not x <> y or f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) ) by A17, A18, A19; ::_thesis: verum
end;

theorem :: RFUNCT_4:8
for X being set
for f being PartFunc of REAL,REAL holds
( f is_convex_on X iff ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds
f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) )
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL holds
( f is_convex_on X iff ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds
f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( f is_convex_on X iff ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds
f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) )
A1: ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds
f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) implies f is_convex_on X )
proof
assume that
A2: X c= dom f and
A3: for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds
f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ; ::_thesis: f is_convex_on X
 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))
proof
let p be Real; ::_thesis: ( 0 <= p & p <= 1 implies 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)) )
assume A4: ( 0 <= p & p <= 1 ) ; ::_thesis: 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))
 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))
proof
let r, s be Real; ::_thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X implies f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) )
assume A5: ( r in X & s in X & (p * r) + ((1 - p) * s) in X ) ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))
 f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))
proof
percases ( p = 0 or p = 1 or ( 0 < p & p < 1 ) ) by A4, XXREAL_0:1;
suppose p = 0 ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))
hence  f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum
end;
suppose p = 1 ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))
hence  f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum
end;
supposeA6: ( 0 < p & p < 1 ) ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))
then A7: 0 < 1 - p by XREAL_1:50;
percases ( r = s or r > s or r < s ) by XXREAL_0:1;
suppose r = s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))
hence  f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum
end;
supposeA8: r > s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))
set t = (p * r) + ((1 - p) * s);
A9: r - s > 0 by A8, XREAL_1:50;
A10: r - ((p * r) + ((1 - p) * s)) = (1 - p) * (r - s) ;
then  r - ((p * r) + ((1 - p) * s)) > 0 by A7, A9, XREAL_1:129;
then A11: (p * r) + ((1 - p) * s) < r by XREAL_1:47;
A12: ((p * r) + ((1 - p) * s)) - s = p * (r - s) ;
then A13: (((p * r) + ((1 - p) * s)) - s) / (r - s) = p by A9, XCMPLX_1:89;
 ((p * r) + ((1 - p) * s)) - s > 0 by A6, A9, A12, XREAL_1:129;
then A14: s < (p * r) + ((1 - p) * s) by XREAL_1:47;
 (r - ((p * r) + ((1 - p) * s))) / (r - s) = 1 - p by A9, A10, XCMPLX_1:89;
hence  f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) by A3, A5, A14, A11, A13; ::_thesis: verum
end;
supposeA15: r < s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))
set t = (p * r) + ((1 - p) * s);
A16: s - r > 0 by A15, XREAL_1:50;
A17: s - ((p * r) + ((1 - p) * s)) = p * (s - r) ;
then  s - ((p * r) + ((1 - p) * s)) > 0 by A6, A16, XREAL_1:129;
then A18: (p * r) + ((1 - p) * s) < s by XREAL_1:47;
A19: ((p * r) + ((1 - p) * s)) - r = (1 - p) * (s - r) ;
then A20: (((p * r) + ((1 - p) * s)) - r) / (s - r) = 1 - p by A16, XCMPLX_1:89;
 ((p * r) + ((1 - p) * s)) - r > 0 by A7, A16, A19, XREAL_1:129;
then A21: r < (p * r) + ((1 - p) * s) by XREAL_1:47;
 (s - ((p * r) + ((1 - p) * s))) / (s - r) = p by A16, A17, XCMPLX_1:89;
hence  f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) by A3, A5, A21, A18, A20; ::_thesis: verum
end;
end;
end;
end;
end;
hence  f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum
end;
hence  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)) ; ::_thesis: verum
end;
hence  f is_convex_on X by A2, RFUNCT_3:def_12; ::_thesis: verum
end;
 ( f is_convex_on X implies ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds
f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) )
proof
assume A22: f is_convex_on X ; ::_thesis: ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds
f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) )
 for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds
f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c))
proof
let a, b, c be Real; ::_thesis: ( a in X & b in X & c in X & a < b & b < c implies f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) )
assume that
A23: ( a in X & b in X & c in X ) and
A24: ( a < b & b < c ) ; ::_thesis: f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c))
set p = (c - b) / (c - a);
A25: ( c - b < c - a & 0 < c - b ) by A24, XREAL_1:10, XREAL_1:50;
then A26: (c - b) / (c - a) < 1 by XREAL_1:189;
A27: ((c - b) / (c - a)) + ((b - a) / (c - a)) = ((c - b) + (b - a)) / (c - a) by XCMPLX_1:62
.= 1 by A25, XCMPLX_1:60 ;
then (((c - b) / (c - a)) * a) + ((1 - ((c - b) / (c - a))) * c) = ((a * (c - b)) / (c - a)) + (c * ((b - a) / (c - a))) by XCMPLX_1:74
.= ((a * (c - b)) / (c - a)) + ((c * (b - a)) / (c - a)) by XCMPLX_1:74
.= (((c * a) - (b * a)) + ((b - a) * c)) / (c - a) by XCMPLX_1:62
.= (b * (c - a)) / (c - a) ;
then  (((c - b) / (c - a)) * a) + ((1 - ((c - b) / (c - a))) * c) = b by A25, XCMPLX_1:89;
hence  f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) by A22, A23, A25, A26, A27, RFUNCT_3:def_12; ::_thesis: verum
end;
hence  ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds
f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) by A22, RFUNCT_3:def_12; ::_thesis: verum
end;
hence  ( f is_convex_on X iff ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds
f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) ) by A1; ::_thesis: verum
end;

theorem :: RFUNCT_4:9
for X being set
for f being PartFunc of REAL,REAL holds
( f is_strictly_convex_on X iff ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds
f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) )
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL holds
( f is_strictly_convex_on X iff ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds
f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( f is_strictly_convex_on X iff ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds
f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) )
A1: ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds
f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) implies f is_strictly_convex_on X )
proof
assume that
A2: X c= dom f and
A3: for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds
f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ; ::_thesis: f is_strictly_convex_on X
 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))
proof
let p be Real; ::_thesis: ( 0 < p & p < 1 implies 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)) )
assume A4: ( 0 < p & p < 1 ) ; ::_thesis: 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))
 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))
proof
let r, s be Real; ::_thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s implies f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) )
assume that
A5: ( r in X & s in X & (p * r) + ((1 - p) * s) in X ) and
A6: r <> s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s))
 f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s))
proof
now__::_thesis:_f_._((p_*_r)_+_((1_-_p)_*_s))_<_(p_*_(f_._r))_+_((1_-_p)_*_(f_._s))
percases ( 0 < p & p < 1 ) by A4;
supposeA7: ( 0 < p & p < 1 ) ; ::_thesis: f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s))
then A8: 0 < 1 - p by XREAL_1:50;
now__::_thesis:_f_._((p_*_r)_+_((1_-_p)_*_s))_<_(p_*_(f_._r))_+_((1_-_p)_*_(f_._s))
percases ( r > s or r < s ) by A6, XXREAL_0:1;
supposeA9: r > s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s))
set t = (p * r) + ((1 - p) * s);
A10: r - s > 0 by A9, XREAL_1:50;
A11: r - ((p * r) + ((1 - p) * s)) = (1 - p) * (r - s) ;
then  r - ((p * r) + ((1 - p) * s)) > 0 by A8, A10, XREAL_1:129;
then A12: (p * r) + ((1 - p) * s) < r by XREAL_1:47;
A13: ((p * r) + ((1 - p) * s)) - s = p * (r - s) ;
then A14: (((p * r) + ((1 - p) * s)) - s) / (r - s) = p by A10, XCMPLX_1:89;
 ((p * r) + ((1 - p) * s)) - s > 0 by A7, A10, A13, XREAL_1:129;
then A15: s < (p * r) + ((1 - p) * s) by XREAL_1:47;
 (r - ((p * r) + ((1 - p) * s))) / (r - s) = 1 - p by A10, A11, XCMPLX_1:89;
hence  f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) by A3, A5, A15, A12, A14; ::_thesis: verum
end;
supposeA16: r < s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s))
set t = (p * r) + ((1 - p) * s);
A17: s - r > 0 by A16, XREAL_1:50;
A18: s - ((p * r) + ((1 - p) * s)) = p * (s - r) ;
then  s - ((p * r) + ((1 - p) * s)) > 0 by A7, A17, XREAL_1:129;
then A19: (p * r) + ((1 - p) * s) < s by XREAL_1:47;
A20: ((p * r) + ((1 - p) * s)) - r = (1 - p) * (s - r) ;
then A21: (((p * r) + ((1 - p) * s)) - r) / (s - r) = 1 - p by A17, XCMPLX_1:89;
 ((p * r) + ((1 - p) * s)) - r > 0 by A8, A17, A20, XREAL_1:129;
then A22: r < (p * r) + ((1 - p) * s) by XREAL_1:47;
 (s - ((p * r) + ((1 - p) * s))) / (s - r) = p by A17, A18, XCMPLX_1:89;
hence  f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) by A3, A5, A22, A19, A21; ::_thesis: verum
end;
end;
end;
hence  f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum
end;
end;
end;
hence  f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum
end;
hence  f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum
end;
hence  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)) ; ::_thesis: verum
end;
hence  f is_strictly_convex_on X by A2, Def1; ::_thesis: verum
end;
 ( f is_strictly_convex_on X implies ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds
f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) )
proof
assume A23: f is_strictly_convex_on X ; ::_thesis: ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds
f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) )
 for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds
f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c))
proof
let a, b, c be Real; ::_thesis: ( a in X & b in X & c in X & a < b & b < c implies f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) )
assume that
A24: ( a in X & b in X & c in X ) and
A25: ( a < b & b < c ) ; ::_thesis: f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c))
set p = (c - b) / (c - a);
A26: ( c - b < c - a & 0 < c - b ) by A25, XREAL_1:10, XREAL_1:50;
then A27: ( 0 < (c - b) / (c - a) & (c - b) / (c - a) < 1 ) by XREAL_1:139, XREAL_1:189;
A28: ((c - b) / (c - a)) + ((b - a) / (c - a)) = ((c - b) + (b - a)) / (c - a) by XCMPLX_1:62
.= 1 by A26, XCMPLX_1:60 ;
then (((c - b) / (c - a)) * a) + ((1 - ((c - b) / (c - a))) * c) = ((a * (c - b)) / (c - a)) + (c * ((b - a) / (c - a))) by XCMPLX_1:74
.= ((a * (c - b)) / (c - a)) + ((c * (b - a)) / (c - a)) by XCMPLX_1:74
.= (((c * a) - (b * a)) + ((b - a) * c)) / (c - a) by XCMPLX_1:62
.= (b * (c - a)) / (c - a) ;
then  (((c - b) / (c - a)) * a) + ((1 - ((c - b) / (c - a))) * c) = b by A26, XCMPLX_1:89;
hence  f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) by A23, A24, A25, A27, A28, Def1; ::_thesis: verum
end;
hence  ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds
f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) by A23, Def1; ::_thesis: verum
end;
hence  ( f is_strictly_convex_on X iff ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds
f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) ) by A1; ::_thesis: verum
end;

theorem :: RFUNCT_4:10
for f being PartFunc of REAL,REAL
for X, Y being set st f is_strictly_convex_on X & Y c= X holds
f is_strictly_convex_on Y
proof
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
end;

Lm1:  for r being Real
for f being PartFunc of REAL,REAL
for X being set st f is_strictly_convex_on X holds
f - r is_strictly_convex_on X
proof
let r be Real; ::_thesis: for f being PartFunc of REAL,REAL
for X being set st f is_strictly_convex_on X holds
f - r is_strictly_convex_on X
let f be PartFunc of REAL,REAL; ::_thesis: for X being set st f is_strictly_convex_on X holds
f - r is_strictly_convex_on X
let X be set ; ::_thesis: ( f is_strictly_convex_on X implies f - r is_strictly_convex_on X )
assume A1: f is_strictly_convex_on X ; ::_thesis: f - r is_strictly_convex_on X
then A2: X c= dom f by Def1;
A3: for p being Real st 0 < p & p < 1 holds
for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds
(f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s))
proof
let p be Real; ::_thesis: ( 0 < p & p < 1 implies for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds
(f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s)) )
assume A4: ( 0 < p & p < 1 ) ; ::_thesis: for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds
(f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s))
 for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds
(f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s))
proof
let t, s be Real; ::_thesis: ( t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s implies (f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s)) )
assume that
A5: ( t in X & s in X ) and
A6: (p * t) + ((1 - p) * s) in X and
A7: t <> s ; ::_thesis: (f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s))
 f . ((p * t) + ((1 - p) * s)) < (p * (f . t)) + ((1 - p) * (f . s)) by A1, A4, A5, A6, A7, Def1;
then A8: (f . ((p * t) + ((1 - p) * s))) - r < ((p * (f . t)) + ((1 - p) * (f . s))) - r by XREAL_1:9;
 ( (f - r) . t = (f . t) - r & (f - r) . s = (f . s) - r ) by A2, A5, VALUED_1:3;
hence  (f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s)) by A2, A6, A8, VALUED_1:3; ::_thesis: verum
end;
hence  for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds
(f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s)) ; ::_thesis: verum
end;
 dom f = dom (f - r) by VALUED_1:3;
hence  f - r is_strictly_convex_on X by A2, A3, Def1; ::_thesis: verum
end;

theorem :: RFUNCT_4:11
for r being Real
for f being PartFunc of REAL,REAL
for X being set holds
( f is_strictly_convex_on X iff f - r is_strictly_convex_on X )
proof
let r be Real; ::_thesis: for f being PartFunc of REAL,REAL
for X being set holds
( f is_strictly_convex_on X iff f - r is_strictly_convex_on X )
let f be PartFunc of REAL,REAL; ::_thesis: for X being set holds
( f is_strictly_convex_on X iff f - r is_strictly_convex_on X )
let X be set ; ::_thesis: ( f is_strictly_convex_on X iff f - r is_strictly_convex_on X )
A1: dom (f - r) = dom f by VALUED_1:3;
A2: for x being Element of REAL st x in dom (f - r) holds
((f - r) - (- r)) . x = f . x
proof
let x be Element of REAL ; ::_thesis: ( x in dom (f - r) implies ((f - r) - (- r)) . x = f . x )
assume A3: x in dom (f - r) ; ::_thesis: ((f - r) - (- r)) . x = f . x
then ((f - r) - (- r)) . x = ((f - r) . x) - (- r) by VALUED_1:3
.= ((f - r) . x) + r
.= ((f . x) - r) + r by A1, A3, VALUED_1:3
.= (f . x) - (r - r) ;
hence  ((f - r) - (- r)) . x = f . x ; ::_thesis: verum
end;
 dom ((f - r) - (- r)) = dom (f - r) by VALUED_1:3;
then  (f - r) - (- r) = f by A1, A2, PARTFUN1:5;
hence  ( f is_strictly_convex_on X iff f - r is_strictly_convex_on X ) by Lm1; ::_thesis: verum
end;

Lm2:  for r being Real
for f being PartFunc of REAL,REAL
for X being set st 0 < r & f is_strictly_convex_on X holds
r (#) f is_strictly_convex_on X
proof
let r be Real; ::_thesis: for f being PartFunc of REAL,REAL
for X being set st 0 < r & f is_strictly_convex_on X holds
r (#) f is_strictly_convex_on X
let f be PartFunc of REAL,REAL; ::_thesis: for X being set st 0 < r & f is_strictly_convex_on X holds
r (#) f is_strictly_convex_on X
let X be set ; ::_thesis: ( 0 < r & f is_strictly_convex_on X implies r (#) f is_strictly_convex_on X )
assume A1: 0 < r ; ::_thesis: ( not f is_strictly_convex_on X or r (#) f is_strictly_convex_on X )
assume A2: f is_strictly_convex_on X ; ::_thesis: r (#) f is_strictly_convex_on X
then  X c= dom f by Def1;
then A3: X c= dom (r (#) f) by VALUED_1:def_5;
 for p being Real st 0 < p & p < 1 holds
for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds
(r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s))
proof
let p be Real; ::_thesis: ( 0 < p & p < 1 implies for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds
(r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s)) )
assume A4: ( 0 < p & p < 1 ) ; ::_thesis: for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds
(r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s))
 for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds
(r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s))
proof
let t, s be Real; ::_thesis: ( t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s implies (r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s)) )
assume that
A5: ( t in X & s in X ) and
A6: (p * t) + ((1 - p) * s) in X and
A7: t <> s ; ::_thesis: (r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s))
 f . ((p * t) + ((1 - p) * s)) < (p * (f . t)) + ((1 - p) * (f . s)) by A2, A4, A5, A6, A7, Def1;
then A8: r * (f . ((p * t) + ((1 - p) * s))) < r * ((p * (f . t)) + ((1 - p) * (f . s))) by A1, XREAL_1:68;
 ( p * ((r (#) f) . t) = p * (r * (f . t)) & (1 - p) * ((r (#) f) . s) = (1 - p) * (r * (f . s)) ) by A3, A5, VALUED_1:def_5;
hence  (r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s)) by A3, A6, A8, VALUED_1:def_5; ::_thesis: verum
end;
hence  for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds
(r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s)) ; ::_thesis: verum
end;
hence  r (#) f is_strictly_convex_on X by A3, Def1; ::_thesis: verum
end;

theorem Th12: :: RFUNCT_4:12
for r being Real
for f being PartFunc of REAL,REAL
for X being set st 0 < r holds
( f is_strictly_convex_on X iff r (#) f is_strictly_convex_on X )
proof
let r be Real; ::_thesis: for f being PartFunc of REAL,REAL
for X being set st 0 < r holds
( f is_strictly_convex_on X iff r (#) f is_strictly_convex_on X )
let f be PartFunc of REAL,REAL; ::_thesis: for X being set st 0 < r holds
( f is_strictly_convex_on X iff r (#) f is_strictly_convex_on X )
let X be set ; ::_thesis: ( 0 < r implies ( f is_strictly_convex_on X iff r (#) f is_strictly_convex_on X ) )
A1: dom ((1 / r) (#) (r (#) f)) = dom (r (#) f) by VALUED_1:def_5;
assume A2: 0 < r ; ::_thesis: ( f is_strictly_convex_on X iff r (#) f is_strictly_convex_on X )
A3: for x being Element of REAL st x in dom (r (#) f) holds
((1 / r) (#) (r (#) f)) . x = f . x
proof
let x be Element of REAL ; ::_thesis: ( x in dom (r (#) f) implies ((1 / r) (#) (r (#) f)) . x = f . x )
assume A4: x in dom (r (#) f) ; ::_thesis: ((1 / r) (#) (r (#) f)) . x = f . x
then ((1 / r) (#) (r (#) f)) . x = (1 / r) * ((r (#) f) . x) by A1, VALUED_1:def_5
.= (1 / r) * (r * (f . x)) by A4, VALUED_1:def_5
.= ((1 / r) * r) * (f . x)
.= 1 * (f . x) by A2, XCMPLX_1:106 ;
hence  ((1 / r) (#) (r (#) f)) . x = f . x ; ::_thesis: verum
end;
 dom (r (#) f) = dom f by VALUED_1:def_5;
then  (1 / r) (#) (r (#) f) = f by A1, A3, PARTFUN1:5;
hence  ( f is_strictly_convex_on X iff r (#) f is_strictly_convex_on X ) by A2, Lm2, XREAL_1:139; ::_thesis: verum
end;

theorem Th13: :: RFUNCT_4:13
for f, g being PartFunc of REAL,REAL
for X being set st f is_strictly_convex_on X & g is_strictly_convex_on X holds
f + g is_strictly_convex_on X
proof
let f, g be PartFunc of REAL,REAL; ::_thesis: for X being set st f is_strictly_convex_on X & g is_strictly_convex_on X holds
f + g is_strictly_convex_on X
let X be set ; ::_thesis: ( f is_strictly_convex_on X & g is_strictly_convex_on X implies f + g is_strictly_convex_on X )
assume A1: ( f is_strictly_convex_on X & g is_strictly_convex_on X ) ; ::_thesis: f + g is_strictly_convex_on X
then  ( X c= dom f & X c= dom g ) by Def1;
then  X c= (dom f) /\ (dom g) by XBOOLE_1:19;
then A2: X c= dom (f + g) by VALUED_1:def_1;
 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 + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s))
proof
let p be Real; ::_thesis: ( 0 < p & p < 1 implies for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds
(f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) )
assume A3: ( 0 < p & p < 1 ) ; ::_thesis: for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds
(f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s))
 for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds
(f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s))
proof
let r, s be Real; ::_thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s implies (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) )
assume that
A4: r in X and
A5: s in X and
A6: (p * r) + ((1 - p) * s) in X and
A7: r <> s ; ::_thesis: (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s))
A8: ( (f + g) . ((p * r) + ((1 - p) * s)) = (f . ((p * r) + ((1 - p) * s))) + (g . ((p * r) + ((1 - p) * s))) & (f + g) . r = (f . r) + (g . r) ) by A2, A4, A6, VALUED_1:def_1;
A9: ( ((p * (f . r)) + ((1 - p) * (f . s))) + ((p * (g . r)) + ((1 - p) * (g . s))) = (p * ((f . r) + (g . r))) + ((1 - p) * ((f . s) + (g . s))) & (f + g) . s = (f . s) + (g . s) ) by A2, A5, VALUED_1:def_1;
 ( f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) & g . ((p * r) + ((1 - p) * s)) < (p * (g . r)) + ((1 - p) * (g . s)) ) by A1, A3, A4, A5, A6, A7, Def1;
hence  (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) by A8, A9, XREAL_1:8; ::_thesis: verum
end;
hence  for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds
(f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) ; ::_thesis: verum
end;
hence  f + g is_strictly_convex_on X by A2, Def1; ::_thesis: verum
end;

theorem Th14: :: RFUNCT_4:14
for f, g being PartFunc of REAL,REAL
for X being set st f is_strictly_convex_on X & g is_convex_on X holds
f + g is_strictly_convex_on X
proof
let f, g be PartFunc of REAL,REAL; ::_thesis: for X being set st f is_strictly_convex_on X & g is_convex_on X holds
f + g is_strictly_convex_on X
let X be set ; ::_thesis: ( f is_strictly_convex_on X & g is_convex_on X implies f + g is_strictly_convex_on X )
assume A1: ( f is_strictly_convex_on X & g is_convex_on X ) ; ::_thesis: f + g is_strictly_convex_on X
then  ( X c= dom f & X c= dom g ) by Def1, RFUNCT_3:def_12;
then  X c= (dom f) /\ (dom g) by XBOOLE_1:19;
then A2: X c= dom (f + g) by VALUED_1:def_1;
 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 + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s))
proof
let p be Real; ::_thesis: ( 0 < p & p < 1 implies for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds
(f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) )
assume A3: ( 0 < p & p < 1 ) ; ::_thesis: for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds
(f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s))
 for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds
(f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s))
proof
let r, s be Real; ::_thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s implies (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) )
assume that
A4: r in X and
A5: s in X and
A6: (p * r) + ((1 - p) * s) in X and
A7: r <> s ; ::_thesis: (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s))
A8: ( (f + g) . ((p * r) + ((1 - p) * s)) = (f . ((p * r) + ((1 - p) * s))) + (g . ((p * r) + ((1 - p) * s))) & (f + g) . r = (f . r) + (g . r) ) by A2, A4, A6, VALUED_1:def_1;
A9: ( ((p * (f . r)) + ((1 - p) * (f . s))) + ((p * (g . r)) + ((1 - p) * (g . s))) = (p * ((f . r) + (g . r))) + ((1 - p) * ((f . s) + (g . s))) & (f + g) . s = (f . s) + (g . s) ) by A2, A5, VALUED_1:def_1;
 ( f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) & g . ((p * r) + ((1 - p) * s)) <= (p * (g . r)) + ((1 - p) * (g . s)) ) by A1, A3, A4, A5, A6, A7, Def1, RFUNCT_3:def_12;
hence  (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) by A8, A9, XREAL_1:8; ::_thesis: verum
end;
hence  for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds
(f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) ; ::_thesis: verum
end;
hence  f + g is_strictly_convex_on X by A2, Def1; ::_thesis: verum
end;

theorem :: RFUNCT_4:15
for a, b being Real
for f, g being PartFunc of REAL,REAL
for X being set st f is_strictly_convex_on X & g is_strictly_convex_on X & ( ( a > 0 & b >= 0 ) or ( a >= 0 & b > 0 ) ) holds
(a (#) f) + (b (#) g) is_strictly_convex_on X
proof
let a, b be Real; ::_thesis: for f, g being PartFunc of REAL,REAL
for X being set st f is_strictly_convex_on X & g is_strictly_convex_on X & ( ( a > 0 & b >= 0 ) or ( a >= 0 & b > 0 ) ) holds
(a (#) f) + (b (#) g) is_strictly_convex_on X
let f, g be PartFunc of REAL,REAL; ::_thesis: for X being set st f is_strictly_convex_on X & g is_strictly_convex_on X & ( ( a > 0 & b >= 0 ) or ( a >= 0 & b > 0 ) ) holds
(a (#) f) + (b (#) g) is_strictly_convex_on X
let X be set ; ::_thesis: ( f is_strictly_convex_on X & g is_strictly_convex_on X & ( ( a > 0 & b >= 0 ) or ( a >= 0 & b > 0 ) ) implies (a (#) f) + (b (#) g) is_strictly_convex_on X )
assume that
A1: f is_strictly_convex_on X and
A2: g is_strictly_convex_on X and
A3: ( ( a > 0 & b >= 0 ) or ( a >= 0 & b > 0 ) ) ; ::_thesis: (a (#) f) + (b (#) g) is_strictly_convex_on X
now__::_thesis:_(a_(#)_f)_+_(b_(#)_g)_is_strictly_convex_on_X
percases ( ( a > 0 & b > 0 ) or ( a > 0 & b = 0 ) or ( a = 0 & b > 0 ) ) by A3;
suppose ( a > 0 & b > 0 ) ; ::_thesis: (a (#) f) + (b (#) g) is_strictly_convex_on X
then  ( a (#) f is_strictly_convex_on X & b (#) g is_strictly_convex_on X ) by A1, A2, Th12;
hence  (a (#) f) + (b (#) g) is_strictly_convex_on X by Th13; ::_thesis: verum
end;
supposeA4: ( a > 0 & b = 0 ) ; ::_thesis: (a (#) f) + (b (#) g) is_strictly_convex_on X
A5: X c= dom g by A2, Def1;
 a (#) f is_strictly_convex_on X by A1, A4, Th12;
hence  (a (#) f) + (b (#) g) is_strictly_convex_on X by A4, A5, Th14, RFUNCT_3:57; ::_thesis: verum
end;
supposeA6: ( a = 0 & b > 0 ) ; ::_thesis: (a (#) f) + (b (#) g) is_strictly_convex_on X
A7: X c= dom f by A1, Def1;
 b (#) g is_strictly_convex_on X by A2, A6, Th12;
hence  (a (#) f) + (b (#) g) is_strictly_convex_on X by A6, A7, Th14, RFUNCT_3:57; ::_thesis: verum
end;
end;
end;
hence  (a (#) f) + (b (#) g) is_strictly_convex_on X ; ::_thesis: verum
end;

theorem Th16: :: RFUNCT_4:16
for f being PartFunc of REAL,REAL
for X being set holds
( f is_convex_on X iff ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) ) )
proof
let f be PartFunc of REAL,REAL; ::_thesis: for X being set holds
( f is_convex_on X iff ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) ) )
let X be set ; ::_thesis: ( f is_convex_on X iff ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) ) )
A1: ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) implies f is_convex_on X )
proof
assume that
A2: X c= dom f and
A3: for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ; ::_thesis: f is_convex_on X
 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))
proof
let p be Real; ::_thesis: ( 0 <= p & p <= 1 implies 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)) )
assume A4: ( 0 <= p & p <= 1 ) ; ::_thesis: 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))
 for s, t being Real st s in X & t in X & (p * s) + ((1 - p) * t) in X holds
f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t))
proof
let s, t be Real; ::_thesis: ( s in X & t in X & (p * s) + ((1 - p) * t) in X implies f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) )
assume A5: ( s in X & t in X & (p * s) + ((1 - p) * t) in X ) ; ::_thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t))
now__::_thesis:_f_._((p_*_s)_+_((1_-_p)_*_t))_<=_(p_*_(f_._s))_+_((1_-_p)_*_(f_._t))
percases ( p = 0 or p = 1 or ( 0 < p & p < 1 ) ) by A4, XXREAL_0:1;
suppose p = 0 ; ::_thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t))
hence  f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) ; ::_thesis: verum
end;
suppose p = 1 ; ::_thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t))
hence  f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) ; ::_thesis: verum
end;
supposeA6: ( 0 < p & p < 1 ) ; ::_thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t))
then A7: 1 - p > 0 by XREAL_1:50;
now__::_thesis:_f_._((p_*_s)_+_((1_-_p)_*_t))_<=_(p_*_(f_._s))_+_((1_-_p)_*_(f_._t))
percases ( s = t or s < t or s > t ) by XXREAL_0:1;
suppose s = t ; ::_thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t))
hence  f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) ; ::_thesis: verum
end;
suppose s < t ; ::_thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t))
then A8: t - s > 0 by XREAL_1:50;
 ((p * s) + ((1 - p) * t)) - s = (1 - p) * (t - s) ;
then A9: ((p * s) + ((1 - p) * t)) - s > 0 by A7, A8, XREAL_1:129;
then A10: (p * s) + ((1 - p) * t) > s by XREAL_1:47;
A11: ( (((f . ((p * s) + ((1 - p) * t))) - (f . s)) * (t - s)) * p = (p * ((t - s) * (f . ((p * s) + ((1 - p) * t))))) - (p * ((t - s) * (f . s))) & (((f . t) - (f . ((p * s) + ((1 - p) * t)))) * (t - s)) * (1 - p) = ((1 - p) * ((t - s) * (f . t))) - ((1 - p) * ((t - s) * (f . ((p * s) + ((1 - p) * t))))) ) ;
 t - ((p * s) + ((1 - p) * t)) = p * (t - s) ;
then A12: t - ((p * s) + ((1 - p) * t)) > 0 by A6, A8, XREAL_1:129;
then  (p * s) + ((1 - p) * t) < t by XREAL_1:47;
then  ( ((f . ((p * s) + ((1 - p) * t))) - (f . s)) / (((p * s) + ((1 - p) * t)) - s) <= ((f . t) - (f . s)) / (t - s) & ((f . t) - (f . s)) / (t - s) <= ((f . t) - (f . ((p * s) + ((1 - p) * t)))) / (t - ((p * s) + ((1 - p) * t))) ) by A3, A5, A10;
then  ((f . ((p * s) + ((1 - p) * t))) - (f . s)) / (((p * s) + ((1 - p) * t)) - s) <= ((f . t) - (f . ((p * s) + ((1 - p) * t)))) / (t - ((p * s) + ((1 - p) * t))) by XXREAL_0:2;
then  ((f . ((p * s) + ((1 - p) * t))) - (f . s)) * (t - ((p * s) + ((1 - p) * t))) <= ((f . t) - (f . ((p * s) + ((1 - p) * t)))) * (((p * s) + ((1 - p) * t)) - s) by A12, A9, XREAL_1:106;
then  (p * ((t - s) * (f . ((p * s) + ((1 - p) * t))))) + ((1 - p) * ((t - s) * (f . ((p * s) + ((1 - p) * t))))) <= ((1 - p) * ((t - s) * (f . t))) + (p * ((t - s) * (f . s))) by A11, XREAL_1:21;
then  f . ((p * s) + ((1 - p) * t)) <= ((((1 - p) * (f . t)) * (t - s)) + ((p * (f . s)) * (t - s))) / (t - s) by A8, XREAL_1:77;
then  f . ((p * s) + ((1 - p) * t)) <= ((((1 - p) * (f . t)) * (t - s)) / (t - s)) + (((p * (f . s)) * (t - s)) / (t - s)) by XCMPLX_1:62;
then  f . ((p * s) + ((1 - p) * t)) <= ((1 - p) * (f . t)) + (((p * (f . s)) * (t - s)) / (t - s)) by A8, XCMPLX_1:89;
hence  f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) by A8, XCMPLX_1:89; ::_thesis: verum
end;
suppose s > t ; ::_thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t))
then A13: s - t > 0 by XREAL_1:50;
 ((p * s) + ((1 - p) * t)) - t = p * (s - t) ;
then A14: ((p * s) + ((1 - p) * t)) - t > 0 by A6, A13, XREAL_1:129;
then A15: (p * s) + ((1 - p) * t) > t by XREAL_1:47;
A16: ( (((f . ((p * s) + ((1 - p) * t))) - (f . t)) * (s - t)) * (1 - p) = ((1 - p) * ((s - t) * (f . ((p * s) + ((1 - p) * t))))) - ((1 - p) * ((s - t) * (f . t))) & (((f . s) - (f . ((p * s) + ((1 - p) * t)))) * (s - t)) * p = (p * ((s - t) * (f . s))) - (p * ((s - t) * (f . ((p * s) + ((1 - p) * t))))) ) ;
 s - ((p * s) + ((1 - p) * t)) = (1 - p) * (s - t) ;
then A17: s - ((p * s) + ((1 - p) * t)) > 0 by A7, A13, XREAL_1:129;
then  (p * s) + ((1 - p) * t) < s by XREAL_1:47;
then  ( ((f . ((p * s) + ((1 - p) * t))) - (f . t)) / (((p * s) + ((1 - p) * t)) - t) <= ((f . s) - (f . t)) / (s - t) & ((f . s) - (f . t)) / (s - t) <= ((f . s) - (f . ((p * s) + ((1 - p) * t)))) / (s - ((p * s) + ((1 - p) * t))) ) by A3, A5, A15;
then  ((f . ((p * s) + ((1 - p) * t))) - (f . t)) / (((p * s) + ((1 - p) * t)) - t) <= ((f . s) - (f . ((p * s) + ((1 - p) * t)))) / (s - ((p * s) + ((1 - p) * t))) by XXREAL_0:2;
then  ((f . ((p * s) + ((1 - p) * t))) - (f . t)) * (s - ((p * s) + ((1 - p) * t))) <= ((f . s) - (f . ((p * s) + ((1 - p) * t)))) * (((p * s) + ((1 - p) * t)) - t) by A17, A14, XREAL_1:106;
then  ((1 - p) * ((s - t) * (f . ((p * s) + ((1 - p) * t))))) + (p * ((s - t) * (f . ((p * s) + ((1 - p) * t))))) <= (p * ((s - t) * (f . s))) + ((1 - p) * ((s - t) * (f . t))) by A16, XREAL_1:21;
then  f . ((p * s) + ((1 - p) * t)) <= (((p * (f . s)) * (s - t)) + (((1 - p) * (f . t)) * (s - t))) / (s - t) by A13, XREAL_1:77;
then  f . ((p * s) + ((1 - p) * t)) <= (((p * (f . s)) * (s - t)) / (s - t)) + ((((1 - p) * (f . t)) * (s - t)) / (s - t)) by XCMPLX_1:62;
then  f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((((1 - p) * (f . t)) * (s - t)) / (s - t)) by A13, XCMPLX_1:89;
hence  f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) by A13, XCMPLX_1:89; ::_thesis: verum
end;
end;
end;
hence  f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) ; ::_thesis: verum
end;
end;
end;
hence  f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) ; ::_thesis: verum
end;
hence  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)) ; ::_thesis: verum
end;
hence  f is_convex_on X by A2, RFUNCT_3:def_12; ::_thesis: verum
end;
 ( f is_convex_on X implies ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) ) )
proof
assume A18: f is_convex_on X ; ::_thesis: ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) )
 for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) )
proof
let a, b, r be Real; ::_thesis: ( a in X & b in X & r in X & a < r & r < b implies ( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) )
assume that
A19: ( a in X & b in X & r in X ) and
A20: a < r and
A21: r < b ; ::_thesis: ( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) )
A22: ( b - r < b - a & 0 < b - r ) by A20, A21, XREAL_1:10, XREAL_1:50;
set p = (b - r) / (b - a);
A23: 0 < r - a by A20, XREAL_1:50;
A24: ((b - r) / (b - a)) + ((r - a) / (b - a)) = ((b - r) + (r - a)) / (b - a) by XCMPLX_1:62
.= 1 by A22, XCMPLX_1:60 ;
then (((b - r) / (b - a)) * a) + ((1 - ((b - r) / (b - a))) * b) = ((a * (b - r)) / (b - a)) + (b * ((r - a) / (b - a))) by XCMPLX_1:74
.= ((a * (b - r)) / (b - a)) + ((b * (r - a)) / (b - a)) by XCMPLX_1:74
.= (((b * a) - (r * a)) + ((r - a) * b)) / (b - a) by XCMPLX_1:62
.= (r * (b - a)) / (b - a) ;
then A25: (((b - r) / (b - a)) * a) + ((1 - ((b - r) / (b - a))) * b) = r by A22, XCMPLX_1:89;
A26: (b - a) * ((((b - r) / (b - a)) * (f . a)) + (((r - a) / (b - a)) * (f . b))) = (((b - a) * ((b - r) / (b - a))) * (f . a)) + ((b - a) * (((r - a) / (b - a)) * (f . b)))
.= ((b - r) * (f . a)) + (((b - a) * ((r - a) / (b - a))) * (f . b)) by A22, XCMPLX_1:87
.= ((b - r) * (f . a)) + ((r - a) * (f . b)) by A22, XCMPLX_1:87 ;
 (b - r) / (b - a) < 1 by A22, XREAL_1:189;
then A27: f . ((((b - r) / (b - a)) * a) + ((1 - ((b - r) / (b - a))) * b)) <= (((b - r) / (b - a)) * (f . a)) + ((1 - ((b - r) / (b - a))) * (f . b)) by A18, A19, A22, A25, RFUNCT_3:def_12;
then  (b - a) * (f . r) <= ((b - a) * (f . a)) + (((r - a) * (f . b)) - ((r - a) * (f . a))) by A22, A24, A25, A26, XREAL_1:64;
then  ((b - a) * (f . r)) - ((b - a) * (f . a)) <= ((r - a) * (f . b)) - ((r - a) * (f . a)) by XREAL_1:20;
then  (b - a) * ((f . r) - (f . a)) <= (r - a) * ((f . b) - (f . a)) ;
hence  ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) by A22, A23, XREAL_1:102; ::_thesis: ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r)
 (b - a) * (f . r) <= ((b - a) * (f . b)) - (((b - r) * (f . b)) - ((b - r) * (f . a))) by A22, A24, A25, A27, A26, XREAL_1:64;
then  (((b - r) * (f . b)) - ((b - r) * (f . a))) + ((b - a) * (f . r)) <= (b - a) * (f . b) by XREAL_1:19;
then  ((b - r) * (f . b)) - ((b - r) * (f . a)) <= ((b - a) * (f . b)) - ((b - a) * (f . r)) by XREAL_1:19;
then  (b - r) * ((f . b) - (f . a)) <= (b - a) * ((f . b) - (f . r)) ;
hence  ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) by A22, XREAL_1:102; ::_thesis: verum
end;
hence  ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) ) by A18, RFUNCT_3:def_12; ::_thesis: verum
end;
hence  ( f is_convex_on X iff ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) ) ) by A1; ::_thesis: verum
end;

theorem :: RFUNCT_4:17
for f being PartFunc of REAL,REAL
for X being set holds
( f is_strictly_convex_on X iff ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) ) ) ) )
proof
let f be PartFunc of REAL,REAL; ::_thesis: for X being set holds
( f is_strictly_convex_on X iff ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) ) ) ) )
let X be set ; ::_thesis: ( f is_strictly_convex_on X iff ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) ) ) ) )
A1: ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) ) ) implies f is_strictly_convex_on X )
proof
assume that
A2: X c= dom f and
A3: for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) ) ; ::_thesis: f is_strictly_convex_on X
 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))
proof
let p be Real; ::_thesis: ( 0 < p & p < 1 implies 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)) )
assume that
A4: 0 < p and
A5: p < 1 ; ::_thesis: 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))
A6: 1 - p > 0 by A5, XREAL_1:50;
 for s, t being Real st s in X & t in X & (p * s) + ((1 - p) * t) in X & s <> t holds
f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((1 - p) * (f . t))
proof
let s, t be Real; ::_thesis: ( s in X & t in X & (p * s) + ((1 - p) * t) in X & s <> t implies f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((1 - p) * (f . t)) )
assume that
A7: ( s in X & t in X & (p * s) + ((1 - p) * t) in X ) and
A8: s <> t ; ::_thesis: f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((1 - p) * (f . t))
now__::_thesis:_f_._((p_*_s)_+_((1_-_p)_*_t))_<_(p_*_(f_._s))_+_((1_-_p)_*_(f_._t))
percases ( s < t or s > t ) by A8, XXREAL_0:1;
suppose s < t ; ::_thesis: f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((1 - p) * (f . t))
then A9: t - s > 0 by XREAL_1:50;
 ((p * s) + ((1 - p) * t)) - s = (1 - p) * (t - s) ;
then A10: ((p * s) + ((1 - p) * t)) - s > 0 by A6, A9, XREAL_1:129;
then A11: (p * s) + ((1 - p) * t) > s by XREAL_1:47;
A12: ( (((f . ((p * s) + ((1 - p) * t))) - (f . s)) * (t - s)) * p = (p * ((t - s) * (f . ((p * s) + ((1 - p) * t))))) - (p * ((t - s) * (f . s))) & (((f . t) - (f . ((p * s) + ((1 - p) * t)))) * (t - s)) * (1 - p) = ((1 - p) * ((t - s) * (f . t))) - ((1 - p) * ((t - s) * (f . ((p * s) + ((1 - p) * t))))) ) ;
 t - ((p * s) + ((1 - p) * t)) = p * (t - s) ;
then A13: t - ((p * s) + ((1 - p) * t)) > 0 by A4, A9, XREAL_1:129;
then  (p * s) + ((1 - p) * t) < t by XREAL_1:47;
then  ( ((f . ((p * s) + ((1 - p) * t))) - (f . s)) / (((p * s) + ((1 - p) * t)) - s) < ((f . t) - (f . s)) / (t - s) & ((f . t) - (f . s)) / (t - s) < ((f . t) - (f . ((p * s) + ((1 - p) * t)))) / (t - ((p * s) + ((1 - p) * t))) ) by A3, A7, A11;
then  ((f . ((p * s) + ((1 - p) * t))) - (f . s)) / (((p * s) + ((1 - p) * t)) - s) < ((f . t) - (f . ((p * s) + ((1 - p) * t)))) / (t - ((p * s) + ((1 - p) * t))) by XXREAL_0:2;
then  ((f . ((p * s) + ((1 - p) * t))) - (f . s)) * (t - ((p * s) + ((1 - p) * t))) < ((f . t) - (f . ((p * s) + ((1 - p) * t)))) * (((p * s) + ((1 - p) * t)) - s) by A13, A10, XREAL_1:102;
then  (p * ((t - s) * (f . ((p * s) + ((1 - p) * t))))) + ((1 - p) * ((t - s) * (f . ((p * s) + ((1 - p) * t))))) < ((1 - p) * ((t - s) * (f . t))) + (p * ((t - s) * (f . s))) by A12, XREAL_1:21;
then  f . ((p * s) + ((1 - p) * t)) < ((((1 - p) * (f . t)) * (t - s)) + ((p * (f . s)) * (t - s))) / (t - s) by A9, XREAL_1:81;
then  f . ((p * s) + ((1 - p) * t)) < ((((1 - p) * (f . t)) * (t - s)) / (t - s)) + (((p * (f . s)) * (t - s)) / (t - s)) by XCMPLX_1:62;
then  f . ((p * s) + ((1 - p) * t)) < ((1 - p) * (f . t)) + (((p * (f . s)) * (t - s)) / (t - s)) by A9, XCMPLX_1:89;
hence  f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((1 - p) * (f . t)) by A9, XCMPLX_1:89; ::_thesis: verum
end;
suppose s > t ; ::_thesis: f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((1 - p) * (f . t))
then A14: s - t > 0 by XREAL_1:50;
 ((p * s) + ((1 - p) * t)) - t = p * (s - t) ;
then A15: ((p * s) + ((1 - p) * t)) - t > 0 by A4, A14, XREAL_1:129;
then A16: (p * s) + ((1 - p) * t) > t by XREAL_1:47;
A17: ( (((f . ((p * s) + ((1 - p) * t))) - (f . t)) * (s - t)) * (1 - p) = ((1 - p) * ((s - t) * (f . ((p * s) + ((1 - p) * t))))) - ((1 - p) * ((s - t) * (f . t))) & (((f . s) - (f . ((p * s) + ((1 - p) * t)))) * (s - t)) * p = (p * ((s - t) * (f . s))) - (p * ((s - t) * (f . ((p * s) + ((1 - p) * t))))) ) ;
 s - ((p * s) + ((1 - p) * t)) = (1 - p) * (s - t) ;
then A18: s - ((p * s) + ((1 - p) * t)) > 0 by A6, A14, XREAL_1:129;
then  (p * s) + ((1 - p) * t) < s by XREAL_1:47;
then  ( ((f . ((p * s) + ((1 - p) * t))) - (f . t)) / (((p * s) + ((1 - p) * t)) - t) < ((f . s) - (f . t)) / (s - t) & ((f . s) - (f . t)) / (s - t) < ((f . s) - (f . ((p * s) + ((1 - p) * t)))) / (s - ((p * s) + ((1 - p) * t))) ) by A3, A7, A16;
then  ((f . ((p * s) + ((1 - p) * t))) - (f . t)) / (((p * s) + ((1 - p) * t)) - t) < ((f . s) - (f . ((p * s) + ((1 - p) * t)))) / (s - ((p * s) + ((1 - p) * t))) by XXREAL_0:2;
then  ((f . ((p * s) + ((1 - p) * t))) - (f . t)) * (s - ((p * s) + ((1 - p) * t))) < ((f . s) - (f . ((p * s) + ((1 - p) * t)))) * (((p * s) + ((1 - p) * t)) - t) by A18, A15, XREAL_1:102;
then  ((1 - p) * ((s - t) * (f . ((p * s) + ((1 - p) * t))))) + (p * ((s - t) * (f . ((p * s) + ((1 - p) * t))))) < (p * ((s - t) * (f . s))) + ((1 - p) * ((s - t) * (f . t))) by A17, XREAL_1:21;
then  f . ((p * s) + ((1 - p) * t)) < (((p * (f . s)) * (s - t)) + (((1 - p) * (f . t)) * (s - t))) / (s - t) by A14, XREAL_1:81;
then  f . ((p * s) + ((1 - p) * t)) < (((p * (f . s)) * (s - t)) / (s - t)) + ((((1 - p) * (f . t)) * (s - t)) / (s - t)) by XCMPLX_1:62;
then  f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((((1 - p) * (f . t)) * (s - t)) / (s - t)) by A14, XCMPLX_1:89;
hence  f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((1 - p) * (f . t)) by A14, XCMPLX_1:89; ::_thesis: verum
end;
end;
end;
hence  f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((1 - p) * (f . t)) ; ::_thesis: verum
end;
hence  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)) ; ::_thesis: verum
end;
hence  f is_strictly_convex_on X by A2, Def1; ::_thesis: verum
end;
 ( f is_strictly_convex_on X implies ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) ) ) ) )
proof
assume A19: f is_strictly_convex_on X ; ::_thesis: ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) ) ) )
 for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) )
proof
let a, b, r be Real; ::_thesis: ( a in X & b in X & r in X & a < r & r < b implies ( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) ) )
assume that
A20: ( a in X & b in X & r in X ) and
A21: a < r and
A22: r < b ; ::_thesis: ( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) )
set p = (b - r) / (b - a);
A23: ( b - r < b - a & 0 < b - r ) by A21, A22, XREAL_1:10, XREAL_1:50;
A24: ((b - r) / (b - a)) + ((r - a) / (b - a)) = ((b - r) + (r - a)) / (b - a) by XCMPLX_1:62
.= 1 by A23, XCMPLX_1:60 ;
then (((b - r) / (b - a)) * a) + ((1 - ((b - r) / (b - a))) * b) = ((a * (b - r)) / (b - a)) + (b * ((r - a) / (b - a))) by XCMPLX_1:74
.= ((a * (b - r)) / (b - a)) + ((b * (r - a)) / (b - a)) by XCMPLX_1:74
.= (((b * a) - (r * a)) + ((r - a) * b)) / (b - a) by XCMPLX_1:62
.= (r * (b - a)) / (b - a) ;
then A25: (((b - r) / (b - a)) * a) + ((1 - ((b - r) / (b - a))) * b) = r by A23, XCMPLX_1:89;
 ( 0 < (b - r) / (b - a) & (b - r) / (b - a) < 1 ) by A23, XREAL_1:139, XREAL_1:189;
then A26: f . r < (((b - r) / (b - a)) * (f . a)) + ((1 - ((b - r) / (b - a))) * (f . b)) by A19, A20, A21, A22, A25, Def1;
A27: 0 < r - a by A21, XREAL_1:50;
A28: ((((b - r) / (b - a)) * (f . a)) + ((1 - ((b - r) / (b - a))) * (f . b))) * (b - a) = (((b - a) * ((b - r) / (b - a))) * (f . a)) + ((b - a) * ((1 - ((b - r) / (b - a))) * (f . b)))
.= ((((b - a) * (b - r)) / (b - a)) * (f . a)) + (((b - a) * ((r - a) / (b - a))) * (f . b)) by A24, XCMPLX_1:74
.= ((((b - r) * (b - a)) / (b - a)) * (f . a)) + ((((b - a) * (r - a)) / (b - a)) * (f . b)) by XCMPLX_1:74
.= (((b - r) * ((b - a) / (b - a))) * (f . a)) + ((((b - a) * (r - a)) / (b - a)) * (f . b)) by XCMPLX_1:74
.= (((b - r) * 1) * (f . a)) + ((((r - a) * (b - a)) / (b - a)) * (f . b)) by A23, XCMPLX_1:60
.= ((b - r) * (f . a)) + (((r - a) * ((b - a) / (b - a))) * (f . b)) by XCMPLX_1:74
.= ((b - r) * (f . a)) + (((r - a) * 1) * (f . b)) by A23, XCMPLX_1:60 ;
then  (f . r) * (b - a) < ((b - a) * (f . a)) + (((r - a) * (f . b)) - ((r - a) * (f . a))) by A23, A26, XREAL_1:68;
then  ((f . r) * (b - a)) - ((b - a) * (f . a)) < ((r - a) * (f . b)) - ((r - a) * (f . a)) by XREAL_1:19;
then  (b - a) * ((f . r) - (f . a)) < (r - a) * ((f . b) - (f . a)) ;
hence  ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) by A23, A27, XREAL_1:106; ::_thesis: ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r)
 (f . r) * (b - a) < (((r - b) * (f . b)) + ((b - r) * (f . a))) + ((b - a) * (f . b)) by A23, A26, A28, XREAL_1:68;
then  ((f . r) * (b - a)) - (((r - b) * (f . b)) + ((b - r) * (f . a))) < (b - a) * (f . b) by XREAL_1:19;
then  ((f . r) * (b - a)) + (- (((r - b) * (f . b)) + ((b - r) * (f . a)))) < (b - a) * (f . b) ;
then  (- ((r - b) * (f . b))) - ((b - r) * (f . a)) < ((b - a) * (f . b)) - ((b - a) * (f . r)) by XREAL_1:20;
then  (b - r) * ((f . b) - (f . a)) < (b - a) * ((f . b) - (f . r)) ;
hence  ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) by A23, XREAL_1:106; ::_thesis: verum
end;
hence  ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) ) ) ) by A19, Def1; ::_thesis: verum
end;
hence  ( f is_strictly_convex_on X iff ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) ) ) ) ) by A1; ::_thesis: verum
end;

theorem :: RFUNCT_4:18
for f being PartFunc of REAL,REAL st f is total holds
( ( for n being Element of NAT
for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) holds
f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ) iff f is_convex_on REAL )
proof
let f be PartFunc of REAL,REAL; ::_thesis: ( f is total implies ( ( for n being Element of NAT
for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) holds
f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ) iff f is_convex_on REAL ) )
A1: ( f is_convex_on REAL implies for n being Element of NAT
for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) holds
f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) )
proof
assume A2: f is_convex_on REAL ; ::_thesis: for n being Element of NAT
for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) holds
f . (Sum (mlt (P,E))) <= Sum (mlt (P,F))
 for n being Element of NAT
for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) holds
f . (Sum (mlt (P,E))) <= Sum (mlt (P,F))
proof
defpred S1[ Element of NAT ] means  for P, E, F being Element of $1 -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) holds
f . (Sum (mlt (P,E))) <= Sum (mlt (P,F));
A3: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: for P, E, F being Element of k -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) holds
f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ; ::_thesis: S1[k + 1]
 for P, E, F being Element of (k + 1) -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) holds
f . (Sum (mlt (P,E))) <= Sum (mlt (P,F))
proof
let P, E, F be Element of (k + 1) -tuples_on REAL; ::_thesis: ( Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) implies f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) )
assume that
A5: Sum P = 1 and
A6: for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ; ::_thesis: f . (Sum (mlt (P,E))) <= Sum (mlt (P,F))
consider E1 being Element of k -tuples_on REAL, e1 being Real such that
A7: E = E1 ^ <*e1*> by FINSEQ_2:117;
consider F1 being Element of k -tuples_on REAL, f1 being Real such that
A8: F = F1 ^ <*f1*> by FINSEQ_2:117;
(len F1) + 1 = k + 1 by CARD_1:def_7
.= len P by CARD_1:def_7 ;
then  (len F1) + 1 in Seg (len P) by FINSEQ_1:4;
then A9: (len F1) + 1 in dom P by FINSEQ_1:def_3;
A10: f1 = F . ((len F1) + 1) by A8, FINSEQ_1:42
.= f . (E . ((len F1) + 1)) by A6, A9
.= f . (E . (k + 1)) by CARD_1:def_7
.= f . (E . ((len E1) + 1)) by CARD_1:def_7
.= f . e1 by A7, FINSEQ_1:42 ;
consider P1 being Element of k -tuples_on REAL, p1 being Real such that
A11: P = P1 ^ <*p1*> by FINSEQ_2:117;
 mlt (P,F) = (mlt (P1,F1)) ^ <*(p1 * f1)*> by A11, A8, Th2;
then A12: Sum (mlt (P,F)) = (1 * (Sum (mlt (P1,F1)))) + (p1 * f1) by RVSUM_1:74;
 mlt (P,E) = (mlt (P1,E1)) ^ <*(p1 * e1)*> by A11, A7, Th2;
then A13: Sum (mlt (P,E)) = (1 * (Sum (mlt (P1,E1)))) + (p1 * e1) by RVSUM_1:74;
A14: for i being Nat st i in dom P1 holds
P1 . i >= 0
proof
let i be Nat; ::_thesis: ( i in dom P1 implies P1 . i >= 0 )
assume A15: i in dom P1 ; ::_thesis: P1 . i >= 0
A16: i in Seg (len P1) by A15, FINSEQ_1:def_3;
then A17: 1 <= i by FINSEQ_1:1;
 i <= len P1 by A16, FINSEQ_1:1;
then A18: i <= k by CARD_1:def_7;
 k <= k + 1 by NAT_1:11;
then  i <= k + 1 by A18, XXREAL_0:2;
then  i in Seg (k + 1) by A17, FINSEQ_1:1;
then  i in Seg (len P) by CARD_1:def_7;
then A19: i in dom P by FINSEQ_1:def_3;
 P1 . i = P . i by A11, A15, FINSEQ_1:def_7;
hence  P1 . i >= 0 by A6, A19; ::_thesis: verum
end;
then A20: for i being Element of NAT st i in dom P1 holds
P1 . i >= 0 ;
now__::_thesis:_f_._(Sum_(mlt_(P,E)))_<=_Sum_(mlt_(P,F))
percases ( Sum P1 = 0 or Sum P1 <> 0 ) ;
supposeA21: Sum P1 = 0 ; ::_thesis: f . (Sum (mlt (P,E))) <= Sum (mlt (P,F))
then  for i being Element of NAT st i in dom P1 holds
P1 . i = 0 by A20, Th3;
then A22: P1 = k |-> 0 by Th4;
then  mlt (P1,E1) = k |-> 0 by Th5;
then A23: Sum (mlt (P1,E1)) = k * 0 by RVSUM_1:80;
 mlt (P1,F1) = k |-> 0 by A22, Th5;
then A24: Sum (mlt (P1,F1)) = k * 0 by RVSUM_1:80;
 Sum P = 0 + p1 by A11, A21, RVSUM_1:74;
hence  f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) by A5, A13, A12, A10, A23, A24; ::_thesis: verum
end;
supposeA25: Sum P1 <> 0 ; ::_thesis: f . (Sum (mlt (P,E))) <= Sum (mlt (P,F))
A26: 0 <= Sum P1 by A14, RVSUM_1:84;
A27: for i being Element of NAT st i in dom (((Sum P1) ") * P1) holds
( (((Sum P1) ") * P1) . i >= 0 & F1 . i = f . (E1 . i) )
proof
let i be Element of NAT ; ::_thesis: ( i in dom (((Sum P1) ") * P1) implies ( (((Sum P1) ") * P1) . i >= 0 & F1 . i = f . (E1 . i) ) )
assume  i in dom (((Sum P1) ") * P1) ; ::_thesis: ( (((Sum P1) ") * P1) . i >= 0 & F1 . i = f . (E1 . i) )
then A28: i in Seg (len (((Sum P1) ") * P1)) by FINSEQ_1:def_3;
then A29: i in Seg k by CARD_1:def_7;
then A30: i in Seg (len P1) by CARD_1:def_7;
then  i <= len P1 by FINSEQ_1:1;
then A31: i <= k by CARD_1:def_7;
A32: 1 <= i by A28, FINSEQ_1:1;
 k <= k + 1 by NAT_1:11;
then  i <= k + 1 by A31, XXREAL_0:2;
then  i in Seg (k + 1) by A32, FINSEQ_1:1;
then  i in Seg (len P) by CARD_1:def_7;
then A33: i in dom P by FINSEQ_1:def_3;
 i in dom P1 by A30, FINSEQ_1:def_3;
then  ( (((Sum P1) ") * P1) . i = ((Sum P1) ") * (P1 . i) & P1 . i >= 0 ) by A14, RVSUM_1:45;
hence  (((Sum P1) ") * P1) . i >= 0 by A26; ::_thesis: F1 . i = f . (E1 . i)
 i in Seg (len E1) by A29, CARD_1:def_7;
then  i in dom E1 by FINSEQ_1:def_3;
then A34: E . i = E1 . i by A7, FINSEQ_1:def_7;
 i in Seg (len F1) by A29, CARD_1:def_7;
then  i in dom F1 by FINSEQ_1:def_3;
then  F . i = F1 . i by A8, FINSEQ_1:def_7;
hence  F1 . i = f . (E1 . i) by A6, A33, A34; ::_thesis: verum
end;
A35: Sum (mlt (P,E)) = (((Sum P1) * ((Sum P1) ")) * (Sum (mlt (P1,E1)))) + (p1 * e1) by A13, A25, XCMPLX_0:def_7
.= ((Sum P1) * (((Sum P1) ") * (Sum (mlt (P1,E1))))) + (p1 * e1)
.= ((Sum P1) * (Sum (((Sum P1) ") * (mlt (P1,E1))))) + (p1 * e1) by RVSUM_1:87
.= ((Sum P1) * (Sum (mlt ((((Sum P1) ") * P1),E1)))) + (p1 * e1) by FINSEQOP:26 ;
A36: ((Sum P1) ") * (Sum (mlt (P1,F1))) = Sum (((Sum P1) ") * (mlt (P1,F1))) by RVSUM_1:87
.= Sum (mlt ((((Sum P1) ") * P1),F1)) by FINSEQOP:26 ;
 (len P1) + 1 = len P by A11, FINSEQ_2:16;
then  (len P1) + 1 in Seg (len P) by FINSEQ_1:4;
then A37: (len P1) + 1 in dom P by FINSEQ_1:def_3;
 (Sum P1) + p1 = 1 by A5, A11, RVSUM_1:74;
then A38: p1 = 1 - (Sum P1) ;
Sum (((Sum P1) ") * P1) = ((Sum P1) ") * (Sum P1) by RVSUM_1:87
.= 1 by A25, XCMPLX_0:def_7 ;
then  (Sum P1) * (f . (Sum (mlt ((((Sum P1) ") * P1),E1)))) <= (Sum P1) * (((Sum P1) ") * (Sum (mlt (P1,F1)))) by A4, A26, A36, A27, XREAL_1:64;
then A39: ((Sum P1) * (f . (Sum (mlt ((((Sum P1) ") * P1),E1))))) + (p1 * (f . e1)) <= ((Sum P1) * (((Sum P1) ") * (Sum (mlt (P1,F1))))) + (p1 * (f . e1)) by XREAL_1:6;
 P . ((len P1) + 1) = p1 by A11, FINSEQ_1:42;
then  Sum P1 <= 1 by A6, A38, A37, XREAL_1:49;
then  f . (Sum (mlt (P,E))) <= ((Sum P1) * (f . (Sum (mlt ((((Sum P1) ") * P1),E1))))) + (p1 * (f . e1)) by A2, A35, A38, A26, RFUNCT_3:def_12;
then  f . (Sum (mlt (P,E))) <= (((Sum P1) * ((Sum P1) ")) * (Sum (mlt (P1,F1)))) + (p1 * (f . e1)) by A39, XXREAL_0:2;
hence  f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) by A12, A10, A25, XCMPLX_0:def_7; ::_thesis: verum
end;
end;
end;
hence  f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
A40: S1[ 0 ] by RVSUM_1:79;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A40, A3);
hence  for n being Element of NAT
for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) holds
f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ; ::_thesis: verum
end;
hence  for n being Element of NAT
for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) holds
f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ; ::_thesis: verum
end;
assume  f is total ; ::_thesis: ( ( for n being Element of NAT
for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) holds
f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ) iff f is_convex_on REAL )
then A41: REAL c= dom f by PARTFUN1:def_2;
 ( ( for n being Element of NAT
for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) holds
f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ) implies f is_convex_on REAL )
proof
assume A42: for n being Element of NAT
for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) holds
f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ; ::_thesis: f is_convex_on REAL
 for p being Real st 0 <= p & p <= 1 holds
for r, s being Real st r in REAL & s in REAL & (p * r) + ((1 - p) * s) in REAL holds
f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))
proof
let p be Real; ::_thesis: ( 0 <= p & p <= 1 implies for r, s being Real st r in REAL & s in REAL & (p * r) + ((1 - p) * s) in REAL holds
f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) )
assume that
A43: 0 <= p and
A44: p <= 1 ; ::_thesis: for r, s being Real st r in REAL & s in REAL & (p * r) + ((1 - p) * s) in REAL holds
f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))
let r, s be Real; ::_thesis: ( r in REAL & s in REAL & (p * r) + ((1 - p) * s) in REAL implies f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) )
assume that
 r in REAL and
 s in REAL and
 (p * r) + ((1 - p) * s) in REAL ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))
reconsider P = <*p,(1 - p)*>, E = <*r,s*>, F = <*(f . r),(f . s)*> as Element of 2 -tuples_on REAL by FINSEQ_2:101;
A45: for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) )
proof
A46: dom P = Seg (len P) by FINSEQ_1:def_3
.= Seg 2 by CARD_1:def_7 ;
let i be Element of NAT ; ::_thesis: ( i in dom P implies ( P . i >= 0 & F . i = f . (E . i) ) )
assume A47: i in dom P ; ::_thesis: ( P . i >= 0 & F . i = f . (E . i) )
now__::_thesis:_(_P_._i_>=_0_&_F_._i_=_f_._(E_._i)_)
percases ( i = 1 or i = 2 ) by A47, A46, FINSEQ_1:2, TARSKI:def_2;
supposeA48: i = 1 ; ::_thesis: ( P . i >= 0 & F . i = f . (E . i) )
then  E . i = r by FINSEQ_1:44;
hence  ( P . i >= 0 & F . i = f . (E . i) ) by A43, A48, FINSEQ_1:44; ::_thesis: verum
end;
supposeA49: i = 2 ; ::_thesis: ( P . i >= 0 & F . i = f . (E . i) )
then  ( E . i = s & P . i = 1 - p ) by FINSEQ_1:44;
hence  ( P . i >= 0 & F . i = f . (E . i) ) by A44, A49, FINSEQ_1:44, XREAL_1:48; ::_thesis: verum
end;
end;
end;
hence  ( P . i >= 0 & F . i = f . (E . i) ) ; ::_thesis: verum
end;
Sum P = p + (1 - p) by RVSUM_1:77
.= 1 ;
then A50: f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) by A42, A45;
A51: ( P . 1 = p & P . 2 = 1 - p ) by FINSEQ_1:44;
len P = 2 by FINSEQ_1:44
.= len E by FINSEQ_1:44 ;
then  len (multreal .: (P,E)) = len P by FINSEQ_2:72;
then A52: len (mlt (P,E)) = 2 by FINSEQ_1:44;
A53: ( (mlt (P,E)) . 1 = (P . 1) * (E . 1) & (mlt (P,E)) . 2 = (P . 2) * (E . 2) ) by RVSUM_1:60;
 ( E . 1 = r & E . 2 = s ) by FINSEQ_1:44;
then  mlt (P,E) = <*(p * r),((1 - p) * s)*> by A51, A52, A53, FINSEQ_1:44;
then A54: Sum (mlt (P,E)) = (p * r) + ((1 - p) * s) by RVSUM_1:77;
A55: ( (mlt (P,F)) . 1 = (P . 1) * (F . 1) & (mlt (P,F)) . 2 = (P . 2) * (F . 2) ) by RVSUM_1:60;
len P = 2 by FINSEQ_1:44
.= len F by FINSEQ_1:44 ;
then  len (multreal .: (P,F)) = len P by FINSEQ_2:72;
then A56: len (mlt (P,F)) = 2 by FINSEQ_1:44;
 ( F . 1 = f . r & F . 2 = f . s ) by FINSEQ_1:44;
then  mlt (P,F) = <*(p * (f . r)),((1 - p) * (f . s))*> by A51, A56, A55, FINSEQ_1:44;
hence  f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) by A50, A54, RVSUM_1:77; ::_thesis: verum
end;
hence  f is_convex_on REAL by A41, RFUNCT_3:def_12; ::_thesis: verum
end;
hence  ( ( for n being Element of NAT
for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) holds
f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ) iff f is_convex_on REAL ) by A1; ::_thesis: verum
end;

theorem :: RFUNCT_4:19
for f being PartFunc of REAL,REAL
for I being Interval
for a being Real st ex x1, x2 being Real st
( x1 in I & x2 in I & x1 < a & a < x2 ) & f is_convex_on I holds
f is_continuous_in a
proof
let f be PartFunc of REAL,REAL; ::_thesis: for I being Interval
for a being Real st ex x1, x2 being Real st
( x1 in I & x2 in I & x1 < a & a < x2 ) & f is_convex_on I holds
f is_continuous_in a
let I be Interval; ::_thesis: for a being Real st ex x1, x2 being Real st
( x1 in I & x2 in I & x1 < a & a < x2 ) & f is_convex_on I holds
f is_continuous_in a
let a be Real; ::_thesis: ( ex x1, x2 being Real st
( x1 in I & x2 in I & x1 < a & a < x2 ) & f is_convex_on I implies f is_continuous_in a )
assume that
A1: ex x1, x2 being Real st
( x1 in I & x2 in I & x1 < a & a < x2 ) and
A2: f is_convex_on I ; ::_thesis: f is_continuous_in a
consider x1, x2 being Real such that
A3: x1 in I and
A4: x2 in I and
A5: x1 < a and
A6: a < x2 by A1;
set M = max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))));
A7: a in I by A3, A4, A5, A6, XXREAL_2:80;
A8: for x being Real st x1 <= x & x <= x2 & x <> a holds
( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) )
proof
let x be Real; ::_thesis: ( x1 <= x & x <= x2 & x <> a implies ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ) )
assume that
A9: x1 <= x and
A10: x <= x2 and
A11: x <> a ; ::_thesis: ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) )
A12: x in I by A3, A4, A9, A10, XXREAL_2:80;
 ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) )
proof
now__::_thesis:_(_((f_._x1)_-_(f_._a))_/_(x1_-_a)_<=_((f_._x)_-_(f_._a))_/_(x_-_a)_&_((f_._x)_-_(f_._a))_/_(x_-_a)_<=_((f_._x2)_-_(f_._a))_/_(x2_-_a)_)
percases ( x < a or x > a ) by A11, XXREAL_0:1;
supposeA13: x < a ; ::_thesis: ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) )
A14: now__::_thesis:_((f_._x1)_-_(f_._a))_/_(x1_-_a)_<=_((f_._x)_-_(f_._a))_/_(x_-_a)
percases ( x1 = x or x1 < x ) by A9, XXREAL_0:1;
suppose x1 = x ; ::_thesis: ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a)
hence  ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) ; ::_thesis: verum
end;
supposeA15: x1 < x ; ::_thesis: ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a)
A16: ((f . a) - (f . x1)) / (a - x1) = (- ((f . a) - (f . x1))) / (- (a - x1)) by XCMPLX_1:191
.= ((f . x1) - (f . a)) / (x1 - a) ;
((f . a) - (f . x)) / (a - x) = (- ((f . a) - (f . x))) / (- (a - x)) by XCMPLX_1:191
.= ((f . x) - (f . a)) / (x - a) ;
hence  ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) by A2, A3, A7, A12, A13, A15, A16, Th16; ::_thesis: verum
end;
end;
end;
 ( ((f . a) - (f . x)) / (a - x) <= ((f . x2) - (f . x)) / (x2 - x) & ((f . x2) - (f . x)) / (x2 - x) <= ((f . x2) - (f . a)) / (x2 - a) ) by A2, A4, A6, A7, A12, A13, Th16;
then  ((f . a) - (f . x)) / (a - x) <= ((f . x2) - (f . a)) / (x2 - a) by XXREAL_0:2;
then  (- ((f . a) - (f . x))) / (- (a - x)) <= ((f . x2) - (f . a)) / (x2 - a) by XCMPLX_1:191;
hence  ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ) by A14; ::_thesis: verum
end;
supposeA17: x > a ; ::_thesis: ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) )
A18: ((f . a) - (f . x1)) / (a - x1) = (- ((f . a) - (f . x1))) / (- (a - x1)) by XCMPLX_1:191
.= ((f . x1) - (f . a)) / (x1 - a) ;
 ( ((f . a) - (f . x1)) / (a - x1) <= ((f . x) - (f . x1)) / (x - x1) & ((f . x) - (f . x1)) / (x - x1) <= ((f . x) - (f . a)) / (x - a) ) by A2, A3, A5, A7, A12, A17, Th16;
hence  ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) by A18, XXREAL_0:2; ::_thesis: ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a)
now__::_thesis:_((f_._x)_-_(f_._a))_/_(x_-_a)_<=_((f_._x2)_-_(f_._a))_/_(x2_-_a)
percases ( x = x2 or x < x2 ) by A10, XXREAL_0:1;
suppose x = x2 ; ::_thesis: ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a)
hence  ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ; ::_thesis: verum
end;
suppose x < x2 ; ::_thesis: ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a)
hence  ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) by A2, A4, A7, A12, A17, Th16; ::_thesis: verum
end;
end;
end;
hence  ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ; ::_thesis: verum
end;
end;
end;
hence  ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ) ; ::_thesis: verum
end;
hence  ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ) ; ::_thesis: verum
end;
A19: for x being real number st x1 <= x & x <= x2 & x <> a holds
abs ((f . x) - (f . a)) <= (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a))
proof
A20: - (abs (((f . x1) - (f . a)) / (x1 - a))) <= ((f . x1) - (f . a)) / (x1 - a) by ABSVALUE:4;
A21: ((f . x2) - (f . a)) / (x2 - a) <= abs (((f . x2) - (f . a)) / (x2 - a)) by ABSVALUE:4;
let x be real number ; ::_thesis: ( x1 <= x & x <= x2 & x <> a implies abs ((f . x) - (f . a)) <= (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) )
assume that
A22: ( x1 <= x & x <= x2 ) and
A23: x <> a ; ::_thesis: abs ((f . x) - (f . a)) <= (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a))
reconsider x = x as Real by XREAL_0:def_1;
 ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) by A8, A22, A23;
then A24: ((f . x) - (f . a)) / (x - a) <= abs (((f . x2) - (f . a)) / (x2 - a)) by A21, XXREAL_0:2;
 x - a <> 0 by A23;
then A25: abs (x - a) > 0 by COMPLEX1:47;
 ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) by A8, A22, A23;
then A26: - (abs (((f . x1) - (f . a)) / (x1 - a))) <= ((f . x) - (f . a)) / (x - a) by A20, XXREAL_0:2;
now__::_thesis:_abs_((f_._x)_-_(f_._a))_<=_(max_((abs_(((f_._x1)_-_(f_._a))_/_(x1_-_a))),(abs_(((f_._x2)_-_(f_._a))_/_(x2_-_a)))))_*_(abs_(x_-_a))
percases ( abs (((f . x1) - (f . a)) / (x1 - a)) <= abs (((f . x2) - (f . a)) / (x2 - a)) or abs (((f . x1) - (f . a)) / (x1 - a)) >= abs (((f . x2) - (f . a)) / (x2 - a)) ) ;
suppose abs (((f . x1) - (f . a)) / (x1 - a)) <= abs (((f . x2) - (f . a)) / (x2 - a)) ; ::_thesis: abs ((f . x) - (f . a)) <= (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a))
then  - (abs (((f . x1) - (f . a)) / (x1 - a))) >= - (abs (((f . x2) - (f . a)) / (x2 - a))) by XREAL_1:24;
then  - (abs (((f . x2) - (f . a)) / (x2 - a))) <= ((f . x) - (f . a)) / (x - a) by A26, XXREAL_0:2;
then  abs (((f . x) - (f . a)) / (x - a)) <= abs (((f . x2) - (f . a)) / (x2 - a)) by A24, ABSVALUE:5;
then A27: (abs ((f . x) - (f . a))) / (abs (x - a)) <= abs (((f . x2) - (f . a)) / (x2 - a)) by COMPLEX1:67;
 abs (((f . x2) - (f . a)) / (x2 - a)) <= max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) by XXREAL_0:25;
then  (abs ((f . x) - (f . a))) / (abs (x - a)) <= max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) by A27, XXREAL_0:2;
hence  abs ((f . x) - (f . a)) <= (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) by A25, XREAL_1:81; ::_thesis: verum
end;
suppose abs (((f . x1) - (f . a)) / (x1 - a)) >= abs (((f . x2) - (f . a)) / (x2 - a)) ; ::_thesis: abs ((f . x) - (f . a)) <= (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a))
then  ((f . x) - (f . a)) / (x - a) <= abs (((f . x1) - (f . a)) / (x1 - a)) by A24, XXREAL_0:2;
then  abs (((f . x) - (f . a)) / (x - a)) <= abs (((f . x1) - (f . a)) / (x1 - a)) by A26, ABSVALUE:5;
then A28: (abs ((f . x) - (f . a))) / (abs (x - a)) <= abs (((f . x1) - (f . a)) / (x1 - a)) by COMPLEX1:67;
 abs (((f . x1) - (f . a)) / (x1 - a)) <= max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) by XXREAL_0:25;
then  (abs ((f . x) - (f . a))) / (abs (x - a)) <= max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) by A28, XXREAL_0:2;
hence  abs ((f . x) - (f . a)) <= (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) by A25, XREAL_1:81; ::_thesis: verum
end;
end;
end;
hence  abs ((f . x) - (f . a)) <= (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) ; ::_thesis: verum
end;
A29: max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) >= min ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) by Th1;
A30: ( abs (((f . x1) - (f . a)) / (x1 - a)) >= 0 & abs (((f . x2) - (f . a)) / (x2 - a)) >= 0 ) by COMPLEX1:46;
then A31: min ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) >= 0 by XXREAL_0:20;
then A32: max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) >= 0 by Th1;
 for r being real number st 0 < r holds
ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds
abs ((f . x) - (f . a)) < r ) )
proof
let r be real number ; ::_thesis: ( 0 < r implies ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds
abs ((f . x) - (f . a)) < r ) ) )
assume A33: 0 < r ; ::_thesis: ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds
abs ((f . x) - (f . a)) < r ) )
reconsider r = r as Real by XREAL_0:def_1;
 ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds
abs ((f . x) - (f . a)) < r ) )
proof
now__::_thesis:_ex_s_being_real_number_st_
(_0_<_s_&_(_for_x_being_real_number_st_x_in_dom_f_&_abs_(x_-_a)_<_s_holds_
abs_((f_._x)_-_(f_._a))_<_r_)_)
percases ( max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) > 0 or max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) = 0 ) by A30, A29, XXREAL_0:20;
supposeA34: max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) > 0 ; ::_thesis: ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds
abs ((f . x) - (f . a)) < r ) )
set s = min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a))));
A35: for x being real number st x in dom f & abs (x - a) < min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) holds
abs ((f . x) - (f . a)) < r
proof
A36: min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) <= min ((a - x1),(x2 - a)) by XXREAL_0:17;
let x be real number ; ::_thesis: ( x in dom f & abs (x - a) < min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) implies abs ((f . x) - (f . a)) < r )
assume that
 x in dom f and
A37: abs (x - a) < min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) ; ::_thesis: abs ((f . x) - (f . a)) < r
 min ((a - x1),(x2 - a)) <= a - x1 by XXREAL_0:17;
then  min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) <= a - x1 by A36, XXREAL_0:2;
then  abs (x - a) < a - x1 by A37, XXREAL_0:2;
then  - (a - x1) <= x - a by ABSVALUE:5;
then  x1 - a <= x - a ;
then A38: x1 <= x by XREAL_1:9;
 min ((a - x1),(x2 - a)) <= x2 - a by XXREAL_0:17;
then  min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) <= x2 - a by A36, XXREAL_0:2;
then  abs (x - a) < x2 - a by A37, XXREAL_0:2;
then  x - a <= x2 - a by ABSVALUE:5;
then A39: x <= x2 by XREAL_1:9;
now__::_thesis:_abs_((f_._x)_-_(f_._a))_<_r
percases ( x <> a or x = a ) ;
suppose x <> a ; ::_thesis: abs ((f . x) - (f . a)) < r
then A40: abs ((f . x) - (f . a)) <= (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) by A19, A38, A39;
now__::_thesis:_abs_((f_._x)_-_(f_._a))_<_r
percases ( max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) <> 0 or max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) = 0 ) ;
supposeA41: max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) <> 0 ; ::_thesis: abs ((f . x) - (f . a)) < r
A42: (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a))))) <= (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))) by A31, A29, XREAL_1:64, XXREAL_0:17;
 (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) < (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a))))) by A32, A37, A41, XREAL_1:68;
then  (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) < (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))) by A42, XXREAL_0:2;
then  (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) < (r * (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))) / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) by XCMPLX_1:74;
then  (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) < r * ((max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))) by XCMPLX_1:74;
then  (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) < r * 1 by A41, XCMPLX_1:60;
hence  abs ((f . x) - (f . a)) < r by A40, XXREAL_0:2; ::_thesis: verum
end;
suppose max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) = 0 ; ::_thesis: abs ((f . x) - (f . a)) < r
hence  abs ((f . x) - (f . a)) < r by A33, A40; ::_thesis: verum
end;
end;
end;
hence  abs ((f . x) - (f . a)) < r ; ::_thesis: verum
end;
suppose x = a ; ::_thesis: abs ((f . x) - (f . a)) < r
hence  abs ((f . x) - (f . a)) < r by A33, ABSVALUE:2; ::_thesis: verum
end;
end;
end;
hence  abs ((f . x) - (f . a)) < r ; ::_thesis: verum
end;
 min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) > 0
proof
A43: min ((a - x1),(x2 - a)) > 0
proof
now__::_thesis:_min_((a_-_x1),(x2_-_a))_>_0
percases ( min ((a - x1),(x2 - a)) = a - x1 or min ((a - x1),(x2 - a)) = x2 - a ) by XXREAL_0:15;
suppose min ((a - x1),(x2 - a)) = a - x1 ; ::_thesis: min ((a - x1),(x2 - a)) > 0
hence  min ((a - x1),(x2 - a)) > 0 by A5, XREAL_1:50; ::_thesis: verum
end;
suppose min ((a - x1),(x2 - a)) = x2 - a ; ::_thesis: min ((a - x1),(x2 - a)) > 0
hence  min ((a - x1),(x2 - a)) > 0 by A6, XREAL_1:50; ::_thesis: verum
end;
end;
end;
hence  min ((a - x1),(x2 - a)) > 0 ; ::_thesis: verum
end;
now__::_thesis:_min_((r_/_(max_((abs_(((f_._x1)_-_(f_._a))_/_(x1_-_a))),(abs_(((f_._x2)_-_(f_._a))_/_(x2_-_a)))))),(min_((a_-_x1),(x2_-_a))))_>_0
percases ( min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) = r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) or min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) = min ((a - x1),(x2 - a)) ) by XXREAL_0:15;
suppose min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) = r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) ; ::_thesis: min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) > 0
hence  min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) > 0 by A33, A34, XREAL_1:139; ::_thesis: verum
end;
suppose min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) = min ((a - x1),(x2 - a)) ; ::_thesis: min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) > 0
hence  min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) > 0 by A43; ::_thesis: verum
end;
end;
end;
hence  min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) > 0 ; ::_thesis: verum
end;
hence  ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds
abs ((f . x) - (f . a)) < r ) ) by A35; ::_thesis: verum
end;
supposeA44: max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) = 0 ; ::_thesis: ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds
abs ((f . x) - (f . a)) < r ) )
set s = min ((a - x1),(x2 - a));
A45: for x being real number st x1 <= x & x <= x2 & x <> a holds
abs ((f . x) - (f . a)) = 0
proof
let x be real number ; ::_thesis: ( x1 <= x & x <= x2 & x <> a implies abs ((f . x) - (f . a)) = 0 )
assume  ( x1 <= x & x <= x2 & x <> a ) ; ::_thesis: abs ((f . x) - (f . a)) = 0
then  abs ((f . x) - (f . a)) <= (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) by A19;
hence  abs ((f . x) - (f . a)) = 0 by A44, COMPLEX1:46; ::_thesis: verum
end;
A46: for x being real number st x in dom f & abs (x - a) < min ((a - x1),(x2 - a)) holds
abs ((f . x) - (f . a)) < r
proof
let x be real number ; ::_thesis: ( x in dom f & abs (x - a) < min ((a - x1),(x2 - a)) implies abs ((f . x) - (f . a)) < r )
assume that
 x in dom f and
A47: abs (x - a) < min ((a - x1),(x2 - a)) ; ::_thesis: abs ((f . x) - (f . a)) < r
 min ((a - x1),(x2 - a)) <= a - x1 by XXREAL_0:17;
then  abs (x - a) < a - x1 by A47, XXREAL_0:2;
then  - (a - x1) <= x - a by ABSVALUE:5;
then  x1 - a <= x - a ;
then A48: x1 <= x by XREAL_1:9;
 min ((a - x1),(x2 - a)) <= x2 - a by XXREAL_0:17;
then  abs (x - a) < x2 - a by A47, XXREAL_0:2;
then  x - a <= x2 - a by ABSVALUE:5;
then A49: x <= x2 by XREAL_1:9;
now__::_thesis:_abs_((f_._x)_-_(f_._a))_<_r
percases ( x <> a or x = a ) ;
suppose x <> a ; ::_thesis: abs ((f . x) - (f . a)) < r
hence  abs ((f . x) - (f . a)) < r by A33, A45, A48, A49; ::_thesis: verum
end;
suppose x = a ; ::_thesis: abs ((f . x) - (f . a)) < r
hence  abs ((f . x) - (f . a)) < r by A33, ABSVALUE:2; ::_thesis: verum
end;
end;
end;
hence  abs ((f . x) - (f . a)) < r ; ::_thesis: verum
end;
 min ((a - x1),(x2 - a)) > 0
proof
now__::_thesis:_min_((a_-_x1),(x2_-_a))_>_0
percases ( min ((a - x1),(x2 - a)) = a - x1 or min ((a - x1),(x2 - a)) = x2 - a ) by XXREAL_0:15;
suppose min ((a - x1),(x2 - a)) = a - x1 ; ::_thesis: min ((a - x1),(x2 - a)) > 0
hence  min ((a - x1),(x2 - a)) > 0 by A5, XREAL_1:50; ::_thesis: verum
end;
suppose min ((a - x1),(x2 - a)) = x2 - a ; ::_thesis: min ((a - x1),(x2 - a)) > 0
hence  min ((a - x1),(x2 - a)) > 0 by A6, XREAL_1:50; ::_thesis: verum
end;
end;
end;
hence  min ((a - x1),(x2 - a)) > 0 ; ::_thesis: verum
end;
hence  ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds
abs ((f . x) - (f . a)) < r ) ) by A46; ::_thesis: verum
end;
end;
end;
hence  ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds
abs ((f . x) - (f . a)) < r ) ) ; ::_thesis: verum
end;
hence  ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds
abs ((f . x) - (f . a)) < r ) ) ; ::_thesis: verum
end;
hence  f is_continuous_in a by FCONT_1:3; ::_thesis: verum
end;

begin

definition
let f be PartFunc of REAL,REAL;
let X be set ;
predf is_quasiconvex_on X means :Def2: :: RFUNCT_4:def 2
( 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)) <= max ((f . r),(f . s)) ) );
end;

:: deftheorem Def2 defines is_quasiconvex_on RFUNCT_4:def_2_:_
 for f being PartFunc of REAL,REAL
for X being set holds
( f is_quasiconvex_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)) <= max ((f . r),(f . s)) ) ) );

definition
let f be PartFunc of REAL,REAL;
let X be set ;
predf is_strictly_quasiconvex_on X means :Def3: :: RFUNCT_4:def 3
( 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 & f . r <> f . s holds
f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) ) );
end;

:: deftheorem Def3 defines is_strictly_quasiconvex_on RFUNCT_4:def_3_:_
 for f being PartFunc of REAL,REAL
for X being set holds
( f is_strictly_quasiconvex_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 & f . r <> f . s holds
f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) ) ) );

definition
let f be PartFunc of REAL,REAL;
let X be set ;
predf is_strongly_quasiconvex_on X means :Def4: :: RFUNCT_4:def 4
( 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)) < max ((f . r),(f . s)) ) );
end;

:: deftheorem Def4 defines is_strongly_quasiconvex_on RFUNCT_4:def_4_:_
 for f being PartFunc of REAL,REAL
for X being set holds
( f is_strongly_quasiconvex_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)) < max ((f . r),(f . s)) ) ) );

definition
let f be PartFunc of REAL,REAL;
let x0 be real number ;
predf is_upper_semicontinuous_in x0 means :Def5: :: RFUNCT_4:def 5
( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x0) - (f . x) < r ) ) ) );
end;

:: deftheorem Def5 defines is_upper_semicontinuous_in RFUNCT_4:def_5_:_
 for f being PartFunc of REAL,REAL
for x0 being real number holds
( f is_upper_semicontinuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x0) - (f . x) < r ) ) ) ) );

definition
let f be PartFunc of REAL,REAL;
let X be set ;
predf is_upper_semicontinuous_on X means :Def6: :: RFUNCT_4:def 6
( X c= dom f & ( for x0 being Real st x0 in X holds
f | X is_upper_semicontinuous_in x0 ) );
end;

:: deftheorem Def6 defines is_upper_semicontinuous_on RFUNCT_4:def_6_:_
 for f being PartFunc of REAL,REAL
for X being set holds
( f is_upper_semicontinuous_on X iff ( X c= dom f & ( for x0 being Real st x0 in X holds
f | X is_upper_semicontinuous_in x0 ) ) );

definition
let f be PartFunc of REAL,REAL;
let x0 be real number ;
predf is_lower_semicontinuous_in x0 means :Def7: :: RFUNCT_4:def 7
( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x) - (f . x0) < r ) ) ) );
end;

:: deftheorem Def7 defines is_lower_semicontinuous_in RFUNCT_4:def_7_:_
 for f being PartFunc of REAL,REAL
for x0 being real number holds
( f is_lower_semicontinuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x) - (f . x0) < r ) ) ) ) );

definition
let f be PartFunc of REAL,REAL;
let X be set ;
predf is_lower_semicontinuous_on X means :Def8: :: RFUNCT_4:def 8
( X c= dom f & ( for x0 being Real st x0 in X holds
f | X is_lower_semicontinuous_in x0 ) );
end;

:: deftheorem Def8 defines is_lower_semicontinuous_on RFUNCT_4:def_8_:_
 for f being PartFunc of REAL,REAL
for X being set holds
( f is_lower_semicontinuous_on X iff ( X c= dom f & ( for x0 being Real st x0 in X holds
f | X is_lower_semicontinuous_in x0 ) ) );

theorem Th20: :: RFUNCT_4:20
for x0 being real number
for f being PartFunc of REAL,REAL st x0 in dom f holds
( ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) iff f is_continuous_in x0 )
proof
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,REAL st x0 in dom f holds
( ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) iff f is_continuous_in x0 )
let f be PartFunc of REAL,REAL; ::_thesis: ( x0 in dom f implies ( ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) iff f is_continuous_in x0 ) )
assume A1: x0 in dom f ; ::_thesis: ( ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) iff f is_continuous_in x0 )
A2: ( f is_continuous_in x0 implies ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) )
proof
assume A3: f is_continuous_in x0 ; ::_thesis: ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 )
A4: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x0) - (f . x) < r ) )
proof
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x0) - (f . x) < r ) ) )
assume  0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x0) - (f . x) < r ) )
then consider s being real number  such that
A5: 0 < s and
A6: for x being real number st x in dom f & abs (x - x0) < s holds
abs ((f . x) - (f . x0)) < r by A3, FCONT_1:3;
take  s ; ::_thesis: ( s is Real & 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x0) - (f . x) < r ) )
thus  s is Real by XREAL_0:def_1; ::_thesis: ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x0) - (f . x) < r ) )
 for x being Real st x in dom f & abs (x - x0) < s holds
(f . x0) - (f . x) < r
proof
let x be Real; ::_thesis: ( x in dom f & abs (x - x0) < s implies (f . x0) - (f . x) < r )
assume  ( x in dom f & abs (x - x0) < s ) ; ::_thesis: (f . x0) - (f . x) < r
then A7: abs ((f . x) - (f . x0)) < r by A6;
 (f . x) - (f . x0) >= - (abs ((f . x) - (f . x0))) by ABSVALUE:4;
then  - ((f . x) - (f . x0)) <= abs ((f . x) - (f . x0)) by XREAL_1:26;
hence  (f . x0) - (f . x) < r by A7, XXREAL_0:2; ::_thesis: verum
end;
hence  ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x0) - (f . x) < r ) ) by A5; ::_thesis: verum
end;
 for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x) - (f . x0) < r ) )
proof
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x) - (f . x0) < r ) ) )
assume  0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x) - (f . x0) < r ) )
then consider s being real number  such that
A8: 0 < s and
A9: for x being real number st x in dom f & abs (x - x0) < s holds
abs ((f . x) - (f . x0)) < r by A3, FCONT_1:3;
take  s ; ::_thesis: ( s is Real & 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x) - (f . x0) < r ) )
thus  s is Real by XREAL_0:def_1; ::_thesis: ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x) - (f . x0) < r ) )
 for x being Real st x in dom f & abs (x - x0) < s holds
(f . x) - (f . x0) < r
proof
let x be Real; ::_thesis: ( x in dom f & abs (x - x0) < s implies (f . x) - (f . x0) < r )
assume  ( x in dom f & abs (x - x0) < s ) ; ::_thesis: (f . x) - (f . x0) < r
then A10: abs ((f . x) - (f . x0)) < r by A9;
 (f . x) - (f . x0) <= abs ((f . x) - (f . x0)) by ABSVALUE:4;
hence  (f . x) - (f . x0) < r by A10, XXREAL_0:2; ::_thesis: verum
end;
hence  ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds
(f . x) - (f . x0) < r ) ) by A8; ::_thesis: verum
end;
hence  ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) by A1, A4, Def5, Def7; ::_thesis: verum
end;
 ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 implies f is_continuous_in x0 )
proof
assume that
A11: f is_upper_semicontinuous_in x0 and
A12: f is_lower_semicontinuous_in x0 ; ::_thesis: f is_continuous_in x0
 for r being real number st 0 < r holds
ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - x0) < s holds
abs ((f . x) - (f . x0)) < r ) )
proof
let r be real number ; ::_thesis: ( 0 < r implies ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - x0) < s holds
abs ((f . x) - (f . x0)) < r ) ) )
assume A13: 0 < r ; ::_thesis: ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - x0) < s holds
abs ((f . x) - (f . x0)) < r ) )
A14: r is Real by XREAL_0:def_1;
then consider s1 being Real such that
A15: 0 < s1 and
A16: for x being Real st x in dom f & abs (x - x0) < s1 holds
(f . x) - (f . x0) < r by A12, A13, Def7;
consider s2 being Real such that
A17: 0 < s2 and
A18: for x being Real st x in dom f & abs (x - x0) < s2 holds
(f . x0) - (f . x) < r by A11, A13, A14, Def5;
set s = min (s1,s2);
A19: for x being real number st x in dom f & abs (x - x0) < min (s1,s2) holds
abs ((f . x) - (f . x0)) < r
proof
let x be real number ; ::_thesis: ( x in dom f & abs (x - x0) < min (s1,s2) implies abs ((f . x) - (f . x0)) < r )
assume that
A20: x in dom f and
A21: abs (x - x0) < min (s1,s2) ; ::_thesis: abs ((f . x) - (f . x0)) < r
A22: x is Real by XREAL_0:def_1;
 min (s1,s2) <= s2 by XXREAL_0:17;
then  abs (x - x0) < s2 by A21, XXREAL_0:2;
then A23: (f . x0) - (f . x) < r by A18, A20, A22;
 min (s1,s2) <= s1 by XXREAL_0:17;
then  abs (x - x0) < s1 by A21, XXREAL_0:2;
then A24: (f . x) - (f . x0) < r by A16, A20, A22;
A25: abs ((f . x) - (f . x0)) <> r
proof
assume A26: abs ((f . x) - (f . x0)) = r ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( (f . x) - (f . x0) >= 0 or not (f . x) - (f . x0) >= 0 ) ;
suppose (f . x) - (f . x0) >= 0 ; ::_thesis: contradiction
hence  contradiction by A24, A26, ABSVALUE:def_1; ::_thesis: verum
end;
suppose not (f . x) - (f . x0) >= 0 ; ::_thesis: contradiction
then  abs ((f . x) - (f . x0)) = - ((f . x) - (f . x0)) by ABSVALUE:def_1;
hence  contradiction by A23, A26; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
 - ((f . x0) - (f . x)) > - r by A23, XREAL_1:24;
then  abs ((f . x) - (f . x0)) <= r by A24, ABSVALUE:5;
hence  abs ((f . x) - (f . x0)) < r by A25, XXREAL_0:1; ::_thesis: verum
end;
take  min (s1,s2) ; ::_thesis: ( 0 < min (s1,s2) & ( for x being real number st x in dom f & abs (x - x0) < min (s1,s2) holds
abs ((f . x) - (f . x0)) < r ) )
 min (s1,s2) > 0
proof
now__::_thesis:_min_(s1,s2)_>_0
percases ( s1 <= s2 or not s1 <= s2 ) ;
suppose s1 <= s2 ; ::_thesis: min (s1,s2) > 0
hence  min (s1,s2) > 0 by A15, XXREAL_0:def_9; ::_thesis: verum
end;
suppose not s1 <= s2 ; ::_thesis: min (s1,s2) > 0
hence  min (s1,s2) > 0 by A17, XXREAL_0:def_9; ::_thesis: verum
end;
end;
end;
hence  min (s1,s2) > 0 ; ::_thesis: verum
end;
hence  ( 0 < min (s1,s2) & ( for x being real number st x in dom f & abs (x - x0) < min (s1,s2) holds
abs ((f . x) - (f . x0)) < r ) ) by A19; ::_thesis: verum
end;
hence  f is_continuous_in x0 by FCONT_1:3; ::_thesis: verum
end;
hence  ( ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) iff f is_continuous_in x0 ) by A2; ::_thesis: verum
end;

theorem :: RFUNCT_4:21
for X being set
for f being PartFunc of REAL,REAL st X c= dom f holds
( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f | X is continuous )
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f holds
( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f | X is continuous )
let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f implies ( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f | X is continuous ) )
assume A1: X c= dom f ; ::_thesis: ( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f | X is continuous )
A2: ( f | X is continuous implies ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) )
proof
assume A3: f | X is continuous ; ::_thesis: ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X )
A4: for x0 being Real st x0 in X holds
f | X is_lower_semicontinuous_in x0
proof
let x0 be Real; ::_thesis: ( x0 in X implies f | X is_lower_semicontinuous_in x0 )
assume  x0 in X ; ::_thesis: f | X is_lower_semicontinuous_in x0
then A5: x0 in dom (f | X) by A1, RELAT_1:57;
then  f | X is_continuous_in x0 by A3, FCONT_1:def_2;
hence  f | X is_lower_semicontinuous_in x0 by A5, Th20; ::_thesis: verum
end;
 for x0 being Real st x0 in X holds
f | X is_upper_semicontinuous_in x0
proof
let x0 be Real; ::_thesis: ( x0 in X implies f | X is_upper_semicontinuous_in x0 )
assume  x0 in X ; ::_thesis: f | X is_upper_semicontinuous_in x0
then A6: x0 in dom (f | X) by A1, RELAT_1:57;
then  f | X is_continuous_in x0 by A3, FCONT_1:def_2;
hence  f | X is_upper_semicontinuous_in x0 by A6, Th20; ::_thesis: verum
end;
hence  ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) by A1, A4, Def6, Def8; ::_thesis: verum
end;
 ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X implies f | X is continuous )
proof
assume that
A7: f is_upper_semicontinuous_on X and
A8: f is_lower_semicontinuous_on X ; ::_thesis: f | X is continuous
 ( X c= dom f & ( for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0 ) )
proof
thus  X c= dom f by A7, Def6; ::_thesis: for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
assume A9: x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0
A10: x0 is Real by XREAL_0:def_1;
 x0 in X by A9, RELAT_1:57;
then  ( f | X is_upper_semicontinuous_in x0 & f | X is_lower_semicontinuous_in x0 ) by A7, A8, A10, Def6, Def8;
hence  f | X is_continuous_in x0 by A9, Th20; ::_thesis: verum
end;
hence  f | X is continuous by FCONT_1:def_2; ::_thesis: verum
end;
hence  ( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f | X is continuous ) by A2; ::_thesis: verum
end;

theorem :: RFUNCT_4:22
for X being set
for f being PartFunc of REAL,REAL st f is_strictly_convex_on X holds
f is_strongly_quasiconvex_on X
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st f is_strictly_convex_on X holds
f is_strongly_quasiconvex_on X
let f be PartFunc of REAL,REAL; ::_thesis: ( f is_strictly_convex_on X implies f is_strongly_quasiconvex_on X )
assume A1: f is_strictly_convex_on X ; ::_thesis: f is_strongly_quasiconvex_on X
A2: 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)) < max ((f . r),(f . s))
proof
let p be Real; ::_thesis: ( 0 < p & p < 1 implies 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)) < max ((f . r),(f . s)) )
assume that
A3: 0 < p and
A4: p < 1 ; ::_thesis: 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)) < max ((f . r),(f . s))
 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)) < max ((f . r),(f . s))
proof
let r, s be Real; ::_thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s implies f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) )
 1 - p > 0 by A4, XREAL_1:50;
then A5: (1 - p) * (f . s) <= (1 - p) * (max ((f . r),(f . s))) by XREAL_1:64, XXREAL_0:25;
assume  ( r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s ) ; ::_thesis: f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s))
then A6: f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) by A1, A3, A4, Def1;
 p * (f . r) <= p * (max ((f . r),(f . s))) by A3, XREAL_1:64, XXREAL_0:25;
then  (p * (f . r)) + ((1 - p) * (f . s)) <= (p * (max ((f . r),(f . s)))) + ((1 - p) * (max ((f . r),(f . s)))) by A5, XREAL_1:7;
hence  f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) by A6, XXREAL_0:2; ::_thesis: verum
end;
hence  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)) < max ((f . r),(f . s)) ; ::_thesis: verum
end;
 X c= dom f by A1, Def1;
hence  f is_strongly_quasiconvex_on X by A2, Def4; ::_thesis: verum
end;

theorem :: RFUNCT_4:23
for X being set
for f being PartFunc of REAL,REAL st f is_strongly_quasiconvex_on X holds
f is_quasiconvex_on X
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st f is_strongly_quasiconvex_on X holds
f is_quasiconvex_on X
let f be PartFunc of REAL,REAL; ::_thesis: ( f is_strongly_quasiconvex_on X implies f is_quasiconvex_on X )
assume A1: f is_strongly_quasiconvex_on X ; ::_thesis: f is_quasiconvex_on X
A2: 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)) <= max ((f . r),(f . s))
proof
let p be Real; ::_thesis: ( 0 < p & p < 1 implies 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)) <= max ((f . r),(f . s)) )
assume A3: ( 0 < p & p < 1 ) ; ::_thesis: 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)) <= max ((f . r),(f . s))
 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)) <= max ((f . r),(f . s))
proof
let r, s be Real; ::_thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X implies f . ((p * r) + ((1 - p) * s)) <= max ((f . r),(f . s)) )
assume A4: ( r in X & s in X & (p * r) + ((1 - p) * s) in X ) ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= max ((f . r),(f . s))
now__::_thesis:_f_._((p_*_r)_+_((1_-_p)_*_s))_<=_max_((f_._r),(f_._s))
percases ( r <> s or r = s ) ;
suppose r <> s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= max ((f . r),(f . s))
hence  f . ((p * r) + ((1 - p) * s)) <= max ((f . r),(f . s)) by A1, A3, A4, Def4; ::_thesis: verum
end;
suppose r = s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= max ((f . r),(f . s))
hence  f . ((p * r) + ((1 - p) * s)) <= max ((f . r),(f . s)) ; ::_thesis: verum
end;
end;
end;
hence  f . ((p * r) + ((1 - p) * s)) <= max ((f . r),(f . s)) ; ::_thesis: verum
end;
hence  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)) <= max ((f . r),(f . s)) ; ::_thesis: verum
end;
 X c= dom f by A1, Def4;
hence  f is_quasiconvex_on X by A2, Def2; ::_thesis: verum
end;

theorem :: RFUNCT_4:24
for X being set
for f being PartFunc of REAL,REAL st f is_convex_on X holds
f is_strictly_quasiconvex_on X
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st f is_convex_on X holds
f is_strictly_quasiconvex_on X
let f be PartFunc of REAL,REAL; ::_thesis: ( f is_convex_on X implies f is_strictly_quasiconvex_on X )
assume A1: f is_convex_on X ; ::_thesis: f is_strictly_quasiconvex_on X
A2: 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 & f . r <> f . s holds
f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s))
proof
let p be Real; ::_thesis: ( 0 < p & p < 1 implies for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & f . r <> f . s holds
f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) )
assume that
A3: 0 < p and
A4: p < 1 ; ::_thesis: for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & f . r <> f . s holds
f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s))
 for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & f . r <> f . s holds
f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s))
proof
let r, s be Real; ::_thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X & f . r <> f . s implies f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) )
assume that
A5: ( r in X & s in X & (p * r) + ((1 - p) * s) in X ) and
A6: f . r <> f . s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s))
A7: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) by A1, A3, A4, A5, RFUNCT_3:def_12;
A8: 1 - p > 0 by A4, XREAL_1:50;
now__::_thesis:_f_._((p_*_r)_+_((1_-_p)_*_s))_<_max_((f_._r),(f_._s))
percases ( f . r < f . s or f . r > f . s ) by A6, XXREAL_0:1;
suppose f . r < f . s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s))
then  p * (f . r) < p * (f . s) by A3, XREAL_1:68;
then  (p * (f . r)) + ((1 - p) * (f . s)) < (p * (f . s)) + ((1 - p) * (f . s)) by XREAL_1:6;
then A9: f . ((p * r) + ((1 - p) * s)) < f . s by A7, XXREAL_0:2;
 f . s <= max ((f . r),(f . s)) by XXREAL_0:25;
hence  f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) by A9, XXREAL_0:2; ::_thesis: verum
end;
suppose f . r > f . s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s))
then  (1 - p) * (f . r) > (1 - p) * (f . s) by A8, XREAL_1:68;
then  (p * (f . r)) + ((1 - p) * (f . s)) < (p * (f . r)) + ((1 - p) * (f . r)) by XREAL_1:6;
then A10: f . ((p * r) + ((1 - p) * s)) < f . r by A7, XXREAL_0:2;
 f . r <= max ((f . r),(f . s)) by XXREAL_0:25;
hence  f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) by A10, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) ; ::_thesis: verum
end;
hence  for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & f . r <> f . s holds
f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) ; ::_thesis: verum
end;
 X c= dom f by A1, RFUNCT_3:def_12;
hence  f is_strictly_quasiconvex_on X by A2, Def3; ::_thesis: verum
end;

theorem :: RFUNCT_4:25
for X being set
for f being PartFunc of REAL,REAL st f is_strongly_quasiconvex_on X holds
f is_strictly_quasiconvex_on X
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st f is_strongly_quasiconvex_on X holds
f is_strictly_quasiconvex_on X
let f be PartFunc of REAL,REAL; ::_thesis: ( f is_strongly_quasiconvex_on X implies f is_strictly_quasiconvex_on X )
assume  f is_strongly_quasiconvex_on X ; ::_thesis: f is_strictly_quasiconvex_on X
then  ( 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 & f . r <> f . s holds
f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) ) ) by Def4;
hence  f is_strictly_quasiconvex_on X by Def3; ::_thesis: verum
end;

theorem :: RFUNCT_4:26
for X being set
for f being PartFunc of REAL,REAL st f is_strictly_quasiconvex_on X & f is one-to-one holds
f is_strongly_quasiconvex_on X
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st f is_strictly_quasiconvex_on X & f is one-to-one holds
f is_strongly_quasiconvex_on X
let f be PartFunc of REAL,REAL; ::_thesis: ( f is_strictly_quasiconvex_on X & f is one-to-one implies f is_strongly_quasiconvex_on X )
assume that
A1: f is_strictly_quasiconvex_on X and
A2: f is one-to-one ; ::_thesis: f is_strongly_quasiconvex_on X
A3: X c= dom f by A1, Def3;
 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)) < max ((f . r),(f . s))
proof
let p be Real; ::_thesis: ( 0 < p & p < 1 implies 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)) < max ((f . r),(f . s)) )
assume A4: ( 0 < p & p < 1 ) ; ::_thesis: 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)) < max ((f . r),(f . s))
 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)) < max ((f . r),(f . s))
proof
let r, s be Real; ::_thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s implies f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) )
assume that
A5: ( r in X & s in X ) and
A6: (p * r) + ((1 - p) * s) in X and
A7: r <> s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s))
 f . r <> f . s by A2, A3, A5, A7, FUNCT_1:def_4;
hence  f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) by A1, A4, A5, A6, Def3; ::_thesis: verum
end;
hence  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)) < max ((f . r),(f . s)) ; ::_thesis: verum
end;
hence  f is_strongly_quasiconvex_on X by A3, Def4; ::_thesis: verum
end;