:: deftheorem defines Big_Oh ASYMPT_0:def 9 :
for f being eventually-nonnegative Real_Sequence holds Big_Oh f = { t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) ) ) } ;