:: by Roland Coghetto

::

:: Received September 3, 2017

:: Copyright (c) 2017-2019 Association of Mizar Users

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

|.(b - d).| <= e

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 )

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

( b is positive & c is positive )

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

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;

ex b_{1} being Function of X,REAL st

for x being Element of X holds b_{1} . x = min ((f . x),(g . x))

for b_{1}, b_{2} being Function of X,REAL st ( for x being Element of X holds b_{1} . x = min ((f . x),(g . x)) ) & ( for x being Element of X holds b_{2} . x = min ((f . x),(g . x)) ) holds

b_{1} = b_{2}

for b_{1}, f, g being Function of X,REAL st ( for x being Element of X holds b_{1} . x = min ((f . x),(g . x)) ) holds

for x being Element of X holds b_{1} . x = min ((g . x),(f . x))
;

ex b_{1} being Function of X,REAL st

for x being Element of X holds b_{1} . x = max ((f . x),(g . x))

for b_{1}, b_{2} being Function of X,REAL st ( for x being Element of X holds b_{1} . x = max ((f . x),(g . x)) ) & ( for x being Element of X holds b_{2} . x = max ((f . x),(g . x)) ) holds

b_{1} = b_{2}

for b_{1}, f, g being Function of X,REAL st ( for x being Element of X holds b_{1} . x = max ((f . x),(g . x)) ) holds

for x being Element of X holds b_{1} . x = max ((g . x),(f . x))
;

end;
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 for x being Element of X holds it . x = min ((f . x),(g . x));

ex b

for x being Element of X holds b

proof end;

uniqueness for b

b

proof end;

commutativity for b

for x being Element of X holds b

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 for x being Element of X holds it . x = max ((f . x),(g . x));

ex b

for x being Element of X holds b

proof end;

uniqueness for b

b

proof end;

commutativity for b

for x being Element of X holds b

:: deftheorem DEFM1 defines min COUSIN2:def 1 :

for X being non empty set

for f, g, b_{4} being Function of X,REAL holds

( b_{4} = min (f,g) iff for x being Element of X holds b_{4} . x = min ((f . x),(g . x)) );

for X being non empty set

for f, g, b

( b

:: deftheorem DEFM2 defines max COUSIN2:def 2 :

for X being non empty set

for f, g, b_{4} being Function of X,REAL holds

( b_{4} = max (f,g) iff for x being Element of X holds b_{4} . x = max ((f . x),(g . x)) );

for X being non empty set

for f, g, b

( b

registration

let X be non empty set ;

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

coherence

min (f,g) is positive-yielding

end;
let f, g be positive-yielding Function of X,REAL;

coherence

min (f,g) is positive-yielding

proof end;

registration

let X be non empty set ;

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

coherence

max (f,g) is positive-yielding

end;
let f, g be positive-yielding Function of X,REAL;

coherence

max (f,g) is positive-yielding

proof 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 );

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 );

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}

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}

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}

ex r being Real st X = {r}

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

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

for s being ExtReal

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

A is bounded_above

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)) )

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 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

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)

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;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff x is tagged_division of A )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff x is tagged_division of A ) ) & ( for x being set holds

( x in b_{2} iff x is tagged_division of A ) ) holds

b_{1} = b_{2}

end;
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 for x being set holds

( x in it iff x is tagged_division of A );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def1 defines tagged_divs COUSIN2:def 4 :

for A being non empty closed_interval Subset of REAL

for b_{2} being set holds

( b_{2} = tagged_divs A iff for x being set holds

( x in b_{2} iff x is tagged_division of A ) );

for A being non empty closed_interval Subset of REAL

for b

( b

( x in b

registration
end;

definition

let A be non empty closed_interval Subset of REAL;

let TD be tagged_division of A;

ex b_{1} 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_{1} = T & TD = [D,T] )

for b_{1}, b_{2} 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_{1} = T & TD = [D,T] ) & ex D being Division of A ex T being Element of set_of_tagged_Division D st

( b_{2} = T & TD = [D,T] ) holds

b_{1} = b_{2}
by XTUPLE_0:1;

end;
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 D being Division of A ex T being Element of set_of_tagged_Division D st

( it = T & TD = [D,T] );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

:: 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_{3} being non empty non-decreasing FinSequence of REAL holds

( b_{3} = tagged_of TD iff ex D being Division of A ex T being Element of set_of_tagged_Division D st

( b_{3} = T & TD = [D,T] ) );

for A being non empty closed_interval Subset of REAL

for TD being tagged_division of A

for b

( b

( b

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 )

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)

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;

coherence

len (division_of TD) is Element of NAT ;

coherence

dom (division_of TD) is set ;

end;
let TD be tagged_division of A;

coherence

len (division_of TD) is Element of NAT ;

coherence

dom (division_of TD) is set ;

:: 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);

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);

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

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_{2} -fine tagged_division of I st jauge1 <= jauge2 holds

TD is b_{3} -fine tagged_division of I

for jauge1, jauge2 being positive-yielding Function of I,REAL

for TD being b

TD is b

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;

ex b_{1} being FinSequence of REAL st

( len b_{1} = len TD & ( for i being Nat st i in dom TD holds

b_{1} . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) ) )

for b_{1}, b_{2} being FinSequence of REAL st len b_{1} = len TD & ( for i being Nat st i in dom TD holds

b_{1} . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) ) & len b_{2} = len TD & ( for i being Nat st i in dom TD holds

b_{2} . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) ) holds

b_{1} = b_{2}

end;
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 ( 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))) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof 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_{4} being FinSequence of REAL holds

( b_{4} = tagged_volume (f,TD) iff ( len b_{4} = len TD & ( for i being Nat st i in dom TD holds

b_{4} . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) ) ) );

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

( b

b

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;

coherence

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

end;
let f be PartFunc of I,REAL;

let TD be tagged_division of I;

coherence

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

:: 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));

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 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

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*>

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;

end;
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;

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;

:: 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 );

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 ;

ex b_{1} 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_{1}).| <= epsilon
by A1;

uniqueness

for b_{1}, b_{2} 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_{1}).| <= 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_{2}).| <= epsilon ) holds

b_{1} = b_{2}

end;
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 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;

ex b

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

uniqueness

for b

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

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

b

proof 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_{3} being Real holds

( b_{3} = 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_{3}).| <= epsilon );

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

( b

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

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 )

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

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 )

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 )

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;

ex b_{1} being Function of I,REAL st b_{1} is HK-integrable

end;
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

proof 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)))

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))

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))))

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))

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) )

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) )

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) ) )

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;

ex b_{1} being Function of I,REAL st b_{1} is integrable

end;
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

proof end;

registration

let X be non empty set ;

ex b_{1} being Function of X,REAL st b_{1} is bounded

end;
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

proof 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 )

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;

ex b_{1} being integrable Function of I,REAL st b_{1} is bounded

end;
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

proof 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)

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

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) )

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 )

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))) )

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 )

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

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

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 )

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))).|) )

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)

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))) ) )

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

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 )

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;

for b_{1} being Function of I,REAL st b_{1} is bounded & b_{1} is integrable holds

b_{1} is HK-integrable
by Th48;

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

coherence for b

b