let m, n be non zero Element of NAT ; for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m)
for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X iff ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y ) )
let f be PartFunc of (REAL m),(REAL n); for g being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m)
for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X iff ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y ) )
let g be PartFunc of (REAL-NS m),(REAL-NS n); for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m)
for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X iff ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y ) )
let X be Subset of (REAL m); for Y being Subset of (REAL-NS m)
for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X iff ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y ) )
let Y be Subset of (REAL-NS m); for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X iff ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y ) )
let i be Nat; ( 1 <= i & i <= m & X is open & g = f & X = Y implies ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X iff ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y ) ) )
assume A1:
( 1 <= i & i <= m & X is open & g = f & X = Y )
; ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X iff ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y ) )
hereby ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y implies ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) )
assume A2:
(
f is_partial_differentiable_on X,
i &
f `partial| (
X,
i)
is_continuous_on X )
;
( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y )hence
g is_partial_differentiable_on Y,
i
by A1, PDIFF_7:33;
g `partial| (Y,i) is_continuous_on Ythen A3:
dom (g `partial| (Y,i)) = Y
by PDIFF_1:def 20;
for
y0 being
Point of
(REAL-NS m) for
r being
Real st
y0 in Y &
0 < r holds
ex
s being
Real st
(
0 < s & ( for
y1 being
Point of
(REAL-NS m) st
y1 in Y &
||.(y1 - y0).|| < s holds
||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| < r ) )
proof
let y0 be
Point of
(REAL-NS m);
for r being Real st y0 in Y & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in Y & ||.(y1 - y0).|| < s holds
||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| < r ) )let r be
Real;
( y0 in Y & 0 < r implies ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in Y & ||.(y1 - y0).|| < s holds
||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| < r ) ) )
reconsider x0 =
y0 as
Element of
REAL m by REAL_NS1:def 4;
assume A4:
(
y0 in Y &
0 < r )
;
ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in Y & ||.(y1 - y0).|| < s holds
||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| < r ) )
then consider s being
Real such that A5:
(
0 < s & ( for
x1 being
Element of
REAL m st
x1 in X &
|.(x1 - x0).| < s holds
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| < r ) )
by A1, A2, PDIFF_7:38;
take
s
;
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in Y & ||.(y1 - y0).|| < s holds
||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| < r ) )
thus
0 < s
by A5;
for y1 being Point of (REAL-NS m) st y1 in Y & ||.(y1 - y0).|| < s holds
||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| < r
let y1 be
Point of
(REAL-NS m);
( y1 in Y & ||.(y1 - y0).|| < s implies ||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| < r )
reconsider x1 =
y1 as
Element of
REAL m by REAL_NS1:def 4;
assume A6:
(
y1 in Y &
||.(y1 - y0).|| < s )
;
||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| < r
then A7:
|.(x1 - x0).| < s
by REAL_NS1:1, REAL_NS1:5;
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| = ||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).||
by A4, A6, A1, A2, Th22;
hence
||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| < r
by A7, A5, A6, A1;
verum
end; hence
g `partial| (
Y,
i)
is_continuous_on Y
by A3, NFCONT_1:19;
verum
end;
assume A8:
( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y )
; ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )
then A9:
f is_partial_differentiable_on X,i
by A1, PDIFF_7:33;
then A10:
dom (f `partial| (X,i)) = X
by PDIFF_7:def 5;
for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| < r ) )
proof
let x0 be
Element of
REAL m;
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| < r ) )let r be
Real;
( x0 in X & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| < r ) ) )
reconsider y0 =
x0 as
Point of
(REAL-NS m) by REAL_NS1:def 4;
assume A11:
(
x0 in X &
0 < r )
;
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| < r ) )
then consider s being
Real such that A12:
(
0 < s & ( for
y1 being
Point of
(REAL-NS m) st
y1 in Y &
||.(y1 - y0).|| < s holds
||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| < r ) )
by A1, A8, NFCONT_1:19;
take
s
;
( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| < r ) )
thus
0 < s
by A12;
for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| < r
let x1 be
Element of
REAL m;
( x1 in X & |.(x1 - x0).| < s implies |.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| < r )
reconsider y1 =
x1 as
Element of
(REAL-NS m) by REAL_NS1:def 4;
assume A13:
(
x1 in X &
|.(x1 - x0).| < s )
;
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| < r
|.(x1 - x0).| = ||.(y1 - y0).||
by REAL_NS1:1, REAL_NS1:5;
then
||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| < r
by A12, A13, A1;
hence
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| < r
by A11, A13, A1, A9, Th22;
verum
end;
hence
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )
by A8, A10, A1, PDIFF_7:33, PDIFF_7:38; verum