Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-05 23:45 e7189651

View on Github →

feat(topology/uniform_space/compact_convergence): when the domain is compact, compact convergence is just uniform convergence (#11262)

Estimated changes