environ
vocabularies HIDDEN, NUMBERS, REAL_1, PARTFUN1, SUBSET_1, XXREAL_0, FINSEQ_2, RVSUM_1, ORDINAL4, FINSEQ_1, RELAT_1, ARYTM_3, NAT_1, FUNCT_1, CARD_3, CARD_1, TARSKI, ARYTM_1, RFUNCT_3, XXREAL_1, VALUED_1, XBOOLE_0, BINOP_2, MEASURE5, FCONT_1, COMPLEX1, ORDINAL2, RFUNCT_4, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, RELAT_1, COMPLEX1, NAT_1, FUNCT_1, FINSEQ_1, REAL_1, FINSEQ_2, PARTFUN1, FUNCOP_1, FINSEQOP, BINOP_1, BINOP_2, VALUED_1, RVSUM_1, RCOMP_1, RFUNCT_3, MEASURE5, FCONT_1, XXREAL_0;
definitions ;
theorems RCOMP_1, RFUNCT_3, TARSKI, PARTFUN1, FINSEQ_1, FINSEQ_2, RVSUM_1, NAT_1, FCONT_1, ABSVALUE, FUNCT_1, XREAL_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, FINSEQOP, VALUED_1, XXREAL_2, RELAT_1, CARD_1;
schemes NAT_1;
registrations RELSET_1, NUMBERS, XXREAL_0, XREAL_0, BINOP_2, MEMBERED, FINSEQ_2, VALUED_0, FINSEQ_1, FUNCT_1, RVSUM_1, ORDINAL1;
constructors HIDDEN, BINOP_1, REAL_1, NAT_1, BINOP_2, COMPLEX1, FINSEQOP, RCOMP_1, RVSUM_1, FCONT_1, RFUNCT_3, MEASURE5, XXREAL_2, RELSET_1, FINSEQ_4, CARD_3, FUNCOP_1;
requirements HIDDEN, NUMERALS, SUBSET, REAL, BOOLE, ARITHM;
equalities RVSUM_1, ORDINAL1;
expansions ;
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
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