Every metric space is separable in function realizability

zbMath1431.03076arXiv1804.00427MaRDI QIDQ5377467

Andrew Swan, Andrej Bauer

Publication date: 24 May 2019

Full work available at URL: https://arxiv.org/abs/1804.00427

zbMATH Keywords

metric spacesconstructive mathematicssynthetic topologyfunction realizability

Mathematics Subject Classification ID

Metric spaces, metrizability (54E35) Constructive and recursive analysis (03F60) Intuitionistic mathematics (03F55)

Cites Work

• Unnamed Item
• Unnamed Item
• Metric spaces in synthetic topology
• Realizability. An introduction to its categorical side
• Generalized real numbers in constructive mathematics
• Principles of intuitionism. Lectures presented at the summer conference on intuitionism and proof theory (1968) at SUNY at Buffalo, NY

This page was built for publication: Every metric space is separable in function realizability