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: Dec 05 2023 at 11:01 UTC