scientific article; zbMATH DE number 1302057

MaRDI QIDQ4247301zbMATH OpenFDO

Authors Jan Cederquist, Thierry Coquand, Sara Negri

Publication date 5 October 1999

zbMATH Keywords

constructive analysisformal topologypointfree approach to functional analysis

Mathematics Subject Classification ID

Constructive and recursive analysis (03F60) Constructive functional analysis (46S30)

Review text

The authors present constructive proofs of theorems of Alaoglu and Helly-Hahn-Banach. The area of their interest is the pointfree approach to functional analysis through formal topology. For the entire collection see [Zbl 0899.00026].

Cited in

(12)

• Helly's selection theorem and the principle of local reflexivity of ordered type
• Constructive metrisability in point-free topology.
• Some points in formal topology.
• Eliminating disjunctions by disjunction elimination
• The symbol of type and the Wilson theorem
• The Hahn-Banach theorem by disjunction elimination
• The intensional side of algebraic-topological representation theorems
• An implementation of the Heine-Borel covering theorem in type theory
• Extension by conservation. Sikorski's theorem
• THE JACOBSON RADICAL OF A PROPOSITIONAL THEORY
• Eliminating disjunctions by disjunction elimination
• Duality theory in linear optimization and its extensions -- formally verified

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4247301)