Stone-Weierstrass

[Benoit]

Prompted by the post on the proof of convergence of Fourier series, I looked at other "100" theorems and stumbled on the Stone-Weierstrass theorem.

~stowei has a dv condition on F,t.  This appears to imply that stowei shows only approximability of constant functions.  Similarly, ~stoweid has the hypothesis |- F/_ t F .

Is there a problem, or did I miss something ?

Thanks,

Benoît

[Mario Carneiro]

In stowei, F is a function, an element of ( J Cn K ) where K is the topology on RR. It is being evaluated at t using ( F ` t ), so I would not expect F to have a free t in it. In metamath we use both the implicit representation of functions via open terms F[t], as well as closed terms F which we evaluate at t using function application (in which case F is a set of ordered pairs). So I don't think anything is wrong here.

If you wanted to have a version of stowei with an implicitly defined function, you could replace F with ( t e. T |-> X ) everywhere, and ( F ` t ) with X.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/d672fc64-7edf-4b7f-abc8-81d15ce462e4%40googlegroups.com.

[Benoit]

Indeed, it totally makes sense.
Thanks.
Benoit