mathlib
36444798 - feat(topology/is_locally_homeomorph): Add `is_locally_homeomorph_on` (#17114)

Commit
3 years ago
feat(topology/is_locally_homeomorph): Add `is_locally_homeomorph_on` (#17114) This PR adds `is_locally_homeomorph_on` and generalizes `is_covering_map.is_locally_homeomorph` to `is_covering_map_on.is_locally_homeomorph_on`.
Author
Parents
Loading