Constructive metrisability in point-free topology.
type: Item
instance of: scholarly article
title: Constructive metrisability in point-free topology.
zbMATH Open document ID: 1045.54002
DOI: 10.1016/S0304-3975(02)00699-0
author: Giovanni Curi
published in: Theoretical Computer Science
publication date: 2004-03-14T00:00:00Z
review text: The author introduces the notion of elementary diameter to provide a constructive notion of metrisability (in the context of locale theory). First, he investigates a predicative formulation and properties of complete regularity. The main notion of metric formal topologies is based on a constructive and predicative notion of metrisability and a point-free axiomatisation of the theory of metrics in spaces. Rather than the properties of a diameter in the general sense, the author describes a diameter of basic or atomic elements. The main result is a point-free version of the Urysohn metrization theorem with a constructive choice-free proof. As an application, the author shows that the points of locally compact metrisable formal topologies can be identified with ``shrinking'' and ``approximating'' sequences of basic neighbourhoods.
Mathematics Subject Classification ID: 54A05
Mathematics Subject Classification ID: 54E35
Mathematics Subject Classification ID: 03F60
zbMATH DE Number: 2055969
zbMATH Keywords: locale theory
zbMATH Keywords: metrisability
zbMATH Keywords: diameter
zbMATH Keywords: complete regularity
zbMATH Keywords: type theory
reviewed by: Bohumil František Šmarda
MaRDI profile type: Publication
cites work: Q3937387
cites work: Compactification of Frames
cites work: Q4955942
cites work: Q3803111
cites work: Q3869847
cites work: Q4247301
cites work: Inductively generated formal topologies.
cites work: Q4552734
cites work: The regular-locally compact coreflection of a stably locally compact locale
cites work: Q3322099
cites work: Atomless Parts of Spaces.
cites work: Q3965241
cites work: Q3322276
cites work: Q3262213
cites work: Q5181669
cites work: Q3688389
cites work: A globalization of the Hahn-Banach theorem
cites work: Q4246953
cites work: Q3999860
cites work: Q3331896
cites work: Q3679869
cites work: Categories of diametric frames
cites work: Q3481701
cites work: Some points in formal topology.
cites work: Q4247310
cites work: Q5649639
cites work: Effectively given domains
cites work: Embedding metric spaces into CPO's
description: scientific article; zbMATH DE number 2055969