:: NDIFF_1 semantic presentation
begin
theorem Th1: :: NDIFF_1:1
for S being RealNormSpace
for x0 being Point of S
for N1, N2 being Neighbourhood of x0 ex N being Neighbourhood of x0 st
( N c= N1 & N c= N2 )
proof
let S be RealNormSpace; ::_thesis: for x0 being Point of S
for N1, N2 being Neighbourhood of x0 ex N being Neighbourhood of x0 st
( N c= N1 & N c= N2 )
let x0 be Point of S; ::_thesis: for N1, N2 being Neighbourhood of x0 ex N being Neighbourhood of x0 st
( N c= N1 & N c= N2 )
let N1, N2 be Neighbourhood of x0; ::_thesis: ex N being Neighbourhood of x0 st
( N c= N1 & N c= N2 )
consider g1 being Real such that
A1: 0 < g1 and
A2: { y where y is Point of S : ||.(y - x0).|| < g1 } c= N1 by NFCONT_1:def_1;
consider g2 being Real such that
A3: 0 < g2 and
A4: { y where y is Point of S : ||.(y - x0).|| < g2 } c= N2 by NFCONT_1:def_1;
set g = min (g1,g2);
take { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } ; ::_thesis: ( { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } is Element of K6( the carrier of S) & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } is Neighbourhood of x0 & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } c= N1 & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } c= N2 )
A5: min (g1,g2) <= g2 by XXREAL_0:17;
A6: { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } c= { y where y is Point of S : ||.(y - x0).|| < g2 }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } or z in { y where y is Point of S : ||.(y - x0).|| < g2 } )
assume z in { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } ; ::_thesis: z in { y where y is Point of S : ||.(y - x0).|| < g2 }
then consider y being Point of S such that
A7: z = y and
A8: ||.(y - x0).|| < min (g1,g2) ;
||.(y - x0).|| < g2 by A5, A8, XXREAL_0:2;
hence z in { y where y is Point of S : ||.(y - x0).|| < g2 } by A7; ::_thesis: verum
end;
A9: min (g1,g2) <= g1 by XXREAL_0:17;
A10: { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } c= { y where y is Point of S : ||.(y - x0).|| < g1 }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } or z in { y where y is Point of S : ||.(y - x0).|| < g1 } )
assume z in { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } ; ::_thesis: z in { y where y is Point of S : ||.(y - x0).|| < g1 }
then consider y being Point of S such that
A11: z = y and
A12: ||.(y - x0).|| < min (g1,g2) ;
||.(y - x0).|| < g1 by A9, A12, XXREAL_0:2;
hence z in { y where y is Point of S : ||.(y - x0).|| < g1 } by A11; ::_thesis: verum
end;
0 < min (g1,g2) by A1, A3, XXREAL_0:15;
hence ( { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } is Element of K6( the carrier of S) & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } is Neighbourhood of x0 & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } c= N1 & { y where y is Point of S : ||.(y - x0).|| < min (g1,g2) } c= N2 ) by A2, A4, A10, A6, NFCONT_1:3, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th2: :: NDIFF_1:2
for S being RealNormSpace
for X being Subset of S st X is open holds
for r being Point of S st r in X holds
ex N being Neighbourhood of r st N c= X
proof
let S be RealNormSpace; ::_thesis: for X being Subset of S st X is open holds
for r being Point of S st r in X holds
ex N being Neighbourhood of r st N c= X
let X be Subset of S; ::_thesis: ( X is open implies for r being Point of S st r in X holds
ex N being Neighbourhood of r st N c= X )
assume X is open ; ::_thesis: for r being Point of S st r in X holds
ex N being Neighbourhood of r st N c= X
then A1: X ` is closed by NFCONT_1:def_4;
let r be Point of S; ::_thesis: ( r in X implies ex N being Neighbourhood of r st N c= X )
assume that
A2: r in X and
A3: for N being Neighbourhood of r holds not N c= X ; ::_thesis: contradiction
defpred S1[ Element of NAT , Point of S] means ( $2 in { y where y is Point of S : ||.(y - r).|| < 1 / ($1 + 1) } & $2 in X ` );
A4: now__::_thesis:_for_g_being_Real_st_0_<_g_holds_
ex_s_being_Point_of_S_st_
(_s_in__{__y_where_y_is_Point_of_S_:_||.(y_-_r).||_<_g__}__&_s_in_X_`_)
let g be Real; ::_thesis: ( 0 < g implies ex s being Point of S st
( s in { y where y is Point of S : ||.(y - r).|| < g } & s in X ` ) )
assume A5: 0 < g ; ::_thesis: ex s being Point of S st
( s in { y where y is Point of S : ||.(y - r).|| < g } & s in X ` )
set N = { y where y is Point of S : ||.(y - r).|| < g } ;
{ y where y is Point of S : ||.(y - r).|| < g } is Neighbourhood of r by A5, NFCONT_1:3;
then not { y where y is Point of S : ||.(y - r).|| < g } c= X by A3;
then consider x being set such that
A6: x in { y where y is Point of S : ||.(y - r).|| < g } and
A7: not x in X by TARSKI:def_3;
consider s being Point of S such that
A8: x = s and
A9: ||.(s - r).|| < g by A6;
take s = s; ::_thesis: ( s in { y where y is Point of S : ||.(y - r).|| < g } & s in X ` )
thus s in { y where y is Point of S : ||.(y - r).|| < g } by A9; ::_thesis: s in X `
thus s in X ` by A7, A8, XBOOLE_0:def_5; ::_thesis: verum
end;
A10: for n being Element of NAT ex s being Point of S st S1[n,s]
proof
let n be Element of NAT ; ::_thesis: ex s being Point of S st S1[n,s]
0 <= n by NAT_1:2;
then 0 < 1 * ((n + 1) ") ;
then 0 < 1 / (n + 1) by XCMPLX_0:def_9;
hence ex s being Point of S st S1[n,s] by A4; ::_thesis: verum
end;
consider s1 being sequence of S such that
A11: for n being Element of NAT holds S1[n,s1 . n] from FUNCT_2:sch_3(A10);
A12: rng s1 c= X `
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng s1 or x in X ` )
assume x in rng s1 ; ::_thesis: x in X `
then consider y being set such that
A13: y in dom s1 and
A14: s1 . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A13;
s1 . y in X ` by A11;
hence x in X ` by A14; ::_thesis: verum
end;
A15: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.((s1_._m)_-_r).||_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((s1 . m) - r).|| < p )
assume A16: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((s1 . m) - r).|| < p
consider n being Element of NAT such that
A17: p " < n by SEQ_4:3;
(p ") + 0 < n + 1 by A17, XREAL_1:8;
then 1 / (n + 1) < 1 / (p ") by A16, XREAL_1:76;
then A18: 1 / (n + 1) < p by XCMPLX_1:216;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
||.((s1 . m) - r).|| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((s1 . m) - r).|| < p )
assume n <= m ; ::_thesis: ||.((s1 . m) - r).|| < p
then A19: n + 1 <= m + 1 by XREAL_1:6;
s1 . m in { y where y is Point of S : ||.(y - r).|| < 1 / (m + 1) } by A11;
then A20: ex y being Point of S st
( s1 . m = y & ||.(y - r).|| < 1 / (m + 1) ) ;
0 <= n by NAT_1:2;
then 1 / (m + 1) <= 1 / (n + 1) by A19, XREAL_1:118;
then ||.((s1 . m) - r).|| < 1 / (n + 1) by A20, XXREAL_0:2;
hence ||.((s1 . m) - r).|| < p by A18, XXREAL_0:2; ::_thesis: verum
end;
then A21: s1 is convergent by NORMSP_1:def_6;
then lim s1 = r by A15, NORMSP_1:def_7;
then r in X ` by A21, A12, A1, NFCONT_1:def_3;
hence contradiction by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem :: NDIFF_1:3
for S being RealNormSpace
for X being Subset of S st X is open holds
for r being Point of S st r in X holds
ex g being Real st
( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X )
proof
let S be RealNormSpace; ::_thesis: for X being Subset of S st X is open holds
for r being Point of S st r in X holds
ex g being Real st
( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X )
let X be Subset of S; ::_thesis: ( X is open implies for r being Point of S st r in X holds
ex g being Real st
( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X ) )
assume A1: X is open ; ::_thesis: for r being Point of S st r in X holds
ex g being Real st
( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X )
let r be Point of S; ::_thesis: ( r in X implies ex g being Real st
( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X ) )
assume r in X ; ::_thesis: ex g being Real st
( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X )
then consider N being Neighbourhood of r such that
A2: N c= X by A1, Th2;
consider g being Real such that
A3: ( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= N ) by NFCONT_1:def_1;
take g ; ::_thesis: ( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X )
thus ( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X ) by A2, A3, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th4: :: NDIFF_1:4
for S being RealNormSpace
for X being Subset of S st ( for r being Point of S st r in X holds
ex N being Neighbourhood of r st N c= X ) holds
X is open
proof
let S be RealNormSpace; ::_thesis: for X being Subset of S st ( for r being Point of S st r in X holds
ex N being Neighbourhood of r st N c= X ) holds
X is open
let X be Subset of S; ::_thesis: ( ( for r being Point of S st r in X holds
ex N being Neighbourhood of r st N c= X ) implies X is open )
assume that
A1: for r being Point of S st r in X holds
ex N being Neighbourhood of r st N c= X and
A2: not X is open ; ::_thesis: contradiction
not X ` is closed by A2, NFCONT_1:def_4;
then consider s1 being sequence of S such that
A3: rng s1 c= X ` and
A4: s1 is convergent and
A5: not lim s1 in X ` by NFCONT_1:def_3;
consider N being Neighbourhood of lim s1 such that
A6: N c= X by A1, A5, SUBSET_1:29;
consider g being Real such that
A7: 0 < g and
A8: { y where y is Point of S : ||.(y - (lim s1)).|| < g } c= N by NFCONT_1:def_1;
consider n being Element of NAT such that
A9: for m being Element of NAT st n <= m holds
||.((s1 . m) - (lim s1)).|| < g by A4, A7, NORMSP_1:def_7;
n in NAT ;
then n in dom s1 by FUNCT_2:def_1;
then A10: s1 . n in rng s1 by FUNCT_1:def_3;
||.((s1 . n) - (lim s1)).|| < g by A9;
then s1 . n in { y where y is Point of S : ||.(y - (lim s1)).|| < g } ;
then s1 . n in N by A8;
hence contradiction by A3, A6, A10, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem :: NDIFF_1:5
for S being RealNormSpace
for X being Subset of S holds
( ( for r being Point of S st r in X holds
ex N being Neighbourhood of r st N c= X ) iff X is open ) by Th2, Th4;
definition
let X be set ;
let S be ZeroStr ;
let f be Function of X,S;
redefine attr f is non-zero means :Def1: :: NDIFF_1:def 1
rng f c= NonZero S;
compatibility
( f is non-zero iff rng f c= NonZero S )
proof
thus ( f is non-zero implies rng f c= NonZero S ) ::_thesis: ( rng f c= NonZero S implies f is non-zero )
proof
assume f is non-zero ; ::_thesis: rng f c= NonZero S
then not 0. S in rng f by STRUCT_0:def_15;
hence rng f c= NonZero S by ZFMISC_1:34; ::_thesis: verum
end;
assume A1: rng f c= NonZero S ; ::_thesis: f is non-zero
assume 0. S in rng f ; :: according to STRUCT_0:def_15 ::_thesis: contradiction
then not 0. S in {(0. S)} by A1, XBOOLE_0:def_5;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines non-zero NDIFF_1:def_1_:_
for X being set
for S being ZeroStr
for f being Function of X,S holds
( f is non-zero iff rng f c= NonZero S );
theorem Th6: :: NDIFF_1:6
for S being RealNormSpace
for seq being sequence of S holds
( seq is non-zero iff for x being set st x in NAT holds
seq . x <> 0. S )
proof
let S be RealNormSpace; ::_thesis: for seq being sequence of S holds
( seq is non-zero iff for x being set st x in NAT holds
seq . x <> 0. S )
let seq be sequence of S; ::_thesis: ( seq is non-zero iff for x being set st x in NAT holds
seq . x <> 0. S )
thus ( seq is non-zero implies for x being set st x in NAT holds
seq . x <> 0. S ) ::_thesis: ( ( for x being set st x in NAT holds
seq . x <> 0. S ) implies seq is non-zero )
proof
assume seq is non-zero ; ::_thesis: for x being set st x in NAT holds
seq . x <> 0. S
then A1: rng seq c= NonZero S by Def1;
let x be set ; ::_thesis: ( x in NAT implies seq . x <> 0. S )
assume x in NAT ; ::_thesis: seq . x <> 0. S
then x in dom seq by FUNCT_2:def_1;
then seq . x in rng seq by FUNCT_1:def_3;
then not seq . x in {(0. S)} by A1, XBOOLE_0:def_5;
hence seq . x <> 0. S by TARSKI:def_1; ::_thesis: verum
end;
assume A2: for x being set st x in NAT holds
seq . x <> 0. S ; ::_thesis: seq is non-zero
now__::_thesis:_for_y_being_set_st_y_in_rng_seq_holds_
y_in_NonZero_S
let y be set ; ::_thesis: ( y in rng seq implies y in NonZero S )
assume A3: y in rng seq ; ::_thesis: y in NonZero S
then ex x being set st
( x in dom seq & seq . x = y ) by FUNCT_1:def_3;
then y <> 0. S by A2;
then not y in {(0. S)} by TARSKI:def_1;
hence y in NonZero S by A3, XBOOLE_0:def_5; ::_thesis: verum
end;
then rng seq c= NonZero S by TARSKI:def_3;
hence seq is non-zero by Def1; ::_thesis: verum
end;
theorem Th7: :: NDIFF_1:7
for S being RealNormSpace
for seq being sequence of S holds
( seq is non-zero iff for n being Element of NAT holds seq . n <> 0. S )
proof
let S be RealNormSpace; ::_thesis: for seq being sequence of S holds
( seq is non-zero iff for n being Element of NAT holds seq . n <> 0. S )
let seq be sequence of S; ::_thesis: ( seq is non-zero iff for n being Element of NAT holds seq . n <> 0. S )
thus ( seq is non-zero implies for n being Element of NAT holds seq . n <> 0. S ) by Th6; ::_thesis: ( ( for n being Element of NAT holds seq . n <> 0. S ) implies seq is non-zero )
assume for n being Element of NAT holds seq . n <> 0. S ; ::_thesis: seq is non-zero
then for x being set st x in NAT holds
seq . x <> 0. S ;
hence seq is non-zero by Th6; ::_thesis: verum
end;
definition
let RNS be RealLinearSpace;
let S be sequence of RNS;
let a be Real_Sequence;
funca (#) S -> sequence of RNS means :Def2: :: NDIFF_1:def 2
for n being Element of NAT holds it . n = (a . n) * (S . n);
existence
ex b1 being sequence of RNS st
for n being Element of NAT holds b1 . n = (a . n) * (S . n)
proof
deffunc H1( Element of NAT ) -> Element of the carrier of RNS = (a . $1) * (S . $1);
thus ex S being sequence of RNS st
for n being Element of NAT holds S . n = H1(n) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
for b1, b2 being sequence of RNS st ( for n being Element of NAT holds b1 . n = (a . n) * (S . n) ) & ( for n being Element of NAT holds b2 . n = (a . n) * (S . n) ) holds
b1 = b2
proof
let S1, S2 be sequence of RNS; ::_thesis: ( ( for n being Element of NAT holds S1 . n = (a . n) * (S . n) ) & ( for n being Element of NAT holds S2 . n = (a . n) * (S . n) ) implies S1 = S2 )
assume that
A1: for n being Element of NAT holds S1 . n = (a . n) * (S . n) and
A2: for n being Element of NAT holds S2 . n = (a . n) * (S . n) ; ::_thesis: S1 = S2
for n being Element of NAT holds S1 . n = S2 . n
proof
let n be Element of NAT ; ::_thesis: S1 . n = S2 . n
S1 . n = (a . n) * (S . n) by A1;
hence S1 . n = S2 . n by A2; ::_thesis: verum
end;
hence S1 = S2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines (#) NDIFF_1:def_2_:_
for RNS being RealLinearSpace
for S being sequence of RNS
for a being Real_Sequence
for b4 being sequence of RNS holds
( b4 = a (#) S iff for n being Element of NAT holds b4 . n = (a . n) * (S . n) );
definition
let RNS be RealLinearSpace;
let z be Point of RNS;
let a be Real_Sequence;
funca * z -> sequence of RNS means :Def3: :: NDIFF_1:def 3
for n being Element of NAT holds it . n = (a . n) * z;
existence
ex b1 being sequence of RNS st
for n being Element of NAT holds b1 . n = (a . n) * z
proof
deffunc H1( Element of NAT ) -> Element of the carrier of RNS = (a . $1) * z;
thus ex S being sequence of RNS st
for n being Element of NAT holds S . n = H1(n) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
for b1, b2 being sequence of RNS st ( for n being Element of NAT holds b1 . n = (a . n) * z ) & ( for n being Element of NAT holds b2 . n = (a . n) * z ) holds
b1 = b2
proof
let S1, S2 be sequence of RNS; ::_thesis: ( ( for n being Element of NAT holds S1 . n = (a . n) * z ) & ( for n being Element of NAT holds S2 . n = (a . n) * z ) implies S1 = S2 )
assume that
A1: for n being Element of NAT holds S1 . n = (a . n) * z and
A2: for n being Element of NAT holds S2 . n = (a . n) * z ; ::_thesis: S1 = S2
for n being Element of NAT holds S1 . n = S2 . n
proof
let n be Element of NAT ; ::_thesis: S1 . n = S2 . n
S1 . n = (a . n) * z by A1;
hence S1 . n = S2 . n by A2; ::_thesis: verum
end;
hence S1 = S2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines * NDIFF_1:def_3_:_
for RNS being RealLinearSpace
for z being Point of RNS
for a being Real_Sequence
for b4 being sequence of RNS holds
( b4 = a * z iff for n being Element of NAT holds b4 . n = (a . n) * z );
theorem :: NDIFF_1:8
for S being RealNormSpace
for seq being sequence of S
for rseq1, rseq2 being Real_Sequence holds (rseq1 + rseq2) (#) seq = (rseq1 (#) seq) + (rseq2 (#) seq)
proof
let S be RealNormSpace; ::_thesis: for seq being sequence of S
for rseq1, rseq2 being Real_Sequence holds (rseq1 + rseq2) (#) seq = (rseq1 (#) seq) + (rseq2 (#) seq)
let seq be sequence of S; ::_thesis: for rseq1, rseq2 being Real_Sequence holds (rseq1 + rseq2) (#) seq = (rseq1 (#) seq) + (rseq2 (#) seq)
let rseq1, rseq2 be Real_Sequence; ::_thesis: (rseq1 + rseq2) (#) seq = (rseq1 (#) seq) + (rseq2 (#) seq)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((rseq1_+_rseq2)_(#)_seq)_._n_=_((rseq1_(#)_seq)_+_(rseq2_(#)_seq))_._n
let n be Element of NAT ; ::_thesis: ((rseq1 + rseq2) (#) seq) . n = ((rseq1 (#) seq) + (rseq2 (#) seq)) . n
thus ((rseq1 + rseq2) (#) seq) . n = ((rseq1 + rseq2) . n) * (seq . n) by Def2
.= ((rseq1 . n) + (rseq2 . n)) * (seq . n) by SEQ_1:7
.= ((rseq1 . n) * (seq . n)) + ((rseq2 . n) * (seq . n)) by RLVECT_1:def_6
.= ((rseq1 (#) seq) . n) + ((rseq2 . n) * (seq . n)) by Def2
.= ((rseq1 (#) seq) . n) + ((rseq2 (#) seq) . n) by Def2
.= ((rseq1 (#) seq) + (rseq2 (#) seq)) . n by NORMSP_1:def_2 ; ::_thesis: verum
end;
hence (rseq1 + rseq2) (#) seq = (rseq1 (#) seq) + (rseq2 (#) seq) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th9: :: NDIFF_1:9
for S being RealNormSpace
for rseq being Real_Sequence
for seq1, seq2 being sequence of S holds rseq (#) (seq1 + seq2) = (rseq (#) seq1) + (rseq (#) seq2)
proof
let S be RealNormSpace; ::_thesis: for rseq being Real_Sequence
for seq1, seq2 being sequence of S holds rseq (#) (seq1 + seq2) = (rseq (#) seq1) + (rseq (#) seq2)
let rseq be Real_Sequence; ::_thesis: for seq1, seq2 being sequence of S holds rseq (#) (seq1 + seq2) = (rseq (#) seq1) + (rseq (#) seq2)
let seq1, seq2 be sequence of S; ::_thesis: rseq (#) (seq1 + seq2) = (rseq (#) seq1) + (rseq (#) seq2)
now__::_thesis:_for_n_being_Element_of_NAT_holds_(rseq_(#)_(seq1_+_seq2))_._n_=_((rseq_(#)_seq1)_+_(rseq_(#)_seq2))_._n
let n be Element of NAT ; ::_thesis: (rseq (#) (seq1 + seq2)) . n = ((rseq (#) seq1) + (rseq (#) seq2)) . n
thus (rseq (#) (seq1 + seq2)) . n = (rseq . n) * ((seq1 + seq2) . n) by Def2
.= (rseq . n) * ((seq1 . n) + (seq2 . n)) by NORMSP_1:def_2
.= ((rseq . n) * (seq1 . n)) + ((rseq . n) * (seq2 . n)) by RLVECT_1:def_5
.= ((rseq (#) seq1) . n) + ((rseq . n) * (seq2 . n)) by Def2
.= ((rseq (#) seq1) . n) + ((rseq (#) seq2) . n) by Def2
.= ((rseq (#) seq1) + (rseq (#) seq2)) . n by NORMSP_1:def_2 ; ::_thesis: verum
end;
hence rseq (#) (seq1 + seq2) = (rseq (#) seq1) + (rseq (#) seq2) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th10: :: NDIFF_1:10
for r being Real
for S being RealNormSpace
for seq being sequence of S
for rseq being Real_Sequence holds r * (rseq (#) seq) = rseq (#) (r * seq)
proof
let r be Real; ::_thesis: for S being RealNormSpace
for seq being sequence of S
for rseq being Real_Sequence holds r * (rseq (#) seq) = rseq (#) (r * seq)
let S be RealNormSpace; ::_thesis: for seq being sequence of S
for rseq being Real_Sequence holds r * (rseq (#) seq) = rseq (#) (r * seq)
let seq be sequence of S; ::_thesis: for rseq being Real_Sequence holds r * (rseq (#) seq) = rseq (#) (r * seq)
let rseq be Real_Sequence; ::_thesis: r * (rseq (#) seq) = rseq (#) (r * seq)
now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_*_(rseq_(#)_seq))_._n_=_(rseq_(#)_(r_*_seq))_._n
let n be Element of NAT ; ::_thesis: (r * (rseq (#) seq)) . n = (rseq (#) (r * seq)) . n
thus (r * (rseq (#) seq)) . n = r * ((rseq (#) seq) . n) by NORMSP_1:def_5
.= r * ((rseq . n) * (seq . n)) by Def2
.= (r * (rseq . n)) * (seq . n) by RLVECT_1:def_7
.= (rseq . n) * (r * (seq . n)) by RLVECT_1:def_7
.= (rseq . n) * ((r * seq) . n) by NORMSP_1:def_5
.= (rseq (#) (r * seq)) . n by Def2 ; ::_thesis: verum
end;
hence r * (rseq (#) seq) = rseq (#) (r * seq) by FUNCT_2:63; ::_thesis: verum
end;
theorem :: NDIFF_1:11
for S being RealNormSpace
for seq being sequence of S
for rseq1, rseq2 being Real_Sequence holds (rseq1 - rseq2) (#) seq = (rseq1 (#) seq) - (rseq2 (#) seq)
proof
let S be RealNormSpace; ::_thesis: for seq being sequence of S
for rseq1, rseq2 being Real_Sequence holds (rseq1 - rseq2) (#) seq = (rseq1 (#) seq) - (rseq2 (#) seq)
let seq be sequence of S; ::_thesis: for rseq1, rseq2 being Real_Sequence holds (rseq1 - rseq2) (#) seq = (rseq1 (#) seq) - (rseq2 (#) seq)
let rseq1, rseq2 be Real_Sequence; ::_thesis: (rseq1 - rseq2) (#) seq = (rseq1 (#) seq) - (rseq2 (#) seq)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((rseq1_-_rseq2)_(#)_seq)_._n_=_((rseq1_(#)_seq)_-_(rseq2_(#)_seq))_._n
let n be Element of NAT ; ::_thesis: ((rseq1 - rseq2) (#) seq) . n = ((rseq1 (#) seq) - (rseq2 (#) seq)) . n
thus ((rseq1 - rseq2) (#) seq) . n = ((rseq1 + (- rseq2)) . n) * (seq . n) by Def2
.= ((rseq1 . n) + ((- rseq2) . n)) * (seq . n) by SEQ_1:7
.= ((rseq1 . n) + (- (rseq2 . n))) * (seq . n) by SEQ_1:10
.= ((rseq1 . n) - (rseq2 . n)) * (seq . n)
.= ((rseq1 . n) * (seq . n)) - ((rseq2 . n) * (seq . n)) by RLVECT_1:35
.= ((rseq1 (#) seq) . n) - ((rseq2 . n) * (seq . n)) by Def2
.= ((rseq1 (#) seq) . n) - ((rseq2 (#) seq) . n) by Def2
.= ((rseq1 (#) seq) - (rseq2 (#) seq)) . n by NORMSP_1:def_3 ; ::_thesis: verum
end;
hence (rseq1 - rseq2) (#) seq = (rseq1 (#) seq) - (rseq2 (#) seq) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th12: :: NDIFF_1:12
for S being RealNormSpace
for rseq being Real_Sequence
for seq1, seq2 being sequence of S holds rseq (#) (seq1 - seq2) = (rseq (#) seq1) - (rseq (#) seq2)
proof
let S be RealNormSpace; ::_thesis: for rseq being Real_Sequence
for seq1, seq2 being sequence of S holds rseq (#) (seq1 - seq2) = (rseq (#) seq1) - (rseq (#) seq2)
let rseq be Real_Sequence; ::_thesis: for seq1, seq2 being sequence of S holds rseq (#) (seq1 - seq2) = (rseq (#) seq1) - (rseq (#) seq2)
let seq1, seq2 be sequence of S; ::_thesis: rseq (#) (seq1 - seq2) = (rseq (#) seq1) - (rseq (#) seq2)
now__::_thesis:_for_n_being_Element_of_NAT_holds_(rseq_(#)_(seq1_-_seq2))_._n_=_((rseq_(#)_seq1)_-_(rseq_(#)_seq2))_._n
let n be Element of NAT ; ::_thesis: (rseq (#) (seq1 - seq2)) . n = ((rseq (#) seq1) - (rseq (#) seq2)) . n
thus (rseq (#) (seq1 - seq2)) . n = (rseq . n) * ((seq1 - seq2) . n) by Def2
.= (rseq . n) * ((seq1 . n) - (seq2 . n)) by NORMSP_1:def_3
.= ((rseq . n) * (seq1 . n)) - ((rseq . n) * (seq2 . n)) by RLVECT_1:34
.= ((rseq (#) seq1) . n) - ((rseq . n) * (seq2 . n)) by Def2
.= ((rseq (#) seq1) . n) - ((rseq (#) seq2) . n) by Def2
.= ((rseq (#) seq1) - (rseq (#) seq2)) . n by NORMSP_1:def_3 ; ::_thesis: verum
end;
hence rseq (#) (seq1 - seq2) = (rseq (#) seq1) - (rseq (#) seq2) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th13: :: NDIFF_1:13
for S being RealNormSpace
for rseq being Real_Sequence
for seq being sequence of S st rseq is convergent & seq is convergent holds
rseq (#) seq is convergent
proof
let S be RealNormSpace; ::_thesis: for rseq being Real_Sequence
for seq being sequence of S st rseq is convergent & seq is convergent holds
rseq (#) seq is convergent
let rseq be Real_Sequence; ::_thesis: for seq being sequence of S st rseq is convergent & seq is convergent holds
rseq (#) seq is convergent
let seq be sequence of S; ::_thesis: ( rseq is convergent & seq is convergent implies rseq (#) seq is convergent )
assume that
A1: rseq is convergent and
A2: seq is convergent ; ::_thesis: rseq (#) seq is convergent
consider g1 being real number such that
A3: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((rseq . m) - g1) < p by A1, SEQ_2:def_6;
consider g2 being Point of S such that
A4: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - g2).|| < p by A2, NORMSP_1:def_6;
reconsider g1 = g1 as Real by XREAL_0:def_1;
take g = g1 * g2; :: according to NORMSP_1:def_6 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= ||.(((rseq (#) seq) . b3) - g).|| ) )
let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= ||.(((rseq (#) seq) . b2) - g).|| ) )
rseq is bounded by A1, SEQ_2:13;
then consider r being real number such that
A5: 0 < r and
A6: for n being Element of NAT holds abs (rseq . n) < r by SEQ_2:3;
reconsider r = r as Real by XREAL_0:def_1;
A7: 0 + 0 < ||.g2.|| + r by A5, NORMSP_1:4, XREAL_1:8;
assume A8: 0 < p ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= ||.(((rseq (#) seq) . b2) - g).|| )
then consider n1 being Element of NAT such that
A9: for m being Element of NAT st n1 <= m holds
abs ((rseq . m) - g1) < p / (||.g2.|| + r) by A3, A7, XREAL_1:139;
consider n2 being Element of NAT such that
A10: for m being Element of NAT st n2 <= m holds
||.((seq . m) - g2).|| < p / (||.g2.|| + r) by A4, A7, A8, XREAL_1:139;
take n = n1 + n2; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or not p <= ||.(((rseq (#) seq) . b1) - g).|| )
let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= ||.(((rseq (#) seq) . m) - g).|| )
assume A11: n <= m ; ::_thesis: not p <= ||.(((rseq (#) seq) . m) - g).||
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A11, XXREAL_0:2;
then A12: abs ((rseq . m) - g1) <= p / (||.g2.|| + r) by A9;
( 0 <= ||.g2.|| & ||.(((rseq . m) - g1) * g2).|| = ||.g2.|| * (abs ((rseq . m) - g1)) ) by NORMSP_1:4, NORMSP_1:def_1;
then A13: ||.(((rseq . m) - g1) * g2).|| <= ||.g2.|| * (p / (||.g2.|| + r)) by A12, XREAL_1:64;
||.(((rseq (#) seq) . m) - g).|| = ||.(((rseq . m) * (seq . m)) - (g1 * g2)).|| by Def2
.= ||.((((rseq . m) * (seq . m)) - (0. S)) - (g1 * g2)).|| by RLVECT_1:13
.= ||.((((rseq . m) * (seq . m)) - (((rseq . m) * g2) - ((rseq . m) * g2))) - (g1 * g2)).|| by RLVECT_1:15
.= ||.(((((rseq . m) * (seq . m)) - ((rseq . m) * g2)) + ((rseq . m) * g2)) - (g1 * g2)).|| by RLVECT_1:29
.= ||.((((rseq . m) * ((seq . m) - g2)) + ((rseq . m) * g2)) - (g1 * g2)).|| by RLVECT_1:34
.= ||.(((rseq . m) * ((seq . m) - g2)) + (((rseq . m) * g2) - (g1 * g2))).|| by RLVECT_1:def_3
.= ||.(((rseq . m) * ((seq . m) - g2)) + (((rseq . m) - g1) * g2)).|| by RLVECT_1:35 ;
then A14: ||.(((rseq (#) seq) . m) - g).|| <= ||.((rseq . m) * ((seq . m) - g2)).|| + ||.(((rseq . m) - g1) * g2).|| by NORMSP_1:def_1;
n2 <= n by NAT_1:12;
then n2 <= m by A11, XXREAL_0:2;
then A15: ||.((seq . m) - g2).|| < p / (||.g2.|| + r) by A10;
A16: ( 0 <= abs (rseq . m) & 0 <= ||.((seq . m) - g2).|| ) by COMPLEX1:46, NORMSP_1:4;
abs (rseq . m) < r by A6;
then (abs (rseq . m)) * ||.((seq . m) - g2).|| < r * (p / (||.g2.|| + r)) by A16, A15, XREAL_1:96;
then A17: ||.((rseq . m) * ((seq . m) - g2)).|| < r * (p / (||.g2.|| + r)) by NORMSP_1:def_1;
(r * (p / (||.g2.|| + r))) + (||.g2.|| * (p / (||.g2.|| + r))) = (p / (||.g2.|| + r)) * (||.g2.|| + r)
.= p by A7, XCMPLX_1:87 ;
then ||.((rseq . m) * ((seq . m) - g2)).|| + ||.(((rseq . m) - g1) * g2).|| < p by A17, A13, XREAL_1:8;
hence not p <= ||.(((rseq (#) seq) . m) - g).|| by A14, XXREAL_0:2; ::_thesis: verum
end;
theorem Th14: :: NDIFF_1:14
for S being RealNormSpace
for rseq being Real_Sequence
for seq being sequence of S st rseq is convergent & seq is convergent holds
lim (rseq (#) seq) = (lim rseq) * (lim seq)
proof
let S be RealNormSpace; ::_thesis: for rseq being Real_Sequence
for seq being sequence of S st rseq is convergent & seq is convergent holds
lim (rseq (#) seq) = (lim rseq) * (lim seq)
let rseq be Real_Sequence; ::_thesis: for seq being sequence of S st rseq is convergent & seq is convergent holds
lim (rseq (#) seq) = (lim rseq) * (lim seq)
let seq be sequence of S; ::_thesis: ( rseq is convergent & seq is convergent implies lim (rseq (#) seq) = (lim rseq) * (lim seq) )
assume that
A1: rseq is convergent and
A2: seq is convergent ; ::_thesis: lim (rseq (#) seq) = (lim rseq) * (lim seq)
set g2 = lim seq;
reconsider g1 = lim rseq as Real ;
set g = g1 * (lim seq);
rseq is bounded by A1, SEQ_2:13;
then consider r being real number such that
A3: 0 < r and
A4: for n being Element of NAT holds abs (rseq . n) < r by SEQ_2:3;
reconsider r = r as Real by XREAL_0:def_1;
A5: 0 + 0 < ||.(lim seq).|| + r by A3, NORMSP_1:4, XREAL_1:8;
A6: 0 <= ||.(lim seq).|| by NORMSP_1:4;
A7: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p
proof
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p )
assume 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p
then A8: 0 < p / (||.(lim seq).|| + r) by A5, XREAL_1:139;
then consider n1 being Element of NAT such that
A9: for m being Element of NAT st n1 <= m holds
abs ((rseq . m) - g1) < p / (||.(lim seq).|| + r) by A1, SEQ_2:def_7;
consider n2 being Element of NAT such that
A10: for m being Element of NAT st n2 <= m holds
||.((seq . m) - (lim seq)).|| < p / (||.(lim seq).|| + r) by A2, A8, NORMSP_1:def_7;
take n = n1 + n2; ::_thesis: for m being Element of NAT st n <= m holds
||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p )
assume A11: n <= m ; ::_thesis: ||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A11, XXREAL_0:2;
then A12: abs ((rseq . m) - g1) <= p / (||.(lim seq).|| + r) by A9;
||.(((rseq . m) - g1) * (lim seq)).|| = ||.(lim seq).|| * (abs ((rseq . m) - g1)) by NORMSP_1:def_1;
then A13: ||.(((rseq . m) - g1) * (lim seq)).|| <= ||.(lim seq).|| * (p / (||.(lim seq).|| + r)) by A6, A12, XREAL_1:64;
A14: ( 0 <= abs (rseq . m) & 0 <= ||.((seq . m) - (lim seq)).|| ) by COMPLEX1:46, NORMSP_1:4;
n2 <= n by NAT_1:12;
then n2 <= m by A11, XXREAL_0:2;
then A15: ||.((seq . m) - (lim seq)).|| < p / (||.(lim seq).|| + r) by A10;
||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| = ||.(((rseq . m) * (seq . m)) - (g1 * (lim seq))).|| by Def2
.= ||.((((rseq . m) * (seq . m)) - (0. S)) - (g1 * (lim seq))).|| by RLVECT_1:13
.= ||.((((rseq . m) * (seq . m)) - (((rseq . m) * (lim seq)) - ((rseq . m) * (lim seq)))) - (g1 * (lim seq))).|| by RLVECT_1:15
.= ||.(((((rseq . m) * (seq . m)) - ((rseq . m) * (lim seq))) + ((rseq . m) * (lim seq))) - (g1 * (lim seq))).|| by RLVECT_1:29
.= ||.((((rseq . m) * ((seq . m) - (lim seq))) + ((rseq . m) * (lim seq))) - (g1 * (lim seq))).|| by RLVECT_1:34
.= ||.(((rseq . m) * ((seq . m) - (lim seq))) + (((rseq . m) * (lim seq)) - (g1 * (lim seq)))).|| by RLVECT_1:def_3
.= ||.(((rseq . m) * ((seq . m) - (lim seq))) + (((rseq . m) - g1) * (lim seq))).|| by RLVECT_1:35 ;
then A16: ||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| <= ||.((rseq . m) * ((seq . m) - (lim seq))).|| + ||.(((rseq . m) - g1) * (lim seq)).|| by NORMSP_1:def_1;
abs (rseq . m) < r by A4;
then (abs (rseq . m)) * ||.((seq . m) - (lim seq)).|| < r * (p / (||.(lim seq).|| + r)) by A14, A15, XREAL_1:96;
then A17: ||.((rseq . m) * ((seq . m) - (lim seq))).|| < r * (p / (||.(lim seq).|| + r)) by NORMSP_1:def_1;
(r * (p / (||.(lim seq).|| + r))) + (||.(lim seq).|| * (p / (||.(lim seq).|| + r))) = (p / (||.(lim seq).|| + r)) * (||.(lim seq).|| + r)
.= p by A5, XCMPLX_1:87 ;
then ||.((rseq . m) * ((seq . m) - (lim seq))).|| + ||.(((rseq . m) - g1) * (lim seq)).|| < p by A17, A13, XREAL_1:8;
hence ||.(((rseq (#) seq) . m) - (g1 * (lim seq))).|| < p by A16, XXREAL_0:2; ::_thesis: verum
end;
rseq (#) seq is convergent by A1, A2, Th13;
hence lim (rseq (#) seq) = (lim rseq) * (lim seq) by A7, NORMSP_1:def_7; ::_thesis: verum
end;
theorem Th15: :: NDIFF_1:15
for k being Element of NAT
for S being RealNormSpace
for seq, seq1 being sequence of S holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)
proof
let k be Element of NAT ; ::_thesis: for S being RealNormSpace
for seq, seq1 being sequence of S holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)
let S be RealNormSpace; ::_thesis: for seq, seq1 being sequence of S holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)
let seq, seq1 be sequence of S; ::_thesis: (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_+_seq1)_^\_k)_._n_=_((seq_^\_k)_+_(seq1_^\_k))_._n
let n be Element of NAT ; ::_thesis: ((seq + seq1) ^\ k) . n = ((seq ^\ k) + (seq1 ^\ k)) . n
thus ((seq + seq1) ^\ k) . n = (seq + seq1) . (n + k) by NAT_1:def_3
.= (seq . (n + k)) + (seq1 . (n + k)) by NORMSP_1:def_2
.= ((seq ^\ k) . n) + (seq1 . (n + k)) by NAT_1:def_3
.= ((seq ^\ k) . n) + ((seq1 ^\ k) . n) by NAT_1:def_3
.= ((seq ^\ k) + (seq1 ^\ k)) . n by NORMSP_1:def_2 ; ::_thesis: verum
end;
hence (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th16: :: NDIFF_1:16
for k being Element of NAT
for S being RealNormSpace
for seq, seq1 being sequence of S holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)
proof
let k be Element of NAT ; ::_thesis: for S being RealNormSpace
for seq, seq1 being sequence of S holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)
let S be RealNormSpace; ::_thesis: for seq, seq1 being sequence of S holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)
let seq, seq1 be sequence of S; ::_thesis: (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_-_seq1)_^\_k)_._n_=_((seq_^\_k)_-_(seq1_^\_k))_._n
let n be Element of NAT ; ::_thesis: ((seq - seq1) ^\ k) . n = ((seq ^\ k) - (seq1 ^\ k)) . n
thus ((seq - seq1) ^\ k) . n = (seq - seq1) . (n + k) by NAT_1:def_3
.= (seq . (n + k)) - (seq1 . (n + k)) by NORMSP_1:def_3
.= ((seq ^\ k) . n) - (seq1 . (n + k)) by NAT_1:def_3
.= ((seq ^\ k) . n) - ((seq1 ^\ k) . n) by NAT_1:def_3
.= ((seq ^\ k) - (seq1 ^\ k)) . n by NORMSP_1:def_3 ; ::_thesis: verum
end;
hence (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th17: :: NDIFF_1:17
for k being Element of NAT
for S being RealNormSpace
for seq being sequence of S st seq is non-zero holds
seq ^\ k is non-zero
proof
let k be Element of NAT ; ::_thesis: for S being RealNormSpace
for seq being sequence of S st seq is non-zero holds
seq ^\ k is non-zero
let S be RealNormSpace; ::_thesis: for seq being sequence of S st seq is non-zero holds
seq ^\ k is non-zero
let seq be sequence of S; ::_thesis: ( seq is non-zero implies seq ^\ k is non-zero )
assume A1: seq is non-zero ; ::_thesis: seq ^\ k is non-zero
now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq_^\_k)_._n_<>_0._S
let n be Element of NAT ; ::_thesis: (seq ^\ k) . n <> 0. S
(seq ^\ k) . n = seq . (n + k) by NAT_1:def_3;
hence (seq ^\ k) . n <> 0. S by A1, Th7; ::_thesis: verum
end;
hence seq ^\ k is non-zero by Th7; ::_thesis: verum
end;
definition
let S be RealNormSpace;
let x be Point of S;
let IT be sequence of S;
attrIT is x -convergent means :Def4: :: NDIFF_1:def 4
( IT is convergent & lim IT = x );
end;
:: deftheorem Def4 defines -convergent NDIFF_1:def_4_:_
for S being RealNormSpace
for x being Point of S
for IT being sequence of S holds
( IT is x -convergent iff ( IT is convergent & lim IT = x ) );
theorem Th18: :: NDIFF_1:18
for X being RealNormSpace
for seq being sequence of X st seq is constant holds
( seq is convergent & ( for k being Element of NAT holds lim seq = seq . k ) )
proof
let X be RealNormSpace; ::_thesis: for seq being sequence of X st seq is constant holds
( seq is convergent & ( for k being Element of NAT holds lim seq = seq . k ) )
let seq be sequence of X; ::_thesis: ( seq is constant implies ( seq is convergent & ( for k being Element of NAT holds lim seq = seq . k ) ) )
assume A1: seq is constant ; ::_thesis: ( seq is convergent & ( for k being Element of NAT holds lim seq = seq . k ) )
then consider r being Point of X such that
A2: for n being Nat holds seq . n = r by VALUED_0:def_18;
thus A3: seq is convergent by A1, LOPBAN_3:12; ::_thesis: for k being Element of NAT holds lim seq = seq . k
now__::_thesis:_for_k_being_Element_of_NAT_holds_lim_seq_=_seq_._k
let k be Element of NAT ; ::_thesis: lim seq = seq . k
now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.((seq_._m)_-_(seq_._k)).||_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . k)).|| < p )
assume A4: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . k)).|| < p
take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . k)).|| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((seq . m) - (seq . k)).|| < p )
assume n <= m ; ::_thesis: ||.((seq . m) - (seq . k)).|| < p
||.((seq . m) - (seq . k)).|| = ||.(r - (seq . k)).|| by A2
.= ||.(r - r).|| by A2
.= ||.(0. X).|| by RLVECT_1:15
.= 0 by NORMSP_1:1 ;
hence ||.((seq . m) - (seq . k)).|| < p by A4; ::_thesis: verum
end;
hence lim seq = seq . k by A3, NORMSP_1:def_7; ::_thesis: verum
end;
hence for k being Element of NAT holds lim seq = seq . k ; ::_thesis: verum
end;
theorem Th19: :: NDIFF_1:19
for S being RealNormSpace
for seq being sequence of S
for x0 being Point of S
for r being Real st 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) holds
seq is convergent
proof
let S be RealNormSpace; ::_thesis: for seq being sequence of S
for x0 being Point of S
for r being Real st 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) holds
seq is convergent
let seq be sequence of S; ::_thesis: for x0 being Point of S
for r being Real st 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) holds
seq is convergent
let x0 be Point of S; ::_thesis: for r being Real st 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) holds
seq is convergent
let r be Real; ::_thesis: ( 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) implies seq is convergent )
assume that
A1: 0 < r and
A2: for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ; ::_thesis: seq is convergent
take g = 0. S; :: according to NORMSP_1:def_6 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= ||.((seq . b3) - g).|| ) )
let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= ||.((seq . b2) - g).|| ) )
assume A3: 0 < p ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= ||.((seq . b2) - g).|| )
ex pp being Real st
( pp > 0 & pp * ||.x0.|| < p )
proof
take pp = p / (||.x0.|| + 1); ::_thesis: ( pp > 0 & pp * ||.x0.|| < p )
A4: ( ||.x0.|| + 0 < ||.x0.|| + 1 & 0 <= ||.x0.|| ) by NORMSP_1:4, XREAL_1:8;
A5: ||.x0.|| + 1 > 0 + 0 by NORMSP_1:4, XREAL_1:8;
then 0 < p / (||.x0.|| + 1) by A3, XREAL_1:139;
then pp * ||.x0.|| < pp * (||.x0.|| + 1) by A4, XREAL_1:97;
hence ( pp > 0 & pp * ||.x0.|| < p ) by A3, A5, XCMPLX_1:87; ::_thesis: verum
end;
then consider pp being Real such that
A6: pp > 0 and
A7: pp * ||.x0.|| < p ;
consider k1 being Element of NAT such that
A8: pp " < k1 by SEQ_4:3;
(pp ") + 0 < k1 + r by A1, A8, XREAL_1:8;
then 1 / (k1 + r) < 1 / (pp ") by A6, XREAL_1:76;
then A9: 1 / (k1 + r) < 1 * ((pp ") ") by XCMPLX_0:def_9;
take n = k1; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or not p <= ||.((seq . b1) - g).|| )
let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= ||.((seq . m) - g).|| )
assume n <= m ; ::_thesis: not p <= ||.((seq . m) - g).||
then A10: n + r <= m + r by XREAL_1:6;
A11: 0 <= ||.x0.|| by NORMSP_1:4;
0 < pp " by A6;
then 1 / (m + r) <= 1 / (n + r) by A1, A8, A10, XREAL_1:118;
then 1 / (m + r) < pp by A9, XXREAL_0:2;
then A12: (1 / (m + r)) * ||.x0.|| <= pp * ||.x0.|| by A11, XREAL_1:64;
A13: 0 <= m by NAT_1:2;
||.((seq . m) - g).|| = ||.(((1 / (m + r)) * x0) - (0. S)).|| by A2
.= ||.((1 / (m + r)) * x0).|| by RLVECT_1:13
.= (abs (1 / (m + r))) * ||.x0.|| by NORMSP_1:def_1
.= (1 / (m + r)) * ||.x0.|| by A1, A13, ABSVALUE:def_1 ;
hence not p <= ||.((seq . m) - g).|| by A7, A12, XXREAL_0:2; ::_thesis: verum
end;
theorem Th20: :: NDIFF_1:20
for S being RealNormSpace
for seq being sequence of S
for x0 being Point of S
for r being Real st 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) holds
lim seq = 0. S
proof
let S be RealNormSpace; ::_thesis: for seq being sequence of S
for x0 being Point of S
for r being Real st 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) holds
lim seq = 0. S
let seq be sequence of S; ::_thesis: for x0 being Point of S
for r being Real st 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) holds
lim seq = 0. S
let x0 be Point of S; ::_thesis: for r being Real st 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) holds
lim seq = 0. S
let r be Real; ::_thesis: ( 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) implies lim seq = 0. S )
assume that
A1: 0 < r and
A2: for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ; ::_thesis: lim seq = 0. S
A3: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.((seq_._m)_-_(0._S)).||_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (0. S)).|| < p )
A4: 0 <= ||.x0.|| by NORMSP_1:4;
assume A5: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (0. S)).|| < p
ex pp being Real st
( pp > 0 & pp * ||.x0.|| < p )
proof
take pp = p / (||.x0.|| + 1); ::_thesis: ( pp > 0 & pp * ||.x0.|| < p )
A6: ( ||.x0.|| + 0 < ||.x0.|| + 1 & 0 <= ||.x0.|| ) by NORMSP_1:4, XREAL_1:8;
A7: ||.x0.|| + 1 > 0 + 0 by NORMSP_1:4, XREAL_1:8;
then 0 < p / (||.x0.|| + 1) by A5, XREAL_1:139;
then pp * ||.x0.|| < pp * (||.x0.|| + 1) by A6, XREAL_1:97;
hence ( pp > 0 & pp * ||.x0.|| < p ) by A5, A7, XCMPLX_1:87; ::_thesis: verum
end;
then consider pp being Real such that
A8: pp > 0 and
A9: pp * ||.x0.|| < p ;
consider k1 being Element of NAT such that
A10: pp " < k1 by SEQ_4:3;
(pp ") + 0 < k1 + r by A1, A10, XREAL_1:8;
then 1 / (k1 + r) < 1 / (pp ") by A8, XREAL_1:76;
then A11: 1 / (k1 + r) < 1 * ((pp ") ") by XCMPLX_0:def_9;
take n = k1; ::_thesis: for m being Element of NAT st n <= m holds
||.((seq . m) - (0. S)).|| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((seq . m) - (0. S)).|| < p )
assume n <= m ; ::_thesis: ||.((seq . m) - (0. S)).|| < p
then A12: n + r <= m + r by XREAL_1:6;
0 < pp " by A8;
then 1 / (m + r) <= 1 / (n + r) by A1, A10, A12, XREAL_1:118;
then 1 / (m + r) < pp by A11, XXREAL_0:2;
then A13: (1 / (m + r)) * ||.x0.|| <= pp * ||.x0.|| by A4, XREAL_1:64;
A14: 0 <= m by NAT_1:2;
||.((seq . m) - (0. S)).|| = ||.(((1 / (m + r)) * x0) - (0. S)).|| by A2
.= ||.((1 / (m + r)) * x0).|| by RLVECT_1:13
.= (abs (1 / (m + r))) * ||.x0.|| by NORMSP_1:def_1
.= (1 / (m + r)) * ||.x0.|| by A1, A14, ABSVALUE:def_1 ;
hence ||.((seq . m) - (0. S)).|| < p by A9, A13, XXREAL_0:2; ::_thesis: verum
end;
seq is convergent by A1, A2, Th19;
hence lim seq = 0. S by A3, NORMSP_1:def_7; ::_thesis: verum
end;
registration
let S be non trivial RealNormSpace;
clusterV1() V16() V19( NAT ) V20( the carrier of S) Function-like total quasi_total non-zero 0. S -convergent for Element of K6(K7(NAT, the carrier of S));
existence
ex b1 being sequence of S st
( b1 is non-zero & b1 is 0. S -convergent )
proof
consider x0 being Point of S such that
A1: x0 <> 0. S by STRUCT_0:def_18;
deffunc H1( Element of NAT ) -> Element of the carrier of S = (1 / (S + 1)) * x0;
consider s1 being sequence of S such that
A2: for n being Element of NAT holds s1 . n = H1(n) from FUNCT_2:sch_4();
take s1 ; ::_thesis: ( s1 is non-zero & s1 is 0. S -convergent )
now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_<>_0._S
let n be Element of NAT ; ::_thesis: s1 . n <> 0. S
(n + 1) " <> 0 by NAT_1:5, XCMPLX_1:202;
then A3: 1 / (n + 1) <> 0 by XCMPLX_1:215;
thus s1 . n <> 0. S ::_thesis: verum
proof
assume s1 . n = 0. S ; ::_thesis: contradiction
then (1 / (n + 1)) * x0 = 0. S by A2;
hence contradiction by A1, A3, RLVECT_1:11; ::_thesis: verum
end;
end;
hence s1 is non-zero by Th7; ::_thesis: s1 is 0. S -convergent
A4: lim s1 = 0. S by A2, Th20;
s1 is convergent by A2, Th19;
then s1 is 0. S -convergent by Def4, A4;
hence s1 is 0. S -convergent ; ::_thesis: verum
end;
end;
theorem :: NDIFF_1:21
for S being RealNormSpace
for a being non-zero 0 -convergent Real_Sequence
for z being Point of S st z <> 0. S holds
( a * z is non-zero & a * z is 0. S -convergent )
proof
let S be RealNormSpace; ::_thesis: for a being non-zero 0 -convergent Real_Sequence
for z being Point of S st z <> 0. S holds
( a * z is non-zero & a * z is 0. S -convergent )
let a be non-zero 0 -convergent Real_Sequence; ::_thesis: for z being Point of S st z <> 0. S holds
( a * z is non-zero & a * z is 0. S -convergent )
let z be Point of S; ::_thesis: ( z <> 0. S implies ( a * z is non-zero & a * z is 0. S -convergent ) )
assume A1: z <> 0. S ; ::_thesis: ( a * z is non-zero & a * z is 0. S -convergent )
now__::_thesis:_for_n_being_Element_of_NAT_holds_not_(a_*_z)_._n_=_0._S
let n be Element of NAT ; ::_thesis: not (a * z) . n = 0. S
A2: a . n <> 0 by SEQ_1:5;
assume (a * z) . n = 0. S ; ::_thesis: contradiction
then (a . n) * z = 0. S by Def3;
hence contradiction by A1, A2, RLVECT_1:11; ::_thesis: verum
end;
hence a * z is non-zero by Th7; ::_thesis: a * z is 0. S -convergent
A3: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.(((a_*_z)_._m)_-_(0._S)).||_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((a * z) . m) - (0. S)).|| < p )
assume A4: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((a * z) . m) - (0. S)).|| < p
ex pp being Real st
( pp > 0 & pp * ||.z.|| < p )
proof
take pp = p / (||.z.|| + 1); ::_thesis: ( pp > 0 & pp * ||.z.|| < p )
A5: ( ||.z.|| + 0 < ||.z.|| + 1 & 0 <= ||.z.|| ) by NORMSP_1:4, XREAL_1:8;
A6: ||.z.|| + 1 > 0 + 0 by NORMSP_1:4, XREAL_1:8;
then 0 < p / (||.z.|| + 1) by A4, XREAL_1:139;
then pp * ||.z.|| < pp * (||.z.|| + 1) by A5, XREAL_1:97;
hence ( pp > 0 & pp * ||.z.|| < p ) by A4, A6, XCMPLX_1:87; ::_thesis: verum
end;
then consider pp being Real such that
A7: pp > 0 and
A8: pp * ||.z.|| < p ;
( a is convergent & lim a = 0 ) ;
then consider n being Element of NAT such that
A9: for m being Element of NAT st n <= m holds
abs ((a . m) - 0) < pp by A7, SEQ_2:def_7;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
||.(((a * z) . m) - (0. S)).|| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((a * z) . m) - (0. S)).|| < p )
assume n <= m ; ::_thesis: ||.(((a * z) . m) - (0. S)).|| < p
then A10: abs ((a . m) - 0) < pp by A9;
A11: ||.(((a * z) . m) - (0. S)).|| = ||.(((a . m) * z) - (0. S)).|| by Def3
.= ||.((a . m) * z).|| by RLVECT_1:13
.= (abs (a . m)) * ||.z.|| by NORMSP_1:def_1 ;
0 <= ||.z.|| by NORMSP_1:4;
then (abs (a . m)) * ||.z.|| <= pp * ||.z.|| by A10, XREAL_1:64;
hence ||.(((a * z) . m) - (0. S)).|| < p by A8, A11, XXREAL_0:2; ::_thesis: verum
end;
hence a * z is convergent by NORMSP_1:def_6; :: according to NDIFF_1:def_4 ::_thesis: lim (a * z) = 0. S
hence lim (a * z) = 0. S by A3, NORMSP_1:def_7; ::_thesis: verum
end;
theorem :: NDIFF_1:22
for S being RealNormSpace
for Y being Subset of S holds
( ( for r being Point of S holds
( r in Y iff r in the carrier of S ) ) iff Y = the carrier of S )
proof
let S be RealNormSpace; ::_thesis: for Y being Subset of S holds
( ( for r being Point of S holds
( r in Y iff r in the carrier of S ) ) iff Y = the carrier of S )
let Y be Subset of S; ::_thesis: ( ( for r being Point of S holds
( r in Y iff r in the carrier of S ) ) iff Y = the carrier of S )
thus ( ( for r being Point of S holds
( r in Y iff r in the carrier of S ) ) implies Y = the carrier of S ) ::_thesis: ( Y = the carrier of S implies for r being Point of S holds
( r in Y iff r in the carrier of S ) )
proof
assume for r being Point of S holds
( r in Y iff r in the carrier of S ) ; ::_thesis: Y = the carrier of S
then for y being set holds
( y in Y iff y in the carrier of S ) ;
hence Y = the carrier of S by TARSKI:1; ::_thesis: verum
end;
assume A1: Y = the carrier of S ; ::_thesis: for r being Point of S holds
( r in Y iff r in the carrier of S )
let r be Point of S; ::_thesis: ( r in Y iff r in the carrier of S )
thus ( r in Y implies r in the carrier of S ) ; ::_thesis: ( r in the carrier of S implies r in Y )
thus ( r in the carrier of S implies r in Y ) by A1; ::_thesis: verum
end;
registration
let S be non trivial RealNormSpace;
clusterV1() V16() V19( NAT ) V20( the carrier of S) Function-like constant total quasi_total for Element of K6(K7(NAT, the carrier of S));
existence
ex b1 being sequence of S st b1 is constant
proof
reconsider s1 = NAT --> (0. S) as sequence of S ;
take s1 ; ::_thesis: s1 is constant
thus s1 is constant ; ::_thesis: verum
end;
end;
definition
let S, T be non trivial RealNormSpace;
let IT be PartFunc of S,T;
attrIT is RestFunc-like means :Def5: :: NDIFF_1:def 5
( IT is total & ( for h being non-zero 0. S -convergent sequence of S holds
( (||.h.|| ") (#) (IT /* h) is convergent & lim ((||.h.|| ") (#) (IT /* h)) = 0. T ) ) );
end;
:: deftheorem Def5 defines RestFunc-like NDIFF_1:def_5_:_
for S, T being non trivial RealNormSpace
for IT being PartFunc of S,T holds
( IT is RestFunc-like iff ( IT is total & ( for h being non-zero 0. b1 -convergent sequence of S holds
( (||.h.|| ") (#) (IT /* h) is convergent & lim ((||.h.|| ") (#) (IT /* h)) = 0. T ) ) ) );
registration
let S, T be non trivial RealNormSpace;
clusterV16() V19( the carrier of S) V20( the carrier of T) Function-like RestFunc-like for Element of K6(K7( the carrier of S, the carrier of T));
existence
ex b1 being PartFunc of S,T st b1 is RestFunc-like
proof
reconsider f = the carrier of S --> (0. T) as PartFunc of S,T ;
take f ; ::_thesis: f is RestFunc-like
thus f is total ; :: according to NDIFF_1:def_5 ::_thesis: for h being non-zero 0. S -convergent sequence of S holds
( (||.h.|| ") (#) (f /* h) is convergent & lim ((||.h.|| ") (#) (f /* h)) = 0. T )
A1: dom f = the carrier of S by FUNCOP_1:13;
now__::_thesis:_for_h_being_non-zero_0._S_-convergent_sequence_of_S_holds_
(_(||.h.||_")_(#)_(f_/*_h)_is_convergent_&_lim_((||.h.||_")_(#)_(f_/*_h))_=_0._T_)
let h be non-zero 0. S -convergent sequence of S; ::_thesis: ( (||.h.|| ") (#) (f /* h) is convergent & lim ((||.h.|| ") (#) (f /* h)) = 0. T )
now__::_thesis:_for_n_being_Nat_holds_((||.h.||_")_(#)_(f_/*_h))_._n_=_0._T
let n be Nat; ::_thesis: ((||.h.|| ") (#) (f /* h)) . n = 0. T
A2: f /. (h . n) = f . (h . n) by A1, PARTFUN1:def_6
.= 0. T by FUNCOP_1:7 ;
A3: rng h c= dom f by A1;
A4: n in NAT by ORDINAL1:def_12;
hence ((||.h.|| ") (#) (f /* h)) . n = ((||.h.|| ") . n) * ((f /* h) . n) by Def2
.= ((||.h.|| ") . n) * (f /. (h . n)) by A3, A4, FUNCT_2:109
.= 0. T by A2, RLVECT_1:10 ;
::_thesis: verum
end;
then ( (||.h.|| ") (#) (f /* h) is constant & ((||.h.|| ") (#) (f /* h)) . 0 = 0. T ) by VALUED_0:def_18;
hence ( (||.h.|| ") (#) (f /* h) is convergent & lim ((||.h.|| ") (#) (f /* h)) = 0. T ) by Th18; ::_thesis: verum
end;
hence for h being non-zero 0. S -convergent sequence of S holds
( (||.h.|| ") (#) (f /* h) is convergent & lim ((||.h.|| ") (#) (f /* h)) = 0. T ) ; ::_thesis: verum
end;
end;
definition
let S, T be non trivial RealNormSpace;
mode RestFunc of S,T is RestFunc-like PartFunc of S,T;
end;
theorem :: NDIFF_1:23
for S, T being non trivial RealNormSpace
for R being PartFunc of S,T st R is total holds
( R is RestFunc-like iff for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) )
proof
let S, T be non trivial RealNormSpace; ::_thesis: for R being PartFunc of S,T st R is total holds
( R is RestFunc-like iff for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) )
let R be PartFunc of S,T; ::_thesis: ( R is total implies ( R is RestFunc-like iff for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) ) )
assume A1: R is total ; ::_thesis: ( R is RestFunc-like iff for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) )
A2: now__::_thesis:_(_R_is_RestFunc-like_&_ex_r_being_Real_st_
(_r_>_0_&_(_for_d_being_Real_holds_
(_not_d_>_0_or_ex_z_being_Point_of_S_st_
(_z_<>_0._S_&_||.z.||_<_d_&_not_(||.z.||_")_*_||.(R_/._z).||_<_r_)_)_)_)_implies_for_r_being_Real_st_r_>_0_holds_
ex_d_being_Real_st_
(_d_>_0_&_(_for_z_being_Point_of_S_st_z_<>_0._S_&_||.z.||_<_d_holds_
(||.z.||_")_*_||.(R_/._z).||_<_r_)_)_)
assume A3: R is RestFunc-like ; ::_thesis: ( ex r being Real st
( r > 0 & ( for d being Real holds
( not d > 0 or ex z being Point of S st
( z <> 0. S & ||.z.|| < d & not (||.z.|| ") * ||.(R /. z).|| < r ) ) ) ) implies for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) )
assume ex r being Real st
( r > 0 & ( for d being Real holds
( not d > 0 or ex z being Point of S st
( z <> 0. S & ||.z.|| < d & not (||.z.|| ") * ||.(R /. z).|| < r ) ) ) ) ; ::_thesis: for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) )
then consider r being Real such that
A4: r > 0 and
A5: for d being Real st d > 0 holds
ex z being Point of S st
( z <> 0. S & ||.z.|| < d & not (||.z.|| ") * ||.(R /. z).|| < r ) ;
defpred S1[ Element of NAT , Point of S] means ( $2 <> 0. S & ||.$2.|| < 1 / ($1 + 1) & not (||.$2.|| ") * ||.(R /. $2).|| < r );
A6: for n being Element of NAT ex z being Point of S st S1[n,z]
proof
let n be Element of NAT ; ::_thesis: ex z being Point of S st S1[n,z]
0 <= n by NAT_1:2;
then 0 < 1 * ((n + 1) ") ;
then 0 < 1 / (n + 1) by XCMPLX_0:def_9;
hence ex z being Point of S st S1[n,z] by A5; ::_thesis: verum
end;
consider s being sequence of S such that
A7: for n being Element of NAT holds S1[n,s . n] from FUNCT_2:sch_3(A6);
A8: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.((s_._m)_-_(0._S)).||_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((s . m) - (0. S)).|| < p )
assume A9: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((s . m) - (0. S)).|| < p
consider n being Element of NAT such that
A10: p " < n by SEQ_4:3;
(p ") + 0 < n + 1 by A10, XREAL_1:8;
then 1 / (n + 1) < 1 / (p ") by A9, XREAL_1:76;
then A11: 1 / (n + 1) < p by XCMPLX_1:216;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
||.((s . m) - (0. S)).|| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((s . m) - (0. S)).|| < p )
assume n <= m ; ::_thesis: ||.((s . m) - (0. S)).|| < p
then A12: n + 1 <= m + 1 by XREAL_1:6;
||.(s . m).|| < 1 / (m + 1) by A7;
then A13: ||.((s . m) - (0. S)).|| < 1 / (m + 1) by RLVECT_1:13;
0 <= n by NAT_1:2;
then 1 / (m + 1) <= 1 / (n + 1) by A12, XREAL_1:118;
then ||.((s . m) - (0. S)).|| < 1 / (n + 1) by A13, XXREAL_0:2;
hence ||.((s . m) - (0. S)).|| < p by A11, XXREAL_0:2; ::_thesis: verum
end;
then A14: s is convergent by NORMSP_1:def_6;
then A15: lim s = 0. S by A8, NORMSP_1:def_7;
s is non-zero by A7, Th7;
then reconsider s = s as non-zero 0. S -convergent sequence of S by A14, A15, Def4;
( (||.s.|| ") (#) (R /* s) is convergent & lim ((||.s.|| ") (#) (R /* s)) = 0. T ) by A3, Def5;
then consider n being Element of NAT such that
A16: for m being Element of NAT st n <= m holds
||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r by A4, NORMSP_1:def_7;
A17: ||.((((||.s.|| ") (#) (R /* s)) . n) - (0. T)).|| < r by A16;
s . n <> 0. S by A7;
then ||.(s . n).|| <> 0 by NORMSP_0:def_5;
then A18: ||.(s . n).|| > 0 by NORMSP_1:4;
A19: ||.((||.(s . n).|| ") * (R /. (s . n))).|| = (abs (||.(s . n).|| ")) * ||.(R /. (s . n)).|| by NORMSP_1:def_1
.= (||.(s . n).|| ") * ||.(R /. (s . n)).|| by A18, ABSVALUE:def_1 ;
dom R = the carrier of S by A1, PARTFUN1:def_2;
then A20: rng s c= dom R ;
||.((((||.s.|| ") (#) (R /* s)) . n) - (0. T)).|| = ||.(((||.s.|| ") (#) (R /* s)) . n).|| by RLVECT_1:13
.= ||.(((||.s.|| ") . n) * ((R /* s) . n)).|| by Def2
.= ||.(((||.s.|| . n) ") * ((R /* s) . n)).|| by VALUED_1:10
.= ||.((||.(s . n).|| ") * ((R /* s) . n)).|| by NORMSP_0:def_4
.= ||.((||.(s . n).|| ") * (R /. (s . n))).|| by A20, FUNCT_2:109 ;
hence for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) by A7, A17, A19; ::_thesis: verum
end;
now__::_thesis:_(_(_for_r_being_Real_st_r_>_0_holds_
ex_d_being_Real_st_
(_d_>_0_&_(_for_z_being_Point_of_S_st_z_<>_0._S_&_||.z.||_<_d_holds_
(||.z.||_")_*_||.(R_/._z).||_<_r_)_)_)_implies_R_is_RestFunc-like_)
assume A21: for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) ; ::_thesis: R is RestFunc-like
now__::_thesis:_for_s_being_non-zero_0._S_-convergent_sequence_of_S_holds_
(_(||.s.||_")_(#)_(R_/*_s)_is_convergent_&_lim_((||.s.||_")_(#)_(R_/*_s))_=_0._T_)
let s be non-zero 0. S -convergent sequence of S; ::_thesis: ( (||.s.|| ") (#) (R /* s) is convergent & lim ((||.s.|| ") (#) (R /* s)) = 0. T )
A22: ( s is convergent & lim s = 0. S ) by Def4;
A23: now__::_thesis:_for_r_being_Real_st_r_>_0_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.((((||.s.||_")_(#)_(R_/*_s))_._m)_-_(0._T)).||_<_r
let r be Real; ::_thesis: ( r > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r )
assume r > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r
then consider d being Real such that
A24: d > 0 and
A25: for z being Point of S st z <> 0. S & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r by A21;
consider n being Element of NAT such that
A26: for m being Element of NAT st n <= m holds
||.((s . m) - (0. S)).|| < d by A22, A24, NORMSP_1:def_7;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r
thus for m being Element of NAT st n <= m holds
||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r ::_thesis: verum
proof
dom R = the carrier of S by A1, PARTFUN1:def_2;
then A27: rng s c= dom R ;
let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r )
assume n <= m ; ::_thesis: ||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r
then ||.((s . m) - (0. S)).|| < d by A26;
then A28: ||.(s . m).|| < d by RLVECT_1:13;
A29: s . m <> 0. S by Th7;
s . m <> 0. S by Th7;
then ||.(s . m).|| <> 0 by NORMSP_0:def_5;
then ||.(s . m).|| > 0 by NORMSP_1:4;
then (||.(s . m).|| ") * ||.(R /. (s . m)).|| = (abs (||.(s . m).|| ")) * ||.(R /. (s . m)).|| by ABSVALUE:def_1
.= ||.((||.(s . m).|| ") * (R /. (s . m))).|| by NORMSP_1:def_1
.= ||.((||.(s . m).|| ") * ((R /* s) . m)).|| by A27, FUNCT_2:109
.= ||.(((||.s.|| . m) ") * ((R /* s) . m)).|| by NORMSP_0:def_4
.= ||.(((||.s.|| ") . m) * ((R /* s) . m)).|| by VALUED_1:10
.= ||.(((||.s.|| ") (#) (R /* s)) . m).|| by Def2
.= ||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| by RLVECT_1:13 ;
hence ||.((((||.s.|| ") (#) (R /* s)) . m) - (0. T)).|| < r by A25, A28, A29; ::_thesis: verum
end;
end;
hence (||.s.|| ") (#) (R /* s) is convergent by NORMSP_1:def_6; ::_thesis: lim ((||.s.|| ") (#) (R /* s)) = 0. T
hence lim ((||.s.|| ") (#) (R /* s)) = 0. T by A23, NORMSP_1:def_7; ::_thesis: verum
end;
hence R is RestFunc-like by A1, Def5; ::_thesis: verum
end;
hence ( R is RestFunc-like iff for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) ) by A2; ::_thesis: verum
end;
theorem Th24: :: NDIFF_1:24
for S, T being non trivial RealNormSpace
for R being RestFunc of S,T
for s being non-zero 0. b1 -convergent sequence of S holds
( R /* s is convergent & lim (R /* s) = 0. T )
proof
let S, T be non trivial RealNormSpace; ::_thesis: for R being RestFunc of S,T
for s being non-zero 0. S -convergent sequence of S holds
( R /* s is convergent & lim (R /* s) = 0. T )
let R be RestFunc of S,T; ::_thesis: for s being non-zero 0. S -convergent sequence of S holds
( R /* s is convergent & lim (R /* s) = 0. T )
let s be non-zero 0. S -convergent sequence of S; ::_thesis: ( R /* s is convergent & lim (R /* s) = 0. T )
A1: (||.s.|| ") (#) (R /* s) is convergent by Def5;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(||.s.||_(#)_((||.s.||_")_(#)_(R_/*_s)))_._n_=_(R_/*_s)_._n
let n be Element of NAT ; ::_thesis: (||.s.|| (#) ((||.s.|| ") (#) (R /* s))) . n = (R /* s) . n
s . n <> 0. S by Th7;
then A2: ||.(s . n).|| <> 0 by NORMSP_0:def_5;
thus (||.s.|| (#) ((||.s.|| ") (#) (R /* s))) . n = (||.s.|| . n) * (((||.s.|| ") (#) (R /* s)) . n) by Def2
.= (||.s.|| . n) * (((||.s.|| ") . n) * ((R /* s) . n)) by Def2
.= ||.(s . n).|| * (((||.s.|| ") . n) * ((R /* s) . n)) by NORMSP_0:def_4
.= ||.(s . n).|| * (((||.s.|| . n) ") * ((R /* s) . n)) by VALUED_1:10
.= ||.(s . n).|| * ((||.(s . n).|| ") * ((R /* s) . n)) by NORMSP_0:def_4
.= (||.(s . n).|| * (||.(s . n).|| ")) * ((R /* s) . n) by RLVECT_1:def_7
.= 1 * ((R /* s) . n) by A2, XCMPLX_0:def_7
.= (R /* s) . n by RLVECT_1:def_8 ; ::_thesis: verum
end;
then A3: ||.s.|| (#) ((||.s.|| ") (#) (R /* s)) = R /* s by FUNCT_2:63;
A4: s is convergent by Def4;
then A5: ||.s.|| is convergent by LOPBAN_1:41;
lim s = 0. S by Def4;
then lim ||.s.|| = ||.(0. S).|| by A4, LOPBAN_1:41;
then A6: lim ||.s.|| = 0 by NORMSP_1:1;
lim ((||.s.|| ") (#) (R /* s)) = 0. T by Def5;
then lim (R /* s) = 0 * (0. T) by A4, A3, A1, A6, Th14, LOPBAN_1:41;
hence ( R /* s is convergent & lim (R /* s) = 0. T ) by A3, A1, A5, Th13, RLVECT_1:10; ::_thesis: verum
end;
theorem Th25: :: NDIFF_1:25
for S, T being non trivial RealNormSpace
for h1, h2 being PartFunc of S,T
for seq being sequence of S st h1 is total & h2 is total holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )
proof
let S, T be non trivial RealNormSpace; ::_thesis: for h1, h2 being PartFunc of S,T
for seq being sequence of S st h1 is total & h2 is total holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )
let h1, h2 be PartFunc of S,T; ::_thesis: for seq being sequence of S st h1 is total & h2 is total holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )
let seq be sequence of S; ::_thesis: ( h1 is total & h2 is total implies ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) ) )
assume ( h1 is total & h2 is total ) ; ::_thesis: ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )
then h1 + h2 is total by VFUNCT_1:32;
then dom (h1 + h2) = the carrier of S by PARTFUN1:def_2;
then (dom h1) /\ (dom h2) = the carrier of S by VFUNCT_1:def_1;
then A1: rng seq c= (dom h1) /\ (dom h2) ;
hence (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) by NFCONT_1:12; ::_thesis: (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq)
thus (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) by A1, NFCONT_1:12; ::_thesis: verum
end;
theorem Th26: :: NDIFF_1:26
for S, T being non trivial RealNormSpace
for h being PartFunc of S,T
for seq being sequence of S
for r being Real st h is total holds
(r (#) h) /* seq = r * (h /* seq)
proof
let S, T be non trivial RealNormSpace; ::_thesis: for h being PartFunc of S,T
for seq being sequence of S
for r being Real st h is total holds
(r (#) h) /* seq = r * (h /* seq)
let h be PartFunc of S,T; ::_thesis: for seq being sequence of S
for r being Real st h is total holds
(r (#) h) /* seq = r * (h /* seq)
let seq be sequence of S; ::_thesis: for r being Real st h is total holds
(r (#) h) /* seq = r * (h /* seq)
let r be Real; ::_thesis: ( h is total implies (r (#) h) /* seq = r * (h /* seq) )
assume h is total ; ::_thesis: (r (#) h) /* seq = r * (h /* seq)
then dom h = the carrier of S by PARTFUN1:def_2;
then rng seq c= dom h ;
hence (r (#) h) /* seq = r * (h /* seq) by NFCONT_1:13; ::_thesis: verum
end;
theorem Th27: :: NDIFF_1:27
for T, S being non trivial RealNormSpace
for f being PartFunc of S,T
for x0 being Point of S holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )
proof
let T, S be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,T
for x0 being Point of S holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )
let f be PartFunc of S,T; ::_thesis: for x0 being Point of S holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )
let x0 be Point of S; ::_thesis: ( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )
thus ( f is_continuous_in x0 implies ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) ) by NFCONT_1:def_5; ::_thesis: ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) implies f is_continuous_in x0 )
assume that
A1: x0 in dom f and
A2: for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ; ::_thesis: f is_continuous_in x0
thus x0 in dom f by A1; :: according to NFCONT_1:def_5 ::_thesis: for b1 being Element of K6(K7(NAT, the carrier of S)) holds
( not rng b1 c= dom f or not b1 is convergent or not lim b1 = x0 or ( f /* b1 is convergent & f /. x0 = lim (f /* b1) ) )
let s2 be sequence of S; ::_thesis: ( not rng s2 c= dom f or not s2 is convergent or not lim s2 = x0 or ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) )
assume that
A3: rng s2 c= dom f and
A4: ( s2 is convergent & lim s2 = x0 ) ; ::_thesis: ( f /* s2 is convergent & f /. x0 = lim (f /* s2) )
now__::_thesis:_(_f_/*_s2_is_convergent_&_f_/._x0_=_lim_(f_/*_s2)_)
percases ( ex n being Element of NAT st
for m being Element of NAT st n <= m holds
s2 . m = x0 or for n being Element of NAT ex m being Element of NAT st
( n <= m & s2 . m <> x0 ) ) ;
suppose ex n being Element of NAT st
for m being Element of NAT st n <= m holds
s2 . m = x0 ; ::_thesis: ( f /* s2 is convergent & f /. x0 = lim (f /* s2) )
then consider N being Element of NAT such that
A5: for m being Element of NAT st N <= m holds
s2 . m = x0 ;
A6: for n being Element of NAT holds (s2 ^\ N) . n = x0
proof
let n be Element of NAT ; ::_thesis: (s2 ^\ N) . n = x0
s2 . (n + N) = x0 by A5, NAT_1:12;
hence (s2 ^\ N) . n = x0 by NAT_1:def_3; ::_thesis: verum
end;
A7: rng (s2 ^\ N) c= rng s2 by VALUED_0:21;
A8: now__::_thesis:_for_p_being_Real_st_p_>_0_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.(((f_/*_(s2_^\_N))_._m)_-_(f_/._x0)).||_<_p
let p be Real; ::_thesis: ( p > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p )
assume A9: p > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p
take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds
||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p )
assume n <= m ; ::_thesis: ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p
||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| = ||.((f /. ((s2 ^\ N) . m)) - (f /. x0)).|| by A3, A7, FUNCT_2:109, XBOOLE_1:1
.= ||.((f /. x0) - (f /. x0)).|| by A6
.= ||.(0. T).|| by RLVECT_1:15
.= 0 by NORMSP_1:1 ;
hence ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p by A9; ::_thesis: verum
end;
then A10: f /* (s2 ^\ N) is convergent by NORMSP_1:def_6;
A11: f /* (s2 ^\ N) = (f /* s2) ^\ N by A3, VALUED_0:27;
then A12: f /* s2 is convergent by A10, LOPBAN_3:10;
f /. x0 = lim ((f /* s2) ^\ N) by A8, A10, A11, NORMSP_1:def_7;
hence ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) by A12, LOPBAN_3:9; ::_thesis: verum
end;
supposeA13: for n being Element of NAT ex m being Element of NAT st
( n <= m & s2 . m <> x0 ) ; ::_thesis: ( f /* s2 is convergent & f /. x0 = lim (f /* s2) )
defpred S1[ Element of NAT , set , set ] means for n, m being Element of NAT st $2 = n & $3 = m holds
( n < m & s2 . m <> x0 & ( for k being Element of NAT st n < k & s2 . k <> x0 holds
m <= k ) );
defpred S2[ Nat] means s2 . $1 <> x0;
ex m1 being Element of NAT st
( 0 <= m1 & s2 . m1 <> x0 ) by A13;
then A14: ex m being Nat st S2[m] ;
consider M being Nat such that
A15: ( S2[M] & ( for n being Nat st S2[n] holds
M <= n ) ) from NAT_1:sch_5(A14);
reconsider M9 = M as Element of NAT by ORDINAL1:def_12;
A16: now__::_thesis:_for_n_being_Element_of_NAT_ex_m_being_Element_of_NAT_st_
(_n_<_m_&_s2_._m_<>_x0_)
let n be Element of NAT ; ::_thesis: ex m being Element of NAT st
( n < m & s2 . m <> x0 )
consider m being Element of NAT such that
A17: ( n + 1 <= m & s2 . m <> x0 ) by A13;
take m = m; ::_thesis: ( n < m & s2 . m <> x0 )
thus ( n < m & s2 . m <> x0 ) by A17, NAT_1:13; ::_thesis: verum
end;
A18: for n, x being Element of NAT ex y being Element of NAT st S1[n,x,y]
proof
let n, x be Element of NAT ; ::_thesis: ex y being Element of NAT st S1[n,x,y]
defpred S3[ Nat] means ( x < $1 & s2 . $1 <> x0 );
ex m being Element of NAT st S3[m] by A16;
then A19: ex m being Nat st S3[m] ;
consider l being Nat such that
A20: ( S3[l] & ( for k being Nat st S3[k] holds
l <= k ) ) from NAT_1:sch_5(A19);
reconsider l = l as Element of NAT by ORDINAL1:def_12;
take l ; ::_thesis: S1[n,x,l]
thus S1[n,x,l] by A20; ::_thesis: verum
end;
consider F being Function of NAT,NAT such that
A21: ( F . 0 = M9 & ( for n being Element of NAT holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A18);
A22: rng F c= REAL by XBOOLE_1:1;
A23: rng F c= NAT ;
A24: dom F = NAT by FUNCT_2:def_1;
then reconsider F = F as Real_Sequence by A22, RELSET_1:4;
A25: now__::_thesis:_for_n_being_Element_of_NAT_holds_F_._n_is_Element_of_NAT
let n be Element of NAT ; ::_thesis: F . n is Element of NAT
F . n in rng F by A24, FUNCT_1:def_3;
hence F . n is Element of NAT by A23; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_F_._n_<_F_._(n_+_1)
let n be Element of NAT ; ::_thesis: F . n < F . (n + 1)
( F . n is Element of NAT & F . (n + 1) is Element of NAT ) by A25;
hence F . n < F . (n + 1) by A21; ::_thesis: verum
end;
then reconsider F = F as V37() sequence of NAT by SEQM_3:def_6;
A26: ( s2 * F is convergent & lim (s2 * F) = x0 ) by A4, LOPBAN_3:7, LOPBAN_3:8;
A27: for n being Element of NAT st s2 . n <> x0 holds
ex m being Element of NAT st F . m = n
proof
defpred S3[ Nat] means ( s2 . $1 <> x0 & ( for m being Element of NAT holds F . m <> $1 ) );
assume ex n being Element of NAT st S3[n] ; ::_thesis: contradiction
then A28: ex n being Nat st S3[n] ;
consider M1 being Nat such that
A29: ( S3[M1] & ( for n being Nat st S3[n] holds
M1 <= n ) ) from NAT_1:sch_5(A28);
defpred S4[ Nat] means ( $1 < M1 & s2 . $1 <> x0 & ex m being Element of NAT st F . m = $1 );
A30: ex n being Nat st S4[n]
proof
take M ; ::_thesis: S4[M]
( M <= M1 & M <> M1 ) by A15, A21, A29;
hence M < M1 by XXREAL_0:1; ::_thesis: ( s2 . M <> x0 & ex m being Element of NAT st F . m = M )
thus s2 . M <> x0 by A15; ::_thesis: ex m being Element of NAT st F . m = M
take 0 ; ::_thesis: F . 0 = M
thus F . 0 = M by A21; ::_thesis: verum
end;
A31: for n being Nat st S4[n] holds
n <= M1 ;
consider MX being Nat such that
A32: ( S4[MX] & ( for n being Nat st S4[n] holds
n <= MX ) ) from NAT_1:sch_6(A31, A30);
A33: for k being Element of NAT st MX < k & k < M1 holds
s2 . k = x0
proof
given k being Element of NAT such that A34: MX < k and
A35: ( k < M1 & s2 . k <> x0 ) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( ex m being Element of NAT st F . m = k or for m being Element of NAT holds F . m <> k ) ;
suppose ex m being Element of NAT st F . m = k ; ::_thesis: contradiction
hence contradiction by A32, A34, A35; ::_thesis: verum
end;
suppose for m being Element of NAT holds F . m <> k ; ::_thesis: contradiction
hence contradiction by A29, A35; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
consider m being Element of NAT such that
A36: F . m = MX by A32;
A37: ( MX < F . (m + 1) & s2 . (F . (m + 1)) <> x0 ) by A21, A36;
M1 in NAT by ORDINAL1:def_12;
then A38: F . (m + 1) <= M1 by A21, A29, A32, A36;
now__::_thesis:_not_F_._(m_+_1)_<>_M1
assume F . (m + 1) <> M1 ; ::_thesis: contradiction
then F . (m + 1) < M1 by A38, XXREAL_0:1;
hence contradiction by A33, A37; ::_thesis: verum
end;
hence contradiction by A29; ::_thesis: verum
end;
A39: for n being Element of NAT holds (s2 * F) . n <> x0
proof
defpred S3[ Element of NAT ] means (s2 * F) . $1 <> x0;
A40: for k being Element of NAT st S3[k] holds
S3[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S3[k] implies S3[k + 1] )
assume (s2 * F) . k <> x0 ; ::_thesis: S3[k + 1]
S1[k,F . k,F . (k + 1)] by A21;
then s2 . (F . (k + 1)) <> x0 ;
hence S3[k + 1] by FUNCT_2:15; ::_thesis: verum
end;
A41: S3[ 0 ] by A15, A21, FUNCT_2:15;
thus for n being Element of NAT holds S3[n] from NAT_1:sch_1(A41, A40); ::_thesis: verum
end;
A42: rng (s2 * F) c= rng s2 by VALUED_0:21;
then rng (s2 * F) c= dom f by A3, XBOOLE_1:1;
then A43: ( f /* (s2 * F) is convergent & f /. x0 = lim (f /* (s2 * F)) ) by A2, A39, A26;
A44: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
||.(((f_/*_s2)_._m)_-_(f_/._x0)).||_<_p
let p be Real; ::_thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
||.(((f /* s2) . m) - (f /. x0)).|| < p )
assume A45: 0 < p ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
||.(((f /* s2) . m) - (f /. x0)).|| < p
then consider n being Element of NAT such that
A46: for m being Element of NAT st n <= m holds
||.(((f /* (s2 * F)) . m) - (f /. x0)).|| < p by A43, NORMSP_1:def_7;
take k = F . n; ::_thesis: for m being Element of NAT st k <= m holds
||.(((f /* s2) . m) - (f /. x0)).|| < p
let m be Element of NAT ; ::_thesis: ( k <= m implies ||.(((f /* s2) . m) - (f /. x0)).|| < p )
assume A47: k <= m ; ::_thesis: ||.(((f /* s2) . m) - (f /. x0)).|| < p
now__::_thesis:_||.(((f_/*_s2)_._m)_-_(f_/._x0)).||_<_p
percases ( s2 . m = x0 or s2 . m <> x0 ) ;
supposeA48: s2 . m = x0 ; ::_thesis: ||.(((f /* s2) . m) - (f /. x0)).|| < p
||.(((f /* s2) . m) - (f /. x0)).|| = ||.((f /. (s2 . m)) - (f /. x0)).|| by A3, FUNCT_2:109
.= ||.(0. T).|| by A48, RLVECT_1:15
.= 0 by NORMSP_1:1 ;
hence ||.(((f /* s2) . m) - (f /. x0)).|| < p by A45; ::_thesis: verum
end;
suppose s2 . m <> x0 ; ::_thesis: ||.(((f /* s2) . m) - (f /. x0)).|| < p
then consider l being Element of NAT such that
A49: m = F . l by A27;
n <= l by A47, A49, SEQM_3:1;
then ||.(((f /* (s2 * F)) . l) - (f /. x0)).|| < p by A46;
then ||.((f /. ((s2 * F) . l)) - (f /. x0)).|| < p by A3, A42, FUNCT_2:109, XBOOLE_1:1;
then ||.((f /. (s2 . m)) - (f /. x0)).|| < p by A49, FUNCT_2:15;
hence ||.(((f /* s2) . m) - (f /. x0)).|| < p by A3, FUNCT_2:109; ::_thesis: verum
end;
end;
end;
hence ||.(((f /* s2) . m) - (f /. x0)).|| < p ; ::_thesis: verum
end;
hence f /* s2 is convergent by NORMSP_1:def_6; ::_thesis: f /. x0 = lim (f /* s2)
hence f /. x0 = lim (f /* s2) by A44, NORMSP_1:def_7; ::_thesis: verum
end;
end;
end;
hence ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) ; ::_thesis: verum
end;
theorem Th28: :: NDIFF_1:28
for T, S being non trivial RealNormSpace
for R1, R2 being RestFunc of S,T holds
( R1 + R2 is RestFunc of S,T & R1 - R2 is RestFunc of S,T )
proof
let T, S be non trivial RealNormSpace; ::_thesis: for R1, R2 being RestFunc of S,T holds
( R1 + R2 is RestFunc of S,T & R1 - R2 is RestFunc of S,T )
let R1, R2 be RestFunc of S,T; ::_thesis: ( R1 + R2 is RestFunc of S,T & R1 - R2 is RestFunc of S,T )
A1: ( R1 is total & R2 is total ) by Def5;
A2: now__::_thesis:_for_h_being_non-zero_0._S_-convergent_sequence_of_S_holds_
(_(||.h.||_")_(#)_((R1_+_R2)_/*_h)_is_convergent_&_lim_((||.h.||_")_(#)_((R1_+_R2)_/*_h))_=_0._T_)
let h be non-zero 0. S -convergent sequence of S; ::_thesis: ( (||.h.|| ") (#) ((R1 + R2) /* h) is convergent & lim ((||.h.|| ") (#) ((R1 + R2) /* h)) = 0. T )
A3: ( (||.h.|| ") (#) (R1 /* h) is convergent & (||.h.|| ") (#) (R2 /* h) is convergent ) by Def5;
A4: (||.h.|| ") (#) ((R1 + R2) /* h) = (||.h.|| ") (#) ((R1 /* h) + (R2 /* h)) by A1, Th25
.= ((||.h.|| ") (#) (R1 /* h)) + ((||.h.|| ") (#) (R2 /* h)) by Th9 ;
hence (||.h.|| ") (#) ((R1 + R2) /* h) is convergent by A3, NORMSP_1:19; ::_thesis: lim ((||.h.|| ") (#) ((R1 + R2) /* h)) = 0. T
( lim ((||.h.|| ") (#) (R1 /* h)) = 0. T & lim ((||.h.|| ") (#) (R2 /* h)) = 0. T ) by Def5;
hence lim ((||.h.|| ") (#) ((R1 + R2) /* h)) = (0. T) + (0. T) by A3, A4, NORMSP_1:25
.= 0. T by RLVECT_1:4 ;
::_thesis: verum
end;
A5: now__::_thesis:_for_h_being_non-zero_0._S_-convergent_sequence_of_S_holds_
(_(||.h.||_")_(#)_((R1_-_R2)_/*_h)_is_convergent_&_lim_((||.h.||_")_(#)_((R1_-_R2)_/*_h))_=_0._T_)
let h be non-zero 0. S -convergent sequence of S; ::_thesis: ( (||.h.|| ") (#) ((R1 - R2) /* h) is convergent & lim ((||.h.|| ") (#) ((R1 - R2) /* h)) = 0. T )
A6: ( (||.h.|| ") (#) (R1 /* h) is convergent & (||.h.|| ") (#) (R2 /* h) is convergent ) by Def5;
A7: (||.h.|| ") (#) ((R1 - R2) /* h) = (||.h.|| ") (#) ((R1 /* h) - (R2 /* h)) by A1, Th25
.= ((||.h.|| ") (#) (R1 /* h)) - ((||.h.|| ") (#) (R2 /* h)) by Th12 ;
hence (||.h.|| ") (#) ((R1 - R2) /* h) is convergent by A6, NORMSP_1:20; ::_thesis: lim ((||.h.|| ") (#) ((R1 - R2) /* h)) = 0. T
( lim ((||.h.|| ") (#) (R1 /* h)) = 0. T & lim ((||.h.|| ") (#) (R2 /* h)) = 0. T ) by Def5;
hence lim ((||.h.|| ") (#) ((R1 - R2) /* h)) = (0. T) - (0. T) by A6, A7, NORMSP_1:26
.= 0. T by RLVECT_1:13 ;
::_thesis: verum
end;
R1 + R2 is total by A1, VFUNCT_1:32;
hence R1 + R2 is RestFunc of S,T by A2, Def5; ::_thesis: R1 - R2 is RestFunc of S,T
R1 - R2 is total by A1, VFUNCT_1:32;
hence R1 - R2 is RestFunc of S,T by A5, Def5; ::_thesis: verum
end;
theorem Th29: :: NDIFF_1:29
for T, S being non trivial RealNormSpace
for r being Real
for R being RestFunc of S,T holds r (#) R is RestFunc of S,T
proof
let T, S be non trivial RealNormSpace; ::_thesis: for r being Real
for R being RestFunc of S,T holds r (#) R is RestFunc of S,T
let r be Real; ::_thesis: for R being RestFunc of S,T holds r (#) R is RestFunc of S,T
let R be RestFunc of S,T; ::_thesis: r (#) R is RestFunc of S,T
A1: R is total by Def5;
A2: now__::_thesis:_for_h_being_non-zero_0._S_-convergent_sequence_of_S_holds_
(_(||.h.||_")_(#)_((r_(#)_R)_/*_h)_is_convergent_&_lim_((||.h.||_")_(#)_((r_(#)_R)_/*_h))_=_0._T_)
let h be non-zero 0. S -convergent sequence of S; ::_thesis: ( (||.h.|| ") (#) ((r (#) R) /* h) is convergent & lim ((||.h.|| ") (#) ((r (#) R) /* h)) = 0. T )
A3: (||.h.|| ") (#) (R /* h) is convergent by Def5;
A4: (||.h.|| ") (#) ((r (#) R) /* h) = (||.h.|| ") (#) (r * (R /* h)) by A1, Th26
.= r * ((||.h.|| ") (#) (R /* h)) by Th10 ;
hence (||.h.|| ") (#) ((r (#) R) /* h) is convergent by A3, NORMSP_1:22; ::_thesis: lim ((||.h.|| ") (#) ((r (#) R) /* h)) = 0. T
lim ((||.h.|| ") (#) (R /* h)) = 0. T by Def5;
hence lim ((||.h.|| ") (#) ((r (#) R) /* h)) = r * (0. T) by A3, A4, NORMSP_1:28
.= 0. T by RLVECT_1:10 ;
::_thesis: verum
end;
r (#) R is total by A1, VFUNCT_1:34;
hence r (#) R is RestFunc of S,T by A2, Def5; ::_thesis: verum
end;
definition
let S, T be non trivial RealNormSpace;
let f be PartFunc of S,T;
let x0 be Point of S;
predf is_differentiable_in x0 means :Def6: :: NDIFF_1:def 6
ex N being Neighbourhood of x0 st
( N c= dom f & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) );
end;
:: deftheorem Def6 defines is_differentiable_in NDIFF_1:def_6_:_
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for x0 being Point of S holds
( f is_differentiable_in x0 iff ex N being Neighbourhood of x0 st
( N c= dom f & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) );
definition
let S, T be non trivial RealNormSpace;
let f be PartFunc of S,T;
let x0 be Point of S;
assume A1: f is_differentiable_in x0 ;
func diff (f,x0) -> Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) means :Def7: :: NDIFF_1:def 7
ex N being Neighbourhood of x0 st
( N c= dom f & ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (it . (x - x0)) + (R /. (x - x0)) );
existence
ex b1 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex N being Neighbourhood of x0 st
( N c= dom f & ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (b1 . (x - x0)) + (R /. (x - x0)) )
proof
consider N being Neighbourhood of x0 such that
A2: N c= dom f and
A3: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A1, Def6;
consider L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R being RestFunc of S,T such that
A4: for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A3;
take L ; ::_thesis: ex N being Neighbourhood of x0 st
( N c= dom f & ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
thus ex N being Neighbourhood of x0 st
( N c= dom f & ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) by A2, A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) st ex N being Neighbourhood of x0 st
( N c= dom f & ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (b1 . (x - x0)) + (R /. (x - x0)) ) & ex N being Neighbourhood of x0 st
( N c= dom f & ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (b2 . (x - x0)) + (R /. (x - x0)) ) holds
b1 = b2
proof
let LB, LB1 be Point of (R_NormSpace_of_BoundedLinearOperators (S,T)); ::_thesis: ( ex N being Neighbourhood of x0 st
( N c= dom f & ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (LB . (x - x0)) + (R /. (x - x0)) ) & ex N being Neighbourhood of x0 st
( N c= dom f & ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (LB1 . (x - x0)) + (R /. (x - x0)) ) implies LB = LB1 )
A5: R_NormSpace_of_BoundedLinearOperators (S,T) = NORMSTR(# (BoundedLinearOperators (S,T)),(Zero_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(Add_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(Mult_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(BoundedLinearOperatorsNorm (S,T)) #) by LOPBAN_1:def_14;
then reconsider L = LB as Element of BoundedLinearOperators (S,T) ;
reconsider L1 = LB1 as Element of BoundedLinearOperators (S,T) by A5;
assume that
A6: ex N being Neighbourhood of x0 st
( N c= dom f & ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (LB . (x - x0)) + (R /. (x - x0)) ) and
A7: ex N being Neighbourhood of x0 st
( N c= dom f & ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (LB1 . (x - x0)) + (R /. (x - x0)) ) ; ::_thesis: LB = LB1
consider N being Neighbourhood of x0 such that
N c= dom f and
A8: ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (LB . (x - x0)) + (R /. (x - x0)) by A6;
consider R being RestFunc of S,T such that
A9: for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (LB . (x - x0)) + (R /. (x - x0)) by A8;
consider N1 being Neighbourhood of x0 such that
N1 c= dom f and
A10: ex R being RestFunc of S,T st
for x being Point of S st x in N1 holds
(f /. x) - (f /. x0) = (LB1 . (x - x0)) + (R /. (x - x0)) by A7;
consider R1 being RestFunc of S,T such that
A11: for x being Point of S st x in N1 holds
(f /. x) - (f /. x0) = (LB1 . (x - x0)) + (R1 /. (x - x0)) by A10;
A12: for z being Point of S holds (modetrans (L,S,T)) . z = (modetrans (L1,S,T)) . z
proof
let z be Point of S; ::_thesis: (modetrans (L,S,T)) . z = (modetrans (L1,S,T)) . z
now__::_thesis:_(_(_z_=_0._S_&_(modetrans_(L,S,T))_._z_=_(modetrans_(L1,S,T))_._z_)_or_(_z_<>_0._S_&_(modetrans_(L,S,T))_._z_=_(modetrans_(L1,S,T))_._z_)_)
percases ( z = 0. S or z <> 0. S ) ;
caseA13: z = 0. S ; ::_thesis: (modetrans (L,S,T)) . z = (modetrans (L1,S,T)) . z
hence (modetrans (L,S,T)) . z = (modetrans (L,S,T)) . (0 * z) by RLVECT_1:10
.= 0 * ((modetrans (L,S,T)) . z) by LOPBAN_1:def_5
.= 0. T by RLVECT_1:10
.= 0 * ((modetrans (L1,S,T)) . z) by RLVECT_1:10
.= (modetrans (L1,S,T)) . (0 * z) by LOPBAN_1:def_5
.= (modetrans (L1,S,T)) . z by A13, RLVECT_1:10 ;
::_thesis: verum
end;
caseA14: z <> 0. S ; ::_thesis: (modetrans (L,S,T)) . z = (modetrans (L1,S,T)) . z
consider N0 being Neighbourhood of x0 such that
A15: ( N0 c= N & N0 c= N1 ) by Th1;
consider g being Real such that
A16: 0 < g and
A17: { y where y is Point of S : ||.(y - x0).|| < g } c= N0 by NFCONT_1:def_1;
consider n0 being Element of NAT such that
A18: ||.z.|| / g < n0 by SEQ_4:3;
set n1 = n0 + 1;
A19: 0 <= n0 by NAT_1:2;
n0 <= n0 + 1 by NAT_1:11;
then ||.z.|| / g < n0 + 1 by A18, XXREAL_0:2;
then (||.z.|| / g) * g < (n0 + 1) * g by A16, XREAL_1:68;
then ||.z.|| < (n0 + 1) * g by A16, XCMPLX_1:87;
then A20: ||.z.|| / (n0 + 1) < g by A19, XREAL_1:83;
ex r being Real_Sequence st
( ( for n being Element of NAT holds
( r . n = 1 / (n + (n0 + 1)) & r . n > 0 & ((r . n) * z) + x0 in N0 ) ) & r is convergent & lim r = 0 )
proof
deffunc H1( Element of NAT ) -> Element of REAL = 1 / ($1 + (n0 + 1));
consider r being Real_Sequence such that
A21: for n being Element of NAT holds r . n = H1(n) from SEQ_1:sch_1();
take r ; ::_thesis: ( ( for n being Element of NAT holds
( r . n = 1 / (n + (n0 + 1)) & r . n > 0 & ((r . n) * z) + x0 in N0 ) ) & r is convergent & lim r = 0 )
thus for n being Element of NAT holds
( r . n = 1 / (n + (n0 + 1)) & r . n > 0 & ((r . n) * z) + x0 in N0 ) ::_thesis: ( r is convergent & lim r = 0 )
proof
let n be Element of NAT ; ::_thesis: ( r . n = 1 / (n + (n0 + 1)) & r . n > 0 & ((r . n) * z) + x0 in N0 )
thus r . n = 1 / (n + (n0 + 1)) by A21; ::_thesis: ( r . n > 0 & ((r . n) * z) + x0 in N0 )
( n0 + 1 <= n + (n0 + 1) & 0 <= ||.z.|| ) by NAT_1:12, NORMSP_1:4;
then A22: ||.z.|| / (n + (n0 + 1)) <= ||.z.|| / (n0 + 1) by A19, XREAL_1:118;
0 <= n by NAT_1:2;
then 0 < 1 * ((n + (n0 + 1)) ") by A19;
then A23: 0 < 1 / (n + (n0 + 1)) by XCMPLX_0:def_9;
hence r . n > 0 by A21; ::_thesis: ((r . n) * z) + x0 in N0
||.((((r . n) * z) + x0) - x0).|| = ||.(((r . n) * z) + (x0 - x0)).|| by RLVECT_1:def_3
.= ||.(((r . n) * z) + (0. S)).|| by RLVECT_1:15
.= ||.((r . n) * z).|| by RLVECT_1:4
.= ||.((1 / (n + (n0 + 1))) * z).|| by A21
.= (abs (1 / (n + (n0 + 1)))) * ||.z.|| by NORMSP_1:def_1
.= (1 / (n + (n0 + 1))) * ||.z.|| by A23, ABSVALUE:def_1
.= ||.z.|| / (n + (n0 + 1)) by XCMPLX_1:99 ;
then ||.((((r . n) * z) + x0) - x0).|| < g by A20, A22, XXREAL_0:2;
then ((r . n) * z) + x0 in { y where y is Point of S : ||.(y - x0).|| < g } ;
hence ((r . n) * z) + x0 in N0 by A17; ::_thesis: verum
end;
thus r is convergent by A21, NAT_1:2, SEQ_4:28; ::_thesis: lim r = 0
thus lim r = 0 by A21, NAT_1:2, SEQ_4:29; ::_thesis: verum
end;
then consider r being Real_Sequence such that
A24: for n being Element of NAT holds
( r . n = 1 / (n + (n0 + 1)) & r . n > 0 & ((r . n) * z) + x0 in N0 ) and
r is convergent and
lim r = 0 ;
deffunc H1( Element of NAT ) -> Element of the carrier of S = (r . $1) * z;
consider s being sequence of S such that
A25: for n being Element of NAT holds s . n = H1(n) from FUNCT_2:sch_4();
now__::_thesis:_for_n_being_Element_of_NAT_holds_not_s_._n_=_0._S
let n be Element of NAT ; ::_thesis: not s . n = 0. S
assume s . n = 0. S ; ::_thesis: contradiction
then (r . n) * z = 0. S by A25;
then ( r . n = 0 or z = 0. S ) by RLVECT_1:11;
hence contradiction by A14, A24; ::_thesis: verum
end;
then A26: s is non-zero by Th7;
now__::_thesis:_for_n_being_Element_of_NAT_holds_s_._n_=_(1_/_(n_+_(n0_+_1)))_*_z
let n be Element of NAT ; ::_thesis: s . n = (1 / (n + (n0 + 1))) * z
thus s . n = (r . n) * z by A25
.= (1 / (n + (n0 + 1))) * z by A24 ; ::_thesis: verum
end;
then ( s is convergent & lim s = 0. S ) by A19, Th19, Th20;
then reconsider s = s as non-zero 0. S -convergent sequence of S by A26, Def4;
A27: now__::_thesis:_for_x_being_Point_of_S_st_x_in_N_&_x_in_N1_holds_
(L_._(x_-_x0))_+_(R_/._(x_-_x0))_=_(L1_._(x_-_x0))_+_(R1_/._(x_-_x0))
let x be Point of S; ::_thesis: ( x in N & x in N1 implies (L . (x - x0)) + (R /. (x - x0)) = (L1 . (x - x0)) + (R1 /. (x - x0)) )
assume that
A28: x in N and
A29: x in N1 ; ::_thesis: (L . (x - x0)) + (R /. (x - x0)) = (L1 . (x - x0)) + (R1 /. (x - x0))
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A9, A28;
hence (L . (x - x0)) + (R /. (x - x0)) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A11, A29; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Nat_holds_(L_._z)_-_(L1_._z)_=_(||.z.||_*_(((||.s.||_")_(#)_(R1_/*_s))_-_((||.s.||_")_(#)_(R_/*_s))))_._n
R1 is total by Def5;
then dom R1 = the carrier of S by PARTFUN1:def_2;
then A30: rng s c= dom R1 ;
R is total by Def5;
then dom R = the carrier of S by PARTFUN1:def_2;
then A31: rng s c= dom R ;
let n be Nat; ::_thesis: (L . z) - (L1 . z) = (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s)))) . n
set x = ((r . n) * z) + x0;
A32: (((r . n) * z) + x0) - x0 = ((r . n) * z) + (x0 - x0) by RLVECT_1:def_3
.= ((r . n) * z) + (0. S) by RLVECT_1:15
.= (r . n) * z by RLVECT_1:4 ;
A33: n in NAT by ORDINAL1:def_12;
then A34: r . n <> 0 by A24;
s . n <> 0. S by A33, Th7;
then A35: ||.(s . n).|| <> 0 by NORMSP_0:def_5;
A36: r . n > 0 by A24, A33;
||.(s . n).|| = ||.((r . n) * z).|| by A25, A33
.= (abs (r . n)) * ||.z.|| by NORMSP_1:def_1
.= (r . n) * ||.z.|| by A36, ABSVALUE:def_1 ;
then ((r . n) ") * ||.(s . n).|| = (((r . n) ") * (r . n)) * ||.z.||
.= ((r . n) / (r . n)) * ||.z.|| by XCMPLX_0:def_9
.= 1 * ||.z.|| by A34, XCMPLX_1:60
.= ||.z.|| ;
then ||.z.|| * (||.(s . n).|| ") = ((r . n) ") * (||.(s . n).|| * (||.(s . n).|| "))
.= ((r . n) ") * (||.(s . n).|| / ||.(s . n).||) by XCMPLX_0:def_9
.= ((r . n) ") * 1 by A35, XCMPLX_1:60
.= (r . n) " ;
then A37: ||.z.|| * ((||.s.|| . n) ") = (r . n) " by A33, NORMSP_0:def_4;
((r . n) * z) + x0 in N0 by A24, A33;
then (L . ((r . n) * z)) + (R /. ((r . n) * z)) = (L1 . ((r . n) * z)) + (R1 /. ((r . n) * z)) by A27, A15, A32;
then A38: (((r . n) ") * (L . ((r . n) * z))) + (((r . n) ") * (R /. ((r . n) * z))) = ((r . n) ") * ((L1 . ((r . n) * z)) + (R1 /. ((r . n) * z))) by RLVECT_1:def_5;
A39: ((r . n) ") * (L1 . ((r . n) * z)) = ((r . n) ") * ((modetrans (L1,S,T)) . ((r . n) * z)) by LOPBAN_1:def_11
.= ((r . n) ") * ((r . n) * ((modetrans (L1,S,T)) . z)) by LOPBAN_1:def_5
.= ((r . n) ") * ((r . n) * (L1 . z)) by LOPBAN_1:def_11
.= (((r . n) ") * (r . n)) * (L1 . z) by RLVECT_1:def_7
.= ((r . n) / (r . n)) * (L1 . z) by XCMPLX_0:def_9
.= 1 * (L1 . z) by A34, XCMPLX_1:60
.= L1 . z by RLVECT_1:def_8 ;
((r . n) ") * (L . ((r . n) * z)) = ((r . n) ") * ((modetrans (L,S,T)) . ((r . n) * z)) by LOPBAN_1:def_11
.= ((r . n) ") * ((r . n) * ((modetrans (L,S,T)) . z)) by LOPBAN_1:def_5
.= ((r . n) ") * ((r . n) * (L . z)) by LOPBAN_1:def_11
.= (((r . n) ") * (r . n)) * (L . z) by RLVECT_1:def_7
.= ((r . n) / (r . n)) * (L . z) by XCMPLX_0:def_9
.= 1 * (L . z) by A34, XCMPLX_1:60
.= L . z by RLVECT_1:def_8 ;
then A40: (L . z) + (((r . n) ") * (R /. ((r . n) * z))) = (L1 . z) + (((r . n) ") * (R1 /. ((r . n) * z))) by A38, A39, RLVECT_1:def_5;
A41: ((r . n) ") * (R1 /. ((r . n) * z)) = ((r . n) ") * (R1 /. (s . n)) by A25, A33
.= (||.z.|| * ((||.s.|| ") . n)) * (R1 /. (s . n)) by A37, VALUED_1:10
.= ||.z.|| * (((||.s.|| ") . n) * (R1 /. (s . n))) by RLVECT_1:def_7
.= ||.z.|| * (((||.s.|| ") . n) * ((R1 /* s) . n)) by A33, A30, FUNCT_2:109
.= ||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n) by A33, Def2 ;
((r . n) ") * (R /. ((r . n) * z)) = ((r . n) ") * (R /. (s . n)) by A25, A33
.= (||.z.|| * ((||.s.|| ") . n)) * (R /. (s . n)) by A37, VALUED_1:10
.= ||.z.|| * (((||.s.|| ") . n) * (R /. (s . n))) by RLVECT_1:def_7
.= ||.z.|| * (((||.s.|| ") . n) * ((R /* s) . n)) by A33, A31, FUNCT_2:109
.= ||.z.|| * (((||.s.|| ") (#) (R /* s)) . n) by A33, Def2 ;
then (L . z) + ((||.z.|| * (((||.s.|| ") (#) (R /* s)) . n)) - (||.z.|| * (((||.s.|| ") (#) (R /* s)) . n))) = ((L1 . z) + (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n))) - (||.z.|| * (((||.s.|| ") (#) (R /* s)) . n)) by A40, A41, RLVECT_1:def_3;
then (L . z) + (0. T) = ((L1 . z) + (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n))) - (||.z.|| * (((||.s.|| ") (#) (R /* s)) . n)) by RLVECT_1:15;
then L . z = ((L1 . z) + (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n))) - (||.z.|| * (((||.s.|| ") (#) (R /* s)) . n)) by RLVECT_1:def_4;
then (L . z) - (L1 . z) = (- (L1 . z)) + ((L1 . z) + ((||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n)) - (||.z.|| * (((||.s.|| ") (#) (R /* s)) . n)))) by RLVECT_1:def_3;
then (L . z) - (L1 . z) = ((- (L1 . z)) + (L1 . z)) + ((||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n)) - (||.z.|| * (((||.s.|| ") (#) (R /* s)) . n))) by RLVECT_1:def_3;
then (L . z) - (L1 . z) = (0. T) + ((||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n)) - (||.z.|| * (((||.s.|| ") (#) (R /* s)) . n))) by RLVECT_1:5;
then (L . z) - (L1 . z) = (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n)) - (||.z.|| * (((||.s.|| ") (#) (R /* s)) . n)) by RLVECT_1:4;
then (L . z) - (L1 . z) = ||.z.|| * ((((||.s.|| ") (#) (R1 /* s)) . n) - (((||.s.|| ") (#) (R /* s)) . n)) by RLVECT_1:34;
then (L . z) - (L1 . z) = ||.z.|| * ((((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s))) . n) by A33, NORMSP_1:def_3;
hence (L . z) - (L1 . z) = (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s)))) . n by A33, NORMSP_1:def_5; ::_thesis: verum
end;
then ( ||.z.|| * (((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s))) is constant & (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s)))) . 1 = (L . z) - (L1 . z) ) by VALUED_0:def_18;
then A42: lim (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s)))) = (L . z) - (L1 . z) by Th18;
A43: ( (||.s.|| ") (#) (R /* s) is convergent & (||.s.|| ") (#) (R1 /* s) is convergent ) by Def5;
( lim ((||.s.|| ") (#) (R /* s)) = 0. T & lim ((||.s.|| ") (#) (R1 /* s)) = 0. T ) by Def5;
then A44: lim (((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s))) = (0. T) - (0. T) by A43, NORMSP_1:26
.= 0. T by RLVECT_1:13 ;
A45: lim (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s)))) = ||.z.|| * (lim (((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s)))) by A43, NORMSP_1:20, NORMSP_1:28
.= 0. T by A44, RLVECT_1:10 ;
thus (modetrans (L,S,T)) . z = L . z by LOPBAN_1:def_11
.= L1 . z by A42, A45, RLVECT_1:21
.= (modetrans (L1,S,T)) . z by LOPBAN_1:def_11 ; ::_thesis: verum
end;
end;
end;
hence (modetrans (L,S,T)) . z = (modetrans (L1,S,T)) . z ; ::_thesis: verum
end;
thus LB = modetrans (L,S,T) by LOPBAN_1:def_11
.= modetrans (L1,S,T) by A12, FUNCT_2:63
.= LB1 by LOPBAN_1:def_11 ; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines diff NDIFF_1:def_7_:_
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for x0 being Point of S st f is_differentiable_in x0 holds
for b5 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) holds
( b5 = diff (f,x0) iff ex N being Neighbourhood of x0 st
( N c= dom f & ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (b5 . (x - x0)) + (R /. (x - x0)) ) );
definition
let X be set ;
let S, T be non trivial RealNormSpace;
let f be PartFunc of S,T;
predf is_differentiable_on X means :Def8: :: NDIFF_1:def 8
( X c= dom f & ( for x being Point of S st x in X holds
f | X is_differentiable_in x ) );
end;
:: deftheorem Def8 defines is_differentiable_on NDIFF_1:def_8_:_
for X being set
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T holds
( f is_differentiable_on X iff ( X c= dom f & ( for x being Point of S st x in X holds
f | X is_differentiable_in x ) ) );
theorem Th30: :: NDIFF_1:30
for X being set
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T st f is_differentiable_on X holds
X is Subset of S
proof
let X be set ; ::_thesis: for S, T being non trivial RealNormSpace
for f being PartFunc of S,T st f is_differentiable_on X holds
X is Subset of S
let S, T be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,T st f is_differentiable_on X holds
X is Subset of S
let f be PartFunc of S,T; ::_thesis: ( f is_differentiable_on X implies X is Subset of S )
assume f is_differentiable_on X ; ::_thesis: X is Subset of S
then X c= dom f by Def8;
hence X is Subset of S by XBOOLE_1:1; ::_thesis: verum
end;
theorem Th31: :: NDIFF_1:31
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S st Z is open holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds
f is_differentiable_in x ) ) )
proof
let S, T be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,T
for Z being Subset of S st Z is open holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds
f is_differentiable_in x ) ) )
let f be PartFunc of S,T; ::_thesis: for Z being Subset of S st Z is open holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds
f is_differentiable_in x ) ) )
let Z be Subset of S; ::_thesis: ( Z is open implies ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds
f is_differentiable_in x ) ) ) )
assume A1: Z is open ; ::_thesis: ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Point of S st x in Z holds
f is_differentiable_in x ) ) )
thus ( f is_differentiable_on Z implies ( Z c= dom f & ( for x being Point of S st x in Z holds
f is_differentiable_in x ) ) ) ::_thesis: ( Z c= dom f & ( for x being Point of S st x in Z holds
f is_differentiable_in x ) implies f is_differentiable_on Z )
proof
assume A2: f is_differentiable_on Z ; ::_thesis: ( Z c= dom f & ( for x being Point of S st x in Z holds
f is_differentiable_in x ) )
hence A3: Z c= dom f by Def8; ::_thesis: for x being Point of S st x in Z holds
f is_differentiable_in x
let x0 be Point of S; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A4: x0 in Z ; ::_thesis: f is_differentiable_in x0
then f | Z is_differentiable_in x0 by A2, Def8;
then consider N being Neighbourhood of x0 such that
A5: N c= dom (f | Z) and
A6: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def6;
consider L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R being RestFunc of S,T such that
A7: for x being Point of S st x in N holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A6;
take N ; :: according to NDIFF_1:def_6 ::_thesis: ( N c= dom f & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A8: dom (f | Z) = (dom f) /\ Z by RELAT_1:61;
then dom (f | Z) c= dom f by XBOOLE_1:17;
hence N c= dom f by A5, XBOOLE_1:1; ::_thesis: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
take L ; ::_thesis: ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
take R ; ::_thesis: for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
let x be Point of S; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
assume A9: x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
then ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A7;
then (f /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A5, A8, A9, PARTFUN2:16;
hence (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A3, A4, PARTFUN2:17; ::_thesis: verum
end;
assume that
A10: Z c= dom f and
A11: for x being Point of S st x in Z holds
f is_differentiable_in x ; ::_thesis: f is_differentiable_on Z
thus Z c= dom f by A10; :: according to NDIFF_1:def_8 ::_thesis: for x being Point of S st x in Z holds
f | Z is_differentiable_in x
let x0 be Point of S; ::_thesis: ( x0 in Z implies f | Z is_differentiable_in x0 )
assume A12: x0 in Z ; ::_thesis: f | Z is_differentiable_in x0
then consider N1 being Neighbourhood of x0 such that
A13: N1 c= Z by A1, Th2;
f is_differentiable_in x0 by A11, A12;
then consider N being Neighbourhood of x0 such that
A14: N c= dom f and
A15: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def6;
consider N2 being Neighbourhood of x0 such that
A16: N2 c= N1 and
A17: N2 c= N by Th1;
A18: N2 c= Z by A13, A16, XBOOLE_1:1;
take N2 ; :: according to NDIFF_1:def_6 ::_thesis: ( N2 c= dom (f | Z) & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N2 holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
N2 c= dom f by A14, A17, XBOOLE_1:1;
then A19: N2 c= (dom f) /\ Z by A18, XBOOLE_1:19;
hence N2 c= dom (f | Z) by RELAT_1:61; ::_thesis: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N2 holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
A20: x0 in N2 by NFCONT_1:4;
consider L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R being RestFunc of S,T such that
A21: for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A15;
take L ; ::_thesis: ex R being RestFunc of S,T st
for x being Point of S st x in N2 holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
take R ; ::_thesis: for x being Point of S st x in N2 holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
let x be Point of S; ::_thesis: ( x in N2 implies ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
assume A22: x in N2 ; ::_thesis: ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
then (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A17, A21;
then ((f | Z) /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A19, A22, PARTFUN2:16;
hence ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A19, A20, PARTFUN2:16; ::_thesis: verum
end;
theorem :: NDIFF_1:32
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for Y being Subset of S st f is_differentiable_on Y holds
Y is open
proof
let S, T be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,T
for Y being Subset of S st f is_differentiable_on Y holds
Y is open
let f be PartFunc of S,T; ::_thesis: for Y being Subset of S st f is_differentiable_on Y holds
Y is open
let Y be Subset of S; ::_thesis: ( f is_differentiable_on Y implies Y is open )
assume A1: f is_differentiable_on Y ; ::_thesis: Y is open
now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_Y_holds_
ex_N_being_Neighbourhood_of_x0_st_N_c=_Y
let x0 be Point of S; ::_thesis: ( x0 in Y implies ex N being Neighbourhood of x0 st N c= Y )
assume x0 in Y ; ::_thesis: ex N being Neighbourhood of x0 st N c= Y
then f | Y is_differentiable_in x0 by A1, Def8;
then consider N being Neighbourhood of x0 such that
A2: N c= dom (f | Y) and
ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N holds
((f | Y) /. x) - ((f | Y) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def6;
take N = N; ::_thesis: N c= Y
dom (f | Y) = (dom f) /\ Y by RELAT_1:61;
then dom (f | Y) c= Y by XBOOLE_1:17;
hence N c= Y by A2, XBOOLE_1:1; ::_thesis: verum
end;
hence Y is open by Th4; ::_thesis: verum
end;
definition
let S, T be non trivial RealNormSpace;
let f be PartFunc of S,T;
let X be set ;
assume A1: f is_differentiable_on X ;
funcf `| X -> PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)) means :Def9: :: NDIFF_1:def 9
( dom it = X & ( for x being Point of S st x in X holds
it /. x = diff (f,x) ) );
existence
ex b1 being PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)) st
( dom b1 = X & ( for x being Point of S st x in X holds
b1 /. x = diff (f,x) ) )
proof
deffunc H1( Point of S) -> Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) = diff (f,$1);
defpred S1[ Point of S] means $1 in X;
consider F being PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)) such that
A2: ( ( for x being Point of S holds
( x in dom F iff S1[x] ) ) & ( for x being Point of S st x in dom F holds
F . x = H1(x) ) ) from SEQ_1:sch_3();
take F ; ::_thesis: ( dom F = X & ( for x being Point of S st x in X holds
F /. x = diff (f,x) ) )
now__::_thesis:_for_y_being_set_st_y_in_X_holds_
y_in_dom_F
A3: X is Subset of S by A1, Th30;
let y be set ; ::_thesis: ( y in X implies y in dom F )
assume y in X ; ::_thesis: y in dom F
hence y in dom F by A2, A3; ::_thesis: verum
end;
then A4: X c= dom F by TARSKI:def_3;
for y being set st y in dom F holds
y in X by A2;
then dom F c= X by TARSKI:def_3;
hence dom F = X by A4, XBOOLE_0:def_10; ::_thesis: for x being Point of S st x in X holds
F /. x = diff (f,x)
now__::_thesis:_for_x_being_Point_of_S_st_x_in_X_holds_
F_/._x_=_diff_(f,x)
let x be Point of S; ::_thesis: ( x in X implies F /. x = diff (f,x) )
assume x in X ; ::_thesis: F /. x = diff (f,x)
then A5: x in dom F by A2;
then F . x = diff (f,x) by A2;
hence F /. x = diff (f,x) by A5, PARTFUN1:def_6; ::_thesis: verum
end;
hence for x being Point of S st x in X holds
F /. x = diff (f,x) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)) st dom b1 = X & ( for x being Point of S st x in X holds
b1 /. x = diff (f,x) ) & dom b2 = X & ( for x being Point of S st x in X holds
b2 /. x = diff (f,x) ) holds
b1 = b2
proof
let F, G be PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)); ::_thesis: ( dom F = X & ( for x being Point of S st x in X holds
F /. x = diff (f,x) ) & dom G = X & ( for x being Point of S st x in X holds
G /. x = diff (f,x) ) implies F = G )
assume that
A6: dom F = X and
A7: for x being Point of S st x in X holds
F /. x = diff (f,x) and
A8: dom G = X and
A9: for x being Point of S st x in X holds
G /. x = diff (f,x) ; ::_thesis: F = G
now__::_thesis:_for_x_being_Point_of_S_st_x_in_dom_F_holds_
F_/._x_=_G_/._x
let x be Point of S; ::_thesis: ( x in dom F implies F /. x = G /. x )
assume A10: x in dom F ; ::_thesis: F /. x = G /. x
then F /. x = diff (f,x) by A6, A7;
hence F /. x = G /. x by A6, A9, A10; ::_thesis: verum
end;
hence F = G by A6, A8, PARTFUN2:1; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines `| NDIFF_1:def_9_:_
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for X being set st f is_differentiable_on X holds
for b5 being PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)) holds
( b5 = f `| X iff ( dom b5 = X & ( for x being Point of S st x in X holds
b5 /. x = diff (f,x) ) ) );
theorem :: NDIFF_1:33
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S st Z is open & Z c= dom f & ex r being Point of T st rng f = {r} holds
( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) )
proof
let S, T be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,T
for Z being Subset of S st Z is open & Z c= dom f & ex r being Point of T st rng f = {r} holds
( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) )
let f be PartFunc of S,T; ::_thesis: for Z being Subset of S st Z is open & Z c= dom f & ex r being Point of T st rng f = {r} holds
( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) )
let Z be Subset of S; ::_thesis: ( Z is open & Z c= dom f & ex r being Point of T st rng f = {r} implies ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) ) )
assume that
A1: Z is open and
A2: Z c= dom f ; ::_thesis: ( for r being Point of T holds not rng f = {r} or ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) ) )
reconsider R = the carrier of S --> (0. T) as PartFunc of S,T ;
set L = 0. (R_NormSpace_of_BoundedLinearOperators (S,T));
given r being Point of T such that A3: rng f = {r} ; ::_thesis: ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) )
R_NormSpace_of_BoundedLinearOperators (S,T) = NORMSTR(# (BoundedLinearOperators (S,T)),(Zero_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(Add_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(Mult_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(BoundedLinearOperatorsNorm (S,T)) #) by LOPBAN_1:def_14;
then reconsider L = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) as Element of BoundedLinearOperators (S,T) ;
A4: dom R = the carrier of S by FUNCOP_1:13;
A5: now__::_thesis:_for_h_being_non-zero_0._S_-convergent_sequence_of_S_holds_
(_(||.h.||_")_(#)_(R_/*_h)_is_convergent_&_lim_((||.h.||_")_(#)_(R_/*_h))_=_0._T_)
let h be non-zero 0. S -convergent sequence of S; ::_thesis: ( (||.h.|| ") (#) (R /* h) is convergent & lim ((||.h.|| ") (#) (R /* h)) = 0. T )
A6: now__::_thesis:_for_n_being_Nat_holds_((||.h.||_")_(#)_(R_/*_h))_._n_=_0._T
let n be Nat; ::_thesis: ((||.h.|| ") (#) (R /* h)) . n = 0. T
A7: R /. (h . n) = R . (h . n) by A4, PARTFUN1:def_6
.= 0. T by FUNCOP_1:7 ;
A8: rng h c= dom R by A4;
A9: n in NAT by ORDINAL1:def_12;
hence ((||.h.|| ") (#) (R /* h)) . n = ((||.h.|| ") . n) * ((R /* h) . n) by Def2
.= ((||.h.|| ") . n) * (R /. (h . n)) by A9, A8, FUNCT_2:109
.= 0. T by A7, RLVECT_1:10 ;
::_thesis: verum
end;
then A10: (||.h.|| ") (#) (R /* h) is constant by VALUED_0:def_18;
hence (||.h.|| ") (#) (R /* h) is convergent by Th18; ::_thesis: lim ((||.h.|| ") (#) (R /* h)) = 0. T
((||.h.|| ") (#) (R /* h)) . 0 = 0. T by A6;
hence lim ((||.h.|| ") (#) (R /* h)) = 0. T by A10, Th18; ::_thesis: verum
end;
A11: now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_dom_f_holds_
f_/._x0_=_r
let x0 be Point of S; ::_thesis: ( x0 in dom f implies f /. x0 = r )
assume A12: x0 in dom f ; ::_thesis: f /. x0 = r
then f . x0 in {r} by A3, FUNCT_1:def_3;
then f /. x0 in {r} by A12, PARTFUN1:def_6;
hence f /. x0 = r by TARSKI:def_1; ::_thesis: verum
end;
reconsider R = R as RestFunc of S,T by A5, Def5;
A13: the carrier of S --> (0. T) = L by LOPBAN_1:31;
A14: now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_Z_holds_
f_is_differentiable_in_x0
let x0 be Point of S; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A15: x0 in Z ; ::_thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A16: N c= Z by A1, Th2;
A17: N c= dom f by A2, A16, XBOOLE_1:1;
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
proof
let x be Point of S; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A18: R /. (x - x0) = R . (x - x0) by A4, PARTFUN1:def_6
.= 0. T by FUNCOP_1:7 ;
assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = r - (f /. x0) by A11, A17
.= r - r by A2, A11, A15
.= 0. T by RLVECT_1:15
.= (0. T) + (0. T) by RLVECT_1:4
.= (L . (x - x0)) + (R /. (x - x0)) by A13, A18, FUNCOP_1:7 ;
::_thesis: verum
end;
hence f is_differentiable_in x0 by A17, Def6; ::_thesis: verum
end;
hence A19: f is_differentiable_on Z by A1, A2, Th31; ::_thesis: for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T))
let x0 be Point of S; ::_thesis: ( x0 in Z implies (f `| Z) /. x0 = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) )
assume A20: x0 in Z ; ::_thesis: (f `| Z) /. x0 = 0. (R_NormSpace_of_BoundedLinearOperators (S,T))
then A21: f is_differentiable_in x0 by A14;
then ex N being Neighbourhood of x0 st
( N c= dom f & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) by Def6;
then consider N being Neighbourhood of x0 such that
A22: N c= dom f ;
A23: for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
proof
let x be Point of S; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A24: R /. (x - x0) = R . (x - x0) by A4, PARTFUN1:def_6
.= 0. T by FUNCOP_1:7 ;
assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = r - (f /. x0) by A11, A22
.= r - r by A2, A11, A20
.= 0. T by RLVECT_1:15
.= (0. T) + (0. T) by RLVECT_1:4
.= (L . (x - x0)) + (R /. (x - x0)) by A13, A24, FUNCOP_1:7 ;
::_thesis: verum
end;
thus (f `| Z) /. x0 = diff (f,x0) by A19, A20, Def9
.= 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) by A21, A22, A23, Def7 ; ::_thesis: verum
end;
registration
let S be non trivial RealNormSpace;
let h be non-zero 0. S -convergent sequence of S;
let n be Element of NAT ;
clusterh ^\ n -> non-zero 0. S -convergent for sequence of S;
coherence
for b1 being sequence of S st b1 = h ^\ n holds
( b1 is 0. S -convergent & b1 is non-zero )
proof
A1: h ^\ n is non-zero by Th17;
A2: h is convergent by Def4;
lim h = 0. S by Def4;
then A3: lim (h ^\ n) = 0. S by A2, LOPBAN_3:9;
h ^\ n is convergent by A2, LOPBAN_3:9;
hence for b1 being sequence of S st b1 = h ^\ n holds
( b1 is 0. S -convergent & b1 is non-zero ) by A1, A3, Def4; ::_thesis: verum
end;
end;
theorem Th34: :: NDIFF_1:34
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for x0 being Point of S
for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds
for h being non-zero 0. b1 -convergent sequence of S
for c being constant sequence of S st rng c = {x0} & rng (h + c) c= N holds
( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T )
proof
let S, T be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,T
for x0 being Point of S
for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds
for h being non-zero 0. S -convergent sequence of S
for c being constant sequence of S st rng c = {x0} & rng (h + c) c= N holds
( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T )
let f be PartFunc of S,T; ::_thesis: for x0 being Point of S
for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds
for h being non-zero 0. S -convergent sequence of S
for c being constant sequence of S st rng c = {x0} & rng (h + c) c= N holds
( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T )
let x0 be Point of S; ::_thesis: for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds
for h being non-zero 0. S -convergent sequence of S
for c being constant sequence of S st rng c = {x0} & rng (h + c) c= N holds
( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T )
let N be Neighbourhood of x0; ::_thesis: ( f is_differentiable_in x0 & N c= dom f implies for h being non-zero 0. S -convergent sequence of S
for c being constant sequence of S st rng c = {x0} & rng (h + c) c= N holds
( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T ) )
assume that
A1: f is_differentiable_in x0 and
A2: N c= dom f ; ::_thesis: for h being non-zero 0. S -convergent sequence of S
for c being constant sequence of S st rng c = {x0} & rng (h + c) c= N holds
( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T )
let h be non-zero 0. S -convergent sequence of S; ::_thesis: for c being constant sequence of S st rng c = {x0} & rng (h + c) c= N holds
( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T )
let c be constant sequence of S; ::_thesis: ( rng c = {x0} & rng (h + c) c= N implies ( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T ) )
assume that
A3: rng c = {x0} and
A4: rng (h + c) c= N ; ::_thesis: ( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T )
consider N1 being Neighbourhood of x0 such that
N1 c= dom f and
A5: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N1 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A1, Def6;
consider N2 being Neighbourhood of x0 such that
A6: N2 c= N and
A7: N2 c= N1 by Th1;
consider L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R being RestFunc of S,T such that
A8: for x being Point of S st x in N1 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A5;
consider g being Real such that
A9: 0 < g and
A10: { y where y is Point of S : ||.(y - x0).|| < g } c= N2 by NFCONT_1:def_1;
A11: x0 in N2 by NFCONT_1:4;
ex n being Element of NAT st
( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )
proof
c . 0 in rng c by NFCONT_1:6;
then c . 0 = x0 by A3, TARSKI:def_1;
then A12: lim c = x0 by Th18;
A13: ( c is convergent & h is convergent ) by Def4, Th18;
then A14: h + c is convergent by NORMSP_1:19;
lim h = 0. S by Def4;
then lim (h + c) = (0. S) + x0 by A12, A13, NORMSP_1:25
.= x0 by RLVECT_1:4 ;
then consider n being Element of NAT such that
A15: for m being Element of NAT st n <= m holds
||.(((h + c) . m) - x0).|| < g by A9, A14, NORMSP_1:def_7;
take n ; ::_thesis: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )
A16: rng (c ^\ n) = {x0} by A3, VALUED_0:26;
thus rng (c ^\ n) c= N2 ::_thesis: rng ((h + c) ^\ n) c= N2
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (c ^\ n) or y in N2 )
assume y in rng (c ^\ n) ; ::_thesis: y in N2
hence y in N2 by A11, A16, TARSKI:def_1; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((h + c) ^\ n) or y in N2 )
assume y in rng ((h + c) ^\ n) ; ::_thesis: y in N2
then consider m being Element of NAT such that
A17: y = ((h + c) ^\ n) . m by NFCONT_1:6;
reconsider y1 = y as Point of S by A17;
0 <= m by NAT_1:2;
then n + 0 <= n + m by XREAL_1:7;
then ||.(((h + c) . (n + m)) - x0).|| < g by A15;
then ||.((((h + c) ^\ n) . m) - x0).|| < g by NAT_1:def_3;
then y1 in { z where z is Point of S : ||.(z - x0).|| < g } by A17;
hence y in N2 by A10; ::_thesis: verum
end;
then consider n being Element of NAT such that
rng (c ^\ n) c= N2 and
A18: rng ((h + c) ^\ n) c= N2 ;
A19: lim (h ^\ n) = 0. S by Def4;
A20: for k being Element of NAT holds (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k))
proof
let k be Element of NAT ; ::_thesis: (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k))
((h + c) ^\ n) . k in rng ((h + c) ^\ n) by NFCONT_1:6;
then A21: ((h + c) ^\ n) . k in N2 by A18;
( (c ^\ n) . k in rng (c ^\ n) & rng (c ^\ n) = rng c ) by NFCONT_1:6, VALUED_0:26;
then A22: (c ^\ n) . k = x0 by A3, TARSKI:def_1;
(((h + c) ^\ n) . k) - ((c ^\ n) . k) = ((h + c) . (k + n)) - ((c ^\ n) . k) by NAT_1:def_3
.= ((h . (k + n)) + (c . (k + n))) - ((c ^\ n) . k) by NORMSP_1:def_2
.= (((h ^\ n) . k) + (c . (k + n))) - ((c ^\ n) . k) by NAT_1:def_3
.= (((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k) by NAT_1:def_3
.= ((h ^\ n) . k) + (((c ^\ n) . k) - ((c ^\ n) . k)) by RLVECT_1:def_3
.= ((h ^\ n) . k) + (0. S) by RLVECT_1:15
.= (h ^\ n) . k by RLVECT_1:4 ;
hence (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A8, A7, A21, A22; ::_thesis: verum
end;
R_NormSpace_of_BoundedLinearOperators (S,T) = NORMSTR(# (BoundedLinearOperators (S,T)),(Zero_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(Add_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(Mult_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(BoundedLinearOperatorsNorm (S,T)) #) by LOPBAN_1:def_14;
then reconsider L = L as Element of BoundedLinearOperators (S,T) ;
reconsider LP = modetrans (L,S,T) as PartFunc of S,T ;
A23: lim (R /* (h ^\ n)) = 0. T by Th24;
A24: rng ((h + c) ^\ n) c= dom f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((h + c) ^\ n) or y in dom f )
assume y in rng ((h + c) ^\ n) ; ::_thesis: y in dom f
then y in N2 by A18;
then y in N by A6;
hence y in dom f by A2; ::_thesis: verum
end;
R is total by Def5;
then dom R = the carrier of S by PARTFUN1:def_2;
then A25: rng (h ^\ n) c= dom R ;
A26: rng (c ^\ n) c= dom f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (c ^\ n) or y in dom f )
assume A27: y in rng (c ^\ n) ; ::_thesis: y in dom f
rng (c ^\ n) = rng c by VALUED_0:26;
then y = x0 by A3, A27, TARSKI:def_1;
then y in N by NFCONT_1:4;
hence y in dom f by A2; ::_thesis: verum
end;
A28: dom (modetrans (L,S,T)) = the carrier of S by FUNCT_2:def_1;
then A29: rng (h ^\ n) c= dom (modetrans (L,S,T)) ;
now__::_thesis:_for_k_being_Element_of_NAT_holds_((f_/*_((h_+_c)_^\_n))_-_(f_/*_(c_^\_n)))_._k_=_((LP_/*_(h_^\_n))_+_(R_/*_(h_^\_n)))_._k
let k be Element of NAT ; ::_thesis: ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((LP /* (h ^\ n)) + (R /* (h ^\ n))) . k
thus ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((f /* ((h + c) ^\ n)) . k) - ((f /* (c ^\ n)) . k) by NORMSP_1:def_3
.= (f /. (((h + c) ^\ n) . k)) - ((f /* (c ^\ n)) . k) by A24, FUNCT_2:109
.= (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) by A26, FUNCT_2:109
.= (L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A20
.= ((modetrans (L,S,T)) . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by LOPBAN_1:def_11
.= (LP /. ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A28, PARTFUN1:def_6
.= ((LP /* (h ^\ n)) . k) + (R /. ((h ^\ n) . k)) by A29, FUNCT_2:109
.= ((LP /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by A25, FUNCT_2:109
.= ((LP /* (h ^\ n)) + (R /* (h ^\ n))) . k by NORMSP_1:def_2 ; ::_thesis: verum
end;
then A30: (f /* ((h + c) ^\ n)) - (f /* (c ^\ n)) = (LP /* (h ^\ n)) + (R /* (h ^\ n)) by FUNCT_2:63;
A31: dom (modetrans (L,S,T)) = the carrier of S by FUNCT_2:def_1;
LP is_Lipschitzian_on the carrier of S
proof
thus the carrier of S c= dom LP by FUNCT_2:def_1; :: according to NFCONT_1:def_9 ::_thesis: ex b1 being Element of REAL st
( not b1 <= 0 & ( for b2, b3 being Element of the carrier of S holds
( not b2 in the carrier of S or not b3 in the carrier of S or ||.((LP /. b2) - (LP /. b3)).|| <= b1 * ||.(b2 - b3).|| ) ) )
set LL = modetrans (L,S,T);
consider K being Real such that
A32: 0 <= K and
A33: for x being VECTOR of S holds ||.((modetrans (L,S,T)) . x).|| <= K * ||.x.|| by LOPBAN_1:def_8;
take K + 1 ; ::_thesis: ( not K + 1 <= 0 & ( for b1, b2 being Element of the carrier of S holds
( not b1 in the carrier of S or not b2 in the carrier of S or ||.((LP /. b1) - (LP /. b2)).|| <= (K + 1) * ||.(b1 - b2).|| ) ) )
A34: 0 + K < 1 + K by XREAL_1:8;
now__::_thesis:_for_x1,_x2_being_Point_of_S_st_x1_in_the_carrier_of_S_&_x2_in_the_carrier_of_S_holds_
||.((LP_/._x1)_-_(LP_/._x2)).||_<=_(K_+_1)_*_||.(x1_-_x2).||
let x1, x2 be Point of S; ::_thesis: ( x1 in the carrier of S & x2 in the carrier of S implies ||.((LP /. x1) - (LP /. x2)).|| <= (K + 1) * ||.(x1 - x2).|| )
assume that
x1 in the carrier of S and
x2 in the carrier of S ; ::_thesis: ||.((LP /. x1) - (LP /. x2)).|| <= (K + 1) * ||.(x1 - x2).||
A35: ||.((modetrans (L,S,T)) . (x1 - x2)).|| <= K * ||.(x1 - x2).|| by A33;
0 <= ||.(x1 - x2).|| by NORMSP_1:4;
then A36: K * ||.(x1 - x2).|| <= (K + 1) * ||.(x1 - x2).|| by A34, XREAL_1:64;
||.((LP /. x1) - (LP /. x2)).|| = ||.(((modetrans (L,S,T)) . x1) - (LP /. x2)).|| by A31, PARTFUN1:def_6
.= ||.(((modetrans (L,S,T)) . x1) + (- ((modetrans (L,S,T)) . x2))).|| by A31, PARTFUN1:def_6
.= ||.(((modetrans (L,S,T)) . x1) + ((- 1) * ((modetrans (L,S,T)) . x2))).|| by RLVECT_1:16
.= ||.(((modetrans (L,S,T)) . x1) + ((modetrans (L,S,T)) . ((- 1) * x2))).|| by LOPBAN_1:def_5
.= ||.((modetrans (L,S,T)) . (x1 + ((- 1) * x2))).|| by VECTSP_1:def_20
.= ||.((modetrans (L,S,T)) . (x1 - x2)).|| by RLVECT_1:16 ;
hence ||.((LP /. x1) - (LP /. x2)).|| <= (K + 1) * ||.(x1 - x2).|| by A35, A36, XXREAL_0:2; ::_thesis: verum
end;
hence ( not K + 1 <= 0 & ( for b1, b2 being Element of the carrier of S holds
( not b1 in the carrier of S or not b2 in the carrier of S or ||.((LP /. b1) - (LP /. b2)).|| <= (K + 1) * ||.(b1 - b2).|| ) ) ) by A32; ::_thesis: verum
end;
then A37: LP is_continuous_on the carrier of S by NFCONT_1:45;
A38: rng c c= dom f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng c or y in dom f )
assume y in rng c ; ::_thesis: y in dom f
then y = x0 by A3, TARSKI:def_1;
then y in N by NFCONT_1:4;
hence y in dom f by A2; ::_thesis: verum
end;
A39: ( h ^\ n is convergent & rng (h ^\ n) c= the carrier of S ) by Def4;
then A40: LP /* (h ^\ n) is convergent by A37, A19, NFCONT_1:18;
A41: R /* (h ^\ n) is convergent by Th24;
then A42: (LP /* (h ^\ n)) + (R /* (h ^\ n)) is convergent by A40, NORMSP_1:19;
LP /. (0. S) = (modetrans (L,S,T)) . (0. S) by A31, PARTFUN1:def_6
.= (modetrans (L,S,T)) . (0 * (0. S)) by RLVECT_1:10
.= 0 * ((modetrans (L,S,T)) . (0. S)) by LOPBAN_1:def_5
.= 0. T by RLVECT_1:10 ;
then lim (LP /* (h ^\ n)) = 0. T by A37, A39, A19, NFCONT_1:18;
then lim ((LP /* (h ^\ n)) + (R /* (h ^\ n))) = (0. T) + (0. T) by A41, A23, A40, NORMSP_1:25;
then A43: lim ((LP /* (h ^\ n)) + (R /* (h ^\ n))) = 0. T by RLVECT_1:4;
rng (h + c) c= dom f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (h + c) or y in dom f )
assume y in rng (h + c) ; ::_thesis: y in dom f
then y in N by A4;
hence y in dom f by A2; ::_thesis: verum
end;
then (f /* ((h + c) ^\ n)) - (f /* (c ^\ n)) = ((f /* (h + c)) ^\ n) - (f /* (c ^\ n)) by VALUED_0:27
.= ((f /* (h + c)) ^\ n) - ((f /* c) ^\ n) by A38, VALUED_0:27
.= ((f /* (h + c)) - (f /* c)) ^\ n by Th16 ;
hence ( (f /* (h + c)) - (f /* c) is convergent & lim ((f /* (h + c)) - (f /* c)) = 0. T ) by A30, A42, A43, LOPBAN_3:10, LOPBAN_3:11; ::_thesis: verum
end;
theorem Th35: :: NDIFF_1:35
for T, S being non trivial RealNormSpace
for f1, f2 being PartFunc of S,T
for x0 being Point of S st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )
proof
let T, S be non trivial RealNormSpace; ::_thesis: for f1, f2 being PartFunc of S,T
for x0 being Point of S st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )
let f1, f2 be PartFunc of S,T; ::_thesis: for x0 being Point of S st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )
let x0 be Point of S; ::_thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) )
assume that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in x0 ; ::_thesis: ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )
consider N1 being Neighbourhood of x0 such that
A3: N1 c= dom f1 and
A4: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A1, Def6;
consider L1 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R1 being RestFunc of S,T such that
A5: for x being Point of S st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A4;
consider N2 being Neighbourhood of x0 such that
A6: N2 c= dom f2 and
A7: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A2, Def6;
consider L2 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R2 being RestFunc of S,T such that
A8: for x being Point of S st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L2 . (x - x0)) + (R2 /. (x - x0)) by A7;
reconsider R = R1 + R2 as RestFunc of S,T by Th28;
set L = L1 + L2;
consider N being Neighbourhood of x0 such that
A9: N c= N1 and
A10: N c= N2 by Th1;
A11: N c= dom f2 by A6, A10, XBOOLE_1:1;
N c= dom f1 by A3, A9, XBOOLE_1:1;
then N /\ N c= (dom f1) /\ (dom f2) by A11, XBOOLE_1:27;
then A12: N c= dom (f1 + f2) by VFUNCT_1:def_1;
A13: ( R1 is total & R2 is total ) by Def5;
A14: now__::_thesis:_for_x_being_Point_of_S_st_x_in_N_holds_
((f1_+_f2)_/._x)_-_((f1_+_f2)_/._x0)_=_((L1_+_L2)_._(x_-_x0))_+_(R_/._(x_-_x0))
let x be Point of S; ::_thesis: ( x in N implies ((f1 + f2) /. x) - ((f1 + f2) /. x0) = ((L1 + L2) . (x - x0)) + (R /. (x - x0)) )
A15: x0 in N by NFCONT_1:4;
assume A16: x in N ; ::_thesis: ((f1 + f2) /. x) - ((f1 + f2) /. x0) = ((L1 + L2) . (x - x0)) + (R /. (x - x0))
hence ((f1 + f2) /. x) - ((f1 + f2) /. x0) = ((f1 /. x) + (f2 /. x)) - ((f1 + f2) /. x0) by A12, VFUNCT_1:def_1
.= ((f1 /. x) + (f2 /. x)) - ((f1 /. x0) + (f2 /. x0)) by A12, A15, VFUNCT_1:def_1
.= (((f1 /. x) + (f2 /. x)) - (f1 /. x0)) - (f2 /. x0) by RLVECT_1:27
.= (((f1 /. x) + (- (f1 /. x0))) + (f2 /. x)) - (f2 /. x0) by RLVECT_1:def_3
.= ((f1 /. x) - (f1 /. x0)) + ((f2 /. x) - (f2 /. x0)) by RLVECT_1:def_3
.= ((L1 . (x - x0)) + (R1 /. (x - x0))) + ((f2 /. x) - (f2 /. x0)) by A5, A9, A16
.= ((L1 . (x - x0)) + (R1 /. (x - x0))) + ((L2 . (x - x0)) + (R2 /. (x - x0))) by A8, A10, A16
.= (((R1 /. (x - x0)) + (L1 . (x - x0))) + (L2 . (x - x0))) + (R2 /. (x - x0)) by RLVECT_1:def_3
.= (((L1 . (x - x0)) + (L2 . (x - x0))) + (R1 /. (x - x0))) + (R2 /. (x - x0)) by RLVECT_1:def_3
.= ((L1 . (x - x0)) + (L2 . (x - x0))) + ((R1 /. (x - x0)) + (R2 /. (x - x0))) by RLVECT_1:def_3
.= ((L1 + L2) . (x - x0)) + ((R1 /. (x - x0)) + (R2 /. (x - x0))) by LOPBAN_1:35
.= ((L1 + L2) . (x - x0)) + (R /. (x - x0)) by A13, VFUNCT_1:37 ;
::_thesis: verum
end;
hence f1 + f2 is_differentiable_in x0 by A12, Def6; ::_thesis: diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0))
hence diff ((f1 + f2),x0) = L1 + L2 by A12, A14, Def7
.= (diff (f1,x0)) + L2 by A1, A3, A5, Def7
.= (diff (f1,x0)) + (diff (f2,x0)) by A2, A6, A8, Def7 ;
::_thesis: verum
end;
theorem Th36: :: NDIFF_1:36
for T, S being non trivial RealNormSpace
for f1, f2 being PartFunc of S,T
for x0 being Point of S st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) )
proof
let T, S be non trivial RealNormSpace; ::_thesis: for f1, f2 being PartFunc of S,T
for x0 being Point of S st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) )
let f1, f2 be PartFunc of S,T; ::_thesis: for x0 being Point of S st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) )
let x0 be Point of S; ::_thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) )
assume that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in x0 ; ::_thesis: ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) )
consider N1 being Neighbourhood of x0 such that
A3: N1 c= dom f1 and
A4: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A1, Def6;
consider L1 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R1 being RestFunc of S,T such that
A5: for x being Point of S st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A4;
consider N2 being Neighbourhood of x0 such that
A6: N2 c= dom f2 and
A7: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A2, Def6;
consider L2 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R2 being RestFunc of S,T such that
A8: for x being Point of S st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L2 . (x - x0)) + (R2 /. (x - x0)) by A7;
reconsider R = R1 - R2 as RestFunc of S,T by Th28;
set L = L1 - L2;
consider N being Neighbourhood of x0 such that
A9: N c= N1 and
A10: N c= N2 by Th1;
A11: N c= dom f2 by A6, A10, XBOOLE_1:1;
N c= dom f1 by A3, A9, XBOOLE_1:1;
then N /\ N c= (dom f1) /\ (dom f2) by A11, XBOOLE_1:27;
then A12: N c= dom (f1 - f2) by VFUNCT_1:def_2;
A13: ( R1 is total & R2 is total ) by Def5;
A14: now__::_thesis:_for_x_being_Point_of_S_st_x_in_N_holds_
((f1_-_f2)_/._x)_-_((f1_-_f2)_/._x0)_=_((L1_-_L2)_._(x_-_x0))_+_(R_/._(x_-_x0))
let x be Point of S; ::_thesis: ( x in N implies ((f1 - f2) /. x) - ((f1 - f2) /. x0) = ((L1 - L2) . (x - x0)) + (R /. (x - x0)) )
A15: x0 in N by NFCONT_1:4;
assume A16: x in N ; ::_thesis: ((f1 - f2) /. x) - ((f1 - f2) /. x0) = ((L1 - L2) . (x - x0)) + (R /. (x - x0))
hence ((f1 - f2) /. x) - ((f1 - f2) /. x0) = ((f1 /. x) - (f2 /. x)) - ((f1 - f2) /. x0) by A12, VFUNCT_1:def_2
.= ((f1 /. x) - (f2 /. x)) - ((f1 /. x0) - (f2 /. x0)) by A12, A15, VFUNCT_1:def_2
.= (((f1 /. x) - (f2 /. x)) - (f1 /. x0)) + (f2 /. x0) by RLVECT_1:29
.= ((f1 /. x) - ((f1 /. x0) + (f2 /. x))) + (f2 /. x0) by RLVECT_1:27
.= (((f1 /. x) - (f1 /. x0)) - (f2 /. x)) + (f2 /. x0) by RLVECT_1:27
.= ((f1 /. x) - (f1 /. x0)) - ((f2 /. x) - (f2 /. x0)) by RLVECT_1:29
.= ((L1 . (x - x0)) + (R1 /. (x - x0))) - ((f2 /. x) - (f2 /. x0)) by A5, A9, A16
.= ((L1 . (x - x0)) + (R1 /. (x - x0))) - ((L2 . (x - x0)) + (R2 /. (x - x0))) by A8, A10, A16
.= (((L1 . (x - x0)) + (R1 /. (x - x0))) - (L2 . (x - x0))) - (R2 /. (x - x0)) by RLVECT_1:27
.= ((L1 . (x - x0)) + ((R1 /. (x - x0)) + (- (L2 . (x - x0))))) - (R2 /. (x - x0)) by RLVECT_1:def_3
.= ((L1 . (x - x0)) - ((L2 . (x - x0)) - (R1 /. (x - x0)))) - (R2 /. (x - x0)) by RLVECT_1:33
.= (((L1 . (x - x0)) - (L2 . (x - x0))) + (R1 /. (x - x0))) - (R2 /. (x - x0)) by RLVECT_1:29
.= ((L1 . (x - x0)) - (L2 . (x - x0))) + ((R1 /. (x - x0)) - (R2 /. (x - x0))) by RLVECT_1:def_3
.= ((L1 - L2) . (x - x0)) + ((R1 /. (x - x0)) - (R2 /. (x - x0))) by LOPBAN_1:40
.= ((L1 - L2) . (x - x0)) + (R /. (x - x0)) by A13, VFUNCT_1:37 ;
::_thesis: verum
end;
hence f1 - f2 is_differentiable_in x0 by A12, Def6; ::_thesis: diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0))
hence diff ((f1 - f2),x0) = L1 - L2 by A12, A14, Def7
.= (diff (f1,x0)) - L2 by A1, A3, A5, Def7
.= (diff (f1,x0)) - (diff (f2,x0)) by A2, A6, A8, Def7 ;
::_thesis: verum
end;
theorem Th37: :: NDIFF_1:37
for T, S being non trivial RealNormSpace
for r being Real
for f being PartFunc of S,T
for x0 being Point of S st f is_differentiable_in x0 holds
( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )
proof
let T, S be non trivial RealNormSpace; ::_thesis: for r being Real
for f being PartFunc of S,T
for x0 being Point of S st f is_differentiable_in x0 holds
( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )
let r be Real; ::_thesis: for f being PartFunc of S,T
for x0 being Point of S st f is_differentiable_in x0 holds
( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )
let f be PartFunc of S,T; ::_thesis: for x0 being Point of S st f is_differentiable_in x0 holds
( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )
let x0 be Point of S; ::_thesis: ( f is_differentiable_in x0 implies ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) ) )
assume A1: f is_differentiable_in x0 ; ::_thesis: ( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )
then consider N1 being Neighbourhood of x0 such that
A2: N1 c= dom f and
A3: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N1 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def6;
consider L1 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R1 being RestFunc of S,T such that
A4: for x being Point of S st x in N1 holds
(f /. x) - (f /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A3;
reconsider R = r (#) R1 as RestFunc of S,T by Th29;
set L = r * L1;
A5: N1 c= dom (r (#) f) by A2, VFUNCT_1:def_4;
A6: R1 is total by Def5;
A7: now__::_thesis:_for_x_being_Point_of_S_st_x_in_N1_holds_
((r_(#)_f)_/._x)_-_((r_(#)_f)_/._x0)_=_((r_*_L1)_._(x_-_x0))_+_(R_/._(x_-_x0))
let x be Point of S; ::_thesis: ( x in N1 implies ((r (#) f) /. x) - ((r (#) f) /. x0) = ((r * L1) . (x - x0)) + (R /. (x - x0)) )
A8: x0 in N1 by NFCONT_1:4;
assume A9: x in N1 ; ::_thesis: ((r (#) f) /. x) - ((r (#) f) /. x0) = ((r * L1) . (x - x0)) + (R /. (x - x0))
hence ((r (#) f) /. x) - ((r (#) f) /. x0) = (r * (f /. x)) - ((r (#) f) /. x0) by A5, VFUNCT_1:def_4
.= (r * (f /. x)) - (r * (f /. x0)) by A5, A8, VFUNCT_1:def_4
.= r * ((f /. x) - (f /. x0)) by RLVECT_1:34
.= r * ((L1 . (x - x0)) + (R1 /. (x - x0))) by A4, A9
.= (r * (L1 . (x - x0))) + (r * (R1 /. (x - x0))) by RLVECT_1:def_5
.= ((r * L1) . (x - x0)) + (r * (R1 /. (x - x0))) by LOPBAN_1:36
.= ((r * L1) . (x - x0)) + (R /. (x - x0)) by A6, VFUNCT_1:39 ;
::_thesis: verum
end;
hence r (#) f is_differentiable_in x0 by A5, Def6; ::_thesis: diff ((r (#) f),x0) = r * (diff (f,x0))
hence diff ((r (#) f),x0) = r * L1 by A5, A7, Def7
.= r * (diff (f,x0)) by A1, A2, A4, Def7 ;
::_thesis: verum
end;
theorem :: NDIFF_1:38
for S being non trivial RealNormSpace
for f being PartFunc of S,S
for Z being Subset of S st Z is open & Z c= dom f & f | Z = id Z holds
( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = id the carrier of S ) )
proof
let S be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,S
for Z being Subset of S st Z is open & Z c= dom f & f | Z = id Z holds
( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = id the carrier of S ) )
set L = id the carrier of S;
( R_NormSpace_of_BoundedLinearOperators (S,S) = NORMSTR(# (BoundedLinearOperators (S,S)),(Zero_ ((BoundedLinearOperators (S,S)),(R_VectorSpace_of_LinearOperators (S,S)))),(Add_ ((BoundedLinearOperators (S,S)),(R_VectorSpace_of_LinearOperators (S,S)))),(Mult_ ((BoundedLinearOperators (S,S)),(R_VectorSpace_of_LinearOperators (S,S)))),(BoundedLinearOperatorsNorm (S,S)) #) & id the carrier of S is Lipschitzian LinearOperator of S,S ) by LOPBAN_1:def_14, LOPBAN_2:3;
then reconsider L = id the carrier of S as Point of (R_NormSpace_of_BoundedLinearOperators (S,S)) by LOPBAN_1:def_9;
let f be PartFunc of S,S; ::_thesis: for Z being Subset of S st Z is open & Z c= dom f & f | Z = id Z holds
( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = id the carrier of S ) )
let Z be Subset of S; ::_thesis: ( Z is open & Z c= dom f & f | Z = id Z implies ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = id the carrier of S ) ) )
assume A1: Z is open ; ::_thesis: ( not Z c= dom f or not f | Z = id Z or ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = id the carrier of S ) ) )
reconsider R = the carrier of S --> (0. S) as PartFunc of S,S ;
A2: dom R = the carrier of S by FUNCOP_1:13;
now__::_thesis:_for_h_being_non-zero_0._S_-convergent_sequence_of_S_holds_
(_(||.h.||_")_(#)_(R_/*_h)_is_convergent_&_lim_((||.h.||_")_(#)_(R_/*_h))_=_0._S_)
let h be non-zero 0. S -convergent sequence of S; ::_thesis: ( (||.h.|| ") (#) (R /* h) is convergent & lim ((||.h.|| ") (#) (R /* h)) = 0. S )
A3: now__::_thesis:_for_n_being_Nat_holds_((||.h.||_")_(#)_(R_/*_h))_._n_=_0._S
let n be Nat; ::_thesis: ((||.h.|| ") (#) (R /* h)) . n = 0. S
A4: R /. (h . n) = R . (h . n) by A2, PARTFUN1:def_6
.= 0. S by FUNCOP_1:7 ;
A5: rng h c= dom R by A2;
A6: n in NAT by ORDINAL1:def_12;
hence ((||.h.|| ") (#) (R /* h)) . n = ((||.h.|| ") . n) * ((R /* h) . n) by Def2
.= ((||.h.|| ") . n) * (R /. (h . n)) by A6, A5, FUNCT_2:109
.= 0. S by A4, RLVECT_1:10 ;
::_thesis: verum
end;
then A7: (||.h.|| ") (#) (R /* h) is constant by VALUED_0:def_18;
hence (||.h.|| ") (#) (R /* h) is convergent by Th18; ::_thesis: lim ((||.h.|| ") (#) (R /* h)) = 0. S
((||.h.|| ") (#) (R /* h)) . 0 = 0. S by A3;
hence lim ((||.h.|| ") (#) (R /* h)) = 0. S by A7, Th18; ::_thesis: verum
end;
then reconsider R = R as RestFunc of S,S by Def5;
assume that
A8: Z c= dom f and
A9: f | Z = id Z ; ::_thesis: ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = id the carrier of S ) )
A10: now__::_thesis:_for_x_being_Point_of_S_st_x_in_Z_holds_
f_/._x_=_x
let x be Point of S; ::_thesis: ( x in Z implies f /. x = x )
assume A11: x in Z ; ::_thesis: f /. x = x
then (f | Z) . x = x by A9, FUNCT_1:18;
then f . x = x by A11, FUNCT_1:49;
hence f /. x = x by A8, A11, PARTFUN1:def_6; ::_thesis: verum
end;
A12: now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_Z_holds_
f_is_differentiable_in_x0
let x0 be Point of S; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A13: x0 in Z ; ::_thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A14: N c= Z by A1, Th2;
A15: for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
proof
let x be Point of S; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A16: R /. (x - x0) = R . (x - x0) by A2, PARTFUN1:def_6
.= 0. S by FUNCOP_1:7 ;
assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = x - (f /. x0) by A10, A14
.= x - x0 by A10, A13
.= L . (x - x0) by FUNCT_1:17
.= (L . (x - x0)) + (R /. (x - x0)) by A16, RLVECT_1:4 ;
::_thesis: verum
end;
N c= dom f by A8, A14, XBOOLE_1:1;
hence f is_differentiable_in x0 by A15, Def6; ::_thesis: verum
end;
hence A17: f is_differentiable_on Z by A1, A8, Th31; ::_thesis: for x being Point of S st x in Z holds
(f `| Z) /. x = id the carrier of S
let x0 be Point of S; ::_thesis: ( x0 in Z implies (f `| Z) /. x0 = id the carrier of S )
assume A18: x0 in Z ; ::_thesis: (f `| Z) /. x0 = id the carrier of S
then consider N1 being Neighbourhood of x0 such that
A19: N1 c= Z by A1, Th2;
A20: f is_differentiable_in x0 by A12, A18;
then ex N being Neighbourhood of x0 st
( N c= dom f & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,S)) ex R being RestFunc of S,S st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) by Def6;
then consider N being Neighbourhood of x0 such that
A21: N c= dom f ;
consider N2 being Neighbourhood of x0 such that
A22: N2 c= N1 and
A23: N2 c= N by Th1;
A24: N2 c= dom f by A21, A23, XBOOLE_1:1;
A25: for x being Point of S st x in N2 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
proof
let x be Point of S; ::_thesis: ( x in N2 implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A26: R /. (x - x0) = R . (x - x0) by A2, PARTFUN1:def_6
.= 0. S by FUNCOP_1:7 ;
assume x in N2 ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
then x in N1 by A22;
hence (f /. x) - (f /. x0) = x - (f /. x0) by A10, A19
.= x - x0 by A10, A18
.= L . (x - x0) by FUNCT_1:17
.= (L . (x - x0)) + (R /. (x - x0)) by A26, RLVECT_1:4 ;
::_thesis: verum
end;
thus (f `| Z) /. x0 = diff (f,x0) by A17, A18, Def9
.= id the carrier of S by A20, A24, A25, Def7 ; ::_thesis: verum
end;
theorem :: NDIFF_1:39
for S, T being non trivial RealNormSpace
for Z being Subset of S st Z is open holds
for f1, f2 being PartFunc of S,T st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 + f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds
((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) )
proof
let S, T be non trivial RealNormSpace; ::_thesis: for Z being Subset of S st Z is open holds
for f1, f2 being PartFunc of S,T st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 + f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds
((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) )
let Z be Subset of S; ::_thesis: ( Z is open implies for f1, f2 being PartFunc of S,T st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 + f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds
((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) ) )
assume A1: Z is open ; ::_thesis: for f1, f2 being PartFunc of S,T st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 + f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds
((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) )
let f1, f2 be PartFunc of S,T; ::_thesis: ( Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z implies ( f1 + f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds
((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) ) )
assume that
A2: Z c= dom (f1 + f2) and
A3: ( f1 is_differentiable_on Z & f2 is_differentiable_on Z ) ; ::_thesis: ( f1 + f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds
((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) )
now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_Z_holds_
f1_+_f2_is_differentiable_in_x0
let x0 be Point of S; ::_thesis: ( x0 in Z implies f1 + f2 is_differentiable_in x0 )
assume x0 in Z ; ::_thesis: f1 + f2 is_differentiable_in x0
then ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 ) by A1, A3, Th31;
hence f1 + f2 is_differentiable_in x0 by Th35; ::_thesis: verum
end;
hence A4: f1 + f2 is_differentiable_on Z by A1, A2, Th31; ::_thesis: for x being Point of S st x in Z holds
((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x))
now__::_thesis:_for_x_being_Point_of_S_st_x_in_Z_holds_
((f1_+_f2)_`|_Z)_/._x_=_(diff_(f1,x))_+_(diff_(f2,x))
let x be Point of S; ::_thesis: ( x in Z implies ((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) )
assume A5: x in Z ; ::_thesis: ((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x))
then A6: ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A1, A3, Th31;
thus ((f1 + f2) `| Z) /. x = diff ((f1 + f2),x) by A4, A5, Def9
.= (diff (f1,x)) + (diff (f2,x)) by A6, Th35 ; ::_thesis: verum
end;
hence for x being Point of S st x in Z holds
((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ; ::_thesis: verum
end;
theorem :: NDIFF_1:40
for S, T being non trivial RealNormSpace
for Z being Subset of S st Z is open holds
for f1, f2 being PartFunc of S,T st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 - f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) )
proof
let S, T be non trivial RealNormSpace; ::_thesis: for Z being Subset of S st Z is open holds
for f1, f2 being PartFunc of S,T st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 - f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) )
let Z be Subset of S; ::_thesis: ( Z is open implies for f1, f2 being PartFunc of S,T st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 - f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) ) )
assume A1: Z is open ; ::_thesis: for f1, f2 being PartFunc of S,T st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 - f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) )
let f1, f2 be PartFunc of S,T; ::_thesis: ( Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z implies ( f1 - f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) ) )
assume that
A2: Z c= dom (f1 - f2) and
A3: ( f1 is_differentiable_on Z & f2 is_differentiable_on Z ) ; ::_thesis: ( f1 - f2 is_differentiable_on Z & ( for x being Point of S st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) )
now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_Z_holds_
f1_-_f2_is_differentiable_in_x0
let x0 be Point of S; ::_thesis: ( x0 in Z implies f1 - f2 is_differentiable_in x0 )
assume x0 in Z ; ::_thesis: f1 - f2 is_differentiable_in x0
then ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 ) by A1, A3, Th31;
hence f1 - f2 is_differentiable_in x0 by Th36; ::_thesis: verum
end;
hence A4: f1 - f2 is_differentiable_on Z by A1, A2, Th31; ::_thesis: for x being Point of S st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x))
now__::_thesis:_for_x_being_Point_of_S_st_x_in_Z_holds_
((f1_-_f2)_`|_Z)_/._x_=_(diff_(f1,x))_-_(diff_(f2,x))
let x be Point of S; ::_thesis: ( x in Z implies ((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) )
assume A5: x in Z ; ::_thesis: ((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x))
then A6: ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A1, A3, Th31;
thus ((f1 - f2) `| Z) /. x = diff ((f1 - f2),x) by A4, A5, Def9
.= (diff (f1,x)) - (diff (f2,x)) by A6, Th36 ; ::_thesis: verum
end;
hence for x being Point of S st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ; ::_thesis: verum
end;
theorem :: NDIFF_1:41
for S, T being non trivial RealNormSpace
for Z being Subset of S st Z is open holds
for r being Real
for f being PartFunc of S,T st Z c= dom (r (#) f) & f is_differentiable_on Z holds
( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds
((r (#) f) `| Z) /. x = r * (diff (f,x)) ) )
proof
let S, T be non trivial RealNormSpace; ::_thesis: for Z being Subset of S st Z is open holds
for r being Real
for f being PartFunc of S,T st Z c= dom (r (#) f) & f is_differentiable_on Z holds
( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds
((r (#) f) `| Z) /. x = r * (diff (f,x)) ) )
let Z be Subset of S; ::_thesis: ( Z is open implies for r being Real
for f being PartFunc of S,T st Z c= dom (r (#) f) & f is_differentiable_on Z holds
( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds
((r (#) f) `| Z) /. x = r * (diff (f,x)) ) ) )
assume A1: Z is open ; ::_thesis: for r being Real
for f being PartFunc of S,T st Z c= dom (r (#) f) & f is_differentiable_on Z holds
( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds
((r (#) f) `| Z) /. x = r * (diff (f,x)) ) )
let r be Real; ::_thesis: for f being PartFunc of S,T st Z c= dom (r (#) f) & f is_differentiable_on Z holds
( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds
((r (#) f) `| Z) /. x = r * (diff (f,x)) ) )
let f be PartFunc of S,T; ::_thesis: ( Z c= dom (r (#) f) & f is_differentiable_on Z implies ( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds
((r (#) f) `| Z) /. x = r * (diff (f,x)) ) ) )
assume that
A2: Z c= dom (r (#) f) and
A3: f is_differentiable_on Z ; ::_thesis: ( r (#) f is_differentiable_on Z & ( for x being Point of S st x in Z holds
((r (#) f) `| Z) /. x = r * (diff (f,x)) ) )
now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_Z_holds_
r_(#)_f_is_differentiable_in_x0
let x0 be Point of S; ::_thesis: ( x0 in Z implies r (#) f is_differentiable_in x0 )
assume x0 in Z ; ::_thesis: r (#) f is_differentiable_in x0
then f is_differentiable_in x0 by A1, A3, Th31;
hence r (#) f is_differentiable_in x0 by Th37; ::_thesis: verum
end;
hence A4: r (#) f is_differentiable_on Z by A1, A2, Th31; ::_thesis: for x being Point of S st x in Z holds
((r (#) f) `| Z) /. x = r * (diff (f,x))
now__::_thesis:_for_x_being_Point_of_S_st_x_in_Z_holds_
((r_(#)_f)_`|_Z)_/._x_=_r_*_(diff_(f,x))
let x be Point of S; ::_thesis: ( x in Z implies ((r (#) f) `| Z) /. x = r * (diff (f,x)) )
assume A5: x in Z ; ::_thesis: ((r (#) f) `| Z) /. x = r * (diff (f,x))
then A6: f is_differentiable_in x by A1, A3, Th31;
thus ((r (#) f) `| Z) /. x = diff ((r (#) f),x) by A4, A5, Def9
.= r * (diff (f,x)) by A6, Th37 ; ::_thesis: verum
end;
hence for x being Point of S st x in Z holds
((r (#) f) `| Z) /. x = r * (diff (f,x)) ; ::_thesis: verum
end;
theorem :: NDIFF_1:42
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S st Z is open & Z c= dom f & f | Z is constant holds
( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) )
proof
let S, T be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,T
for Z being Subset of S st Z is open & Z c= dom f & f | Z is constant holds
( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) )
let f be PartFunc of S,T; ::_thesis: for Z being Subset of S st Z is open & Z c= dom f & f | Z is constant holds
( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) )
let Z be Subset of S; ::_thesis: ( Z is open & Z c= dom f & f | Z is constant implies ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) ) )
assume A1: Z is open ; ::_thesis: ( not Z c= dom f or not f | Z is constant or ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) ) )
reconsider R = the carrier of S --> (0. T) as PartFunc of S,T ;
set L = 0. (R_NormSpace_of_BoundedLinearOperators (S,T));
assume that
A2: Z c= dom f and
A3: f | Z is constant ; ::_thesis: ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) )
R_NormSpace_of_BoundedLinearOperators (S,T) = NORMSTR(# (BoundedLinearOperators (S,T)),(Zero_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(Add_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(Mult_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(BoundedLinearOperatorsNorm (S,T)) #) by LOPBAN_1:def_14;
then reconsider L = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) as Element of BoundedLinearOperators (S,T) ;
A4: dom R = the carrier of S by FUNCOP_1:13;
now__::_thesis:_for_h_being_non-zero_0._S_-convergent_sequence_of_S_holds_
(_(||.h.||_")_(#)_(R_/*_h)_is_convergent_&_lim_((||.h.||_")_(#)_(R_/*_h))_=_0._T_)
let h be non-zero 0. S -convergent sequence of S; ::_thesis: ( (||.h.|| ") (#) (R /* h) is convergent & lim ((||.h.|| ") (#) (R /* h)) = 0. T )
A5: now__::_thesis:_for_n_being_Nat_holds_((||.h.||_")_(#)_(R_/*_h))_._n_=_0._T
let n be Nat; ::_thesis: ((||.h.|| ") (#) (R /* h)) . n = 0. T
A6: R /. (h . n) = R . (h . n) by A4, PARTFUN1:def_6
.= 0. T by FUNCOP_1:7 ;
A7: rng h c= dom R by A4;
A8: n in NAT by ORDINAL1:def_12;
hence ((||.h.|| ") (#) (R /* h)) . n = ((||.h.|| ") . n) * ((R /* h) . n) by Def2
.= ((||.h.|| ") . n) * (R /. (h . n)) by A8, A7, FUNCT_2:109
.= 0. T by A6, RLVECT_1:10 ;
::_thesis: verum
end;
then A9: (||.h.|| ") (#) (R /* h) is constant by VALUED_0:def_18;
hence (||.h.|| ") (#) (R /* h) is convergent by Th18; ::_thesis: lim ((||.h.|| ") (#) (R /* h)) = 0. T
((||.h.|| ") (#) (R /* h)) . 0 = 0. T by A5;
hence lim ((||.h.|| ") (#) (R /* h)) = 0. T by A9, Th18; ::_thesis: verum
end;
then reconsider R = R as RestFunc of S,T by Def5;
consider r being Point of T such that
A10: for x being Point of S st x in Z /\ (dom f) holds
f . x = r by A3, PARTFUN2:57;
A11: now__::_thesis:_for_x_being_Point_of_S_st_x_in_Z_/\_(dom_f)_holds_
f_/._x_=_r
let x be Point of S; ::_thesis: ( x in Z /\ (dom f) implies f /. x = r )
assume A12: x in Z /\ (dom f) ; ::_thesis: f /. x = r
Z /\ (dom f) c= dom f by XBOOLE_1:17;
hence f /. x = f . x by A12, PARTFUN1:def_6
.= r by A10, A12 ;
::_thesis: verum
end;
A13: the carrier of S --> (0. T) = L by LOPBAN_1:31;
A14: now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_Z_holds_
f_is_differentiable_in_x0
let x0 be Point of S; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A15: x0 in Z ; ::_thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A16: N c= Z by A1, Th2;
A17: N c= dom f by A2, A16, XBOOLE_1:1;
A18: x0 in Z /\ (dom f) by A2, A15, XBOOLE_0:def_4;
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
proof
let x be Point of S; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A19: R /. (x - x0) = R . (x - x0) by A4, PARTFUN1:def_6
.= 0. T by FUNCOP_1:7 ;
assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
then x in Z /\ (dom f) by A16, A17, XBOOLE_0:def_4;
hence (f /. x) - (f /. x0) = r - (f /. x0) by A11
.= r - r by A11, A18
.= 0. T by RLVECT_1:15
.= (0. T) + (0. T) by RLVECT_1:4
.= (L . (x - x0)) + (R /. (x - x0)) by A13, A19, FUNCOP_1:7 ;
::_thesis: verum
end;
hence f is_differentiable_in x0 by A17, Def6; ::_thesis: verum
end;
hence A20: f is_differentiable_on Z by A1, A2, Th31; ::_thesis: for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T))
let x0 be Point of S; ::_thesis: ( x0 in Z implies (f `| Z) /. x0 = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) )
assume A21: x0 in Z ; ::_thesis: (f `| Z) /. x0 = 0. (R_NormSpace_of_BoundedLinearOperators (S,T))
then consider N being Neighbourhood of x0 such that
A22: N c= Z by A1, Th2;
A23: N c= dom f by A2, A22, XBOOLE_1:1;
A24: x0 in Z /\ (dom f) by A2, A21, XBOOLE_0:def_4;
A25: for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
proof
let x be Point of S; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A26: R /. (x - x0) = R . (x - x0) by A4, PARTFUN1:def_6
.= 0. T by FUNCOP_1:7 ;
assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
then x in Z /\ (dom f) by A22, A23, XBOOLE_0:def_4;
hence (f /. x) - (f /. x0) = r - (f /. x0) by A11
.= r - r by A11, A24
.= 0. T by RLVECT_1:15
.= (0. T) + (0. T) by RLVECT_1:4
.= (L . (x - x0)) + (R /. (x - x0)) by A13, A26, FUNCOP_1:7 ;
::_thesis: verum
end;
A27: f is_differentiable_in x0 by A14, A21;
thus (f `| Z) /. x0 = diff (f,x0) by A20, A21, Def9
.= 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) by A27, A23, A25, Def7 ; ::_thesis: verum
end;
theorem :: NDIFF_1:43
for S being non trivial RealNormSpace
for f being PartFunc of S,S
for r being Real
for p being Point of S
for Z being Subset of S st Z is open & Z c= dom f & ( for x being Point of S st x in Z holds
f /. x = (r * x) + p ) holds
( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = r * (FuncUnit S) ) )
proof
let S be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,S
for r being Real
for p being Point of S
for Z being Subset of S st Z is open & Z c= dom f & ( for x being Point of S st x in Z holds
f /. x = (r * x) + p ) holds
( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = r * (FuncUnit S) ) )
let f be PartFunc of S,S; ::_thesis: for r being Real
for p being Point of S
for Z being Subset of S st Z is open & Z c= dom f & ( for x being Point of S st x in Z holds
f /. x = (r * x) + p ) holds
( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = r * (FuncUnit S) ) )
let r be Real; ::_thesis: for p being Point of S
for Z being Subset of S st Z is open & Z c= dom f & ( for x being Point of S st x in Z holds
f /. x = (r * x) + p ) holds
( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = r * (FuncUnit S) ) )
let p be Point of S; ::_thesis: for Z being Subset of S st Z is open & Z c= dom f & ( for x being Point of S st x in Z holds
f /. x = (r * x) + p ) holds
( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = r * (FuncUnit S) ) )
let Z be Subset of S; ::_thesis: ( Z is open & Z c= dom f & ( for x being Point of S st x in Z holds
f /. x = (r * x) + p ) implies ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = r * (FuncUnit S) ) ) )
assume A1: Z is open ; ::_thesis: ( not Z c= dom f or ex x being Point of S st
( x in Z & not f /. x = (r * x) + p ) or ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = r * (FuncUnit S) ) ) )
A2: R_NormSpace_of_BoundedLinearOperators (S,S) = NORMSTR(# (BoundedLinearOperators (S,S)),(Zero_ ((BoundedLinearOperators (S,S)),(R_VectorSpace_of_LinearOperators (S,S)))),(Add_ ((BoundedLinearOperators (S,S)),(R_VectorSpace_of_LinearOperators (S,S)))),(Mult_ ((BoundedLinearOperators (S,S)),(R_VectorSpace_of_LinearOperators (S,S)))),(BoundedLinearOperatorsNorm (S,S)) #) by LOPBAN_1:def_14;
then reconsider II = FuncUnit S as Point of (R_NormSpace_of_BoundedLinearOperators (S,S)) ;
set L = r * II;
reconsider L = r * II as Point of (R_NormSpace_of_BoundedLinearOperators (S,S)) ;
reconsider R = the carrier of S --> (0. S) as PartFunc of S,S ;
assume that
A3: Z c= dom f and
A4: for x being Point of S st x in Z holds
f /. x = (r * x) + p ; ::_thesis: ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = r * (FuncUnit S) ) )
A5: L = r * (FuncUnit S) by A2, LOPBAN_2:def_3;
A6: dom R = the carrier of S by FUNCOP_1:13;
now__::_thesis:_for_h_being_non-zero_0._S_-convergent_sequence_of_S_holds_
(_(||.h.||_")_(#)_(R_/*_h)_is_convergent_&_lim_((||.h.||_")_(#)_(R_/*_h))_=_0._S_)
let h be non-zero 0. S -convergent sequence of S; ::_thesis: ( (||.h.|| ") (#) (R /* h) is convergent & lim ((||.h.|| ") (#) (R /* h)) = 0. S )
A7: now__::_thesis:_for_n_being_Nat_holds_((||.h.||_")_(#)_(R_/*_h))_._n_=_0._S
let n be Nat; ::_thesis: ((||.h.|| ") (#) (R /* h)) . n = 0. S
A8: R /. (h . n) = R . (h . n) by A6, PARTFUN1:def_6
.= 0. S by FUNCOP_1:7 ;
A9: rng h c= dom R by A6;
A10: n in NAT by ORDINAL1:def_12;
hence ((||.h.|| ") (#) (R /* h)) . n = ((||.h.|| ") . n) * ((R /* h) . n) by Def2
.= ((||.h.|| ") . n) * (R /. (h . n)) by A10, A9, FUNCT_2:109
.= 0. S by A8, RLVECT_1:10 ;
::_thesis: verum
end;
then A11: (||.h.|| ") (#) (R /* h) is constant by VALUED_0:def_18;
hence (||.h.|| ") (#) (R /* h) is convergent by Th18; ::_thesis: lim ((||.h.|| ") (#) (R /* h)) = 0. S
((||.h.|| ") (#) (R /* h)) . 0 = 0. S by A7;
hence lim ((||.h.|| ") (#) (R /* h)) = 0. S by A11, Th18; ::_thesis: verum
end;
then reconsider R = R as RestFunc of S,S by Def5;
A12: now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_Z_holds_
f_is_differentiable_in_x0
let x0 be Point of S; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A13: x0 in Z ; ::_thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A14: N c= Z by A1, Th2;
A15: for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
proof
let x be Point of S; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A16: R /. (x - x0) = R . (x - x0) by A6, PARTFUN1:def_6
.= 0. S by FUNCOP_1:7 ;
x - x0 = (id the carrier of S) . (x - x0) by FUNCT_1:17;
then A17: r * (x - x0) = r * ((FuncUnit S) . (x - x0)) by LOPBAN_2:def_5
.= L . (x - x0) by LOPBAN_1:36 ;
assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = ((r * x) + p) - (f /. x0) by A4, A14
.= ((r * x) + p) - ((r * x0) + p) by A4, A13
.= (r * x) + (p - ((r * x0) + p)) by RLVECT_1:def_3
.= (r * x) + ((p - (r * x0)) - p) by RLVECT_1:27
.= (r * x) + ((p + (- (r * x0))) - p)
.= (r * x) + ((- (r * x0)) + (p - p)) by RLVECT_1:def_3
.= (r * x) + ((- (r * x0)) + (0. S)) by RLVECT_1:15
.= (r * x) - (r * x0) by RLVECT_1:4
.= r * (x - x0) by RLVECT_1:34
.= (L . (x - x0)) + (R /. (x - x0)) by A16, A17, RLVECT_1:4 ;
::_thesis: verum
end;
N c= dom f by A3, A14, XBOOLE_1:1;
hence f is_differentiable_in x0 by A15, Def6; ::_thesis: verum
end;
hence A18: f is_differentiable_on Z by A1, A3, Th31; ::_thesis: for x being Point of S st x in Z holds
(f `| Z) /. x = r * (FuncUnit S)
let x0 be Point of S; ::_thesis: ( x0 in Z implies (f `| Z) /. x0 = r * (FuncUnit S) )
assume A19: x0 in Z ; ::_thesis: (f `| Z) /. x0 = r * (FuncUnit S)
then consider N being Neighbourhood of x0 such that
A20: N c= Z by A1, Th2;
A21: for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
proof
let x be Point of S; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A22: R /. (x - x0) = R . (x - x0) by A6, PARTFUN1:def_6
.= 0. S by FUNCOP_1:7 ;
x - x0 = (id the carrier of S) . (x - x0) by FUNCT_1:17;
then A23: r * (x - x0) = r * ((FuncUnit S) . (x - x0)) by LOPBAN_2:def_5
.= L . (x - x0) by LOPBAN_1:36 ;
assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = ((r * x) + p) - (f /. x0) by A4, A20
.= ((r * x) + p) - ((r * x0) + p) by A4, A19
.= (r * x) + (p - ((r * x0) + p)) by RLVECT_1:def_3
.= (r * x) + ((p - (r * x0)) - p) by RLVECT_1:27
.= (r * x) + ((p + (- (r * x0))) - p)
.= (r * x) + ((- (r * x0)) + (p - p)) by RLVECT_1:def_3
.= (r * x) + ((- (r * x0)) + (0. S)) by RLVECT_1:15
.= (r * x) - (r * x0) by RLVECT_1:4
.= r * (x - x0) by RLVECT_1:34
.= (L . (x - x0)) + (R /. (x - x0)) by A22, A23, RLVECT_1:4 ;
::_thesis: verum
end;
A24: N c= dom f by A3, A20, XBOOLE_1:1;
A25: f is_differentiable_in x0 by A12, A19;
thus (f `| Z) /. x0 = diff (f,x0) by A18, A19, Def9
.= r * (FuncUnit S) by A5, A25, A24, A21, Def7 ; ::_thesis: verum
end;
theorem Th44: :: NDIFF_1:44
for T, S being non trivial RealNormSpace
for f being PartFunc of S,T
for x0 being Point of S st f is_differentiable_in x0 holds
f is_continuous_in x0
proof
let T, S be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,T
for x0 being Point of S st f is_differentiable_in x0 holds
f is_continuous_in x0
let f be PartFunc of S,T; ::_thesis: for x0 being Point of S st f is_differentiable_in x0 holds
f is_continuous_in x0
let x0 be Point of S; ::_thesis: ( f is_differentiable_in x0 implies f is_continuous_in x0 )
assume A1: f is_differentiable_in x0 ; ::_thesis: f is_continuous_in x0
then consider N being Neighbourhood of x0 such that
A2: N c= dom f and
ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def6;
A3: now__::_thesis:_for_s1_being_sequence_of_S_st_rng_s1_c=_dom_f_&_s1_is_convergent_&_lim_s1_=_x0_&_(_for_n_being_Element_of_NAT_holds_s1_._n_<>_x0_)_holds_
(_f_/*_s1_is_convergent_&_f_/._x0_=_lim_(f_/*_s1)_)
consider g being Real such that
A4: 0 < g and
A5: { y where y is Point of S : ||.(y - x0).|| < g } c= N by NFCONT_1:def_1;
reconsider s2 = NAT --> x0 as sequence of S ;
let s1 be sequence of S; ::_thesis: ( rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) implies ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) )
assume that
A6: rng s1 c= dom f and
A7: s1 is convergent and
A8: lim s1 = x0 and
A9: for n being Element of NAT holds s1 . n <> x0 ; ::_thesis: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) )
consider l being Element of NAT such that
A10: for m being Element of NAT st l <= m holds
||.((s1 . m) - x0).|| < g by A7, A8, A4, NORMSP_1:def_7;
deffunc H1( Element of NAT ) -> Element of the carrier of S = (s1 . $1) - (s2 . $1);
consider s3 being sequence of S such that
A11: for n being Element of NAT holds s3 . n = H1(n) from FUNCT_2:sch_4();
A12: now__::_thesis:_for_n_being_Element_of_NAT_holds_not_s3_._n_=_0._S
given n being Element of NAT such that A13: s3 . n = 0. S ; ::_thesis: contradiction
(s1 . n) - (s2 . n) = 0. S by A11, A13;
then (s1 . n) - x0 = 0. S by FUNCOP_1:7;
hence contradiction by A9, RLVECT_1:21; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_not_(s3_^\_l)_._n_=_0._S
given n being Element of NAT such that A14: (s3 ^\ l) . n = 0. S ; ::_thesis: contradiction
s3 . (n + l) = 0. S by A14, NAT_1:def_3;
hence contradiction by A12; ::_thesis: verum
end;
then A15: s3 ^\ l is non-zero by Th7;
reconsider c = s2 ^\ l as constant sequence of S ;
A16: s3 = s1 - s2 by A11, NORMSP_1:def_3;
A17: s2 is convergent by Th18;
then A18: s3 is convergent by A7, A16, NORMSP_1:20;
then A19: s3 ^\ l is convergent by LOPBAN_3:9;
lim s2 = s2 . 0 by Th18
.= x0 by FUNCOP_1:7 ;
then lim s3 = x0 - x0 by A7, A8, A17, A16, NORMSP_1:26
.= 0. S by RLVECT_1:15 ;
then lim (s3 ^\ l) = 0. S by A18, LOPBAN_3:9;
then reconsider h = s3 ^\ l as non-zero 0. S -convergent sequence of S by A19, A15, Def4;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(((f_/*_(h_+_c))_-_(f_/*_c))_+_(f_/*_c))_._n_=_(f_/*_(h_+_c))_._n
let n be Element of NAT ; ::_thesis: (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (f /* (h + c)) . n
thus (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (((f /* (h + c)) - (f /* c)) . n) + ((f /* c) . n) by NORMSP_1:def_2
.= (((f /* (h + c)) . n) - ((f /* c) . n)) + ((f /* c) . n) by NORMSP_1:def_3
.= ((f /* (h + c)) . n) - (((f /* c) . n) - ((f /* c) . n)) by RLVECT_1:29
.= ((f /* (h + c)) . n) - (0. T) by RLVECT_1:15
.= (f /* (h + c)) . n by RLVECT_1:13 ; ::_thesis: verum
end;
then A20: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (h + c) by FUNCT_2:63;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(h_+_c)_._n_=_(s1_^\_l)_._n
let n be Element of NAT ; ::_thesis: (h + c) . n = (s1 ^\ l) . n
thus (h + c) . n = (((s1 - s2) + s2) ^\ l) . n by A16, Th15
.= ((s1 - s2) + s2) . (n + l) by NAT_1:def_3
.= ((s1 - s2) . (n + l)) + (s2 . (n + l)) by NORMSP_1:def_2
.= ((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l)) by NORMSP_1:def_3
.= (s1 . (n + l)) - ((s2 . (n + l)) - (s2 . (n + l))) by RLVECT_1:29
.= (s1 . (n + l)) - (0. S) by RLVECT_1:15
.= s1 . (l + n) by RLVECT_1:13
.= (s1 ^\ l) . n by NAT_1:def_3 ; ::_thesis: verum
end;
then A21: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (s1 ^\ l) by A20, FUNCT_2:63
.= (f /* s1) ^\ l by A6, VALUED_0:27 ;
A22: rng c = {x0}
proof
thus rng c c= {x0} :: according to XBOOLE_0:def_10 ::_thesis: {x0} c= rng c
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng c or y in {x0} )
assume y in rng c ; ::_thesis: y in {x0}
then consider n being Element of NAT such that
A23: y = (s2 ^\ l) . n by NFCONT_1:6;
y = s2 . (n + l) by A23, NAT_1:def_3;
then y = x0 by FUNCOP_1:7;
hence y in {x0} by TARSKI:def_1; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {x0} or y in rng c )
assume y in {x0} ; ::_thesis: y in rng c
then A24: y = x0 by TARSKI:def_1;
c . 0 = s2 . (0 + l) by NAT_1:def_3
.= y by A24, FUNCOP_1:7 ;
hence y in rng c by NFCONT_1:6; ::_thesis: verum
end;
A25: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.(((f_/*_c)_._m)_-_(f_/._x0)).||_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((f /* c) . m) - (f /. x0)).|| < p )
assume A26: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((f /* c) . m) - (f /. x0)).|| < p
take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds
||.(((f /* c) . m) - (f /. x0)).|| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((f /* c) . m) - (f /. x0)).|| < p )
assume n <= m ; ::_thesis: ||.(((f /* c) . m) - (f /. x0)).|| < p
x0 in N by NFCONT_1:4;
then rng c c= dom f by A2, A22, ZFMISC_1:31;
then ||.(((f /* c) . m) - (f /. x0)).|| = ||.((f /. (c . m)) - (f /. x0)).|| by FUNCT_2:109
.= ||.((f /. (s2 . (m + l))) - (f /. x0)).|| by NAT_1:def_3
.= ||.((f /. x0) - (f /. x0)).|| by FUNCOP_1:7
.= ||.(0. T).|| by RLVECT_1:15
.= 0 by NORMSP_1:1 ;
hence ||.(((f /* c) . m) - (f /. x0)).|| < p by A26; ::_thesis: verum
end;
then A27: f /* c is convergent by NORMSP_1:def_6;
A28: rng (h + c) c= N
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (h + c) or y in N )
assume A29: y in rng (h + c) ; ::_thesis: y in N
then consider n being Element of NAT such that
A30: y = (h + c) . n by NFCONT_1:6;
reconsider y1 = y as Point of S by A29;
(h + c) . n = (((s1 - s2) + s2) ^\ l) . n by A16, Th15
.= ((s1 - s2) + s2) . (n + l) by NAT_1:def_3
.= ((s1 - s2) . (n + l)) + (s2 . (n + l)) by NORMSP_1:def_2
.= ((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l)) by NORMSP_1:def_3
.= (s1 . (n + l)) - ((s2 . (n + l)) - (s2 . (n + l))) by RLVECT_1:29
.= (s1 . (n + l)) - (0. S) by RLVECT_1:15
.= s1 . (l + n) by RLVECT_1:13 ;
then ||.(((h + c) . n) - x0).|| < g by A10, NAT_1:12;
then y1 in { z where z is Point of S : ||.(z - x0).|| < g } by A30;
hence y in N by A5; ::_thesis: verum
end;
then A31: (f /* (h + c)) - (f /* c) is convergent by A1, A2, A22, Th34;
then ((f /* (h + c)) - (f /* c)) + (f /* c) is convergent by A27, NORMSP_1:19;
hence f /* s1 is convergent by A21, LOPBAN_3:10; ::_thesis: f /. x0 = lim (f /* s1)
A32: lim ((f /* (h + c)) - (f /* c)) = 0. T by A1, A2, A22, A28, Th34;
lim (f /* c) = f /. x0 by A25, A27, NORMSP_1:def_7;
then lim (((f /* (h + c)) - (f /* c)) + (f /* c)) = (0. T) + (f /. x0) by A31, A32, A27, NORMSP_1:25
.= f /. x0 by RLVECT_1:4 ;
hence f /. x0 = lim (f /* s1) by A31, A27, A21, LOPBAN_3:11, NORMSP_1:19; ::_thesis: verum
end;
x0 in N by NFCONT_1:4;
hence f is_continuous_in x0 by A2, A3, Th27; ::_thesis: verum
end;
theorem :: NDIFF_1:45
for X being set
for S, T being non trivial RealNormSpace
for f being PartFunc of S,T st f is_differentiable_on X holds
f is_continuous_on X
proof
let X be set ; ::_thesis: for S, T being non trivial RealNormSpace
for f being PartFunc of S,T st f is_differentiable_on X holds
f is_continuous_on X
let S, T be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,T st f is_differentiable_on X holds
f is_continuous_on X
let f be PartFunc of S,T; ::_thesis: ( f is_differentiable_on X implies f is_continuous_on X )
assume A1: f is_differentiable_on X ; ::_thesis: f is_continuous_on X
hence X c= dom f by Def8; :: according to NFCONT_1:def_7 ::_thesis: for b1 being Element of the carrier of S holds
( not b1 in X or f | X is_continuous_in b1 )
let x be Point of S; ::_thesis: ( not x in X or f | X is_continuous_in x )
assume x in X ; ::_thesis: f | X is_continuous_in x
then f | X is_differentiable_in x by A1, Def8;
hence f | X is_continuous_in x by Th44; ::_thesis: verum
end;
theorem :: NDIFF_1:46
for X being set
for T, S being non trivial RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S st Z is open & f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
proof
let X be set ; ::_thesis: for T, S being non trivial RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S st Z is open & f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
let T, S be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,T
for Z being Subset of S st Z is open & f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
let f be PartFunc of S,T; ::_thesis: for Z being Subset of S st Z is open & f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
let Z be Subset of S; ::_thesis: ( Z is open & f is_differentiable_on X & Z c= X implies f is_differentiable_on Z )
assume A1: Z is open ; ::_thesis: ( not f is_differentiable_on X or not Z c= X or f is_differentiable_on Z )
assume that
A2: f is_differentiable_on X and
A3: Z c= X ; ::_thesis: f is_differentiable_on Z
X c= dom f by A2, Def8;
hence A4: Z c= dom f by A3, XBOOLE_1:1; :: according to NDIFF_1:def_8 ::_thesis: for x being Point of S st x in Z holds
f | Z is_differentiable_in x
let x0 be Point of S; ::_thesis: ( x0 in Z implies f | Z is_differentiable_in x0 )
assume A5: x0 in Z ; ::_thesis: f | Z is_differentiable_in x0
then consider N1 being Neighbourhood of x0 such that
A6: N1 c= Z by A1, Th2;
f | X is_differentiable_in x0 by A2, A3, A5, Def8;
then consider N being Neighbourhood of x0 such that
A7: N c= dom (f | X) and
A8: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N holds
((f | X) /. x) - ((f | X) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def6;
consider N2 being Neighbourhood of x0 such that
A9: N2 c= N and
A10: N2 c= N1 by Th1;
A11: N2 c= Z by A6, A10, XBOOLE_1:1;
take N2 ; :: according to NDIFF_1:def_6 ::_thesis: ( N2 c= dom (f | Z) & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N2 holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
dom (f | X) = (dom f) /\ X by RELAT_1:61;
then dom (f | X) c= dom f by XBOOLE_1:17;
then N c= dom f by A7, XBOOLE_1:1;
then N2 c= dom f by A9, XBOOLE_1:1;
then N2 c= (dom f) /\ Z by A11, XBOOLE_1:19;
hence A12: N2 c= dom (f | Z) by RELAT_1:61; ::_thesis: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N2 holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
consider L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R being RestFunc of S,T such that
A13: for x being Point of S st x in N holds
((f | X) /. x) - ((f | X) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A8;
take L ; ::_thesis: ex R being RestFunc of S,T st
for x being Point of S st x in N2 holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
take R ; ::_thesis: for x being Point of S st x in N2 holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
let x be Point of S; ::_thesis: ( x in N2 implies ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
assume A14: x in N2 ; ::_thesis: ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0))
then ((f | X) /. x) - ((f | X) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A9, A13;
then A15: ((f | X) /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A3, A4, A5, PARTFUN2:17;
x in N by A9, A14;
then (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A7, A15, PARTFUN2:15;
then (f /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A4, A5, PARTFUN2:17;
hence ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A12, A14, PARTFUN2:15; ::_thesis: verum
end;
theorem :: NDIFF_1:47
for T, S being non trivial RealNormSpace
for f being PartFunc of S,T
for x0 being Point of S st f is_differentiable_in x0 holds
ex N being Neighbourhood of x0 st
( N c= dom f & ex R being RestFunc of S,T st
( R /. (0. S) = 0. T & R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff (f,x0)) . (x - x0)) + (R /. (x - x0)) ) ) )
proof
let T, S be non trivial RealNormSpace; ::_thesis: for f being PartFunc of S,T
for x0 being Point of S st f is_differentiable_in x0 holds
ex N being Neighbourhood of x0 st
( N c= dom f & ex R being RestFunc of S,T st
( R /. (0. S) = 0. T & R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff (f,x0)) . (x - x0)) + (R /. (x - x0)) ) ) )
let f be PartFunc of S,T; ::_thesis: for x0 being Point of S st f is_differentiable_in x0 holds
ex N being Neighbourhood of x0 st
( N c= dom f & ex R being RestFunc of S,T st
( R /. (0. S) = 0. T & R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff (f,x0)) . (x - x0)) + (R /. (x - x0)) ) ) )
let x0 be Point of S; ::_thesis: ( f is_differentiable_in x0 implies ex N being Neighbourhood of x0 st
( N c= dom f & ex R being RestFunc of S,T st
( R /. (0. S) = 0. T & R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff (f,x0)) . (x - x0)) + (R /. (x - x0)) ) ) ) )
assume f is_differentiable_in x0 ; ::_thesis: ex N being Neighbourhood of x0 st
( N c= dom f & ex R being RestFunc of S,T st
( R /. (0. S) = 0. T & R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff (f,x0)) . (x - x0)) + (R /. (x - x0)) ) ) )
then consider N being Neighbourhood of x0 such that
A1: N c= dom f and
A2: ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff (f,x0)) . (x - x0)) + (R /. (x - x0)) by Def7;
take N ; ::_thesis: ( N c= dom f & ex R being RestFunc of S,T st
( R /. (0. S) = 0. T & R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff (f,x0)) . (x - x0)) + (R /. (x - x0)) ) ) )
ex R being RestFunc of S,T st
( R /. (0. S) = 0. T & R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff (f,x0)) . (x - x0)) + (R /. (x - x0)) ) )
proof
R_NormSpace_of_BoundedLinearOperators (S,T) = NORMSTR(# (BoundedLinearOperators (S,T)),(Zero_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(Add_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(Mult_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(BoundedLinearOperatorsNorm (S,T)) #) by LOPBAN_1:def_14;
then reconsider L = diff (f,x0) as Element of BoundedLinearOperators (S,T) ;
consider R being RestFunc of S,T such that
A3: for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff (f,x0)) . (x - x0)) + (R /. (x - x0)) by A2;
take R ; ::_thesis: ( R /. (0. S) = 0. T & R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff (f,x0)) . (x - x0)) + (R /. (x - x0)) ) )
(f /. x0) - (f /. x0) = (L . (x0 - x0)) + (R /. (x0 - x0)) by A3, NFCONT_1:4;
then 0. T = (L . (x0 - x0)) + (R /. (x0 - x0)) by RLVECT_1:15;
then 0. T = (L . (0. S)) + (R /. (x0 - x0)) by RLVECT_1:15;
then A4: 0. T = (L . (0. S)) + (R /. (0. S)) by RLVECT_1:15;
L . (0. S) = (modetrans (L,S,T)) . (0. S) by LOPBAN_1:def_11
.= (modetrans (L,S,T)) . (0 * (0. S)) by RLVECT_1:10
.= 0 * ((modetrans (L,S,T)) . (0. S)) by LOPBAN_1:def_5
.= 0. T by RLVECT_1:10 ;
hence A5: R /. (0. S) = 0. T by A4, RLVECT_1:4; ::_thesis: ( R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff (f,x0)) . (x - x0)) + (R /. (x - x0)) ) )
A6: now__::_thesis:_for_s1_being_sequence_of_S_st_rng_s1_c=_dom_R_&_s1_is_convergent_&_lim_s1_=_0._S_&_(_for_n_being_Element_of_NAT_holds_s1_._n_<>_0._S_)_holds_
(_R_/*_s1_is_convergent_&_lim_(R_/*_s1)_=_R_/._(0._S)_)
let s1 be sequence of S; ::_thesis: ( rng s1 c= dom R & s1 is convergent & lim s1 = 0. S & ( for n being Element of NAT holds s1 . n <> 0. S ) implies ( R /* s1 is convergent & lim (R /* s1) = R /. (0. S) ) )
assume that
rng s1 c= dom R and
A7: ( s1 is convergent & lim s1 = 0. S ) and
A8: for n being Element of NAT holds s1 . n <> 0. S ; ::_thesis: ( R /* s1 is convergent & lim (R /* s1) = R /. (0. S) )
s1 is non-zero by A8, Th7;
then s1 is non-zero 0. S -convergent sequence of S by A7, Def4;
hence ( R /* s1 is convergent & lim (R /* s1) = R /. (0. S) ) by A5, Th24; ::_thesis: verum
end;
R is total by Def5;
then dom R = the carrier of S by PARTFUN1:def_2;
hence ( R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff (f,x0)) . (x - x0)) + (R /. (x - x0)) ) ) by A3, A6, Th27; ::_thesis: verum
end;
hence ( N c= dom f & ex R being RestFunc of S,T st
( R /. (0. S) = 0. T & R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff (f,x0)) . (x - x0)) + (R /. (x - x0)) ) ) ) by A1; ::_thesis: verum
end;