Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-18 18:52 3ac609b9

View on Github →

chore(topology/continuous_function/compact): relax typeclass assumptions for metric space structure on C(X, Y) (#8717)

Estimated changes