Metric spaces in synthetic topology

DOI10.1016/j.apal.2011.06.017zbMath1251.03081WikidataQ115902567 ScholiaQ115902567MaRDI QIDQ651311

Davorin Lešnik, Andrej Bauer

Publication date: 12 December 2011

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2011.06.017

zbMATH Keywords

constructive metric spaces; metrization axiom; synthetic topology

Mathematics Subject Classification ID

54E35: Metric spaces, metrizability

03F60: Constructive and recursive analysis

18B25: Topoi

03F65: Other constructive mathematics

03F55: Intuitionistic mathematics

Related Items

Quotienting the delay monad by weak bisimilarity, Brouwer's fixed-point theorem in real-cohesive homotopy type theory, Unnamed Item, Every metric space is separable in function realizability, On the topological aspects of the theory of represented spaces, Constructive decidability of classical continuity, The intrinsic topology of Martin-Löf universes, On fixed-point theorems in synthetic computability

Cites Work

• Constructivism in mathematics. An introduction. Volume II
• Church's thesis without tears
• On the interpretation of intuitionistic number theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item