Commit 2020-06-13 11:08 a22b657f

refactor(topology/uniform_space): docstring and notation (#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. 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.