Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems
Дата
Авторы
Coquand,Thierry
Spitters,Bas
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
We present a constructive proof of the Stone-Yosida representation theorem for Riesz spaces motivated by considerations from formal topology. This theorem is used to derive a representation theorem for f-algebras. In turn, this theorem implies the Gelfand representation theorem for C*-algebras of operators on Hilbert spaces as formulated by Bishop and Bridges. Our proof is shorter, clearer, and we avoid the use of approximate eigenvalues.
Ключевые слова
formal topology , constructive mathematics , Riesz space , f-algebra , axiom of choice