Abstract
We present a constructive proof of a Stone-Weierstrass theorem for totally bounded metric spaces (\(\mathrm {\mathbf {SWtbms}}\)) which implies Bishop’s Stone-Weierstrass theorem for compact metric spaces (\(\mathrm {\mathbf {BSWcms}}\)) found in [3]. Our proof has a clear computational content, in contrast to Bishop’s highly technical proof of \(\mathrm {\mathbf {BSWcms}}\) and his hard to motivate concept of a (Bishop-)separating set of uniformly continuous functions. All corollaries of \(\mathrm {\mathbf {BSWcms}}\) in [3] are proved directly by \(\mathrm {\mathbf {SWtbms}}\). We work within Bishop’s informal system of constructive mathematics \(\mathrm {BISH}\).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
Bishop’s original term is that of a separating set, which we avoid here in the presence of the standard classical notion of a separating subset of C(X).
- 2.
The proof goes as follows. By the constructive trichotomy property (see [3], p. 26) either \(a < c\) or \(a \wedge b < a\). In the first case we get immediately what we want to show. In the second case we get that \(b \le a\), since if \(b > a\), we have that \(a = a \wedge b < a\), which is a contradiction. Thus \(a \wedge b = b\) and the hypothesis \(a \wedge b < c\) becomes \(b < c\).
- 3.
By the definition of \(\inf A\) in [3], p. 37, we have that \(\forall _{\epsilon > 0}\exists _{a \in A}(a < \inf A + \epsilon )\), therefore if \(b > \inf A\) and \(\epsilon = b - \inf A > 0\) we get that \(\exists _{a \in A}(a < \inf A + (b - \inf A) = b)\).
- 4.
To show that \(\lnot {(g^{*}(x) > f(x) + \epsilon )}\) we just use the fact that if \(A \subseteq {\mathbb R}, b \in {\mathbb R}\), then \(\sup A> b \rightarrow \exists _{a \in A}(a > b)\). The function \(g^{*}\) is mentioned in [19], where non-constructive properties of the classical \(({\mathbb R}, <)\) are used.
- 5.
The first, in p. 414, is the uniform approximation of a test function f(x, y) on \(G \times G\), where G is a locally compact group, by finite sums of the form \(\sum _{i}f_{i}(x)g_{i}(y)\), and the second, in p. 375, is a density theorem in the theory of Hilbert spaces.
References
Banaschewski, B., Mulvey, C.J.: A constructive proof of the Stone-Weierstrass theorem. J. Pure Appl. Algebra 116, 25–40 (1997)
Bishop, E.: Foundations of Constructive Analysis. McGraw-Hill, New York (1967)
Bishop, E., Bridges, D.: Constructive Analysis. Grundlehren der mathematischen Wissenschaften, vol. 279. Springer, New York (1985)
Bridges, D.S.: Reflections on function spaces. Ann. Pure Appl. Logic 163(12), 101–110 (2012)
Bridges, D.S., Vîţă, L.S.: Techniques of Constructive Analysis: Universitext. Springer, New York (2006)
Bridges, D.S., Richman, F.: Varieties of Constructive Mathematics. Cambridge University Press, New York (1987)
Coquand, T.: A Constructive Analysis of the Stone-Weierstrass Theorem, Manuscript (2001)
Coquand, T.: About Stone’s notion of spectrum. J. Pure Appl. Algebra 197, 141–158 (2005)
Coquand, T., Spitters, B.A.W.: Constructive Gelfand duality for C\(^{*}\)-algebras. Math. Proc. Camb. Philos. Soc. 147(2), 339–344 (2009)
Dugundji, J.: Topology. Brown Publishers Wm. C, Dubuque (1989)
Ishihara, H.: Two subcategories of apartness spaces. Ann. Pure Appl. Logic 163, 132–139 (2013)
Ishihara, H.: Relating Bishop’s function spaces to neighborhood spaces. Ann. Pure Appl. Logic 164, 482–490 (2013)
Ishihara, H., Mines, R., Schuster, P., Vîţă, L.S.: Quasi-apartness and neighborhood spaces. Ann. Pure Appl. Logic 141, 296–306 (2006)
Miculescu, R.: Approximations by Lipschitz functions generated by extensions. Real Anal. Exch. 28(1), 33–40 (2002)
Petrakis, I.: Constructive Topology of Bishop Spaces, Ph.D. Thesis. Ludwig-Maximilians-Universität, München (2015)
Petrakis, I.: Completely regular Bishop spaces. In: Beckmann, A., Mitrana, V., Soskova, M. (eds.) CiE 2015. LNCS, vol. 9136, pp. 302–312. Springer, Heidelberg (2015)
Petrakis, I.: The Urysohn extension theorem for Bishop spaces. In: Artemov, S., et al. (eds.) LFCS 2016. LNCS, vol. 9537, pp. 299–316. Springer, Heidelberg (2016). doi:10.1007/978-3-319-27683-0_21
Tuominen, H.: Analysis in Metric Spaces, Lecture notes (2014)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Petrakis, I. (2016). A Direct Constructive Proof of a Stone-Weierstrass Theorem for Metric Spaces. In: Beckmann, A., Bienvenu, L., Jonoska, N. (eds) Pursuit of the Universal. CiE 2016. Lecture Notes in Computer Science(), vol 9709. Springer, Cham. https://doi.org/10.1007/978-3-319-40189-8_37
Download citation
DOI: https://doi.org/10.1007/978-3-319-40189-8_37
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-40188-1
Online ISBN: 978-3-319-40189-8
eBook Packages: Computer ScienceComputer Science (R0)