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 ?
obvious answer: use funext!!!
This topic was moved here from #math-comp users > Problem of extensionality in filters by Cyril Cohen
Last updated: Feb 05 2023 at 06:28 UTC