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] - doc(MetricSpace/Hausdorff): style fixes in doc comments #9856
Conversation
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.
Thanks! Although in the future I wouldn't worry too much about the full stops.
bors d+
theorem infDist_le_hausdorffDist_of_mem (hx : x ∈ s) (fin : hausdorffEdist s t ≠ ⊤) : | ||
infDist x t ≤ hausdorffDist s t := | ||
toReal_mono fin (infEdist_le_hausdorffEdist_of_mem hx) | ||
#align metric.inf_dist_le_Hausdorff_dist_of_mem Metric.infDist_le_hausdorffDist_of_mem | ||
|
||
/-- If the Hausdorff distance is `< r`, then any point in one of the sets is at distance | ||
`< r` of a point in the other set -/ | ||
/-- If the Hausdorff distance is `< r`, any point in one of the sets is at distance |
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.
/-- If the Hausdorff distance is `< r`, any point in one of the sets is at distance | |
/-- If the Hausdorff distance is `< r`, then any point in one of the sets is at distance |
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.
As I understand it, correct grammar doesn't require the "then". Hence, I'd like to leave this as-is.
@@ -806,8 +806,8 @@ theorem exists_dist_lt_of_hausdorffDist_lt {r : ℝ} (h : x ∈ s) (H : hausdorf | |||
exact ⟨y, hy, yr⟩ | |||
#align metric.exists_dist_lt_of_Hausdorff_dist_lt Metric.exists_dist_lt_of_hausdorffDist_lt | |||
|
|||
/-- If the Hausdorff distance is `< r`, then any point in one of the sets is at distance | |||
`< r` of a point in the other set -/ | |||
/-- If the Hausdorff distance is `< r`, any point in one of the sets is at distance |
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.
/-- If the Hausdorff distance is `< r`, any point in one of the sets is at distance | |
/-- If the Hausdorff distance is `< r`, then any point in one of the sets is at distance |
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.
Same here
✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with |
Thanks for the fast review. Indeed, this is not a PR I would create out of the blue - but as I was in the area already, that felt appropriate. |
* End sentences with a full stop (per the style guide). * Fix grammar in a few trivial cases. * Use "triangle inequality", not "triangular inequality".
Pull request successfully merged into master. Build succeeded: |
By-product of creating module docstrings in #9809.
Reviewing this should not require deeply understanding the mathematics.
All the docstrings "is continuous in point" still read strangely to me (I'd rather write "for a fixed set s" instead); I didn't modify them.