:: The Linearity of Riemann Integral on Functions from $\mathbbbR$ into Real {B}anach Space
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received October 7, 2013
:: Copyright (c) 2013-2018 Association of Mizar Users

Lm2: for a, b, c, d being Real st a <= b & c in ['a,b'] & d in ['a,b'] holds
['(min (c,d)),(max (c,d))'] c= ['a,b']

proof end;

Lm3: for X, Y, Z being non empty set
for f being PartFunc of X,Y st Z c= dom f holds
f | Z is Function of Z,Y

proof end;

theorem Th1915: :: INTEGR21:1
for Z being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of Z st f is bounded & A c= dom f holds
f | A is bounded
proof end;

theorem Th1915a: :: INTEGR21:2
for Z being RealNormSpace
for A, B being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of Z st f | A is bounded & B c= A & B c= dom (f | A) holds
f | B is bounded
proof end;

theorem Th1915b: :: INTEGR21:3
for Z being RealNormSpace
for a, b, c, d being Real
for f being PartFunc of REAL, the carrier of Z st a <= c & c <= d & d <= b & f | ['a,b'] is bounded & ['a,b'] c= dom f holds
f | ['c,d'] is bounded
proof end;

theorem Th1935: :: INTEGR21:4
for Z being RealNormSpace
for X, Y being set
for f1, f2 being PartFunc of REAL, the carrier of Z st f1 | X is bounded & f2 | Y is bounded holds
( (f1 + f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded )
proof end;

theorem Th1935a: :: INTEGR21:5
for Z being RealNormSpace
for r being Real
for X being set
for f being PartFunc of REAL, the carrier of Z st f | X is bounded holds
(r (#) f) | X is bounded
proof end;

theorem Th1935b: :: INTEGR21:6
for Z being RealNormSpace
for X being set
for f being PartFunc of REAL, the carrier of Z st f | X is bounded holds
(- f) | X is bounded
proof end;

theorem Th1914: :: INTEGR21:7
for Z being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of Z holds
( f is bounded iff is bounded )
proof end;

theorem Th1918: :: INTEGR21:8
for Z being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL, the carrier of Z st A c= dom f holds
||.(f | A).|| = | A
proof end;

theorem Th1919: :: INTEGR21:9
for Z being RealNormSpace
for A being non empty closed_interval Subset of REAL
for g being PartFunc of REAL, the carrier of Z st A c= dom g & g | A is bounded holds
| A is bounded
proof end;

theorem Th3: :: INTEGR21:10
for a, b being Real
for Y being RealNormSpace
for f being continuous PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f holds
| ['a,b'] is bounded
proof end;

theorem Th1: :: INTEGR21:11
for a, b being Real
for Y being RealNormSpace
for f being continuous PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f holds
f | ['a,b'] is bounded
proof end;

theorem Th4: :: INTEGR21:12
for a, b being Real
for Y being RealNormSpace
for f being continuous PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f holds
is_integrable_on ['a,b']
proof end;

theorem Th1909: :: INTEGR21:13
for a, b, c, d being Real
for Y being RealBanachSpace
for f being continuous PartFunc of REAL, the carrier of Y st a <= c & c <= d & d <= b & ['a,b'] c= dom f holds
f is_integrable_on ['c,d']
proof end;

theorem Th1947: :: INTEGR21:14
for a, b being Real
for Y being RealBanachSpace
for f being PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f holds
integral (f,b,a) = - (integral (f,a,b))
proof end;

Lm62: for a, b, c being Real
for X being RealBanachSpace
for f being continuous PartFunc of REAL, the carrier of X st a <= b & ['a,b'] c= dom f & c in ['a,b'] & b <> c holds
integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b))

proof end;

theorem Th1908: :: INTEGR21:15
for a, b, c being 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'] holds
( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) )
proof end;

theorem :: INTEGR21:16
for a, b, c, d being Real
for Y being RealBanachSpace
for f, g being continuous PartFunc of REAL, the carrier of Y st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g holds
( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded )
proof end;

theorem Th1911: :: INTEGR21:17
for a, b, c, d, r being Real
for Y being RealBanachSpace
for f being continuous PartFunc of REAL, the carrier of Y st a <= c & c <= d & d <= b & ['a,b'] c= dom f holds
( r (#) f is_integrable_on ['c,d'] & (r (#) f) | ['c,d'] is bounded )
proof end;

theorem :: INTEGR21:18
for a, b, c, d being Real
for Y being RealBanachSpace
for f being continuous PartFunc of REAL, the carrier of Y st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f holds
( - f is_integrable_on ['c,d'] & (- f) | ['c,d'] is bounded )
proof end;

theorem :: INTEGR21:19
for a, b, c, d being Real
for Y being RealBanachSpace
for f, g being continuous PartFunc of REAL, the carrier of Y st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g holds
( f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded )
proof end;

Lm8: for A being non empty closed_interval Subset of REAL
for Y being RealBanachSpace
for h being Function of A, the carrier of Y
for f being Function of A,REAL st h is bounded & h is integrable & f = & f is integrable holds
||.().|| <= integral f

proof end;

theorem Th1920: :: INTEGR21:20
for A being non empty closed_interval Subset of REAL
for Y being RealBanachSpace
for f being PartFunc of REAL, the carrier of Y st A c= dom f & f | A is bounded & f is_integrable_on A & is_integrable_on A holds
||.(integral (f,A)).|| <= integral (,A)
proof end;

theorem Th1921: :: INTEGR21:21
for a, b being Real
for Y being RealBanachSpace
for f being PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds
||.(integral (f,a,b)).|| <= integral (,a,b)
proof end;

Lm10: for a, b, c, d being Real
for Y being RealBanachSpace
for f being continuous PartFunc of REAL, the carrier of Y st a <= b & c <= d & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
( f is_integrable_on ['c,d'] & is_integrable_on ['c,d'] & | ['c,d'] is bounded & ||.(integral (f,c,d)).|| <= integral (,c,d) )

proof end;

theorem Th1922: :: INTEGR21:22
for a, b, c, d being 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
( is_integrable_on ['(min (c,d)),(max (c,d))'] & | ['(min (c,d)),(max (c,d))'] is bounded & ||.(integral (f,c,d)).|| <= integral (,(min (c,d)),(max (c,d))) )
proof end;

Th1925a: for a, b, c, d, r being Real
for Y being RealBanachSpace
for f being continuous PartFunc of REAL, the carrier of Y st a <= b & c <= d & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral ((r (#) f),c,d) = r * (integral (f,c,d))

proof end;

theorem Th1925: :: INTEGR21:23
for a, b, c, d, r being 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
integral ((r (#) f),c,d) = r * (integral (f,c,d))
proof end;

theorem :: INTEGR21:24
for a, b, c, d being 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
integral ((- f),c,d) = - (integral (f,c,d))
proof end;

theorem :: INTEGR21:25
for a, b, c, d, e being 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'] & ( for x being Real st x in ['(min (c,d)),(max (c,d))'] holds
||.(f /. x).|| <= e ) holds
||.(integral (f,c,d)).|| <= e * |.(d - c).|
proof end;

Th1928: for a, b, c, d being Real
for Y being RealBanachSpace
for f, g being continuous PartFunc of REAL, the carrier of Y st a <= b & c <= d & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d))

proof end;

theorem Th404: :: INTEGR21:26
for Y being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of Y
for E being Point of Y st rng f = {E} holds
( f is integrable & integral f = (vol A) * E )
proof end;

theorem Th1929: :: INTEGR21:27
for a, b being Real
for Y being RealBanachSpace
for f being PartFunc of REAL, the carrier of Y
for E being Point of Y st a <= b & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds
f /. x = E ) holds
( f is_integrable_on ['a,b'] & integral (f,a,b) = (b - a) * E )
proof end;

theorem :: INTEGR21:28
for a, b, c, d being Real
for Y being RealBanachSpace
for E being Point of Y
for f being PartFunc of REAL, the carrier of Y st a <= b & c in ['a,b'] & d in ['a,b'] & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds
f /. x = E ) holds
integral (f,c,d) = (d - c) * E
proof end;

Th1931: for a, b, c, d being Real
for Y being RealBanachSpace
for f being continuous PartFunc of REAL, the carrier of Y st a <= b & c <= d & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))

proof end;

theorem :: INTEGR21:29
for a, b, c, d being 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
integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
proof end;

theorem :: INTEGR21:30
for a, b, c, d being Real
for Y being RealBanachSpace
for f, g being continuous PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d))
proof end;