Yves Bertot (Jun 01 2021 at 07:05): 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 ?
Yves Bertot (Jun 01 2021 at 07:28):obvious answer: use funext!!!
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: Aug 19 2022 at 19:03 UTC