:: INTEGRA2 semantic presentation

theorem :: INTEGRA2:1

for A being closed-interval Subset of REAL
for x being real number holds
( x in A iff ( inf A <= x & x <= sup A ) )

proof end;

definition

let IT be FinSequence of REAL ;
attr IT is non-decreasing means :Def1: :: INTEGRA2:def 1
for n being Nat st n in dom IT & n + 1 in dom IT holds
IT . n <= IT . (n + 1);

end;

:: deftheorem Def1 defines non-decreasing INTEGRA2:def 1 :

registration

cluster non-decreasing FinSequence of REAL ;
existence

proof end;

end;

theorem :: INTEGRA2:2

for p being non-decreasing FinSequence of REAL
for i, j being Nat st i in dom p & j in dom p & i <= j holds
p . i <= p . j

proof end;

theorem :: INTEGRA2:3

for p being FinSequence of REAL ex q being non-decreasing FinSequence of REAL st p,q are_fiberwise_equipotent

proof end;

theorem :: INTEGRA2:4

for D being non empty set
for f being FinSequence of D
for k1, k2, k3 being Nat st 1 <= k1 & k3 <= len f & k1 <= k2 & k2 < k3 holds
(mid f,k1,k2) ^ (mid f,(k2 + 1),k3) = mid f,k1,k3

proof end;

definition

let A be Subset of REAL ;
let x be real number ;
func x * A -> Subset of REAL means :Def2: :: INTEGRA2:def 2
for y being Real holds
( y in it iff ex z being Real st
( z in A & y = x * z ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines * INTEGRA2:def 2 :

theorem :: INTEGRA2:5

for X, Y being non empty set
for f being PartFunc of X, REAL st f is_bounded_above_on X & Y c= X holds
f | Y is_bounded_above_on Y

proof end;

theorem :: INTEGRA2:6

for X, Y being non empty set
for f being PartFunc of X, REAL st f is_bounded_below_on X & Y c= X holds
f | Y is_bounded_below_on Y

proof end;

theorem Th7: :: INTEGRA2:7

for r being Real
for X being non empty Subset of REAL holds not r * X is empty

proof end;

theorem Th8: :: INTEGRA2:8

for r being Real
for X being Subset of REAL holds r * X = { (r * x) where x is Real : x in X }

proof end;

theorem :: INTEGRA2:9

for r being Real
for X being non empty Subset of REAL st X is bounded_above & 0 <= r holds
r * X is bounded_above

proof end;

theorem :: INTEGRA2:10

for r being Real
for X being non empty Subset of REAL st X is bounded_above & r <= 0 holds
r * X is bounded_below

proof end;

theorem :: INTEGRA2:11

for r being Real
for X being non empty Subset of REAL st X is bounded_below & 0 <= r holds
r * X is bounded_below

proof end;

theorem :: INTEGRA2:12

for r being Real
for X being non empty Subset of REAL st X is bounded_below & r <= 0 holds
r * X is bounded_above

proof end;

theorem Th13: :: INTEGRA2:13

for r being Real
for X being non empty Subset of REAL st X is bounded_above & 0 <= r holds
sup (r * X) = r * (sup X)

proof end;

theorem Th14: :: INTEGRA2:14

for r being Real
for X being non empty Subset of REAL st X is bounded_above & r <= 0 holds
inf (r * X) = r * (sup X)

proof end;

theorem Th15: :: INTEGRA2:15

for r being Real
for X being non empty Subset of REAL st X is bounded_below & 0 <= r holds
inf (r * X) = r * (inf X)

proof end;

theorem Th16: :: INTEGRA2:16

for r being Real
for X being non empty Subset of REAL st X is bounded_below & r <= 0 holds
sup (r * X) = r * (inf X)

proof end;

theorem Th17: :: INTEGRA2:17

for r being Real
for X being non empty set
for f being Function of X, REAL holds rng (r (#) f) = r * (rng f)

proof end;

theorem Th18: :: INTEGRA2:18

for r being Real
for X, Z being non empty set
for f being PartFunc of X, REAL holds rng (r (#) (f | Z)) = r * (rng (f | Z))

proof end;

theorem Th19: :: INTEGRA2:19

for r being Real
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for D being Element of divs A st f is_bounded_on A & r >= 0 holds
(upper_sum_set (r (#) f)) . D >= (r * (inf (rng f))) * (vol A)

proof end;

theorem Th20: :: INTEGRA2:20

for r being Real
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for D being Element of divs A st f is_bounded_on A & r <= 0 holds
(upper_sum_set (r (#) f)) . D >= (r * (sup (rng f))) * (vol A)

proof end;

theorem Th21: :: INTEGRA2:21

for r being Real
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for D being Element of divs A st f is_bounded_on A & r >= 0 holds
(lower_sum_set (r (#) f)) . D <= (r * (sup (rng f))) * (vol A)

proof end;

theorem Th22: :: INTEGRA2:22

for r being Real
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for D being Element of divs A st f is_bounded_on A & r <= 0 holds
(lower_sum_set (r (#) f)) . D <= (r * (inf (rng f))) * (vol A)

proof end;

theorem Th23: :: INTEGRA2:23

for r being Real
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for S being non empty Division of A
for D being Element of S
for i being Nat st i in Seg (len D) & f is_bounded_above_on A & r >= 0 holds
(upper_volume (r (#) f),D) . i = r * ((upper_volume f,D) . i)

proof end;

theorem Th24: :: INTEGRA2:24

for r being Real
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for S being non empty Division of A
for D being Element of S
for i being Nat st i in Seg (len D) & f is_bounded_above_on A & r <= 0 holds
(lower_volume (r (#) f),D) . i = r * ((upper_volume f,D) . i)

proof end;

theorem Th25: :: INTEGRA2:25

for r being Real
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for S being non empty Division of A
for D being Element of S
for i being Nat st i in Seg (len D) & f is_bounded_below_on A & r >= 0 holds
(lower_volume (r (#) f),D) . i = r * ((lower_volume f,D) . i)

proof end;

theorem Th26: :: INTEGRA2:26

for r being Real
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for S being non empty Division of A
for D being Element of S
for i being Nat st i in Seg (len D) & f is_bounded_below_on A & r <= 0 holds
(upper_volume (r (#) f),D) . i = r * ((lower_volume f,D) . i)

proof end;

theorem Th27: :: INTEGRA2:27

for r being Real
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for S being non empty Division of A
for D being Element of S st f is_bounded_above_on A & r >= 0 holds
upper_sum (r (#) f),D = r * (upper_sum f,D)

proof end;

theorem Th28: :: INTEGRA2:28

for r being Real
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for S being non empty Division of A
for D being Element of S st f is_bounded_above_on A & r <= 0 holds
lower_sum (r (#) f),D = r * (upper_sum f,D)

proof end;

theorem Th29: :: INTEGRA2:29

for r being Real
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for S being non empty Division of A
for D being Element of S st f is_bounded_below_on A & r >= 0 holds
lower_sum (r (#) f),D = r * (lower_sum f,D)

proof end;

theorem Th30: :: INTEGRA2:30

for r being Real
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for S being non empty Division of A
for D being Element of S st f is_bounded_below_on A & r <= 0 holds
upper_sum (r (#) f),D = r * (lower_sum f,D)

proof end;

theorem Th31: :: INTEGRA2:31

for r being Real
for A being closed-interval Subset of REAL
for f being Function of A, REAL st f is_bounded_on A & f is_integrable_on A holds
( r (#) f is_integrable_on A & integral (r (#) f) = r * (integral f) )

proof end;

theorem Th32: :: INTEGRA2:32

for A being closed-interval Subset of REAL
for f being Function of A, REAL st f is_bounded_on A & f is_integrable_on A & ( for x being Real st x in A holds
f . x >= 0 ) holds
integral f >= 0

proof end;

theorem Th33: :: INTEGRA2:33

for A being closed-interval Subset of REAL
for f, g being Function of A, REAL st f is_bounded_on A & f is_integrable_on A & g is_bounded_on A & g is_integrable_on A holds
( f - g is_integrable_on A & integral (f - g) = (integral f) - (integral g) )

proof end;

theorem :: INTEGRA2:34

for A being closed-interval Subset of REAL
for f, g being Function of A, REAL st f is_bounded_on A & f is_integrable_on A & g is_bounded_on A & g is_integrable_on A & ( for x being Real st x in A holds
f . x >= g . x ) holds
integral f >= integral g

proof end;

theorem :: INTEGRA2:35

for A being closed-interval Subset of REAL
for f being Function of A, REAL st f is_bounded_on A holds
rng (upper_sum_set f) is bounded_below

proof end;

theorem :: INTEGRA2:36

for A being closed-interval Subset of REAL
for f being Function of A, REAL st f is_bounded_on A holds
rng (lower_sum_set f) is bounded_above

proof end;

definition

let A be closed-interval Subset of REAL ;
mode DivSequence of A is Function of NAT , divs A;

end;

definition

let A be closed-interval Subset of REAL ;
let T be DivSequence of A;
func delta T -> Real_Sequence means :: INTEGRA2:def 3
for i being Nat holds it . i = delta (T . i);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines delta INTEGRA2:def 3 :

definition

let A be closed-interval Subset of REAL ;
let f be PartFunc of A, REAL ;
let T be DivSequence of A;
func upper_sum f,T -> Real_Sequence means :: INTEGRA2:def 4
for i being Nat holds it . i = upper_sum f,(T . i);
existence

proof end;

uniqueness

proof end;

func lower_sum f,T -> Real_Sequence means :: INTEGRA2:def 5
for i being Nat holds it . i = lower_sum f,(T . i);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines upper_sum INTEGRA2:def 4 :

:: deftheorem defines lower_sum INTEGRA2:def 5 :

theorem Th37: :: INTEGRA2:37

for A being closed-interval Subset of REAL
for D1, D2 being Element of divs A st D1 <= D2 holds
for j being Nat st j in dom D2 holds
ex i being Nat st
( i in dom D1 & divset D2,j c= divset D1,i )

proof end;

theorem :: INTEGRA2:38

for X, Y being non empty finite Subset of REAL st X c= Y holds
max X <= max Y

proof end;

theorem Th39: :: INTEGRA2:39

for X, Y being non empty finite Subset of REAL st ex y being Real st
( y in Y & max X <= y ) holds
max X <= max Y

proof end;

theorem Th40: :: INTEGRA2:40

for A, B being closed-interval Subset of REAL st A c= B holds
vol A <= vol B

proof end;

theorem :: INTEGRA2:41

for A being closed-interval Subset of REAL
for D1, D2 being Element of divs A st D1 <= D2 holds
delta D1 >= delta D2

proof end;