Commit 2022-08-16 04:10 f1e5c657

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