:: Real Function One-Side Differantiability
:: by Ewa Burakowska and Beata Madras
::
:: Received December 12, 1991
:: Copyright (c) 1991 Association of Mizar Users
theorem Th1: :: FDIFF_3:1
theorem Th2: :: FDIFF_3:2
theorem Th3: :: FDIFF_3:3
theorem Th4: :: FDIFF_3:4
:: deftheorem Def1 defines is_Lcontinuous_in FDIFF_3:def 1 :
:: deftheorem Def2 defines is_Rcontinuous_in FDIFF_3:def 2 :
:: deftheorem Def3 defines is_right_differentiable_in FDIFF_3:def 3 :
:: deftheorem Def4 defines is_left_differentiable_in FDIFF_3:def 4 :
theorem Th5: :: FDIFF_3:5
theorem Th6: :: FDIFF_3:6
theorem Th7: :: FDIFF_3:7
theorem Th8: :: FDIFF_3:8
:: deftheorem Def5 defines Ldiff FDIFF_3:def 5 :
:: deftheorem Def6 defines Rdiff FDIFF_3:def 6 :
theorem Th9: :: FDIFF_3:9
theorem :: FDIFF_3:10
theorem :: FDIFF_3:11
theorem :: FDIFF_3:12
Lm1:
for f1, f2 being PartFunc of REAL ,REAL
for x0 being Real st f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 & ex r0 being Real st
( r0 > 0 & ( for g being Real st g in dom f2 & g in [.(x0 - r0),x0.] holds
f2 . g <> 0 ) ) holds
( f1 / f2 is_left_differentiable_in x0 & Ldiff (f1 / f2),x0 = (((Ldiff f1,x0) * (f2 . x0)) - ((Ldiff f2,x0) * (f1 . x0))) / ((f2 . x0) ^2 ) )
theorem :: FDIFF_3:13
Lm2:
for f being PartFunc of REAL ,REAL
for x0 being Real st f is_left_differentiable_in x0 & ex r0 being Real st
( r0 > 0 & ( for g being Real st g in dom f & g in [.(x0 - r0),x0.] holds
f . g <> 0 ) ) holds
( f ^ is_left_differentiable_in x0 & Ldiff (f ^ ),x0 = - ((Ldiff f,x0) / ((f . x0) ^2 )) )
theorem :: FDIFF_3:14
theorem Th15: :: FDIFF_3:15
theorem :: FDIFF_3:16
theorem :: FDIFF_3:17
theorem :: FDIFF_3:18
Lm3:
for f1, f2 being PartFunc of REAL ,REAL
for x0 being Real st f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 & ex r0 being Real st
( r0 > 0 & ( for g being Real st g in dom f2 & g in [.x0,(x0 + r0).] holds
f2 . g <> 0 ) ) holds
( f1 / f2 is_right_differentiable_in x0 & Rdiff (f1 / f2),x0 = (((Rdiff f1,x0) * (f2 . x0)) - ((Rdiff f2,x0) * (f1 . x0))) / ((f2 . x0) ^2 ) )
theorem :: FDIFF_3:19
Lm4:
for f being PartFunc of REAL ,REAL
for x0 being Real st f is_right_differentiable_in x0 & ex r0 being Real st
( r0 > 0 & ( for g being Real st g in dom f & g in [.x0,(x0 + r0).] holds
f . g <> 0 ) ) holds
( f ^ is_right_differentiable_in x0 & Rdiff (f ^ ),x0 = - ((Rdiff f,x0) / ((f . x0) ^2 )) )
theorem :: FDIFF_3:20
theorem :: FDIFF_3:21
theorem :: FDIFF_3:22