uniform_convergence): more locally uniform limit API (#17092)

Commit

3 years ago

feat(topology/uniform_space/uniform_convergence): more locally uniform limit API (#17092) Add more API around `tendsto_locally_uniformly_on`, needed for #17074.

Author

vbeffara

Parents

4150728b

mathlib 18b61ef3 - feat(topology/uniform_space/uniform_convergence): more locally uniform limit API (#17092)

mathlib
18b61ef3 - feat(topology/uniform_space/uniform_convergence): more locally uniform limit API (#17092)