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
.