let m be non zero Element of NAT ; for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for i being Nat st X is open & 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) ) )
let X be Subset of (REAL m); for f being PartFunc of (REAL m),REAL
for i being Nat st X is open & 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) ) )
let f be PartFunc of (REAL m),REAL; for i being Nat st X is open & 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) ) )
let i be Nat; ( X is open & 1 <= i & i <= m implies ( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) ) ) )
assume that
A1:
X is open
and
A2:
( 1 <= i & i <= m )
; ( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) ) )
thus
( f is_partial_differentiable_on X,i implies ( X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) ) )
( X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) implies f is_partial_differentiable_on X,i )proof
assume A3:
f is_partial_differentiable_on X,
i
;
( X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) )
hence A4:
X c= dom f
;
for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i
let nx0 be
Element of
REAL m;
( nx0 in X implies f is_partial_differentiable_in nx0,i )
reconsider x0 =
(proj (i,m)) . nx0 as
Element of
REAL ;
assume A5:
nx0 in X
;
f is_partial_differentiable_in nx0,i
then
f | X is_partial_differentiable_in nx0,
i
by A3;
then consider N0 being
Neighbourhood of
x0 such that A6:
N0 c= dom ((f | X) * (reproj (i,nx0)))
and A7:
ex
L being
LinearFunc ex
R being
RestFunc st
for
x being
Real st
x in N0 holds
(((f | X) * (reproj (i,nx0))) . x) - (((f | X) * (reproj (i,nx0))) . x0) = (L . (x - x0)) + (R . (x - x0))
by FDIFF_1:def 4;
consider L being
LinearFunc,
R being
RestFunc such that A8:
for
x being
Real st
x in N0 holds
(((f | X) * (reproj (i,nx0))) . x) - (((f | X) * (reproj (i,nx0))) . x0) = (L . (x - x0)) + (R . (x - x0))
by A7;
consider N1 being
Neighbourhood of
x0 such that A9:
for
x being
Element of
REAL st
x in N1 holds
(reproj (i,nx0)) . x in X
by A1, A2, A5, Lm2;
consider N being
Neighbourhood of
x0 such that A11:
(
N c= N0 &
N c= N1 )
by RCOMP_1:17;
(f | X) * (reproj (i,nx0)) c= f * (reproj (i,nx0))
by RELAT_1:29, RELAT_1:59;
then
dom ((f | X) * (reproj (i,nx0))) c= dom (f * (reproj (i,nx0)))
by RELAT_1:11;
then A13:
N c= dom (f * (reproj (i,nx0)))
by A6, A11;
now for xx being Real st xx in N holds
((f * (reproj (i,nx0))) . xx) - ((f * (reproj (i,nx0))) . x0) = (L . (xx - x0)) + (R . (xx - x0))let xx be
Real;
( xx in N implies ((f * (reproj (i,nx0))) . xx) - ((f * (reproj (i,nx0))) . x0) = (L . (xx - x0)) + (R . (xx - x0)) )reconsider x =
xx as
Element of
REAL by XREAL_0:def 1;
assume A14:
xx in N
;
((f * (reproj (i,nx0))) . xx) - ((f * (reproj (i,nx0))) . x0) = (L . (xx - x0)) + (R . (xx - x0))then
(reproj (i,nx0)) . x in dom (f | X)
by A10, A11;
then A15:
(
(reproj (i,nx0)) . x in dom f &
(reproj (i,nx0)) . x in X )
by RELAT_1:57;
(reproj (i,nx0)) . x0 in dom (f | X)
by A10, RCOMP_1:16;
then A16:
(
(reproj (i,nx0)) . x0 in dom f &
(reproj (i,nx0)) . x0 in X )
by RELAT_1:57;
A17:
dom (reproj (i,nx0)) = REAL
by FUNCT_2:def 1;
then A18:
((f | X) * (reproj (i,nx0))) . x =
(f | X) . ((reproj (i,nx0)) . x)
by FUNCT_1:13
.=
f . ((reproj (i,nx0)) . x)
by A15, FUNCT_1:49
.=
(f * (reproj (i,nx0))) . x
by A17, FUNCT_1:13
;
((f | X) * (reproj (i,nx0))) . x0 =
(f | X) . ((reproj (i,nx0)) . x0)
by A17, FUNCT_1:13
.=
f . ((reproj (i,nx0)) . x0)
by A16, FUNCT_1:49
.=
(f * (reproj (i,nx0))) . x0
by A17, FUNCT_1:13
;
hence
((f * (reproj (i,nx0))) . xx) - ((f * (reproj (i,nx0))) . x0) = (L . (xx - x0)) + (R . (xx - x0))
by A8, A14, A11, A18;
verum end;
hence
f is_partial_differentiable_in nx0,
i
by A13, FDIFF_1:def 4;
verum
end;
assume that
A19:
X c= dom f
and
A20:
for nx being Element of REAL m st nx in X holds
f is_partial_differentiable_in nx,i
; f is_partial_differentiable_on X,i
thus
X c= dom f
by A19; PDIFF_9:def 5 for x being Element of REAL m st x in X holds
f | X is_partial_differentiable_in x,i
now for nx0 being Element of REAL m st nx0 in X holds
f | X is_partial_differentiable_in nx0,ilet nx0 be
Element of
REAL m;
( nx0 in X implies f | X is_partial_differentiable_in nx0,i )assume A21:
nx0 in X
;
f | X is_partial_differentiable_in nx0,ithen A22:
f is_partial_differentiable_in nx0,
i
by A20;
reconsider x0 =
(proj (i,m)) . nx0 as
Element of
REAL ;
consider N0 being
Neighbourhood of
x0 such that
N0 c= dom (f * (reproj (i,nx0)))
and A23:
ex
L being
LinearFunc ex
R being
RestFunc st
for
x being
Real st
x in N0 holds
((f * (reproj (i,nx0))) . x) - ((f * (reproj (i,nx0))) . x0) = (L . (x - x0)) + (R . (x - x0))
by FDIFF_1:def 4, A22;
consider N1 being
Neighbourhood of
x0 such that A24:
for
x being
Element of
REAL st
x in N1 holds
(reproj (i,nx0)) . x in X
by A1, A2, A21, Lm2;
A26:
N1 c= dom ((f | X) * (reproj (i,nx0)))
consider N being
Neighbourhood of
x0 such that A30:
(
N c= N0 &
N c= N1 )
by RCOMP_1:17;
A31:
N c= dom ((f | X) * (reproj (i,nx0)))
by A30, A26;
consider L being
LinearFunc,
R being
RestFunc such that A32:
for
x being
Real st
x in N0 holds
((f * (reproj (i,nx0))) . x) - ((f * (reproj (i,nx0))) . x0) = (L . (x - x0)) + (R . (x - x0))
by A23;
now for xx being Real st xx in N holds
(((f | X) * (reproj (i,nx0))) . xx) - (((f | X) * (reproj (i,nx0))) . x0) = (L . (xx - x0)) + (R . (xx - x0))let xx be
Real;
( xx in N implies (((f | X) * (reproj (i,nx0))) . xx) - (((f | X) * (reproj (i,nx0))) . x0) = (L . (xx - x0)) + (R . (xx - x0)) )assume A33:
xx in N
;
(((f | X) * (reproj (i,nx0))) . xx) - (((f | X) * (reproj (i,nx0))) . x0) = (L . (xx - x0)) + (R . (xx - x0))reconsider x =
xx as
Element of
REAL by XREAL_0:def 1;
A34:
dom (reproj (i,nx0)) = REAL
by FUNCT_2:def 1;
(reproj (i,nx0)) . x in dom (f | X)
by A25, A33, A30;
then A35:
(reproj (i,nx0)) . x in (dom f) /\ X
by RELAT_1:61;
(reproj (i,nx0)) . x0 in dom (f | X)
by A25, RCOMP_1:16;
then A36:
(reproj (i,nx0)) . x0 in (dom f) /\ X
by RELAT_1:61;
A37:
((f | X) * (reproj (i,nx0))) . x =
(f | X) . ((reproj (i,nx0)) /. x)
by A34, FUNCT_1:13
.=
f . ((reproj (i,nx0)) . x)
by A35, FUNCT_1:48
.=
(f * (reproj (i,nx0))) . x
by A34, FUNCT_1:13
;
((f | X) * (reproj (i,nx0))) . x0 =
(f | X) . ((reproj (i,nx0)) . x0)
by A34, FUNCT_1:13
.=
f . ((reproj (i,nx0)) . x0)
by A36, FUNCT_1:48
.=
(f * (reproj (i,nx0))) . x0
by A34, FUNCT_1:13
;
hence
(((f | X) * (reproj (i,nx0))) . xx) - (((f | X) * (reproj (i,nx0))) . x0) = (L . (xx - x0)) + (R . (xx - x0))
by A37, A33, A32, A30;
verum end; hence
f | X is_partial_differentiable_in nx0,
i
by A31, FDIFF_1:def 4;
verum end;
hence
for x being Element of REAL m st x in X holds
f | X is_partial_differentiable_in x,i
; verum