Commit 2022-09-29 19:48 71e28e0c

feat(topology/uniform_space/uniform_convergence_topology): bases for uniform structures of 𝔖-convergence (#14778) By definition, the sets S(V) := {(f, g) | ∀ x, (f x, g x) ∈ V} for V∈𝓤 β form a basis for the uniformity of uniform convergence on α → β. We extend this result in the two following ways :

• we show that it suffices to consider only the sets V in a basis of 𝓤 β instead of all the entourages
• we deduce a similar result for the uniformity of 𝔖-convergence for a directed 𝔖 : in that case, a basis is given by the sets S'(A,V) := {(f, g) | ∀ x ∈ A, (f x, g x) ∈ V} for A ∈𝔖 and V in a basis of 𝓤 β