mathlib

036fc996 - feat(topology/uniform_space/uniform_convergence): add `tendsto_uniformly_iff_seq_tendsto_uniformly` (#13128)

feat(topology/uniform_space/uniform_convergence): add `tendsto_uniformly_iff_seq_tendsto_uniformly` (#13128) For countably generated filters, uniform convergence is equivalent to uniform convergence of sub-sequences. Co-authored-by: RemyDegenne <Remydegenne@gmail.com>