Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-18 18:52 6a83c7da

View on Github →

feat(topology/compact_open): the family of constant maps collectively form a continuous map (#8721)

Estimated changes