:: Differentiable Functions on Normed Linear Spaces
:: by Yasunari Shidama
::
:: Received June 2, 2011
:: Copyright (c) 2011-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, ZFMISC_1, NORMSP_1, PRE_TOPC, PARTFUN1, FUNCT_1,
FUNCT_4, NAT_1, FDIFF_1, SUBSET_1, SEQ_4, RELAT_1, GLIB_000, LOPBAN_1,
ORDINAL4, RFINSEQ, RCOMP_1, TARSKI, SEQ_1, ARYTM_3, VALUED_1, FUNCT_2,
ARYTM_1, SEQ_2, ORDINAL2, SUPINF_2, FCONT_1, COMPLEX1, STRUCT_0, CARD_1,
VALUED_0, XXREAL_0, GROUP_2, FUNCOP_1, MEMBERED, FINSEQ_5, XXREAL_2,
XBOOLE_0, CARD_3, FINSEQ_1, FINSEQ_2, AFINSQ_1, RLVECT_1, SQUARE_1,
RVSUM_1, XXREAL_1, PDIFF_1, PRVECT_1, PRVECT_2, ALGSTR_0, EUCLID,
CFCONT_1, RFINSEQ2, NORMSP_0, MONOID_0, RLTOPSP1, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, FUNCT_2, FUNCOP_1, FUNCT_4, CARD_1, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, REAL_1, SQUARE_1, NAT_1, MEMBERED, VALUED_0, COMPLEX1,
NAT_D, XXREAL_2, CARD_3, FINSEQ_1, VALUED_1, FINSEQ_2, SEQ_1, SEQ_2,
RVSUM_1, RFINSEQ, SEQ_4, RCOMP_1, FCONT_1, FDIFF_1, FINSEQ_5, FINSEQ_7,
RFINSEQ2, STRUCT_0, MONOID_0, ALGSTR_0, PRE_TOPC, RLVECT_1, NORMSP_0,
NORMSP_1, VFUNCT_1, EUCLID, LOPBAN_1, PRVECT_1, NFCONT_1, NDIFF_1,
PRVECT_2, NFCONT_3, NDIFF_3, RLTOPSP1, FUNCT_7;
constructors REAL_1, SQUARE_1, SEQ_2, FDIFF_1, NFCONT_1, RSSPACE, VFUNCT_1,
NDIFF_1, RELSET_1, FINSEQ_7, FINSEQ_5, RVSUM_1, BINOP_2, PRVECT_2,
RLVECT_2, NAT_D, FINSEQOP, RFINSEQ, RFINSEQ2, SEQ_4, FCONT_1, NFCONT_3,
NDIFF_3, MONOID_0, RLTOPSP1, FUNCT_7, COMSEQ_2, FUNCT_4, NUMBERS,
RCOMP_1;
registrations RELSET_1, STRUCT_0, ORDINAL1, XREAL_0, MEMBERED, FUNCT_1,
NDIFF_1, FUNCT_2, NUMBERS, XBOOLE_0, VALUED_0, PRVECT_2, FINSEQ_2,
FINSEQ_1, CARD_3, NORMSP_0, NORMSP_1, RELAT_1, XXREAL_0, LOPBAN_1,
LOPBAN_2, PRVECT_3, FUNCOP_1, NAT_1, FINSEQ_5, XXREAL_2, RCOMP_1,
VALUED_1, FDIFF_1, NFCONT_3, FINSET_1, XCMPLX_0, PARTFUN1, CARD_1,
MONOID_0, FUNCT_4, SQUARE_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
begin :: Preliminaries
reserve j for set;
reserve p,r for Real;
reserve S,T,F for RealNormSpace;
reserve x0 for Point of S;
reserve g for PartFunc of S,T;
reserve c for constant sequence of S;
reserve R for RestFunc of S,T;
reserve G for RealNormSpace-Sequence;
reserve i for Element of dom G;
reserve f for PartFunc of product G,F;
reserve x for Element of product G;
theorem :: NDIFF_5:1
for R be Function of REAL,S
holds R is RestFunc-like
iff for r be Real st r > 0
ex d be Real st d > 0 &
for z be Real
st z <> 0 & |. z .| < d holds |.z.|"* ||. R/.z .|| < r;
theorem :: NDIFF_5:2
for R be RestFunc of S st R/.0=0.S
for e be Real st e > 0 ex d be Real st
d > 0 & for h be Real st |.h.| < d holds ||.R/.h.|| <= e*|.h.|;
theorem :: NDIFF_5:3
for R be RestFunc of S
for L be Lipschitzian LinearOperator of S,T holds
L*R is RestFunc of T;
theorem :: NDIFF_5:4
for R1 be RestFunc of S st R1/.0 = 0.S
for R2 be RestFunc of S,T st R2/.(0.S) = 0.T
for L be LinearFunc of S holds
R2*(L+R1) is RestFunc of T;
theorem :: NDIFF_5:5
for R1 be RestFunc of S st R1/.0=0.S
for R2 be RestFunc of S,T st R2/.(0.S)=0.T
for L1 be LinearFunc of S
for L2 be Lipschitzian LinearOperator of S,T holds
L2*R1 + R2*(L1+R1) is RestFunc of T;
theorem :: NDIFF_5:6
for x0 be Real
for g be PartFunc of REAL,the carrier of S st
g is_differentiable_in x0
for f be PartFunc of the carrier of S,the carrier of T st
f is_differentiable_in (g/.x0) holds
f*g is_differentiable_in x0 & diff(f*g,x0) = diff(f,g/.x0).diff(g,x0);
theorem :: NDIFF_5:7
for S be RealNormSpace,
xseq be FinSequence of S,
yseq be FinSequence of REAL st
len xseq = len yseq &
( for i be Element of NAT st i in dom xseq holds
yseq.i = ||. xseq/.i .|| )
holds ||.Sum xseq.|| <= Sum yseq;
theorem :: NDIFF_5:8
for S be RealNormSpace, x be Point of S, N1,N2 be Neighbourhood of x holds
N1/\ N2 is Neighbourhood of x;
theorem :: NDIFF_5:9
for X be non-empty FinSequence,
x be set st x in product X holds x is FinSequence;
registration
let G be RealNormSpace-Sequence;
cluster product G -> constituted-FinSeqs;
end;
definition
let G be RealLinearSpace-Sequence;
let z be Element of product carr G;
let j be Element of dom G;
redefine func z.j -> Element of G.j;
end;
theorem :: NDIFF_5:10
the carrier of product G = product carr G;
theorem :: NDIFF_5:11
for i be Element of dom G, r be set, x be Function
st r in the carrier of (G.i) & x in product carr G
holds x +* (i,r) in the carrier of product G;
definition
let G be RealNormSpace-Sequence;
attr G is non-trivial means
:: NDIFF_5:def 1
for j be Element of dom G holds G.j is non trivial;
end;
registration
cluster non-trivial for RealNormSpace-Sequence;
end;
registration
let G be non-trivial RealNormSpace-Sequence;
let i be Element of dom G;
cluster G.i -> non trivial for RealNormSpace;
end;
registration
let G be non-trivial RealNormSpace-Sequence;
cluster product G -> non trivial;
end;
theorem :: NDIFF_5:12
for G be RealNormSpace-Sequence, p,q be Point of product G,
r0,p0,q0 be Element of product carr G st p=p0 & q=q0
holds p+q = r0
iff for i be Element of dom G holds r0.i = p0.i + q0.i;
theorem :: NDIFF_5:13
for G be RealNormSpace-Sequence, p be Point of product G,
r be Real, r0,p0 be Element of product carr G
st p=p0
holds r*p = r0
iff for i be Element of dom G holds r0.i = r*(p0.i);
theorem :: NDIFF_5:14
for G be RealNormSpace-Sequence, p0 be Element of product carr G
holds 0.(product G)=p0
iff for i be Element of dom G holds p0.i = 0.(G.i);
theorem :: NDIFF_5:15
for G be RealNormSpace-Sequence, p,q be Point of product G,
r0,p0,q0 be Element of product carr G
st p=p0 & q=q0
holds p-q = r0
iff for i be Element of dom G holds r0.i = p0.i - q0.i;
begin
notation
let S be RealLinearSpace;
let p,q be Point of S;
synonym [.p,q.] for LSeg(p,q);
end;
definition
let S be RealLinearSpace;
let p,q be Point of S;
func ]. p,q .[ -> Subset of S equals
:: NDIFF_5:def 2
[.p,q.] \ {p,q};
end;
theorem :: NDIFF_5:16
for S be RealLinearSpace, p,q be Point of S st p <> q
holds ].p,q.[ = { p+t*(q-p) where t is Real : 0 < t & t < 1};
theorem :: NDIFF_5:17
for T be RealNormSpace, R be PartFunc of REAL,T
st R is total holds
R is RestFunc-like
iff for r be Real st r > 0
ex d be Real st d > 0 & for z be Real
st z <> 0 & |.z.| < d holds ( ||. R/.z .||/ |.z.| ) < r;
theorem :: NDIFF_5:18
for R be Function of REAL,REAL holds R is RestFunc-like iff
for r be Real st r > 0
ex d be Real st d > 0 & for z be Real
st z <> 0 & |.z.| < d holds (|.R.z.|/ |.z.|) < r;
theorem :: NDIFF_5:19
for S,T be RealNormSpace,
f be PartFunc of S,T, p,q be Point of S, M be Real
st [.p,q.] c= dom f
& (for x be Point of S st x in [.p,q.] holds f is_continuous_in x)
& (for x be Point of S st x in ].p,q.[ holds f is_differentiable_in x)
& (for x be Point of S st x in ].p,q.[ holds ||. diff(f,x) .|| <= M)
holds ||. f/.q - f/.p .|| <= M*||. q-p .||;
theorem :: NDIFF_5:20
for S,T be RealNormSpace, f be PartFunc of S,T,
p,q be Point of S, M be Real,
L be Point of R_NormSpace_of_BoundedLinearOperators(S,T)
st [.p,q.] c= dom f
& (for x be Point of S st x in [.p,q.] holds f is_continuous_in x)
& (for x be Point of S st x in ].p,q.[ holds f is_differentiable_in x)
& (for x be Point of S st x in ].p,q.[ holds ||. diff(f,x) - L .|| <= M)
holds ||. f/.q - f/.p -L.(q-p).|| <= M*||. q-p .||;
begin :: Partial derivative of a function of several variables
definition
let G be RealNormSpace-Sequence;
let i be Element of dom G;
func proj i -> Function of product G,G.i means
:: NDIFF_5:def 3
for x be Element of product carr G holds it.x = x.i;
end;
definition
let G be RealNormSpace-Sequence;
let i be Element of dom G;
let x be Element of product G;
func reproj(i,x) -> Function of G.i,product G means
:: NDIFF_5:def 4
for r be Element of G.i holds it.r = x +* (i,r);
end;
definition
::$CD
let G be RealNormSpace-Sequence;
let F be RealNormSpace;
let i be set;
let f be PartFunc of product G,F;
let x being Element of product G;
pred f is_partial_differentiable_in x,i means
:: NDIFF_5:def 6
f*reproj(In(i,dom G),x) is_differentiable_in proj(In(i,dom G)).x;
end;
definition
let G be RealNormSpace-Sequence;
let F be RealNormSpace;
let i be set;
let f be PartFunc of product G,F;
let x be Point of product G;
func partdiff(f,x,i)
-> Point of R_NormSpace_of_BoundedLinearOperators(G.In(i,dom G),F)
equals
:: NDIFF_5:def 7
diff(f*reproj(In(i,dom G),x),proj(In(i,dom G)).x);
end;
begin :: Linearity of Partial Differential Operator
reserve G for RealNormSpace-Sequence;
reserve F for RealNormSpace;
reserve i for Element of dom G;
reserve f,f1,f2 for PartFunc of product G, F;
reserve x for Point of product G;
reserve X for set;
definition
let G be RealNormSpace-Sequence;
let F be RealNormSpace;
let i be set;
let f be PartFunc of product G,F;
let X be set;
pred f is_partial_differentiable_on X,i means
:: NDIFF_5:def 8
X c= dom f & for x be Point of product G st x in X
holds f|X is_partial_differentiable_in x,i;
end;
theorem :: NDIFF_5:21
for xi be Element of G.i
holds ||. reproj(i,0.(product G)).xi .|| = ||.xi.||;
theorem :: NDIFF_5:22
for G be RealNormSpace-Sequence,
i be Element of dom G,
x be Point of product G,
r be Point of G.i holds
reproj(i,x).r - x = reproj(i,0.(product G)).(r - proj(i).x) &
x - reproj(i,x).r = reproj(i,0.(product G)).(proj(i).x - r);
theorem :: NDIFF_5:23
for G be RealNormSpace-Sequence,
i be Element of dom G,
x be Point of product G,
Z be Subset of product G
st Z is open & x in Z holds
ex N be Neighbourhood of proj(i).x st
for z be Point of G.i st z in N holds (reproj(i,x)).z in Z;
theorem :: NDIFF_5:24
for G be RealNormSpace-Sequence,
T be RealNormSpace,
i be set,
f be PartFunc of product G, T,
Z be Subset of product G
st Z is open holds
f is_partial_differentiable_on Z,i
iff
Z c=dom f &
for x be Point of product G st x in Z holds
f is_partial_differentiable_in x,i;
theorem :: NDIFF_5:25
for i be set st i in dom G & f is_partial_differentiable_on X,i
holds X is Subset of product G;
definition
let G be RealNormSpace-Sequence;
let S be RealNormSpace;
let i be set;
let f be PartFunc of product G, S;
let X be set;
assume f is_partial_differentiable_on X,i;
func f `partial|(X,i) -> PartFunc of product G,
R_NormSpace_of_BoundedLinearOperators(G.In(i,dom G),S) means
:: NDIFF_5:def 9
dom it = X &
for x be Point of product G st x in X holds it/.x = partdiff(f,x,i);
end;
theorem :: NDIFF_5:26
for i be set st i in dom G holds
(f1+f2)*reproj(In(i,dom G),x) = f1*reproj(In(i,dom G),x)
+f2*reproj(In(i,dom G),x)
& (f1-f2)*reproj(In(i,dom G),x) = f1*reproj(In(i,dom G),x)
-f2*reproj(In(i,dom G),x);
theorem :: NDIFF_5:27
for i be set st i in dom G holds
r(#)(f*reproj(In(i,dom G),x)) = (r(#)f)*reproj(In(i,dom G),x);
theorem :: NDIFF_5:28
for i be set st i in dom G
& f1 is_partial_differentiable_in x,i
& f2 is_partial_differentiable_in x,i
holds f1+f2 is_partial_differentiable_in x,i
& partdiff(f1+f2,x,i)=partdiff(f1,x,i)+partdiff(f2,x,i);
theorem :: NDIFF_5:29
for i be set st i in dom G
& f1 is_partial_differentiable_in x,i
& f2 is_partial_differentiable_in x,i
holds f1-f2 is_partial_differentiable_in x,i
& partdiff(f1-f2,x,i)=partdiff(f1,x,i)-partdiff(f2,x,i);
theorem :: NDIFF_5:30
for i be set st i in dom G
& f is_partial_differentiable_in x,i
holds r(#)f is_partial_differentiable_in x,i & partdiff((r(#)f),x,i)
= r*partdiff(f,x,i);
begin :: Continuously differentiable and Partial derivative
theorem :: NDIFF_5:31
||. proj(i).x .|| <= ||.x.||;
registration
let G be RealNormSpace-Sequence;
cluster -> (len G)-element for Point of product G;
end;
theorem :: NDIFF_5:32
for G be RealNormSpace-Sequence,
T be RealNormSpace,
i be set,
Z be Subset of product G,
f be PartFunc of product G,T
st Z is open holds
f is_partial_differentiable_on Z,i
iff
Z c=dom f &
for x be Point of product G st x in Z holds
f is_partial_differentiable_in x,i;
theorem :: NDIFF_5:33
for i,j be Element of dom G,
x be Point of G.i,
z be Element of product carr G
st z= reproj(i,0.(product G)).x
holds
(i = j implies z.j = x) & (i <> j implies z.j = 0.(G.j));
theorem :: NDIFF_5:34
for x,y be Point of G.i
holds reproj(i,0.(product G)).(x+y)
= reproj(i,0.(product G)).x + reproj(i,0.(product G)).y;
theorem :: NDIFF_5:35
for x,y be Point of product G
holds proj(i).(x+y) = proj(i).x + proj(i).y;
theorem :: NDIFF_5:36
for x,y be Point of G.i
holds reproj(i,0.(product G)).(x-y)
= reproj(i,0.(product G)).x - reproj(i,0.(product G)).y;
theorem :: NDIFF_5:37
for x,y be Point of product G
holds proj(i).(x-y) = proj(i).x - proj(i).y;
theorem :: NDIFF_5:38
for x be Point of G.i st x <> 0.(G.i)
holds reproj(i,0.(product G)).x <> 0.(product G);
theorem :: NDIFF_5:39
for x be Point of G.i, a be Real
holds reproj(i,0.(product G)).(a*x)
= a*(reproj(i,0.(product G)).x);
theorem :: NDIFF_5:40
for x be Point of product G,a be Real
holds proj(i).(a*x) = a*(proj(i).x);
theorem :: NDIFF_5:41
for G be RealNormSpace-Sequence,
S be RealNormSpace,
f be PartFunc of product G, S,
x be Point of product G,
i be set
st f is_differentiable_in x holds
f is_partial_differentiable_in x,i
& partdiff(f,x,i) = diff(f,x) * reproj(In(i,dom G),0.(product G));
theorem :: NDIFF_5:42
for S be RealNormSpace, h,g be FinSequence of S
st len h = len g + 1 &
(for i be Nat st i in dom g holds g/.i = h /.i - h/.(i+1)) holds
h /.1 - h/.(len h) = Sum g;
theorem :: NDIFF_5:43
for G be RealNormSpace-Sequence,
x,y be Element of product carr G, Z be set
holds x +* (y|Z) is Element of product carr G;
theorem :: NDIFF_5:44
for G be RealNormSpace-Sequence,
x,y be Point of product G,
Z,x0 be Element of product carr G,
X be set
st Z=0.(product G) & x0=x & y= Z +* (x0|X)
holds ||.y.|| <= ||.x.||;
theorem :: NDIFF_5:45
for G be RealNormSpace-Sequence,
S be RealNormSpace,
f be PartFunc of product G, S,
x,y be Point of product G
ex h be FinSequence of product G, g be FinSequence of S,
Z,y0 be Element of product carr G st
y0=y & Z = 0.(product G)
& len h = len G + 1 & len g = len G &
(for i be Nat st i in dom h holds h/.i = Z +* (y0| Seg (len G + 1-'i))) &
(for i be Nat st i in dom g holds g/.i = f/.(x+h/.i) - f/.(x+h/.(i+1))) &
(for i be Nat, hi be Point of product G st
i in dom h & h/.i= hi holds ||. hi .|| <=||. y .||) &
f /.(x+y) - f/.x = Sum g;
theorem :: NDIFF_5:46
for G be RealNormSpace-Sequence,
i be Element of dom G,
x,y be Point of product G,
xi be Point of G.i
st y = reproj(i,x).xi holds proj(i).y = xi;
theorem :: NDIFF_5:47
for G be RealNormSpace-Sequence, i be Element of dom G,
y be Point of product G, q be Point of G.i
st q = proj(i).y holds y = reproj(i,y).q;
theorem :: NDIFF_5:48
for G be RealNormSpace-Sequence,
i be Element of dom G, x,y be Point of product G,
xi be Point of G.i
st y = reproj(i,x).xi holds reproj(i,x)=reproj(i,y);
theorem :: NDIFF_5:49
for G be RealNormSpace-Sequence,
i,j be Element of dom G, x,y be Point of product G,
xi be Point of G.i
st y = reproj(i,x).xi & i <> j holds proj(j).x = proj(j).y;
theorem :: NDIFF_5:50
for G be RealNormSpace-Sequence,
F be RealNormSpace,
i be Element of dom G,
x be Point of product G,
xi be Point of G.i,
f be PartFunc of product G,F,
g be PartFunc of G.i,F
st proj(i).x=xi & g=f*reproj(i,x)
holds
diff(g,xi) = partdiff(f,x,i);
theorem :: NDIFF_5:51
for G be RealNormSpace-Sequence,
F be RealNormSpace,
f be PartFunc of product G,F,
x be Point of product G,
i be set,
M be Real,
L be Point of R_NormSpace_of_BoundedLinearOperators
(G.(In(i,dom G)),F),
p,q be Point of G.(In(i,dom G))
st i in dom G
& (for h be Point of G.(In(i,dom G)) st h in ]. p,q .[ holds
||. partdiff(f,reproj(In(i,dom G),x).h,i) - L .|| <= M)
& (for h be Point of G.(In(i,dom G)) st h in [. p,q .] holds
reproj(In(i,dom G),x).h in dom f)
& (for h be Point of G.(In(i,dom G)) st h in [. p,q .] holds
f is_partial_differentiable_in (reproj(In(i,dom G),x).h),i)
holds
||.f/.(reproj(In(i,dom G),x).q) - f/.(reproj(In(i,dom G),x).p)
- L.(q-p) .|| <= M * ||.q-p.||;
theorem :: NDIFF_5:52
for G be RealNormSpace-Sequence,
x,y,z,w be Point of product G,
i be Element of dom G,
d be Real,
p,q,r be Point of G.i
st ||. y-x .|| < d & ||. z-x .|| < d & p= proj(i).y & z=reproj(i,y).q
& r in [. p,q .] & w= reproj(i,y).r
holds ||. w-x .|| < d;
theorem :: NDIFF_5:53
for G be RealNormSpace-Sequence,
S be RealNormSpace,
f be PartFunc of product G,S,
X be Subset of product G,
x,y,z be Point of product G,
i be set,
p,q be Point of G.(In(i,dom G)),
d,r be Real
st i in dom G & X is open & x in X &
||. y-x .|| < d & ||. z-x .|| < d & X c= dom f &
(for x be Point of product G st x in X holds
f is_partial_differentiable_in x,i) &
(for z be Point of product G st ||. z-x .|| < d holds z in X) &
(for z be Point of product G st ||. z-x .|| < d
holds ||. partdiff(f,z,i) - partdiff(f,x,i).|| <=r) &
z = reproj(In(i,dom G),y).p & q = proj(In(i,dom G)).y
holds
||. f/.z - f/.y - ((partdiff(f,x,i)).(p-q)) .|| <= ||. p-q .||*r;
theorem :: NDIFF_5:54
for G be RealNormSpace-Sequence,
h be FinSequence of product G,
y,x be Point of product G,
y0,Z be Element of product carr G,
j be Element of NAT
st y=y0 & Z=0.(product G)
& len h = (len G)+1 & 1 <= j & j <= len G &
(for i be Nat st i in dom h holds h/.i=Z +* (y0| Seg (len G + 1-'i)))
holds x + h/.j = reproj(In((len G)+1-'j,dom G),(x+h/.(j+1)))
.(proj(In((len G)+1-'j,dom G)).(x+y));
theorem :: NDIFF_5:55
for G be RealNormSpace-Sequence,
h be FinSequence of product G,
y,x be Point of product G,
y0,Z be Element of product carr G,
j be Element of NAT
st y=y0 & Z=0.(product G)
& len h = (len G)+1 & 1 <= j & j <= len G &
(for i be Nat st i in dom h holds h/.i=Z +* (y0| Seg (len G + 1-'i)))
holds
(proj(In((len G)+1-'j,dom G)).(x+y))
- proj(In((len G)+1-'j,dom G)).(x+h/.(j+1))
= (proj(In((len G)+1-'j,dom G)).y);
theorem :: NDIFF_5:56
for G be RealNormSpace-Sequence,
S be RealNormSpace,
f be PartFunc of product G, S,
X be Subset of product G,
x be Point of product G
st X is open & x in X &
(for i be set st i in dom G holds
f is_partial_differentiable_on X,i & f`partial|(X,i) is_continuous_on X)
holds
f is_differentiable_in x & for h be Point of product G
ex w be FinSequence of S st
dom w = dom G &
(for i be set st i in dom G holds
w.i = partdiff(f,x,i).(proj(In(i,dom G)).h))
& diff(f,x).h = Sum w;
theorem :: NDIFF_5:57
for G be RealNormSpace-Sequence,
F be RealNormSpace,
f be PartFunc of product G, F,
X be Subset of product G
st X is open holds
(for i be set st i in dom G holds
f is_partial_differentiable_on X,i & f`partial|(X,i) is_continuous_on X)
iff
f is_differentiable_on X & f`|X is_continuous_on X;