let I be 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))).|) )
let TD be 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))).|) )
let jauge be 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))).|) )
let r1, r2, s be 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))).|) )
let D1 be 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))).|) )
let fc, f be 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))).|) )
let epsilon be Real; ( 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 implies ( 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))).|) ) )
assume that
A1:
fc = chi (I,I)
and
A2:
r1 = min (rng (upper_volume (fc,D1)))
and
A3:
r2 = epsilon / ((2 * (len D1)) * |.((upper_bound (rng f)) - (lower_bound (rng f))).|)
and
A4:
0 < r1
and
A5:
0 < r2
and
A6:
s = (min (r1,r2)) / 2
and
A7:
jauge = s (#) fc
and
A8:
TD is jauge -fine
; ( 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))).|) )
A9:
delta (division_of TD) <= (min (r1,r2)) / 2
by A1, A6, A7, A8, Th42;
(min (r1,r2)) / 2 < (min (r1,r2)) / 1
by A4, A5, XREAL_1:76;
then
delta (division_of TD) < min (r1,r2)
by A9, XXREAL_0:2;
hence
( 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))).|) )
by A2, A3, XXREAL_0:23; verum