mathlib

4df3fb9e - chore(topology/maps): add tendsto_nhds_iff lemmas (#8693)

chore(topology/maps): add tendsto_nhds_iff lemmas (#8693) This adds lemmas of the form `something.tendsto_nhds_iff` to ease use. I also had to get lemmas out of a section because `α` was duplicated and that caused typechecking problems.