A constructive proof of the Heine-Borel covering theorem for formal reals

DOI10.1007/3-540-61780-9_62zbMath1434.03141OpenAlexW1534635720MaRDI QIDQ4647570

Sara Negri, Jan Cederquist

Publication date: 15 January 2019

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://research.utwente.nl/en/publications/a-constructive-proof-of-the-heineborel-covering-theorem-for-formal-reals(84cb46d6-1df0-479b-ad6f-07a9540ae5e7).html

zbMATH Keywords

formal spacefinite subsetformal pointinduction hypothesisformal real

Mathematics Subject Classification ID

Constructive and recursive analysis (03F60)

Related Items (6)

Unnamed Item ⋮ The intensional side of algebraic-topological representation theorems ⋮ Inductively generated formal topologies. ⋮ Locatedness and overt sublocales ⋮ The principle of pointfree continuity ⋮ Formal Zariski topology: Positivity and points

Uses Software

• ALF

Cites Work

• Constructive domain theory as a branch of intuitionistic pointfree topology
• The continuum as a formal space
• Intuitionism. An introduction. 3rd revised ed
• An intuitionistic proof of Tychonoff's theorem
• Tychonoff's theorem in the framework of formal topologies
• Constructive topology and combinatorics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A constructive proof of the Heine-Borel covering theorem for formal reals