let m, n be non zero Nat; for i being Nat
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for Z being Subset of (REAL-NS m) st Z is open & 1 <= i & i <= m holds
( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Point of (REAL-NS m) st x in Z holds
f is_partial_differentiable_in x,i ) ) )
let i be Nat; for f being PartFunc of (REAL-NS m),(REAL-NS n)
for Z being Subset of (REAL-NS m) st Z is open & 1 <= i & i <= m holds
( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Point of (REAL-NS m) st x in Z holds
f is_partial_differentiable_in x,i ) ) )
let f be PartFunc of (REAL-NS m),(REAL-NS n); for Z being Subset of (REAL-NS m) st Z is open & 1 <= i & i <= m holds
( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Point of (REAL-NS m) st x in Z holds
f is_partial_differentiable_in x,i ) ) )
let Z be Subset of (REAL-NS m); ( Z is open & 1 <= i & i <= m implies ( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Point of (REAL-NS m) st x in Z holds
f is_partial_differentiable_in x,i ) ) ) )
assume that
A1:
Z is open
and
A2:
( 1 <= i & i <= m )
; ( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Point of (REAL-NS m) st x in Z holds
f is_partial_differentiable_in x,i ) ) )
set S = REAL-NS 1;
set T = REAL-NS n;
set RNS = R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n));
thus
( f is_partial_differentiable_on Z,i implies ( Z c= dom f & ( for x being Point of (REAL-NS m) st x in Z holds
f is_partial_differentiable_in x,i ) ) )
( Z c= dom f & ( for x being Point of (REAL-NS m) st x in Z holds
f is_partial_differentiable_in x,i ) implies f is_partial_differentiable_on Z,i )proof
assume A3:
f is_partial_differentiable_on Z,
i
;
( Z c= dom f & ( for x being Point of (REAL-NS m) st x in Z holds
f is_partial_differentiable_in x,i ) )
hence A4:
Z c= dom f
;
for x being Point of (REAL-NS m) st x in Z holds
f is_partial_differentiable_in x,i
let nx0 be
Point of
(REAL-NS m);
( nx0 in Z implies f is_partial_differentiable_in nx0,i )
reconsider x0 =
(Proj (i,m)) . nx0 as
Point of
(REAL-NS 1) ;
assume A5:
nx0 in Z
;
f is_partial_differentiable_in nx0,i
then
f | Z is_partial_differentiable_in nx0,
i
by A3;
then
(f | Z) * (reproj (i,nx0)) is_differentiable_in x0
;
then consider N0 being
Neighbourhood of
x0 such that A6:
N0 c= dom ((f | Z) * (reproj (i,nx0)))
and A7:
ex
L being
Point of
(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) ex
R being
RestFunc of
(REAL-NS 1),
(REAL-NS n) st
for
x being
Point of
(REAL-NS 1) st
x in N0 holds
(((f | Z) * (reproj (i,nx0))) /. x) - (((f | Z) * (reproj (i,nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0))
by NDIFF_1:def 6;
consider L being
Point of
(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))),
R being
RestFunc of
(REAL-NS 1),
(REAL-NS n) such that A8:
for
x being
Point of
(REAL-NS 1) st
x in N0 holds
(((f | Z) * (reproj (i,nx0))) /. x) - (((f | Z) * (reproj (i,nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0))
by A7;
consider N1 being
Neighbourhood of
x0 such that A9:
for
x being
Point of
(REAL-NS 1) st
x in N1 holds
(reproj (i,nx0)) . x in Z
by A1, A2, A5, Lm5;
reconsider N =
N0 /\ N1 as
Neighbourhood of
x0 by Lm1;
(f | Z) * (reproj (i,nx0)) c= f * (reproj (i,nx0))
by RELAT_1:29, RELAT_1:59;
then A11:
dom ((f | Z) * (reproj (i,nx0))) c= dom (f * (reproj (i,nx0)))
by RELAT_1:11;
N c= N0
by XBOOLE_1:17;
then
N c= dom ((f | Z) * (reproj (i,nx0)))
by A6;
then A12:
N c= dom (f * (reproj (i,nx0)))
by A11;
now for x being Point of (REAL-NS 1) st x in N holds
((f * (reproj (i,nx0))) /. x) - ((f * (reproj (i,nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0))let x be
Point of
(REAL-NS 1);
( x in N implies ((f * (reproj (i,nx0))) /. x) - ((f * (reproj (i,nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )assume A13:
x in N
;
((f * (reproj (i,nx0))) /. x) - ((f * (reproj (i,nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0))then A14:
x in N0
by XBOOLE_0:def 4;
A15:
dom (reproj (i,nx0)) = the
carrier of
(REAL-NS 1)
by FUNCT_2:def 1;
x in N1
by A13, XBOOLE_0:def 4;
then A16:
(reproj (i,nx0)) . x in dom (f | Z)
by A10;
then A17:
(
(reproj (i,nx0)) . x in dom f &
(reproj (i,nx0)) . x in Z )
by RELAT_1:57;
A18:
(reproj (i,nx0)) . x0 in dom (f | Z)
by A10, NFCONT_1:4;
then A19:
(
(reproj (i,nx0)) . x0 in dom f &
(reproj (i,nx0)) . x0 in Z )
by RELAT_1:57;
A20:
((f | Z) * (reproj (i,nx0))) /. x =
(f | Z) /. ((reproj (i,nx0)) /. x)
by A16, A15, PARTFUN2:4
.=
f /. ((reproj (i,nx0)) /. x)
by A17, PARTFUN2:17
.=
(f * (reproj (i,nx0))) /. x
by A15, A17, PARTFUN2:4
;
((f | Z) * (reproj (i,nx0))) /. x0 =
(f | Z) /. ((reproj (i,nx0)) /. x0)
by A15, A18, PARTFUN2:4
.=
f /. ((reproj (i,nx0)) /. x0)
by A19, PARTFUN2:17
.=
(f * (reproj (i,nx0))) /. x0
by A15, A19, PARTFUN2:4
;
hence
((f * (reproj (i,nx0))) /. x) - ((f * (reproj (i,nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0))
by A8, A14, A20;
verum end;
then
f * (reproj (i,nx0)) is_differentiable_in x0
by A12, NDIFF_1:def 6;
hence
f is_partial_differentiable_in nx0,
i
;
verum
end;
assume that
A21:
Z c= dom f
and
A22:
for nx being Point of (REAL-NS m) st nx in Z holds
f is_partial_differentiable_in nx,i
; f is_partial_differentiable_on Z,i
thus
Z c= dom f
by A21; PDIFF_1:def 19 for b1 being Element of the carrier of (REAL-NS m) holds
( not b1 in Z or f | Z is_partial_differentiable_in b1,i )
now for nx0 being Point of (REAL-NS m) st nx0 in Z holds
f | Z is_partial_differentiable_in nx0,ilet nx0 be
Point of
(REAL-NS m);
( nx0 in Z implies f | Z is_partial_differentiable_in nx0,i )assume A23:
nx0 in Z
;
f | Z is_partial_differentiable_in nx0,ithen A24:
f is_partial_differentiable_in nx0,
i
by A22;
reconsider x0 =
(Proj (i,m)) . nx0 as
Point of
(REAL-NS 1) ;
f * (reproj (i,nx0)) is_differentiable_in x0
by A24;
then consider N0 being
Neighbourhood of
x0 such that
N0 c= dom (f * (reproj (i,nx0)))
and A25:
ex
L being
Point of
(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) ex
R being
RestFunc of
(REAL-NS 1),
(REAL-NS n) st
for
x being
Point of
(REAL-NS 1) st
x in N0 holds
((f * (reproj (i,nx0))) /. x) - ((f * (reproj (i,nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0))
by NDIFF_1:def 6;
consider N1 being
Neighbourhood of
x0 such that A26:
for
x being
Point of
(REAL-NS 1) st
x in N1 holds
(reproj (i,nx0)) . x in Z
by A1, A2, A23, Lm5;
A28:
N1 c= dom ((f | Z) * (reproj (i,nx0)))
reconsider N =
N0 /\ N1 as
Neighbourhood of
x0 by Lm1;
N c= N1
by XBOOLE_1:17;
then A32:
N c= dom ((f | Z) * (reproj (i,nx0)))
by A28;
consider L being
Point of
(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))),
R being
RestFunc of
(REAL-NS 1),
(REAL-NS n) such that A33:
for
x being
Point of
(REAL-NS 1) st
x in N0 holds
((f * (reproj (i,nx0))) /. x) - ((f * (reproj (i,nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0))
by A25;
now for x being Point of (REAL-NS 1) st x in N holds
(((f | Z) * (reproj (i,nx0))) /. x) - (((f | Z) * (reproj (i,nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0))let x be
Point of
(REAL-NS 1);
( x in N implies (((f | Z) * (reproj (i,nx0))) /. x) - (((f | Z) * (reproj (i,nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )assume A34:
x in N
;
(((f | Z) * (reproj (i,nx0))) /. x) - (((f | Z) * (reproj (i,nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0))then A35:
x in N0
by XBOOLE_0:def 4;
A36:
dom (reproj (i,nx0)) = the
carrier of
(REAL-NS 1)
by FUNCT_2:def 1;
x in N1
by A34, XBOOLE_0:def 4;
then A37:
(reproj (i,nx0)) . x in dom (f | Z)
by A27;
then A38:
(reproj (i,nx0)) . x in (dom f) /\ Z
by RELAT_1:61;
then A39:
(reproj (i,nx0)) . x in dom f
by XBOOLE_0:def 4;
A40:
(reproj (i,nx0)) . x0 in dom (f | Z)
by A27, NFCONT_1:4;
then A41:
(reproj (i,nx0)) . x0 in (dom f) /\ Z
by RELAT_1:61;
then A42:
(reproj (i,nx0)) . x0 in dom f
by XBOOLE_0:def 4;
A43:
((f | Z) * (reproj (i,nx0))) /. x =
(f | Z) /. ((reproj (i,nx0)) /. x)
by A37, A36, PARTFUN2:4
.=
f /. ((reproj (i,nx0)) /. x)
by A38, PARTFUN2:16
.=
(f * (reproj (i,nx0))) /. x
by A36, A39, PARTFUN2:4
;
((f | Z) * (reproj (i,nx0))) /. x0 =
(f | Z) /. ((reproj (i,nx0)) /. x0)
by A36, A40, PARTFUN2:4
.=
f /. ((reproj (i,nx0)) /. x0)
by A41, PARTFUN2:16
.=
(f * (reproj (i,nx0))) /. x0
by A36, A42, PARTFUN2:4
;
hence
(((f | Z) * (reproj (i,nx0))) /. x) - (((f | Z) * (reproj (i,nx0))) /. x0) = (L . (x - x0)) + (R /. (x - x0))
by A43, A35, A33;
verum end; then
(f | Z) * (reproj (i,nx0)) is_differentiable_in x0
by A32, NDIFF_1:def 6;
hence
f | Z is_partial_differentiable_in nx0,
i
;
verum end;
hence
for b1 being Element of the carrier of (REAL-NS m) holds
( not b1 in Z or f | Z is_partial_differentiable_in b1,i )
; verum