mathlib
mathlib copied to clipboard
leanprover-community
feat(topology/uniform_space/uniform_convergence_topology): bases for uniform structures of š-convergence
By definition, the sets S(V) := {(f, g) | ā x, (f x, g x) ā V} for Vāš¤ Ī² form a basis for the uniformity of uniform convergence on Ī± ā Ī². We extend this result in the two following ways :
- we show that it suffices to consider only the sets
Vin a basis ofš¤ Ī²instead of all the entourages - we deduce a similar result for the uniformity of š-convergence for a directed š : in that case, a basis is given by the sets
S'(A,V) := {(f, g) | ā x ā A, (f x, g x) ā V}forA āšandVin a basis ofš¤ Ī²
- [x] depends on: #14775
- [ ] depends on: #14534
This PR/issue depends on:
- ~~leanprover-community/mathlib#14775~~
- ~~leanprover-community/mathlib#14534~~ By Dependent Issues (š¤). Happy coding!
:v: ADedecker can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.
![bors[bot] avatar](https://avatars.githubusercontent.com/in/1847?v=4 "Published by a pub.dev verified publisher"){kind=small}
Yes I've thought about making a type alias before (it's written in the TODO section of the module docstring with a question mark), but I'm not sure there will be enough uses of this to justify making a type alias. But if you think we should do it I'm happy to take care of that in a future PR.
I don't know how often these concepts are used. Feel free to leave it like this if you think it's rarely used.
I'll ask on Zulip this evening. I would say it's not super annoying, but maybe I just got used to it.
Pull request successfully merged into master.
Build succeeded: