mathlib

d88042c1 - feat(order/filter/at_top_bot): lemmas about `map/comap` of `at_top`/`at_bot` (#4878)

feat(order/filter/at_top_bot): lemmas about `map/comap` of `at_top`/`at_bot` (#4878) * Redefine `at_top`/`at_bot` using `Ici`/`Iic`. * Add lemmas about `map`/`comap` of `at_top`/`at_bot` under `coe : s → α`, where `s` is one of `Ici a`, `Iic a`, `Ioi a`, `Iio a`.