let m be non zero Element of NAT ; for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL st X is open & X c= dom f holds
( ( 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 ) ) 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 Subset of (REAL m); for f being PartFunc of (REAL m),REAL st X is open & X c= dom f holds
( ( 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 ) ) 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 ( ( 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 ) ) 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.| ) ) ) ) ) )
set g = <>* f;
assume A1:
( X is open & X c= dom f )
; ( ( 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 ) ) 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.| ) ) ) ) )
then A2:
X c= dom (<>* f)
by Th3;
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 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 ) )
assume A3:
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 )
;
( 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.| ) ) ) )A4:
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 )
proof
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 A5:
( 1
<= i &
i <= m )
;
( <>* f is_partial_differentiable_on X,i & (<>* f) `partial| (X,i) is_continuous_on X )
then
(
f is_partial_differentiable_on X,
i &
f `partial| (
X,
i)
is_continuous_on X )
by A3;
hence
(
<>* f is_partial_differentiable_on X,
i &
(<>* f) `partial| (
X,
i)
is_continuous_on X )
by A1, Th61, Th62, A5;
verum
end; then
<>* f is_differentiable_on X
by Th26, A1, A2;
hence
f is_differentiable_on X
by Th53;
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.| ) )thus
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.| ) )
verumproof
let x0 be
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 r be
Real;
( x0 in X & 0 < r implies 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
(
x0 in X &
0 < r )
;
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.| ) )
then consider s being
Real such that A6:
(
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 A4, Th26, A1, A2;
take
s
;
( 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.| ) )
thus
0 < s
by A6;
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 x1 be
Element of
REAL m;
( x1 in X & |.(x1 - x0).| < s implies for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.| )
assume A7:
(
x1 in X &
|.(x1 - x0).| < s )
;
for v being Element of REAL m holds |.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.|
let v be
Element of
REAL m;
|.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.|
|.(((diff ((<>* f),x1)) . v) - ((diff ((<>* f),x0)) . v)).| <= r * |.v.|
by A7, A6;
hence
|.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.|
by Lm4;
verum
end;
end;
now ( 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 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 ) )assume A8:
(
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.| ) ) ) )
;
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 )then A9:
<>* f is_differentiable_on X
by A1, Th53;
A10:
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.| ) )
proof
let x0 be
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 r be
Real;
( x0 in X & 0 < r implies 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
(
x0 in X &
0 < r )
;
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.| ) )
then consider s being
Real such that A11:
(
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 A8;
take
s
;
( 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.| ) )
thus
0 < s
by A11;
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 x1 be
Element of
REAL m;
( x1 in X & |.(x1 - x0).| < s implies for v being Element of REAL m holds |.(((diff ((<>* f),x1)) . v) - ((diff ((<>* f),x0)) . v)).| <= r * |.v.| )
assume A12:
(
x1 in X &
|.(x1 - x0).| < s )
;
for v being Element of REAL m holds |.(((diff ((<>* f),x1)) . v) - ((diff ((<>* f),x0)) . v)).| <= r * |.v.|
let v be
Element of
REAL m;
|.(((diff ((<>* f),x1)) . v) - ((diff ((<>* f),x0)) . v)).| <= r * |.v.|
|.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| <= r * |.v.|
by A12, A11;
hence
|.(((diff ((<>* f),x1)) . v) - ((diff ((<>* f),x0)) . v)).| <= r * |.v.|
by Lm4;
verum
end; thus
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 )
verumproof
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 A13:
( 1
<= i &
i <= m )
;
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )
then A14:
(
<>* f is_partial_differentiable_on X,
i &
(<>* f) `partial| (
X,
i)
is_continuous_on X )
by A10, Th26, A2, A1, A9;
hence
f is_partial_differentiable_on X,
i
by A13, Th61, A1;
f `partial| (X,i) is_continuous_on X
hence
f `partial| (
X,
i)
is_continuous_on X
by A13, A14, Th62, A1;
verum
end; 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.| ) ) ) implies 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 ) )
; verum