Commit 2022-07-22 18:27 0b1e039b
View on Github →feat(topology/metric_space/isometry): use namespace, add lemmas (#15591)
- Use
namespace isometry
. - Add lemmas like
isometry.preimage_ball
.
feat(topology/metric_space/isometry): use namespace, add lemmas (#15591)
namespace isometry
.isometry.preimage_ball
.