@article{lmcs:4651, title = {Every metric space is separable in function realizability}, author = {Andrej Bauer and Andrew Swan}, url = {https://lmcs.episciences.org/4651}, doi = {10.23638/LMCS-15(2:14)2019}, journal = {Logical Methods in Computer Science}, issn = {1860-5974}, volume = {Volume 15, Issue 2}, eid = 16, year = {2019}, month = {May}, keywords = {Mathematics - Logic, Computer Science - Logic in Computer Science, 54E35, 03F60, 03F55}, }