:: Gauge Integral
:: by Roland Coghetto
::
:: Received September 3, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users

theorem Th01: :: COUSIN2:1

for a, b, c being Real st a - b <= c & b <= a holds
|.(b - a).| <= c

proof end;

theorem Th02: :: COUSIN2:2

for a, b, c being Real st b - a <= c & a <= b holds
|.(b - a).| <= c

proof end;

Lm01: for a, b, c, d being Real st a <= b + c & b <= d holds
a <= d + c

proof end;

Lm02: for a, b, c, d being Real st a < b + c & b - c < d holds
a - d < 2 * c

proof end;

theorem Th03: :: COUSIN2:3

for a, b, c, d, e being Real st a <= b & b <= c & |.(a - d).| <= e & |.(c - d).| <= e holds
|.(b - d).| <= e

proof end;

theorem Th04: :: COUSIN2:4

for a, b being Real st ( for c being Real st 0 < c holds
|.(a - b).| <= c ) holds
a = b

proof end;

theorem Th05: :: COUSIN2:5

for e being Real
for b, c, d being non negative Real st d < e / ((2 * b) * |.c.|) holds
( b is positive & c is positive )

proof end;

theorem Th06: :: COUSIN2:6

for a, b being Real st a <> 0 holds
a * (b / (2 * a)) = b / 2

proof end;

theorem Th07: :: COUSIN2:7

for a, e being Real
for b, c, d being non negative Real st a <= (b * c) * d & d < e / ((2 * b) * |.c.|) holds
a <= e / 2

proof end;

definition

let X be non empty set ;
let f, g be Function of X,REAL;

func min (f,g) -> Function of X,REAL means :DEFM1: :: COUSIN2:def 1
for x being Element of X holds it . x = min ((f . x),(g . x));

existence
ex b₁ being Function of X,REAL st
for x being Element of X holds b₁ . x = min ((f . x),(g . x))

proof end;

uniqueness
for b₁, b₂ being Function of X,REAL st ( for x being Element of X holds b₁ . x = min ((f . x),(g . x)) ) & ( for x being Element of X holds b₂ . x = min ((f . x),(g . x)) ) holds
b₁ = b₂

proof end;

commutativity
for b₁, f, g being Function of X,REAL st ( for x being Element of X holds b₁ . x = min ((f . x),(g . x)) ) holds
for x being Element of X holds b₁ . x = min ((g . x),(f . x)) ;

func max (f,g) -> Function of X,REAL means :DEFM2: :: COUSIN2:def 2
for x being Element of X holds it . x = max ((f . x),(g . x));

existence
ex b₁ being Function of X,REAL st
for x being Element of X holds b₁ . x = max ((f . x),(g . x))

proof end;

uniqueness
for b₁, b₂ being Function of X,REAL st ( for x being Element of X holds b₁ . x = max ((f . x),(g . x)) ) & ( for x being Element of X holds b₂ . x = max ((f . x),(g . x)) ) holds
b₁ = b₂

proof end;

commutativity
for b₁, f, g being Function of X,REAL st ( for x being Element of X holds b₁ . x = max ((f . x),(g . x)) ) holds
for x being Element of X holds b₁ . x = max ((g . x),(f . x)) ;

end;

:: deftheorem DEFM1 defines min COUSIN2:def 1 :
for X being non empty set
for f, g, b₄ being Function of X,REAL holds
( b₄ = min (f,g) iff for x being Element of X holds b₄ . x = min ((f . x),(g . x)) );

:: deftheorem DEFM2 defines max COUSIN2:def 2 :
for X being non empty set
for f, g, b₄ being Function of X,REAL holds
( b₄ = max (f,g) iff for x being Element of X holds b₄ . x = max ((f . x),(g . x)) );

registration

let X be non empty set ;
let f, g be positive-yielding Function of X,REAL;

cluster min (f,g) -> positive-yielding ;

coherence
min (f,g) is positive-yielding

proof end;

end;

registration

let X be non empty set ;
let f, g be positive-yielding Function of X,REAL;

cluster max (f,g) -> positive-yielding ;

coherence
max (f,g) is positive-yielding

proof end;

end;

definition

let X be non empty set ;
let f, g be Function of X,REAL;

pred f <= g means :: COUSIN2:def 3
for x being Element of X holds f . x <= g . x;

end;

:: deftheorem defines <= COUSIN2:def 3 :
for X being non empty set
for f, g being Function of X,REAL holds
( f <= g iff for x being Element of X holds f . x <= g . x );

theorem Th08: :: COUSIN2:8

for X being non empty set
for f, g being Function of X,REAL holds min (f,g) <= f

proof end;

Lm03: for X being non empty set st ex s being object st
for r being object st r in X holds
s = r holds
ex r being object st X = {r}

proof end;

theorem Th09: :: COUSIN2:9

for X being non empty real-membered set st ( for r being Real st r in X holds
upper_bound X = r ) holds
ex r being Real st X = {r}

proof end;

theorem :: COUSIN2:10

for X being non empty real-membered set st ( for r being Real st r in X holds
lower_bound X = r ) holds
ex r being Real st X = {r}

proof end;

theorem Th10: :: COUSIN2:11

for X being non empty real-membered bounded_below bounded_above set st upper_bound X = lower_bound X holds
ex r being Real st X = {r}

proof end;

theorem Th11: :: COUSIN2:12

for X, Y being set holds chi (X,Y) is Function of Y,REAL

proof end;

theorem :: COUSIN2:13

for r being Real
for s being ExtReal
for A being Subset of REAL st A c= ].r,s.[ holds
A is bounded_below

proof end;

theorem :: COUSIN2:14

for r being Real
for s being ExtReal
for A being Subset of REAL st A c= ].s,r.[ holds
A is bounded_above

proof end;

theorem Th12: :: COUSIN2:15

for a, b being Real
for f being real-valued Function st rng f c= [.a,b.] holds
f is bounded

proof end;

theorem Th13: :: COUSIN2:16

for a, b being Real st a <= b holds
{a,b} c= [.a,b.]

proof end;

theorem Th14: :: COUSIN2:17

for X, Y being set holds chi (X,Y) is bounded

proof end;

theorem Th15: :: COUSIN2:18

for X, Y being set st X misses Y holds
for x being Element of X holds (chi (Y,X)) . x = 0

proof end;

theorem Th16: :: COUSIN2:19

for Z being non empty set
for f being Function of Z,REAL holds
( f is constant iff ex r being Real st f = r (#) (chi (Z,Z)) )

proof end;

theorem Th17: :: COUSIN2:20

for X being set holds chi (X,X) is positive-yielding

proof end;

theorem Th18: :: COUSIN2:21

for I being non empty closed_interval Subset of REAL
for D being Division of I
for f being PartFunc of I,REAL st f is lower_integrable holds
lower_sum (f,D) <= lower_integral f

proof end;

theorem Th19: :: COUSIN2:22

for I being non empty closed_interval Subset of REAL
for D being Division of I
for f being PartFunc of I,REAL st f is upper_integrable holds
upper_integral f <= upper_sum (f,D)

proof end;

definition

let A be non empty closed_interval Subset of REAL;

func tagged_divs A -> set means :Def1: :: COUSIN2:def 4
for x being set holds
( x in it iff x is tagged_division of A );

existence
ex b₁ being set st
for x being set holds
( x in b₁ iff x is tagged_division of A )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being set holds
( x in b₁ iff x is tagged_division of A ) ) & ( for x being set holds
( x in b₂ iff x is tagged_division of A ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines tagged_divs COUSIN2:def 4 :
for A being non empty closed_interval Subset of REAL
for b₂ being set holds
( b₂ = tagged_divs A iff for x being set holds
( x in b₂ iff x is tagged_division of A ) );

registration

let A be non empty closed_interval Subset of REAL;

cluster tagged_divs A -> non empty ;

coherence
not tagged_divs A is empty

proof end;

end;

definition

let A be non empty closed_interval Subset of REAL;
let TD be tagged_division of A;

func tagged_of TD -> non empty non-decreasing FinSequence of REAL means :Def2: :: COUSIN2:def 5
ex D being Division of A ex T being Element of set_of_tagged_Division D st
( it = T & TD = [D,T] );

existence
ex b₁ being non empty non-decreasing FinSequence of REAL ex D being Division of A ex T being Element of set_of_tagged_Division D st
( b₁ = T & TD = [D,T] )

proof end;

uniqueness
for b₁, b₂ being non empty non-decreasing FinSequence of REAL st ex D being Division of A ex T being Element of set_of_tagged_Division D st
( b₁ = T & TD = [D,T] ) & ex D being Division of A ex T being Element of set_of_tagged_Division D st
( b₂ = T & TD = [D,T] ) holds
b₁ = b₂ by XTUPLE_0:1;

end;

:: deftheorem Def2 defines tagged_of COUSIN2:def 5 :
for A being non empty closed_interval Subset of REAL
for TD being tagged_division of A
for b₃ being non empty non-decreasing FinSequence of REAL holds
( b₃ = tagged_of TD iff ex D being Division of A ex T being Element of set_of_tagged_Division D st
( b₃ = T & TD = [D,T] ) );

theorem Th20: :: COUSIN2:23

for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for D being Division of I
for T being Element of set_of_tagged_Division D st TD = [D,T] holds
( T = tagged_of TD & D = division_of TD )

proof end;

theorem Th21: :: COUSIN2:24

for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I holds len (tagged_of TD) = len (division_of TD)

proof end;

definition

let A be non empty closed_interval Subset of REAL;
let TD be tagged_division of A;

func len TD -> Element of NAT equals :: COUSIN2:def 6
len (division_of TD);

coherence
len (division_of TD) is Element of NAT ;

func dom TD -> set equals :: COUSIN2:def 7
dom (division_of TD);

coherence
dom (division_of TD) is set ;

end;

:: deftheorem defines len COUSIN2:def 6 :
for A being non empty closed_interval Subset of REAL
for TD being tagged_division of A holds len TD = len (division_of TD);

:: deftheorem defines dom COUSIN2:def 7 :
for A being non empty closed_interval Subset of REAL
for TD being tagged_division of A holds dom TD = dom (division_of TD);

theorem Th22: :: COUSIN2:25

for I being non empty closed_interval Subset of REAL
for D being Division of I
for T being Element of set_of_tagged_Division D holds rng T c= I

proof end;

theorem Th23: :: COUSIN2:26

for I being non empty closed_interval Subset of REAL
for jauge1, jauge2 being positive-yielding Function of I,REAL
for TD being b₂ -fine tagged_division of I st jauge1 <= jauge2 holds
TD is b₃ -fine tagged_division of I

proof end;

definition

let I be non empty closed_interval Subset of REAL;
let f be PartFunc of I,REAL;
let TD be tagged_division of I;

func tagged_volume (f,TD) -> FinSequence of REAL means :Def4: :: COUSIN2:def 8
( len it = len TD & ( for i being Nat st i in dom TD holds
it . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) ) );

existence
ex b₁ being FinSequence of REAL st
( len b₁ = len TD & ( for i being Nat st i in dom TD holds
b₁ . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of REAL st len b₁ = len TD & ( for i being Nat st i in dom TD holds
b₁ . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) ) & len b₂ = len TD & ( for i being Nat st i in dom TD holds
b₂ . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines tagged_volume COUSIN2:def 8 :
for I being non empty closed_interval Subset of REAL
for f being PartFunc of I,REAL
for TD being tagged_division of I
for b₄ being FinSequence of REAL holds
( b₄ = tagged_volume (f,TD) iff ( len b₄ = len TD & ( for i being Nat st i in dom TD holds
b₄ . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) ) ) );

definition

let I be non empty closed_interval Subset of REAL;
let f be PartFunc of I,REAL;
let TD be tagged_division of I;

func tagged_sum (f,TD) -> Real equals :: COUSIN2:def 9
Sum (tagged_volume (f,TD));

coherence
Sum (tagged_volume (f,TD)) is Real ;

end;

:: deftheorem defines tagged_sum COUSIN2:def 9 :
for I being non empty closed_interval Subset of REAL
for f being PartFunc of I,REAL
for TD being tagged_division of I holds tagged_sum (f,TD) = Sum (tagged_volume (f,TD));

theorem Th24: :: COUSIN2:27

for X, Y being set st Y c= X holds
chi (X,Y) = chi (Y,Y)

proof end;

theorem Th25: :: COUSIN2:28

for I being non empty closed_interval Subset of REAL st not I is empty & I is trivial holds
vol I = 0

proof end;

theorem Th26: :: COUSIN2:29

for I being non empty closed_interval Subset of REAL
for r being Real st I = {r} holds
for D being Division of I holds D = <*r*>

proof end;

Lm04: for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for f being Function of I,REAL st f = chi (I,I) holds
tagged_sum (f,TD) = vol I

proof end;

definition

let I be non empty closed_interval Subset of REAL;
let f be Function of I,REAL;

attr f is HK-integrable means :: COUSIN2:def 10
ex J being Real st
for epsilon being Real st epsilon > 0 holds
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (f,TD)) - J).| <= epsilon;

end;

:: deftheorem defines HK-integrable COUSIN2:def 10 :
for I being non empty closed_interval Subset of REAL
for f being Function of I,REAL holds
( f is HK-integrable iff ex J being Real st
for epsilon being Real st epsilon > 0 holds
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (f,TD)) - J).| <= epsilon );

definition

let I be non empty closed_interval Subset of REAL;
let f be Function of I,REAL;
assume A1: f is HK-integrable ;

func HK-integral f -> Real means :DEFCC: :: COUSIN2:def 11
for epsilon being Real st epsilon > 0 holds
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (f,TD)) - it).| <= epsilon;

existence
ex b₁ being Real st
for epsilon being Real st epsilon > 0 holds
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (f,TD)) - b₁).| <= epsilon by A1;
uniqueness
for b₁, b₂ being Real st ( for epsilon being Real st epsilon > 0 holds
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (f,TD)) - b₁).| <= epsilon ) & ( for epsilon being Real st epsilon > 0 holds
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (f,TD)) - b₂).| <= epsilon ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DEFCC defines HK-integral COUSIN2:def 11 :
for I being non empty closed_interval Subset of REAL
for f being Function of I,REAL st f is HK-integrable holds
for b₃ being Real holds
( b₃ = HK-integral f iff for epsilon being Real st epsilon > 0 holds
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (f,TD)) - b₃).| <= epsilon );

theorem Th27: :: COUSIN2:30

for I being non empty closed_interval Subset of REAL
for f being Function of I,REAL st I is trivial holds
( f is HK-integrable & HK-integral f = 0 )

proof end;

theorem Th28: :: COUSIN2:31

for A being Subset of REAL
for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for f being Function of I,REAL st A misses I & f = chi (A,I) holds
tagged_sum (f,TD) = 0

proof end;

theorem Th29: :: COUSIN2:32

for A being Subset of REAL
for I being non empty closed_interval Subset of REAL
for f being Function of I,REAL st A misses I & f = chi (A,I) holds
( f is HK-integrable & HK-integral f = 0 )

proof end;

theorem Th30: :: COUSIN2:33

for A being Subset of REAL
for I being non empty closed_interval Subset of REAL
for f being Function of I,REAL st I c= A & f = chi (A,I) holds
( f is HK-integrable & HK-integral f = vol I )

proof end;

registration

let I be non empty closed_interval Subset of REAL;

cluster V1() V4(I) V5( REAL ) Function-like non empty total V55(I, REAL ) complex-valued ext-real-valued real-valued HK-integrable for Element of bool [:I,REAL:];

existence
ex b₁ being Function of I,REAL st b₁ is HK-integrable

proof end;

end;

theorem Th31: :: COUSIN2:34

for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for f being HK-integrable Function of I,REAL
for r being Real
for i being Nat st i in dom TD holds
(tagged_volume ((r (#) f),TD)) . i = (r * (f . ((tagged_of TD) . i))) * (vol (divset ((division_of TD),i)))

proof end;

theorem Th32: :: COUSIN2:35

for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for f being HK-integrable Function of I,REAL
for r being Real holds tagged_volume ((r (#) f),TD) = r * (tagged_volume (f,TD))

proof end;

theorem Th33: :: COUSIN2:36

for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for f, g being HK-integrable Function of I,REAL
for i being Nat st i in dom TD holds
(tagged_volume ((f + g),TD)) . i = ((f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i)))) + ((g . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))))

proof end;

theorem Th34: :: COUSIN2:37

for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for f, g being HK-integrable Function of I,REAL holds tagged_volume ((f + g),TD) = (tagged_volume (f,TD)) + (tagged_volume (g,TD))

proof end;

theorem Th35: :: COUSIN2:38

for I being non empty closed_interval Subset of REAL
for f being HK-integrable Function of I,REAL
for r being Real st f is HK-integrable holds
( r (#) f is HK-integrable Function of I,REAL & HK-integral (r (#) f) = r * (HK-integral f) )

proof end;

theorem :: COUSIN2:39

for I being non empty closed_interval Subset of REAL
for f, g being HK-integrable Function of I,REAL holds
( f + g is HK-integrable Function of I,REAL & HK-integral (f + g) = (HK-integral f) + (HK-integral g) )

proof end;

theorem Th36: :: COUSIN2:40

for I being non empty closed_interval Subset of REAL
for f being Function of I,REAL st f is constant holds
( f is HK-integrable & ex r being Real st
( f = r (#) (chi (I,I)) & HK-integral f = r * (vol I) ) )

proof end;

registration

let I be non empty closed_interval Subset of REAL;

cluster V1() V4(I) V5( REAL ) Function-like non empty total V55(I, REAL ) complex-valued ext-real-valued real-valued integrable for Element of bool [:I,REAL:];

existence
ex b₁ being Function of I,REAL st b₁ is integrable

proof end;

end;

registration

let X be non empty set ;

cluster V1() V4(X) V5( REAL ) Function-like non empty total V55(X, REAL ) complex-valued ext-real-valued real-valued bounded for Element of bool [:X,REAL:];

existence
ex b₁ being Function of X,REAL st b₁ is bounded

proof end;

end;

theorem Th37: :: COUSIN2:41

for I being non empty closed_interval Subset of REAL
for f being bounded Function of I,REAL holds
( |.((upper_bound (rng f)) - (lower_bound (rng f))).| = 0 iff f is constant )

proof end;

registration

let I be non empty closed_interval Subset of REAL;

cluster V1() V4(I) V5( REAL ) Function-like non empty total V55(I, REAL ) complex-valued ext-real-valued real-valued bounded integrable for Element of bool [:I,REAL:];

existence
ex b₁ being integrable Function of I,REAL st b₁ is bounded

proof end;

end;

theorem :: COUSIN2:42

for I being non empty closed_interval Subset of REAL
for f being PartFunc of I,REAL st f is upper_integrable holds
ex r being Real st
for D being Division of I holds r < upper_sum (f,D)

proof end;

theorem :: COUSIN2:43

for I being non empty closed_interval Subset of REAL
for f being PartFunc of I,REAL st f is lower_integrable holds
ex r being Real st
for D being Division of I holds lower_sum (f,D) < r

proof end;

theorem Th38: :: COUSIN2:44

for I being non empty closed_interval Subset of REAL
for f being Function of I,REAL
for D, D1 being Division of I st D . 1 = lower_bound I & D1 = D /^ 1 holds
( upper_sum (f,D1) = upper_sum (f,D) & lower_sum (f,D1) = lower_sum (f,D) )

proof end;

theorem Th39: :: COUSIN2:45

for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for f being bounded integrable Function of I,REAL
for i being Nat st i in dom TD holds
( (lower_volume (f,(division_of TD))) . i <= (tagged_volume (f,TD)) . i & (tagged_volume (f,TD)) . i <= (upper_volume (f,(division_of TD))) . i )

proof end;

theorem Th40: :: COUSIN2:46

for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for f being bounded integrable Function of I,REAL holds
( Sum (lower_volume (f,(division_of TD))) <= Sum (tagged_volume (f,TD)) & Sum (tagged_volume (f,TD)) <= Sum (upper_volume (f,(division_of TD))) )

proof end;

theorem Th41: :: COUSIN2:47

for I being non empty closed_interval Subset of REAL
for f being bounded integrable Function of I,REAL
for epsilon being Real st not I is trivial & 0 < epsilon holds
ex D being Division of I st
( D . 1 <> lower_bound I & upper_sum (f,D) < (integral f) + (epsilon / 2) & (integral f) - (epsilon / 2) < lower_sum (f,D) & (upper_sum (f,D)) - (lower_sum (f,D)) < epsilon )

proof end;

theorem :: COUSIN2:48

for I being non empty closed_interval Subset of REAL
for r being Real
for jauge being positive-yielding Function of I,REAL st jauge = r (#) (chi (I,I)) holds
0 < r

proof end;

theorem Th42: :: COUSIN2:49

for I being non empty closed_interval Subset of REAL
for r being Real
for jauge being positive-yielding Function of I,REAL
for D being tagged_division of I st jauge = r (#) (chi (I,I)) & D is jauge -fine holds
delta (division_of D) <= r

proof end;

theorem Th43: :: COUSIN2:50

for I being non empty closed_interval Subset of REAL
for D being Division of I
for fc being Function of I,REAL ex i being Nat st
( i in dom D & min (rng (upper_volume (fc,D))) = (upper_volume (fc,D)) . i )

proof end;

theorem Th44: :: COUSIN2:51

for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for jauge being positive-yielding Function of I,REAL
for r1, r2, s being Real
for D1 being Division of I
for fc, f being Function of I,REAL
for epsilon being Real st fc = chi (I,I) & r1 = min (rng (upper_volume (fc,D1))) & r2 = epsilon / ((2 * (len D1)) * |.((upper_bound (rng f)) - (lower_bound (rng f))).|) & 0 < r1 & 0 < r2 & s = (min (r1,r2)) / 2 & jauge = s (#) fc & TD is jauge -fine holds
( delta (division_of TD) < min (rng (upper_volume (fc,D1))) & delta (division_of TD) < epsilon / ((2 * (len D1)) * |.((upper_bound (rng f)) - (lower_bound (rng f))).|) )

proof end;

theorem Th45: :: COUSIN2:52

for r being Real
for p being FinSequence of REAL st ( for i being Nat st i in dom p holds
r <= p . i ) & ex i0 being Nat st
( i0 in dom p & p . i0 = r ) holds
r = inf (rng p)

proof end;

theorem Th46: :: COUSIN2:53

for I being non empty closed_interval Subset of REAL
for D being Division of I
for fc being Function of I,REAL st fc = chi (I,I) holds
( 0 <= min (rng (upper_volume (fc,D))) & ( 0 = min (rng (upper_volume (fc,D))) implies divset (D,1) = [.(D . 1),(D . 1).] ) & ( divset (D,1) = [.(D . 1),(D . 1).] implies 0 = min (rng (upper_volume (fc,D))) ) )

proof end;

theorem Th47: :: COUSIN2:54

for I being non empty closed_interval Subset of REAL
for D being Division of I st divset (D,1) = [.(D . 1),(D . 1).] holds
D . 1 = lower_bound I

proof end;

theorem Th48: :: COUSIN2:55

for I being non empty closed_interval Subset of REAL
for f being bounded integrable Function of I,REAL holds
( f is HK-integrable & HK-integral f = integral f )

proof end;

registration

let I be non empty closed_interval Subset of REAL;

cluster Function-like V55(I, REAL ) bounded integrable -> HK-integrable for Element of bool [:I,REAL:];

coherence
for b₁ being Function of I,REAL st b₁ is bounded & b₁ is integrable holds
b₁ is HK-integrable by Th48;

end;