:: deftheorem defines Big_Omega ASYMPT_0:def 10 :

for f being eventually-nonnegative Real_Sequence holds Big_Omega f = { t where t is Element of Funcs (NAT,REAL) : ex d being Real ex N being Element of NAT st

( d > 0 & ( for n being Element of NAT st n >= N holds

( t . n >= d * (f . n) & t . n >= 0 ) ) ) } ;

for f being eventually-nonnegative Real_Sequence holds Big_Omega f = { t where t is Element of Funcs (NAT,REAL) : ex d being Real ex N being Element of NAT st

( d > 0 & ( for n being Element of NAT st n >= N holds

( t . n >= d * (f . n) & t . n >= 0 ) ) ) } ;