mathlib3

bfe595d3 - feat(order/filter,topology/instances/real): lemmas about `at_top`, `at_bot`, and `cocompact` (#10652)

feat(order/filter,topology/instances/real): lemmas about `at_top`, `at_bot`, and `cocompact` (#10652) * prove `comap abs at_top = at_bot ⊔ at_top`; * prove `comap coe at_top = at_top` and `comap coe at_bot = at_bot` for coercion from `ℕ`, `ℤ`, or `ℚ` to an archimedian semiring, ring, or field, respectively; * prove `cocompact ℤ = at_bot ⊔ at_top` and `cocompact ℝ = at_bot ⊔ at_top`.