let A be closed-interval Subset of REAL ; :: thesis: 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 )
let f be PartFunc of A,REAL ; :: thesis: for D being Element of divs A st vol A = 0 holds
( f is lower_integrable & lower_integral f = 0 )
let D be Element of divs A; :: thesis: ( vol A = 0 implies ( f is lower_integrable & lower_integral f = 0 ) )
assume A1:
vol A = 0
; :: thesis: ( f is lower_integrable & lower_integral f = 0 )
(divs A) /\ (dom (lower_sum_set f)) = (divs A) /\ (divs A)
by INTEGRA1:def 12;
then A2:
divs A meets dom (lower_sum_set f)
by XBOOLE_0:def 7;
A3:
for D1 being Element of divs A st D1 in (divs A) /\ (dom (lower_sum_set f)) holds
(lower_sum_set f) /. D1 = 0
proof
let D1 be
Element of
divs A;
:: thesis: ( D1 in (divs A) /\ (dom (lower_sum_set f)) implies (lower_sum_set f) /. D1 = 0 )
assume
D1 in (divs A) /\ (dom (lower_sum_set f))
;
:: thesis: (lower_sum_set f) /. D1 = 0
then A4:
D1 in dom (lower_sum_set f)
by XBOOLE_0:def 4;
reconsider D2 =
D1 as
Division of
A by INTEGRA1:def 3;
A5:
(lower_sum_set f) /. D1 =
(lower_sum_set f) . D1
by A4, PARTFUN1:def 8
.=
lower_sum f,
D2
by A4, INTEGRA1:def 12
.=
Sum (lower_volume f,D2)
by INTEGRA1:def 10
;
lower_volume f,
D2 = <*0 *>
proof
A6:
len (lower_volume f,D2) =
len D2
by INTEGRA1:def 8
.=
1
by A1, Th1
;
rng D2 <> {}
;
then A7:
(
len D2 = 1 & 1
in dom D2 )
by A1, Th1, FINSEQ_3:34;
A8:
divset D2,1
= A
proof
A9:
upper_bound (divset D2,(len D2)) =
D2 . (len D2)
by A7, INTEGRA1:def 5
.=
upper_bound A
by INTEGRA1:def 2
;
divset D2,1 =
[.(lower_bound (divset D2,(len D2))),(upper_bound (divset D2,(len D2))).]
by A7, INTEGRA1:5
.=
[.(lower_bound A),(upper_bound A).]
by A7, A9, INTEGRA1:def 5
;
hence
divset D2,1
= A
by INTEGRA1:5;
:: thesis: verum
end;
1
in Seg (len D2)
by A7, FINSEQ_1:3;
then
1
in dom D2
by FINSEQ_1:def 3;
then (lower_volume f,D2) . 1 =
(lower_bound (rng (f | (divset D2,1)))) * (vol A)
by A8, INTEGRA1:def 8
.=
0
by A1
;
hence
lower_volume f,
D2 = <*0 *>
by A6, FINSEQ_1:57;
:: thesis: verum
end;
hence
(lower_sum_set f) /. D1 = 0
by A5, FINSOP_1:12;
:: thesis: verum
end;
then
(lower_sum_set f) | (divs A) is constant
by PARTFUN2:54;
then consider x being Element of REAL such that
A10:
rng ((lower_sum_set f) | (divs A)) = {x}
by A2, PARTFUN2:56;
A11:
rng ((lower_sum_set f) | (divs A)) c= rng (lower_sum_set f)
by RELAT_1:99;
A12:
rng (lower_sum_set f) c= rng ((lower_sum_set f) | (divs A))
then A15:
rng (lower_sum_set f) = {x}
by A10, A11, XBOOLE_0:def 10;
then
rng (lower_sum_set f) is bounded
;
then
rng (lower_sum_set f) is bounded_above
;
hence
f is lower_integrable
by INTEGRA1:def 14; :: thesis: lower_integral f = 0
x = 0
then
upper_bound (rng (lower_sum_set f)) = 0
by A15, SEQ_4:22;
hence
lower_integral f = 0
by INTEGRA1:def 16; :: thesis: verum