Commit 2021-03-04 08:43 3329ec4e
View on Github →chore(topology/algebra/*): tendsto namespacing (#6528)
Correct a few lemmas which I noticed were namespaced as tendsto.*** rather than filter.tendsto.***, and thus couldn't be used with projection notation.
Also use the projection notation, where now permitted.
Zulip