:: INTEGR15 semantic presentation

REAL is non empty V32() V129() V130() V131() V135() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V32() V37() V38() V129() V130() V131() V132() V133() V134() V135() Element of K6(REAL)
K6(REAL) is V32() set
omega is non empty epsilon-transitive epsilon-connected ordinal V32() V37() V38() V129() V130() V131() V132() V133() V134() V135() set
K6(omega) is V32() set
K6(NAT) is V32() set
COMPLEX is non empty V32() V129() V135() set
RAT is non empty V32() V129() V130() V131() V132() V135() set
INT is non empty V32() V129() V130() V131() V132() V133() V135() set
K7(REAL,REAL) is V32() V119() V120() V121() set
K6(K7(REAL,REAL)) is V32() set
K316() is non empty V75() L8()
the carrier of K316() is set
K321() is non empty L8()
K322() is non empty V75() M13(K321())
K323() is non empty V75() V97() V157() M16(K321(),K322())
K325() is non empty V75() V97() V99() V101() L8()
K326() is non empty V75() V97() V157() M13(K325())
K7(COMPLEX,COMPLEX) is V32() V119() set
K6(K7(COMPLEX,COMPLEX)) is V32() set
K7(COMPLEX,REAL) is V32() V119() V120() V121() set
K6(K7(COMPLEX,REAL)) is V32() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
K7(1,1) is V17( RAT ) V17( INT ) V119() V120() V121() V122() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is V17( RAT ) V17( INT ) V119() V120() V121() V122() set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is V119() V120() V121() set
K6(K7(K7(1,1),REAL)) is set
K7(K7(REAL,REAL),REAL) is V32() V119() V120() V121() set
K6(K7(K7(REAL,REAL),REAL)) is V32() set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
K7(2,2) is V17( RAT ) V17( INT ) V119() V120() V121() V122() set
K7(K7(2,2),REAL) is V119() V120() V121() set
K6(K7(K7(2,2),REAL)) is set
K424(2) is non empty V73() V142() TopSpace-like V194() V195() V196() V197() V198() V199() V200() V206() L16()
the carrier of K424(2) is set
K7( the carrier of K424(2),REAL) is V119() V120() V121() set
K6(K7( the carrier of K424(2),REAL)) is set
K6( the carrier of K424(2)) is set
K7(NAT,REAL) is V32() V119() V120() V121() set
K6(K7(NAT,REAL)) is V32() set
REAL 1 is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7((REAL 1),(REAL 1)) is set
K6(K7((REAL 1),(REAL 1))) is set
REAL-NS 1 is non empty V52() V73() V194() V195() V196() V197() V198() V199() V200() V216() V217() strict V219() V225() L19()
the carrier of (REAL-NS 1) is set
K522((REAL-NS 1),(REAL-NS 1)) is non empty L19()
the carrier of K522((REAL-NS 1),(REAL-NS 1)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V32() V119() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is V32() set
K7(RAT,RAT) is V17( RAT ) V32() V119() V120() V121() set
K6(K7(RAT,RAT)) is V32() set
K7(K7(RAT,RAT),RAT) is V17( RAT ) V32() V119() V120() V121() set
K6(K7(K7(RAT,RAT),RAT)) is V32() set
K7(INT,INT) is V17( RAT ) V17( INT ) V32() V119() V120() V121() set
K6(K7(INT,INT)) is V32() set
K7(K7(INT,INT),INT) is V17( RAT ) V17( INT ) V32() V119() V120() V121() set
K6(K7(K7(INT,INT),INT)) is V32() set
K7(NAT,NAT) is V17( RAT ) V17( INT ) V32() V119() V120() V121() V122() set
K7(K7(NAT,NAT),NAT) is V17( RAT ) V17( INT ) V32() V119() V120() V121() V122() set
K6(K7(K7(NAT,NAT),NAT)) is V32() set
ExtREAL is non empty V130() set
{} is set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real functional V32() V37() V39( {} ) FinSequence-membered ext-real non positive non negative V129() V130() V131() V132() V133() V134() V135() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real functional V32() V37() V39( {} ) FinSequence-membered ext-real non positive non negative V129() V130() V131() V132() V133() V134() V135() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered set
0 is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
K38(1) is V11() real ext-real non positive set
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
x is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
len x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
dom x is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Seg (len x) is non empty V32() V39( len x) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
f is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
divset (x,f) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
Z | (divset (x,f)) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
rng (Z | (divset (x,f))) is V129() V130() V131() Element of K6(REAL)
vol (divset (x,f)) is V11() real ext-real Element of REAL
upper_bound (divset (x,f)) is V11() real ext-real Element of REAL
lower_bound (divset (x,f)) is V11() real ext-real Element of REAL
(upper_bound (divset (x,f))) - (lower_bound (divset (x,f))) is V11() real ext-real Element of REAL
dom Z is V129() V130() V131() Element of K6(n)
K6(n) is set
dom (Z | (divset (x,f))) is V129() V130() V131() Element of K6(n)
r is set
i is V11() real ext-real Element of REAL
i * (vol (divset (x,f))) is V11() real ext-real Element of REAL
f is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
dom f is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
len f is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
dom x is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
lower_volume (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
f is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x)
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
(lower_volume (Z,x)) . r is V11() real ext-real Element of REAL
f . r is V11() real ext-real Element of REAL
divset (x,r) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
Z | (divset (x,r)) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
rng (Z | (divset (x,r))) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (Z | (divset (x,r)))) is V11() real ext-real Element of REAL
vol (divset (x,r)) is V11() real ext-real Element of REAL
upper_bound (divset (x,r)) is V11() real ext-real Element of REAL
lower_bound (divset (x,r)) is V11() real ext-real Element of REAL
(upper_bound (divset (x,r))) - (lower_bound (divset (x,r))) is V11() real ext-real Element of REAL
(lower_bound (rng (Z | (divset (x,r))))) * (vol (divset (x,r))) is V11() real ext-real Element of REAL
i is V11() real ext-real Element of REAL
i * (vol (divset (x,r))) is V11() real ext-real Element of REAL
rng Z is V129() V130() V131() Element of K6(REAL)
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
dom x is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
lower_volume (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
f is V11() real ext-real Element of REAL
len x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
Seg (len x) is non empty V32() V39( len x) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
divset (x,r) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
Z | (divset (x,r)) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
rng (Z | (divset (x,r))) is V129() V130() V131() Element of K6(REAL)
vol (divset (x,r)) is V11() real ext-real Element of REAL
upper_bound (divset (x,r)) is V11() real ext-real Element of REAL
lower_bound (divset (x,r)) is V11() real ext-real Element of REAL
(upper_bound (divset (x,r))) - (lower_bound (divset (x,r))) is V11() real ext-real Element of REAL
(lower_volume (Z,x)) . r is V11() real ext-real Element of REAL
((lower_volume (Z,x)) . r) + f is V11() real ext-real Element of REAL
dom Z is V129() V130() V131() Element of K6(n)
K6(n) is set
dom (Z | (divset (x,r))) is V129() V130() V131() Element of K6(n)
rng Z is V129() V130() V131() Element of K6(REAL)
i is set
k is V11() real ext-real Element of REAL
k * (vol (divset (x,r))) is V11() real ext-real Element of REAL
lower_bound (rng (Z | (divset (x,r)))) is V11() real ext-real Element of REAL
(lower_bound (rng (Z | (divset (x,r))))) * (vol (divset (x,r))) is V11() real ext-real Element of REAL
rfz is V11() real ext-real Element of REAL
lower_bound (rng (Z | (divset (x,r)))) is V11() real ext-real Element of REAL
f / (vol (divset (x,r))) is V11() real ext-real Element of REAL
(lower_bound (rng (Z | (divset (x,r))))) + (f / (vol (divset (x,r)))) is V11() real ext-real Element of REAL
rfz is V11() real ext-real set
(lower_bound (rng (Z | (divset (x,r))))) * (vol (divset (x,r))) is V11() real ext-real Element of REAL
rfz * (vol (divset (x,r))) is V11() real ext-real Element of REAL
((lower_bound (rng (Z | (divset (x,r))))) + (f / (vol (divset (x,r))))) * (vol (divset (x,r))) is V11() real ext-real Element of REAL
Si is V11() real ext-real Element of REAL
(f / (vol (divset (x,r)))) * (vol (divset (x,r))) is V11() real ext-real Element of REAL
((lower_volume (Z,x)) . r) + ((f / (vol (divset (x,r)))) * (vol (divset (x,r)))) is V11() real ext-real Element of REAL
r is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
dom r is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
divset (x,i) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
Z | (divset (x,i)) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
rng (Z | (divset (x,i))) is V129() V130() V131() Element of K6(REAL)
r . i is V11() real ext-real Element of REAL
vol (divset (x,i)) is V11() real ext-real Element of REAL
upper_bound (divset (x,i)) is V11() real ext-real Element of REAL
lower_bound (divset (x,i)) is V11() real ext-real Element of REAL
(upper_bound (divset (x,i))) - (lower_bound (divset (x,i))) is V11() real ext-real Element of REAL
(lower_volume (Z,x)) . i is V11() real ext-real Element of REAL
((lower_volume (Z,x)) . i) + f is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
k * (vol (divset (x,i))) is V11() real ext-real Element of REAL
rfz is V11() real ext-real Element of REAL
rfz * (vol (divset (x,i))) is V11() real ext-real Element of REAL
len r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
divset (x,k) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
Z | (divset (x,k)) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
rng (Z | (divset (x,k))) is V129() V130() V131() Element of K6(REAL)
i is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x)
i . k is V11() real ext-real Element of REAL
vol (divset (x,k)) is V11() real ext-real Element of REAL
upper_bound (divset (x,k)) is V11() real ext-real Element of REAL
lower_bound (divset (x,k)) is V11() real ext-real Element of REAL
(upper_bound (divset (x,k))) - (lower_bound (divset (x,k))) is V11() real ext-real Element of REAL
(lower_volume (Z,x)) . k is V11() real ext-real Element of REAL
((lower_volume (Z,x)) . k) + f is V11() real ext-real Element of REAL
rfz is V11() real ext-real Element of REAL
rfz * (vol (divset (x,k))) is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
dom x is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
upper_volume (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
f is V11() real ext-real Element of REAL
len x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
Seg (len x) is non empty V32() V39( len x) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
divset (x,r) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
Z | (divset (x,r)) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
rng (Z | (divset (x,r))) is V129() V130() V131() Element of K6(REAL)
vol (divset (x,r)) is V11() real ext-real Element of REAL
upper_bound (divset (x,r)) is V11() real ext-real Element of REAL
lower_bound (divset (x,r)) is V11() real ext-real Element of REAL
(upper_bound (divset (x,r))) - (lower_bound (divset (x,r))) is V11() real ext-real Element of REAL
(upper_volume (Z,x)) . r is V11() real ext-real Element of REAL
((upper_volume (Z,x)) . r) - f is V11() real ext-real Element of REAL
dom Z is V129() V130() V131() Element of K6(n)
K6(n) is set
dom (Z | (divset (x,r))) is V129() V130() V131() Element of K6(n)
rng Z is V129() V130() V131() Element of K6(REAL)
i is set
k is V11() real ext-real Element of REAL
k * (vol (divset (x,r))) is V11() real ext-real Element of REAL
upper_bound (rng (Z | (divset (x,r)))) is V11() real ext-real Element of REAL
(upper_bound (rng (Z | (divset (x,r))))) * (vol (divset (x,r))) is V11() real ext-real Element of REAL
rfz is V11() real ext-real Element of REAL
upper_bound (rng (Z | (divset (x,r)))) is V11() real ext-real Element of REAL
f / (vol (divset (x,r))) is V11() real ext-real Element of REAL
(upper_bound (rng (Z | (divset (x,r))))) - (f / (vol (divset (x,r)))) is V11() real ext-real Element of REAL
rfz is V11() real ext-real set
(upper_bound (rng (Z | (divset (x,r))))) * (vol (divset (x,r))) is V11() real ext-real Element of REAL
rfz * (vol (divset (x,r))) is V11() real ext-real Element of REAL
Si is V11() real ext-real Element of REAL
((upper_bound (rng (Z | (divset (x,r))))) - (f / (vol (divset (x,r))))) * (vol (divset (x,r))) is V11() real ext-real Element of REAL
(f / (vol (divset (x,r)))) * (vol (divset (x,r))) is V11() real ext-real Element of REAL
((upper_volume (Z,x)) . r) - ((f / (vol (divset (x,r)))) * (vol (divset (x,r)))) is V11() real ext-real Element of REAL
r is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
dom r is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
divset (x,i) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
Z | (divset (x,i)) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
rng (Z | (divset (x,i))) is V129() V130() V131() Element of K6(REAL)
r . i is V11() real ext-real Element of REAL
vol (divset (x,i)) is V11() real ext-real Element of REAL
upper_bound (divset (x,i)) is V11() real ext-real Element of REAL
lower_bound (divset (x,i)) is V11() real ext-real Element of REAL
(upper_bound (divset (x,i))) - (lower_bound (divset (x,i))) is V11() real ext-real Element of REAL
(upper_volume (Z,x)) . i is V11() real ext-real Element of REAL
((upper_volume (Z,x)) . i) - f is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
k * (vol (divset (x,i))) is V11() real ext-real Element of REAL
rfz is V11() real ext-real Element of REAL
rfz * (vol (divset (x,i))) is V11() real ext-real Element of REAL
len r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
divset (x,k) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
Z | (divset (x,k)) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
rng (Z | (divset (x,k))) is V129() V130() V131() Element of K6(REAL)
i is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x)
i . k is V11() real ext-real Element of REAL
vol (divset (x,k)) is V11() real ext-real Element of REAL
upper_bound (divset (x,k)) is V11() real ext-real Element of REAL
lower_bound (divset (x,k)) is V11() real ext-real Element of REAL
(upper_bound (divset (x,k))) - (lower_bound (divset (x,k))) is V11() real ext-real Element of REAL
(upper_volume (Z,x)) . k is V11() real ext-real Element of REAL
((upper_volume (Z,x)) . k) - f is V11() real ext-real Element of REAL
rfz is V11() real ext-real Element of REAL
rfz * (vol (divset (x,k))) is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
dom x is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
upper_volume (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
f is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x)
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
f . r is V11() real ext-real Element of REAL
(upper_volume (Z,x)) . r is V11() real ext-real Element of REAL
divset (x,r) is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
Z | (divset (x,r)) is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
rng (Z | (divset (x,r))) is V129() V130() V131() Element of K6(REAL)
upper_bound (rng (Z | (divset (x,r)))) is V11() real ext-real Element of REAL
vol (divset (x,r)) is V11() real ext-real Element of REAL
upper_bound (divset (x,r)) is V11() real ext-real Element of REAL
lower_bound (divset (x,r)) is V11() real ext-real Element of REAL
(upper_bound (divset (x,r))) - (lower_bound (divset (x,r))) is V11() real ext-real Element of REAL
(upper_bound (rng (Z | (divset (x,r))))) * (vol (divset (x,r))) is V11() real ext-real Element of REAL
i is V11() real ext-real Element of REAL
i * (vol (divset (x,r))) is V11() real ext-real Element of REAL
rng Z is V129() V130() V131() Element of K6(REAL)
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
f is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x)
Sum f is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
lower_sum (Z,x) is V11() real ext-real Element of REAL
lower_volume (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum (lower_volume (Z,x)) is V11() real ext-real Element of REAL
f is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x)
(n,Z,x,f) is V11() real ext-real Element of REAL
Sum f is V11() real ext-real Element of REAL
len (lower_volume (Z,x)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
len x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
(len x) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
len f is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
Seg (len x) is non empty V32() V39( len x) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
dom x is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
r is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
r . k is V11() real ext-real Element of REAL
i is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
i . k is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
upper_sum (Z,x) is V11() real ext-real Element of REAL
upper_volume (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum (upper_volume (Z,x)) is V11() real ext-real Element of REAL
f is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x)
(n,Z,x,f) is V11() real ext-real Element of REAL
Sum f is V11() real ext-real Element of REAL
len (upper_volume (Z,x)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
len x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
(len x) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
len f is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
Seg (len x) is non empty V32() V39( len x) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
dom x is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
i is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
i . k is V11() real ext-real Element of REAL
r is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
r . k is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
lower_sum (Z,x) is V11() real ext-real Element of REAL
lower_volume (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum (lower_volume (Z,x)) is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
(lower_sum (Z,x)) + f is V11() real ext-real Element of REAL
len (lower_volume (Z,x)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
len x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
(len x) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
f / (len x) is V11() real ext-real Element of REAL
dom x is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
k is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x)
(len x) |-> (f / (len x)) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
r is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
r + ((len x) |-> (f / (len x))) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
(n,Z,x,k) is V11() real ext-real Element of REAL
Sum k is V11() real ext-real Element of REAL
len k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
S is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
Seg (len x) is non empty V32() V39( len x) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
xs is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
xs . S is V11() real ext-real Element of REAL
r . S is V11() real ext-real Element of REAL
(r . S) + (f / (len x)) is V11() real ext-real Element of REAL
((len x) |-> (f / (len x))) . S is V11() real ext-real Element of REAL
(r . S) + (((len x) |-> (f / (len x))) . S) is V11() real ext-real Element of REAL
Si is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
Si . S is V11() real ext-real Element of REAL
Sum xs is V11() real ext-real Element of REAL
Sum Si is V11() real ext-real Element of REAL
Sum r is V11() real ext-real Element of REAL
Sum ((len x) |-> (f / (len x))) is V11() real ext-real Element of REAL
(Sum r) + (Sum ((len x) |-> (f / (len x)))) is V11() real ext-real Element of REAL
(len x) * (f / (len x)) is V11() real ext-real Element of REAL
(Sum r) + ((len x) * (f / (len x))) is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
upper_sum (Z,x) is V11() real ext-real Element of REAL
upper_volume (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum (upper_volume (Z,x)) is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
(upper_sum (Z,x)) - f is V11() real ext-real Element of REAL
len (upper_volume (Z,x)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
len x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() Element of NAT
(len x) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
f / (len x) is V11() real ext-real Element of REAL
dom x is V129() V130() V131() V132() V133() V134() Element of K6(NAT)
k is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x)
(len x) |-> (f / (len x)) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
r is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
r - ((len x) |-> (f / (len x))) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
(n,Z,x,k) is V11() real ext-real Element of REAL
Sum k is V11() real ext-real Element of REAL
len k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
S is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
Seg (len x) is non empty V32() V39( len x) V129() V130() V131() V132() V133() V134() Element of K6(NAT)
r . S is V11() real ext-real Element of REAL
(r . S) - (f / (len x)) is V11() real ext-real Element of REAL
xs is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
xs . S is V11() real ext-real Element of REAL
((len x) |-> (f / (len x))) . S is V11() real ext-real Element of REAL
(r . S) - (((len x) |-> (f / (len x))) . S) is V11() real ext-real Element of REAL
Si is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len x) FinSequence-like FinSubsequence-like V119() V120() V121() Element of (len x) -tuples_on REAL
Si . S is V11() real ext-real Element of REAL
Sum Si is V11() real ext-real Element of REAL
Sum xs is V11() real ext-real Element of REAL
Sum r is V11() real ext-real Element of REAL
Sum ((len x) |-> (f / (len x))) is V11() real ext-real Element of REAL
(Sum r) - (Sum ((len x) |-> (f / (len x)))) is V11() real ext-real Element of REAL
(len x) * (f / (len x)) is V11() real ext-real Element of REAL
(Sum r) - ((len x) * (f / (len x))) is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
divs n is non empty set
K7(NAT,(divs n)) is V32() set
K6(K7(NAT,(divs n))) is V32() set
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(NAT,(REAL *)) is V32() set
K6(K7(NAT,(REAL *))) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( divs n) Function-like total V27( NAT , divs n) Element of K6(K7(NAT,(divs n)))
f is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
x . f is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
the V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x . f) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x . f)
i is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL *
f is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) Element of K6(K7(NAT,(REAL *)))
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
divs n is non empty set
K7(NAT,(divs n)) is V32() set
K6(K7(NAT,(divs n))) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( divs n) Function-like total V27( NAT , divs n) Element of K6(K7(NAT,(divs n)))
f is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,x)
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
f . r is FinSequence-like set
x . r is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
divs n is non empty set
K7(NAT,(divs n)) is V32() set
K6(K7(NAT,(divs n))) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( divs n) Function-like total V27( NAT , divs n) Element of K6(K7(NAT,(divs n)))
f is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,x)
r is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
i is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
r . k is V11() real ext-real Element of REAL
i . k is V11() real ext-real Element of REAL
x . k is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
(n,Z,x,f,k) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x . k)
(n,Z,(x . k),(n,Z,x,f,k)) is V11() real ext-real Element of REAL
Sum (n,Z,x,f,k) is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
divs n is non empty set
K7(NAT,(divs n)) is V32() set
K6(K7(NAT,(divs n))) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( divs n) Function-like total V27( NAT , divs n) Element of K6(K7(NAT,(divs n)))
lower_sum (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
f is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,x)
(n,Z,x,f) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(lower_sum (Z,x)) . r is V11() real ext-real Element of REAL
(n,Z,x,f) . r is V11() real ext-real Element of REAL
x . r is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
(n,Z,x,f,r) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x . r)
(n,Z,(x . r),(n,Z,x,f,r)) is V11() real ext-real Element of REAL
Sum (n,Z,x,f,r) is V11() real ext-real Element of REAL
lower_sum (Z,(x . r)) is V11() real ext-real Element of REAL
lower_volume (Z,(x . r)) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum (lower_volume (Z,(x . r))) is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
divs n is non empty set
K7(NAT,(divs n)) is V32() set
K6(K7(NAT,(divs n))) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( divs n) Function-like total V27( NAT , divs n) Element of K6(K7(NAT,(divs n)))
upper_sum (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
f is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,x)
(n,Z,x,f) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(n,Z,x,f) . r is V11() real ext-real Element of REAL
(upper_sum (Z,x)) . r is V11() real ext-real Element of REAL
x . r is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
(n,Z,x,f,r) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x . r)
(n,Z,(x . r),(n,Z,x,f,r)) is V11() real ext-real Element of REAL
Sum (n,Z,x,f,r) is V11() real ext-real Element of REAL
upper_sum (Z,(x . r)) is V11() real ext-real Element of REAL
upper_volume (Z,(x . r)) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum (upper_volume (Z,(x . r))) is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
divs n is non empty set
K7(NAT,(divs n)) is V32() set
K6(K7(NAT,(divs n))) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( divs n) Function-like total V27( NAT , divs n) Element of K6(K7(NAT,(divs n)))
lower_sum (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
f is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
x . r is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
lower_sum (Z,(x . r)) is V11() real ext-real Element of REAL
lower_volume (Z,(x . r)) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum (lower_volume (Z,(x . r))) is V11() real ext-real Element of REAL
(lower_sum (Z,(x . r))) + f is V11() real ext-real Element of REAL
i is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x . r)
(n,Z,(x . r),i) is V11() real ext-real Element of REAL
Sum i is V11() real ext-real Element of REAL
k is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL *
r is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) Element of K6(K7(NAT,(REAL *)))
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
x . k is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
i is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,x)
(n,Z,x,i,k) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x . k)
lower_sum (Z,(x . k)) is V11() real ext-real Element of REAL
lower_volume (Z,(x . k)) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum (lower_volume (Z,(x . k))) is V11() real ext-real Element of REAL
(lower_sum (Z,(x . k))) + f is V11() real ext-real Element of REAL
(n,Z,x,i) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
(n,Z,x,i) . k is V11() real ext-real Element of REAL
rfz is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x . k)
(n,Z,(x . k),rfz) is V11() real ext-real Element of REAL
Sum rfz is V11() real ext-real Element of REAL
(lower_sum (Z,x)) . k is V11() real ext-real Element of REAL
((lower_sum (Z,x)) . k) + f is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
divs n is non empty set
K7(NAT,(divs n)) is V32() set
K6(K7(NAT,(divs n))) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is non empty V13() V16( NAT ) V17( divs n) Function-like total V27( NAT , divs n) Element of K6(K7(NAT,(divs n)))
upper_sum (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
f is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
x . r is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
upper_sum (Z,(x . r)) is V11() real ext-real Element of REAL
upper_volume (Z,(x . r)) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum (upper_volume (Z,(x . r))) is V11() real ext-real Element of REAL
(upper_sum (Z,(x . r))) - f is V11() real ext-real Element of REAL
i is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x . r)
(n,Z,(x . r),i) is V11() real ext-real Element of REAL
Sum i is V11() real ext-real Element of REAL
k is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() Element of REAL *
r is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) Element of K6(K7(NAT,(REAL *)))
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
x . k is non empty V13() V16( NAT ) V17( REAL ) Function-like one-to-one V32() FinSequence-like FinSubsequence-like V119() V120() V121() V123() V125() Division of n
i is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,x)
(n,Z,x,i,k) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x . k)
upper_sum (Z,(x . k)) is V11() real ext-real Element of REAL
upper_volume (Z,(x . k)) is non empty V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() FinSequence of REAL
Sum (upper_volume (Z,(x . k))) is V11() real ext-real Element of REAL
(upper_sum (Z,(x . k))) - f is V11() real ext-real Element of REAL
(n,Z,x,i) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
(n,Z,x,i) . k is V11() real ext-real Element of REAL
rfz is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like V119() V120() V121() (n,Z,x . k)
(n,Z,(x . k),rfz) is V11() real ext-real Element of REAL
Sum rfz is V11() real ext-real Element of REAL
(upper_sum (Z,x)) . k is V11() real ext-real Element of REAL
((upper_sum (Z,x)) . k) - f is V11() real ext-real Element of REAL
n is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
x is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim n is V11() real ext-real Element of REAL
lim x is V11() real ext-real Element of REAL
Z is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim Z is V11() real ext-real Element of REAL
f is V11() real ext-real set
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
max (r,i) is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
k is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
rfz is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
Si is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
Z . Si is V11() real ext-real Element of REAL
(Z . Si) - (lim n) is V11() real ext-real Element of REAL
abs ((Z . Si) - (lim n)) is V11() real ext-real Element of REAL
n . Si is V11() real ext-real Element of REAL
(n . Si) - (lim n) is V11() real ext-real Element of REAL
abs ((n . Si) - (lim n)) is V11() real ext-real Element of REAL
(lim n) - f is V11() real ext-real Element of REAL
(lim n) + f is V11() real ext-real Element of REAL
].((lim n) - f),((lim n) + f).[ is V129() V130() V131() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= (lim n) - f & not (lim n) + f <= b₁ ) } is set
xs is V11() real ext-real Element of REAL
x . Si is V11() real ext-real Element of REAL
(x . Si) - (lim x) is V11() real ext-real Element of REAL
abs ((x . Si) - (lim x)) is V11() real ext-real Element of REAL
(lim x) - f is V11() real ext-real Element of REAL
(lim x) + f is V11() real ext-real Element of REAL
].((lim x) - f),((lim x) + f).[ is V129() V130() V131() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= (lim x) - f & not (lim x) + f <= b₁ ) } is set
xs is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
divs n is non empty set
K7(NAT,(divs n)) is V32() set
K6(K7(NAT,(divs n))) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
integral Z is V11() real ext-real Element of REAL
upper_integral Z is V11() real ext-real Element of REAL
upper_sum_set Z is non empty V13() V16( divs n) V17( REAL ) Function-like total V27( divs n, REAL ) V119() V120() V121() Element of K6(K7((divs n),REAL))
K7((divs n),REAL) is V32() V119() V120() V121() set
K6(K7((divs n),REAL)) is V32() set
rng (upper_sum_set Z) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set Z)) is V11() real ext-real Element of REAL
x is non empty V13() V16( NAT ) V17( divs n) Function-like total V27( NAT , divs n) Element of K6(K7(NAT,(divs n)))
delta x is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim (delta x) is V11() real ext-real Element of REAL
f is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,x)
(n,Z,x,f) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim (n,Z,x,f) is V11() real ext-real Element of REAL
dom Z is V129() V130() V131() Element of K6(n)
K6(n) is set
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
lower_sum (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(lower_sum (Z,x)) . r is V11() real ext-real Element of REAL
(n,Z,x,f) . r is V11() real ext-real Element of REAL
upper_sum (Z,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
r is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(n,Z,x,f) . r is V11() real ext-real Element of REAL
(upper_sum (Z,x)) . r is V11() real ext-real Element of REAL
lim (upper_sum (Z,x)) is V11() real ext-real Element of REAL
lim (lower_sum (Z,x)) is V11() real ext-real Element of REAL
(lim (upper_sum (Z,x))) - (lim (lower_sum (Z,x))) is V11() real ext-real Element of REAL
n is non empty V129() V130() V131() real-bounded interval V226() closed_interval Element of K6(REAL)
K7(n,REAL) is V32() V119() V120() V121() set
K6(K7(n,REAL)) is V32() set
divs n is non empty set
K7(NAT,(divs n)) is V32() set
K6(K7(NAT,(divs n))) is V32() set
Z is non empty V13() V16(n) V17( REAL ) Function-like total V27(n, REAL ) V119() V120() V121() Element of K6(K7(n,REAL))
integral Z is V11() real ext-real Element of REAL
upper_integral Z is V11() real ext-real Element of REAL
upper_sum_set Z is non empty V13() V16( divs n) V17( REAL ) Function-like total V27( divs n, REAL ) V119() V120() V121() Element of K6(K7((divs n),REAL))
K7((divs n),REAL) is V32() V119() V120() V121() set
K6(K7((divs n),REAL)) is V32() set
rng (upper_sum_set Z) is V129() V130() V131() Element of K6(REAL)
lower_bound (rng (upper_sum_set Z)) is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
f is non empty V13() V16( NAT ) V17( divs n) Function-like total V27( NAT , divs n) Element of K6(K7(NAT,(divs n)))
delta f is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim (delta f) is V11() real ext-real Element of REAL
r is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)
(n,Z,f,r) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim (n,Z,f,r) is V11() real ext-real Element of REAL
dom Z is V129() V130() V131() Element of K6(n)
K6(n) is set
Z | n is V13() V16(n) V17( REAL ) Function-like V119() V120() V121() Element of K6(K7(n,REAL))
x is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
f is non empty V13() V16( NAT ) V17( divs n) Function-like total V27( NAT , divs n) Element of K6(K7(NAT,(divs n)))
delta f is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim (delta f) is V11() real ext-real Element of REAL
upper_sum (Z,f) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
lim (upper_sum (Z,f)) is V11() real ext-real Element of REAL
the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f) is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)
(n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
i is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)) . i is V11() real ext-real Element of REAL
(upper_sum (Z,f)) . i is V11() real ext-real Element of REAL
((n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)) . i) - ((n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)) . i) is V11() real ext-real Element of REAL
((upper_sum (Z,f)) . i) - ((n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)) . i) is V11() real ext-real Element of REAL
(upper_sum (Z,f)) - (n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
((upper_sum (Z,f)) - (n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f))) . i is V11() real ext-real Element of REAL
i is V11() real ext-real set
k is V11() real ext-real Element of REAL
rfz is non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f)
(n,Z,f,rfz) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
Si is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() Element of NAT
(upper_sum (Z,f)) . Si is V11() real ext-real Element of REAL
((upper_sum (Z,f)) . Si) - k is V11() real ext-real Element of REAL
(n,Z,f,rfz) . Si is V11() real ext-real Element of REAL
(((upper_sum (Z,f)) . Si) - k) + k is V11() real ext-real Element of REAL
((n,Z,f,rfz) . Si) + k is V11() real ext-real Element of REAL
((upper_sum (Z,f)) . Si) - ((n,Z,f,rfz) . Si) is V11() real ext-real Element of REAL
(((n,Z,f,rfz) . Si) + k) - ((n,Z,f,rfz) . Si) is V11() real ext-real Element of REAL
(upper_sum (Z,f)) - (n,Z,f,rfz) is non empty V13() V16( NAT ) V17( REAL ) Function-like total V27( NAT , REAL ) V119() V120() V121() Element of K6(K7(NAT,REAL))
((upper_sum (Z,f)) - (n,Z,f,rfz)) . Si is V11() real ext-real Element of REAL
lim ((upper_sum (Z,f)) - (n,Z,f,rfz)) is V11() real ext-real Element of REAL
lim (n,Z,f,rfz) is V11() real ext-real Element of REAL
(lim (upper_sum (Z,f))) - (lim (n,Z,f,rfz)) is V11() real ext-real Element of REAL
(lim (upper_sum (Z,f))) - x is V11() real ext-real Element of REAL
lim ((upper_sum (Z,f)) - (n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27( NAT ,REAL * ) (n,Z,f))) is V11() real ext-real Element of REAL
lim (n,Z,f, the non empty V13() V16( NAT ) V17(REAL * ) Function-like total V27(