basic): golf a proof (#3521)

Commit

5 years ago

chore(topology/uniform_space/basic): golf a proof (#3521) Also prove that a `subsingleton` has a unique `topological_space` structure.

Author

urkud

Parents