REAL is non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V50() V56() V57() set
RAT is non empty V50() V51() V52() V53() V56() V57() set
INT is non empty V50() V51() V52() V53() V54() V56() V57() set
omega is non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below set
K19(omega) is set
K19(NAT) is set
K20(COMPLEX,COMPLEX) is complex-valued set
K19(K20(COMPLEX,COMPLEX)) is set
K20(COMPLEX,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(COMPLEX,REAL)) is set
K20(REAL,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(REAL,REAL)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is complex-valued set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(K20(REAL,REAL),REAL) is complex-valued ext-real-valued real-valued set
K19(K20(K20(REAL,REAL),REAL)) is set
K20(RAT,RAT) is RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(K20(RAT,RAT),RAT)) is set
K20(INT,INT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K20(K20(NAT,NAT),NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(K20(NAT,NAT),NAT)) is set
{} is set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V50() V51() V52() V53() V54() V55() V56() bounded_below V71() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V50() V51() V52() V53() V54() V55() V56() bounded_below V71() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT
K20(NAT,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(NAT,REAL)) is set
0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
K19(K20(NAT,NAT)) is set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT
ExtREAL is non empty V51() V71() set
g is V30() real ext-real set
s is V30() real ext-real set
[.g,s.] is V71() set
{ b1 where b1 is ext-real Element of ExtREAL : ( g <= b1 & b1 <= s ) } is set
Y is set
X is ext-real Element of ExtREAL
{ b1 where b1 is V30() real ext-real Element of REAL : ( g <= b1 & b1 <= s ) } is set
X is V50() V51() V52() Element of K19(REAL)
e is set
r is ext-real Element of ExtREAL
e is set
r is V30() real ext-real Element of REAL
g is ext-real set
s is ext-real set
].g,s.[ is non left_end non right_end V71() set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= g & not s <= b1 ) } is set
Y is set
X is ext-real Element of ExtREAL
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= g & not s <= b1 ) } is set
X is V50() V51() V52() Element of K19(REAL)
e is set
r is V30() real ext-real Element of REAL
e is set
r is ext-real Element of ExtREAL
g is V30() real ext-real set
s is V30() real ext-real set
g - s is V30() real ext-real set
abs (g - s) is V30() real ext-real Element of REAL
Y is V30() real ext-real set
s - Y is V30() real ext-real set
s + Y is V30() real ext-real set
((s - Y),(s + Y)) is V50() V51() V52() non left_end non right_end V71() Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s - Y & not s + Y <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= s - Y & not s + Y <= b1 ) } is set
- Y is V30() real ext-real set
s + (- Y) is V30() real ext-real set
X is V30() real ext-real Element of REAL
X is V30() real ext-real Element of REAL
- Y is V30() real ext-real set
s + (- Y) is V30() real ext-real set
g is V30() real ext-real set
2 * g is V30() real ext-real Element of REAL
s is V30() real ext-real set
Y is V30() real ext-real set
(s,Y) is V50() V51() V52() V71() Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= Y ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( s <= b1 & b1 <= Y ) } is set
s + Y is V30() real ext-real set
(s + Y) - (2 * g) is V30() real ext-real Element of REAL
abs ((s + Y) - (2 * g)) is V30() real ext-real Element of REAL
Y - s is V30() real ext-real set
2 * Y is V30() real ext-real Element of REAL
X is V30() real ext-real Element of REAL
- (2 * Y) is V30() real ext-real Element of REAL
- (2 * g) is V30() real ext-real Element of REAL
(s + Y) + (- (2 * Y)) is V30() real ext-real Element of REAL
(s + Y) + (- (2 * g)) is V30() real ext-real Element of REAL
- (Y - s) is V30() real ext-real set
2 * s is V30() real ext-real Element of REAL
X is V30() real ext-real Element of REAL
- (2 * s) is V30() real ext-real Element of REAL
(s + Y) + (- (2 * s)) is V30() real ext-real Element of REAL
- (Y - s) is V30() real ext-real set
s - Y is V30() real ext-real set
(s - Y) + (2 * g) is V30() real ext-real Element of REAL
(s + Y) - (s - Y) is V30() real ext-real set
1 / 2 is V30() real ext-real non negative Element of REAL
(1 / 2) * (2 * g) is V30() real ext-real Element of REAL
2 * Y is V30() real ext-real Element of REAL
(1 / 2) * (2 * Y) is V30() real ext-real Element of REAL
(2 * g) + (Y - s) is V30() real ext-real Element of REAL
(s + Y) - (Y - s) is V30() real ext-real set
2 * s is V30() real ext-real Element of REAL
(1 / 2) * (2 * s) is V30() real ext-real Element of REAL
g is V30() real ext-real set
2 * g is V30() real ext-real Element of REAL
s is V30() real ext-real set
Y is V30() real ext-real set
(s,Y) is V50() V51() V52() non left_end non right_end V71() Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not Y <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= s & not Y <= b1 ) } is set
Y - s is V30() real ext-real set
s + Y is V30() real ext-real set
(s + Y) - (2 * g) is V30() real ext-real Element of REAL
abs ((s + Y) - (2 * g)) is V30() real ext-real Element of REAL
2 * Y is V30() real ext-real Element of REAL
X is V30() real ext-real Element of REAL
- (2 * g) is V30() real ext-real Element of REAL
- (2 * Y) is V30() real ext-real Element of REAL
(s + Y) + (- (2 * g)) is V30() real ext-real Element of REAL
(s + Y) + (- (2 * Y)) is V30() real ext-real Element of REAL
- (Y - s) is V30() real ext-real set
2 * s is V30() real ext-real Element of REAL
X is V30() real ext-real Element of REAL
- (2 * s) is V30() real ext-real Element of REAL
(s + Y) + (- (2 * s)) is V30() real ext-real Element of REAL
- (Y - s) is V30() real ext-real set
s - Y is V30() real ext-real set
(s - Y) + (2 * g) is V30() real ext-real Element of REAL
(s + Y) - (s - Y) is V30() real ext-real set
1 / 2 is V30() real ext-real non negative Element of REAL
2 * Y is V30() real ext-real Element of REAL
(1 / 2) * (2 * Y) is V30() real ext-real Element of REAL
(1 / 2) * (2 * g) is V30() real ext-real Element of REAL
(2 * g) + (Y - s) is V30() real ext-real Element of REAL
(s + Y) - (Y - s) is V30() real ext-real set
2 * s is V30() real ext-real Element of REAL
(1 / 2) * (2 * s) is V30() real ext-real Element of REAL
g is V30() real ext-real set
s is V30() real ext-real set
(g,s) is V50() V51() V52() V71() Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( g <= b1 & b1 <= s ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( g <= b1 & b1 <= s ) } is set
Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng Y is V50() V51() V52() set
s + 1 is V30() real ext-real Element of REAL
X is V30() real ext-real Element of REAL
e is V30() real ext-real set
r is V30() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
Y . e is V30() real ext-real Element of REAL
dom Y is set
e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
Y . e is V30() real ext-real Element of REAL
g - 1 is V30() real ext-real Element of REAL
X is V30() real ext-real Element of REAL
X + 1 is V30() real ext-real Element of REAL
1 - 1 is V30() real ext-real Element of REAL
g - (1 - 1) is V30() real ext-real Element of REAL
e is V30() real ext-real set
r is V30() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
Y . e is V30() real ext-real Element of REAL
dom Y is set
e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
Y . e is V30() real ext-real Element of REAL
g is V30() real ext-real set
s is V30() real ext-real set
(g,s) is V50() V51() V52() V71() Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( g <= b1 & b1 <= s ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( g <= b1 & b1 <= s ) } is set
Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng Y is V50() V51() V52() set
lim Y is V30() real ext-real Element of REAL
NAT --> g is Relation-like NAT -defined {g} -valued V6() constant non empty V14( NAT ) V18( NAT ,{g}) T-Sequence-like complex-valued ext-real-valued real-valued Element of K19(K20(NAT,{g}))
{g} is V50() V51() V52() set
K20(NAT,{g}) is complex-valued ext-real-valued real-valued set
K19(K20(NAT,{g})) is set
e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
dom Y is set
Y . e is V30() real ext-real Element of REAL
X is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
X . e is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
X . 0 is V30() real ext-real Element of REAL
lim X is V30() real ext-real Element of REAL
NAT --> s is Relation-like NAT -defined {s} -valued V6() constant non empty V14( NAT ) V18( NAT ,{s}) T-Sequence-like complex-valued ext-real-valued real-valued Element of K19(K20(NAT,{s}))
{s} is V50() V51() V52() set
K20(NAT,{s}) is complex-valued ext-real-valued real-valued set
K19(K20(NAT,{s})) is set
e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
dom Y is set
Y . e is V30() real ext-real Element of REAL
X is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
X . e is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
X . 0 is V30() real ext-real Element of REAL
lim X is V30() real ext-real Element of REAL
g is V30() real ext-real set
s is V30() real ext-real set
(g,s) is V50() V51() V52() V71() Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( g <= b1 & b1 <= s ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( g <= b1 & b1 <= s ) } is set
Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng Y is V50() V51() V52() set
X is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim X is V30() real ext-real Element of REAL
rng X is V50() V51() V52() set
e is Relation-like NAT -defined NAT -valued V6() non empty V14( NAT ) V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
Y * e is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of Y
g is V30() real ext-real set
s is V30() real ext-real set
(g,s) is V50() V51() V52() non left_end non right_end V71() Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= g & not s <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= g & not s <= b1 ) } is set
Y is V50() V51() V52() Element of K19(REAL)
X is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng X is V50() V51() V52() set
lim X is V30() real ext-real Element of REAL
(lim X) - g is V30() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
s - (lim X) is V30() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
max (r,e) is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative set
g1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
X . g1 is V30() real ext-real Element of REAL
(X . g1) - (lim X) is V30() real ext-real Element of REAL
abs ((X . g1) - (lim X)) is V30() real ext-real Element of REAL
- (abs ((X . g1) - (lim X))) is V30() real ext-real Element of REAL
- ((X . g1) - (lim X)) is V30() real ext-real Element of REAL
- (- (abs ((X . g1) - (lim X)))) is V30() real ext-real Element of REAL
- (- ((X . g1) - (lim X))) is V30() real ext-real Element of REAL
- ((lim X) - g) is V30() real ext-real Element of REAL
g - (lim X) is V30() real ext-real Element of REAL
dom X is set
X is V30() real ext-real set
(g,s) ` is V50() V51() V52() Element of K19(REAL)
REAL \ (g,s) is V50() V51() V52() set
X is V30() real ext-real set
e is V30() real ext-real Element of REAL
g is V30() real ext-real set
s is V30() real ext-real set
(g,s) is V50() V51() V52() non left_end non right_end V71() Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= g & not s <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= g & not s <= b1 ) } is set
Y is V50() V51() V52() Element of K19(REAL)
(g,s) is V50() V51() V52() V71() Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( g <= b1 & b1 <= s ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( g <= b1 & b1 <= s ) } is set
Y is V50() V51() V52() Element of K19(REAL)
g is V50() V51() V52() Element of K19(REAL)
s is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V50() V51() V52() set
lim s is V30() real ext-real Element of REAL
Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim Y is V30() real ext-real Element of REAL
g is V50() V51() V52() Element of K19(REAL)
g is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V50() V51() V52() Element of K19(REAL)
Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim Y is V30() real ext-real Element of REAL
Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim Y is V30() real ext-real Element of REAL
X is V30() real ext-real set
e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
g1 is Relation-like NAT -defined NAT -valued V6() non empty V14( NAT ) V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
g * g1 is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of g
e + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT
(e + 1) + r is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT
(g * g1) . ((e + 1) + r) is V30() real ext-real Element of REAL
((g * g1) . ((e + 1) + r)) - (lim Y) is V30() real ext-real Element of REAL
abs (((g * g1) . ((e + 1) + r)) - (lim Y)) is V30() real ext-real Element of REAL
g1 . ((e + 1) + r) is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
g . (g1 . ((e + 1) + r)) is V30() real ext-real Element of REAL
(g . (g1 . ((e + 1) + r))) - (lim Y) is V30() real ext-real Element of REAL
abs ((g . (g1 . ((e + 1) + r))) - (lim Y)) is V30() real ext-real Element of REAL
g is V50() V51() V52() Element of K19(REAL)
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
Y is ext-real set
s is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Y is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
s . Y is V30() real ext-real Element of REAL
X is V30() real ext-real set
Y is V30() real ext-real set
X is V30() real ext-real set
e is V30() real ext-real set
Y + 1 is V30() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
g1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
s . g2 is V30() real ext-real Element of REAL
(s . g2) - Y is V30() real ext-real Element of REAL
abs ((s . g2) - Y) is V30() real ext-real Element of REAL
rng s is V50() V51() V52() set
Y is set
dom s is set
X is set
s . X is V30() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
s . e is V30() real ext-real Element of REAL
Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim Y is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
- s is V30() real ext-real non positive Element of REAL
Y is ext-real set
s is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Y is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
s . Y is V30() real ext-real Element of REAL
- Y is V30() real ext-real non positive Element of REAL
X is V30() real ext-real set
Y is V30() real ext-real set
X is V30() real ext-real set
e is V30() real ext-real set
Y - 1 is V30() real ext-real Element of REAL
abs (Y - 1) is V30() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
g1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
s . g2 is V30() real ext-real Element of REAL
(s . g2) - Y is V30() real ext-real Element of REAL
abs ((s . g2) - Y) is V30() real ext-real Element of REAL
- g1 is V30() real ext-real non positive Element of REAL
- g2 is V30() real ext-real non positive Element of REAL
- r is V30() real ext-real non positive Element of REAL
(s . g2) + 1 is V30() real ext-real Element of REAL
Y - (s . g2) is V30() real ext-real Element of REAL
- ((s . g2) - Y) is V30() real ext-real Element of REAL
abs (- ((s . g2) - Y)) is V30() real ext-real Element of REAL
rng s is V50() V51() V52() set
Y is set
dom s is set
X is set
s . X is V30() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
s . e is V30() real ext-real Element of REAL
Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim Y is V30() real ext-real Element of REAL
g is V50() V51() V52() Element of K19(REAL)
s is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V50() V51() V52() set
Y is V30() real ext-real set
X is V30() real ext-real set
Y - 1 is V30() real ext-real Element of REAL
X is V30() real ext-real Element of REAL
X + 1 is V30() real ext-real Element of REAL
1 - 1 is V30() real ext-real Element of REAL
Y - (1 - 1) is V30() real ext-real Element of REAL
e is V30() real ext-real set
e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
s . e is V30() real ext-real Element of REAL
dom s is set
e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
s . e is V30() real ext-real Element of REAL
Y is V30() real ext-real set
X is V30() real ext-real set
Y + 1 is V30() real ext-real Element of REAL
X is V30() real ext-real Element of REAL
e is V30() real ext-real set
e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
s . e is V30() real ext-real Element of REAL
dom s is set
e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
s . e is V30() real ext-real Element of REAL
Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng Y is V50() V51() V52() set
X is Relation-like NAT -defined NAT -valued V6() non empty V14( NAT ) V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
s * X is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s
lim Y is V30() real ext-real Element of REAL
g is V50() V51() V52() Element of K19(REAL)
upper_bound g is V30() real ext-real Element of REAL
Y is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
Y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT
1 / (Y + 1) is V30() real ext-real non negative Element of REAL
(Y + 1) " is non empty V30() real ext-real positive non negative Element of REAL
(upper_bound g) - (1 / (Y + 1)) is V30() real ext-real Element of REAL
X is V30() real ext-real set
X + (1 / (Y + 1)) is V30() real ext-real Element of REAL
(upper_bound g) - X is V30() real ext-real Element of REAL
Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
X is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
Y . X is V30() real ext-real Element of REAL
X + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT
1 / (X + 1) is V30() real ext-real non negative Element of REAL
(upper_bound g) - (Y . X) is V30() real ext-real Element of REAL
e is V30() real ext-real set
(upper_bound g) - e is V30() real ext-real Element of REAL
rng Y is V50() V51() V52() set
X is set
dom Y is set
e is set
Y . e is V30() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
Y . r is V30() real ext-real Element of REAL
X is V30() real ext-real set
X " is V30() real ext-real set
e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
g1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT
g1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT
1 / (g1 + 1) is V30() real ext-real non negative Element of REAL
1 / (r + 1) is V30() real ext-real non negative Element of REAL
Y . g1 is V30() real ext-real Element of REAL
(upper_bound g) - (Y . g1) is V30() real ext-real Element of REAL
e + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT
(X ") + 0 is V30() real ext-real Element of REAL
1 / (X ") is V30() real ext-real Element of REAL
1 / (e + 1) is V30() real ext-real non negative Element of REAL
(Y . g1) - (upper_bound g) is V30() real ext-real Element of REAL
- ((Y . g1) - (upper_bound g)) is V30() real ext-real Element of REAL
abs (- ((Y . g1) - (upper_bound g))) is V30() real ext-real Element of REAL
abs ((Y . g1) - (upper_bound g)) is V30() real ext-real Element of REAL
lim Y is V30() real ext-real Element of REAL
g is V50() V51() V52() Element of K19(REAL)
lower_bound g is V30() real ext-real Element of REAL
Y is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
Y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT
1 / (Y + 1) is V30() real ext-real non negative Element of REAL
(Y + 1) " is non empty V30() real ext-real positive non negative Element of REAL
(lower_bound g) + (1 / (Y + 1)) is V30() real ext-real Element of REAL
X is V30() real ext-real set
X - (lower_bound g) is V30() real ext-real Element of REAL
Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
X is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
Y . X is V30() real ext-real Element of REAL
X + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT
1 / (X + 1) is V30() real ext-real non negative Element of REAL
(Y . X) - (lower_bound g) is V30() real ext-real Element of REAL
e is V30() real ext-real set
e - (lower_bound g) is V30() real ext-real Element of REAL
rng Y is V50() V51() V52() set
X is set
dom Y is set
e is set
Y . e is V30() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
Y . r is V30() real ext-real Element of REAL
X is V30() real ext-real set
X " is V30() real ext-real set
e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
g1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT
g1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT
1 / (g1 + 1) is V30() real ext-real non negative Element of REAL
1 / (r + 1) is V30() real ext-real non negative Element of REAL
Y . g1 is V30() real ext-real Element of REAL
(Y . g1) - (lower_bound g) is V30() real ext-real Element of REAL
e + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT
(X ") + 0 is V30() real ext-real Element of REAL
1 / (X ") is V30() real ext-real Element of REAL
1 / (e + 1) is V30() real ext-real non negative Element of REAL
abs ((Y . g1) - (lower_bound g)) is V30() real ext-real Element of REAL
lim Y is V30() real ext-real Element of REAL
g is V50() V51() V52() Element of K19(REAL)
upper_bound g is V30() real ext-real Element of REAL
lower_bound g is V30() real ext-real Element of REAL
g is V50() V51() V52() Element of K19(REAL)
(1,0) is V50() V51() V52() V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( 1 <= b1 & b1 <= 0 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( 1 <= b1 & b1 <= 0 ) } is set
lower_bound g is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
upper_bound g is V30() real ext-real Element of REAL
Y is V30() real ext-real Element of REAL
(s,Y) is V50() V51() V52() V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= Y ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( s <= b1 & b1 <= Y ) } is set
X is V30() real ext-real Element of REAL
(0,1) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= 0 & not 1 <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= 0 & not 1 <= b1 ) } is set
g is V30() real ext-real set
g - 1 is V30() real ext-real Element of REAL
g + 1 is V30() real ext-real Element of REAL
((g - 1),(g + 1)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= g - 1 & not g + 1 <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= g - 1 & not g + 1 <= b1 ) } is set
g is V30() real ext-real set
s is V50() V51() V52() (g)
Y is V30() real ext-real set
g - Y is V30() real ext-real set
g + Y is V30() real ext-real set
((g - Y),(g + Y)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= g - Y & not g + Y <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= g - Y & not g + Y <= b1 ) } is set
g is V30() real ext-real set
s is V50() V51() V52() () (g)
g - g is V30() real ext-real set
abs (g - g) is V30() real ext-real Element of REAL
Y is V30() real ext-real set
g - Y is V30() real ext-real set
g + Y is V30() real ext-real set
((g - Y),(g + Y)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= g - Y & not g + Y <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= g - Y & not g + Y <= b1 ) } is set
g is V30() real ext-real set
s is V50() V51() V52() () (g)
Y is V50() V51() V52() () (g)
X is V30() real ext-real set
g - X is V30() real ext-real set
g + X is V30() real ext-real set
((g - X),(g + X)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= g - X & not g + X <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= g - X & not g + X <= b1 ) } is set
e is V30() real ext-real set
g - e is V30() real ext-real set
g + e is V30() real ext-real set
((g - e),(g + e)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= g - e & not g + e <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= g - e & not g + e <= b1 ) } is set
min (X,e) is V30() real ext-real set
g - (min (X,e)) is V30() real ext-real set
g + (min (X,e)) is V30() real ext-real set
((g - (min (X,e))),(g + (min (X,e)))) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= g - (min (X,e)) & not g + (min (X,e)) <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= g - (min (X,e)) & not g + (min (X,e)) <= b1 ) } is set
g1 is V50() V51() V52() () (g)
- X is V30() real ext-real set
- (min (X,e)) is V30() real ext-real set
g + (- X) is V30() real ext-real set
g + (- (min (X,e))) is V30() real ext-real set
- e is V30() real ext-real set
g + (- e) is V30() real ext-real set
g2 is set
m is V30() real ext-real Element of REAL
c10 is V30() real ext-real Element of REAL
g2 is set
m is V30() real ext-real Element of REAL
c10 is V30() real ext-real Element of REAL
g is V50() V51() V52() () Element of K19(REAL)
s is V30() real ext-real set
g ` is V50() V51() V52() Element of K19(REAL)
REAL \ g is V50() V51() V52() set
Y is V50() V51() V52() () (s)
X is V30() real ext-real set
s - X is V30() real ext-real set
s + X is V30() real ext-real set
((s - X),(s + X)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s - X & not s + X <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= s - X & not s + X <= b1 ) } is set
e is set
r is V30() real ext-real Element of REAL
g1 is V30() real ext-real Element of REAL
Y is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
Y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT
1 / (Y + 1) is V30() real ext-real non negative Element of REAL
s - (1 / (Y + 1)) is V30() real ext-real Element of REAL
s + (1 / (Y + 1)) is V30() real ext-real Element of REAL
((s - (1 / (Y + 1))),(s + (1 / (Y + 1)))) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s - (1 / (Y + 1)) & not s + (1 / (Y + 1)) <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= s - (1 / (Y + 1)) & not s + (1 / (Y + 1)) <= b1 ) } is set
(Y + 1) " is non empty V30() real ext-real positive non negative Element of REAL
1 * ((Y + 1) ") is V30() real ext-real non negative Element of REAL
X is V50() V51() V52() () (s)
e is V30() real ext-real Element of REAL
Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
X is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
e is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
X . r is V30() real ext-real Element of REAL
Y . r is V30() real ext-real Element of REAL
e . r is V30() real ext-real Element of REAL
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT
1 / (r + 1) is V30() real ext-real non negative Element of REAL
s - (1 / (r + 1)) is V30() real ext-real Element of REAL
s + (1 / (r + 1)) is V30() real ext-real Element of REAL
((s - (1 / (r + 1))),(s + (1 / (r + 1)))) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s - (1 / (r + 1)) & not s + (1 / (r + 1)) <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= s - (1 / (r + 1)) & not s + (1 / (r + 1)) <= b1 ) } is set
g1 is V30() real ext-real Element of REAL
g1 is V30() real ext-real Element of REAL
rng Y is V50() V51() V52() set
r is set
dom Y is set
g1 is set
Y . g1 is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
Y . g2 is V30() real ext-real Element of REAL
r is V30() real ext-real set
r " is V30() real ext-real set
g1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
g2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT
1 / (m + 1) is V30() real ext-real non negative Element of REAL
1 / (g2 + 1) is V30() real ext-real non negative Element of REAL
(r ") + 0 is V30() real ext-real Element of REAL
1 / (r ") is V30() real ext-real Element of REAL
e . m is V30() real ext-real Element of REAL
(e . m) - s is V30() real ext-real Element of REAL
abs ((e . m) - s) is V30() real ext-real Element of REAL
s + (1 / (m + 1)) is V30() real ext-real Element of REAL
(s + (1 / (m + 1))) - s is V30() real ext-real Element of REAL
abs ((s + (1 / (m + 1))) - s) is V30() real ext-real Element of REAL
lim e is V30() real ext-real Element of REAL
r is V30() real ext-real set
r " is V30() real ext-real set
g1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
g2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT
1 / (m + 1) is V30() real ext-real non negative Element of REAL
1 / (g2 + 1) is V30() real ext-real non negative Element of REAL
(r ") + 0 is V30() real ext-real Element of REAL
1 / (r ") is V30() real ext-real Element of REAL
X . m is V30() real ext-real Element of REAL
(X . m) - s is V30() real ext-real Element of REAL
abs ((X . m) - s) is V30() real ext-real Element of REAL
s - (1 / (m + 1)) is V30() real ext-real Element of REAL
(s - (1 / (m + 1))) - s is V30() real ext-real Element of REAL
abs ((s - (1 / (m + 1))) - s) is V30() real ext-real Element of REAL
- (1 / (m + 1)) is V30() real ext-real non positive Element of REAL
abs (- (1 / (m + 1))) is V30() real ext-real Element of REAL
abs (1 / (m + 1)) is V30() real ext-real Element of REAL
lim X is V30() real ext-real Element of REAL
lim Y is V30() real ext-real Element of REAL
g is V50() V51() V52() () Element of K19(REAL)
s is V30() real ext-real set
Y is V50() V51() V52() () (s)
X is V30() real ext-real set
s - X is V30() real ext-real set
s + X is V30() real ext-real set
((s - X),(s + X)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s - X & not s + X <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= s - X & not s + X <= b1 ) } is set
g is V50() V51() V52() Element of K19(REAL)
g ` is V50() V51() V52() Element of K19(REAL)
REAL \ g is V50() V51() V52() set
s is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V50() V51() V52() set
lim s is V30() real ext-real Element of REAL
Y is V50() V51() V52() () ( lim s)
X is V30() real ext-real set
(lim s) - X is V30() real ext-real Element of REAL
(lim s) + X is V30() real ext-real Element of REAL
(((lim s) - X),((lim s) + X)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= (lim s) - X & not (lim s) + X <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= (lim s) - X & not (lim s) + X <= b1 ) } is set
e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
dom s is set
s . e is V30() real ext-real Element of REAL
(s . e) - (lim s) is V30() real ext-real Element of REAL
abs ((s . e) - (lim s)) is V30() real ext-real Element of REAL
- X is V30() real ext-real set
(lim s) + ((s . e) - (lim s)) is V30() real ext-real Element of REAL
(lim s) + (- X) is V30() real ext-real Element of REAL
g is V50() V51() V52() Element of K19(REAL)
upper_bound g is V30() real ext-real Element of REAL
s is V50() V51() V52() () ( upper_bound g)
Y is V30() real ext-real set
(upper_bound g) - Y is V30() real ext-real Element of REAL
(upper_bound g) + Y is V30() real ext-real Element of REAL
(((upper_bound g) - Y),((upper_bound g) + Y)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= (upper_bound g) - Y & not (upper_bound g) + Y <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= (upper_bound g) - Y & not (upper_bound g) + Y <= b1 ) } is set
Y / 2 is V30() real ext-real Element of REAL
(upper_bound g) + (Y / 2) is V30() real ext-real Element of REAL
((upper_bound g) + (Y / 2)) + (Y / 2) is V30() real ext-real Element of REAL
g is V50() V51() V52() Element of K19(REAL)
lower_bound g is V30() real ext-real Element of REAL
s is V50() V51() V52() () ( lower_bound g)
Y is V30() real ext-real set
(lower_bound g) - Y is V30() real ext-real Element of REAL
(lower_bound g) + Y is V30() real ext-real Element of REAL
(((lower_bound g) - Y),((lower_bound g) + Y)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= (lower_bound g) - Y & not (lower_bound g) + Y <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= (lower_bound g) - Y & not (lower_bound g) + Y <= b1 ) } is set
Y / 2 is V30() real ext-real Element of REAL
(lower_bound g) - (Y / 2) is V30() real ext-real Element of REAL
((lower_bound g) - (Y / 2)) - (Y / 2) is V30() real ext-real Element of REAL
g is V50() V51() V52() Element of K19(REAL)
(1,0) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= 1 & not 0 <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= 1 & not 0 <= b1 ) } is set
lower_bound g is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
upper_bound g is V30() real ext-real Element of REAL
Y is V30() real ext-real Element of REAL
(s,Y) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not Y <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= s & not Y <= b1 ) } is set
X is V30() real ext-real Element of REAL
Y - X is V30() real ext-real Element of REAL
e is V30() real ext-real Element of REAL
Y - (Y - X) is V30() real ext-real Element of REAL
e is V30() real ext-real set
X - s is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s + (X - s) is V30() real ext-real Element of REAL
r is V30() real ext-real set
g1 is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : ( g1 <= b1 & b1 <= g2 ) } is set
(g1,g2) is V50() V51() V52() V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( g1 <= b1 & b1 <= g2 ) } is set
g is V30() real ext-real set
s is ext-real set
[.g,s.[ is non right_end V71() set
{ b1 where b1 is ext-real Element of ExtREAL : ( g <= b1 & not s <= b1 ) } is set
Y is set
X is ext-real Element of ExtREAL
{ b1 where b1 is V30() real ext-real Element of REAL : ( g <= b1 & not s <= b1 ) } is set
X is V50() V51() V52() Element of K19(REAL)
e is set
r is ext-real Element of ExtREAL
e is set
r is V30() real ext-real Element of REAL
g is ext-real set
s is V30() real ext-real set
].g,s.] is non left_end V71() set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= g & b1 <= s ) } is set
Y is set
X is ext-real Element of ExtREAL
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= g & b1 <= s ) } is set
X is V50() V51() V52() Element of K19(REAL)
e is set
r is ext-real Element of ExtREAL
e is set
r is V30() real ext-real Element of REAL