mathlib

2c4a5161 - chore(topology/metric_space/isometry): a few more lemmas (#5780)

chore(topology/metric_space/isometry): a few more lemmas (#5780) Also reuse more proofs about `inducing` and `quotient_map` in `topology/homeomorph`. Non-bc change: rename `isometric.range_coe` to `isometric.range_eq_univ` to match `equiv.range_eq_univ`.