-
Notifications
You must be signed in to change notification settings - Fork 299
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] - refactor(topology/uniform_space): docstring and notation #3052
Conversation
@PatrickMassot I changed the PR title. Feel free to change it again. |
I hopefully fixed build. I forgot I modified one statement to a defeq one, but it seems this is not equal enough for some later proof. I also noticed I forgot the |
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.
This looks very nice!
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Thank you very much Rob and Bryan for translating my docstrings into English. I'm sorry I should probably have caught some of these. |
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.
Just some long lines and other style nitpicks.
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
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 🎉
bors merge
The goal of this PR is to make `topology/uniform_space/basic.lean` more accessible. First it introduces the standard notation for relation composition that was inexplicably not used before. I used a non-standard unicode circle here `\ciw` but this is up for discussion as long as it looks like a composition circle. Then I introduced balls as discussed on [this Zulip topic](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/notations.20for.20uniform.20spaces). There could be used more, but at least this should be mostly sufficient for following PRs. And of course I put a huge module docstring. As with `order/filter/basic.lean`, I think we need more mathematical explanations than in the average mathlib file. I also added a bit of content about symmetric entourages but I don't have enough courage to split this off unless someone really insists.
Pull request successfully merged into master. Build succeeded: |
…community#3052) The goal of this PR is to make `topology/uniform_space/basic.lean` more accessible. First it introduces the standard notation for relation composition that was inexplicably not used before. I used a non-standard unicode circle here `\ciw` but this is up for discussion as long as it looks like a composition circle. Then I introduced balls as discussed on [this Zulip topic](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/notations.20for.20uniform.20spaces). There could be used more, but at least this should be mostly sufficient for following PRs. And of course I put a huge module docstring. As with `order/filter/basic.lean`, I think we need more mathematical explanations than in the average mathlib file. I also added a bit of content about symmetric entourages but I don't have enough courage to split this off unless someone really insists.
The goal of this PR is to make
topology/uniform_space/basic.lean
more accessible.First it introduces the standard notation for relation composition that was inexplicably not used before. I used a non-standard unicode circle here
\ciw
but this is up for discussion as long as it looks like a composition circle.Then I introduced balls as discussed on this Zulip topic. There could be used more, but at least this should be mostly sufficient for following PRs.
And of course I put a huge module docstring. As with
order/filter/basic.lean
, I think we need more mathematical explanations than in the average mathlib file.I also added a bit of content about symmetric entourages but I don't have enough courage to split this off unless someone really insists.