:: INTEGRA6 semantic presentation

REAL is non empty V2() V45() V46() V47() V51() V58() non bounded_below non bounded_above interval set
NAT is non empty V2() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V58() V63() V64() left_end bounded_below Element of K6(REAL)
K6(REAL) is V2() V58() set
COMPLEX is non empty V2() V45() V51() V58() set
RAT is non empty V2() V45() V46() V47() V48() V51() V58() set
INT is non empty V2() V45() V46() V47() V48() V49() V51() V58() set
K7(COMPLEX,COMPLEX) is V2() Relation-like complex-valued V58() set
K6(K7(COMPLEX,COMPLEX)) is V2() V58() set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V2() Relation-like complex-valued V58() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is V2() V58() set
K7(REAL,REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(REAL,REAL)) is V2() V58() set
K7(K7(REAL,REAL),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(K7(REAL,REAL),REAL)) is V2() V58() set
K7(RAT,RAT) is V2() Relation-like RAT -valued complex-valued ext-real-valued real-valued V58() set
K6(K7(RAT,RAT)) is V2() V58() set
K7(K7(RAT,RAT),RAT) is V2() Relation-like RAT -valued complex-valued ext-real-valued real-valued V58() set
K6(K7(K7(RAT,RAT),RAT)) is V2() V58() set
K7(INT,INT) is V2() Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued V58() set
K6(K7(INT,INT)) is V2() V58() set
K7(K7(INT,INT),INT) is V2() Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued V58() set
K6(K7(K7(INT,INT),INT)) is V2() V58() set
K7(NAT,NAT) is V2() Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued V58() set
K7(K7(NAT,NAT),NAT) is V2() Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued V58() set
K6(K7(K7(NAT,NAT),NAT)) is V2() V58() set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued functional integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V45() V46() V47() V48() V49() V50() V51() V58() V59() V62() V63() V65( {} ) FinSequence-like FinSequence-membered bounded_below bounded_above real-bounded interval set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
{{},1} is non empty V45() V46() V47() V48() V49() V50() V58() V62() left_end right_end bounded_below bounded_above real-bounded set
omega is non empty V2() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V58() V63() V64() left_end bounded_below set
K6(omega) is V2() V58() set
K6(NAT) is V2() V58() set
K7(NAT,REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(NAT,REAL)) is V2() V58() set
the_set_of_RealSequences is non empty set
K7(the_set_of_RealSequences,the_set_of_RealSequences) is Relation-like set
K7(K7(the_set_of_RealSequences,the_set_of_RealSequences),the_set_of_RealSequences) is Relation-like set
K6(K7(K7(the_set_of_RealSequences,the_set_of_RealSequences),the_set_of_RealSequences)) is set
K7(REAL,the_set_of_RealSequences) is V2() Relation-like V58() set
K7(K7(REAL,the_set_of_RealSequences),the_set_of_RealSequences) is V2() Relation-like V58() set
K6(K7(K7(REAL,the_set_of_RealSequences),the_set_of_RealSequences)) is V2() V58() set
Linear_Space_of_RealSequences is L12()
the U1 of Linear_Space_of_RealSequences is set
K6( the U1 of Linear_Space_of_RealSequences) is set
the_set_of_l2RealSequences is Element of K6( the U1 of Linear_Space_of_RealSequences)
K7(the_set_of_l2RealSequences,the_set_of_l2RealSequences) is Relation-like set
K7(K7(the_set_of_l2RealSequences,the_set_of_l2RealSequences),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(K7(the_set_of_l2RealSequences,the_set_of_l2RealSequences),REAL)) is set
ExtREAL is non empty V46() interval set
K7(COMPLEX,REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(COMPLEX,REAL)) is V2() V58() set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued functional integer V31() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V45() V46() V47() V48() V49() V50() V51() V58() V59() V62() V63() V65( {} ) FinSequence-like FinSequence-membered bounded_below bounded_above real-bounded interval Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() 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 integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
a is V11() real ext-real set
b is V11() real ext-real set
f is V11() real ext-real set
a + f is V11() real ext-real set
x0 is V11() real ext-real set
b + x0 is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
f is V11() real ext-real set
f - a is V11() real ext-real set
- a is V11() real ext-real set
f + (- a) is V11() real ext-real set
f + a is V11() real ext-real set
].(f - a),(f + a).[ is V45() V46() V47() open non left_end non right_end interval Element of K6(REAL)
f - b is V11() real ext-real set
- b is V11() real ext-real set
f + (- b) is V11() real ext-real set
f + b is V11() real ext-real set
].(f - b),(f + b).[ is V45() V46() V47() open non left_end non right_end interval Element of K6(REAL)
a is Relation-like set
b is set
f is set
x0 is set
a | f is Relation-like set
(a | f) | b is Relation-like set
a | x0 is Relation-like set
(a | x0) | b is Relation-like set
a | b is Relation-like set
a is set
b is set
f is set
chi (b,b) is Relation-like b -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(b,REAL))
K7(b,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(b,REAL)) is set
(chi (b,b)) | a is Relation-like a -defined b -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(b,REAL))
chi (f,f) is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(f,REAL))
K7(f,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(f,REAL)) is set
(chi (f,f)) | a is Relation-like a -defined f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(f,REAL))
dom ((chi (f,f)) | a) is set
dom (chi (f,f)) is set
(dom (chi (f,f))) /\ a is set
f /\ a is set
dom ((chi (b,b)) | a) is set
dom (chi (b,b)) is set
(dom (chi (b,b))) /\ a is set
b /\ a is set
x0 is set
((chi (b,b)) | a) . x0 is V11() real ext-real Element of REAL
(chi (b,b)) . x0 is V11() real ext-real Element of REAL
(chi (f,f)) . x0 is V11() real ext-real Element of REAL
((chi (f,f)) | a) . x0 is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
vol ['a,b'] is V11() real ext-real Element of REAL
upper_bound ['a,b'] is V11() real ext-real Element of REAL
lower_bound ['a,b'] is V11() real ext-real Element of REAL
(upper_bound ['a,b']) - (lower_bound ['a,b']) is V11() real ext-real Element of REAL
- (lower_bound ['a,b']) is V11() real ext-real set
(upper_bound ['a,b']) + (- (lower_bound ['a,b'])) is V11() real ext-real set
b - a is V11() real ext-real set
- a is V11() real ext-real set
b + (- a) is V11() real ext-real set
[.a,b.] is V45() V46() V47() closed interval Element of K6(REAL)
lower_bound [.a,b.] is V11() real ext-real Element of REAL
upper_bound [.a,b.] is V11() real ext-real Element of REAL
[.(lower_bound [.a,b.]),(upper_bound [.a,b.]).] is V45() V46() V47() closed interval Element of K6(REAL)
a is V11() real ext-real set
b is V11() real ext-real set
min (a,b) is V11() real ext-real set
max (a,b) is V11() real ext-real set
['(min (a,b)),(max (a,b))'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
vol ['(min (a,b)),(max (a,b))'] is V11() real ext-real Element of REAL
upper_bound ['(min (a,b)),(max (a,b))'] is V11() real ext-real Element of REAL
lower_bound ['(min (a,b)),(max (a,b))'] is V11() real ext-real Element of REAL
(upper_bound ['(min (a,b)),(max (a,b))']) - (lower_bound ['(min (a,b)),(max (a,b))']) is V11() real ext-real Element of REAL
- (lower_bound ['(min (a,b)),(max (a,b))']) is V11() real ext-real set
(upper_bound ['(min (a,b)),(max (a,b))']) + (- (lower_bound ['(min (a,b)),(max (a,b))'])) is V11() real ext-real set
b - a is V11() real ext-real set
- a is V11() real ext-real set
b + (- a) is V11() real ext-real set
abs (b - a) is V11() real ext-real Element of REAL
a - b is V11() real ext-real set
- b is V11() real ext-real set
a + (- b) is V11() real ext-real set
abs (a - b) is V11() real ext-real Element of REAL
a is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
K7(a,REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(a,REAL)) is V2() V58() set
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom b is set
b || a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
rng b is V45() V46() V47() Element of K6(REAL)
K7((dom b),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7((dom b),REAL)) is set
a is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom b is set
b | a is Relation-like REAL -defined a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
abs b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral (b,a) is V11() real ext-real Element of REAL
b || a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
K7(a,REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(a,REAL)) is V2() V58() set
integral (b || a) is V11() real ext-real Element of REAL
upper_integral (b || a) is V11() real ext-real Element of REAL
upper_sum_set (b || a) is non empty Relation-like divs a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs a),REAL))
divs a is non empty set
K7((divs a),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs a),REAL)) is V2() V58() set
rng (upper_sum_set (b || a)) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (b || a))) is V11() real ext-real Element of REAL
abs (integral (b,a)) is V11() real ext-real Element of REAL
integral ((abs b),a) is V11() real ext-real Element of REAL
(abs b) || a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
integral ((abs b) || a) is V11() real ext-real Element of REAL
upper_integral ((abs b) || a) is V11() real ext-real Element of REAL
upper_sum_set ((abs b) || a) is non empty Relation-like divs a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs a),REAL))
rng (upper_sum_set ((abs b) || a)) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((abs b) || a))) is V11() real ext-real Element of REAL
abs (b || a) is Relation-like REAL -defined a -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
(b || a) | a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
f is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
f | ['a,b'] is Relation-like REAL -defined ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral (f,a,b) is V11() real ext-real Element of REAL
abs (integral (f,a,b)) is V11() real ext-real Element of REAL
abs f is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral ((abs f),a,b) is V11() real ext-real Element of REAL
integral (f,['a,b']) is V11() real ext-real Element of REAL
f || ['a,b'] is Relation-like ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
K7(['a,b'],REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(['a,b'],REAL)) is V2() V58() set
integral (f || ['a,b']) is V11() real ext-real Element of REAL
upper_integral (f || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set (f || ['a,b']) is non empty Relation-like divs ['a,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['a,b']),REAL))
divs ['a,b'] is non empty set
K7((divs ['a,b']),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs ['a,b']),REAL)) is V2() V58() set
rng (upper_sum_set (f || ['a,b'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (f || ['a,b']))) is V11() real ext-real Element of REAL
integral ((abs f),['a,b']) is V11() real ext-real Element of REAL
(abs f) || ['a,b'] is Relation-like ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
integral ((abs f) || ['a,b']) is V11() real ext-real Element of REAL
upper_integral ((abs f) || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set ((abs f) || ['a,b']) is non empty Relation-like divs ['a,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['a,b']),REAL))
rng (upper_sum_set ((abs f) || ['a,b'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((abs f) || ['a,b']))) is V11() real ext-real Element of REAL
a is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom b is set
b | a is Relation-like REAL -defined a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral (b,a) is V11() real ext-real Element of REAL
b || a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
K7(a,REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(a,REAL)) is V2() V58() set
integral (b || a) is V11() real ext-real Element of REAL
upper_integral (b || a) is V11() real ext-real Element of REAL
upper_sum_set (b || a) is non empty Relation-like divs a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs a),REAL))
divs a is non empty set
K7((divs a),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs a),REAL)) is V2() V58() set
rng (upper_sum_set (b || a)) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (b || a))) is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
f (#) b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral ((f (#) b),a) is V11() real ext-real Element of REAL
(f (#) b) || a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
integral ((f (#) b) || a) is V11() real ext-real Element of REAL
upper_integral ((f (#) b) || a) is V11() real ext-real Element of REAL
upper_sum_set ((f (#) b) || a) is non empty Relation-like divs a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs a),REAL))
rng (upper_sum_set ((f (#) b) || a)) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((f (#) b) || a))) is V11() real ext-real Element of REAL
f * (integral (b,a)) is V11() real ext-real Element of REAL
(b || a) | a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
rng b is V45() V46() V47() Element of K6(REAL)
K7((dom b),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7((dom b),REAL)) is set
f (#) (b || a) is Relation-like REAL -defined a -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
(f (#) b) | a is Relation-like REAL -defined a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral (f (#) (b || a)) is V11() real ext-real Element of REAL
upper_integral (f (#) (b || a)) is V11() real ext-real Element of REAL
upper_sum_set (f (#) (b || a)) is non empty Relation-like divs a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs a),REAL))
rng (upper_sum_set (f (#) (b || a))) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (f (#) (b || a)))) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
f is V11() real ext-real set
x0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom x0 is set
x0 | ['a,b'] is Relation-like REAL -defined ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f (#) x0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral ((f (#) x0),a,b) is V11() real ext-real Element of REAL
integral (x0,a,b) is V11() real ext-real Element of REAL
f * (integral (x0,a,b)) is V11() real ext-real Element of REAL
integral (x0,['a,b']) is V11() real ext-real Element of REAL
x0 || ['a,b'] is Relation-like ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
K7(['a,b'],REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(['a,b'],REAL)) is V2() V58() set
integral (x0 || ['a,b']) is V11() real ext-real Element of REAL
upper_integral (x0 || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set (x0 || ['a,b']) is non empty Relation-like divs ['a,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['a,b']),REAL))
divs ['a,b'] is non empty set
K7((divs ['a,b']),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs ['a,b']),REAL)) is V2() V58() set
rng (upper_sum_set (x0 || ['a,b'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (x0 || ['a,b']))) is V11() real ext-real Element of REAL
integral ((f (#) x0),['a,b']) is V11() real ext-real Element of REAL
(f (#) x0) || ['a,b'] is Relation-like ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
integral ((f (#) x0) || ['a,b']) is V11() real ext-real Element of REAL
upper_integral ((f (#) x0) || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set ((f (#) x0) || ['a,b']) is non empty Relation-like divs ['a,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['a,b']),REAL))
rng (upper_sum_set ((f (#) x0) || ['a,b'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((f (#) x0) || ['a,b']))) is V11() real ext-real Element of REAL
a is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom b is set
b | a is Relation-like REAL -defined a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral (b,a) is V11() real ext-real Element of REAL
b || a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
K7(a,REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(a,REAL)) is V2() V58() set
integral (b || a) is V11() real ext-real Element of REAL
upper_integral (b || a) is V11() real ext-real Element of REAL
upper_sum_set (b || a) is non empty Relation-like divs a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs a),REAL))
divs a is non empty set
K7((divs a),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs a),REAL)) is V2() V58() set
rng (upper_sum_set (b || a)) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (b || a))) is V11() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
f | a is Relation-like REAL -defined a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
b + f is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
b - f is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral ((b + f),a) is V11() real ext-real Element of REAL
(b + f) || a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
integral ((b + f) || a) is V11() real ext-real Element of REAL
upper_integral ((b + f) || a) is V11() real ext-real Element of REAL
upper_sum_set ((b + f) || a) is non empty Relation-like divs a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs a),REAL))
rng (upper_sum_set ((b + f) || a)) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((b + f) || a))) is V11() real ext-real Element of REAL
integral (f,a) is V11() real ext-real Element of REAL
f || a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
integral (f || a) is V11() real ext-real Element of REAL
upper_integral (f || a) is V11() real ext-real Element of REAL
upper_sum_set (f || a) is non empty Relation-like divs a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs a),REAL))
rng (upper_sum_set (f || a)) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (f || a))) is V11() real ext-real Element of REAL
(integral (b,a)) + (integral (f,a)) is V11() real ext-real Element of REAL
integral ((b - f),a) is V11() real ext-real Element of REAL
(b - f) || a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
integral ((b - f) || a) is V11() real ext-real Element of REAL
upper_integral ((b - f) || a) is V11() real ext-real Element of REAL
upper_sum_set ((b - f) || a) is non empty Relation-like divs a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs a),REAL))
rng (upper_sum_set ((b - f) || a)) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((b - f) || a))) is V11() real ext-real Element of REAL
(integral (b,a)) - (integral (f,a)) is V11() real ext-real Element of REAL
- (integral (f,a)) is V11() real ext-real set
(integral (b,a)) + (- (integral (f,a))) is V11() real ext-real set
(b || a) | a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
(f || a) | a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
(b || a) + (f || a) is Relation-like REAL -defined a -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
(b || a) - (f || a) is Relation-like REAL -defined a -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
f is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
f | ['a,b'] is Relation-like REAL -defined ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral (f,a,b) is V11() real ext-real Element of REAL
x0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom x0 is set
x0 | ['a,b'] is Relation-like REAL -defined ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f + x0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral ((f + x0),a,b) is V11() real ext-real Element of REAL
integral (x0,a,b) is V11() real ext-real Element of REAL
(integral (f,a,b)) + (integral (x0,a,b)) is V11() real ext-real Element of REAL
f - x0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral ((f - x0),a,b) is V11() real ext-real Element of REAL
(integral (f,a,b)) - (integral (x0,a,b)) is V11() real ext-real Element of REAL
- (integral (x0,a,b)) is V11() real ext-real set
(integral (f,a,b)) + (- (integral (x0,a,b))) is V11() real ext-real set
integral ((f + x0),['a,b']) is V11() real ext-real Element of REAL
(f + x0) || ['a,b'] is Relation-like ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
K7(['a,b'],REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(['a,b'],REAL)) is V2() V58() set
integral ((f + x0) || ['a,b']) is V11() real ext-real Element of REAL
upper_integral ((f + x0) || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set ((f + x0) || ['a,b']) is non empty Relation-like divs ['a,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['a,b']),REAL))
divs ['a,b'] is non empty set
K7((divs ['a,b']),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs ['a,b']),REAL)) is V2() V58() set
rng (upper_sum_set ((f + x0) || ['a,b'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((f + x0) || ['a,b']))) is V11() real ext-real Element of REAL
integral ((f - x0),['a,b']) is V11() real ext-real Element of REAL
(f - x0) || ['a,b'] is Relation-like ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
integral ((f - x0) || ['a,b']) is V11() real ext-real Element of REAL
upper_integral ((f - x0) || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set ((f - x0) || ['a,b']) is non empty Relation-like divs ['a,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['a,b']),REAL))
rng (upper_sum_set ((f - x0) || ['a,b'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((f - x0) || ['a,b']))) is V11() real ext-real Element of REAL
integral (f,['a,b']) is V11() real ext-real Element of REAL
f || ['a,b'] is Relation-like ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
integral (f || ['a,b']) is V11() real ext-real Element of REAL
upper_integral (f || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set (f || ['a,b']) is non empty Relation-like divs ['a,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['a,b']),REAL))
rng (upper_sum_set (f || ['a,b'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (f || ['a,b']))) is V11() real ext-real Element of REAL
integral (x0,['a,b']) is V11() real ext-real Element of REAL
x0 || ['a,b'] is Relation-like ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
integral (x0 || ['a,b']) is V11() real ext-real Element of REAL
upper_integral (x0 || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set (x0 || ['a,b']) is non empty Relation-like divs ['a,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['a,b']),REAL))
rng (upper_sum_set (x0 || ['a,b'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (x0 || ['a,b']))) is V11() real ext-real Element of REAL
a is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
b | a is Relation-like REAL -defined a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f | a is Relation-like REAL -defined a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
b (#) f is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(b (#) f) | a is Relation-like REAL -defined a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
a /\ a is V45() V46() V47() interval Element of K6(REAL)
(b (#) f) | (a /\ a) is Relation-like REAL -defined a /\ a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
a is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom b is set
b | a is Relation-like REAL -defined a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
f | a is Relation-like REAL -defined a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
b (#) f is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
b || a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
K7(a,REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(a,REAL)) is V2() V58() set
(b || a) | a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
f || a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
(f || a) | a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
(b || a) (#) (f || a) is Relation-like REAL -defined a -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
(b (#) f) || a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
a is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
vol a is V11() real ext-real Element of REAL
upper_bound a is V11() real ext-real Element of REAL
lower_bound a is V11() real ext-real Element of REAL
(upper_bound a) - (lower_bound a) is V11() real ext-real Element of REAL
- (lower_bound a) is V11() real ext-real set
(upper_bound a) + (- (lower_bound a)) is V11() real ext-real set
b is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(vol a) / b is V11() real ext-real Element of REAL
b " is V11() real ext-real non negative set
(vol a) * (b ") is V11() real ext-real set
f is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
len f is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
dom f is V45() V46() V47() V48() V49() V50() V58() bounded_below bounded_above real-bounded Element of K6(NAT)
x0 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
f . F is V11() real ext-real Element of REAL
f . x0 is V11() real ext-real Element of REAL
((vol a) / b) * F is V11() real ext-real Element of REAL
((vol a) / b) * x0 is V11() real ext-real Element of REAL
(lower_bound a) + (((vol a) / b) * F) is V11() real ext-real Element of REAL
(lower_bound a) + (((vol a) / b) * x0) is V11() real ext-real Element of REAL
Seg b is V45() V46() V47() V48() V49() V50() V58() V65(b) bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= b ) } is set
x0 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like FinSequence of REAL
len x0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
x0 . (len x0) is V11() real ext-real Element of REAL
((vol a) / b) * b is V11() real ext-real Element of REAL
(lower_bound a) + (((vol a) / b) * b) is V11() real ext-real Element of REAL
(lower_bound a) + (vol a) is V11() real ext-real Element of REAL
rng x0 is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
F is set
dom x0 is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
c₆ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
x0 . c₆ is V11() real ext-real Element of REAL
((vol a) / b) * c₆ is V11() real ext-real Element of REAL
(lower_bound a) + (((vol a) / b) * c₆) is V11() real ext-real Element of REAL
F is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
len F is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
dom F is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
c₆ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
F . c₆ is V11() real ext-real Element of REAL
((vol a) / b) * c₆ is V11() real ext-real Element of REAL
(lower_bound a) + (((vol a) / b) * c₆) is V11() real ext-real Element of REAL
a is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
vol a is V11() real ext-real Element of REAL
upper_bound a is V11() real ext-real Element of REAL
lower_bound a is V11() real ext-real Element of REAL
(upper_bound a) - (lower_bound a) is V11() real ext-real Element of REAL
- (lower_bound a) is V11() real ext-real set
(upper_bound a) + (- (lower_bound a)) is V11() real ext-real set
divs a is non empty set
K7(NAT,(divs a)) is V2() Relation-like V58() set
K6(K7(NAT,(divs a))) is V2() V58() set
b is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
b + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(vol a) / (b + 1) is V11() real ext-real Element of REAL
(b + 1) " is non empty V11() real ext-real positive non negative set
(vol a) * ((b + 1) ") is V11() real ext-real set
f is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
len f is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
dom f is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
x0 is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like Element of divs a
b is non empty Relation-like NAT -defined divs a -valued Function-like total quasi_total Element of K6(K7(NAT,(divs a)))
f is non empty Relation-like NAT -defined divs a -valued Function-like total quasi_total Element of K6(K7(NAT,(divs a)))
x0 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
x0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
f . x0 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
F is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
c₆ is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
F + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
delta f is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
x0 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(delta f) . x0 is V11() real ext-real Element of REAL
x0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(vol a) / (x0 + 1) is V11() real ext-real Element of REAL
(x0 + 1) " is non empty V11() real ext-real positive non negative set
(vol a) * ((x0 + 1) ") is V11() real ext-real set
chi (a,a) is Relation-like a -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
K7(a,REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(a,REAL)) is V2() V58() set
f . x0 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
upper_volume ((chi (a,a)),(f . x0)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
rng (upper_volume ((chi (a,a)),(f . x0))) is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
{((vol a) / (x0 + 1))} is non empty V2() V45() V46() V47() V58() V65(1) left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
c₆ is set
dom (upper_volume ((chi (a,a)),(f . x0))) is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
x is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(upper_volume ((chi (a,a)),(f . x0))) . x is V11() real ext-real Element of REAL
len (upper_volume ((chi (a,a)),(f . x0))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len (upper_volume ((chi (a,a)),(f . x0)))) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len (upper_volume ((chi (a,a)),(f . x0)))) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len (upper_volume ((chi (a,a)),(f . x0))) ) } is set
F is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
len F is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len F) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len F) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len F ) } is set
dom F is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
divset (F,x) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
upper_bound (divset (F,x)) is V11() real ext-real Element of REAL
lower_bound (divset (F,x)) is V11() real ext-real Element of REAL
(upper_bound (divset (F,x))) - (lower_bound (divset (F,x))) is V11() real ext-real Element of REAL
- (lower_bound (divset (F,x))) is V11() real ext-real set
(upper_bound (divset (F,x))) + (- (lower_bound (divset (F,x)))) is V11() real ext-real set
L is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
R is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
L + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
F . 1 is V11() real ext-real Element of REAL
((vol a) / (x0 + 1)) * 1 is V11() real ext-real Element of REAL
(lower_bound a) + (((vol a) / (x0 + 1)) * 1) is V11() real ext-real Element of REAL
L is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
R is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
L + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(lower_bound a) + ((vol a) / (x0 + 1)) is V11() real ext-real Element of REAL
((lower_bound a) + ((vol a) / (x0 + 1))) - (lower_bound a) is V11() real ext-real Element of REAL
((lower_bound a) + ((vol a) / (x0 + 1))) + (- (lower_bound a)) is V11() real ext-real set
x - 1 is V11() real integer ext-real Element of REAL
- 1 is V11() real integer ext-real non positive set
x + (- 1) is V11() real integer ext-real set
F . (x - 1) is V11() real ext-real Element of REAL
(vol a) / (len F) is V11() real ext-real Element of REAL
(len F) " is non empty V11() real ext-real positive non negative set
(vol a) * ((len F) ") is V11() real ext-real set
((vol a) / (len F)) * (x - 1) is V11() real ext-real Element of REAL
(lower_bound a) + (((vol a) / (len F)) * (x - 1)) is V11() real ext-real Element of REAL
L is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
R is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
L + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
F . x is V11() real ext-real Element of REAL
((vol a) / (len F)) * x is V11() real ext-real Element of REAL
(lower_bound a) + (((vol a) / (len F)) * x) is V11() real ext-real Element of REAL
L is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
R is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
L + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
L is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
R is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
L + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
vol (divset (F,x)) is V11() real ext-real Element of REAL
c₆ is set
F is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
rng F is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
dom F is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
divset (F,1) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
upper_bound (divset (F,1)) is V11() real ext-real Element of REAL
F . 1 is V11() real ext-real Element of REAL
len F is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(vol a) / (len F) is V11() real ext-real Element of REAL
(len F) " is non empty V11() real ext-real positive non negative set
(vol a) * ((len F) ") is V11() real ext-real set
((vol a) / (len F)) * 1 is V11() real ext-real Element of REAL
(lower_bound a) + (((vol a) / (len F)) * 1) is V11() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
L is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
vol (divset (F,1)) is V11() real ext-real Element of REAL
lower_bound (divset (F,1)) is V11() real ext-real Element of REAL
(upper_bound (divset (F,1))) - (lower_bound (divset (F,1))) is V11() real ext-real Element of REAL
- (lower_bound (divset (F,1))) is V11() real ext-real set
(upper_bound (divset (F,1))) + (- (lower_bound (divset (F,1)))) is V11() real ext-real set
(lower_bound a) + ((vol a) / (len F)) is V11() real ext-real Element of REAL
((lower_bound a) + ((vol a) / (len F))) - (lower_bound a) is V11() real ext-real Element of REAL
((lower_bound a) + ((vol a) / (len F))) + (- (lower_bound a)) is V11() real ext-real set
Seg (len F) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len F) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len F ) } is set
upper_volume ((chi (a,a)),F) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
len (upper_volume ((chi (a,a)),F)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len (upper_volume ((chi (a,a)),F))) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len (upper_volume ((chi (a,a)),F))) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len (upper_volume ((chi (a,a)),F)) ) } is set
dom (upper_volume ((chi (a,a)),F)) is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
(upper_volume ((chi (a,a)),F)) . 1 is V11() real ext-real Element of REAL
rng (upper_volume ((chi (a,a)),F)) is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
x is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
L is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
delta (f . x0) is V11() real ext-real Element of REAL
sup (rng (upper_volume ((chi (a,a)),(f . x0)))) is V11() real ext-real set
x0 is V11() real ext-real Element of REAL
(vol a) / x0 is V11() real ext-real Element of REAL
x0 " is V11() real ext-real set
(vol a) * (x0 ") is V11() real ext-real set
[\((vol a) / x0)/] is V11() real integer ext-real set
[\((vol a) / x0)/] + 1 is V11() real integer ext-real Element of REAL
F is V11() real integer ext-real set
c₆ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
c₆ + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
1 * (c₆ + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
1 * x0 is V11() real ext-real Element of REAL
(vol a) / (c₆ + 1) is V11() real ext-real Element of REAL
(c₆ + 1) " is non empty V11() real ext-real positive non negative set
(vol a) * ((c₆ + 1) ") is V11() real ext-real set
(delta f) . c₆ is V11() real ext-real Element of REAL
((vol a) / (c₆ + 1)) - 0 is V11() real ext-real Element of REAL
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued functional integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V45() V46() V47() V48() V49() V50() V51() V58() V59() V62() V63() V65( {} ) FinSequence-like FinSequence-membered bounded_below bounded_above real-bounded interval set
((vol a) / (c₆ + 1)) + (- 0) is V11() real ext-real set
abs (((vol a) / (c₆ + 1)) - 0) is V11() real ext-real Element of REAL
x0 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(delta f) . F is V11() real ext-real Element of REAL
(delta f) . x0 is V11() real ext-real Element of REAL
x0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
F + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(vol a) / (F + 1) is V11() real ext-real Element of REAL
(F + 1) " is non empty V11() real ext-real positive non negative set
(vol a) * ((F + 1) ") is V11() real ext-real set
(vol a) / (x0 + 1) is V11() real ext-real Element of REAL
(x0 + 1) " is non empty V11() real ext-real positive non negative set
(vol a) * ((x0 + 1) ") is V11() real ext-real set
x0 is V11() real ext-real set
F is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(delta f) . F is V11() real ext-real Element of REAL
((delta f) . F) - 0 is V11() real ext-real Element of REAL
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued functional integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V45() V46() V47() V48() V49() V50() V51() V58() V59() V62() V63() V65( {} ) FinSequence-like FinSequence-membered bounded_below bounded_above real-bounded interval set
((delta f) . F) + (- 0) is V11() real ext-real set
abs (((delta f) . F) - 0) is V11() real ext-real Element of REAL
f . F is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
delta (f . F) is V11() real ext-real Element of REAL
chi (a,a) is Relation-like a -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
K7(a,REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(a,REAL)) is V2() V58() set
upper_volume ((chi (a,a)),(f . F)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
rng (upper_volume ((chi (a,a)),(f . F))) is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
sup (rng (upper_volume ((chi (a,a)),(f . F)))) is V11() real ext-real set
c₆ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(delta f) . c₆ is V11() real ext-real Element of REAL
f . c₆ is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
delta (f . c₆) is V11() real ext-real Element of REAL
upper_volume ((chi (a,a)),(f . c₆)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
rng (upper_volume ((chi (a,a)),(f . c₆))) is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
sup (rng (upper_volume ((chi (a,a)),(f . c₆)))) is V11() real ext-real set
((delta f) . c₆) - 0 is V11() real ext-real Element of REAL
((delta f) . c₆) + (- 0) is V11() real ext-real set
abs (((delta f) . c₆) - 0) is V11() real ext-real Element of REAL
lim (delta f) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
f is V11() real ext-real set
['a,f'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
['f,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
x0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom x0 is set
x0 | ['a,b