Mathlib v3 is deprecated. Go to Mathlib v4

Theorem local_homeomorph.map_nhds_within_eq

Modification history

2021-03-05 21:45

src/topology/local_homeomorph.lean

feat(topology/local_homeomorph): preimage of `closure` and `frontier` (#6547)

Added local_homeomorph.map_nhds_within_eq View on Github →