mathlib
dbddee69 - feat(topology/continuous_on): add `set.left_inv_on.map_nhds_within_eq` (#6529)

Commit

5 years ago

feat(topology/continuous_on): add `set.left_inv_on.map_nhds_within_eq` (#6529) Also add some trivial lemmas to `data/set/function` and `order/filter/basic`.

Author

urkud

Parents

0690d970

mathlib dbddee69 - feat(topology/continuous_on): add `set.left_inv_on.map_nhds_within_eq` (#6529)

mathlib
dbddee69 - feat(topology/continuous_on): add `set.left_inv_on.map_nhds_within_eq` (#6529)