let X be RealBanachSpace; :: thesis: for a, b being Real
for F being PartFunc of REAL, the carrier of X
for f being continuous PartFunc of REAL, the carrier of X st dom f = [.a,b.] & dom F = [.a,b.] & ( for t being Real st t in [.a,b.] holds
F /. t = integral (f,a,t) ) holds
for x being Real st x in [.a,b.] holds
F is_continuous_in x
let a, b be Real; :: thesis: for F being PartFunc of REAL, the carrier of X
for f being continuous PartFunc of REAL, the carrier of X st dom f = [.a,b.] & dom F = [.a,b.] & ( for t being Real st t in [.a,b.] holds
F /. t = integral (f,a,t) ) holds
for x being Real st x in [.a,b.] holds
F is_continuous_in x
let F be PartFunc of REAL, the carrier of X; :: thesis: for f being continuous PartFunc of REAL, the carrier of X st dom f = [.a,b.] & dom F = [.a,b.] & ( for t being Real st t in [.a,b.] holds
F /. t = integral (f,a,t) ) holds
for x being Real st x in [.a,b.] holds
F is_continuous_in x
let f be continuous PartFunc of REAL, the carrier of X; :: thesis: ( dom f = [.a,b.] & dom F = [.a,b.] & ( for t being Real st t in [.a,b.] holds
F /. t = integral (f,a,t) ) implies for x being Real st x in [.a,b.] holds
F is_continuous_in x )
set f1 = ||.f.||;
assume A1: ( dom f = [.a,b.] & dom F = [.a,b.] & ( for t being Real st t in [.a,b.] holds
F /. t = integral (f,a,t) ) ) ; :: thesis: for x being Real st x in [.a,b.] holds
F is_continuous_in x
let x0 be Real; :: thesis: ( x0 in [.a,b.] implies F is_continuous_in x0 )
assume A12: x0 in [.a,b.] ; :: thesis: F is_continuous_in x0
per cases ( a > b or a <= b ) ;
suppose a > b ; :: thesis: F is_continuous_in x0
hence F is_continuous_in x0 by A12, XXREAL_1:29; :: thesis: verum
end;
suppose X1: a <= b ; :: thesis: F is_continuous_in x0
reconsider AB = ['a,b'] as non empty closed_interval Subset of REAL ;
X2: AB = [.a,b.] by X1, INTEGRA5:def 3;
then A2: f | AB is bounded by A1, X1, INTEGR21:11;
B1: dom f = dom ||.f.|| by NORMSP_0:def 2;
then ||.f.|| | AB = ||.f.|| by A1, X2;
then ||.f.|| is bounded by A1, A2, X2, INTEGR21:9;
then consider K being Real such that
A3: for y being set st y in dom ||.f.|| holds
|.(||.f.|| . y).| < K by COMSEQ_2:def 3;
B2: [.a,b.] = AB by X1, INTEGRA5:def 3;
then a in AB by X1;
then |.(||.f.|| . a).| < K by A1, X2, B1, A3;
then A5: 0 < K by COMPLEX1:46;
A6: now :: thesis: for c, d being Real st c in ['a,b'] & d in ['a,b'] holds
||.(integral (f,c,d)).|| <= K * |.(d - c).|
let c, d be Real; :: thesis: ( c in ['a,b'] & d in ['a,b'] implies ||.(integral (f,c,d)).|| <= K * |.(d - c).| )
assume A11: ( c in ['a,b'] & d in ['a,b'] ) ; :: thesis: ||.(integral (f,c,d)).|| <= K * |.(d - c).|
then A7: ['(min (c,d)),(max (c,d))'] c= ['a,b'] by X1, INTEGR19:3;
now :: thesis: for y being Real st y in ['(min (c,d)),(max (c,d))'] holds
||.(f /. y).|| <= K
let y be Real; :: thesis: ( y in ['(min (c,d)),(max (c,d))'] implies ||.(f /. y).|| <= K )
assume y in ['(min (c,d)),(max (c,d))'] ; :: thesis: ||.(f /. y).|| <= K
then y in ['a,b'] by A7;
then A9: y in dom ||.f.|| by X2, NORMSP_0:def 2, A1;
then |.(||.f.|| . y).| < K by A3;
then |.||.(f /. y).||.| < K by A9, NORMSP_0:def 2;
hence ||.(f /. y).|| <= K by ABSVALUE:def 1; :: thesis: verum
end;
hence ||.(integral (f,c,d)).|| <= K * |.(d - c).| by A1, X1, X2, A11, INTEGR21:25; :: thesis: verum
end;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds
||.((F /. x1) - (F /. x0)).|| < r ) )
proof
let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds
||.((F /. x1) - (F /. x0)).|| < r ) ) )
assume 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds
||.((F /. x1) - (F /. x0)).|| < r ) )
then consider s being Real such that
A16: ( 0 < s & s < r / K ) by A5, XREAL_1:5, XREAL_1:139;
s * K < (r / K) * K by A5, A16, XREAL_1:68;
then A17: K * s < r by A5, XCMPLX_1:87;
take s ; :: thesis: ( 0 < s & ( for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds
||.((F /. x1) - (F /. x0)).|| < r ) )
thus 0 < s by A16; :: thesis: for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds
||.((F /. x1) - (F /. x0)).|| < r
let x1 be Real; :: thesis: ( x1 in dom F & |.(x1 - x0).| < s implies ||.((F /. x1) - (F /. x0)).|| < r )
assume A18: ( x1 in dom F & |.(x1 - x0).| < s ) ; :: thesis: ||.((F /. x1) - (F /. x0)).|| < r
then A20: ||.(integral (f,x0,x1)).|| <= K * |.(x1 - x0).| by A1, A12, B2, A6;
K * |.(x1 - x0).| <= K * s by A5, A18, XREAL_1:64;
then A21: K * |.(x1 - x0).| < r by A17, XXREAL_0:2;
A23: ( F /. x0 = integral (f,a,x0) & F /. x1 = integral (f,a,x1) ) by A1, A12, A18;
reconsider R1 = F /. x0 as VECTOR of X ;
reconsider R2 = integral (f,x0,x1) as VECTOR of X ;
((F /. x0) + (integral (f,x0,x1))) - (F /. x0) = ((F /. x0) + (- (F /. x0))) + (integral (f,x0,x1)) by RLVECT_1:def 3
.= (0. X) + (integral (f,x0,x1)) by RLVECT_1:5
.= integral (f,x0,x1) ;
then ||.((F /. x1) - (F /. x0)).|| <= K * |.(x1 - x0).| by A23, A1, X1, A12, B2, A18, INTEGR21:29, A20;
hence ||.((F /. x1) - (F /. x0)).|| < r by A21, XXREAL_0:2; :: thesis: verum
end;
hence F is_continuous_in x0 by A1, A12, NFCONT_3:8; :: thesis: verum
end;
end;