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,(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:]
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 + 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
(vol A) / (r + 1) 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:]
[: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
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
{((vol A) / (r + 1))} is non empty trivial finite V44(1) V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
y is set
dom (upper_volume ((chi (A,A)),(r . 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
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
(upper_volume ((chi (A,A)),(r . r))) . x 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 (upper_volume ((chi (A,A)),(r . 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
Seg (len (upper_volume ((chi (A,A)),(r . r)))) is non empty finite V44( len (upper_volume ((chi (A,A)),(r . r)))) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool 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
divset (x,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,x)) is V11() real ext-real Element of REAL
sup (divset (x,x)) is V11() real ext-real set
lower_bound (divset (x,x)) is V11() real ext-real Element of REAL
inf (divset (x,x)) is V11() real ext-real set
(upper_bound (divset (x,x))) - (lower_bound (divset (x,x))) is V11() real ext-real Element of REAL
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 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 + 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
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
x . 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
((vol A) / (r + 1)) * 1 is V11() real ext-real Element of REAL
(lower_bound A) + (((vol A) / (r + 1)) * 1) is V11() real ext-real Element of REAL
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 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 + 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) + ((vol A) / (r + 1)) is V11() real ext-real Element of REAL
((lower_bound A) + ((vol A) / (r + 1))) - (lower_bound A) is V11() real ext-real Element of REAL
(lower_bound A) - (lower_bound A) is V11() real ext-real Element of REAL
((vol A) / (r + 1)) - ((lower_bound A) - (lower_bound A)) is V11() real ext-real Element of 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
x - 1 is V11() real ext-real integer Element of REAL
x . (x - 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
(vol A) / (len x) is V11() real ext-real Element of REAL
((vol A) / (len x)) * (x - 1) is V11() real ext-real Element of REAL
(lower_bound A) + (((vol A) / (len x)) * (x - 1)) is V11() real ext-real Element of REAL
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 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 + 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
x . x is V11() real ext-real Element of REAL
((vol A) / (len x)) * x is V11() real ext-real Element of REAL
(lower_bound A) + (((vol A) / (len x)) * x) is V11() real ext-real Element of REAL
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 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 + 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
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 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 + 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
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
vol (divset (x,x)) is V11() real ext-real Element of REAL
y is 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
divset (x,1) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
vol (divset (x,1)) is V11() real ext-real Element of REAL
upper_bound (divset (x,1)) is V11() real ext-real Element of REAL
sup (divset (x,1)) is V11() real ext-real set
lower_bound (divset (x,1)) is V11() real ext-real Element of REAL
inf (divset (x,1)) is V11() real ext-real set
(upper_bound (divset (x,1))) - (lower_bound (divset (x,1))) is V11() real ext-real Element of REAL
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
x . 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
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
(vol A) / (len x) is V11() real ext-real Element of REAL
((vol A) / (len x)) * 1 is V11() real ext-real Element of REAL
(lower_bound A) + (((vol A) / (len x)) * 1) 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
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
x + 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) + ((vol A) / (len x)) is V11() real ext-real Element of REAL
((lower_bound A) + ((vol A) / (len x))) - (lower_bound A) is V11() real ext-real Element of REAL
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)) . 1 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
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
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
x + 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
r is V11() real ext-real Element of REAL
(vol A) / r is V11() real ext-real Element of REAL
[\((vol A) / r)/] is V11() real ext-real integer set
[\((vol A) / r)/] + 1 is V11() real ext-real integer Element of REAL
x is V11() real ext-real integer set
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
y + 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 * (y + 1) 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
1 * r is V11() real ext-real Element of REAL
(vol A) / (y + 1) is V11() real ext-real Element of REAL
(delta r) . y is V11() real ext-real Element of REAL
((vol A) / (y + 1)) - 0 is V11() real ext-real Element of REAL
abs (((vol A) / (y + 1)) - 0) 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
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
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
(delta r) . x is V11() real ext-real Element of REAL
r + 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
x + 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
(vol A) / (x + 1) is V11() real ext-real Element of REAL
(vol A) / (r + 1) is V11() real ext-real Element of REAL
r is V11() real ext-real set
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
(delta r) . x is V11() real ext-real Element of REAL
((delta r) . x) - 0 is V11() real ext-real Element of REAL
abs (((delta r) . x) - 0) is V11() real ext-real Element of REAL
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
(delta r) . y is V11() real ext-real Element of REAL
((delta r) . y) - 0 is V11() real ext-real Element of REAL
abs (((delta r) . y) - 0) is V11() real ext-real Element of REAL
lim (delta r) 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
the non empty V16() V19( NAT ) V20( divs A) Function-like total V30( NAT , divs A) Element of bool [:NAT,(divs A):] is non empty V16() V19( NAT ) V20( divs A) Function-like total V30( NAT , divs A) Element of bool [:NAT,(divs A):]
delta the non empty V16() V19( NAT ) V20( divs A) Function-like total V30( NAT , divs A) Element of bool [:NAT,(divs A):] 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:]
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer finite V42() set
(delta the non empty V16() V19( NAT ) V20( divs A) Function-like total V30( NAT , divs A) Element of bool [:NAT,(divs A):]) . r 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
the 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( REAL ) Function-like one-to-one finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A
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
delta x 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:]
[: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
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
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
sup (rng (upper_volume ((chi (A,A)),x))) is V11() real ext-real set
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
x . 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
x . 2 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
{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 Element of bool REAL
y 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
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
(upper_volume ((chi (A,A)),x)) . 1 is V11() real ext-real Element of REAL
divset (x,1) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
vol (divset (x,1)) is V11() real ext-real Element 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_bound (divset (x,1)) is V11() real ext-real Element of REAL
sup (divset (x,1)) 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
lower_bound (divset (x,1)) is V11() real ext-real Element of REAL
inf (divset (x,1)) is V11() real ext-real set
lower_bound A is V11() real ext-real Element of REAL
inf A is V11() real ext-real set
(upper_bound A) - (lower_bound A) is V11() real ext-real Element of REAL
y is set
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
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
(upper_volume ((chi (A,A)),x)) . x is V11() real ext-real Element 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
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
y is V11() real ext-real Element of REAL
divset (x,x) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
vol (divset (x,x)) is V11() real ext-real Element of REAL
(delta the non empty V16() V19( NAT ) V20( divs A) Function-like total V30( NAT , divs A) Element of bool [:NAT,(divs A):]) . 1 is V11() real ext-real Element of REAL
lim (delta the non empty V16() V19( NAT ) V20( divs A) Function-like total V30( NAT , divs A) Element of bool [:NAT,(divs 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
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
vol A is V11() real ext-real Element of REAL
vol A is V11() real ext-real Element of REAL
vol A is V11() real ext-real Element of REAL
f is non empty V16() V19( NAT ) V20( divs A) Function-like total V30( NAT , divs A) Element of bool [:NAT,(divs A):]
delta f 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 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
[: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
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
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
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
(lim (upper_sum (f,r))) - (lim (lower_sum (f,r))) 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
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
(lim (upper_sum (f,r))) - (lim (lower_sum (f,r))) 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
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
(lim (upper_sum (f,r))) - (lim (lower_sum (f,r))) is V11() real ext-real Element of REAL
upper_integral f is V11() real ext-real Element of REAL
(upper_integral f) - (lim (lower_sum (f,r))) is V11() real ext-real Element of REAL
lower_integral f is V11() real ext-real Element of REAL
(upper_integral f) - (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
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
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
(lim (upper_sum (f,r))) - (lim (lower_sum (f,r))) 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
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
(lim (upper_sum (f,r))) - (lim (lower_sum (f,r))) is V11() real ext-real Element of REAL
A is non empty set
[: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:]
max+ f is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
max- f is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
dom f is non empty Element of bool A
bool A is set
dom (max- f) is Element of bool A
dom (max+ f) is Element of bool A
A is non empty set
[: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 set
r is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
r | f is V16() V19(A) V19(f) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
max+ r is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
(max+ r) | f is V16() V19(A) V19(f) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
dom r is Element of bool A
bool A is set
f /\ (dom r) is Element of bool A
r is V11() real ext-real set
dom (max+ r) is Element of bool A
f /\ (dom (max+ r)) is Element of bool A
x is set
(max+ r) . x is V11() real ext-real Element of REAL
r . x is V11() real ext-real Element of REAL
max ((r . x),0) is V11() real ext-real set
max+ (r . x) is V11() real ext-real Element of REAL
x is set
(max+ r) . x is V11() real ext-real Element of REAL
r . x is V11() real ext-real Element of REAL
max ((r . x),0) is V11() real ext-real set
max+ (r . x) is V11() real ext-real Element of REAL
x is V11() real ext-real set
x is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
A is non empty set
[: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 set
r is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
max+ r is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
(max+ r) | f is V16() V19(A) V19(f) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
dom (max+ r) is Element of bool A
bool A is set
f /\ (dom (max+ r)) is Element of bool A
r is set
(max+ r) . r is V11() real ext-real Element of REAL
A is non empty set
[: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 set
r is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
r | f is V16() V19(A) V19(f) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
max- r is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
(max- r) | f is V16() V19(A) V19(f) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
dom r is Element of bool A
bool A is set
f /\ (dom r) is Element of bool A
r is V11() real ext-real set
dom (max- r) is Element of bool A
f /\ (dom (max- r)) is Element of bool A
x is set
(max- r) . x is V11() real ext-real Element of REAL
r . x is V11() real ext-real Element of REAL
- (r . x) is V11() real ext-real Element of REAL
max ((- (r . x)),0) is V11() real ext-real set
max- (r . x) is V11() real ext-real Element of REAL
- r is V11() real ext-real set
x is set
(max- r) . x is V11() real ext-real Element of REAL
r . x is V11() real ext-real Element of REAL
- (r . x) is V11() real ext-real Element of REAL
max ((- (r . x)),0) is V11() real ext-real set
max- (r . x) is V11() real ext-real Element of REAL
x is V11() real ext-real set
x is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
A is non empty set
[: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 set
r is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
max- r is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
(max- r) | f is V16() V19(A) V19(f) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
dom (max- r) is Element of bool A
bool A is set
f /\ (dom (max- r)) is Element of bool A
r is set
(max- r) . r 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 set
r is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,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:]
r | f is V16() V19(A) V19(f) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
rng (r | f) is V68() V69() V70() Element of bool REAL
rng r is V68() V69() V70() 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
[: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 set
r is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,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:]
r | f is V16() V19(A) V19(f) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
rng (r | f) is V68() V69() V70() Element of bool REAL
rng r is V68() V69() V70() 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
[: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:]
max+ f is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
(max+ f) | A is V16() V19(A) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,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
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 ((max+ 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 ((max+ f),r)) is V11() real ext-real Element of REAL
lower_sum ((max+ 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 ((max+ f),r)) is V11() real ext-real Element of REAL
(lim (upper_sum ((max+ f),r))) - (lim (lower_sum ((max+ f),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:]
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:]
(upper_sum (f,r)) - (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:]
- (lower_sum (f,r)) is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
- 1 is V11() real ext-real non positive integer set
(- 1) (#) (lower_sum (f,r)) is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(upper_sum (f,r)) + (- (lower_sum (f,r))) is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(upper_sum ((max+ f),r)) - (lower_sum ((max+ 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:]
- (lower_sum ((max+ f),r)) is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) (lower_sum ((max+ f),r)) is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(upper_sum ((max+ f),r)) + (- (lower_sum ((max+ f),r))) is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
lim (upper_sum (f,r)) is V11() real ext-real Element of REAL
lim (lower_sum (f,r)) is V11() real ext-real Element of REAL
(lim (upper_sum (f,r))) - (lim (lower_sum (f,r))) is V11() real ext-real Element of REAL
lim ((upper_sum (f,r)) - (lower_sum (f,r))) is V11() real ext-real Element of REAL
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:]
y is V11() real ext-real set
x 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:]
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
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
r . y is V11() real ext-real Element of REAL
(r . y) - 0 is V11() real ext-real Element of REAL
abs ((r . y) - 0) is V11() real ext-real Element of REAL
r . 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
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 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
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
upper_volume ((max+ 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 ((max+ 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
lower_volume ((max+ 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 ((max+ 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
n2 is V16() 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
n is V16() 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
n2 - n is V16() 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
K176() 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:]
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:]
id REAL is non empty V16() V19( REAL ) V20( REAL ) total V30( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
K173() is non empty V16() V19( REAL ) V20( REAL ) Function-like total V30( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
K258(REAL,K175(),(id REAL),K173()) 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:]
K211(K176(),n2,n) is set
- n is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K173() * n is V16() V19( NAT ) V20( REAL ) finite complex-valued ext-real-valued real-valued set
(- 1) (#) n is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K463((- 1)) is non empty V16() V19( REAL ) V20( REAL ) Function-like total V30( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
K177() 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:]
K213(K177(),(- 1),(id REAL)) is set
K463((- 1)) * n is V16() V19( NAT ) V20( REAL ) finite complex-valued ext-real-valued real-valued set
n2 + (- n) is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K211(K175(),n2,(- n)) is set
(upper_sum ((max+ f),r)) . y is V11() real ext-real Element of REAL
- (lower_sum ((max+ 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:]
(- (lower_sum ((max+ f),r))) . y is V11() real ext-real Element of REAL
((upper_sum ((max+ f),r)) . y) + ((- (lower_sum ((max+ f),r))) . y) is V11() real ext-real Element of REAL
(lower_sum ((max+ f),r)) . y is V11() real ext-real Element of REAL
- ((lower_sum ((max+ f),r)) . y) is V11() real ext-real Element of REAL
((upper_sum ((max+ f),r)) . y) + (- ((lower_sum ((max+ f),r)) . y)) is V11() real ext-real Element of REAL
((upper_sum ((max+ f),r)) . y) - ((lower_sum ((max+ f),r)) . y) is V11() real ext-real Element of REAL
upper_sum ((max+ f),(r . y)) is V11() real ext-real Element of REAL
(upper_sum ((max+ f),(r . y))) - ((lower_sum ((max+ f),r)) . y) is V11() real ext-real Element of REAL
lower_sum ((max+ f),(r . y)) is V11() real ext-real Element of REAL
(upper_sum ((max+ f),(r . y))) - (lower_sum ((max+ f),(r . y))) is V11() real ext-real Element of REAL
Sum (upper_volume ((max+ f),x)) is V11() real ext-real Element of REAL
K271(REAL,(upper_volume ((max+ f),x)),K175()) is V11() real ext-real Element of REAL
(Sum (upper_volume ((max+ f),x))) - (lower_sum ((max+ f),(r . y))) is V11() real ext-real Element of REAL
Sum (lower_volume ((max+ f),x)) is V11() real ext-real Element of REAL
K271(REAL,(lower_volume ((max+ f),x)),K175()) is V11() real ext-real Element of REAL
(Sum (upper_volume ((max+ f),x))) - (Sum (lower_volume ((max+ f),x))) is V11() real ext-real Element of REAL
Sum (n2 - n) is V11() real ext-real Element of REAL
K271(REAL,(n2 - n),K175()) is V11() real ext-real Element of REAL
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
y is V16() 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
n1 is V16() 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
y - n1 is V16() 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
K211(K176(),y,n1) is set
- n1 is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K173() * n1 is V16() V19( NAT ) V20( REAL ) finite complex-valued ext-real-valued real-valued set
(- 1) (#) n1 is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K463((- 1)) * n1 is V16() V19( NAT ) V20( REAL ) finite complex-valued ext-real-valued real-valued set
y + (- n1) is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K211(K175(),y,(- n1)) is set
D is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer finite V42() set
(n2 - n) . D is V11() real ext-real Element of REAL
(y - n1) . D is V11() real ext-real Element of 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
n . D is V11() real ext-real Element of REAL
divset (x,D) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
(max+ f) | (divset (x,D)) is V16() V19(A) V19( divset (x,D)) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
rng ((max+ f) | (divset (x,D))) is V68() V69() V70() Element of bool REAL
lower_bound (rng ((max+ f) | (divset (x,D)))) is V11() real ext-real Element of REAL
vol (divset (x,D)) is V11() real ext-real Element of REAL
(lower_bound (rng ((max+ f) | (divset (x,D))))) * (vol (divset (x,D))) is V11() real ext-real Element of REAL
f | (divset (x,D)) is V16() V19(A) V19( divset (x,D)) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
rng (f | (divset (x,D))) is V68() V69() V70() Element of bool REAL
rng f is non empty V68() V69() V70() Element of bool REAL
LV2 is V11() real ext-real Element of REAL
dom f is non empty V68() V69() V70() Element of bool A
bool A is set
f . LV2 is V11() real ext-real Element of REAL
upper_bound (rng ((max+ f) | (divset (x,D)))) is V11() real ext-real Element of REAL
(upper_bound (rng ((max+ f) | (divset (x,D))))) - (lower_bound (rng ((max+ f) | (divset (x,D))))) is V11() real ext-real Element of REAL
upper_bound (rng (f | (divset (x,D)))) is V11() real ext-real Element of REAL
lower_bound (rng (f | (divset (x,D)))) is V11() real ext-real Element of REAL
(upper_bound (rng (f | (divset (x,D))))) - (lower_bound (rng (f | (divset (x,D))))) is V11() real ext-real Element of REAL
dom f is non empty V68() V69() V70() Element of bool A
bool A is set
dom (max+ f) is V68() V69() V70() Element of bool A
dom (f | (divset (x,D))) is V68() V69() V70() Element of bool A
(dom f) /\ (divset (x,D)) is V68() V69() V70() Element of bool REAL
A /\ (divset (x,D)) is V68() V69() V70() interval Element of bool REAL
dom ((max+ f) | (divset (x,D))) is V68() V69() V70() Element of bool A
H is V11() real ext-real set
G is V11() real ext-real Element of A
((max+ f) | (divset (x,D))) . G is V11() real ext-real Element of REAL
max+ (f | (divset (x,D))) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
(max+ (f | (divset (x,D)))) . G is V11() real ext-real Element of REAL
dom (max+ (f | (divset (x,D)))) is V68() V69() V70() Element of bool A
(f | (divset (x,D))) . G is V11() real ext-real Element of REAL
max+ ((f | (divset (x,D))) . G) is V11() real ext-real Element of REAL
max (((f | (divset (x,D))) . G),0) is V11() real ext-real set
H is V11() real ext-real set
(lower_bound (rng (f | (divset (x,D))))) + H is V11() real ext-real Element of REAL
G is V11() real ext-real set
F is V11() real ext-real Element of REAL
j is V11() real ext-real Element of A
(f | (divset (x,D))) . j is V11() real ext-real Element of REAL
max+ (f | (divset (x,D))) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
dom (max+ (f | (divset (x,D)))) is V68() V69() V70() Element of bool A
(max+ (f | (divset (x,D)))) . j is V11() real ext-real Element of REAL
max+ F is V11() real ext-real Element of REAL
max (F,0) is V11() real ext-real set
rng (max+ (f | (divset (x,D)))) is V68() V69() V70() Element of bool REAL
H is V11() real ext-real set
G is V11() real ext-real Element of A
((max+ f) | (divset (x,D))) . G is V11() real ext-real Element of REAL
max+ (f | (divset (x,D))) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
dom (max+ (f | (divset (x,D)))) is V68() V69() V70() Element of bool A
(f | (divset (x,D))) . G is V11() real ext-real Element of REAL
(max+ (f | (divset (x,D)))) . G is V11() real ext-real Element of REAL
max+ ((f | (divset (x,D))) . G) is V11() real ext-real Element of REAL
max (((f | (divset (x,D))) . G),0) is V11() real ext-real set
H is V11() real ext-real set
(upper_bound (rng (f | (divset (x,D))))) - H is V11() real ext-real Element of REAL
G is V11() real ext-real set
j is V11() real ext-real Element of A
(f | (divset (x,D))) . j is V11() real ext-real Element of REAL
max+ (f | (divset (x,D))) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
dom (max+ (f | (divset (x,D)))) is V68() V69() V70() Element of bool A
(max+ (f | (divset (x,D)))) . j is V11() real ext-real Element of REAL
F is V11() real ext-real Element of REAL
max+ F is V11() real ext-real Element of REAL
max (G,0) is V11() real ext-real set
rng (max+ (f | (divset (x,D)))) is V68() V69() V70() Element of bool REAL
H is V11() real ext-real set
0 + H is V11() real ext-real Element of REAL
(lower_bound (rng (f | (divset (x,D))))) + H is V11() real ext-real Element of REAL
G is V11() real ext-real set
F is V11() real ext-real Element of A
(f | (divset (x,D))) . F is V11() real ext-real Element of REAL
max+ (f | (divset (x,D))) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
dom (max+ (f | (divset (x,D)))) is V68() V69() V70() Element of bool A
(max+ (f | (divset (x,D)))) . F is V11() real ext-real Element of REAL
max+ ((f | (divset (x,D))) . F) is V11() real ext-real Element of REAL
max (((f | (divset (x,D))) . F),0) is V11() real ext-real set
rng (max+ (f | (divset (x,D)))) is V68() V69() V70() Element of bool REAL
G - H is V11() real ext-real set
j is V11() real ext-real Element of REAL
H is V11() real ext-real set
max+ (f | (divset (x,D))) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
rng (max+ (f | (divset (x,D)))) is V68() V69() V70() Element of bool REAL
dom (max+ (f | (divset (x,D)))) is V68() V69() V70() Element of bool A
G is V11() real ext-real Element of A
(max+ (f | (divset (x,D)))) . G is V11() real ext-real Element of REAL
H is V11() real ext-real Element of REAL
G is V11() real ext-real Element of A
((max+ f) | (divset (x,D))) . G is V11() real ext-real Element of REAL
max+ (f | (divset (x,D))) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
(max+ (f | (divset (x,D)))) . G is V11() real ext-real Element of REAL
dom (max+ (f | (divset (x,D)))) is V68() V69() V70() Element of bool A
(f | (divset (x,D))) . G is V11() real ext-real Element of REAL
max+ ((f | (divset (x,D))) . G) is V11() real ext-real Element of REAL
max (((f | (divset (x,D))) . G),0) is V11() real ext-real set
H is V11() real ext-real set
H is V11() real ext-real set
(upper_bound (rng (f | (divset (x,D))))) - H is V11() real ext-real Element of REAL
H is V11() real ext-real set
(upper_bound (rng (f | (divset (x,D))))) - H is V11() real ext-real Element of REAL
G is V11() real ext-real set
F is V11() real ext-real Element of A
(f | (divset (x,D))) . F is V11() real ext-real Element of REAL
max+ (f | (divset (x,D))) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
dom (max+ (f | (divset (x,D)))) is V68() V69() V70() Element of bool A
((max+ f) | (divset (x,D))) . F is V11() real ext-real Element of REAL
(max+ (f | (divset (x,D)))) . F is V11() real ext-real Element of REAL
max+ ((f | (divset (x,D))) . F) is V11() real ext-real Element of REAL
max (G,0) is V11() real ext-real set
H is V11() real ext-real set
0 + H is V11() real ext-real Element of REAL
G is V11() real ext-real Element of REAL
F is V11() real ext-real Element of A
((max+ f) | (divset (x,D))) . F is V11() real ext-real Element of REAL
max+ (f | (divset (x,D))) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
dom (max+ (f | (divset (x,D)))) is V68() V69() V70() Element of bool A
(f | (divset (x,D))) . F is V11() real ext-real Element of REAL
(max+ (f | (divset (x,D)))) . F is V11() real ext-real Element of REAL
max+ ((f | (divset (x,D))) . F) is V11() real ext-real Element of REAL
max (((f | (divset (x,D))) . F),0) is V11() real ext-real set
H is V11() real ext-real set
G is V11() real ext-real Element of A
((max+ f) | (divset (x,D))) . G is V11() real ext-real Element of REAL
max+ (f | (divset (x,D))) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
(max+ (f | (divset (x,D)))) . G is V11() real ext-real Element of REAL
H is V11() real ext-real set
G is V11() real ext-real Element of A
((max+ f) | (divset (x,D))) . G is V11() real ext-real Element of REAL
max+ (f | (divset (x,D))) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
dom (max+ (f | (divset (x,D)))) is V68() V69() V70() Element of bool A
(f | (divset (x,D))) . G is V11() real ext-real Element of REAL
(max+ (f | (divset (x,D)))) . G is V11() real ext-real Element of REAL
max+ ((f | (divset (x,D))) . G) is V11() real ext-real Element of REAL
max (((f | (divset (x,D))) . G),0) is V11() real ext-real set
H is V11() real ext-real set
0 - H is V11() real ext-real Element of REAL
G is V11() real ext-real Element of REAL
F is V11() real ext-real Element of A
((max+ f) | (divset (x,D))) . F is V11() real ext-real Element of REAL
max+ (f | (divset (x,D))) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
(max+ (f | (divset (x,D)))) . F is V11() real ext-real Element of REAL
H is V11() real ext-real Element of REAL
H is V11() real ext-real Element of REAL
n1 . D is V11() real ext-real Element of REAL
(lower_bound (rng (f | (divset (x,D))))) * (vol (divset (x,D))) is V11() real ext-real Element of REAL
y . D is V11() real ext-real Element of REAL
(upper_bound (rng (f | (divset (x,D))))) * (vol (divset (x,D))) is V11() real ext-real Element of REAL
((upper_bound (rng (f | (divset (x,D))))) * (vol (divset (x,D)))) - ((lower_bound (rng (f | (divset (x,D))))) * (vol (divset (x,D)))) is V11() real ext-real Element of REAL
((upper_bound (rng (f | (divset (x,D))))) - (lower_bound (rng (f | (divset (x,D)))))) * (vol (divset (x,D))) is V11() real ext-real Element of REAL
n2 . D is V11() real ext-real Element of REAL
(upper_bound (rng ((max+ f) | (divset (x,D))))) * (vol (divset (x,D))) is V11() real ext-real Element of REAL
((upper_bound (rng ((max+ f) | (divset (x,D))))) * (vol (divset (x,D)))) - ((lower_bound (rng ((max+ f) | (divset (x,D))))) * (vol (divset (x,D)))) is V11() real ext-real Element of REAL
((upper_bound (rng ((max+ f) | (divset (x,D))))) - (lower_bound (rng ((max+ f) | (divset (x,D)))))) * (vol (divset (x,D))) is V11() real ext-real Element of REAL
x . y is V11() real ext-real Element of REAL
(x . y) - 0 is V11() real ext-real Element of REAL
abs ((x . y) - 0) is V11() real ext-real Element of REAL
m is V16() V19( NAT ) V20( REAL ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
dom m is finite V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of bool NAT
D is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer finite V42() set
m . D is V11() real ext-real Element of REAL
rng (max+ f) is V68() V69() V70() Element of bool REAL
len m 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 m) is finite V44( len m) V68() V69() V70() V71() V72() V73() 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
n . D is V11() real ext-real Element of REAL
divset (x,D) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
(max+ f) | (divset (x,D)) is V16() V19(A) V19( divset (x,D)) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
rng ((max+ f) | (divset (x,D))) is V68() V69() V70() Element of bool REAL
lower_bound (rng ((max+ f) | (divset (x,D)))) is V11() real ext-real Element of REAL
vol (divset (x,D)) is V11() real ext-real Element of REAL
(lower_bound (rng ((max+ f) | (divset (x,D))))) * (vol (divset (x,D))) is V11() real ext-real Element of REAL
LV is V11() real ext-real Element of REAL
dom f is non empty V68() V69() V70() Element of bool A
bool A is set
(dom f) /\ (divset (x,D)) is V68() V69() V70() Element of bool REAL
f | (divset (x,D)) is V16() V19(A) V19( divset (x,D)) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
dom (f | (divset (x,D))) is V68() V69() V70() Element of bool A
max+ (f | (divset (x,D))) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
dom (max+ (f | (divset (x,D)))) is V68() V69() V70() Element of bool A
dom ((max+ f) | (divset (x,D))) is V68() V69() V70() Element of bool A
((max+ f) | (divset (x,D))) . LV is V11() real ext-real Element of REAL
upper_bound (rng ((max+ f) | (divset (x,D)))) is V11() real ext-real Element of REAL
(upper_bound (rng ((max+ f) | (divset (x,D))))) - (lower_bound (rng ((max+ f) | (divset (x,D))))) is V11() real ext-real Element of REAL
LV is V11() real ext-real Element of REAL
n2 . D is V11() real ext-real Element of REAL
(upper_bound (rng ((max+ f) | (divset (x,D))))) * (vol (divset (x,D))) is V11() real ext-real Element of REAL
((upper_bound (rng ((max+ f) | (divset (x,D))))) * (vol (divset (x,D)))) - ((lower_bound (rng ((max+ f) | (divset (x,D))))) * (vol (divset (x,D)))) is V11() real ext-real Element of REAL
((upper_bound (rng ((max+ f) | (divset (x,D))))) - (lower_bound (rng ((max+ f) | (divset (x,D)))))) * (vol (divset (x,D))) is V11() real ext-real Element of REAL
(upper_sum (f,r)) . y 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:]
(- (lower_sum (f,r))) . y is V11() real ext-real Element of REAL
((upper_sum (f,r)) . y) + ((- (lower_sum (f,r))) . y) is V11() real ext-real Element of REAL
(lower_sum (f,r)) . y is V11() real ext-real Element of REAL
- ((lower_sum (f,r)) . y) is V11() real ext-real Element of REAL
((upper_sum (f,r)) . y) + (- ((lower_sum (f,r)) . y)) is V11() real ext-real Element of REAL
((upper_sum (f,r)) . y) - ((lower_sum (f,r)) . y) is V11() real ext-real Element of REAL
upper_sum (f,(r . y)) is V11() real ext-real Element of REAL
(upper_sum (f,(r . y))) - ((lower_sum (f,r)) . y) is V11() real ext-real Element of REAL
lower_sum (f,(r . y)) is V11() real ext-real Element of REAL
(upper_sum (f,(r . y))) - (lower_sum (f,(r . y))) is V11() real ext-real Element of REAL
Sum (upper_volume (f,x)) is V11() real ext-real Element of REAL
K271(REAL,(upper_volume (f,x)),K175()) is V11() real ext-real Element of REAL
(Sum (upper_volume (f,x))) - (lower_sum (f,(r . y))) is V11() real ext-real Element of REAL
Sum (lower_volume (f,x)) is V11() real ext-real Element of REAL
K271(REAL,(lower_volume (f,x)),K175()) is V11() real ext-real Element of REAL
(Sum (upper_volume (f,x))) - (Sum (lower_volume (f,x))) is V11() real ext-real Element of REAL
Sum (y - n1) is V11() real ext-real Element of REAL
K271(REAL,(y - n1),K175()) is V11() real ext-real Element of REAL
abs (x . y) is V11() real ext-real Element of REAL
lim ((upper_sum ((max+ f),r)) - (lower_sum ((max+ f),r))) is V11() real ext-real Element of REAL
A is non empty set
[: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 V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
max- f 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:]
- 1 is V11() real ext-real non positive integer set
(- 1) (#) f is V16() V19(A) Function-like complex-valued ext-real-valued real-valued set
max+ (- f) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
dom (max+ (- f)) is Element of bool A
bool A is set
dom (- f) is Element of bool A
dom f is Element of bool A
dom (max- f) is Element of bool A
r is Element of A
(max- f) . r is V11() real ext-real Element of REAL
(max+ (- f)) . r is V11() real ext-real Element of REAL
(- f) . r is V11() real ext-real Element of REAL
max+ ((- f) . r) is V11() real ext-real Element of REAL
max (((- f) . r),0) is V11() real ext-real set
f . r is V11() real ext-real Element of REAL
- (f . r) is V11() real ext-real Element of REAL
max ((- (f . r)),0) is V11() real ext-real set
max- (f . r) 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:]
max- f is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,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:]
- 1 is V11() real ext-real non positive integer set
(- 1) (#) f is V16() V19(A) Function-like total complex-valued ext-real-valued real-valued set
(- f) | A is V16() V19(A) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
- 1 is V11() real ext-real non positive integer Element of REAL
(- 1) (#) 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:]
max+ (- f) is V16() 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 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:]
abs 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:]
integral f is V11() real ext-real Element of REAL
abs (integral f) is V11() real ext-real Element of REAL
integral (abs f) is V11() real ext-real Element of REAL
max- f is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
max+ f is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
(max+ f) | A is V16() V19(A) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
(max- f) | A is V16() V19(A) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
(max+ f) + (max- f) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
integral (max+ f) is V11() real ext-real Element of REAL
integral (max- f) is V11() real ext-real Element of REAL
(integral (max+ f)) - (integral (max- f)) is V11() real ext-real Element of REAL
(max+ f) - (max- f) is V16() V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
- (max- f) is V16() V19(A) Function-like complex-valued ext-real-valued real-valued set
- 1 is V11() real ext-real non positive integer set
(- 1) (#) (max- f) is V16() V19(A) Function-like complex-valued ext-real-valued real-valued set
(max+ f) + (- (max- f)) is V16() V19(A) Function-like complex-valued ext-real-valued real-valued set
integral ((max+ f) - (max- f)) is V11() real ext-real Element of REAL
(integral (max+ f)) + (integral (max- f)) is V11() real ext-real Element of REAL
integral ((max+ f) + (max- f)) is V11() real ext-real Element of REAL
(integral (abs f)) - (integral f) is V11() real ext-real Element of REAL
2 * (integral (max- f)) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
(max- f) . r is V11() real ext-real Element of REAL
(integral (abs f)) + (integral f) is V11() real ext-real Element of REAL
2 * (integral (max+ f)) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
(max+ f) . r is V11() real ext-real Element of REAL
- (integral (abs f)) is V11() real ext-real Element of REAL
A is V11() real ext-real Element of REAL
f is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
[:f,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set
bool [:f,REAL:] is non trivial non finite set
r is non empty V16() V19(f) V20( REAL ) Function-like total V30(f, REAL ) complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
rng r is non empty V68() V69() V70() Element of bool REAL
upper_bound (rng r) is V11() real ext-real Element of REAL
lower_bound (rng r) is V11() real ext-real Element of REAL
(upper_bound (rng r)) - (lower_bound (rng r)) is V11() real ext-real Element of REAL
(upper_bound (rng r)) - A is V11() real ext-real Element of REAL
r is V11() real ext-real set
r . r is V11() real ext-real Element of REAL
A + (r . r) is V11() real ext-real Element of REAL
x is V11() real ext-real set
dom r is non empty V68() V69() V70() Element of bool f
bool f is set
y is V11() real ext-real Element of f
r . y is V11() real ext-real Element of REAL
(r . y) - (r . r) is V11() real ext-real Element of REAL
abs ((r . y) - (r . r)) is V11() real ext-real Element of REAL
r is V11() real ext-real set
dom r is non empty V68() V69() V70() Element of bool f
bool f is set
x is V11() real ext-real Element of f
r . x is V11() real ext-real Element of REAL
A + (lower_bound (rng r)) is V11() real ext-real Element of REAL
A is V11() real ext-real Element of REAL
f is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
[:f,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set
bool [:f,REAL:] is non trivial non finite set
r is non empty V16() V19(f) V20( REAL ) Function-like total V30(f, REAL ) complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
r | f is V16() V19(f) V19(f) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
r is non empty V16() V19(f) V20( REAL ) Function-like total V30(f, REAL ) complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
rng r is non empty V68() V69() V70() Element of bool REAL
upper_bound (rng r) is V11() real ext-real Element of REAL
lower_bound (rng r) is V11() real ext-real Element of REAL
(upper_bound (rng r)) - (lower_bound (rng r)) is V11() real ext-real Element of REAL
rng r is non empty V68() V69() V70() Element of bool REAL
upper_bound (rng r) is V11() real ext-real Element of REAL
lower_bound (rng r) is V11() real ext-real Element of REAL
(upper_bound (rng r)) - (lower_bound (rng r)) is V11() real ext-real Element of REAL
A * ((upper_bound (rng r)) - (lower_bound (rng r))) is V11() real ext-real Element of REAL
dom r is non empty V68() V69() V70() Element of bool f
bool f is set
x is V11() real ext-real Element of REAL
r . x is V11() real ext-real Element of REAL
y is V11() real ext-real Element of REAL
r . y is V11() real ext-real Element of REAL
(r . x) - (r . y) is V11() real ext-real Element of REAL
abs ((r . x) - (r . y)) is V11() real ext-real Element of REAL
(abs ((r . x) - (r . y))) + (r . y) is V11() real ext-real Element of REAL
(upper_bound (rng r)) - (abs ((r . x) - (r . y))) is V11() real ext-real Element of REAL
(lower_bound (rng r)) + (abs ((r . x) - (r . y))) is V11() real ext-real Element of REAL
- ((r . x) - (r . y)) is V11() real ext-real Element of REAL
(r . y) - (r . x) is V11() real ext-real Element of REAL
(abs ((r . x) - (r . y))) + (r . x) is V11() real ext-real Element of REAL
(upper_bound (rng r)) - (abs ((r . x) - (r . y))) is V11() real ext-real Element of REAL
(lower_bound (rng r)) + (abs ((r . x) - (r . y))) is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
r . x is V11() real ext-real Element of REAL
y is V11() real ext-real Element of REAL
r . y is V11() real ext-real Element of REAL
(r . x) - (r . y) is V11() real ext-real Element of REAL
abs ((r . x) - (r . y)) is V11() real ext-real Element of REAL
r . x is V11() real ext-real Element of REAL
r . y is V11() real ext-real Element of REAL
(r . x) - (r . y) is V11() real ext-real Element of REAL
abs ((r . x) - (r . y)) is V11() real ext-real Element of REAL
A * (abs ((r . x) - (r . y))) is V11() real ext-real Element of REAL
A is V11() real ext-real Element of REAL
f is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
[:f,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set
bool [:f,REAL:] is non trivial non finite set
r is non empty V16() V19(f) V20( REAL ) Function-like total V30(f, REAL ) complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
r | f is V16() V19(f) V19(f) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
r is non empty V16() V19(f) V20( REAL ) Function-like total V30(f, REAL ) complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
r | f is V16() V19(f) V19(f) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
x is non empty V16() V19(f) V20( REAL ) Function-like total V30(f, REAL ) complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
rng x is non empty V68() V69() V70() Element of bool REAL
upper_bound (rng x) is V11() real ext-real Element of REAL
lower_bound (rng x) is V11() real ext-real Element of REAL
(upper_bound (rng x)) - (lower_bound (rng x)) is V11() real ext-real Element of REAL
rng r is non empty V68() V69() V70() Element of bool REAL
upper_bound (rng r) is V11() real ext-real Element of REAL
lower_bound (rng r) is V11() real ext-real Element of REAL
(upper_bound (rng r)) - (lower_bound (rng r)) is V11() real ext-real Element of REAL
rng r is non empty V68() V69() V70() Element of bool REAL
upper_bound (rng r) is V11() real ext-real Element of REAL
lower_bound (rng r) is V11() real ext-real Element of REAL
(upper_bound (rng r)) - (lower_bound (rng r)) is V11() real ext-real Element of REAL
((upper_bound (rng r)) - (lower_bound (rng r))) + ((upper_bound (rng r)) - (lower_bound (rng r))) is V11() real ext-real Element of REAL
A * (((upper_bound (rng r)) - (lower_bound (rng r))) + ((upper_bound (rng r)) - (lower_bound (rng r)))) is V11() real ext-real Element of REAL
dom r is non empty V68() V69() V70() Element of bool f
bool f is set
y is V11() real ext-real Element of REAL
r . y is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
r . x is V11() real ext-real Element of REAL
(r . y) - (r . x) is V11() real ext-real Element of REAL
abs ((r . y) - (r . x)) is V11() real ext-real Element of REAL
(abs ((r . y) - (r . x))) + (r . x) is V11() real ext-real Element of REAL
(upper_bound (rng r)) - (abs ((r . y) - (r . x))) is V11() real ext-real Element of REAL
(lower_bound (rng r)) + (abs ((r . y) - (r . x))) is V11() real ext-real Element of REAL
- ((r . y) - (r . x)) is V11() real ext-real Element of REAL
(r . x) - (r . y) is V11() real ext-real Element of REAL
(abs ((r . y) - (r . x))) + (r . y) is V11() real ext-real Element of REAL
(upper_bound (rng r)) - (abs ((r . y) - (r . x))) is V11() real ext-real Element of REAL
(lower_bound (rng r)) + (abs ((r . y) - (r . x))) is V11() real ext-real Element of REAL
dom r is non empty V68() V69() V70() Element of bool f
y is V11() real ext-real Element of REAL
r . y is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
r . x is V11() real ext-real Element of REAL
(r . y) - (r . x) is V11() real ext-real Element of REAL
abs ((r . y) - (r . x)) is V11() real ext-real Element of REAL
(abs ((r . y) - (r . x))) + (r . x) is V11() real ext-real Element of REAL
(upper_bound (rng r)) - (abs ((r . y) - (r . x))) is V11() real ext-real Element of REAL
(lower_bound (rng r)) + (abs ((r . y) - (r . x))) is V11() real ext-real Element of REAL
- ((r . y) - (r . x)) is V11() real ext-real Element of REAL
(r . x) - (r . y) is V11() real ext-real Element of REAL
(abs ((r . y) - (r . x))) + (r . y) is V11() real ext-real Element of REAL
(upper_bound (rng r)) - (abs ((r . y) - (r . x))) is V11() real ext-real Element of REAL
(lower_bound (rng r)) + (abs ((r . y) - (r . x))) is V11() real ext-real Element of REAL
y is V11() real ext-real Element of REAL
x . y is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
x . x is V11() real ext-real Element of REAL
(x . y) - (x . x) is V11() real ext-real Element of REAL
abs ((x . y) - (x . x)) is V11() real ext-real Element of REAL
r . y is V11() real ext-real Element of REAL
r . x is V11() real ext-real Element of REAL
(r . y) - (r . x) is V11() real ext-real Element of REAL
abs ((r . y) - (r . x)) is V11() real ext-real Element of REAL
A * (abs ((r . y) - (r . x))) is V11() real ext-real Element of REAL
A * ((upper_bound (rng r)) - (lower_bound (rng r))) is V11() real ext-real Element of REAL
r . y is V11() real ext-real Element of REAL
r . x is V11() real ext-real Element of REAL
(r . y) - (r . x) is V11() real ext-real Element of REAL
abs ((r . y) - (r . x)) is V11() real ext-real Element of REAL
A * (abs ((r . y) - (r . x))) is V11() real ext-real Element of REAL
A * ((upper_bound (rng r)) - (lower_bound (rng r))) is V11() real ext-real Element of REAL
(A * (abs ((r . y) - (r . x)))) + (A * (abs ((r . y) - (r . x)))) is V11() real ext-real Element of REAL
(A * ((upper_bound (rng r)) - (lower_bound (rng r)))) + (A * ((upper_bound (rng r)) - (lower_bound (rng r)))) is V11() real ext-real Element of REAL
(abs ((r . y) - (r . x))) + (abs ((r . y) - (r . x))) is V11() real ext-real Element of REAL
A * ((abs ((r . y) - (r . x))) + (abs ((r . y) - (r . x)))) is V11() real ext-real Element of REAL
A is V11() real ext-real Element of REAL
f is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
[:f,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set
bool [:f,REAL:] is non trivial non finite set
r is non empty V16() V19(f) V20( REAL ) Function-like total V30(f, REAL ) complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
r | f is V16() V19(f) V19(f) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
r is non empty V16() V19(f) V20( REAL ) Function-like total V30(f, REAL ) complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
r | f is V16() V19(f) V19(f) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
divs f is non empty set
[:NAT,(divs f):] is non trivial V16() non finite set
bool [:NAT,(divs f):] is non trivial non finite set
x is non empty V16() V19( NAT ) V20( divs f) Function-like total V30( NAT , divs f) Element of bool [:NAT,(divs f):]
delta x 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 x) is V11() real ext-real Element of REAL
upper_sum (r,x) 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 (r,x)) is V11() real ext-real Element of REAL
lower_sum (r,x) 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 (r,x)) is V11() real ext-real Element of REAL
(lim (upper_sum (r,x))) - (lim (lower_sum (r,x))) is V11() real ext-real Element of REAL
lower_sum (r,x) 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:]
upper_sum (r,x) 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:]
(upper_sum (r,x)) - (lower_sum (r,x)) 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:]
- (lower_sum (r,x)) is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
- 1 is V11() real ext-real non positive integer set
(- 1) (#) (lower_sum (r,x)) is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(upper_sum (r,x)) + (- (lower_sum (r,x))) is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(upper_sum (r,x)) - (lower_sum (r,x)) 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:]
- (lower_sum (r,x)) is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) (lower_sum (r,x)) is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(upper_sum (r,x)) + (- (lower_sum (r,x))) is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
lim (upper_sum (r,x)) is V11() real ext-real Element of REAL
lim (lower_sum (r,x)) is V11() real ext-real Element of REAL
(lim (upper_sum (r,x))) - (lim (lower_sum (r,x))) is V11() real ext-real Element of REAL
lim ((upper_sum (r,x)) - (lower_sum (r,x))) is V11() real ext-real Element of REAL
y 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:]
y is V11() real ext-real set
y / A is V11() real ext-real Element of REAL
x 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:]
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
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
y . y is V11() real ext-real Element of REAL
(y . y) - 0 is V11() real ext-real Element of REAL
abs ((y . y) - 0) is V11() real ext-real Element of REAL
x . 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 f
n1 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 f
upper_volume (r,n1) 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 (r,n1)) 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 n1 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 n1) -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 n1 } is set
lower_volume (r,n1) 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 (r,n1)) 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
x . y is V11() real ext-real Element of REAL
(upper_sum (r,x)) . y is V11() real ext-real Element of REAL
- (lower_sum (r,x)) 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:]
(- (lower_sum (r,x))) . y is V11() real ext-real Element of REAL
((upper_sum (r,x)) . y) + ((- (lower_sum (r,x))) . y) is V11() real ext-real Element of REAL
(lower_sum (r,x)) . y is V11() real ext-real Element of REAL
- ((lower_sum (r,x)) . y) is V11() real ext-real Element of REAL
((upper_sum (r,x)) . y) + (- ((lower_sum (r,x)) . y)) is V11() real ext-real Element of REAL
((upper_sum (r,x)) . y) - ((lower_sum (r,x)) . y) is V11() real ext-real Element of REAL
upper_sum (r,(x . y)) is V11() real ext-real Element of REAL
(upper_sum (r,(x . y))) - ((lower_sum (r,x)) . y) is V11() real ext-real Element of REAL
lower_sum (r,(x . y)) is V11() real ext-real Element of REAL
(upper_sum (r,(x . y))) - (lower_sum (r,(x . y))) is V11() real ext-real Element of REAL
Sum (upper_volume (r,n1)) 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 (r,n1)),K175()) is V11() real ext-real Element of REAL
(Sum (upper_volume (r,n1))) - (lower_sum (r,(x . y))) is V11() real ext-real Element of REAL
Sum (lower_volume (r,n1)) is V11() real ext-real Element of REAL
K271(REAL,(lower_volume (r,n1)),K175()) is V11() real ext-real Element of REAL
(Sum (upper_volume (r,n1))) - (Sum (lower_volume (r,n1))) is V11() real ext-real Element of REAL
n2 is V16() V19( NAT ) V20( REAL ) Function-like finite V44( len n1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len n1) -tuples_on REAL
n is V16() V19( NAT ) V20( REAL ) Function-like finite V44( len n1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len n1) -tuples_on REAL
n2 - n is V16() V19( NAT ) V20( REAL ) Function-like finite V44( len n1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len n1) -tuples_on REAL
K176() 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:]
id REAL is non empty V16() V19( REAL ) V20( REAL ) total V30( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
K173() is non empty V16() V19( REAL ) V20( REAL ) Function-like total V30( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
K258(REAL,K175(),(id REAL),K173()) 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:]
K211(K176(),n2,n) is set
- n is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K173() * n is V16() V19( NAT ) V20( REAL ) finite complex-valued ext-real-valued real-valued set
(- 1) (#) n is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K463((- 1)) is non empty V16() V19( REAL ) V20( REAL ) Function-like total V30( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
K177() 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:]
K213(K177(),(- 1),(id REAL)) is set
K463((- 1)) * n is V16() V19( NAT ) V20( REAL ) finite complex-valued ext-real-valued real-valued set
n2 + (- n) is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K211(K175(),n2,(- n)) is set
Sum (n2 - n) is V11() real ext-real Element of REAL
K271(REAL,(n2 - n),K175()) is V11() real ext-real Element of REAL
(x . y) - 0 is V11() real ext-real Element of REAL
abs ((x . y) - 0) is V11() real ext-real Element of REAL
lower_volume (r,n1) 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 (r,n1)) 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 (r,n1) 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 (r,n1)) 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
D is V16() V19( NAT ) V20( REAL ) Function-like finite V44( len n1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len n1) -tuples_on REAL
m is V16() V19( NAT ) V20( REAL ) Function-like finite V44( len n1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len n1) -tuples_on REAL
D - m is V16() V19( NAT ) V20( REAL ) Function-like finite V44( len n1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len n1) -tuples_on REAL
K211(K176(),D,m) is set
- m is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K173() * m is V16() V19( NAT ) V20( REAL ) finite complex-valued ext-real-valued real-valued set
(- 1) (#) m is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K463((- 1)) * m is V16() V19( NAT ) V20( REAL ) finite complex-valued ext-real-valued real-valued set
D + (- m) is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K211(K175(),D,(- m)) is set
(upper_sum (r,x)) . y is V11() real ext-real Element of REAL
- (lower_sum (r,x)) 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:]
(- (lower_sum (r,x))) . y is V11() real ext-real Element of REAL
((upper_sum (r,x)) . y) + ((- (lower_sum (r,x))) . y) is V11() real ext-real Element of REAL
(lower_sum (r,x)) . y is V11() real ext-real Element of REAL
- ((lower_sum (r,x)) . y) is V11() real ext-real Element of REAL
((upper_sum (r,x)) . y) + (- ((lower_sum (r,x)) . y)) is V11() real ext-real Element of REAL
((upper_sum (r,x)) . y) - ((lower_sum (r,x)) . y) is V11() real ext-real Element of REAL
upper_sum (r,(x . y)) is V11() real ext-real Element of REAL
(upper_sum (r,(x . y))) - ((lower_sum (r,x)) . y) is V11() real ext-real Element of REAL
lower_sum (r,(x . y)) is V11() real ext-real Element of REAL
(upper_sum (r,(x . y))) - (lower_sum (r,(x . y))) is V11() real ext-real Element of REAL
Sum (upper_volume (r,n1)) is V11() real ext-real Element of REAL
K271(REAL,(upper_volume (r,n1)),K175()) is V11() real ext-real Element of REAL
(Sum (upper_volume (r,n1))) - (lower_sum (r,(x . y))) is V11() real ext-real Element of REAL
Sum (lower_volume (r,n1)) is V11() real ext-real Element of REAL
K271(REAL,(lower_volume (r,n1)),K175()) is V11() real ext-real Element of REAL
(Sum (upper_volume (r,n1))) - (Sum (lower_volume (r,n1))) is V11() real ext-real Element of REAL
Sum (D - m) is V11() real ext-real Element of REAL
K271(REAL,(D - m),K175()) is V11() real ext-real Element of REAL
UV is V16() V19( NAT ) V20( REAL ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
dom UV is finite V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of bool NAT
LV is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer finite V42() set
UV . LV is V11() real ext-real Element of REAL
rng r is non empty V68() V69() V70() Element of bool REAL
len UV 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 UV) is finite V44( len UV) V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of bool NAT
Seg (len n1) is non empty finite V44( len n1) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
dom n1 is non empty finite V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
m . LV is V11() real ext-real Element of REAL
divset (n1,LV) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
r | (divset (n1,LV)) is V16() V19(f) V19( divset (n1,LV)) V19(f) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
rng (r | (divset (n1,LV))) is V68() V69() V70() Element of bool REAL
lower_bound (rng (r | (divset (n1,LV)))) is V11() real ext-real Element of REAL
vol (divset (n1,LV)) is V11() real ext-real Element of REAL
(lower_bound (rng (r | (divset (n1,LV))))) * (vol (divset (n1,LV))) is V11() real ext-real Element of REAL
UV2 is V11() real ext-real Element of REAL
dom r is non empty V68() V69() V70() Element of bool f
bool f is set
(dom r) /\ (divset (n1,LV)) is V68() V69() V70() Element of bool REAL
dom (r | (divset (n1,LV))) is V68() V69() V70() Element of bool f
(r | (divset (n1,LV))) . UV2 is V11() real ext-real Element of REAL
upper_bound (rng (r | (divset (n1,LV)))) is V11() real ext-real Element of REAL
(upper_bound (rng (r | (divset (n1,LV))))) - (lower_bound (rng (r | (divset (n1,LV))))) is V11() real ext-real Element of REAL
UV2 is V11() real ext-real Element of REAL
D . LV is V11() real ext-real Element of REAL
(upper_bound (rng (r | (divset (n1,LV))))) * (vol (divset (n1,LV))) is V11() real ext-real Element of REAL
((upper_bound (rng (r | (divset (n1,LV))))) * (vol (divset (n1,LV)))) - ((lower_bound (rng (r | (divset (n1,LV))))) * (vol (divset (n1,LV)))) is V11() real ext-real Element of REAL
((upper_bound (rng (r | (divset (n1,LV))))) - (lower_bound (rng (r | (divset (n1,LV)))))) * (vol (divset (n1,LV))) is V11() real ext-real Element of REAL
abs (y . y) is V11() real ext-real Element of REAL
Seg (len n1) is non empty finite V44( len n1) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
A * (n2 - n) is V16() V19( NAT ) V20( REAL ) Function-like finite V44( len n1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len n1) -tuples_on REAL
K463(A) is non empty V16() V19( REAL ) V20( REAL ) Function-like total V30( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
K213(K177(),A,(id REAL)) is set
K463(A) * (n2 - n) is V16() V19( NAT ) V20( REAL ) finite complex-valued ext-real-valued real-valued set
LV is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer finite V42() set
(D - m) . LV is V11() real ext-real Element of REAL
(A * (n2 - n)) . LV is V11() real ext-real Element of REAL
(n2 - n) . LV is V11() real ext-real Element of REAL
A * ((n2 - n) . LV) is V11() real ext-real Element of REAL
dom n1 is non empty finite V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
m . LV is V11() real ext-real Element of REAL
divset (n1,LV) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
r | (divset (n1,LV)) is V16() V19(f) V19( divset (n1,LV)) V19(f) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
rng (r | (divset (n1,LV))) is V68() V69() V70() Element of bool REAL
lower_bound (rng (r | (divset (n1,LV)))) is V11() real ext-real Element of REAL
vol (divset (n1,LV)) is V11() real ext-real Element of REAL
(lower_bound (rng (r | (divset (n1,LV))))) * (vol (divset (n1,LV))) is V11() real ext-real Element of REAL
upper_bound (rng (r | (divset (n1,LV)))) is V11() real ext-real Element of REAL
(upper_bound (rng (r | (divset (n1,LV))))) - (lower_bound (rng (r | (divset (n1,LV))))) is V11() real ext-real Element of REAL
r | (divset (n1,LV)) is V16() V19(f) V19( divset (n1,LV)) V19(f) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
rng (r | (divset (n1,LV))) is V68() V69() V70() Element of bool REAL
upper_bound (rng (r | (divset (n1,LV)))) is V11() real ext-real Element of REAL
lower_bound (rng (r | (divset (n1,LV)))) is V11() real ext-real Element of REAL
(upper_bound (rng (r | (divset (n1,LV))))) - (lower_bound (rng (r | (divset (n1,LV))))) is V11() real ext-real Element of REAL
A * ((upper_bound (rng (r | (divset (n1,LV))))) - (lower_bound (rng (r | (divset (n1,LV)))))) is V11() real ext-real Element of REAL
(r | (divset (n1,LV))) | (divset (n1,LV)) is V16() V19(f) V19( divset (n1,LV)) V19(f) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
dom (r | (divset (n1,LV))) is V68() V69() V70() Element of bool f
bool f is set
dom r is non empty V68() V69() V70() Element of bool f
(dom r) /\ (divset (n1,LV)) is V68() V69() V70() Element of bool REAL
f /\ (divset (n1,LV)) is V68() V69() V70() interval Element of bool REAL
[:(divset (n1,LV)),REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set
bool [:(divset (n1,LV)),REAL:] is non trivial non finite set
dom (r | (divset (n1,LV))) is V68() V69() V70() Element of bool f
dom r is non empty V68() V69() V70() Element of bool f
(dom r) /\ (divset (n1,LV)) is V68() V69() V70() Element of bool REAL
LV1 is V16() V19( divset (n1,LV)) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:(divset (n1,LV)),REAL:]
UV1 is V16() V19( divset (n1,LV)) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:(divset (n1,LV)),REAL:]
H is non empty V16() V19( divset (n1,LV)) V20( REAL ) Function-like total V30( divset (n1,LV), REAL ) complex-valued ext-real-valued real-valued Element of bool [:(divset (n1,LV)),REAL:]
G is non empty V16() V19( divset (n1,LV)) V20( REAL ) Function-like total V30( divset (n1,LV), REAL ) complex-valued ext-real-valued real-valued Element of bool [:(divset (n1,LV)),REAL:]
F is V11() real ext-real Element of REAL
H . F is V11() real ext-real Element of REAL
G . F is V11() real ext-real Element of REAL
j is V11() real ext-real Element of REAL
H . j is V11() real ext-real Element of REAL
(H . F) - (H . j) is V11() real ext-real Element of REAL
abs ((H . F) - (H . j)) is V11() real ext-real Element of REAL
G . j is V11() real ext-real Element of REAL
(G . F) - (G . j) is V11() real ext-real Element of REAL
abs ((G . F) - (G . j)) is V11() real ext-real Element of REAL
A * (abs ((G . F) - (G . j))) is V11() real ext-real Element of REAL
r . j is V11() real ext-real Element of REAL
r . j is V11() real ext-real Element of REAL
r . F is V11() real ext-real Element of REAL
r . F is V11() real ext-real Element of REAL
G | (divset (n1,LV)) is V16() V19( divset (n1,LV)) V19( divset (n1,LV)) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:(divset (n1,LV)),REAL:]
((upper_bound (rng (r | (divset (n1,LV))))) - (lower_bound (rng (r | (divset (n1,LV)))))) * (vol (divset (n1,LV))) is V11() real ext-real Element of REAL
(A * ((upper_bound (rng (r | (divset (n1,LV))))) - (lower_bound (rng (r | (divset (n1,LV))))))) * (vol (divset (n1,LV))) is V11() real ext-real Element of REAL
D . LV is V11() real ext-real Element of REAL
(upper_bound (rng (r | (divset (n1,LV))))) * (vol (divset (n1,LV))) is V11() real ext-real Element of REAL
((upper_bound (rng (r | (divset (n1,LV))))) * (vol (divset (n1,LV)))) - ((lower_bound (rng (r | (divset (n1,LV))))) * (vol (divset (n1,LV)))) is V11() real ext-real Element of REAL
n . LV is V11() real ext-real Element of REAL
(lower_bound (rng (r | (divset (n1,LV))))) * (vol (divset (n1,LV))) is V11() real ext-real Element of REAL
n2 . LV is V11() real ext-real Element of REAL
(upper_bound (rng (r | (divset (n1,LV))))) * (vol (divset (n1,LV))) is V11() real ext-real Element of REAL
((upper_bound (rng (r | (divset (n1,LV))))) * (vol (divset (n1,LV)))) - ((lower_bound (rng (r | (divset (n1,LV))))) * (vol (divset (n1,LV)))) is V11() real ext-real Element of REAL
A * (((upper_bound (rng (r | (divset (n1,LV))))) * (vol (divset (n1,LV)))) - ((lower_bound (rng (r | (divset (n1,LV))))) * (vol (divset (n1,LV))))) is V11() real ext-real Element of REAL
((upper_bound (rng (r | (divset (n1,LV))))) - (lower_bound (rng (r | (divset (n1,LV)))))) * (vol (divset (n1,LV))) is V11() real ext-real Element of REAL
A * (((upper_bound (rng (r | (divset (n1,LV))))) - (lower_bound (rng (r | (divset (n1,LV)))))) * (vol (divset (n1,LV)))) is V11() real ext-real Element of REAL
Sum (A * (n2 - n)) is V11() real ext-real Element of REAL
K271(REAL,(A * (n2 - n)),K175()) is V11() real ext-real Element of REAL
A * (x . y) is V11() real ext-real Element of REAL
0 / A is V11() real ext-real Element of REAL
abs (x . y) is V11() real ext-real Element of REAL
A * (y / A) is V11() real ext-real Element of REAL
lim ((upper_sum (r,x)) - (lower_sum (r,x))) is V11() real ext-real Element of REAL
A is V11() real ext-real Element of REAL
f is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
[:f,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set
bool [:f,REAL:] is non trivial non finite set
r is non empty V16() V19(f) V20( REAL ) Function-like total V30(f, REAL ) complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
r | f is V16() V19(f) V19(f) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
r is non empty V16() V19(f) V20( REAL ) Function-like total V30(f, REAL ) complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
r | f is V16() V19(f) V19(f) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
x is non empty V16() V19(f) V20( REAL ) Function-like total V30(f, REAL ) complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
x | f is V16() V19(f) V19(f) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
divs f is non empty set
[:NAT,(divs f):] is non trivial V16() non finite set
bool [:NAT,(divs f):] is non trivial non finite set
y is non empty V16() V19( NAT ) V20( divs f) Function-like total V30( NAT , divs f) Element of bool [:NAT,(divs f):]
delta y 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 y) is V11() real ext-real Element of REAL
upper_sum (x,y) 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 (x,y)) is V11() real ext-real Element of REAL
lower_sum (x,y) 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 (x,y)) is V11() real ext-real Element of REAL
(lim (upper_sum (x,y))) - (lim (lower_sum (x,y))) is V11() real ext-real Element of REAL
lower_sum (r,y) 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:]
upper_sum (r,y) 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:]
(upper_sum (r,y)) - (lower_sum (r,y)) 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:]
- (lower_sum (r,y)) is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
- 1 is V11() real ext-real non positive integer set
(- 1) (#) (lower_sum (r,y)) is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(upper_sum (r,y)) + (- (lower_sum (r,y))) is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
lim (upper_sum (r,y)) is V11() real ext-real Element of REAL
lim (lower_sum (r,y)) is V11() real ext-real Element of REAL
(lim (upper_sum (r,y))) - (lim (lower_sum (r,y))) is V11() real ext-real Element of REAL
lim ((upper_sum (r,y)) - (lower_sum (r,y))) is V11() real ext-real Element of REAL
lower_sum (r,y) 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:]
(upper_sum (x,y)) - (lower_sum (x,y)) 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:]
- (lower_sum (x,y)) is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) (lower_sum (x,y)) is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(upper_sum (x,y)) + (- (lower_sum (x,y))) is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
upper_sum (r,y) 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:]
(upper_sum (r,y)) - (lower_sum (r,y)) 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:]
- (lower_sum (r,y)) is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) (lower_sum (r,y)) is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(upper_sum (r,y)) + (- (lower_sum (r,y))) is V16() V19( NAT ) Function-like total complex-valued ext-real-valued real-valued set
lim (upper_sum (r,y)) is V11() real ext-real Element of REAL
lim (lower_sum (r,y)) is V11() real ext-real Element of REAL
(lim (upper_sum (r,y))) - (lim (lower_sum (r,y))) is V11() real ext-real Element of REAL
lim ((upper_sum (r,y)) - (lower_sum (r,y))) is V11() real ext-real Element of REAL
x 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:]
y is V11() real ext-real set
y / A is V11() real ext-real Element of REAL
(y / A) / 2 is V11() real ext-real Element of REAL
x 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:]
n1 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
y 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:]
n2 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
max (n1,n2) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer finite V42() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer finite V42() set
m 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
n 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
n 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
m 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 . m is V11() real ext-real Element of REAL
(x . m) - 0 is V11() real ext-real Element of REAL
abs ((x . m) - 0) is V11() real ext-real Element of REAL
y . m 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 f
D 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 f
upper_volume (r,D) 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 (r,D)) 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 D 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 D) -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 D } is set
lower_volume (r,D) 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 (r,D)) 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
x . m is V11() real ext-real Element of REAL
(upper_sum (r,y)) . m is V11() real ext-real Element of REAL
- (lower_sum (r,y)) 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:]
(- (lower_sum (r,y))) . m is V11() real ext-real Element of REAL
((upper_sum (r,y)) . m) + ((- (lower_sum (r,y))) . m) is V11() real ext-real Element of REAL
(lower_sum (r,y)) . m is V11() real ext-real Element of REAL
- ((lower_sum (r,y)) . m) is V11() real ext-real Element of REAL
((upper_sum (r,y)) . m) + (- ((lower_sum (r,y)) . m)) is V11() real ext-real Element of REAL
((upper_sum (r,y)) . m) - ((lower_sum (r,y)) . m) is V11() real ext-real Element of REAL
upper_sum (r,(y . m)) is V11() real ext-real Element of REAL
(upper_sum (r,(y . m))) - ((lower_sum (r,y)) . m) is V11() real ext-real Element of REAL
lower_sum (r,(y . m)) is V11() real ext-real Element of REAL
(upper_sum (r,(y . m))) - (lower_sum (r,(y . m))) is V11() real ext-real Element of REAL
Sum (upper_volume (r,D)) 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 (r,D)),K175()) is V11() real ext-real Element of REAL
(Sum (upper_volume (r,D))) - (lower_sum (r,(y . m))) is V11() real ext-real Element of REAL
Sum (lower_volume (r,D)) is V11() real ext-real Element of REAL
K271(REAL,(lower_volume (r,D)),K175()) is V11() real ext-real Element of REAL
(Sum (upper_volume (r,D))) - (Sum (lower_volume (r,D))) is V11() real ext-real Element of REAL
UV is V16() V19( NAT ) V20( REAL ) Function-like finite V44( len D) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len D) -tuples_on REAL
LV is V16() V19( NAT ) V20( REAL ) Function-like finite V44( len D) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len D) -tuples_on REAL
UV - LV is V16() V19( NAT ) V20( REAL ) Function-like finite V44( len D) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len D) -tuples_on REAL
K176() 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:]
id REAL is non empty V16() V19( REAL ) V20( REAL ) total V30( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
K173() is non empty V16() V19( REAL ) V20( REAL ) Function-like total V30( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
K258(REAL,K175(),(id REAL),K173()) 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:]
K211(K176(),UV,LV) is set
- LV is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K173() * LV is V16() V19( NAT ) V20( REAL ) finite complex-valued ext-real-valued real-valued set
(- 1) (#) LV is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K463((- 1)) is non empty V16() V19( REAL ) V20( REAL ) Function-like total V30( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
K177() 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:]
K213(K177(),(- 1),(id REAL)) is set
K463((- 1)) * LV is V16() V19( NAT ) V20( REAL ) finite complex-valued ext-real-valued real-valued set
UV + (- LV) is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K211(K175(),UV,(- LV)) is set
Sum (UV - LV) is V11() real ext-real Element of REAL
K271(REAL,(UV - LV),K175()) is V11() real ext-real Element of REAL
lower_volume (x,D) 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 (x,D)) 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 (x,D) 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 (x,D)) 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 (r,D) 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 (r,D)) 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 (r,D) 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 (r,D)) 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
UV1 is V16() V19( NAT ) V20( REAL ) Function-like finite V44( len D) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len D) -tuples_on REAL
LV1 is V16() V19( NAT ) V20( REAL ) Function-like finite V44( len D) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len D) -tuples_on REAL
UV1 - LV1 is V16() V19( NAT ) V20( REAL ) Function-like finite V44( len D) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len D) -tuples_on REAL
K211(K176(),UV1,LV1) is set
- LV1 is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K173() * LV1 is V16() V19( NAT ) V20( REAL ) finite complex-valued ext-real-valued real-valued set
(- 1) (#) LV1 is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K463((- 1)) * LV1 is V16() V19( NAT ) V20( REAL ) finite complex-valued ext-real-valued real-valued set
UV1 + (- LV1) is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K211(K175(),UV1,(- LV1)) is set
UV2 is V16() V19( NAT ) V20( REAL ) Function-like finite V44( len D) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len D) -tuples_on REAL
LV2 is V16() V19( NAT ) V20( REAL ) Function-like finite V44( len D) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len D) -tuples_on REAL
UV2 - LV2 is V16() V19( NAT ) V20( REAL ) Function-like finite V44( len D) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len D) -tuples_on REAL
K211(K176(),UV2,LV2) is set
- LV2 is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K173() * LV2 is V16() V19( NAT ) V20( REAL ) finite complex-valued ext-real-valued real-valued set
(- 1) (#) LV2 is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K463((- 1)) * LV2 is V16() V19( NAT ) V20( REAL ) finite complex-valued ext-real-valued real-valued set
UV2 + (- LV2) is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K211(K175(),UV2,(- LV2)) is set
y . m is V11() real ext-real Element of REAL
(upper_sum (r,y)) . m is V11() real ext-real Element of REAL
- (lower_sum (r,y)) 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:]
(- (lower_sum (r,y))) . m is V11() real ext-real Element of REAL
((upper_sum (r,y)) . m) + ((- (lower_sum (r,y))) . m) is V11() real ext-real Element of REAL
(lower_sum (r,y)) . m is V11() real ext-real Element of REAL
- ((lower_sum (r,y)) . m) is V11() real ext-real Element of REAL
((upper_sum (r,y)) . m) + (- ((lower_sum (r,y)) . m)) is V11() real ext-real Element of REAL
((upper_sum (r,y)) . m) - ((lower_sum (r,y)) . m) is V11() real ext-real Element of REAL
upper_sum (r,(y . m)) is V11() real ext-real Element of REAL
(upper_sum (r,(y . m))) - ((lower_sum (r,y)) . m) is V11() real ext-real Element of REAL
lower_sum (r,(y . m)) is V11() real ext-real Element of REAL
(upper_sum (r,(y . m))) - (lower_sum (r,(y . m))) is V11() real ext-real Element of REAL
Sum (upper_volume (r,D)) is V11() real ext-real Element of REAL
K271(REAL,(upper_volume (r,D)),K175()) is V11() real ext-real Element of REAL
(Sum (upper_volume (r,D))) - (lower_sum (r,(y . m))) is V11() real ext-real Element of REAL
Sum (lower_volume (r,D)) is V11() real ext-real Element of REAL
K271(REAL,(lower_volume (r,D)),K175()) is V11() real ext-real Element of REAL
(Sum (upper_volume (r,D))) - (Sum (lower_volume (r,D))) is V11() real ext-real Element of REAL
Sum (UV1 - LV1) is V11() real ext-real Element of REAL
K271(REAL,(UV1 - LV1),K175()) is V11() real ext-real Element of REAL
G is V16() V19( NAT ) V20( REAL ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
dom G is finite V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of bool NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer finite V42() set
G . j is V11() real ext-real Element of REAL
rng r is non empty V68() V69() V70() Element of bool REAL
len G 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 G) is finite V44( len G) V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of bool NAT
Seg (len D) is non empty finite V44( len D) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
dom D is non empty finite V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
LV1 . j is V11() real ext-real Element of REAL
divset (D,j) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
r | (divset (D,j)) is V16() V19(f) V19( divset (D,j)) V19(f) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
rng (r | (divset (D,j))) is V68() V69() V70() Element of bool REAL
lower_bound (rng (r | (divset (D,j)))) is V11() real ext-real Element of REAL
vol (divset (D,j)) is V11() real ext-real Element of REAL
(lower_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j))) is V11() real ext-real Element of REAL
y is V11() real ext-real Element of REAL
dom r is non empty V68() V69() V70() Element of bool f
bool f is set
(dom r) /\ (divset (D,j)) is V68() V69() V70() Element of bool REAL
dom (r | (divset (D,j))) is V68() V69() V70() Element of bool f
(r | (divset (D,j))) . y is V11() real ext-real Element of REAL
upper_bound (rng (r | (divset (D,j)))) is V11() real ext-real Element of REAL
(upper_bound (rng (r | (divset (D,j))))) - (lower_bound (rng (r | (divset (D,j))))) is V11() real ext-real Element of REAL
y is V11() real ext-real Element of REAL
UV1 . j is V11() real ext-real Element of REAL
(upper_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j))) is V11() real ext-real Element of REAL
((upper_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j)))) is V11() real ext-real Element of REAL
((upper_bound (rng (r | (divset (D,j))))) - (lower_bound (rng (r | (divset (D,j)))))) * (vol (divset (D,j))) is V11() real ext-real Element of REAL
(x . m) - 0 is V11() real ext-real Element of REAL
abs ((x . m) - 0) is V11() real ext-real Element of REAL
(y . m) - 0 is V11() real ext-real Element of REAL
abs ((y . m) - 0) is V11() real ext-real Element of REAL
H is V16() V19( NAT ) V20( REAL ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
dom H is finite V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of bool NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer finite V42() set
H . j is V11() real ext-real Element of REAL
rng r is non empty V68() V69() V70() Element of bool REAL
len H 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 H) is finite V44( len H) V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of bool NAT
Seg (len D) is non empty finite V44( len D) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
dom D is non empty finite V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
LV . j is V11() real ext-real Element of REAL
divset (D,j) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
r | (divset (D,j)) is V16() V19(f) V19( divset (D,j)) V19(f) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
rng (r | (divset (D,j))) is V68() V69() V70() Element of bool REAL
lower_bound (rng (r | (divset (D,j)))) is V11() real ext-real Element of REAL
vol (divset (D,j)) is V11() real ext-real Element of REAL
(lower_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j))) is V11() real ext-real Element of REAL
y is V11() real ext-real Element of REAL
dom r is non empty V68() V69() V70() Element of bool f
bool f is set
(dom r) /\ (divset (D,j)) is V68() V69() V70() Element of bool REAL
dom (r | (divset (D,j))) is V68() V69() V70() Element of bool f
(r | (divset (D,j))) . y is V11() real ext-real Element of REAL
upper_bound (rng (r | (divset (D,j)))) is V11() real ext-real Element of REAL
(upper_bound (rng (r | (divset (D,j))))) - (lower_bound (rng (r | (divset (D,j))))) is V11() real ext-real Element of REAL
y is V11() real ext-real Element of REAL
UV . j is V11() real ext-real Element of REAL
(upper_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j))) is V11() real ext-real Element of REAL
((upper_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j)))) is V11() real ext-real Element of REAL
((upper_bound (rng (r | (divset (D,j))))) - (lower_bound (rng (r | (divset (D,j)))))) * (vol (divset (D,j))) is V11() real ext-real Element of REAL
(x . m) * (y . m) is V11() real ext-real Element of REAL
abs (x . m) is V11() real ext-real Element of REAL
abs (y . m) is V11() real ext-real Element of REAL
(abs (x . m)) + (abs (y . m)) is V11() real ext-real Element of REAL
(x . m) + (y . m) is V11() real ext-real Element of REAL
abs ((x . m) + (y . m)) is V11() real ext-real Element of REAL
(abs ((x . m) - 0)) + (abs (y . m)) is V11() real ext-real Element of REAL
((y / A) / 2) + ((y / A) / 2) is V11() real ext-real Element of REAL
A * (y / A) is V11() real ext-real Element of REAL
A * ((x . m) + (y . m)) is V11() real ext-real Element of REAL
(upper_sum (x,y)) . m is V11() real ext-real Element of REAL
- (lower_sum (x,y)) 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:]
(- (lower_sum (x,y))) . m is V11() real ext-real Element of REAL
((upper_sum (x,y)) . m) + ((- (lower_sum (x,y))) . m) is V11() real ext-real Element of REAL
(lower_sum (x,y)) . m is V11() real ext-real Element of REAL
- ((lower_sum (x,y)) . m) is V11() real ext-real Element of REAL
((upper_sum (x,y)) . m) + (- ((lower_sum (x,y)) . m)) is V11() real ext-real Element of REAL
((upper_sum (x,y)) . m) - ((lower_sum (x,y)) . m) is V11() real ext-real Element of REAL
upper_sum (x,(y . m)) is V11() real ext-real Element of REAL
(upper_sum (x,(y . m))) - ((lower_sum (x,y)) . m) is V11() real ext-real Element of REAL
lower_sum (x,(y . m)) is V11() real ext-real Element of REAL
(upper_sum (x,(y . m))) - (lower_sum (x,(y . m))) is V11() real ext-real Element of REAL
Sum (upper_volume (x,D)) is V11() real ext-real Element of REAL
K271(REAL,(upper_volume (x,D)),K175()) is V11() real ext-real Element of REAL
(Sum (upper_volume (x,D))) - (lower_sum (x,(y . m))) is V11() real ext-real Element of REAL
Sum (lower_volume (x,D)) is V11() real ext-real Element of REAL
K271(REAL,(lower_volume (x,D)),K175()) is V11() real ext-real Element of REAL
(Sum (upper_volume (x,D))) - (Sum (lower_volume (x,D))) is V11() real ext-real Element of REAL
Sum (UV2 - LV2) is V11() real ext-real Element of REAL
K271(REAL,(UV2 - LV2),K175()) is V11() real ext-real Element of REAL
F is V16() V19( NAT ) V20( REAL ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
dom F is finite V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of bool NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer finite V42() set
F . j is V11() real ext-real Element of REAL
rng x is non empty V68() V69() V70() Element of bool REAL
len 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
Seg (len F) is finite V44( len F) V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of bool NAT
Seg (len D) is non empty finite V44( len D) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
dom D is non empty finite V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
LV2 . j is V11() real ext-real Element of REAL
divset (D,j) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
x | (divset (D,j)) is V16() V19(f) V19( divset (D,j)) V19(f) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
rng (x | (divset (D,j))) is V68() V69() V70() Element of bool REAL
lower_bound (rng (x | (divset (D,j)))) is V11() real ext-real Element of REAL
vol (divset (D,j)) is V11() real ext-real Element of REAL
(lower_bound (rng (x | (divset (D,j))))) * (vol (divset (D,j))) is V11() real ext-real Element of REAL
y is V11() real ext-real Element of REAL
dom x is non empty V68() V69() V70() Element of bool f
bool f is set
(dom x) /\ (divset (D,j)) is V68() V69() V70() Element of bool REAL
dom (x | (divset (D,j))) is V68() V69() V70() Element of bool f
(x | (divset (D,j))) . y is V11() real ext-real Element of REAL
upper_bound (rng (x | (divset (D,j)))) is V11() real ext-real Element of REAL
(upper_bound (rng (x | (divset (D,j))))) - (lower_bound (rng (x | (divset (D,j))))) is V11() real ext-real Element of REAL
y is V11() real ext-real Element of REAL
UV2 . j is V11() real ext-real Element of REAL
(upper_bound (rng (x | (divset (D,j))))) * (vol (divset (D,j))) is V11() real ext-real Element of REAL
((upper_bound (rng (x | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (x | (divset (D,j))))) * (vol (divset (D,j)))) is V11() real ext-real Element of REAL
((upper_bound (rng (x | (divset (D,j))))) - (lower_bound (rng (x | (divset (D,j)))))) * (vol (divset (D,j))) is V11() real ext-real Element of REAL
abs (x . m) is V11() real ext-real Element of REAL
Seg (len D) is non empty finite V44( len D) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
(UV - LV) + (UV1 - LV1) is V16() V19( NAT ) V20( REAL ) Function-like finite V44( len D) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len D) -tuples_on REAL
K211(K175(),(UV - LV),(UV1 - LV1)) is set
A * ((UV - LV) + (UV1 - LV1)) is V16() V19( NAT ) V20( REAL ) Function-like finite V44( len D) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len D) -tuples_on REAL
K463(A) is non empty V16() V19( REAL ) V20( REAL ) Function-like total V30( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
K213(K177(),A,(id REAL)) is set
K463(A) * ((UV - LV) + (UV1 - LV1)) is V16() V19( NAT ) V20( REAL ) finite complex-valued ext-real-valued real-valued set
j is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer finite V42() set
(UV2 - LV2) . j is V11() real ext-real Element of REAL
(A * ((UV - LV) + (UV1 - LV1))) . j is V11() real ext-real Element of REAL
((UV - LV) + (UV1 - LV1)) . j is V11() real ext-real Element of REAL
A * (((UV - LV) + (UV1 - LV1)) . j) is V11() real ext-real Element of REAL
(UV - LV) . j is V11() real ext-real Element of REAL
(UV1 - LV1) . j is V11() real ext-real Element of REAL
((UV - LV) . j) + ((UV1 - LV1) . j) is V11() real ext-real Element of REAL
A * (((UV - LV) . j) + ((UV1 - LV1) . j)) is V11() real ext-real Element of REAL
UV . j is V11() real ext-real Element of REAL
LV . j is V11() real ext-real Element of REAL
(UV . j) - (LV . j) is V11() real ext-real Element of REAL
((UV . j) - (LV . j)) + ((UV1 - LV1) . j) is V11() real ext-real Element of REAL
A * (((UV . j) - (LV . j)) + ((UV1 - LV1) . j)) is V11() real ext-real Element of REAL
UV1 . j is V11() real ext-real Element of REAL
LV1 . j is V11() real ext-real Element of REAL
(UV1 . j) - (LV1 . j) is V11() real ext-real Element of REAL
((UV . j) - (LV . j)) + ((UV1 . j) - (LV1 . j)) is V11() real ext-real Element of REAL
A * (((UV . j) - (LV . j)) + ((UV1 . j) - (LV1 . j))) is V11() real ext-real Element of REAL
divset (D,j) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
vol (divset (D,j)) is V11() real ext-real Element of REAL
dom D is non empty finite V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
LV2 . j is V11() real ext-real Element of REAL
x | (divset (D,j)) is V16() V19(f) V19( divset (D,j)) V19(f) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
rng (x | (divset (D,j))) is V68() V69() V70() Element of bool REAL
lower_bound (rng (x | (divset (D,j)))) is V11() real ext-real Element of REAL
(lower_bound (rng (x | (divset (D,j))))) * (vol (divset (D,j))) is V11() real ext-real Element of REAL
UV2 . j is V11() real ext-real Element of REAL
upper_bound (rng (x | (divset (D,j)))) is V11() real ext-real Element of REAL
(upper_bound (rng (x | (divset (D,j))))) * (vol (divset (D,j))) is V11() real ext-real Element of REAL
((upper_bound (rng (x | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (x | (divset (D,j))))) * (vol (divset (D,j)))) is V11() real ext-real Element of REAL
(upper_bound (rng (x | (divset (D,j))))) - (lower_bound (rng (x | (divset (D,j))))) is V11() real ext-real Element of REAL
((upper_bound (rng (x | (divset (D,j))))) - (lower_bound (rng (x | (divset (D,j)))))) * (vol (divset (D,j))) is V11() real ext-real Element of REAL
r | (divset (D,j)) is V16() V19(f) V19( divset (D,j)) V19(f) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
rng (r | (divset (D,j))) is V68() V69() V70() Element of bool REAL
lower_bound (rng (r | (divset (D,j)))) is V11() real ext-real Element of REAL
(lower_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j))) is V11() real ext-real Element of REAL
upper_bound (rng (r | (divset (D,j)))) is V11() real ext-real Element of REAL
(upper_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j))) is V11() real ext-real Element of REAL
r | (divset (D,j)) is V16() V19(f) V19( divset (D,j)) V19(f) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
rng (r | (divset (D,j))) is V68() V69() V70() Element of bool REAL
upper_bound (rng (r | (divset (D,j)))) is V11() real ext-real Element of REAL
lower_bound (rng (r | (divset (D,j)))) is V11() real ext-real Element of REAL
(upper_bound (rng (r | (divset (D,j))))) - (lower_bound (rng (r | (divset (D,j))))) is V11() real ext-real Element of REAL
(upper_bound (rng (r | (divset (D,j))))) - (lower_bound (rng (r | (divset (D,j))))) is V11() real ext-real Element of REAL
((upper_bound (rng (r | (divset (D,j))))) - (lower_bound (rng (r | (divset (D,j)))))) + ((upper_bound (rng (r | (divset (D,j))))) - (lower_bound (rng (r | (divset (D,j)))))) is V11() real ext-real Element of REAL
A * (((upper_bound (rng (r | (divset (D,j))))) - (lower_bound (rng (r | (divset (D,j)))))) + ((upper_bound (rng (r | (divset (D,j))))) - (lower_bound (rng (r | (divset (D,j))))))) is V11() real ext-real Element of REAL
dom (r | (divset (D,j))) is V68() V69() V70() Element of bool f
bool f is set
dom r is non empty V68() V69() V70() Element of bool f
(dom r) /\ (divset (D,j)) is V68() V69() V70() Element of bool REAL
f /\ (divset (D,j)) is V68() V69() V70() interval Element of bool REAL
[:(divset (D,j)),REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set
bool [:(divset (D,j)),REAL:] is non trivial non finite set
g1 is V16() V19( divset (D,j)) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:(divset (D,j)),REAL:]
(r | (divset (D,j))) | (divset (D,j)) is V16() V19(f) V19( divset (D,j)) V19(f) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
dom (x | (divset (D,j))) is V68() V69() V70() Element of bool f
dom x is non empty V68() V69() V70() Element of bool f
(dom x) /\ (divset (D,j)) is V68() V69() V70() Element of bool REAL
h1 is V16() V19( divset (D,j)) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:(divset (D,j)),REAL:]
dom (r | (divset (D,j))) is V68() V69() V70() Element of bool f
dom r is non empty V68() V69() V70() Element of bool f
(dom r) /\ (divset (D,j)) is V68() V69() V70() Element of bool REAL
(r | (divset (D,j))) | (divset (D,j)) is V16() V19(f) V19( divset (D,j)) V19(f) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
h1 is non empty V16() V19( divset (D,j)) V20( REAL ) Function-like total V30( divset (D,j), REAL ) complex-valued ext-real-valued real-valued Element of bool [:(divset (D,j)),REAL:]
f1 is V16() V19( divset (D,j)) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:(divset (D,j)),REAL:]
g1 is non empty V16() V19( divset (D,j)) V20( REAL ) Function-like total V30( divset (D,j), REAL ) complex-valued ext-real-valued real-valued Element of bool [:(divset (D,j)),REAL:]
x is V11() real ext-real Element of REAL
h1 . x is V11() real ext-real Element of REAL
f1 . x is V11() real ext-real Element of REAL
g1 . x is V11() real ext-real Element of REAL
y is V11() real ext-real Element of REAL
h1 . y is V11() real ext-real Element of REAL
(h1 . x) - (h1 . y) is V11() real ext-real Element of REAL
abs ((h1 . x) - (h1 . y)) is V11() real ext-real Element of REAL
f1 . y is V11() real ext-real Element of REAL
(f1 . x) - (f1 . y) is V11() real ext-real Element of REAL
abs ((f1 . x) - (f1 . y)) is V11() real ext-real Element of REAL
g1 . y is V11() real ext-real Element of REAL
(g1 . x) - (g1 . y) is V11() real ext-real Element of REAL
abs ((g1 . x) - (g1 . y)) is V11() real ext-real Element of REAL
(abs ((f1 . x) - (f1 . y))) + (abs ((g1 . x) - (g1 . y))) is V11() real ext-real Element of REAL
A * ((abs ((f1 . x) - (f1 . y))) + (abs ((g1 . x) - (g1 . y)))) is V11() real ext-real Element of REAL
r . y is V11() real ext-real Element of REAL
x . y is V11() real ext-real Element of REAL
x . x is V11() real ext-real Element of REAL
r . y is V11() real ext-real Element of REAL
r . x is V11() real ext-real Element of REAL
r . x is V11() real ext-real Element of REAL
g1 | (divset (D,j)) is V16() V19( divset (D,j)) V19( divset (D,j)) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:(divset (D,j)),REAL:]
f1 | (divset (D,j)) is V16() V19( divset (D,j)) V19( divset (D,j)) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:(divset (D,j)),REAL:]
(lower_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j))) is V11() real ext-real Element of REAL
(upper_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j))) is V11() real ext-real Element of REAL
((upper_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j)))) is V11() real ext-real Element of REAL
((upper_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j)))) is V11() real ext-real Element of REAL
(((upper_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j))))) + (((upper_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j))))) is V11() real ext-real Element of REAL
A * ((((upper_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j))))) + (((upper_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (r | (divset (D,j))))) * (vol (divset (D,j)))))) is V11() real ext-real Element of REAL
(A * (((upper_bound (rng (r | (divset (D,j))))) - (lower_bound (rng (r | (divset (D,j)))))) + ((upper_bound (rng (r | (divset (D,j))))) - (lower_bound (rng (r | (divset (D,j)))))))) * (vol (divset (D,j))) is V11() real ext-real Element of REAL
Sum (A * ((UV - LV) + (UV1 - LV1))) is V11() real ext-real Element of REAL
K271(REAL,(A * ((UV - LV) + (UV1 - LV1))),K175()) is V11() real ext-real Element of REAL
Sum ((UV - LV) + (UV1 - LV1)) is V11() real ext-real Element of REAL
K271(REAL,((UV - LV) + (UV1 - LV1)),K175()) is V11() real ext-real Element of REAL
A * (Sum ((UV - LV) + (UV1 - LV1))) is V11() real ext-real Element of REAL
lim ((upper_sum (x,y)) - (lower_sum (x,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
[: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:]
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:]
r | A is V16() V19(A) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
f (#) 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:]
A /\ A is V68() V69() V70() interval Element of bool REAL
(f (#) r) | (A /\ A) is V16() V19(A) V19(A /\ A) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
dom r is non empty V68() V69() V70() Element of bool A
bool A is set
A /\ (dom r) is V68() V69() V70() Element of bool A
r is V11() real ext-real set
dom f is non empty V68() V69() V70() Element of bool A
A /\ (dom f) is V68() V69() V70() Element of bool A
x is V11() real ext-real Element of REAL
y is V11() real ext-real Element of A
f . y is V11() real ext-real Element of REAL
abs (f . y) is V11() real ext-real Element of REAL
x is V11() real ext-real set
max (x,r) is V11() real ext-real set
y is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
(f (#) r) . 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
y is V11() real ext-real Element of REAL
(f (#) r) . y is V11() real ext-real Element of REAL
((f (#) r) . x) - ((f (#) r) . y) is V11() real ext-real Element of REAL
abs (((f (#) r) . x) - ((f (#) r) . y)) is V11() real ext-real Element of REAL
r . y is V11() real ext-real Element of REAL
(r . x) - (r . y) is V11() real ext-real Element of REAL
abs ((r . x) - (r . y)) is V11() real ext-real Element of REAL
f . y is V11() real ext-real Element of REAL
(f . x) - (f . y) is V11() real ext-real Element of REAL
abs ((f . x) - (f . y)) is V11() real ext-real Element of REAL
(abs ((r . x) - (r . y))) + (abs ((f . x) - (f . y))) is V11() real ext-real Element of REAL
y * ((abs ((r . x) - (r . y))) + (abs ((f . x) - (f . y)))) is V11() real ext-real Element of REAL
(f . y) * (r . y) is V11() real ext-real Element of REAL
abs (r . y) is V11() real ext-real Element of REAL
((f . x) - (f . y)) * (r . y) is V11() real ext-real Element of REAL
abs (((f . x) - (f . y)) * (r . y)) is V11() real ext-real Element of REAL
(abs ((f . x) - (f . y))) * (abs (r . y)) is V11() real ext-real Element of REAL
y * (abs ((f . x) - (f . y))) is V11() real ext-real Element of REAL
(f . x) * (r . x) is V11() real ext-real Element of REAL
(f . x) * ((r . x) - (r . y)) is V11() real ext-real Element of REAL
((f . x) * ((r . x) - (r . y))) + (((f . x) - (f . y)) * (r . y)) is V11() real ext-real Element of REAL
abs (((f . x) * ((r . x) - (r . y))) + (((f . x) - (f . y)) * (r . y))) is V11() real ext-real Element of REAL
abs ((f . x) * ((r . x) - (r . y))) is V11() real ext-real Element of REAL
(abs ((f . x) * ((r . x) - (r . y)))) + (abs (((f . x) - (f . y)) * (r . y))) is V11() real ext-real Element of REAL
abs (f . x) is V11() real ext-real Element of REAL
(abs (f . x)) * (abs ((r . x) - (r . y))) is V11() real ext-real Element of REAL
y * (abs ((r . x) - (r . y))) is V11() real ext-real Element of REAL
(y * (abs ((r . x) - (r . y)))) + (y * (abs ((f . x) - (f . y)))) is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
(f (#) r) . x is V11() real ext-real Element of REAL
f . x is V11() real ext-real Element of REAL
y is V11() real ext-real Element of REAL
(f (#) r) . y is V11() real ext-real Element of REAL
((f (#) r) . x) - ((f (#) r) . y) is V11() real ext-real Element of REAL
abs (((f (#) r) . x) - ((f (#) r) . y)) is V11() real ext-real Element of REAL
f . y is V11() real ext-real Element of REAL
(f . x) - (f . y) is V11() real ext-real Element of REAL
abs ((f . x) - (f . y)) is V11() real ext-real Element of REAL
1 * (abs ((f . x) - (f . y))) is V11() real ext-real Element of REAL
r . x is V11() real ext-real Element of REAL
r . y is V11() real ext-real Element of REAL
(r . x) - (r . y) is V11() real ext-real Element of REAL
abs ((r . x) - (r . y)) is V11() real ext-real Element of REAL
(abs ((r . x) - (r . y))) + (abs ((f . x) - (f . y))) is V11() real ext-real Element of REAL
y * ((abs ((r . x) - (r . y))) + (abs ((f . x) - (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
[: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
f ^ is V16() V19(A) V20( REAL ) Function-like 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:]
dom (f ^) is V68() V69() V70() Element of bool A
bool A is set
A /\ (dom (f ^)) is V68() V69() V70() Element of bool A
r is V11() real ext-real set
{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 Element of bool REAL
f " {0} is V68() V69() V70() Element of bool A
r is V11() real ext-real Element of REAL
r ^2 is V11() real ext-real Element of REAL
r * r is V11() real ext-real set
x is V11() real ext-real Element of REAL
(f ^) . x is V11() real ext-real Element of REAL
f . x is V11() real ext-real Element of REAL
y is V11() real ext-real Element of REAL
(f ^) . y is V11() real ext-real Element of REAL
((f ^) . x) - ((f ^) . y) is V11() real ext-real Element of REAL
abs (((f ^) . x) - ((f ^) . y)) is V11() real ext-real Element of REAL
f . y is V11() real ext-real Element of REAL
(f . x) - (f . y) is V11() real ext-real Element of REAL
abs ((f . x) - (f . y)) is V11() real ext-real Element of REAL
(r ^2) * (abs ((f . x) - (f . y))) is V11() real ext-real Element of REAL
abs (f . x) is V11() real ext-real Element of REAL
1 / (abs (f . x)) is V11() real ext-real Element of REAL
abs (f . y) is V11() real ext-real Element of REAL
1 / (abs (f . y)) is V11() real ext-real Element of REAL
y is V11() real ext-real Element of A
(f ^) . y is V11() real ext-real Element of REAL
abs ((f ^) . y) is V11() real ext-real Element of REAL
f . y is V11() real ext-real Element of REAL
(f . y) " is V11() real ext-real Element of REAL
1 * ((f . y) ") is V11() real ext-real Element of REAL
abs (1 * ((f . y) ")) is V11() real ext-real Element of REAL
1 / (f . y) is V11() real ext-real Element of REAL
abs (1 / (f . y)) is V11() real ext-real Element of REAL
x is V11() real ext-real Element of A
(f ^) . x is V11() real ext-real Element of REAL
abs ((f ^) . x) is V11() real ext-real Element of REAL
f . x is V11() real ext-real Element of REAL
(f . x) " is V11() real ext-real Element of REAL
1 * ((f . x) ") is V11() real ext-real Element of REAL
abs (1 * ((f . x) ")) is V11() real ext-real Element of REAL
1 / (f . x) is V11() real ext-real Element of REAL
abs (1 / (f . x)) is V11() real ext-real Element of REAL
(1 / (abs (f . x))) * (1 / (abs (f . y))) is V11() real ext-real Element of REAL
r * r is V11() real ext-real Element of REAL
(abs ((f . x) - (f . y))) * ((1 / (abs (f . x))) * (1 / (abs (f . y)))) is V11() real ext-real Element of REAL
(abs ((f . x) - (f . y))) * (r ^2) is V11() real ext-real Element of REAL
(f . x) " is V11() real ext-real Element of REAL
((f . x) ") - ((f ^) . y) is V11() real ext-real Element of REAL
(f . y) " is V11() real ext-real Element of REAL
((f . x) ") - ((f . y) ") is V11() real ext-real Element of REAL
(abs (f . x)) * (abs (f . y)) is V11() real ext-real Element of REAL
(abs ((f . x) - (f . y))) / ((abs (f . x)) * (abs (f . y))) is V11() real ext-real Element of REAL
(abs ((f . x) - (f . y))) / (abs (f . x)) is V11() real ext-real Element of REAL
((abs ((f . x) - (f . y))) / (abs (f . x))) * (1 / (abs (f . y))) is V11() real ext-real Element of REAL
(abs ((f . x) - (f . y))) * (1 / (abs (f . x))) is V11() real ext-real Element of REAL
((abs ((f . x) - (f . y))) * (1 / (abs (f . x)))) * (1 / (abs (f . y))) 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
f . x is V11() real ext-real Element of REAL
y is V11() real ext-real Element of REAL
(f ^) . y is V11() real ext-real Element of REAL
((f ^) . x) - ((f ^) . y) is V11() real ext-real Element of REAL
abs (((f ^) . x) - ((f ^) . y)) is V11() real ext-real Element of REAL
f . y is V11() real ext-real Element of REAL
(f . x) - (f . y) is V11() real ext-real Element of REAL
abs ((f . x) - (f . y)) is V11() real ext-real Element of REAL
1 * (abs ((f . x) - (f . y))) is V11() real ext-real Element of REAL
0 * (abs ((f . x) - (f . y))) is V11() real ext-real Element of REAL