:: RFUNCT_4 semantic presentation
theorem Th1: :: RFUNCT_4:1
theorem Th2: :: RFUNCT_4:2
theorem Th3: :: RFUNCT_4:3
theorem Th4: :: RFUNCT_4:4
theorem Th5: :: RFUNCT_4:5
:: deftheorem Def1 defines is_strictly_convex_on RFUNCT_4:def 1 :
theorem Th6: :: RFUNCT_4:6
theorem Th7: :: RFUNCT_4:7
theorem Th8: :: RFUNCT_4:8
theorem Th9: :: RFUNCT_4:9
theorem Th10: :: RFUNCT_4:10
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
theorem Th11: :: RFUNCT_4:11
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
theorem Th12: :: RFUNCT_4:12
theorem Th13: :: RFUNCT_4:13
theorem Th14: :: RFUNCT_4:14
theorem Th15: :: RFUNCT_4:15
Lemma13:
for b1, b2, b3 being real number holds b3 * (b1 / b2) = (b3 * b1) / b2
by XCMPLX_1:75;
theorem Th16: :: RFUNCT_4:16
theorem Th17: :: RFUNCT_4:17
theorem Th18: :: RFUNCT_4:18
theorem Th19: :: RFUNCT_4:19
:: 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: :: RFUNCT_4:20
theorem Th21: :: RFUNCT_4:21
theorem Th22: :: RFUNCT_4:22
theorem Th23: :: RFUNCT_4:23
theorem Th24: :: RFUNCT_4:24
theorem Th25: :: RFUNCT_4:25
theorem Th26: :: RFUNCT_4:26