:: deftheorem defines Big_Theta ASYMPT_0:def 14 :

for f being eventually-nonnegative Real_Sequence

for X being set holds Big_Theta (f,X) = { t where t is Element of Funcs (NAT,REAL) : ex c, d being Real ex N being Element of NAT st

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

( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) } ;

for f being eventually-nonnegative Real_Sequence

for X being set holds Big_Theta (f,X) = { t where t is Element of Funcs (NAT,REAL) : ex c, d being Real ex N being Element of NAT st

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

( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) } ;