:: deftheorem Def6 defines eventually-nondecreasing ASYMPT_0:def 6 :

for f being Real_Sequence holds

( f is eventually-nondecreasing iff ex N being Nat st

for n being Nat st n >= N holds

f . n <= f . (n + 1) );

for f being Real_Sequence holds

( f is eventually-nondecreasing iff ex N being Nat st

for n being Nat st n >= N holds

f . n <= f . (n + 1) );