Countable spaces are second countable

Stream: Is there code for X?

[Felix Weilacher]

example [Countable α] [TopologicalSpace α] : SecondCountableTopology α := inferInstance --fails

[Felix Weilacher]

there is docs#TopologicalSpace.Countable.to_separableSpace which is weaker

[Alex J. Best]

If I'm interpreting the question right then it appears it's not true: https://math.stackexchange.com/questions/3272545/are-countable-topological-spaces-second-countable

[Felix Weilacher]

Woah! Thanks for the find

[Wojciech Nawrocki]

Also https://topology.pi-base.org/spaces?q=countable%20%2B%20~second