mathlib3

71e28e0c - feat(topology/uniform_space/uniform_convergence_topology): bases for uniform structures of 𝔖-convergence (#14778)

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 `𝓤 β`