let X, Y, W be RealNormSpace; for Z being Subset of [:X,Y:]
for f being PartFunc of [:X,Y:],W st Z is open holds
( f is_partial_differentiable_on`2 Z iff ( Z c= dom f & ( for x being Point of [:X,Y:] st x in Z holds
f is_partial_differentiable_in`2 x ) ) )
let Z be Subset of [:X,Y:]; for f being PartFunc of [:X,Y:],W st Z is open holds
( f is_partial_differentiable_on`2 Z iff ( Z c= dom f & ( for x being Point of [:X,Y:] st x in Z holds
f is_partial_differentiable_in`2 x ) ) )
let f be PartFunc of [:X,Y:],W; ( Z is open implies ( f is_partial_differentiable_on`2 Z iff ( Z c= dom f & ( for x being Point of [:X,Y:] st x in Z holds
f is_partial_differentiable_in`2 x ) ) ) )
assume AS:
Z is open
; ( f is_partial_differentiable_on`2 Z iff ( Z c= dom f & ( for x being Point of [:X,Y:] st x in Z holds
f is_partial_differentiable_in`2 x ) ) )
set I = (IsoCPNrSP (X,Y)) " ;
set J = IsoCPNrSP (X,Y);
set g = f * ((IsoCPNrSP (X,Y)) ");
set E = ((IsoCPNrSP (X,Y)) ") " Z;
X1:
( (IsoCPNrSP (X,Y)) " = (IsoCPNrSP (X,Y)) " & (IsoCPNrSP (X,Y)) " is one-to-one & (IsoCPNrSP (X,Y)) " is onto & ( for x being Point of X
for y being Point of Y holds ((IsoCPNrSP (X,Y)) ") . <*x,y*> = [x,y] ) & 0. [:X,Y:] = ((IsoCPNrSP (X,Y)) ") . (0. (product <*X,Y*>)) & (IsoCPNrSP (X,Y)) " is isometric )
by defISOA1, defISOA2;
X2:
( IsoCPNrSP (X,Y) is one-to-one & IsoCPNrSP (X,Y) is onto & ( for x being Point of X
for y being Point of Y holds (IsoCPNrSP (X,Y)) . (x,y) = <*x,y*> ) & 0. (product <*X,Y*>) = (IsoCPNrSP (X,Y)) . (0. [:X,Y:]) & IsoCPNrSP (X,Y) is isometric )
by defISO, ZeZe;
A2:
dom (IsoCPNrSP (X,Y)) = the carrier of [:X,Y:]
by FUNCT_2:def 1;
((IsoCPNrSP (X,Y)) ") " Z = (IsoCPNrSP (X,Y)) .: Z
by FUNCT_1:84;
then OP1:
((IsoCPNrSP (X,Y)) ") " Z is open
by AS, LM025;
hereby ( Z c= dom f & ( for x being Point of [:X,Y:] st x in Z holds
f is_partial_differentiable_in`2 x ) implies f is_partial_differentiable_on`2 Z )
assume
f is_partial_differentiable_on`2 Z
;
( Z c= dom f & ( for x being Point of [:X,Y:] st x in Z holds
f is_partial_differentiable_in`2 x ) )then P2:
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2
by LM300;
then
((IsoCPNrSP (X,Y)) ") " Z c= ((IsoCPNrSP (X,Y)) ") " (dom f)
by RELAT_1:147;
hence
Z c= dom f
by X1, FUNCT_1:88;
for x being Point of [:X,Y:] st x in Z holds
f is_partial_differentiable_in`2 xthus
for
x being
Point of
[:X,Y:] st
x in Z holds
f is_partial_differentiable_in`2 x
verumproof
let z be
Point of
[:X,Y:];
( z in Z implies f is_partial_differentiable_in`2 z )
assume A4:
z in Z
;
f is_partial_differentiable_in`2 z
set w =
(IsoCPNrSP (X,Y)) . z;
((IsoCPNrSP (X,Y)) ") . ((IsoCPNrSP (X,Y)) . z) = z
by A2, FUNCT_1:34;
then
(IsoCPNrSP (X,Y)) . z in ((IsoCPNrSP (X,Y)) ") " Z
by FUNCT_2:38, A4;
then
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,2
by OP1, P2, NDIFF_5:24;
hence
f is_partial_differentiable_in`2 z
by LM200;
verum
end;
end;
assume P1:
( Z c= dom f & ( for x being Point of [:X,Y:] st x in Z holds
f is_partial_differentiable_in`2 x ) )
; f is_partial_differentiable_on`2 Z
then
((IsoCPNrSP (X,Y)) ") " Z c= ((IsoCPNrSP (X,Y)) ") " (dom f)
by RELAT_1:143;
then P3:
((IsoCPNrSP (X,Y)) ") " Z c= dom (f * ((IsoCPNrSP (X,Y)) "))
by RELAT_1:147;
for w being Point of (product <*X,Y*>) st w in ((IsoCPNrSP (X,Y)) ") " Z holds
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in w,2
proof
let w be
Point of
(product <*X,Y*>);
( w in ((IsoCPNrSP (X,Y)) ") " Z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in w,2 )
assume A4:
w in ((IsoCPNrSP (X,Y)) ") " Z
;
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in w,2
consider z being
Point of
[:X,Y:] such that F4:
w = (IsoCPNrSP (X,Y)) . z
by X2, FUNCT_2:113;
((IsoCPNrSP (X,Y)) ") . w = z
by A2, F4, FUNCT_1:34;
then
z in Z
by A4, FUNCT_2:38;
hence
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in w,2
by F4, P1, LM200;
verum
end;
then
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2
by NDIFF_5:24, P3, OP1;
hence
f is_partial_differentiable_on`2 Z
by LM300; verum