begin
Lm1:
for j being Element of NAT holds (j -' j) + 1 = 1
Lm2:
for n being Element of NAT st 1 <= n & n <= 2 & not n = 1 holds
n = 2
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
Lm3:
for A being closed-interval Subset of
for g being Function of A, REAL st g | A is bounded holds
upper_bound (rng g) >= lower_bound (rng g)
Lm4:
for A, B being closed-interval Subset of
for f being Function of A, REAL st f | A is bounded & B c= A holds
( lower_bound (rng (f | B)) >= lower_bound (rng f) & lower_bound (rng f) <= upper_bound (rng (f | B)) & upper_bound (rng (f | B)) <= upper_bound (rng f) & lower_bound (rng (f | B)) <= upper_bound (rng f) )
Lm5:
for j being Element of NAT
for A being closed-interval Subset of
for D1 being Division of A st j in dom D1 holds
vol (divset D1,j) <= delta D1
Lm6:
for x being Real
for A being closed-interval Subset of
for D1, D2 being Division of A
for j1 being Element of NAT st j1 = (len D1) - 1 & x in divset D1,(len D1) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} holds
rng (D2 | (indx D2,D1,j1)) = rng (D1 | j1)
theorem Th9:
theorem Th10:
Lm7:
for y being Real
for A being closed-interval Subset of
for f being Function of A, REAL st vol A <> 0 & y in rng (lower_sum_set f) holds
ex D being Division of A st
( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A )
theorem Th11:
for
r being
Real for
i,
j being
Element of
NAT for
A being
closed-interval Subset of
for
D being
Division of
A st
i in dom D &
j in dom D &
i <= j &
r < (mid D,i,j) . 1 holds
ex
B being
closed-interval Subset of st
(
r = lower_bound B &
upper_bound B = (mid D,i,j) . (len (mid D,i,j)) &
len (mid D,i,j) = (j - i) + 1 &
mid D,
i,
j is
Division of
B )
Lm8:
for A being closed-interval Subset of
for D1 being Division of A st vol A <> 0 & len D1 = 1 holds
<*(lower_bound A)*> ^ D1 is non empty increasing FinSequence of REAL
Lm9:
for A being closed-interval Subset of
for D2 being Division of A st lower_bound A < D2 . 1 holds
<*(lower_bound A)*> ^ D2 is non empty increasing FinSequence of REAL
Lm10:
for A being closed-interval Subset of
for D1 being Division of A
for f being Function of A, REAL
for MD1 being Division of A st MD1 = <*(lower_bound A)*> ^ D1 holds
( ( for i being Element of NAT st i in Seg (len D1) holds
divset MD1,(i + 1) = divset D1,i ) & upper_volume f,D1 = (upper_volume f,MD1) /^ 1 & lower_volume f,D1 = (lower_volume f,MD1) /^ 1 )
Lm11:
for A being closed-interval Subset of
for D2, MD2 being Division of A st MD2 = <*(lower_bound A)*> ^ D2 holds
vol (divset MD2,1) = 0
Lm12:
for A being closed-interval Subset of
for D1, MD1 being Division of A st MD1 = <*(lower_bound A)*> ^ D1 holds
delta MD1 = delta D1
theorem Th12:
theorem Th13:
theorem Th14:
for
r being
Real for
i,
j being
Element of
NAT for
A being
closed-interval Subset of
for
D1,
D2 being
Division of
A st
i in dom D1 &
j in dom D1 &
i <= j &
D1 <= D2 &
r < (mid D2,(indx D2,D1,i),(indx D2,D1,j)) . 1 holds
ex
B being
closed-interval Subset of ex
MD1,
MD2 being
Division of
B st
(
r = lower_bound B &
upper_bound B = MD2 . (len MD2) &
upper_bound B = MD1 . (len MD1) &
MD1 <= MD2 &
MD1 = mid D1,
i,
j &
MD2 = mid D2,
(indx D2,D1,i),
(indx D2,D1,j) )
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
begin
theorem
theorem