let a, b, c, d be Real; for Y being RealBanachSpace
for f being continuous PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
( ||.f.|| is_integrable_on ['(min (c,d)),(max (c,d))'] & ||.f.|| | ['(min (c,d)),(max (c,d))'] is bounded & ||.(integral (f,c,d)).|| <= integral (||.f.||,(min (c,d)),(max (c,d))) )
let Y be RealBanachSpace; for f being continuous PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
( ||.f.|| is_integrable_on ['(min (c,d)),(max (c,d))'] & ||.f.|| | ['(min (c,d)),(max (c,d))'] is bounded & ||.(integral (f,c,d)).|| <= integral (||.f.||,(min (c,d)),(max (c,d))) )
let f be continuous PartFunc of REAL, the carrier of Y; ( a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies ( ||.f.|| is_integrable_on ['(min (c,d)),(max (c,d))'] & ||.f.|| | ['(min (c,d)),(max (c,d))'] is bounded & ||.(integral (f,c,d)).|| <= integral (||.f.||,(min (c,d)),(max (c,d))) ) )
assume A1:
( a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] )
; ( ||.f.|| is_integrable_on ['(min (c,d)),(max (c,d))'] & ||.f.|| | ['(min (c,d)),(max (c,d))'] is bounded & ||.(integral (f,c,d)).|| <= integral (||.f.||,(min (c,d)),(max (c,d))) )
per cases
( not c <= d or c <= d )
;
suppose A3:
not
c <= d
;
( ||.f.|| is_integrable_on ['(min (c,d)),(max (c,d))'] & ||.f.|| | ['(min (c,d)),(max (c,d))'] is bounded & ||.(integral (f,c,d)).|| <= integral (||.f.||,(min (c,d)),(max (c,d))) )then A5:
(
d = min (
c,
d) &
c = max (
c,
d) )
by XXREAL_0:def 9, XXREAL_0:def 10;
then
['d,c'] c= dom f
by A1, INTEGR19:3;
then
integral (
f,
c,
d)
= - (integral (f,d,c))
by A3, Th1947;
then
||.(integral (f,c,d)).|| = ||.(integral (f,d,c)).||
by NORMSP_1:2;
hence
(
||.f.|| is_integrable_on ['(min (c,d)),(max (c,d))'] &
||.f.|| | ['(min (c,d)),(max (c,d))'] is
bounded &
||.(integral (f,c,d)).|| <= integral (
||.f.||,
(min (c,d)),
(max (c,d))) )
by A1, A3, A5, Lm10;
verum end; suppose A6:
c <= d
;
( ||.f.|| is_integrable_on ['(min (c,d)),(max (c,d))'] & ||.f.|| | ['(min (c,d)),(max (c,d))'] is bounded & ||.(integral (f,c,d)).|| <= integral (||.f.||,(min (c,d)),(max (c,d))) )then
(
c = min (
c,
d) &
d = max (
c,
d) )
by XXREAL_0:def 9, XXREAL_0:def 10;
hence
(
||.f.|| is_integrable_on ['(min (c,d)),(max (c,d))'] &
||.f.|| | ['(min (c,d)),(max (c,d))'] is
bounded &
||.(integral (f,c,d)).|| <= integral (
||.f.||,
(min (c,d)),
(max (c,d))) )
by A1, A6, Lm10;
verum end; end;