mathlib3

e109c8f6 - feat(topology): basis for `𝓤 C(α, β)` and convergence of a series of `f : C(α, β)` (#11229)

feat(topology): basis for `𝓤 C(α, β)` and convergence of a series of `f : C(α, β)` (#11229) * add `filter.has_basis.compact_convergence_uniformity`; * add a few facts about `compacts X`; * add `summable_of_locally_summable_norm`. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>