let m be non zero Nat; for f being PartFunc of (REAL m),REAL
for X being Subset of (REAL m)
for x, y, z being Element of REAL m
for i being Nat
for d, p, q being Real st 1 <= i & i <= m & X is open & x in X & |.(y - x).| < d & |.(z - x).| < d & X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) & 0 < d & ( for z being Element of REAL m st |.(z - x).| < d holds
z in X ) & z = (reproj (i,y)) . p & q = (proj (i,m)) . y holds
ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) )
let f be PartFunc of (REAL m),REAL; for X being Subset of (REAL m)
for x, y, z being Element of REAL m
for i being Nat
for d, p, q being Real st 1 <= i & i <= m & X is open & x in X & |.(y - x).| < d & |.(z - x).| < d & X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) & 0 < d & ( for z being Element of REAL m st |.(z - x).| < d holds
z in X ) & z = (reproj (i,y)) . p & q = (proj (i,m)) . y holds
ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) )
let X be Subset of (REAL m); for x, y, z being Element of REAL m
for i being Nat
for d, p, q being Real st 1 <= i & i <= m & X is open & x in X & |.(y - x).| < d & |.(z - x).| < d & X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) & 0 < d & ( for z being Element of REAL m st |.(z - x).| < d holds
z in X ) & z = (reproj (i,y)) . p & q = (proj (i,m)) . y holds
ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) )
let x, y, z be Element of REAL m; for i being Nat
for d, p, q being Real st 1 <= i & i <= m & X is open & x in X & |.(y - x).| < d & |.(z - x).| < d & X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) & 0 < d & ( for z being Element of REAL m st |.(z - x).| < d holds
z in X ) & z = (reproj (i,y)) . p & q = (proj (i,m)) . y holds
ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) )
let i be Nat; for d, p, q being Real st 1 <= i & i <= m & X is open & x in X & |.(y - x).| < d & |.(z - x).| < d & X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) & 0 < d & ( for z being Element of REAL m st |.(z - x).| < d holds
z in X ) & z = (reproj (i,y)) . p & q = (proj (i,m)) . y holds
ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) )
let d, p, q be Real; ( 1 <= i & i <= m & X is open & x in X & |.(y - x).| < d & |.(z - x).| < d & X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) & 0 < d & ( for z being Element of REAL m st |.(z - x).| < d holds
z in X ) & z = (reproj (i,y)) . p & q = (proj (i,m)) . y implies ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) ) )
assume A1:
( 1 <= i & i <= m & X is open & x in X & |.(y - x).| < d & |.(z - x).| < d & X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) & 0 < d & ( for z being Element of REAL m st |.(z - x).| < d holds
z in X ) & z = (reproj (i,y)) . p & q = (proj (i,m)) . y )
; ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) )
then A2:
p = (proj (i,m)) . z
by Th39;
reconsider yi = y . i as Element of REAL by XREAL_0:def 1;
(reproj (i,y)) . q = (reproj (i,y)) . (y . i)
by A1, PDIFF_1:def 1;
then
(reproj (i,y)) . q = Replace (y,i,yi)
by PDIFF_1:def 5;
then A3:
y = (reproj (i,y)) . q
by FUNCT_7:35;
per cases
( q <= p or p < q )
;
suppose A4:
q <= p
;
ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) )A5:
for
h being
Element of
REAL st
h in [.q,p.] holds
(reproj (i,y)) . h in X
then A6:
for
h being
Real st
h in [.q,p.] holds
(reproj (i,y)) . h in dom f
by A1;
reconsider p =
p,
q =
q as
Real ;
for
h being
Element of
REAL st
h in [.q,p.] holds
f is_partial_differentiable_in (reproj (i,y)) . h,
i
by A1, A5;
then consider r being
Real,
w being
Element of
REAL m such that A7:
(
r in [.q,p.] &
w = (reproj (i,y)) . r &
(f /. ((reproj (i,y)) . p)) - (f /. ((reproj (i,y)) . q)) = (p - q) * (partdiff (f,w,i)) )
by Th43, A1, A4, A6;
A8:
|.(w - x).| < d
by A7, A1, Th44;
then
f is_partial_differentiable_in w,
i
by A1;
hence
ex
w being
Element of
REAL m st
(
|.(w - x).| < d &
f is_partial_differentiable_in w,
i &
(f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) )
by A7, A3, A1, A8;
verum end; suppose A9:
p < q
;
ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) )reconsider p =
p as
Element of
REAL by XREAL_0:def 1;
reconsider mm =
m as
Element of
NAT by ORDINAL1:def 12;
A10:
dom y = Seg m
by FINSEQ_1:89;
then A11:
(
i in dom y &
len y = mm )
by A1, FINSEQ_1:def 3;
then
len (Replace (y,i,p)) = m
by FINSEQ_7:5;
then A12:
dom y = dom (Replace (y,i,p))
by A10, FINSEQ_1:def 3;
z = Replace (
y,
i,
p)
by A1, PDIFF_1:def 5;
then
z . i = (Replace (y,i,p)) /. i
by A11, A12, PARTFUN1:def 6;
then A13:
z . i = p
by A1, A11, FINSEQ_7:8;
A14:
y = (reproj (i,z)) . q
by A1, Th40, A3;
A15:
for
h being
Element of
REAL st
h in [.p,q.] holds
(reproj (i,z)) . h in X
proof
let h be
Element of
REAL ;
( h in [.p,q.] implies (reproj (i,z)) . h in X )
assume
h in [.p,q.]
;
(reproj (i,z)) . h in X
then
|.(((reproj (i,z)) . h) - x).| < d
by A2, A14, A1, Th44;
then
(reproj (i,z)) . h in X
by A1;
hence
(reproj (i,z)) . h in X
;
verum
end; A16:
for
h being
Real st
h in [.p,q.] holds
(reproj (i,z)) . h in dom f
by A15, A1;
for
h being
Element of
REAL st
h in [.p,q.] holds
f is_partial_differentiable_in (reproj (i,z)) . h,
i
by A15, A1;
then consider r being
Real,
w being
Element of
REAL m such that A17:
(
r in [.p,q.] &
w = (reproj (i,z)) . r &
(f /. ((reproj (i,z)) . q)) - (f /. ((reproj (i,z)) . p)) = (q - p) * (partdiff (f,w,i)) )
by Th43, A1, A9, A16;
A18:
|.(w - x).| < d
by A2, A14, A17, A1, Th44;
then A19:
f is_partial_differentiable_in w,
i
by A1;
reconsider zi =
z . i as
Real ;
(reproj (i,z)) . p = Replace (
z,
i,
zi)
by A13, PDIFF_1:def 5;
then
(f /. y) - (f /. z) = (q - p) * (partdiff (f,w,i))
by A14, A17, FUNCT_7:35;
then
(f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i))
;
hence
ex
w being
Element of
REAL m st
(
|.(w - x).| < d &
f is_partial_differentiable_in w,
i &
(f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) )
by A18, A19;
verum end; end;