Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-02 13:45 ad2e9365

View on Github →

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

Estimated changes

Modified src/number_theory/modular.lean

Modified src/topology/homeomorph.lean

added theorem homeomorph.comap_cocompact

added theorem homeomorph.map_cocompact

Modified src/topology/subset_properties.lean

deleted theorem filter.comap_cocompact

added theorem filter.comap_cocompact_le