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
{ b1 where b1 is V16() V19( NAT ) V20( REAL ) Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = len y } is 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
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
{ b1 where b1 is V16() V19( NAT ) V20( REAL ) Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = len x } is set
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,(