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. On Sat, Dec 14, 2019 at 12:49 PM Benoit <[email protected]> wrote: > 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 > > -- > 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 [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/d672fc64-7edf-4b7f-abc8-81d15ce462e4%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/d672fc64-7edf-4b7f-abc8-81d15ce462e4%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSsNUFWqD2_0UAa0taDipFNBtbHifUkVY4V%3D0SUqpyONZw%40mail.gmail.com.
