let F be RealNormSpace; for f being PartFunc of REAL, the carrier of F
for x0 being Real st f is_differentiable_in x0 holds
f is_continuous_in x0
let f be PartFunc of REAL, the carrier of F; for x0 being Real st f is_differentiable_in x0 holds
f is_continuous_in x0
let x0 be Real; ( f is_differentiable_in x0 implies f is_continuous_in x0 )
assume A1:
f is_differentiable_in x0
; f is_continuous_in x0
then consider N being Neighbourhood of x0 such that
A2:
N c= dom f
and
ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
;
A3:
x0 in N
by RCOMP_1:16;
now for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) )consider g being
Real such that A4:
0 < g
and A5:
N = ].(x0 - g),(x0 + g).[
by RCOMP_1:def 6;
reconsider xx =
x0 as
Element of
REAL by XREAL_0:def 1;
set s2 =
seq_const x0;
let s1 be
Real_Sequence;
( rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) implies ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) )assume that A6:
rng s1 c= dom f
and A7:
s1 is
convergent
and A8:
lim s1 = x0
and A9:
for
n being
Nat holds
s1 . n <> x0
;
( f /* s1 is convergent & f /. x0 = lim (f /* s1) )consider l being
Nat such that A10:
for
m being
Nat st
l <= m holds
|.((s1 . m) - x0).| < g
by A7, A8, A4, SEQ_2:def 7;
reconsider c =
(seq_const x0) ^\ l as
constant Real_Sequence ;
deffunc H1(
Real)
-> set =
(s1 . $1) - ((seq_const x0) . $1);
consider s3 being
Real_Sequence such that A11:
for
n being
Nat holds
s3 . n = H1(
n)
from SEQ_1:sch 1();
A12:
s3 = s1 - (seq_const x0)
by A11, RFUNCT_2:1;
then A13:
s3 is
convergent
by A7;
A14:
rng c = {x0}
then A20:
f /* c is
convergent
by NORMSP_1:def 6;
lim (seq_const x0) =
(seq_const x0) . 0
by SEQ_4:26
.=
x0
by SEQ_1:57
;
then lim s3 =
x0 - x0
by A7, A8, A12, SEQ_2:12
.=
0
;
then A21:
lim (s3 ^\ l) = 0
by A13, SEQ_4:20;
A24:
now for n being Nat holds not (s3 ^\ l) . n = 0 end; then
s3 ^\ l is
non-zero
by SEQ_1:5;
then reconsider h =
s3 ^\ l as
non-zero 0 -convergent Real_Sequence by A13, A21, FDIFF_1:def 1;
then A27:
((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (h + c)
by FUNCT_2:63;
then A28:
((f /* (h + c)) - (f /* c)) + (f /* c) =
f /* (s1 ^\ l)
by A27, FUNCT_2:63
.=
(f /* s1) ^\ l
by A6, VALUED_0:27
;
then A30:
rng (h + c) c= N
;
A31:
lim (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) =
0 * (lim ((h ") (#) ((f /* (h + c)) - (f /* c))))
by A21, A1, A2, A14, Th13, A30, NDIFF_1:14
.=
0. F
by RLVECT_1:10
;
then A33:
h (#) ((h ") (#) ((f /* (h + c)) - (f /* c))) = (f /* (h + c)) - (f /* c)
by FUNCT_2:63;
then A34:
(f /* (h + c)) - (f /* c) is
convergent
by A30, A1, A2, A14, Th13, NDIFF_1:13;
then
((f /* (h + c)) - (f /* c)) + (f /* c) is
convergent
by A20, NORMSP_1:19;
hence
f /* s1 is
convergent
by A28, LOPBAN_3:10;
f /. x0 = lim (f /* s1)
lim (f /* c) = f /. x0
by A17, A20, NORMSP_1:def 7;
then lim (((f /* (h + c)) - (f /* c)) + (f /* c)) =
(0. F) + (f /. x0)
by A31, A33, A34, A20, NORMSP_1:25
.=
f /. x0
by RLVECT_1:4
;
hence
f /. x0 = lim (f /* s1)
by A34, A28, A20, LOPBAN_3:11, NORMSP_1:19;
verum end;
hence
f is_continuous_in x0
by A3, A2, NFCONT_3:7; verum