Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-22 22:26 bfa24650

View on Github →

refactor(topology/metric_space/lipschitz): redefine for an emetric_space (#2035)

  • refactor(topology/metric_space/lipschitz): redefine for an emetric_space
  • Fix compile
  • Fixes, thanks @sgouzel

Estimated changes