:: INTEGRA3 semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
Lm1:
for a being Real
for p being FinSequence of REAL st a in dom p holds
( 1 <= a & a <= len p )
Lm2:
for a being Real holds a - 1 <= a
by XREAL_1:148;
Lm3:
for j being Nat holds (j -' j) + 1 = 1
Lm4:
for n being Nat st 1 <= n & n <= 2 & not n = 1 holds
n = 2
theorem Th1: :: INTEGRA3:1
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th2: :: INTEGRA3:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th3: :: INTEGRA3:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th4: :: INTEGRA3:4
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th5: :: INTEGRA3:5
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th6: :: INTEGRA3:6
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th7: :: INTEGRA3:7
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th8: :: INTEGRA3:8
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
Lm5:
for A being closed-interval Subset of REAL
for g being Function of A, REAL st g is_bounded_on A holds
sup (rng g) >= inf (rng g)
Lm6:
for A, B being closed-interval Subset of REAL
for f being Function of A, REAL st f is_bounded_on A & B c= A holds
( inf (rng (f | B)) >= inf (rng f) & inf (rng f) <= sup (rng (f | B)) & sup (rng (f | B)) <= sup (rng f) & inf (rng (f | B)) <= sup (rng f) )
Lm7:
for j being 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
Lm8:
for x being Real
for A being closed-interval Subset of REAL
for j1 being 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
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th10: :: INTEGRA3:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
Lm9:
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 > inf A )
theorem Th11: :: INTEGRA3:11
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
A being
closed-interval Subset of
REAL for
D being
Element of
divs A for
r being
Real for
i,
j being
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 = inf B &
sup 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 )
Lm10:
for A being closed-interval Subset of REAL
for D1 being Element of divs A st vol A <> 0 & len D1 = 1 holds
<*(inf A)*> ^ D1 is non empty increasing FinSequence of REAL
Lm11:
for A being closed-interval Subset of REAL
for D2 being Element of divs A st inf A < D2 . 1 holds
<*(inf A)*> ^ D2 is non empty increasing FinSequence of REAL
Lm12:
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 = <*(inf A)*> ^ D1 holds
( ( for i being 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 )
Lm13:
for A being closed-interval Subset of REAL
for D2, MD2 being Element of divs A st MD2 = <*(inf A)*> ^ D2 holds
vol (divset MD2,1) = 0
Lm14:
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 = <*(inf A)*> ^ D1 holds
delta MD1 = delta D1
theorem Th12: :: INTEGRA3:12
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th13: :: INTEGRA3:13
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th14: :: INTEGRA3:14
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
A being
closed-interval Subset of
REAL for
D1,
D2 being
Element of
divs A for
r being
Real for
i,
j being
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 = inf B &
sup B = MD2 . (len MD2) &
sup 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
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th16: :: INTEGRA3:16
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th17: :: INTEGRA3:17
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th18: :: INTEGRA3:18
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: INTEGRA3:19
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: INTEGRA3:20
:: Showing IDV graph ... (Click the Palm Tree again to close it) 