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: Aug 19 2022 at 19:03 UTC