mathlib3
3329ec4e - chore(topology/algebra/*): tendsto namespacing (#6528)

Commit
4 years ago
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](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Search.20for.20all.20declarations.20in.20a.20namespace) Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Author
Parents
Loading