feat(topology/uniform_space/uniform_convergence_topology): continuity…

… of [pre,post]composition, and other topological properties (#14534)

We refactor a bit the beginning of the file to define a lower adjoint to the operation sending a filter on `β × β` to the corresponding "filter of uniform convergence" on `(α → β) × (α → β)` (applied to the uniformity on `β`, this gives the uniformity of uniform convergence on `α → β`).

Using this lower adjoint and general facts about Galois connections, we prove (among other things) that, for the uniform structure of uniform convergence : 
- if `f : γ → β` is uniformly continuous, then `(f ∘ ⬝) : (α → γ) → (α → β)` is too
- for any function `g : γ → α`, `(⬝ ∘ g) : (α → β) → (γ → β)` is uniformly continuous
- "swapping the arguments" is an isomorphism of uniform spaces between `α → Π i, δ i` and `Π i, α → δ i`, where the `α → *` types are endowed with the uniform structure of uniform convergence and the `Π i, *` are endowed with the product uniform structure

We then generalize these results to uniform structures of uniform convergence on a set of subsets of `α`.