Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-24 23:51 5770369f

View on Github →

refactor(topology/metric_space/isometry): remove isometry_inv_fun from isometric (#2051)

  • refactor(topology/metric_space/isometry): remove isometry_inv_fun from isometric; it is automatic
  • Alternative constructor for isometric bijections

Estimated changes