mathlib3
0b1e039b - feat(topology/metric_space/isometry): use namespace, add lemmas (#15591)

Commit
3 years ago
feat(topology/metric_space/isometry): use namespace, add lemmas (#15591) * Use `namespace isometry`. * Add lemmas like `isometry.preimage_ball`.
Author
Parents
Loading