We define isometries, i.e., maps between emetric spaces that preserve the edistance (on metric spaces, these are exactly the maps that preserve distances), and prove their basic properties. We also introduce isometric bijections.
- toFun : α → β
- invFun : β → α
- left_inv : Function.LeftInverse s.invFun s.toFun
- right_inv : Function.RightInverse s.invFun s.toFun
- isometry_toFun : Isometry s.toFun
β are isometric if there is an isometric bijection between them.