mathlib3

316d1886 - feat(order/filter): add `map_neg_at_top`, change some assumptions (#15237)

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`.