mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

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

Open ADedecker opened this issue 3 years ago • 1 comments

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

  • [x] depends on: #14806
  • [x] depends on: #14693
  • [x] depends on: #14778

Open in Gitpod

ADedecker avatar Jun 20 '22 22:06 ADedecker

This PR/issue depends on:

  • ~~leanprover-community/mathlib#14806~~
  • ~~leanprover-community/mathlib#14693~~
  • ~~leanprover-community/mathlib#14778~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Sep 29 '22 21:09 mathlib-dependent-issues-bot

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

j-loreaux avatar Oct 19 '22 00:10 j-loreaux

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

github-actions[bot] avatar Oct 19 '22 00:10 github-actions[bot]

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Oct 19 '22 07:10 bors[bot]