A constructive and functorial embedding of locally compact metric spaces into locales

DOI10.1016/j.topol.2007.01.018zbMath1116.03057OpenAlexW2085491633MaRDI QIDQ881455

Erik Palmgren

Publication date: 30 May 2007

Published in: Topology and its Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.topol.2007.01.018

zbMATH Keywords

localeslocally compact metric spacesformal topologies

Mathematics Subject Classification ID

Metric spaces, metrizability (54E35) Categorical methods in general topology (54B30) Frames, locales (06D22) Other constructive mathematics (03F65) Local compactness, (sigma)-compactness (54D45)

Related Items (8)

Atomicity, coherence of information, and point-free structures ⋮ Metric complements of overt closed sets ⋮ Formally continuous functions on Baire space ⋮ Locatedness and overt sublocales ⋮ Brouwer's fixed-point theorem in real-cohesive homotopy type theory ⋮ Formal continuity implies uniform continuity near compact images on metric spaces ⋮ Problems, solutions, and completions ⋮ Closed subsets in Bishop topological groups

Cites Work

• Domain representability of metric spaces
• Inductively generated formal topologies.
• Some points in formal topology.
• Aspects of general topology in constructive set theory
• On the collection of points of a formal space
• Regular universes and formal spaces
• Localic completion of generalized metric spaces II: Powerlocales
• From Intuitionistic to Point-Free Topology: On the Foundation of Homotopy Theory
• Forcing in intuitionistic systems without power-set
• From Sets and Types to Topology and Analysis
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A constructive and functorial embedding of locally compact metric spaces into locales