[Merged by Bors] - feat(topology/algebra/uniform_convergence): criterion for a vector subspace of α → E to be a TVS for the topology of 𝔖-convergence

[ADedecker]

The main theorem is uniform_convergence_on.has_continuous_smul_induced_of_image_bounded. As explained in the module docstring, one could get rid of requiring 𝔖 to be nonempty and directed, but the easiest way to get that is to wait until we know that replacing 𝔖 by its noncovering bornology (i.e not what bornology currently refers to in mathlib) doesn't change the topology.

This will allow to prove that strong topologies on the space of continuous linear maps between two TVSs are also TVS topologies

---

• depends on: [Merged by Bors] - feat(topology/algebra/filter_basis): add a variant of module_filter_basis.has_continuous_smul when we already have a topological group #14806
• depends on: [Merged by Bors] - feat(topology/algebra/uniform_convergence): maps to a uniform group form a uniform group when equipped with the uniform structure of 𝔖-convergence #14693
• depends on: [Merged by Bors] - feat(topology/uniform_space/uniform_convergence_topology): bases for uniform structures of 𝔖-convergence #14778

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(topology/algebra/filter_basis): add a variant of module_filter_basis.has_continuous_smul when we already have a topological group #14806
• [Merged by Bors] - feat(topology/algebra/uniform_convergence): maps to a uniform group form a uniform group when equipped with the uniform structure of 𝔖-convergence #14693
• [Merged by Bors] - feat(topology/uniform_space/uniform_convergence_topology): bases for uniform structures of 𝔖-convergence #14778
  By Dependent Issues (🤖). Happy coding!

[j-loreaux]

I haven't yet looked carefully, but just a cursory glance to understand. I'll review more thoroughly later.

[j-loreaux]

The statements look ugly. I was able to improve some of them, but the ones with uniform_convergence_on are still rough. It would be nice to figure out how to deal with it, but otherwise the PR looks good to me.

[j-loreaux]

I'm okay with this as is for now. If we eventually decide that this is coming up frequently enough on bare functions and it's a pain to use then we can implement a type synonym, but that can wait for another PR.

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by j-loreaux.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests