Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-24 06:44 196c2a8a

View on Github →

feat(topology/separation): a cont. function with a cont. left inverse is a closed embedding (#6329)

Estimated changes

Modified src/topology/continuous_on.lean

modified theorem tendsto_nhds_within_of_tendsto_nhds_of_eventually_within

added theorem tendsto_nhds_within_range

Modified src/topology/local_homeomorph.lean

added theorem local_homeomorph.image_mem_nhds

Modified src/topology/maps.lean

Modified src/topology/separation.lean

added theorem function.left_inverse.closed_embedding

added theorem function.left_inverse.closed_range