begin
set W = (proj (1,1)) " ;
Lm1:
( proj (1,1) is bijective & dom (proj (1,1)) = REAL 1 & rng (proj (1,1)) = REAL & ( for x being Element of REAL holds
( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) )
Lm2:
for i, n being Element of NAT st i in Seg n holds
proj (i,n) is onto
definition
let m,
n be non
empty Element of
NAT ;
let f be
PartFunc of
(REAL m),
(REAL n);
let x be
Element of
REAL m;
assume A1:
f is_differentiable_in x
;
correctness
existence
ex b1 being Function of (REAL m),(REAL n) ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b1 = diff (g,y) );
uniqueness
for b1, b2 being Function of (REAL m),(REAL n) st ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b1 = diff (g,y) ) & ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b2 = diff (g,y) ) holds
b1 = b2;
end;
reconsider I = (proj (1,1)) " as Function of REAL,(REAL 1) by Th2;
begin
definition
let m,
n be non
empty Element of
NAT ;
let i be
Element of
NAT ;
let f be
PartFunc of
(REAL m),
(REAL n);
let x be
Element of
REAL m;
assume A1:
f is_partial_differentiable_in x,
i
;
correctness
existence
ex b1 being Element of REAL n ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b1 = (partdiff (g,y,i)) . <*1*> );
uniqueness
for b1, b2 being Element of REAL n st ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b1 = (partdiff (g,y,i)) . <*1*> ) & ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b2 = (partdiff (g,y,i)) . <*1*> ) holds
b1 = b2;
end;
begin
::
deftheorem defines
partdiff PDIFF_1:def 16 :
for m, n being non empty Element of NAT
for i, j being Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds partdiff (f,x,i,j) = diff ((((Proj (j,n)) * f) * (reproj (i,x))),((Proj (i,m)) . x));
::
deftheorem defines
partdiff PDIFF_1:def 18 :
for m, n being non empty Element of NAT
for i, j being Element of NAT
for h being PartFunc of (REAL m),(REAL n)
for z being Element of REAL m holds partdiff (h,z,i,j) = diff ((((proj (j,n)) * h) * (reproj (i,z))),((proj (i,m)) . z));
theorem
for
n,
m being non
empty Element of
NAT for
i,
j being
Element of
NAT for
f being
PartFunc of
(REAL-NS m),
(REAL-NS n) for
h being
PartFunc of
(REAL m),
(REAL n) for
x being
Point of
(REAL-NS m) for
z being
Element of
REAL m st
f = h &
x = z &
f is_partial_differentiable_in x,
i,
j holds
(partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,z,i,j))*>
definition
let m,
n be non
empty Element of
NAT ;
let i be
Element of
NAT ;
let f be
PartFunc of
(REAL-NS m),
(REAL-NS n);
let X be
set ;
assume A1:
f is_partial_differentiable_on X,
i
;
existence
ex b1 being PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) st
( dom b1 = X & ( for x being Point of (REAL-NS m) st x in X holds
b1 /. x = partdiff (f,x,i) ) )
uniqueness
for b1, b2 being PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) st dom b1 = X & ( for x being Point of (REAL-NS m) st x in X holds
b1 /. x = partdiff (f,x,i) ) & dom b2 = X & ( for x being Point of (REAL-NS m) st x in X holds
b2 /. x = partdiff (f,x,i) ) holds
b1 = b2
end;
theorem Th28:
for
n,
m being non
empty Element of
NAT for
i being
Element of
NAT for
f1,
f2 being
PartFunc of
(REAL-NS m),
(REAL-NS n) for
x being
Point of
(REAL-NS m) st
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
for
n being non
empty Element of
NAT for
i being
Element of
NAT for
g1,
g2 being
PartFunc of
(REAL n),
REAL for
y being
Element of
REAL n st
g1 is_partial_differentiable_in y,
i &
g2 is_partial_differentiable_in y,
i holds
(
g1 + g2 is_partial_differentiable_in y,
i &
partdiff (
(g1 + g2),
y,
i)
= (partdiff (g1,y,i)) + (partdiff (g2,y,i)) )
theorem Th30:
for
n,
m being non
empty Element of
NAT for
i being
Element of
NAT for
f1,
f2 being
PartFunc of
(REAL-NS m),
(REAL-NS n) for
x being
Point of
(REAL-NS m) st
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
for
n being non
empty Element of
NAT for
i being
Element of
NAT for
g1,
g2 being
PartFunc of
(REAL n),
REAL for
y being
Element of
REAL n st
g1 is_partial_differentiable_in y,
i &
g2 is_partial_differentiable_in y,
i holds
(
g1 - g2 is_partial_differentiable_in y,
i &
partdiff (
(g1 - g2),
y,
i)
= (partdiff (g1,y,i)) - (partdiff (g2,y,i)) )