Commit 2022-07-16 11:29 316d1886

feat(order/filter): add map_neg_at_top, change some assumptions (#15237)

• add map_neg_at_top, map_neg_at_bot, comap_neg_at_top, and comap_neg_at_bot;
• add disjoint_pure_at_top, disjoint_pure_at_bot, not_tendsto_const_at_top, not_tendsto_const_at_bot;
• more lemmas about order_iso and at_top/at_bot up, no modifications to the code;
• rename tendsto_at_top_iff_tends_to_neg_at_bot to tendsto_neg_at_top_iff, swap LHS and RHS, mark as @[simp];
• rename tendsto_at_bot_iff_tends_to_neg_at_top to tendsto_neg_at_bot_iff, swap LHS and RHS, mark as @[simp];
• use n ≠ 0 instead of 1 ≤ n in tendsto_pow_at_top, tendsto_const_mul_pow_at_top, tendsto_const_mul_pow_at_top_iff, tendsto_neg_const_mul_pow_at_top, tendsto_neg_const_mul_pow_at_top_iff.