let m, n be non zero Nat; :: thesis: 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; :: thesis: 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); :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: ( 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 ) ) ) :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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;
A10: now :: thesis: for x being Point of (REAL-NS 1) st x in N1 holds
(reproj (i,nx0)) . x in dom (f | Z)
let x be Point of (REAL-NS 1); :: thesis: ( x in N1 implies (reproj (i,nx0)) . x in dom (f | Z) )
assume x in N1 ; :: thesis: (reproj (i,nx0)) . x in dom (f | Z)
then (reproj (i,nx0)) . x in Z by A9;
then (reproj (i,nx0)) . x in (dom f) /\ Z by A4, XBOOLE_0:def 4;
hence (reproj (i,nx0)) . x in dom (f | Z) by RELAT_1:61; :: thesis: verum
end;
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 :: thesis: 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); :: thesis: ( 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 ; :: thesis: ((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; :: thesis: 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 ; :: thesis: 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 ; :: thesis: f is_partial_differentiable_on Z,i
thus Z c= dom f by A21; :: according to PDIFF_1:def 19 :: thesis: 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 :: thesis: for nx0 being Point of (REAL-NS m) st nx0 in Z holds
f | Z is_partial_differentiable_in nx0,i
let nx0 be Point of (REAL-NS m); :: thesis: ( nx0 in Z implies f | Z is_partial_differentiable_in nx0,i )
assume A23: nx0 in Z ; :: thesis: f | Z is_partial_differentiable_in nx0,i
then 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;
A27: now :: thesis: for x being Point of (REAL-NS 1) st x in N1 holds
(reproj (i,nx0)) . x in dom (f | Z)
let x be Point of (REAL-NS 1); :: thesis: ( x in N1 implies (reproj (i,nx0)) . x in dom (f | Z) )
assume x in N1 ; :: thesis: (reproj (i,nx0)) . x in dom (f | Z)
then (reproj (i,nx0)) . x in Z by A26;
then (reproj (i,nx0)) . x in (dom f) /\ Z by A21, XBOOLE_0:def 4;
hence (reproj (i,nx0)) . x in dom (f | Z) by RELAT_1:61; :: thesis: verum
end;
A28: N1 c= dom ((f | Z) * (reproj (i,nx0)))
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in N1 or z in dom ((f | Z) * (reproj (i,nx0))) )
assume A29: z in N1 ; :: thesis: z in dom ((f | Z) * (reproj (i,nx0)))
then A30: z in the carrier of (REAL-NS 1) ;
reconsider x = z as Point of (REAL-NS 1) by A29;
A31: (reproj (i,nx0)) . x in dom (f | Z) by A29, A27;
z in dom (reproj (i,nx0)) by A30, FUNCT_2:def 1;
hence z in dom ((f | Z) * (reproj (i,nx0))) by A31, FUNCT_1:11; :: thesis: verum
end;
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 :: thesis: 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); :: thesis: ( 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 ; :: thesis: (((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; :: thesis: 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 ; :: thesis: 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 ) ; :: thesis: verum