Commit 2021-08-17 10:49 4df3fb9e

View on Github →

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.

Estimated changes

Modified src/topology/maps.lean

added theorem closed_embedding.tendsto_nhds_iff

added theorem open_embedding.tendsto_nhds_iff

Modified src/topology/metric_space/isometry.lean

modified theorem isometry.closed_embedding

added theorem isometry.tendsto_nhds_iff

modified theorem isometry.uniform_embedding