Theorem uniform_convergence_on.has_continuous_smul_submodule_of_image_bounded

chore(topology/uniform_space/uniform_convergence_topology): use type aliases (#17516)

feat(topology/algebra/uniform_convergence): criterion for a vector subspace of `α → E` to be a TVS for the topology of 𝔖-convergence (#14857) …