:: Darboux's Theorem
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received December 7, 1999
:: Copyright (c) 1999 Association of Mizar Users
Lm1:
for a being Real
for p being FinSequence of REAL st a in dom p holds
( 1 <= a & a <= len p )
by FINSEQ_3:27;
Lm2:
for j being Element of NAT holds (j -' j) + 1 = 1
Lm3:
for n being Element of NAT st 1 <= n & n <= 2 & not n = 1 holds
n = 2
theorem Th1: :: INTEGRA3:1
theorem Th2: :: INTEGRA3:2
theorem Th3: :: INTEGRA3:3
theorem Th4: :: INTEGRA3:4
theorem Th5: :: INTEGRA3:5
theorem Th6: :: INTEGRA3:6
theorem Th7: :: INTEGRA3:7
theorem Th8: :: INTEGRA3:8
Lm4:
for A being closed-interval Subset of REAL
for g being Function of A, REAL st g | A is bounded holds
upper_bound (rng g) >= lower_bound (rng g)
Lm5:
for A, B being closed-interval Subset of REAL
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) )
Lm6:
for j being Element of NAT
for A being closed-interval Subset of REAL
for D1 being Element of divs A st j in dom D1 holds
vol (divset D1,j) <= delta D1
Lm7:
for x being Real
for A being closed-interval Subset of REAL
for j1 being Element of NAT
for D1, D2 being Element of divs A 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: :: INTEGRA3:9
theorem Th10: :: INTEGRA3:10
Lm8:
for y being Real
for A being closed-interval Subset of REAL
for f being PartFunc of A, REAL st vol A <> 0 & y in rng (lower_sum_set f) holds
ex D being Element of divs A st
( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A )
theorem Th11: :: INTEGRA3:11
for
A being
closed-interval Subset of
REAL for
D being
Element of
divs A for
r being
Real for
i,
j being
Element of
NAT 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
REAL 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
DivisionPoint of
B )
Lm9:
for A being closed-interval Subset of REAL
for D1 being Element of divs A st vol A <> 0 & len D1 = 1 holds
<*(lower_bound A)*> ^ D1 is non empty increasing FinSequence of REAL
Lm10:
for A being closed-interval Subset of REAL
for D2 being Element of divs A st lower_bound A < D2 . 1 holds
<*(lower_bound A)*> ^ D2 is non empty increasing FinSequence of REAL
Lm11:
for A being closed-interval Subset of REAL
for f being PartFunc of A, REAL
for D1, MD1 being Element of divs 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 )
Lm12:
for A being closed-interval Subset of REAL
for D2, MD2 being Element of divs A st MD2 = <*(lower_bound A)*> ^ D2 holds
vol (divset MD2,1) = 0
Lm13:
for A being closed-interval Subset of REAL
for f being Function of A, REAL
for D1, MD1 being Element of divs A st MD1 = <*(lower_bound A)*> ^ D1 holds
delta MD1 = delta D1
theorem Th12: :: INTEGRA3:12
theorem Th13: :: INTEGRA3:13
theorem Th14: :: INTEGRA3:14
for
A being
closed-interval Subset of
REAL for
D1,
D2 being
Element of
divs A for
r being
Real for
i,
j being
Element of
NAT 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
REAL ex
MD1,
MD2 being
Element of
divs 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: :: INTEGRA3:15
theorem Th16: :: INTEGRA3:16
theorem Th17: :: INTEGRA3:17
theorem Th18: :: INTEGRA3:18
theorem :: INTEGRA3:19
theorem :: INTEGRA3:20