mathlib

a22b657f - refactor(topology/uniform_space): docstring and notation (#3052)

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](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.