New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(topology/metric_space/isometry): use namespace, add lemmas #15591
Conversation
* Use `namespace isometry`. * Add lemmas like `isometry.preimage_ball`.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
Thanks!
@@ -30,130 +30,137 @@ between pseudoemetric spaces, or equivalently the distance between pseudometric | |||
def isometry [pseudo_emetric_space α] [pseudo_emetric_space β] (f : α → β) : Prop := | |||
∀x1 x2 : α, edist (f x1) (f x2) = edist x1 x2 | |||
|
|||
/-- On pseudometric spaces, a map is an isometry if and only if it preserves nonnegative | |||
distances. -/ | |||
lemma isometry_emetric_iff_nndist [pseudo_metric_space α] [pseudo_metric_space β] {f : α → β} : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The name looks uselessly verbose to me, especially since there is absolutely no emetric
in sight. What about isometry_iff_nndist_eq
(and the next one could be renamed isometry_iff_dist_eq
).
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…unity/mathlib into YK-isometry-lemmas
bors merge |
* Use `namespace isometry`. * Add lemmas like `isometry.preimage_ball`.
Pull request successfully merged into master. Build succeeded: |
* Use `namespace isometry`. * Add lemmas like `isometry.preimage_ball`.
…prover-community#15591) * Use `namespace isometry`. * Add lemmas like `isometry.preimage_ball`.
* Use `namespace isometry`. * Add lemmas like `isometry.preimage_ball`.
namespace isometry
.isometry.preimage_ball
.