let m be non zero Element of NAT ; :: thesis: 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); :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( ( 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 :: thesis: ( 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 ) ; :: thesis: ( 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; :: thesis: ( 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 ) ; :: thesis: ( <>* 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; :: thesis: verum
end;
then <>* f is_differentiable_on X by Th26, A1, A2;
hence f is_differentiable_on X by Th53; :: thesis: 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.| ) ) :: thesis: verum
proof
let x0 be Element of REAL m; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: |.(((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; :: thesis: verum
end;
end;
now :: thesis: ( 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.| ) ) ) ) ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: |.(((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; :: thesis: 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 ) :: thesis: verum
proof
let i be Nat; :: thesis: ( 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 ) ; :: thesis: ( 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; :: thesis: f `partial| (X,i) is_continuous_on X
hence f `partial| (X,i) is_continuous_on X by A13, A14, Th62, A1; :: thesis: 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 ) ) ; :: thesis: verum