:: Real Function Differentiability - Part II
:: by Jaros{\l}aw Kotowicz and Konrad Raczkowski
::
:: Received January 10, 1991
:: Copyright (c) 1991 Association of Mizar Users
theorem Th1: :: FDIFF_2:1
theorem Th2: :: FDIFF_2:2
theorem Th3: :: FDIFF_2:3
theorem Th4: :: FDIFF_2:4
theorem Th5: :: FDIFF_2:5
theorem Th6: :: FDIFF_2:6
theorem Th7: :: FDIFF_2:7
theorem Th8: :: FDIFF_2:8
theorem Th9: :: FDIFF_2:9
theorem :: FDIFF_2:10
Lm1:
for x0 being Real
for f being PartFunc of REAL , REAL st ex N being Neighbourhood of x0 st N c= dom f & ( for h being convergent_to_0 Real_Sequence
for c being V6 Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent ) holds
( f is_differentiable_in x0 & ( for h being convergent_to_0 Real_Sequence
for c being V6 Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
diff f,x0 = lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) ) )
theorem Th11: :: FDIFF_2:11
theorem Th12: :: FDIFF_2:12
Lm2:
for x0 being Real
for f2, f1 being PartFunc of REAL , REAL st ex N being Neighbourhood of x0 st N c= dom (f2 * f1) & f1 is_differentiable_in x0 & f2 is_differentiable_in f1 . x0 holds
( f2 * f1 is_differentiable_in x0 & diff (f2 * f1),x0 = (diff f2,(f1 . x0)) * (diff f1,x0) )
theorem Th13: :: FDIFF_2:13
theorem Th14: :: FDIFF_2:14
theorem Th15: :: FDIFF_2:15
theorem :: FDIFF_2:16
theorem :: FDIFF_2:17
theorem :: FDIFF_2:18
theorem :: FDIFF_2:19
theorem :: FDIFF_2:20
Lm3:
for f being PartFunc of REAL , REAL holds (f (#) f) " {0 } = f " {0 }
theorem :: FDIFF_2:21
theorem :: FDIFF_2:22
theorem :: FDIFF_2:23
theorem Th24: :: FDIFF_2:24
theorem Th25: :: FDIFF_2:25
theorem :: FDIFF_2:26
theorem :: FDIFF_2:27
theorem :: FDIFF_2:28
theorem Th29: :: FDIFF_2:29
theorem Th30: :: FDIFF_2:30
theorem :: FDIFF_2:31
theorem :: FDIFF_2:32
theorem Th33: :: FDIFF_2:33
theorem Th34: :: FDIFF_2:34
theorem :: FDIFF_2:35
theorem :: FDIFF_2:36
theorem Th37: :: FDIFF_2:37
theorem Th38: :: FDIFF_2:38
theorem :: FDIFF_2:39
theorem :: FDIFF_2:40
theorem Th41: :: FDIFF_2:41
theorem Th42: :: FDIFF_2:42
theorem Th43: :: FDIFF_2:43
theorem Th44: :: FDIFF_2:44
theorem :: FDIFF_2:45
theorem :: FDIFF_2:46
theorem :: FDIFF_2:47
theorem :: FDIFF_2:48
for
p,
g being
Real for
f being
one-to-one PartFunc of
REAL ,
REAL st
].p,g.[ c= dom f &
f is_differentiable_on ].p,g.[ & ( for
x0 being
Real st
x0 in ].p,g.[ holds
0 < diff f,
x0 or for
x0 being
Real st
x0 in ].p,g.[ holds
diff f,
x0 < 0 ) holds
(
f | ].p,g.[ is
one-to-one &
(f | ].p,g.[) " is_differentiable_on dom ((f | ].p,g.[) " ) & ( for
x0 being
Real st
x0 in dom ((f | ].p,g.[) " ) holds
diff ((f | ].p,g.[) " ),
x0 = 1
/ (diff f,(((f | ].p,g.[) " ) . x0)) ) )
theorem :: FDIFF_2:49