:: Introduction to Several Concepts of Convexity and Semicontinuityfor Function from REAL to REAL
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received March 23, 2000
:: Copyright (c) 2000 Association of Mizar Users
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 :: RFUNCT_4:7
theorem :: RFUNCT_4:8
theorem :: RFUNCT_4:9
theorem :: RFUNCT_4:10
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 :: RFUNCT_4:11
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: :: RFUNCT_4:12
theorem Th13: :: RFUNCT_4:13
theorem Th14: :: RFUNCT_4:14
theorem :: RFUNCT_4:15
theorem Th16: :: RFUNCT_4:16
theorem :: RFUNCT_4:17
theorem :: RFUNCT_4:18
theorem :: 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 :: RFUNCT_4:21
theorem :: RFUNCT_4:22
theorem :: RFUNCT_4:23
theorem :: RFUNCT_4:24
theorem :: RFUNCT_4:25
theorem :: RFUNCT_4:26