mathlib

dc788a0b - feat(topology/sequences): every first-countable space is sequential (#1528)

feat(topology/sequences): every first-countable space is sequential (#1528) * feat(topology/sequences): every first-countable space is sequential * fixup style * fixup comments * remove redundant type ascription