Commit 2021-12-09 11:18 bfe595d3

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.