let x0 be Real; for f being PartFunc of REAL,REAL holds
( f is_differentiable_in x0 iff ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) ) )
let f be PartFunc of REAL,REAL; ( f is_differentiable_in x0 iff ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) ) )
thus
( f is_differentiable_in x0 implies ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) ) )
( ex N being Neighbourhood of x0 st N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) implies f is_differentiable_in x0 )proof
assume A1:
f is_differentiable_in x0
;
( ex N being Neighbourhood of x0 st N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) )
then consider N being
Neighbourhood of
x0 such that A2:
N c= dom f
and
ex
L being
LinearFunc ex
R being
RestFunc st
for
g being
Real st
g in N holds
(f . g) - (f . x0) = (L . (g - x0)) + (R . (g - x0))
;
thus
ex
N being
Neighbourhood of
x0 st
N c= dom f
by A2;
for h being non-zero 0 -convergent Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent
let h be
non-zero 0 -convergent Real_Sequence;
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent let c be
V8()
Real_Sequence;
( rng c = {x0} & rng (h + c) c= dom f implies (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent )
assume that A3:
rng c = {x0}
and A4:
rng (h + c) c= dom f
;
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent
A5:
lim h = 0
;
consider r being
Real such that A6:
0 < r
and A7:
N = ].(x0 - r),(x0 + r).[
by RCOMP_1:def 6;
consider k being
Nat such that A8:
for
n being
Nat st
k <= n holds
|.((h . n) - 0).| < r
by A5, A6, SEQ_2:def 7;
set h1 =
h ^\ k;
rng ((h ^\ k) + c) c= N
then A13:
((h ^\ k) ") (#) ((f /* ((h ^\ k) + c)) - (f /* c)) is
convergent
by A1, A2, A3, FDIFF_1:12;
A14:
{x0} c= dom f
c ^\ k = c
by VALUED_0:26;
then ((h ^\ k) ") (#) ((f /* ((h ^\ k) + c)) - (f /* c)) =
((h ^\ k) ") (#) ((f /* ((h + c) ^\ k)) - (f /* (c ^\ k)))
by SEQM_3:15
.=
((h ^\ k) ") (#) (((f /* (h + c)) ^\ k) - (f /* (c ^\ k)))
by A4, VALUED_0:27
.=
((h ^\ k) ") (#) (((f /* (h + c)) ^\ k) - ((f /* c) ^\ k))
by A3, A14, VALUED_0:27
.=
((h ^\ k) ") (#) (((f /* (h + c)) - (f /* c)) ^\ k)
by SEQM_3:17
.=
((h ") ^\ k) (#) (((f /* (h + c)) - (f /* c)) ^\ k)
by SEQM_3:18
.=
((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ k
by SEQM_3:19
;
hence
(h ") (#) ((f /* (h + c)) - (f /* c)) is
convergent
by A13, SEQ_4:21;
verum
end;
assume that
A16:
ex N being Neighbourhood of x0 st N c= dom f
and
A17:
for h being non-zero 0 -convergent Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent
; f is_differentiable_in x0
thus
f is_differentiable_in x0
by A16, A17, Lm1; verum