Description: This theorem proves the Stone-Weierstrass theorem for real-valued
functions: let J be a compact topology on T , and C be the
set of real continuous functions on T . Assume that A is a
subalgebra of C (closed under addition and multiplication of
functions) containing constant functions and discriminating points (if
r and t are distinct points in T , then there exists a
function h in A such that h(r) is distinct from h(t) ). Then,
for any continuous function F and for any positive real E ,
there exists a function f in the subalgebra A , such that f
approximates F up to E ( E represents the usual ε
value). As a classical example, given any a, b reals, the closed
interval T = [ a , b ] could be taken, along with the subalgebra
A of real polynomials on T , and then use this theorem to easily
prove that real polynomials are dense in the standard metric space of
continuous functions on [ a , b ] . 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 : often times it will be better to
use stoweid in other proofs (but this version is probably easier to be
read and understood). (Contributed by Glauco Siliprandi, 20-Apr-2017)
Ref
Expression
Hypotheses
stowei.1
|- K = ( topGen ` ran (,) )
stowei.2
|- J e. Comp
stowei.3
|- T = U. J
stowei.4
|- C = ( J Cn K )
stowei.5
|- A C_ C
stowei.6
|- ( ( f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
stowei.7
|- ( ( f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
stowei.8
|- ( x e. RR -> ( t e. T |-> x ) e. A )
stowei.9
|- ( ( r e. T /\ t e. T /\ r =/= t ) -> E. h e. A ( h ` r ) =/= ( h ` t ) )