:: RFUNCT_4 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: RFUNCT_4:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number holds max a,b >= min a,b
proof end;

theorem Th2: :: RFUNCT_4:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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 end;

theorem Th3: :: RFUNCT_4:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for R being Element of n -tuples_on REAL st Sum R = 0 & ( for i being Nat st i in dom R holds
0 <= R . i ) holds
for i being Nat st i in dom R holds
R . i = 0
proof end;

theorem Th4: :: RFUNCT_4:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for R being Element of n -tuples_on REAL st ( for i being Nat st i in dom R holds
0 = R . i ) holds
R = n |-> 0
proof end;

theorem Th5: :: RFUNCT_4:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for R being Element of n -tuples_on REAL holds mlt (n |-> 0),R = n |-> 0
proof end;

definition
let f be PartFunc of REAL , REAL ;
let X be set ;
pred f 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 Th6: :: RFUNCT_4:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RFUNCT_4:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RFUNCT_4:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RFUNCT_4:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RFUNCT_4:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 end;

theorem :: RFUNCT_4:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 end;

theorem Th12: :: RFUNCT_4:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th13: :: RFUNCT_4:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th14: :: RFUNCT_4:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RFUNCT_4:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

Lm3: for a, b, r being real number holds r * (a / b) = (r * a) / b
by XCMPLX_1:75;

theorem Th16: :: RFUNCT_4:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RFUNCT_4:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RFUNCT_4:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being PartFunc of REAL , REAL st f is total holds
( ( for n being Nat
for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being 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 end;

theorem :: RFUNCT_4:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let f be PartFunc of REAL , REAL ;
let X be set ;
pred f 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 ;
pred f 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 ;
pred f 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 ;
pred f 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 ;
pred f 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 ;
pred f 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 ;
pred f 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x0 being real number
for f being PartFunc of REAL , REAL holds
( ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) iff f is_continuous_in x0 )
proof end;

theorem :: RFUNCT_4:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for f being PartFunc of REAL , REAL holds
( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f is_continuous_on X )
proof end;

theorem :: RFUNCT_4:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RFUNCT_4:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RFUNCT_4:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RFUNCT_4:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RFUNCT_4:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;