mathlib
ad2e9365 - feat(topology/homeomorph): add `(co)map_cocompact` (#13861)

Commit

3 years ago

feat(topology/homeomorph): add `(co)map_cocompact` (#13861) Also rename `filter.comap_cocompact` to `filter.comap_cocompact_le`.

Author

urkud

Parents