mathlib

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

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 Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>