Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stowei Unicode version

Theorem stowei 27134
 Description: This theorem proves the Stone-Weierstrass theorem for real valued functions: let be a compact topology on , and be the set of real continuous functions on . Assume that is a subalgebra of (closed under addition and multiplication of functions) containing constant functions and discriminating points (if and are distinct points in , then there exists a function in such that h(r) is distinct from h(t) ). Then, for any continuous function and for any positive real , there exists a function in the subalgebra , such that approximates up to ( represents the usual ε value). As a classical example, given any a,b reals, the closed interval could be taken, along with the subalgebra of real polynomials on , and then use this theorem to easily prove that real polynomials are dense in the standard metric space of continuous functions on . The proof and lemmas are written following [BrosowskiDeutsh] p. 89 (through page 92). Some effort is put in avoiding the use of the axiom of choice. The deduction version of this theorem is stoweid 27133: often times it will be better to use stoweid 27133 in other proofs (but this version is probably easier to be read and understood). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stowei.1
stowei.2
stowei.3
stowei.4
stowei.5
stowei.6
stowei.7
stowei.8
stowei.9
stowei.10
stowei.11
Assertion
Ref Expression
stowei
Distinct variable groups:   ,,,   ,,,,,   ,,,   ,,,   ,,,   ,,,   ,,,   ,,,   ,,,   ,
Allowed substitution hints:   (,,,,,)   (,,)   (,,,,)

Proof of Theorem stowei
StepHypRef Expression
1 nfcv 2392 . . 3
2 nftru 1559 . . 3
3 stowei.1 . . 3
4 stowei.2 . . . 4
54a1i 12 . . 3
6 stowei.3 . . 3
7 stowei.4 . . 3
8 stowei.5 . . . 4
98a1i 12 . . 3
10 3simpc 959 . . . 4
11 stowei.6 . . . 4
1210, 11syl 17 . . 3
13 stowei.7 . . . 4
1410, 13syl 17 . . 3
15 stowei.8 . . . 4