:: RFUNCT_4 semantic presentation

theorem Th1: :: RFUNCT_4:1
for b1, b2 being real number holds max b1,b2 >= min b1,b2
proof end;

theorem Th2: :: RFUNCT_4:2
for b1 being Nat
for b2, b3 being Element of b1 -tuples_on REAL
for b4, b5 being Real holds mlt (b2 ^ <*b4*>),(b3 ^ <*b5*>) = (mlt b2,b3) ^ <*(b4 * b5)*>
proof end;

theorem Th3: :: RFUNCT_4:3
for b1 being Nat
for b2 being Element of b1 -tuples_on REAL st Sum b2 = 0 & ( for b3 being Nat st b3 in dom b2 holds
0 <= b2 . b3 ) holds
for b3 being Nat st b3 in dom b2 holds
b2 . b3 = 0
proof end;

theorem Th4: :: RFUNCT_4:4
for b1 being Nat
for b2 being Element of b1 -tuples_on REAL st ( for b3 being Nat st b3 in dom b2 holds
0 = b2 . b3 ) holds
b2 = b1 |-> 0
proof end;

theorem Th5: :: RFUNCT_4:5
for b1 being Nat
for b2 being Element of b1 -tuples_on REAL holds mlt (b1 |-> 0),b2 = b1 |-> 0
proof end;

definition
let c1 be PartFunc of REAL , REAL ;
let c2 be set ;
pred c1 is_strictly_convex_on c2 means :Def1: :: RFUNCT_4:def 1
( a2 c= dom a1 & ( for b1 being Real st 0 < b1 & b1 < 1 holds
for b2, b3 being Real st b2 in a2 & b3 in a2 & (b1 * b2) + ((1 - b1) * b3) in a2 & b2 <> b3 holds
a1 . ((b1 * b2) + ((1 - b1) * b3)) < (b1 * (a1 . b2)) + ((1 - b1) * (a1 . b3)) ) );
end;

:: deftheorem Def1 defines is_strictly_convex_on RFUNCT_4:def 1 :
for b1 being PartFunc of REAL , REAL
for b2 being set holds
( b1 is_strictly_convex_on b2 iff ( b2 c= dom b1 & ( for b3 being Real st 0 < b3 & b3 < 1 holds
for b4, b5 being Real st b4 in b2 & b5 in b2 & (b3 * b4) + ((1 - b3) * b5) in b2 & b4 <> b5 holds
b1 . ((b3 * b4) + ((1 - b3) * b5)) < (b3 * (b1 . b4)) + ((1 - b3) * (b1 . b5)) ) ) );

theorem Th6: :: RFUNCT_4:6
for b1 being PartFunc of REAL , REAL
for b2 being set st b1 is_strictly_convex_on b2 holds
b1 is_convex_on b2
proof end;

theorem Th7: :: RFUNCT_4:7
for b1, b2 being Real
for b3 being PartFunc of REAL , REAL holds
( b3 is_strictly_convex_on [.b1,b2.] iff ( [.b1,b2.] c= dom b3 & ( for b4 being Real st 0 < b4 & b4 < 1 holds
for b5, b6 being Real st b5 in [.b1,b2.] & b6 in [.b1,b2.] & b5 <> b6 holds
b3 . ((b4 * b5) + ((1 - b4) * b6)) < (b4 * (b3 . b5)) + ((1 - b4) * (b3 . b6)) ) ) )
proof end;

theorem Th8: :: RFUNCT_4:8
for b1 being set
for b2 being PartFunc of REAL , REAL holds
( b2 is_convex_on b1 iff ( b1 c= dom b2 & ( for b3, b4, b5 being Real st b3 in b1 & b4 in b1 & b5 in b1 & b3 < b4 & b4 < b5 holds
b2 . b4 <= (((b5 - b4) / (b5 - b3)) * (b2 . b3)) + (((b4 - b3) / (b5 - b3)) * (b2 . b5)) ) ) )
proof end;

theorem Th9: :: RFUNCT_4:9
for b1 being set
for b2 being PartFunc of REAL , REAL holds
( b2 is_strictly_convex_on b1 iff ( b1 c= dom b2 & ( for b3, b4, b5 being Real st b3 in b1 & b4 in b1 & b5 in b1 & b3 < b4 & b4 < b5 holds
b2 . b4 < (((b5 - b4) / (b5 - b3)) * (b2 . b3)) + (((b4 - b3) / (b5 - b3)) * (b2 . b5)) ) ) )
proof end;

theorem Th10: :: RFUNCT_4:10
for b1 being PartFunc of REAL , REAL
for b2, b3 being set st b1 is_strictly_convex_on b2 & b3 c= b2 holds
b1 is_strictly_convex_on b3
proof end;

Lemma8: for b1 being Real
for b2 being PartFunc of REAL , REAL
for b3 being set st b2 is_strictly_convex_on b3 holds
b2 - b1 is_strictly_convex_on b3
proof end;

theorem Th11: :: RFUNCT_4:11
for b1 being Real
for b2 being PartFunc of REAL , REAL
for b3 being set holds
( b2 is_strictly_convex_on b3 iff b2 - b1 is_strictly_convex_on b3 )
proof end;

Lemma9: for b1 being Real
for b2 being PartFunc of REAL , REAL
for b3 being set st 0 < b1 & b2 is_strictly_convex_on b3 holds
b1 (#) b2 is_strictly_convex_on b3
proof end;

theorem Th12: :: RFUNCT_4:12
for b1 being Real
for b2 being PartFunc of REAL , REAL
for b3 being set st 0 < b1 holds
( b2 is_strictly_convex_on b3 iff b1 (#) b2 is_strictly_convex_on b3 )
proof end;

theorem Th13: :: RFUNCT_4:13
for b1, b2 being PartFunc of REAL , REAL
for b3 being set st b1 is_strictly_convex_on b3 & b2 is_strictly_convex_on b3 holds
b1 + b2 is_strictly_convex_on b3
proof end;

theorem Th14: :: RFUNCT_4:14
for b1, b2 being PartFunc of REAL , REAL
for b3 being set st b1 is_strictly_convex_on b3 & b2 is_convex_on b3 holds
b1 + b2 is_strictly_convex_on b3
proof end;

theorem Th15: :: RFUNCT_4:15
for b1, b2 being Real
for b3, b4 being PartFunc of REAL , REAL
for b5 being set st b3 is_strictly_convex_on b5 & b4 is_strictly_convex_on b5 & ( ( b1 > 0 & b2 >= 0 ) or ( b1 >= 0 & b2 > 0 ) ) holds
(b1 (#) b3) + (b2 (#) b4) is_strictly_convex_on b5
proof end;

Lemma13: for b1, b2, b3 being real number holds b3 * (b1 / b2) = (b3 * b1) / b2
by XCMPLX_1:75;

theorem Th16: :: RFUNCT_4:16
for b1 being PartFunc of REAL , REAL
for b2 being set holds
( b1 is_convex_on b2 iff ( b2 c= dom b1 & ( for b3, b4, b5 being Real st b3 in b2 & b4 in b2 & b5 in b2 & b3 < b5 & b5 < b4 holds
( ((b1 . b5) - (b1 . b3)) / (b5 - b3) <= ((b1 . b4) - (b1 . b3)) / (b4 - b3) & ((b1 . b4) - (b1 . b3)) / (b4 - b3) <= ((b1 . b4) - (b1 . b5)) / (b4 - b5) ) ) ) )
proof end;

theorem Th17: :: RFUNCT_4:17
for b1 being PartFunc of REAL , REAL
for b2 being set holds
( b1 is_strictly_convex_on b2 iff ( b2 c= dom b1 & ( for b3, b4, b5 being Real st b3 in b2 & b4 in b2 & b5 in b2 & b3 < b5 & b5 < b4 holds
( ((b1 . b5) - (b1 . b3)) / (b5 - b3) < ((b1 . b4) - (b1 . b3)) / (b4 - b3) & ((b1 . b4) - (b1 . b3)) / (b4 - b3) < ((b1 . b4) - (b1 . b5)) / (b4 - b5) ) ) ) )
proof end;

theorem Th18: :: RFUNCT_4:18
for b1 being PartFunc of REAL , REAL st b1 is total holds
( ( for b2 being Nat
for b3, b4, b5 being Element of b2 -tuples_on REAL st Sum b3 = 1 & ( for b6 being Nat st b6 in dom b3 holds
( b3 . b6 >= 0 & b5 . b6 = b1 . (b4 . b6) ) ) holds
b1 . (Sum (mlt b3,b4)) <= Sum (mlt b3,b5) ) iff b1 is_convex_on REAL )
proof end;

theorem Th19: :: RFUNCT_4:19
for b1 being PartFunc of REAL , REAL
for b2 being Interval
for b3 being Real st ex b4, b5 being Real st
( b4 in b2 & b5 in b2 & b4 < b3 & b3 < b5 ) & b1 is_convex_on b2 holds
b1 is_continuous_in b3
proof end;

definition
let c1 be PartFunc of REAL , REAL ;
let c2 be set ;
pred c1 is_quasiconvex_on c2 means :Def2: :: RFUNCT_4:def 2
( a2 c= dom a1 & ( for b1 being Real st 0 < b1 & b1 < 1 holds
for b2, b3 being Real st b2 in a2 & b3 in a2 & (b1 * b2) + ((1 - b1) * b3) in a2 holds
a1 . ((b1 * b2) + ((1 - b1) * b3)) <= max (a1 . b2),(a1 . b3) ) );
end;

:: deftheorem Def2 defines is_quasiconvex_on RFUNCT_4:def 2 :
for b1 being PartFunc of REAL , REAL
for b2 being set holds
( b1 is_quasiconvex_on b2 iff ( b2 c= dom b1 & ( for b3 being Real st 0 < b3 & b3 < 1 holds
for b4, b5 being Real st b4 in b2 & b5 in b2 & (b3 * b4) + ((1 - b3) * b5) in b2 holds
b1 . ((b3 * b4) + ((1 - b3) * b5)) <= max (b1 . b4),(b1 . b5) ) ) );

definition
let c1 be PartFunc of REAL , REAL ;
let c2 be set ;
pred c1 is_strictly_quasiconvex_on c2 means :Def3: :: RFUNCT_4:def 3
( a2 c= dom a1 & ( for b1 being Real st 0 < b1 & b1 < 1 holds
for b2, b3 being Real st b2 in a2 & b3 in a2 & (b1 * b2) + ((1 - b1) * b3) in a2 & a1 . b2 <> a1 . b3 holds
a1 . ((b1 * b2) + ((1 - b1) * b3)) < max (a1 . b2),(a1 . b3) ) );
end;

:: deftheorem Def3 defines is_strictly_quasiconvex_on RFUNCT_4:def 3 :
for b1 being PartFunc of REAL , REAL
for b2 being set holds
( b1 is_strictly_quasiconvex_on b2 iff ( b2 c= dom b1 & ( for b3 being Real st 0 < b3 & b3 < 1 holds
for b4, b5 being Real st b4 in b2 & b5 in b2 & (b3 * b4) + ((1 - b3) * b5) in b2 & b1 . b4 <> b1 . b5 holds
b1 . ((b3 * b4) + ((1 - b3) * b5)) < max (b1 . b4),(b1 . b5) ) ) );

definition
let c1 be PartFunc of REAL , REAL ;
let c2 be set ;
pred c1 is_strongly_quasiconvex_on c2 means :Def4: :: RFUNCT_4:def 4
( a2 c= dom a1 & ( for b1 being Real st 0 < b1 & b1 < 1 holds
for b2, b3 being Real st b2 in a2 & b3 in a2 & (b1 * b2) + ((1 - b1) * b3) in a2 & b2 <> b3 holds
a1 . ((b1 * b2) + ((1 - b1) * b3)) < max (a1 . b2),(a1 . b3) ) );
end;

:: deftheorem Def4 defines is_strongly_quasiconvex_on RFUNCT_4:def 4 :
for b1 being PartFunc of REAL , REAL
for b2 being set holds
( b1 is_strongly_quasiconvex_on b2 iff ( b2 c= dom b1 & ( for b3 being Real st 0 < b3 & b3 < 1 holds
for b4, b5 being Real st b4 in b2 & b5 in b2 & (b3 * b4) + ((1 - b3) * b5) in b2 & b4 <> b5 holds
b1 . ((b3 * b4) + ((1 - b3) * b5)) < max (b1 . b4),(b1 . b5) ) ) );

definition
let c1 be PartFunc of REAL , REAL ;
let c2 be real number ;
pred c1 is_upper_semicontinuous_in c2 means :Def5: :: RFUNCT_4:def 5
( a2 in dom a1 & ( for b1 being Real st 0 < b1 holds
ex b2 being Real st
( 0 < b2 & ( for b3 being Real st b3 in dom a1 & abs (b3 - a2) < b2 holds
(a1 . a2) - (a1 . b3) < b1 ) ) ) );
end;

:: deftheorem Def5 defines is_upper_semicontinuous_in RFUNCT_4:def 5 :
for b1 being PartFunc of REAL , REAL
for b2 being real number holds
( b1 is_upper_semicontinuous_in b2 iff ( b2 in dom b1 & ( for b3 being Real st 0 < b3 holds
ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in dom b1 & abs (b5 - b2) < b4 holds
(b1 . b2) - (b1 . b5) < b3 ) ) ) ) );

definition
let c1 be PartFunc of REAL , REAL ;
let c2 be set ;
pred c1 is_upper_semicontinuous_on c2 means :Def6: :: RFUNCT_4:def 6
( a2 c= dom a1 & ( for b1 being Real st b1 in a2 holds
a1 | a2 is_upper_semicontinuous_in b1 ) );
end;

:: deftheorem Def6 defines is_upper_semicontinuous_on RFUNCT_4:def 6 :
for b1 being PartFunc of REAL , REAL
for b2 being set holds
( b1 is_upper_semicontinuous_on b2 iff ( b2 c= dom b1 & ( for b3 being Real st b3 in b2 holds
b1 | b2 is_upper_semicontinuous_in b3 ) ) );

definition
let c1 be PartFunc of REAL , REAL ;
let c2 be real number ;
pred c1 is_lower_semicontinuous_in c2 means :Def7: :: RFUNCT_4:def 7
( a2 in dom a1 & ( for b1 being Real st 0 < b1 holds
ex b2 being Real st
( 0 < b2 & ( for b3 being Real st b3 in dom a1 & abs (b3 - a2) < b2 holds
(a1 . b3) - (a1 . a2) < b1 ) ) ) );
end;

:: deftheorem Def7 defines is_lower_semicontinuous_in RFUNCT_4:def 7 :
for b1 being PartFunc of REAL , REAL
for b2 being real number holds
( b1 is_lower_semicontinuous_in b2 iff ( b2 in dom b1 & ( for b3 being Real st 0 < b3 holds
ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in dom b1 & abs (b5 - b2) < b4 holds
(b1 . b5) - (b1 . b2) < b3 ) ) ) ) );

definition
let c1 be PartFunc of REAL , REAL ;
let c2 be set ;
pred c1 is_lower_semicontinuous_on c2 means :Def8: :: RFUNCT_4:def 8
( a2 c= dom a1 & ( for b1 being Real st b1 in a2 holds
a1 | a2 is_lower_semicontinuous_in b1 ) );
end;

:: deftheorem Def8 defines is_lower_semicontinuous_on RFUNCT_4:def 8 :
for b1 being PartFunc of REAL , REAL
for b2 being set holds
( b1 is_lower_semicontinuous_on b2 iff ( b2 c= dom b1 & ( for b3 being Real st b3 in b2 holds
b1 | b2 is_lower_semicontinuous_in b3 ) ) );

theorem Th20: :: RFUNCT_4:20
for b1 being real number
for b2 being PartFunc of REAL , REAL holds
( ( b2 is_upper_semicontinuous_in b1 & b2 is_lower_semicontinuous_in b1 ) iff b2 is_continuous_in b1 )
proof end;

theorem Th21: :: RFUNCT_4:21
for b1 being set
for b2 being PartFunc of REAL , REAL holds
( ( b2 is_upper_semicontinuous_on b1 & b2 is_lower_semicontinuous_on b1 ) iff b2 is_continuous_on b1 )
proof end;

theorem Th22: :: RFUNCT_4:22
for b1 being set
for b2 being PartFunc of REAL , REAL st b2 is_strictly_convex_on b1 holds
b2 is_strongly_quasiconvex_on b1
proof end;

theorem Th23: :: RFUNCT_4:23
for b1 being set
for b2 being PartFunc of REAL , REAL st b2 is_strongly_quasiconvex_on b1 holds
b2 is_quasiconvex_on b1
proof end;

theorem Th24: :: RFUNCT_4:24
for b1 being set
for b2 being PartFunc of REAL , REAL st b2 is_convex_on b1 holds
b2 is_strictly_quasiconvex_on b1
proof end;

theorem Th25: :: RFUNCT_4:25
for b1 being set
for b2 being PartFunc of REAL , REAL st b2 is_strongly_quasiconvex_on b1 holds
b2 is_strictly_quasiconvex_on b1
proof end;

theorem Th26: :: RFUNCT_4:26
for b1 being set
for b2 being PartFunc of REAL , REAL st b2 is_strictly_quasiconvex_on b1 & b2 is one-to-one holds
b2 is_strongly_quasiconvex_on b1
proof end;