mathlib

27df8a0d - feat(topology/instances/rat): some facts about topology on `rat` (#11832)

feat(topology/instances/rat): some facts about topology on `rat` (#11832) * `ℚ` is a totally disconnected space; * `cocompact ℚ` is not a countably generated filter; * hence, `alexandroff ℚ` is not a first countable topological space.