Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-17 11:01 85f36400

View on Github →

feat(topology/instances/ennreal): {f | lipschitz_with K f} is a closed set (#9766)

Estimated changes