:: PDIFF_3 semantic presentation
begin
registration
clusterV21() RestFunc-like -> total for Element of K6(K7(REAL,REAL));
coherence
for b1 being RestFunc holds b1 is total by FDIFF_1:def_2;
end;
definition
let i be Element of NAT ;
let n be non empty Element of NAT ;
let f be PartFunc of (REAL n),REAL;
func pdiff1 (f,i) -> Function of (REAL n),REAL means :: PDIFF_3:def 1
for z being Element of REAL n holds it . z = partdiff (f,z,i);
existence
ex b1 being Function of (REAL n),REAL st
for z being Element of REAL n holds b1 . z = partdiff (f,z,i)
proof
deffunc H1( Element of REAL n) -> Element of REAL = partdiff (f,$1,i);
consider g being Function of (REAL n),REAL such that
A1: for z being Element of REAL n holds g . z = H1(z) from FUNCT_2:sch_4();
take g ; ::_thesis: for z being Element of REAL n holds g . z = partdiff (f,z,i)
thus for z being Element of REAL n holds g . z = partdiff (f,z,i) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (REAL n),REAL st ( for z being Element of REAL n holds b1 . z = partdiff (f,z,i) ) & ( for z being Element of REAL n holds b2 . z = partdiff (f,z,i) ) holds
b1 = b2
proof
let F, G be Function of (REAL n),REAL; ::_thesis: ( ( for z being Element of REAL n holds F . z = partdiff (f,z,i) ) & ( for z being Element of REAL n holds G . z = partdiff (f,z,i) ) implies F = G )
assume that
A2: for z being Element of REAL n holds F . z = partdiff (f,z,i) and
A3: for z being Element of REAL n holds G . z = partdiff (f,z,i) ; ::_thesis: F = G
now__::_thesis:_for_z_being_Element_of_REAL_n_holds_F_._z_=_G_._z
let z be Element of REAL n; ::_thesis: F . z = G . z
F . z = partdiff (f,z,i) by A2;
hence F . z = G . z by A3; ::_thesis: verum
end;
hence F = G by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem defines pdiff1 PDIFF_3:def_1_:_
for i being Element of NAT
for n being non empty Element of NAT
for f being PartFunc of (REAL n),REAL
for b4 being Function of (REAL n),REAL holds
( b4 = pdiff1 (f,i) iff for z being Element of REAL n holds b4 . z = partdiff (f,z,i) );
definition
let f be PartFunc of (REAL 2),REAL;
let z be Element of REAL 2;
predf is_hpartial_differentiable`11_in z means :Def2: :: PDIFF_3:def 2
ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) );
predf is_hpartial_differentiable`12_in z means :Def3: :: PDIFF_3:def 3
ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) );
predf is_hpartial_differentiable`21_in z means :Def4: :: PDIFF_3:def 4
ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) );
predf is_hpartial_differentiable`22_in z means :Def5: :: PDIFF_3:def 5
ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) );
end;
:: deftheorem Def2 defines is_hpartial_differentiable`11_in PDIFF_3:def_2_:_
for f being PartFunc of (REAL 2),REAL
for z being Element of REAL 2 holds
( f is_hpartial_differentiable`11_in z iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) );
:: deftheorem Def3 defines is_hpartial_differentiable`12_in PDIFF_3:def_3_:_
for f being PartFunc of (REAL 2),REAL
for z being Element of REAL 2 holds
( f is_hpartial_differentiable`12_in z iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) );
:: deftheorem Def4 defines is_hpartial_differentiable`21_in PDIFF_3:def_4_:_
for f being PartFunc of (REAL 2),REAL
for z being Element of REAL 2 holds
( f is_hpartial_differentiable`21_in z iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) );
:: deftheorem Def5 defines is_hpartial_differentiable`22_in PDIFF_3:def_5_:_
for f being PartFunc of (REAL 2),REAL
for z being Element of REAL 2 holds
( f is_hpartial_differentiable`22_in z iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) );
definition
let f be PartFunc of (REAL 2),REAL;
let z be Element of REAL 2;
assume A1: f is_hpartial_differentiable`11_in z ;
func hpartdiff11 (f,z) -> Real means :Def6: :: PDIFF_3:def 6
ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( it = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) );
existence
ex b1, x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( b1 = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )
proof
consider x0, y0 being Real such that
A2: z = <*x0,y0*> and
A3: ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) by A1, Def2;
consider N being Neighbourhood of x0 such that
A4: N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) and
A5: ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A3;
consider L being LinearFunc, R being RestFunc such that
A6: for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A5;
consider r being Real such that
A7: for p being Real holds L . p = r * p by FDIFF_1:def_3;
take r ; ::_thesis: ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )
L . 1 = r * 1 by A7
.= r ;
hence ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) by A2, A4, A6; ::_thesis: verum
end;
uniqueness
for b1, b2 being Real st ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( b1 = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) & ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( b2 = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) holds
b1 = b2
proof
let r, s be Real; ::_thesis: ( ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) & ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) implies r = s )
assume that
A8: ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) and
A9: ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) ; ::_thesis: r = s
consider x1, y1 being Real such that
A10: z = <*x1,y1*> and
A11: ex N being Neighbourhood of x1 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) ) ) by A9;
consider N1 being Neighbourhood of x1 such that
N1 c= dom (SVF1 (1,(pdiff1 (f,1)),z)) and
A12: ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for x being Real st x in N1 holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) ) by A11;
consider L1 being LinearFunc, R1 being RestFunc such that
A13: s = L1 . 1 and
A14: for x being Real st x in N1 holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x1) = (L1 . (x - x1)) + (R1 . (x - x1)) by A12;
consider p1 being Real such that
A15: for p being Real holds L1 . p = p1 * p by FDIFF_1:def_3;
A16: s = p1 * 1 by A13, A15;
consider x0, y0 being Real such that
A17: z = <*x0,y0*> and
A18: ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) by A8;
consider N being Neighbourhood of x0 such that
N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) and
A19: ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by A18;
consider L being LinearFunc, R being RestFunc such that
A20: r = L . 1 and
A21: for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A19;
consider r1 being Real such that
A22: for p being Real holds L . p = r1 * p by FDIFF_1:def_3;
A23: x0 = x1 by A17, A10, FINSEQ_1:77;
then consider N0 being Neighbourhood of x0 such that
A24: ( N0 c= N & N0 c= N1 ) by RCOMP_1:17;
consider g being real number such that
A25: 0 < g and
A26: N0 = ].(x0 - g),(x0 + g).[ by RCOMP_1:def_6;
deffunc H1( Element of NAT ) -> Element of REAL = g / ($1 + 2);
consider s1 being Real_Sequence such that
A27: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1();
now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_<>_0
let n be Element of NAT ; ::_thesis: s1 . n <> 0
g / (n + 2) <> 0 by A25, XREAL_1:139;
hence s1 . n <> 0 by A27; ::_thesis: verum
end;
then A28: s1 is non-zero by SEQ_1:5;
( s1 is convergent & lim s1 = 0 ) by A27, SEQ_4:31;
then reconsider h = s1 as non-zero 0 -convergent Real_Sequence by A28, FDIFF_1:def_1;
A29: for n being Element of NAT ex x being Real st
( x in N & x in N1 & h . n = x - x0 )
proof
let n be Element of NAT ; ::_thesis: ex x being Real st
( x in N & x in N1 & h . n = x - x0 )
take x0 + (g / (n + 2)) ; ::_thesis: ( x0 + (g / (n + 2)) in N & x0 + (g / (n + 2)) in N1 & h . n = (x0 + (g / (n + 2))) - x0 )
0 + 1 < (n + 1) + 1 by XREAL_1:6;
then g / (n + 2) < g / 1 by A25, XREAL_1:76;
then A30: x0 + (g / (n + 2)) < x0 + g by XREAL_1:6;
g / (n + 2) > 0 by A25, XREAL_1:139;
then x0 + (- g) < x0 + (g / (n + 2)) by A25, XREAL_1:6;
then x0 + (g / (n + 2)) in ].(x0 - g),(x0 + g).[ by A30;
hence ( x0 + (g / (n + 2)) in N & x0 + (g / (n + 2)) in N1 & h . n = (x0 + (g / (n + 2))) - x0 ) by A24, A26, A27; ::_thesis: verum
end;
A31: r = r1 * 1 by A20, A22;
A32: now__::_thesis:_for_x_being_Real_st_x_in_N_&_x_in_N1_holds_
(r_*_(x_-_x0))_+_(R_._(x_-_x0))_=_(s_*_(x_-_x0))_+_(R1_._(x_-_x0))
let x be Real; ::_thesis: ( x in N & x in N1 implies (r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0)) )
assume that
A33: x in N and
A34: x in N1 ; ::_thesis: (r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0))
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A21, A33;
then (L . (x - x0)) + (R . (x - x0)) = (L1 . (x - x0)) + (R1 . (x - x0)) by A14, A23, A34;
then (r1 * (x - x0)) + (R . (x - x0)) = (L1 . (x - x0)) + (R1 . (x - x0)) by A22;
hence (r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0)) by A15, A31, A16; ::_thesis: verum
end;
for n being Nat holds r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n
proof
dom R1 = REAL by PARTFUN1:def_2;
then A35: rng h c= dom R1 ;
let n be Nat; ::_thesis: r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n
dom R = REAL by PARTFUN1:def_2;
then A36: rng h c= dom R ;
A37: n in NAT by ORDINAL1:def_12;
then ex x being Real st
( x in N & x in N1 & h . n = x - x0 ) by A29;
then (r * (h . n)) + (R . (h . n)) = (s * (h . n)) + (R1 . (h . n)) by A32;
then A38: ((r * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n)) = ((s * (h . n)) + (R1 . (h . n))) / (h . n) by XCMPLX_1:62;
A39: (R . (h . n)) / (h . n) = (R . (h . n)) * ((h . n) ") by XCMPLX_0:def_9
.= (R . (h . n)) * ((h ") . n) by VALUED_1:10
.= ((R /* h) . n) * ((h ") . n) by A37, A36, FUNCT_2:108
.= ((h ") (#) (R /* h)) . n by VALUED_1:5 ;
A40: h . n <> 0 by A37, SEQ_1:5;
A41: (R1 . (h . n)) / (h . n) = (R1 . (h . n)) * ((h . n) ") by XCMPLX_0:def_9
.= (R1 . (h . n)) * ((h ") . n) by VALUED_1:10
.= ((R1 /* h) . n) * ((h ") . n) by A37, A35, FUNCT_2:108
.= ((h ") (#) (R1 /* h)) . n by VALUED_1:5 ;
A42: (s * (h . n)) / (h . n) = s * ((h . n) / (h . n)) by XCMPLX_1:74
.= s * 1 by A40, XCMPLX_1:60
.= s ;
(r * (h . n)) / (h . n) = r * ((h . n) / (h . n)) by XCMPLX_1:74
.= r * 1 by A40, XCMPLX_1:60
.= r ;
then r + ((R . (h . n)) / (h . n)) = s + ((R1 . (h . n)) / (h . n)) by A38, A42, XCMPLX_1:62;
then r = s + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) by A39, A41;
hence r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n by A37, RFUNCT_2:1; ::_thesis: verum
end;
then ( ((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h)) is constant & (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . 1 = r - s ) by VALUED_0:def_18;
then A43: lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = r - s by SEQ_4:25;
A44: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) by FDIFF_1:def_2;
( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) by FDIFF_1:def_2;
then r - s = 0 - 0 by A43, A44, SEQ_2:12;
hence r = s ; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines hpartdiff11 PDIFF_3:def_6_:_
for f being PartFunc of (REAL 2),REAL
for z being Element of REAL 2 st f is_hpartial_differentiable`11_in z holds
for b3 being Real holds
( b3 = hpartdiff11 (f,z) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( b3 = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) );
definition
let f be PartFunc of (REAL 2),REAL;
let z be Element of REAL 2;
assume A1: f is_hpartial_differentiable`12_in z ;
func hpartdiff12 (f,z) -> Real means :Def7: :: PDIFF_3:def 7
ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( it = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) );
existence
ex b1, x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( b1 = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) )
proof
consider x0, y0 being Real such that
A2: z = <*x0,y0*> and
A3: ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) by A1, Def3;
consider N being Neighbourhood of y0 such that
A4: N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) and
A5: ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A3;
consider L being LinearFunc, R being RestFunc such that
A6: for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A5;
consider r being Real such that
A7: for p being Real holds L . p = r * p by FDIFF_1:def_3;
take r ; ::_thesis: ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) )
L . 1 = r * 1 by A7
.= r ;
hence ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) by A2, A4, A6; ::_thesis: verum
end;
uniqueness
for b1, b2 being Real st ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( b1 = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) & ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( b2 = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) holds
b1 = b2
proof
let r, s be Real; ::_thesis: ( ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) & ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) implies r = s )
assume that
A8: ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) and
A9: ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) ; ::_thesis: r = s
consider x1, y1 being Real such that
A10: z = <*x1,y1*> and
A11: ex N being Neighbourhood of y1 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) ) ) by A9;
consider N1 being Neighbourhood of y1 such that
N1 c= dom (SVF1 (2,(pdiff1 (f,1)),z)) and
A12: ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for y being Real st y in N1 holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) ) by A11;
consider L1 being LinearFunc, R1 being RestFunc such that
A13: s = L1 . 1 and
A14: for y being Real st y in N1 holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y1) = (L1 . (y - y1)) + (R1 . (y - y1)) by A12;
consider p1 being Real such that
A15: for p being Real holds L1 . p = p1 * p by FDIFF_1:def_3;
A16: s = p1 * 1 by A13, A15;
consider x0, y0 being Real such that
A17: z = <*x0,y0*> and
A18: ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) by A8;
consider N being Neighbourhood of y0 such that
N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) and
A19: ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) by A18;
consider L being LinearFunc, R being RestFunc such that
A20: r = L . 1 and
A21: for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A19;
consider r1 being Real such that
A22: for p being Real holds L . p = r1 * p by FDIFF_1:def_3;
A23: y0 = y1 by A17, A10, FINSEQ_1:77;
then consider N0 being Neighbourhood of y0 such that
A24: ( N0 c= N & N0 c= N1 ) by RCOMP_1:17;
consider g being real number such that
A25: 0 < g and
A26: N0 = ].(y0 - g),(y0 + g).[ by RCOMP_1:def_6;
deffunc H1( Element of NAT ) -> Element of REAL = g / ($1 + 2);
consider s1 being Real_Sequence such that
A27: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1();
now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_<>_0
let n be Element of NAT ; ::_thesis: s1 . n <> 0
g / (n + 2) <> 0 by A25, XREAL_1:139;
hence s1 . n <> 0 by A27; ::_thesis: verum
end;
then A28: s1 is non-zero by SEQ_1:5;
( s1 is convergent & lim s1 = 0 ) by A27, SEQ_4:31;
then reconsider h = s1 as non-zero 0 -convergent Real_Sequence by A28, FDIFF_1:def_1;
A29: for n being Element of NAT ex y being Real st
( y in N & y in N1 & h . n = y - y0 )
proof
let n be Element of NAT ; ::_thesis: ex y being Real st
( y in N & y in N1 & h . n = y - y0 )
take y0 + (g / (n + 2)) ; ::_thesis: ( y0 + (g / (n + 2)) in N & y0 + (g / (n + 2)) in N1 & h . n = (y0 + (g / (n + 2))) - y0 )
0 + 1 < (n + 1) + 1 by XREAL_1:6;
then g / (n + 2) < g / 1 by A25, XREAL_1:76;
then A30: y0 + (g / (n + 2)) < y0 + g by XREAL_1:6;
g / (n + 2) > 0 by A25, XREAL_1:139;
then y0 + (- g) < y0 + (g / (n + 2)) by A25, XREAL_1:6;
then y0 + (g / (n + 2)) in ].(y0 - g),(y0 + g).[ by A30;
hence ( y0 + (g / (n + 2)) in N & y0 + (g / (n + 2)) in N1 & h . n = (y0 + (g / (n + 2))) - y0 ) by A24, A26, A27; ::_thesis: verum
end;
A31: r = r1 * 1 by A20, A22;
A32: now__::_thesis:_for_y_being_Real_st_y_in_N_&_y_in_N1_holds_
(r_*_(y_-_y0))_+_(R_._(y_-_y0))_=_(s_*_(y_-_y0))_+_(R1_._(y_-_y0))
let y be Real; ::_thesis: ( y in N & y in N1 implies (r * (y - y0)) + (R . (y - y0)) = (s * (y - y0)) + (R1 . (y - y0)) )
assume that
A33: y in N and
A34: y in N1 ; ::_thesis: (r * (y - y0)) + (R . (y - y0)) = (s * (y - y0)) + (R1 . (y - y0))
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A21, A33;
then (L . (y - y0)) + (R . (y - y0)) = (L1 . (y - y0)) + (R1 . (y - y0)) by A14, A23, A34;
then (r1 * (y - y0)) + (R . (y - y0)) = (L1 . (y - y0)) + (R1 . (y - y0)) by A22;
hence (r * (y - y0)) + (R . (y - y0)) = (s * (y - y0)) + (R1 . (y - y0)) by A15, A31, A16; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Nat_holds_r_-_s_=_(((h_")_(#)_(R1_/*_h))_-_((h_")_(#)_(R_/*_h)))_._n
dom R1 = REAL by PARTFUN1:def_2;
then A35: rng h c= dom R1 ;
let n be Nat; ::_thesis: r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n
dom R = REAL by PARTFUN1:def_2;
then A36: rng h c= dom R ;
A37: n in NAT by ORDINAL1:def_12;
then ex y being Real st
( y in N & y in N1 & h . n = y - y0 ) by A29;
then (r * (h . n)) + (R . (h . n)) = (s * (h . n)) + (R1 . (h . n)) by A32;
then A38: ((r * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n)) = ((s * (h . n)) + (R1 . (h . n))) / (h . n) by XCMPLX_1:62;
A39: (R . (h . n)) / (h . n) = (R . (h . n)) * ((h . n) ") by XCMPLX_0:def_9
.= (R . (h . n)) * ((h ") . n) by VALUED_1:10
.= ((R /* h) . n) * ((h ") . n) by A37, A36, FUNCT_2:108
.= ((h ") (#) (R /* h)) . n by VALUED_1:5 ;
A40: h . n <> 0 by A37, SEQ_1:5;
A41: (R1 . (h . n)) / (h . n) = (R1 . (h . n)) * ((h . n) ") by XCMPLX_0:def_9
.= (R1 . (h . n)) * ((h ") . n) by VALUED_1:10
.= ((R1 /* h) . n) * ((h ") . n) by A37, A35, FUNCT_2:108
.= ((h ") (#) (R1 /* h)) . n by VALUED_1:5 ;
A42: (s * (h . n)) / (h . n) = s * ((h . n) / (h . n)) by XCMPLX_1:74
.= s * 1 by A40, XCMPLX_1:60
.= s ;
(r * (h . n)) / (h . n) = r * ((h . n) / (h . n)) by XCMPLX_1:74
.= r * 1 by A40, XCMPLX_1:60
.= r ;
then r + ((R . (h . n)) / (h . n)) = s + ((R1 . (h . n)) / (h . n)) by A38, A42, XCMPLX_1:62;
then r = s + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) by A39, A41;
hence r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n by A37, RFUNCT_2:1; ::_thesis: verum
end;
then ( ((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h)) is constant & (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . 1 = r - s ) by VALUED_0:def_18;
then A43: lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = r - s by SEQ_4:25;
A44: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) by FDIFF_1:def_2;
( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) by FDIFF_1:def_2;
then r - s = 0 - 0 by A43, A44, SEQ_2:12;
hence r = s ; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines hpartdiff12 PDIFF_3:def_7_:_
for f being PartFunc of (REAL 2),REAL
for z being Element of REAL 2 st f is_hpartial_differentiable`12_in z holds
for b3 being Real holds
( b3 = hpartdiff12 (f,z) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
( b3 = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) );
definition
let f be PartFunc of (REAL 2),REAL;
let z be Element of REAL 2;
assume A1: f is_hpartial_differentiable`21_in z ;
func hpartdiff21 (f,z) -> Real means :Def8: :: PDIFF_3:def 8
ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( it = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) );
existence
ex b1, x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( b1 = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )
proof
consider x0, y0 being Real such that
A2: z = <*x0,y0*> and
A3: ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) by A1, Def4;
consider N being Neighbourhood of x0 such that
A4: N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) and
A5: ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A3;
consider L being LinearFunc, R being RestFunc such that
A6: for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A5;
consider r being Real such that
A7: for p being Real holds L . p = r * p by FDIFF_1:def_3;
take r ; ::_thesis: ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )
L . 1 = r * 1 by A7
.= r ;
hence ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) by A2, A4, A6; ::_thesis: verum
end;
uniqueness
for b1, b2 being Real st ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( b1 = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) & ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( b2 = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) holds
b1 = b2
proof
let r, s be Real; ::_thesis: ( ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) & ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) implies r = s )
assume that
A8: ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) and
A9: ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) ; ::_thesis: r = s
consider x1, y1 being Real such that
A10: z = <*x1,y1*> and
A11: ex N being Neighbourhood of x1 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) ) ) by A9;
consider N1 being Neighbourhood of x1 such that
N1 c= dom (SVF1 (1,(pdiff1 (f,2)),z)) and
A12: ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for x being Real st x in N1 holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) ) by A11;
consider L1 being LinearFunc, R1 being RestFunc such that
A13: s = L1 . 1 and
A14: for x being Real st x in N1 holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x1) = (L1 . (x - x1)) + (R1 . (x - x1)) by A12;
consider p1 being Real such that
A15: for p being Real holds L1 . p = p1 * p by FDIFF_1:def_3;
A16: s = p1 * 1 by A13, A15;
consider x0, y0 being Real such that
A17: z = <*x0,y0*> and
A18: ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) by A8;
consider N being Neighbourhood of x0 such that
N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) and
A19: ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by A18;
consider L being LinearFunc, R being RestFunc such that
A20: r = L . 1 and
A21: for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A19;
consider r1 being Real such that
A22: for p being Real holds L . p = r1 * p by FDIFF_1:def_3;
A23: x0 = x1 by A17, A10, FINSEQ_1:77;
then consider N0 being Neighbourhood of x0 such that
A24: ( N0 c= N & N0 c= N1 ) by RCOMP_1:17;
consider g being real number such that
A25: 0 < g and
A26: N0 = ].(x0 - g),(x0 + g).[ by RCOMP_1:def_6;
deffunc H1( Element of NAT ) -> Element of REAL = g / ($1 + 2);
consider s1 being Real_Sequence such that
A27: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1();
now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_<>_0
let n be Element of NAT ; ::_thesis: s1 . n <> 0
g / (n + 2) <> 0 by A25, XREAL_1:139;
hence s1 . n <> 0 by A27; ::_thesis: verum
end;
then A28: s1 is non-zero by SEQ_1:5;
( s1 is convergent & lim s1 = 0 ) by A27, SEQ_4:31;
then reconsider h = s1 as non-zero 0 -convergent Real_Sequence by A28, FDIFF_1:def_1;
A29: for n being Element of NAT ex x being Real st
( x in N & x in N1 & h . n = x - x0 )
proof
let n be Element of NAT ; ::_thesis: ex x being Real st
( x in N & x in N1 & h . n = x - x0 )
take x0 + (g / (n + 2)) ; ::_thesis: ( x0 + (g / (n + 2)) in N & x0 + (g / (n + 2)) in N1 & h . n = (x0 + (g / (n + 2))) - x0 )
0 + 1 < (n + 1) + 1 by XREAL_1:6;
then g / (n + 2) < g / 1 by A25, XREAL_1:76;
then A30: x0 + (g / (n + 2)) < x0 + g by XREAL_1:6;
g / (n + 2) > 0 by A25, XREAL_1:139;
then x0 + (- g) < x0 + (g / (n + 2)) by A25, XREAL_1:6;
then x0 + (g / (n + 2)) in ].(x0 - g),(x0 + g).[ by A30;
hence ( x0 + (g / (n + 2)) in N & x0 + (g / (n + 2)) in N1 & h . n = (x0 + (g / (n + 2))) - x0 ) by A24, A26, A27; ::_thesis: verum
end;
A31: r = r1 * 1 by A20, A22;
A32: now__::_thesis:_for_x_being_Real_st_x_in_N_&_x_in_N1_holds_
(r_*_(x_-_x0))_+_(R_._(x_-_x0))_=_(s_*_(x_-_x0))_+_(R1_._(x_-_x0))
let x be Real; ::_thesis: ( x in N & x in N1 implies (r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0)) )
assume that
A33: x in N and
A34: x in N1 ; ::_thesis: (r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0))
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A21, A33;
then (L . (x - x0)) + (R . (x - x0)) = (L1 . (x - x0)) + (R1 . (x - x0)) by A14, A23, A34;
then (r1 * (x - x0)) + (R . (x - x0)) = (L1 . (x - x0)) + (R1 . (x - x0)) by A22;
hence (r * (x - x0)) + (R . (x - x0)) = (s * (x - x0)) + (R1 . (x - x0)) by A15, A31, A16; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Nat_holds_r_-_s_=_(((h_")_(#)_(R1_/*_h))_-_((h_")_(#)_(R_/*_h)))_._n
dom R1 = REAL by PARTFUN1:def_2;
then A35: rng h c= dom R1 ;
let n be Nat; ::_thesis: r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n
dom R = REAL by PARTFUN1:def_2;
then A36: rng h c= dom R ;
A37: n in NAT by ORDINAL1:def_12;
then ex x being Real st
( x in N & x in N1 & h . n = x - x0 ) by A29;
then (r * (h . n)) + (R . (h . n)) = (s * (h . n)) + (R1 . (h . n)) by A32;
then A38: ((r * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n)) = ((s * (h . n)) + (R1 . (h . n))) / (h . n) by XCMPLX_1:62;
A39: (R . (h . n)) / (h . n) = (R . (h . n)) * ((h . n) ") by XCMPLX_0:def_9
.= (R . (h . n)) * ((h ") . n) by VALUED_1:10
.= ((R /* h) . n) * ((h ") . n) by A37, A36, FUNCT_2:108
.= ((h ") (#) (R /* h)) . n by VALUED_1:5 ;
A40: h . n <> 0 by A37, SEQ_1:5;
A41: (R1 . (h . n)) / (h . n) = (R1 . (h . n)) * ((h . n) ") by XCMPLX_0:def_9
.= (R1 . (h . n)) * ((h ") . n) by VALUED_1:10
.= ((R1 /* h) . n) * ((h ") . n) by A37, A35, FUNCT_2:108
.= ((h ") (#) (R1 /* h)) . n by VALUED_1:5 ;
A42: (s * (h . n)) / (h . n) = s * ((h . n) / (h . n)) by XCMPLX_1:74
.= s * 1 by A40, XCMPLX_1:60
.= s ;
(r * (h . n)) / (h . n) = r * ((h . n) / (h . n)) by XCMPLX_1:74
.= r * 1 by A40, XCMPLX_1:60
.= r ;
then r + ((R . (h . n)) / (h . n)) = s + ((R1 . (h . n)) / (h . n)) by A38, A42, XCMPLX_1:62;
then r = s + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) by A39, A41;
hence r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n by A37, VALUED_1:15; ::_thesis: verum
end;
then ( ((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h)) is constant & (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . 1 = r - s ) by VALUED_0:def_18;
then A43: lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = r - s by SEQ_4:25;
A44: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) by FDIFF_1:def_2;
( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) by FDIFF_1:def_2;
then r - s = 0 - 0 by A43, A44, SEQ_2:12;
hence r = s ; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines hpartdiff21 PDIFF_3:def_8_:_
for f being PartFunc of (REAL 2),REAL
for z being Element of REAL 2 st f is_hpartial_differentiable`21_in z holds
for b3 being Real holds
( b3 = hpartdiff21 (f,z) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( b3 = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) );
definition
let f be PartFunc of (REAL 2),REAL;
let z be Element of REAL 2;
assume A1: f is_hpartial_differentiable`22_in z ;
func hpartdiff22 (f,z) -> Real means :Def9: :: PDIFF_3:def 9
ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( it = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) );
existence
ex b1, x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( b1 = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) )
proof
consider x0, y0 being Real such that
A2: z = <*x0,y0*> and
A3: ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) by A1, Def5;
consider N being Neighbourhood of y0 such that
A4: N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) and
A5: ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A3;
consider L being LinearFunc, R being RestFunc such that
A6: for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A5;
consider r being Real such that
A7: for p being Real holds L . p = r * p by FDIFF_1:def_3;
take r ; ::_thesis: ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) )
L . 1 = r * 1 by A7
.= r ;
hence ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) by A2, A4, A6; ::_thesis: verum
end;
uniqueness
for b1, b2 being Real st ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( b1 = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) & ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( b2 = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) holds
b1 = b2
proof
let r, s be Real; ::_thesis: ( ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) & ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) implies r = s )
assume that
A8: ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) and
A9: ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) ; ::_thesis: r = s
consider x1, y1 being Real such that
A10: z = <*x1,y1*> and
A11: ex N being Neighbourhood of y1 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) ) ) by A9;
consider N1 being Neighbourhood of y1 such that
N1 c= dom (SVF1 (2,(pdiff1 (f,2)),z)) and
A12: ex L being LinearFunc ex R being RestFunc st
( s = L . 1 & ( for y being Real st y in N1 holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) ) by A11;
consider L1 being LinearFunc, R1 being RestFunc such that
A13: s = L1 . 1 and
A14: for y being Real st y in N1 holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y1) = (L1 . (y - y1)) + (R1 . (y - y1)) by A12;
consider p1 being Real such that
A15: for p being Real holds L1 . p = p1 * p by FDIFF_1:def_3;
A16: s = p1 * 1 by A13, A15;
consider x0, y0 being Real such that
A17: z = <*x0,y0*> and
A18: ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) by A8;
consider N being Neighbourhood of y0 such that
N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) and
A19: ex L being LinearFunc ex R being RestFunc st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) by A18;
consider L being LinearFunc, R being RestFunc such that
A20: r = L . 1 and
A21: for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A19;
consider r1 being Real such that
A22: for p being Real holds L . p = r1 * p by FDIFF_1:def_3;
A23: y0 = y1 by A17, A10, FINSEQ_1:77;
then consider N0 being Neighbourhood of y0 such that
A24: ( N0 c= N & N0 c= N1 ) by RCOMP_1:17;
consider g being real number such that
A25: 0 < g and
A26: N0 = ].(y0 - g),(y0 + g).[ by RCOMP_1:def_6;
deffunc H1( Element of NAT ) -> Element of REAL = g / ($1 + 2);
consider s1 being Real_Sequence such that
A27: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1();
now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_<>_0
let n be Element of NAT ; ::_thesis: s1 . n <> 0
g / (n + 2) <> 0 by A25, XREAL_1:139;
hence s1 . n <> 0 by A27; ::_thesis: verum
end;
then A28: s1 is non-zero by SEQ_1:5;
( s1 is convergent & lim s1 = 0 ) by A27, SEQ_4:31;
then reconsider h = s1 as non-zero 0 -convergent Real_Sequence by A28, FDIFF_1:def_1;
A29: for n being Element of NAT ex y being Real st
( y in N & y in N1 & h . n = y - y0 )
proof
let n be Element of NAT ; ::_thesis: ex y being Real st
( y in N & y in N1 & h . n = y - y0 )
take y0 + (g / (n + 2)) ; ::_thesis: ( y0 + (g / (n + 2)) in N & y0 + (g / (n + 2)) in N1 & h . n = (y0 + (g / (n + 2))) - y0 )
0 + 1 < (n + 1) + 1 by XREAL_1:6;
then g / (n + 2) < g / 1 by A25, XREAL_1:76;
then A30: y0 + (g / (n + 2)) < y0 + g by XREAL_1:6;
g / (n + 2) > 0 by A25, XREAL_1:139;
then y0 + (- g) < y0 + (g / (n + 2)) by A25, XREAL_1:6;
then y0 + (g / (n + 2)) in ].(y0 - g),(y0 + g).[ by A30;
hence ( y0 + (g / (n + 2)) in N & y0 + (g / (n + 2)) in N1 & h . n = (y0 + (g / (n + 2))) - y0 ) by A24, A26, A27; ::_thesis: verum
end;
A31: r = r1 * 1 by A20, A22;
A32: now__::_thesis:_for_y_being_Real_st_y_in_N_&_y_in_N1_holds_
(r_*_(y_-_y0))_+_(R_._(y_-_y0))_=_(s_*_(y_-_y0))_+_(R1_._(y_-_y0))
let y be Real; ::_thesis: ( y in N & y in N1 implies (r * (y - y0)) + (R . (y - y0)) = (s * (y - y0)) + (R1 . (y - y0)) )
assume that
A33: y in N and
A34: y in N1 ; ::_thesis: (r * (y - y0)) + (R . (y - y0)) = (s * (y - y0)) + (R1 . (y - y0))
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) by A21, A33;
then (L . (y - y0)) + (R . (y - y0)) = (L1 . (y - y0)) + (R1 . (y - y0)) by A14, A23, A34;
then (r1 * (y - y0)) + (R . (y - y0)) = (L1 . (y - y0)) + (R1 . (y - y0)) by A22;
hence (r * (y - y0)) + (R . (y - y0)) = (s * (y - y0)) + (R1 . (y - y0)) by A15, A31, A16; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Nat_holds_r_-_s_=_(((h_")_(#)_(R1_/*_h))_-_((h_")_(#)_(R_/*_h)))_._n
dom R1 = REAL by PARTFUN1:def_2;
then A35: rng h c= dom R1 ;
let n be Nat; ::_thesis: r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n
dom R = REAL by PARTFUN1:def_2;
then A36: rng h c= dom R ;
A37: n in NAT by ORDINAL1:def_12;
then ex y being Real st
( y in N & y in N1 & h . n = y - y0 ) by A29;
then (r * (h . n)) + (R . (h . n)) = (s * (h . n)) + (R1 . (h . n)) by A32;
then A38: ((r * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n)) = ((s * (h . n)) + (R1 . (h . n))) / (h . n) by XCMPLX_1:62;
A39: (R . (h . n)) / (h . n) = (R . (h . n)) * ((h . n) ") by XCMPLX_0:def_9
.= (R . (h . n)) * ((h ") . n) by VALUED_1:10
.= ((R /* h) . n) * ((h ") . n) by A37, A36, FUNCT_2:108
.= ((h ") (#) (R /* h)) . n by VALUED_1:5 ;
A40: h . n <> 0 by A37, SEQ_1:5;
A41: (R1 . (h . n)) / (h . n) = (R1 . (h . n)) * ((h . n) ") by XCMPLX_0:def_9
.= (R1 . (h . n)) * ((h ") . n) by VALUED_1:10
.= ((R1 /* h) . n) * ((h ") . n) by A37, A35, FUNCT_2:108
.= ((h ") (#) (R1 /* h)) . n by VALUED_1:5 ;
A42: (s * (h . n)) / (h . n) = s * ((h . n) / (h . n)) by XCMPLX_1:74
.= s * 1 by A40, XCMPLX_1:60
.= s ;
(r * (h . n)) / (h . n) = r * ((h . n) / (h . n)) by XCMPLX_1:74
.= r * 1 by A40, XCMPLX_1:60
.= r ;
then r + ((R . (h . n)) / (h . n)) = s + ((R1 . (h . n)) / (h . n)) by A38, A42, XCMPLX_1:62;
then r = s + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) by A39, A41;
hence r - s = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n by A37, RFUNCT_2:1; ::_thesis: verum
end;
then ( ((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h)) is constant & (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . 1 = r - s ) by VALUED_0:def_18;
then A43: lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = r - s by SEQ_4:25;
A44: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) by FDIFF_1:def_2;
( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) by FDIFF_1:def_2;
then r - s = 0 - 0 by A43, A44, SEQ_2:12;
hence r = s ; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines hpartdiff22 PDIFF_3:def_9_:_
for f being PartFunc of (REAL 2),REAL
for z being Element of REAL 2 st f is_hpartial_differentiable`22_in z holds
for b3 being Real holds
( b3 = hpartdiff22 (f,z) iff ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
( b3 = L . 1 & ( for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) );
theorem :: PDIFF_3:1
for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`11_in z holds
SVF1 (1,(pdiff1 (f,1)),z) is_differentiable_in x0
proof
let x0, y0 be Real; ::_thesis: for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`11_in z holds
SVF1 (1,(pdiff1 (f,1)),z) is_differentiable_in x0
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`11_in z holds
SVF1 (1,(pdiff1 (f,1)),z) is_differentiable_in x0
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_hpartial_differentiable`11_in z implies SVF1 (1,(pdiff1 (f,1)),z) is_differentiable_in x0 )
assume that
A1: z = <*x0,y0*> and
A2: f is_hpartial_differentiable`11_in z ; ::_thesis: SVF1 (1,(pdiff1 (f,1)),z) is_differentiable_in x0
consider x1, y1 being Real such that
A3: z = <*x1,y1*> and
A4: ex N being Neighbourhood of x1 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) by A2, Def2;
x0 = x1 by A1, A3, FINSEQ_1:77;
hence SVF1 (1,(pdiff1 (f,1)),z) is_differentiable_in x0 by A4, FDIFF_1:def_4; ::_thesis: verum
end;
theorem :: PDIFF_3:2
for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`12_in z holds
SVF1 (2,(pdiff1 (f,1)),z) is_differentiable_in y0
proof
let x0, y0 be Real; ::_thesis: for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`12_in z holds
SVF1 (2,(pdiff1 (f,1)),z) is_differentiable_in y0
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`12_in z holds
SVF1 (2,(pdiff1 (f,1)),z) is_differentiable_in y0
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_hpartial_differentiable`12_in z implies SVF1 (2,(pdiff1 (f,1)),z) is_differentiable_in y0 )
assume that
A1: z = <*x0,y0*> and
A2: f is_hpartial_differentiable`12_in z ; ::_thesis: SVF1 (2,(pdiff1 (f,1)),z) is_differentiable_in y0
consider x1, y1 being Real such that
A3: z = <*x1,y1*> and
A4: ex N being Neighbourhood of y1 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) by A2, Def3;
y0 = y1 by A1, A3, FINSEQ_1:77;
hence SVF1 (2,(pdiff1 (f,1)),z) is_differentiable_in y0 by A4, FDIFF_1:def_4; ::_thesis: verum
end;
theorem :: PDIFF_3:3
for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`21_in z holds
SVF1 (1,(pdiff1 (f,2)),z) is_differentiable_in x0
proof
let x0, y0 be Real; ::_thesis: for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`21_in z holds
SVF1 (1,(pdiff1 (f,2)),z) is_differentiable_in x0
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`21_in z holds
SVF1 (1,(pdiff1 (f,2)),z) is_differentiable_in x0
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_hpartial_differentiable`21_in z implies SVF1 (1,(pdiff1 (f,2)),z) is_differentiable_in x0 )
assume that
A1: z = <*x0,y0*> and
A2: f is_hpartial_differentiable`21_in z ; ::_thesis: SVF1 (1,(pdiff1 (f,2)),z) is_differentiable_in x0
consider x1, y1 being Real such that
A3: z = <*x1,y1*> and
A4: ex N being Neighbourhood of x1 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) by A2, Def4;
x0 = x1 by A1, A3, FINSEQ_1:77;
hence SVF1 (1,(pdiff1 (f,2)),z) is_differentiable_in x0 by A4, FDIFF_1:def_4; ::_thesis: verum
end;
theorem :: PDIFF_3:4
for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`22_in z holds
SVF1 (2,(pdiff1 (f,2)),z) is_differentiable_in y0
proof
let x0, y0 be Real; ::_thesis: for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`22_in z holds
SVF1 (2,(pdiff1 (f,2)),z) is_differentiable_in y0
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`22_in z holds
SVF1 (2,(pdiff1 (f,2)),z) is_differentiable_in y0
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_hpartial_differentiable`22_in z implies SVF1 (2,(pdiff1 (f,2)),z) is_differentiable_in y0 )
assume that
A1: z = <*x0,y0*> and
A2: f is_hpartial_differentiable`22_in z ; ::_thesis: SVF1 (2,(pdiff1 (f,2)),z) is_differentiable_in y0
consider x1, y1 being Real such that
A3: z = <*x1,y1*> and
A4: ex N being Neighbourhood of y1 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) by A2, Def5;
y0 = y1 by A1, A3, FINSEQ_1:77;
hence SVF1 (2,(pdiff1 (f,2)),z) is_differentiable_in y0 by A4, FDIFF_1:def_4; ::_thesis: verum
end;
theorem Th5: :: PDIFF_3:5
for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`11_in z holds
hpartdiff11 (f,z) = diff ((SVF1 (1,(pdiff1 (f,1)),z)),x0)
proof
let x0, y0 be Real; ::_thesis: for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`11_in z holds
hpartdiff11 (f,z) = diff ((SVF1 (1,(pdiff1 (f,1)),z)),x0)
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`11_in z holds
hpartdiff11 (f,z) = diff ((SVF1 (1,(pdiff1 (f,1)),z)),x0)
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_hpartial_differentiable`11_in z implies hpartdiff11 (f,z) = diff ((SVF1 (1,(pdiff1 (f,1)),z)),x0) )
set r = hpartdiff11 (f,z);
assume that
A1: z = <*x0,y0*> and
A2: f is_hpartial_differentiable`11_in z ; ::_thesis: hpartdiff11 (f,z) = diff ((SVF1 (1,(pdiff1 (f,1)),z)),x0)
consider x1, y1 being Real such that
A3: z = <*x1,y1*> and
A4: ex N being Neighbourhood of x1 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) by A2, Def2;
consider N being Neighbourhood of x1 such that
A5: N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) and
A6: ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) by A4;
A7: x0 = x1 by A1, A3, FINSEQ_1:77;
then A8: SVF1 (1,(pdiff1 (f,1)),z) is_differentiable_in x0 by A5, A6, FDIFF_1:def_4;
consider L being LinearFunc, R being RestFunc such that
A9: for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) by A6;
hpartdiff11 (f,z) = L . 1 by A2, A3, A5, A9, Def6;
hence hpartdiff11 (f,z) = diff ((SVF1 (1,(pdiff1 (f,1)),z)),x0) by A5, A9, A7, A8, FDIFF_1:def_5; ::_thesis: verum
end;
theorem Th6: :: PDIFF_3:6
for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`12_in z holds
hpartdiff12 (f,z) = diff ((SVF1 (2,(pdiff1 (f,1)),z)),y0)
proof
let x0, y0 be Real; ::_thesis: for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`12_in z holds
hpartdiff12 (f,z) = diff ((SVF1 (2,(pdiff1 (f,1)),z)),y0)
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`12_in z holds
hpartdiff12 (f,z) = diff ((SVF1 (2,(pdiff1 (f,1)),z)),y0)
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_hpartial_differentiable`12_in z implies hpartdiff12 (f,z) = diff ((SVF1 (2,(pdiff1 (f,1)),z)),y0) )
set r = hpartdiff12 (f,z);
assume that
A1: z = <*x0,y0*> and
A2: f is_hpartial_differentiable`12_in z ; ::_thesis: hpartdiff12 (f,z) = diff ((SVF1 (2,(pdiff1 (f,1)),z)),y0)
consider x1, y1 being Real such that
A3: z = <*x1,y1*> and
A4: ex N being Neighbourhood of y1 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) by A2, Def3;
consider N being Neighbourhood of y1 such that
A5: N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) and
A6: ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) by A4;
A7: y0 = y1 by A1, A3, FINSEQ_1:77;
then A8: SVF1 (2,(pdiff1 (f,1)),z) is_differentiable_in y0 by A5, A6, FDIFF_1:def_4;
consider L being LinearFunc, R being RestFunc such that
A9: for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) by A6;
hpartdiff12 (f,z) = L . 1 by A2, A3, A5, A9, Def7;
hence hpartdiff12 (f,z) = diff ((SVF1 (2,(pdiff1 (f,1)),z)),y0) by A5, A9, A7, A8, FDIFF_1:def_5; ::_thesis: verum
end;
theorem Th7: :: PDIFF_3:7
for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`21_in z holds
hpartdiff21 (f,z) = diff ((SVF1 (1,(pdiff1 (f,2)),z)),x0)
proof
let x0, y0 be Real; ::_thesis: for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`21_in z holds
hpartdiff21 (f,z) = diff ((SVF1 (1,(pdiff1 (f,2)),z)),x0)
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`21_in z holds
hpartdiff21 (f,z) = diff ((SVF1 (1,(pdiff1 (f,2)),z)),x0)
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_hpartial_differentiable`21_in z implies hpartdiff21 (f,z) = diff ((SVF1 (1,(pdiff1 (f,2)),z)),x0) )
set r = hpartdiff21 (f,z);
assume that
A1: z = <*x0,y0*> and
A2: f is_hpartial_differentiable`21_in z ; ::_thesis: hpartdiff21 (f,z) = diff ((SVF1 (1,(pdiff1 (f,2)),z)),x0)
consider x1, y1 being Real such that
A3: z = <*x1,y1*> and
A4: ex N being Neighbourhood of x1 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) by A2, Def4;
consider N being Neighbourhood of x1 such that
A5: N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) and
A6: ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) by A4;
A7: x0 = x1 by A1, A3, FINSEQ_1:77;
then A8: SVF1 (1,(pdiff1 (f,2)),z) is_differentiable_in x0 by A5, A6, FDIFF_1:def_4;
consider L being LinearFunc, R being RestFunc such that
A9: for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x1) = (L . (x - x1)) + (R . (x - x1)) by A6;
hpartdiff21 (f,z) = L . 1 by A2, A3, A5, A9, Def8;
hence hpartdiff21 (f,z) = diff ((SVF1 (1,(pdiff1 (f,2)),z)),x0) by A5, A9, A7, A8, FDIFF_1:def_5; ::_thesis: verum
end;
theorem Th8: :: PDIFF_3:8
for x0, y0 being Real
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`22_in z holds
hpartdiff22 (f,z) = diff ((SVF1 (2,(pdiff1 (f,2)),z)),y0)
proof
let x0, y0 be Real; ::_thesis: for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`22_in z holds
hpartdiff22 (f,z) = diff ((SVF1 (2,(pdiff1 (f,2)),z)),y0)
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_hpartial_differentiable`22_in z holds
hpartdiff22 (f,z) = diff ((SVF1 (2,(pdiff1 (f,2)),z)),y0)
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( z = <*x0,y0*> & f is_hpartial_differentiable`22_in z implies hpartdiff22 (f,z) = diff ((SVF1 (2,(pdiff1 (f,2)),z)),y0) )
set r = hpartdiff22 (f,z);
assume that
A1: z = <*x0,y0*> and
A2: f is_hpartial_differentiable`22_in z ; ::_thesis: hpartdiff22 (f,z) = diff ((SVF1 (2,(pdiff1 (f,2)),z)),y0)
consider x1, y1 being Real such that
A3: z = <*x1,y1*> and
A4: ex N being Neighbourhood of y1 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) ) by A2, Def5;
consider N being Neighbourhood of y1 such that
A5: N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) and
A6: ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) by A4;
A7: y0 = y1 by A1, A3, FINSEQ_1:77;
then A8: SVF1 (2,(pdiff1 (f,2)),z) is_differentiable_in y0 by A5, A6, FDIFF_1:def_4;
consider L being LinearFunc, R being RestFunc such that
A9: for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y1) = (L . (y - y1)) + (R . (y - y1)) by A6;
hpartdiff22 (f,z) = L . 1 by A2, A3, A5, A9, Def9;
hence hpartdiff22 (f,z) = diff ((SVF1 (2,(pdiff1 (f,2)),z)),y0) by A5, A9, A7, A8, FDIFF_1:def_5; ::_thesis: verum
end;
definition
let f be PartFunc of (REAL 2),REAL;
let Z be set ;
predf is_hpartial_differentiable`11_on Z means :Def10: :: PDIFF_3:def 10
( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f | Z is_hpartial_differentiable`11_in z ) );
predf is_hpartial_differentiable`12_on Z means :Def11: :: PDIFF_3:def 11
( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f | Z is_hpartial_differentiable`12_in z ) );
predf is_hpartial_differentiable`21_on Z means :Def12: :: PDIFF_3:def 12
( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f | Z is_hpartial_differentiable`21_in z ) );
predf is_hpartial_differentiable`22_on Z means :Def13: :: PDIFF_3:def 13
( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f | Z is_hpartial_differentiable`22_in z ) );
end;
:: deftheorem Def10 defines is_hpartial_differentiable`11_on PDIFF_3:def_10_:_
for f being PartFunc of (REAL 2),REAL
for Z being set holds
( f is_hpartial_differentiable`11_on Z iff ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f | Z is_hpartial_differentiable`11_in z ) ) );
:: deftheorem Def11 defines is_hpartial_differentiable`12_on PDIFF_3:def_11_:_
for f being PartFunc of (REAL 2),REAL
for Z being set holds
( f is_hpartial_differentiable`12_on Z iff ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f | Z is_hpartial_differentiable`12_in z ) ) );
:: deftheorem Def12 defines is_hpartial_differentiable`21_on PDIFF_3:def_12_:_
for f being PartFunc of (REAL 2),REAL
for Z being set holds
( f is_hpartial_differentiable`21_on Z iff ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f | Z is_hpartial_differentiable`21_in z ) ) );
:: deftheorem Def13 defines is_hpartial_differentiable`22_on PDIFF_3:def_13_:_
for f being PartFunc of (REAL 2),REAL
for Z being set holds
( f is_hpartial_differentiable`22_on Z iff ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f | Z is_hpartial_differentiable`22_in z ) ) );
definition
let f be PartFunc of (REAL 2),REAL;
let Z be set ;
assume A1: f is_hpartial_differentiable`11_on Z ;
funcf `hpartial11| Z -> PartFunc of (REAL 2),REAL means :: PDIFF_3:def 14
( dom it = Z & ( for z being Element of REAL 2 st z in Z holds
it . z = hpartdiff11 (f,z) ) );
existence
ex b1 being PartFunc of (REAL 2),REAL st
( dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds
b1 . z = hpartdiff11 (f,z) ) )
proof
deffunc H1( Element of REAL 2) -> Real = hpartdiff11 (f,$1);
defpred S1[ Element of REAL 2] means $1 in Z;
consider F being PartFunc of (REAL 2),REAL such that
A2: ( ( for z being Element of REAL 2 holds
( z in dom F iff S1[z] ) ) & ( for z being Element of REAL 2 st z in dom F holds
F . z = H1(z) ) ) from SEQ_1:sch_3();
take F ; ::_thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds
F . z = hpartdiff11 (f,z) ) )
now__::_thesis:_for_y_being_set_st_y_in_Z_holds_
y_in_dom_F
Z c= dom f by A1, Def10;
then A3: Z is Subset of (REAL 2) by XBOOLE_1:1;
let y be set ; ::_thesis: ( y in Z implies y in dom F )
assume y in Z ; ::_thesis: y in dom F
hence y in dom F by A2, A3; ::_thesis: verum
end;
then A4: Z c= dom F by TARSKI:def_3;
for y being set st y in dom F holds
y in Z by A2;
then dom F c= Z by TARSKI:def_3;
hence dom F = Z by A4, XBOOLE_0:def_10; ::_thesis: for z being Element of REAL 2 st z in Z holds
F . z = hpartdiff11 (f,z)
hereby ::_thesis: verum
let z be Element of REAL 2; ::_thesis: ( z in Z implies F . z = hpartdiff11 (f,z) )
assume z in Z ; ::_thesis: F . z = hpartdiff11 (f,z)
then z in dom F by A2;
hence F . z = hpartdiff11 (f,z) by A2; ::_thesis: verum
end;
end;
uniqueness
for b1, b2 being PartFunc of (REAL 2),REAL st dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds
b1 . z = hpartdiff11 (f,z) ) & dom b2 = Z & ( for z being Element of REAL 2 st z in Z holds
b2 . z = hpartdiff11 (f,z) ) holds
b1 = b2
proof
let F, G be PartFunc of (REAL 2),REAL; ::_thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds
F . z = hpartdiff11 (f,z) ) & dom G = Z & ( for z being Element of REAL 2 st z in Z holds
G . z = hpartdiff11 (f,z) ) implies F = G )
assume that
A5: dom F = Z and
A6: for z being Element of REAL 2 st z in Z holds
F . z = hpartdiff11 (f,z) and
A7: dom G = Z and
A8: for z being Element of REAL 2 st z in Z holds
G . z = hpartdiff11 (f,z) ; ::_thesis: F = G
now__::_thesis:_for_z_being_Element_of_REAL_2_st_z_in_dom_F_holds_
F_._z_=_G_._z
let z be Element of REAL 2; ::_thesis: ( z in dom F implies F . z = G . z )
assume A9: z in dom F ; ::_thesis: F . z = G . z
then F . z = hpartdiff11 (f,z) by A5, A6;
hence F . z = G . z by A5, A8, A9; ::_thesis: verum
end;
hence F = G by A5, A7, PARTFUN1:5; ::_thesis: verum
end;
end;
:: deftheorem defines `hpartial11| PDIFF_3:def_14_:_
for f being PartFunc of (REAL 2),REAL
for Z being set st f is_hpartial_differentiable`11_on Z holds
for b3 being PartFunc of (REAL 2),REAL holds
( b3 = f `hpartial11| Z iff ( dom b3 = Z & ( for z being Element of REAL 2 st z in Z holds
b3 . z = hpartdiff11 (f,z) ) ) );
definition
let f be PartFunc of (REAL 2),REAL;
let Z be set ;
assume A1: f is_hpartial_differentiable`12_on Z ;
funcf `hpartial12| Z -> PartFunc of (REAL 2),REAL means :: PDIFF_3:def 15
( dom it = Z & ( for z being Element of REAL 2 st z in Z holds
it . z = hpartdiff12 (f,z) ) );
existence
ex b1 being PartFunc of (REAL 2),REAL st
( dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds
b1 . z = hpartdiff12 (f,z) ) )
proof
deffunc H1( Element of REAL 2) -> Real = hpartdiff12 (f,$1);
defpred S1[ Element of REAL 2] means $1 in Z;
consider F being PartFunc of (REAL 2),REAL such that
A2: ( ( for z being Element of REAL 2 holds
( z in dom F iff S1[z] ) ) & ( for z being Element of REAL 2 st z in dom F holds
F . z = H1(z) ) ) from SEQ_1:sch_3();
take F ; ::_thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds
F . z = hpartdiff12 (f,z) ) )
now__::_thesis:_for_y_being_set_st_y_in_Z_holds_
y_in_dom_F
Z c= dom f by A1, Def11;
then A3: Z is Subset of (REAL 2) by XBOOLE_1:1;
let y be set ; ::_thesis: ( y in Z implies y in dom F )
assume y in Z ; ::_thesis: y in dom F
hence y in dom F by A2, A3; ::_thesis: verum
end;
then A4: Z c= dom F by TARSKI:def_3;
for y being set st y in dom F holds
y in Z by A2;
then dom F c= Z by TARSKI:def_3;
hence dom F = Z by A4, XBOOLE_0:def_10; ::_thesis: for z being Element of REAL 2 st z in Z holds
F . z = hpartdiff12 (f,z)
hereby ::_thesis: verum
let z be Element of REAL 2; ::_thesis: ( z in Z implies F . z = hpartdiff12 (f,z) )
assume z in Z ; ::_thesis: F . z = hpartdiff12 (f,z)
then z in dom F by A2;
hence F . z = hpartdiff12 (f,z) by A2; ::_thesis: verum
end;
end;
uniqueness
for b1, b2 being PartFunc of (REAL 2),REAL st dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds
b1 . z = hpartdiff12 (f,z) ) & dom b2 = Z & ( for z being Element of REAL 2 st z in Z holds
b2 . z = hpartdiff12 (f,z) ) holds
b1 = b2
proof
let F, G be PartFunc of (REAL 2),REAL; ::_thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds
F . z = hpartdiff12 (f,z) ) & dom G = Z & ( for z being Element of REAL 2 st z in Z holds
G . z = hpartdiff12 (f,z) ) implies F = G )
assume that
A5: dom F = Z and
A6: for z being Element of REAL 2 st z in Z holds
F . z = hpartdiff12 (f,z) and
A7: dom G = Z and
A8: for z being Element of REAL 2 st z in Z holds
G . z = hpartdiff12 (f,z) ; ::_thesis: F = G
now__::_thesis:_for_z_being_Element_of_REAL_2_st_z_in_dom_F_holds_
F_._z_=_G_._z
let z be Element of REAL 2; ::_thesis: ( z in dom F implies F . z = G . z )
assume A9: z in dom F ; ::_thesis: F . z = G . z
then F . z = hpartdiff12 (f,z) by A5, A6;
hence F . z = G . z by A5, A8, A9; ::_thesis: verum
end;
hence F = G by A5, A7, PARTFUN1:5; ::_thesis: verum
end;
end;
:: deftheorem defines `hpartial12| PDIFF_3:def_15_:_
for f being PartFunc of (REAL 2),REAL
for Z being set st f is_hpartial_differentiable`12_on Z holds
for b3 being PartFunc of (REAL 2),REAL holds
( b3 = f `hpartial12| Z iff ( dom b3 = Z & ( for z being Element of REAL 2 st z in Z holds
b3 . z = hpartdiff12 (f,z) ) ) );
definition
let f be PartFunc of (REAL 2),REAL;
let Z be set ;
assume A1: f is_hpartial_differentiable`21_on Z ;
funcf `hpartial21| Z -> PartFunc of (REAL 2),REAL means :: PDIFF_3:def 16
( dom it = Z & ( for z being Element of REAL 2 st z in Z holds
it . z = hpartdiff21 (f,z) ) );
existence
ex b1 being PartFunc of (REAL 2),REAL st
( dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds
b1 . z = hpartdiff21 (f,z) ) )
proof
deffunc H1( Element of REAL 2) -> Real = hpartdiff21 (f,$1);
defpred S1[ Element of REAL 2] means $1 in Z;
consider F being PartFunc of (REAL 2),REAL such that
A2: ( ( for z being Element of REAL 2 holds
( z in dom F iff S1[z] ) ) & ( for z being Element of REAL 2 st z in dom F holds
F . z = H1(z) ) ) from SEQ_1:sch_3();
take F ; ::_thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds
F . z = hpartdiff21 (f,z) ) )
now__::_thesis:_for_y_being_set_st_y_in_Z_holds_
y_in_dom_F
Z c= dom f by A1, Def12;
then A3: Z is Subset of (REAL 2) by XBOOLE_1:1;
let y be set ; ::_thesis: ( y in Z implies y in dom F )
assume y in Z ; ::_thesis: y in dom F
hence y in dom F by A2, A3; ::_thesis: verum
end;
then A4: Z c= dom F by TARSKI:def_3;
for y being set st y in dom F holds
y in Z by A2;
then dom F c= Z by TARSKI:def_3;
hence dom F = Z by A4, XBOOLE_0:def_10; ::_thesis: for z being Element of REAL 2 st z in Z holds
F . z = hpartdiff21 (f,z)
hereby ::_thesis: verum
let z be Element of REAL 2; ::_thesis: ( z in Z implies F . z = hpartdiff21 (f,z) )
assume z in Z ; ::_thesis: F . z = hpartdiff21 (f,z)
then z in dom F by A2;
hence F . z = hpartdiff21 (f,z) by A2; ::_thesis: verum
end;
end;
uniqueness
for b1, b2 being PartFunc of (REAL 2),REAL st dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds
b1 . z = hpartdiff21 (f,z) ) & dom b2 = Z & ( for z being Element of REAL 2 st z in Z holds
b2 . z = hpartdiff21 (f,z) ) holds
b1 = b2
proof
let F, G be PartFunc of (REAL 2),REAL; ::_thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds
F . z = hpartdiff21 (f,z) ) & dom G = Z & ( for z being Element of REAL 2 st z in Z holds
G . z = hpartdiff21 (f,z) ) implies F = G )
assume that
A5: dom F = Z and
A6: for z being Element of REAL 2 st z in Z holds
F . z = hpartdiff21 (f,z) and
A7: dom G = Z and
A8: for z being Element of REAL 2 st z in Z holds
G . z = hpartdiff21 (f,z) ; ::_thesis: F = G
now__::_thesis:_for_z_being_Element_of_REAL_2_st_z_in_dom_F_holds_
F_._z_=_G_._z
let z be Element of REAL 2; ::_thesis: ( z in dom F implies F . z = G . z )
assume A9: z in dom F ; ::_thesis: F . z = G . z
then F . z = hpartdiff21 (f,z) by A5, A6;
hence F . z = G . z by A5, A8, A9; ::_thesis: verum
end;
hence F = G by A5, A7, PARTFUN1:5; ::_thesis: verum
end;
end;
:: deftheorem defines `hpartial21| PDIFF_3:def_16_:_
for f being PartFunc of (REAL 2),REAL
for Z being set st f is_hpartial_differentiable`21_on Z holds
for b3 being PartFunc of (REAL 2),REAL holds
( b3 = f `hpartial21| Z iff ( dom b3 = Z & ( for z being Element of REAL 2 st z in Z holds
b3 . z = hpartdiff21 (f,z) ) ) );
definition
let f be PartFunc of (REAL 2),REAL;
let Z be set ;
assume A1: f is_hpartial_differentiable`22_on Z ;
funcf `hpartial22| Z -> PartFunc of (REAL 2),REAL means :: PDIFF_3:def 17
( dom it = Z & ( for z being Element of REAL 2 st z in Z holds
it . z = hpartdiff22 (f,z) ) );
existence
ex b1 being PartFunc of (REAL 2),REAL st
( dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds
b1 . z = hpartdiff22 (f,z) ) )
proof
deffunc H1( Element of REAL 2) -> Real = hpartdiff22 (f,$1);
defpred S1[ Element of REAL 2] means $1 in Z;
consider F being PartFunc of (REAL 2),REAL such that
A2: ( ( for z being Element of REAL 2 holds
( z in dom F iff S1[z] ) ) & ( for z being Element of REAL 2 st z in dom F holds
F . z = H1(z) ) ) from SEQ_1:sch_3();
take F ; ::_thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds
F . z = hpartdiff22 (f,z) ) )
now__::_thesis:_for_y_being_set_st_y_in_Z_holds_
y_in_dom_F
Z c= dom f by A1, Def13;
then A3: Z is Subset of (REAL 2) by XBOOLE_1:1;
let y be set ; ::_thesis: ( y in Z implies y in dom F )
assume y in Z ; ::_thesis: y in dom F
hence y in dom F by A2, A3; ::_thesis: verum
end;
then A4: Z c= dom F by TARSKI:def_3;
for y being set st y in dom F holds
y in Z by A2;
then dom F c= Z by TARSKI:def_3;
hence dom F = Z by A4, XBOOLE_0:def_10; ::_thesis: for z being Element of REAL 2 st z in Z holds
F . z = hpartdiff22 (f,z)
hereby ::_thesis: verum
let z be Element of REAL 2; ::_thesis: ( z in Z implies F . z = hpartdiff22 (f,z) )
assume z in Z ; ::_thesis: F . z = hpartdiff22 (f,z)
then z in dom F by A2;
hence F . z = hpartdiff22 (f,z) by A2; ::_thesis: verum
end;
end;
uniqueness
for b1, b2 being PartFunc of (REAL 2),REAL st dom b1 = Z & ( for z being Element of REAL 2 st z in Z holds
b1 . z = hpartdiff22 (f,z) ) & dom b2 = Z & ( for z being Element of REAL 2 st z in Z holds
b2 . z = hpartdiff22 (f,z) ) holds
b1 = b2
proof
let F, G be PartFunc of (REAL 2),REAL; ::_thesis: ( dom F = Z & ( for z being Element of REAL 2 st z in Z holds
F . z = hpartdiff22 (f,z) ) & dom G = Z & ( for z being Element of REAL 2 st z in Z holds
G . z = hpartdiff22 (f,z) ) implies F = G )
assume that
A5: dom F = Z and
A6: for z being Element of REAL 2 st z in Z holds
F . z = hpartdiff22 (f,z) and
A7: dom G = Z and
A8: for z being Element of REAL 2 st z in Z holds
G . z = hpartdiff22 (f,z) ; ::_thesis: F = G
now__::_thesis:_for_z_being_Element_of_REAL_2_st_z_in_dom_F_holds_
F_._z_=_G_._z
let z be Element of REAL 2; ::_thesis: ( z in dom F implies F . z = G . z )
assume A9: z in dom F ; ::_thesis: F . z = G . z
then F . z = hpartdiff22 (f,z) by A5, A6;
hence F . z = G . z by A5, A8, A9; ::_thesis: verum
end;
hence F = G by A5, A7, PARTFUN1:5; ::_thesis: verum
end;
end;
:: deftheorem defines `hpartial22| PDIFF_3:def_17_:_
for f being PartFunc of (REAL 2),REAL
for Z being set st f is_hpartial_differentiable`22_on Z holds
for b3 being PartFunc of (REAL 2),REAL holds
( b3 = f `hpartial22| Z iff ( dom b3 = Z & ( for z being Element of REAL 2 st z in Z holds
b3 . z = hpartdiff22 (f,z) ) ) );
begin
theorem Th9: :: PDIFF_3:9
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL holds
( f is_hpartial_differentiable`11_in z iff pdiff1 (f,1) is_partial_differentiable_in z,1 )
proof
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL holds
( f is_hpartial_differentiable`11_in z iff pdiff1 (f,1) is_partial_differentiable_in z,1 )
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`11_in z iff pdiff1 (f,1) is_partial_differentiable_in z,1 )
thus ( f is_hpartial_differentiable`11_in z implies pdiff1 (f,1) is_partial_differentiable_in z,1 ) ::_thesis: ( pdiff1 (f,1) is_partial_differentiable_in z,1 implies f is_hpartial_differentiable`11_in z )
proof
assume f is_hpartial_differentiable`11_in z ; ::_thesis: pdiff1 (f,1) is_partial_differentiable_in z,1
then ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by Def2;
hence pdiff1 (f,1) is_partial_differentiable_in z,1 by PDIFF_2:9; ::_thesis: verum
end;
assume pdiff1 (f,1) is_partial_differentiable_in z,1 ; ::_thesis: f is_hpartial_differentiable`11_in z
then ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,1)),z)) . x) - ((SVF1 (1,(pdiff1 (f,1)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by PDIFF_2:9;
hence f is_hpartial_differentiable`11_in z by Def2; ::_thesis: verum
end;
theorem Th10: :: PDIFF_3:10
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL holds
( f is_hpartial_differentiable`12_in z iff pdiff1 (f,1) is_partial_differentiable_in z,2 )
proof
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL holds
( f is_hpartial_differentiable`12_in z iff pdiff1 (f,1) is_partial_differentiable_in z,2 )
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`12_in z iff pdiff1 (f,1) is_partial_differentiable_in z,2 )
thus ( f is_hpartial_differentiable`12_in z implies pdiff1 (f,1) is_partial_differentiable_in z,2 ) ::_thesis: ( pdiff1 (f,1) is_partial_differentiable_in z,2 implies f is_hpartial_differentiable`12_in z )
proof
assume f is_hpartial_differentiable`12_in z ; ::_thesis: pdiff1 (f,1) is_partial_differentiable_in z,2
then ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) by Def3;
hence pdiff1 (f,1) is_partial_differentiable_in z,2 by PDIFF_2:10; ::_thesis: verum
end;
assume pdiff1 (f,1) is_partial_differentiable_in z,2 ; ::_thesis: f is_hpartial_differentiable`12_in z
then ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,1)),z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,1)),z)) . y) - ((SVF1 (2,(pdiff1 (f,1)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) by PDIFF_2:10;
hence f is_hpartial_differentiable`12_in z by Def3; ::_thesis: verum
end;
theorem Th11: :: PDIFF_3:11
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL holds
( f is_hpartial_differentiable`21_in z iff pdiff1 (f,2) is_partial_differentiable_in z,1 )
proof
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL holds
( f is_hpartial_differentiable`21_in z iff pdiff1 (f,2) is_partial_differentiable_in z,1 )
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`21_in z iff pdiff1 (f,2) is_partial_differentiable_in z,1 )
thus ( f is_hpartial_differentiable`21_in z implies pdiff1 (f,2) is_partial_differentiable_in z,1 ) ::_thesis: ( pdiff1 (f,2) is_partial_differentiable_in z,1 implies f is_hpartial_differentiable`21_in z )
proof
assume f is_hpartial_differentiable`21_in z ; ::_thesis: pdiff1 (f,2) is_partial_differentiable_in z,1
then ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by Def4;
hence pdiff1 (f,2) is_partial_differentiable_in z,1 by PDIFF_2:9; ::_thesis: verum
end;
assume pdiff1 (f,2) is_partial_differentiable_in z,1 ; ::_thesis: f is_hpartial_differentiable`21_in z
then ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(pdiff1 (f,2)),z)) . x) - ((SVF1 (1,(pdiff1 (f,2)),z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by PDIFF_2:9;
hence f is_hpartial_differentiable`21_in z by Def4; ::_thesis: verum
end;
theorem Th12: :: PDIFF_3:12
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL holds
( f is_hpartial_differentiable`22_in z iff pdiff1 (f,2) is_partial_differentiable_in z,2 )
proof
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL holds
( f is_hpartial_differentiable`22_in z iff pdiff1 (f,2) is_partial_differentiable_in z,2 )
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`22_in z iff pdiff1 (f,2) is_partial_differentiable_in z,2 )
thus ( f is_hpartial_differentiable`22_in z implies pdiff1 (f,2) is_partial_differentiable_in z,2 ) ::_thesis: ( pdiff1 (f,2) is_partial_differentiable_in z,2 implies f is_hpartial_differentiable`22_in z )
proof
assume f is_hpartial_differentiable`22_in z ; ::_thesis: pdiff1 (f,2) is_partial_differentiable_in z,2
then ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) by Def5;
hence pdiff1 (f,2) is_partial_differentiable_in z,2 by PDIFF_2:10; ::_thesis: verum
end;
assume pdiff1 (f,2) is_partial_differentiable_in z,2 ; ::_thesis: f is_hpartial_differentiable`22_in z
then ex x0, y0 being Real st
( z = <*x0,y0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(pdiff1 (f,2)),z)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(pdiff1 (f,2)),z)) . y) - ((SVF1 (2,(pdiff1 (f,2)),z)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) by PDIFF_2:10;
hence f is_hpartial_differentiable`22_in z by Def5; ::_thesis: verum
end;
theorem Th13: :: PDIFF_3:13
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`11_in z holds
hpartdiff11 (f,z) = partdiff ((pdiff1 (f,1)),z,1)
proof
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`11_in z holds
hpartdiff11 (f,z) = partdiff ((pdiff1 (f,1)),z,1)
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`11_in z implies hpartdiff11 (f,z) = partdiff ((pdiff1 (f,1)),z,1) )
consider x0, y0 being Real such that
A1: z = <*x0,y0*> by FINSEQ_2:100;
assume A2: f is_hpartial_differentiable`11_in z ; ::_thesis: hpartdiff11 (f,z) = partdiff ((pdiff1 (f,1)),z,1)
then A3: pdiff1 (f,1) is_partial_differentiable_in z,1 by Th9;
hpartdiff11 (f,z) = diff ((SVF1 (1,(pdiff1 (f,1)),z)),x0) by A2, A1, Th5
.= partdiff ((pdiff1 (f,1)),z,1) by A1, A3, PDIFF_2:13 ;
hence hpartdiff11 (f,z) = partdiff ((pdiff1 (f,1)),z,1) ; ::_thesis: verum
end;
theorem Th14: :: PDIFF_3:14
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`12_in z holds
hpartdiff12 (f,z) = partdiff ((pdiff1 (f,1)),z,2)
proof
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`12_in z holds
hpartdiff12 (f,z) = partdiff ((pdiff1 (f,1)),z,2)
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`12_in z implies hpartdiff12 (f,z) = partdiff ((pdiff1 (f,1)),z,2) )
consider x0, y0 being Real such that
A1: z = <*x0,y0*> by FINSEQ_2:100;
assume A2: f is_hpartial_differentiable`12_in z ; ::_thesis: hpartdiff12 (f,z) = partdiff ((pdiff1 (f,1)),z,2)
then A3: pdiff1 (f,1) is_partial_differentiable_in z,2 by Th10;
hpartdiff12 (f,z) = diff ((SVF1 (2,(pdiff1 (f,1)),z)),y0) by A2, A1, Th6
.= partdiff ((pdiff1 (f,1)),z,2) by A1, A3, PDIFF_2:14 ;
hence hpartdiff12 (f,z) = partdiff ((pdiff1 (f,1)),z,2) ; ::_thesis: verum
end;
theorem Th15: :: PDIFF_3:15
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`21_in z holds
hpartdiff21 (f,z) = partdiff ((pdiff1 (f,2)),z,1)
proof
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`21_in z holds
hpartdiff21 (f,z) = partdiff ((pdiff1 (f,2)),z,1)
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`21_in z implies hpartdiff21 (f,z) = partdiff ((pdiff1 (f,2)),z,1) )
consider x0, y0 being Real such that
A1: z = <*x0,y0*> by FINSEQ_2:100;
assume A2: f is_hpartial_differentiable`21_in z ; ::_thesis: hpartdiff21 (f,z) = partdiff ((pdiff1 (f,2)),z,1)
then A3: pdiff1 (f,2) is_partial_differentiable_in z,1 by Th11;
hpartdiff21 (f,z) = diff ((SVF1 (1,(pdiff1 (f,2)),z)),x0) by A2, A1, Th7
.= partdiff ((pdiff1 (f,2)),z,1) by A1, A3, PDIFF_2:13 ;
hence hpartdiff21 (f,z) = partdiff ((pdiff1 (f,2)),z,1) ; ::_thesis: verum
end;
theorem Th16: :: PDIFF_3:16
for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`22_in z holds
hpartdiff22 (f,z) = partdiff ((pdiff1 (f,2)),z,2)
proof
let z be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`22_in z holds
hpartdiff22 (f,z) = partdiff ((pdiff1 (f,2)),z,2)
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`22_in z implies hpartdiff22 (f,z) = partdiff ((pdiff1 (f,2)),z,2) )
consider x0, y0 being Real such that
A1: z = <*x0,y0*> by FINSEQ_2:100;
assume A2: f is_hpartial_differentiable`22_in z ; ::_thesis: hpartdiff22 (f,z) = partdiff ((pdiff1 (f,2)),z,2)
then A3: pdiff1 (f,2) is_partial_differentiable_in z,2 by Th12;
hpartdiff22 (f,z) = diff ((SVF1 (2,(pdiff1 (f,2)),z)),y0) by A2, A1, Th8
.= partdiff ((pdiff1 (f,2)),z,2) by A1, A3, PDIFF_2:14 ;
hence hpartdiff22 (f,z) = partdiff ((pdiff1 (f,2)),z,2) ; ::_thesis: verum
end;
theorem :: PDIFF_3:17
for f being PartFunc of (REAL 2),REAL
for z0 being Element of REAL 2
for N being Neighbourhood of (proj (1,2)) . z0 st f is_hpartial_differentiable`11_in z0 & N c= dom (SVF1 (1,(pdiff1 (f,1)),z0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff11 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c))) )
proof
let f be PartFunc of (REAL 2),REAL; ::_thesis: for z0 being Element of REAL 2
for N being Neighbourhood of (proj (1,2)) . z0 st f is_hpartial_differentiable`11_in z0 & N c= dom (SVF1 (1,(pdiff1 (f,1)),z0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff11 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c))) )
let z0 be Element of REAL 2; ::_thesis: for N being Neighbourhood of (proj (1,2)) . z0 st f is_hpartial_differentiable`11_in z0 & N c= dom (SVF1 (1,(pdiff1 (f,1)),z0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff11 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c))) )
let N be Neighbourhood of (proj (1,2)) . z0; ::_thesis: ( f is_hpartial_differentiable`11_in z0 & N c= dom (SVF1 (1,(pdiff1 (f,1)),z0)) implies for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff11 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c))) ) )
assume that
A1: f is_hpartial_differentiable`11_in z0 and
A2: N c= dom (SVF1 (1,(pdiff1 (f,1)),z0)) ; ::_thesis: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff11 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c))) )
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff11 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c))) )
let c be constant Real_Sequence; ::_thesis: ( rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N implies ( (h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff11 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c))) ) )
assume A3: ( rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N ) ; ::_thesis: ( (h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff11 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c))) )
consider x0, y0 being Real such that
A4: z0 = <*x0,y0*> by FINSEQ_2:100;
A5: pdiff1 (f,1) is_partial_differentiable_in z0,1 by A1, Th9;
then partdiff ((pdiff1 (f,1)),z0,1) = diff ((SVF1 (1,(pdiff1 (f,1)),z0)),x0) by A4, PDIFF_2:13
.= hpartdiff11 (f,z0) by A1, A4, Th5 ;
hence ( (h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff11 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,1)),z0)) /* c))) ) by A2, A3, A5, PDIFF_2:17; ::_thesis: verum
end;
theorem :: PDIFF_3:18
for f being PartFunc of (REAL 2),REAL
for z0 being Element of REAL 2
for N being Neighbourhood of (proj (2,2)) . z0 st f is_hpartial_differentiable`12_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,1)),z0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff12 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c))) )
proof
let f be PartFunc of (REAL 2),REAL; ::_thesis: for z0 being Element of REAL 2
for N being Neighbourhood of (proj (2,2)) . z0 st f is_hpartial_differentiable`12_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,1)),z0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff12 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c))) )
let z0 be Element of REAL 2; ::_thesis: for N being Neighbourhood of (proj (2,2)) . z0 st f is_hpartial_differentiable`12_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,1)),z0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff12 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c))) )
let N be Neighbourhood of (proj (2,2)) . z0; ::_thesis: ( f is_hpartial_differentiable`12_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,1)),z0)) implies for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff12 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c))) ) )
assume that
A1: f is_hpartial_differentiable`12_in z0 and
A2: N c= dom (SVF1 (2,(pdiff1 (f,1)),z0)) ; ::_thesis: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff12 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c))) )
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff12 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c))) )
let c be constant Real_Sequence; ::_thesis: ( rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N implies ( (h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff12 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c))) ) )
assume A3: ( rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N ) ; ::_thesis: ( (h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff12 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c))) )
consider x0, y0 being Real such that
A4: z0 = <*x0,y0*> by FINSEQ_2:100;
A5: pdiff1 (f,1) is_partial_differentiable_in z0,2 by A1, Th10;
then partdiff ((pdiff1 (f,1)),z0,2) = diff ((SVF1 (2,(pdiff1 (f,1)),z0)),y0) by A4, PDIFF_2:14
.= hpartdiff12 (f,z0) by A1, A4, Th6 ;
hence ( (h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c)) is convergent & hpartdiff12 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),z0)) /* c))) ) by A2, A3, A5, PDIFF_2:18; ::_thesis: verum
end;
theorem :: PDIFF_3:19
for f being PartFunc of (REAL 2),REAL
for z0 being Element of REAL 2
for N being Neighbourhood of (proj (1,2)) . z0 st f is_hpartial_differentiable`21_in z0 & N c= dom (SVF1 (1,(pdiff1 (f,2)),z0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff21 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c))) )
proof
let f be PartFunc of (REAL 2),REAL; ::_thesis: for z0 being Element of REAL 2
for N being Neighbourhood of (proj (1,2)) . z0 st f is_hpartial_differentiable`21_in z0 & N c= dom (SVF1 (1,(pdiff1 (f,2)),z0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff21 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c))) )
let z0 be Element of REAL 2; ::_thesis: for N being Neighbourhood of (proj (1,2)) . z0 st f is_hpartial_differentiable`21_in z0 & N c= dom (SVF1 (1,(pdiff1 (f,2)),z0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff21 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c))) )
let N be Neighbourhood of (proj (1,2)) . z0; ::_thesis: ( f is_hpartial_differentiable`21_in z0 & N c= dom (SVF1 (1,(pdiff1 (f,2)),z0)) implies for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff21 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c))) ) )
assume that
A1: f is_hpartial_differentiable`21_in z0 and
A2: N c= dom (SVF1 (1,(pdiff1 (f,2)),z0)) ; ::_thesis: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff21 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c))) )
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: for c being constant Real_Sequence st rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff21 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c))) )
let c be constant Real_Sequence; ::_thesis: ( rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N implies ( (h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff21 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c))) ) )
assume A3: ( rng c = {((proj (1,2)) . z0)} & rng (h + c) c= N ) ; ::_thesis: ( (h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff21 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c))) )
consider x0, y0 being Real such that
A4: z0 = <*x0,y0*> by FINSEQ_2:100;
A5: pdiff1 (f,2) is_partial_differentiable_in z0,1 by A1, Th11;
then partdiff ((pdiff1 (f,2)),z0,1) = diff ((SVF1 (1,(pdiff1 (f,2)),z0)),x0) by A4, PDIFF_2:13
.= hpartdiff21 (f,z0) by A1, A4, Th7 ;
hence ( (h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff21 (f,z0) = lim ((h ") (#) (((SVF1 (1,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (1,(pdiff1 (f,2)),z0)) /* c))) ) by A2, A3, A5, PDIFF_2:17; ::_thesis: verum
end;
theorem :: PDIFF_3:20
for f being PartFunc of (REAL 2),REAL
for z0 being Element of REAL 2
for N being Neighbourhood of (proj (2,2)) . z0 st f is_hpartial_differentiable`22_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,2)),z0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) )
proof
let f be PartFunc of (REAL 2),REAL; ::_thesis: for z0 being Element of REAL 2
for N being Neighbourhood of (proj (2,2)) . z0 st f is_hpartial_differentiable`22_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,2)),z0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) )
let z0 be Element of REAL 2; ::_thesis: for N being Neighbourhood of (proj (2,2)) . z0 st f is_hpartial_differentiable`22_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,2)),z0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) )
let N be Neighbourhood of (proj (2,2)) . z0; ::_thesis: ( f is_hpartial_differentiable`22_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,2)),z0)) implies for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) ) )
assume that
A1: f is_hpartial_differentiable`22_in z0 and
A2: N c= dom (SVF1 (2,(pdiff1 (f,2)),z0)) ; ::_thesis: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) )
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) )
let c be constant Real_Sequence; ::_thesis: ( rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N implies ( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) ) )
assume A3: ( rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N ) ; ::_thesis: ( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) )
consider x0, y0 being Real such that
A4: z0 = <*x0,y0*> by FINSEQ_2:100;
A5: pdiff1 (f,2) is_partial_differentiable_in z0,2 by A1, Th12;
then partdiff ((pdiff1 (f,2)),z0,2) = diff ((SVF1 (2,(pdiff1 (f,2)),z0)),y0) by A4, PDIFF_2:14
.= hpartdiff22 (f,z0) by A1, A4, Th8 ;
hence ( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) ) by A2, A3, A5, PDIFF_2:18; ::_thesis: verum
end;
theorem :: PDIFF_3:21
for z0 being Element of REAL 2
for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 holds
( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) + (hpartdiff11 (f2,z0)) )
proof
let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 holds
( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) + (hpartdiff11 (f2,z0)) )
let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 implies ( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) + (hpartdiff11 (f2,z0)) ) )
assume that
A1: f1 is_hpartial_differentiable`11_in z0 and
A2: f2 is_hpartial_differentiable`11_in z0 ; ::_thesis: ( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) + (hpartdiff11 (f2,z0)) )
A3: ( pdiff1 (f1,1) is_partial_differentiable_in z0,1 & pdiff1 (f2,1) is_partial_differentiable_in z0,1 ) by A1, A2, Th9;
then partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,1) = (partdiff ((pdiff1 (f1,1)),z0,1)) + (partdiff ((pdiff1 (f2,1)),z0,1)) by PDIFF_1:29;
then partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) + (partdiff ((pdiff1 (f2,1)),z0,1)) by A1, Th13
.= (hpartdiff11 (f1,z0)) + (hpartdiff11 (f2,z0)) by A2, Th13 ;
hence ( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) + (hpartdiff11 (f2,z0)) ) by A3, PDIFF_1:29; ::_thesis: verum
end;
theorem :: PDIFF_3:22
for z0 being Element of REAL 2
for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 holds
( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) + (hpartdiff12 (f2,z0)) )
proof
let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 holds
( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) + (hpartdiff12 (f2,z0)) )
let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 implies ( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) + (hpartdiff12 (f2,z0)) ) )
assume that
A1: f1 is_hpartial_differentiable`12_in z0 and
A2: f2 is_hpartial_differentiable`12_in z0 ; ::_thesis: ( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) + (hpartdiff12 (f2,z0)) )
A3: ( pdiff1 (f1,1) is_partial_differentiable_in z0,2 & pdiff1 (f2,1) is_partial_differentiable_in z0,2 ) by A1, A2, Th10;
then partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,2) = (partdiff ((pdiff1 (f1,1)),z0,2)) + (partdiff ((pdiff1 (f2,1)),z0,2)) by PDIFF_1:29;
then partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) + (partdiff ((pdiff1 (f2,1)),z0,2)) by A1, Th14
.= (hpartdiff12 (f1,z0)) + (hpartdiff12 (f2,z0)) by A2, Th14 ;
hence ( (pdiff1 (f1,1)) + (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) + (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) + (hpartdiff12 (f2,z0)) ) by A3, PDIFF_1:29; ::_thesis: verum
end;
theorem :: PDIFF_3:23
for z0 being Element of REAL 2
for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 holds
( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) + (hpartdiff21 (f2,z0)) )
proof
let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 holds
( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) + (hpartdiff21 (f2,z0)) )
let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 implies ( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) + (hpartdiff21 (f2,z0)) ) )
assume that
A1: f1 is_hpartial_differentiable`21_in z0 and
A2: f2 is_hpartial_differentiable`21_in z0 ; ::_thesis: ( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) + (hpartdiff21 (f2,z0)) )
A3: ( pdiff1 (f1,2) is_partial_differentiable_in z0,1 & pdiff1 (f2,2) is_partial_differentiable_in z0,1 ) by A1, A2, Th11;
then partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,1) = (partdiff ((pdiff1 (f1,2)),z0,1)) + (partdiff ((pdiff1 (f2,2)),z0,1)) by PDIFF_1:29;
then partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) + (partdiff ((pdiff1 (f2,2)),z0,1)) by A1, Th15
.= (hpartdiff21 (f1,z0)) + (hpartdiff21 (f2,z0)) by A2, Th15 ;
hence ( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) + (hpartdiff21 (f2,z0)) ) by A3, PDIFF_1:29; ::_thesis: verum
end;
theorem :: PDIFF_3:24
for z0 being Element of REAL 2
for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 holds
( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) + (hpartdiff22 (f2,z0)) )
proof
let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 holds
( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) + (hpartdiff22 (f2,z0)) )
let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 implies ( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) + (hpartdiff22 (f2,z0)) ) )
assume that
A1: f1 is_hpartial_differentiable`22_in z0 and
A2: f2 is_hpartial_differentiable`22_in z0 ; ::_thesis: ( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) + (hpartdiff22 (f2,z0)) )
A3: ( pdiff1 (f1,2) is_partial_differentiable_in z0,2 & pdiff1 (f2,2) is_partial_differentiable_in z0,2 ) by A1, A2, Th12;
then partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,2) = (partdiff ((pdiff1 (f1,2)),z0,2)) + (partdiff ((pdiff1 (f2,2)),z0,2)) by PDIFF_1:29;
then partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) + (partdiff ((pdiff1 (f2,2)),z0,2)) by A1, Th16
.= (hpartdiff22 (f1,z0)) + (hpartdiff22 (f2,z0)) by A2, Th16 ;
hence ( (pdiff1 (f1,2)) + (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) + (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) + (hpartdiff22 (f2,z0)) ) by A3, PDIFF_1:29; ::_thesis: verum
end;
theorem :: PDIFF_3:25
for z0 being Element of REAL 2
for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 holds
( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) - (hpartdiff11 (f2,z0)) )
proof
let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 holds
( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) - (hpartdiff11 (f2,z0)) )
let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 implies ( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) - (hpartdiff11 (f2,z0)) ) )
assume that
A1: f1 is_hpartial_differentiable`11_in z0 and
A2: f2 is_hpartial_differentiable`11_in z0 ; ::_thesis: ( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) - (hpartdiff11 (f2,z0)) )
A3: ( pdiff1 (f1,1) is_partial_differentiable_in z0,1 & pdiff1 (f2,1) is_partial_differentiable_in z0,1 ) by A1, A2, Th9;
then partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,1) = (partdiff ((pdiff1 (f1,1)),z0,1)) - (partdiff ((pdiff1 (f2,1)),z0,1)) by PDIFF_1:31;
then partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) - (partdiff ((pdiff1 (f2,1)),z0,1)) by A1, Th13
.= (hpartdiff11 (f1,z0)) - (hpartdiff11 (f2,z0)) by A2, Th13 ;
hence ( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,1) = (hpartdiff11 (f1,z0)) - (hpartdiff11 (f2,z0)) ) by A3, PDIFF_1:31; ::_thesis: verum
end;
theorem :: PDIFF_3:26
for z0 being Element of REAL 2
for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 holds
( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) - (hpartdiff12 (f2,z0)) )
proof
let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 holds
( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) - (hpartdiff12 (f2,z0)) )
let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 implies ( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) - (hpartdiff12 (f2,z0)) ) )
assume that
A1: f1 is_hpartial_differentiable`12_in z0 and
A2: f2 is_hpartial_differentiable`12_in z0 ; ::_thesis: ( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) - (hpartdiff12 (f2,z0)) )
A3: ( pdiff1 (f1,1) is_partial_differentiable_in z0,2 & pdiff1 (f2,1) is_partial_differentiable_in z0,2 ) by A1, A2, Th10;
then partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,2) = (partdiff ((pdiff1 (f1,1)),z0,2)) - (partdiff ((pdiff1 (f2,1)),z0,2)) by PDIFF_1:31;
then partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) - (partdiff ((pdiff1 (f2,1)),z0,2)) by A1, Th14
.= (hpartdiff12 (f1,z0)) - (hpartdiff12 (f2,z0)) by A2, Th14 ;
hence ( (pdiff1 (f1,1)) - (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,1)) - (pdiff1 (f2,1))),z0,2) = (hpartdiff12 (f1,z0)) - (hpartdiff12 (f2,z0)) ) by A3, PDIFF_1:31; ::_thesis: verum
end;
theorem :: PDIFF_3:27
for z0 being Element of REAL 2
for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 holds
( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) - (hpartdiff21 (f2,z0)) )
proof
let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 holds
( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) - (hpartdiff21 (f2,z0)) )
let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 implies ( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) - (hpartdiff21 (f2,z0)) ) )
assume that
A1: f1 is_hpartial_differentiable`21_in z0 and
A2: f2 is_hpartial_differentiable`21_in z0 ; ::_thesis: ( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) - (hpartdiff21 (f2,z0)) )
A3: ( pdiff1 (f1,2) is_partial_differentiable_in z0,1 & pdiff1 (f2,2) is_partial_differentiable_in z0,1 ) by A1, A2, Th11;
then partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,1) = (partdiff ((pdiff1 (f1,2)),z0,1)) - (partdiff ((pdiff1 (f2,2)),z0,1)) by PDIFF_1:31;
then partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) - (partdiff ((pdiff1 (f2,2)),z0,1)) by A1, Th15
.= (hpartdiff21 (f1,z0)) - (hpartdiff21 (f2,z0)) by A2, Th15 ;
hence ( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,1) = (hpartdiff21 (f1,z0)) - (hpartdiff21 (f2,z0)) ) by A3, PDIFF_1:31; ::_thesis: verum
end;
theorem :: PDIFF_3:28
for z0 being Element of REAL 2
for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 holds
( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) - (hpartdiff22 (f2,z0)) )
proof
let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 holds
( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) - (hpartdiff22 (f2,z0)) )
let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 implies ( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) - (hpartdiff22 (f2,z0)) ) )
assume that
A1: f1 is_hpartial_differentiable`22_in z0 and
A2: f2 is_hpartial_differentiable`22_in z0 ; ::_thesis: ( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) - (hpartdiff22 (f2,z0)) )
A3: ( pdiff1 (f1,2) is_partial_differentiable_in z0,2 & pdiff1 (f2,2) is_partial_differentiable_in z0,2 ) by A1, A2, Th12;
then partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,2) = (partdiff ((pdiff1 (f1,2)),z0,2)) - (partdiff ((pdiff1 (f2,2)),z0,2)) by PDIFF_1:31;
then partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) - (partdiff ((pdiff1 (f2,2)),z0,2)) by A1, Th16
.= (hpartdiff22 (f1,z0)) - (hpartdiff22 (f2,z0)) by A2, Th16 ;
hence ( (pdiff1 (f1,2)) - (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 & partdiff (((pdiff1 (f1,2)) - (pdiff1 (f2,2))),z0,2) = (hpartdiff22 (f1,z0)) - (hpartdiff22 (f2,z0)) ) by A3, PDIFF_1:31; ::_thesis: verum
end;
theorem :: PDIFF_3:29
for r being Real
for z0 being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`11_in z0 holds
( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,1))),z0,1) = r * (hpartdiff11 (f,z0)) )
proof
let r be Real; ::_thesis: for z0 being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`11_in z0 holds
( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,1))),z0,1) = r * (hpartdiff11 (f,z0)) )
let z0 be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`11_in z0 holds
( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,1))),z0,1) = r * (hpartdiff11 (f,z0)) )
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`11_in z0 implies ( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,1))),z0,1) = r * (hpartdiff11 (f,z0)) ) )
assume A1: f is_hpartial_differentiable`11_in z0 ; ::_thesis: ( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,1))),z0,1) = r * (hpartdiff11 (f,z0)) )
then A2: pdiff1 (f,1) is_partial_differentiable_in z0,1 by Th9;
then partdiff ((r (#) (pdiff1 (f,1))),z0,1) = r * (partdiff ((pdiff1 (f,1)),z0,1)) by PDIFF_1:33;
hence ( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,1))),z0,1) = r * (hpartdiff11 (f,z0)) ) by A1, A2, Th13, PDIFF_1:33; ::_thesis: verum
end;
theorem :: PDIFF_3:30
for r being Real
for z0 being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`12_in z0 holds
( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,1))),z0,2) = r * (hpartdiff12 (f,z0)) )
proof
let r be Real; ::_thesis: for z0 being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`12_in z0 holds
( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,1))),z0,2) = r * (hpartdiff12 (f,z0)) )
let z0 be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`12_in z0 holds
( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,1))),z0,2) = r * (hpartdiff12 (f,z0)) )
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`12_in z0 implies ( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,1))),z0,2) = r * (hpartdiff12 (f,z0)) ) )
assume A1: f is_hpartial_differentiable`12_in z0 ; ::_thesis: ( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,1))),z0,2) = r * (hpartdiff12 (f,z0)) )
then A2: pdiff1 (f,1) is_partial_differentiable_in z0,2 by Th10;
then partdiff ((r (#) (pdiff1 (f,1))),z0,2) = r * (partdiff ((pdiff1 (f,1)),z0,2)) by PDIFF_1:33;
hence ( r (#) (pdiff1 (f,1)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,1))),z0,2) = r * (hpartdiff12 (f,z0)) ) by A1, A2, Th14, PDIFF_1:33; ::_thesis: verum
end;
theorem :: PDIFF_3:31
for r being Real
for z0 being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`21_in z0 holds
( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,2))),z0,1) = r * (hpartdiff21 (f,z0)) )
proof
let r be Real; ::_thesis: for z0 being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`21_in z0 holds
( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,2))),z0,1) = r * (hpartdiff21 (f,z0)) )
let z0 be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`21_in z0 holds
( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,2))),z0,1) = r * (hpartdiff21 (f,z0)) )
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`21_in z0 implies ( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,2))),z0,1) = r * (hpartdiff21 (f,z0)) ) )
assume A1: f is_hpartial_differentiable`21_in z0 ; ::_thesis: ( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,2))),z0,1) = r * (hpartdiff21 (f,z0)) )
then A2: pdiff1 (f,2) is_partial_differentiable_in z0,1 by Th11;
then partdiff ((r (#) (pdiff1 (f,2))),z0,1) = r * (partdiff ((pdiff1 (f,2)),z0,1)) by PDIFF_1:33;
hence ( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,1 & partdiff ((r (#) (pdiff1 (f,2))),z0,1) = r * (hpartdiff21 (f,z0)) ) by A1, A2, Th15, PDIFF_1:33; ::_thesis: verum
end;
theorem :: PDIFF_3:32
for r being Real
for z0 being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`22_in z0 holds
( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,2))),z0,2) = r * (hpartdiff22 (f,z0)) )
proof
let r be Real; ::_thesis: for z0 being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`22_in z0 holds
( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,2))),z0,2) = r * (hpartdiff22 (f,z0)) )
let z0 be Element of REAL 2; ::_thesis: for f being PartFunc of (REAL 2),REAL st f is_hpartial_differentiable`22_in z0 holds
( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,2))),z0,2) = r * (hpartdiff22 (f,z0)) )
let f be PartFunc of (REAL 2),REAL; ::_thesis: ( f is_hpartial_differentiable`22_in z0 implies ( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,2))),z0,2) = r * (hpartdiff22 (f,z0)) ) )
assume A1: f is_hpartial_differentiable`22_in z0 ; ::_thesis: ( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,2))),z0,2) = r * (hpartdiff22 (f,z0)) )
then A2: pdiff1 (f,2) is_partial_differentiable_in z0,2 by Th12;
then partdiff ((r (#) (pdiff1 (f,2))),z0,2) = r * (partdiff ((pdiff1 (f,2)),z0,2)) by PDIFF_1:33;
hence ( r (#) (pdiff1 (f,2)) is_partial_differentiable_in z0,2 & partdiff ((r (#) (pdiff1 (f,2))),z0,2) = r * (hpartdiff22 (f,z0)) ) by A1, A2, Th16, PDIFF_1:33; ::_thesis: verum
end;
theorem :: PDIFF_3:33
for z0 being Element of REAL 2
for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 holds
(pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,1
proof
let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 holds
(pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,1
let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 implies (pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 )
assume ( f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 ) ; ::_thesis: (pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,1
then ( pdiff1 (f1,1) is_partial_differentiable_in z0,1 & pdiff1 (f2,1) is_partial_differentiable_in z0,1 ) by Th9;
hence (pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,1 by PDIFF_2:19; ::_thesis: verum
end;
theorem :: PDIFF_3:34
for z0 being Element of REAL 2
for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 holds
(pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,2
proof
let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 holds
(pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,2
let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 implies (pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 )
assume ( f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 ) ; ::_thesis: (pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,2
then ( pdiff1 (f1,1) is_partial_differentiable_in z0,2 & pdiff1 (f2,1) is_partial_differentiable_in z0,2 ) by Th10;
hence (pdiff1 (f1,1)) (#) (pdiff1 (f2,1)) is_partial_differentiable_in z0,2 by PDIFF_2:20; ::_thesis: verum
end;
theorem :: PDIFF_3:35
for z0 being Element of REAL 2
for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 holds
(pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,1
proof
let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 holds
(pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,1
let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 implies (pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 )
assume ( f1 is_hpartial_differentiable`21_in z0 & f2 is_hpartial_differentiable`21_in z0 ) ; ::_thesis: (pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,1
then ( pdiff1 (f1,2) is_partial_differentiable_in z0,1 & pdiff1 (f2,2) is_partial_differentiable_in z0,1 ) by Th11;
hence (pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,1 by PDIFF_2:19; ::_thesis: verum
end;
theorem :: PDIFF_3:36
for z0 being Element of REAL 2
for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 holds
(pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,2
proof
let z0 be Element of REAL 2; ::_thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 holds
(pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,2
let f1, f2 be PartFunc of (REAL 2),REAL; ::_thesis: ( f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 implies (pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 )
assume ( f1 is_hpartial_differentiable`22_in z0 & f2 is_hpartial_differentiable`22_in z0 ) ; ::_thesis: (pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,2
then ( pdiff1 (f1,2) is_partial_differentiable_in z0,2 & pdiff1 (f2,2) is_partial_differentiable_in z0,2 ) by Th12;
hence (pdiff1 (f1,2)) (#) (pdiff1 (f2,2)) is_partial_differentiable_in z0,2 by PDIFF_2:20; ::_thesis: verum
end;
theorem :: PDIFF_3:37
for f being PartFunc of (REAL 2),REAL
for z0 being Element of REAL 2 st f is_hpartial_differentiable`11_in z0 holds
SVF1 (1,(pdiff1 (f,1)),z0) is_continuous_in (proj (1,2)) . z0
proof
let f be PartFunc of (REAL 2),REAL; ::_thesis: for z0 being Element of REAL 2 st f is_hpartial_differentiable`11_in z0 holds
SVF1 (1,(pdiff1 (f,1)),z0) is_continuous_in (proj (1,2)) . z0
let z0 be Element of REAL 2; ::_thesis: ( f is_hpartial_differentiable`11_in z0 implies SVF1 (1,(pdiff1 (f,1)),z0) is_continuous_in (proj (1,2)) . z0 )
assume f is_hpartial_differentiable`11_in z0 ; ::_thesis: SVF1 (1,(pdiff1 (f,1)),z0) is_continuous_in (proj (1,2)) . z0
then pdiff1 (f,1) is_partial_differentiable_in z0,1 by Th9;
hence SVF1 (1,(pdiff1 (f,1)),z0) is_continuous_in (proj (1,2)) . z0 by PDIFF_2:21; ::_thesis: verum
end;
theorem :: PDIFF_3:38
for f being PartFunc of (REAL 2),REAL
for z0 being Element of REAL 2 st f is_hpartial_differentiable`12_in z0 holds
SVF1 (2,(pdiff1 (f,1)),z0) is_continuous_in (proj (2,2)) . z0
proof
let f be PartFunc of (REAL 2),REAL; ::_thesis: for z0 being Element of REAL 2 st f is_hpartial_differentiable`12_in z0 holds
SVF1 (2,(pdiff1 (f,1)),z0) is_continuous_in (proj (2,2)) . z0
let z0 be Element of REAL 2; ::_thesis: ( f is_hpartial_differentiable`12_in z0 implies SVF1 (2,(pdiff1 (f,1)),z0) is_continuous_in (proj (2,2)) . z0 )
assume f is_hpartial_differentiable`12_in z0 ; ::_thesis: SVF1 (2,(pdiff1 (f,1)),z0) is_continuous_in (proj (2,2)) . z0
then pdiff1 (f,1) is_partial_differentiable_in z0,2 by Th10;
hence SVF1 (2,(pdiff1 (f,1)),z0) is_continuous_in (proj (2,2)) . z0 by PDIFF_2:22; ::_thesis: verum
end;
theorem :: PDIFF_3:39
for f being PartFunc of (REAL 2),REAL
for z0 being Element of REAL 2 st f is_hpartial_differentiable`21_in z0 holds
SVF1 (1,(pdiff1 (f,2)),z0) is_continuous_in (proj (1,2)) . z0
proof
let f be PartFunc of (REAL 2),REAL; ::_thesis: for z0 being Element of REAL 2 st f is_hpartial_differentiable`21_in z0 holds
SVF1 (1,(pdiff1 (f,2)),z0) is_continuous_in (proj (1,2)) . z0
let z0 be Element of REAL 2; ::_thesis: ( f is_hpartial_differentiable`21_in z0 implies SVF1 (1,(pdiff1 (f,2)),z0) is_continuous_in (proj (1,2)) . z0 )
assume f is_hpartial_differentiable`21_in z0 ; ::_thesis: SVF1 (1,(pdiff1 (f,2)),z0) is_continuous_in (proj (1,2)) . z0
then pdiff1 (f,2) is_partial_differentiable_in z0,1 by Th11;
hence SVF1 (1,(pdiff1 (f,2)),z0) is_continuous_in (proj (1,2)) . z0 by PDIFF_2:21; ::_thesis: verum
end;
theorem :: PDIFF_3:40
for f being PartFunc of (REAL 2),REAL
for z0 being Element of REAL 2 st f is_hpartial_differentiable`22_in z0 holds
SVF1 (2,(pdiff1 (f,2)),z0) is_continuous_in (proj (2,2)) . z0
proof
let f be PartFunc of (REAL 2),REAL; ::_thesis: for z0 being Element of REAL 2 st f is_hpartial_differentiable`22_in z0 holds
SVF1 (2,(pdiff1 (f,2)),z0) is_continuous_in (proj (2,2)) . z0
let z0 be Element of REAL 2; ::_thesis: ( f is_hpartial_differentiable`22_in z0 implies SVF1 (2,(pdiff1 (f,2)),z0) is_continuous_in (proj (2,2)) . z0 )
assume f is_hpartial_differentiable`22_in z0 ; ::_thesis: SVF1 (2,(pdiff1 (f,2)),z0) is_continuous_in (proj (2,2)) . z0
then pdiff1 (f,2) is_partial_differentiable_in z0,2 by Th12;
hence SVF1 (2,(pdiff1 (f,2)),z0) is_continuous_in (proj (2,2)) . z0 by PDIFF_2:22; ::_thesis: verum
end;