:: Integrability of Bounded Total Functions
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received February 1, 2000
:: Copyright (c) 2000 Association of Mizar Users
theorem Th1: :: INTEGRA4:1
theorem Th2: :: INTEGRA4:2
theorem Th3: :: INTEGRA4:3
theorem Th4: :: INTEGRA4:4
theorem Th5: :: INTEGRA4:5
Lm1:
for A being closed-interval Subset of REAL
for f being PartFunc of A, REAL
for D being Element of divs A st vol A = 0 holds
( f is upper_integrable & upper_integral f = 0 )
Lm2:
for A being closed-interval Subset of REAL
for f being PartFunc of A, REAL
for D being Element of divs A st vol A = 0 holds
( f is lower_integrable & lower_integral f = 0 )
theorem Th6: :: INTEGRA4:6
theorem :: INTEGRA4:7
theorem Th8: :: INTEGRA4:8
theorem Th9: :: INTEGRA4:9
theorem Th10: :: INTEGRA4:10
:: deftheorem Def1 defines divide_into_equal INTEGRA4:def 1 :
Lm3:
for A being closed-interval Subset of REAL
for n being Element of NAT st n > 0 & vol A > 0 holds
ex D being Element of divs A st
( len D = n & ( for i being Element of NAT st i in dom D holds
D . i = (lower_bound A) + (((vol A) / n) * i) ) )
Lm4:
for A being closed-interval Subset of REAL st vol A > 0 holds
ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )
Lm5:
for A being closed-interval Subset of REAL st vol A = 0 holds
ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )
theorem Th11: :: INTEGRA4:11
theorem Th12: :: INTEGRA4:12
theorem Th13: :: INTEGRA4:13
theorem Th14: :: INTEGRA4:14
theorem Th15: :: INTEGRA4:15
theorem Th16: :: INTEGRA4:16
theorem Th17: :: INTEGRA4:17
theorem Th18: :: INTEGRA4:18
theorem Th19: :: INTEGRA4:19
theorem Th20: :: INTEGRA4:20
theorem Th21: :: INTEGRA4:21
theorem Th22: :: INTEGRA4:22
theorem :: INTEGRA4:23
theorem Th24: :: INTEGRA4:24
theorem Th25: :: INTEGRA4:25
theorem Th26: :: INTEGRA4:26
theorem Th27: :: INTEGRA4:27
theorem Th28: :: INTEGRA4:28
theorem :: INTEGRA4:29
theorem :: INTEGRA4:30