:: deftheorem defines is_smooth_wrt ASYMPT_0:def 16 :

for f being eventually-nonnegative Real_Sequence

for b being Nat holds

( f is_smooth_wrt b iff ( f is eventually-nondecreasing & f taken_every b in Big_Oh f ) );

for f being eventually-nonnegative Real_Sequence

for b being Nat holds

( f is_smooth_wrt b iff ( f is eventually-nondecreasing & f taken_every b in Big_Oh f ) );