Stream: math-comp analysis

Topic: Problem of extensionality in filters

view this post on Zulip Yves Bertot (Jun 01 2021 at 07:05):

Now I know that w *+ 2 @[w --> x] converges to the sensible value, but I need to prove 2%:R * w @[w -->x] converges to the same value. How do I do that ?

view this post on Zulip Yves Bertot (Jun 01 2021 at 07:28):

obvious answer: use funext!!!

view this post on Zulip Notification Bot (Jun 01 2021 at 10:08):

This topic was moved here from #math-comp users > Problem of extensionality in filters by Cyril Cohen

Last updated: Dec 05 2023 at 11:01 UTC