:: INTEGRA4 semantic presentation

REAL is non empty non trivial non finite V68() V69() V70() V74() non bounded_below non bounded_above interval set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite V42() V43() V68() V69() V70() V71() V72() V73() V74() left_end bounded_below Element of bool REAL

bool REAL is non trivial non finite set

COMPLEX is non empty non trivial non finite V68() V74() set

RAT is non empty non trivial non finite V68() V69() V70() V71() V74() set

INT is non empty non trivial non finite V68() V69() V70() V71() V72() V74() set

[:COMPLEX,COMPLEX:] is non trivial V16() non finite complex-valued set

bool [:COMPLEX,COMPLEX:] is non trivial non finite set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is non trivial V16() non finite complex-valued set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non trivial non finite set

[:REAL,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set

bool [:REAL,REAL:] is non trivial non finite set

[:[:REAL,REAL:],REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set

bool [:[:REAL,REAL:],REAL:] is non trivial non finite set

[:RAT,RAT:] is non trivial V16() V20( RAT ) non finite complex-valued ext-real-valued real-valued set

bool [:RAT,RAT:] is non trivial non finite set

[:[:RAT,RAT:],RAT:] is non trivial V16() V20( RAT ) non finite complex-valued ext-real-valued real-valued set

bool [:[:RAT,RAT:],RAT:] is non trivial non finite set

[:INT,INT:] is non trivial V16() V20( RAT ) V20( INT ) non finite complex-valued ext-real-valued real-valued set

bool [:INT,INT:] is non trivial non finite set

[:[:INT,INT:],INT:] is non trivial V16() V20( RAT ) V20( INT ) non finite complex-valued ext-real-valued real-valued set

bool [:[:INT,INT:],INT:] is non trivial non finite set

[:NAT,NAT:] is non trivial V16() V20( RAT ) V20( INT ) non finite complex-valued ext-real-valued real-valued natural-valued set

[:[:NAT,NAT:],NAT:] is non trivial V16() V20( RAT ) V20( INT ) non finite complex-valued ext-real-valued real-valued natural-valued set

bool [:[:NAT,NAT:],NAT:] is non trivial non finite set

omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite V42() V43() V68() V69() V70() V71() V72() V73() V74() left_end bounded_below set

bool omega is non trivial non finite set

bool NAT is non trivial non finite set

K270(NAT) is V52() set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V16() non-zero empty-yielding V20( RAT ) functional integer finite finite-yielding V41() V42() V44( {} ) FinSequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V68() V69() V70() V71() V72() V73() V74() bounded_below bounded_above real-bounded interval set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

{{},1} is non empty finite V41() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded set

ExtREAL is non empty V69() interval set

[:NAT,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set

bool [:NAT,REAL:] is non trivial non finite set

[:COMPLEX,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set

bool [:COMPLEX,REAL:] is non trivial non finite set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V16() non-zero empty-yielding V20( RAT ) functional integer V34() finite finite-yielding V41() V42() V44( {} ) FinSequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V68() V69() V70() V71() V72() V73() V74() bounded_below bounded_above real-bounded interval Element of NAT

{1} is non empty trivial finite V41() V44(1) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

{0} is non empty trivial finite V41() V44(1) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded set

A is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

vol A is V11() real ext-real Element of REAL

f is non empty V16() V19( NAT ) V20( REAL ) Function-like one-to-one finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

len f is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

rng f is non empty finite V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

dom f is non empty finite V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

f . 1 is V11() real ext-real Element of REAL

lower_bound A is V11() real ext-real Element of REAL

inf A is V11() real ext-real set

f . (len f) is V11() real ext-real Element of REAL

upper_bound A is V11() real ext-real Element of REAL

sup A is V11() real ext-real set

(upper_bound A) - (lower_bound A) is V11() real ext-real Element of REAL

A is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

chi (A,A) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

[:A,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set

bool [:A,REAL:] is non trivial non finite set

integral (chi (A,A)) is V11() real ext-real Element of REAL

vol A is V11() real ext-real Element of REAL

divs A is non empty set

upper_sum_set (chi (A,A)) is non empty V16() V19( divs A) V20( REAL ) Function-like total V30( divs A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:(divs A),REAL:]

[:(divs A),REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set

bool [:(divs A),REAL:] is non trivial non finite set

dom (upper_sum_set (chi (A,A))) is non empty Element of bool (divs A)

bool (divs A) is set

(divs A) /\ (dom (upper_sum_set (chi (A,A)))) is Element of bool (divs A)

(divs A) /\ (divs A) is set

f is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A

(upper_sum_set (chi (A,A))) /. f is V11() real ext-real Element of REAL

(upper_sum_set (chi (A,A))) . f is V11() real ext-real Element of REAL

(upper_sum_set (chi (A,A))) . f is V11() real ext-real Element of REAL

r is non empty V16() V19( NAT ) V20( REAL ) Function-like one-to-one finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

upper_sum ((chi (A,A)),r) is V11() real ext-real Element of REAL

upper_volume ((chi (A,A)),r) is non empty V16() V19( NAT ) V20( REAL ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

Sum (upper_volume ((chi (A,A)),r)) is V11() real ext-real Element of REAL

K175() is V16() V19([:REAL,REAL:]) V20( REAL ) Function-like total V30([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

K271(REAL,(upper_volume ((chi (A,A)),r)),K175()) is V11() real ext-real Element of REAL

(upper_sum_set (chi (A,A))) | (divs A) is V16() V19( divs A) V19( divs A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:(divs A),REAL:]

rng ((upper_sum_set (chi (A,A))) | (divs A)) is V68() V69() V70() Element of bool REAL

f is V11() real ext-real Element of REAL

{f} is non empty trivial finite V44(1) V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

rng (upper_sum_set (chi (A,A))) is non empty V68() V69() V70() Element of bool REAL

the V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A

(upper_sum_set (chi (A,A))) . the V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A is V11() real ext-real Element of REAL

(upper_sum_set (chi (A,A))) /. the V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A is V11() real ext-real Element of REAL

(upper_sum_set (chi (A,A))) . the V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A is V11() real ext-real Element of REAL

lower_bound (rng (upper_sum_set (chi (A,A)))) is V11() real ext-real Element of REAL

upper_integral (chi (A,A)) is V11() real ext-real Element of REAL

lower_sum_set (chi (A,A)) is non empty V16() V19( divs A) V20( REAL ) Function-like total V30( divs A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:(divs A),REAL:]

dom (lower_sum_set (chi (A,A))) is non empty Element of bool (divs A)

(divs A) /\ (dom (lower_sum_set (chi (A,A)))) is Element of bool (divs A)

r is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A

(lower_sum_set (chi (A,A))) /. r is V11() real ext-real Element of REAL

(lower_sum_set (chi (A,A))) . r is V11() real ext-real Element of REAL

(lower_sum_set (chi (A,A))) . r is V11() real ext-real Element of REAL

r is non empty V16() V19( NAT ) V20( REAL ) Function-like one-to-one finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

lower_sum ((chi (A,A)),r) is V11() real ext-real Element of REAL

lower_volume ((chi (A,A)),r) is non empty V16() V19( NAT ) V20( REAL ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

Sum (lower_volume ((chi (A,A)),r)) is V11() real ext-real Element of REAL

K175() is V16() V19([:REAL,REAL:]) V20( REAL ) Function-like total V30([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

K271(REAL,(lower_volume ((chi (A,A)),r)),K175()) is V11() real ext-real Element of REAL

(lower_sum_set (chi (A,A))) | (divs A) is V16() V19( divs A) V19( divs A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:(divs A),REAL:]

rng ((lower_sum_set (chi (A,A))) | (divs A)) is V68() V69() V70() Element of bool REAL

r is V11() real ext-real Element of REAL

{r} is non empty trivial finite V44(1) V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

rng (lower_sum_set (chi (A,A))) is non empty V68() V69() V70() Element of bool REAL

the V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A

(lower_sum_set (chi (A,A))) . the V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A is V11() real ext-real Element of REAL

(lower_sum_set (chi (A,A))) /. the V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A is V11() real ext-real Element of REAL

(lower_sum_set (chi (A,A))) . the V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A is V11() real ext-real Element of REAL

upper_bound (rng (lower_sum_set (chi (A,A)))) is V11() real ext-real Element of REAL

lower_integral (chi (A,A)) is V11() real ext-real Element of REAL

A is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

[:A,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set

bool [:A,REAL:] is non trivial non finite set

chi (A,A) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

f is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

rng f is V68() V69() V70() Element of bool REAL

r is V11() real ext-real Element of REAL

{r} is non empty trivial finite V44(1) V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

r (#) (chi (A,A)) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

dom f is V68() V69() V70() Element of bool A

bool A is set

r is set

x is V11() real ext-real Element of REAL

(chi (A,A)) . x is V11() real ext-real Element of REAL

f . x is V11() real ext-real Element of REAL

r * 1 is V11() real ext-real Element of REAL

r is set

x is V11() real ext-real Element of A

f . x is V11() real ext-real Element of REAL

(chi (A,A)) . x is V11() real ext-real Element of REAL

r * 1 is V11() real ext-real Element of REAL

r is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

dom r is V68() V69() V70() Element of bool A

bool A is set

dom (chi (A,A)) is V68() V69() V70() Element of bool A

dom f is V68() V69() V70() Element of bool A

x is V11() real ext-real Element of A

f /. x is V11() real ext-real Element of REAL

r /. x is V11() real ext-real Element of REAL

f . x is V11() real ext-real Element of REAL

r . x is V11() real ext-real Element of REAL

(chi (A,A)) . x is V11() real ext-real Element of REAL

r * ((chi (A,A)) . x) is V11() real ext-real Element of REAL

r * 1 is V11() real ext-real Element of REAL

A is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

[:A,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set

bool [:A,REAL:] is non trivial non finite set

vol A is V11() real ext-real Element of REAL

f is non empty V16() V19(A) V20( REAL ) Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

rng f is non empty V68() V69() V70() Element of bool REAL

integral f is V11() real ext-real Element of REAL

r is V11() real ext-real Element of REAL

{r} is non empty trivial finite V44(1) V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

r * (vol A) is V11() real ext-real Element of REAL

chi (A,A) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

integral (chi (A,A)) is V11() real ext-real Element of REAL

r (#) (chi (A,A)) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

rng (chi (A,A)) is V68() V69() V70() Element of bool REAL

(chi (A,A)) | A is V16() V19(A) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

A is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

[:A,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set

bool [:A,REAL:] is non trivial non finite set

f is V11() real ext-real Element of REAL

{f} is non empty trivial finite V44(1) V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

chi (A,A) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

f (#) (chi (A,A)) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

r is non empty V16() V19(A) V20( REAL ) Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

rng r is non empty V68() V69() V70() Element of bool REAL

r | A is V16() V19(A) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

A is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

[:A,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set

bool [:A,REAL:] is non trivial non finite set

divs A is non empty set

vol A is V11() real ext-real Element of REAL

f is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

upper_integral f is V11() real ext-real Element of REAL

upper_sum_set f is non empty V16() V19( divs A) V20( REAL ) Function-like total V30( divs A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:(divs A),REAL:]

[:(divs A),REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set

bool [:(divs A),REAL:] is non trivial non finite set

dom (upper_sum_set f) is non empty Element of bool (divs A)

bool (divs A) is set

(divs A) /\ (dom (upper_sum_set f)) is Element of bool (divs A)

(divs A) /\ (divs A) is set

r is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A

(upper_sum_set f) /. r is V11() real ext-real Element of REAL

(upper_sum_set f) . r is V11() real ext-real Element of REAL

x is non empty V16() V19( NAT ) V20( REAL ) Function-like one-to-one finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

upper_volume (f,x) is non empty V16() V19( NAT ) V20( REAL ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

len (upper_volume (f,x)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

len x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

len r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of NAT

Seg (len r) is finite V44( len r) V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of bool NAT

dom r is finite V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of bool NAT

rng x is non empty finite V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

dom x is non empty finite V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

divset (x,(len x)) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

upper_bound (divset (x,(len x))) is V11() real ext-real Element of REAL

sup (divset (x,(len x))) is V11() real ext-real set

x . (len x) is V11() real ext-real Element of REAL

upper_bound A is V11() real ext-real Element of REAL

sup A is V11() real ext-real set

divset (x,1) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

lower_bound (divset (x,(len x))) is V11() real ext-real Element of REAL

inf (divset (x,(len x))) is V11() real ext-real set

[.(lower_bound (divset (x,(len x)))),(upper_bound (divset (x,(len x)))).] is V68() V69() V70() interval Element of bool REAL

lower_bound A is V11() real ext-real Element of REAL

inf A is V11() real ext-real set

[.(lower_bound A),(upper_bound A).] is V68() V69() V70() interval Element of bool REAL

(upper_volume (f,x)) . 1 is V11() real ext-real Element of REAL

f | (divset (x,1)) is V16() V19(A) V19( divset (x,1)) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

rng (f | (divset (x,1))) is V68() V69() V70() Element of bool REAL

upper_bound (rng (f | (divset (x,1)))) is V11() real ext-real Element of REAL

(upper_bound (rng (f | (divset (x,1))))) * (vol A) is V11() real ext-real Element of REAL

<*0*> is non empty trivial V16() V19( NAT ) V20( REAL ) Function-like one-to-one constant finite V44(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing FinSequence of REAL

(upper_sum_set f) . r is V11() real ext-real Element of REAL

upper_sum (f,x) is V11() real ext-real Element of REAL

Sum (upper_volume (f,x)) is V11() real ext-real Element of REAL

K175() is V16() V19([:REAL,REAL:]) V20( REAL ) Function-like total V30([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

K271(REAL,(upper_volume (f,x)),K175()) is V11() real ext-real Element of REAL

(upper_sum_set f) | (divs A) is V16() V19( divs A) V19( divs A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:(divs A),REAL:]

rng ((upper_sum_set f) | (divs A)) is V68() V69() V70() Element of bool REAL

r is V11() real ext-real Element of REAL

{r} is non empty trivial finite V44(1) V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

rng (upper_sum_set f) is non empty V68() V69() V70() Element of bool REAL

the V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A

(upper_sum_set f) . the V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A is V11() real ext-real Element of REAL

(upper_sum_set f) /. the V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A is V11() real ext-real Element of REAL

(upper_sum_set f) . the V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A is V11() real ext-real Element of REAL

lower_bound (rng (upper_sum_set f)) is V11() real ext-real Element of REAL

A is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

[:A,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set

bool [:A,REAL:] is non trivial non finite set

divs A is non empty set

vol A is V11() real ext-real Element of REAL

f is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

lower_integral f is V11() real ext-real Element of REAL

lower_sum_set f is non empty V16() V19( divs A) V20( REAL ) Function-like total V30( divs A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:(divs A),REAL:]

[:(divs A),REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set

bool [:(divs A),REAL:] is non trivial non finite set

dom (lower_sum_set f) is non empty Element of bool (divs A)

bool (divs A) is set

(divs A) /\ (dom (lower_sum_set f)) is Element of bool (divs A)

(divs A) /\ (divs A) is set

r is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A

(lower_sum_set f) /. r is V11() real ext-real Element of REAL

(lower_sum_set f) . r is V11() real ext-real Element of REAL

x is non empty V16() V19( NAT ) V20( REAL ) Function-like one-to-one finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

lower_volume (f,x) is non empty V16() V19( NAT ) V20( REAL ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

len (lower_volume (f,x)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

len x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

Seg (len x) is non empty finite V44( len x) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

dom x is non empty finite V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

rng x is non empty finite V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

divset (x,(len x)) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

upper_bound (divset (x,(len x))) is V11() real ext-real Element of REAL

sup (divset (x,(len x))) is V11() real ext-real set

x . (len x) is V11() real ext-real Element of REAL

upper_bound A is V11() real ext-real Element of REAL

sup A is V11() real ext-real set

divset (x,1) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

lower_bound (divset (x,(len x))) is V11() real ext-real Element of REAL

inf (divset (x,(len x))) is V11() real ext-real set

[.(lower_bound (divset (x,(len x)))),(upper_bound (divset (x,(len x)))).] is V68() V69() V70() interval Element of bool REAL

lower_bound A is V11() real ext-real Element of REAL

inf A is V11() real ext-real set

[.(lower_bound A),(upper_bound A).] is V68() V69() V70() interval Element of bool REAL

(lower_volume (f,x)) . 1 is V11() real ext-real Element of REAL

f | (divset (x,1)) is V16() V19(A) V19( divset (x,1)) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

rng (f | (divset (x,1))) is V68() V69() V70() Element of bool REAL

lower_bound (rng (f | (divset (x,1)))) is V11() real ext-real Element of REAL

(lower_bound (rng (f | (divset (x,1))))) * (vol A) is V11() real ext-real Element of REAL

<*0*> is non empty trivial V16() V19( NAT ) V20( REAL ) Function-like one-to-one constant finite V44(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing FinSequence of REAL

(lower_sum_set f) . r is V11() real ext-real Element of REAL

lower_sum (f,x) is V11() real ext-real Element of REAL

Sum (lower_volume (f,x)) is V11() real ext-real Element of REAL

K175() is V16() V19([:REAL,REAL:]) V20( REAL ) Function-like total V30([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

K271(REAL,(lower_volume (f,x)),K175()) is V11() real ext-real Element of REAL

(lower_sum_set f) | (divs A) is V16() V19( divs A) V19( divs A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:(divs A),REAL:]

rng ((lower_sum_set f) | (divs A)) is V68() V69() V70() Element of bool REAL

r is V11() real ext-real Element of REAL

{r} is non empty trivial finite V44(1) V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

rng (lower_sum_set f) is non empty V68() V69() V70() Element of bool REAL

the V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A

(lower_sum_set f) . the V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A is V11() real ext-real Element of REAL

(lower_sum_set f) /. the V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A is V11() real ext-real Element of REAL

(lower_sum_set f) . the V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A is V11() real ext-real Element of REAL

upper_bound (rng (lower_sum_set f)) is V11() real ext-real Element of REAL

A is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

[:A,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set

bool [:A,REAL:] is non trivial non finite set

divs A is non empty set

vol A is V11() real ext-real Element of REAL

f is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

integral f is V11() real ext-real Element of REAL

upper_integral f is V11() real ext-real Element of REAL

lower_integral f is V11() real ext-real Element of REAL

A is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

[:A,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set

bool [:A,REAL:] is non trivial non finite set

vol A is V11() real ext-real Element of REAL

f is non empty V16() V19(A) V20( REAL ) Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

f | A is V16() V19(A) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

rng f is non empty V68() V69() V70() Element of bool REAL

lower_bound (rng f) is V11() real ext-real Element of REAL

upper_bound (rng f) is V11() real ext-real Element of REAL

integral f is V11() real ext-real Element of REAL

{(lower_bound (rng f))} is non empty trivial finite V44(1) V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

r is non empty V16() V19(A) V20( REAL ) Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

rng r is non empty V68() V69() V70() Element of bool REAL

r | A is V16() V19(A) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

{(upper_bound (rng f))} is non empty trivial finite V44(1) V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

r is non empty V16() V19(A) V20( REAL ) Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

rng r is non empty V68() V69() V70() Element of bool REAL

r | A is V16() V19(A) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

integral r is V11() real ext-real Element of REAL

(lower_bound (rng f)) * (vol A) is V11() real ext-real Element of REAL

dom f is non empty V68() V69() V70() Element of bool A

bool A is set

x is V11() real ext-real Element of REAL

f . x is V11() real ext-real Element of REAL

x is V11() real ext-real Element of REAL

f . x is V11() real ext-real Element of REAL

r . x is V11() real ext-real Element of REAL

dom r is non empty V68() V69() V70() Element of bool A

x is V11() real ext-real Element of REAL

r . x is V11() real ext-real Element of REAL

f . x is V11() real ext-real Element of REAL

dom r is non empty V68() V69() V70() Element of bool A

integral r is V11() real ext-real Element of REAL

(upper_bound (rng f)) * (vol A) is V11() real ext-real Element of REAL

(integral f) / (vol A) is V11() real ext-real Element of REAL

x is V11() real ext-real Element of REAL

x * (vol A) is V11() real ext-real Element of REAL

x is V11() real ext-real Element of REAL

f . x is V11() real ext-real Element of REAL

x is V11() real ext-real Element of REAL

x * (vol A) is V11() real ext-real Element of REAL

A is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

[:A,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set

bool [:A,REAL:] is non trivial non finite set

divs A is non empty set

[:NAT,(divs A):] is non trivial V16() non finite set

bool [:NAT,(divs A):] is non trivial non finite set

f is non empty V16() V19(A) V20( REAL ) Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

f | A is V16() V19(A) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

lower_integral f is V11() real ext-real Element of REAL

r is non empty V16() V19( NAT ) V20( divs A) Function-like total V30( NAT , divs A) Element of bool [:NAT,(divs A):]

delta r is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

lim (delta r) is V11() real ext-real Element of REAL

lower_sum (f,r) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

lim (lower_sum (f,r)) is V11() real ext-real Element of REAL

vol A is V11() real ext-real Element of REAL

r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of NAT

(delta r) . r is V11() real ext-real Element of REAL

chi (A,A) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

r . r is non empty V16() V19( NAT ) V20( REAL ) Function-like one-to-one finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

upper_volume ((chi (A,A)),(r . r)) is non empty V16() V19( NAT ) V20( REAL ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

rng (upper_volume ((chi (A,A)),(r . r))) is non empty finite V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

delta (r . r) is V11() real ext-real Element of REAL

x is non empty finite V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

sup x is V11() real ext-real set

y is non empty V16() V19( NAT ) V20( REAL ) Function-like one-to-one finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

dom y is non empty finite V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of NAT

divset (y,x) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

vol (divset (y,x)) is V11() real ext-real Element of REAL

len y is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

Seg (len y) is non empty finite V44( len y) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

upper_volume ((chi (A,A)),y) is non empty V16() V19( NAT ) V20( REAL ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

len (upper_volume ((chi (A,A)),y)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

Seg (len (upper_volume ((chi (A,A)),y))) is non empty finite V44( len (upper_volume ((chi (A,A)),y))) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

dom (upper_volume ((chi (A,A)),y)) is non empty finite V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

(upper_volume ((chi (A,A)),y)) . x is V11() real ext-real Element of REAL

rng (upper_volume ((chi (A,A)),y)) is non empty finite V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

upper_volume ((chi (A,A)),y) is non empty V16() V19( NAT ) V20( REAL ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

len (upper_volume ((chi (A,A)),y)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

len y is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

(len y) |-> 0 is V16() empty-yielding V19( NAT ) V20( REAL ) Function-like finite V44( len y) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len y) -tuples_on REAL

(len y) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg (len y) is non empty finite V44( len y) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

K215((Seg (len y)),0) is non empty V16() V19( Seg (len y)) V20( RAT ) V20( INT ) V20({0}) Function-like total V30( Seg (len y),{0}) finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(Seg (len y)),{0}:]

[:(Seg (len y)),{0}:] is V16() V20( RAT ) V20( INT ) finite complex-valued ext-real-valued real-valued natural-valued set

bool [:(Seg (len y)),{0}:] is finite V41() set

x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer finite V42() set

(upper_volume ((chi (A,A)),y)) . x is V11() real ext-real Element of REAL

((len y) |-> 0) . x is V11() real ext-real Element of REAL

Seg (len (upper_volume ((chi (A,A)),y))) is non empty finite V44( len (upper_volume ((chi (A,A)),y))) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

divset (y,x) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

vol (divset (y,x)) is V11() real ext-real Element of REAL

len ((len y) |-> 0) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of NAT

Sum (upper_volume ((chi (A,A)),y)) is V11() real ext-real Element of REAL

K175() is V16() V19([:REAL,REAL:]) V20( REAL ) Function-like total V30([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

K271(REAL,(upper_volume ((chi (A,A)),y)),K175()) is V11() real ext-real Element of REAL

vol A is V11() real ext-real Element of REAL

r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer finite V42() set

(lower_sum (f,r)) . r is V11() real ext-real Element of REAL

x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of NAT

r . x is non empty V16() V19( NAT ) V20( REAL ) Function-like one-to-one finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

y is non empty V16() V19( NAT ) V20( REAL ) Function-like one-to-one finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

len y is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

lower_volume (f,y) is non empty V16() V19( NAT ) V20( REAL ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

len (lower_volume (f,y)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

rng y is non empty finite V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

dom y is non empty finite V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

divset (y,(len y)) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

upper_bound (divset (y,(len y))) is V11() real ext-real Element of REAL

sup (divset (y,(len y))) is V11() real ext-real set

y . (len y) is V11() real ext-real Element of REAL

upper_bound A is V11() real ext-real Element of REAL

sup A is V11() real ext-real set

Seg (len y) is non empty finite V44( len y) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

divset (y,1) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

lower_bound (divset (y,(len y))) is V11() real ext-real Element of REAL

inf (divset (y,(len y))) is V11() real ext-real set

[.(lower_bound (divset (y,(len y)))),(upper_bound (divset (y,(len y)))).] is V68() V69() V70() interval Element of bool REAL

lower_bound A is V11() real ext-real Element of REAL

inf A is V11() real ext-real set

[.(lower_bound A),(upper_bound A).] is V68() V69() V70() interval Element of bool REAL

(lower_volume (f,y)) . 1 is V11() real ext-real Element of REAL

f | (divset (y,1)) is V16() V19(A) V19( divset (y,1)) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

rng (f | (divset (y,1))) is V68() V69() V70() Element of bool REAL

lower_bound (rng (f | (divset (y,1)))) is V11() real ext-real Element of REAL

(lower_bound (rng (f | (divset (y,1))))) * (vol A) is V11() real ext-real Element of REAL

<*0*> is non empty trivial V16() V19( NAT ) V20( REAL ) Function-like one-to-one constant finite V44(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing FinSequence of REAL

Sum (lower_volume (f,y)) is V11() real ext-real Element of REAL

K175() is V16() V19([:REAL,REAL:]) V20( REAL ) Function-like total V30([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

K271(REAL,(lower_volume (f,y)),K175()) is V11() real ext-real Element of REAL

lower_sum (f,y) is V11() real ext-real Element of REAL

(lower_sum (f,r)) . 1 is V11() real ext-real Element of REAL

vol A is V11() real ext-real Element of REAL

A is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

[:A,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set

bool [:A,REAL:] is non trivial non finite set

divs A is non empty set

[:NAT,(divs A):] is non trivial V16() non finite set

bool [:NAT,(divs A):] is non trivial non finite set

f is non empty V16() V19(A) V20( REAL ) Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

f | A is V16() V19(A) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

upper_integral f is V11() real ext-real Element of REAL

r is non empty V16() V19( NAT ) V20( divs A) Function-like total V30( NAT , divs A) Element of bool [:NAT,(divs A):]

delta r is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

lim (delta r) is V11() real ext-real Element of REAL

upper_sum (f,r) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

lim (upper_sum (f,r)) is V11() real ext-real Element of REAL

vol A is V11() real ext-real Element of REAL

r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of NAT

(delta r) . r is V11() real ext-real Element of REAL

r . r is non empty V16() V19( NAT ) V20( REAL ) Function-like one-to-one finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

delta (r . r) is V11() real ext-real Element of REAL

chi (A,A) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

upper_volume ((chi (A,A)),(r . r)) is non empty V16() V19( NAT ) V20( REAL ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

rng (upper_volume ((chi (A,A)),(r . r))) is non empty finite V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

sup (rng (upper_volume ((chi (A,A)),(r . r)))) is V11() real ext-real set

x is non empty V16() V19( NAT ) V20( REAL ) Function-like one-to-one finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

dom x is non empty finite V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of NAT

divset (x,y) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

vol (divset (x,y)) is V11() real ext-real Element of REAL

len x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

Seg (len x) is non empty finite V44( len x) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

upper_volume ((chi (A,A)),x) is non empty V16() V19( NAT ) V20( REAL ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

len (upper_volume ((chi (A,A)),x)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

Seg (len (upper_volume ((chi (A,A)),x))) is non empty finite V44( len (upper_volume ((chi (A,A)),x))) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

dom (upper_volume ((chi (A,A)),x)) is non empty finite V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

(upper_volume ((chi (A,A)),x)) . y is V11() real ext-real Element of REAL

rng (upper_volume ((chi (A,A)),x)) is non empty finite V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

upper_volume ((chi (A,A)),x) is non empty V16() V19( NAT ) V20( REAL ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

len (upper_volume ((chi (A,A)),x)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

len x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

(len x) |-> 0 is V16() empty-yielding V19( NAT ) V20( REAL ) Function-like finite V44( len x) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len x) -tuples_on REAL

(len x) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL

{ b

Seg (len x) is non empty finite V44( len x) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

K215((Seg (len x)),0) is non empty V16() V19( Seg (len x)) V20( RAT ) V20( INT ) V20({0}) Function-like total V30( Seg (len x),{0}) finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(Seg (len x)),{0}:]

[:(Seg (len x)),{0}:] is V16() V20( RAT ) V20( INT ) finite complex-valued ext-real-valued real-valued natural-valued set

bool [:(Seg (len x)),{0}:] is finite V41() set

y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer finite V42() set

(upper_volume ((chi (A,A)),x)) . y is V11() real ext-real Element of REAL

((len x) |-> 0) . y is V11() real ext-real Element of REAL

Seg (len (upper_volume ((chi (A,A)),x))) is non empty finite V44( len (upper_volume ((chi (A,A)),x))) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

divset (x,y) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

vol (divset (x,y)) is V11() real ext-real Element of REAL

len ((len x) |-> 0) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of NAT

Sum (upper_volume ((chi (A,A)),x)) is V11() real ext-real Element of REAL

K175() is V16() V19([:REAL,REAL:]) V20( REAL ) Function-like total V30([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

K271(REAL,(upper_volume ((chi (A,A)),x)),K175()) is V11() real ext-real Element of REAL

vol A is V11() real ext-real Element of REAL

r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer finite V42() set

(upper_sum (f,r)) . r is V11() real ext-real Element of REAL

x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of NAT

r . x is non empty V16() V19( NAT ) V20( REAL ) Function-like one-to-one finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

y is non empty V16() V19( NAT ) V20( REAL ) Function-like one-to-one finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

len y is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

upper_volume (f,y) is non empty V16() V19( NAT ) V20( REAL ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

len (upper_volume (f,y)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

rng y is non empty finite V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

dom y is non empty finite V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

divset (y,(len y)) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

upper_bound (divset (y,(len y))) is V11() real ext-real Element of REAL

sup (divset (y,(len y))) is V11() real ext-real set

y . (len y) is V11() real ext-real Element of REAL

upper_bound A is V11() real ext-real Element of REAL

sup A is V11() real ext-real set

Seg (len y) is non empty finite V44( len y) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

divset (y,1) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

lower_bound (divset (y,(len y))) is V11() real ext-real Element of REAL

inf (divset (y,(len y))) is V11() real ext-real set

[.(lower_bound (divset (y,(len y)))),(upper_bound (divset (y,(len y)))).] is V68() V69() V70() interval Element of bool REAL

lower_bound A is V11() real ext-real Element of REAL

inf A is V11() real ext-real set

[.(lower_bound A),(upper_bound A).] is V68() V69() V70() interval Element of bool REAL

(upper_volume (f,y)) . 1 is V11() real ext-real Element of REAL

f | (divset (y,1)) is V16() V19(A) V19( divset (y,1)) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

rng (f | (divset (y,1))) is V68() V69() V70() Element of bool REAL

upper_bound (rng (f | (divset (y,1)))) is V11() real ext-real Element of REAL

(upper_bound (rng (f | (divset (y,1))))) * (vol A) is V11() real ext-real Element of REAL

<*0*> is non empty trivial V16() V19( NAT ) V20( REAL ) Function-like one-to-one constant finite V44(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing FinSequence of REAL

Sum (upper_volume (f,y)) is V11() real ext-real Element of REAL

K175() is V16() V19([:REAL,REAL:]) V20( REAL ) Function-like total V30([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

K271(REAL,(upper_volume (f,y)),K175()) is V11() real ext-real Element of REAL

upper_sum (f,y) is V11() real ext-real Element of REAL

(upper_sum (f,r)) . 1 is V11() real ext-real Element of REAL

vol A is V11() real ext-real Element of REAL

A is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

[:A,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set

bool [:A,REAL:] is non trivial non finite set

f is non empty V16() V19(A) V20( REAL ) Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

f | A is V16() V19(A) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

rng f is non empty V68() V69() V70() Element of bool REAL

lower_bound (rng f) is V11() real ext-real Element of REAL

vol A is V11() real ext-real Element of REAL

(lower_bound (rng f)) * (vol A) is V11() real ext-real Element of REAL

upper_sum_set f is non empty V16() V19( divs A) V20( REAL ) Function-like total V30( divs A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:(divs A),REAL:]

divs A is non empty set

[:(divs A),REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set

bool [:(divs A),REAL:] is non trivial non finite set

rng (upper_sum_set f) is non empty V68() V69() V70() Element of bool REAL

r is ext-real set

dom (upper_sum_set f) is non empty Element of bool (divs A)

bool (divs A) is set

r is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A

(upper_sum_set f) . r is V11() real ext-real Element of REAL

x is non empty V16() V19( NAT ) V20( REAL ) Function-like one-to-one finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

upper_sum (f,x) is V11() real ext-real Element of REAL

lower_sum (f,x) is V11() real ext-real Element of REAL

upper_bound (rng f) is V11() real ext-real Element of REAL

(upper_bound (rng f)) * (vol A) is V11() real ext-real Element of REAL

lower_sum_set f is non empty V16() V19( divs A) V20( REAL ) Function-like total V30( divs A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:(divs A),REAL:]

rng (lower_sum_set f) is non empty V68() V69() V70() Element of bool REAL

r is ext-real set

dom (lower_sum_set f) is non empty Element of bool (divs A)

bool (divs A) is set

r is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of divs A

(lower_sum_set f) . r is V11() real ext-real Element of REAL

x is non empty V16() V19( NAT ) V20( REAL ) Function-like one-to-one finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

lower_sum (f,x) is V11() real ext-real Element of REAL

upper_sum (f,x) is V11() real ext-real Element of REAL

A is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

A is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

vol A is V11() real ext-real Element of REAL

lower_bound A is V11() real ext-real Element of REAL

inf A is V11() real ext-real set

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of NAT

(vol A) / f is V11() real ext-real Element of REAL

r is V16() V19( NAT ) V20( REAL ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

len r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of NAT

dom r is finite V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of bool NAT

r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of NAT

r . r is V11() real ext-real Element of REAL

x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of NAT

r . x is V11() real ext-real Element of REAL

((vol A) / f) * x is V11() real ext-real Element of REAL

((vol A) / f) * r is V11() real ext-real Element of REAL

(lower_bound A) + (((vol A) / f) * x) is V11() real ext-real Element of REAL

(lower_bound A) + (((vol A) / f) * r) is V11() real ext-real Element of REAL

Seg f is finite V44(f) V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of bool NAT

r is non empty V16() V19( NAT ) V20( REAL ) Function-like one-to-one finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing FinSequence of REAL

len r is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

r . (len r) is V11() real ext-real Element of REAL

((vol A) / f) * f is V11() real ext-real Element of REAL

(lower_bound A) + (((vol A) / f) * f) is V11() real ext-real Element of REAL

(lower_bound A) + (vol A) is V11() real ext-real Element of REAL

rng r is non empty finite V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

x is set

upper_bound A is V11() real ext-real Element of REAL

sup A is V11() real ext-real set

(upper_bound A) - (lower_bound A) is V11() real ext-real Element of REAL

(lower_bound A) + ((upper_bound A) - (lower_bound A)) is V11() real ext-real Element of REAL

dom r is non empty finite V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

y is V11() real ext-real Element of REAL

x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of NAT

r . x is V11() real ext-real Element of REAL

((vol A) / f) * x is V11() real ext-real Element of REAL

(lower_bound A) + (((vol A) / f) * x) is V11() real ext-real Element of REAL

upper_bound A is V11() real ext-real Element of REAL

sup A is V11() real ext-real set

(upper_bound A) - (lower_bound A) is V11() real ext-real Element of REAL

x is non empty V16() V19( NAT ) V20( REAL ) Function-like one-to-one finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

len x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

dom x is non empty finite V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of NAT

x . y is V11() real ext-real Element of REAL

((vol A) / f) * y is V11() real ext-real Element of REAL

(lower_bound A) + (((vol A) / f) * y) is V11() real ext-real Element of REAL

A is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL

vol A is V11() real ext-real Element of REAL

divs A is non empty set

[:NAT,(divs A):] is non trivial V16() non finite set

bool [:NAT,(divs A):] is non trivial non finite set

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of NAT

f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

lower_bound A is V11() real ext-real Element of REAL

inf A is V11() real ext-real set

(vol A) / (f + 1) is V11() real ext-real Element of REAL

r is non empty V16() V19( NAT ) V20( REAL ) Function-like one-to-one finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

len r is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V34() finite V42() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of NAT

dom r is non empty finite V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

f is non empty V16() V19( NAT ) V20( divs A) Function-like total V30( NAT , divs A) Element of bool [:NAT,(divs A):]

r is non empty V16() V19( NAT ) V20( divs A) Function-like total V30( NAT , divs A) Element of bool [:NAT,(