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