feat(topology/uniform_space/uniform_convergence_topology): continuity of [pre,post]composition, and other topological properties

[ADedecker]

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 α.

---

• [x] depends on: #14537
• [x] depends on: #14561
• [x] depends on: #14678

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#14537~~
• ~~leanprover-community/mathlib#14561~~
• ~~leanprover-community/mathlib#14678~~ By Dependent Issues (🤖). Happy coding!

[bors[bot]]

:v: ADedecker can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ADedecker]

bors r+

[bors[bot]]

Build failed (retrying...):

• Build mathlib

[bors[bot]]

Build failed (retrying...):

• Build mathlib

[bors[bot]]

Build failed (retrying...):

• Build mathlib
• Lint mathlib
• Run tests

[ADedecker]

bors cancel

[ADedecker]

bors r+

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests