Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-28 03:07 f5d63f9f

View on Github →

feat(topology/category/Compactum): forget creates limits (#11690) Will likely be used in LTE.

Estimated changes