:: Isometric Differentiable Functions on Real Normed Space
:: by Yuichi Futa , Noboru Endou and Yasunari Shidama
::
:: Received December 31, 2013
:: Copyright (c) 2013-2021 Association of Mizar Users

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

theorem FX1: :: NDIFF_7:1

for X being set
for I, f being Function holds (f | X) * I = (f * I) | (I " X)

proof end;

theorem LM001: :: NDIFF_7:2

for S, T being RealNormSpace
for L being LinearOperator of S,T
for x, y being Point of S holds (L . x) - (L . y) = L . (x - y)

proof end;

theorem Th26: :: NDIFF_7:3

for X, Y, W being RealNormSpace
for I being Function of X,Y
for f1, f2 being PartFunc of Y,W holds
( (f1 + f2) * I = (f1 * I) + (f2 * I) & (f1 - f2) * I = (f1 * I) - (f2 * I) )

proof end;

theorem Th27: :: NDIFF_7:4

for X, Y, W being RealNormSpace
for I being Function of X,Y
for f being PartFunc of Y,W
for r being Real holds r (#) (f * I) = (r (#) f) * I

proof end;

theorem LM030: :: NDIFF_7:5

for S, T, W being RealNormSpace
for f being PartFunc of T,W
for g being Function of S,T
for x being Point of S st x in dom g & g /. x in dom f & g is_continuous_in x & f is_continuous_in g /. x holds
f * g is_continuous_in x

proof end;

definition

let X, Y be RealNormSpace;
let x be Element of [:X,Y:];

func reproj1 x -> Function of X,[:X,Y:] means :Defrep1: :: NDIFF_7:def 1
for r being Element of X holds it . r = [r,(x `2)];

existence
ex b₁ being Function of X,[:X,Y:] st
for r being Element of X holds b₁ . r = [r,(x `2)]

proof end;

uniqueness
for b₁, b₂ being Function of X,[:X,Y:] st ( for r being Element of X holds b₁ . r = [r,(x `2)] ) & ( for r being Element of X holds b<sub>2</sub> . r = [r,(x `2)] ) holds
b₁ = b₂

proof end;

func reproj2 x -> Function of Y,[:X,Y:] means :Defrep2: :: NDIFF_7:def 2
for r being Element of Y holds it . r = [(x `1),r];

existence
ex b₁ being Function of Y,[:X,Y:] st
for r being Element of Y holds b₁ . r = [(x `1),r]

proof end;

uniqueness
for b₁, b₂ being Function of Y,[:X,Y:] st ( for r being Element of Y holds b₁ . r = [(x `1),r] ) & ( for r being Element of Y holds b<sub>2</sub> . r = [(x `1),r] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Defrep1 defines reproj1 NDIFF_7:def 1 :
for X, Y being RealNormSpace
for x being Element of [:X,Y:]
for b₄ being Function of X,[:X,Y:] holds
( b₄ = reproj1 x iff for r being Element of X holds b₄ . r = [r,(x `2)] );

:: deftheorem Defrep2 defines reproj2 NDIFF_7:def 2 :
for X, Y being RealNormSpace
for x being Element of [:X,Y:]
for b₄ being Function of Y,[:X,Y:] holds
( b₄ = reproj2 x iff for r being Element of Y holds b₄ . r = [(x `1),r] );

theorem LM010: :: NDIFF_7:6

for S, T being RealNormSpace
for I being LinearOperator of S,T
for x being Point of S st I is isometric holds
I is_continuous_in x

proof end;

theorem LMMAZU: :: NDIFF_7:7

for S, T being RealNormSpace
for f being LinearOperator of S,T holds
( f is isometric iff for x being Element of S holds ||.(f . x).|| = ||.x.|| )

proof end;

theorem LM015: :: NDIFF_7:8

for S, T being RealNormSpace
for I being LinearOperator of S,T
for Z being Subset of S st I is isometric holds
I is_continuous_on Z

proof end;

theorem LM020: :: NDIFF_7:9

for S, T being RealNormSpace
for I being LinearOperator of S,T st I is one-to-one & I is onto & I is isometric holds
ex J being LinearOperator of T,S st
( J = I " & J is one-to-one & J is onto & J is isometric )

proof end;

theorem LM021: :: NDIFF_7:10

for S, T being RealNormSpace
for I being LinearOperator of S,T
for s1 being sequence of S st I is isometric & s1 is convergent holds
( I * s1 is convergent & lim (I * s1) = I . (lim s1) )

proof end;

theorem LM022: :: NDIFF_7:11

for S, T being RealNormSpace
for I being LinearOperator of S,T
for s1 being sequence of S st I is one-to-one & I is onto & I is isometric holds
( s1 is convergent iff I * s1 is convergent )

proof end;

LM023: for S, T being RealNormSpace
for I being LinearOperator of S,T
for Z being Subset of S st I is one-to-one & I is onto & I is isometric & Z is closed holds
I .: Z is closed

proof end;

theorem LM024: :: NDIFF_7:12

for S, T being RealNormSpace
for I being LinearOperator of S,T
for Z being Subset of S st I is one-to-one & I is onto & I is isometric holds
( Z is closed iff I .: Z is closed )

proof end;

theorem LM025: :: NDIFF_7:13

for S, T being RealNormSpace
for I being LinearOperator of S,T
for Z being Subset of S st I is one-to-one & I is onto & I is isometric holds
( Z is open iff I .: Z is open )

proof end;

LM026: for S, T being RealNormSpace
for I being LinearOperator of S,T
for Z being Subset of S st I is isometric & Z is compact holds
I .: Z is compact

proof end;

theorem :: NDIFF_7:14

for S, T being RealNormSpace
for I being LinearOperator of S,T
for Z being Subset of S st I is one-to-one & I is onto & I is isometric holds
( Z is compact iff I .: Z is compact )

proof end;

theorem LM040: :: NDIFF_7:15

for S, T, W being RealNormSpace
for f being PartFunc of T,W
for I being LinearOperator of S,T st I is one-to-one & I is onto & I is isometric holds
for x being Point of S st I . x in dom f holds
( f * I is_continuous_in x iff f is_continuous_in I . x )

proof end;

theorem LM045: :: NDIFF_7:16

for S, T, W being RealNormSpace
for f being PartFunc of T,W
for I being LinearOperator of S,T
for X being set st X c= the carrier of T & I is one-to-one & I is onto & I is isometric holds
( f is_continuous_on X iff f * I is_continuous_on I " X )

proof end;

definition

let X, Y be RealNormSpace;

func IsoCPNrSP (X,Y) -> LinearOperator of [:X,Y:],(product <*X,Y*>) means :defISO: :: NDIFF_7:def 3
for x being Point of X
for y being Point of Y holds it . (x,y) = <*x,y*>;

existence
ex b₁ being LinearOperator of [:X,Y:],(product <*X,Y*>) st
for x being Point of X
for y being Point of Y holds b₁ . (x,y) = <*x,y*>

proof end;

uniqueness
for b₁, b₂ being LinearOperator of [:X,Y:],(product <*X,Y*>) st ( for x being Point of X
for y being Point of Y holds b₁ . (x,y) = <*x,y*> ) & ( for x being Point of X
for y being Point of Y holds b₂ . (x,y) = <*x,y*> ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defISO defines IsoCPNrSP NDIFF_7:def 3 :
for X, Y being RealNormSpace
for b₃ being LinearOperator of [:X,Y:],(product <*X,Y*>) holds
( b₃ = IsoCPNrSP (X,Y) iff for x being Point of X
for y being Point of Y holds b₃ . (x,y) = <*x,y*> );

theorem ZeZe: :: NDIFF_7:17

for X, Y being RealNormSpace holds 0. (product <*X,Y*>) = (IsoCPNrSP (X,Y)) . (0. [:X,Y:])

proof end;

registration

let X, Y be RealNormSpace;

cluster IsoCPNrSP (X,Y) -> one-to-one onto isometric ;

correctness
coherence
( IsoCPNrSP (X,Y) is one-to-one & IsoCPNrSP (X,Y) is onto & IsoCPNrSP (X,Y) is isometric );

proof end;

end;

registration

let X, Y be RealNormSpace;

cluster Relation-like the carrier of [:X,Y:] -defined the carrier of (product <*X,Y*>) -valued non empty Function-like one-to-one total quasi_total onto V152([:X,Y:], product <*X,Y*>) V153([:X,Y:], product <*X,Y*>) isometric for Element of bool [: the carrier of [:X,Y:], the carrier of (product <*X,Y*>):];

correctness
existence
ex b₁ being LinearOperator of [:X,Y:],(product <*X,Y*>) st
( b₁ is one-to-one & b₁ is onto & b₁ is isometric );

proof end;

end;

definition

let X, Y be RealNormSpace;
let f be one-to-one onto isometric LinearOperator of [:X,Y:],(product <*X,Y*>);
:: original: "
redefine func f " -> LinearOperator of (product <*X,Y*>),[:X,Y:];
correctness
coherence
f " is LinearOperator of (product <*X,Y*>),[:X,Y:];

proof end;

end;

registration

let X, Y be RealNormSpace;
let f be one-to-one onto isometric LinearOperator of [:X,Y:],(product <*X,Y*>);

cluster f " -> one-to-one onto isometric for LinearOperator of (product <*X,Y*>),[:X,Y:];

correctness
coherence
for b₁ being LinearOperator of (product <*X,Y*>),[:X,Y:] st b₁ = f " holds
( b₁ is one-to-one & b₁ is onto & b₁ is isometric );

proof end;

end;

registration

let X, Y be RealNormSpace;

cluster Relation-like the carrier of (product <*X,Y*>) -defined the carrier of [:X,Y:] -valued non empty Function-like one-to-one total quasi_total onto V152( product <*X,Y*>,[:X,Y:]) V153( product <*X,Y*>,[:X,Y:]) isometric for Element of bool [: the carrier of (product <*X,Y*>), the carrier of [:X,Y:]:];

correctness
existence
ex b₁ being LinearOperator of (product <*X,Y*>),[:X,Y:] st
( b₁ is one-to-one & b₁ is onto & b₁ is isometric );

proof end;

end;

theorem defISOA1: :: NDIFF_7:18

for X, Y being RealNormSpace
for x being Point of X
for y being Point of Y holds ((IsoCPNrSP (X,Y)) ") . <*x,y*> = [x,y]

proof end;

theorem defISOA2: :: NDIFF_7:19

for X, Y being RealNormSpace holds ((IsoCPNrSP (X,Y)) ") . (0. (product <*X,Y*>)) = 0. [:X,Y:]

proof end;

theorem :: NDIFF_7:20

for X, Y being RealNormSpace
for Z being Subset of [:X,Y:] holds IsoCPNrSP (X,Y) is_continuous_on Z by LM015;

theorem :: NDIFF_7:21

for X, Y being RealNormSpace
for Z being Subset of (product <*X,Y*>) holds (IsoCPNrSP (X,Y)) " is_continuous_on Z by LM015;

theorem LMX00: :: NDIFF_7:22

for S, T, W being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedLinearOperators (S,W))
for g being Point of (R_NormSpace_of_BoundedLinearOperators (T,W))
for I being LinearOperator of S,T st I is one-to-one & I is onto & I is isometric & f = g * I holds
||.f.|| = ||.g.||

proof end;

registration

let S, T be RealNormSpace;

cluster Function-like quasi_total V152(S,T) V153(S,T) isometric -> Lipschitzian for Element of bool [: the carrier of S, the carrier of T:];

coherence
for b₁ being LinearOperator of S,T st b₁ is isometric holds
b₁ is Lipschitzian

proof end;

end;

theorem :: NDIFF_7:23

for G being RealNormSpace-Sequence
for F being RealNormSpace
for i being set
for f, g being PartFunc of (product G),F
for X being Subset of (product G) st X is open & i in dom G & f is_partial_differentiable_on X,i & g is_partial_differentiable_on X,i holds
( f + g is_partial_differentiable_on X,i & (f + g) `partial| (X,i) = (f `partial| (X,i)) + (g `partial| (X,i)) )

proof end;

theorem :: NDIFF_7:24

for G being RealNormSpace-Sequence
for F being RealNormSpace
for i being set
for f, g being PartFunc of (product G),F
for X being Subset of (product G) st X is open & i in dom G & f is_partial_differentiable_on X,i & g is_partial_differentiable_on X,i holds
( f - g is_partial_differentiable_on X,i & (f - g) `partial| (X,i) = (f `partial| (X,i)) - (g `partial| (X,i)) )

proof end;

theorem :: NDIFF_7:25

for G being RealNormSpace-Sequence
for F being RealNormSpace
for i being set
for f being PartFunc of (product G),F
for r being Real
for X being Subset of (product G) st X is open & i in dom G & f is_partial_differentiable_on X,i holds
( r (#) f is_partial_differentiable_on X,i & (r (#) f) `partial| (X,i) = r (#) (f `partial| (X,i)) )

proof end;

theorem LM090: :: NDIFF_7:26

for S, T being RealNormSpace
for L being Lipschitzian LinearOperator of S,T
for x0 being Point of S holds
( L is_differentiable_in x0 & diff (L,x0) = L )

proof end;

theorem LM120: :: NDIFF_7:27

for S, T, W being RealNormSpace
for f being PartFunc of T,W
for I being Lipschitzian LinearOperator of S,T
for I0 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) st I0 = I holds
for x being Point of S st f is_differentiable_in I . x holds
( f * I is_differentiable_in x & diff ((f * I),x) = (diff (f,(I . x))) * I0 )

proof end;

theorem LM150: :: NDIFF_7:28

for S, T, W being RealNormSpace
for f being PartFunc of T,W
for I being LinearOperator of S,T st I is one-to-one & I is onto & I is isometric holds
for x being Point of S holds
( f * I is_differentiable_in x iff f is_differentiable_in I . x )

proof end;

theorem LM155: :: NDIFF_7:29

for S, T, W being RealNormSpace
for f being PartFunc of T,W
for I being LinearOperator of S,T
for X being set st X c= the carrier of T & I is one-to-one & I is onto & I is isometric holds
( f is_differentiable_on X iff f * I is_differentiable_on I " X )

proof end;

theorem :: NDIFF_7:30

for W, X, Y being RealNormSpace
for f being PartFunc of (product <*X,Y*>),W
for D being Subset of (product <*X,Y*>) st f is_differentiable_on D holds
for z being Point of (product <*X,Y*>) st z in dom (f `| D) holds
(f `| D) . z = (((f * (IsoCPNrSP (X,Y))) `| ((IsoCPNrSP (X,Y)) " D)) /. (((IsoCPNrSP (X,Y)) ") . z)) * ((IsoCPNrSP (X,Y)) ")

proof end;

theorem LM166: :: NDIFF_7:31

for W, X, Y being RealNormSpace
for f being PartFunc of [:X,Y:],W
for D being Subset of [:X,Y:] st f is_differentiable_on D holds
for z being Point of [:X,Y:] st z in dom (f `| D) holds
(f `| D) . z = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " D)) /. ((IsoCPNrSP (X,Y)) . z)) * (((IsoCPNrSP (X,Y)) ") ")

proof end;

theorem LM180: :: NDIFF_7:32

for X, Y being RealNormSpace
for z being Point of [:X,Y:] holds
( reproj1 z = ((IsoCPNrSP (X,Y)) ") * (reproj ((In (1,(dom <*X,Y*>))),((IsoCPNrSP (X,Y)) . z))) & reproj2 z = ((IsoCPNrSP (X,Y)) ") * (reproj ((In (2,(dom <*X,Y*>))),((IsoCPNrSP (X,Y)) . z))) )

proof end;

definition

let X, Y be RealNormSpace;
let z be Point of [:X,Y:];
:: original: `1
redefine func z `1 -> Point of X;
correctness
coherence
z `1 is Point of X;

proof end;

:: original: `2
redefine func z `2 -> Point of Y;
correctness
coherence
z `2 is Point of Y;

proof end;

end;

definition

let X, Y, W be RealNormSpace;
let z be Point of [:X,Y:];
let f be PartFunc of [:X,Y:],W;

pred f is_partial_differentiable_in`1 z means :: NDIFF_7:def 4
f * (reproj1 z) is_differentiable_in z `1 ;

pred f is_partial_differentiable_in`2 z means :: NDIFF_7:def 5
f * (reproj2 z) is_differentiable_in z `2 ;

end;

:: deftheorem defines is_partial_differentiable_in`1 NDIFF_7:def 4 :
for X, Y, W being RealNormSpace
for z being Point of [:X,Y:]
for f being PartFunc of [:X,Y:],W holds
( f is_partial_differentiable_in`1 z iff f * (reproj1 z) is_differentiable_in z `1 );

:: deftheorem defines is_partial_differentiable_in`2 NDIFF_7:def 5 :
for X, Y, W being RealNormSpace
for z being Point of [:X,Y:]
for f being PartFunc of [:X,Y:],W holds
( f is_partial_differentiable_in`2 z iff f * (reproj2 z) is_differentiable_in z `2 );

theorem LM190: :: NDIFF_7:33

for X, Y being RealNormSpace
for z being Point of [:X,Y:] holds
( z `1 = (proj (In (1,(dom <*X,Y*>)))) . ((IsoCPNrSP (X,Y)) . z) & z `2 = (proj (In (2,(dom <*X,Y*>)))) . ((IsoCPNrSP (X,Y)) . z) )

proof end;

theorem LM200: :: NDIFF_7:34

for X, Y, W being RealNormSpace
for z being Point of [:X,Y:]
for f being PartFunc of [:X,Y:],W holds
( ( f is_partial_differentiable_in`1 z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,1 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,1 implies f is_partial_differentiable_in`1 z ) & ( f is_partial_differentiable_in`2 z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,2 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,2 implies f is_partial_differentiable_in`2 z ) )

proof end;

definition

let X, Y, W be RealNormSpace;
let z be Point of [:X,Y:];
let f be PartFunc of [:X,Y:],W;

func partdiff`1 (f,z) -> Point of (R_NormSpace_of_BoundedLinearOperators (X,W)) equals :: NDIFF_7:def 6
diff ((f * (reproj1 z)),(z `1));

coherence
diff ((f * (reproj1 z)),(z `1)) is Point of (R_NormSpace_of_BoundedLinearOperators (X,W)) ;

func partdiff`2 (f,z) -> Point of (R_NormSpace_of_BoundedLinearOperators (Y,W)) equals :: NDIFF_7:def 7
diff ((f * (reproj2 z)),(z `2));

coherence
diff ((f * (reproj2 z)),(z `2)) is Point of (R_NormSpace_of_BoundedLinearOperators (Y,W)) ;

end;

:: deftheorem defines partdiff`1 NDIFF_7:def 6 :
for X, Y, W being RealNormSpace
for z being Point of [:X,Y:]
for f being PartFunc of [:X,Y:],W holds partdiff`1 (f,z) = diff ((f * (reproj1 z)),(z `1));

:: deftheorem defines partdiff`2 NDIFF_7:def 7 :
for X, Y, W being RealNormSpace
for z being Point of [:X,Y:]
for f being PartFunc of [:X,Y:],W holds partdiff`2 (f,z) = diff ((f * (reproj2 z)),(z `2));

theorem LM210: :: NDIFF_7:35

for X, Y, W being RealNormSpace
for z being Point of [:X,Y:]
for f being PartFunc of [:X,Y:],W holds
( partdiff`1 (f,z) = partdiff ((f * ((IsoCPNrSP (X,Y)) ")),((IsoCPNrSP (X,Y)) . z),1) & partdiff`2 (f,z) = partdiff ((f * ((IsoCPNrSP (X,Y)) ")),((IsoCPNrSP (X,Y)) . z),2) )

proof end;

theorem LM215: :: NDIFF_7:36

for X, Y, W being RealNormSpace
for z being Point of [:X,Y:]
for f1, f2 being PartFunc of [:X,Y:],W st f1 is_partial_differentiable_in`1 z & f2 is_partial_differentiable_in`1 z holds
( f1 + f2 is_partial_differentiable_in`1 z & partdiff`1 ((f1 + f2),z) = (partdiff`1 (f1,z)) + (partdiff`1 (f2,z)) & f1 - f2 is_partial_differentiable_in`1 z & partdiff`1 ((f1 - f2),z) = (partdiff`1 (f1,z)) - (partdiff`1 (f2,z)) )

proof end;

theorem LM216: :: NDIFF_7:37

for X, Y, W being RealNormSpace
for z being Point of [:X,Y:]
for f1, f2 being PartFunc of [:X,Y:],W st f1 is_partial_differentiable_in`2 z & f2 is_partial_differentiable_in`2 z holds
( f1 + f2 is_partial_differentiable_in`2 z & partdiff`2 ((f1 + f2),z) = (partdiff`2 (f1,z)) + (partdiff`2 (f2,z)) & f1 - f2 is_partial_differentiable_in`2 z & partdiff`2 ((f1 - f2),z) = (partdiff`2 (f1,z)) - (partdiff`2 (f2,z)) )

proof end;

theorem LM217: :: NDIFF_7:38

for X, Y, W being RealNormSpace
for z being Point of [:X,Y:]
for r being Real
for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_in`1 z holds
( r (#) f is_partial_differentiable_in`1 z & partdiff`1 ((r (#) f),z) = r * (partdiff`1 (f,z)) )

proof end;

theorem LM218: :: NDIFF_7:39

for X, Y, W being RealNormSpace
for z being Point of [:X,Y:]
for r being Real
for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_in`2 z holds
( r (#) f is_partial_differentiable_in`2 z & partdiff`2 ((r (#) f),z) = r * (partdiff`2 (f,z)) )

proof end;

definition

let X, Y, W be RealNormSpace;
let Z be set ;
let f be PartFunc of [:X,Y:],W;

pred f is_partial_differentiable_on`1 Z means :: NDIFF_7:def 8
( Z c= dom f & ( for z being Point of [:X,Y:] st z in Z holds
f | Z is_partial_differentiable_in`1 z ) );

pred f is_partial_differentiable_on`2 Z means :: NDIFF_7:def 9
( Z c= dom f & ( for z being Point of [:X,Y:] st z in Z holds
f | Z is_partial_differentiable_in`2 z ) );

end;

:: deftheorem defines is_partial_differentiable_on`1 NDIFF_7:def 8 :
for X, Y, W being RealNormSpace
for Z being set
for f being PartFunc of [:X,Y:],W holds
( f is_partial_differentiable_on`1 Z iff ( Z c= dom f & ( for z being Point of [:X,Y:] st z in Z holds
f | Z is_partial_differentiable_in`1 z ) ) );

:: deftheorem defines is_partial_differentiable_on`2 NDIFF_7:def 9 :
for X, Y, W being RealNormSpace
for Z being set
for f being PartFunc of [:X,Y:],W holds
( f is_partial_differentiable_on`2 Z iff ( Z c= dom f & ( for z being Point of [:X,Y:] st z in Z holds
f | Z is_partial_differentiable_in`2 z ) ) );

theorem LM300: :: NDIFF_7:40

for X, Y, W being RealNormSpace
for Z being Subset of [:X,Y:]
for f being PartFunc of [:X,Y:],W holds
( ( f is_partial_differentiable_on`1 Z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 implies f is_partial_differentiable_on`1 Z ) & ( f is_partial_differentiable_on`2 Z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 implies f is_partial_differentiable_on`2 Z ) )

proof end;

definition

let X, Y, W be RealNormSpace;
let Z be set ;
let f be PartFunc of [:X,Y:],W;
assume A2: f is_partial_differentiable_on`1 Z ;

func f `partial`1| Z -> PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (X,W)) means :Def91: :: NDIFF_7:def 10
( dom it = Z & ( for z being Point of [:X,Y:] st z in Z holds
it /. z = partdiff`1 (f,z) ) );

existence
ex b₁ being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (X,W)) st
( dom b₁ = Z & ( for z being Point of [:X,Y:] st z in Z holds
b₁ /. z = partdiff`1 (f,z) ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (X,W)) st dom b₁ = Z & ( for z being Point of [:X,Y:] st z in Z holds
b₁ /. z = partdiff`1 (f,z) ) & dom b<sub>2</sub> = Z & ( for z being Point of [:X,Y:] st z in Z holds
b<sub>2</sub> /. z = partdiff`1 (f,z) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def91 defines `partial`1| NDIFF_7:def 10 :
for X, Y, W being RealNormSpace
for Z being set
for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_on`1 Z holds
for b<sub>6</sub> being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (X,W)) holds
( b<sub>6</sub> = f `partial`1| Z iff ( dom b<sub>6</sub> = Z & ( for z being Point of [:X,Y:] st z in Z holds
b<sub>6</sub> /. z = partdiff`1 (f,z) ) ) );

definition

let X, Y, W be RealNormSpace;
let Z be set ;
let f be PartFunc of [:X,Y:],W;
assume A2: f is_partial_differentiable_on`2 Z ;

func f `partial`2| Z -> PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (Y,W)) means :Def92: :: NDIFF_7:def 11
( dom it = Z & ( for z being Point of [:X,Y:] st z in Z holds
it /. z = partdiff`2 (f,z) ) );

existence
ex b₁ being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (Y,W)) st
( dom b₁ = Z & ( for z being Point of [:X,Y:] st z in Z holds
b₁ /. z = partdiff`2 (f,z) ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (Y,W)) st dom b₁ = Z & ( for z being Point of [:X,Y:] st z in Z holds
b₁ /. z = partdiff`2 (f,z) ) & dom b<sub>2</sub> = Z & ( for z being Point of [:X,Y:] st z in Z holds
b<sub>2</sub> /. z = partdiff`2 (f,z) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def92 defines `partial`2| NDIFF_7:def 11 :
for X, Y, W being RealNormSpace
for Z being set
for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_on`2 Z holds
for b<sub>6</sub> being PartFunc of [:X,Y:],(R_NormSpace_of_BoundedLinearOperators (Y,W)) holds
( b<sub>6</sub> = f `partial`2| Z iff ( dom b<sub>6</sub> = Z & ( for z being Point of [:X,Y:] st z in Z holds
b<sub>6</sub> /. z = partdiff`2 (f,z) ) ) );

theorem LM400: :: NDIFF_7:41

for X, Y, W being RealNormSpace
for Z being Subset of [:X,Y:]
for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_on`1 Z holds
f `partial`1| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1)) * (IsoCPNrSP (X,Y))

proof end;

theorem LM401: :: NDIFF_7:42

for X, Y, W being RealNormSpace
for Z being Subset of [:X,Y:]
for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_on`2 Z holds
f `partial`2| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2)) * (IsoCPNrSP (X,Y))

proof end;

theorem NDIFF5241: :: NDIFF_7:43

for X, Y, W being 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`1 Z iff ( Z c= dom f & ( for x being Point of [:X,Y:] st x in Z holds
f is_partial_differentiable_in`1 x ) ) )

proof end;

theorem NDIFF5242: :: NDIFF_7:44

for X, Y, W being 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 ) ) )

proof end;

theorem :: NDIFF_7:45

for X, Y, W being RealNormSpace
for Z being Subset of [:X,Y:]
for f, g being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`1 Z & g is_partial_differentiable_on`1 Z holds
( f + g is_partial_differentiable_on`1 Z & (f + g) `partial`1| Z = (f `partial`1| Z) + (g `partial`1| Z) )

proof end;

theorem :: NDIFF_7:46

for X, Y, W being RealNormSpace
for Z being Subset of [:X,Y:]
for f, g being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`1 Z & g is_partial_differentiable_on`1 Z holds
( f - g is_partial_differentiable_on`1 Z & (f - g) `partial`1| Z = (f `partial`1| Z) - (g `partial`1| Z) )

proof end;

theorem :: NDIFF_7:47

for X, Y, W being RealNormSpace
for Z being Subset of [:X,Y:]
for f, g being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`2 Z & g is_partial_differentiable_on`2 Z holds
( f + g is_partial_differentiable_on`2 Z & (f + g) `partial`2| Z = (f `partial`2| Z) + (g `partial`2| Z) )

proof end;

theorem :: NDIFF_7:48

for X, Y, W being RealNormSpace
for Z being Subset of [:X,Y:]
for f, g being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`2 Z & g is_partial_differentiable_on`2 Z holds
( f - g is_partial_differentiable_on`2 Z & (f - g) `partial`2| Z = (f `partial`2| Z) - (g `partial`2| Z) )

proof end;

theorem :: NDIFF_7:49

for X, Y, W being RealNormSpace
for Z being Subset of [:X,Y:]
for r being Real
for f being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`1 Z holds
( r (#) f is_partial_differentiable_on`1 Z & (r (#) f) `partial`1| Z = r (#) (f `partial`1| Z) )

proof end;

theorem :: NDIFF_7:50

for X, Y, W being RealNormSpace
for Z being Subset of [:X,Y:]
for r being Real
for f being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`2 Z holds
( r (#) f is_partial_differentiable_on`2 Z & (r (#) f) `partial`2| Z = r (#) (f `partial`2| Z) )

proof end;

theorem LMX1: :: NDIFF_7:51

for X, Y, W being RealNormSpace
for Z being Subset of [:X,Y:]
for f being PartFunc of [:X,Y:],W st f is_differentiable_on Z holds
( f `| Z is_continuous_on Z iff (f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z )

proof end;

theorem :: NDIFF_7:52

for X, Y, W being 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`1 Z & f is_partial_differentiable_on`2 Z & f `partial`1| Z is_continuous_on Z & f `partial`2| Z is_continuous_on Z iff ( f is_differentiable_on Z & f `| Z is_continuous_on Z ) )

proof end;