theorem Th39: :: ASYMPT_0:39

for f being eventually-nonnegative Real_Sequence

for t being eventually-nonnegative eventually-nondecreasing Real_Sequence

for b being Element of NAT st f is smooth & b >= 2 & t in Big_Omega (f, { (b |^ n) where n is Element of NAT : verum } ) holds

t in Big_Omega f

for t being eventually-nonnegative eventually-nondecreasing Real_Sequence

for b being Element of NAT st f is smooth & b >= 2 & t in Big_Omega (f, { (b |^ n) where n is Element of NAT : verum } ) holds

t in Big_Omega f