let I be non empty closed_interval Subset of REAL; :: thesis: for jauge being positive-yielding Function of I,REAL ex TD being tagged_division of I st TD is jauge -fine
let jauge be positive-yielding Function of I,REAL; :: thesis: ex TD being tagged_division of I st TD is jauge -fine
consider a, b being Real such that
A1: a <= b and
A2: I = [.a,b.] by Th33;
A3: ( lower_bound I = a & upper_bound I = b ) by A1, A2, JORDAN5A:19;
reconsider r = 1 / 2 as positive Real ;
reconsider jauge2 = r (#) jauge as positive-yielding Function of I,REAL ;
consider x being non empty increasing FinSequence of REAL , t being non empty FinSequence of REAL such that
A4: x . 1 = a and
A5: x . (len x) = b and
A6: t . 1 = a and
A7: dom x = dom t and
A8: for i being Nat st i - 1 in dom t & i in dom t holds
( (t . i) - (jauge2 . (t . i)) <= x . (i - 1) & x . (i - 1) <= t . i ) and
A9: for i being Nat st i in dom t holds
( t . i <= x . i & x . i <= (t . i) + (jauge2 . (t . i)) ) by A1, A2, Th46;

now :: thesis: ( rng x c= I & x . (len x) = upper_bound I )

thus rng x c= I :: thesis: x . (len x) = upper_bound I

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in rng x or u in I )
assume A10: u in rng x ; :: thesis: u in I
then consider v being object such that
A11: v in dom x and
A12: x . v = u by FUNCT_1:def 3;
rng x c= REAL ;
then reconsider u1 = u as Element of REAL by A11, A12, FUNCT_1:3;
reconsider v1 = v as Nat by A11;
A13: 1 in dom x by A10, FINSEQ_3:31;
1 <= v1 by A11, FINSEQ_3:25;

per cases then ( v1 = 1 or 1 < v1 ) by XXREAL_0:1;

suppose v1 = 1 ; :: thesis: u in I

hence u in I by A1, A2, A4, A12, XXREAL_1:1; :: thesis: verum

end;

suppose A14: 1 < v1 ; :: thesis: u in I

v1 <= len x by A11, FINSEQ_3:25;

per cases then ( v1 < len x or v1 = len x ) by XXREAL_0:1;

suppose A15: v1 < len x ; :: thesis: u in I

len x in dom x by FINSEQ_5:6;
then ( a <= u1 & u1 <= b ) by A5, A15, A14, A13, A4, A12, A11, VALUED_0:def 13;
hence u in I by A2, XXREAL_1:1; :: thesis: verum

end;

suppose v1 = len x ; :: thesis: u in I

hence u in I by A1, A2, A5, A12, XXREAL_1:1; :: thesis: verum

end;

end;

end;

end;

end;

thus x . (len x) = upper_bound I by A5, A1, A2, JORDAN5A:19; :: thesis: verum

end;

then reconsider D = x as Division of I by INTEGRA1:def 2;

now :: thesis: ex s being non empty non-decreasing FinSequence of REAL st
( t = s & dom s = dom D & ( for i being Nat st i in dom s holds
s . i in divset (D,i) ) )

t is non-decreasing

proof

assume not t is non-decreasing ; :: thesis: contradiction
then consider e1, e2 being ExtReal such that
A16: e1 in dom t and
A17: e2 in dom t and
A18: e1 <= e2 and
A19: t . e2 < t . e1 ;
1 <= e1 by FINSEQ_3:25, A16;

per cases then ( e1 = 1 or 1 < e1 ) by XXREAL_0:1;

suppose A20: e1 = 1 ; :: thesis: contradiction

1 <= e2 by FINSEQ_3:25, A17;

per cases then ( e2 = 1 or 1 < e2 ) by XXREAL_0:1;

suppose e2 = 1 ; :: thesis: contradiction

hence contradiction by A19, A20; :: thesis: verum

end;

suppose A21: 1 < e2 ; :: thesis: contradiction

reconsider f2 = e2 as Nat by A17;
f2 - 1 in dom t by A17, A21, CGAMES_1:20;
then A22: x . (f2 - 1) <= t . f2 by A8, A17;
rng x <> {} ;
then A23: 1 in dom x by FINSEQ_3:32;
f2 - 1 in dom x by A17, A21, CGAMES_1:20, A7;
then x . 1 <= x . (f2 - 1) by A23, FINSEQ_3:25, VALUED_0:def 15;
hence contradiction by A4, A22, XXREAL_0:2, A19, A6, A20; :: thesis: verum

end;

end;

end;

suppose A24: 1 < e1 ; :: thesis: contradiction

per cases ( e1 = e2 or e1 < e2 ) by A18, XXREAL_0:1;

suppose e1 = e2 ; :: thesis: contradiction

hence contradiction by A19; :: thesis: verum

end;

suppose A25: e1 < e2 ; :: thesis: contradiction

A26: t . e1 <= x . e1 by A16, A9;
reconsider f2 = e2 as Nat by A17;
1 < e2 by A24, A25, XXREAL_0:2;
then A27: f2 - 1 in dom t by A17, CGAMES_1:20;
then A28: x . (f2 - 1) <= t . e2 by A17, A8;

per cases ( e1 = f2 - 1 or e1 <> f2 - 1 ) ;

suppose e1 = f2 - 1 ; :: thesis: contradiction

then x . e1 <= t . e2 by A27, A17, A8;
hence contradiction by A26, XXREAL_0:2, A19; :: thesis: verum

end;

suppose A29: e1 <> f2 - 1 ; :: thesis: contradiction

reconsider f1 = e1 as Nat by A16;
f1 < f2 - 1

proof

assume f2 - 1 <= f1 ; :: thesis: contradiction
then (f2 - 1) + 1 <= f1 + 1 by XREAL_1:6;
then ( f1 = f2 or f2 = f1 + 1 ) by A18, NAT_1:9;
hence contradiction by A25, A29; :: thesis: verum

end;

then x . e1 < x . (f2 - 1) by A27, A7, A16, VALUED_0:def 13;
then x . e1 <= t . e2 by A28, XXREAL_0:2;
hence contradiction by A19, A26, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

then reconsider s = t as non empty non-decreasing FinSequence of REAL ;
take s = s; :: thesis: ( t = s & dom s = dom D & ( for i being Nat st i in dom s holds
s . i in divset (D,i) ) )
thus t = s ; :: thesis: ( dom s = dom D & ( for i being Nat st i in dom s holds
s . i in divset (D,i) ) )
thus dom s = dom D by A7; :: thesis: for i being Nat st i in dom s holds
s . i in divset (D,i)
thus for i being Nat st i in dom s holds
s . i in divset (D,i) :: thesis: verum

proof

let i be Nat; :: thesis: ( i in dom s implies s . i in divset (D,i) )
assume A30: i in dom s ; :: thesis: s . i in divset (D,i)
consider d1, d2 being Real such that
A31: divset (D,i) = [.d1,d2.] by MEASURE5:def 3;
A32: d1 <= d2 by A31, XXREAL_1:29;
1 <= i by FINSEQ_3:25, A30;

per cases then ( i = 1 or 1 < i ) by XXREAL_0:1;

suppose A33: i = 1 ; :: thesis: s . i in divset (D,i)

then ( lower_bound (divset (D,i)) = lower_bound I & upper_bound (divset (D,i)) = D . 1 ) by A7, A30, INTEGRA1:def 4;
then ( d1 = a & d2 = D . 1 ) by A32, A31, JORDAN5A:19, A3;
hence s . i in divset (D,i) by A6, A4, A31, A33, XXREAL_1:1; :: thesis: verum

end;

suppose A34: 1 < i ; :: thesis: s . i in divset (D,i)

then ( lower_bound (divset (D,i)) = D . (i - 1) & upper_bound (divset (D,i)) = D . i ) by A7, A30, INTEGRA1:def 4;
then A35: ( d1 = D . (i - 1) & d2 = D . i ) by A32, A31, JORDAN5A:19;
i - 1 in dom t by A30, CGAMES_1:20, A34;
then ( D . (i - 1) <= s . i & s . i <= D . i ) by A30, A8, A9;
hence s . i in divset (D,i) by A31, A35, XXREAL_1:1; :: thesis: verum

end;

end;

end;

end;

then reconsider T = t as Element of set_of_tagged_Division D by Def2;
reconsider TD = [D,T] as tagged_division of I by Def3;
take TD ; :: thesis: TD is jauge -fine

now :: thesis: ex D being Division of I st
( D is Division of I & ex T being Element of set_of_tagged_Division D st
( T is Element of set_of_tagged_Division D & TD = [D,T] & ( for i being Nat st i in dom D holds
vol (divset (D,i)) <= jauge . (T . i) ) ) )

take D = D; :: thesis: ( D is Division of I & ex T being Element of set_of_tagged_Division D st
( T is Element of set_of_tagged_Division D & TD = [D,T] & ( for i being Nat st i in dom D holds
vol (divset (D,i)) <= jauge . (T . i) ) ) )
thus D is Division of I ; :: thesis: ex T being Element of set_of_tagged_Division D st
( T is Element of set_of_tagged_Division D & TD = [D,T] & ( for i being Nat st i in dom D holds
vol (divset (D,i)) <= jauge . (T . i) ) )
take T = T; :: thesis: ( T is Element of set_of_tagged_Division D & TD = [D,T] & ( for i being Nat st i in dom D holds
vol (divset (D,i)) <= jauge . (T . i) ) )
thus T is Element of set_of_tagged_Division D ; :: thesis: ( TD = [D,T] & ( for i being Nat st i in dom D holds
vol (divset (D,i)) <= jauge . (T . i) ) )
thus TD = [D,T] ; :: thesis: for i being Nat st i in dom D holds
vol (divset (D,i)) <= jauge . (T . i)
thus for i being Nat st i in dom D holds
vol (divset (D,i)) <= jauge . (T . i) :: thesis: verum

proof

let i be Nat; :: thesis: ( i in dom D implies vol (divset (D,i)) <= jauge . (T . i) )
assume A36: i in dom D ; :: thesis: vol (divset (D,i)) <= jauge . (T . i)
consider u, v being Real such that
A37: divset (D,i) = [.u,v.] by MEASURE5:def 3;
u <= v by A37, XXREAL_1:29;
then A38: ( lower_bound (divset (D,i)) = u & upper_bound (divset (D,i)) = v ) by A37, JORDAN5A:19;
1 <= i by FINSEQ_3:25, A36;

per cases then ( i = 1 or 1 < i ) by XXREAL_0:1;

suppose A39: i = 1 ; :: thesis: vol (divset (D,i)) <= jauge . (T . i)

then A40: ( u = lower_bound I & v = D . 1 ) by A36, A38, INTEGRA1:def 4;
A41: vol (divset (D,i)) = v - u by A38, INTEGRA1:def 5
.= (D . 1) - a by A40, A1, A2, JORDAN5A:19
.= 0 by A4 ;
T . i in [.a,b.] by A39, A6, A1, XXREAL_1:1;
then T . i in dom jauge by A2, FUNCT_2:def 1;
then jauge . (T . i) in rng jauge by FUNCT_1:3;
hence vol (divset (D,i)) <= jauge . (T . i) by A41, PARTFUN3:def 1; :: thesis: verum

end;

suppose A42: 1 < i ; :: thesis: vol (divset (D,i)) <= jauge . (T . i)

then A43: ( u = D . (i - 1) & v = D . i ) by A36, A38, INTEGRA1:def 4;
i - 1 in dom t by A36, A7, A42, CGAMES_1:20;
then A44: (t . i) - (jauge2 . (t . i)) <= x . (i - 1) by A36, A7, A8;
consider s being non empty non-decreasing FinSequence of REAL such that
A46: T = s and
A47: dom s = dom D and
A48: for i being Nat st i in dom s holds
s . i in divset (D,i) by Def2;
divset (D,i) c= I by A36, INTEGRA1:8;
then t . i in I by A46, A47, A48, A36;
then A49: t . i in dom jauge2 by FUNCT_2:def 1;
x . i <= (t . i) + (jauge2 . (t . i)) by A36, A7, A9;
then (x . i) - (x . (i - 1)) <= ((t . i) + (jauge2 . (t . i))) - ((t . i) - (jauge2 . (t . i))) by A44, XREAL_1:13;
then (x . i) - (x . (i - 1)) <= 2 * (jauge2 . (t . i)) ;
then (x . i) - (x . (i - 1)) <= 2 * ((1 / 2) * (jauge . (t . i))) by A49, VALUED_1:def 5;
hence vol (divset (D,i)) <= jauge . (T . i) by A38, INTEGRA1:def 5, A43; :: thesis: verum

end;

end;

end;

end;

hence TD is jauge -fine ; :: thesis: verum