Commit 2020-12-14 13:16 0d7ddf1f

chore(order/filter/at_top_bot): add/rename lemmas about limits like ±∞*c (#5333)

New lemmas

• filter.tendsto.nsmul_at_top and filter.tendsto.nsmul_at_bot;
• filter.tendsto_mul_self_at_top;
• filter.tendsto.at_top_mul_at_bot, filter.tendsto.at_bot_mul_at_top, filter.tendsto.at_bot_mul_at_bot;
• filter.tendsto.at_top_of_const_mul, filter.tendsto.at_top_of_mul_const;
• filter.tendsto.at_top_div_const, filter.tendsto.neg_const_mul_at_top, filter.tendsto.at_top_mul_neg_const, filter.tendsto.const_mul_at_bot, filter.tendsto.at_bot_mul_const, filer.tendsto.at_bot_div_const, filter.tendsto.neg_const_mul_at_bot, filter.tendsto.at_bot_mul_neg_const.

Renamed lemmas

• tendsto_pow_at_top → filter.tendsto_pow_at_top;
• tendsto_at_top_mul_left → filter.tendsto.const_mul_at_top';
• tendsto_at_top_mul_right → filter.tendsto.at_top_mul_const';
• tendsto_at_top_mul_left' → filter.tendsto.const_mul_at_top;
• tendsto_at_top_mul_right' → filer.tendsto.at_top_mul_const;
• tendsto_mul_at_top → filter.tendsto.at_top_mul;
• tendsto_mul_at_bot → filter.tendsto.at_top_mul_neg;
• tendsto_at_top_mul_at_top → filter.tendsto.at_top_mul_at_top.