Commit 2021-01-17 03:47 2c4a5161
View on Github →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.