begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
begin
:: deftheorem Def1 defines is_strictly_convex_on RFUNCT_4:def 1 :
theorem
theorem
theorem
theorem
theorem
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
theorem
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
theorem Th12:
theorem Th13:
theorem Th14:
theorem
theorem Th16:
theorem
theorem
theorem
begin
:: deftheorem Def2 defines is_quasiconvex_on RFUNCT_4:def 2 :
:: deftheorem Def3 defines is_strictly_quasiconvex_on RFUNCT_4:def 3 :
:: deftheorem Def4 defines is_strongly_quasiconvex_on RFUNCT_4:def 4 :
:: deftheorem Def5 defines is_upper_semicontinuous_in RFUNCT_4:def 5 :
:: deftheorem Def6 defines is_upper_semicontinuous_on RFUNCT_4:def 6 :
:: deftheorem Def7 defines is_lower_semicontinuous_in RFUNCT_4:def 7 :
:: deftheorem Def8 defines is_lower_semicontinuous_on RFUNCT_4:def 8 :
theorem Th20:
theorem
theorem
theorem
theorem
theorem
theorem