:: RINFSUP2 semantic presentation

REAL is non empty V33() V44() V45() V46() V50() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V44() V45() V46() V47() V48() V49() V50() Element of K6(REAL)
K6(REAL) is non empty set
ExtREAL is non empty V45() set
K7(NAT,ExtREAL) is non empty ext-real-valued set
K6(K7(NAT,ExtREAL)) is non empty set
K6(ExtREAL) is non empty set
omega is non empty epsilon-transitive epsilon-connected ordinal V44() V45() V46() V47() V48() V49() V50() set
K6(omega) is non empty set
K6(NAT) is non empty set
COMPLEX is non empty V33() V44() V50() set
RAT is non empty V33() V44() V45() V46() V47() V50() set
INT is non empty V33() V44() V45() V46() V47() V48() V50() set
K7(NAT,REAL) is non empty complex-valued ext-real-valued real-valued set
K6(K7(NAT,REAL)) is non empty set
K6(K6(REAL)) is non empty set
K6(RAT) is non empty set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real V44() V45() V46() V47() V48() V49() V50() V66() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
{{},1} is non empty V44() V45() V46() V47() V48() V49() set
K7(COMPLEX,COMPLEX) is non empty complex-valued set
K6(K7(COMPLEX,COMPLEX)) is non empty set
K7(COMPLEX,REAL) is non empty complex-valued ext-real-valued real-valued set
K6(K7(COMPLEX,REAL)) is non empty set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is non empty complex-valued set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is non empty set
K7(REAL,REAL) is non empty complex-valued ext-real-valued real-valued set
K6(K7(REAL,REAL)) is non empty set
K7(K7(REAL,REAL),REAL) is non empty complex-valued ext-real-valued real-valued set
K6(K7(K7(REAL,REAL),REAL)) is non empty set
K7(RAT,RAT) is non empty V20( RAT ) complex-valued ext-real-valued real-valued set
K6(K7(RAT,RAT)) is non empty set
K7(K7(RAT,RAT),RAT) is non empty V20( RAT ) complex-valued ext-real-valued real-valued set
K6(K7(K7(RAT,RAT),RAT)) is non empty set
K7(INT,INT) is non empty V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued set
K6(K7(INT,INT)) is non empty set
K7(K7(INT,INT),INT) is non empty V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued set
K6(K7(K7(INT,INT),INT)) is non empty set
K7(NAT,NAT) is non empty V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K7(K7(NAT,NAT),NAT) is non empty V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K6(K7(K7(NAT,NAT),NAT)) is non empty set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real V44() V45() V46() V47() V48() V49() V50() V66() V67() Element of NAT
+infty is non real set
-infty is non real set
+infty is non real ext-real Element of ExtREAL
-infty is non real ext-real Element of ExtREAL
{-infty} is non empty set
{+infty} is non empty set
seq is non empty V45() Element of K6(ExtREAL)
sup seq is ext-real Element of ExtREAL
a is non empty V44() V45() V46() Element of K6(REAL)
upper_bound a is V11() real ext-real Element of REAL
iseq is V11() real ext-real set
{-infty} is non empty V45() set
iseq is ext-real set
seq is non empty V45() Element of K6(ExtREAL)
a is non empty V44() V45() V46() Element of K6(REAL)
sup seq is ext-real Element of ExtREAL
upper_bound a is V11() real ext-real Element of REAL
seq is non empty V45() Element of K6(ExtREAL)
inf seq is ext-real Element of ExtREAL
a is non empty V44() V45() V46() Element of K6(REAL)
lower_bound a is V11() real ext-real Element of REAL
iseq is V11() real ext-real set
{+infty} is non empty V45() set
iseq is ext-real set
seq is non empty V45() Element of K6(ExtREAL)
a is non empty V44() V45() V46() Element of K6(REAL)
inf seq is ext-real Element of ExtREAL
lower_bound a is V11() real ext-real Element of REAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
rng seq is non empty V45() V81() Element of K6(ExtREAL)
sup (rng seq) is ext-real Element of ExtREAL
inf (rng seq) is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
{ (seq . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : a <= b₁ } is set
{ H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : S₁[b₁] } is set
seq . a is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
{ (seq . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : a₁ <= b₁ } is set
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
{ (seq . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : a <= b₁ } is set
iseq is non empty V45() Element of K6(ExtREAL)
inf iseq is ext-real Element of ExtREAL
g is ext-real Element of ExtREAL
a is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
iseq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
g is set
a . g is ext-real Element of ExtREAL
iseq . g is ext-real Element of ExtREAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
{ (seq . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : N <= b₁ } is set
iseq . N is ext-real Element of ExtREAL
a . N is ext-real Element of ExtREAL
m is non empty V45() Element of K6(ExtREAL)
inf m is ext-real Element of ExtREAL
Y is non empty V45() Element of K6(ExtREAL)
inf Y is ext-real Element of ExtREAL
dom iseq is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
dom a is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
{ (seq . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : a₁ <= b₁ } is set
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
{ (seq . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : a <= b₁ } is set
iseq is non empty V45() Element of K6(ExtREAL)
sup iseq is ext-real Element of ExtREAL
g is ext-real Element of ExtREAL
a is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
iseq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
g is set
a . g is ext-real Element of ExtREAL
iseq . g is ext-real Element of ExtREAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
{ (seq . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : N <= b₁ } is set
iseq . N is ext-real Element of ExtREAL
a . N is ext-real Element of ExtREAL
m is non empty V45() Element of K6(ExtREAL)
sup m is ext-real Element of ExtREAL
Y is non empty V45() Element of K6(ExtREAL)
sup Y is ext-real Element of ExtREAL
dom iseq is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
dom a is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
rng seq is non empty V45() V81() Element of K6(ExtREAL)
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
dom seq is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
a is ext-real set
K86(seq) is set
K68(seq,a) is ext-real set
iseq is ext-real set
K68(seq,iseq) is ext-real set
a is ext-real set
K86(seq) is set
K68(seq,a) is ext-real set
iseq is ext-real set
K68(seq,iseq) is ext-real set
a is ext-real set
K86(seq) is set
K68(seq,a) is ext-real set
iseq is ext-real set
K68(seq,iseq) is ext-real set
a is ext-real set
K86(seq) is set
K68(seq,a) is ext-real set
iseq is ext-real set
K68(seq,iseq) is ext-real set
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
iseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . a is ext-real Element of ExtREAL
seq . iseq is ext-real Element of ExtREAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . N is ext-real Element of ExtREAL
seq . g is ext-real Element of ExtREAL
Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . Y is ext-real Element of ExtREAL
seq . m is ext-real Element of ExtREAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . x is ext-real Element of ExtREAL
seq . k is ext-real Element of ExtREAL
UB is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
rseq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . rseq2 is ext-real Element of ExtREAL
seq . UB is ext-real Element of ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . n is ext-real Element of ExtREAL
seq . n is ext-real Element of ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
c₁₅ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . c₁₅ is ext-real Element of ExtREAL
seq . n is ext-real Element of ExtREAL
c₁₆ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
c₁₇ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . c₁₆ is ext-real Element of ExtREAL
seq . c₁₇ is ext-real Element of ExtREAL
seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(a) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(a) . seq is ext-real Element of ExtREAL
a . seq is ext-real Element of ExtREAL
(a) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(a) . seq is ext-real Element of ExtREAL
{ (a . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : seq <= b₁ } is set
iseq is non empty V45() Element of K6(ExtREAL)
inf iseq is ext-real Element of ExtREAL
g is non empty V45() Element of K6(ExtREAL)
sup g is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
iseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
{ (seq . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : iseq <= b₁ } is set
(seq) . iseq is ext-real Element of ExtREAL
g is non empty V45() Element of K6(ExtREAL)
sup g is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
{ (seq . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : a <= b₁ } is set
(seq) . a is ext-real Element of ExtREAL
N is non empty V45() Element of K6(ExtREAL)
sup N is ext-real Element of ExtREAL
m is set
Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . Y is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
iseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
{ (seq . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : iseq <= b₁ } is set
(seq) . iseq is ext-real Element of ExtREAL
g is non empty V45() Element of K6(ExtREAL)
inf g is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
{ (seq . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : a <= b₁ } is set
(seq) . a is ext-real Element of ExtREAL
N is non empty V45() Element of K6(ExtREAL)
inf N is ext-real Element of ExtREAL
m is set
Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . Y is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
((seq)) is ext-real Element of ExtREAL
rng (seq) is non empty V45() V81() Element of K6(ExtREAL)
inf (rng (seq)) is ext-real Element of ExtREAL
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
((seq)) is ext-real Element of ExtREAL
rng (seq) is non empty V45() V81() Element of K6(ExtREAL)
sup (rng (seq)) is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
(seq) is ext-real Element of ExtREAL
((seq)) is ext-real Element of ExtREAL
rng (seq) is non empty V45() V81() Element of K6(ExtREAL)
inf (rng (seq)) is ext-real Element of ExtREAL
a is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
superior_realsequence a is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim_sup a is V11() real ext-real Element of REAL
lower_bound (superior_realsequence a) is V11() real ext-real Element of REAL
rng (superior_realsequence a) is V44() V45() V46() Element of K6(REAL)
lower_bound (rng (superior_realsequence a)) is V11() real ext-real Element of REAL
dom (superior_realsequence a) is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
iseq is set
N is set
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
{ (a . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : g <= b₁ } is set
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . m is V11() real ext-real Element of REAL
N is V44() V45() V46() Element of K6(REAL)
{ (seq . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : g <= b₁ } is set
(seq) . g is ext-real Element of ExtREAL
(seq) . iseq is ext-real Element of ExtREAL
upper_bound N is V11() real ext-real Element of REAL
m is non empty V45() Element of K6(ExtREAL)
sup m is ext-real Element of ExtREAL
(superior_realsequence a) . iseq is V11() real ext-real Element of REAL
dom (seq) is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
(seq) is ext-real Element of ExtREAL
((seq)) is ext-real Element of ExtREAL
rng (seq) is non empty V45() V81() Element of K6(ExtREAL)
sup (rng (seq)) is ext-real Element of ExtREAL
a is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
inferior_realsequence a is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim_inf a is V11() real ext-real Element of REAL
upper_bound (inferior_realsequence a) is V11() real ext-real Element of REAL
rng (inferior_realsequence a) is V44() V45() V46() Element of K6(REAL)
upper_bound (rng (inferior_realsequence a)) is V11() real ext-real Element of REAL
dom (inferior_realsequence a) is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
iseq is set
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
{ (seq . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : g <= b₁ } is set
(seq) . g is ext-real Element of ExtREAL
N is non empty V45() Element of K6(ExtREAL)
inf N is ext-real Element of ExtREAL
m is set
{ (a . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : g <= b₁ } is set
Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . Y is V11() real ext-real Element of REAL
m is V44() V45() V46() Element of K6(REAL)
lower_bound m is V11() real ext-real Element of REAL
(seq) . iseq is ext-real Element of ExtREAL
(inferior_realsequence a) . iseq is V11() real ext-real Element of REAL
dom (seq) is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
rng seq is non empty V45() V81() Element of K6(ExtREAL)
a is V11() real ext-real set
iseq is V11() real ext-real set
g is set
seq . g is ext-real Element of ExtREAL
dom seq is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
a is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng a is V44() V45() V46() Element of K6(REAL)
iseq is V11() real ext-real set
g is V11() real ext-real set
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . g is V11() real ext-real Element of REAL
1 + iseq is V11() real ext-real Element of REAL
0 + (a . g) is V11() real ext-real Element of REAL
iseq + 1 is V11() real ext-real Element of REAL
iseq is V11() real ext-real set
g is ext-real set
rng seq is non empty V45() V81() Element of K6(ExtREAL)
dom a is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
N is set
a . N is V11() real ext-real Element of REAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
a is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng a is V44() V45() V46() Element of K6(REAL)
iseq is V11() real ext-real set
g is V11() real ext-real set
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . g is V11() real ext-real Element of REAL
(a . g) - 0 is V11() real ext-real Element of REAL
iseq - 1 is V11() real ext-real Element of REAL
iseq is V11() real ext-real set
g is ext-real set
rng seq is non empty V45() V81() Element of K6(ExtREAL)
dom a is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
N is set
a . N is V11() real ext-real Element of REAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim seq is ext-real Element of ExtREAL
a is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim a is V11() real ext-real Element of REAL
iseq is V11() real ext-real set
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
a . m is V11() real ext-real Element of REAL
(a . m) - (lim a) is V11() real ext-real Element of REAL
seq . m is ext-real Element of ExtREAL
R_EAL (lim a) is ext-real Element of ExtREAL
(seq . m) - (R_EAL (lim a)) is ext-real Element of ExtREAL
K179((R_EAL (lim a))) is ext-real set
K178((seq . m),K179((R_EAL (lim a)))) is ext-real set
abs ((a . m) - (lim a)) is V11() real ext-real Element of REAL
|.((seq . m) - (R_EAL (lim a))).| is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim seq is ext-real Element of ExtREAL
a is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim a is V11() real ext-real Element of REAL
iseq is V11() real ext-real set
g is V11() real ext-real set
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . Y is ext-real Element of ExtREAL
(seq . Y) - (lim seq) is ext-real Element of ExtREAL
K179((lim seq)) is ext-real set
K178((seq . Y),K179((lim seq))) is ext-real set
|.((seq . Y) - (lim seq)).| is ext-real Element of ExtREAL
a . Y is V11() real ext-real Element of REAL
(a . Y) - iseq is V11() real ext-real Element of REAL
abs ((a . Y) - iseq) is V11() real ext-real Element of REAL
seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
a ^\ seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of a
lim a is ext-real Element of ExtREAL
lim (a ^\ seq) is ext-real Element of ExtREAL
g is V11() real ext-real set
g is V11() real ext-real set
N is V11() real ext-real set
m is V11() real ext-real set
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
m + seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
x - seq is V11() real ext-real V66() Element of REAL
(a ^\ seq) . (x - seq) is ext-real Element of ExtREAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
k + seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . (k + seq) is ext-real Element of ExtREAL
(m + seq) - seq is V11() real ext-real V66() Element of REAL
a . x is ext-real Element of ExtREAL
(a . x) - (lim (a ^\ seq)) is ext-real Element of ExtREAL
K179((lim (a ^\ seq))) is ext-real set
K178((a . x),K179((lim (a ^\ seq)))) is ext-real set
|.((a . x) - (lim (a ^\ seq))).| is ext-real Element of ExtREAL
R_EAL g is ext-real Element of ExtREAL
seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
a ^\ seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of a
lim a is ext-real Element of ExtREAL
lim (a ^\ seq) is ext-real Element of ExtREAL
g is V11() real ext-real set
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
N + seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
Y - seq is V11() real ext-real V66() Element of REAL
(a ^\ seq) . (Y - seq) is ext-real Element of ExtREAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
x + seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . (x + seq) is ext-real Element of ExtREAL
(N + seq) - seq is V11() real ext-real V66() Element of REAL
a . Y is ext-real Element of ExtREAL
g is V11() real ext-real set
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
N + seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
Y - seq is V11() real ext-real V66() Element of REAL
(a ^\ seq) . (Y - seq) is ext-real Element of ExtREAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
x + seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . (x + seq) is ext-real Element of ExtREAL
(N + seq) - seq is V11() real ext-real V66() Element of REAL
a . Y is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(seq) is ext-real Element of ExtREAL
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
((seq)) is ext-real Element of ExtREAL
rng (seq) is non empty V45() V81() Element of K6(ExtREAL)
inf (rng (seq)) is ext-real Element of ExtREAL
(seq) is ext-real Element of ExtREAL
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
((seq)) is ext-real Element of ExtREAL
rng (seq) is non empty V45() V81() Element of K6(ExtREAL)
sup (rng (seq)) is ext-real Element of ExtREAL
a is V11() real ext-real Element of REAL
a + 1 is V11() real ext-real Element of REAL
g is ext-real set
dom (seq) is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
N is set
(seq) . N is ext-real Element of ExtREAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
(seq) . g is ext-real Element of ExtREAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
(seq) . g is ext-real Element of ExtREAL
a - 1 is V11() real ext-real Element of REAL
m is ext-real set
dom (seq) is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
Y is set
(seq) . Y is ext-real Element of ExtREAL
(a - 1) + 1 is V11() real ext-real Element of REAL
a + 0 is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
(seq) . m is ext-real Element of ExtREAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
(seq) . m is ext-real Element of ExtREAL
max (g,m) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq ^\ Y is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of seq
(seq) . Y is ext-real Element of ExtREAL
(seq) . Y is ext-real Element of ExtREAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . x is ext-real Element of ExtREAL
(seq) . x is ext-real Element of ExtREAL
(seq) . x is ext-real Element of ExtREAL
x is ext-real set
rng (seq ^\ Y) is non empty V45() V81() Element of K6(ExtREAL)
dom (seq ^\ Y) is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
k is set
(seq ^\ Y) . k is ext-real Element of ExtREAL
UB is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
UB + Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . (UB + Y) is ext-real Element of ExtREAL
x is ext-real set
k is set
(seq ^\ Y) . k is ext-real Element of ExtREAL
UB is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
UB + Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . (UB + Y) is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim seq is ext-real Element of ExtREAL
a is V11() real ext-real set
a is V11() real ext-real set
a + 1 is V11() real ext-real Element of REAL
g is V11() real ext-real set
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq ^\ N is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of seq
m is ext-real set
rng (seq ^\ N) is non empty V45() V81() Element of K6(ExtREAL)
dom (seq ^\ N) is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
Y is set
(seq ^\ N) . Y is ext-real Element of ExtREAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
x + g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . (x + g) is ext-real Element of ExtREAL
(seq . (x + g)) - (lim seq) is ext-real Element of ExtREAL
K179((lim seq)) is ext-real set
K178((seq . (x + g)),K179((lim seq))) is ext-real set
|.((seq . (x + g)) - (lim seq)).| is ext-real Element of ExtREAL
1. is ext-real Element of ExtREAL
- (lim seq) is ext-real Element of ExtREAL
(seq . (x + g)) + (- (lim seq)) is ext-real Element of ExtREAL
((seq . (x + g)) + (- (lim seq))) + (lim seq) is ext-real Element of ExtREAL
1. + (lim seq) is ext-real Element of ExtREAL
(- (lim seq)) + (lim seq) is ext-real Element of ExtREAL
(seq . (x + g)) + ((- (lim seq)) + (lim seq)) is ext-real Element of ExtREAL
0. is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real V44() V45() V46() V47() V48() V49() V50() V66() Element of ExtREAL
(seq . (x + g)) + 0. is ext-real Element of ExtREAL
a - 1 is V11() real ext-real Element of REAL
Y is ext-real set
x is set
(seq ^\ N) . x is ext-real Element of ExtREAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
k + g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . (k + g) is ext-real Element of ExtREAL
(seq . (k + g)) - (lim seq) is ext-real Element of ExtREAL
K178((seq . (k + g)),K179((lim seq))) is ext-real set
|.((seq . (k + g)) - (lim seq)).| is ext-real Element of ExtREAL
- 1. is ext-real Element of ExtREAL
(- 1.) + (lim seq) is ext-real Element of ExtREAL
(seq . (k + g)) + (- (lim seq)) is ext-real Element of ExtREAL
((seq . (k + g)) + (- (lim seq))) + (lim seq) is ext-real Element of ExtREAL
(seq . (k + g)) + ((- (lim seq)) + (lim seq)) is ext-real Element of ExtREAL
(seq . (k + g)) + 0. is ext-real Element of ExtREAL
- 1 is V11() real ext-real V66() Element of REAL
(- 1) + a is V11() real ext-real Element of REAL
seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
a ^\ seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of a
lim a is ext-real Element of ExtREAL
lim (a ^\ seq) is ext-real Element of ExtREAL
g is V11() real ext-real set
g is V11() real ext-real set
N is V11() real ext-real set
m is V11() real ext-real set
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
Y + seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . (Y + seq) is ext-real Element of ExtREAL
(a . (Y + seq)) - (lim a) is ext-real Element of ExtREAL
K179((lim a)) is ext-real set
K178((a . (Y + seq)),K179((lim a))) is ext-real set
|.((a . (Y + seq)) - (lim a)).| is ext-real Element of ExtREAL
(a ^\ seq) . Y is ext-real Element of ExtREAL
((a ^\ seq) . Y) - (lim a) is ext-real Element of ExtREAL
K178(((a ^\ seq) . Y),K179((lim a))) is ext-real set
|.(((a ^\ seq) . Y) - (lim a)).| is ext-real Element of ExtREAL
R_EAL g is ext-real Element of ExtREAL
seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
a ^\ seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of a
lim a is ext-real Element of ExtREAL
lim (a ^\ seq) is ext-real Element of ExtREAL
g is V11() real ext-real set
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
m + seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . (m + seq) is ext-real Element of ExtREAL
(a ^\ seq) . m is ext-real Element of ExtREAL
g is V11() real ext-real set
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
m + seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . (m + seq) is ext-real Element of ExtREAL
(a ^\ seq) . m is ext-real Element of ExtREAL
seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
a ^\ seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of a
rng a is non empty V45() V81() Element of K6(ExtREAL)
iseq is V11() real ext-real set
g is ext-real set
rng (a ^\ seq) is non empty V45() V81() Element of K6(ExtREAL)
dom (a ^\ seq) is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
N is set
(a ^\ seq) . N is ext-real Element of ExtREAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
m + seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . (m + seq) is ext-real Element of ExtREAL
iseq is V11() real ext-real set
g is ext-real set
N is set
(a ^\ seq) . N is ext-real Element of ExtREAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
m + seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . (m + seq) is ext-real Element of ExtREAL
seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(a) is ext-real Element of ExtREAL
rng a is non empty V45() V81() Element of K6(ExtREAL)
inf (rng a) is ext-real Element of ExtREAL
a . seq is ext-real Element of ExtREAL
(a) is ext-real Element of ExtREAL
sup (rng a) is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(seq) is ext-real Element of ExtREAL
rng seq is non empty V45() V81() Element of K6(ExtREAL)
inf (rng seq) is ext-real Element of ExtREAL
(seq) is ext-real Element of ExtREAL
sup (rng seq) is ext-real Element of ExtREAL
seq . 0 is ext-real Element of ExtREAL
seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
a ^\ seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of a
(a) is ext-real Element of ExtREAL
rng a is non empty V45() V81() Element of K6(ExtREAL)
inf (rng a) is ext-real Element of ExtREAL
((a ^\ seq)) is ext-real Element of ExtREAL
rng (a ^\ seq) is non empty V45() V81() Element of K6(ExtREAL)
inf (rng (a ^\ seq)) is ext-real Element of ExtREAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq + N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq + g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . (seq + g) is ext-real Element of ExtREAL
a . (seq + N) is ext-real Element of ExtREAL
(a ^\ seq) . g is ext-real Element of ExtREAL
(a ^\ seq) . N is ext-real Element of ExtREAL
g is ext-real set
dom a is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
N is set
a . N is ext-real Element of ExtREAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
(a ^\ seq) . m is ext-real Element of ExtREAL
m + seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . (m + seq) is ext-real Element of ExtREAL
a . m is ext-real Element of ExtREAL
g is ext-real set
dom (a ^\ seq) is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
N is set
(a ^\ seq) . N is ext-real Element of ExtREAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
(a ^\ seq) . m is ext-real Element of ExtREAL
m + seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . (m + seq) is ext-real Element of ExtREAL
seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
a ^\ seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of a
(a) is ext-real Element of ExtREAL
rng a is non empty V45() V81() Element of K6(ExtREAL)
sup (rng a) is ext-real Element of ExtREAL
((a ^\ seq)) is ext-real Element of ExtREAL
rng (a ^\ seq) is non empty V45() V81() Element of K6(ExtREAL)
sup (rng (a ^\ seq)) is ext-real Element of ExtREAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq + N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq + g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . (seq + N) is ext-real Element of ExtREAL
a . (seq + g) is ext-real Element of ExtREAL
(a ^\ seq) . N is ext-real Element of ExtREAL
(a ^\ seq) . g is ext-real Element of ExtREAL
g is ext-real set
dom a is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
N is set
a . N is ext-real Element of ExtREAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
(a ^\ seq) . m is ext-real Element of ExtREAL
m + seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . (m + seq) is ext-real Element of ExtREAL
a . m is ext-real Element of ExtREAL
g is ext-real set
dom (a ^\ seq) is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
N is set
(a ^\ seq) . N is ext-real Element of ExtREAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
(a ^\ seq) . m is ext-real Element of ExtREAL
m + seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . (m + seq) is ext-real Element of ExtREAL
seq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(a) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
(a) . seq is ext-real Element of ExtREAL
a ^\ seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of a
((a ^\ seq)) is ext-real Element of ExtREAL
rng (a ^\ seq) is non empty V45() V81() Element of K6(ExtREAL)
sup (rng (a ^\ seq)) is ext-real Element of ExtREAL
(a) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
(a) . seq is ext-real Element of ExtREAL
((a ^\ seq)) is ext-real Element of ExtREAL
inf (rng (a ^\ seq)) is ext-real Element of ExtREAL
{ (a . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : seq <= b₁ } is set
g is set
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . N is ext-real Element of ExtREAL
N - seq is V11() real ext-real V66() Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq + m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . (seq + m) is ext-real Element of ExtREAL
(a ^\ seq) . m is ext-real Element of ExtREAL
g is set
dom (a ^\ seq) is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
N is set
(a ^\ seq) . N is ext-real Element of ExtREAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq + m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . (seq + m) is ext-real Element of ExtREAL
g is non empty V45() Element of K6(ExtREAL)
sup g is ext-real Element of ExtREAL
N is non empty V45() Element of K6(ExtREAL)
inf N is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
(seq) is ext-real Element of ExtREAL
((seq)) is ext-real Element of ExtREAL
rng (seq) is non empty V45() V81() Element of K6(ExtREAL)
inf (rng (seq)) is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq ^\ a is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of seq
((seq ^\ a)) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
(seq) ^\ a is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of (seq)
((seq ^\ a)) is ext-real Element of ExtREAL
(((seq ^\ a))) is ext-real Element of ExtREAL
rng ((seq ^\ a)) is non empty V45() V81() Element of K6(ExtREAL)
inf (rng ((seq ^\ a))) is ext-real Element of ExtREAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
{ ((seq ^\ a) . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : g <= b₁ } is set
((seq ^\ a)) . g is ext-real Element of ExtREAL
a + g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
{ (seq . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : a + g <= b₁ } is set
(seq) . (a + g) is ext-real Element of ExtREAL
N is set
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . m is ext-real Element of ExtREAL
m - a is V11() real ext-real V66() Element of REAL
Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a + Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . (a + Y) is ext-real Element of ExtREAL
(a + g) - a is V11() real ext-real V66() Element of REAL
{ (seq . (a + b₁)) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : g <= b₁ } is set
N is set
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a + m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . (a + m) is ext-real Element of ExtREAL
N is set
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a + m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . (a + m) is ext-real Element of ExtREAL
(seq ^\ a) . m is ext-real Element of ExtREAL
N is set
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
(seq ^\ a) . m is ext-real Element of ExtREAL
a + m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . (a + m) is ext-real Element of ExtREAL
((seq) ^\ a) . g is ext-real Element of ExtREAL
N is non empty V45() Element of K6(ExtREAL)
sup N is ext-real Element of ExtREAL
m is non empty V45() Element of K6(ExtREAL)
sup m is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
(seq) is ext-real Element of ExtREAL
((seq)) is ext-real Element of ExtREAL
rng (seq) is non empty V45() V81() Element of K6(ExtREAL)
sup (rng (seq)) is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq ^\ a is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of seq
((seq ^\ a)) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
(seq) ^\ a is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of (seq)
((seq ^\ a)) is ext-real Element of ExtREAL
(((seq ^\ a))) is ext-real Element of ExtREAL
rng ((seq ^\ a)) is non empty V45() V81() Element of K6(ExtREAL)
sup (rng ((seq ^\ a))) is ext-real Element of ExtREAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
{ ((seq ^\ a) . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : g <= b₁ } is set
((seq ^\ a)) . g is ext-real Element of ExtREAL
a + g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
{ (seq . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : a + g <= b₁ } is set
(seq) . (a + g) is ext-real Element of ExtREAL
N is set
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . m is ext-real Element of ExtREAL
m - a is V11() real ext-real V66() Element of REAL
Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a + Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . (a + Y) is ext-real Element of ExtREAL
(a + g) - a is V11() real ext-real V66() Element of REAL
{ (seq . (a + b₁)) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : g <= b₁ } is set
N is set
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a + m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . (a + m) is ext-real Element of ExtREAL
N is set
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a + m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . (a + m) is ext-real Element of ExtREAL
(seq ^\ a) . m is ext-real Element of ExtREAL
N is set
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
(seq ^\ a) . m is ext-real Element of ExtREAL
a + m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . (a + m) is ext-real Element of ExtREAL
((seq) ^\ a) . g is ext-real Element of ExtREAL
N is non empty V45() Element of K6(ExtREAL)
inf N is ext-real Element of ExtREAL
m is non empty V45() Element of K6(ExtREAL)
inf m is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . a is ext-real Element of ExtREAL
seq ^\ a is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of seq
((seq ^\ a)) is ext-real Element of ExtREAL
rng (seq ^\ a) is non empty V45() V81() Element of K6(ExtREAL)
sup (rng (seq ^\ a)) is ext-real Element of ExtREAL
g is ext-real set
dom (seq ^\ a) is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
N is set
(seq ^\ a) . N is ext-real Element of ExtREAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
m + a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . (m + a) is ext-real Element of ExtREAL
(seq ^\ a) . 0 is ext-real Element of ExtREAL
0 + a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . (0 + a) is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . a is ext-real Element of ExtREAL
seq ^\ a is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of seq
((seq ^\ a)) is ext-real Element of ExtREAL
rng (seq ^\ a) is non empty V45() V81() Element of K6(ExtREAL)
inf (rng (seq ^\ a)) is ext-real Element of ExtREAL
g is ext-real set
dom (seq ^\ a) is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
N is set
(seq ^\ a) . N is ext-real Element of ExtREAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
m + a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . (m + a) is ext-real Element of ExtREAL
(seq ^\ a) . 0 is ext-real Element of ExtREAL
0 + a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . (0 + a) is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim seq is ext-real Element of ExtREAL
(seq) is ext-real Element of ExtREAL
rng seq is non empty V45() V81() Element of K6(ExtREAL)
inf (rng seq) is ext-real Element of ExtREAL
a is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim a is V11() real ext-real Element of REAL
lim_sup a is V11() real ext-real Element of REAL
superior_realsequence a is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lower_bound (superior_realsequence a) is V11() real ext-real Element of REAL
rng (superior_realsequence a) is V44() V45() V46() Element of K6(REAL)
lower_bound (rng (superior_realsequence a)) is V11() real ext-real Element of REAL
lower_bound a is V11() real ext-real Element of REAL
rng a is V44() V45() V46() Element of K6(REAL)
lower_bound (rng a) is V11() real ext-real Element of REAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim seq is ext-real Element of ExtREAL
(seq) is ext-real Element of ExtREAL
rng seq is non empty V45() V81() Element of K6(ExtREAL)
sup (rng seq) is ext-real Element of ExtREAL
a is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim a is V11() real ext-real Element of REAL
lim_inf a is V11() real ext-real Element of REAL
inferior_realsequence a is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
upper_bound (inferior_realsequence a) is V11() real ext-real Element of REAL
rng (inferior_realsequence a) is V44() V45() V46() Element of K6(REAL)
upper_bound (rng (inferior_realsequence a)) is V11() real ext-real Element of REAL
upper_bound a is V11() real ext-real Element of REAL
rng a is V44() V45() V46() Element of K6(REAL)
upper_bound (rng a) is V11() real ext-real Element of REAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
a is V11() real ext-real set
iseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
seq . iseq is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
a is V11() real ext-real set
iseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
seq . iseq is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(seq) is ext-real Element of ExtREAL
rng seq is non empty V45() V81() Element of K6(ExtREAL)
inf (rng seq) is ext-real Element of ExtREAL
lim seq is ext-real Element of ExtREAL
a is V11() real ext-real set
iseq is ext-real set
g is set
seq . g is ext-real Element of ExtREAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
seq . m is ext-real Element of ExtREAL
seq . N is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(seq) is ext-real Element of ExtREAL
rng seq is non empty V45() V81() Element of K6(ExtREAL)
sup (rng seq) is ext-real Element of ExtREAL
lim seq is ext-real Element of ExtREAL
a is V11() real ext-real set
iseq is ext-real set
g is set
seq . g is ext-real Element of ExtREAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
seq . m is ext-real Element of ExtREAL
seq . N is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim seq is ext-real Element of ExtREAL
(seq) is ext-real Element of ExtREAL
rng seq is non empty V45() V81() Element of K6(ExtREAL)
inf (rng seq) is ext-real Element of ExtREAL
a is set
{+infty} is non empty V45() set
iseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
dom seq is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
seq . iseq is ext-real Element of ExtREAL
a is set
iseq is set
seq . iseq is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . a is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . a is ext-real Element of ExtREAL
seq ^\ a is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of seq
((seq ^\ a)) is ext-real Element of ExtREAL
rng (seq ^\ a) is non empty V45() V81() Element of K6(ExtREAL)
inf (rng (seq ^\ a)) is ext-real Element of ExtREAL
{-infty} is non empty V45() set
((seq ^\ a)) is ext-real Element of ExtREAL
sup (rng (seq ^\ a)) is ext-real Element of ExtREAL
lim (seq ^\ a) is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . a is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim seq is ext-real Element of ExtREAL
(seq) is ext-real Element of ExtREAL
rng seq is non empty V45() V81() Element of K6(ExtREAL)
sup (rng seq) is ext-real Element of ExtREAL
a is set
{-infty} is non empty V45() set
iseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
dom seq is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
seq . iseq is ext-real Element of ExtREAL
a is set
iseq is set
seq . iseq is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . a is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . a is ext-real Element of ExtREAL
seq ^\ a is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of seq
((seq ^\ a)) is ext-real Element of ExtREAL
rng (seq ^\ a) is non empty V45() V81() Element of K6(ExtREAL)
sup (rng (seq ^\ a)) is ext-real Element of ExtREAL
{+infty} is non empty V45() set
((seq ^\ a)) is ext-real Element of ExtREAL
inf (rng (seq ^\ a)) is ext-real Element of ExtREAL
lim (seq ^\ a) is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . a is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
a is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim seq is ext-real Element of ExtREAL
lim a is ext-real Element of ExtREAL
iseq is V11() real ext-real set
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
seq . N is ext-real Element of ExtREAL
a . N is ext-real Element of ExtREAL
iseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq ^\ iseq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of seq
rng (seq ^\ iseq) is non empty V45() V81() Element of K6(ExtREAL)
g is V11() real ext-real set
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a ^\ N is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of a
max (iseq,N) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a ^\ m is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of a
lim (a ^\ m) is ext-real Element of ExtREAL
dom (seq ^\ iseq) is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
m - iseq is V11() real ext-real V66() Element of REAL
x is set
seq ^\ m is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of seq
rng (seq ^\ m) is non empty V45() V81() Element of K6(ExtREAL)
dom (seq ^\ m) is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
k is set
(seq ^\ m) . k is ext-real Element of ExtREAL
UB is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
m + UB is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . (m + UB) is ext-real Element of ExtREAL
Y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
Y + UB is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
iseq + (Y + UB) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . (iseq + (Y + UB)) is ext-real Element of ExtREAL
(seq ^\ iseq) . (Y + UB) is ext-real Element of ExtREAL
Y is V11() real ext-real set
rng (a ^\ N) is non empty V45() V81() Element of K6(ExtREAL)
k is V11() real ext-real set
lim (seq ^\ m) is ext-real Element of ExtREAL
UB is V11() real ext-real set
dom (a ^\ N) is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
m - N is V11() real ext-real V66() Element of REAL
n is set
rng (a ^\ m) is non empty V45() V81() Element of K6(ExtREAL)
dom (a ^\ m) is V44() V45() V46() V47() V48() V49() Element of K6(NAT)
n is set
(a ^\ m) . n is ext-real Element of ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
m + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . (m + n) is ext-real Element of ExtREAL
rseq2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
rseq2 + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
N + (rseq2 + n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . (N + (rseq2 + n)) is ext-real Element of ExtREAL
(a ^\ N) . (rseq2 + n) is ext-real Element of ExtREAL
rseq2 is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
x is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
x . n is V11() real ext-real Element of REAL
rseq2 . n is V11() real ext-real Element of REAL
(a ^\ m) . n is ext-real Element of ExtREAL
m + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
a . (m + n) is ext-real Element of ExtREAL
(seq ^\ m) . n is ext-real Element of ExtREAL
seq . (m + n) is ext-real Element of ExtREAL
lim x is V11() real ext-real Element of REAL
lim rseq2 is V11() real ext-real Element of REAL
iseq is V11() real ext-real set
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
seq . N is ext-real Element of ExtREAL
a . N is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(seq) is ext-real Element of ExtREAL
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
((seq)) is ext-real Element of ExtREAL
rng (seq) is non empty V45() V81() Element of K6(ExtREAL)
sup (rng (seq)) is ext-real Element of ExtREAL
(seq) is ext-real Element of ExtREAL
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
((seq)) is ext-real Element of ExtREAL
rng (seq) is non empty V45() V81() Element of K6(ExtREAL)
inf (rng (seq)) is ext-real Element of ExtREAL
lim (seq) is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . a is ext-real Element of ExtREAL
(seq) . a is ext-real Element of ExtREAL
(seq) . a is ext-real Element of ExtREAL
lim (seq) is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(seq) is ext-real Element of ExtREAL
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
((seq)) is ext-real Element of ExtREAL
rng (seq) is non empty V45() V81() Element of K6(ExtREAL)
sup (rng (seq)) is ext-real Element of ExtREAL
(seq) is ext-real Element of ExtREAL
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
((seq)) is ext-real Element of ExtREAL
rng (seq) is non empty V45() V81() Element of K6(ExtREAL)
inf (rng (seq)) is ext-real Element of ExtREAL
lim seq is ext-real Element of ExtREAL
a is V11() real ext-real set
iseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
(seq) . g is ext-real Element of ExtREAL
seq . g is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(seq) is ext-real Element of ExtREAL
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
((seq)) is ext-real Element of ExtREAL
rng (seq) is non empty V45() V81() Element of K6(ExtREAL)
sup (rng (seq)) is ext-real Element of ExtREAL
(seq) is ext-real Element of ExtREAL
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
((seq)) is ext-real Element of ExtREAL
rng (seq) is non empty V45() V81() Element of K6(ExtREAL)
inf (rng (seq)) is ext-real Element of ExtREAL
lim seq is ext-real Element of ExtREAL
a is V11() real ext-real set
iseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
seq . g is ext-real Element of ExtREAL
(seq) . g is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(seq) is ext-real Element of ExtREAL
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
((seq)) is ext-real Element of ExtREAL
rng (seq) is non empty V45() V81() Element of K6(ExtREAL)
sup (rng (seq)) is ext-real Element of ExtREAL
(seq) is ext-real Element of ExtREAL
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
((seq)) is ext-real Element of ExtREAL
rng (seq) is non empty V45() V81() Element of K6(ExtREAL)
inf (rng (seq)) is ext-real Element of ExtREAL
lim seq is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq ^\ a is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of seq
iseq is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim_sup iseq is V11() real ext-real Element of REAL
superior_realsequence iseq is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lower_bound (superior_realsequence iseq) is V11() real ext-real Element of REAL
rng (superior_realsequence iseq) is V44() V45() V46() Element of K6(REAL)
lower_bound (rng (superior_realsequence iseq)) is V11() real ext-real Element of REAL
((seq ^\ a)) is ext-real Element of ExtREAL
((seq ^\ a)) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
(((seq ^\ a))) is ext-real Element of ExtREAL
rng ((seq ^\ a)) is non empty V45() V81() Element of K6(ExtREAL)
inf (rng ((seq ^\ a))) is ext-real Element of ExtREAL
lim_inf iseq is V11() real ext-real Element of REAL
inferior_realsequence iseq is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
upper_bound (inferior_realsequence iseq) is V11() real ext-real Element of REAL
rng (inferior_realsequence iseq) is V44() V45() V46() Element of K6(REAL)
upper_bound (rng (inferior_realsequence iseq)) is V11() real ext-real Element of REAL
((seq ^\ a)) is ext-real Element of ExtREAL
((seq ^\ a)) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
(((seq ^\ a))) is ext-real Element of ExtREAL
rng ((seq ^\ a)) is non empty V45() V81() Element of K6(ExtREAL)
sup (rng ((seq ^\ a))) is ext-real Element of ExtREAL
lim iseq is V11() real ext-real Element of REAL
lim (seq ^\ a) is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
(seq) is ext-real Element of ExtREAL
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
((seq)) is ext-real Element of ExtREAL
rng (seq) is non empty V45() V81() Element of K6(ExtREAL)
sup (rng (seq)) is ext-real Element of ExtREAL
(seq) is ext-real Element of ExtREAL
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
((seq)) is ext-real Element of ExtREAL
rng (seq) is non empty V45() V81() Element of K6(ExtREAL)
inf (rng (seq)) is ext-real Element of ExtREAL
iseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq ^\ iseq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued subsequence of seq
g is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim_sup g is V11() real ext-real Element of REAL
superior_realsequence g is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lower_bound (superior_realsequence g) is V11() real ext-real Element of REAL
rng (superior_realsequence g) is V44() V45() V46() Element of K6(REAL)
lower_bound (rng (superior_realsequence g)) is V11() real ext-real Element of REAL
((seq ^\ iseq)) is ext-real Element of ExtREAL
((seq ^\ iseq)) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
(((seq ^\ iseq))) is ext-real Element of ExtREAL
rng ((seq ^\ iseq)) is non empty V45() V81() Element of K6(ExtREAL)
inf (rng ((seq ^\ iseq))) is ext-real Element of ExtREAL
lim_inf g is V11() real ext-real Element of REAL
inferior_realsequence g is non empty V16() V19( NAT ) V20( REAL ) V21() V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
upper_bound (inferior_realsequence g) is V11() real ext-real Element of REAL
rng (inferior_realsequence g) is V44() V45() V46() Element of K6(REAL)
upper_bound (rng (inferior_realsequence g)) is V11() real ext-real Element of REAL
((seq ^\ iseq)) is ext-real Element of ExtREAL
((seq ^\ iseq)) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
(((seq ^\ iseq))) is ext-real Element of ExtREAL
rng ((seq ^\ iseq)) is non empty V45() V81() Element of K6(ExtREAL)
sup (rng ((seq ^\ iseq))) is ext-real Element of ExtREAL
iseq is V11() real ext-real set
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
(seq) . N is ext-real Element of ExtREAL
seq . N is ext-real Element of ExtREAL
lim (seq) is ext-real Element of ExtREAL
g is V11() real ext-real set
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
{ (seq . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : m <= b₁ } is set
(seq) . m is ext-real Element of ExtREAL
Y is non empty V45() Element of K6(ExtREAL)
sup Y is ext-real Element of ExtREAL
x is ext-real set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . k is ext-real Element of ExtREAL
lim (seq) is ext-real Element of ExtREAL
iseq is V11() real ext-real set
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
seq . N is ext-real Element of ExtREAL
(seq) . N is ext-real Element of ExtREAL
lim (seq) is ext-real Element of ExtREAL
g is V11() real ext-real set
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V66() set
{ (seq . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT : m <= b₁ } is set
(seq) . m is ext-real Element of ExtREAL
Y is non empty V45() Element of K6(ExtREAL)
inf Y is ext-real Element of ExtREAL
x is ext-real set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V44() V45() V46() V47() V48() V49() V66() V67() Element of NAT
seq . k is ext-real Element of ExtREAL
lim (seq) is ext-real Element of ExtREAL
seq is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of K6(K7(NAT,ExtREAL))
lim seq is ext-real Element of ExtREAL
(seq) is ext-real Element of ExtREAL
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-decreasing Element of K6(K7(NAT,ExtREAL))
((seq)) is ext-real Element of ExtREAL
rng (seq) is non empty V45() V81() Element of K6(ExtREAL)
sup (rng (seq)) is ext-real Element of ExtREAL
(seq) is ext-real Element of ExtREAL
(seq) is non empty V16() V19( NAT ) V20( ExtREAL ) V21() V26( NAT ) V30( NAT , ExtREAL ) ext-real-valued non-increasing Element of K6(K7(NAT,ExtREAL))
((seq)) is ext-real Element of ExtREAL
rng (seq) is non empty V45() V81() Element of K6(ExtREAL)
inf (rng (seq)) is ext-real Element of ExtREAL