ﻻ يوجد ملخص باللغة العربية
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.
In Riesz space theory it is good practice to avoid representation theorems which depend on the axiom of choice. Here we present a general methodology to do this using pointfree topology. To illustrate the technique we show that almost f-algebras are
We present a constructive proof of Gelfand duality for C*-algebras by reducing the problem to Gelfand duality for real C*-algebras.
Let $X$ and $Y$ be completely regular spaces and $E$ and $F$ be Hausdorff topological vector spaces. We call a linear map $T$ from a subspace of $C(X,E)$ into $C(Y,F)$ a emph{Banach-Stone map} if it has the form $Tf(y) = S_{y}(f(h(y))$ for a family o
We show that numerous distinctive concepts of constructive mathematics arise automatically from an antithesis translation of affine logic into intuitionistic logic via a Chu/Dialectica construction. This includes apartness relations, complemented sub
Interactive theorem provers based on dependent type theory have the flexibility to support both constructive and classical reasoning. Constructive reasoning is supported natively by dependent type theory and classical reasoning is typically supported