let m be non zero Element of NAT ; for k being Element of NAT
for X being non empty Subset of (REAL m)
for f being PartFunc of (REAL m),REAL st X is open & X c= dom f holds
( f is_continuously_differentiable_up_to_order 1,X iff ( f is_differentiable_on X & ( for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) ) )
let k be Element of NAT ; for X being non empty Subset of (REAL m)
for f being PartFunc of (REAL m),REAL st X is open & X c= dom f holds
( f is_continuously_differentiable_up_to_order 1,X iff ( f is_differentiable_on X & ( for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) ) )
let X be non empty Subset of (REAL m); for f being PartFunc of (REAL m),REAL st X is open & X c= dom f holds
( f is_continuously_differentiable_up_to_order 1,X iff ( f is_differentiable_on X & ( for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) ) )
let f be PartFunc of (REAL m),REAL; ( X is open & X c= dom f implies ( f is_continuously_differentiable_up_to_order 1,X iff ( f is_differentiable_on X & ( for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) ) ) )
assume A1:
( X is open & X c= dom f )
; ( f is_continuously_differentiable_up_to_order 1,X iff ( f is_differentiable_on X & ( for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) ) )
hereby ( f is_differentiable_on X & ( for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) implies f is_continuously_differentiable_up_to_order 1,X )
assume A2:
f is_continuously_differentiable_up_to_order 1,
X
;
( f is_differentiable_on X & ( for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) )now for i being Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )let i be
Nat;
( 1 <= i & i <= m implies ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) )assume A3:
( 1
<= i &
i <= m )
;
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )reconsider ii =
i as
Element of
NAT by ORDINAL1:def 12;
set I =
<*ii*>;
A4:
len <*ii*> = 1
by FINSEQ_1:40;
i in Seg m
by A3;
then
{i} c= Seg m
by ZFMISC_1:31;
then A5:
rng <*ii*> c= Seg m
by FINSEQ_1:38;
then A6:
f `partial| (
X,
<*ii*>)
is_continuous_on X
by A2, A4;
thus
f is_partial_differentiable_on X,
i
by A4, A5, A2, PDIFF_9:def 11, PDIFF_9:81;
f `partial| (X,i) is_continuous_on Xhence
f `partial| (
X,
i)
is_continuous_on X
by A1, A3, PDIFF_9:82, A6;
verum end; hence
(
f is_differentiable_on X & ( for
x0 being
Element of
REAL m for
r being
Real st
x0 in X &
0 < r holds
ex
s being
Real st
(
0 < s & ( for
x1 being
Element of
REAL m st
x1 in X &
|.(x1 - x0).| < s holds
for
v being
Element of
REAL m holds
|.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) )
by A1, PDIFF_9:63;
verum
end;
assume A7:
( f is_differentiable_on X & ( for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| ) ) ) )
; f is_continuously_differentiable_up_to_order 1,X
then A8:
for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )
by A1, PDIFF_9:63;
A9:
now for I being non empty FinSequence of NAT st len I <= 1 & rng I c= Seg m holds
( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X )let I be non
empty FinSequence of
NAT ;
( len I <= 1 & rng I c= Seg m implies ( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X ) )assume A10:
(
len I <= 1 &
rng I c= Seg m )
;
( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X )A11:
1
<= len I
by FINSEQ_1:20;
then
1
in dom I
by FINSEQ_3:25;
then A14:
I . 1
in rng I
by FUNCT_1:3;
reconsider i =
I . 1 as
Element of
NAT by ORDINAL1:def 12;
A15:
( 1
<= i &
i <= m )
by A14, A10, FINSEQ_1:1;
A16:
I = <*(I . 1)*>
by FINSEQ_5:14, A10, A11, XXREAL_0:1;
then A17:
I = <*i*>
;
thus
f is_partial_differentiable_on X,
I
by A16, PDIFF_9:81, A15, A8;
f `partial| (X,I) is_continuous_on X
f `partial| (
X,
i)
is_continuous_on X
by A15, A1, PDIFF_9:63, A7;
hence
f `partial| (
X,
I)
is_continuous_on X
by A1, A8, A17, A15, PDIFF_9:82;
verum end;
then
for I being non empty FinSequence of NAT st len I <= 1 & rng I c= Seg m holds
f is_partial_differentiable_on X,I
;
hence
f is_continuously_differentiable_up_to_order 1,X
by A1, A9, PDIFF_9:def 11; verum