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.

Author: PatrickMassot